Theorem bcthlem21 10315

Description: Lemma for bcth 10328. 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) C_ 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		gt0ne0 7246	. . . . . . 7 |- ((w e. RR /\ 0 < w) -> w =/= 0)
2		rereccl 7414	. . . . . . 7 |- ((w e. RR /\ w =/= 0) -> (1 / w) e. RR)
3	1, 2	syldan 691	. . . . . 6 |- ((w e. RR /\ 0 < w) -> (1 / w) e. RR)
4		2re 7598	. . . . . . 7 |- 2 e. RR
5		1lt2 7651	. . . . . . 7 |- 1 < 2
6		expnbnd 8401	. . . . . . 7 |- (((1 / w) e. RR /\ 2 e. RR /\ 1 < 2) -> E.m e. NN (1 / w) < (2^m))
7	4, 5, 6	mp3an23 1486	. . . . . 6 |- ((1 / w) e. RR -> E.m e. NN (1 / w) < (2^m))
8	3, 7	syl 13	. . . . 5 |- ((w e. RR /\ 0 < w) -> E.m e. NN (1 / w) < (2^m))
9		nnnn0 7767	. . . . . . . 8 |- (m e. NN -> m e. NN0)
10		reexpcl 8323	. . . . . . . . . 10 |- ((2 e. RR /\ m e. NN0) -> (2^m) e. RR)
11	4, 10	mpan 773	. . . . . . . . 9 |- (m e. NN0 -> (2^m) e. RR)
12		2pos 7609	. . . . . . . . . 10 |- 0 < 2
13		expgt0 8331	. . . . . . . . . 10 |- ((2 e. RR /\ m e. NN0 /\ 0 < 2) -> 0 < (2^m))
14	4, 12, 13	mp3an13 1485	. . . . . . . . 9 |- (m e. NN0 -> 0 < (2^m))
15	11, 14	jca 590	. . . . . . . 8 |- (m e. NN0 -> ((2^m) e. RR /\ 0 < (2^m)))
16	9, 15	syl 13	. . . . . . 7 |- (m e. NN -> ((2^m) e. RR /\ 0 < (2^m)))
17		ltrec1 7506	. . . . . . 7 |- (((w e. RR /\ 0 < w) /\ ((2^m) e. RR /\ 0 < (2^m))) -> ((1 / w) < (2^m) <-> (1 / (2^m)) < w))
18	16, 17	sylan2 696	. . . . . 6 |- (((w e. RR /\ 0 < w) /\ m e. NN) -> ((1 / w) < (2^m) <-> (1 / (2^m)) < w))
19	18	rexbidva 2400	. . . . 5 |- ((w e. RR /\ 0 < w) -> (E.m e. NN (1 / w) < (2^m) <-> E.m e. NN (1 / (2^m)) < w))
20	8, 19	mpbid 256	. . . 4 |- ((w e. RR /\ 0 < w) -> E.m e. NN (1 / (2^m)) < w)
21	20	adantl 544	. . 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)
22		bcthlem3 10297	. . . . . . . . . . . . . . . . 17 |- ((g:NN-->A /\ m e. NN) -> ((1st o. g)` m) = (1st` (g` m)))
23	22	adantr 543	. . . . . . . . . . . . . . . 16 |- (((g:NN-->A /\ m e. NN) /\ n e. NN) -> ((1st o. g)` m) = (1st` (g` m)))
24		bcthlem3 10297	. . . . . . . . . . . . . . . . 17 |- ((g:NN-->A /\ n e. NN) -> ((1st o. g)` n) = (1st` (g` n)))
25	24	adantlr 834	. . . . . . . . . . . . . . . 16 |- (((g:NN-->A /\ m e. NN) /\ n e. NN) -> ((1st o. g)` n) = (1st` (g` n)))
26	23, 25	opreq12d 5035	. . . . . . . . . . . . . . 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))))
27	26	adantrr 838	. . . . . . . . . . . . . 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))))
28	27	adantrl 836	. . . . . . . . . . . . 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))))
29	28	exp31 673	. . . . . . . . . . . 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))))))
30	29	a1d 18	. . . . . . . . . . 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)))))))
31	30	adantr 543	. . . . . . . . . 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)))))))
32	31	imp 489	. . . . . . . . 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))))))
33	32	imp 489	. . . . . . . 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)))))
34	33	imp 489	. . . . . . 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))))
35		bcthlem18.7	. . . . . . . . . . . . . . . . . . . . . . 23 |- A = (X X. {x e. RR | 0 < x})
36	35	bcthlem4 10298	. . . . . . . . . . . . . . . . . . . . . 22 |- ((g:NN-->A /\ m e. NN) -> ((1st` (g` m)) e. X /\ ((2nd` (g` m)) e. RR /\ 0 < (2nd` (g` m)))))
37	36	simpld 536	. . . . . . . . . . . . . . . . . . . . 21 |- ((g:NN-->A /\ m e. NN) -> (1st` (g` m)) e. X)
38	35	bcthlem4 10298	. . . . . . . . . . . . . . . . . . . . . 22 |- ((g:NN-->A /\ n e. NN) -> ((1st` (g` n)) e. X /\ ((2nd` (g` n)) e. RR /\ 0 < (2nd` (g` n)))))
39	38	simpld 536	. . . . . . . . . . . . . . . . . . . . 21 |- ((g:NN-->A /\ n e. NN) -> (1st` (g` n)) e. X)
40		bcthlem18.1	. . . . . . . . . . . . . . . . . . . . . . 23 |- D e. CMet
41	40	cmsmeti 10256	. . . . . . . . . . . . . . . . . . . . . 22 |- D e. Met
42		bcthlem18.3	. . . . . . . . . . . . . . . . . . . . . . 23 |- X = dom dom D
43	42	metcl 10104	. . . . . . . . . . . . . . . . . . . . . 22 |- ((D e. Met /\ (1st` (g` m)) e. X /\ (1st` (g` n)) e. X) -> ((1st` (g` m))D(1st` (g` n))) e. RR)
44	41, 43	mp3an1 1481	. . . . . . . . . . . . . . . . . . . . 21 |- (((1st` (g` m)) e. X /\ (1st` (g` n)) e. X) -> ((1st` (g` m))D(1st` (g` n))) e. RR)
45	37, 39, 44	syl2an 699	. . . . . . . . . . . . . . . . . . . 20 |- (((g:NN-->A /\ m e. NN) /\ (g:NN-->A /\ n e. NN)) -> ((1st` (g` m))D(1st` (g` n))) e. RR)
46	45	anandis 946	. . . . . . . . . . . . . . . . . . 19 |- ((g:NN-->A /\ (m e. NN /\ n e. NN)) -> ((1st` (g` m))D(1st` (g` n))) e. RR)
47	46	exp32 674	. . . . . . . . . . . . . . . . . 18 |- (g:NN-->A -> (m e. NN -> (n e. NN -> ((1st` (g` m))D(1st` (g` n))) e. RR)))
48	47	adantr 543	. . . . . . . . . . . . . . . . 17 |- ((g:NN-->A /\ ((2nd` (g` 1)) < (1 / 2) /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) -> (m e. NN -> (n e. NN -> ((1st` (g` m))D(1st` (g` n))) e. RR)))
49	48	com23 68	. . . . . . . . . . . . . . . 16 |- ((g:NN-->A /\ ((2nd` (g` 1)) < (1 / 2) /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) -> (n e. NN -> (m e. NN -> ((1st` (g` m))D(1st` (g` n))) e. RR)))
50	49	com12 26	. . . . . . . . . . . . . . 15 |- (n e. NN -> ((g:NN-->A /\ ((2nd` (g` 1)) < (1 / 2) /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) -> (m e. NN -> ((1st` (g` m))D(1st` (g` n))) e. RR)))
51	50	imp32 493	. . . . . . . . . . . . . 14 |- ((n e. NN /\ ((g:NN-->A /\ ((2nd` (g` 1)) < (1 / 2) /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) /\ m e. NN)) -> ((1st` (g` m))D(1st` (g` n))) e. RR)
52	51	adantlr 834	. . . . . . . . . . . . 13 |- (((n e. NN /\ m <_ n) /\ ((g:NN-->A /\ ((2nd` (g` 1)) < (1 / 2) /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) /\ m e. NN)) -> ((1st` (g` m))D(1st` (g` n))) e. RR)
53	52	adantrlr 850	. . . . . . . . . . . 12 |- (((n e. NN /\ m <_ n) /\ (((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)) -> ((1st` (g` m))D(1st` (g` n))) e. RR)
54	36	simprd 541	. . . . . . . . . . . . . . . 16 |- ((g:NN-->A /\ m e. NN) -> ((2nd` (g` m)) e. RR /\ 0 < (2nd` (g` m))))
55	54	simpld 536	. . . . . . . . . . . . . . 15 |- ((g:NN-->A /\ m e. NN) -> (2nd` (g` m)) e. RR)
56	55	adantlr 834	. . . . . . . . . . . . . 14 |- (((g:NN-->A /\ ((2nd` (g` 1)) < (1 / 2) /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) /\ m e. NN) -> (2nd` (g` m)) e. RR)
57	56	adantlr 834	. . . . . . . . . . . . 13 |- ((((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) -> (2nd` (g` m)) e. RR)
58	57	adantl 544	. . . . . . . . . . . 12 |- (((n e. NN /\ m <_ n) /\ (((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)) -> (2nd` (g` m)) e. RR)
59		2cn 7599	. . . . . . . . . . . . . . . . 17 |- 2 e. CC
60		2ne0 7610	. . . . . . . . . . . . . . . . 17 |- 2 =/= 0
61		expne0i 8330	. . . . . . . . . . . . . . . . 17 |- ((2 e. CC /\ 2 =/= 0 /\ m e. NN0) -> (2^m) =/= 0)
62	59, 60, 61	mp3an12 1484	. . . . . . . . . . . . . . . 16 |- (m e. NN0 -> (2^m) =/= 0)
63		rereccl 7414	. . . . . . . . . . . . . . . 16 |- (((2^m) e. RR /\ (2^m) =/= 0) -> (1 / (2^m)) e. RR)
64	11, 62, 63	syl11anc 755	. . . . . . . . . . . . . . 15 |- (m e. NN0 -> (1 / (2^m)) e. RR)
65	9, 64	syl 13	. . . . . . . . . . . . . 14 |- (m e. NN -> (1 / (2^m)) e. RR)
66	65	adantl 544	. . . . . . . . . . . . 13 |- ((((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)) e. RR)
67	66	adantl 544	. . . . . . . . . . . 12 |- (((n e. NN /\ m <_ n) /\ (((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)) e. RR)
68		id 15	. . . . . . . . . . . . . . 15 |- ((g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))) -> (g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))))
69	68	adantrl 836	. . . . . . . . . . . . . 14 |- ((g:NN-->A /\ ((2nd` (g` 1)) < (1 / 2) /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) -> (g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))))
70		bcthlem18.6	. . . . . . . . . . . . . . 15 |- 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) C_ O))})}
71		bcthlem18.8	. . . . . . . . . . . . . . 15 |- O = ((X \ ((cls` J)` (M` j))) i^i ((1st` y)( ball ` D)((2nd` y) / 2)))
72	40, 42, 70, 35, 71	bcthlem20 10314	. . . . . . . . . . . . . 14 |- (((n e. NN /\ m <_ n) /\ ((g:NN-->A /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))) /\ m e. NN)) -> ((1st` (g` m))D(1st` (g` n))) < (2nd` (g` m)))
73	69, 72	sylanr1 741	. . . . . . . . . . . . 13 |- (((n e. NN /\ m <_ n) /\ ((g:NN-->A /\ ((2nd` (g` 1)) < (1 / 2) /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) /\ m e. NN)) -> ((1st` (g` m))D(1st` (g` n))) < (2nd` (g` m)))
74	73	adantrlr 850	. . . . . . . . . . . 12 |- (((n e. NN /\ m <_ n) /\ (((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)) -> ((1st` (g` m))D(1st` (g` n))) < (2nd` (g` m)))
75	40, 42, 70, 35, 71	bcthlem17 10311	. . . . . . . . . . . . . . . 16 |- (m e. NN -> ((g:NN-->A /\ ((2nd` (g` 1)) < (1 / 2) /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) -> (2nd` (g` m)) < (1 / (2^m))))
76	75	imp 489	. . . . . . . . . . . . . . 15 |- ((m e. NN /\ (g:NN-->A /\ ((2nd` (g` 1)) < (1 / 2) /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))))) -> (2nd` (g` m)) < (1 / (2^m)))
77	76	ancoms 512	. . . . . . . . . . . . . 14 |- (((g:NN-->A /\ ((2nd` (g` 1)) < (1 / 2) /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) /\ m e. NN) -> (2nd` (g` m)) < (1 / (2^m)))
78	77	adantlr 834	. . . . . . . . . . . . 13 |- ((((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) -> (2nd` (g` m)) < (1 / (2^m)))
79	78	adantl 544	. . . . . . . . . . . 12 |- (((n e. NN /\ m <_ n) /\ (((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)) -> (2nd` (g` m)) < (1 / (2^m)))
80	53, 58, 67, 74, 79	lttrd 6990	. . . . . . . . . . 11 |- (((n e. NN /\ m <_ n) /\ (((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)) -> ((1st` (g` m))D(1st` (g` n))) < (1 / (2^m)))
81		simplrl 873	. . . . . . . . . . . . 13 |- ((((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) -> w e. RR)
82	81	adantl 544	. . . . . . . . . . . 12 |- (((n e. NN /\ m <_ n) /\ (((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)) -> w e. RR)
83		axlttrn 6965	. . . . . . . . . . . 12 |- ((((1st` (g` m))D(1st` (g` n))) e. RR /\ (1 / (2^m)) e. RR /\ w e. RR) -> ((((1st` (g` m))D(1st` (g` n))) < (1 / (2^m)) /\ (1 / (2^m)) < w) -> ((1st` (g` m))D(1st` (g` n))) < w))
84	53, 67, 82, 83	syl111anc 1377	. . . . . . . . . . 11 |- (((n e. NN /\ m <_ n) /\ (((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)) -> ((((1st` (g` m))D(1st` (g` n))) < (1 / (2^m)) /\ (1 / (2^m)) < w) -> ((1st` (g` m))D(1st` (g` n))) < w))
85	80, 84	mpand 780	. . . . . . . . . 10 |- (((n e. NN /\ m <_ n) /\ (((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 -> ((1st` (g` m))D(1st` (g` n))) < w))
86	85	exp31 673	. . . . . . . . 9 |- (n e. NN -> (m <_ n -> ((((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 -> ((1st` (g` m))D(1st` (g` n))) < w))))
87	86	com4t 80	. . . . . . . 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` (g` m))D(1st` (g` n))) < w))))
88	87	imp45 669	. . . . . . 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` (g` m))D(1st` (g` n))) < w)
89	34, 88	eqbrtrd 3559	. . . . . 6 |- (((((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)) < w)
90	89	exp45 684	. . . . 5 |- ((((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)) < w))))
91	90	r19.21adv 2461	. . . 4 |- ((((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 -> A.n e. NN (m <_ n -> (((1st o. g)` m)D((1st o. g)` n)) < w)))
92	91	reximdva 2483	. . 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 -> E.m e. NN A.n e. NN (m <_ n -> (((1st o. g)` m)D((1st o. g)` n)) < w)))
93	21, 92	mpd 11	. 2 |- (((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))
94	93	exp32 674	1 |- ((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))))

Syntax hints:   -> wi 3   <-> wb 231   /\ wa 433   = wceq 1615   e. wcel 1617   =/= wne 2295  A.wral 2385  E.wrex 2386  {crab 2388   \ cdif 2856   i^i cin 2858   C_ wss 2859   class class class wbr 3539  {copab 3597   X. cxp 4149  dom cdm 4151   o. ccom 4155  -->wf 4159  ` cfv 4163  (class class class)co 5020  {copab2 5021  1stc1st 5164  2ndc2nd 5165  CCcc 6827  RRcr 6828  0cc0 6829  1c1 6830   + caddc 6832   <_ cle 6943   < clt 6947   / cdiv 7093  NNcn 7094  NN0cn0 7095  2c2 7580  ^cexp 8311  clsccl 9949  Metcme 10082   ball cbl 10084  CMetcms 10215

This theorem is referenced by:  bcthlem22 10316

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-13 1628  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-rep 3628  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719  ax-un 3961  ax-cnex 6885  ax-resscn 6886  ax-1cn 6887  ax-icn 6888  ax-addcl 6889  ax-addrcl 6890  ax-mulcl 6891  ax-mulrcl 6892  ax-mulcom 6893  ax-addass 6894  ax-mulass 6895  ax-distr 6896  ax-i2m1 6897  ax-1ne0 6898  ax-1rid 6899  ax-rnegex 6900  ax-rrecex 6901  ax-cnre 6902  ax-pre-lttri 6903  ax-pre-lttrn 6904  ax-pre-ltadd 6905  ax-pre-mulgt0 6906  ax-pre-sup 6907  ax-mulopr 6909

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3or 1131  df-3an 1132  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-nel 2298  df-ral 2389  df-rex 2390  df-reu 2391  df-rab 2392  df-v 2571  df-sbc 2731  df-csb 2806  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-pss 2870  df-nul 3115  df-if 3213  df-pw 3261  df-sn 3274  df-pr 3275  df-tp 3277  df-op 3278  df-uni 3399  df-int 3433  df-iun 3470  df-br 3540  df-opab 3598  df-tr 3612  df-eprel 3776  df-id 3779  df-po 3784  df-so 3796  df-fr 3814  df-we 3830  df-ord 3846  df-on 3847  df-lim 3848  df-suc 3849  df-om 4118  df-xp 4165  df-rel 4166  df-cnv 4167  df-co 4168  df-dm 4169  df-rn 4170  df-res 4171  df-ima 4172  df-fun 4173  df-fn 4174  df-f 4175  df-f1 4176  df-fo 4177  df-f1o 4178  df-fv 4179  df-opr 5022  df-oprab 5023  df-mpt 5138  df-1st 5166  df-2nd 5167  df-iota 5259  df-rdg 5344  df-er 5519  df-en 5631  df-dom 5632  df-sdom 5633  df-undef 5769  df-riota 5773  df-pnf 6948  df-mnf 6949  df-xr 6950  df-ltxr 6951  df-le 6952  df-sub 7111  df-neg 7113  df-div 7325  df-n 7543  df-2 7589  df-n0 7761  df-z 7798  df-fl 7921  df-seq1 8210  df-exp 8312  df-met 10086  df-bl 10088  df-cmet 10218

Copyright terms: Public domain