Theorem cvgrat

Description: Ratio test for convergence of a complex infinite series. If the ratio A of the absolute values of successive terms in an infinite sequence F is less than 1 for all terms beyond some index B , then the infinite sum of the terms of F converges to a complex number. Equivalent to first part of Exercise 4 of Gleason p. 182. (Contributed by NM, 26-Apr-2005) (Proof shortened by Mario Carneiro, 27-Apr-2014)

	Ref	Expression
Hypotheses	cvgrat.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	cvgrat.2	$$⊢W={\mathbb{Z}}_{\ge N}$$
	cvgrat.3	$$⊢\phi \to A\in ℝ$$
	cvgrat.4	$$⊢\phi \to A<1$$
	cvgrat.5	$$⊢\phi \to N\in Z$$
	cvgrat.6	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℂ$$
	cvgrat.7	$$⊢\left(\phi \wedge k\in W\right)\to \left|F\left(k+1\right)\right|\le A\left|F\left(k\right)\right|$$
Assertion	cvgrat	$$⊢\phi \to seqM\left(+,F\right)\in \mathrm{dom}⇝$$

Proof

Step	Hyp	Ref	Expression
1		cvgrat.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		cvgrat.2	$$⊢W={\mathbb{Z}}_{\ge N}$$
3		cvgrat.3	$$⊢\phi \to A\in ℝ$$
4		cvgrat.4	$$⊢\phi \to A<1$$
5		cvgrat.5	$$⊢\phi \to N\in Z$$
6		cvgrat.6	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℂ$$
7		cvgrat.7	$$⊢\left(\phi \wedge k\in W\right)\to \left|F\left(k+1\right)\right|\le A\left|F\left(k\right)\right|$$
8	5 1	eleqtrdi	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
9		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in \mathbb{Z}$$
10	8 9	syl	$$⊢\phi \to N\in \mathbb{Z}$$
11		uzid	$$⊢N\in \mathbb{Z}\to N\in {\mathbb{Z}}_{\ge N}$$
12	10 11	syl	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge N}$$
13	12 2	eleqtrrdi	$$⊢\phi \to N\in W$$
14		oveq1	$$⊢n=k\to n-N=k-N$$
15	14	oveq2d	$$⊢n=k\to {if\left(A\le 0,0,A\right)}^{n-N}={if\left(A\le 0,0,A\right)}^{k-N}$$
16		eqid	$$⊢\left(n\in W⟼{if\left(A\le 0,0,A\right)}^{n-N}\right)=\left(n\in W⟼{if\left(A\le 0,0,A\right)}^{n-N}\right)$$
17		ovex	$$⊢{if\left(A\le 0,0,A\right)}^{k-N}\in \mathrm{V}$$
18	15 16 17	fvmpt	$$⊢k\in W\to \left(n\in W⟼{if\left(A\le 0,0,A\right)}^{n-N}\right)\left(k\right)={if\left(A\le 0,0,A\right)}^{k-N}$$
19	18	adantl	$$⊢\left(\phi \wedge k\in W\right)\to \left(n\in W⟼{if\left(A\le 0,0,A\right)}^{n-N}\right)\left(k\right)={if\left(A\le 0,0,A\right)}^{k-N}$$
20		0re	$$⊢0\in ℝ$$
21		ifcl	$$⊢\left(0\in ℝ\wedge A\in ℝ\right)\to if\left(A\le 0,0,A\right)\in ℝ$$
22	20 3 21	sylancr	$$⊢\phi \to if\left(A\le 0,0,A\right)\in ℝ$$
23	22	adantr	$$⊢\left(\phi \wedge k\in W\right)\to if\left(A\le 0,0,A\right)\in ℝ$$
24		simpr	$$⊢\left(\phi \wedge k\in W\right)\to k\in W$$
25	24 2	eleqtrdi	$$⊢\left(\phi \wedge k\in W\right)\to k\in {\mathbb{Z}}_{\ge N}$$
26		uznn0sub	$$⊢k\in {\mathbb{Z}}_{\ge N}\to k-N\in {\mathbb{N}}_0$$
27	25 26	syl	$$⊢\left(\phi \wedge k\in W\right)\to k-N\in {\mathbb{N}}_0$$
28	23 27	reexpcld	$$⊢\left(\phi \wedge k\in W\right)\to {if\left(A\le 0,0,A\right)}^{k-N}\in ℝ$$
29	19 28	eqeltrd	$$⊢\left(\phi \wedge k\in W\right)\to \left(n\in W⟼{if\left(A\le 0,0,A\right)}^{n-N}\right)\left(k\right)\in ℝ$$
30		uzss	$$⊢N\in {\mathbb{Z}}_{\ge M}\to {\mathbb{Z}}_{\ge N}\subseteq {\mathbb{Z}}_{\ge M}$$
31	8 30	syl	$$⊢\phi \to {\mathbb{Z}}_{\ge N}\subseteq {\mathbb{Z}}_{\ge M}$$
32	31 2 1	3sstr4g	$$⊢\phi \to W\subseteq Z$$
33	32	sselda	$$⊢\left(\phi \wedge k\in W\right)\to k\in Z$$
34	33 6	syldan	$$⊢\left(\phi \wedge k\in W\right)\to F\left(k\right)\in ℂ$$
35	26	adantl	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge N}\right)\to k-N\in {\mathbb{N}}_0$$
36		oveq2	$$⊢n=k-N\to {if\left(A\le 0,0,A\right)}^n={if\left(A\le 0,0,A\right)}^{k-N}$$
37		eqid	$$⊢\left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)=\left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)$$
38	36 37 17	fvmpt	$$⊢k-N\in {\mathbb{N}}_0\to \left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\left(k-N\right)={if\left(A\le 0,0,A\right)}^{k-N}$$
39	35 38	syl	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge N}\right)\to \left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\left(k-N\right)={if\left(A\le 0,0,A\right)}^{k-N}$$
40	10	zcnd	$$⊢\phi \to N\in ℂ$$
41		eluzelz	$$⊢k\in {\mathbb{Z}}_{\ge N}\to k\in \mathbb{Z}$$
42	41	zcnd	$$⊢k\in {\mathbb{Z}}_{\ge N}\to k\in ℂ$$
43		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
44	43	mptex	$$⊢\left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\in \mathrm{V}$$
45	44	shftval	$$⊢\left(N\in ℂ\wedge k\in ℂ\right)\to \left(\left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\mathrm{shift}N\right)\left(k\right)=\left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\left(k-N\right)$$
46	40 42 45	syl2an	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge N}\right)\to \left(\left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\mathrm{shift}N\right)\left(k\right)=\left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\left(k-N\right)$$
47		simpr	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge N}\right)\to k\in {\mathbb{Z}}_{\ge N}$$
48	47 2	eleqtrrdi	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge N}\right)\to k\in W$$
49	48 18	syl	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge N}\right)\to \left(n\in W⟼{if\left(A\le 0,0,A\right)}^{n-N}\right)\left(k\right)={if\left(A\le 0,0,A\right)}^{k-N}$$
50	39 46 49	3eqtr4rd	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge N}\right)\to \left(n\in W⟼{if\left(A\le 0,0,A\right)}^{n-N}\right)\left(k\right)=\left(\left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\mathrm{shift}N\right)\left(k\right)$$
51	10 50	seqfeq	$$⊢\phi \to seqN\left(+,\left(n\in W⟼{if\left(A\le 0,0,A\right)}^{n-N}\right)\right)=seqN\left(+,\left(\left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\mathrm{shift}N\right)\right)$$
52	44	seqshft	$$⊢\left(N\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to seqN\left(+,\left(\left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\mathrm{shift}N\right)\right)=seq\left(N-N\right)\left(+,\left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\right)\mathrm{shift}N$$
53	10 10 52	syl2anc	$$⊢\phi \to seqN\left(+,\left(\left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\mathrm{shift}N\right)\right)=seq\left(N-N\right)\left(+,\left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\right)\mathrm{shift}N$$
54	40	subidd	$$⊢\phi \to N-N=0$$
55	54	seqeq1d	$$⊢\phi \to seq\left(N-N\right)\left(+,\left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\right)=seq0\left(+,\left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\right)$$
56	55	oveq1d	$$⊢\phi \to seq\left(N-N\right)\left(+,\left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\right)\mathrm{shift}N=seq0\left(+,\left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\right)\mathrm{shift}N$$
57	51 53 56	3eqtrd	$$⊢\phi \to seqN\left(+,\left(n\in W⟼{if\left(A\le 0,0,A\right)}^{n-N}\right)\right)=seq0\left(+,\left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\right)\mathrm{shift}N$$
58	22	recnd	$$⊢\phi \to if\left(A\le 0,0,A\right)\in ℂ$$
59		max2	$$⊢\left(A\in ℝ\wedge 0\in ℝ\right)\to 0\le if\left(A\le 0,0,A\right)$$
60	3 20 59	sylancl	$$⊢\phi \to 0\le if\left(A\le 0,0,A\right)$$
61	22 60	absidd	$$⊢\phi \to \left|if\left(A\le 0,0,A\right)\right|=if\left(A\le 0,0,A\right)$$
62		0lt1	$$⊢0<1$$
63		breq1	$$⊢0=if\left(A\le 0,0,A\right)\to \left(0<1\leftrightarrow if\left(A\le 0,0,A\right)<1\right)$$
64		breq1	$$⊢A=if\left(A\le 0,0,A\right)\to \left(A<1\leftrightarrow if\left(A\le 0,0,A\right)<1\right)$$
65	63 64	ifboth	$$⊢\left(0<1\wedge A<1\right)\to if\left(A\le 0,0,A\right)<1$$
66	62 4 65	sylancr	$$⊢\phi \to if\left(A\le 0,0,A\right)<1$$
67	61 66	eqbrtrd	$$⊢\phi \to \left|if\left(A\le 0,0,A\right)\right|<1$$
68		oveq2	$$⊢n=k\to {if\left(A\le 0,0,A\right)}^n={if\left(A\le 0,0,A\right)}^k$$
69		ovex	$$⊢{if\left(A\le 0,0,A\right)}^k\in \mathrm{V}$$
70	68 37 69	fvmpt	$$⊢k\in {\mathbb{N}}_0\to \left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\left(k\right)={if\left(A\le 0,0,A\right)}^k$$
71	70	adantl	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\left(k\right)={if\left(A\le 0,0,A\right)}^k$$
72	58 67 71	geolim	$$⊢\phi \to seq0\left(+,\left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\right)⇝\left(\frac{1}{1-if\left(A\le 0,0,A\right)}\right)$$
73		seqex	$$⊢seq0\left(+,\left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\right)\in \mathrm{V}$$
74		climshft	$$⊢\left(N\in \mathbb{Z}\wedge seq0\left(+,\left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\right)\in \mathrm{V}\right)\to \left(\left(seq0\left(+,\left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\right)\mathrm{shift}N\right)⇝\left(\frac{1}{1-if\left(A\le 0,0,A\right)}\right)\leftrightarrow seq0\left(+,\left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\right)⇝\left(\frac{1}{1-if\left(A\le 0,0,A\right)}\right)\right)$$
75	10 73 74	sylancl	$$⊢\phi \to \left(\left(seq0\left(+,\left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\right)\mathrm{shift}N\right)⇝\left(\frac{1}{1-if\left(A\le 0,0,A\right)}\right)\leftrightarrow seq0\left(+,\left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\right)⇝\left(\frac{1}{1-if\left(A\le 0,0,A\right)}\right)\right)$$
76	72 75	mpbird	$$⊢\phi \to \left(seq0\left(+,\left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\right)\mathrm{shift}N\right)⇝\left(\frac{1}{1-if\left(A\le 0,0,A\right)}\right)$$
77		ovex	$$⊢seq0\left(+,\left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\right)\mathrm{shift}N\in \mathrm{V}$$
78		ovex	$$⊢\frac{1}{1-if\left(A\le 0,0,A\right)}\in \mathrm{V}$$
79	77 78	breldm	$$⊢\left(seq0\left(+,\left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\right)\mathrm{shift}N\right)⇝\left(\frac{1}{1-if\left(A\le 0,0,A\right)}\right)\to seq0\left(+,\left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\right)\mathrm{shift}N\in \mathrm{dom}⇝$$
80	76 79	syl	$$⊢\phi \to seq0\left(+,\left(n\in {\mathbb{N}}_0⟼{if\left(A\le 0,0,A\right)}^n\right)\right)\mathrm{shift}N\in \mathrm{dom}⇝$$
81	57 80	eqeltrd	$$⊢\phi \to seqN\left(+,\left(n\in W⟼{if\left(A\le 0,0,A\right)}^{n-N}\right)\right)\in \mathrm{dom}⇝$$
82		fveq2	$$⊢k=N\to F\left(k\right)=F\left(N\right)$$
83	82	eleq1d	$$⊢k=N\to \left(F\left(k\right)\in ℂ\leftrightarrow F\left(N\right)\in ℂ\right)$$
84	6	ralrimiva	$$⊢\phi \to \forall k\in ZF\left(k\right)\in ℂ$$
85	83 84 5	rspcdva	$$⊢\phi \to F\left(N\right)\in ℂ$$
86	85	abscld	$$⊢\phi \to \left|F\left(N\right)\right|\in ℝ$$
87		2fveq3	$$⊢n=N\to \left|F\left(n\right)\right|=\left|F\left(N\right)\right|$$
88		oveq1	$$⊢n=N\to n-N=N-N$$
89	88	oveq2d	$$⊢n=N\to {if\left(A\le 0,0,A\right)}^{n-N}={if\left(A\le 0,0,A\right)}^{N-N}$$
90	89	oveq2d	$$⊢n=N\to \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{n-N}=\left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{N-N}$$
91	87 90	breq12d	$$⊢n=N\to \left(\left|F\left(n\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{n-N}\leftrightarrow \left|F\left(N\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{N-N}\right)$$
92	91	imbi2d	$$⊢n=N\to \left(\left(\phi \to \left|F\left(n\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{n-N}\right)\leftrightarrow \left(\phi \to \left|F\left(N\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{N-N}\right)\right)$$
93		2fveq3	$$⊢n=k\to \left|F\left(n\right)\right|=\left|F\left(k\right)\right|$$
94	15	oveq2d	$$⊢n=k\to \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{n-N}=\left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k-N}$$
95	93 94	breq12d	$$⊢n=k\to \left(\left|F\left(n\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{n-N}\leftrightarrow \left|F\left(k\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k-N}\right)$$
96	95	imbi2d	$$⊢n=k\to \left(\left(\phi \to \left|F\left(n\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{n-N}\right)\leftrightarrow \left(\phi \to \left|F\left(k\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k-N}\right)\right)$$
97		2fveq3	$$⊢n=k+1\to \left|F\left(n\right)\right|=\left|F\left(k+1\right)\right|$$
98		oveq1	$$⊢n=k+1\to n-N=k+1-N$$
99	98	oveq2d	$$⊢n=k+1\to {if\left(A\le 0,0,A\right)}^{n-N}={if\left(A\le 0,0,A\right)}^{k+1-N}$$
100	99	oveq2d	$$⊢n=k+1\to \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{n-N}=\left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k+1-N}$$
101	97 100	breq12d	$$⊢n=k+1\to \left(\left|F\left(n\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{n-N}\leftrightarrow \left|F\left(k+1\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k+1-N}\right)$$
102	101	imbi2d	$$⊢n=k+1\to \left(\left(\phi \to \left|F\left(n\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{n-N}\right)\leftrightarrow \left(\phi \to \left|F\left(k+1\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k+1-N}\right)\right)$$
103	86	leidd	$$⊢\phi \to \left|F\left(N\right)\right|\le \left|F\left(N\right)\right|$$
104	54	oveq2d	$$⊢\phi \to {if\left(A\le 0,0,A\right)}^{N-N}={if\left(A\le 0,0,A\right)}^0$$
105	58	exp0d	$$⊢\phi \to {if\left(A\le 0,0,A\right)}^0=1$$
106	104 105	eqtrd	$$⊢\phi \to {if\left(A\le 0,0,A\right)}^{N-N}=1$$
107	106	oveq2d	$$⊢\phi \to \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{N-N}=\left|F\left(N\right)\right|\cdot 1$$
108	86	recnd	$$⊢\phi \to \left|F\left(N\right)\right|\in ℂ$$
109	108	mulridd	$$⊢\phi \to \left|F\left(N\right)\right|\cdot 1=\left|F\left(N\right)\right|$$
110	107 109	eqtrd	$$⊢\phi \to \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{N-N}=\left|F\left(N\right)\right|$$
111	103 110	breqtrrd	$$⊢\phi \to \left|F\left(N\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{N-N}$$
112	34	abscld	$$⊢\left(\phi \wedge k\in W\right)\to \left|F\left(k\right)\right|\in ℝ$$
113	86	adantr	$$⊢\left(\phi \wedge k\in W\right)\to \left|F\left(N\right)\right|\in ℝ$$
114	113 28	remulcld	$$⊢\left(\phi \wedge k\in W\right)\to \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k-N}\in ℝ$$
115	60	adantr	$$⊢\left(\phi \wedge k\in W\right)\to 0\le if\left(A\le 0,0,A\right)$$
116		lemul2a	$$⊢\left(\left(\left|F\left(k\right)\right|\in ℝ\wedge \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k-N}\in ℝ\wedge \left(if\left(A\le 0,0,A\right)\in ℝ\wedge 0\le if\left(A\le 0,0,A\right)\right)\right)\wedge \left|F\left(k\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k-N}\right)\to if\left(A\le 0,0,A\right)\left|F\left(k\right)\right|\le if\left(A\le 0,0,A\right)\left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k-N}$$
117	116	ex	$$⊢\left(\left|F\left(k\right)\right|\in ℝ\wedge \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k-N}\in ℝ\wedge \left(if\left(A\le 0,0,A\right)\in ℝ\wedge 0\le if\left(A\le 0,0,A\right)\right)\right)\to \left(\left|F\left(k\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k-N}\to if\left(A\le 0,0,A\right)\left|F\left(k\right)\right|\le if\left(A\le 0,0,A\right)\left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k-N}\right)$$
118	112 114 23 115 117	syl112anc	$$⊢\left(\phi \wedge k\in W\right)\to \left(\left|F\left(k\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k-N}\to if\left(A\le 0,0,A\right)\left|F\left(k\right)\right|\le if\left(A\le 0,0,A\right)\left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k-N}\right)$$
119	58	adantr	$$⊢\left(\phi \wedge k\in W\right)\to if\left(A\le 0,0,A\right)\in ℂ$$
120	108	adantr	$$⊢\left(\phi \wedge k\in W\right)\to \left|F\left(N\right)\right|\in ℂ$$
121	28	recnd	$$⊢\left(\phi \wedge k\in W\right)\to {if\left(A\le 0,0,A\right)}^{k-N}\in ℂ$$
122	119 120 121	mul12d	$$⊢\left(\phi \wedge k\in W\right)\to if\left(A\le 0,0,A\right)\left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k-N}=\left|F\left(N\right)\right|if\left(A\le 0,0,A\right){if\left(A\le 0,0,A\right)}^{k-N}$$
123	119 27	expp1d	$$⊢\left(\phi \wedge k\in W\right)\to {if\left(A\le 0,0,A\right)}^{k-N+1}={if\left(A\le 0,0,A\right)}^{k-N}if\left(A\le 0,0,A\right)$$
124	42 2	eleq2s	$$⊢k\in W\to k\in ℂ$$
125		ax-1cn	$$⊢1\in ℂ$$
126		addsub	$$⊢\left(k\in ℂ\wedge 1\in ℂ\wedge N\in ℂ\right)\to k+1-N=k-N+1$$
127	125 126	mp3an2	$$⊢\left(k\in ℂ\wedge N\in ℂ\right)\to k+1-N=k-N+1$$
128	124 40 127	syl2anr	$$⊢\left(\phi \wedge k\in W\right)\to k+1-N=k-N+1$$
129	128	oveq2d	$$⊢\left(\phi \wedge k\in W\right)\to {if\left(A\le 0,0,A\right)}^{k+1-N}={if\left(A\le 0,0,A\right)}^{k-N+1}$$
130	119 121	mulcomd	$$⊢\left(\phi \wedge k\in W\right)\to if\left(A\le 0,0,A\right){if\left(A\le 0,0,A\right)}^{k-N}={if\left(A\le 0,0,A\right)}^{k-N}if\left(A\le 0,0,A\right)$$
131	123 129 130	3eqtr4rd	$$⊢\left(\phi \wedge k\in W\right)\to if\left(A\le 0,0,A\right){if\left(A\le 0,0,A\right)}^{k-N}={if\left(A\le 0,0,A\right)}^{k+1-N}$$
132	131	oveq2d	$$⊢\left(\phi \wedge k\in W\right)\to \left|F\left(N\right)\right|if\left(A\le 0,0,A\right){if\left(A\le 0,0,A\right)}^{k-N}=\left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k+1-N}$$
133	122 132	eqtrd	$$⊢\left(\phi \wedge k\in W\right)\to if\left(A\le 0,0,A\right)\left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k-N}=\left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k+1-N}$$
134	133	breq2d	$$⊢\left(\phi \wedge k\in W\right)\to \left(if\left(A\le 0,0,A\right)\left|F\left(k\right)\right|\le if\left(A\le 0,0,A\right)\left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k-N}\leftrightarrow if\left(A\le 0,0,A\right)\left|F\left(k\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k+1-N}\right)$$
135	118 134	sylibd	$$⊢\left(\phi \wedge k\in W\right)\to \left(\left|F\left(k\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k-N}\to if\left(A\le 0,0,A\right)\left|F\left(k\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k+1-N}\right)$$
136		fveq2	$$⊢n=k+1\to F\left(n\right)=F\left(k+1\right)$$
137	136	eleq1d	$$⊢n=k+1\to \left(F\left(n\right)\in ℂ\leftrightarrow F\left(k+1\right)\in ℂ\right)$$
138		fveq2	$$⊢k=n\to F\left(k\right)=F\left(n\right)$$
139	138	eleq1d	$$⊢k=n\to \left(F\left(k\right)\in ℂ\leftrightarrow F\left(n\right)\in ℂ\right)$$
140	139	cbvralvw	$$⊢\forall k\in ZF\left(k\right)\in ℂ\leftrightarrow \forall n\in ZF\left(n\right)\in ℂ$$
141	84 140	sylib	$$⊢\phi \to \forall n\in ZF\left(n\right)\in ℂ$$
142	141	adantr	$$⊢\left(\phi \wedge k\in W\right)\to \forall n\in ZF\left(n\right)\in ℂ$$
143	2	peano2uzs	$$⊢k\in W\to k+1\in W$$
144	32	sselda	$$⊢\left(\phi \wedge k+1\in W\right)\to k+1\in Z$$
145	143 144	sylan2	$$⊢\left(\phi \wedge k\in W\right)\to k+1\in Z$$
146	137 142 145	rspcdva	$$⊢\left(\phi \wedge k\in W\right)\to F\left(k+1\right)\in ℂ$$
147	146	abscld	$$⊢\left(\phi \wedge k\in W\right)\to \left|F\left(k+1\right)\right|\in ℝ$$
148	3	adantr	$$⊢\left(\phi \wedge k\in W\right)\to A\in ℝ$$
149	148 112	remulcld	$$⊢\left(\phi \wedge k\in W\right)\to A\left|F\left(k\right)\right|\in ℝ$$
150	23 112	remulcld	$$⊢\left(\phi \wedge k\in W\right)\to if\left(A\le 0,0,A\right)\left|F\left(k\right)\right|\in ℝ$$
151	34	absge0d	$$⊢\left(\phi \wedge k\in W\right)\to 0\le \left|F\left(k\right)\right|$$
152		max1	$$⊢\left(A\in ℝ\wedge 0\in ℝ\right)\to A\le if\left(A\le 0,0,A\right)$$
153	3 20 152	sylancl	$$⊢\phi \to A\le if\left(A\le 0,0,A\right)$$
154	153	adantr	$$⊢\left(\phi \wedge k\in W\right)\to A\le if\left(A\le 0,0,A\right)$$
155	148 23 112 151 154	lemul1ad	$$⊢\left(\phi \wedge k\in W\right)\to A\left|F\left(k\right)\right|\le if\left(A\le 0,0,A\right)\left|F\left(k\right)\right|$$
156	147 149 150 7 155	letrd	$$⊢\left(\phi \wedge k\in W\right)\to \left|F\left(k+1\right)\right|\le if\left(A\le 0,0,A\right)\left|F\left(k\right)\right|$$
157		peano2uz	$$⊢k\in {\mathbb{Z}}_{\ge N}\to k+1\in {\mathbb{Z}}_{\ge N}$$
158	25 157	syl	$$⊢\left(\phi \wedge k\in W\right)\to k+1\in {\mathbb{Z}}_{\ge N}$$
159		uznn0sub	$$⊢k+1\in {\mathbb{Z}}_{\ge N}\to k+1-N\in {\mathbb{N}}_0$$
160	158 159	syl	$$⊢\left(\phi \wedge k\in W\right)\to k+1-N\in {\mathbb{N}}_0$$
161	23 160	reexpcld	$$⊢\left(\phi \wedge k\in W\right)\to {if\left(A\le 0,0,A\right)}^{k+1-N}\in ℝ$$
162	113 161	remulcld	$$⊢\left(\phi \wedge k\in W\right)\to \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k+1-N}\in ℝ$$
163		letr	$$⊢\left(\left|F\left(k+1\right)\right|\in ℝ\wedge if\left(A\le 0,0,A\right)\left|F\left(k\right)\right|\in ℝ\wedge \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k+1-N}\in ℝ\right)\to \left(\left(\left|F\left(k+1\right)\right|\le if\left(A\le 0,0,A\right)\left|F\left(k\right)\right|\wedge if\left(A\le 0,0,A\right)\left|F\left(k\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k+1-N}\right)\to \left|F\left(k+1\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k+1-N}\right)$$
164	147 150 162 163	syl3anc	$$⊢\left(\phi \wedge k\in W\right)\to \left(\left(\left|F\left(k+1\right)\right|\le if\left(A\le 0,0,A\right)\left|F\left(k\right)\right|\wedge if\left(A\le 0,0,A\right)\left|F\left(k\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k+1-N}\right)\to \left|F\left(k+1\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k+1-N}\right)$$
165	156 164	mpand	$$⊢\left(\phi \wedge k\in W\right)\to \left(if\left(A\le 0,0,A\right)\left|F\left(k\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k+1-N}\to \left|F\left(k+1\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k+1-N}\right)$$
166	135 165	syld	$$⊢\left(\phi \wedge k\in W\right)\to \left(\left|F\left(k\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k-N}\to \left|F\left(k+1\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k+1-N}\right)$$
167	48 166	syldan	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge N}\right)\to \left(\left|F\left(k\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k-N}\to \left|F\left(k+1\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k+1-N}\right)$$
168	167	expcom	$$⊢k\in {\mathbb{Z}}_{\ge N}\to \left(\phi \to \left(\left|F\left(k\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k-N}\to \left|F\left(k+1\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k+1-N}\right)\right)$$
169	168	a2d	$$⊢k\in {\mathbb{Z}}_{\ge N}\to \left(\left(\phi \to \left|F\left(k\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k-N}\right)\to \left(\phi \to \left|F\left(k+1\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k+1-N}\right)\right)$$
170	92 96 102 96 111 169	uzind4i	$$⊢k\in {\mathbb{Z}}_{\ge N}\to \left(\phi \to \left|F\left(k\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k-N}\right)$$
171	170	impcom	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge N}\right)\to \left|F\left(k\right)\right|\le \left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k-N}$$
172	49	oveq2d	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge N}\right)\to \left|F\left(N\right)\right|\left(n\in W⟼{if\left(A\le 0,0,A\right)}^{n-N}\right)\left(k\right)=\left|F\left(N\right)\right|{if\left(A\le 0,0,A\right)}^{k-N}$$
173	171 172	breqtrrd	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge N}\right)\to \left|F\left(k\right)\right|\le \left|F\left(N\right)\right|\left(n\in W⟼{if\left(A\le 0,0,A\right)}^{n-N}\right)\left(k\right)$$
174	2 13 29 34 81 86 173	cvgcmpce	$$⊢\phi \to seqN\left(+,F\right)\in \mathrm{dom}⇝$$
175	1 5 6	iserex	$$⊢\phi \to \left(seqM\left(+,F\right)\in \mathrm{dom}⇝\leftrightarrow seqN\left(+,F\right)\in \mathrm{dom}⇝\right)$$
176	174 175	mpbird	$$⊢\phi \to seqM\left(+,F\right)\in \mathrm{dom}⇝$$