Theorem bcthlem21 7969

Description: Lemma for bcth 7982. A defining property for (1st o. g) to be a Cauchy sequence.

Hypotheses

Ref	Expression
bcthlem18.1	|- D e. CMet
bcthlem18.3	|- X = dom dom D
bcthlem18.6	|- F = {<.<.j, y>., z>. | ((j e. NN /\ y e. A) /\ z = {<.p, r>. | ((p e. X /\ (r e. RR /\ 0 < r)) /\ (r < ((2nd` y) / 2) /\ (p( ball ` D)r) (_ O))})}
bcthlem18.7	|- A = (X X. {x e. RR | 0 < x})
bcthlem18.8	|- O = ((X \ ((cls` J)` (M` j))) i^i ((1st` y)( ball ` D)((2nd` y) / 2)))

Assertion

Ref	Expression
bcthlem21	|- ((g:NN-->A /\ ((2nd` (g` 1)) < (1 / 2) /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) -> (w e. RR -> (0 < w -> E.m e. NN A.n e. NN (m <_ n -> (((1st o. g)` m)D((1st o. g)` n)) < w))))

Distinct variable groups:   j,m,n,w,y,z,A   j,p,r,D,m,n,w,y,z   k,m,n,w,F   j,J,p,r,y,z   j,M,p,r,y,z   z,O   j,X,m,n,p,r,w,y,z   j,k,x,g,p,r,y,z,m,n,w

Proof of Theorem bcthlem21

Step	Hyp	Ref	Expression
1		gt0ne0t 5600	. . . . . . 7 |- ((w e. RR /\ 0 < w) -> w =/= 0)
2		rerecclt 5767	. . . . . . 7 |- ((w e. RR /\ w =/= 0) -> (1 / w) e. RR)
3	1, 2	syldan 467	. . . . . 6 |- ((w e. RR /\ 0 < w) -> (1 / w) e. RR)
4		2re 5934	. . . . . . 7 |- 2 e. RR
5		1lt2 5983	. . . . . . . 8 |- 1 < 2
6		expnbndt 6593	. . . . . . . 8 |- (((1 / w) e. RR /\ 2 e. RR /\ 1 < 2) -> E.m e. NN (1 / w) < (2^m))
7	5, 6	mp3an3 903	. . . . . . 7 |- (((1 / w) e. RR /\ 2 e. RR) -> E.m e. NN (1 / w) < (2^m))
8	4, 7	mpan2 695	. . . . . 6 |- ((1 / w) e. RR -> E.m e. NN (1 / w) < (2^m))
9	3, 8	syl 10	. . . . 5 |- ((w e. RR /\ 0 < w) -> E.m e. NN (1 / w) < (2^m))
10		ltrec1t 5844	. . . . . . 7 |- (((w e. RR /\ 0 < w) /\ ((2^m) e. RR /\ 0 < (2^m))) -> ((1 / w) < (2^m) <-> (1 / (2^m)) < w))
11		nnnn0t 6061	. . . . . . . 8 |- (m e. NN -> m e. NN0)
12		reexpclt 6520	. . . . . . . . . 10 |- ((2 e. RR /\ m e. NN0) -> (2^m) e. RR)
13	4, 12	mpan 694	. . . . . . . . 9 |- (m e. NN0 -> (2^m) e. RR)
14		2pos 5944	. . . . . . . . . . 11 |- 0 < 2
15		expgt0t 6528	. . . . . . . . . . 11 |- ((2 e. RR /\ m e. NN0 /\ 0 < 2) -> 0 < (2^m))
16	14, 15	mp3an3 903	. . . . . . . . . 10 |- ((2 e. RR /\ m e. NN0) -> 0 < (2^m))
17	4, 16	mpan 694	. . . . . . . . 9 |- (m e. NN0 -> 0 < (2^m))
18	13, 17	jca 288	. . . . . . . 8 |- (m e. NN0 -> ((2^m) e. RR /\ 0 < (2^m)))
19	11, 18	syl 10	. . . . . . 7 |- (m e. NN -> ((2^m) e. RR /\ 0 < (2^m)))
20	10, 19	sylan2 451	. . . . . 6 |- (((w e. RR /\ 0 < w) /\ m e. NN) -> ((1 / w) < (2^m) <-> (1 / (2^m)) < w))
21	20	rexbidva 1657	. . . . 5 |- ((w e. RR /\ 0 < w) -> (E.m e. NN (1 / w) < (2^m) <-> E.m e. NN (1 / (2^m)) < w))
22	9, 21	mpbid 195	. . . 4 |- ((w e. RR /\ 0 < w) -> E.m e. NN (1 / (2^m)) < w)
23	22	adantl 388	. . 3 |- (((g:NN-->A /\ ((2nd` (g` 1)) < (1 / 2) /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) /\ (w e. RR /\ 0 < w)) -> E.m e. NN (1 / (2^m)) < w)
24		bcthlem3 7951	. . . . . . . . . . . . . . . . 17 |- ((g:NN-->A /\ m e. NN) -> ((1st o. g)` m) = (1st` (g` m)))
25	24	adantr 389	. . . . . . . . . . . . . . . 16 |- (((g:NN-->A /\ m e. NN) /\ n e. NN) -> ((1st o. g)` m) = (1st` (g` m)))
26		bcthlem3 7951	. . . . . . . . . . . . . . . . 17 |- ((g:NN-->A /\ n e. NN) -> ((1st o. g)` n) = (1st` (g` n)))
27	26	adantlr 393	. . . . . . . . . . . . . . . 16 |- (((g:NN-->A /\ m e. NN) /\ n e. NN) -> ((1st o. g)` n) = (1st` (g` n)))
28	25, 27	opreq12d 3969	. . . . . . . . . . . . . . 15 |- (((g:NN-->A /\ m e. NN) /\ n e. NN) -> (((1st o. g)` m)D((1st o. g)` n)) = ((1st` (g` m))D(1st` (g` n))))
29	28	adantrr 395	. . . . . . . . . . . . . 14 |- (((g:NN-->A /\ m e. NN) /\ (n e. NN /\ m <_ n)) -> (((1st o. g)` m)D((1st o. g)` n)) = ((1st` (g` m))D(1st` (g` n))))
30	29	adantrl 394	. . . . . . . . . . . . 13 |- (((g:NN-->A /\ m e. NN) /\ ((1 / (2^m)) < w /\ (n e. NN /\ m <_ n))) -> (((1st o. g)` m)D((1st o. g)` n)) = ((1st` (g` m))D(1st` (g` n))))
31	30	exp31 376	. . . . . . . . . . . 12 |- (g:NN-->A -> (m e. NN -> (((1 / (2^m)) < w /\ (n e. NN /\ m <_ n)) -> (((1st o. g)` m)D((1st o. g)` n)) = ((1st` (g` m))D(1st` (g` n))))))
32	31	a1d 12	. . . . . . . . . . 11 |- (g:NN-->A -> ((w e. RR /\ 0 < w) -> (m e. NN -> (((1 / (2^m)) < w /\ (n e. NN /\ m <_ n)) -> (((1st o. g)` m)D((1st o. g)` n)) = ((1st` (g` m))D(1st` (g` n)))))))
33	32	adantr 389	. . . . . . . . . 10 |- ((g:NN-->A /\ ((2nd` (g` 1)) < (1 / 2) /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) -> ((w e. RR /\ 0 < w) -> (m e. NN -> (((1 / (2^m)) < w /\ (n e. NN /\ m <_ n)) -> (((1st o. g)` m)D((1st o. g)` n)) = ((1st` (g` m))D(1st` (g` n)))))))
34	33	imp 350	. . . . . . . . 9 |- (((g:NN-->A /\ ((2nd` (g` 1)) < (1 / 2) /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) /\ (w e. RR /\ 0 < w)) -> (m e. NN -> (((1 / (2^m)) < w /\ (n e. NN /\ m <_ n)) -> (((1st o. g)` m)D((1st o. g)` n)) = ((1st` (g` m))D(1st` (g` n))))))
35	34	imp 350	. . . . . . . 8 |- ((((g:NN-->A /\ ((2nd` (g` 1)) < (1 / 2) /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) /\ (w e. RR /\ 0 < w)) /\ m e. NN) -> (((1 / (2^m)) < w /\ (n e. NN /\ m <_ n)) -> (((1st o. g)` m)D((1st o. g)` n)) = ((1st` (g` m))D(1st` (g` n)))))
36	35	imp 350	. . . . . . 7 |- (((((g:NN-->A /\ ((2nd` (g` 1)) < (1 / 2) /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) /\ (w e. RR /\ 0 < w)) /\ m e. NN) /\ ((1 / (2^m)) < w /\ (n e. NN /\ m <_ n))) -> (((1st o. g)` m)D((1st o. g)` n)) = ((1st` (g` m))D(1st` (g` n))))
37		bcthlem18.1	. . . . . . . . . . . . . . . . . . . . . . 23 |- D e. CMet
38	37	cmsmeti 7913	. . . . . . . . . . . . . . . . . . . . . 22 |- D e. Met
39		bcthlem18.3	. . . . . . . . . . . . . . . . . . . . . . 23 |- X = dom dom D
40	39	metcl 7761	. . . . . . . . . . . . . . . . . . . . . 22 |- ((D e. Met /\ (1st` (g` m)) e. X /\ (1st` (g` n)) e. X) -> ((1st` (g` m))D(1st` (g` n)))