Step | Hyp | Ref
| Expression |
1 | | simpr 476 |
. 2
⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝑀)) → 𝑛 ∈ (0...𝑀)) |
2 | | simpl 472 |
. 2
⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝑀)) → 𝜑) |
3 | | fveq2 6103 |
. . . . 5
⊢ (𝑘 = 0 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑘) = ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘0)) |
4 | | csbeq1 3502 |
. . . . . . 7
⊢ (𝑘 = 0 → ⦋𝑘 / 𝑛⦌𝐵 = ⦋0 / 𝑛⦌𝐵) |
5 | 4 | oveq1d 6564 |
. . . . . 6
⊢ (𝑘 = 0 →
(⦋𝑘 / 𝑛⦌𝐵 / 𝐶) = (⦋0 / 𝑛⦌𝐵 / 𝐶)) |
6 | 5 | mpteq2dv 4673 |
. . . . 5
⊢ (𝑘 = 0 → (𝑥 ∈ 𝑋 ↦ (⦋𝑘 / 𝑛⦌𝐵 / 𝐶)) = (𝑥 ∈ 𝑋 ↦ (⦋0 / 𝑛⦌𝐵 / 𝐶))) |
7 | 3, 6 | eqeq12d 2625 |
. . . 4
⊢ (𝑘 = 0 → (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ (⦋𝑘 / 𝑛⦌𝐵 / 𝐶)) ↔ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘0) = (𝑥 ∈ 𝑋 ↦ (⦋0 / 𝑛⦌𝐵 / 𝐶)))) |
8 | 7 | imbi2d 329 |
. . 3
⊢ (𝑘 = 0 → ((𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ (⦋𝑘 / 𝑛⦌𝐵 / 𝐶))) ↔ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘0) = (𝑥 ∈ 𝑋 ↦ (⦋0 / 𝑛⦌𝐵 / 𝐶))))) |
9 | | fveq2 6103 |
. . . . 5
⊢ (𝑘 = 𝑗 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑘) = ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗)) |
10 | | csbeq1 3502 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → ⦋𝑘 / 𝑛⦌𝐵 = ⦋𝑗 / 𝑛⦌𝐵) |
11 | 10 | oveq1d 6564 |
. . . . . 6
⊢ (𝑘 = 𝑗 → (⦋𝑘 / 𝑛⦌𝐵 / 𝐶) = (⦋𝑗 / 𝑛⦌𝐵 / 𝐶)) |
12 | 11 | mpteq2dv 4673 |
. . . . 5
⊢ (𝑘 = 𝑗 → (𝑥 ∈ 𝑋 ↦ (⦋𝑘 / 𝑛⦌𝐵 / 𝐶)) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) |
13 | 9, 12 | eqeq12d 2625 |
. . . 4
⊢ (𝑘 = 𝑗 → (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ (⦋𝑘 / 𝑛⦌𝐵 / 𝐶)) ↔ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶)))) |
14 | 13 | imbi2d 329 |
. . 3
⊢ (𝑘 = 𝑗 → ((𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ (⦋𝑘 / 𝑛⦌𝐵 / 𝐶))) ↔ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))))) |
15 | | fveq2 6103 |
. . . . 5
⊢ (𝑘 = (𝑗 + 1) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑘) = ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘(𝑗 + 1))) |
16 | | csbeq1 3502 |
. . . . . . 7
⊢ (𝑘 = (𝑗 + 1) → ⦋𝑘 / 𝑛⦌𝐵 = ⦋(𝑗 + 1) / 𝑛⦌𝐵) |
17 | 16 | oveq1d 6564 |
. . . . . 6
⊢ (𝑘 = (𝑗 + 1) → (⦋𝑘 / 𝑛⦌𝐵 / 𝐶) = (⦋(𝑗 + 1) / 𝑛⦌𝐵 / 𝐶)) |
18 | 17 | mpteq2dv 4673 |
. . . . 5
⊢ (𝑘 = (𝑗 + 1) → (𝑥 ∈ 𝑋 ↦ (⦋𝑘 / 𝑛⦌𝐵 / 𝐶)) = (𝑥 ∈ 𝑋 ↦ (⦋(𝑗 + 1) / 𝑛⦌𝐵 / 𝐶))) |
19 | 15, 18 | eqeq12d 2625 |
. . . 4
⊢ (𝑘 = (𝑗 + 1) → (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ (⦋𝑘 / 𝑛⦌𝐵 / 𝐶)) ↔ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘(𝑗 + 1)) = (𝑥 ∈ 𝑋 ↦ (⦋(𝑗 + 1) / 𝑛⦌𝐵 / 𝐶)))) |
20 | 19 | imbi2d 329 |
. . 3
⊢ (𝑘 = (𝑗 + 1) → ((𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ (⦋𝑘 / 𝑛⦌𝐵 / 𝐶))) ↔ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘(𝑗 + 1)) = (𝑥 ∈ 𝑋 ↦ (⦋(𝑗 + 1) / 𝑛⦌𝐵 / 𝐶))))) |
21 | | fveq2 6103 |
. . . . 5
⊢ (𝑘 = 𝑛 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑘) = ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑛)) |
22 | | csbeq1a 3508 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → 𝐵 = ⦋𝑘 / 𝑛⦌𝐵) |
23 | 22 | equcoms 1934 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → 𝐵 = ⦋𝑘 / 𝑛⦌𝐵) |
24 | 23 | eqcomd 2616 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → ⦋𝑘 / 𝑛⦌𝐵 = 𝐵) |
25 | 24 | oveq1d 6564 |
. . . . . 6
⊢ (𝑘 = 𝑛 → (⦋𝑘 / 𝑛⦌𝐵 / 𝐶) = (𝐵 / 𝐶)) |
26 | 25 | mpteq2dv 4673 |
. . . . 5
⊢ (𝑘 = 𝑛 → (𝑥 ∈ 𝑋 ↦ (⦋𝑘 / 𝑛⦌𝐵 / 𝐶)) = (𝑥 ∈ 𝑋 ↦ (𝐵 / 𝐶))) |
27 | 21, 26 | eqeq12d 2625 |
. . . 4
⊢ (𝑘 = 𝑛 → (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ (⦋𝑘 / 𝑛⦌𝐵 / 𝐶)) ↔ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑛) = (𝑥 ∈ 𝑋 ↦ (𝐵 / 𝐶)))) |
28 | 27 | imbi2d 329 |
. . 3
⊢ (𝑘 = 𝑛 → ((𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑘) = (𝑥 ∈ 𝑋 ↦ (⦋𝑘 / 𝑛⦌𝐵 / 𝐶))) ↔ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑛) = (𝑥 ∈ 𝑋 ↦ (𝐵 / 𝐶))))) |
29 | | dvnmptdivc.s |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
30 | | recnprss 23474 |
. . . . . . 7
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
31 | 29, 30 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
32 | | cnex 9896 |
. . . . . . . 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 10680 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐴 / 𝐶) ∈ ℂ) |
40 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)) = (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)) |
41 | 39, 40 | fmptd 6292 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)):𝑋⟶ℂ) |
42 | | dvnmptdivc.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ⊆ 𝑆) |
43 | | elpm2r 7761 |
. . . . . . 7
⊢
(((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ ((𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)):𝑋⟶ℂ ∧ 𝑋 ⊆ 𝑆)) → (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)) ∈ (ℂ
↑pm 𝑆)) |
44 | 33, 29, 41, 42, 43 | syl22anc 1319 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)) ∈ (ℂ
↑pm 𝑆)) |
45 | | dvn0 23493 |
. . . . . 6
⊢ ((𝑆 ⊆ ℂ ∧ (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)) ∈ (ℂ
↑pm 𝑆)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘0) = (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶))) |
46 | 31, 44, 45 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘0) = (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶))) |
47 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝜑) |
48 | | dvnmptdivc.8 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
49 | | nn0uz 11598 |
. . . . . . . . . . . . . 14
⊢
ℕ0 = (ℤ≥‘0) |
50 | 48, 49 | syl6eleq 2698 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘0)) |
51 | | eluzfz1 12219 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈
(ℤ≥‘0) → 0 ∈ (0...𝑀)) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈ (0...𝑀)) |
53 | | nfv 1830 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛(𝜑 ∧ 0 ∈ (0...𝑀)) |
54 | | nfcv 2751 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘0) |
55 | | nfcv 2751 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛𝑋 |
56 | | nfcsb1v 3515 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛⦋0 / 𝑛⦌𝐵 |
57 | 55, 56 | nfmpt 4674 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛(𝑥 ∈ 𝑋 ↦ ⦋0 / 𝑛⦌𝐵) |
58 | 54, 57 | nfeq 2762 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘0) = (𝑥 ∈ 𝑋 ↦ ⦋0 / 𝑛⦌𝐵) |
59 | 53, 58 | nfim 1813 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛((𝜑 ∧ 0 ∈ (0...𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘0) = (𝑥 ∈ 𝑋 ↦ ⦋0 / 𝑛⦌𝐵)) |
60 | | c0ex 9913 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
61 | | eleq1 2676 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 0 → (𝑛 ∈ (0...𝑀) ↔ 0 ∈ (0...𝑀))) |
62 | 61 | anbi2d 736 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 0 → ((𝜑 ∧ 𝑛 ∈ (0...𝑀)) ↔ (𝜑 ∧ 0 ∈ (0...𝑀)))) |
63 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 0 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘0)) |
64 | | csbeq1a 3508 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 0 → 𝐵 = ⦋0 / 𝑛⦌𝐵) |
65 | 64 | mpteq2dv 4673 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 0 → (𝑥 ∈ 𝑋 ↦ 𝐵) = (𝑥 ∈ 𝑋 ↦ ⦋0 / 𝑛⦌𝐵)) |
66 | 63, 65 | eqeq12d 2625 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 0 → (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = (𝑥 ∈ 𝑋 ↦ 𝐵) ↔ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘0) = (𝑥 ∈ 𝑋 ↦ ⦋0 / 𝑛⦌𝐵))) |
67 | 62, 66 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 0 → (((𝜑 ∧ 𝑛 ∈ (0...𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = (𝑥 ∈ 𝑋 ↦ 𝐵)) ↔ ((𝜑 ∧ 0 ∈ (0...𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘0) = (𝑥 ∈ 𝑋 ↦ ⦋0 / 𝑛⦌𝐵)))) |
68 | | dvnmptdivc.dvn |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = (𝑥 ∈ 𝑋 ↦ 𝐵)) |
69 | 59, 60, 67, 68 | vtoclf 3231 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 0 ∈ (0...𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘0) = (𝑥 ∈ 𝑋 ↦ ⦋0 / 𝑛⦌𝐵)) |
70 | 47, 52, 69 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘0) = (𝑥 ∈ 𝑋 ↦ ⦋0 / 𝑛⦌𝐵)) |
71 | 70 | fveq1d 6105 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘0)‘𝑥) = ((𝑥 ∈ 𝑋 ↦ ⦋0 / 𝑛⦌𝐵)‘𝑥)) |
72 | 71 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘0)‘𝑥) = ((𝑥 ∈ 𝑋 ↦ ⦋0 / 𝑛⦌𝐵)‘𝑥)) |
73 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
74 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝜑) |
75 | 52 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 0 ∈ (0...𝑀)) |
76 | | 0re 9919 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ |
77 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛0 |
78 | | nfv 1830 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛(𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 0 ∈ (0...𝑀)) |
79 | | nfcv 2751 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛ℂ |
80 | 56, 79 | nfel 2763 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛⦋0 / 𝑛⦌𝐵 ∈ ℂ |
81 | 78, 80 | nfim 1813 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 0 ∈ (0...𝑀)) → ⦋0 / 𝑛⦌𝐵 ∈ ℂ) |
82 | 61 | 3anbi3d 1397 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 0 → ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑛 ∈ (0...𝑀)) ↔ (𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 0 ∈ (0...𝑀)))) |
83 | 64 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 0 → (𝐵 ∈ ℂ ↔ ⦋0 /
𝑛⦌𝐵 ∈
ℂ)) |
84 | 82, 83 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 0 → (((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑛 ∈ (0...𝑀)) → 𝐵 ∈ ℂ) ↔ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 0 ∈ (0...𝑀)) → ⦋0 / 𝑛⦌𝐵 ∈ ℂ))) |
85 | | dvnmptdivc.b |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑛 ∈ (0...𝑀)) → 𝐵 ∈ ℂ) |
86 | 77, 81, 84, 85 | vtoclgf 3237 |
. . . . . . . . . . . 12
⊢ (0 ∈
ℝ → ((𝜑 ∧
𝑥 ∈ 𝑋 ∧ 0 ∈ (0...𝑀)) → ⦋0 / 𝑛⦌𝐵 ∈ ℂ)) |
87 | 76, 86 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 0 ∈ (0...𝑀)) → ⦋0 / 𝑛⦌𝐵 ∈ ℂ) |
88 | 74, 73, 75, 87 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ⦋0 / 𝑛⦌𝐵 ∈ ℂ) |
89 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝑋 ↦ ⦋0 / 𝑛⦌𝐵) = (𝑥 ∈ 𝑋 ↦ ⦋0 / 𝑛⦌𝐵) |
90 | 89 | fvmpt2 6200 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑋 ∧ ⦋0 / 𝑛⦌𝐵 ∈ ℂ) → ((𝑥 ∈ 𝑋 ↦ ⦋0 / 𝑛⦌𝐵)‘𝑥) = ⦋0 / 𝑛⦌𝐵) |
91 | 73, 88, 90 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ↦ ⦋0 / 𝑛⦌𝐵)‘𝑥) = ⦋0 / 𝑛⦌𝐵) |
92 | 72, 91 | eqtr2d 2645 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ⦋0 / 𝑛⦌𝐵 = (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘0)‘𝑥)) |
93 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝑋 ↦ 𝐴) = (𝑥 ∈ 𝑋 ↦ 𝐴) |
94 | 34, 93 | fmptd 6292 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶ℂ) |
95 | | elpm2r 7761 |
. . . . . . . . . . . 12
⊢
(((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ ((𝑥 ∈ 𝑋 ↦ 𝐴):𝑋⟶ℂ ∧ 𝑋 ⊆ 𝑆)) → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (ℂ ↑pm
𝑆)) |
96 | 33, 29, 94, 42, 95 | syl22anc 1319 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (ℂ ↑pm
𝑆)) |
97 | | dvn0 23493 |
. . . . . . . . . . 11
⊢ ((𝑆 ⊆ ℂ ∧ (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (ℂ ↑pm
𝑆)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘0) = (𝑥 ∈ 𝑋 ↦ 𝐴)) |
98 | 31, 96, 97 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘0) = (𝑥 ∈ 𝑋 ↦ 𝐴)) |
99 | 98 | fveq1d 6105 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘0)‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) |
100 | 99 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘0)‘𝑥) = ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥)) |
101 | 93 | fvmpt2 6200 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑋 ∧ 𝐴 ∈ ℂ) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴) |
102 | 73, 34, 101 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ↦ 𝐴)‘𝑥) = 𝐴) |
103 | 92, 100, 102 | 3eqtrrd 2649 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 = ⦋0 / 𝑛⦌𝐵) |
104 | 103 | oveq1d 6564 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐴 / 𝐶) = (⦋0 / 𝑛⦌𝐵 / 𝐶)) |
105 | 104 | mpteq2dva 4672 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)) = (𝑥 ∈ 𝑋 ↦ (⦋0 / 𝑛⦌𝐵 / 𝐶))) |
106 | 46, 105 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘0) = (𝑥 ∈ 𝑋 ↦ (⦋0 / 𝑛⦌𝐵 / 𝐶))) |
107 | 106 | a1i 11 |
. . 3
⊢ (𝑀 ∈
(ℤ≥‘0) → (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘0) = (𝑥 ∈ 𝑋 ↦ (⦋0 / 𝑛⦌𝐵 / 𝐶)))) |
108 | | simp3 1056 |
. . . . 5
⊢ ((𝑗 ∈ (0..^𝑀) ∧ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) ∧ 𝜑) → 𝜑) |
109 | | simp1 1054 |
. . . . 5
⊢ ((𝑗 ∈ (0..^𝑀) ∧ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) ∧ 𝜑) → 𝑗 ∈ (0..^𝑀)) |
110 | | simpr 476 |
. . . . . . 7
⊢ (((𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) ∧ 𝜑) → 𝜑) |
111 | | simpl 472 |
. . . . . . 7
⊢ (((𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) ∧ 𝜑) → (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶)))) |
112 | 110, 111 | mpd 15 |
. . . . . 6
⊢ (((𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) ∧ 𝜑) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) |
113 | 112 | 3adant1 1072 |
. . . . 5
⊢ ((𝑗 ∈ (0..^𝑀) ∧ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) ∧ 𝜑) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) |
114 | 31 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) → 𝑆 ⊆ ℂ) |
115 | 44 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) → (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)) ∈ (ℂ
↑pm 𝑆)) |
116 | | elfzofz 12354 |
. . . . . . . 8
⊢ (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ (0...𝑀)) |
117 | | elfznn0 12302 |
. . . . . . . . 9
⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ0) |
118 | 117 | ad2antlr 759 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) → 𝑗 ∈ ℕ0) |
119 | 116, 118 | sylanl2 681 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) → 𝑗 ∈ ℕ0) |
120 | | dvnp1 23494 |
. . . . . . 7
⊢ ((𝑆 ⊆ ℂ ∧ (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)) ∈ (ℂ
↑pm 𝑆) ∧ 𝑗 ∈ ℕ0) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘(𝑗 + 1)) = (𝑆 D ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗))) |
121 | 114, 115,
119, 120 | syl3anc 1318 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘(𝑗 + 1)) = (𝑆 D ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗))) |
122 | | oveq2 6557 |
. . . . . . 7
⊢ (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶)) → (𝑆 D ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗)) = (𝑆 D (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶)))) |
123 | 122 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) → (𝑆 D ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗)) = (𝑆 D (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶)))) |
124 | 31 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑆 ⊆ ℂ) |
125 | 44 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)) ∈ (ℂ
↑pm 𝑆)) |
126 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ (0...𝑀)) |
127 | 126, 117 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ0) |
128 | 116, 127 | sylan2 490 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑗 ∈ ℕ0) |
129 | 124, 125,
128, 120 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘(𝑗 + 1)) = (𝑆 D ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗))) |
130 | 129 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘(𝑗 + 1)) = (𝑆 D ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗))) |
131 | 29 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑆 ∈ {ℝ, ℂ}) |
132 | | simplr 788 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ 𝑋) → 𝑗 ∈ (0...𝑀)) |
133 | 47 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ 𝑋) → 𝜑) |
134 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
135 | 133, 134,
132 | 3jca 1235 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ 𝑋) → (𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑗 ∈ (0...𝑀))) |
136 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛𝑗 |
137 | | nfv 1830 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛(𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑗 ∈ (0...𝑀)) |
138 | 136 | nfcsb1 3514 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛⦋𝑗 / 𝑛⦌𝐵 |
139 | 138, 79 | nfel 2763 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛⦋𝑗 / 𝑛⦌𝐵 ∈ ℂ |
140 | 137, 139 | nfim 1813 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑗 ∈ (0...𝑀)) → ⦋𝑗 / 𝑛⦌𝐵 ∈ ℂ) |
141 | | eleq1 2676 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑗 → (𝑛 ∈ (0...𝑀) ↔ 𝑗 ∈ (0...𝑀))) |
142 | 141 | 3anbi3d 1397 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑗 → ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑛 ∈ (0...𝑀)) ↔ (𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑗 ∈ (0...𝑀)))) |
143 | | csbeq1a 3508 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑗 → 𝐵 = ⦋𝑗 / 𝑛⦌𝐵) |
144 | 143 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑗 → (𝐵 ∈ ℂ ↔ ⦋𝑗 / 𝑛⦌𝐵 ∈ ℂ)) |
145 | 142, 144 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑗 → (((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑛 ∈ (0...𝑀)) → 𝐵 ∈ ℂ) ↔ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑗 ∈ (0...𝑀)) → ⦋𝑗 / 𝑛⦌𝐵 ∈ ℂ))) |
146 | 136, 140,
145, 85 | vtoclgf 3237 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (0...𝑀) → ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑗 ∈ (0...𝑀)) → ⦋𝑗 / 𝑛⦌𝐵 ∈ ℂ)) |
147 | 132, 135,
146 | sylc 63 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ 𝑋) → ⦋𝑗 / 𝑛⦌𝐵 ∈ ℂ) |
148 | 116, 147 | sylanl2 681 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑥 ∈ 𝑋) → ⦋𝑗 / 𝑛⦌𝐵 ∈ ℂ) |
149 | | fzofzp1 12431 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (0..^𝑀) → (𝑗 + 1) ∈ (0...𝑀)) |
150 | 149 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑥 ∈ 𝑋) → (𝑗 + 1) ∈ (0...𝑀)) |
151 | 116, 133 | sylanl2 681 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑥 ∈ 𝑋) → 𝜑) |
152 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
153 | 151, 152,
150 | 3jca 1235 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑥 ∈ 𝑋) → (𝜑 ∧ 𝑥 ∈ 𝑋 ∧ (𝑗 + 1) ∈ (0...𝑀))) |
154 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛(𝑗 + 1) |
155 | | nfv 1830 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛(𝜑 ∧ 𝑥 ∈ 𝑋 ∧ (𝑗 + 1) ∈ (0...𝑀)) |
156 | 154 | nfcsb1 3514 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛⦋(𝑗 + 1) / 𝑛⦌𝐵 |
157 | 156, 79 | nfel 2763 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛⦋(𝑗 + 1) / 𝑛⦌𝐵 ∈ ℂ |
158 | 155, 157 | nfim 1813 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ (𝑗 + 1) ∈ (0...𝑀)) → ⦋(𝑗 + 1) / 𝑛⦌𝐵 ∈ ℂ) |
159 | | eleq1 2676 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (𝑗 + 1) → (𝑛 ∈ (0...𝑀) ↔ (𝑗 + 1) ∈ (0...𝑀))) |
160 | 159 | 3anbi3d 1397 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (𝑗 + 1) → ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑛 ∈ (0...𝑀)) ↔ (𝜑 ∧ 𝑥 ∈ 𝑋 ∧ (𝑗 + 1) ∈ (0...𝑀)))) |
161 | | csbeq1a 3508 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (𝑗 + 1) → 𝐵 = ⦋(𝑗 + 1) / 𝑛⦌𝐵) |
162 | 161 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (𝑗 + 1) → (𝐵 ∈ ℂ ↔ ⦋(𝑗 + 1) / 𝑛⦌𝐵 ∈ ℂ)) |
163 | 160, 162 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (𝑗 + 1) → (((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑛 ∈ (0...𝑀)) → 𝐵 ∈ ℂ) ↔ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ (𝑗 + 1) ∈ (0...𝑀)) → ⦋(𝑗 + 1) / 𝑛⦌𝐵 ∈ ℂ))) |
164 | 154, 158,
163, 85 | vtoclgf 3237 |
. . . . . . . . . . . 12
⊢ ((𝑗 + 1) ∈ (0...𝑀) → ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ (𝑗 + 1) ∈ (0...𝑀)) → ⦋(𝑗 + 1) / 𝑛⦌𝐵 ∈ ℂ)) |
165 | 150, 153,
164 | sylc 63 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑥 ∈ 𝑋) → ⦋(𝑗 + 1) / 𝑛⦌𝐵 ∈ ℂ) |
166 | | simpl 472 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝜑) |
167 | 116 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑗 ∈ (0...𝑀)) |
168 | | nfv 1830 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑛(𝜑 ∧ 𝑗 ∈ (0...𝑀)) |
169 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑛((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑗) |
170 | 55, 138 | nfmpt 4674 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑛(𝑥 ∈ 𝑋 ↦ ⦋𝑗 / 𝑛⦌𝐵) |
171 | 169, 170 | nfeq 2762 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑛((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑗) = (𝑥 ∈ 𝑋 ↦ ⦋𝑗 / 𝑛⦌𝐵) |
172 | 168, 171 | nfim 1813 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑗) = (𝑥 ∈ 𝑋 ↦ ⦋𝑗 / 𝑛⦌𝐵)) |
173 | 141 | anbi2d 736 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑗 → ((𝜑 ∧ 𝑛 ∈ (0...𝑀)) ↔ (𝜑 ∧ 𝑗 ∈ (0...𝑀)))) |
174 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑗 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑗)) |
175 | 143 | mpteq2dv 4673 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑗 → (𝑥 ∈ 𝑋 ↦ 𝐵) = (𝑥 ∈ 𝑋 ↦ ⦋𝑗 / 𝑛⦌𝐵)) |
176 | 174, 175 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑗 → (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = (𝑥 ∈ 𝑋 ↦ 𝐵) ↔ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑗) = (𝑥 ∈ 𝑋 ↦ ⦋𝑗 / 𝑛⦌𝐵))) |
177 | 173, 176 | imbi12d 333 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑗 → (((𝜑 ∧ 𝑛 ∈ (0...𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = (𝑥 ∈ 𝑋 ↦ 𝐵)) ↔ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑗) = (𝑥 ∈ 𝑋 ↦ ⦋𝑗 / 𝑛⦌𝐵)))) |
178 | 172, 177,
68 | chvar 2250 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑗) = (𝑥 ∈ 𝑋 ↦ ⦋𝑗 / 𝑛⦌𝐵)) |
179 | 166, 167,
178 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑗) = (𝑥 ∈ 𝑋 ↦ ⦋𝑗 / 𝑛⦌𝐵)) |
180 | 179 | eqcomd 2616 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑥 ∈ 𝑋 ↦ ⦋𝑗 / 𝑛⦌𝐵) = ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑗)) |
181 | 180 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑆 D (𝑥 ∈ 𝑋 ↦ ⦋𝑗 / 𝑛⦌𝐵)) = (𝑆 D ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑗))) |
182 | 166, 96 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (ℂ ↑pm
𝑆)) |
183 | | dvnp1 23494 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ⊆ ℂ ∧ (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (ℂ ↑pm
𝑆) ∧ 𝑗 ∈ ℕ0) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘(𝑗 + 1)) = (𝑆 D ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑗))) |
184 | 124, 182,
128, 183 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘(𝑗 + 1)) = (𝑆 D ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑗))) |
185 | 184 | eqcomd 2616 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑆 D ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑗)) = ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘(𝑗 + 1))) |
186 | 149 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑗 + 1) ∈ (0...𝑀)) |
187 | 166, 186 | jca 553 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝜑 ∧ (𝑗 + 1) ∈ (0...𝑀))) |
188 | | nfv 1830 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛(𝜑 ∧ (𝑗 + 1) ∈ (0...𝑀)) |
189 | | nfcv 2751 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘(𝑗 + 1)) |
190 | 55, 156 | nfmpt 4674 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛(𝑥 ∈ 𝑋 ↦ ⦋(𝑗 + 1) / 𝑛⦌𝐵) |
191 | 189, 190 | nfeq 2762 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘(𝑗 + 1)) = (𝑥 ∈ 𝑋 ↦ ⦋(𝑗 + 1) / 𝑛⦌𝐵) |
192 | 188, 191 | nfim 1813 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛((𝜑 ∧ (𝑗 + 1) ∈ (0...𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘(𝑗 + 1)) = (𝑥 ∈ 𝑋 ↦ ⦋(𝑗 + 1) / 𝑛⦌𝐵)) |
193 | 159 | anbi2d 736 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (𝑗 + 1) → ((𝜑 ∧ 𝑛 ∈ (0...𝑀)) ↔ (𝜑 ∧ (𝑗 + 1) ∈ (0...𝑀)))) |
194 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (𝑗 + 1) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘(𝑗 + 1))) |
195 | 161 | mpteq2dv 4673 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (𝑗 + 1) → (𝑥 ∈ 𝑋 ↦ 𝐵) = (𝑥 ∈ 𝑋 ↦ ⦋(𝑗 + 1) / 𝑛⦌𝐵)) |
196 | 194, 195 | eqeq12d 2625 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (𝑗 + 1) → (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = (𝑥 ∈ 𝑋 ↦ 𝐵) ↔ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘(𝑗 + 1)) = (𝑥 ∈ 𝑋 ↦ ⦋(𝑗 + 1) / 𝑛⦌𝐵))) |
197 | 193, 196 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (𝑗 + 1) → (((𝜑 ∧ 𝑛 ∈ (0...𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = (𝑥 ∈ 𝑋 ↦ 𝐵)) ↔ ((𝜑 ∧ (𝑗 + 1) ∈ (0...𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘(𝑗 + 1)) = (𝑥 ∈ 𝑋 ↦ ⦋(𝑗 + 1) / 𝑛⦌𝐵)))) |
198 | 154, 192,
197, 68 | vtoclgf 3237 |
. . . . . . . . . . . . 13
⊢ ((𝑗 + 1) ∈ (0...𝑀) → ((𝜑 ∧ (𝑗 + 1) ∈ (0...𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘(𝑗 + 1)) = (𝑥 ∈ 𝑋 ↦ ⦋(𝑗 + 1) / 𝑛⦌𝐵))) |
199 | 186, 187,
198 | sylc 63 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘(𝑗 + 1)) = (𝑥 ∈ 𝑋 ↦ ⦋(𝑗 + 1) / 𝑛⦌𝐵)) |
200 | 181, 185,
199 | 3eqtrd 2648 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑆 D (𝑥 ∈ 𝑋 ↦ ⦋𝑗 / 𝑛⦌𝐵)) = (𝑥 ∈ 𝑋 ↦ ⦋(𝑗 + 1) / 𝑛⦌𝐵)) |
201 | 35 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝐶 ∈ ℂ) |
202 | 37 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝐶 ≠ 0) |
203 | 131, 148,
165, 200, 201, 202 | dvmptdivc 23534 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑆 D (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) = (𝑥 ∈ 𝑋 ↦ (⦋(𝑗 + 1) / 𝑛⦌𝐵 / 𝐶))) |
204 | 203 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) → (𝑆 D (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) = (𝑥 ∈ 𝑋 ↦ (⦋(𝑗 + 1) / 𝑛⦌𝐵 / 𝐶))) |
205 | 130, 123,
204 | 3eqtrd 2648 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘(𝑗 + 1)) = (𝑥 ∈ 𝑋 ↦ (⦋(𝑗 + 1) / 𝑛⦌𝐵 / 𝐶))) |
206 | 205 | eqcomd 2616 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) → (𝑥 ∈ 𝑋 ↦ (⦋(𝑗 + 1) / 𝑛⦌𝐵 / 𝐶)) = ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘(𝑗 + 1))) |
207 | 206, 121,
123 | 3eqtrrd 2649 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) → (𝑆 D (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) = (𝑥 ∈ 𝑋 ↦ (⦋(𝑗 + 1) / 𝑛⦌𝐵 / 𝐶))) |
208 | 121, 123,
207 | 3eqtrd 2648 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘(𝑗 + 1)) = (𝑥 ∈ 𝑋 ↦ (⦋(𝑗 + 1) / 𝑛⦌𝐵 / 𝐶))) |
209 | 108, 109,
113, 208 | syl21anc 1317 |
. . . 4
⊢ ((𝑗 ∈ (0..^𝑀) ∧ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) ∧ 𝜑) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘(𝑗 + 1)) = (𝑥 ∈ 𝑋 ↦ (⦋(𝑗 + 1) / 𝑛⦌𝐵 / 𝐶))) |
210 | 209 | 3exp 1256 |
. . 3
⊢ (𝑗 ∈ (0..^𝑀) → ((𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑗) = (𝑥 ∈ 𝑋 ↦ (⦋𝑗 / 𝑛⦌𝐵 / 𝐶))) → (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘(𝑗 + 1)) = (𝑥 ∈ 𝑋 ↦ (⦋(𝑗 + 1) / 𝑛⦌𝐵 / 𝐶))))) |
211 | 8, 14, 20, 28, 107, 210 | fzind2 12448 |
. 2
⊢ (𝑛 ∈ (0...𝑀) → (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑛) = (𝑥 ∈ 𝑋 ↦ (𝐵 / 𝐶)))) |
212 | 1, 2, 211 | sylc 63 |
1
⊢ ((𝜑 ∧ 𝑛 ∈ (0...𝑀)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ (𝐴 / 𝐶)))‘𝑛) = (𝑥 ∈ 𝑋 ↦ (𝐵 / 𝐶))) |