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

Theorem cvgratz 11675
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 276 . . . 4 ((𝜑 ∧ 1 ≤ 𝑀) → 𝑀 ∈ ℤ)
3 fveq2 5554 . . . . . 6 (𝑘 = 𝑥 → (𝐹𝑘) = (𝐹𝑥))
43eleq1d 2262 . . . . 5 (𝑘 = 𝑥 → ((𝐹𝑘) ∈ ℂ ↔ (𝐹𝑥) ∈ ℂ))
5 cvgratz.6 . . . . . . 7 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)
65ralrimiva 2567 . . . . . 6 (𝜑 → ∀𝑘𝑍 (𝐹𝑘) ∈ ℂ)
76ad2antrr 488 . . . . 5 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑥 ∈ (ℤ𝑀)) → ∀𝑘𝑍 (𝐹𝑘) ∈ ℂ)
8 cvgratz.1 . . . . . . . 8 𝑍 = (ℤ𝑀)
98eleq2i 2260 . . . . . . 7 (𝑥𝑍𝑥 ∈ (ℤ𝑀))
109biimpri 133 . . . . . 6 (𝑥 ∈ (ℤ𝑀) → 𝑥𝑍)
1110adantl 277 . . . . 5 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑥 ∈ (ℤ𝑀)) → 𝑥𝑍)
124, 7, 11rspcdva 2869 . . . 4 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑥 ∈ (ℤ𝑀)) → (𝐹𝑥) ∈ ℂ)
13 eluzelz 9601 . . . . . . . 8 (𝑘 ∈ (ℤ𝑀) → 𝑘 ∈ ℤ)
1413adantl 277 . . . . . . 7 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ𝑀)) → 𝑘 ∈ ℤ)
15 1red 8034 . . . . . . . 8 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ𝑀)) → 1 ∈ ℝ)
161zred 9439 . . . . . . . . 9 (𝜑𝑀 ∈ ℝ)
1716ad2antrr 488 . . . . . . . 8 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ𝑀)) → 𝑀 ∈ ℝ)
1814zred 9439 . . . . . . . 8 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ𝑀)) → 𝑘 ∈ ℝ)
19 simplr 528 . . . . . . . 8 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ𝑀)) → 1 ≤ 𝑀)
20 eluzle 9604 . . . . . . . . 9 (𝑘 ∈ (ℤ𝑀) → 𝑀𝑘)
2120adantl 277 . . . . . . . 8 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ𝑀)) → 𝑀𝑘)
2215, 17, 18, 19, 21letrd 8143 . . . . . . 7 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ𝑀)) → 1 ≤ 𝑘)
23 elnnz1 9340 . . . . . . 7 (𝑘 ∈ ℕ ↔ (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
2414, 22, 23sylanbrc 417 . . . . . 6 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ𝑀)) → 𝑘 ∈ ℕ)
25 elnnuz 9629 . . . . . . . 8 (𝑘 ∈ ℕ ↔ 𝑘 ∈ (ℤ‘1))
26 fveq2 5554 . . . . . . . . . . . . 13 (𝑘 = 𝑀 → (𝐹𝑘) = (𝐹𝑀))
2726eleq1d 2262 . . . . . . . . . . . 12 (𝑘 = 𝑀 → ((𝐹𝑘) ∈ ℂ ↔ (𝐹𝑀) ∈ ℂ))
28 uzid 9606 . . . . . . . . . . . . . 14 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
291, 28syl 14 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ (ℤ𝑀))
3029, 8eleqtrrdi 2287 . . . . . . . . . . . 12 (𝜑𝑀𝑍)
3127, 6, 30rspcdva 2869 . . . . . . . . . . 11 (𝜑 → (𝐹𝑀) ∈ ℂ)
3231ad3antrrr 492 . . . . . . . . . 10 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ 𝑘 < 𝑀) → (𝐹𝑀) ∈ ℂ)
33 cvgratz.3 . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ ℝ)
34 cvgratz.gt0 . . . . . . . . . . . . . 14 (𝜑 → 0 < 𝐴)
3533, 34elrpd 9759 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℝ+)
3635ad3antrrr 492 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ 𝑘 < 𝑀) → 𝐴 ∈ ℝ+)
372adantr 276 . . . . . . . . . . . . . 14 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) → 𝑀 ∈ ℤ)
3837adantr 276 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ 𝑘 < 𝑀) → 𝑀 ∈ ℤ)
3925biimpri 133 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (ℤ‘1) → 𝑘 ∈ ℕ)
4039adantl 277 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) → 𝑘 ∈ ℕ)
4140nnzd 9438 . . . . . . . . . . . . . 14 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) → 𝑘 ∈ ℤ)
4241adantr 276 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ 𝑘 < 𝑀) → 𝑘 ∈ ℤ)
4338, 42zsubcld 9444 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ 𝑘 < 𝑀) → (𝑀𝑘) ∈ ℤ)
4436, 43rpexpcld 10768 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ 𝑘 < 𝑀) → (𝐴↑(𝑀𝑘)) ∈ ℝ+)
4544rpcnd 9764 . . . . . . . . . 10 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ 𝑘 < 𝑀) → (𝐴↑(𝑀𝑘)) ∈ ℂ)
4644rpap0d 9768 . . . . . . . . . 10 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ 𝑘 < 𝑀) → (𝐴↑(𝑀𝑘)) # 0)
4732, 45, 46divclapd 8809 . . . . . . . . 9 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ 𝑘 < 𝑀) → ((𝐹𝑀) / (𝐴↑(𝑀𝑘))) ∈ ℂ)
48 simplll 533 . . . . . . . . . 10 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ ¬ 𝑘 < 𝑀) → 𝜑)
4937adantr 276 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ ¬ 𝑘 < 𝑀) → 𝑀 ∈ ℤ)
5041adantr 276 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ ¬ 𝑘 < 𝑀) → 𝑘 ∈ ℤ)
5116ad3antrrr 492 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ ¬ 𝑘 < 𝑀) → 𝑀 ∈ ℝ)
5250zred 9439 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ ¬ 𝑘 < 𝑀) → 𝑘 ∈ ℝ)
53 simpr 110 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ ¬ 𝑘 < 𝑀) → ¬ 𝑘 < 𝑀)
5451, 52, 53nltled 8140 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ ¬ 𝑘 < 𝑀) → 𝑀𝑘)
55 eluz2 9598 . . . . . . . . . . . 12 (𝑘 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀𝑘))
5649, 50, 54, 55syl3anbrc 1183 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ ¬ 𝑘 < 𝑀) → 𝑘 ∈ (ℤ𝑀))
5756, 8eleqtrrdi 2287 . . . . . . . . . 10 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ ¬ 𝑘 < 𝑀) → 𝑘𝑍)
5848, 57, 5syl2anc 411 . . . . . . . . 9 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) ∧ ¬ 𝑘 < 𝑀) → (𝐹𝑘) ∈ ℂ)
59 zdclt 9394 . . . . . . . . . 10 ((𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ) → DECID 𝑘 < 𝑀)
6041, 37, 59syl2anc 411 . . . . . . . . 9 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) → DECID 𝑘 < 𝑀)
6147, 58, 60ifcldadc 3586 . . . . . . . 8 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) → if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)) ∈ ℂ)
6225, 61sylan2b 287 . . . . . . 7 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)) ∈ ℂ)
6324, 62syldan 282 . . . . . 6 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ𝑀)) → if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)) ∈ ℂ)
64 breq1 4032 . . . . . . . 8 (𝑖 = 𝑘 → (𝑖 < 𝑀𝑘 < 𝑀))
65 oveq2 5926 . . . . . . . . . 10 (𝑖 = 𝑘 → (𝑀𝑖) = (𝑀𝑘))
6665oveq2d 5934 . . . . . . . . 9 (𝑖 = 𝑘 → (𝐴↑(𝑀𝑖)) = (𝐴↑(𝑀𝑘)))
6766oveq2d 5934 . . . . . . . 8 (𝑖 = 𝑘 → ((𝐹𝑀) / (𝐴↑(𝑀𝑖))) = ((𝐹𝑀) / (𝐴↑(𝑀𝑘))))
68 fveq2 5554 . . . . . . . 8 (𝑖 = 𝑘 → (𝐹𝑖) = (𝐹𝑘))
6964, 67, 68ifbieq12d 3583 . . . . . . 7 (𝑖 = 𝑘 → if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)) = if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))
70 eqid 2193 . . . . . . 7 (𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖))) = (𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))
7169, 70fvmptg 5633 . . . . . 6 ((𝑘 ∈ ℕ ∧ if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)) ∈ ℂ) → ((𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))‘𝑘) = if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))
7224, 63, 71syl2anc 411 . . . . 5 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ𝑀)) → ((𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))‘𝑘) = if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))
7317, 18, 21lensymd 8141 . . . . . 6 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ𝑀)) → ¬ 𝑘 < 𝑀)
7473iffalsed 3567 . . . . 5 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ𝑀)) → if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)) = (𝐹𝑘))
7572, 74eqtr2d 2227 . . . 4 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) = ((𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))‘𝑘))
76 addcl 7997 . . . . 5 ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + 𝑦) ∈ ℂ)
7776adantl 277 . . . 4 (((𝜑 ∧ 1 ≤ 𝑀) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 + 𝑦) ∈ ℂ)
782, 12, 75, 77seq3feq 10551 . . 3 ((𝜑 ∧ 1 ≤ 𝑀) → seq𝑀( + , 𝐹) = seq𝑀( + , (𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))))
7933adantr 276 . . . . 5 ((𝜑 ∧ 1 ≤ 𝑀) → 𝐴 ∈ ℝ)
80 cvgratz.4 . . . . . 6 (𝜑𝐴 < 1)
8180adantr 276 . . . . 5 ((𝜑 ∧ 1 ≤ 𝑀) → 𝐴 < 1)
8234adantr 276 . . . . 5 ((𝜑 ∧ 1 ≤ 𝑀) → 0 < 𝐴)
8371eleq1d 2262 . . . . . . . 8 ((𝑘 ∈ ℕ ∧ if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)) ∈ ℂ) → (((𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))‘𝑘) ∈ ℂ ↔ if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)) ∈ ℂ))
8440, 61, 83syl2anc 411 . . . . . . 7 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) → (((𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))‘𝑘) ∈ ℂ ↔ if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)) ∈ ℂ))
8561, 84mpbird 167 . . . . . 6 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ (ℤ‘1)) → ((𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))‘𝑘) ∈ ℂ)
8625, 85sylan2b 287 . . . . 5 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → ((𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))‘𝑘) ∈ ℂ)
8731ad3antrrr 492 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → (𝐹𝑀) ∈ ℂ)
8835ad3antrrr 492 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → 𝐴 ∈ ℝ+)
892ad2antrr 488 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → 𝑀 ∈ ℤ)
9025, 41sylan2b 287 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ)
9190adantr 276 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → 𝑘 ∈ ℤ)
9291peano2zd 9442 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → (𝑘 + 1) ∈ ℤ)
9389, 92zsubcld 9444 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → (𝑀 − (𝑘 + 1)) ∈ ℤ)
9488, 93rpexpcld 10768 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → (𝐴↑(𝑀 − (𝑘 + 1))) ∈ ℝ+)
9594rpcnd 9764 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → (𝐴↑(𝑀 − (𝑘 + 1))) ∈ ℂ)
9694rpap0d 9768 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → (𝐴↑(𝑀 − (𝑘 + 1))) # 0)
9787, 95, 96divclapd 8809 . . . . . . . . . 10 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))) ∈ ℂ)
98 fveq2 5554 . . . . . . . . . . . 12 (𝑎 = (𝑘 + 1) → (𝐹𝑎) = (𝐹‘(𝑘 + 1)))
9998eleq1d 2262 . . . . . . . . . . 11 (𝑎 = (𝑘 + 1) → ((𝐹𝑎) ∈ ℂ ↔ (𝐹‘(𝑘 + 1)) ∈ ℂ))
100 fveq2 5554 . . . . . . . . . . . . . . 15 (𝑘 = 𝑎 → (𝐹𝑘) = (𝐹𝑎))
101100eleq1d 2262 . . . . . . . . . . . . . 14 (𝑘 = 𝑎 → ((𝐹𝑘) ∈ ℂ ↔ (𝐹𝑎) ∈ ℂ))
102101cbvralv 2726 . . . . . . . . . . . . 13 (∀𝑘𝑍 (𝐹𝑘) ∈ ℂ ↔ ∀𝑎𝑍 (𝐹𝑎) ∈ ℂ)
1036, 102sylib 122 . . . . . . . . . . . 12 (𝜑 → ∀𝑎𝑍 (𝐹𝑎) ∈ ℂ)
104103ad3antrrr 492 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) < 𝑀) → ∀𝑎𝑍 (𝐹𝑎) ∈ ℂ)
1052ad2antrr 488 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) < 𝑀) → 𝑀 ∈ ℤ)
106 peano2nn 8994 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
107106adantl 277 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
108107nnzd 9438 . . . . . . . . . . . . . 14 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℤ)
109108adantr 276 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) < 𝑀) → (𝑘 + 1) ∈ ℤ)
11016ad3antrrr 492 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) < 𝑀) → 𝑀 ∈ ℝ)
111107nnred 8995 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℝ)
112111adantr 276 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) < 𝑀) → (𝑘 + 1) ∈ ℝ)
113 simpr 110 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) < 𝑀) → ¬ (𝑘 + 1) < 𝑀)
114110, 112, 113nltled 8140 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) < 𝑀) → 𝑀 ≤ (𝑘 + 1))
115 eluz2 9598 . . . . . . . . . . . . 13 ((𝑘 + 1) ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑘 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑘 + 1)))
116105, 109, 114, 115syl3anbrc 1183 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) < 𝑀) → (𝑘 + 1) ∈ (ℤ𝑀))
117116, 8eleqtrrdi 2287 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) < 𝑀) → (𝑘 + 1) ∈ 𝑍)
11899, 104, 117rspcdva 2869 . . . . . . . . . 10 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) < 𝑀) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
1192adantr 276 . . . . . . . . . . 11 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → 𝑀 ∈ ℤ)
120 zdclt 9394 . . . . . . . . . . 11 (((𝑘 + 1) ∈ ℤ ∧ 𝑀 ∈ ℤ) → DECID (𝑘 + 1) < 𝑀)
121108, 119, 120syl2anc 411 . . . . . . . . . 10 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → DECID (𝑘 + 1) < 𝑀)
12297, 118, 121ifcldadc 3586 . . . . . . . . 9 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1))) ∈ ℂ)
123122abscld 11325 . . . . . . . 8 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (abs‘if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1)))) ∈ ℝ)
12416recnd 8048 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ∈ ℂ)
125124ad2antrr 488 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → 𝑀 ∈ ℂ)
126 simpr 110 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
127126nncnd 8996 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℂ)
128 1cnd 8035 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → 1 ∈ ℂ)
129125, 127, 128subsub4d 8361 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → ((𝑀𝑘) − 1) = (𝑀 − (𝑘 + 1)))
130129oveq2d 5934 . . . . . . . . . . . . . 14 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (𝐴↑((𝑀𝑘) − 1)) = (𝐴↑(𝑀 − (𝑘 + 1))))
13133recnd 8048 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ ℂ)
132131ad2antrr 488 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ℂ)
13333, 34gt0ap0d 8648 . . . . . . . . . . . . . . . 16 (𝜑𝐴 # 0)
134133ad2antrr 488 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → 𝐴 # 0)
135119, 90zsubcld 9444 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (𝑀𝑘) ∈ ℤ)
136132, 134, 135expm1apd 10754 . . . . . . . . . . . . . 14 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (𝐴↑((𝑀𝑘) − 1)) = ((𝐴↑(𝑀𝑘)) / 𝐴))
137130, 136eqtr3d 2228 . . . . . . . . . . . . 13 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (𝐴↑(𝑀 − (𝑘 + 1))) = ((𝐴↑(𝑀𝑘)) / 𝐴))
138137oveq2d 5934 . . . . . . . . . . . 12 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))) = ((𝐹𝑀) / ((𝐴↑(𝑀𝑘)) / 𝐴)))
139138adantr 276 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))) = ((𝐹𝑀) / ((𝐴↑(𝑀𝑘)) / 𝐴)))
140 simpr 110 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → (𝑘 + 1) < 𝑀)
141140iftrued 3564 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1))) = ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))))
142126nnred 8995 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ)
143142adantr 276 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → 𝑘 ∈ ℝ)
144 peano2re 8155 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℝ → (𝑘 + 1) ∈ ℝ)
145143, 144syl 14 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → (𝑘 + 1) ∈ ℝ)
14616ad3antrrr 492 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → 𝑀 ∈ ℝ)
147143ltp1d 8949 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → 𝑘 < (𝑘 + 1))
148143, 145, 146, 147, 140lttrd 8145 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → 𝑘 < 𝑀)
149148iftrued 3564 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)) = ((𝐹𝑀) / (𝐴↑(𝑀𝑘))))
150149oveq2d 5934 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → (𝐴 · if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘))) = (𝐴 · ((𝐹𝑀) / (𝐴↑(𝑀𝑘)))))
15131ad2antrr 488 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (𝐹𝑀) ∈ ℂ)
152132, 134, 135expclzapd 10749 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (𝐴↑(𝑀𝑘)) ∈ ℂ)
153132, 134, 135expap0d 10750 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (𝐴↑(𝑀𝑘)) # 0)
154151, 152, 132, 153, 134divdivap2d 8842 . . . . . . . . . . . . . 14 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → ((𝐹𝑀) / ((𝐴↑(𝑀𝑘)) / 𝐴)) = (((𝐹𝑀) · 𝐴) / (𝐴↑(𝑀𝑘))))
155151, 132mulcomd 8041 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → ((𝐹𝑀) · 𝐴) = (𝐴 · (𝐹𝑀)))
156155oveq1d 5933 . . . . . . . . . . . . . 14 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (((𝐹𝑀) · 𝐴) / (𝐴↑(𝑀𝑘))) = ((𝐴 · (𝐹𝑀)) / (𝐴↑(𝑀𝑘))))
157132, 151, 152, 153divassapd 8845 . . . . . . . . . . . . . 14 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → ((𝐴 · (𝐹𝑀)) / (𝐴↑(𝑀𝑘))) = (𝐴 · ((𝐹𝑀) / (𝐴↑(𝑀𝑘)))))
158154, 156, 1573eqtrd 2230 . . . . . . . . . . . . 13 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → ((𝐹𝑀) / ((𝐴↑(𝑀𝑘)) / 𝐴)) = (𝐴 · ((𝐹𝑀) / (𝐴↑(𝑀𝑘)))))
159158adantr 276 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → ((𝐹𝑀) / ((𝐴↑(𝑀𝑘)) / 𝐴)) = (𝐴 · ((𝐹𝑀) / (𝐴↑(𝑀𝑘)))))
160150, 159eqtr4d 2229 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → (𝐴 · if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘))) = ((𝐹𝑀) / ((𝐴↑(𝑀𝑘)) / 𝐴)))
161139, 141, 1603eqtr4d 2236 . . . . . . . . . 10 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1))) = (𝐴 · if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘))))
162161fveq2d 5558 . . . . . . . . 9 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → (abs‘if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1)))) = (abs‘(𝐴 · if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
163132, 62absmuld 11338 . . . . . . . . . 10 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (abs‘(𝐴 · if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))) = ((abs‘𝐴) · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
164163adantr 276 . . . . . . . . 9 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → (abs‘(𝐴 · if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))) = ((abs‘𝐴) · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
16535rpge0d 9766 . . . . . . . . . . . 12 (𝜑 → 0 ≤ 𝐴)
16633, 165absidd 11311 . . . . . . . . . . 11 (𝜑 → (abs‘𝐴) = 𝐴)
167166oveq1d 5933 . . . . . . . . . 10 (𝜑 → ((abs‘𝐴) · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))) = (𝐴 · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
168167ad3antrrr 492 . . . . . . . . 9 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → ((abs‘𝐴) · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))) = (𝐴 · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
169162, 164, 1683eqtrd 2230 . . . . . . . 8 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → (abs‘if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1)))) = (𝐴 · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
170 eqle 8111 . . . . . . . 8 (((abs‘if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1)))) ∈ ℝ ∧ (abs‘if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1)))) = (𝐴 · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘))))) → (abs‘if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1)))) ≤ (𝐴 · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
171123, 169, 170syl2an2r 595 . . . . . . 7 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) < 𝑀) → (abs‘if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1)))) ≤ (𝐴 · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
17216ad2antrr 488 . . . . . . . . . . . . . 14 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → 𝑀 ∈ ℝ)
173111, 172lttri3d 8134 . . . . . . . . . . . . 13 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) = 𝑀 ↔ (¬ (𝑘 + 1) < 𝑀 ∧ ¬ 𝑀 < (𝑘 + 1))))
174173simprbda 383 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → ¬ (𝑘 + 1) < 𝑀)
175174iffalsed 3567 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1))) = (𝐹‘(𝑘 + 1)))
176 simpr 110 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → (𝑘 + 1) = 𝑀)
177176fveq2d 5558 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → (𝐹‘(𝑘 + 1)) = (𝐹𝑀))
178175, 177eqtrd 2226 . . . . . . . . . 10 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1))) = (𝐹𝑀))
179178fveq2d 5558 . . . . . . . . 9 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → (abs‘if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1)))) = (abs‘(𝐹𝑀)))
180142adantr 276 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → 𝑘 ∈ ℝ)
181180ltp1d 8949 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → 𝑘 < (𝑘 + 1))
182 breq2 4033 . . . . . . . . . . . . . . . 16 ((𝑘 + 1) = 𝑀 → (𝑘 < (𝑘 + 1) ↔ 𝑘 < 𝑀))
183182adantl 277 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → (𝑘 < (𝑘 + 1) ↔ 𝑘 < 𝑀))
184181, 183mpbid 147 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → 𝑘 < 𝑀)
185184iftrued 3564 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)) = ((𝐹𝑀) / (𝐴↑(𝑀𝑘))))
186176oveq1d 5933 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → ((𝑘 + 1) − 𝑘) = (𝑀𝑘))
187127adantr 276 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → 𝑘 ∈ ℂ)
188 1cnd 8035 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → 1 ∈ ℂ)
189187, 188pncan2d 8332 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → ((𝑘 + 1) − 𝑘) = 1)
190186, 189eqtr3d 2228 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → (𝑀𝑘) = 1)
191190oveq2d 5934 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → (𝐴↑(𝑀𝑘)) = (𝐴↑1))
192132adantr 276 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → 𝐴 ∈ ℂ)
193192exp1d 10739 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → (𝐴↑1) = 𝐴)
194191, 193eqtrd 2226 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → (𝐴↑(𝑀𝑘)) = 𝐴)
195194oveq2d 5934 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → ((𝐹𝑀) / (𝐴↑(𝑀𝑘))) = ((𝐹𝑀) / 𝐴))
196185, 195eqtrd 2226 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)) = ((𝐹𝑀) / 𝐴))
197196oveq2d 5934 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → (𝐴 · if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘))) = (𝐴 · ((𝐹𝑀) / 𝐴)))
19831, 131, 133divcanap2d 8811 . . . . . . . . . . . 12 (𝜑 → (𝐴 · ((𝐹𝑀) / 𝐴)) = (𝐹𝑀))
199198ad3antrrr 492 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → (𝐴 · ((𝐹𝑀) / 𝐴)) = (𝐹𝑀))
200197, 199eqtrd 2226 . . . . . . . . . 10 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → (𝐴 · if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘))) = (𝐹𝑀))
201200fveq2d 5558 . . . . . . . . 9 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → (abs‘(𝐴 · if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))) = (abs‘(𝐹𝑀)))
202167ad2antrr 488 . . . . . . . . . . 11 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → ((abs‘𝐴) · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))) = (𝐴 · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
203163, 202eqtrd 2226 . . . . . . . . . 10 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (abs‘(𝐴 · if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))) = (𝐴 · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
204203adantr 276 . . . . . . . . 9 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → (abs‘(𝐴 · if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))) = (𝐴 · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
205179, 201, 2043eqtr2d 2232 . . . . . . . 8 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → (abs‘if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1)))) = (𝐴 · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
206123, 205, 170syl2an2r 595 . . . . . . 7 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) = 𝑀) → (abs‘if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1)))) ≤ (𝐴 · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
207 simplll 533 . . . . . . . . 9 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → 𝜑)
208119adantr 276 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → 𝑀 ∈ ℤ)
20990adantr 276 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → 𝑘 ∈ ℤ)
210 simpr 110 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → 𝑀 < (𝑘 + 1))
211 zleltp1 9372 . . . . . . . . . . . . 13 ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑀𝑘𝑀 < (𝑘 + 1)))
212119, 209, 211syl2an2r 595 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → (𝑀𝑘𝑀 < (𝑘 + 1)))
213210, 212mpbird 167 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → 𝑀𝑘)
214208, 209, 213, 55syl3anbrc 1183 . . . . . . . . . 10 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → 𝑘 ∈ (ℤ𝑀))
215214, 8eleqtrrdi 2287 . . . . . . . . 9 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → 𝑘𝑍)
216 cvgratz.7 . . . . . . . . 9 ((𝜑𝑘𝑍) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹𝑘))))
217207, 215, 216syl2anc 411 . . . . . . . 8 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹𝑘))))
218172adantr 276 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → 𝑀 ∈ ℝ)
219111adantr 276 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → (𝑘 + 1) ∈ ℝ)
220218, 219, 210ltnsymd 8139 . . . . . . . . . 10 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → ¬ (𝑘 + 1) < 𝑀)
221220iffalsed 3567 . . . . . . . . 9 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1))) = (𝐹‘(𝑘 + 1)))
222221fveq2d 5558 . . . . . . . 8 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → (abs‘if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1)))) = (abs‘(𝐹‘(𝑘 + 1))))
223142adantr 276 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → 𝑘 ∈ ℝ)
224218, 223, 213lensymd 8141 . . . . . . . . . . 11 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → ¬ 𝑘 < 𝑀)
225224iffalsed 3567 . . . . . . . . . 10 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)) = (𝐹𝑘))
226225fveq2d 5558 . . . . . . . . 9 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘))) = (abs‘(𝐹𝑘)))
227226oveq2d 5934 . . . . . . . 8 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → (𝐴 · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))) = (𝐴 · (abs‘(𝐹𝑘))))
228217, 222, 2273brtr4d 4061 . . . . . . 7 ((((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) ∧ 𝑀 < (𝑘 + 1)) → (abs‘if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1)))) ≤ (𝐴 · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
229 ztri3or 9360 . . . . . . . 8 (((𝑘 + 1) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑘 + 1) < 𝑀 ∨ (𝑘 + 1) = 𝑀𝑀 < (𝑘 + 1)))
230108, 119, 229syl2anc 411 . . . . . . 7 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) < 𝑀 ∨ (𝑘 + 1) = 𝑀𝑀 < (𝑘 + 1)))
231171, 206, 228, 230mpjao3dan 1318 . . . . . 6 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (abs‘if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1)))) ≤ (𝐴 · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
232 breq1 4032 . . . . . . . . . 10 (𝑖 = (𝑘 + 1) → (𝑖 < 𝑀 ↔ (𝑘 + 1) < 𝑀))
233 oveq2 5926 . . . . . . . . . . . 12 (𝑖 = (𝑘 + 1) → (𝑀𝑖) = (𝑀 − (𝑘 + 1)))
234233oveq2d 5934 . . . . . . . . . . 11 (𝑖 = (𝑘 + 1) → (𝐴↑(𝑀𝑖)) = (𝐴↑(𝑀 − (𝑘 + 1))))
235234oveq2d 5934 . . . . . . . . . 10 (𝑖 = (𝑘 + 1) → ((𝐹𝑀) / (𝐴↑(𝑀𝑖))) = ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))))
236 fveq2 5554 . . . . . . . . . 10 (𝑖 = (𝑘 + 1) → (𝐹𝑖) = (𝐹‘(𝑘 + 1)))
237232, 235, 236ifbieq12d 3583 . . . . . . . . 9 (𝑖 = (𝑘 + 1) → if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)) = if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1))))
238237, 70fvmptg 5633 . . . . . . . 8 (((𝑘 + 1) ∈ ℕ ∧ if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1))) ∈ ℂ) → ((𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))‘(𝑘 + 1)) = if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1))))
239107, 122, 238syl2anc 411 . . . . . . 7 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → ((𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))‘(𝑘 + 1)) = if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1))))
240239fveq2d 5558 . . . . . 6 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (abs‘((𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))‘(𝑘 + 1))) = (abs‘if((𝑘 + 1) < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀 − (𝑘 + 1)))), (𝐹‘(𝑘 + 1)))))
241126, 62, 71syl2anc 411 . . . . . . . 8 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → ((𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))‘𝑘) = if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))
242241fveq2d 5558 . . . . . . 7 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (abs‘((𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))‘𝑘)) = (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘))))
243242oveq2d 5934 . . . . . 6 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (𝐴 · (abs‘((𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))‘𝑘))) = (𝐴 · (abs‘if(𝑘 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑘))), (𝐹𝑘)))))
244231, 240, 2433brtr4d 4061 . . . . 5 (((𝜑 ∧ 1 ≤ 𝑀) ∧ 𝑘 ∈ ℕ) → (abs‘((𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))‘(𝑘 + 1))) ≤ (𝐴 · (abs‘((𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))‘𝑘))))
24579, 81, 82, 86, 244cvgratnn 11674 . . . 4 ((𝜑 ∧ 1 ≤ 𝑀) → seq1( + , (𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))) ∈ dom ⇝ )
246 eqid 2193 . . . . 5 (ℤ‘1) = (ℤ‘1)
247 1zzd 9344 . . . . . 6 ((𝜑 ∧ 1 ≤ 𝑀) → 1 ∈ ℤ)
248 simpr 110 . . . . . 6 ((𝜑 ∧ 1 ≤ 𝑀) → 1 ≤ 𝑀)
249 eluz2 9598 . . . . . 6 (𝑀 ∈ (ℤ‘1) ↔ (1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 1 ≤ 𝑀))
250247, 2, 248, 249syl3anbrc 1183 . . . . 5 ((𝜑 ∧ 1 ≤ 𝑀) → 𝑀 ∈ (ℤ‘1))
251246, 250, 85iserex 11482 . . . 4 ((𝜑 ∧ 1 ≤ 𝑀) → (seq1( + , (𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))) ∈ dom ⇝ ↔ seq𝑀( + , (𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))) ∈ dom ⇝ ))
252245, 251mpbid 147 . . 3 ((𝜑 ∧ 1 ≤ 𝑀) → seq𝑀( + , (𝑖 ∈ ℕ ↦ if(𝑖 < 𝑀, ((𝐹𝑀) / (𝐴↑(𝑀𝑖))), (𝐹𝑖)))) ∈ dom ⇝ )
25378, 252eqeltrd 2270 . 2 ((𝜑 ∧ 1 ≤ 𝑀) → seq𝑀( + , 𝐹) ∈ dom ⇝ )
25433adantr 276 . . . 4 ((𝜑𝑀 ≤ 1) → 𝐴 ∈ ℝ)
25580adantr 276 . . . 4 ((𝜑𝑀 ≤ 1) → 𝐴 < 1)
25634adantr 276 . . . 4 ((𝜑𝑀 ≤ 1) → 0 < 𝐴)
2571adantr 276 . . . . . . 7 ((𝜑𝑀 ≤ 1) → 𝑀 ∈ ℤ)
258257adantr 276 . . . . . 6 (((𝜑𝑀 ≤ 1) ∧ 𝑘 ∈ ℕ) → 𝑀 ∈ ℤ)
259 nnz 9336 . . . . . . 7 (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
260259adantl 277 . . . . . 6 (((𝜑𝑀 ≤ 1) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ)
261258zred 9439 . . . . . . 7 (((𝜑𝑀 ≤ 1) ∧ 𝑘 ∈ ℕ) → 𝑀 ∈ ℝ)
262 1red 8034 . . . . . . 7 (((𝜑𝑀 ≤ 1) ∧ 𝑘 ∈ ℕ) → 1 ∈ ℝ)
263260zred 9439 . . . . . . 7 (((𝜑𝑀 ≤ 1) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ)
264 simplr 528 . . . . . . 7 (((𝜑𝑀 ≤ 1) ∧ 𝑘 ∈ ℕ) → 𝑀 ≤ 1)
265 nnge1 9005 . . . . . . . 8 (𝑘 ∈ ℕ → 1 ≤ 𝑘)
266265adantl 277 . . . . . . 7 (((𝜑𝑀 ≤ 1) ∧ 𝑘 ∈ ℕ) → 1 ≤ 𝑘)
267261, 262, 263, 264, 266letrd 8143 . . . . . 6 (((𝜑𝑀 ≤ 1) ∧ 𝑘 ∈ ℕ) → 𝑀𝑘)
268258, 260, 267, 55syl3anbrc 1183 . . . . 5 (((𝜑𝑀 ≤ 1) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ𝑀))
2698eleq2i 2260 . . . . . . 7 (𝑘𝑍𝑘 ∈ (ℤ𝑀))
270269, 5sylan2br 288 . . . . . 6 ((𝜑𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) ∈ ℂ)
271270adantlr 477 . . . . 5 (((𝜑𝑀 ≤ 1) ∧ 𝑘 ∈ (ℤ𝑀)) → (𝐹𝑘) ∈ ℂ)
272268, 271syldan 282 . . . 4 (((𝜑𝑀 ≤ 1) ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℂ)
273269, 216sylan2br 288 . . . . . 6 ((𝜑𝑘 ∈ (ℤ𝑀)) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹𝑘))))
274273adantlr 477 . . . . 5 (((𝜑𝑀 ≤ 1) ∧ 𝑘 ∈ (ℤ𝑀)) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹𝑘))))
275268, 274syldan 282 . . . 4 (((𝜑𝑀 ≤ 1) ∧ 𝑘 ∈ ℕ) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹𝑘))))
276254, 255, 256, 272, 275cvgratnn 11674 . . 3 ((𝜑𝑀 ≤ 1) → seq1( + , 𝐹) ∈ dom ⇝ )
277 eqid 2193 . . . 4 (ℤ𝑀) = (ℤ𝑀)
278 1zzd 9344 . . . . 5 ((𝜑𝑀 ≤ 1) → 1 ∈ ℤ)
279 simpr 110 . . . . 5 ((𝜑𝑀 ≤ 1) → 𝑀 ≤ 1)
280 eluz2 9598 . . . . 5 (1 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑀 ≤ 1))
281257, 278, 279, 280syl3anbrc 1183 . . . 4 ((𝜑𝑀 ≤ 1) → 1 ∈ (ℤ𝑀))
282277, 281, 271iserex 11482 . . 3 ((𝜑𝑀 ≤ 1) → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq1( + , 𝐹) ∈ dom ⇝ ))
283276, 282mpbird 167 . 2 ((𝜑𝑀 ≤ 1) → seq𝑀( + , 𝐹) ∈ dom ⇝ )
284 1z 9343 . . 3 1 ∈ ℤ
285 zletric 9361 . . 3 ((1 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (1 ≤ 𝑀𝑀 ≤ 1))
286284, 1, 285sylancr 414 . 2 (𝜑 → (1 ≤ 𝑀𝑀 ≤ 1))
287253, 283, 286mpjaodan 799 1 (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 709  DECID wdc 835  w3o 979   = wceq 1364  wcel 2164  wral 2472  ifcif 3557   class class class wbr 4029  cmpt 4090  dom cdm 4659  cfv 5254  (class class class)co 5918  cc 7870  cr 7871  0cc0 7872  1c1 7873   + caddc 7875   · cmul 7877   < clt 8054  cle 8055  cmin 8190   # cap 8600   / cdiv 8691  cn 8982  cz 9317  cuz 9592  +crp 9719  seqcseq 10518  cexp 10609  abscabs 11141  cli 11421
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-coll 4144  ax-sep 4147  ax-nul 4155  ax-pow 4203  ax-pr 4238  ax-un 4464  ax-setind 4569  ax-iinf 4620  ax-cnex 7963  ax-resscn 7964  ax-1cn 7965  ax-1re 7966  ax-icn 7967  ax-addcl 7968  ax-addrcl 7969  ax-mulcl 7970  ax-mulrcl 7971  ax-addcom 7972  ax-mulcom 7973  ax-addass 7974  ax-mulass 7975  ax-distr 7976  ax-i2m1 7977  ax-0lt1 7978  ax-1rid 7979  ax-0id 7980  ax-rnegex 7981  ax-precex 7982  ax-cnre 7983  ax-pre-ltirr 7984  ax-pre-ltwlin 7985  ax-pre-lttrn 7986  ax-pre-apti 7987  ax-pre-ltadd 7988  ax-pre-mulgt0 7989  ax-pre-mulext 7990  ax-arch 7991  ax-caucvg 7992
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-reu 2479  df-rmo 2480  df-rab 2481  df-v 2762  df-sbc 2986  df-csb 3081  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3447  df-if 3558  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-int 3871  df-iun 3914  df-br 4030  df-opab 4091  df-mpt 4092  df-tr 4128  df-id 4324  df-po 4327  df-iso 4328  df-iord 4397  df-on 4399  df-ilim 4400  df-suc 4402  df-iom 4623  df-xp 4665  df-rel 4666  df-cnv 4667  df-co 4668  df-dm 4669  df-rn 4670  df-res 4671  df-ima 4672  df-iota 5215  df-fun 5256  df-fn 5257  df-f 5258  df-f1 5259  df-fo 5260  df-f1o 5261  df-fv 5262  df-isom 5263  df-riota 5873  df-ov 5921  df-oprab 5922  df-mpo 5923  df-1st 6193  df-2nd 6194  df-recs 6358  df-irdg 6423  df-frec 6444  df-1o 6469  df-oadd 6473  df-er 6587  df-en 6795  df-dom 6796  df-fin 6797  df-pnf 8056  df-mnf 8057  df-xr 8058  df-ltxr 8059  df-le 8060  df-sub 8192  df-neg 8193  df-reap 8594  df-ap 8601  df-div 8692  df-inn 8983  df-2 9041  df-3 9042  df-4 9043  df-n0 9241  df-z 9318  df-uz 9593  df-q 9685  df-rp 9720  df-ico 9960  df-fz 10075  df-fzo 10209  df-seqfrec 10519  df-exp 10610  df-ihash 10847  df-cj 10986  df-re 10987  df-im 10988  df-rsqrt 11142  df-abs 11143  df-clim 11422  df-sumdc 11497
This theorem is referenced by:  cvgratgt0  11676
  Copyright terms: Public domain W3C validator