| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2737 | . 2
⊢
(ℤ≥‘(𝑁 + 1)) =
(ℤ≥‘(𝑁 + 1)) | 
| 2 |  | clim2prod.1 | . . . . 5
⊢ 𝑍 =
(ℤ≥‘𝑀) | 
| 3 |  | uzssz 12899 | . . . . 5
⊢
(ℤ≥‘𝑀) ⊆ ℤ | 
| 4 | 2, 3 | eqsstri 4030 | . . . 4
⊢ 𝑍 ⊆
ℤ | 
| 5 |  | clim2prod.2 | . . . 4
⊢ (𝜑 → 𝑁 ∈ 𝑍) | 
| 6 | 4, 5 | sselid 3981 | . . 3
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 7 | 6 | peano2zd 12725 | . 2
⊢ (𝜑 → (𝑁 + 1) ∈ ℤ) | 
| 8 |  | clim2prod.4 | . 2
⊢ (𝜑 → seq(𝑁 + 1)( · , 𝐹) ⇝ 𝐴) | 
| 9 | 5, 2 | eleqtrdi 2851 | . . . . 5
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) | 
| 10 |  | eluzel2 12883 | . . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) | 
| 11 | 9, 10 | syl 17 | . . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 12 |  | clim2prod.3 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) | 
| 13 | 2, 11, 12 | prodf 15923 | . . 3
⊢ (𝜑 → seq𝑀( · , 𝐹):𝑍⟶ℂ) | 
| 14 | 13, 5 | ffvelcdmd 7105 | . 2
⊢ (𝜑 → (seq𝑀( · , 𝐹)‘𝑁) ∈ ℂ) | 
| 15 |  | seqex 14044 | . . 3
⊢ seq𝑀( · , 𝐹) ∈ V | 
| 16 | 15 | a1i 11 | . 2
⊢ (𝜑 → seq𝑀( · , 𝐹) ∈ V) | 
| 17 |  | peano2uz 12943 | . . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑁 + 1) ∈
(ℤ≥‘𝑀)) | 
| 18 |  | uzss 12901 | . . . . . . . 8
⊢ ((𝑁 + 1) ∈
(ℤ≥‘𝑀) →
(ℤ≥‘(𝑁 + 1)) ⊆
(ℤ≥‘𝑀)) | 
| 19 | 9, 17, 18 | 3syl 18 | . . . . . . 7
⊢ (𝜑 →
(ℤ≥‘(𝑁 + 1)) ⊆
(ℤ≥‘𝑀)) | 
| 20 | 19, 2 | sseqtrrdi 4025 | . . . . . 6
⊢ (𝜑 →
(ℤ≥‘(𝑁 + 1)) ⊆ 𝑍) | 
| 21 | 20 | sselda 3983 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑘 ∈ 𝑍) | 
| 22 | 21, 12 | syldan 591 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (𝐹‘𝑘) ∈ ℂ) | 
| 23 | 1, 7, 22 | prodf 15923 | . . 3
⊢ (𝜑 → seq(𝑁 + 1)( · , 𝐹):(ℤ≥‘(𝑁 +
1))⟶ℂ) | 
| 24 | 23 | ffvelcdmda 7104 | . 2
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (seq(𝑁 + 1)( · , 𝐹)‘𝑘) ∈ ℂ) | 
| 25 |  | fveq2 6906 | . . . . . 6
⊢ (𝑥 = (𝑁 + 1) → (seq𝑀( · , 𝐹)‘𝑥) = (seq𝑀( · , 𝐹)‘(𝑁 + 1))) | 
| 26 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑥 = (𝑁 + 1) → (seq(𝑁 + 1)( · , 𝐹)‘𝑥) = (seq(𝑁 + 1)( · , 𝐹)‘(𝑁 + 1))) | 
| 27 | 26 | oveq2d 7447 | . . . . . 6
⊢ (𝑥 = (𝑁 + 1) → ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑥)) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑁 + 1)))) | 
| 28 | 25, 27 | eqeq12d 2753 | . . . . 5
⊢ (𝑥 = (𝑁 + 1) → ((seq𝑀( · , 𝐹)‘𝑥) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑥)) ↔ (seq𝑀( · , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑁 + 1))))) | 
| 29 | 28 | imbi2d 340 | . . . 4
⊢ (𝑥 = (𝑁 + 1) → ((𝜑 → (seq𝑀( · , 𝐹)‘𝑥) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑥))) ↔ (𝜑 → (seq𝑀( · , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑁 + 1)))))) | 
| 30 |  | fveq2 6906 | . . . . . 6
⊢ (𝑥 = 𝑛 → (seq𝑀( · , 𝐹)‘𝑥) = (seq𝑀( · , 𝐹)‘𝑛)) | 
| 31 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑥 = 𝑛 → (seq(𝑁 + 1)( · , 𝐹)‘𝑥) = (seq(𝑁 + 1)( · , 𝐹)‘𝑛)) | 
| 32 | 31 | oveq2d 7447 | . . . . . 6
⊢ (𝑥 = 𝑛 → ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑥)) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛))) | 
| 33 | 30, 32 | eqeq12d 2753 | . . . . 5
⊢ (𝑥 = 𝑛 → ((seq𝑀( · , 𝐹)‘𝑥) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑥)) ↔ (seq𝑀( · , 𝐹)‘𝑛) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛)))) | 
| 34 | 33 | imbi2d 340 | . . . 4
⊢ (𝑥 = 𝑛 → ((𝜑 → (seq𝑀( · , 𝐹)‘𝑥) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑥))) ↔ (𝜑 → (seq𝑀( · , 𝐹)‘𝑛) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛))))) | 
| 35 |  | fveq2 6906 | . . . . . 6
⊢ (𝑥 = (𝑛 + 1) → (seq𝑀( · , 𝐹)‘𝑥) = (seq𝑀( · , 𝐹)‘(𝑛 + 1))) | 
| 36 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → (seq(𝑁 + 1)( · , 𝐹)‘𝑥) = (seq(𝑁 + 1)( · , 𝐹)‘(𝑛 + 1))) | 
| 37 | 36 | oveq2d 7447 | . . . . . 6
⊢ (𝑥 = (𝑛 + 1) → ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑥)) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑛 + 1)))) | 
| 38 | 35, 37 | eqeq12d 2753 | . . . . 5
⊢ (𝑥 = (𝑛 + 1) → ((seq𝑀( · , 𝐹)‘𝑥) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑥)) ↔ (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑛 + 1))))) | 
| 39 | 38 | imbi2d 340 | . . . 4
⊢ (𝑥 = (𝑛 + 1) → ((𝜑 → (seq𝑀( · , 𝐹)‘𝑥) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑥))) ↔ (𝜑 → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑛 + 1)))))) | 
| 40 |  | fveq2 6906 | . . . . . 6
⊢ (𝑥 = 𝑘 → (seq𝑀( · , 𝐹)‘𝑥) = (seq𝑀( · , 𝐹)‘𝑘)) | 
| 41 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑥 = 𝑘 → (seq(𝑁 + 1)( · , 𝐹)‘𝑥) = (seq(𝑁 + 1)( · , 𝐹)‘𝑘)) | 
| 42 | 41 | oveq2d 7447 | . . . . . 6
⊢ (𝑥 = 𝑘 → ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑥)) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑘))) | 
| 43 | 40, 42 | eqeq12d 2753 | . . . . 5
⊢ (𝑥 = 𝑘 → ((seq𝑀( · , 𝐹)‘𝑥) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑥)) ↔ (seq𝑀( · , 𝐹)‘𝑘) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑘)))) | 
| 44 | 43 | imbi2d 340 | . . . 4
⊢ (𝑥 = 𝑘 → ((𝜑 → (seq𝑀( · , 𝐹)‘𝑥) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑥))) ↔ (𝜑 → (seq𝑀( · , 𝐹)‘𝑘) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑘))))) | 
| 45 | 9 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑁 + 1) ∈ ℤ) → 𝑁 ∈
(ℤ≥‘𝑀)) | 
| 46 |  | seqp1 14057 | . . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (seq𝑀( · , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( · , 𝐹)‘𝑁) · (𝐹‘(𝑁 + 1)))) | 
| 47 | 45, 46 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ (𝑁 + 1) ∈ ℤ) → (seq𝑀( · , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( · , 𝐹)‘𝑁) · (𝐹‘(𝑁 + 1)))) | 
| 48 |  | seq1 14055 | . . . . . . . 8
⊢ ((𝑁 + 1) ∈ ℤ →
(seq(𝑁 + 1)( · ,
𝐹)‘(𝑁 + 1)) = (𝐹‘(𝑁 + 1))) | 
| 49 | 48 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑁 + 1) ∈ ℤ) → (seq(𝑁 + 1)( · , 𝐹)‘(𝑁 + 1)) = (𝐹‘(𝑁 + 1))) | 
| 50 | 49 | oveq2d 7447 | . . . . . 6
⊢ ((𝜑 ∧ (𝑁 + 1) ∈ ℤ) → ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑁 + 1))) = ((seq𝑀( · , 𝐹)‘𝑁) · (𝐹‘(𝑁 + 1)))) | 
| 51 | 47, 50 | eqtr4d 2780 | . . . . 5
⊢ ((𝜑 ∧ (𝑁 + 1) ∈ ℤ) → (seq𝑀( · , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑁 + 1)))) | 
| 52 | 51 | expcom 413 | . . . 4
⊢ ((𝑁 + 1) ∈ ℤ →
(𝜑 → (seq𝑀( · , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑁 + 1))))) | 
| 53 | 19 | sselda 3983 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) → 𝑛 ∈
(ℤ≥‘𝑀)) | 
| 54 |  | seqp1 14057 | . . . . . . . . . 10
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1)))) | 
| 55 | 53, 54 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1)))) | 
| 56 | 55 | adantr 480 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ (seq𝑀( · , 𝐹)‘𝑛) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛))) → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1)))) | 
| 57 |  | oveq1 7438 | . . . . . . . . 9
⊢
((seq𝑀( · ,
𝐹)‘𝑛) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛)) → ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1))) = (((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛)) · (𝐹‘(𝑛 + 1)))) | 
| 58 | 57 | adantl 481 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ (seq𝑀( · , 𝐹)‘𝑛) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛))) → ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1))) = (((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛)) · (𝐹‘(𝑛 + 1)))) | 
| 59 | 14 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) → (seq𝑀( · , 𝐹)‘𝑁) ∈ ℂ) | 
| 60 | 23 | ffvelcdmda 7104 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) → (seq(𝑁 + 1)( · , 𝐹)‘𝑛) ∈ ℂ) | 
| 61 |  | peano2uz 12943 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (𝑛 + 1) ∈
(ℤ≥‘𝑀)) | 
| 62 | 61, 2 | eleqtrrdi 2852 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (𝑛 + 1) ∈ 𝑍) | 
| 63 | 53, 62 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) → (𝑛 + 1) ∈ 𝑍) | 
| 64 | 12 | ralrimiva 3146 | . . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ∈ ℂ) | 
| 65 |  | fveq2 6906 | . . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝑛 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑛 + 1))) | 
| 66 | 65 | eleq1d 2826 | . . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘𝑘) ∈ ℂ ↔ (𝐹‘(𝑛 + 1)) ∈ ℂ)) | 
| 67 | 66 | rspcv 3618 | . . . . . . . . . . . . 13
⊢ ((𝑛 + 1) ∈ 𝑍 → (∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ∈ ℂ → (𝐹‘(𝑛 + 1)) ∈ ℂ)) | 
| 68 | 64, 67 | mpan9 506 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 + 1) ∈ 𝑍) → (𝐹‘(𝑛 + 1)) ∈ ℂ) | 
| 69 | 63, 68 | syldan 591 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) → (𝐹‘(𝑛 + 1)) ∈ ℂ) | 
| 70 | 59, 60, 69 | mulassd 11284 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) → (((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛)) · (𝐹‘(𝑛 + 1))) = ((seq𝑀( · , 𝐹)‘𝑁) · ((seq(𝑁 + 1)( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1))))) | 
| 71 | 70 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ (seq𝑀( · , 𝐹)‘𝑛) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛))) → (((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛)) · (𝐹‘(𝑛 + 1))) = ((seq𝑀( · , 𝐹)‘𝑁) · ((seq(𝑁 + 1)( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1))))) | 
| 72 |  | seqp1 14057 | . . . . . . . . . . . 12
⊢ (𝑛 ∈
(ℤ≥‘(𝑁 + 1)) → (seq(𝑁 + 1)( · , 𝐹)‘(𝑛 + 1)) = ((seq(𝑁 + 1)( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1)))) | 
| 73 | 72 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) → (seq(𝑁 + 1)( · , 𝐹)‘(𝑛 + 1)) = ((seq(𝑁 + 1)( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1)))) | 
| 74 | 73 | oveq2d 7447 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) → ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑛 + 1))) = ((seq𝑀( · , 𝐹)‘𝑁) · ((seq(𝑁 + 1)( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1))))) | 
| 75 | 74 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ (seq𝑀( · , 𝐹)‘𝑛) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛))) → ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑛 + 1))) = ((seq𝑀( · , 𝐹)‘𝑁) · ((seq(𝑁 + 1)( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1))))) | 
| 76 | 71, 75 | eqtr4d 2780 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ (seq𝑀( · , 𝐹)‘𝑛) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛))) → (((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛)) · (𝐹‘(𝑛 + 1))) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑛 + 1)))) | 
| 77 | 56, 58, 76 | 3eqtrd 2781 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) ∧ (seq𝑀( · , 𝐹)‘𝑛) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛))) → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑛 + 1)))) | 
| 78 | 77 | exp31 419 | . . . . . 6
⊢ (𝜑 → (𝑛 ∈ (ℤ≥‘(𝑁 + 1)) → ((seq𝑀( · , 𝐹)‘𝑛) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛)) → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑛 + 1)))))) | 
| 79 | 78 | com12 32 | . . . . 5
⊢ (𝑛 ∈
(ℤ≥‘(𝑁 + 1)) → (𝜑 → ((seq𝑀( · , 𝐹)‘𝑛) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛)) → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑛 + 1)))))) | 
| 80 | 79 | a2d 29 | . . . 4
⊢ (𝑛 ∈
(ℤ≥‘(𝑁 + 1)) → ((𝜑 → (seq𝑀( · , 𝐹)‘𝑛) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑛))) → (𝜑 → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘(𝑛 + 1)))))) | 
| 81 | 29, 34, 39, 44, 52, 80 | uzind4 12948 | . . 3
⊢ (𝑘 ∈
(ℤ≥‘(𝑁 + 1)) → (𝜑 → (seq𝑀( · , 𝐹)‘𝑘) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑘)))) | 
| 82 | 81 | impcom 407 | . 2
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝑁 + 1))) → (seq𝑀( · , 𝐹)‘𝑘) = ((seq𝑀( · , 𝐹)‘𝑁) · (seq(𝑁 + 1)( · , 𝐹)‘𝑘))) | 
| 83 | 1, 7, 8, 14, 16, 24, 82 | climmulc2 15673 | 1
⊢ (𝜑 → seq𝑀( · , 𝐹) ⇝ ((seq𝑀( · , 𝐹)‘𝑁) · 𝐴)) |