Step | Hyp | Ref
| Expression |
1 | | eqid 2157 |
. 2
⊢
(ℤ≥‘(𝑁 + 1)) =
(ℤ≥‘(𝑁 + 1)) |
2 | | clim2prod.1 |
. . . . 5
⊢ 𝑍 =
(ℤ≥‘𝑀) |
3 | | uzssz 9453 |
. . . . 5
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
4 | 2, 3 | eqsstri 3160 |
. . . 4
⊢ 𝑍 ⊆
ℤ |
5 | | clim2prod.2 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ 𝑍) |
6 | 4, 5 | sseldi 3126 |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℤ) |
7 | 6 | peano2zd 9284 |
. 2
⊢ (𝜑 → (𝑁 + 1) ∈ ℤ) |
8 | | clim2prod.4 |
. 2
⊢ (𝜑 → seq(𝑁 + 1)( · , 𝐹) ⇝ 𝐴) |
9 | 5, 2 | eleqtrdi 2250 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
10 | | eluzel2 9439 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
11 | 9, 10 | syl 14 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
12 | | clim2prod.3 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
13 | 2, 11, 12 | prodf 11430 |
. . 3
⊢ (𝜑 → seq𝑀( · , 𝐹):𝑍⟶ℂ) |
14 | 13, 5 | ffvelrnd 5602 |
. 2
⊢ (𝜑 → (seq𝑀( · , 𝐹)‘𝑁) ∈ ℂ) |
15 | | seqex 10341 |
. . 3
⊢ seq𝑀( · , 𝐹) ∈ V |
16 | 15 | a1i 9 |
. 2
⊢ (𝜑 → seq𝑀( · , 𝐹) ∈ V) |
17 | | peano2uz 9489 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑁 + 1) ∈
(ℤ≥‘𝑀)) |
18 | | uzss 9454 |
. . . . . . . 8
⊢ ((𝑁 + 1) ∈
(ℤ≥‘𝑀) →
(ℤ≥‘(𝑁 + 1)) ⊆
(ℤ≥‘𝑀)) |
19 | 9, 17, 18 | 3syl 17 |
. . . . . . 7
⊢ (𝜑 →
(ℤ≥‘(𝑁 + 1)) ⊆
(ℤ≥‘𝑀)) |
20 | 19, 2 | sseqtrrdi 3177 |
. . . . . 6
⊢ (𝜑 →
(ℤ≥‘(𝑁 + 1)) ⊆ 𝑍) |
21 | 20 | sselda 3128 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑘 ∈ 𝑍) |
22 | 21, 12 | syldan 280 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝐹‘𝑘) ∈ ℂ) |
23 | 1, 7, 22 | prodf 11430 |
. . 3
⊢ (𝜑 → seq(𝑁 + 1)( · , 𝐹):(ℤ≥‘(𝑁 +
1))⟶ℂ) |
24 | 23 | ffvelrnda 5601 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (seq(𝑁 + 1)( · , 𝐹)‘𝑘) ∈ ℂ) |
25 | | fveq2 5467 |
. . . . . 6
⊢ (𝑥 = (𝑁 + 1) → (seq𝑀( · , 𝐹)‘𝑥) = (seq𝑀( · , 𝐹)‘(𝑁 + 1))) |
26 | | fveq2 5467 |
. . . . . . 7
⊢ (𝑥 = (𝑁 + 1) → (seq(𝑁 + 1)( · , 𝐹)‘𝑥) = (seq(𝑁 + 1)( · , 𝐹)‘(𝑁 + 1))) |
27 | 26 | oveq2d 5837 |
. . . . . 6
⊢ (𝑥 = (𝑁 + 1) → ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑥)) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑁 + 1)))) |
28 | 25, 27 | eqeq12d 2172 |
. . . . 5
⊢ (𝑥 = (𝑁 + 1) → ((seq𝑀( · , 𝐹)‘𝑥) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑥)) ↔ (seq𝑀( · , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑁 + 1))))) |
29 | 28 | imbi2d 229 |
. . . 4
⊢ (𝑥 = (𝑁 + 1) → ((𝜑 → (seq𝑀( · , 𝐹)‘𝑥) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑥))) ↔ (𝜑 → (seq𝑀( · , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑁 + 1)))))) |
30 | | fveq2 5467 |
. . . . . 6
⊢ (𝑥 = 𝑛 → (seq𝑀( · , 𝐹)‘𝑥) = (seq𝑀( · , 𝐹)‘𝑛)) |
31 | | fveq2 5467 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (seq(𝑁 + 1)( · , 𝐹)‘𝑥) = (seq(𝑁 + 1)( · , 𝐹)‘𝑛)) |
32 | 31 | oveq2d 5837 |
. . . . . 6
⊢ (𝑥 = 𝑛 → ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑥)) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛))) |
33 | 30, 32 | eqeq12d 2172 |
. . . . 5
⊢ (𝑥 = 𝑛 → ((seq𝑀( · , 𝐹)‘𝑥) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑥)) ↔ (seq𝑀( · , 𝐹)‘𝑛) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛)))) |
34 | 33 | imbi2d 229 |
. . . 4
⊢ (𝑥 = 𝑛 → ((𝜑 → (seq𝑀( · , 𝐹)‘𝑥) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑥))) ↔ (𝜑 → (seq𝑀( · , 𝐹)‘𝑛) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛))))) |
35 | | fveq2 5467 |
. . . . . 6
⊢ (𝑥 = (𝑛 + 1) → (seq𝑀( · , 𝐹)‘𝑥) = (seq𝑀( · , 𝐹)‘(𝑛 + 1))) |
36 | | fveq2 5467 |
. . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → (seq(𝑁 + 1)( · , 𝐹)‘𝑥) = (seq(𝑁 + 1)( · , 𝐹)‘(𝑛 + 1))) |
37 | 36 | oveq2d 5837 |
. . . . . 6
⊢ (𝑥 = (𝑛 + 1) → ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑥)) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑛 + 1)))) |
38 | 35, 37 | eqeq12d 2172 |
. . . . 5
⊢ (𝑥 = (𝑛 + 1) → ((seq𝑀( · , 𝐹)‘𝑥) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑥)) ↔ (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑛 + 1))))) |
39 | 38 | imbi2d 229 |
. . . 4
⊢ (𝑥 = (𝑛 + 1) → ((𝜑 → (seq𝑀( · , 𝐹)‘𝑥) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑥))) ↔ (𝜑 → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑛 + 1)))))) |
40 | | fveq2 5467 |
. . . . . 6
⊢ (𝑥 = 𝑘 → (seq𝑀( · , 𝐹)‘𝑥) = (seq𝑀( · , 𝐹)‘𝑘)) |
41 | | fveq2 5467 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → (seq(𝑁 + 1)( · , 𝐹)‘𝑥) = (seq(𝑁 + 1)( · , 𝐹)‘𝑘)) |
42 | 41 | oveq2d 5837 |
. . . . . 6
⊢ (𝑥 = 𝑘 → ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑥)) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑘))) |
43 | 40, 42 | eqeq12d 2172 |
. . . . 5
⊢ (𝑥 = 𝑘 → ((seq𝑀( · , 𝐹)‘𝑥) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑥)) ↔ (seq𝑀( · , 𝐹)‘𝑘) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑘)))) |
44 | 43 | imbi2d 229 |
. . . 4
⊢ (𝑥 = 𝑘 → ((𝜑 → (seq𝑀( · , 𝐹)‘𝑥) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑥))) ↔ (𝜑 → (seq𝑀( · , 𝐹)‘𝑘) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑘))))) |
45 | 2 | eleq2i 2224 |
. . . . . . . 8
⊢ (𝑘 ∈ 𝑍 ↔ 𝑘 ∈ (ℤ≥‘𝑀)) |
46 | 45, 12 | sylan2br 286 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ) |
47 | | mulcl 7854 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℂ ∧ 𝑣 ∈ ℂ) → (𝑘 · 𝑣) ∈ ℂ) |
48 | 47 | adantl 275 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (𝑘 · 𝑣) ∈ ℂ) |
49 | 9, 46, 48 | seq3p1 10356 |
. . . . . 6
⊢ (𝜑 → (seq𝑀( · , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( · , 𝐹)‘𝑁) · (𝐹‘(𝑁 + 1)))) |
50 | 7, 22, 48 | seq3-1 10354 |
. . . . . . 7
⊢ (𝜑 → (seq(𝑁 + 1)( · , 𝐹)‘(𝑁 + 1)) = (𝐹‘(𝑁 + 1))) |
51 | 50 | oveq2d 5837 |
. . . . . 6
⊢ (𝜑 → ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑁 + 1))) = ((seq𝑀( · , 𝐹)‘𝑁) · (𝐹‘(𝑁 + 1)))) |
52 | 49, 51 | eqtr4d 2193 |
. . . . 5
⊢ (𝜑 → (seq𝑀( · , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑁 + 1)))) |
53 | 52 | a1i 9 |
. . . 4
⊢ ((𝑁 + 1) ∈ ℤ →
(𝜑 → (seq𝑀( · , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑁 + 1))))) |
54 | 19 | sselda 3128 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑛 ∈
(ℤ≥‘𝑀)) |
55 | 46 | adantlr 469 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ) |
56 | 47 | adantl 275 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ (𝑘 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (𝑘 · 𝑣) ∈ ℂ) |
57 | 54, 55, 56 | seq3p1 10356 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1)))) |
58 | 57 | adantr 274 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ (seq𝑀( · , 𝐹)‘𝑛) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛))) → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1)))) |
59 | | oveq1 5828 |
. . . . . . . . 9
⊢
((seq𝑀( · ,
𝐹)‘𝑛) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛)) → ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1))) = (((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛)) · (𝐹‘(𝑛 + 1)))) |
60 | 59 | adantl 275 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ (seq𝑀( · , 𝐹)‘𝑛) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛))) → ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1))) = (((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛)) · (𝐹‘(𝑛 + 1)))) |
61 | 14 | adantr 274 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) → (seq𝑀( · , 𝐹)‘𝑁) ∈ ℂ) |
62 | 23 | ffvelrnda 5601 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) → (seq(𝑁 + 1)( · , 𝐹)‘𝑛) ∈ ℂ) |
63 | | peano2uz 9489 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (𝑛 + 1) ∈
(ℤ≥‘𝑀)) |
64 | 63, 2 | eleqtrrdi 2251 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (𝑛 + 1) ∈ 𝑍) |
65 | 54, 64 | syl 14 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑛 + 1) ∈ 𝑍) |
66 | 12 | ralrimiva 2530 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ∈ ℂ) |
67 | | fveq2 5467 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝑛 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑛 + 1))) |
68 | 67 | eleq1d 2226 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘𝑘) ∈ ℂ ↔ (𝐹‘(𝑛 + 1)) ∈ ℂ)) |
69 | 68 | rspcv 2812 |
. . . . . . . . . . . . 13
⊢ ((𝑛 + 1) ∈ 𝑍 → (∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ∈ ℂ → (𝐹‘(𝑛 + 1)) ∈ ℂ)) |
70 | 66, 69 | mpan9 279 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 + 1) ∈ 𝑍) → (𝐹‘(𝑛 + 1)) ∈ ℂ) |
71 | 65, 70 | syldan 280 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) → (𝐹‘(𝑛 + 1)) ∈ ℂ) |
72 | 61, 62, 71 | mulassd 7896 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) → (((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛)) · (𝐹‘(𝑛 + 1))) = ((seq𝑀( · , 𝐹)‘𝑁) · ((seq(𝑁 + 1)( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1))))) |
73 | 72 | adantr 274 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ (seq𝑀( · , 𝐹)‘𝑛) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛))) → (((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛)) · (𝐹‘(𝑛 + 1))) = ((seq𝑀( · , 𝐹)‘𝑁) · ((seq(𝑁 + 1)( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1))))) |
74 | | simpr 109 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑛 ∈
(ℤ≥‘(𝑁 + 1))) |
75 | 22 | adantlr 469 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝐹‘𝑘) ∈ ℂ) |
76 | 74, 75, 56 | seq3p1 10356 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) → (seq(𝑁 + 1)( · , 𝐹)‘(𝑛 + 1)) = ((seq(𝑁 + 1)( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1)))) |
77 | 76 | oveq2d 5837 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) → ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑛 + 1))) = ((seq𝑀( · , 𝐹)‘𝑁) · ((seq(𝑁 + 1)( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1))))) |
78 | 77 | adantr 274 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ (seq𝑀( · , 𝐹)‘𝑛) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛))) → ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑛 + 1))) = ((seq𝑀( · , 𝐹)‘𝑁) · ((seq(𝑁 + 1)( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1))))) |
79 | 73, 78 | eqtr4d 2193 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ (seq𝑀( · , 𝐹)‘𝑛) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛))) → (((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛)) · (𝐹‘(𝑛 + 1))) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑛 + 1)))) |
80 | 58, 60, 79 | 3eqtrd 2194 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ (seq𝑀( · , 𝐹)‘𝑛) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛))) → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑛 + 1)))) |
81 | 80 | exp31 362 |
. . . . . 6
⊢ (𝜑 → (𝑛 ∈ (ℤ≥‘(𝑁 + 1)) → ((seq𝑀( · , 𝐹)‘𝑛) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛)) → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑛 + 1)))))) |
82 | 81 | com12 30 |
. . . . 5
⊢ (𝑛 ∈
(ℤ≥‘(𝑁 + 1)) → (𝜑 → ((seq𝑀( · , 𝐹)‘𝑛) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛)) → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑛 + 1)))))) |
83 | 82 | a2d 26 |
. . . 4
⊢ (𝑛 ∈
(ℤ≥‘(𝑁 + 1)) → ((𝜑 → (seq𝑀( · , 𝐹)‘𝑛) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛))) → (𝜑 → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑛 + 1)))))) |
84 | 29, 34, 39, 44, 53, 83 | uzind4 9494 |
. . 3
⊢ (𝑘 ∈
(ℤ≥‘(𝑁 + 1)) → (𝜑 → (seq𝑀( · , 𝐹)‘𝑘) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑘)))) |
85 | 84 | impcom 124 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (seq𝑀( · , 𝐹)‘𝑘) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑘))) |
86 | 1, 7, 8, 14, 16, 24, 85 | climmulc2 11223 |
1
⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ ((seq𝑀( · , 𝐹)‘𝑁) · 𝐴)) |