Step | Hyp | Ref
| Expression |
1 | | eqid 2170 |
. . 3
⊢
(ℤ≥‘(𝑁 + 1)) =
(ℤ≥‘(𝑁 + 1)) |
2 | | clim2div.2 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ 𝑍) |
3 | | eluzelz 9483 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
4 | | clim2div.1 |
. . . . . 6
⊢ 𝑍 =
(ℤ≥‘𝑀) |
5 | 3, 4 | eleq2s 2265 |
. . . . 5
⊢ (𝑁 ∈ 𝑍 → 𝑁 ∈ ℤ) |
6 | 2, 5 | syl 14 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℤ) |
7 | 6 | peano2zd 9324 |
. . 3
⊢ (𝜑 → (𝑁 + 1) ∈ ℤ) |
8 | | clim2div.4 |
. . 3
⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ 𝐴) |
9 | | eluzel2 9479 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
10 | 9, 4 | eleq2s 2265 |
. . . . . . 7
⊢ (𝑁 ∈ 𝑍 → 𝑀 ∈ ℤ) |
11 | 2, 10 | syl 14 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
12 | | clim2div.3 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
13 | 4, 11, 12 | prodf 11488 |
. . . . 5
⊢ (𝜑 → seq𝑀( · , 𝐹):𝑍⟶ℂ) |
14 | 13, 2 | ffvelrnd 5629 |
. . . 4
⊢ (𝜑 → (seq𝑀( · , 𝐹)‘𝑁) ∈ ℂ) |
15 | | clim2divap.5 |
. . . 4
⊢ (𝜑 → (seq𝑀( · , 𝐹)‘𝑁) # 0) |
16 | 14, 15 | recclapd 8685 |
. . 3
⊢ (𝜑 → (1 / (seq𝑀( · , 𝐹)‘𝑁)) ∈ ℂ) |
17 | | seqex 10390 |
. . . 4
⊢ seq(𝑁 + 1)( · , 𝐹) ∈ V |
18 | 17 | a1i 9 |
. . 3
⊢ (𝜑 → seq(𝑁 + 1)( · , 𝐹) ∈ V) |
19 | 2, 4 | eleqtrdi 2263 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
20 | | peano2uz 9529 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑁 + 1) ∈
(ℤ≥‘𝑀)) |
21 | 19, 20 | syl 14 |
. . . . . 6
⊢ (𝜑 → (𝑁 + 1) ∈
(ℤ≥‘𝑀)) |
22 | 21, 4 | eleqtrrdi 2264 |
. . . . 5
⊢ (𝜑 → (𝑁 + 1) ∈ 𝑍) |
23 | 4 | uztrn2 9491 |
. . . . 5
⊢ (((𝑁 + 1) ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑗 ∈ 𝑍) |
24 | 22, 23 | sylan 281 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑗 ∈ 𝑍) |
25 | 13 | ffvelrnda 5628 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (seq𝑀( · , 𝐹)‘𝑗) ∈ ℂ) |
26 | 24, 25 | syldan 280 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → (seq𝑀( · , 𝐹)‘𝑗) ∈ ℂ) |
27 | | mulcl 7888 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑘 · 𝑥) ∈ ℂ) |
28 | 27 | adantl 275 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 · 𝑥) ∈ ℂ) |
29 | | mulass 7892 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑘 · 𝑥) · 𝑦) = (𝑘 · (𝑥 · 𝑦))) |
30 | 29 | adantl 275 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → ((𝑘 · 𝑥) · 𝑦) = (𝑘 · (𝑥 · 𝑦))) |
31 | | simpr 109 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑗 ∈
(ℤ≥‘(𝑁 + 1))) |
32 | 19 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑁 ∈ (ℤ≥‘𝑀)) |
33 | 4 | eleq2i 2237 |
. . . . . . . . 9
⊢ (𝑘 ∈ 𝑍 ↔ 𝑘 ∈ (ℤ≥‘𝑀)) |
34 | 33, 12 | sylan2br 286 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ) |
35 | 34 | adantlr 474 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ) |
36 | 28, 30, 31, 32, 35 | seq3split 10422 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → (seq𝑀( · , 𝐹)‘𝑗) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑗))) |
37 | 36 | eqcomd 2176 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑗)) = (seq𝑀( · , 𝐹)‘𝑗)) |
38 | 14 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → (seq𝑀( · , 𝐹)‘𝑁) ∈ ℂ) |
39 | 4 | uztrn2 9491 |
. . . . . . . . . 10
⊢ (((𝑁 + 1) ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑘 ∈ 𝑍) |
40 | 22, 39 | sylan 281 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑘 ∈ 𝑍) |
41 | 40, 12 | syldan 280 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝐹‘𝑘) ∈ ℂ) |
42 | 1, 7, 41 | prodf 11488 |
. . . . . . 7
⊢ (𝜑 → seq(𝑁 + 1)( · , 𝐹):(ℤ≥‘(𝑁 +
1))⟶ℂ) |
43 | 42 | ffvelrnda 5628 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → (seq(𝑁 + 1)( · , 𝐹)‘𝑗) ∈ ℂ) |
44 | 15 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → (seq𝑀( · , 𝐹)‘𝑁) # 0) |
45 | 26, 38, 43, 44 | divmulapd 8716 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → (((seq𝑀( · , 𝐹)‘𝑗) / (seq𝑀( · , 𝐹)‘𝑁)) = (seq(𝑁 + 1)( · , 𝐹)‘𝑗) ↔ ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑗)) = (seq𝑀( · , 𝐹)‘𝑗))) |
46 | 37, 45 | mpbird 166 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → ((seq𝑀( · , 𝐹)‘𝑗) / (seq𝑀( · , 𝐹)‘𝑁)) = (seq(𝑁 + 1)( · , 𝐹)‘𝑗)) |
47 | 26, 38, 44 | divrecap2d 8698 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → ((seq𝑀( · , 𝐹)‘𝑗) / (seq𝑀( · , 𝐹)‘𝑁)) = ((1 / (seq𝑀( · , 𝐹)‘𝑁)) · (seq𝑀( · , 𝐹)‘𝑗))) |
48 | 46, 47 | eqtr3d 2205 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑁 + 1))) → (seq(𝑁 + 1)( · , 𝐹)‘𝑗) = ((1 / (seq𝑀( · , 𝐹)‘𝑁)) · (seq𝑀( · , 𝐹)‘𝑗))) |
49 | 1, 7, 8, 16, 18, 26, 48 | climmulc2 11281 |
. 2
⊢ (𝜑 → seq(𝑁 + 1)( · , 𝐹) ⇝ ((1 / (seq𝑀( · , 𝐹)‘𝑁)) · 𝐴)) |
50 | | climcl 11232 |
. . . 4
⊢ (seq𝑀( · , 𝐹) ⇝ 𝐴 → 𝐴 ∈ ℂ) |
51 | 8, 50 | syl 14 |
. . 3
⊢ (𝜑 → 𝐴 ∈ ℂ) |
52 | 51, 14, 15 | divrecap2d 8698 |
. 2
⊢ (𝜑 → (𝐴 / (seq𝑀( · , 𝐹)‘𝑁)) = ((1 / (seq𝑀( · , 𝐹)‘𝑁)) · 𝐴)) |
53 | 49, 52 | breqtrrd 4015 |
1
⊢ (𝜑 → seq(𝑁 + 1)( · , 𝐹) ⇝ (𝐴 / (seq𝑀( · , 𝐹)‘𝑁))) |