Theorem cau5 6856

Description: A relationship used to derive two ways to express a Cauchy sequence. ph is ph(j, k).

Hypotheses

Ref	Expression
cau4i.1	|- M e. ZZ
cau4i.2	|- Z = (ZZ>` M)

Assertion

Ref	Expression
cau5	|- (E.m e. ZZ A.j e. ZZ A.k e. ZZ ((m <_ j /\ m <_ k) -> ph) <-> E.m e. Z A.j e. Z A.k e. Z ((m <_ j /\ m <_ k) -> ph))

Distinct variable groups:   j,k,m,M   j,Z,k,m   ph,m

Proof of Theorem cau5

Step	Hyp	Ref	Expression
1		cau4i.1	. . 3 |- M e. ZZ
2		cau4i.2	. . 3 |- Z = (ZZ>` M)
3		uzssz 6362	. . . 4 |- (ZZ>` M) (_ ZZ
4	2, 3	eqsstr 2081	. . 3 |- Z (_ ZZ
5	1, 2, 4, 4	cau5i 6854	. 2 |- (E.m e. ZZ A.j e. ZZ A.k e. ZZ ((m <_ j /\ m <_ k) -> ph) -> E.m e. Z A.j e. Z A.k e. Z ((m <_ j /\ m <_ k) -> ph))
6		rexeq1 1779	. . . . 5 |- (Z = (ZZ>` M) -> (E.m e. Z A.j e. Z A.k e. Z ((m <_ j /\ m <_ k) -> ph) <-> E.m e. (ZZ>` M)A.j e. Z A.k e. Z ((m <_ j /\ m <_ k) -> ph)))
7	2, 6	ax-mp 7	. . . 4 |- (E.m e. Z A.j e. Z A.k e. Z ((m <_ j /\ m <_ k) -> ph) <-> E.m e. (ZZ>` M)A.j e. Z A.k e. Z ((m <_ j /\ m <_ k) -> ph))
8		rexuz 6376	. . . . 5 |- (M e. ZZ -> (E.m e. (ZZ>` M)A.j e. Z A.k e. Z ((m <_ j /\ m <_ k) -> ph) <-> E.m e. ZZ (M <_ m /\ A.j e. Z A.k e. Z ((m <_ j /\ m <_ k) -> ph))))
9	1, 8	ax-mp 7	. . . 4 |- (E.m e. (ZZ>` M)A.j e. Z A.k e. Z ((m <_ j /\ m <_ k) -> ph) <-> E.m e. ZZ (M <_ m /\ A.j e. Z A.k e. Z ((m <_ j /\ m <_ k) -> ph)))
10	7, 9	bitr 173	. . 3 |- (E.m e. Z A.j e. Z A.k e. Z ((m <_ j /\ m <_ k) -> ph) <-> E.m e. ZZ (M <_ m /\ A.j e. Z A.k e. Z ((m <_ j /\ m <_ k) -> ph)))
11	1	zre 6088	. . . . . . . . . . . . . . . . . . . . . 22 |- M e. RR
12		letrt 5498	. . . . . . . . . . . . . . . . . . . . . 22 |- ((M e. RR /\ m e. RR /\ j e. RR) -> ((M <_ m /\ m <_ j) -> M <_ j))
13	11, 12	mp3an1 900	. . . . . . . . . . . . . . . . . . . . 21 |- ((m e. RR /\ j e. RR) -> ((M <_ m /\ m <_ j) -> M <_ j))
14		letrt 5498	. . . . . . . . . . . . . . . . . . . . . 22 |- ((M e. RR /\ m e. RR /\ k e. RR) -> ((M <_ m /\ m <_ k) -> M <_ k))
15	11, 14	mp3an1 900	. . . . . . . . . . . . . . . . . . . . 21 |- ((m e. RR /\ k e. RR) -> ((M <_ m /\ m <_ k) -> M <_ k))
16	13, 15	im2anan9 561	. . . . . . . . . . . . . . . . . . . 20 |- (((m e. RR /\ j e. RR) /\ (m e. RR /\ k e. RR)) -> (((M <_ m /\ m <_ j) /\ (M <_ m /\ m <_ k)) -> (M <_ j /\ M <_ k)))
17		ancom 435	. . . . . . . . . . . . . . . . . . . 20 |- ((M <_ j /\ M <_ k) <-> (M <_ k /\ M <_ j))
18	16, 17	syl6ib 212	. . . . . . . . . . . . . . . . . . 19 |- (((m e. RR /\ j e. RR) /\ (m e. RR /\ k e. RR)) -> (((M <_ m /\ m <_ j) /\ (M <_ m /\ m <_ k)) -> (M <_ k /\ M <_ j)))
19	18	anandis 511	. . . . . . . . . . . . . . . . . 18 |- ((m e. RR /\ (j e. RR /\ k e. RR)) -> (((M <_ m /\ m <_ j) /\ (M <_ m /\ m <_ k)) -> (M <_ k /\ M <_ j)))
20		anandi 509	. . . . . . . . . . . . . . . . . 18 |- ((M <_ m /\ (m <_ j /\ m <_ k)) <-> ((M <_ m /\ m <_ j) /\ (M <_ m /\ m <_ k)))
21	19, 20	syl5ib 206	. . . . . . . . . . . . . . . . 17 |- ((m e. RR /\ (j e. RR /\ k e. RR)) -> ((M <_ m /\ (m <_ j /\ m <_ k)) -> (M <_ k /\ M <_ j)))
22		zret 6086	. . . . . . . . . . . . . . . . 17 |- (m e. ZZ -> m e. RR)
23		zret 6086	. . . . . . . . . . . . . . . . . 18 |- (j e. ZZ -> j e. RR)
24		zret 6086	. . . . . . . . . . . . . . . . . 18 |- (k e. ZZ -> k e. RR)
25	23, 24	anim12i 333	. . . . . . . . . . . . . . . . 17 |- ((j e. ZZ /\ k e. ZZ) -> (j e. RR /\ k e. RR))
26	21, 22, 25	syl2an 454	. . . . . . . . . . . . . . . 16 |- ((m e. ZZ /\ (j e. ZZ /\ k e. ZZ)) -> ((M <_ m /\ (m <_ j /\ m <_ k)) -> (M <_ k /\ M <_ j)))
27	26	exp4b 379	. . . . . . . . . . . . . . 15 |- (m e. ZZ -> ((j e. ZZ /\ k e. ZZ) -> (M <_ m -> ((m <_ j /\ m <_ k) -> (M <_ k /\ M <_ j)))))
28	27	com23 32	. . . . . . . . . . . . . 14 |- (m e. ZZ -> (M <_ m -> ((j e. ZZ /\ k e. ZZ) -> ((m <_ j /\ m <_ k) -> (M <_ k /\ M <_ j)))))
29	28	imp31 362	. . . . . . . . . . . . 13 |- (((m e. ZZ /\ M <_ m) /\ (j e. ZZ /\ k e. ZZ)) -> ((m <_ j /\ m <_ k) -> (M <_ k /\ M <_ j)))
30	29	anassrs 441	. . . . . . . . . . . 12 |- ((((m e. ZZ /\ M <_ m) /\ j e. ZZ) /\ k e. ZZ) -> ((m <_ j /\ m <_ k) -> (M <_ k /\ M <_ j)))
31	30	ancrd 299	. . . . . . . . . . 11 |- ((((m e. ZZ /\ M <_ m) /\ j e. ZZ) /\ k e. ZZ) -> ((m <_ j /\ m <_ k) -> ((M <_ k /\ M <_ j) /\ (m <_ j /\ m <_ k))))
32	31	imim1d 28	. . . . . . . . . 10 |- ((((m e. ZZ /\ M <_ m) /\ j e. ZZ) /\ k e. ZZ) -> ((((M <_ k /\ M <_ j) /\ (m <_ j /\ m <_ k)) -> ph) -> ((m <_ j /\ m <_ k) -> ph)))
33		impexp 347	. . . . . . . . . . 11 |- ((((M <_ k /\ M <_ j) /\ (m <_ j /\ m <_ k)) -> ph) <-> ((M <_ k /\ M <_ j) -> ((m <_ j /\ m <_ k) -> ph)))
34		impexp 347	. . . . . . . . . . 11 |- (((M <_ k /\ M <_ j) -> ((m <_ j /\ m <_ k) -> ph)) <-> (M <_ k -> (M <_ j -> ((m <_ j /\ m <_ k) -> ph))))
35	33, 34	bitr 173	. . . . . . . . . 10 |- ((((M <_ k /\ M <_ j) /\ (m <_ j /\ m <_ k)) -> ph) <-> (M <_ k -> (M <_ j -> ((m <_ j /\ m <_ k) -> ph))))
36	32, 35	syl5ibr 207	. . . . . . . . 9 |- ((((m e. ZZ /\ M <_ m) /\ j e. ZZ) /\ k e. ZZ) -> ((M <_ k -> (M <_ j -> ((m <_ j /\ m <_ k) -> ph))) -> ((m <_ j /\ m <_ k) -> ph)))
37	36	r19.20dva 1701	. . . . . . . 8 |- (((m e. ZZ /\ M <_ m) /\ j e. ZZ) -> (A.k e. ZZ (M <_ k -> (M <_ j -> ((m <_ j /\ m <_ k) -> ph))) -> A.k e. ZZ ((m <_ j /\ m <_ k) -> ph)))
38	37	r19.20dva 1701	. . . . . . 7 |- ((m e. ZZ /\ M <_ m) -> (A.j e. ZZ A.k e. ZZ (M <_ k -> (M <_ j -> ((m <_ j /\ m <_ k) -> ph))) -> A.j e. ZZ A.k e. ZZ ((m <_ j /\ m <_ k) -> ph)))
39		raleq1 1778	. . . . . . . . 9 |- (Z = (ZZ>` M) -> (A.j e. Z A.k e. Z ((m <_ j /\ m <_ k) -> ph) <-> A.j e. (ZZ>` M)A.k e. Z ((m <_ j /\ m <_ k) -> ph)))
40	2, 39	ax-mp 7	. . . . . . . 8 |- (A.j e. Z A.k e. Z ((m <_ j /\ m <_ k) -> ph) <-> A.j e. (ZZ>` M)A.k e. Z ((m <_ j /\ m <_ k) -> ph))
41		raluz 6374	. . . . . . . . 9 |- (M e. ZZ -> (A.j e. (ZZ>` M)A.k e. Z ((m <_ j /\ m <_ k) -> ph) <-> A.j e. ZZ (M <_ j -> A.k e. Z ((m <_ j /\ m <_ k) -> ph))))
42	1, 41	ax-mp 7	. . . . . . . 8 |- (A.j e. (ZZ>` M)A.k e. Z ((m <_ j /\ m <_ k) -> ph) <-> A.j e. ZZ (M <_ j -> A.k e. Z ((m <_ j /\ m <_ k) -> ph)))
43		raleq1 1778	. . . . . . . . . . 11 |- (Z = (ZZ>` M) -> (A.k e. Z (M <_ j -> ((m <_ j /\ m <_ k) -> ph)) <-> A.k e. (ZZ>` M)(M <_ j -> ((m <_ j /\ m <_ k) -> ph))))
44	2, 43	ax-mp 7	. . . . . . . . . 10 |- (A.k e. Z (M <_ j -> ((m <_ j /\ m <_ k) -> ph)) <-> A.k e. (ZZ>` M)(M <_ j -> ((m <_ j /\ m <_ k) -> ph)))
45		r19.21v 1708	. . . . . . . . . 10 |- (A.k e. Z (M <_ j -> ((m <_ j /\ m <_ k) -> ph)) <-> (M <_ j -> A.k e. Z ((m <_ j /\ m <_ k) -> ph)))
46