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	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	cvgrat.2	⊢ 𝑊 = ( ℤ≥ ‘ 𝑁 )
	cvgrat.3	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	cvgrat.4	⊢ ( 𝜑 → 𝐴 < 1 )
	cvgrat.5	⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
	cvgrat.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
	cvgrat.7	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( 𝐴 · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
Assertion	cvgrat	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )

Proof

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