Theorem caucvglem5 7097

Description: Lemma for caucvg 7099.

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
caucvglem5	|- ((x e. RR /\ w e. NN) -> (A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < (x / 2)) -> -u(x / 2) <_ (sup(S, RR, < ) - (F` w))))

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

Proof of Theorem caucvglem5

Step	Hyp	Ref	Expression
1		nnltp1let 5902	. . . . . . . . . . 11 |- ((w e. NN /\ y e. NN) -> (w < y <-> (w + 1) <_ y))
2	1	biimprd 154	. . . . . . . . . 10 |- ((w e. NN /\ y e. NN) -> ((w + 1) <_ y -> w < y))
3	2	adantll 392	. . . . . . . . 9 |- ((((x / 2) e. RR /\ w e. NN) /\ y e. NN) -> ((w + 1) <_ y -> w < y))
4		absltt 6817	. . . . . . . . . . . . . . . . 17 |- ((((F` y) - (F` w)) e. RR /\ (x / 2) e. RR) -> ((abs` ((F` y) - (F` w))) < (x / 2) <-> (-u(x / 2) < ((F` y) - (F` w)) /\ ((F` y) - (F` w)) < (x / 2))))
5		pm3.26 319	. . . . . . . . . . . . . . . . 17 |- ((-u(x / 2) < ((F` y) - (F` w)) /\ ((F` y) - (F` w)) < (x / 2)) -> -u(x / 2) < ((F` y) - (F` w)))
6	4, 5	syl6bi 214	. . . . . . . . . . . . . . . 16 |- ((((F` y) - (F` w)) e. RR /\ (x / 2) e. RR) -> ((abs` ((F` y) - (F` w))) < (x / 2) -> -u(x / 2) < ((F` y) - (F` w))))
7		resubclt 5410	. . . . . . . . . . . . . . . 16 |- (((F` y) e. RR /\ (F` w) e. RR) -> ((F` y) - (F` w)) e. RR)
8	6, 7	sylan 448	. . . . . . . . . . . . . . 15 |- ((((F` y) e. RR /\ (F` w) e. RR) /\ (x / 2) e. RR) -> ((abs` ((F` y) - (F` w))) < (x / 2) -> -u(x / 2) < ((F` y) - (F` w))))
9	8	3impa 826	. . . . . . . . . . . . . 14 |- (((F` y) e. RR /\ (F` w) e. RR /\ (x / 2) e. RR) -> ((abs` ((F` y) - (F` w))) < (x / 2) -> -u(x / 2) < ((F` y) - (F` w))))
10	9	3com13 836	. . . . . . . . . . . . 13 |- (((x / 2) e. RR /\ (F` w) e. RR /\ (F` y) e. RR) -> ((abs` ((F` y) - (F` w))) < (x / 2) -> -u(x / 2) < ((F` y) - (F` w))))
11		ltaddsubt 5605	. . . . . . . . . . . . . 14 |- ((-u(x / 2) e. RR /\ (F` w) e. RR /\ (F` y) e. RR) -> ((-u(x / 2) + (F` w)) < (F` y) <-> -u(x / 2) < ((F` y) - (F` w))))
12		renegclt 5409	. . . . . . . . . . . . . 14 |- ((x / 2) e. RR -> -u(x / 2) e. RR)
13	11, 12	syl3an1 857	. . . . . . . . . . . . 13 |- (((x / 2) e. RR /\ (F` w) e. RR /\ (F` y) e. RR) -> ((-u(x / 2) + (F` w)) < (F` y) <-> -u(x / 2) < ((F` y) - (F` w))))
14	10, 13	sylibrd 204	. . . . . . . . . . . 12 |- (((x / 2) e. RR /\ (F` w) e. RR /\ (F` y) e. RR) -> ((abs` ((F` y) - (F` w))) < (x / 2) -> (-u(x / 2) + (F` w)) < (F` y)))
15		caucvg.1	. . . . . . . . . . . . 13 |- F:NN-->RR
16	15	ffvelrni 3800	. . . . . . . . . . . 12 |- (w e. NN -> (F` w) e. RR)
17	14, 16	syl3an2 858	. . . . . . . . . . 11 |- (((x / 2) e. RR /\ w e. NN /\ (F` y) e. RR) -> ((abs` ((F` y) - (F` w))) < (x / 2) -> (-u(x / 2) + (F` w)) < (F` y)))
18	15	ffvelrni 3800	. . . . . . . . . . 11 |- (y e. NN -> (F` y) e. RR)
19	17, 18	syl3an3 859	. . . . . . . . . 10 |- (((x / 2) e. RR /\ w e. NN /\ y e. NN) -> ((abs` ((F` y) - (F` w))) < (x / 2) -> (-u(x / 2) + (F` w)) < (F` y)))
20	19	3expa 831	. . . . . . . . 9 |- ((((x / 2) e. RR /\ w e. NN) /\ y e. NN) -> ((abs` ((F` y) - (F` w))) < (x / 2) -> (-u(x / 2) + (F` w)) < (F` y)))
21	3, 20	imim12d 29	. . . . . . . 8 |- ((((x / 2) e. RR /\ w e. NN) /\ y e. NN) -> ((w < y -> (abs` ((F` y) - (F` w))) < (x / 2)) -> ((w + 1) <_ y -> (-u(x / 2) + (F` w)) < (F` y))))
22	21	r19.20dva 1701	. . . . . . 7 |- (((x / 2) e. RR /\ w e. NN) -> (A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < (x / 2)) -> A.y e. NN ((w + 1) <_ y -> (-u(x / 2) + (F` w)) < (F` y))))
23		peano2nn 5883	. . . . . . . 8 |- (w e. NN -> (w + 1) e. NN)
24	23	adantl 388	. . . . . . 7 |- (((x / 2) e. RR /\ w e. NN) -> (w + 1) e. NN)
25	22, 24	jctild 599	. . . . . 6 |- (((x / 2) e. RR /\ w e. NN) -> (A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < (x / 2)) -> ((w + 1) e. NN /\ A.y e. NN ((w + 1) <_ y -> (-u(x / 2) + (F` w)) < (F` y)))))
26		breq1 2612	. . . . . . . . 9 |- (v = (w + 1) -> (v <_ y <-> (w + 1) <_ y))
27	26	imbi1d 611	. . . . . . . 8 |- (v = (w + 1) -> ((v <_ y -> (-u(x / 2) + (F` w)) < (F` y)) <-> ((w + 1) <_ y -> (-u(x / 2) + (F` w)) < (F` y))))
28	27	ralbidv 1655	. . . . . . 7 |- (v = (w + 1) -> (A.y e. NN (v <_ y -> (-u(x / 2) + (F` w)) < (F` y)) <-> A.y e. NN ((w + 1) <_ y -> (-u(x / 2) + (F` w)) < (F` y))))
29	28	rcla4ev 1868	. . . . . 6 |- (((w + 1) e. NN /\ A.y e. NN ((w + 1) <_ y -> (-u(x / 2) + (F` w)) < (F` y))) -> E.v e. NN A.y e. NN (v <_ y -> (-u(x / 2) + (F` w)) < (F` y)))
30	25, 29	syl6 22	. . . . 5 |- (((x / 2) e. RR /\ w e. NN) -> (A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < (x / 2)) -> E.v e. NN A.y e. NN (v <_ y -> (-u(x / 2) + (F` w)) < (F` y))))
31		axaddrcl 5244	. . . . . 6 |- ((-u(x / 2) e. RR /\ (F` w) e. RR) -> (-u(x / 2) + (F` w)) e. RR)
32	31, 12, 16	syl2an 454	. . . . 5 |- (((x / 2) e. RR /\ w e. NN) -> (-u(x / 2) + (F` w)) e. RR)
33	30, 32	jctild 599	. . . 4 |- (((x / 2) e. RR /\ w e. NN) -> (A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < (x / 2)) -> ((-u(x / 2) + (F` w)) e. RR /\ E.v e. NN A.y e. NN (v <_ y -> (-u(x / 2) + (F` w)) < (F` y)))))
34		caucvg.2	. . . . . 6 |- A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < z))
35		caucvg.3	. . . . . 6 |- S = {u e. RR | E.v e. NN A.y e. NN (v <_ y ->