Theorem caucvglem2 8814

Description: Lemma for caucvgi 8819. S is a nonempty bounded subset of RR.

Hypotheses

Ref	Expression
caucvg.1	|- F:NN-->RR
caucvg.2	|- A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < z))
caucvg.3	|- S = {u e. RR | E.v e. NN A.y e. NN (v <_ y -> u < (F` y))}

Assertion

Ref	Expression
caucvglem2	|- (S C_ RR /\ S =/= (/) /\ E.x e. RR A.f e. S f <_ x)

Distinct variable groups:   x,y,z,w,u,v,f,F   x,S,z,w,f

Proof of Theorem caucvglem2

Step	Hyp	Ref	Expression
1		caucvg.3	. . 3 |- S = {u e. RR | E.v e. NN A.y e. NN (v <_ y -> u < (F` y))}
2		ssrab2 2917	. . 3 |- {u e. RR | E.v e. NN A.y e. NN (v <_ y -> u < (F` y))} C_ RR
3	1, 2	eqsstri 2874	. 2 |- S C_ RR
4		caucvg.1	. . . . 5 |- F:NN-->RR
5		axresscn 6786	. . . . 5 |- RR C_ CC
6		fss 4667	. . . . 5 |- ((F:NN-->RR /\ RR C_ CC) -> F:NN-->CC)
7	4, 5, 6	mp2an 681	. . . 4 |- F:NN-->CC
8		caucvg.2	. . . 4 |- A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < z))
9	7, 8	caubndi 8563	. . 3 |- E.x e. RR A.y e. NN (abs` (F` y)) < x
10	4	ffvelrni 4878	. . . . . . . . . . . . 13 |- (y e. NN -> (F` y) e. RR)
11		abslt 8516	. . . . . . . . . . . . . 14 |- (((F` y) e. RR /\ x e. RR) -> ((abs` (F` y)) < x <-> (-ux < (F` y) /\ (F` y) < x)))
12		simpl 437	. . . . . . . . . . . . . 14 |- ((-ux < (F` y) /\ (F` y) < x) -> -ux < (F` y))
13	11, 12	syl6bi 263	. . . . . . . . . . . . 13 |- (((F` y) e. RR /\ x e. RR) -> ((abs` (F` y)) < x -> -ux < (F` y)))
14	10, 13	sylan 597	. . . . . . . . . . . 12 |- ((y e. NN /\ x e. RR) -> ((abs` (F` y)) < x -> -ux < (F` y)))
15	14	ancoms 416	. . . . . . . . . . 11 |- ((x e. RR /\ y e. NN) -> ((abs` (F` y)) < x -> -ux < (F` y)))
16	15	a1dd 94	. . . . . . . . . 10 |- ((x e. RR /\ y e. NN) -> ((abs` (F` y)) < x -> (1 <_ y -> -ux < (F` y))))
17	16	ralimdva 2421	. . . . . . . . 9 |- (x e. RR -> (A.y e. NN (abs` (F` y)) < x -> A.y e. NN (1 <_ y -> -ux < (F` y))))
18		1nn 7450	. . . . . . . . . 10 |- 1 e. NN
19	18	a1i 8	. . . . . . . . 9 |- (x e. RR -> 1 e. NN)
20	17, 19	jctild 507	. . . . . . . 8 |- (x e. RR -> (A.y e. NN (abs` (F` y)) < x -> (1 e. NN /\ A.y e. NN (1 <_ y -> -ux < (F` y)))))
21		breq1 3510	. . . . . . . . . . 11 |- (v = 1 -> (v <_ y <-> 1 <_ y))
22	21	imbi1d 748	. . . . . . . . . 10 |- (v = 1 -> ((v <_ y -> -ux < (F` y)) <-> (1 <_ y -> -ux < (F` y))))
23	22	ralbidv 2373	. . . . . . . . 9 |- (v = 1 -> (A.y e. NN (v <_ y -> -ux < (F` y)) <-> A.y e. NN (1 <_ y -> -ux < (F` y))))
24	23	rcla4ev 2620	. . . . . . . 8 |- ((1 e. NN /\ A.y e. NN (1 <_ y -> -ux < (F` y))) -> E.v e. NN A.y e. NN (v <_ y -> -ux < (F` y)))
25	20, 24	syl6 42	. . . . . . 7 |- (x e. RR -> (A.y e. NN (abs` (F` y)) < x -> E.v e. NN A.y e. NN (v <_ y -> -ux < (F` y))))
26		renegcl 7077	. . . . . . 7 |- (x e. RR -> -ux e. RR)
27	25, 26	jctild 507	. . . . . 6 |- (x e. RR -> (A.y e. NN (abs` (F` y)) < x -> (-ux e. RR /\ E.v e. NN A.y e. NN (v <_ y -> -ux < (F` y)))))
28	4, 8, 1	caucvglem1 8813	. . . . . 6 |- (-ux e. S <-> (-ux e. RR /\ E.v e. NN A.y e. NN (v <_ y -> -ux < (F` y))))
29	27, 28	syl6ibr 262	. . . . 5 |- (x e. RR -> (A.y e. NN (abs` (F` y)) < x -> -ux e. S))
30		ne0i 3088	. . . . 5 |- (-ux e. S -> S =/= (/))
31	29, 30	syl6 42	. . . 4 |- (x e. RR -> (A.y e. NN (abs` (F` y)) < x -> S =/= (/)))
32	31	r19.23aiv 2459	. . 3 |- (E.x e. RR A.y e. NN (abs` (F` y)) < x -> S =/= (/))
33	9, 32	ax-mp 7	. 2 |- S =/= (/)
34	4, 8, 1	caucvglem1 8813	. . . . . . 7 |- (f e. S <-> (f e. RR /\ E.v e. NN A.y e. NN (v <_ y -> f < (F` y))))
35		nnre 7445	. . . . . . . . . . . . . . . . 17 |- (v e. NN -> v e. RR)
36		leid 6890	. . . . . . . . . . . . . . . . 17 |- (v e. RR -> v <_ v)
37	35, 36	syl 13	. . . . . . . . . . . . . . . 16 |- (v e. NN -> v <_ v)
38		breq2 3511	. . . . . . . . . . . . . . . . . 18 |- (y = v -> (v <_ y <-> v <_ v))
39		fveq2 4765	. . . . . . . . . . . . . . . . . . 19 |- (y = v -> (F` y) = (F` v))
40	39	breq2d 3519	. . . . . . . . . . . . . . . . . 18 |- (y = v -> (f < (F` y) <-> f < (F` v)))
41	38, 40	imbi12d 761	. . . . . . . . . . . . . . . . 17 |- (y = v -> ((v <_ y -> f < (F` y)) <-> (v <_ v -> f < (F` v))))
42	41	rcla4v 2616	. . . . . . . . . . . . . . . 16 |- (v e. NN -> (A.y e. NN (v <_ y -> f < (F` y)) -> (v <_ v -> f < (F` v))))
43	37, 42	mpid 21	. . . . . . . . . . . . . . 15 |- (v e. NN -> (A.y e. NN (v <_ y -> f < (F` y)) -> f < (F` v)))
44	43	adantr 447	. . . . . . . . . . . . . 14 |- ((v e. NN /\ x e. RR) -> (A.y e. NN (v <_ y -> f < (F` y)) -> f < (F` v)))
45	39	fveq2d 4769	. . . . . . . . . . . . . . . . . 18 |- (y = v -> (abs` (F` y)) = (abs` (F` v)))
46	45	breq1d 3517	. . . . . . . . . . . . . . . . 17 |- (y = v -> ((abs` (F` y)) < x <-> (abs` (F` v)) < x))
47	46	rcla4v 2616	. . . . . . . . . . . . . . . 16 |- (v e. NN -> (A.y e. NN (abs` (F` y)) < x -> (abs` (F` v)) < x))
48	47	adantr 447	. . . . . . . . . . . . . . 15 |- ((v e. NN /\ x e. RR) -> (A.y e. NN (abs` (F` y)) < x -> (abs` (F` v)) < x))
49	4	ffvelrni 4878	. . . . . . . . . . . . . . . . 17 |- (v e. NN -> (F` v) e. RR)
50		abslt 8516	. . . . . . . . . . . . . . . . 17 |- (((F` v) e. RR /\ x e. RR) -> ((abs` (F` v)) < x <-> (-ux < (F` v) /\ (F` v) < x)))
51	49, 50	sylan 597	. . . . . . . . . . . . . . . 16 |- ((v e. NN /\ x e. RR) -> ((abs` (F` v)) < x <-> (-ux < (F` v) /\ (F` v) < x)))
52		simpr 442	. . . . . . . . . . . . . . . 16 |- ((-ux < (F` v) /\ (F` v) < x) -> (F` v) < x)
53	51, 52	syl6bi 263	. . . . . . . . . . . . . . 15 |- ((v e. NN /\ x e. RR) -> ((abs` (F` v)) < x -> (F` v) < x))
54	48, 53	syld 33	. . . . . . . . . . . . . 14 |- ((v e. NN /\ x e. RR) -> (A.y e. NN (abs` (F` y)) < x -> (F` v) < x))
55	44, 54	anim12d 533	. . . . . . . . . . . . 13 |- ((v e. NN /\ x e. RR) -> ((A.y e. NN (v <_ y -> f < (F` y)) /\ A.y e. NN (abs` (F` y)) < x) -> (f < (F` v) /\ (F` v) < x)))
56	55	3adant1 1138	. . . . . . . . . . . 12 |- ((f e. RR /\ v e. NN /\ x e. RR) -> ((A.y e. NN (v <_ y -> f < (F` y)) /\ A.y e. NN (abs` (F` y)) < x) -> (f < (F` v) /\ (F` v) < x)))
57		axlttrn 6863	. . . . . . . . . . . . 13 |- ((f e. RR /\ (F` v) e. RR /\ x e. RR) -> ((f < (F` v) /\ (F` v) < x) -> f < x))
58	49, 57	syl3an2 1383	. . . . . . . . . . . 12 |- ((f e. RR /\ v e. NN /\ x e. RR) -> ((f < (F` v) /\ (F` v) < x) -> f < x))
59		ltle 6879	. . . . . . . . . . . . 13 |- ((f e. RR /\ x e. RR) -> (f < x -> f <_ x))
60	59	3adant2 1139	. . . . . . . . . . . 12 |- ((f e. RR /\ v e. NN /\ x e. RR) -> (f < x -> f <_ x))
61	56, 58, 60	3syld 59	. . . . . . . . . . 11 |- ((f e. RR /\ v e. NN /\ x e. RR) -> ((A.y e. NN (v <_ y -> f < (F` y)) /\ A.y e. NN (abs` (F` y)) < x) -> f <_ x))
62	61	exp5o 1336	. . . . . . . . . 10 |- (f e. RR -> (v e. NN -> (x e. RR -> (A.y e. NN (v <_ y -> f < (F` y)) -> (A.y e. NN (abs` (F` y)) < x -> f <_ x)))))
63	62	com34 75	. . . . . . . . 9 |- (f e. RR -> (v e. NN -> (A.y e. NN (v <_ y -> f < (F` y)) -> (x e. RR -> (A.y e. NN (abs` (F` y)) < x -> f <_ x)))))
64	63	r19.23adv 2463	. . . . . . . 8 |- (f e. RR -> (E.v e. NN A.y e. NN (v <_ y -> f < (F` y)) -> (x e. RR -> (A.y e. NN (abs` (F` y)) < x -> f <_ x))))
65	64	imp 393	. . . . . . 7 |- ((f e. RR /\ E.v e. NN A.y e. NN (v <_ y -> f < (F` y))) -> (x e. RR -> (A.y e. NN (abs` (F` y)) < x -> f <_ x)))
66	34, 65	sylbi 225	. . . . . 6 |- (f e. S -> (x e. RR -> (A.y e. NN (abs` (F` y)) < x -> f <_ x)))
67	66	com3l 68	. . . . 5 |- (x e. RR -> (A.y e. NN (abs` (F` y)) < x -> (f e. S -> f <_ x)))
68	67	r19.21adv 2431	. . . 4 |- (x e. RR -> (A.y e. NN (abs` (F` y)) < x -> A.f e. S f <_ x))
69	68	reximia 2446	. . 3 |- (E.x e. RR A.y e. NN (abs` (F` y)) < x -> E.x e. RR A.f e. S f <_ x)
70	9, 69	ax-mp 7	. 2 |- E.x e. RR A.f e. S f <_ x
71	3, 33, 70	3pm3.2i 1298	1 |- (S C_ RR /\ S =/= (/) /\ E.x e. RR A.f e. S f <_ x)

Syntax hints:   -> wi 3   <-> wb 219   /\ wa 337   /\ w3a 1102   = wceq 1586   e. wcel 1588   =/= wne 2266  A.wral 2355  E.wrex 2356  {crab 2358   C_ wss 2827  (/)c0 3082   class class class wbr 3507  -->wf 4127  ` cfv 4131  (class class class)co 4981  CCcc 6750  RRcr 6751  0cc0 6752  1c1 6753   <_ cle 6841   < clt 6845   - cmin 6989  -ucneg 6990  NNcn 6992  abscabs 8384

This theorem is referenced by:  caucvglem3 8815  caucvglem4 8816  caucvglem5 8817

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929  ax-inf2 5964

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-nel 2269  df-ral 2359  df-rex 2360  df-reu 2361  df-rab 2362  df-v 2540  df-sbc 2700  df-csb 2774  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-if 3181  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-int 3401  df-iun 3438  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-id 3747  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-lim 3816  df-suc 3817  df-om 4086  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-f1 4144  df-fo 4145  df-f1o 4146  df-fv 4147  df-opr 4983  df-oprab 4984  df-mpt 5099  df-1st 5126  df-2nd 5127  df-iota 5219  df-rdg 5304  df-1o 5344  df-oadd 5346  df-omul 5347  df-er 5479  df-ec 5481  df-qs 5484  df-en 5588  df-dom 5589  df-sdom 5590  df-undef 5725  df-riota 5729  df-sup 5888  df-ni 6518  df-pli 6519  df-mi 6520  df-lti 6521  df-plpq 6553  df-mpq 6554  df-enq 6555  df-nq 6556  df-plq 6557  df-mq 6558  df-rq 6559  df-ltq 6560  df-1q 6561  df-np 6604  df-1p 6605  df-plp 6606  df-mp 6607  df-ltp 6608  df-plpr 6682  df-mpr 6683  df-enr 6684  df-nr 6685  df-plr 6686  df-mr 6687  df-ltr 6688  df-0r 6689  df-1r 6690  df-m1r 6691  df-c 6758  df-0 6759  df-1 6760  df-i 6761  df-r 6762  df-plus 6763  df-mul 6764  df-lt 6765  df-pnf 6846  df-mnf 6847  df-xr 6848  df-ltxr 6849  df-le 6850  df-sub 7009  df-neg 7011  df-div 7223  df-n 7441  df-2 7487  df-n0 7649  df-z 7686  df-seq1 8094  df-exp 8196  df-sqr 8304  df-re 8385  df-im 8386  df-cj 8387  df-abs 8388

Copyright terms: Public domain