| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq1 7439 | . . . . . 6
⊢ (𝑛 = 𝑘 → (𝑛 BernPoly (𝑋 + 1)) = (𝑘 BernPoly (𝑋 + 1))) | 
| 2 |  | oveq1 7439 | . . . . . 6
⊢ (𝑛 = 𝑘 → (𝑛 BernPoly 𝑋) = (𝑘 BernPoly 𝑋)) | 
| 3 | 1, 2 | oveq12d 7450 | . . . . 5
⊢ (𝑛 = 𝑘 → ((𝑛 BernPoly (𝑋 + 1)) − (𝑛 BernPoly 𝑋)) = ((𝑘 BernPoly (𝑋 + 1)) − (𝑘 BernPoly 𝑋))) | 
| 4 |  | id 22 | . . . . . 6
⊢ (𝑛 = 𝑘 → 𝑛 = 𝑘) | 
| 5 |  | oveq1 7439 | . . . . . . 7
⊢ (𝑛 = 𝑘 → (𝑛 − 1) = (𝑘 − 1)) | 
| 6 | 5 | oveq2d 7448 | . . . . . 6
⊢ (𝑛 = 𝑘 → (𝑋↑(𝑛 − 1)) = (𝑋↑(𝑘 − 1))) | 
| 7 | 4, 6 | oveq12d 7450 | . . . . 5
⊢ (𝑛 = 𝑘 → (𝑛 · (𝑋↑(𝑛 − 1))) = (𝑘 · (𝑋↑(𝑘 − 1)))) | 
| 8 | 3, 7 | eqeq12d 2752 | . . . 4
⊢ (𝑛 = 𝑘 → (((𝑛 BernPoly (𝑋 + 1)) − (𝑛 BernPoly 𝑋)) = (𝑛 · (𝑋↑(𝑛 − 1))) ↔ ((𝑘 BernPoly (𝑋 + 1)) − (𝑘 BernPoly 𝑋)) = (𝑘 · (𝑋↑(𝑘 − 1))))) | 
| 9 | 8 | imbi2d 340 | . . 3
⊢ (𝑛 = 𝑘 → ((𝑋 ∈ ℂ → ((𝑛 BernPoly (𝑋 + 1)) − (𝑛 BernPoly 𝑋)) = (𝑛 · (𝑋↑(𝑛 − 1)))) ↔ (𝑋 ∈ ℂ → ((𝑘 BernPoly (𝑋 + 1)) − (𝑘 BernPoly 𝑋)) = (𝑘 · (𝑋↑(𝑘 − 1)))))) | 
| 10 |  | oveq1 7439 | . . . . . 6
⊢ (𝑛 = 𝑁 → (𝑛 BernPoly (𝑋 + 1)) = (𝑁 BernPoly (𝑋 + 1))) | 
| 11 |  | oveq1 7439 | . . . . . 6
⊢ (𝑛 = 𝑁 → (𝑛 BernPoly 𝑋) = (𝑁 BernPoly 𝑋)) | 
| 12 | 10, 11 | oveq12d 7450 | . . . . 5
⊢ (𝑛 = 𝑁 → ((𝑛 BernPoly (𝑋 + 1)) − (𝑛 BernPoly 𝑋)) = ((𝑁 BernPoly (𝑋 + 1)) − (𝑁 BernPoly 𝑋))) | 
| 13 |  | id 22 | . . . . . 6
⊢ (𝑛 = 𝑁 → 𝑛 = 𝑁) | 
| 14 |  | oveq1 7439 | . . . . . . 7
⊢ (𝑛 = 𝑁 → (𝑛 − 1) = (𝑁 − 1)) | 
| 15 | 14 | oveq2d 7448 | . . . . . 6
⊢ (𝑛 = 𝑁 → (𝑋↑(𝑛 − 1)) = (𝑋↑(𝑁 − 1))) | 
| 16 | 13, 15 | oveq12d 7450 | . . . . 5
⊢ (𝑛 = 𝑁 → (𝑛 · (𝑋↑(𝑛 − 1))) = (𝑁 · (𝑋↑(𝑁 − 1)))) | 
| 17 | 12, 16 | eqeq12d 2752 | . . . 4
⊢ (𝑛 = 𝑁 → (((𝑛 BernPoly (𝑋 + 1)) − (𝑛 BernPoly 𝑋)) = (𝑛 · (𝑋↑(𝑛 − 1))) ↔ ((𝑁 BernPoly (𝑋 + 1)) − (𝑁 BernPoly 𝑋)) = (𝑁 · (𝑋↑(𝑁 − 1))))) | 
| 18 | 17 | imbi2d 340 | . . 3
⊢ (𝑛 = 𝑁 → ((𝑋 ∈ ℂ → ((𝑛 BernPoly (𝑋 + 1)) − (𝑛 BernPoly 𝑋)) = (𝑛 · (𝑋↑(𝑛 − 1)))) ↔ (𝑋 ∈ ℂ → ((𝑁 BernPoly (𝑋 + 1)) − (𝑁 BernPoly 𝑋)) = (𝑁 · (𝑋↑(𝑁 − 1)))))) | 
| 19 |  | simp1 1136 | . . . . 5
⊢ ((𝑛 ∈ ℕ ∧
∀𝑘 ∈
(1...(𝑛 − 1))(𝑋 ∈ ℂ → ((𝑘 BernPoly (𝑋 + 1)) − (𝑘 BernPoly 𝑋)) = (𝑘 · (𝑋↑(𝑘 − 1)))) ∧ 𝑋 ∈ ℂ) → 𝑛 ∈ ℕ) | 
| 20 |  | simp3 1138 | . . . . 5
⊢ ((𝑛 ∈ ℕ ∧
∀𝑘 ∈
(1...(𝑛 − 1))(𝑋 ∈ ℂ → ((𝑘 BernPoly (𝑋 + 1)) − (𝑘 BernPoly 𝑋)) = (𝑘 · (𝑋↑(𝑘 − 1)))) ∧ 𝑋 ∈ ℂ) → 𝑋 ∈ ℂ) | 
| 21 |  | simpl3 1193 | . . . . . 6
⊢ (((𝑛 ∈ ℕ ∧
∀𝑘 ∈
(1...(𝑛 − 1))(𝑋 ∈ ℂ → ((𝑘 BernPoly (𝑋 + 1)) − (𝑘 BernPoly 𝑋)) = (𝑘 · (𝑋↑(𝑘 − 1)))) ∧ 𝑋 ∈ ℂ) ∧ 𝑚 ∈ (1...(𝑛 − 1))) → 𝑋 ∈ ℂ) | 
| 22 |  | oveq1 7439 | . . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → (𝑘 BernPoly (𝑋 + 1)) = (𝑚 BernPoly (𝑋 + 1))) | 
| 23 |  | oveq1 7439 | . . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → (𝑘 BernPoly 𝑋) = (𝑚 BernPoly 𝑋)) | 
| 24 | 22, 23 | oveq12d 7450 | . . . . . . . . . 10
⊢ (𝑘 = 𝑚 → ((𝑘 BernPoly (𝑋 + 1)) − (𝑘 BernPoly 𝑋)) = ((𝑚 BernPoly (𝑋 + 1)) − (𝑚 BernPoly 𝑋))) | 
| 25 |  | id 22 | . . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → 𝑘 = 𝑚) | 
| 26 |  | oveq1 7439 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝑚 → (𝑘 − 1) = (𝑚 − 1)) | 
| 27 | 26 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → (𝑋↑(𝑘 − 1)) = (𝑋↑(𝑚 − 1))) | 
| 28 | 25, 27 | oveq12d 7450 | . . . . . . . . . 10
⊢ (𝑘 = 𝑚 → (𝑘 · (𝑋↑(𝑘 − 1))) = (𝑚 · (𝑋↑(𝑚 − 1)))) | 
| 29 | 24, 28 | eqeq12d 2752 | . . . . . . . . 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 3620 | . . . . . . 7
⊢
((∀𝑘 ∈
(1...(𝑛 − 1))(𝑋 ∈ ℂ → ((𝑘 BernPoly (𝑋 + 1)) − (𝑘 BernPoly 𝑋)) = (𝑘 · (𝑋↑(𝑘 − 1)))) ∧ 𝑚 ∈ (1...(𝑛 − 1))) → (𝑋 ∈ ℂ → ((𝑚 BernPoly (𝑋 + 1)) − (𝑚 BernPoly 𝑋)) = (𝑚 · (𝑋↑(𝑚 − 1))))) | 
| 32 | 31 | 3ad2antl2 1186 | . . . . . 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 16091 | . . . 4
⊢ ((𝑛 ∈ ℕ ∧
∀𝑘 ∈
(1...(𝑛 − 1))(𝑋 ∈ ℂ → ((𝑘 BernPoly (𝑋 + 1)) − (𝑘 BernPoly 𝑋)) = (𝑘 · (𝑋↑(𝑘 − 1)))) ∧ 𝑋 ∈ ℂ) → ((𝑛 BernPoly (𝑋 + 1)) − (𝑛 BernPoly 𝑋)) = (𝑛 · (𝑋↑(𝑛 − 1)))) | 
| 35 | 34 | 3exp 1119 | . . 3
⊢ (𝑛 ∈ ℕ →
(∀𝑘 ∈
(1...(𝑛 − 1))(𝑋 ∈ ℂ → ((𝑘 BernPoly (𝑋 + 1)) − (𝑘 BernPoly 𝑋)) = (𝑘 · (𝑋↑(𝑘 − 1)))) → (𝑋 ∈ ℂ → ((𝑛 BernPoly (𝑋 + 1)) − (𝑛 BernPoly 𝑋)) = (𝑛 · (𝑋↑(𝑛 − 1)))))) | 
| 36 | 9, 18, 35 | nnsinds 14030 | . 2
⊢ (𝑁 ∈ ℕ → (𝑋 ∈ ℂ → ((𝑁 BernPoly (𝑋 + 1)) − (𝑁 BernPoly 𝑋)) = (𝑁 · (𝑋↑(𝑁 − 1))))) | 
| 37 | 36 | imp 406 | 1
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ ℂ) → ((𝑁 BernPoly (𝑋 + 1)) − (𝑁 BernPoly 𝑋)) = (𝑁 · (𝑋↑(𝑁 − 1)))) |