Theorem cvg3 6868

Description: A relationship used to derive two ways to express convergence. ph is ph(k).

Hypotheses

Ref	Expression
cvg3.1	|- M e. ZZ
cvg3.2	|- (ZZ>` M) (_ Z
cvg3.3	|- Z (_ ZZ
cvg3.4	|- N e. ZZ
cvg3.5	|- (ZZ>` N) (_ W
cvg3.6	|- W (_ ZZ

Assertion

Ref	Expression
cvg3	|- (E.j e. ZZ A.k e. ZZ (j <_ k -> ph) <-> E.j e. Z A.k e. W (j <_ k -> ph))

Distinct variable groups:   j,k,M   k,N   k,W   j,Z,k   ph,j

Proof of Theorem cvg3

Step	Hyp	Ref	Expression
1		breq1 2617	. . . . 5 |- (j = m -> (j <_ k <-> m <_ k))
2	1	imbi1d 612	. . . 4 |- (j = m -> ((j <_ k -> ph) <-> (m <_ k -> ph)))
3	2	ralbidv 1660	. . 3 |- (j = m -> (A.k e. ZZ (j <_ k -> ph) <-> A.k e. ZZ (m <_ k -> ph)))
4	3	cbvrexv 1797	. 2 |- (E.j e. ZZ A.k e. ZZ (j <_ k -> ph) <-> E.m e. ZZ A.k e. ZZ (m <_ k -> ph))
5		cvg3.1	. . . . . . . 8 |- M e. ZZ
6	5	zre 6096	. . . . . . 7 |- M e. RR
7	6	a1i 8	. . . . . 6 |- (m e. ZZ -> M e. RR)
8		zret 6094	. . . . . 6 |- (m e. ZZ -> m e. RR)
9	3	rcla4ev 1873	. . . . . . . 8 |- ((m e. Z /\ A.k e. ZZ (m <_ k -> ph)) -> E.j e. Z A.k e. ZZ (j <_ k -> ph))
10	5	eluz1 6362	. . . . . . . . 9 |- (m e. (ZZ>` M) <-> (m e. ZZ /\ M <_ m))
11		cvg3.2	. . . . . . . . . 10 |- (ZZ>` M) (_ Z
12	11	sseli 2061	. . . . . . . . 9 |- (m e. (ZZ>` M) -> m e. Z)
13	10, 12	sylbir 201	. . . . . . . 8 |- ((m e. ZZ /\ M <_ m) -> m e. Z)
14	9, 13	sylan 448	. . . . . . 7 |- (((m e. ZZ /\ M <_ m) /\ A.k e. ZZ (m <_ k -> ph)) -> E.j e. Z A.k e. ZZ (j <_ k -> ph))
15	14	ex 373	. . . . . 6 |- ((m e. ZZ /\ M <_ m) -> (A.k e. ZZ (m <_ k -> ph) -> E.j e. Z A.k e. ZZ (j <_ k -> ph)))
16		letrt 5506	. . . . . . . . . . . . . 14 |- ((m e. RR /\ M e. RR /\ k e. RR) -> ((m <_ M /\ M <_ k) -> m <_ k))
17	6, 16	mp3an2 902	. . . . . . . . . . . . 13 |- ((m e. RR /\ k e. RR) -> ((m <_ M /\ M <_ k) -> m <_ k))
18		zret 6094	. . . . . . . . . . . . 13 |- (k e. ZZ -> k e. RR)
19	17, 8, 18	syl2an 454	. . . . . . . . . . . 12 |- ((m e. ZZ /\ k e. ZZ) -> ((m <_ M /\ M <_ k) -> m <_ k))
20	19	exp3a 375	. . . . . . . . . . 11 |- ((m e. ZZ /\ k e. ZZ) -> (m <_ M -> (M <_ k -> m <_ k)))
21	20	imp 350	. . . . . . . . . 10 |- (((m e. ZZ /\ k e. ZZ) /\ m <_ M) -> (M <_ k -> m <_ k))
22	21	an1rs 489	. . . . . . . . 9 |- (((m e. ZZ /\ m <_ M) /\ k e. ZZ) -> (M <_ k -> m <_ k))
23	22	imim1d 28	. . . . . . . 8 |- (((m e. ZZ /\ m <_ M) /\ k e. ZZ) -> ((m <_ k -> ph) -> (M <_ k -> ph)))
24	23	r19.20dva 1706	. . . . . . 7 |- ((m e. ZZ /\ m <_ M) -> (A.k e. ZZ (m <_ k -> ph) -> A.k e. ZZ (M <_ k -> ph)))
25		uzidt 6367	. . . . . . . . . 10 |- (M e. ZZ -> M e. (ZZ>` M))
26	5, 25	ax-mp 7	. . . . . . . . 9 |- M e. (ZZ>` M)
27	11, 26	sselii 2062	. . . . . . . 8 |- M e. Z
28		breq1 2617	. . . . . . . . . . 11 |- (j = M -> (j <_ k <-> M <_ k))
29	28	imbi1d 612	. . . . . . . . . 10 |- (j = M -> ((j <_ k -> ph) <-> (M <_ k -> ph)))
30	29	ralbidv 1660	. . . . . . . . 9 |- (j = M -> (A.k e. ZZ (j <_ k -> ph) <-> A.k e. ZZ (M <_ k -> ph)))
31	30	rcla4ev 1873	. . . . . . . 8 |- ((M e. Z /\ A.k e. ZZ (M <_ k -> ph)) -> E.j e. Z A.k e. ZZ (j <_ k -> ph))
32	27, 31	mpan 694	. . . . . . 7 |- (A.k e. ZZ (M <_ k -> ph) -> E.j e. Z A.k e. ZZ (j <_ k -> ph))
33	24, 32	syl6 22	. . . . . 6 |- ((m e. ZZ /\ m <_ M) -> (A.k e. ZZ (m <_ k -> ph) -> E.j e. Z A.k e. ZZ (j <_ k -> ph)))
34	7, 8, 15, 33	lecase 5603	. . . . 5 |- (m e. ZZ -> (A.k e. ZZ (m <_ k -> ph) -> E.j e. Z A.k e. ZZ (j <_ k -> ph)))
35	34	r19.23aiv 1740	. . . 4 |- (E.m e. ZZ A.k e. ZZ (m <_ k -> ph) -> E.j e. Z A.k e. ZZ (j <_ k -> ph))
36		cvg3.6	. . . . . 6 |- W (_ ZZ
37		ssralv 2110	. . . . . 6 |- (W (_ ZZ -> (A.k e. ZZ (j <_ k -> ph) -> A.k e. W (j <_ k -> ph)))
38	36, 37	ax-mp 7	. . . . 5 |- (A.k e. ZZ (j <_ k -> ph) -> A.k e. W (j <_ k -> ph))
39	38	r19.22si 1731	. . . 4 |- (E.j e. Z A.k e. ZZ (j <_ k -> ph) -> E.j e. Z A.k e. W (j <_ k -> ph))
40	35, 39	syl 10	. . 3 |- (E.m e. ZZ A.k e. ZZ (m <_ k -> ph) -> E.j e. Z A.k e. W (j <_ k -> ph))
41		cvg3.3	. . . . . . . 8 |- Z (_ ZZ
42	41	sseli 2061	. . . . . . 7 |- (j e. Z -> j e. ZZ)
43		zret 6094	. . . . . . 7 |- (j e. ZZ -> j e. RR)
44	42, 43	syl 10	. . . . . 6 |- (j e. Z -> j e. RR)
45		cvg3.4	. . . . . . . 8 |- N e. ZZ
46	45	zre 6096	. . . . . . 7 |- N e. RR
47		letrit 5602	. . . . . . 7 |- ((N e. RR /\ j e. RR) -> (N <_ j \/ j <_ N))
48	46, 47	mpan 694	. . . . . 6 |- (j e. RR -> (N <_ j \/ j <_ N))
49	44, 48	syl 10	. . . . 5 |- (j e. Z -> (N <_ j \/ j <_ N))
50		letrt 5506	. . . . . . . . . . . . . . . . 17 |- ((N e. RR /\ j e. RR /\ k e. RR) -> ((N <_ j /\ j <_ k) -> N <_ k))
51	46, 50	mp3an1 901	. . . . . . . . . . . . . . . 16 |- ((j e. RR /\ k e. RR) -> ((N <_ j /\ j <_ k) -> N <_ k))
52	51, 44, 18	syl2an 454	. . . . . . . . . . . . . . 15 |- ((j e. Z /\ k e. ZZ) -> ((N <_ j /\ j <_ k) -> N <_ k))
53	52	exp3a 375	. . . . . . . . . . . . . 14 |- ((j e. Z /\ k e. ZZ) -> (N <_ j -> (j <_ k -> N <_ k)))
54	53	imp 350	. . . . . . . . . . . . 13 |- (((j e. Z /\ k e. ZZ) /\ N <_ j) -> (j <_ k -> N <_ k))
55	54	an1rs 489	. . . . . . . . . . . 12 |- (((j e. Z /\ N <_ j) /\ k e. ZZ) -> (j <_ k -> N <_ k))
56	55	ancrd 299	. . . . . . . . . . 11 |- (((j e. Z /\ N <_ j) /\ k e. ZZ) -> (j <_ k -> (N <_ k /\ j <_ k)))
57	56	imim1d 28	. . . . . . . . . 10 |- (((j e. Z /\ N <_ j) /\ k e. ZZ) -> (((N <_ k /\ j <_ k) -> ph) -> (j <_ k -> ph)))
58	57	r19.20dva 1706	. . . . . . . . 9 |- ((j e. Z /\ N <_ j) -> (A.k e. ZZ ((N <_ k /\ j <_ k) -> ph) -> A.k e. ZZ (j <_ k -> ph)))
59	42	adantr 389	. . . . . . . . 9 |- ((j e. Z /\ N <_ j) -> j e. ZZ)
60	58, 59	jctild 600	. . . . . . . 8 |- ((j e. Z /\ N <_ j) -> (A.k e. ZZ ((N <_ k /\ j <_ k) -> ph) -> (j e. ZZ /\ A.k e. ZZ (j <_ k -> ph))))
61		breq1 2617	. . . . . . . . . . 11 |- (m = j -> (m <_ k <-> j <_ k))
62	61	imbi1d 612	. . . . . . . . . 10 |- (m = j -> ((m <_ k -> ph) <-> (j <_ k -> ph)))
63	62	ralbidv 1660	. . . . . . . . 9 |- (m = j -> (A.k e. ZZ (m <_ k -> ph) <-> A.k e. ZZ (j <_ k -> ph)))
64	63	rcla4ev 1873	. . . . . . . 8 |- ((j e. ZZ /\ A.k e. ZZ (j <_ k -> ph)) -> E.m e. ZZ A.k e. ZZ (m <_ k -> ph))
65	60, 64	syl6 22	. . . . . . 7 |- ((j e. Z /\ N <_ j) -> (A.k e. ZZ ((N <_ k /\ j <_ k) -> ph) -> E.m e. ZZ A.k e. ZZ (m <_ k -> ph)))
66	45	a1i 8	. . . . . . . . . 10 |- (A.k e. ZZ ((N <_ k /\ j <_ k) -> ph) -> N e. ZZ)
67	66	a1i 8	. . . . . . . . 9 |- ((j e. Z /\ j <_ N) -> (A.k e. ZZ ((N <_ k /\ j <_ k) -> ph) -> N e. ZZ))
68		letrt 5506	. . . . . . . . . . . . . . . . 17 |- ((j e. RR /\ N e. RR /\ k e. RR) -> ((j <_ N /\ N <_ k) -> j <_ k))
69	46, 68	mp3an2 902	. . . . . . . . . . . . . . . 16 |- ((j e. RR /\ k e. RR) -> ((j <_ N /\ N <_ k) -> j <_ k))
70	69, 44, 18	syl2an 454	. . . . . . . . . . . . . . 15 |- ((j e. Z /\ k e. ZZ) -> ((j <_ N /\ N <_ k) -> j <_ k))
71	70	exp3a 375	. . . . . . . . . . . . . 14 |- ((j e. Z /\ k e. ZZ) -> (j <_ N -> (N <_ k -> j <_ k)))
72	71	imp 350	. . . . . . . . . . . . 13 |- (((j e. Z /\ k e. ZZ) /\ j <_ N) -> (N <_ k -> j <_ k))
73	72	an1rs 489	. . . . . . . . . . . 12 |- (((j e. Z /\ j <_ N) /\ k e. ZZ) -> (N <_ k -> j <_ k))
74	73	ancld 298	. . . . . . . . . . 11 |- (((j e. Z /\ j <_ N) /\ k e. ZZ) -> (N <_ k -> (N <_ k /\ j <_ k)))
75	74	imim1d 28	. . . . . . . . . 10