Theorem bcthlem2 7950

Description: Lemma for bcth 7982. For any m, we can always find a greater n meeting the convergence criterion.

Assertion

Ref	Expression
bcthlem2	|- (((m e. NN /\ j e. NN) /\ A.k e. NN (j <_ k -> (((1st o. g)` k)Dq) < S)) -> E.n e. NN (m < n /\ (((1st o. g)` n)Dq) < S))

Distinct variable groups:   k,n,D   S,k,n   g,k,n   j,k,n   k,m,n   k,q,n

Proof of Theorem bcthlem2

Step	Hyp	Ref	Expression
1		breq2 2618	. . . . . . 7 |- (k = j -> (j <_ k <-> j <_ j))
2		fveq2 3715	. . . . . . . . 9 |- (k = j -> ((1st o. g)` k) = ((1st o. g)` j))
3	2	opreq1d 3966	. . . . . . . 8 |- (k = j -> (((1st o. g)` k)Dq) = (((1st o. g)` j)Dq))
4	3	breq1d 2624	. . . . . . 7 |- (k = j -> ((((1st o. g)` k)Dq) < S <-> (((1st o. g)` j)Dq) < S))
5	1, 4	imbi12d 625	. . . . . 6 |- (k = j -> ((j <_ k -> (((1st o. g)` k)Dq) < S) <-> (j <_ j -> (((1st o. g)` j)Dq) < S)))
6	5	rcla4v 1869	. . . . 5 |- (j e. NN -> (A.k e. NN (j <_ k -> (((1st o. g)` k)Dq) < S) -> (j <_ j -> (((1st o. g)` j)Dq) < S)))
7	6	ad2antlr 405	. . . 4 |- (((m e. NN /\ j e. NN) /\ m < j) -> (A.k e. NN (j <_ k -> (((1st o. g)` k)Dq) < S) -> (j <_ j -> (((1st o. g)` j)Dq) < S)))
8		nnret 5885	. . . . . . . 8 |- (j e. NN -> j e. RR)
9		leidt 5512	. . . . . . . 8 |- (j e. RR -> j <_ j)
10	8, 9	syl 10	. . . . . . 7 |- (j e. NN -> j <_ j)
11	10	ad2antlr 405	. . . . . 6 |- (((m e. NN /\ j e. NN) /\ m < j) -> j <_ j)
12		pm2.27 62	. . . . . 6 |- (j <_ j -> ((j <_ j -> (((1st o. g)` j)Dq) < S) -> (((1st o. g)` j)Dq) < S))
13	11, 12	syl 10	. . . . 5 |- (((m e. NN /\ j e. NN) /\ m < j) -> ((j <_ j -> (((1st o. g)` j)Dq) < S) -> (((1st o. g)` j)Dq) < S))
14		breq2 2618	. . . . . . . . 9 |- (n = j -> (m < n <-> m < j))
15		fveq2 3715	. . . . . . . . . . 11 |- (n = j -> ((1st o. g)` n) = ((1st o. g)` j))
16	15	opreq1d 3966	. . . . . . . . . 10 |- (n = j -> (((1st o. g)` n)Dq) = (((1st o. g)` j)Dq))
17	16	breq1d 2624	. . . . . . . . 9 |- (n = j -> ((((1st o. g)` n)Dq) < S <-> (((1st o. g)` j)Dq) < S))
18	14, 17	anbi12d 627	. . . . . . . 8 |- (n = j -> ((m < n /\ (((1st o. g)` n)Dq) < S) <-> (m < j /\ (((1st o. g)` j)Dq) < S)))
19	18	rcla4ev 1873	. . . . . . 7 |- ((j e. NN /\ (m < j /\ (((1st o. g)` j)Dq) < S)) -> E.n e. NN (m < n /\ (((1st o. g)` n)Dq) < S))
20		simplr 413	. . . . . . . 8 |- (((m e. NN /\ j e. NN) /\ m < j) -> j e. NN)
21	20	adantr 389	. . . . . . 7 |- ((((m e. NN /\ j e. NN) /\ m < j) /\ (((1st o. g)` j)Dq) < S) -> j e. NN)
22		id 59	. . . . . . . 8 |- ((m < j /\ (((1st o. g)` j)Dq) < S) -> (m < j /\ (((1st o. g)` j)Dq) < S))
23	22	adantll 392	. . . . . . 7 |- ((((m e. NN /\ j e. NN) /\ m < j) /\ (((1st o. g)` j)Dq) < S) -> (m < j /\ (((1st o. g)` j)Dq) < S))
24	19, 21, 23	sylanc 471	. . . . . 6 |- ((((m e. NN /\ j e. NN) /\ m < j) /\ (((1st o. g)` j)Dq) < S) -> E.n e. NN (m < n /\ (((1st o. g)` n)Dq) < S))
25	24	ex 373	. . . . 5 |- (((m e. NN /\ j e. NN) /\ m < j) -> ((((1st o. g)` j)Dq) < S -> E.n e. NN (m < n /\ (((1st o. g)` n)Dq) < S)))
26	13, 25	syld 27	. . . 4 |- (((m e. NN /\ j e. NN) /\ m < j) -> ((j <_ j -> (((1st o. g)` j)Dq) < S) -> E.n e. NN (m < n /\ (((1st o. g)` n)Dq) < S)))
27	7, 26	syld 27	. . 3 |- (((m e. NN /\ j e. NN) /\ m < j) -> (A.k e. NN (j <_ k -> (((1st o. g)` k)Dq) < S) -> E.n e. NN (m < n /\ (((1st o. g)` n)Dq) < S)))
28		peano2nn 5891	. . . . . 6 |- (m e. NN -> (m + 1) e. NN)
29		breq2 2618	. . . . . . . 8 |- (k = (m + 1) -> (j <_ k <-> j <_ (m + 1)))
30		fveq2 3715	. . . . . . . . . 10 |- (k = (m + 1) -> ((1st o. g)` k) = ((1st o. g)` (m + 1)))
31	30	opreq1d 3966	. . . . . . . . 9 |- (k = (m + 1) -> (((1st o. g)` k)Dq) = (((1st o. g)` (m + 1))Dq))
32	31	breq1d 2624	. . . . . . . 8 |- (k = (m + 1) -> ((((1st o. g)` k)Dq) < S <-> (((1st o. g)` (m + 1))Dq) < S))
33	29, 32	imbi12d 625	. . . . . . 7 |- (k = (m + 1) -> ((j <_ k -> (((1st o. g)` k)Dq) < S) <-> (j <_ (m + 1) -> (((1st o. g)` (m + 1))Dq) < S)))
34	33	rcla4v 1869	. . . . . 6 |- ((m + 1) e. NN -> (A.k e. NN (j <_ k -> (((1st o. g)` k)Dq) < S) -> (j <_ (m + 1) -> (((1st o. g)` (m + 1))Dq) < S)))
35	28, 34	syl 10	. . . . 5 |- (m e. NN -> (A.k e. NN (j <_ k -> (((1st o. g)` k)Dq) < S) -> (j <_ (m + 1) -> (((1st o. g)` (m + 1))Dq) < S)))
36	35	ad2antrr 404	. . . 4 |- (((m e. NN /\ j e. NN) /\ j <_ m) -> (A.k e. NN (j <_ k -> (((1st o. g)` k)Dq) < S) -> (j <_ (m + 1) -> (((1st o. g)` (m + 1))Dq) < S)))
37		nnret 5885	. . . . . . . . . 10 |- (m e. NN -> m e. RR)
38		lep1t 5776	. . . . . . . . . 10 |- (m e. RR -> m <_ (m + 1))
39	37, 38	syl 10	. . . . . . . . 9 |- (m e. NN -> m <_ (m + 1))
40	39	adantr 389	. . . . . . . 8 |- ((m e. NN /\ j e. NN) -> m <_ (m + 1))
41		letrt 5506	. . . . . . . . 9 |- ((j e. RR /\ m e. RR /\ (m + 1) e. RR) -> ((j <_ m /\ m <_ (m + 1)) -> j <_ (m + 1)))
42	8	adantl 388	. . . . . . . . 9 |- ((m e. NN /\ j e. NN) -> j e. RR)
43	37	adantr 389	. . . . . . . . 9 |- ((m e. NN /\ j e. NN) -> m e. RR)
44		peano2re 5416	. . . . . . . . . . 11 |- (m e. RR -> (m + 1) e. RR)
45	37, 44	syl 10	. . . . . . . . . 10 |- (m e. NN -> (m + 1) e. RR)
46	45	adantr 389	. . . . . . . . 9 |- ((m e. NN /\ j e. NN) -> (m + 1) e. RR)
47	41, 42, 43, 46	syl3anc 857	. . . . . . . 8 |- ((m e. NN /\ j e. NN) -> ((j <_ m /\ m <_ (m + 1)) -> j <_ (m + 1)))
48	40, 47	mpan2d 701	. . . . . . 7 |- ((m e. NN /\ j e. NN) -> (j <_ m -> j <_ (m + 1)))
49	48	imp 350	. . . . . 6 |- (((m e. NN /\ j e. NN) /\ j <_ m) -> j <_ (m + 1))
50		pm2.27 62	. . . . . 6 |- (j <_ (m + 1) -> ((j <_ (m + 1) -> (((1st o. g)` (m + 1))Dq) < S) -> (((1st o. g)` (m + 1))Dq) < S))
51	49, 50	syl 10	. . . . 5 |- (((m e. NN /\ j e. NN) /\ j <_ m) -> ((j <_ (m + 1) -> (((1st o. g)` (m + 1))Dq) < S) -> (((1st o. g)` (m + 1))Dq) < S))
52		breq2 2618	. . . . . . . . 9 |- (n = (m + 1) -> (m < n <-> m < (m + 1)))
53		fveq2 3715	. . . . . . . . . . 11 |- (n