| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2736 | . . 3
⊢
(ℤ≥‘(𝑁 + 1)) =
(ℤ≥‘(𝑁 + 1)) | 
| 2 |  | clim2div.2 | . . . . 5
⊢ (𝜑 → 𝑁 ∈ 𝑍) | 
| 3 |  | eluzelz 12889 | . . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) | 
| 4 |  | clim2div.1 | . . . . . 6
⊢ 𝑍 =
(ℤ≥‘𝑀) | 
| 5 | 3, 4 | eleq2s 2858 | . . . . 5
⊢ (𝑁 ∈ 𝑍 → 𝑁 ∈ ℤ) | 
| 6 | 2, 5 | syl 17 | . . . 4
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 7 | 6 | peano2zd 12727 | . . 3
⊢ (𝜑 → (𝑁 + 1) ∈ ℤ) | 
| 8 |  | clim2div.4 | . . 3
⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ 𝐴) | 
| 9 |  | eluzel2 12884 | . . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) | 
| 10 | 9, 4 | eleq2s 2858 | . . . . . . 7
⊢ (𝑁 ∈ 𝑍 → 𝑀 ∈ ℤ) | 
| 11 | 2, 10 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 12 |  | clim2div.3 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) | 
| 13 | 4, 11, 12 | prodf 15924 | . . . . 5
⊢ (𝜑 → seq𝑀( · , 𝐹):𝑍⟶ℂ) | 
| 14 | 13, 2 | ffvelcdmd 7104 | . . . 4
⊢ (𝜑 → (seq𝑀( · , 𝐹)‘𝑁) ∈ ℂ) | 
| 15 |  | clim2div.5 | . . . 4
⊢ (𝜑 → (seq𝑀( · , 𝐹)‘𝑁) ≠ 0) | 
| 16 | 14, 15 | reccld 12037 | . . 3
⊢ (𝜑 → (1 / (seq𝑀( · , 𝐹)‘𝑁)) ∈ ℂ) | 
| 17 |  | seqex 14045 | . . . 4
⊢ seq(𝑁 + 1)( · , 𝐹) ∈ V | 
| 18 | 17 | a1i 11 | . . 3
⊢ (𝜑 → seq(𝑁 + 1)( · , 𝐹) ∈ V) | 
| 19 | 2, 4 | eleqtrdi 2850 | . . . . . . 7
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) | 
| 20 |  | peano2uz 12944 | . . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑁 + 1) ∈
(ℤ≥‘𝑀)) | 
| 21 | 19, 20 | syl 17 | . . . . . 6
⊢ (𝜑 → (𝑁 + 1) ∈
(ℤ≥‘𝑀)) | 
| 22 | 21, 4 | eleqtrrdi 2851 | . . . . 5
⊢ (𝜑 → (𝑁 + 1) ∈ 𝑍) | 
| 23 | 4 | uztrn2 12898 | . . . . 5
⊢ (((𝑁 + 1) ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑗 ∈ 𝑍) | 
| 24 | 22, 23 | sylan 580 | . . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑗 ∈ 𝑍) | 
| 25 | 13 | ffvelcdmda 7103 | . . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (seq𝑀( · , 𝐹)‘𝑗) ∈ ℂ) | 
| 26 | 24, 25 | syldan 591 | . . 3
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → (seq𝑀( · , 𝐹)‘𝑗) ∈ ℂ) | 
| 27 |  | mulcl 11240 | . . . . . . . 8
⊢ ((𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑘 · 𝑥) ∈ ℂ) | 
| 28 | 27 | adantl 481 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 · 𝑥) ∈ ℂ) | 
| 29 |  | mulass 11244 | . . . . . . . 8
⊢ ((𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑘 · 𝑥) · 𝑦) = (𝑘 · (𝑥 · 𝑦))) | 
| 30 | 29 | adantl 481 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → ((𝑘 · 𝑥) · 𝑦) = (𝑘 · (𝑥 · 𝑦))) | 
| 31 |  | simpr 484 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑗 ∈
(ℤ≥‘(𝑁 + 1))) | 
| 32 | 19 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈ (ℤ≥‘𝑀)) | 
| 33 |  | elfzuz 13561 | . . . . . . . . . 10
⊢ (𝑘 ∈ (𝑀...𝑗) → 𝑘 ∈ (ℤ≥‘𝑀)) | 
| 34 | 33, 4 | eleqtrrdi 2851 | . . . . . . . . 9
⊢ (𝑘 ∈ (𝑀...𝑗) → 𝑘 ∈ 𝑍) | 
| 35 | 34, 12 | sylan2 593 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹‘𝑘) ∈ ℂ) | 
| 36 | 35 | adantlr 715 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹‘𝑘) ∈ ℂ) | 
| 37 | 28, 30, 31, 32, 36 | seqsplit 14077 | . . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → (seq𝑀( · , 𝐹)‘𝑗) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑗))) | 
| 38 | 37 | eqcomd 2742 | . . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑗)) = (seq𝑀( · , 𝐹)‘𝑗)) | 
| 39 | 14 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → (seq𝑀( · , 𝐹)‘𝑁) ∈ ℂ) | 
| 40 | 4 | uztrn2 12898 | . . . . . . . . . 10
⊢ (((𝑁 + 1) ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑘 ∈ 𝑍) | 
| 41 | 22, 40 | sylan 580 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑘 ∈ 𝑍) | 
| 42 | 41, 12 | syldan 591 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝐹‘𝑘) ∈ ℂ) | 
| 43 | 1, 7, 42 | prodf 15924 | . . . . . . 7
⊢ (𝜑 → seq(𝑁 + 1)( · , 𝐹):(ℤ≥‘(𝑁 +
1))⟶ℂ) | 
| 44 | 43 | ffvelcdmda 7103 | . . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → (seq(𝑁 + 1)( · , 𝐹)‘𝑗) ∈ ℂ) | 
| 45 | 15 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → (seq𝑀( · , 𝐹)‘𝑁) ≠ 0) | 
| 46 | 26, 39, 44, 45 | divmuld 12066 | . . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → (((seq𝑀( · , 𝐹)‘𝑗) / (seq𝑀( · , 𝐹)‘𝑁)) = (seq(𝑁 + 1)( · , 𝐹)‘𝑗) ↔ ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑗)) = (seq𝑀( · , 𝐹)‘𝑗))) | 
| 47 | 38, 46 | mpbird 257 | . . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → ((seq𝑀( · , 𝐹)‘𝑗) / (seq𝑀( · , 𝐹)‘𝑁)) = (seq(𝑁 + 1)( · , 𝐹)‘𝑗)) | 
| 48 | 26, 39, 45 | divrec2d 12048 | . . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → ((seq𝑀( · , 𝐹)‘𝑗) / (seq𝑀( · , 𝐹)‘𝑁)) = ((1 / (seq𝑀( · , 𝐹)‘𝑁)) · (seq𝑀( · , 𝐹)‘𝑗))) | 
| 49 | 47, 48 | eqtr3d 2778 | . . 3
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → (seq(𝑁 + 1)( · , 𝐹)‘𝑗) = ((1 / (seq𝑀( · , 𝐹)‘𝑁)) · (seq𝑀( · , 𝐹)‘𝑗))) | 
| 50 | 1, 7, 8, 16, 18, 26, 49 | climmulc2 15674 | . 2
⊢ (𝜑 → seq(𝑁 + 1)( · , 𝐹) ⇝ ((1 / (seq𝑀( · , 𝐹)‘𝑁)) · 𝐴)) | 
| 51 |  | climcl 15536 | . . . 4
⊢ (seq𝑀( · , 𝐹) ⇝ 𝐴 → 𝐴 ∈ ℂ) | 
| 52 | 8, 51 | syl 17 | . . 3
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 53 | 52, 14, 15 | divrec2d 12048 | . 2
⊢ (𝜑 → (𝐴 / (seq𝑀( · , 𝐹)‘𝑁)) = ((1 / (seq𝑀( · , 𝐹)‘𝑁)) · 𝐴)) | 
| 54 | 50, 53 | breqtrrd 5170 | 1
⊢ (𝜑 → seq(𝑁 + 1)( · , 𝐹) ⇝ (𝐴 / (seq𝑀( · , 𝐹)‘𝑁))) |