| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | prodfn0.1 | . . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) | 
| 2 |  | eluzfz2 13573 | . . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁)) | 
| 3 | 1, 2 | syl 17 | . 2
⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁)) | 
| 4 |  | fveq2 6905 | . . . . 5
⊢ (𝑚 = 𝑀 → (seq𝑀( · , 𝐺)‘𝑚) = (seq𝑀( · , 𝐺)‘𝑀)) | 
| 5 |  | fveq2 6905 | . . . . . 6
⊢ (𝑚 = 𝑀 → (seq𝑀( · , 𝐹)‘𝑚) = (seq𝑀( · , 𝐹)‘𝑀)) | 
| 6 | 5 | oveq2d 7448 | . . . . 5
⊢ (𝑚 = 𝑀 → (1 / (seq𝑀( · , 𝐹)‘𝑚)) = (1 / (seq𝑀( · , 𝐹)‘𝑀))) | 
| 7 | 4, 6 | eqeq12d 2752 | . . . 4
⊢ (𝑚 = 𝑀 → ((seq𝑀( · , 𝐺)‘𝑚) = (1 / (seq𝑀( · , 𝐹)‘𝑚)) ↔ (seq𝑀( · , 𝐺)‘𝑀) = (1 / (seq𝑀( · , 𝐹)‘𝑀)))) | 
| 8 | 7 | imbi2d 340 | . . 3
⊢ (𝑚 = 𝑀 → ((𝜑 → (seq𝑀( · , 𝐺)‘𝑚) = (1 / (seq𝑀( · , 𝐹)‘𝑚))) ↔ (𝜑 → (seq𝑀( · , 𝐺)‘𝑀) = (1 / (seq𝑀( · , 𝐹)‘𝑀))))) | 
| 9 |  | fveq2 6905 | . . . . 5
⊢ (𝑚 = 𝑛 → (seq𝑀( · , 𝐺)‘𝑚) = (seq𝑀( · , 𝐺)‘𝑛)) | 
| 10 |  | fveq2 6905 | . . . . . 6
⊢ (𝑚 = 𝑛 → (seq𝑀( · , 𝐹)‘𝑚) = (seq𝑀( · , 𝐹)‘𝑛)) | 
| 11 | 10 | oveq2d 7448 | . . . . 5
⊢ (𝑚 = 𝑛 → (1 / (seq𝑀( · , 𝐹)‘𝑚)) = (1 / (seq𝑀( · , 𝐹)‘𝑛))) | 
| 12 | 9, 11 | eqeq12d 2752 | . . . 4
⊢ (𝑚 = 𝑛 → ((seq𝑀( · , 𝐺)‘𝑚) = (1 / (seq𝑀( · , 𝐹)‘𝑚)) ↔ (seq𝑀( · , 𝐺)‘𝑛) = (1 / (seq𝑀( · , 𝐹)‘𝑛)))) | 
| 13 | 12 | imbi2d 340 | . . 3
⊢ (𝑚 = 𝑛 → ((𝜑 → (seq𝑀( · , 𝐺)‘𝑚) = (1 / (seq𝑀( · , 𝐹)‘𝑚))) ↔ (𝜑 → (seq𝑀( · , 𝐺)‘𝑛) = (1 / (seq𝑀( · , 𝐹)‘𝑛))))) | 
| 14 |  | fveq2 6905 | . . . . 5
⊢ (𝑚 = (𝑛 + 1) → (seq𝑀( · , 𝐺)‘𝑚) = (seq𝑀( · , 𝐺)‘(𝑛 + 1))) | 
| 15 |  | fveq2 6905 | . . . . . 6
⊢ (𝑚 = (𝑛 + 1) → (seq𝑀( · , 𝐹)‘𝑚) = (seq𝑀( · , 𝐹)‘(𝑛 + 1))) | 
| 16 | 15 | oveq2d 7448 | . . . . 5
⊢ (𝑚 = (𝑛 + 1) → (1 / (seq𝑀( · , 𝐹)‘𝑚)) = (1 / (seq𝑀( · , 𝐹)‘(𝑛 + 1)))) | 
| 17 | 14, 16 | eqeq12d 2752 | . . . 4
⊢ (𝑚 = (𝑛 + 1) → ((seq𝑀( · , 𝐺)‘𝑚) = (1 / (seq𝑀( · , 𝐹)‘𝑚)) ↔ (seq𝑀( · , 𝐺)‘(𝑛 + 1)) = (1 / (seq𝑀( · , 𝐹)‘(𝑛 + 1))))) | 
| 18 | 17 | imbi2d 340 | . . 3
⊢ (𝑚 = (𝑛 + 1) → ((𝜑 → (seq𝑀( · , 𝐺)‘𝑚) = (1 / (seq𝑀( · , 𝐹)‘𝑚))) ↔ (𝜑 → (seq𝑀( · , 𝐺)‘(𝑛 + 1)) = (1 / (seq𝑀( · , 𝐹)‘(𝑛 + 1)))))) | 
| 19 |  | fveq2 6905 | . . . . 5
⊢ (𝑚 = 𝑁 → (seq𝑀( · , 𝐺)‘𝑚) = (seq𝑀( · , 𝐺)‘𝑁)) | 
| 20 |  | fveq2 6905 | . . . . . 6
⊢ (𝑚 = 𝑁 → (seq𝑀( · , 𝐹)‘𝑚) = (seq𝑀( · , 𝐹)‘𝑁)) | 
| 21 | 20 | oveq2d 7448 | . . . . 5
⊢ (𝑚 = 𝑁 → (1 / (seq𝑀( · , 𝐹)‘𝑚)) = (1 / (seq𝑀( · , 𝐹)‘𝑁))) | 
| 22 | 19, 21 | eqeq12d 2752 | . . . 4
⊢ (𝑚 = 𝑁 → ((seq𝑀( · , 𝐺)‘𝑚) = (1 / (seq𝑀( · , 𝐹)‘𝑚)) ↔ (seq𝑀( · , 𝐺)‘𝑁) = (1 / (seq𝑀( · , 𝐹)‘𝑁)))) | 
| 23 | 22 | imbi2d 340 | . . 3
⊢ (𝑚 = 𝑁 → ((𝜑 → (seq𝑀( · , 𝐺)‘𝑚) = (1 / (seq𝑀( · , 𝐹)‘𝑚))) ↔ (𝜑 → (seq𝑀( · , 𝐺)‘𝑁) = (1 / (seq𝑀( · , 𝐹)‘𝑁))))) | 
| 24 |  | eluzfz1 13572 | . . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁)) | 
| 25 | 1, 24 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑀 ∈ (𝑀...𝑁)) | 
| 26 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑘 = 𝑀 → (𝐺‘𝑘) = (𝐺‘𝑀)) | 
| 27 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑘 = 𝑀 → (𝐹‘𝑘) = (𝐹‘𝑀)) | 
| 28 | 27 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑘 = 𝑀 → (1 / (𝐹‘𝑘)) = (1 / (𝐹‘𝑀))) | 
| 29 | 26, 28 | eqeq12d 2752 | . . . . . . . 8
⊢ (𝑘 = 𝑀 → ((𝐺‘𝑘) = (1 / (𝐹‘𝑘)) ↔ (𝐺‘𝑀) = (1 / (𝐹‘𝑀)))) | 
| 30 | 29 | imbi2d 340 | . . . . . . 7
⊢ (𝑘 = 𝑀 → ((𝜑 → (𝐺‘𝑘) = (1 / (𝐹‘𝑘))) ↔ (𝜑 → (𝐺‘𝑀) = (1 / (𝐹‘𝑀))))) | 
| 31 |  | prodfrec.4 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) = (1 / (𝐹‘𝑘))) | 
| 32 | 31 | expcom 413 | . . . . . . 7
⊢ (𝑘 ∈ (𝑀...𝑁) → (𝜑 → (𝐺‘𝑘) = (1 / (𝐹‘𝑘)))) | 
| 33 | 30, 32 | vtoclga 3576 | . . . . . 6
⊢ (𝑀 ∈ (𝑀...𝑁) → (𝜑 → (𝐺‘𝑀) = (1 / (𝐹‘𝑀)))) | 
| 34 | 25, 33 | mpcom 38 | . . . . 5
⊢ (𝜑 → (𝐺‘𝑀) = (1 / (𝐹‘𝑀))) | 
| 35 |  | eluzel2 12884 | . . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) | 
| 36 | 1, 35 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 37 |  | seq1 14056 | . . . . . 6
⊢ (𝑀 ∈ ℤ → (seq𝑀( · , 𝐺)‘𝑀) = (𝐺‘𝑀)) | 
| 38 | 36, 37 | syl 17 | . . . . 5
⊢ (𝜑 → (seq𝑀( · , 𝐺)‘𝑀) = (𝐺‘𝑀)) | 
| 39 |  | seq1 14056 | . . . . . . 7
⊢ (𝑀 ∈ ℤ → (seq𝑀( · , 𝐹)‘𝑀) = (𝐹‘𝑀)) | 
| 40 | 36, 39 | syl 17 | . . . . . 6
⊢ (𝜑 → (seq𝑀( · , 𝐹)‘𝑀) = (𝐹‘𝑀)) | 
| 41 | 40 | oveq2d 7448 | . . . . 5
⊢ (𝜑 → (1 / (seq𝑀( · , 𝐹)‘𝑀)) = (1 / (𝐹‘𝑀))) | 
| 42 | 34, 38, 41 | 3eqtr4d 2786 | . . . 4
⊢ (𝜑 → (seq𝑀( · , 𝐺)‘𝑀) = (1 / (seq𝑀( · , 𝐹)‘𝑀))) | 
| 43 | 42 | a1i 11 | . . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝜑 → (seq𝑀( · , 𝐺)‘𝑀) = (1 / (seq𝑀( · , 𝐹)‘𝑀)))) | 
| 44 |  | oveq1 7439 | . . . . . . . . 9
⊢
((seq𝑀( · ,
𝐺)‘𝑛) = (1 / (seq𝑀( · , 𝐹)‘𝑛)) → ((seq𝑀( · , 𝐺)‘𝑛) · (𝐺‘(𝑛 + 1))) = ((1 / (seq𝑀( · , 𝐹)‘𝑛)) · (𝐺‘(𝑛 + 1)))) | 
| 45 | 44 | 3ad2ant3 1135 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁) ∧ (seq𝑀( · , 𝐺)‘𝑛) = (1 / (seq𝑀( · , 𝐹)‘𝑛))) → ((seq𝑀( · , 𝐺)‘𝑛) · (𝐺‘(𝑛 + 1))) = ((1 / (seq𝑀( · , 𝐹)‘𝑛)) · (𝐺‘(𝑛 + 1)))) | 
| 46 |  | fzofzp1 13804 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ (𝑀..^𝑁) → (𝑛 + 1) ∈ (𝑀...𝑁)) | 
| 47 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 = (𝑛 + 1) → (𝐺‘𝑘) = (𝐺‘(𝑛 + 1))) | 
| 48 |  | fveq2 6905 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 = (𝑛 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑛 + 1))) | 
| 49 | 48 | oveq2d 7448 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 = (𝑛 + 1) → (1 / (𝐹‘𝑘)) = (1 / (𝐹‘(𝑛 + 1)))) | 
| 50 | 47, 49 | eqeq12d 2752 | . . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝑛 + 1) → ((𝐺‘𝑘) = (1 / (𝐹‘𝑘)) ↔ (𝐺‘(𝑛 + 1)) = (1 / (𝐹‘(𝑛 + 1))))) | 
| 51 | 50 | imbi2d 340 | . . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑛 + 1) → ((𝜑 → (𝐺‘𝑘) = (1 / (𝐹‘𝑘))) ↔ (𝜑 → (𝐺‘(𝑛 + 1)) = (1 / (𝐹‘(𝑛 + 1)))))) | 
| 52 | 51, 32 | vtoclga 3576 | . . . . . . . . . . . . 13
⊢ ((𝑛 + 1) ∈ (𝑀...𝑁) → (𝜑 → (𝐺‘(𝑛 + 1)) = (1 / (𝐹‘(𝑛 + 1))))) | 
| 53 | 46, 52 | syl 17 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ (𝑀..^𝑁) → (𝜑 → (𝐺‘(𝑛 + 1)) = (1 / (𝐹‘(𝑛 + 1))))) | 
| 54 | 53 | impcom 407 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (𝐺‘(𝑛 + 1)) = (1 / (𝐹‘(𝑛 + 1)))) | 
| 55 | 54 | oveq2d 7448 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → ((1 / (seq𝑀( · , 𝐹)‘𝑛)) · (𝐺‘(𝑛 + 1))) = ((1 / (seq𝑀( · , 𝐹)‘𝑛)) · (1 / (𝐹‘(𝑛 + 1))))) | 
| 56 |  | 1cnd 11257 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → 1 ∈ ℂ) | 
| 57 |  | elfzouz 13704 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (𝑀..^𝑁) → 𝑛 ∈ (ℤ≥‘𝑀)) | 
| 58 | 57 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → 𝑛 ∈ (ℤ≥‘𝑀)) | 
| 59 |  | elfzouz2 13715 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (𝑀..^𝑁) → 𝑁 ∈ (ℤ≥‘𝑛)) | 
| 60 |  | fzss2 13605 | . . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘𝑛) → (𝑀...𝑛) ⊆ (𝑀...𝑁)) | 
| 61 | 59, 60 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (𝑀..^𝑁) → (𝑀...𝑛) ⊆ (𝑀...𝑁)) | 
| 62 | 61 | sselda 3982 | . . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ (𝑀..^𝑁) ∧ 𝑘 ∈ (𝑀...𝑛)) → 𝑘 ∈ (𝑀...𝑁)) | 
| 63 |  | prodfn0.2 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℂ) | 
| 64 | 62, 63 | sylan2 593 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ (𝑀..^𝑁) ∧ 𝑘 ∈ (𝑀...𝑛))) → (𝐹‘𝑘) ∈ ℂ) | 
| 65 | 64 | anassrs 467 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) ∧ 𝑘 ∈ (𝑀...𝑛)) → (𝐹‘𝑘) ∈ ℂ) | 
| 66 |  | mulcl 11240 | . . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑘 · 𝑥) ∈ ℂ) | 
| 67 | 66 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) ∧ (𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑘 · 𝑥) ∈ ℂ) | 
| 68 | 58, 65, 67 | seqcl 14064 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (seq𝑀( · , 𝐹)‘𝑛) ∈ ℂ) | 
| 69 | 48 | eleq1d 2825 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘𝑘) ∈ ℂ ↔ (𝐹‘(𝑛 + 1)) ∈ ℂ)) | 
| 70 | 69 | imbi2d 340 | . . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝑛 + 1) → ((𝜑 → (𝐹‘𝑘) ∈ ℂ) ↔ (𝜑 → (𝐹‘(𝑛 + 1)) ∈ ℂ))) | 
| 71 | 63 | expcom 413 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (𝑀...𝑁) → (𝜑 → (𝐹‘𝑘) ∈ ℂ)) | 
| 72 | 70, 71 | vtoclga 3576 | . . . . . . . . . . . . . 14
⊢ ((𝑛 + 1) ∈ (𝑀...𝑁) → (𝜑 → (𝐹‘(𝑛 + 1)) ∈ ℂ)) | 
| 73 | 46, 72 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ (𝑀..^𝑁) → (𝜑 → (𝐹‘(𝑛 + 1)) ∈ ℂ)) | 
| 74 | 73 | impcom 407 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (𝐹‘(𝑛 + 1)) ∈ ℂ) | 
| 75 |  | prodfn0.3 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ≠ 0) | 
| 76 | 62, 75 | sylan2 593 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑛 ∈ (𝑀..^𝑁) ∧ 𝑘 ∈ (𝑀...𝑛))) → (𝐹‘𝑘) ≠ 0) | 
| 77 | 76 | anassrs 467 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) ∧ 𝑘 ∈ (𝑀...𝑛)) → (𝐹‘𝑘) ≠ 0) | 
| 78 | 58, 65, 77 | prodfn0 15931 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (seq𝑀( · , 𝐹)‘𝑛) ≠ 0) | 
| 79 | 48 | neeq1d 2999 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘𝑘) ≠ 0 ↔ (𝐹‘(𝑛 + 1)) ≠ 0)) | 
| 80 | 79 | imbi2d 340 | . . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝑛 + 1) → ((𝜑 → (𝐹‘𝑘) ≠ 0) ↔ (𝜑 → (𝐹‘(𝑛 + 1)) ≠ 0))) | 
| 81 | 75 | expcom 413 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (𝑀...𝑁) → (𝜑 → (𝐹‘𝑘) ≠ 0)) | 
| 82 | 80, 81 | vtoclga 3576 | . . . . . . . . . . . . . 14
⊢ ((𝑛 + 1) ∈ (𝑀...𝑁) → (𝜑 → (𝐹‘(𝑛 + 1)) ≠ 0)) | 
| 83 | 46, 82 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ (𝑀..^𝑁) → (𝜑 → (𝐹‘(𝑛 + 1)) ≠ 0)) | 
| 84 | 83 | impcom 407 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (𝐹‘(𝑛 + 1)) ≠ 0) | 
| 85 | 56, 68, 56, 74, 78, 84 | divmuldivd 12085 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → ((1 / (seq𝑀( · , 𝐹)‘𝑛)) · (1 / (𝐹‘(𝑛 + 1)))) = ((1 · 1) / ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1))))) | 
| 86 |  | 1t1e1 12429 | . . . . . . . . . . . 12
⊢ (1
· 1) = 1 | 
| 87 | 86 | oveq1i 7442 | . . . . . . . . . . 11
⊢ ((1
· 1) / ((seq𝑀(
· , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1)))) = (1 / ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1)))) | 
| 88 | 85, 87 | eqtrdi 2792 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → ((1 / (seq𝑀( · , 𝐹)‘𝑛)) · (1 / (𝐹‘(𝑛 + 1)))) = (1 / ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1))))) | 
| 89 | 55, 88 | eqtrd 2776 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → ((1 / (seq𝑀( · , 𝐹)‘𝑛)) · (𝐺‘(𝑛 + 1))) = (1 / ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1))))) | 
| 90 | 89 | 3adant3 1132 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁) ∧ (seq𝑀( · , 𝐺)‘𝑛) = (1 / (seq𝑀( · , 𝐹)‘𝑛))) → ((1 / (seq𝑀( · , 𝐹)‘𝑛)) · (𝐺‘(𝑛 + 1))) = (1 / ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1))))) | 
| 91 | 45, 90 | eqtrd 2776 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁) ∧ (seq𝑀( · , 𝐺)‘𝑛) = (1 / (seq𝑀( · , 𝐹)‘𝑛))) → ((seq𝑀( · , 𝐺)‘𝑛) · (𝐺‘(𝑛 + 1))) = (1 / ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1))))) | 
| 92 |  | seqp1 14058 | . . . . . . . . 9
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (seq𝑀( · , 𝐺)‘(𝑛 + 1)) = ((seq𝑀( · , 𝐺)‘𝑛) · (𝐺‘(𝑛 + 1)))) | 
| 93 | 57, 92 | syl 17 | . . . . . . . 8
⊢ (𝑛 ∈ (𝑀..^𝑁) → (seq𝑀( · , 𝐺)‘(𝑛 + 1)) = ((seq𝑀( · , 𝐺)‘𝑛) · (𝐺‘(𝑛 + 1)))) | 
| 94 | 93 | 3ad2ant2 1134 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁) ∧ (seq𝑀( · , 𝐺)‘𝑛) = (1 / (seq𝑀( · , 𝐹)‘𝑛))) → (seq𝑀( · , 𝐺)‘(𝑛 + 1)) = ((seq𝑀( · , 𝐺)‘𝑛) · (𝐺‘(𝑛 + 1)))) | 
| 95 |  | seqp1 14058 | . . . . . . . . . 10
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1)))) | 
| 96 | 57, 95 | syl 17 | . . . . . . . . 9
⊢ (𝑛 ∈ (𝑀..^𝑁) → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1)))) | 
| 97 | 96 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑛 ∈ (𝑀..^𝑁) → (1 / (seq𝑀( · , 𝐹)‘(𝑛 + 1))) = (1 / ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1))))) | 
| 98 | 97 | 3ad2ant2 1134 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁) ∧ (seq𝑀( · , 𝐺)‘𝑛) = (1 / (seq𝑀( · , 𝐹)‘𝑛))) → (1 / (seq𝑀( · , 𝐹)‘(𝑛 + 1))) = (1 / ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1))))) | 
| 99 | 91, 94, 98 | 3eqtr4d 2786 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁) ∧ (seq𝑀( · , 𝐺)‘𝑛) = (1 / (seq𝑀( · , 𝐹)‘𝑛))) → (seq𝑀( · , 𝐺)‘(𝑛 + 1)) = (1 / (seq𝑀( · , 𝐹)‘(𝑛 + 1)))) | 
| 100 | 99 | 3exp 1119 | . . . . 5
⊢ (𝜑 → (𝑛 ∈ (𝑀..^𝑁) → ((seq𝑀( · , 𝐺)‘𝑛) = (1 / (seq𝑀( · , 𝐹)‘𝑛)) → (seq𝑀( · , 𝐺)‘(𝑛 + 1)) = (1 / (seq𝑀( · , 𝐹)‘(𝑛 + 1)))))) | 
| 101 | 100 | com12 32 | . . . 4
⊢ (𝑛 ∈ (𝑀..^𝑁) → (𝜑 → ((seq𝑀( · , 𝐺)‘𝑛) = (1 / (seq𝑀( · , 𝐹)‘𝑛)) → (seq𝑀( · , 𝐺)‘(𝑛 + 1)) = (1 / (seq𝑀( · , 𝐹)‘(𝑛 + 1)))))) | 
| 102 | 101 | a2d 29 | . . 3
⊢ (𝑛 ∈ (𝑀..^𝑁) → ((𝜑 → (seq𝑀( · , 𝐺)‘𝑛) = (1 / (seq𝑀( · , 𝐹)‘𝑛))) → (𝜑 → (seq𝑀( · , 𝐺)‘(𝑛 + 1)) = (1 / (seq𝑀( · , 𝐹)‘(𝑛 + 1)))))) | 
| 103 | 8, 13, 18, 23, 43, 102 | fzind2 13825 | . 2
⊢ (𝑁 ∈ (𝑀...𝑁) → (𝜑 → (seq𝑀( · , 𝐺)‘𝑁) = (1 / (seq𝑀( · , 𝐹)‘𝑁)))) | 
| 104 | 3, 103 | mpcom 38 | 1
⊢ (𝜑 → (seq𝑀( · , 𝐺)‘𝑁) = (1 / (seq𝑀( · , 𝐹)‘𝑁))) |