Metamath Proof Explorer

Theorem basellem2

Description: Lemma for basel . Show that P is a polynomial of degree M , and compute its coefficient function. (Contributed by Mario Carneiro, 30-Jul-2014)

Ref Expression
Hypotheses basel.n ⊢ 𝑁 = ( ( 2 · 𝑀 ) + 1 )
basel.p ⊢ 𝑃 = ( 𝑡 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑁 C ( 2 · 𝑗 ) ) · ( - 1 ↑ ( 𝑀 − 𝑗 ) ) ) · ( 𝑡 ↑ 𝑗 ) ) )
Assertion basellem2 ( 𝑀 ∈ ℕ → ( 𝑃 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝑃 ) = 𝑀 ∧ ( coeff ‘ 𝑃 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 basel.n ⊢ 𝑁 = ( ( 2 · 𝑀 ) + 1 )
2 basel.p ⊢ 𝑃 = ( 𝑡 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑁 C ( 2 · 𝑗 ) ) · ( - 1 ↑ ( 𝑀 − 𝑗 ) ) ) · ( 𝑡 ↑ 𝑗 ) ) )
3 ssidd ⊢ ( 𝑀 ∈ ℕ → ℂ ⊆ ℂ )
4 nnnn0 ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℕ0 )
5 elfznn0 ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℕ0 )
6 oveq2 ⊢ ( 𝑛 = 𝑗 → ( 2 · 𝑛 ) = ( 2 · 𝑗 ) )
7 6 oveq2d ⊢ ( 𝑛 = 𝑗 → ( 𝑁 C ( 2 · 𝑛 ) ) = ( 𝑁 C ( 2 · 𝑗 ) ) )
8 oveq2 ⊢ ( 𝑛 = 𝑗 → ( 𝑀 − 𝑛 ) = ( 𝑀 − 𝑗 ) )
9 8 oveq2d ⊢ ( 𝑛 = 𝑗 → ( - 1 ↑ ( 𝑀 − 𝑛 ) ) = ( - 1 ↑ ( 𝑀 − 𝑗 ) ) )
10 7 9 oveq12d ⊢ ( 𝑛 = 𝑗 → ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) = ( ( 𝑁 C ( 2 · 𝑗 ) ) · ( - 1 ↑ ( 𝑀 − 𝑗 ) ) ) )
11 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) )
12 ovex ⊢ ( ( 𝑁 C ( 2 · 𝑗 ) ) · ( - 1 ↑ ( 𝑀 − 𝑗 ) ) ) ∈ V
13 10 11 12 fvmpt ⊢ ( 𝑗 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ‘ 𝑗 ) = ( ( 𝑁 C ( 2 · 𝑗 ) ) · ( - 1 ↑ ( 𝑀 − 𝑗 ) ) ) )
14 5 13 syl ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ‘ 𝑗 ) = ( ( 𝑁 C ( 2 · 𝑗 ) ) · ( - 1 ↑ ( 𝑀 − 𝑗 ) ) ) )
15 14 adantl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ‘ 𝑗 ) = ( ( 𝑁 C ( 2 · 𝑗 ) ) · ( - 1 ↑ ( 𝑀 − 𝑗 ) ) ) )
16 2nn ⊢ 2 ∈ ℕ
17 nnmulcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 2 · 𝑀 ) ∈ ℕ )
18 16 17 mpan ⊢ ( 𝑀 ∈ ℕ → ( 2 · 𝑀 ) ∈ ℕ )
19 18 peano2nnd ⊢ ( 𝑀 ∈ ℕ → ( ( 2 · 𝑀 ) + 1 ) ∈ ℕ )
20 1 19 eqeltrid ⊢ ( 𝑀 ∈ ℕ → 𝑁 ∈ ℕ )
21 20 nnnn0d ⊢ ( 𝑀 ∈ ℕ → 𝑁 ∈ ℕ0 )
22 2z ⊢ 2 ∈ ℤ
23 nn0z ⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℤ )
24 zmulcl ⊢ ( ( 2 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 2 · 𝑛 ) ∈ ℤ )
25 22 23 24 sylancr ⊢ ( 𝑛 ∈ ℕ0 → ( 2 · 𝑛 ) ∈ ℤ )
26 bccl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 2 · 𝑛 ) ∈ ℤ ) → ( 𝑁 C ( 2 · 𝑛 ) ) ∈ ℕ0 )
27 21 25 26 syl2an ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( 𝑁 C ( 2 · 𝑛 ) ) ∈ ℕ0 )
28 27 nn0cnd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( 𝑁 C ( 2 · 𝑛 ) ) ∈ ℂ )
29 neg1cn ⊢ - 1 ∈ ℂ
30 neg1ne0 ⊢ - 1 ≠ 0
31 nnz ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℤ )
32 zsubcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑀 − 𝑛 ) ∈ ℤ )
33 31 23 32 syl2an ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( 𝑀 − 𝑛 ) ∈ ℤ )
34 expclz ⊢ ( ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ∧ ( 𝑀 − 𝑛 ) ∈ ℤ ) → ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ∈ ℂ )
35 29 30 33 34 mp3an12i ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ∈ ℂ )
36 28 35 mulcld ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ∈ ℂ )
37 36 fmpttd ⊢ ( 𝑀 ∈ ℕ → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) : ℕ0 ⟶ ℂ )
38 ffvelcdm ⊢ ( ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) : ℕ0 ⟶ ℂ ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ‘ 𝑗 ) ∈ ℂ )
39 37 5 38 syl2an ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ‘ 𝑗 ) ∈ ℂ )
40 15 39 eqeltrrd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑁 C ( 2 · 𝑗 ) ) · ( - 1 ↑ ( 𝑀 − 𝑗 ) ) ) ∈ ℂ )
41 3 4 40 elplyd ⊢ ( 𝑀 ∈ ℕ → ( 𝑡 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑁 C ( 2 · 𝑗 ) ) · ( - 1 ↑ ( 𝑀 − 𝑗 ) ) ) · ( 𝑡 ↑ 𝑗 ) ) ) ∈ ( Poly ‘ ℂ ) )
42 2 41 eqeltrid ⊢ ( 𝑀 ∈ ℕ → 𝑃 ∈ ( Poly ‘ ℂ ) )
43 nnre ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℝ )
44 nn0re ⊢ ( 𝑗 ∈ ℕ0 → 𝑗 ∈ ℝ )
45 ltnle ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑗 ∈ ℝ ) → ( 𝑀 < 𝑗 ↔ ¬ 𝑗 ≤ 𝑀 ) )
46 43 44 45 syl2an ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → ( 𝑀 < 𝑗 ↔ ¬ 𝑗 ≤ 𝑀 ) )
47 13 ad2antlr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑀 < 𝑗 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ‘ 𝑗 ) = ( ( 𝑁 C ( 2 · 𝑗 ) ) · ( - 1 ↑ ( 𝑀 − 𝑗 ) ) ) )
48 21 ad2antrr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑀 < 𝑗 ) → 𝑁 ∈ ℕ0 )
49 nn0z ⊢ ( 𝑗 ∈ ℕ0 → 𝑗 ∈ ℤ )
50 49 ad2antlr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑀 < 𝑗 ) → 𝑗 ∈ ℤ )
51 zmulcl ⊢ ( ( 2 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → ( 2 · 𝑗 ) ∈ ℤ )
52 22 50 51 sylancr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑀 < 𝑗 ) → ( 2 · 𝑗 ) ∈ ℤ )
53 ax-1cn ⊢ 1 ∈ ℂ
54 53 2timesi ⊢ ( 2 · 1 ) = ( 1 + 1 )
55 54 oveq2i ⊢ ( ( 2 · 𝑀 ) + ( 2 · 1 ) ) = ( ( 2 · 𝑀 ) + ( 1 + 1 ) )
56 2cnd ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑀 < 𝑗 ) → 2 ∈ ℂ )
57 nncn ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℂ )
58 57 ad2antrr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑀 < 𝑗 ) → 𝑀 ∈ ℂ )
59 53 a1i ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑀 < 𝑗 ) → 1 ∈ ℂ )
60 56 58 59 adddid ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑀 < 𝑗 ) → ( 2 · ( 𝑀 + 1 ) ) = ( ( 2 · 𝑀 ) + ( 2 · 1 ) ) )
61 1 oveq1i ⊢ ( 𝑁 + 1 ) = ( ( ( 2 · 𝑀 ) + 1 ) + 1 )
62 18 ad2antrr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑀 < 𝑗 ) → ( 2 · 𝑀 ) ∈ ℕ )
63 62 nncnd ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑀 < 𝑗 ) → ( 2 · 𝑀 ) ∈ ℂ )
64 63 59 59 addassd ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑀 < 𝑗 ) → ( ( ( 2 · 𝑀 ) + 1 ) + 1 ) = ( ( 2 · 𝑀 ) + ( 1 + 1 ) ) )
65 61 64 eqtrid ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑀 < 𝑗 ) → ( 𝑁 + 1 ) = ( ( 2 · 𝑀 ) + ( 1 + 1 ) ) )
66 55 60 65 3eqtr4a ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑀 < 𝑗 ) → ( 2 · ( 𝑀 + 1 ) ) = ( 𝑁 + 1 ) )
67 zltp1le ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → ( 𝑀 < 𝑗 ↔ ( 𝑀 + 1 ) ≤ 𝑗 ) )
68 31 49 67 syl2an ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → ( 𝑀 < 𝑗 ↔ ( 𝑀 + 1 ) ≤ 𝑗 ) )
69 68 biimpa ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑀 < 𝑗 ) → ( 𝑀 + 1 ) ≤ 𝑗 )
70 43 ad2antrr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑀 < 𝑗 ) → 𝑀 ∈ ℝ )
71 peano2re ⊢ ( 𝑀 ∈ ℝ → ( 𝑀 + 1 ) ∈ ℝ )
72 70 71 syl ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑀 < 𝑗 ) → ( 𝑀 + 1 ) ∈ ℝ )
73 44 ad2antlr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑀 < 𝑗 ) → 𝑗 ∈ ℝ )
74 2re ⊢ 2 ∈ ℝ
75 2pos ⊢ 0 < 2
76 74 75 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
77 76 a1i ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑀 < 𝑗 ) → ( 2 ∈ ℝ ∧ 0 < 2 ) )
78 lemul2 ⊢ ( ( ( 𝑀 + 1 ) ∈ ℝ ∧ 𝑗 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 𝑀 + 1 ) ≤ 𝑗 ↔ ( 2 · ( 𝑀 + 1 ) ) ≤ ( 2 · 𝑗 ) ) )
79 72 73 77 78 syl3anc ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑀 < 𝑗 ) → ( ( 𝑀 + 1 ) ≤ 𝑗 ↔ ( 2 · ( 𝑀 + 1 ) ) ≤ ( 2 · 𝑗 ) ) )
80 69 79 mpbid ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑀 < 𝑗 ) → ( 2 · ( 𝑀 + 1 ) ) ≤ ( 2 · 𝑗 ) )
81 66 80 eqbrtrrd ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑀 < 𝑗 ) → ( 𝑁 + 1 ) ≤ ( 2 · 𝑗 ) )
82 20 nnzd ⊢ ( 𝑀 ∈ ℕ → 𝑁 ∈ ℤ )
83 82 ad2antrr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑀 < 𝑗 ) → 𝑁 ∈ ℤ )
84 zltp1le ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 2 · 𝑗 ) ∈ ℤ ) → ( 𝑁 < ( 2 · 𝑗 ) ↔ ( 𝑁 + 1 ) ≤ ( 2 · 𝑗 ) ) )
85 83 52 84 syl2anc ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑀 < 𝑗 ) → ( 𝑁 < ( 2 · 𝑗 ) ↔ ( 𝑁 + 1 ) ≤ ( 2 · 𝑗 ) ) )
86 81 85 mpbird ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑀 < 𝑗 ) → 𝑁 < ( 2 · 𝑗 ) )
87 86 olcd ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑀 < 𝑗 ) → ( ( 2 · 𝑗 ) < 0 ∨ 𝑁 < ( 2 · 𝑗 ) ) )
88 bcval4 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 2 · 𝑗 ) ∈ ℤ ∧ ( ( 2 · 𝑗 ) < 0 ∨ 𝑁 < ( 2 · 𝑗 ) ) ) → ( 𝑁 C ( 2 · 𝑗 ) ) = 0 )
89 48 52 87 88 syl3anc ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑀 < 𝑗 ) → ( 𝑁 C ( 2 · 𝑗 ) ) = 0 )
90 89 oveq1d ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑀 < 𝑗 ) → ( ( 𝑁 C ( 2 · 𝑗 ) ) · ( - 1 ↑ ( 𝑀 − 𝑗 ) ) ) = ( 0 · ( - 1 ↑ ( 𝑀 − 𝑗 ) ) ) )
91 zsubcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → ( 𝑀 − 𝑗 ) ∈ ℤ )
92 31 49 91 syl2an ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → ( 𝑀 − 𝑗 ) ∈ ℤ )
93 expclz ⊢ ( ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ∧ ( 𝑀 − 𝑗 ) ∈ ℤ ) → ( - 1 ↑ ( 𝑀 − 𝑗 ) ) ∈ ℂ )
94 29 30 92 93 mp3an12i ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → ( - 1 ↑ ( 𝑀 − 𝑗 ) ) ∈ ℂ )
95 94 adantr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑀 < 𝑗 ) → ( - 1 ↑ ( 𝑀 − 𝑗 ) ) ∈ ℂ )
96 95 mul02d ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑀 < 𝑗 ) → ( 0 · ( - 1 ↑ ( 𝑀 − 𝑗 ) ) ) = 0 )
97 47 90 96 3eqtrd ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑀 < 𝑗 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ‘ 𝑗 ) = 0 )
98 97 ex ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → ( 𝑀 < 𝑗 → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ‘ 𝑗 ) = 0 ) )
99 46 98 sylbird ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → ( ¬ 𝑗 ≤ 𝑀 → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ‘ 𝑗 ) = 0 ) )
100 99 necon1ad ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → ( ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ‘ 𝑗 ) ≠ 0 → 𝑗 ≤ 𝑀 ) )
101 100 ralrimiva ⊢ ( 𝑀 ∈ ℕ → ∀ 𝑗 ∈ ℕ0 ( ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ‘ 𝑗 ) ≠ 0 → 𝑗 ≤ 𝑀 ) )
102 plyco0 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) : ℕ0 ⟶ ℂ ) → ( ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ↔ ∀ 𝑗 ∈ ℕ0 ( ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ‘ 𝑗 ) ≠ 0 → 𝑗 ≤ 𝑀 ) ) )
103 4 37 102 syl2anc ⊢ ( 𝑀 ∈ ℕ → ( ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ↔ ∀ 𝑗 ∈ ℕ0 ( ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ‘ 𝑗 ) ≠ 0 → 𝑗 ≤ 𝑀 ) ) )
104 101 103 mpbird ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } )
105 14 oveq1d ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → ( ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ‘ 𝑗 ) · ( 𝑡 ↑ 𝑗 ) ) = ( ( ( 𝑁 C ( 2 · 𝑗 ) ) · ( - 1 ↑ ( 𝑀 − 𝑗 ) ) ) · ( 𝑡 ↑ 𝑗 ) ) )
106 105 sumeq2i ⊢ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ‘ 𝑗 ) · ( 𝑡 ↑ 𝑗 ) ) = Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑁 C ( 2 · 𝑗 ) ) · ( - 1 ↑ ( 𝑀 − 𝑗 ) ) ) · ( 𝑡 ↑ 𝑗 ) )
107 106 mpteq2i ⊢ ( 𝑡 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ‘ 𝑗 ) · ( 𝑡 ↑ 𝑗 ) ) ) = ( 𝑡 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑁 C ( 2 · 𝑗 ) ) · ( - 1 ↑ ( 𝑀 − 𝑗 ) ) ) · ( 𝑡 ↑ 𝑗 ) ) )
108 2 107 eqtr4i ⊢ 𝑃 = ( 𝑡 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ‘ 𝑗 ) · ( 𝑡 ↑ 𝑗 ) ) )
109 108 a1i ⊢ ( 𝑀 ∈ ℕ → 𝑃 = ( 𝑡 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ‘ 𝑗 ) · ( 𝑡 ↑ 𝑗 ) ) ) )
110 oveq2 ⊢ ( 𝑛 = 𝑀 → ( 2 · 𝑛 ) = ( 2 · 𝑀 ) )
111 110 oveq2d ⊢ ( 𝑛 = 𝑀 → ( 𝑁 C ( 2 · 𝑛 ) ) = ( 𝑁 C ( 2 · 𝑀 ) ) )
112 oveq2 ⊢ ( 𝑛 = 𝑀 → ( 𝑀 − 𝑛 ) = ( 𝑀 − 𝑀 ) )
113 112 oveq2d ⊢ ( 𝑛 = 𝑀 → ( - 1 ↑ ( 𝑀 − 𝑛 ) ) = ( - 1 ↑ ( 𝑀 − 𝑀 ) ) )
114 111 113 oveq12d ⊢ ( 𝑛 = 𝑀 → ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) = ( ( 𝑁 C ( 2 · 𝑀 ) ) · ( - 1 ↑ ( 𝑀 − 𝑀 ) ) ) )
115 ovex ⊢ ( ( 𝑁 C ( 2 · 𝑀 ) ) · ( - 1 ↑ ( 𝑀 − 𝑀 ) ) ) ∈ V
116 114 11 115 fvmpt ⊢ ( 𝑀 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ‘ 𝑀 ) = ( ( 𝑁 C ( 2 · 𝑀 ) ) · ( - 1 ↑ ( 𝑀 − 𝑀 ) ) ) )
117 4 116 syl ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ‘ 𝑀 ) = ( ( 𝑁 C ( 2 · 𝑀 ) ) · ( - 1 ↑ ( 𝑀 − 𝑀 ) ) ) )
118 57 subidd ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 − 𝑀 ) = 0 )
119 118 oveq2d ⊢ ( 𝑀 ∈ ℕ → ( - 1 ↑ ( 𝑀 − 𝑀 ) ) = ( - 1 ↑ 0 ) )
120 exp0 ⊢ ( - 1 ∈ ℂ → ( - 1 ↑ 0 ) = 1 )
121 29 120 ax-mp ⊢ ( - 1 ↑ 0 ) = 1
122 119 121 eqtrdi ⊢ ( 𝑀 ∈ ℕ → ( - 1 ↑ ( 𝑀 − 𝑀 ) ) = 1 )
123 122 oveq2d ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 C ( 2 · 𝑀 ) ) · ( - 1 ↑ ( 𝑀 − 𝑀 ) ) ) = ( ( 𝑁 C ( 2 · 𝑀 ) ) · 1 ) )
124 18 nnred ⊢ ( 𝑀 ∈ ℕ → ( 2 · 𝑀 ) ∈ ℝ )
125 124 lep1d ⊢ ( 𝑀 ∈ ℕ → ( 2 · 𝑀 ) ≤ ( ( 2 · 𝑀 ) + 1 ) )
126 125 1 breqtrrdi ⊢ ( 𝑀 ∈ ℕ → ( 2 · 𝑀 ) ≤ 𝑁 )
127 18 nnnn0d ⊢ ( 𝑀 ∈ ℕ → ( 2 · 𝑀 ) ∈ ℕ0 )
128 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
129 127 128 eleqtrdi ⊢ ( 𝑀 ∈ ℕ → ( 2 · 𝑀 ) ∈ ( ℤ≥ ‘ 0 ) )
130 elfz5 ⊢ ( ( ( 2 · 𝑀 ) ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑁 ∈ ℤ ) → ( ( 2 · 𝑀 ) ∈ ( 0 ... 𝑁 ) ↔ ( 2 · 𝑀 ) ≤ 𝑁 ) )
131 129 82 130 syl2anc ⊢ ( 𝑀 ∈ ℕ → ( ( 2 · 𝑀 ) ∈ ( 0 ... 𝑁 ) ↔ ( 2 · 𝑀 ) ≤ 𝑁 ) )
132 126 131 mpbird ⊢ ( 𝑀 ∈ ℕ → ( 2 · 𝑀 ) ∈ ( 0 ... 𝑁 ) )
133 bccl2 ⊢ ( ( 2 · 𝑀 ) ∈ ( 0 ... 𝑁 ) → ( 𝑁 C ( 2 · 𝑀 ) ) ∈ ℕ )
134 132 133 syl ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 C ( 2 · 𝑀 ) ) ∈ ℕ )
135 134 nncnd ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 C ( 2 · 𝑀 ) ) ∈ ℂ )
136 135 mulridd ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 C ( 2 · 𝑀 ) ) · 1 ) = ( 𝑁 C ( 2 · 𝑀 ) ) )
137 117 123 136 3eqtrd ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ‘ 𝑀 ) = ( 𝑁 C ( 2 · 𝑀 ) ) )
138 134 nnne0d ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 C ( 2 · 𝑀 ) ) ≠ 0 )
139 137 138 eqnetrd ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ‘ 𝑀 ) ≠ 0 )
140 42 4 37 104 109 139 dgreq ⊢ ( 𝑀 ∈ ℕ → ( deg ‘ 𝑃 ) = 𝑀 )
141 42 4 37 104 109 coeeq ⊢ ( 𝑀 ∈ ℕ → ( coeff ‘ 𝑃 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) )
142 42 140 141 3jca ⊢ ( 𝑀 ∈ ℕ → ( 𝑃 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝑃 ) = 𝑀 ∧ ( coeff ‘ 𝑃 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ) )