Step | Hyp | Ref
| Expression |
1 | | oveq1 7275 |
. . . . . 6
⊢ (𝑛 = 𝑘 → (𝑛 BernPoly (𝑋 + 1)) = (𝑘 BernPoly (𝑋 + 1))) |
2 | | oveq1 7275 |
. . . . . 6
⊢ (𝑛 = 𝑘 → (𝑛 BernPoly 𝑋) = (𝑘 BernPoly 𝑋)) |
3 | 1, 2 | oveq12d 7286 |
. . . . 5
⊢ (𝑛 = 𝑘 → ((𝑛 BernPoly (𝑋 + 1)) − (𝑛 BernPoly 𝑋)) = ((𝑘 BernPoly (𝑋 + 1)) − (𝑘 BernPoly 𝑋))) |
4 | | id 22 |
. . . . . 6
⊢ (𝑛 = 𝑘 → 𝑛 = 𝑘) |
5 | | oveq1 7275 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (𝑛 − 1) = (𝑘 − 1)) |
6 | 5 | oveq2d 7284 |
. . . . . 6
⊢ (𝑛 = 𝑘 → (𝑋↑(𝑛 − 1)) = (𝑋↑(𝑘 − 1))) |
7 | 4, 6 | oveq12d 7286 |
. . . . 5
⊢ (𝑛 = 𝑘 → (𝑛 · (𝑋↑(𝑛 − 1))) = (𝑘 · (𝑋↑(𝑘 − 1)))) |
8 | 3, 7 | eqeq12d 2755 |
. . . 4
⊢ (𝑛 = 𝑘 → (((𝑛 BernPoly (𝑋 + 1)) − (𝑛 BernPoly 𝑋)) = (𝑛 · (𝑋↑(𝑛 − 1))) ↔ ((𝑘 BernPoly (𝑋 + 1)) − (𝑘 BernPoly 𝑋)) = (𝑘 · (𝑋↑(𝑘 − 1))))) |
9 | 8 | imbi2d 340 |
. . 3
⊢ (𝑛 = 𝑘 → ((𝑋 ∈ ℂ → ((𝑛 BernPoly (𝑋 + 1)) − (𝑛 BernPoly 𝑋)) = (𝑛 · (𝑋↑(𝑛 − 1)))) ↔ (𝑋 ∈ ℂ → ((𝑘 BernPoly (𝑋 + 1)) − (𝑘 BernPoly 𝑋)) = (𝑘 · (𝑋↑(𝑘 − 1)))))) |
10 | | oveq1 7275 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (𝑛 BernPoly (𝑋 + 1)) = (𝑁 BernPoly (𝑋 + 1))) |
11 | | oveq1 7275 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (𝑛 BernPoly 𝑋) = (𝑁 BernPoly 𝑋)) |
12 | 10, 11 | oveq12d 7286 |
. . . . 5
⊢ (𝑛 = 𝑁 → ((𝑛 BernPoly (𝑋 + 1)) − (𝑛 BernPoly 𝑋)) = ((𝑁 BernPoly (𝑋 + 1)) − (𝑁 BernPoly 𝑋))) |
13 | | id 22 |
. . . . . 6
⊢ (𝑛 = 𝑁 → 𝑛 = 𝑁) |
14 | | oveq1 7275 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (𝑛 − 1) = (𝑁 − 1)) |
15 | 14 | oveq2d 7284 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (𝑋↑(𝑛 − 1)) = (𝑋↑(𝑁 − 1))) |
16 | 13, 15 | oveq12d 7286 |
. . . . 5
⊢ (𝑛 = 𝑁 → (𝑛 · (𝑋↑(𝑛 − 1))) = (𝑁 · (𝑋↑(𝑁 − 1)))) |
17 | 12, 16 | eqeq12d 2755 |
. . . 4
⊢ (𝑛 = 𝑁 → (((𝑛 BernPoly (𝑋 + 1)) − (𝑛 BernPoly 𝑋)) = (𝑛 · (𝑋↑(𝑛 − 1))) ↔ ((𝑁 BernPoly (𝑋 + 1)) − (𝑁 BernPoly 𝑋)) = (𝑁 · (𝑋↑(𝑁 − 1))))) |
18 | 17 | imbi2d 340 |
. . 3
⊢ (𝑛 = 𝑁 → ((𝑋 ∈ ℂ → ((𝑛 BernPoly (𝑋 + 1)) − (𝑛 BernPoly 𝑋)) = (𝑛 · (𝑋↑(𝑛 − 1)))) ↔ (𝑋 ∈ ℂ → ((𝑁 BernPoly (𝑋 + 1)) − (𝑁 BernPoly 𝑋)) = (𝑁 · (𝑋↑(𝑁 − 1)))))) |
19 | | simp1 1134 |
. . . . 5
⊢ ((𝑛 ∈ ℕ ∧
∀𝑘 ∈
(1...(𝑛 − 1))(𝑋 ∈ ℂ → ((𝑘 BernPoly (𝑋 + 1)) − (𝑘 BernPoly 𝑋)) = (𝑘 · (𝑋↑(𝑘 − 1)))) ∧ 𝑋 ∈ ℂ) → 𝑛 ∈ ℕ) |
20 | | simp3 1136 |
. . . . 5
⊢ ((𝑛 ∈ ℕ ∧
∀𝑘 ∈
(1...(𝑛 − 1))(𝑋 ∈ ℂ → ((𝑘 BernPoly (𝑋 + 1)) − (𝑘 BernPoly 𝑋)) = (𝑘 · (𝑋↑(𝑘 − 1)))) ∧ 𝑋 ∈ ℂ) → 𝑋 ∈ ℂ) |
21 | | simpl3 1191 |
. . . . . 6
⊢ (((𝑛 ∈ ℕ ∧
∀𝑘 ∈
(1...(𝑛 − 1))(𝑋 ∈ ℂ → ((𝑘 BernPoly (𝑋 + 1)) − (𝑘 BernPoly 𝑋)) = (𝑘 · (𝑋↑(𝑘 − 1)))) ∧ 𝑋 ∈ ℂ) ∧ 𝑚 ∈ (1...(𝑛 − 1))) → 𝑋 ∈ ℂ) |
22 | | oveq1 7275 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → (𝑘 BernPoly (𝑋 + 1)) = (𝑚 BernPoly (𝑋 + 1))) |
23 | | oveq1 7275 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → (𝑘 BernPoly 𝑋) = (𝑚 BernPoly 𝑋)) |
24 | 22, 23 | oveq12d 7286 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑚 → ((𝑘 BernPoly (𝑋 + 1)) − (𝑘 BernPoly 𝑋)) = ((𝑚 BernPoly (𝑋 + 1)) − (𝑚 BernPoly 𝑋))) |
25 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → 𝑘 = 𝑚) |
26 | | oveq1 7275 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑚 → (𝑘 − 1) = (𝑚 − 1)) |
27 | 26 | oveq2d 7284 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → (𝑋↑(𝑘 − 1)) = (𝑋↑(𝑚 − 1))) |
28 | 25, 27 | oveq12d 7286 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑚 → (𝑘 · (𝑋↑(𝑘 − 1))) = (𝑚 · (𝑋↑(𝑚 − 1)))) |
29 | 24, 28 | eqeq12d 2755 |
. . . . . . . . 9
⊢ (𝑘 = 𝑚 → (((𝑘 BernPoly (𝑋 + 1)) − (𝑘 BernPoly 𝑋)) = (𝑘 · (𝑋↑(𝑘 − 1))) ↔ ((𝑚 BernPoly (𝑋 + 1)) − (𝑚 BernPoly 𝑋)) = (𝑚 · (𝑋↑(𝑚 − 1))))) |
30 | 29 | imbi2d 340 |
. . . . . . . 8
⊢ (𝑘 = 𝑚 → ((𝑋 ∈ ℂ → ((𝑘 BernPoly (𝑋 + 1)) − (𝑘 BernPoly 𝑋)) = (𝑘 · (𝑋↑(𝑘 − 1)))) ↔ (𝑋 ∈ ℂ → ((𝑚 BernPoly (𝑋 + 1)) − (𝑚 BernPoly 𝑋)) = (𝑚 · (𝑋↑(𝑚 − 1)))))) |
31 | 30 | rspccva 3559 |
. . . . . . 7
⊢
((∀𝑘 ∈
(1...(𝑛 − 1))(𝑋 ∈ ℂ → ((𝑘 BernPoly (𝑋 + 1)) − (𝑘 BernPoly 𝑋)) = (𝑘 · (𝑋↑(𝑘 − 1)))) ∧ 𝑚 ∈ (1...(𝑛 − 1))) → (𝑋 ∈ ℂ → ((𝑚 BernPoly (𝑋 + 1)) − (𝑚 BernPoly 𝑋)) = (𝑚 · (𝑋↑(𝑚 − 1))))) |
32 | 31 | 3ad2antl2 1184 |
. . . . . 6
⊢ (((𝑛 ∈ ℕ ∧
∀𝑘 ∈
(1...(𝑛 − 1))(𝑋 ∈ ℂ → ((𝑘 BernPoly (𝑋 + 1)) − (𝑘 BernPoly 𝑋)) = (𝑘 · (𝑋↑(𝑘 − 1)))) ∧ 𝑋 ∈ ℂ) ∧ 𝑚 ∈ (1...(𝑛 − 1))) → (𝑋 ∈ ℂ → ((𝑚 BernPoly (𝑋 + 1)) − (𝑚 BernPoly 𝑋)) = (𝑚 · (𝑋↑(𝑚 − 1))))) |
33 | 21, 32 | mpd 15 |
. . . . 5
⊢ (((𝑛 ∈ ℕ ∧
∀𝑘 ∈
(1...(𝑛 − 1))(𝑋 ∈ ℂ → ((𝑘 BernPoly (𝑋 + 1)) − (𝑘 BernPoly 𝑋)) = (𝑘 · (𝑋↑(𝑘 − 1)))) ∧ 𝑋 ∈ ℂ) ∧ 𝑚 ∈ (1...(𝑛 − 1))) → ((𝑚 BernPoly (𝑋 + 1)) − (𝑚 BernPoly 𝑋)) = (𝑚 · (𝑋↑(𝑚 − 1)))) |
34 | 19, 20, 33 | bpolydiflem 15745 |
. . . 4
⊢ ((𝑛 ∈ ℕ ∧
∀𝑘 ∈
(1...(𝑛 − 1))(𝑋 ∈ ℂ → ((𝑘 BernPoly (𝑋 + 1)) − (𝑘 BernPoly 𝑋)) = (𝑘 · (𝑋↑(𝑘 − 1)))) ∧ 𝑋 ∈ ℂ) → ((𝑛 BernPoly (𝑋 + 1)) − (𝑛 BernPoly 𝑋)) = (𝑛 · (𝑋↑(𝑛 − 1)))) |
35 | 34 | 3exp 1117 |
. . 3
⊢ (𝑛 ∈ ℕ →
(∀𝑘 ∈
(1...(𝑛 − 1))(𝑋 ∈ ℂ → ((𝑘 BernPoly (𝑋 + 1)) − (𝑘 BernPoly 𝑋)) = (𝑘 · (𝑋↑(𝑘 − 1)))) → (𝑋 ∈ ℂ → ((𝑛 BernPoly (𝑋 + 1)) − (𝑛 BernPoly 𝑋)) = (𝑛 · (𝑋↑(𝑛 − 1)))))) |
36 | 9, 18, 35 | nnsinds 13689 |
. 2
⊢ (𝑁 ∈ ℕ → (𝑋 ∈ ℂ → ((𝑁 BernPoly (𝑋 + 1)) − (𝑁 BernPoly 𝑋)) = (𝑁 · (𝑋↑(𝑁 − 1))))) |
37 | 36 | imp 406 |
1
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ ℂ) → ((𝑁 BernPoly (𝑋 + 1)) − (𝑁 BernPoly 𝑋)) = (𝑁 · (𝑋↑(𝑁 − 1)))) |