Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  cvgratz GIF version

Theorem cvgratz 11308
 Description: Ratio test for convergence of a complex infinite series. If the ratio 𝐴 of the absolute values of successive terms in an infinite sequence 𝐹 is less than 1 for all terms, then the infinite sum of the terms of 𝐹 converges to a complex number. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon, 11-Nov-2022.)
Hypotheses
Ref Expression
cvgratz.1 𝑍 = (ℤ𝑀)
cvgratz.m (𝜑𝑀 ∈ ℤ)
cvgratz.3 (𝜑𝐴 ∈ ℝ)
cvgratz.4 (𝜑𝐴 < 1)
cvgratz.gt0 (𝜑 → 0 < 𝐴)
cvgratz.6 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)
cvgratz.7 ((𝜑𝑘𝑍) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹𝑘))))
Assertion
Ref Expression
cvgratz (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )
Distinct variable groups:   𝐴,𝑘   𝑘,𝐹   𝑘,𝑀   𝑘,𝑍   𝜑,𝑘

Proof of Theorem cvgratz
Dummy variables 𝑖 𝑥 𝑦 𝑎 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cvgratz.m . . . . 5 (𝜑𝑀 ∈ ℤ)
21adantr 274 . . . 4 ((𝜑 ∧ 1 ≤ 𝑀) → 𝑀 ∈ ℤ)
3 fveq2 5421 . . . . . 6 (𝑘 = 𝑥 → (𝐹𝑘) = (𝐹𝑥))
43eleq1d 2208 . . . . 5 (𝑘 = 𝑥 → ((𝐹𝑘) ∈ ℂ ↔ (𝐹𝑥) ∈ ℂ))
5 cvgratz.6 . . . . . . 7 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)
65ralrimiva 2505 . . . . . 6 (𝜑 → ∀𝑘𝑍 (𝐹𝑘) ∈ ℂ)
76ad2antrr 479 . . . . 5 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑥 ∈ (ℤ𝑀)) → ∀𝑘𝑍 (𝐹𝑘) ∈ ℂ)
8 cvgratz.1 . . . . . . . 8 𝑍 = (ℤ𝑀)
98eleq2i 2206 . . . . . . 7 (𝑥𝑍𝑥 ∈ (ℤ𝑀))
109biimpri 132 . . . . . 6 (𝑥 ∈ (ℤ𝑀) → 𝑥𝑍)
1110adantl 275 . . . . 5 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑥 ∈ (ℤ𝑀)) → 𝑥𝑍)
124, 7, 11rspcdva 2794 . . . 4 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑥 ∈ (ℤ𝑀)) → (𝐹𝑥) ∈ ℂ)
13 eluzelz 9342 . . . . . . . 8 (𝑘 ∈ (ℤ𝑀) → 𝑘 ∈ ℤ)
1413adantl 275 . . . . . . 7 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ𝑀)) → 𝑘 ∈ ℤ)
15 1red 7788 . . . . . . . 8 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ𝑀)) → 1 ∈ ℝ)
161zred 9180 . . . . . . . . 9 (𝜑𝑀 ∈ ℝ)
1716ad2antrr 479 . . . . . . . 8 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ𝑀)) → 𝑀 ∈ ℝ)
1814zred 9180 . . . . . . . 8 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ𝑀)) → 𝑘 ∈ ℝ)
19 simplr 519 . . . . . . . 8 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ𝑀)) → 1 ≤ 𝑀)
20 eluzle 9345 . . . . . . . . 9 (𝑘 ∈ (ℤ𝑀) → 𝑀𝑘)
2120adantl 275 . . . . . . . 8 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ𝑀)) → 𝑀𝑘)
2215, 17, 18, 19, 21letrd 7893 . . . . . . 7 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ𝑀)) → 1 ≤ 𝑘)
23 elnnz1 9084 . . . . . . 7 (𝑘 ∈ ℕ ↔ (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
2414, 22, 23sylanbrc 413 . . . . . 6 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ𝑀)) → 𝑘 ∈ ℕ)
25 elnnuz 9369 . . . . . . . 8 (𝑘 ∈ ℕ ↔ 𝑘 ∈ (ℤ‘1))
26 fveq2 5421 . . . . . . . . . . . . 13 (𝑘 = 𝑀 → (𝐹𝑘) = (𝐹𝑀))
2726eleq1d 2208 . . . . . . . . . . . 12 (𝑘 = 𝑀 → ((𝐹𝑘) ∈ ℂ ↔ (𝐹𝑀) ∈ ℂ))
28 uzid 9347 . . . . . . . . . . . . . 14 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
291, 28syl 14 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ (ℤ𝑀))
3029, 8eleqtrrdi 2233 . . . . . . . . . . . 12 (𝜑𝑀𝑍)
3127, 6, 30rspcdva 2794 . . . . . . . . . . 11 (𝜑 → (𝐹𝑀) ∈ ℂ)
3231ad3antrrr 483 . . . . . . . . . 10 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ 𝑘 < 𝑀) → (𝐹𝑀) ∈ ℂ)
33 cvgratz.3 . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ ℝ)
34 cvgratz.gt0 . . . . . . . . . . . . . 14 (𝜑 → 0 < 𝐴)
3533, 34elrpd 9488 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℝ+)
3635ad3antrrr 483 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ 𝑘 < 𝑀) → 𝐴 ∈ ℝ+)
372adantr 274 . . . . . . . . . . . . . 14 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) → 𝑀 ∈ ℤ)
3837adantr 274 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ 𝑘 < 𝑀) → 𝑀 ∈ ℤ)
3925biimpri 132 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (ℤ‘1) → 𝑘 ∈ ℕ)
4039adantl 275 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) → 𝑘 ∈ ℕ)
4140nnzd 9179 . . . . . . . . . . . . . 14 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) → 𝑘 ∈ ℤ)
4241adantr 274 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ 𝑘 < 𝑀) → 𝑘 ∈ ℤ)
4338, 42zsubcld 9185 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ 𝑘 < 𝑀) → (𝑀𝑘) ∈ ℤ)
4436, 43rpexpcld 10455 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ 𝑘 < 𝑀) → (𝐴↑(𝑀𝑘)) ∈ ℝ+)
4544rpcnd 9492 . . . . . . . . . 10 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ 𝑘 < 𝑀) → (𝐴↑(𝑀𝑘)) ∈ ℂ)
4644rpap0d 9496 . . . . . . . . . 10 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ 𝑘 < 𝑀) → (𝐴↑(𝑀𝑘)) # 0)
4732, 45, 46divclapd 8557 . . . . . . . . 9 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ 𝑘 < 𝑀) → ((𝐹𝑀) / (𝐴↑(𝑀𝑘))) ∈ ℂ)
48 simplll 522 . . . . . . . . . 10 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ ¬ 𝑘 < 𝑀) → 𝜑)
4937adantr 274 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ ¬ 𝑘 < 𝑀) → 𝑀 ∈ ℤ)
5041adantr 274 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ ¬ 𝑘 < 𝑀) → 𝑘 ∈ ℤ)
5116ad3antrrr 483 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ ¬ 𝑘 < 𝑀) → 𝑀 ∈ ℝ)
5250zred 9180 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ ¬ 𝑘 < 𝑀) → 𝑘 ∈ ℝ)
53 simpr 109 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ ¬ 𝑘 < 𝑀) → ¬ 𝑘 < 𝑀)
5451, 52, 53nltled 7890 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ ¬ 𝑘 < 𝑀) → 𝑀𝑘)
55 eluz2 9339 . . . . . . . . . . . 12 (𝑘 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀𝑘))
5649, 50, 54, 55syl3anbrc 1165 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ ¬ 𝑘 < 𝑀) → 𝑘 ∈ (ℤ𝑀))
5756, 8eleqtrrdi 2233 . . . . . . . . . 10 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ ¬ 𝑘 < 𝑀) → 𝑘𝑍)
5848, 57, 5syl2anc 408 . . . . . . . . 9 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ ¬ 𝑘 < 𝑀) → (𝐹𝑘) ∈ ℂ)
59 zdclt 9135 . . . . . . . . . 10 ((𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ) → DECID 𝑘 < 𝑀)
6041, 37, 59syl2anc 408 . . . . . . . . 9 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) → DECID 𝑘 < 𝑀)
6147, 58, 60ifcldadc 3501 . . . . . . . 8 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) → if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)) ∈ ℂ)
6225, 61sylan2b 285 . . . . . . 7 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)) ∈ ℂ)
6324, 62syldan 280 . . . . . 6 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ𝑀)) → if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)) ∈ ℂ)
64 breq1 3932 . . . . . . . 8 (𝑖 = 𝑘 → (𝑖 < 𝑀𝑘 < 𝑀))
65 oveq2 5782 . . . . . . . . . 10 (𝑖 = 𝑘 → (𝑀𝑖) = (𝑀𝑘))
6665oveq2d 5790 . . . . . . . . 9 (𝑖 = 𝑘 → (𝐴↑(𝑀𝑖)) = (𝐴↑(𝑀𝑘)))
6766oveq2d 5790 . . . . . . . 8 (𝑖 = 𝑘 → ((𝐹𝑀) / (𝐴↑(𝑀𝑖))) = ((𝐹𝑀) / (𝐴↑(𝑀𝑘))))
68 fveq2 5421 . . . . . . . 8 (𝑖 = 𝑘 → (𝐹𝑖) = (𝐹𝑘))
6964, 67, 68ifbieq12d 3498 . . . . . . 7 (𝑖 = 𝑘 → if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)) = if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))
70 eqid 2139 . . . . . . 7 (𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖))) = (𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))
7169, 70fvmptg 5497 . . . . . 6 ((𝑘 ∈ ℕ ∧ if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)) ∈ ℂ) → ((𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))‘𝑘) = if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))
7224, 63, 71syl2anc 408 . . . . 5 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ𝑀)) → ((𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))‘𝑘) = if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))
7317, 18, 21lensymd 7891 . . . . . 6 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ𝑀)) → ¬ 𝑘 < 𝑀)
7473iffalsed 3484 . . . . 5 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ𝑀)) → if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)) = (𝐹𝑘))
7572, 74eqtr2d 2173 . . . 4 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) = ((𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))‘𝑘))
76 addcl 7752 . . . . 5 ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + 𝑦) ∈ ℂ)
7776adantl 275 . . . 4 (((𝜑 ∧ 1 ≤ 𝑀) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 + 𝑦) ∈ ℂ)
782, 12, 75, 77seq3feq 10252 . . 3 ((𝜑 ∧ 1 ≤ 𝑀) → seq𝑀( + , 𝐹) = seq𝑀( + , (𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))))
7933adantr 274 . . . . 5 ((𝜑 ∧ 1 ≤ 𝑀) → 𝐴 ∈ ℝ)
80 cvgratz.4 . . . . . 6 (𝜑𝐴 < 1)
8180adantr 274 . . . . 5 ((𝜑 ∧ 1 ≤ 𝑀) → 𝐴 < 1)
8234adantr 274 . . . . 5 ((𝜑 ∧ 1 ≤ 𝑀) → 0 < 𝐴)
8371eleq1d 2208 . . . . . . . 8 ((𝑘 ∈ ℕ ∧ if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)) ∈ ℂ) → (((𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))‘𝑘) ∈ ℂ ↔ if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)) ∈ ℂ))
8440, 61, 83syl2anc 408 . . . . . . 7 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) → (((𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))‘𝑘) ∈ ℂ ↔ if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)) ∈ ℂ))
8561, 84mpbird 166 . . . . . 6 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) → ((𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))‘𝑘) ∈ ℂ)
8625, 85sylan2b 285 . . . . 5 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → ((𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))‘𝑘) ∈ ℂ)
8731ad3antrrr 483 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → (𝐹𝑀) ∈ ℂ)
8835ad3antrrr 483 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → 𝐴 ∈ ℝ+)
892ad2antrr 479 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → 𝑀 ∈ ℤ)
9025, 41sylan2b 285 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ)
9190adantr 274 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → 𝑘 ∈ ℤ)
9291peano2zd 9183 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → (𝑘 + 1) ∈ ℤ)
9389, 92zsubcld 9185 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → (𝑀 − (𝑘 + 1)) ∈ ℤ)
9488, 93rpexpcld 10455 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → (𝐴↑(𝑀 − (𝑘 + 1))) ∈ ℝ+)
9594rpcnd 9492 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → (𝐴↑(𝑀 − (𝑘 + 1))) ∈ ℂ)
9694rpap0d 9496 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → (𝐴↑(𝑀 − (𝑘 + 1))) # 0)
9787, 95, 96divclapd 8557 . . . . . . . . . 10 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))) ∈ ℂ)
98 fveq2 5421 . . . . . . . . . . . 12 (𝑎 = (𝑘 + 1) → (𝐹𝑎) = (𝐹‘(𝑘 + 1)))
9998eleq1d 2208 . . . . . . . . . . 11 (𝑎 = (𝑘 + 1) → ((𝐹𝑎) ∈ ℂ ↔ (𝐹‘(𝑘 + 1)) ∈ ℂ))
100 fveq2 5421 . . . . . . . . . . . . . . 15 (𝑘 = 𝑎 → (𝐹𝑘) = (𝐹𝑎))
101100eleq1d 2208 . . . . . . . . . . . . . 14 (𝑘 = 𝑎 → ((𝐹𝑘) ∈ ℂ ↔ (𝐹𝑎) ∈ ℂ))
102101cbvralv 2654 . . . . . . . . . . . . 13 (∀𝑘𝑍 (𝐹𝑘) ∈ ℂ ↔ ∀𝑎𝑍 (𝐹𝑎) ∈ ℂ)
1036, 102sylib 121 . . . . . . . . . . . 12 (𝜑 → ∀𝑎𝑍 (𝐹𝑎) ∈ ℂ)
104103ad3antrrr 483 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) < 𝑀) → ∀𝑎𝑍 (𝐹𝑎) ∈ ℂ)
1052ad2antrr 479 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) < 𝑀) → 𝑀 ∈ ℤ)
106 peano2nn 8739 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
107106adantl 275 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
108107nnzd 9179 . . . . . . . . . . . . . 14 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℤ)
109108adantr 274 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) < 𝑀) → (𝑘 + 1) ∈ ℤ)
11016ad3antrrr 483 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) < 𝑀) → 𝑀 ∈ ℝ)
111107nnred 8740 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℝ)
112111adantr 274 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) < 𝑀) → (𝑘 + 1) ∈ ℝ)
113 simpr 109 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) < 𝑀) → ¬ (𝑘 + 1) < 𝑀)
114110, 112, 113nltled 7890 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) < 𝑀) → 𝑀 ≤ (𝑘 + 1))
115 eluz2 9339 . . . . . . . . . . . . 13 ((𝑘 + 1) ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑘 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑘 + 1)))
116105, 109, 114, 115syl3anbrc 1165 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) < 𝑀) → (𝑘 + 1) ∈ (ℤ𝑀))
117116, 8eleqtrrdi 2233 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) < 𝑀) → (𝑘 + 1) ∈ 𝑍)
11899, 104, 117rspcdva 2794 . . . . . . . . . 10 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) < 𝑀) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
1192adantr 274 . . . . . . . . . . 11 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → 𝑀 ∈ ℤ)
120 zdclt 9135 . . . . . . . . . . 11 (((𝑘 + 1) ∈ ℤ ∧ 𝑀 ∈ ℤ) → DECID (𝑘 + 1) < 𝑀)
121108, 119, 120syl2anc 408 . . . . . . . . . 10 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → DECID (𝑘 + 1) < 𝑀)
12297, 118, 121ifcldadc 3501 . . . . . . . . 9 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1))) ∈ ℂ)
123122abscld 10960 . . . . . . . 8 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (abs‘if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1)))) ∈ ℝ)
12416recnd 7801 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ∈ ℂ)
125124ad2antrr 479 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → 𝑀 ∈ ℂ)
126 simpr 109 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
127126nncnd 8741 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℂ)
128 1cnd 7789 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → 1 ∈ ℂ)
129125, 127, 128subsub4d 8111 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → ((𝑀𝑘) − 1) = (𝑀 − (𝑘 + 1)))
130129oveq2d 5790 . . . . . . . . . . . . . 14 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (𝐴↑((𝑀𝑘) − 1)) = (𝐴↑(𝑀 − (𝑘 + 1))))
13133recnd 7801 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ ℂ)
132131ad2antrr 479 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ℂ)
13333, 34gt0ap0d 8398 . . . . . . . . . . . . . . . 16 (𝜑𝐴 # 0)
134133ad2antrr 479 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → 𝐴 # 0)
135119, 90zsubcld 9185 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (𝑀𝑘) ∈ ℤ)
136132, 134, 135expm1apd 10441 . . . . . . . . . . . . . 14 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (𝐴↑((𝑀𝑘) − 1)) = ((𝐴↑(𝑀𝑘)) / 𝐴))
137130, 136eqtr3d 2174 . . . . . . . . . . . . 13 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (𝐴↑(𝑀 − (𝑘 + 1))) = ((𝐴↑(𝑀𝑘)) / 𝐴))
138137oveq2d 5790 . . . . . . . . . . . 12 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))) = ((𝐹𝑀) / ((𝐴↑(𝑀𝑘)) / 𝐴)))
139138adantr 274 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))) = ((𝐹𝑀) / ((𝐴↑(𝑀𝑘)) / 𝐴)))
140 simpr 109 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → (𝑘 + 1) < 𝑀)
141140iftrued 3481 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1))) = ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))))
142126nnred 8740 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ)
143142adantr 274 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → 𝑘 ∈ ℝ)
144 peano2re 7905 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℝ → (𝑘 + 1) ∈ ℝ)
145143, 144syl 14 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → (𝑘 + 1) ∈ ℝ)
14616ad3antrrr 483 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → 𝑀 ∈ ℝ)
147143ltp1d 8695 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → 𝑘 < (𝑘 + 1))
148143, 145, 146, 147, 140lttrd 7895 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → 𝑘 < 𝑀)
149148iftrued 3481 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)) = ((𝐹𝑀) / (𝐴↑(𝑀𝑘))))
150149oveq2d 5790 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → (𝐴 · if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘))) = (𝐴 · ((𝐹𝑀) / (𝐴↑(𝑀𝑘)))))
15131ad2antrr 479 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (𝐹𝑀) ∈ ℂ)
152132, 134, 135expclzapd 10436 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (𝐴↑(𝑀𝑘)) ∈ ℂ)
153132, 134, 135expap0d 10437 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (𝐴↑(𝑀𝑘)) # 0)
154151, 152, 132, 153, 134divdivap2d 8590 . . . . . . . . . . . . . 14 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → ((𝐹𝑀) / ((𝐴↑(𝑀𝑘)) / 𝐴)) = (((𝐹𝑀) · 𝐴) / (𝐴↑(𝑀𝑘))))
155151, 132mulcomd 7794 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → ((𝐹𝑀) · 𝐴) = (𝐴 · (𝐹𝑀)))
156155oveq1d 5789 . . . . . . . . . . . . . 14 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (((𝐹𝑀) · 𝐴) / (𝐴↑(𝑀𝑘))) = ((𝐴 · (𝐹𝑀)) / (𝐴↑(𝑀𝑘))))
157132, 151, 152, 153divassapd 8593 . . . . . . . . . . . . . 14 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → ((𝐴 · (𝐹𝑀)) / (𝐴↑(𝑀𝑘))) = (𝐴 · ((𝐹𝑀) / (𝐴↑(𝑀𝑘)))))
158154, 156, 1573eqtrd 2176 . . . . . . . . . . . . 13 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → ((𝐹𝑀) / ((𝐴↑(𝑀𝑘)) / 𝐴)) = (𝐴 · ((𝐹𝑀) / (𝐴↑(𝑀𝑘)))))
159158adantr 274 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → ((𝐹𝑀) / ((𝐴↑(𝑀𝑘)) / 𝐴)) = (𝐴 · ((𝐹𝑀) / (𝐴↑(𝑀𝑘)))))
160150, 159eqtr4d 2175 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → (𝐴 · if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘))) = ((𝐹𝑀) / ((𝐴↑(𝑀𝑘)) / 𝐴)))
161139, 141, 1603eqtr4d 2182 . . . . . . . . . 10 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1))) = (𝐴 · if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘))))
162161fveq2d 5425 . . . . . . . . 9 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → (abs‘if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1)))) = (abs‘(𝐴 · if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
163132, 62absmuld 10973 . . . . . . . . . 10 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (abs‘(𝐴 · if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))) = ((abs‘𝐴) · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
164163adantr 274 . . . . . . . . 9 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → (abs‘(𝐴 · if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))) = ((abs‘𝐴) · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
16535rpge0d 9494 . . . . . . . . . . . 12 (𝜑 → 0 ≤ 𝐴)
16633, 165absidd 10946 . . . . . . . . . . 11 (𝜑 → (abs‘𝐴) = 𝐴)
167166oveq1d 5789 . . . . . . . . . 10 (𝜑 → ((abs‘𝐴) · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))) = (𝐴 · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
168167ad3antrrr 483 . . . . . . . . 9 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → ((abs‘𝐴) · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))) = (𝐴 · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
169162, 164, 1683eqtrd 2176 . . . . . . . 8 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → (abs‘if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1)))) = (𝐴 · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
170 eqle 7862 . . . . . . . 8 (((abs‘if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1)))) ∈ ℝ ∧ (abs‘if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1)))) = (𝐴 · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘))))) → (abs‘if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1)))) ≤ (𝐴 · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
171123, 169, 170syl2an2r 584 . . . . . . 7 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → (abs‘if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1)))) ≤ (𝐴 · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
17216ad2antrr 479 . . . . . . . . . . . . . 14 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → 𝑀 ∈ ℝ)
173111, 172lttri3d 7885 . . . . . . . . . . . . 13 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) = 𝑀 ↔ (¬ (𝑘 + 1) < 𝑀 ∧ ¬ 𝑀 < (𝑘 + 1))))
174173simprbda 380 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → ¬ (𝑘 + 1) < 𝑀)
175174iffalsed 3484 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1))) = (𝐹‘(𝑘 + 1)))
176 simpr 109 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → (𝑘 + 1) = 𝑀)
177176fveq2d 5425 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → (𝐹‘(𝑘 + 1)) = (𝐹𝑀))
178175, 177eqtrd 2172 . . . . . . . . . 10 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1))) = (𝐹𝑀))
179178fveq2d 5425 . . . . . . . . 9 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → (abs‘if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1)))) = (abs‘(𝐹𝑀)))
180142adantr 274 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → 𝑘 ∈ ℝ)
181180ltp1d 8695 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → 𝑘 < (𝑘 + 1))
182 breq2 3933 . . . . . . . . . . . . . . . 16 ((𝑘 + 1) = 𝑀 → (𝑘 < (𝑘 + 1) ↔ 𝑘 < 𝑀))
183182adantl 275 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → (𝑘 < (𝑘 + 1) ↔ 𝑘 < 𝑀))
184181, 183mpbid 146 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → 𝑘 < 𝑀)
185184iftrued 3481 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)) = ((𝐹𝑀) / (𝐴↑(𝑀𝑘))))
186176oveq1d 5789 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → ((𝑘 + 1) − 𝑘) = (𝑀𝑘))
187127adantr 274 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → 𝑘 ∈ ℂ)
188 1cnd 7789 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → 1 ∈ ℂ)
189187, 188pncan2d 8082 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → ((𝑘 + 1) − 𝑘) = 1)
190186, 189eqtr3d 2174 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → (𝑀𝑘) = 1)
191190oveq2d 5790 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → (𝐴↑(𝑀𝑘)) = (𝐴↑1))
192132adantr 274 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → 𝐴 ∈ ℂ)
193192exp1d 10426 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → (𝐴↑1) = 𝐴)
194191, 193eqtrd 2172 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → (𝐴↑(𝑀𝑘)) = 𝐴)
195194oveq2d 5790 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → ((𝐹𝑀) / (𝐴↑(𝑀𝑘))) = ((𝐹𝑀) / 𝐴))
196185, 195eqtrd 2172 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)) = ((𝐹𝑀) / 𝐴))
197196oveq2d 5790 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → (𝐴 · if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘))) = (𝐴 · ((𝐹𝑀) / 𝐴)))
19831, 131, 133divcanap2d 8559 . . . . . . . . . . . 12 (𝜑 → (𝐴 · ((𝐹𝑀) / 𝐴)) = (𝐹𝑀))
199198ad3antrrr 483 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → (𝐴 · ((𝐹𝑀) / 𝐴)) = (𝐹𝑀))
200197, 199eqtrd 2172 . . . . . . . . . 10 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → (𝐴 · if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘))) = (𝐹𝑀))
201200fveq2d 5425 . . . . . . . . 9 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → (abs‘(𝐴 · if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))) = (abs‘(𝐹𝑀)))
202167ad2antrr 479 . . . . . . . . . . 11 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → ((abs‘𝐴) · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))) = (𝐴 · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
203163, 202eqtrd 2172 . . . . . . . . . 10 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (abs‘(𝐴 · if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))) = (𝐴 · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
204203adantr 274 . . . . . . . . 9 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → (abs‘(𝐴 · if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))) = (𝐴 · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
205179, 201, 2043eqtr2d 2178 . . . . . . . 8 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → (abs‘if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1)))) = (𝐴 · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
206123, 205, 170syl2an2r 584 . . . . . . 7 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → (abs‘if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1)))) ≤ (𝐴 · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
207 simplll 522 . . . . . . . . 9 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → 𝜑)
208119adantr 274 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → 𝑀 ∈ ℤ)
20990adantr 274 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → 𝑘 ∈ ℤ)
210 simpr 109 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → 𝑀 < (𝑘 + 1))
211 zleltp1 9116 . . . . . . . . . . . . 13 ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑀𝑘𝑀 < (𝑘 + 1)))
212119, 209, 211syl2an2r 584 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → (𝑀𝑘𝑀 < (𝑘 + 1)))
213210, 212mpbird 166 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → 𝑀𝑘)
214208, 209, 213, 55syl3anbrc 1165 . . . . . . . . . 10 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → 𝑘 ∈ (ℤ𝑀))
215214, 8eleqtrrdi 2233 . . . . . . . . 9 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → 𝑘𝑍)
216 cvgratz.7 . . . . . . . . 9 ((𝜑𝑘𝑍) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹𝑘))))
217207, 215, 216syl2anc 408 . . . . . . . 8 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹𝑘))))
218172adantr 274 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → 𝑀 ∈ ℝ)
219111adantr 274 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → (𝑘 + 1) ∈ ℝ)
220218, 219, 210ltnsymd 7889 . . . . . . . . . 10 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → ¬ (𝑘 + 1) < 𝑀)
221220iffalsed 3484 . . . . . . . . 9 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1))) = (𝐹‘(𝑘 + 1)))
222221fveq2d 5425 . . . . . . . 8 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → (abs‘if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1)))) = (abs‘(𝐹‘(𝑘 + 1))))
223142adantr 274 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → 𝑘 ∈ ℝ)
224218, 223, 213lensymd 7891 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → ¬ 𝑘 < 𝑀)
225224iffalsed 3484 . . . . . . . . . 10 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)) = (𝐹𝑘))
226225fveq2d 5425 . . . . . . . . 9 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘))) = (abs‘(𝐹𝑘)))
227226oveq2d 5790 . . . . . . . 8 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → (𝐴 · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))) = (𝐴 · (abs‘(𝐹𝑘))))
228217, 222, 2273brtr4d 3960 . . . . . . 7 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → (abs‘if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1)))) ≤ (𝐴 · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
229 ztri3or 9104 . . . . . . . 8 (((𝑘 + 1) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑘 + 1) < 𝑀 ∨ (𝑘 + 1) = 𝑀𝑀 < (𝑘 + 1)))
230108, 119, 229syl2anc 408 . . . . . . 7 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) < 𝑀 ∨ (𝑘 + 1) = 𝑀𝑀 < (𝑘 + 1)))
231171, 206, 228, 230mpjao3dan 1285 . . . . . 6 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (abs‘if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1)))) ≤ (𝐴 · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
232 breq1 3932 . . . . . . . . . 10 (𝑖 = (𝑘 + 1) → (𝑖 < 𝑀 ↔ (𝑘 + 1) < 𝑀))
233 oveq2 5782 . . . . . . . . . . . 12 (𝑖 = (𝑘 + 1) → (𝑀𝑖) = (𝑀 − (𝑘 + 1)))
234233oveq2d 5790 . . . . . . . . . . 11 (𝑖 = (𝑘 + 1) → (𝐴↑(𝑀𝑖)) = (𝐴↑(𝑀 − (𝑘 + 1))))
235234oveq2d 5790 . . . . . . . . . 10 (𝑖 = (𝑘 + 1) → ((𝐹𝑀) / (𝐴↑(𝑀𝑖))) = ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))))
236 fveq2 5421 . . . . . . . . . 10 (𝑖 = (𝑘 + 1) → (𝐹𝑖) = (𝐹‘(𝑘 + 1)))
237232, 235, 236ifbieq12d 3498 . . . . . . . . 9 (𝑖 = (𝑘 + 1) → if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)) = if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1))))
238237, 70fvmptg 5497 . . . . . . . 8 (((𝑘 + 1) ∈ ℕ ∧ if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1))) ∈ ℂ) → ((𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))‘(𝑘 + 1)) = if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1))))
239107, 122, 238syl2anc 408 . . . . . . 7 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → ((𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))‘(𝑘 + 1)) = if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1))))
240239fveq2d 5425 . . . . . 6 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (abs‘((𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))‘(𝑘 + 1))) = (abs‘if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1)))))
241126, 62, 71syl2anc 408 . . . . . . . 8 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → ((𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))‘𝑘) = if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))
242241fveq2d 5425 . . . . . . 7 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (abs‘((𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))‘𝑘)) = (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘))))
243242oveq2d 5790 . . . . . 6 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (𝐴 · (abs‘((𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))‘𝑘))) = (𝐴 · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
244231, 240, 2433brtr4d 3960 . . . . 5 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (abs‘((𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))‘(𝑘 + 1))) ≤ (𝐴 · (abs‘((𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))‘𝑘))))
24579, 81, 82, 86, 244cvgratnn 11307 . . . 4 ((𝜑 ∧ 1 ≤ 𝑀) → seq1( + , (𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))) ∈ dom ⇝ )
246 eqid 2139 . . . . 5 (ℤ‘1) = (ℤ‘1)
247 1zzd 9088 . . . . . 6 ((𝜑 ∧ 1 ≤ 𝑀) → 1 ∈ ℤ)
248 simpr 109 . . . . . 6 ((𝜑 ∧ 1 ≤ 𝑀) → 1 ≤ 𝑀)
249 eluz2 9339 . . . . . 6 (𝑀 ∈ (ℤ‘1) ↔ (1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 1 ≤ 𝑀))
250247, 2, 248, 249syl3anbrc 1165 . . . . 5 ((𝜑 ∧ 1 ≤ 𝑀) → 𝑀 ∈ (ℤ‘1))
251246, 250, 85iserex 11115 . . . 4 ((𝜑 ∧ 1 ≤ 𝑀) → (seq1( + , (𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))) ∈ dom ⇝ ↔ seq𝑀( + , (𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))) ∈ dom ⇝ ))
252245, 251mpbid 146 . . 3 ((𝜑 ∧ 1 ≤ 𝑀) → seq𝑀( + , (𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))) ∈ dom ⇝ )
25378, 252eqeltrd 2216 . 2 ((𝜑 ∧ 1 ≤ 𝑀) → seq𝑀( + , 𝐹) ∈ dom ⇝ )
25433adantr 274 . . . 4 ((𝜑𝑀 ≤ 1) → 𝐴 ∈ ℝ)
25580adantr 274 . . . 4 ((𝜑𝑀 ≤ 1) → 𝐴 < 1)
25634adantr 274 . . . 4 ((𝜑𝑀 ≤ 1) → 0 < 𝐴)
2571adantr 274 . . . . . . 7 ((𝜑𝑀 ≤ 1) → 𝑀 ∈ ℤ)
258257adantr 274 . . . . . 6 (((𝜑𝑀 ≤ 1) ∧ 𝑘 ∈ ℕ) → 𝑀 ∈ ℤ)
259 nnz 9080 . . . . . . 7 (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
260259adantl 275 . . . . . 6 (((𝜑𝑀 ≤ 1) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ)
261258zred 9180 . . . . . . 7 (((𝜑𝑀 ≤ 1) ∧ 𝑘 ∈ ℕ) → 𝑀 ∈ ℝ)
262 1red 7788 . . . . . . 7 (((𝜑𝑀 ≤ 1) ∧ 𝑘 ∈ ℕ) → 1 ∈ ℝ)
263260zred 9180 . . . . . . 7 (((𝜑𝑀 ≤ 1) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ)
264 simplr 519 . . . . . . 7 (((𝜑𝑀 ≤ 1) ∧ 𝑘 ∈ ℕ) → 𝑀 ≤ 1)
265 nnge1 8750 . . . . . . . 8 (𝑘 ∈ ℕ → 1 ≤ 𝑘)
266265adantl 275 . . . . . . 7 (((𝜑𝑀 ≤ 1) ∧ 𝑘 ∈ ℕ) → 1 ≤ 𝑘)
267261, 262, 263, 264, 266letrd 7893 . . . . . 6 (((𝜑𝑀 ≤ 1) ∧ 𝑘 ∈ ℕ) → 𝑀𝑘)
268258, 260, 267, 55syl3anbrc 1165 . . . . 5 (((𝜑𝑀 ≤ 1) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ𝑀))
2698eleq2i 2206 . . . . . . 7 (𝑘𝑍𝑘 ∈ (ℤ𝑀))
270269, 5sylan2br 286 . . . . . 6 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) ∈ ℂ)
271270adantlr 468 . . . . 5 (((𝜑𝑀 ≤ 1) ∧ 𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) ∈ ℂ)
272268, 271syldan 280 . . . 4 (((𝜑𝑀 ≤ 1) ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℂ)
273269, 216sylan2br 286 . . . . . 6 ((𝜑𝑘 ∈ (ℤ𝑀)) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹𝑘))))
274273adantlr 468 . . . . 5 (((𝜑𝑀 ≤ 1) ∧ 𝑘 ∈ (ℤ𝑀)) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹𝑘))))
275268, 274syldan 280 . . . 4 (((𝜑𝑀 ≤ 1) ∧ 𝑘 ∈ ℕ) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹𝑘))))
276254, 255, 256, 272, 275cvgratnn 11307 . . 3 ((𝜑𝑀 ≤ 1) → seq1( + , 𝐹) ∈ dom ⇝ )
277 eqid 2139 . . . 4 (ℤ𝑀) = (ℤ𝑀)
278 1zzd 9088 . . . . 5 ((𝜑𝑀 ≤ 1) → 1 ∈ ℤ)
279 simpr 109 . . . . 5 ((𝜑𝑀 ≤ 1) → 𝑀 ≤ 1)
280 eluz2 9339 . . . . 5 (1 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑀 ≤ 1))
281257, 278, 279, 280syl3anbrc 1165 . . . 4 ((𝜑𝑀 ≤ 1) → 1 ∈ (ℤ𝑀))
282277, 281, 271iserex 11115 . . 3 ((𝜑𝑀 ≤ 1) → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq1( + , 𝐹) ∈ dom ⇝ ))
283276, 282mpbird 166 . 2 ((𝜑𝑀 ≤ 1) → seq𝑀( + , 𝐹) ∈ dom ⇝ )
284 1z 9087 . . 3 1 ∈ ℤ
285 zletric 9105 . . 3 ((1 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (1 ≤ 𝑀𝑀 ≤ 1))
286284, 1, 285sylancr 410 . 2 (𝜑 → (1 ≤ 𝑀𝑀 ≤ 1))
287253, 283, 286mpjaodan 787 1 (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 697  DECID wdc 819   ∨ w3o 961   = wceq 1331   ∈ wcel 1480  ∀wral 2416  ifcif 3474   class class class wbr 3929   ↦ cmpt 3989  dom cdm 4539  ‘cfv 5123  (class class class)co 5774  ℂcc 7625  ℝcr 7626  0cc0 7627  1c1 7628   + caddc 7630   · cmul 7632   < clt 7807   ≤ cle 7808   − cmin 7940   # cap 8350   / cdiv 8439  ℕcn 8727  ℤcz 9061  ℤ≥cuz 9333  ℝ+crp 9448  seqcseq 10225  ↑cexp 10299  abscabs 10776   ⇝ cli 11054 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502  ax-cnex 7718  ax-resscn 7719  ax-1cn 7720  ax-1re 7721  ax-icn 7722  ax-addcl 7723  ax-addrcl 7724  ax-mulcl 7725  ax-mulrcl 7726  ax-addcom 7727  ax-mulcom 7728  ax-addass 7729  ax-mulass 7730  ax-distr 7731  ax-i2m1 7732  ax-0lt1 7733  ax-1rid 7734  ax-0id 7735  ax-rnegex 7736  ax-precex 7737  ax-cnre 7738  ax-pre-ltirr 7739  ax-pre-ltwlin 7740  ax-pre-lttrn 7741  ax-pre-apti 7742  ax-pre-ltadd 7743  ax-pre-mulgt0 7744  ax-pre-mulext 7745  ax-arch 7746  ax-caucvg 7747 This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-nel 2404  df-ral 2421  df-rex 2422  df-reu 2423  df-rmo 2424  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-if 3475  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-id 4215  df-po 4218  df-iso 4219  df-iord 4288  df-on 4290  df-ilim 4291  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-isom 5132  df-riota 5730  df-ov 5777  df-oprab 5778  df-mpo 5779  df-1st 6038  df-2nd 6039  df-recs 6202  df-irdg 6267  df-frec 6288  df-1o 6313  df-oadd 6317  df-er 6429  df-en 6635  df-dom 6636  df-fin 6637  df-pnf 7809  df-mnf 7810  df-xr 7811  df-ltxr 7812  df-le 7813  df-sub 7942  df-neg 7943  df-reap 8344  df-ap 8351  df-div 8440  df-inn 8728  df-2 8786  df-3 8787  df-4 8788  df-n0 8985  df-z 9062  df-uz 9334  df-q 9419  df-rp 9449  df-ico 9684  df-fz 9798  df-fzo 9927  df-seqfrec 10226  df-exp 10300  df-ihash 10529  df-cj 10621  df-re 10622  df-im 10623  df-rsqrt 10777  df-abs 10778  df-clim 11055  df-sumdc 11130 This theorem is referenced by:  cvgratgt0  11309
 Copyright terms: Public domain W3C validator