Theorem cvg2 6922

Description: Two ways to express that a sequence converges or is Cauchy.

Hypothesis

Ref	Expression
cvg2.1	|- ((y e. F /\ z e. G) -> A e. RR)

Assertion

Ref	Expression
cvg2	|- (A.x e. RR (0 < x -> E.y e. F A.z e. G (ph -> A < x)) <-> A.x e. RR (0 < x -> E.y e. F A.z e. G (ph -> A <_ x)))

Distinct variable groups:   x,y,z   x,A   x,F,z   x,G   ph,x

Proof of Theorem cvg2

Step	Hyp	Ref	Expression
1		ltlet 5520	. . . . . . . . . 10 |- ((A e. RR /\ x e. RR) -> (A < x -> A <_ x))
2	1	ancoms 436	. . . . . . . . 9 |- ((x e. RR /\ A e. RR) -> (A < x -> A <_ x))
3		cvg2.1	. . . . . . . . 9 |- ((y e. F /\ z e. G) -> A e. RR)
4	2, 3	sylan2 451	. . . . . . . 8 |- ((x e. RR /\ (y e. F /\ z e. G)) -> (A < x -> A <_ x))
5	4	anassrs 441	. . . . . . 7 |- (((x e. RR /\ y e. F) /\ z e. G) -> (A < x -> A <_ x))
6	5	imim2d 25	. . . . . 6 |- (((x e. RR /\ y e. F) /\ z e. G) -> ((ph -> A < x) -> (ph -> A <_ x)))
7	6	r19.20dva 1709	. . . . 5 |- ((x e. RR /\ y e. F) -> (A.z e. G (ph -> A < x) -> A.z e. G (ph -> A <_ x)))
8	7	r19.22dva 1739	. . . 4 |- (x e. RR -> (E.y e. F A.z e. G (ph -> A < x) -> E.y e. F A.z e. G (ph -> A <_ x)))
9	8	imim2d 25	. . 3 |- (x e. RR -> ((0 < x -> E.y e. F A.z e. G (ph -> A < x)) -> (0 < x -> E.y e. F A.z e. G (ph -> A <_ x))))
10	9	r19.20i 1704	. 2 |- (A.x e. RR (0 < x -> E.y e. F A.z e. G (ph -> A < x)) -> A.x e. RR (0 < x -> E.y e. F A.z e. G (ph -> A <_ x)))
11		breq2 2623	. . . . . . 7 |- (x = (w / 2) -> (0 < x <-> 0 < (w / 2)))
12		breq2 2623	. . . . . . . . 9 |- (x = (w / 2) -> (A <_ x <-> A <_ (w / 2)))
13	12	imbi2d 612	. . . . . . . 8 |- (x = (w / 2) -> ((ph -> A <_ x) <-> (ph -> A <_ (w / 2))))
14	13	rexralbidv 1682	. . . . . . 7 |- (x = (w / 2) -> (E.y e. F A.z e. G (ph -> A <_ x) <-> E.y e. F A.z e. G (ph -> A <_ (w / 2))))
15	11, 14	imbi12d 626	. . . . . 6 |- (x = (w / 2) -> ((0 < x -> E.y e. F A.z e. G (ph -> A <_ x)) <-> (0 < (w / 2) -> E.y e. F A.z e. G (ph -> A <_ (w / 2)))))
16	15	rcla4cv 1874	. . . . 5 |- (A.x e. RR (0 < x -> E.y e. F A.z e. G (ph -> A <_ x)) -> ((w / 2) e. RR -> (0 < (w / 2) -> E.y e. F A.z e. G (ph -> A <_ (w / 2)))))
17		biimt 731	. . . . . . . . . 10 |- (((w / 2) e. RR /\ 0 < (w / 2)) -> (E.y e. F A.z e. G (ph -> A <_ (w / 2)) <-> (((w / 2) e. RR /\ 0 < (w / 2)) -> E.y e. F A.z e. G (ph -> A <_ (w / 2)))))
18		rehalfclt 6034	. . . . . . . . . . 11 |- (w e. RR -> (w / 2) e. RR)
19	18	adantr 389	. . . . . . . . . 10 |- ((w e. RR /\ 0 < w) -> (w / 2) e. RR)
20		halfpos2t 6037	. . . . . . . . . . 11 |- (w e. RR -> (0 < w <-> 0 < (w / 2)))
21	20	biimpa 416	. . . . . . . . . 10 |- ((w e. RR /\ 0 < w) -> 0 < (w / 2))
22	17, 19, 21	sylanc 471	. . . . . . . . 9 |- ((w e. RR /\ 0 < w) -> (E.y e. F A.z e. G (ph -> A <_ (w / 2)) <-> (((w / 2) e. RR /\ 0 < (w / 2)) -> E.y e. F A.z e. G (ph -> A <_ (w / 2)))))
23		impexp 347	. . . . . . . . 9 |- ((((w / 2) e. RR /\ 0 < (w / 2)) -> E.y e. F A.z e. G (ph -> A <_ (w / 2))) <-> ((w / 2) e. RR -> (0 < (w / 2) -> E.y e. F A.z e. G (ph -> A <_ (w / 2)))))
24	22, 23	syl6bb 536	. . . . . . . 8 |- ((w e. RR /\ 0 < w) -> (E.y e. F A.z e. G (ph -> A <_ (w / 2)) <-> ((w / 2) e. RR -> (0 < (w / 2) -> E.y e. F A.z e. G (ph -> A <_ (w / 2))))))
25		halfpost 6036	. . . . . . . . . . . . . . . 16 |- (w e. RR -> (0 < w <-> (w / 2) < w))
26	25	biimpa 416	. . . . . . . . . . . . . . 15 |- ((w e. RR /\ 0 < w) -> (w / 2) < w)
27	26	adantr 389	. . . . . . . . . . . . . 14 |- (((w e. RR /\ 0 < w) /\ A e. RR) -> (w / 2) < w)
28		lelttrt 5523	. . . . . . . . . . . . . . 15 |- ((A e. RR /\ (w / 2) e. RR /\ w e. RR) -> ((A <_ (w / 2) /\ (w / 2) < w) -> A < w))
29		pm3.27 323	. . . . . . . . . . . . . . 15 |- (((w e. RR /\ 0 < w) /\ A e. RR) -> A e. RR)
30	18	ad2antrr 404	. . . . . . . . . . . . . . 15 |- (((w e. RR /\ 0 < w) /\ A e. RR) -> (w / 2) e. RR)
31		simpll 412	. . . . . . . . . . . . . . 15 |- (((w e. RR /\ 0 < w) /\ A e. RR) -> w e. RR)
32	28, 29, 30, 31	syl3anc 858	. . . . . . . . . . . . . 14 |- (((w e. RR /\ 0 < w) /\ A e. RR) -> ((A <_ (w / 2) /\ (w / 2) < w) -> A < w))
33	27, 32	mpan2d 702	. . . . . . . . . . . . 13 |- (((w e. RR /\ 0 < w) /\ A e. RR) -> (A <_ (w / 2) -> A < w))
34	33, 3	sylan2 451	. . . . . . . . . . . 12 |- (((w e. RR /\ 0 < w) /\ (y e. F /\ z e. G)) -> (A <_ (w / 2) -> A < w))
35	34	anassrs 441	. . . . . . . . . . 11 |- ((((w e. RR /\ 0 < w) /\ y e. F) /\ z e. G) -> (A <_ (w / 2) -> A < w))
36	35	imim2d 25	. . . . . . . . . 10 |- ((((w e. RR /\ 0 < w) /\ y e. F) /\ z e. G) -> ((ph -> A <_ (w / 2)) -> (ph -> A < w)))
37	36	r19.20dva 1709	. . . . . . . . 9 |- (((w e. RR /\ 0 < w) /\ y e. F) -> (A.z e. G (ph -> A <_ (w / 2)) -> A.z e. G (ph -> A < w)))
38	37	r19.22dva 1739	. . . . . . . 8 |- ((w e. RR /\ 0 < w) -> (E.y e. F A.z e. G (ph -> A <_ (w / 2)) -> E.y e. F A.z e. G (ph -> A < w)))
39	24, 38	sylbird 205	. . . . . . 7 |- ((w e. RR /\ 0 < w) -> (((w / 2) e. RR -> (0 < (w / 2) -> E.y e. F A.z e. G (ph -> A <_ (w / 2)))) -> E.y e. F A.z e. G (ph -> A < w)))
40	39	com12 11	. . . . . 6 |- (((w / 2) e. RR -> (0 < (w / 2) -> E.y e. F A.z e. G (ph -> A <_ (w / 2)))) -> ((w e. RR /\ 0 < w) -> E.y e. F A.z e. G (ph -> A < w)))
41	40	exp3a 375	. . . . 5 |- (((w / 2) e. RR -> (0 < (w / 2) -> E.y e. F A.z e. G (ph -> A <_ (w / 2)))) -> (w e. RR -> (0 < w -> E.y e. F A.z e. G (ph -> A < w))))
42	16, 41	syl 10	. . . 4 |- (A.x e. RR (0 < x -> E.y e. F A.z e. G (ph -> A <_ x)) -> (w e. RR -> (0 < w -> E.y e. F A.z e. G (ph -> A < w))))
43	42	r19.21aiv 1713	. . 3 |- (A.x e. RR (0 < x -> E.y e. F A.z e. G (ph -> A <_ x)) -> A.w e. RR (0 < w -> E.y e. F A.z e. G (ph -> A < w)))
44		breq2 2623	. . . . 5 |- (w = x -> (0 < w <-> 0 < x))
45		breq2 2623	. . . . . . 7 |- (w = x -> (A < w <-> A < x))
46	45	imbi2d 612	. . . . . 6 |- (w = x -> ((ph -> A < w) <-> (ph -> A < x)))
47	46	rexralbidv 1682	. . . . 5 |- (w = x -> (E.y e. F A.z e. G (ph -> A < w) <-> E.y e. F A.z e. G (ph -> A < x)))
48	44, 47	imbi12d 626	. . . 4 |- (w = x -> ((0 < w -> E.y e. F A.z e. G (ph -> A < w)) <-> (0 < x -> E.y e. F A.z e. G (ph -> A < x))))
49	48	cbvralv 1800	. . 3 |- (A.w e. RR (0 < w -> E.y e. F A.z e. G (ph -> A < w)) <-> A.x e. RR (0 < x -> E.