| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpr 484 | . 2
⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝑀)) → 𝑛 ∈ (0...𝑀)) | 
| 2 |  | simpl 482 | . 2
⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝑀)) → 𝜑) | 
| 3 |  | fveq2 6906 | . . . . 5
⊢ (𝑘 = 0 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑘) = ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘0)) | 
| 4 |  | csbeq1 3902 | . . . . . . 7
⊢ (𝑘 = 0 → ⦋𝑘 / 𝑛⦌𝐵 = ⦋0 / 𝑛⦌𝐵) | 
| 5 | 4 | oveq1d 7446 | . . . . . 6
⊢ (𝑘 = 0 →
(⦋𝑘 / 𝑛⦌𝐵 / 𝐶) = (⦋0 / 𝑛⦌𝐵 / 𝐶)) | 
| 6 | 5 | mpteq2dv 5244 | . . . . 5
⊢ (𝑘 = 0 → (𝑥 ∈ 𝑋 ↦ (⦋𝑘 / 𝑛⦌𝐵 / 𝐶)) = (𝑥 ∈ 𝑋 ↦ (⦋0 / 𝑛⦌𝐵 / 𝐶))) | 
| 7 | 3, 6 | eqeq12d 2753 | . . . 4
⊢ (𝑘 = 0 → (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ (⦋𝑘 / 𝑛⦌𝐵 / 𝐶)) ↔ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘0) = (𝑥 ∈ 𝑋 ↦ (⦋0 / 𝑛⦌𝐵 / 𝐶)))) | 
| 8 | 7 | imbi2d 340 | . . 3
⊢ (𝑘 = 0 → ((𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ (⦋𝑘 / 𝑛⦌𝐵 / 𝐶))) ↔ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘0) = (𝑥 ∈ 𝑋 ↦ (⦋0 / 𝑛⦌𝐵 / 𝐶))))) | 
| 9 |  | fveq2 6906 | . . . . 5
⊢ (𝑘 = 𝑗 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑘) = ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗)) | 
| 10 |  | csbeq1 3902 | . . . . . . 7
⊢ (𝑘 = 𝑗 → ⦋𝑘 / 𝑛⦌𝐵 = ⦋𝑗 / 𝑛⦌𝐵) | 
| 11 | 10 | oveq1d 7446 | . . . . . 6
⊢ (𝑘 = 𝑗 → (⦋𝑘 / 𝑛⦌𝐵 / 𝐶) = (⦋𝑗 / 𝑛⦌𝐵 / 𝐶)) | 
| 12 | 11 | mpteq2dv 5244 | . . . . 5
⊢ (𝑘 = 𝑗 → (𝑥 ∈ 𝑋 ↦ (⦋𝑘 / 𝑛⦌𝐵 / 𝐶)) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) | 
| 13 | 9, 12 | eqeq12d 2753 | . . . 4
⊢ (𝑘 = 𝑗 → (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ (⦋𝑘 / 𝑛⦌𝐵 / 𝐶)) ↔ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶)))) | 
| 14 | 13 | imbi2d 340 | . . 3
⊢ (𝑘 = 𝑗 → ((𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ (⦋𝑘 / 𝑛⦌𝐵 / 𝐶))) ↔ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))))) | 
| 15 |  | fveq2 6906 | . . . . 5
⊢ (𝑘 = (𝑗 + 1) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑘) = ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘(𝑗 + 1))) | 
| 16 |  | csbeq1 3902 | . . . . . . 7
⊢ (𝑘 = (𝑗 + 1) → ⦋𝑘 / 𝑛⦌𝐵 = ⦋(𝑗 + 1) / 𝑛⦌𝐵) | 
| 17 | 16 | oveq1d 7446 | . . . . . 6
⊢ (𝑘 = (𝑗 + 1) → (⦋𝑘 / 𝑛⦌𝐵 / 𝐶) = (⦋(𝑗 + 1) / 𝑛⦌𝐵 / 𝐶)) | 
| 18 | 17 | mpteq2dv 5244 | . . . . 5
⊢ (𝑘 = (𝑗 + 1) → (𝑥 ∈ 𝑋 ↦ (⦋𝑘 / 𝑛⦌𝐵 / 𝐶)) = (𝑥 ∈ 𝑋 ↦ (⦋(𝑗 + 1) / 𝑛⦌𝐵 / 𝐶))) | 
| 19 | 15, 18 | eqeq12d 2753 | . . . 4
⊢ (𝑘 = (𝑗 + 1) → (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ (⦋𝑘 / 𝑛⦌𝐵 / 𝐶)) ↔ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘(𝑗 + 1)) = (𝑥 ∈ 𝑋 ↦ (⦋(𝑗 + 1) / 𝑛⦌𝐵 / 𝐶)))) | 
| 20 | 19 | imbi2d 340 | . . 3
⊢ (𝑘 = (𝑗 + 1) → ((𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ (⦋𝑘 / 𝑛⦌𝐵 / 𝐶))) ↔ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘(𝑗 + 1)) = (𝑥 ∈ 𝑋 ↦ (⦋(𝑗 + 1) / 𝑛⦌𝐵 / 𝐶))))) | 
| 21 |  | fveq2 6906 | . . . . 5
⊢ (𝑘 = 𝑛 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑘) = ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑛)) | 
| 22 |  | csbeq1a 3913 | . . . . . . . . 9
⊢ (𝑛 = 𝑘 → 𝐵 = ⦋𝑘 / 𝑛⦌𝐵) | 
| 23 | 22 | equcoms 2019 | . . . . . . . 8
⊢ (𝑘 = 𝑛 → 𝐵 = ⦋𝑘 / 𝑛⦌𝐵) | 
| 24 | 23 | eqcomd 2743 | . . . . . . 7
⊢ (𝑘 = 𝑛 → ⦋𝑘 / 𝑛⦌𝐵 = 𝐵) | 
| 25 | 24 | oveq1d 7446 | . . . . . 6
⊢ (𝑘 = 𝑛 → (⦋𝑘 / 𝑛⦌𝐵 / 𝐶) = (𝐵 / 𝐶)) | 
| 26 | 25 | mpteq2dv 5244 | . . . . 5
⊢ (𝑘 = 𝑛 → (𝑥 ∈ 𝑋 ↦ (⦋𝑘 / 𝑛⦌𝐵 / 𝐶)) = (𝑥 ∈ 𝑋 ↦ (𝐵 / 𝐶))) | 
| 27 | 21, 26 | eqeq12d 2753 | . . . 4
⊢ (𝑘 = 𝑛 → (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ (⦋𝑘 / 𝑛⦌𝐵 / 𝐶)) ↔ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑛) = (𝑥 ∈ 𝑋 ↦ (𝐵 / 𝐶)))) | 
| 28 | 27 | imbi2d 340 | . . 3
⊢ (𝑘 = 𝑛 → ((𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ (⦋𝑘 / 𝑛⦌𝐵 / 𝐶))) ↔ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑛) = (𝑥 ∈ 𝑋 ↦ (𝐵 / 𝐶))))) | 
| 29 |  | dvnmptdivc.s | . . . . . . 7
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) | 
| 30 |  | recnprss 25939 | . . . . . . 7
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) | 
| 31 | 29, 30 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑆 ⊆ ℂ) | 
| 32 |  | cnex 11236 | . . . . . . . 8
⊢ ℂ
∈ V | 
| 33 | 32 | a1i 11 | . . . . . . 7
⊢ (𝜑 → ℂ ∈
V) | 
| 34 |  | dvnmptdivc.a | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) | 
| 35 |  | dvnmptdivc.c | . . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ ℂ) | 
| 36 | 35 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ ℂ) | 
| 37 |  | dvnmptdivc.cne0 | . . . . . . . . . 10
⊢ (𝜑 → 𝐶 ≠ 0) | 
| 38 | 37 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ≠ 0) | 
| 39 | 34, 36, 38 | divcld 12043 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐴 / 𝐶) ∈ ℂ) | 
| 40 | 39 | fmpttd 7135 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)):𝑋⟶ℂ) | 
| 41 |  | dvnmptdivc.x | . . . . . . 7
⊢ (𝜑 → 𝑋 ⊆ 𝑆) | 
| 42 |  | elpm2r 8885 | . . . . . . 7
⊢
(((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ ((𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)):𝑋⟶ℂ ∧ 𝑋 ⊆ 𝑆)) → (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)) ∈ (ℂ ↑pm 𝑆)) | 
| 43 | 33, 29, 40, 41, 42 | syl22anc 839 | . . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)) ∈ (ℂ ↑pm 𝑆)) | 
| 44 |  | dvn0 25960 | . . . . . 6
⊢ ((𝑆 ⊆ ℂ ∧ (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)) ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘0) = (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶))) | 
| 45 | 31, 43, 44 | syl2anc 584 | . . . . 5
⊢ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘0) = (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶))) | 
| 46 |  | id 22 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝜑) | 
| 47 |  | dvnmptdivc.8 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈
ℕ0) | 
| 48 |  | nn0uz 12920 | . . . . . . . . . . . . . 14
⊢
ℕ0 = (ℤ≥‘0) | 
| 49 | 47, 48 | eleqtrdi 2851 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘0)) | 
| 50 |  | eluzfz1 13571 | . . . . . . . . . . . . 13
⊢ (𝑀 ∈
(ℤ≥‘0) → 0 ∈ (0...𝑀)) | 
| 51 | 49, 50 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈ (0...𝑀)) | 
| 52 |  | nfv 1914 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑛(𝜑 ∧ 0 ∈ (0...𝑀)) | 
| 53 |  | nfcv 2905 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘0) | 
| 54 |  | nfcv 2905 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛𝑋 | 
| 55 |  | nfcsb1v 3923 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛⦋0 / 𝑛⦌𝐵 | 
| 56 | 54, 55 | nfmpt 5249 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛(𝑥 ∈ 𝑋 ↦ ⦋0 / 𝑛⦌𝐵) | 
| 57 | 53, 56 | nfeq 2919 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑛((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘0) = (𝑥 ∈ 𝑋 ↦ ⦋0 / 𝑛⦌𝐵) | 
| 58 | 52, 57 | nfim 1896 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑛((𝜑 ∧ 0 ∈ (0...𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘0) = (𝑥 ∈ 𝑋 ↦ ⦋0 / 𝑛⦌𝐵)) | 
| 59 |  | c0ex 11255 | . . . . . . . . . . . . 13
⊢ 0 ∈
V | 
| 60 |  | eleq1 2829 | . . . . . . . . . . . . . . 15
⊢ (𝑛 = 0 → (𝑛 ∈ (0...𝑀) ↔ 0 ∈ (0...𝑀))) | 
| 61 | 60 | anbi2d 630 | . . . . . . . . . . . . . 14
⊢ (𝑛 = 0 → ((𝜑 ∧ 𝑛 ∈ (0...𝑀)) ↔ (𝜑 ∧ 0 ∈ (0...𝑀)))) | 
| 62 |  | fveq2 6906 | . . . . . . . . . . . . . . 15
⊢ (𝑛 = 0 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘0)) | 
| 63 |  | csbeq1a 3913 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 = 0 → 𝐵 = ⦋0 / 𝑛⦌𝐵) | 
| 64 | 63 | mpteq2dv 5244 | . . . . . . . . . . . . . . 15
⊢ (𝑛 = 0 → (𝑥 ∈ 𝑋 ↦ 𝐵) = (𝑥 ∈ 𝑋 ↦ ⦋0 / 𝑛⦌𝐵)) | 
| 65 | 62, 64 | eqeq12d 2753 | . . . . . . . . . . . . . 14
⊢ (𝑛 = 0 → (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = (𝑥 ∈ 𝑋 ↦ 𝐵) ↔ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘0) = (𝑥 ∈ 𝑋 ↦ ⦋0 / 𝑛⦌𝐵))) | 
| 66 | 61, 65 | imbi12d 344 | . . . . . . . . . . . . 13
⊢ (𝑛 = 0 → (((𝜑 ∧ 𝑛 ∈ (0...𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = (𝑥 ∈ 𝑋 ↦ 𝐵)) ↔ ((𝜑 ∧ 0 ∈ (0...𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘0) = (𝑥 ∈ 𝑋 ↦ ⦋0 / 𝑛⦌𝐵)))) | 
| 67 |  | dvnmptdivc.dvn | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = (𝑥 ∈ 𝑋 ↦ 𝐵)) | 
| 68 | 58, 59, 66, 67 | vtoclf 3564 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 0 ∈ (0...𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘0) = (𝑥 ∈ 𝑋 ↦ ⦋0 / 𝑛⦌𝐵)) | 
| 69 | 46, 51, 68 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘0) = (𝑥 ∈ 𝑋 ↦ ⦋0 / 𝑛⦌𝐵)) | 
| 70 | 69 | fveq1d 6908 | . . . . . . . . . 10
⊢ (𝜑 → (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘0)‘𝑥) = ((𝑥 ∈ 𝑋 ↦ ⦋0 / 𝑛⦌𝐵)‘𝑥)) | 
| 71 | 70 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘0)‘𝑥) = ((𝑥 ∈ 𝑋 ↦ ⦋0 / 𝑛⦌𝐵)‘𝑥)) | 
| 72 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) | 
| 73 |  | simpl 482 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝜑) | 
| 74 | 51 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 0 ∈ (0...𝑀)) | 
| 75 |  | 0re 11263 | . . . . . . . . . . . 12
⊢ 0 ∈
ℝ | 
| 76 |  | nfcv 2905 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑛0 | 
| 77 |  | nfv 1914 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑛(𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 0 ∈ (0...𝑀)) | 
| 78 |  | nfcv 2905 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛ℂ | 
| 79 | 55, 78 | nfel 2920 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑛⦋0 / 𝑛⦌𝐵 ∈ ℂ | 
| 80 | 77, 79 | nfim 1896 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑛((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 0 ∈ (0...𝑀)) → ⦋0 / 𝑛⦌𝐵 ∈ ℂ) | 
| 81 | 60 | 3anbi3d 1444 | . . . . . . . . . . . . . 14
⊢ (𝑛 = 0 → ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑛 ∈ (0...𝑀)) ↔ (𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 0 ∈ (0...𝑀)))) | 
| 82 | 63 | eleq1d 2826 | . . . . . . . . . . . . . 14
⊢ (𝑛 = 0 → (𝐵 ∈ ℂ ↔ ⦋0 /
𝑛⦌𝐵 ∈
ℂ)) | 
| 83 | 81, 82 | imbi12d 344 | . . . . . . . . . . . . 13
⊢ (𝑛 = 0 → (((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑛 ∈ (0...𝑀)) → 𝐵 ∈ ℂ) ↔ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 0 ∈ (0...𝑀)) → ⦋0 / 𝑛⦌𝐵 ∈ ℂ))) | 
| 84 |  | dvnmptdivc.b | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑛 ∈ (0...𝑀)) → 𝐵 ∈ ℂ) | 
| 85 | 76, 80, 83, 84 | vtoclgf 3569 | . . . . . . . . . . . 12
⊢ (0 ∈
ℝ → ((𝜑 ∧
𝑥 ∈ 𝑋 ∧ 0 ∈ (0...𝑀)) → ⦋0 / 𝑛⦌𝐵 ∈ ℂ)) | 
| 86 | 75, 85 | ax-mp 5 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 0 ∈ (0...𝑀)) → ⦋0 / 𝑛⦌𝐵 ∈ ℂ) | 
| 87 | 73, 72, 74, 86 | syl3anc 1373 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ⦋0 / 𝑛⦌𝐵 ∈ ℂ) | 
| 88 |  | eqid 2737 | . . . . . . . . . . 11
⊢ (𝑥 ∈ 𝑋 ↦ ⦋0 / 𝑛⦌𝐵) = (𝑥 ∈ 𝑋 ↦ ⦋0 / 𝑛⦌𝐵) | 
| 89 | 88 | fvmpt2 7027 | . . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑋 ∧ ⦋0 / 𝑛⦌𝐵 ∈ ℂ) → ((𝑥 ∈ 𝑋 ↦ ⦋0 / 𝑛⦌𝐵)‘𝑥) = ⦋0 / 𝑛⦌𝐵) | 
| 90 | 72, 87, 89 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ↦ ⦋0 / 𝑛⦌𝐵)‘𝑥) = ⦋0 / 𝑛⦌𝐵) | 
| 91 | 71, 90 | eqtr2d 2778 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ⦋0 / 𝑛⦌𝐵 = (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘0)‘𝑥)) | 
| 92 | 34 | fmpttd 7135 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶ℂ) | 
| 93 |  | elpm2r 8885 | . . . . . . . . . . . 12
⊢
(((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶ℂ ∧ 𝑋 ⊆ 𝑆)) → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (ℂ ↑pm 𝑆)) | 
| 94 | 33, 29, 92, 41, 93 | syl22anc 839 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (ℂ ↑pm 𝑆)) | 
| 95 |  | dvn0 25960 | . . . . . . . . . . 11
⊢ ((𝑆 ⊆ ℂ ∧ (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘0) = (𝑥 ∈ 𝑋 ↦ 𝐴)) | 
| 96 | 31, 94, 95 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘0) = (𝑥 ∈ 𝑋 ↦ 𝐴)) | 
| 97 | 96 | fveq1d 6908 | . . . . . . . . 9
⊢ (𝜑 → (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘0)‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) | 
| 98 | 97 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘0)‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) | 
| 99 |  | eqid 2737 | . . . . . . . . . 10
⊢ (𝑥 ∈ 𝑋 ↦ 𝐴) = (𝑥 ∈ 𝑋 ↦ 𝐴) | 
| 100 | 99 | fvmpt2 7027 | . . . . . . . . 9
⊢ ((𝑥 ∈ 𝑋 ∧ 𝐴 ∈ ℂ) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴) | 
| 101 | 72, 34, 100 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴) | 
| 102 | 91, 98, 101 | 3eqtrrd 2782 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 = ⦋0 / 𝑛⦌𝐵) | 
| 103 | 102 | oveq1d 7446 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐴 / 𝐶) = (⦋0 / 𝑛⦌𝐵 / 𝐶)) | 
| 104 | 103 | mpteq2dva 5242 | . . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)) = (𝑥 ∈ 𝑋 ↦ (⦋0 / 𝑛⦌𝐵 / 𝐶))) | 
| 105 | 45, 104 | eqtrd 2777 | . . . 4
⊢ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘0) = (𝑥 ∈ 𝑋 ↦ (⦋0 / 𝑛⦌𝐵 / 𝐶))) | 
| 106 | 105 | a1i 11 | . . 3
⊢ (𝑀 ∈
(ℤ≥‘0) → (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘0) = (𝑥 ∈ 𝑋 ↦ (⦋0 / 𝑛⦌𝐵 / 𝐶)))) | 
| 107 |  | simp3 1139 | . . . . 5
⊢ ((𝑗 ∈ (0..^𝑀) ∧ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) ∧ 𝜑) → 𝜑) | 
| 108 |  | simp1 1137 | . . . . 5
⊢ ((𝑗 ∈ (0..^𝑀) ∧ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) ∧ 𝜑) → 𝑗 ∈ (0..^𝑀)) | 
| 109 |  | simpr 484 | . . . . . . 7
⊢ (((𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) ∧ 𝜑) → 𝜑) | 
| 110 |  | simpl 482 | . . . . . . 7
⊢ (((𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) ∧ 𝜑) → (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶)))) | 
| 111 | 109, 110 | mpd 15 | . . . . . 6
⊢ (((𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) ∧ 𝜑) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) | 
| 112 | 111 | 3adant1 1131 | . . . . 5
⊢ ((𝑗 ∈ (0..^𝑀) ∧ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) ∧ 𝜑) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) | 
| 113 | 31 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) → 𝑆 ⊆ ℂ) | 
| 114 | 43 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) → (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)) ∈ (ℂ ↑pm 𝑆)) | 
| 115 |  | elfzofz 13715 | . . . . . . . 8
⊢ (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ (0...𝑀)) | 
| 116 |  | elfznn0 13660 | . . . . . . . . 9
⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ0) | 
| 117 | 116 | ad2antlr 727 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) → 𝑗 ∈ ℕ0) | 
| 118 | 115, 117 | sylanl2 681 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) → 𝑗 ∈ ℕ0) | 
| 119 |  | dvnp1 25961 | . . . . . . 7
⊢ ((𝑆 ⊆ ℂ ∧ (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)) ∈ (ℂ ↑pm 𝑆) ∧ 𝑗 ∈ ℕ0) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘(𝑗 + 1)) = (𝑆 D ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗))) | 
| 120 | 113, 114,
118, 119 | syl3anc 1373 | . . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘(𝑗 + 1)) = (𝑆 D ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗))) | 
| 121 |  | oveq2 7439 | . . . . . . 7
⊢ (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶)) → (𝑆 D ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗)) = (𝑆 D (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶)))) | 
| 122 | 121 | adantl 481 | . . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) → (𝑆 D ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗)) = (𝑆 D (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶)))) | 
| 123 | 31 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑆 ⊆ ℂ) | 
| 124 | 43 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)) ∈ (ℂ ↑pm 𝑆)) | 
| 125 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ (0...𝑀)) | 
| 126 | 125, 116 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ0) | 
| 127 | 115, 126 | sylan2 593 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑗 ∈ ℕ0) | 
| 128 | 123, 124,
127, 119 | syl3anc 1373 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘(𝑗 + 1)) = (𝑆 D ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗))) | 
| 129 | 128 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘(𝑗 + 1)) = (𝑆 D ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗))) | 
| 130 | 29 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑆 ∈ {ℝ, ℂ}) | 
| 131 |  | simplr 769 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ 𝑋) → 𝑗 ∈ (0...𝑀)) | 
| 132 | 46 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ 𝑋) → 𝜑) | 
| 133 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) | 
| 134 | 132, 133,
131 | 3jca 1129 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ 𝑋) → (𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑗 ∈ (0...𝑀))) | 
| 135 |  | nfcv 2905 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑛𝑗 | 
| 136 |  | nfv 1914 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛(𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑗 ∈ (0...𝑀)) | 
| 137 | 135 | nfcsb1 3922 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛⦋𝑗 / 𝑛⦌𝐵 | 
| 138 | 137, 78 | nfel 2920 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛⦋𝑗 / 𝑛⦌𝐵 ∈ ℂ | 
| 139 | 136, 138 | nfim 1896 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑛((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑗 ∈ (0...𝑀)) → ⦋𝑗 / 𝑛⦌𝐵 ∈ ℂ) | 
| 140 |  | eleq1 2829 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑗 → (𝑛 ∈ (0...𝑀) ↔ 𝑗 ∈ (0...𝑀))) | 
| 141 | 140 | 3anbi3d 1444 | . . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑗 → ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑛 ∈ (0...𝑀)) ↔ (𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑗 ∈ (0...𝑀)))) | 
| 142 |  | csbeq1a 3913 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑗 → 𝐵 = ⦋𝑗 / 𝑛⦌𝐵) | 
| 143 | 142 | eleq1d 2826 | . . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑗 → (𝐵 ∈ ℂ ↔ ⦋𝑗 / 𝑛⦌𝐵 ∈ ℂ)) | 
| 144 | 141, 143 | imbi12d 344 | . . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑗 → (((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑛 ∈ (0...𝑀)) → 𝐵 ∈ ℂ) ↔ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑗 ∈ (0...𝑀)) → ⦋𝑗 / 𝑛⦌𝐵 ∈ ℂ))) | 
| 145 | 135, 139,
144, 84 | vtoclgf 3569 | . . . . . . . . . . . . 13
⊢ (𝑗 ∈ (0...𝑀) → ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑗 ∈ (0...𝑀)) → ⦋𝑗 / 𝑛⦌𝐵 ∈ ℂ)) | 
| 146 | 131, 134,
145 | sylc 65 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ 𝑋) → ⦋𝑗 / 𝑛⦌𝐵 ∈ ℂ) | 
| 147 | 115, 146 | sylanl2 681 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑥 ∈ 𝑋) → ⦋𝑗 / 𝑛⦌𝐵 ∈ ℂ) | 
| 148 |  | fzofzp1 13803 | . . . . . . . . . . . . 13
⊢ (𝑗 ∈ (0..^𝑀) → (𝑗 + 1) ∈ (0...𝑀)) | 
| 149 | 148 | ad2antlr 727 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑥 ∈ 𝑋) → (𝑗 + 1) ∈ (0...𝑀)) | 
| 150 | 115, 132 | sylanl2 681 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑥 ∈ 𝑋) → 𝜑) | 
| 151 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) | 
| 152 | 150, 151,
149 | 3jca 1129 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑥 ∈ 𝑋) → (𝜑 ∧ 𝑥 ∈ 𝑋 ∧ (𝑗 + 1) ∈ (0...𝑀))) | 
| 153 |  | nfcv 2905 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑛(𝑗 + 1) | 
| 154 |  | nfv 1914 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑛(𝜑 ∧ 𝑥 ∈ 𝑋 ∧ (𝑗 + 1) ∈ (0...𝑀)) | 
| 155 | 153 | nfcsb1 3922 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛⦋(𝑗 + 1) / 𝑛⦌𝐵 | 
| 156 | 155, 78 | nfel 2920 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑛⦋(𝑗 + 1) / 𝑛⦌𝐵 ∈ ℂ | 
| 157 | 154, 156 | nfim 1896 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑛((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ (𝑗 + 1) ∈ (0...𝑀)) → ⦋(𝑗 + 1) / 𝑛⦌𝐵 ∈ ℂ) | 
| 158 |  | eleq1 2829 | . . . . . . . . . . . . . . 15
⊢ (𝑛 = (𝑗 + 1) → (𝑛 ∈ (0...𝑀) ↔ (𝑗 + 1) ∈ (0...𝑀))) | 
| 159 | 158 | 3anbi3d 1444 | . . . . . . . . . . . . . 14
⊢ (𝑛 = (𝑗 + 1) → ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑛 ∈ (0...𝑀)) ↔ (𝜑 ∧ 𝑥 ∈ 𝑋 ∧ (𝑗 + 1) ∈ (0...𝑀)))) | 
| 160 |  | csbeq1a 3913 | . . . . . . . . . . . . . . 15
⊢ (𝑛 = (𝑗 + 1) → 𝐵 = ⦋(𝑗 + 1) / 𝑛⦌𝐵) | 
| 161 | 160 | eleq1d 2826 | . . . . . . . . . . . . . 14
⊢ (𝑛 = (𝑗 + 1) → (𝐵 ∈ ℂ ↔ ⦋(𝑗 + 1) / 𝑛⦌𝐵 ∈ ℂ)) | 
| 162 | 159, 161 | imbi12d 344 | . . . . . . . . . . . . 13
⊢ (𝑛 = (𝑗 + 1) → (((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑛 ∈ (0...𝑀)) → 𝐵 ∈ ℂ) ↔ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ (𝑗 + 1) ∈ (0...𝑀)) → ⦋(𝑗 + 1) / 𝑛⦌𝐵 ∈ ℂ))) | 
| 163 | 153, 157,
162, 84 | vtoclgf 3569 | . . . . . . . . . . . 12
⊢ ((𝑗 + 1) ∈ (0...𝑀) → ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ (𝑗 + 1) ∈ (0...𝑀)) → ⦋(𝑗 + 1) / 𝑛⦌𝐵 ∈ ℂ)) | 
| 164 | 149, 152,
163 | sylc 65 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑥 ∈ 𝑋) → ⦋(𝑗 + 1) / 𝑛⦌𝐵 ∈ ℂ) | 
| 165 |  | simpl 482 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝜑) | 
| 166 | 115 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑗 ∈ (0...𝑀)) | 
| 167 |  | nfv 1914 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑛(𝜑 ∧ 𝑗 ∈ (0...𝑀)) | 
| 168 |  | nfcv 2905 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑛((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑗) | 
| 169 | 54, 137 | nfmpt 5249 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑛(𝑥 ∈ 𝑋 ↦ ⦋𝑗 / 𝑛⦌𝐵) | 
| 170 | 168, 169 | nfeq 2919 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑛((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑗) = (𝑥 ∈ 𝑋 ↦ ⦋𝑗 / 𝑛⦌𝐵) | 
| 171 | 167, 170 | nfim 1896 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑗) = (𝑥 ∈ 𝑋 ↦ ⦋𝑗 / 𝑛⦌𝐵)) | 
| 172 | 140 | anbi2d 630 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑗 → ((𝜑 ∧ 𝑛 ∈ (0...𝑀)) ↔ (𝜑 ∧ 𝑗 ∈ (0...𝑀)))) | 
| 173 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑗 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑗)) | 
| 174 | 142 | mpteq2dv 5244 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑗 → (𝑥 ∈ 𝑋 ↦ 𝐵) = (𝑥 ∈ 𝑋 ↦ ⦋𝑗 / 𝑛⦌𝐵)) | 
| 175 | 173, 174 | eqeq12d 2753 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑗 → (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = (𝑥 ∈ 𝑋 ↦ 𝐵) ↔ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑗) = (𝑥 ∈ 𝑋 ↦ ⦋𝑗 / 𝑛⦌𝐵))) | 
| 176 | 172, 175 | imbi12d 344 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑗 → (((𝜑 ∧ 𝑛 ∈ (0...𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = (𝑥 ∈ 𝑋 ↦ 𝐵)) ↔ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑗) = (𝑥 ∈ 𝑋 ↦ ⦋𝑗 / 𝑛⦌𝐵)))) | 
| 177 | 171, 176,
67 | chvarfv 2240 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑗) = (𝑥 ∈ 𝑋 ↦ ⦋𝑗 / 𝑛⦌𝐵)) | 
| 178 | 165, 166,
177 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑗) = (𝑥 ∈ 𝑋 ↦ ⦋𝑗 / 𝑛⦌𝐵)) | 
| 179 | 178 | eqcomd 2743 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑥 ∈ 𝑋 ↦ ⦋𝑗 / 𝑛⦌𝐵) = ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑗)) | 
| 180 | 179 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑆 D (𝑥 ∈ 𝑋 ↦ ⦋𝑗 / 𝑛⦌𝐵)) = (𝑆 D ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑗))) | 
| 181 | 165, 94 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (ℂ ↑pm 𝑆)) | 
| 182 |  | dvnp1 25961 | . . . . . . . . . . . . . 14
⊢ ((𝑆 ⊆ ℂ ∧ (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (ℂ ↑pm 𝑆) ∧ 𝑗 ∈ ℕ0) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘(𝑗 + 1)) = (𝑆 D ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑗))) | 
| 183 | 123, 181,
127, 182 | syl3anc 1373 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘(𝑗 + 1)) = (𝑆 D ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑗))) | 
| 184 | 183 | eqcomd 2743 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑆 D ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑗)) = ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘(𝑗 + 1))) | 
| 185 | 148 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑗 + 1) ∈ (0...𝑀)) | 
| 186 | 165, 185 | jca 511 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝜑 ∧ (𝑗 + 1) ∈ (0...𝑀))) | 
| 187 |  | nfv 1914 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛(𝜑 ∧ (𝑗 + 1) ∈ (0...𝑀)) | 
| 188 |  | nfcv 2905 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘(𝑗 + 1)) | 
| 189 | 54, 155 | nfmpt 5249 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛(𝑥 ∈ 𝑋 ↦ ⦋(𝑗 + 1) / 𝑛⦌𝐵) | 
| 190 | 188, 189 | nfeq 2919 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘(𝑗 + 1)) = (𝑥 ∈ 𝑋 ↦ ⦋(𝑗 + 1) / 𝑛⦌𝐵) | 
| 191 | 187, 190 | nfim 1896 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑛((𝜑 ∧ (𝑗 + 1) ∈ (0...𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘(𝑗 + 1)) = (𝑥 ∈ 𝑋 ↦ ⦋(𝑗 + 1) / 𝑛⦌𝐵)) | 
| 192 | 158 | anbi2d 630 | . . . . . . . . . . . . . . 15
⊢ (𝑛 = (𝑗 + 1) → ((𝜑 ∧ 𝑛 ∈ (0...𝑀)) ↔ (𝜑 ∧ (𝑗 + 1) ∈ (0...𝑀)))) | 
| 193 |  | fveq2 6906 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 = (𝑗 + 1) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘(𝑗 + 1))) | 
| 194 | 160 | mpteq2dv 5244 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 = (𝑗 + 1) → (𝑥 ∈ 𝑋 ↦ 𝐵) = (𝑥 ∈ 𝑋 ↦ ⦋(𝑗 + 1) / 𝑛⦌𝐵)) | 
| 195 | 193, 194 | eqeq12d 2753 | . . . . . . . . . . . . . . 15
⊢ (𝑛 = (𝑗 + 1) → (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = (𝑥 ∈ 𝑋 ↦ 𝐵) ↔ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘(𝑗 + 1)) = (𝑥 ∈ 𝑋 ↦ ⦋(𝑗 + 1) / 𝑛⦌𝐵))) | 
| 196 | 192, 195 | imbi12d 344 | . . . . . . . . . . . . . 14
⊢ (𝑛 = (𝑗 + 1) → (((𝜑 ∧ 𝑛 ∈ (0...𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = (𝑥 ∈ 𝑋 ↦ 𝐵)) ↔ ((𝜑 ∧ (𝑗 + 1) ∈ (0...𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘(𝑗 + 1)) = (𝑥 ∈ 𝑋 ↦ ⦋(𝑗 + 1) / 𝑛⦌𝐵)))) | 
| 197 | 153, 191,
196, 67 | vtoclgf 3569 | . . . . . . . . . . . . 13
⊢ ((𝑗 + 1) ∈ (0...𝑀) → ((𝜑 ∧ (𝑗 + 1) ∈ (0...𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘(𝑗 + 1)) = (𝑥 ∈ 𝑋 ↦ ⦋(𝑗 + 1) / 𝑛⦌𝐵))) | 
| 198 | 185, 186,
197 | sylc 65 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘(𝑗 + 1)) = (𝑥 ∈ 𝑋 ↦ ⦋(𝑗 + 1) / 𝑛⦌𝐵)) | 
| 199 | 180, 184,
198 | 3eqtrd 2781 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑆 D (𝑥 ∈ 𝑋 ↦ ⦋𝑗 / 𝑛⦌𝐵)) = (𝑥 ∈ 𝑋 ↦ ⦋(𝑗 + 1) / 𝑛⦌𝐵)) | 
| 200 | 35 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝐶 ∈ ℂ) | 
| 201 | 37 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝐶 ≠ 0) | 
| 202 | 130, 147,
164, 199, 200, 201 | dvmptdivc 26003 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑆 D (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) = (𝑥 ∈ 𝑋 ↦ (⦋(𝑗 + 1) / 𝑛⦌𝐵 / 𝐶))) | 
| 203 | 202 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) → (𝑆 D (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) = (𝑥 ∈ 𝑋 ↦ (⦋(𝑗 + 1) / 𝑛⦌𝐵 / 𝐶))) | 
| 204 | 129, 122,
203 | 3eqtrd 2781 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘(𝑗 + 1)) = (𝑥 ∈ 𝑋 ↦ (⦋(𝑗 + 1) / 𝑛⦌𝐵 / 𝐶))) | 
| 205 | 204 | eqcomd 2743 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) → (𝑥 ∈ 𝑋 ↦ (⦋(𝑗 + 1) / 𝑛⦌𝐵 / 𝐶)) = ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘(𝑗 + 1))) | 
| 206 | 205, 120,
122 | 3eqtrrd 2782 | . . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) → (𝑆 D (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) = (𝑥 ∈ 𝑋 ↦ (⦋(𝑗 + 1) / 𝑛⦌𝐵 / 𝐶))) | 
| 207 | 120, 122,
206 | 3eqtrd 2781 | . . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘(𝑗 + 1)) = (𝑥 ∈ 𝑋 ↦ (⦋(𝑗 + 1) / 𝑛⦌𝐵 / 𝐶))) | 
| 208 | 107, 108,
112, 207 | syl21anc 838 | . . . 4
⊢ ((𝑗 ∈ (0..^𝑀) ∧ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) ∧ 𝜑) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘(𝑗 + 1)) = (𝑥 ∈ 𝑋 ↦ (⦋(𝑗 + 1) / 𝑛⦌𝐵 / 𝐶))) | 
| 209 | 208 | 3exp 1120 | . . 3
⊢ (𝑗 ∈ (0..^𝑀) → ((𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) → (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘(𝑗 + 1)) = (𝑥 ∈ 𝑋 ↦ (⦋(𝑗 + 1) / 𝑛⦌𝐵 / 𝐶))))) | 
| 210 | 8, 14, 20, 28, 106, 209 | fzind2 13824 | . 2
⊢ (𝑛 ∈ (0...𝑀) → (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑛) = (𝑥 ∈ 𝑋 ↦ (𝐵 / 𝐶)))) | 
| 211 | 1, 2, 210 | sylc 65 | 1
⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑛) = (𝑥 ∈ 𝑋 ↦ (𝐵 / 𝐶))) |