Theorem cvg3 6923

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 2627	. . . . 5 |- (j = m -> (j <_ k <-> m <_ k))
2	1	imbi1d 615	. . . 4 |- (j = m -> ((j <_ k -> ph) <-> (m <_ k -> ph)))
3	2	ralbidv 1666	. . 3 |- (j = m -> (A.k e. ZZ (j <_ k -> ph) <-> A.k e. ZZ (m <_ k -> ph)))
4	3	cbvrexv 1804	. 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 6143	. . . . . . 7 |- M e. RR
7	6	a1i 8	. . . . . 6 |- (m e. ZZ -> M e. RR)
8		zret 6141	. . . . . 6 |- (m e. ZZ -> m e. RR)
9	3	rcla4ev 1880	. . . . . . . 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 6423	. . . . . . . . 9 |- (m e. (ZZ>` M) <-> (m e. ZZ /\ M <_ m))
11		cvg3.2	. . . . . . . . . 10 |- (ZZ>` M) (_ Z
12	11	sseli 2068	. . . . . . . . 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 450	. . . . . . 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 5537	. . . . . . . . . . . . 13 |- ((m e. RR /\ M e. RR /\ k e. RR) -> ((m <_ M /\ M <_ k) -> m <_ k))
17	6, 16	mp3an2 906	. . . . . . . . . . . 12 |- ((m e. RR /\ k e. RR) -> ((m <_ M /\ M <_ k) -> m <_ k))
18		zret 6141	. . . . . . . . . . . 12 |- (k e. ZZ -> k e. RR)
19	17, 8, 18	syl2an 456	. . . . . . . . . . 11 |- ((m e. ZZ /\ k e. ZZ) -> ((m <_ M /\ M <_ k) -> m <_ k))
20	19	expdimp 377	. . . . . . . . . 10 |- (((m e. ZZ /\ k e. ZZ) /\ m <_ M) -> (M <_ k -> m <_ k))
21	20	an1rs 491	. . . . . . . . 9 |- (((m e. ZZ /\ m <_ M) /\ k e. ZZ) -> (M <_ k -> m <_ k))
22	21	imim1d 28	. . . . . . . 8 |- (((m e. ZZ /\ m <_ M) /\ k e. ZZ) -> ((m <_ k -> ph) -> (M <_ k -> ph)))
23	22	r19.20dva 1712	. . . . . . 7 |- ((m e. ZZ /\ m <_ M) -> (A.k e. ZZ (m <_ k -> ph) -> A.k e. ZZ (M <_ k -> ph)))
24		uzidt 6428	. . . . . . . . . 10 |- (M e. ZZ -> M e. (ZZ>` M))
25	5, 24	ax-mp 7	. . . . . . . . 9 |- M e. (ZZ>` M)
26	11, 25	sselii 2069	. . . . . . . 8 |- M e. Z
27		breq1 2627	. . . . . . . . . . 11 |- (j = M -> (j <_ k <-> M <_ k))
28	27	imbi1d 615	. . . . . . . . . 10 |- (j = M -> ((j <_ k -> ph) <-> (M <_ k -> ph)))
29	28	ralbidv 1666	. . . . . . . . 9 |- (j = M -> (A.k e. ZZ (j <_ k -> ph) <-> A.k e. ZZ (M <_ k -> ph)))
30	29	rcla4ev 1880	. . . . . . . 8 |- ((M e. Z /\ A.k e. ZZ (M <_ k -> ph)) -> E.j e. Z A.k e. ZZ (j <_ k -> ph))
31	26, 30	mpan 697	. . . . . . 7 |- (A.k e. ZZ (M <_ k -> ph) -> E.j e. Z A.k e. ZZ (j <_ k -> ph))
32	23, 31	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)))
33	7, 8, 15, 32	lecase 5633	. . . . 5 |- (m e. ZZ -> (A.k e. ZZ (m <_ k -> ph) -> E.j e. Z A.k e. ZZ (j <_ k -> ph)))
34	33	r19.23aiv 1746	. . . 4 |- (E.m e. ZZ A.k e. ZZ (m <_ k -> ph) -> E.j e. Z A.k e. ZZ (j <_ k -> ph))
35		cvg3.6	. . . . . 6 |- W (_ ZZ
36		ssralv 2117	. . . . . 6 |- (W (_ ZZ -> (A.k e. ZZ (j <_ k -> ph) -> A.k e. W (j <_ k -> ph)))
37	35, 36	ax-mp 7	. . . . 5 |- (A.k e. ZZ (j <_ k -> ph) -> A.k e. W (j <_ k -> ph))
38	37	r19.22si 1737	. . . 4 |- (E.j e. Z A.k e. ZZ (j <_ k -> ph) -> E.j e. Z A.k e. W (j <_ k -> ph))
39	34, 38	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))
40		cvg3.3	. . . . . . . 8 |- Z (_ ZZ
41	40	sseli 2068	. . . . . . 7 |- (j e. Z -> j e. ZZ)
42		zret 6141	. . . . . . 7 |- (j e. ZZ -> j e. RR)
43	41, 42	syl 10	. . . . . 6 |- (j e. Z -> j e. RR)
44		cvg3.4	. . . . . . . 8 |- N e. ZZ
45	44	zre 6143	. . . . . . 7 |- N e. RR
46		letrit 5632	. . . . . . 7 |- ((N e. RR /\ j e. RR) -> (N <_ j \/ j <_ N))
47	45, 46	mpan 697	. . . . . 6 |- (j e. RR -> (N <_ j \/ j <_ N))
48	43, 47	syl 10	. . . . 5 |- (j e. Z -> (N <_ j \/ j <_ N))
49		letrt 5537	. . . . . . . . . . . . . . . 16 |- ((N e. RR /\ j e. RR /\ k e. RR) -> ((N <_ j /\ j <_ k) -> N <_ k))
50	45, 49	mp3an1 905	. . . . . . . . . . . . . . 15 |- ((j e. RR /\ k e. RR) -> ((N <_ j /\ j <_ k) -> N <_ k))
51	50, 43, 18	syl2an 456	. . . . . . . . . . . . . 14 |- ((j e. Z /\ k e. ZZ) -> ((N <_ j /\ j <_ k) -> N <_ k))
52	51	expdimp 377	. . . . . . . . . . . . 13 |- (((j e. Z /\ k e. ZZ) /\ N <_ j) -> (j <_ k -> N <_ k))
53	52	an1rs 491	. . . . . . . . . . . 12 |- (((j e. Z /\ N <_ j) /\ k e. ZZ) -> (j <_ k -> N <_ k))
54	53	ancrd 299	. . . . . . . . . . 11 |- (((j e. Z /\ N <_ j) /\ k e. ZZ) -> (j <_ k -> (N <_ k /\ j <_ k)))
55	54	imim1d 28	. . . . . . . . . 10 |- (((j e. Z /\ N <_ j) /\ k e. ZZ) -> (((N <_ k /\ j <_ k) -> ph) -> (j <_ k -> ph)))
56	55	r19.20dva 1712	. . . . . . . . 9 |- ((j e. Z /\ N <_ j) -> (A.k e. ZZ ((N <_ k /\ j <_ k) -> ph) -> A.k e. ZZ (j <_ k -> ph)))
57	41	adantr 391	. . . . . . . . 9 |- ((j e. Z /\ N <_ j) -> j e. ZZ)
58	56, 57	jctild 603	. . . . . . . 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))))
59		breq1 2627	. . . . . . . . . . 11 |- (m = j -> (m <_ k <-> j <_ k))
60	59	imbi1d 615	. . . . . . . . . 10 |- (m = j -> ((m <_ k -> ph) <-> (j <_ k -> ph)))
61	60	ralbidv 1666	. . . . . . . . 9 |- (m = j -> (A.k e. ZZ (m <_ k -> ph) <-> A.k e. ZZ (j <_ k -> ph)))
62	61	rcla4ev 1880	. . . . . . . 8 |- ((j e. ZZ /\ A.k e. ZZ (j <_ k -> ph)) -> E.m e. ZZ A.k e. ZZ (m <_ k -> ph))
63	58, 62	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)))
64	44	a1i 8	. . . . . . . . . 10 |- (A.k e. ZZ ((N <_ k /\ j <_ k) -> ph) -> N e. ZZ)
65	64	a1i 8	. . . . . . . . 9 |- ((j e. Z /\ j <_ N) -> (A.k e. ZZ ((N <_ k /\ j <_ k) -> ph) -> N e. ZZ))
66		letrt 5537	. . . . . . . . . . . . . . . 16 |- ((j e. RR /\ N e. RR /\ k e. RR) -> ((j <_ N /\ N <_ k) -> j <_ k))
67	45, 66	mp3an2 906	. . . . . . . . . . . . . . 15 |- ((j e. RR /\ k e. RR) -> ((j <_ N /\ N <_ k) -> j <_ k))
68	67, 43, 18	syl2an 456	. . . . . . . . . . . . . 14 |- ((j e. Z /\ k e. ZZ) -> ((j <_ N /\ N <_ k) -> j <_ k))
69	68	expdimp 377	. . . . . . . . . . . . 13 |- (((j e. Z /\ k e. ZZ) /\ j <_ N) -> (N <_ k -> j <_ k))
70	69	an1rs 491	. . . . . . . . . . . 12 |- (((j e. Z /\ j <_ N) /\ k e. ZZ) -> (N <_ k -> j <_ k))
71	70	ancld 298	. . . . . . . . . . 11 |- (((j e. Z /\ j <_ N) /\ k e. ZZ) -> (N <_ k -> (N <_ k /\ j <_ k)))
72	71	imim1d 28	. . . . . . . . . 10 |- (((j e. Z /\ j <_ N) /\ k e. ZZ) -> (((N <_ k /\ j <_ k) -> ph) -> (N <_ k -> ph)))
73	72	r19.20dva 1712	. . . . . . . . 9 |- ((j e. Z /\ j <_ N) -> (A.k e. ZZ ((N <_ k /\ j <_ k) -> ph) -> A.k e. ZZ (N <_ k -> ph)))
74	65, 73	jcad 602	. . . . . . . 8