Theorem caucvglem6 7162

Description: Lemma for caucvg 7163.

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

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

Proof of Theorem caucvglem6

Step	Hyp	Ref	Expression
1		breq2 2628	. . . . . . . . . . . . 13 |- (y = (w + v) -> ((w + v) <_ y <-> (w + v) <_ (w + v)))
2	1	rcla4ev 1880	. . . . . . . . . . . 12 |- (((w + v) e. NN /\ (w + v) <_ (w + v)) -> E.y e. NN (w + v) <_ y)
3		nnaddclt 5942	. . . . . . . . . . . 12 |- ((w e. NN /\ v e. NN) -> (w + v) e. NN)
4		nnret 5931	. . . . . . . . . . . . . 14 |- ((w + v) e. NN -> (w + v) e. RR)
5	3, 4	syl 10	. . . . . . . . . . . . 13 |- ((w e. NN /\ v e. NN) -> (w + v) e. RR)
6		leidt 5543	. . . . . . . . . . . . 13 |- ((w + v) e. RR -> (w + v) <_ (w + v))
7	5, 6	syl 10	. . . . . . . . . . . 12 |- ((w e. NN /\ v e. NN) -> (w + v) <_ (w + v))
8	2, 3, 7	sylanc 473	. . . . . . . . . . 11 |- ((w e. NN /\ v e. NN) -> E.y e. NN (w + v) <_ y)
9	8	adantll 394	. . . . . . . . . 10 |- ((((x / 2) e. RR /\ w e. NN) /\ v e. NN) -> E.y e. NN (w + v) <_ y)
10		ax-17 973	. . . . . . . . . . . 12 |- (((x / 2) e. RR /\ (w e. NN /\ v e. NN)) -> A.y((x / 2) e. RR /\ (w e. NN /\ v e. NN)))
11		hbra1 1690	. . . . . . . . . . . . 13 |- (A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < (x / 2)) -> A.yA.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < (x / 2)))
12		hbra1 1690	. . . . . . . . . . . . . 14 |- (A.y e. NN (v <_ y -> ((x / 2) + (F` w)) < (F` y)) -> A.yA.y e. NN (v <_ y -> ((x / 2) + (F` w)) < (F` y)))
13	12	hbn 1006	. . . . . . . . . . . . 13 |- (-. A.y e. NN (v <_ y -> ((x / 2) + (F` w)) < (F` y)) -> A.y -. A.y e. NN (v <_ y -> ((x / 2) + (F` w)) < (F` y)))
14	11, 13	hbim 1009	. . . . . . . . . . . 12 |- ((A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < (x / 2)) -> -. A.y e. NN (v <_ y -> ((x / 2) + (F` w)) < (F` y))) -> A.y(A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < (x / 2)) -> -. A.y e. NN (v <_ y -> ((x / 2) + (F` w)) < (F` y))))
15		nngt0t 5948	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (v e. NN -> 0 < v)
16	15	adantl 390	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((w e. NN /\ v e. NN) -> 0 < v)
17		ltaddpost 5663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((v e. RR /\ w e. RR) -> (0 < v <-> w < (w + v)))
18	17	ancoms 438	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((w e. RR /\ v e. RR) -> (0 < v <-> w < (w + v)))
19		nnret 5931	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (w e. NN -> w e. RR)
20		nnret 5931	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (v e. NN -> v e. RR)
21	18, 19, 20	syl2an 456	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((w e. NN /\ v e. NN) -> (0 < v <-> w < (w + v)))
22	16, 21	mpbid 195	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((w e. NN /\ v e. NN) -> w < (w + v))
23	22	adantl 390	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((y e. RR /\ (w e. NN /\ v e. NN)) -> w < (w + v))
24		ltletrt 5536	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((w e. RR /\ (w + v) e. RR /\ y e. RR) -> ((w < (w + v) /\ (w + v) <_ y) -> w < y))
25	19	ad2antrl 408	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((y e. RR /\ (w e. NN /\ v e. NN)) -> w e. RR)
26	5	adantl 390	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((y e. RR /\ (w e. NN /\ v e. NN)) -> (w + v) e. RR)
27		pm3.26 319	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((y e. RR /\ (w e. NN /\ v e. NN)) -> y e. RR)
28	24, 25, 26, 27	syl3anc 860	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((y e. RR /\ (w e. NN /\ v e. NN)) -> ((w < (w + v) /\ (w + v) <_ y) -> w < y))
29	23, 28	mpand 703	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((y e. RR /\ (w e. NN /\ v e. NN)) -> ((w + v) <_ y -> w < y))
30		nnret 5931	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y e. NN -> y e. RR)
31	29, 30	sylan 450	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((y e. NN /\ (w e. NN /\ v e. NN)) -> ((w + v) <_ y -> w < y))
32	31	adantrl 396	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y e. NN /\ ((x / 2) e. RR /\ (w e. NN /\ v e. NN))) -> ((w + v) <_ y -> w < y))
33		absltt 6880	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((((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))))
34		pm3.27 323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((-u(x / 2) < ((F` y) - (F` w)) /\ ((F` y) - (F` w)) < (x / 2)) -> ((F` y) - (F` w)) < (x / 2))
35	33, 34	syl6bi 214	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((F` y) - (F` w)) e. RR /\ (x / 2) e. RR) -> ((abs` ((F` y) - (F` w))) < (x / 2) -> ((F` y) - (F` w)) < (x / 2)))
36	35	ancoms 438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((x / 2) e. RR /\ ((F` y) - (F` w)) e. RR) -> ((abs` ((F` y) - (F` w))) < (x / 2) -> ((F` y) - (F` w)) < (x / 2)))
37		resubclt 5450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((F` y) e. RR /\ (F` w) e. RR) -> ((F` y) - (F` w)) e. RR)
38	36, 37	sylan2 453	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((x / 2) e. RR /\ ((F` y) e. RR /\ (F` w) e. RR)) -> ((abs` ((F` y) - (F` w))) < (x / 2) -> ((F` y) - (F` w)) < (x / 2)))
39	38	an1s 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((F` y) e. RR /\ ((x / 2) e. RR /\ (F` w) e. RR)) -> ((abs` ((F` y) - (F` w))) < (x / 2) -> ((F` y) - (F` w)) < (x / 2)))
40		ltsubaddt 5639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((F` y) e. RR /\ (F` w) e. RR /\ (x / 2) e. RR) -> (((F` y) - (F` w)) < (x / 2) <-> (F` y) < ((x / 2) + (F` w))))
41	40	3com23 841	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((F` y) e. RR /\ (x / 2) e. RR /\ (F` w) e. RR) -> (((F` y) - (F` w)) < (x / 2) <-> (F` y) < ((x / 2) + (F` w))))
42	41	3expb 836	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((F` y) e. RR /\ ((x / 2) e. RR /\ (F` w) e. RR)) -> (((F` y) - (F` w)) < (x / 2) <-> (F` y) < ((x / 2) + (F` w))))
43	39, 42	sylibd 202	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((F` y) e. RR /\ ((x / 2) e. RR /\ (F` w) e. RR)) -> ((abs` ((F` y) - (F` w))) < (x / 2) -> (F` y) < ((x / 2) + (F` w))))
44		ltnsymt 5544	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((F` y) e. RR /\ ((x / 2) + (F` w)) e. RR) -> ((F` y) < ((x / 2) + (F` w)) -> -. ((x / 2