| Step | Hyp | Ref
| Expression |
| 1 | | oveq1 7438 |
. . . . 5
⊢ (𝑛 = 𝑘 → (𝑛 BernPoly 𝑋) = (𝑘 BernPoly 𝑋)) |
| 2 | 1 | eleq1d 2826 |
. . . 4
⊢ (𝑛 = 𝑘 → ((𝑛 BernPoly 𝑋) ∈ ℂ ↔ (𝑘 BernPoly 𝑋) ∈ ℂ)) |
| 3 | 2 | imbi2d 340 |
. . 3
⊢ (𝑛 = 𝑘 → ((𝑋 ∈ ℂ → (𝑛 BernPoly 𝑋) ∈ ℂ) ↔ (𝑋 ∈ ℂ → (𝑘 BernPoly 𝑋) ∈ ℂ))) |
| 4 | | oveq1 7438 |
. . . . 5
⊢ (𝑛 = 𝑁 → (𝑛 BernPoly 𝑋) = (𝑁 BernPoly 𝑋)) |
| 5 | 4 | eleq1d 2826 |
. . . 4
⊢ (𝑛 = 𝑁 → ((𝑛 BernPoly 𝑋) ∈ ℂ ↔ (𝑁 BernPoly 𝑋) ∈ ℂ)) |
| 6 | 5 | imbi2d 340 |
. . 3
⊢ (𝑛 = 𝑁 → ((𝑋 ∈ ℂ → (𝑛 BernPoly 𝑋) ∈ ℂ) ↔ (𝑋 ∈ ℂ → (𝑁 BernPoly 𝑋) ∈ ℂ))) |
| 7 | | r19.21v 3180 |
. . . 4
⊢
(∀𝑘 ∈
(0...(𝑛 − 1))(𝑋 ∈ ℂ → (𝑘 BernPoly 𝑋) ∈ ℂ) ↔ (𝑋 ∈ ℂ → ∀𝑘 ∈ (0...(𝑛 − 1))(𝑘 BernPoly 𝑋) ∈ ℂ)) |
| 8 | | bpolyval 16085 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (𝑛 BernPoly 𝑋) = ((𝑋↑𝑛) − Σ𝑚 ∈ (0...(𝑛 − 1))((𝑛C𝑚) · ((𝑚 BernPoly 𝑋) / ((𝑛 − 𝑚) + 1))))) |
| 9 | 8 | 3adant3 1133 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ0
∧ 𝑋 ∈ ℂ
∧ ∀𝑘 ∈
(0...(𝑛 − 1))(𝑘 BernPoly 𝑋) ∈ ℂ) → (𝑛 BernPoly 𝑋) = ((𝑋↑𝑛) − Σ𝑚 ∈ (0...(𝑛 − 1))((𝑛C𝑚) · ((𝑚 BernPoly 𝑋) / ((𝑛 − 𝑚) + 1))))) |
| 10 | | simp2 1138 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ0
∧ 𝑋 ∈ ℂ
∧ ∀𝑘 ∈
(0...(𝑛 − 1))(𝑘 BernPoly 𝑋) ∈ ℂ) → 𝑋 ∈ ℂ) |
| 11 | | simp1 1137 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ0
∧ 𝑋 ∈ ℂ
∧ ∀𝑘 ∈
(0...(𝑛 − 1))(𝑘 BernPoly 𝑋) ∈ ℂ) → 𝑛 ∈ ℕ0) |
| 12 | 10, 11 | expcld 14186 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ0
∧ 𝑋 ∈ ℂ
∧ ∀𝑘 ∈
(0...(𝑛 − 1))(𝑘 BernPoly 𝑋) ∈ ℂ) → (𝑋↑𝑛) ∈ ℂ) |
| 13 | | fzfid 14014 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ0
∧ 𝑋 ∈ ℂ
∧ ∀𝑘 ∈
(0...(𝑛 − 1))(𝑘 BernPoly 𝑋) ∈ ℂ) → (0...(𝑛 − 1)) ∈
Fin) |
| 14 | | elfzelz 13564 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ (0...(𝑛 − 1)) → 𝑚 ∈ ℤ) |
| 15 | | bccl 14361 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℕ0
∧ 𝑚 ∈ ℤ)
→ (𝑛C𝑚) ∈
ℕ0) |
| 16 | 11, 14, 15 | syl2an 596 |
. . . . . . . . . . 11
⊢ (((𝑛 ∈ ℕ0
∧ 𝑋 ∈ ℂ
∧ ∀𝑘 ∈
(0...(𝑛 − 1))(𝑘 BernPoly 𝑋) ∈ ℂ) ∧ 𝑚 ∈ (0...(𝑛 − 1))) → (𝑛C𝑚) ∈
ℕ0) |
| 17 | 16 | nn0cnd 12589 |
. . . . . . . . . 10
⊢ (((𝑛 ∈ ℕ0
∧ 𝑋 ∈ ℂ
∧ ∀𝑘 ∈
(0...(𝑛 − 1))(𝑘 BernPoly 𝑋) ∈ ℂ) ∧ 𝑚 ∈ (0...(𝑛 − 1))) → (𝑛C𝑚) ∈ ℂ) |
| 18 | | oveq1 7438 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑚 → (𝑘 BernPoly 𝑋) = (𝑚 BernPoly 𝑋)) |
| 19 | 18 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑚 → ((𝑘 BernPoly 𝑋) ∈ ℂ ↔ (𝑚 BernPoly 𝑋) ∈ ℂ)) |
| 20 | 19 | rspccva 3621 |
. . . . . . . . . . . 12
⊢
((∀𝑘 ∈
(0...(𝑛 − 1))(𝑘 BernPoly 𝑋) ∈ ℂ ∧ 𝑚 ∈ (0...(𝑛 − 1))) → (𝑚 BernPoly 𝑋) ∈ ℂ) |
| 21 | 20 | 3ad2antl3 1188 |
. . . . . . . . . . 11
⊢ (((𝑛 ∈ ℕ0
∧ 𝑋 ∈ ℂ
∧ ∀𝑘 ∈
(0...(𝑛 − 1))(𝑘 BernPoly 𝑋) ∈ ℂ) ∧ 𝑚 ∈ (0...(𝑛 − 1))) → (𝑚 BernPoly 𝑋) ∈ ℂ) |
| 22 | | fzssp1 13607 |
. . . . . . . . . . . . . . 15
⊢
(0...(𝑛 − 1))
⊆ (0...((𝑛 − 1)
+ 1)) |
| 23 | 11 | nn0cnd 12589 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℕ0
∧ 𝑋 ∈ ℂ
∧ ∀𝑘 ∈
(0...(𝑛 − 1))(𝑘 BernPoly 𝑋) ∈ ℂ) → 𝑛 ∈ ℂ) |
| 24 | | ax-1cn 11213 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℂ |
| 25 | | npcan 11517 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 −
1) + 1) = 𝑛) |
| 26 | 23, 24, 25 | sylancl 586 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ℕ0
∧ 𝑋 ∈ ℂ
∧ ∀𝑘 ∈
(0...(𝑛 − 1))(𝑘 BernPoly 𝑋) ∈ ℂ) → ((𝑛 − 1) + 1) = 𝑛) |
| 27 | 26 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℕ0
∧ 𝑋 ∈ ℂ
∧ ∀𝑘 ∈
(0...(𝑛 − 1))(𝑘 BernPoly 𝑋) ∈ ℂ) → (0...((𝑛 − 1) + 1)) = (0...𝑛)) |
| 28 | 22, 27 | sseqtrid 4026 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ0
∧ 𝑋 ∈ ℂ
∧ ∀𝑘 ∈
(0...(𝑛 − 1))(𝑘 BernPoly 𝑋) ∈ ℂ) → (0...(𝑛 − 1)) ⊆ (0...𝑛)) |
| 29 | 28 | sselda 3983 |
. . . . . . . . . . . . 13
⊢ (((𝑛 ∈ ℕ0
∧ 𝑋 ∈ ℂ
∧ ∀𝑘 ∈
(0...(𝑛 − 1))(𝑘 BernPoly 𝑋) ∈ ℂ) ∧ 𝑚 ∈ (0...(𝑛 − 1))) → 𝑚 ∈ (0...𝑛)) |
| 30 | | fznn0sub 13596 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ (0...𝑛) → (𝑛 − 𝑚) ∈
ℕ0) |
| 31 | | nn0p1nn 12565 |
. . . . . . . . . . . . 13
⊢ ((𝑛 − 𝑚) ∈ ℕ0 → ((𝑛 − 𝑚) + 1) ∈ ℕ) |
| 32 | 29, 30, 31 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((𝑛 ∈ ℕ0
∧ 𝑋 ∈ ℂ
∧ ∀𝑘 ∈
(0...(𝑛 − 1))(𝑘 BernPoly 𝑋) ∈ ℂ) ∧ 𝑚 ∈ (0...(𝑛 − 1))) → ((𝑛 − 𝑚) + 1) ∈ ℕ) |
| 33 | 32 | nncnd 12282 |
. . . . . . . . . . 11
⊢ (((𝑛 ∈ ℕ0
∧ 𝑋 ∈ ℂ
∧ ∀𝑘 ∈
(0...(𝑛 − 1))(𝑘 BernPoly 𝑋) ∈ ℂ) ∧ 𝑚 ∈ (0...(𝑛 − 1))) → ((𝑛 − 𝑚) + 1) ∈ ℂ) |
| 34 | 32 | nnne0d 12316 |
. . . . . . . . . . 11
⊢ (((𝑛 ∈ ℕ0
∧ 𝑋 ∈ ℂ
∧ ∀𝑘 ∈
(0...(𝑛 − 1))(𝑘 BernPoly 𝑋) ∈ ℂ) ∧ 𝑚 ∈ (0...(𝑛 − 1))) → ((𝑛 − 𝑚) + 1) ≠ 0) |
| 35 | 21, 33, 34 | divcld 12043 |
. . . . . . . . . 10
⊢ (((𝑛 ∈ ℕ0
∧ 𝑋 ∈ ℂ
∧ ∀𝑘 ∈
(0...(𝑛 − 1))(𝑘 BernPoly 𝑋) ∈ ℂ) ∧ 𝑚 ∈ (0...(𝑛 − 1))) → ((𝑚 BernPoly 𝑋) / ((𝑛 − 𝑚) + 1)) ∈ ℂ) |
| 36 | 17, 35 | mulcld 11281 |
. . . . . . . . 9
⊢ (((𝑛 ∈ ℕ0
∧ 𝑋 ∈ ℂ
∧ ∀𝑘 ∈
(0...(𝑛 − 1))(𝑘 BernPoly 𝑋) ∈ ℂ) ∧ 𝑚 ∈ (0...(𝑛 − 1))) → ((𝑛C𝑚) · ((𝑚 BernPoly 𝑋) / ((𝑛 − 𝑚) + 1))) ∈ ℂ) |
| 37 | 13, 36 | fsumcl 15769 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ0
∧ 𝑋 ∈ ℂ
∧ ∀𝑘 ∈
(0...(𝑛 − 1))(𝑘 BernPoly 𝑋) ∈ ℂ) → Σ𝑚 ∈ (0...(𝑛 − 1))((𝑛C𝑚) · ((𝑚 BernPoly 𝑋) / ((𝑛 − 𝑚) + 1))) ∈ ℂ) |
| 38 | 12, 37 | subcld 11620 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ0
∧ 𝑋 ∈ ℂ
∧ ∀𝑘 ∈
(0...(𝑛 − 1))(𝑘 BernPoly 𝑋) ∈ ℂ) → ((𝑋↑𝑛) − Σ𝑚 ∈ (0...(𝑛 − 1))((𝑛C𝑚) · ((𝑚 BernPoly 𝑋) / ((𝑛 − 𝑚) + 1)))) ∈ ℂ) |
| 39 | 9, 38 | eqeltrd 2841 |
. . . . . 6
⊢ ((𝑛 ∈ ℕ0
∧ 𝑋 ∈ ℂ
∧ ∀𝑘 ∈
(0...(𝑛 − 1))(𝑘 BernPoly 𝑋) ∈ ℂ) → (𝑛 BernPoly 𝑋) ∈ ℂ) |
| 40 | 39 | 3exp 1120 |
. . . . 5
⊢ (𝑛 ∈ ℕ0
→ (𝑋 ∈ ℂ
→ (∀𝑘 ∈
(0...(𝑛 − 1))(𝑘 BernPoly 𝑋) ∈ ℂ → (𝑛 BernPoly 𝑋) ∈ ℂ))) |
| 41 | 40 | a2d 29 |
. . . 4
⊢ (𝑛 ∈ ℕ0
→ ((𝑋 ∈ ℂ
→ ∀𝑘 ∈
(0...(𝑛 − 1))(𝑘 BernPoly 𝑋) ∈ ℂ) → (𝑋 ∈ ℂ → (𝑛 BernPoly 𝑋) ∈ ℂ))) |
| 42 | 7, 41 | biimtrid 242 |
. . 3
⊢ (𝑛 ∈ ℕ0
→ (∀𝑘 ∈
(0...(𝑛 − 1))(𝑋 ∈ ℂ → (𝑘 BernPoly 𝑋) ∈ ℂ) → (𝑋 ∈ ℂ → (𝑛 BernPoly 𝑋) ∈ ℂ))) |
| 43 | 3, 6, 42 | nn0sinds 14030 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝑋 ∈ ℂ
→ (𝑁 BernPoly 𝑋) ∈
ℂ)) |
| 44 | 43 | imp 406 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (𝑁 BernPoly 𝑋) ∈
ℂ) |