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	$⊢ N = 2 \cdot M + 1$
	basel.p	$⊢ P = (t \in ℂ ⟼ \sum_{j = 0}^{M} (\binom{N}{2 j}) {(- 1)}^{M - j} t^{j})$
	basel.t	$⊢ T = (n \in (1 \dots M) ⟼ {\tan (\frac{n π}{N})}^{- 2})$
Assertion	basellem4	$⊢ M \in ℕ \to T : (1 \dots M) \underset{1-1 onto}{⟶} P^{-1} [\{0\}]$

Proof

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

Metamath Proof Explorer

Theorem basellem4

Proof