Theorem cau5i 6854

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

Hypotheses

Ref	Expression
cau5i.1	|- M e. ZZ
cau5i.1a	|- Z = (ZZ>` M)
cau5i.2	|- W (_ ZZ
cau5i.3	|- U (_ ZZ

Assertion

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

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

Proof of Theorem cau5i

Step	Hyp	Ref	Expression
1		zret 6086	. . . . 5 |- (n e. ZZ -> n e. RR)
2		cau5i.1	. . . . . . 7 |- M e. ZZ
3	2	zre 6088	. . . . . 6 |- M e. RR
4	3	a1i 8	. . . . 5 |- (n e. ZZ -> M e. RR)
5		letrt 5498	. . . . . . . . . . . . . . . . . . 19 |- ((n e. RR /\ M e. RR /\ j e. RR) -> ((n <_ M /\ M <_ j) -> n <_ j))
6	3, 5	mp3an2 901	. . . . . . . . . . . . . . . . . 18 |- ((n e. RR /\ j e. RR) -> ((n <_ M /\ M <_ j) -> n <_ j))
7		zret 6086	. . . . . . . . . . . . . . . . . 18 |- (j e. ZZ -> j e. RR)
8	6, 7	sylan2 451	. . . . . . . . . . . . . . . . 17 |- ((n e. RR /\ j e. ZZ) -> ((n <_ M /\ M <_ j) -> n <_ j))
9		letrt 5498	. . . . . . . . . . . . . . . . . . 19 |- ((n e. RR /\ M e. RR /\ k e. RR) -> ((n <_ M /\ M <_ k) -> n <_ k))
10	3, 9	mp3an2 901	. . . . . . . . . . . . . . . . . 18 |- ((n e. RR /\ k e. RR) -> ((n <_ M /\ M <_ k) -> n <_ k))
11		zret 6086	. . . . . . . . . . . . . . . . . 18 |- (k e. ZZ -> k e. RR)
12	10, 11	sylan2 451	. . . . . . . . . . . . . . . . 17 |- ((n e. RR /\ k e. ZZ) -> ((n <_ M /\ M <_ k) -> n <_ k))
13	8, 12	im2anan9 561	. . . . . . . . . . . . . . . 16 |- (((n e. RR /\ j e. ZZ) /\ (n e. RR /\ k e. ZZ)) -> (((n <_ M /\ M <_ j) /\ (n <_ M /\ M <_ k)) -> (n <_ j /\ n <_ k)))
14	13	anandis 511	. . . . . . . . . . . . . . 15 |- ((n e. RR /\ (j e. ZZ /\ k e. ZZ)) -> (((n <_ M /\ M <_ j) /\ (n <_ M /\ M <_ k)) -> (n <_ j /\ n <_ k)))
15	14, 1	sylan 448	. . . . . . . . . . . . . 14 |- ((n e. ZZ /\ (j e. ZZ /\ k e. ZZ)) -> (((n <_ M /\ M <_ j) /\ (n <_ M /\ M <_ k)) -> (n <_ j /\ n <_ k)))
16		anandi 509	. . . . . . . . . . . . . 14 |- ((n <_ M /\ (M <_ j /\ M <_ k)) <-> ((n <_ M /\ M <_ j) /\ (n <_ M /\ M <_ k)))
17	15, 16	syl5ib 206	. . . . . . . . . . . . 13 |- ((n e. ZZ /\ (j e. ZZ /\ k e. ZZ)) -> ((n <_ M /\ (M <_ j /\ M <_ k)) -> (n <_ j /\ n <_ k)))
18	17	exp3a 375	. . . . . . . . . . . 12 |- ((n e. ZZ /\ (j e. ZZ /\ k e. ZZ)) -> (n <_ M -> ((M <_ j /\ M <_ k) -> (n <_ j /\ n <_ k))))
19	18	imp 350	. . . . . . . . . . 11 |- (((n e. ZZ /\ (j e. ZZ /\ k e. ZZ)) /\ n <_ M) -> ((M <_ j /\ M <_ k) -> (n <_ j /\ n <_ k)))
20	19	an1rs 488	. . . . . . . . . 10 |- (((n e. ZZ /\ n <_ M) /\ (j e. ZZ /\ k e. ZZ)) -> ((M <_ j /\ M <_ k) -> (n <_ j /\ n <_ k)))
21	20	anassrs 441	. . . . . . . . 9 |- ((((n e. ZZ /\ n <_ M) /\ j e. ZZ) /\ k e. ZZ) -> ((M <_ j /\ M <_ k) -> (n <_ j /\ n <_ k)))
22	21	imim1d 28	. . . . . . . 8 |- ((((n e. ZZ /\ n <_ M) /\ j e. ZZ) /\ k e. ZZ) -> (((n <_ j /\ n <_ k) -> ph) -> ((M <_ j /\ M <_ k) -> ph)))
23	22	r19.20dva 1701	. . . . . . 7 |- (((n e. ZZ /\ n <_ M) /\ j e. ZZ) -> (A.k e. ZZ ((n <_ j /\ n <_ k) -> ph) -> A.k e. ZZ ((M <_ j /\ M <_ k) -> ph)))
24	23	r19.20dva 1701	. . . . . 6 |- ((n e. ZZ /\ n <_ M) -> (A.j e. ZZ A.k e. ZZ ((n <_ j /\ n <_ k) -> ph) -> A.j e. ZZ A.k e. ZZ ((M <_ j /\ M <_ k) -> ph)))
25		uzidt 6359	. . . . . . . 8 |- (M e. ZZ -> M e. (ZZ>` M))
26	2, 25	ax-mp 7	. . . . . . 7 |- M e. (ZZ>` M)
27		breq1 2612	. . . . . . . . . . 11 |- (m = M -> (m <_ j <-> M <_ j))
28		breq1 2612	. . . . . . . . . . 11 |- (m = M -> (m <_ k <-> M <_ k))
29	27, 28	anbi12d 626	. . . . . . . . . 10 |- (m = M -> ((m <_ j /\ m <_ k) <-> (M <_ j /\ M <_ k)))
30	29	imbi1d 611	. . . . . . . . 9 |- (m = M -> (((m <_ j /\ m <_ k) -> ph) <-> ((M <_ j /\ M <_ k) -> ph)))
31	30	2ralbidv 1672	. . . . . . . 8 |- (m = M -> (A.j e. ZZ A.k e. ZZ ((m <_ j /\ m <_ k) -> ph) <-> A.j e. ZZ A.k e. ZZ ((M <_ j /\ M <_ k) -> ph)))
32	31	rcla4ev 1868	. . . . . . 7 |- ((M e. (ZZ>` M) /\ A.j e. ZZ A.k e. ZZ ((M <_ j /\ M <_ k) -> ph)) -> E.m e. (ZZ>` M)A.j e. ZZ A.k e. ZZ ((m <_ j /\ m <_ k) -> ph))
33	26, 32	mpan 693	. . . . . 6 |- (A.j e. ZZ A.k e. ZZ ((M <_ j /\ M <_ k) -> ph) -> E.m e. (ZZ>` M)A.j e. ZZ A.k e. ZZ ((m <_ j /\ m <_ k) -> ph))
34	24, 33	syl6 22	. . . . 5 |- ((n e. ZZ /\ n <_ M) -> (A.j e. ZZ A.k e. ZZ ((n <_ j /\ n <_ k) -> ph) -> E.m e. (ZZ>` M)A.j e. ZZ A.k e. ZZ ((m <_ j /\ m <_ k) -> ph)))
35	2	eluz1 6354	. . . . . 6 |- (n e. (ZZ>` M) <-> (n e. ZZ /\ M <_ n))
36		breq1 2612	. . . . . . . . . . 11 |- (m = n -> (m <_ j <-> n <_ j))
37		breq1 2612	. . . . . . . . . . 11 |- (m = n -> (m <_ k <-> n <_ k))
38	36, 37	anbi12d 626	. . . . . . . . . 10 |- (m = n -> ((m <_ j /\ m <_ k) <-> (n <_ j /\ n <_ k)))
39	38	imbi1d 611	. . . . . . . . 9 |- (m = n -> (((m <_ j /\ m <_ k) -> ph) <-> ((n <_ j /\ n <_ k) -> ph)))
40	39	2ralbidv 1672	. . . . . . . 8 |- (m = n -> (A.j e. ZZ A.k e. ZZ ((m <_ j /\ m <_ k) -> ph) <-> A.j e. ZZ A.k e. ZZ ((n <_ j /\ n <_ k) -> ph)))
41	40	rcla4ev 1868	. . . . . . 7 |- ((n e. (ZZ>` M) /\ A.j e. ZZ A.k e. ZZ ((n <_ j /\ n <_ k) -> ph)) -> E.m e. (ZZ>` M)A.j e. ZZ A.k e. ZZ ((m <_ j /\ m <_ k) -> ph))
42	41	ex 373	. . . . . 6 |- (n e. (ZZ>` M) -> (A.j e. ZZ A.k e. ZZ ((n <_ j /\ n <_ k) -> ph) -> E.m e. (ZZ>` M)A.j e. ZZ A.k e. ZZ ((m <_ j /\ m <_ k) -> ph)))
43	35, 42	sylbir 201	. . . . 5 |- ((n e. ZZ /\ M <_ n) -> (A.j e. ZZ A.k e. ZZ ((n <_ j /\ n <_ k) -> ph) -> E.m e. (ZZ>` M)A.j e. ZZ A.k e. ZZ ((m <_ j /\ m <_ k) -> ph)))
44	1, 4, 34, 43	lecase 5595	. . . 4 |- (n e. ZZ -> (A.j e. ZZ A.k e. ZZ ((n <_ j /\ n <_ k) -> ph) -> E.m e. (ZZ>` M)A.j e. ZZ A.k e. ZZ ((m <_ j /\ m <_ k) -> ph)))
45	44	r19.23aiv 1735	. . 3 |- (E.n e. ZZ A.j e. ZZ A.k e. ZZ ((n <_ j /\ n <_ k) -> ph) -> E.m e. (ZZ>` M)A.j e. ZZ A.k e. ZZ ((m <_ j /\ m <_ k) -> ph))
46		cau5i.2	. . . . . . 7 |- W (_ ZZ
47	46	sseli 2055	. . . . . 6 |- (j e. W -> j e. ZZ)
48		cau5i.3	. . . . . . . . 9 |- U (_ ZZ
49	48	sseli 2055	. . . . . . . 8 |- (k e. U -> k e. ZZ)
50	49	imim1i 16	. . . . . . 7 |- ((k e. ZZ -> ((m <_ j /\ m <_ k) -> ph)) -> (k e. U -> ((m <_ j /\ m <_ k) -> ph)))
51	50	r19.20i2 1695	. . . . . 6 |- (A.k e. ZZ ((m <_ j /\ m <_ k) -> ph) -> A.k e. U ((m <_ j /\ m <_ k) -> ph))
52	47, 51	imim12i 18	. . . . 5 |- ((j e. ZZ -> A.k e. ZZ ((m <_ j /\ m <_ k) -> ph)) -> (j e. W -> A.k e. U ((m <_ j /\ m <_ k) -> ph)))
53	52	r19.20i2 1695	. . . 4 |- (A.j e. ZZ A.k e. ZZ ((m <_ j /\ m <_ k) -> ph) -> A.j e. W A.k e. U ((m <_ j /\ m <_ k) -> ph))
54	53	r19.22si 1726	. . 3 |- (E.m e. (ZZ>` M)A.j e. ZZ A.k e. ZZ ((m <_ j /\ m <_ k) -> ph) -> E.m e. (ZZ>` M)A.j e. W A.k e. U ((m <_ j /\ m <_ k) -> ph))
55	45, 54	syl 10	. 2 |- (