Theorem cau3ir 6852

Description: A relationship used to derive two ways to express a Cauchy sequence. Normally Z and W are subsets of ZZ, and R is <_ or <. ph is ph(j, k, x).

Hypotheses

Ref	Expression
cau3ir.1	|- (k = m -> (ph <-> ps))
cau3ir.2	|- (j = k -> (ps <-> ch))
cau3ir.3	|- (x = (y / 2) -> ((ph /\ ps) <-> th))
cau3ir.4	|- (x = y -> (ch <-> ta))
cau3ir.5	|- (((et /\ y e. RR) /\ (j e. Z /\ k e. W /\ m e. W)) -> (th -> ta))

Assertion

Ref	Expression
cau3ir	|- (et -> (A.x e. RR (0 < x -> E.j e. Z A.k e. W (jRk -> ph)) -> A.x e. RR (0 < x -> E.m e. Z A.j e. W A.k e. W ((mRj /\ mRk) -> ph))))

Distinct variable groups:   j,k,m,x,y,R   j,W,k,m,x,y   j,Z,k,m,x,y   ch,j,y   j,et,k,m,y   ph,m,y   ps,k   th,x   ta,x

Proof of Theorem cau3ir

Step	Hyp	Ref	Expression
1		halfpos2t 5984	. . . . . . . . 9 |- (y e. RR -> (0 < y <-> 0 < (y / 2)))
2	1	adantl 388	. . . . . . . 8 |- ((A.x e. RR (0 < x -> E.j e. Z A.k e. W A.m e. W ((jRk /\ jRm) -> (ph /\ ps))) /\ y e. RR) -> (0 < y <-> 0 < (y / 2)))
3		breq2 2613	. . . . . . . . . . 11 |- (x = (y / 2) -> (0 < x <-> 0 < (y / 2)))
4		cau3ir.3	. . . . . . . . . . . . . 14 |- (x = (y / 2) -> ((ph /\ ps) <-> th))
5	4	imbi2d 610	. . . . . . . . . . . . 13 |- (x = (y / 2) -> (((jRk /\ jRm) -> (ph /\ ps)) <-> ((jRk /\ jRm) -> th)))
6	5	2ralbidv 1672	. . . . . . . . . . . 12 |- (x = (y / 2) -> (A.k e. W A.m e. W ((jRk /\ jRm) -> (ph /\ ps)) <-> A.k e. W A.m e. W ((jRk /\ jRm) -> th)))
7	6	rexbidv 1656	. . . . . . . . . . 11 |- (x = (y / 2) -> (E.j e. Z A.k e. W A.m e. W ((jRk /\ jRm) -> (ph /\ ps)) <-> E.j e. Z A.k e. W A.m e. W ((jRk /\ jRm) -> th)))
8	3, 7	imbi12d 624	. . . . . . . . . 10 |- (x = (y / 2) -> ((0 < x -> E.j e. Z A.k e. W A.m e. W ((jRk /\ jRm) -> (ph /\ ps))) <-> (0 < (y / 2) -> E.j e. Z A.k e. W A.m e. W ((jRk /\ jRm) -> th))))
9	8	rcla4cva 1867	. . . . . . . . 9 |- ((A.x e. RR (0 < x -> E.j e. Z A.k e. W A.m e. W ((jRk /\ jRm) -> (ph /\ ps))) /\ (y / 2) e. RR) -> (0 < (y / 2) -> E.j e. Z A.k e. W A.m e. W ((jRk /\ jRm) -> th)))
10		rehalfclt 5981	. . . . . . . . 9 |- (y e. RR -> (y / 2) e. RR)
11	9, 10	sylan2 451	. . . . . . . 8 |- ((A.x e. RR (0 < x -> E.j e. Z A.k e. W A.m e. W ((jRk /\ jRm) -> (ph /\ ps))) /\ y e. RR) -> (0 < (y / 2) -> E.j e. Z A.k e. W A.m e. W ((jRk /\ jRm) -> th)))
12	2, 11	sylbid 203	. . . . . . 7 |- ((A.x e. RR (0 < x -> E.j e. Z A.k e. W A.m e. W ((jRk /\ jRm) -> (ph /\ ps))) /\ y e. RR) -> (0 < y -> E.j e. Z A.k e. W A.m e. W ((jRk /\ jRm) -> th)))
13		raaan 2350	. . . . . . . . . . . 12 |- (A.k e. W A.m e. W ((jRk -> ph) /\ (jRm -> ps)) <-> (A.k e. W (jRk -> ph) /\ A.m e. W (jRm -> ps)))
14		breq2 2613	. . . . . . . . . . . . . . 15 |- (k = m -> (jRk <-> jRm))
15		cau3ir.1	. . . . . . . . . . . . . . 15 |- (k = m -> (ph <-> ps))
16	14, 15	imbi12d 624	. . . . . . . . . . . . . 14 |- (k = m -> ((jRk -> ph) <-> (jRm -> ps)))
17	16	cbvralv 1791	. . . . . . . . . . . . 13 |- (A.k e. W (jRk -> ph) <-> A.m e. W (jRm -> ps))
18	17	anbi2i 479	. . . . . . . . . . . 12 |- ((A.k e. W (jRk -> ph) /\ A.k e. W (jRk -> ph)) <-> (A.k e. W (jRk -> ph) /\ A.m e. W (jRm -> ps)))
19		anidm 432	. . . . . . . . . . . 12 |- ((A.k e. W (jRk -> ph) /\ A.k e. W (jRk -> ph)) <-> A.k e. W (jRk -> ph))
20	13, 18, 19	3bitr2r 180	. . . . . . . . . . 11 |- (A.k e. W (jRk -> ph) <-> A.k e. W A.m e. W ((jRk -> ph) /\ (jRm -> ps)))
21		prth 554	. . . . . . . . . . . . 13 |- (((jRk -> ph) /\ (jRm -> ps)) -> ((jRk /\ jRm) -> (ph /\ ps)))
22	21	r19.20si 1698	. . . . . . . . . . . 12 |- (A.m e. W ((jRk -> ph) /\ (jRm -> ps)) -> A.m e. W ((jRk /\ jRm) -> (ph /\ ps)))
23	22	r19.20si 1698	. . . . . . . . . . 11 |- (A.k e. W A.m e. W ((jRk -> ph) /\ (jRm -> ps)) -> A.k e. W A.m e. W ((jRk /\ jRm) -> (ph /\ ps)))
24	20, 23	sylbi 199	. . . . . . . . . 10 |- (A.k e. W (jRk -> ph) -> A.k e. W A.m e. W ((jRk /\ jRm) -> (ph /\ ps)))
25	24	r19.22si 1726	. . . . . . . . 9 |- (E.j e. Z A.k e. W (jRk -> ph) -> E.j e. Z A.k e. W A.m e. W ((jRk /\ jRm) -> (ph /\ ps)))
26	25	imim2i 17	. . . . . . . 8 |- ((0 < x -> E.j e. Z A.k e. W (jRk -> ph)) -> (0 < x -> E.j e. Z A.k e. W A.m e. W ((jRk /\ jRm) -> (ph /\ ps))))
27	26	r19.20si 1698	. . . . . . 7 |- (A.x e. RR (0 < x -> E.j e. Z A.k e. W (jRk -> ph)) -> A.x e. RR (0 < x -> E.j e. Z A.k e. W A.m e. W ((jRk /\ jRm) -> (ph /\ ps))))
28	12, 27	sylan 448	. . . . . 6 |- ((A.x e. RR (0 < x -> E.j e. Z A.k e. W (jRk -> ph)) /\ y e. RR) -> (0 < y -> E.j e. Z A.k e. W A.m e. W ((jRk /\ jRm) -> th)))
29	28	adantl 388	. . . . 5 |- ((et /\ (A.x e. RR (0 < x -> E.j e. Z A.k e. W (jRk -> ph)) /\ y e. RR)) -> (0 < y -> E.j e. Z A.k e. W A.m e. W ((jRk /\ jRm) -> th)))
30		cau3ir.5	. . . . . . . . . . . 12 |- (((et /\ y e. RR) /\ (j e. Z /\ k e. W /\ m e. W)) -> (th -> ta))
31	30	3exp2 849	. . . . . . . . . . 11 |- ((et /\ y e. RR) -> (j e. Z -> (k e. W -> (m e. W -> (th -> ta)))))
32	31	imp41 368	. . . . . . . . . 10 |- (((((et /\ y e. RR) /\ j e. Z) /\ k e. W) /\ m e. W) -> (th -> ta))
33	32	imim2d 25	. . . . . . . . 9 |- (((((et /\ y e. RR) /\ j e. Z) /\ k e. W) /\ m e. W) -> (((jRk /\ jRm) -> th) -> ((jRk /\ jRm) -> ta)))
34	33	r19.20dva 1701	. . . . . . . 8 |- ((((et /\ y e. RR) /\ j e. Z) /\ k e. W) -> (A.m e. W ((jRk /\ jRm) -> th) -> A.m e. W ((jRk /\ jRm) -> ta)))
35	34	r19.20dva 1701	. . . . . . 7 |- (((et /\ y e. RR) /\ j e. Z) -> (A.k e. W A.m e. W ((jRk /\ jRm) -> th) -> A.k e. W A.m e. W ((jRk /\ jRm) -> ta)))
36	35	r19.22dva 1731	. . . . . 6 |- ((et /\ y e. RR) -> (E.j e. Z A.k e. W A.m e. W ((jRk /\ jRm) -> th) -> E.j e. Z A.k e. W A.m e. W ((jRk /\ jRm) -> ta)))
37	36	adantrl 394	. . . . 5 |- ((et /\ (A.x e. RR (0 < x -> E.j e. Z A.k e. W (jRk -> ph)) /\ y e. RR)) -> (E.j e. Z A.k e. W A.m e. W ((jRk /\ jRm) -> th) -> E.j e. Z A.k e. W A.m e. W ((jRk /\ jRm) -> ta)))
38	29, 37	syld 27	. . . 4 |- ((et /\ (A.x e. RR (0 < x -> E.j e. Z A.k e. W (jRk -> ph)) /\ y e. RR)) -> (0 < y -> E.j e. Z A.k