Metamath Proof Explorer

Theorem basellem4

Description: Lemma for basel . By basellem3 , the expression P ( ( cot x ) ^ 2 ) = sin ( N x ) / ( sin x ) ^ N goes to zero whenever x = n _pi / N for some n e. ( 1 ... M ) , so this function enumerates M distinct roots of a degree- M polynomial, which must therefore be all the roots by fta1 . (Contributed by Mario Carneiro, 28-Jul-2014)

Ref Expression
Hypotheses basel.n ⊢ 𝑁 = ( ( 2 · 𝑀 ) + 1 )
basel.p ⊢ 𝑃 = ( 𝑡 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑁 C ( 2 · 𝑗 ) ) · ( - 1 ↑ ( 𝑀 − 𝑗 ) ) ) · ( 𝑡 ↑ 𝑗 ) ) )
basel.t ⊢ 𝑇 = ( 𝑛 ∈ ( 1 ... 𝑀 ) ↦ ( ( tan ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ↑ - 2 ) )
Assertion basellem4 ( 𝑀 ∈ ℕ → 𝑇 : ( 1 ... 𝑀 ) –1-1-onto→ ( ◡ 𝑃 “ { 0 } ) )

Proof

Step Hyp Ref Expression
1 basel.n ⊢ 𝑁 = ( ( 2 · 𝑀 ) + 1 )
2 basel.p ⊢ 𝑃 = ( 𝑡 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑁 C ( 2 · 𝑗 ) ) · ( - 1 ↑ ( 𝑀 − 𝑗 ) ) ) · ( 𝑡 ↑ 𝑗 ) ) )
3 basel.t ⊢ 𝑇 = ( 𝑛 ∈ ( 1 ... 𝑀 ) ↦ ( ( tan ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ↑ - 2 ) )
4 1 basellem1 ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑛 · π ) / 𝑁 ) ∈ ( 0 (,) ( π / 2 ) ) )
5 tanrpcl ⊢ ( ( ( 𝑛 · π ) / 𝑁 ) ∈ ( 0 (,) ( π / 2 ) ) → ( tan ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ∈ ℝ+ )
6 4 5 syl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( tan ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ∈ ℝ+ )
7 2z ⊢ 2 ∈ ℤ
8 znegcl ⊢ ( 2 ∈ ℤ → - 2 ∈ ℤ )
9 7 8 ax-mp ⊢ - 2 ∈ ℤ
10 rpexpcl ⊢ ( ( ( tan ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ∈ ℝ+ ∧ - 2 ∈ ℤ ) → ( ( tan ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ↑ - 2 ) ∈ ℝ+ )
11 6 9 10 sylancl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( ( tan ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ↑ - 2 ) ∈ ℝ+ )
12 11 rpcnd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( ( tan ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ↑ - 2 ) ∈ ℂ )
13 1 2 basellem3 ⊢ ( ( 𝑀 ∈ ℕ ∧ ( ( 𝑛 · π ) / 𝑁 ) ∈ ( 0 (,) ( π / 2 ) ) ) → ( 𝑃 ‘ ( ( tan ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ↑ - 2 ) ) = ( ( sin ‘ ( 𝑁 · ( ( 𝑛 · π ) / 𝑁 ) ) ) / ( ( sin ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ↑ 𝑁 ) ) )
14 4 13 syldan ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( 𝑃 ‘ ( ( tan ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ↑ - 2 ) ) = ( ( sin ‘ ( 𝑁 · ( ( 𝑛 · π ) / 𝑁 ) ) ) / ( ( sin ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ↑ 𝑁 ) ) )
15 elfzelz ⊢ ( 𝑛 ∈ ( 1 ... 𝑀 ) → 𝑛 ∈ ℤ )
16 15 adantl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → 𝑛 ∈ ℤ )
17 16 zred ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → 𝑛 ∈ ℝ )
18 pire ⊢ π ∈ ℝ
19 remulcl ⊢ ( ( 𝑛 ∈ ℝ ∧ π ∈ ℝ ) → ( 𝑛 · π ) ∈ ℝ )
20 17 18 19 sylancl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( 𝑛 · π ) ∈ ℝ )
21 20 recnd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( 𝑛 · π ) ∈ ℂ )
22 2nn ⊢ 2 ∈ ℕ
23 nnmulcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 2 · 𝑀 ) ∈ ℕ )
24 22 23 mpan ⊢ ( 𝑀 ∈ ℕ → ( 2 · 𝑀 ) ∈ ℕ )
25 24 peano2nnd ⊢ ( 𝑀 ∈ ℕ → ( ( 2 · 𝑀 ) + 1 ) ∈ ℕ )
26 1 25 eqeltrid ⊢ ( 𝑀 ∈ ℕ → 𝑁 ∈ ℕ )
27 26 adantr ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → 𝑁 ∈ ℕ )
28 27 nncnd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → 𝑁 ∈ ℂ )
29 27 nnne0d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → 𝑁 ≠ 0 )
30 21 28 29 divcan2d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( 𝑁 · ( ( 𝑛 · π ) / 𝑁 ) ) = ( 𝑛 · π ) )
31 30 fveq2d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( sin ‘ ( 𝑁 · ( ( 𝑛 · π ) / 𝑁 ) ) ) = ( sin ‘ ( 𝑛 · π ) ) )
32 sinkpi ⊢ ( 𝑛 ∈ ℤ → ( sin ‘ ( 𝑛 · π ) ) = 0 )
33 16 32 syl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( sin ‘ ( 𝑛 · π ) ) = 0 )
34 31 33 eqtrd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( sin ‘ ( 𝑁 · ( ( 𝑛 · π ) / 𝑁 ) ) ) = 0 )
35 34 oveq1d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( ( sin ‘ ( 𝑁 · ( ( 𝑛 · π ) / 𝑁 ) ) ) / ( ( sin ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ↑ 𝑁 ) ) = ( 0 / ( ( sin ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ↑ 𝑁 ) ) )
36 20 27 nndivred ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑛 · π ) / 𝑁 ) ∈ ℝ )
37 36 resincld ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( sin ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ∈ ℝ )
38 37 recnd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( sin ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ∈ ℂ )
39 27 nnnn0d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → 𝑁 ∈ ℕ0 )
40 38 39 expcld ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( ( sin ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ↑ 𝑁 ) ∈ ℂ )
41 sincosq1sgn ⊢ ( ( ( 𝑛 · π ) / 𝑁 ) ∈ ( 0 (,) ( π / 2 ) ) → ( 0 < ( sin ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ∧ 0 < ( cos ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ) )
42 4 41 syl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( 0 < ( sin ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ∧ 0 < ( cos ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ) )
43 42 simpld ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → 0 < ( sin ‘ ( ( 𝑛 · π ) / 𝑁 ) ) )
44 43 gt0ne0d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( sin ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ≠ 0 )
45 27 nnzd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → 𝑁 ∈ ℤ )
46 38 44 45 expne0d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( ( sin ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ↑ 𝑁 ) ≠ 0 )
47 40 46 div0d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( 0 / ( ( sin ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ↑ 𝑁 ) ) = 0 )
48 14 35 47 3eqtrd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( 𝑃 ‘ ( ( tan ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ↑ - 2 ) ) = 0 )
49 1 2 basellem2 ⊢ ( 𝑀 ∈ ℕ → ( 𝑃 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝑃 ) = 𝑀 ∧ ( coeff ‘ 𝑃 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ) )
50 49 simp1d ⊢ ( 𝑀 ∈ ℕ → 𝑃 ∈ ( Poly ‘ ℂ ) )
51 plyf ⊢ ( 𝑃 ∈ ( Poly ‘ ℂ ) → 𝑃 : ℂ ⟶ ℂ )
52 ffn ⊢ ( 𝑃 : ℂ ⟶ ℂ → 𝑃 Fn ℂ )
53 50 51 52 3syl ⊢ ( 𝑀 ∈ ℕ → 𝑃 Fn ℂ )
54 53 adantr ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → 𝑃 Fn ℂ )
55 fniniseg ⊢ ( 𝑃 Fn ℂ → ( ( ( tan ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ↑ - 2 ) ∈ ( ◡ 𝑃 “ { 0 } ) ↔ ( ( ( tan ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ↑ - 2 ) ∈ ℂ ∧ ( 𝑃 ‘ ( ( tan ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ↑ - 2 ) ) = 0 ) ) )
56 54 55 syl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( ( ( tan ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ↑ - 2 ) ∈ ( ◡ 𝑃 “ { 0 } ) ↔ ( ( ( tan ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ↑ - 2 ) ∈ ℂ ∧ ( 𝑃 ‘ ( ( tan ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ↑ - 2 ) ) = 0 ) ) )
57 12 48 56 mpbir2and ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( ( tan ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ↑ - 2 ) ∈ ( ◡ 𝑃 “ { 0 } ) )
58 57 3 fmptd ⊢ ( 𝑀 ∈ ℕ → 𝑇 : ( 1 ... 𝑀 ) ⟶ ( ◡ 𝑃 “ { 0 } ) )
59 fveq2 ⊢ ( 𝑘 = 𝑚 → ( 𝑇 ‘ 𝑘 ) = ( 𝑇 ‘ 𝑚 ) )
60 fveq2 ⊢ ( 𝑘 = 𝑥 → ( 𝑇 ‘ 𝑘 ) = ( 𝑇 ‘ 𝑥 ) )
61 fveq2 ⊢ ( 𝑘 = 𝑦 → ( 𝑇 ‘ 𝑘 ) = ( 𝑇 ‘ 𝑦 ) )
62 15 zred ⊢ ( 𝑛 ∈ ( 1 ... 𝑀 ) → 𝑛 ∈ ℝ )
63 62 ssriv ⊢ ( 1 ... 𝑀 ) ⊆ ℝ
64 11 rpred ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( ( tan ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ↑ - 2 ) ∈ ℝ )
65 64 3 fmptd ⊢ ( 𝑀 ∈ ℕ → 𝑇 : ( 1 ... 𝑀 ) ⟶ ℝ )
66 65 ffvelrnda ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝑇 ‘ 𝑘 ) ∈ ℝ )
67 simplr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → 𝑘 < 𝑚 )
68 63 sseli ⊢ ( 𝑘 ∈ ( 1 ... 𝑀 ) → 𝑘 ∈ ℝ )
69 68 ad2antrl ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → 𝑘 ∈ ℝ )
70 63 sseli ⊢ ( 𝑚 ∈ ( 1 ... 𝑀 ) → 𝑚 ∈ ℝ )
71 70 ad2antll ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → 𝑚 ∈ ℝ )
72 18 a1i ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → π ∈ ℝ )
73 pipos ⊢ 0 < π
74 73 a1i ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → 0 < π )
75 ltmul1 ⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑚 ∈ ℝ ∧ ( π ∈ ℝ ∧ 0 < π ) ) → ( 𝑘 < 𝑚 ↔ ( 𝑘 · π ) < ( 𝑚 · π ) ) )
76 69 71 72 74 75 syl112anc ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → ( 𝑘 < 𝑚 ↔ ( 𝑘 · π ) < ( 𝑚 · π ) ) )
77 67 76 mpbid ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → ( 𝑘 · π ) < ( 𝑚 · π ) )
78 remulcl ⊢ ( ( 𝑘 ∈ ℝ ∧ π ∈ ℝ ) → ( 𝑘 · π ) ∈ ℝ )
79 69 18 78 sylancl ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → ( 𝑘 · π ) ∈ ℝ )
80 remulcl ⊢ ( ( 𝑚 ∈ ℝ ∧ π ∈ ℝ ) → ( 𝑚 · π ) ∈ ℝ )
81 71 18 80 sylancl ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → ( 𝑚 · π ) ∈ ℝ )
82 26 ad2antrr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → 𝑁 ∈ ℕ )
83 82 nnred ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → 𝑁 ∈ ℝ )
84 82 nngt0d ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → 0 < 𝑁 )
85 ltdiv1 ⊢ ( ( ( 𝑘 · π ) ∈ ℝ ∧ ( 𝑚 · π ) ∈ ℝ ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → ( ( 𝑘 · π ) < ( 𝑚 · π ) ↔ ( ( 𝑘 · π ) / 𝑁 ) < ( ( 𝑚 · π ) / 𝑁 ) ) )
86 79 81 83 84 85 syl112anc ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → ( ( 𝑘 · π ) < ( 𝑚 · π ) ↔ ( ( 𝑘 · π ) / 𝑁 ) < ( ( 𝑚 · π ) / 𝑁 ) ) )
87 77 86 mpbid ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → ( ( 𝑘 · π ) / 𝑁 ) < ( ( 𝑚 · π ) / 𝑁 ) )
88 neghalfpirx ⊢ - ( π / 2 ) ∈ ℝ*
89 pirp ⊢ π ∈ ℝ+
90 rphalfcl ⊢ ( π ∈ ℝ+ → ( π / 2 ) ∈ ℝ+ )
91 rpge0 ⊢ ( ( π / 2 ) ∈ ℝ+ → 0 ≤ ( π / 2 ) )
92 89 90 91 mp2b ⊢ 0 ≤ ( π / 2 )
93 halfpire ⊢ ( π / 2 ) ∈ ℝ
94 le0neg2 ⊢ ( ( π / 2 ) ∈ ℝ → ( 0 ≤ ( π / 2 ) ↔ - ( π / 2 ) ≤ 0 ) )
95 93 94 ax-mp ⊢ ( 0 ≤ ( π / 2 ) ↔ - ( π / 2 ) ≤ 0 )
96 92 95 mpbi ⊢ - ( π / 2 ) ≤ 0
97 iooss1 ⊢ ( ( - ( π / 2 ) ∈ ℝ* ∧ - ( π / 2 ) ≤ 0 ) → ( 0 (,) ( π / 2 ) ) ⊆ ( - ( π / 2 ) (,) ( π / 2 ) ) )
98 88 96 97 mp2an ⊢ ( 0 (,) ( π / 2 ) ) ⊆ ( - ( π / 2 ) (,) ( π / 2 ) )
99 1 basellem1 ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑘 · π ) / 𝑁 ) ∈ ( 0 (,) ( π / 2 ) ) )
100 99 ad2ant2r ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → ( ( 𝑘 · π ) / 𝑁 ) ∈ ( 0 (,) ( π / 2 ) ) )
101 98 100 sselid ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → ( ( 𝑘 · π ) / 𝑁 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) )
102 1 basellem1 ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑚 · π ) / 𝑁 ) ∈ ( 0 (,) ( π / 2 ) ) )
103 102 ad2ant2rl ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → ( ( 𝑚 · π ) / 𝑁 ) ∈ ( 0 (,) ( π / 2 ) ) )
104 98 103 sselid ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → ( ( 𝑚 · π ) / 𝑁 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) )
105 tanord ⊢ ( ( ( ( 𝑘 · π ) / 𝑁 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ ( ( 𝑚 · π ) / 𝑁 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( 𝑘 · π ) / 𝑁 ) < ( ( 𝑚 · π ) / 𝑁 ) ↔ ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) < ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ) )
106 101 104 105 syl2anc ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → ( ( ( 𝑘 · π ) / 𝑁 ) < ( ( 𝑚 · π ) / 𝑁 ) ↔ ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) < ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ) )
107 87 106 mpbid ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) < ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) )
108 tanrpcl ⊢ ( ( ( 𝑘 · π ) / 𝑁 ) ∈ ( 0 (,) ( π / 2 ) ) → ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ∈ ℝ+ )
109 100 108 syl ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ∈ ℝ+ )
110 tanrpcl ⊢ ( ( ( 𝑚 · π ) / 𝑁 ) ∈ ( 0 (,) ( π / 2 ) ) → ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ∈ ℝ+ )
111 103 110 syl ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ∈ ℝ+ )
112 rprege0 ⊢ ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ∈ ℝ+ → ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ∈ ℝ ∧ 0 ≤ ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ) )
113 rprege0 ⊢ ( ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ∈ ℝ+ → ( ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ∈ ℝ ∧ 0 ≤ ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ) )
114 lt2sq ⊢ ( ( ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ∈ ℝ ∧ 0 ≤ ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ) ∧ ( ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ∈ ℝ ∧ 0 ≤ ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ) ) → ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) < ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ↔ ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) < ( ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ↑ 2 ) ) )
115 112 113 114 syl2an ⊢ ( ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ∈ ℝ+ ∧ ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ∈ ℝ+ ) → ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) < ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ↔ ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) < ( ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ↑ 2 ) ) )
116 109 111 115 syl2anc ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) < ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ↔ ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) < ( ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ↑ 2 ) ) )
117 107 116 mpbid ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) < ( ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ↑ 2 ) )
118 rpexpcl ⊢ ( ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ∈ ℝ+ )
119 109 7 118 sylancl ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ∈ ℝ+ )
120 rpexpcl ⊢ ( ( ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ↑ 2 ) ∈ ℝ+ )
121 111 7 120 sylancl ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → ( ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ↑ 2 ) ∈ ℝ+ )
122 119 121 ltrecd ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → ( ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) < ( ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ↑ 2 ) ↔ ( 1 / ( ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ↑ 2 ) ) < ( 1 / ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) ) )
123 117 122 mpbid ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → ( 1 / ( ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ↑ 2 ) ) < ( 1 / ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) )
124 oveq1 ⊢ ( 𝑛 = 𝑚 → ( 𝑛 · π ) = ( 𝑚 · π ) )
125 124 fvoveq1d ⊢ ( 𝑛 = 𝑚 → ( tan ‘ ( ( 𝑛 · π ) / 𝑁 ) ) = ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) )
126 125 oveq1d ⊢ ( 𝑛 = 𝑚 → ( ( tan ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ↑ - 2 ) = ( ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ↑ - 2 ) )
127 ovex ⊢ ( ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ↑ - 2 ) ∈ V
128 126 3 127 fvmpt ⊢ ( 𝑚 ∈ ( 1 ... 𝑀 ) → ( 𝑇 ‘ 𝑚 ) = ( ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ↑ - 2 ) )
129 128 ad2antll ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → ( 𝑇 ‘ 𝑚 ) = ( ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ↑ - 2 ) )
130 111 rpcnd ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ∈ ℂ )
131 2nn0 ⊢ 2 ∈ ℕ0
132 expneg ⊢ ( ( ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ↑ - 2 ) = ( 1 / ( ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ↑ 2 ) ) )
133 130 131 132 sylancl ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → ( ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ↑ - 2 ) = ( 1 / ( ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ↑ 2 ) ) )
134 129 133 eqtrd ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → ( 𝑇 ‘ 𝑚 ) = ( 1 / ( ( tan ‘ ( ( 𝑚 · π ) / 𝑁 ) ) ↑ 2 ) ) )
135 oveq1 ⊢ ( 𝑛 = 𝑘 → ( 𝑛 · π ) = ( 𝑘 · π ) )
136 135 fvoveq1d ⊢ ( 𝑛 = 𝑘 → ( tan ‘ ( ( 𝑛 · π ) / 𝑁 ) ) = ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) )
137 136 oveq1d ⊢ ( 𝑛 = 𝑘 → ( ( tan ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ↑ - 2 ) = ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) )
138 ovex ⊢ ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ∈ V
139 137 3 138 fvmpt ⊢ ( 𝑘 ∈ ( 1 ... 𝑀 ) → ( 𝑇 ‘ 𝑘 ) = ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) )
140 139 ad2antrl ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → ( 𝑇 ‘ 𝑘 ) = ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) )
141 109 rpcnd ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ∈ ℂ )
142 expneg ⊢ ( ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) = ( 1 / ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) )
143 141 131 142 sylancl ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) = ( 1 / ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) )
144 140 143 eqtrd ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → ( 𝑇 ‘ 𝑘 ) = ( 1 / ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ 2 ) ) )
145 123 134 144 3brtr4d ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑘 < 𝑚 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → ( 𝑇 ‘ 𝑚 ) < ( 𝑇 ‘ 𝑘 ) )
146 145 an32s ⊢ ( ( ( 𝑀 ∈ ℕ ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) ∧ 𝑘 < 𝑚 ) → ( 𝑇 ‘ 𝑚 ) < ( 𝑇 ‘ 𝑘 ) )
147 146 ex ⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝑘 ∈ ( 1 ... 𝑀 ) ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) ) → ( 𝑘 < 𝑚 → ( 𝑇 ‘ 𝑚 ) < ( 𝑇 ‘ 𝑘 ) ) )
148 59 60 61 63 66 147 eqord2 ⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝑦 ∈ ( 1 ... 𝑀 ) ) ) → ( 𝑥 = 𝑦 ↔ ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑦 ) ) )
149 148 biimprd ⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝑦 ∈ ( 1 ... 𝑀 ) ) ) → ( ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
150 149 ralrimivva ⊢ ( 𝑀 ∈ ℕ → ∀ 𝑥 ∈ ( 1 ... 𝑀 ) ∀ 𝑦 ∈ ( 1 ... 𝑀 ) ( ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
151 dff13 ⊢ ( 𝑇 : ( 1 ... 𝑀 ) –1-1→ ( ◡ 𝑃 “ { 0 } ) ↔ ( 𝑇 : ( 1 ... 𝑀 ) ⟶ ( ◡ 𝑃 “ { 0 } ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝑀 ) ∀ 𝑦 ∈ ( 1 ... 𝑀 ) ( ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
152 58 150 151 sylanbrc ⊢ ( 𝑀 ∈ ℕ → 𝑇 : ( 1 ... 𝑀 ) –1-1→ ( ◡ 𝑃 “ { 0 } ) )
153 49 simp2d ⊢ ( 𝑀 ∈ ℕ → ( deg ‘ 𝑃 ) = 𝑀 )
154 nnne0 ⊢ ( 𝑀 ∈ ℕ → 𝑀 ≠ 0 )
155 153 154 eqnetrd ⊢ ( 𝑀 ∈ ℕ → ( deg ‘ 𝑃 ) ≠ 0 )
156 fveq2 ⊢ ( 𝑃 = 0𝑝 → ( deg ‘ 𝑃 ) = ( deg ‘ 0𝑝 ) )
157 dgr0 ⊢ ( deg ‘ 0𝑝 ) = 0
158 156 157 eqtrdi ⊢ ( 𝑃 = 0𝑝 → ( deg ‘ 𝑃 ) = 0 )
159 158 necon3i ⊢ ( ( deg ‘ 𝑃 ) ≠ 0 → 𝑃 ≠ 0𝑝 )
160 155 159 syl ⊢ ( 𝑀 ∈ ℕ → 𝑃 ≠ 0𝑝 )
161 eqid ⊢ ( ◡ 𝑃 “ { 0 } ) = ( ◡ 𝑃 “ { 0 } )
162 161 fta1 ⊢ ( ( 𝑃 ∈ ( Poly ‘ ℂ ) ∧ 𝑃 ≠ 0𝑝 ) → ( ( ◡ 𝑃 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( ◡ 𝑃 “ { 0 } ) ) ≤ ( deg ‘ 𝑃 ) ) )
163 50 160 162 syl2anc ⊢ ( 𝑀 ∈ ℕ → ( ( ◡ 𝑃 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( ◡ 𝑃 “ { 0 } ) ) ≤ ( deg ‘ 𝑃 ) ) )
164 163 simpld ⊢ ( 𝑀 ∈ ℕ → ( ◡ 𝑃 “ { 0 } ) ∈ Fin )
165 f1domg ⊢ ( ( ◡ 𝑃 “ { 0 } ) ∈ Fin → ( 𝑇 : ( 1 ... 𝑀 ) –1-1→ ( ◡ 𝑃 “ { 0 } ) → ( 1 ... 𝑀 ) ≼ ( ◡ 𝑃 “ { 0 } ) ) )
166 164 152 165 sylc ⊢ ( 𝑀 ∈ ℕ → ( 1 ... 𝑀 ) ≼ ( ◡ 𝑃 “ { 0 } ) )
167 163 simprd ⊢ ( 𝑀 ∈ ℕ → ( ♯ ‘ ( ◡ 𝑃 “ { 0 } ) ) ≤ ( deg ‘ 𝑃 ) )
168 nnnn0 ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℕ0 )
169 hashfz1 ⊢ ( 𝑀 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑀 ) ) = 𝑀 )
170 168 169 syl ⊢ ( 𝑀 ∈ ℕ → ( ♯ ‘ ( 1 ... 𝑀 ) ) = 𝑀 )
171 153 170 eqtr4d ⊢ ( 𝑀 ∈ ℕ → ( deg ‘ 𝑃 ) = ( ♯ ‘ ( 1 ... 𝑀 ) ) )
172 167 171 breqtrd ⊢ ( 𝑀 ∈ ℕ → ( ♯ ‘ ( ◡ 𝑃 “ { 0 } ) ) ≤ ( ♯ ‘ ( 1 ... 𝑀 ) ) )
173 fzfid ⊢ ( 𝑀 ∈ ℕ → ( 1 ... 𝑀 ) ∈ Fin )
174 hashdom ⊢ ( ( ( ◡ 𝑃 “ { 0 } ) ∈ Fin ∧ ( 1 ... 𝑀 ) ∈ Fin ) → ( ( ♯ ‘ ( ◡ 𝑃 “ { 0 } ) ) ≤ ( ♯ ‘ ( 1 ... 𝑀 ) ) ↔ ( ◡ 𝑃 “ { 0 } ) ≼ ( 1 ... 𝑀 ) ) )
175 164 173 174 syl2anc ⊢ ( 𝑀 ∈ ℕ → ( ( ♯ ‘ ( ◡ 𝑃 “ { 0 } ) ) ≤ ( ♯ ‘ ( 1 ... 𝑀 ) ) ↔ ( ◡ 𝑃 “ { 0 } ) ≼ ( 1 ... 𝑀 ) ) )
176 172 175 mpbid ⊢ ( 𝑀 ∈ ℕ → ( ◡ 𝑃 “ { 0 } ) ≼ ( 1 ... 𝑀 ) )
177 sbth ⊢ ( ( ( 1 ... 𝑀 ) ≼ ( ◡ 𝑃 “ { 0 } ) ∧ ( ◡ 𝑃 “ { 0 } ) ≼ ( 1 ... 𝑀 ) ) → ( 1 ... 𝑀 ) ≈ ( ◡ 𝑃 “ { 0 } ) )
178 166 176 177 syl2anc ⊢ ( 𝑀 ∈ ℕ → ( 1 ... 𝑀 ) ≈ ( ◡ 𝑃 “ { 0 } ) )
179 f1finf1o ⊢ ( ( ( 1 ... 𝑀 ) ≈ ( ◡ 𝑃 “ { 0 } ) ∧ ( ◡ 𝑃 “ { 0 } ) ∈ Fin ) → ( 𝑇 : ( 1 ... 𝑀 ) –1-1→ ( ◡ 𝑃 “ { 0 } ) ↔ 𝑇 : ( 1 ... 𝑀 ) –1-1-onto→ ( ◡ 𝑃 “ { 0 } ) ) )
180 178 164 179 syl2anc ⊢ ( 𝑀 ∈ ℕ → ( 𝑇 : ( 1 ... 𝑀 ) –1-1→ ( ◡ 𝑃 “ { 0 } ) ↔ 𝑇 : ( 1 ... 𝑀 ) –1-1-onto→ ( ◡ 𝑃 “ { 0 } ) ) )
181 152 180 mpbid ⊢ ( 𝑀 ∈ ℕ → 𝑇 : ( 1 ... 𝑀 ) –1-1-onto→ ( ◡ 𝑃 “ { 0 } ) )