Theorem basellem4 22306

Description: Lemma for basel 22312. By basellem3 22305, 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 21659. (Contributed by Mario Carneiro, 28-Jul-2014.)

Hypotheses

Ref	Expression
basel.n	|- N = ( ( 2 x. M ) + 1 )
basel.p	|- P = ( t e. CC |-> sum_ j e. ( 0 ... M ) ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( t ^ j ) ) )
basel.t	|- T = ( n e. ( 1 ... M ) |-> ( ( tan ` ( ( n x. pi ) / N ) ) ^ -u 2 ) )

Assertion

Ref	Expression
basellem4	|- ( M e. NN -> T : ( 1 ... M ) -1-1-onto-> ( `' P " { 0 } ) )

Distinct variable groups:   t, j, n, M   j, N, n, t   P, n

Allowed substitution hints:   P( t, j)   T( t, j, n)

Proof of Theorem basellem4

Dummy variables k m x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		basel.n	. . . . . . . . 9 |- N = ( ( 2 x. M ) + 1 )
2	1	basellem1 22303	. . . . . . . 8 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( ( n x. pi ) / N ) e. ( 0 (,) ( pi / 2 ) ) )
3		tanrpcl 21851	. . . . . . . 8 |- ( ( ( n x. pi ) / N ) e. ( 0 (,) ( pi / 2 ) ) -> ( tan ` ( ( n x. pi ) / N ) ) e. RR+ )
4	2, 3	syl 16	. . . . . . 7 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( tan ` ( ( n x. pi ) / N ) ) e. RR+ )
5		2z 10666	. . . . . . . 8 |- 2 e. ZZ
6		znegcl 10668	. . . . . . . 8 |- ( 2 e. ZZ -> -u 2 e. ZZ )
7	5, 6	ax-mp 5	. . . . . . 7 |- -u 2 e. ZZ
8		rpexpcl 11868	. . . . . . 7 |- ( ( ( tan ` ( ( n x. pi ) / N ) ) e. RR+ /\ -u 2 e. ZZ ) -> ( ( tan ` ( ( n x. pi ) / N ) ) ^ -u 2 ) e. RR+ )
9	4, 7, 8	sylancl 655	. . . . . 6 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( ( tan ` ( ( n x. pi ) / N ) ) ^ -u 2 ) e. RR+ )
10	9	rpcnd 11017	. . . . 5 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( ( tan ` ( ( n x. pi ) / N ) ) ^ -u 2 ) e. CC )
11		basel.p	. . . . . . . 8 |- P = ( t e. CC |-> sum_ j e. ( 0 ... M ) ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( t ^ j ) ) )
12	1, 11	basellem3 22305	. . . . . . 7 |- ( ( M e. NN /\ ( ( n x. pi ) / N ) e. ( 0 (,) ( pi / 2 ) ) ) -> ( P ` ( ( tan ` ( ( n x. pi ) / N ) ) ^ -u 2 ) ) = ( ( sin ` ( N x. ( ( n x. pi ) / N ) ) ) / ( ( sin ` ( ( n x. pi ) / N ) ) ^ N ) ) )
13	2, 12	syldan 467	. . . . . 6 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( P ` ( ( tan ` ( ( n x. pi ) / N ) ) ^ -u 2 ) ) = ( ( sin ` ( N x. ( ( n x. pi ) / N ) ) ) / ( ( sin ` ( ( n x. pi ) / N ) ) ^ N ) ) )
14		elfzelz 11440	. . . . . . . . . . . . . 14 |- ( n e. ( 1 ... M ) -> n e. ZZ )
15	14	adantl 463	. . . . . . . . . . . . 13 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> n e. ZZ )
16	15	zred 10735	. . . . . . . . . . . 12 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> n e. RR )
17		pire 21806	. . . . . . . . . . . 12 |- pi e. RR
18		remulcl 9355	. . . . . . . . . . . 12 |- ( ( n e. RR /\ pi e. RR ) -> ( n x. pi ) e. RR )
19	16, 17, 18	sylancl 655	. . . . . . . . . . 11 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( n x. pi ) e. RR )
20	19	recnd 9400	. . . . . . . . . 10 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( n x. pi ) e. CC )
21		2nn 10467	. . . . . . . . . . . . . . 15 |- 2 e. NN
22		nnmulcl 10333	. . . . . . . . . . . . . . 15 |- ( ( 2 e. NN /\ M e. NN ) -> ( 2 x. M ) e. NN )
23	21, 22	mpan 663	. . . . . . . . . . . . . 14 |- ( M e. NN -> ( 2 x. M ) e. NN )
24	23	peano2nnd 10327	. . . . . . . . . . . . 13 |- ( M e. NN -> ( ( 2 x. M ) + 1 ) e. NN )
25	1, 24	syl5eqel 2517	. . . . . . . . . . . 12 |- ( M e. NN -> N e. NN )
26	25	adantr 462	. . . . . . . . . . 11 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> N e. NN )
27	26	nncnd 10326	. . . . . . . . . 10 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> N e. CC )
28	26	nnne0d 10354	. . . . . . . . . 10 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> N =/= 0 )
29	20, 27, 28	divcan2d 10097	. . . . . . . . 9 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( N x. ( ( n x. pi ) / N ) ) = ( n x. pi ) )
30	29	fveq2d 5683	. . . . . . . 8 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( sin ` ( N x. ( ( n x. pi ) / N ) ) ) = ( sin ` ( n x. pi ) ) )
31		sinkpi 21866	. . . . . . . . 9 |- ( n e. ZZ -> ( sin ` ( n x. pi ) ) = 0 )
32	15, 31	syl 16	. . . . . . . 8 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( sin ` ( n x. pi ) ) = 0 )
33	30, 32	eqtrd 2465	. . . . . . 7 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( sin ` ( N x. ( ( n x. pi ) / N ) ) ) = 0 )
34	33	oveq1d 6095	. . . . . 6 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( ( sin ` ( N x. ( ( n x. pi ) / N ) ) ) / ( ( sin ` ( ( n x. pi ) / N ) ) ^ N ) ) = ( 0 / ( ( sin ` ( ( n x. pi ) / N ) ) ^ N ) ) )
35	19, 26	nndivred 10358	. . . . . . . . . 10 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( ( n x. pi ) / N ) e. RR )
36	35	resincld 13410	. . . . . . . . 9 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( sin ` ( ( n x. pi ) / N ) ) e. RR )
37	36	recnd 9400	. . . . . . . 8 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( sin ` ( ( n x. pi ) / N ) ) e. CC )
38	26	nnnn0d 10624	. . . . . . . 8 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> N e. NN0 )
39	37, 38	expcld 11992	. . . . . . 7 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( ( sin ` ( ( n x. pi ) / N ) ) ^ N ) e. CC )
40		sincosq1sgn 21845	. . . . . . . . . . 11 |- ( ( ( n x. pi ) / N ) e. ( 0 (,) ( pi / 2 ) ) -> ( 0 < ( sin ` ( ( n x. pi ) / N ) ) /\ 0 < ( cos ` ( ( n x. pi ) / N ) ) ) )
41	2, 40	syl 16	. . . . . . . . . 10 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( 0 < ( sin ` ( ( n x. pi ) / N ) ) /\ 0 < ( cos ` ( ( n x. pi ) / N ) ) ) )
42	41	simpld 456	. . . . . . . . 9 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> 0 < ( sin ` ( ( n x. pi ) / N ) ) )
43	42	gt0ne0d 9892	. . . . . . . 8 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( sin ` ( ( n x. pi ) / N ) ) =/= 0 )
44	26	nnzd 10734	. . . . . . . 8 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> N e. ZZ )
45	37, 43, 44	expne0d 11998	. . . . . . 7 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( ( sin ` ( ( n x. pi ) / N ) ) ^ N ) =/= 0 )
46	39, 45	div0d 10094	. . . . . 6 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( 0 / ( ( sin ` ( ( n x. pi ) / N ) ) ^ N ) ) = 0 )
47	13, 34, 46	3eqtrd 2469	. . . . 5 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( P ` ( ( tan ` ( ( n x. pi ) / N ) ) ^ -u 2 ) ) = 0 )
48	1, 11	basellem2 22304	. . . . . . . . 9 |- ( M e. NN -> ( P e. (Poly ` CC ) /\ (deg ` P ) = M /\ (coeff ` P ) = ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ) )
49	48	simp1d 993	. . . . . . . 8 |- ( M e. NN -> P e. (Poly ` CC ) )
50		plyf 21551	. . . . . . . 8 |- ( P e. (Poly ` CC ) -> P : CC --> CC )
51		ffn 5547	. . . . . . . 8 |- ( P : CC --> CC -> P Fn CC )
52	49, 50, 51	3syl 20	. . . . . . 7 |- ( M e. NN -> P Fn CC )
53	52	adantr 462	. . . . . 6 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> P Fn CC )
54		fniniseg 5812	. . . . . 6 |- ( P Fn CC -> ( ( ( tan ` ( ( n x. pi ) / N ) ) ^ -u 2 ) e. ( `' P " { 0 } ) <-> ( ( ( tan ` ( ( n x. pi ) / N ) ) ^ -u 2 ) e. CC /\ ( P ` ( ( tan ` ( ( n x. pi ) / N ) ) ^ -u 2 ) ) = 0 ) ) )
55	53, 54	syl 16	. . . . 5 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( ( ( tan ` ( ( n x. pi ) / N ) ) ^ -u 2 ) e. ( `' P " { 0 } ) <-> ( ( ( tan ` ( ( n x. pi ) / N ) ) ^ -u 2 ) e. CC /\ ( P ` ( ( tan ` ( ( n x. pi ) / N ) ) ^ -u 2 ) ) = 0 ) ) )
56	10, 47, 55	mpbir2and 906	. . . 4 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( ( tan ` ( ( n x. pi ) / N ) ) ^ -u 2 ) e. ( `' P " { 0 } ) )
57		basel.t	. . . 4 |- T = ( n e. ( 1 ... M ) |-> ( ( tan ` ( ( n x. pi ) / N ) ) ^ -u 2 ) )
58	56, 57	fmptd 5855	. . 3 |- ( M e. NN -> T : ( 1 ... M ) --> ( `' P " { 0 } ) )
59		fveq2 5679	. . . . . 6 |- ( k = m -> ( T ` k ) = ( T ` m ) )
60		fveq2 5679	. . . . . 6 |- ( k = x -> ( T ` k ) = ( T ` x ) )
61		fveq2 5679	. . . . . 6 |- ( k = y -> ( T ` k ) = ( T ` y ) )
62	14	zred 10735	. . . . . . 7 |- ( n e. ( 1 ... M ) -> n e. RR )
63	62	ssriv 3348	. . . . . 6 |- ( 1 ... M ) C_ RR
64	9	rpred 11015	. . . . . . . 8 |- ( ( M e. NN /\ n e. ( 1 ... M ) ) -> ( ( tan ` ( ( n x. pi ) / N ) ) ^ -u 2 ) e. RR )
65	64, 57	fmptd 5855	. . . . . . 7 |- ( M e. NN -> T : ( 1 ... M ) --> RR )
66	65	ffvelrnda 5831	. . . . . 6 |- ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( T ` k ) e. RR )
67		simplr 747	. . . . . . . . . . . . . 14 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> k < m )
68	63	sseli 3340	. . . . . . . . . . . . . . . 16 |- ( k e. ( 1 ... M ) -> k e. RR )
69	68	ad2antrl 720	. . . . . . . . . . . . . . 15 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> k e. RR )
70	63	sseli 3340	. . . . . . . . . . . . . . . 16 |- ( m e. ( 1 ... M ) -> m e. RR )
71	70	ad2antll 721	. . . . . . . . . . . . . . 15 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> m e. RR )
72	17	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> pi e. RR )
73		pipos 21808	. . . . . . . . . . . . . . . 16 |- 0 < pi
74	73	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> 0 < pi )
75		ltmul1 10167	. . . . . . . . . . . . . . 15 |- ( ( k e. RR /\ m e. RR /\ ( pi e. RR /\ 0 < pi ) ) -> ( k < m <-> ( k x. pi ) < ( m x. pi ) ) )
76	69, 71, 72, 74, 75	syl112anc 1215	. . . . . . . . . . . . . 14 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( k < m <-> ( k x. pi ) < ( m x. pi ) ) )
77	67, 76	mpbid 210	. . . . . . . . . . . . 13 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( k x. pi ) < ( m x. pi ) )
78		remulcl 9355	. . . . . . . . . . . . . . 15 |- ( ( k e. RR /\ pi e. RR ) -> ( k x. pi ) e. RR )
79	69, 17, 78	sylancl 655	. . . . . . . . . . . . . 14 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( k x. pi ) e. RR )
80		remulcl 9355	. . . . . . . . . . . . . . 15 |- ( ( m e. RR /\ pi e. RR ) -> ( m x. pi ) e. RR )
81	71, 17, 80	sylancl 655	. . . . . . . . . . . . . 14 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( m x. pi ) e. RR )
82	25	ad2antrr 718	. . . . . . . . . . . . . . 15 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> N e. NN )
83	82	nnred 10325	. . . . . . . . . . . . . 14 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> N e. RR )
84	82	nngt0d 10353	. . . . . . . . . . . . . 14 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> 0 < N )
85		ltdiv1 10181	. . . . . . . . . . . . . 14 |- ( ( ( k x. pi ) e. RR /\ ( m x. pi ) e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( k x. pi ) < ( m x. pi ) <-> ( ( k x. pi ) / N ) < ( ( m x. pi ) / N ) ) )
86	79, 81, 83, 84, 85	syl112anc 1215	. . . . . . . . . . . . 13 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( ( k x. pi ) < ( m x. pi ) <-> ( ( k x. pi ) / N ) < ( ( m x. pi ) / N ) ) )
87	77, 86	mpbid 210	. . . . . . . . . . . 12 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( ( k x. pi ) / N ) < ( ( m x. pi ) / N ) )
88		neghalfpirx 21813	. . . . . . . . . . . . . . 15 |- -u ( pi / 2 ) e. RR*
89	17, 73	elrpii 10982	. . . . . . . . . . . . . . . . 17 |- pi e. RR+
90		rphalfcl 11003	. . . . . . . . . . . . . . . . 17 |- ( pi e. RR+ -> ( pi / 2 ) e. RR+ )
91		rpge0 10991	. . . . . . . . . . . . . . . . 17 |- ( ( pi / 2 ) e. RR+ -> 0 <_ ( pi / 2 ) )
92	89, 90, 91	mp2b 10	. . . . . . . . . . . . . . . 16 |- 0 <_ ( pi / 2 )
93		halfpire 21811	. . . . . . . . . . . . . . . . 17 |- ( pi / 2 ) e. RR
94		le0neg2 9836	. . . . . . . . . . . . . . . . 17 |- ( ( pi / 2 ) e. RR -> ( 0 <_ ( pi / 2 ) <-> -u ( pi / 2 ) <_ 0 ) )
95	93, 94	ax-mp 5	. . . . . . . . . . . . . . . 16 |- ( 0 <_ ( pi / 2 ) <-> -u ( pi / 2 ) <_ 0 )
96	92, 95	mpbi 208	. . . . . . . . . . . . . . 15 |- -u ( pi / 2 ) <_ 0
97		iooss1 11323	. . . . . . . . . . . . . . 15 |- ( ( -u ( pi / 2 ) e. RR* /\ -u ( pi / 2 ) <_ 0 ) -> ( 0 (,) ( pi / 2 ) ) C_ ( -u ( pi / 2 ) (,) ( pi / 2 ) ) )
98	88, 96, 97	mp2an 665	. . . . . . . . . . . . . 14 |- ( 0 (,) ( pi / 2 ) ) C_ ( -u ( pi / 2 ) (,) ( pi / 2 ) )
99	1	basellem1 22303	. . . . . . . . . . . . . . 15 |- ( ( M e. NN /\ k e. ( 1 ... M ) ) -> ( ( k x. pi ) / N ) e. ( 0 (,) ( pi / 2 ) ) )
100	99	ad2ant2r 739	. . . . . . . . . . . . . 14 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( ( k x. pi ) / N ) e. ( 0 (,) ( pi / 2 ) ) )
101	98, 100	sseldi 3342	. . . . . . . . . . . . 13 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( ( k x. pi ) / N ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) )
102	1	basellem1 22303	. . . . . . . . . . . . . . 15 |- ( ( M e. NN /\ m e. ( 1 ... M ) ) -> ( ( m x. pi ) / N ) e. ( 0 (,) ( pi / 2 ) ) )
103	102	ad2ant2rl 741	. . . . . . . . . . . . . 14 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( ( m x. pi ) / N ) e. ( 0 (,) ( pi / 2 ) ) )
104	98, 103	sseldi 3342	. . . . . . . . . . . . 13 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( ( m x. pi ) / N ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) )
105		tanord 21879	. . . . . . . . . . . . 13 |- ( ( ( ( k x. pi ) / N ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) /\ ( ( m x. pi ) / N ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) ) -> ( ( ( k x. pi ) / N ) < ( ( m x. pi ) / N ) <-> ( tan ` ( ( k x. pi ) / N ) ) < ( tan ` ( ( m x. pi ) / N ) ) ) )
106	101, 104, 105	syl2anc 654	. . . . . . . . . . . 12 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( ( ( k x. pi ) / N ) < ( ( m x. pi ) / N ) <-> ( tan ` ( ( k x. pi ) / N ) ) < ( tan ` ( ( m x. pi ) / N ) ) ) )
107	87, 106	mpbid 210	. . . . . . . . . . 11 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( tan ` ( ( k x. pi ) / N ) ) < ( tan ` ( ( m x. pi ) / N ) ) )
108		tanrpcl 21851	. . . . . . . . . . . . 13 |- ( ( ( k x. pi ) / N ) e. ( 0 (,) ( pi / 2 ) ) -> ( tan ` ( ( k x. pi ) / N ) ) e. RR+ )
109	100, 108	syl 16	. . . . . . . . . . . 12 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( tan ` ( ( k x. pi ) / N ) ) e. RR+ )
110		tanrpcl 21851	. . . . . . . . . . . . 13 |- ( ( ( m x. pi ) / N ) e. ( 0 (,) ( pi / 2 ) ) -> ( tan ` ( ( m x. pi ) / N ) ) e. RR+ )
111	103, 110	syl 16	. . . . . . . . . . . 12 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( tan ` ( ( m x. pi ) / N ) ) e. RR+ )
112		rprege0 10993	. . . . . . . . . . . . 13 |- ( ( tan ` ( ( k x. pi ) / N ) ) e. RR+ -> ( ( tan ` ( ( k x. pi ) / N ) ) e. RR /\ 0 <_ ( tan ` ( ( k x. pi ) / N ) ) ) )
113		rprege0 10993	. . . . . . . . . . . . 13 |- ( ( tan ` ( ( m x. pi ) / N ) ) e. RR+ -> ( ( tan ` ( ( m x. pi ) / N ) ) e. RR /\ 0 <_ ( tan ` ( ( m x. pi ) / N ) ) ) )
114		lt2sq 11923	. . . . . . . . . . . . 13 |- ( ( ( ( tan ` ( ( k x. pi ) / N ) ) e. RR /\ 0 <_ ( tan ` ( ( k x. pi ) / N ) ) ) /\ ( ( tan ` ( ( m x. pi ) / N ) ) e. RR /\ 0 <_ ( tan ` ( ( m x. pi ) / N ) ) ) ) -> ( ( tan ` ( ( k x. pi ) / N ) ) < ( tan ` ( ( m x. pi ) / N ) ) <-> ( ( tan ` ( ( k x. pi ) / N ) ) ^ 2 ) < ( ( tan ` ( ( m x. pi ) / N ) ) ^ 2 ) ) )
115	112, 113, 114	syl2an 474	. . . . . . . . . . . 12 |- ( ( ( tan ` ( ( k x. pi ) / N ) ) e. RR+ /\ ( tan ` ( ( m x. pi ) / N ) ) e. RR+ ) -> ( ( tan ` ( ( k x. pi ) / N ) ) < ( tan ` ( ( m x. pi ) / N ) ) <-> ( ( tan ` ( ( k x. pi ) / N ) ) ^ 2 ) < ( ( tan ` ( ( m x. pi ) / N ) ) ^ 2 ) ) )
116	109, 111, 115	syl2anc 654	. . . . . . . . . . 11 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( ( tan ` ( ( k x. pi ) / N ) ) < ( tan ` ( ( m x. pi ) / N ) ) <-> ( ( tan ` ( ( k x. pi ) / N ) ) ^ 2 ) < ( ( tan ` ( ( m x. pi ) / N ) ) ^ 2 ) ) )
117	107, 116	mpbid 210	. . . . . . . . . 10 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( ( tan ` ( ( k x. pi ) / N ) ) ^ 2 ) < ( ( tan ` ( ( m x. pi ) / N ) ) ^ 2 ) )
118		rpexpcl 11868	. . . . . . . . . . . 12 |- ( ( ( tan ` ( ( k x. pi ) / N ) ) e. RR+ /\ 2 e. ZZ ) -> ( ( tan ` ( ( k x. pi ) / N ) ) ^ 2 ) e. RR+ )
119	109, 5, 118	sylancl 655	. . . . . . . . . . 11 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( ( tan ` ( ( k x. pi ) / N ) ) ^ 2 ) e. RR+ )
120		rpexpcl 11868	. . . . . . . . . . . 12 |- ( ( ( tan ` ( ( m x. pi ) / N ) ) e. RR+ /\ 2 e. ZZ ) -> ( ( tan ` ( ( m x. pi ) / N ) ) ^ 2 ) e. RR+ )
121	111, 5, 120	sylancl 655	. . . . . . . . . . 11 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( ( tan ` ( ( m x. pi ) / N ) ) ^ 2 ) e. RR+ )
122	119, 121	ltrecd 11033	. . . . . . . . . 10 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( ( ( tan ` ( ( k x. pi ) / N ) ) ^ 2 ) < ( ( tan ` ( ( m x. pi ) / N ) ) ^ 2 ) <-> ( 1 / ( ( tan ` ( ( m x. pi ) / N ) ) ^ 2 ) ) < ( 1 / ( ( tan ` ( ( k x. pi ) / N ) ) ^ 2 ) ) ) )
123	117, 122	mpbid 210	. . . . . . . . 9 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( 1 / ( ( tan ` ( ( m x. pi ) / N ) ) ^ 2 ) ) < ( 1 / ( ( tan ` ( ( k x. pi ) / N ) ) ^ 2 ) ) )
124		oveq1 6087	. . . . . . . . . . . . . . 15 |- ( n = m -> ( n x. pi ) = ( m x. pi ) )
125	124	oveq1d 6095	. . . . . . . . . . . . . 14 |- ( n = m -> ( ( n x. pi ) / N ) = ( ( m x. pi ) / N ) )
126	125	fveq2d 5683	. . . . . . . . . . . . 13 |- ( n = m -> ( tan ` ( ( n x. pi ) / N ) ) = ( tan ` ( ( m x. pi ) / N ) ) )
127	126	oveq1d 6095	. . . . . . . . . . . 12 |- ( n = m -> ( ( tan ` ( ( n x. pi ) / N ) ) ^ -u 2 ) = ( ( tan ` ( ( m x. pi ) / N ) ) ^ -u 2 ) )
128		ovex 6105	. . . . . . . . . . . 12 |- ( ( tan ` ( ( m x. pi ) / N ) ) ^ -u 2 ) e. _V
129	127, 57, 128	fvmpt 5762	. . . . . . . . . . 11 |- ( m e. ( 1 ... M ) -> ( T ` m ) = ( ( tan ` ( ( m x. pi ) / N ) ) ^ -u 2 ) )
130	129	ad2antll 721	. . . . . . . . . 10 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( T ` m ) = ( ( tan ` ( ( m x. pi ) / N ) ) ^ -u 2 ) )
131	111	rpcnd 11017	. . . . . . . . . . 11 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( tan ` ( ( m x. pi ) / N ) ) e. CC )
132		2nn0 10584	. . . . . . . . . . 11 |- 2 e. NN0
133		expneg 11857	. . . . . . . . . . 11 |- ( ( ( tan ` ( ( m x. pi ) / N ) ) e. CC /\ 2 e. NN0 ) -> ( ( tan ` ( ( m x. pi ) / N ) ) ^ -u 2 ) = ( 1 / ( ( tan ` ( ( m x. pi ) / N ) ) ^ 2 ) ) )
134	131, 132, 133	sylancl 655	. . . . . . . . . 10 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( ( tan ` ( ( m x. pi ) / N ) ) ^ -u 2 ) = ( 1 / ( ( tan ` ( ( m x. pi ) / N ) ) ^ 2 ) ) )
135	130, 134	eqtrd 2465	. . . . . . . . 9 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( T ` m ) = ( 1 / ( ( tan ` ( ( m x. pi ) / N ) ) ^ 2 ) ) )
136		oveq1 6087	. . . . . . . . . . . . . . 15 |- ( n = k -> ( n x. pi ) = ( k x. pi ) )
137	136	oveq1d 6095	. . . . . . . . . . . . . 14 |- ( n = k -> ( ( n x. pi ) / N ) = ( ( k x. pi ) / N ) )
138	137	fveq2d 5683	. . . . . . . . . . . . 13 |- ( n = k -> ( tan ` ( ( n x. pi ) / N ) ) = ( tan ` ( ( k x. pi ) / N ) ) )
139	138	oveq1d 6095	. . . . . . . . . . . 12 |- ( n = k -> ( ( tan ` ( ( n x. pi ) / N ) ) ^ -u 2 ) = ( ( tan ` ( ( k x. pi ) / N ) ) ^ -u 2 ) )
140		ovex 6105	. . . . . . . . . . . 12 |- ( ( tan ` ( ( k x. pi ) / N ) ) ^ -u 2 ) e. _V
141	139, 57, 140	fvmpt 5762	. . . . . . . . . . 11 |- ( k e. ( 1 ... M ) -> ( T ` k ) = ( ( tan ` ( ( k x. pi ) / N ) ) ^ -u 2 ) )
142	141	ad2antrl 720	. . . . . . . . . 10 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( T ` k ) = ( ( tan ` ( ( k x. pi ) / N ) ) ^ -u 2 ) )
143	109	rpcnd 11017	. . . . . . . . . . 11 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( tan ` ( ( k x. pi ) / N ) ) e. CC )
144		expneg 11857	. . . . . . . . . . 11 |- ( ( ( tan ` ( ( k x. pi ) / N ) ) e. CC /\ 2 e. NN0 ) -> ( ( tan ` ( ( k x. pi ) / N ) ) ^ -u 2 ) = ( 1 / ( ( tan ` ( ( k x. pi ) / N ) ) ^ 2 ) ) )
145	143, 132, 144	sylancl 655	. . . . . . . . . 10 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( ( tan ` ( ( k x. pi ) / N ) ) ^ -u 2 ) = ( 1 / ( ( tan ` ( ( k x. pi ) / N ) ) ^ 2 ) ) )
146	142, 145	eqtrd 2465	. . . . . . . . 9 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( T ` k ) = ( 1 / ( ( tan ` ( ( k x. pi ) / N ) ) ^ 2 ) ) )
147	123, 135, 146	3brtr4d 4310	. . . . . . . 8 |- ( ( ( M e. NN /\ k < m ) /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( T ` m ) < ( T ` k ) )
148	147	an32s 795	. . . . . . 7 |- ( ( ( M e. NN /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) /\ k < m ) -> ( T ` m ) < ( T ` k ) )
149	148	ex 434	. . . . . 6 |- ( ( M e. NN /\ ( k e. ( 1 ... M ) /\ m e. ( 1 ... M ) ) ) -> ( k < m -> ( T ` m ) < ( T ` k ) ) )
150	59, 60, 61, 63, 66, 149	eqord2 9859	. . . . 5 |- ( ( M e. NN /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... M ) ) ) -> ( x = y <-> ( T ` x ) = ( T ` y ) ) )
151	150	biimprd 223	. . . 4 |- ( ( M e. NN /\ ( x e. ( 1 ... M ) /\ y e. ( 1 ... M ) ) ) -> ( ( T ` x ) = ( T ` y ) -> x = y ) )
152	151	ralrimivva 2798	. . 3 |- ( M e. NN -> A. x e. ( 1 ... M ) A. y e. ( 1 ... M ) ( ( T ` x ) = ( T ` y ) -> x = y ) )
153		dff13 5958	. . 3 |- ( T : ( 1 ... M ) -1-1-> ( `' P " { 0 } ) <-> ( T : ( 1 ... M ) --> ( `' P " { 0 } ) /\ A. x e. ( 1 ... M ) A. y e. ( 1 ... M ) ( ( T ` x ) = ( T ` y ) -> x = y ) ) )
154	58, 152, 153	sylanbrc 657	. 2 |- ( M e. NN -> T : ( 1 ... M ) -1-1-> ( `' P " { 0 } ) )
155	48	simp2d 994	. . . . . . . . 9 |- ( M e. NN -> (deg ` P ) = M )
156		nnne0 10342	. . . . . . . . 9 |- ( M e. NN -> M =/= 0 )
157	155, 156	eqnetrd 2616	. . . . . . . 8 |- ( M e. NN -> (deg ` P ) =/= 0 )
158		fveq2 5679	. . . . . . . . . 10 |- ( P = 0p -> (deg ` P ) = (deg ` 0p ) )
159		dgr0 21614	. . . . . . . . . 10 |- (deg ` 0p ) = 0
160	158, 159	syl6eq 2481	. . . . . . . . 9 |- ( P = 0p -> (deg ` P ) = 0 )
161	160	necon3i 2640	. . . . . . . 8 |- ( (deg ` P ) =/= 0 -> P =/= 0p )
162	157, 161	syl 16	. . . . . . 7 |- ( M e. NN -> P =/= 0p )
163		eqid 2433	. . . . . . . 8 |- ( `' P " { 0 } ) = ( `' P " { 0 } )
164	163	fta1 21659	. . . . . . 7 |- ( ( P e. (Poly ` CC ) /\ P =/= 0p ) -> ( ( `' P " { 0 } ) e. Fin /\ ( # ` ( `' P " { 0 } ) ) <_ (deg ` P ) ) )
165	49, 162, 164	syl2anc 654	. . . . . 6 |- ( M e. NN -> ( ( `' P " { 0 } ) e. Fin /\ ( # ` ( `' P " { 0 } ) ) <_ (deg ` P ) ) )
166	165	simpld 456	. . . . 5 |- ( M e. NN -> ( `' P " { 0 } ) e. Fin )
167		f1domg 7317	. . . . 5 |- ( ( `' P " { 0 } ) e. Fin -> ( T : ( 1 ... M ) -1-1-> ( `' P " { 0 } ) -> ( 1 ... M ) ~<_ ( `' P " { 0 } ) ) )
168	166, 154, 167	sylc 60	. . . 4 |- ( M e. NN -> ( 1 ... M ) ~<_ ( `' P " { 0 } ) )
169	165	simprd 460	. . . . . 6 |- ( M e. NN -> ( # ` ( `' P " { 0 } ) ) <_ (deg ` P ) )
170		nnnn0 10574	. . . . . . . 8 |- ( M e. NN -> M e. NN0 )
171		hashfz1 12101	. . . . . . . 8 |- ( M e. NN0 -> ( # ` ( 1 ... M ) ) = M )
172	170, 171	syl 16	. . . . . . 7 |- ( M e. NN -> ( # ` ( 1 ... M ) ) = M )
173	155, 172	eqtr4d 2468	. . . . . 6 |- ( M e. NN -> (deg ` P ) = ( # ` ( 1 ... M ) ) )
174	169, 173	breqtrd 4304	. . . . 5 |- ( M e. NN -> ( # ` ( `' P " { 0 } ) ) <_ ( # ` ( 1 ... M ) ) )
175		fzfid 11779	. . . . . 6 |- ( M e. NN -> ( 1 ... M ) e. Fin )
176		hashdom 12126	. . . . . 6 |- ( ( ( `' P " { 0 } ) e. Fin /\ ( 1 ... M ) e. Fin ) -> ( ( # ` ( `' P " { 0 } ) ) <_ ( # ` ( 1 ... M ) ) <-> ( `' P " { 0 } ) ~<_ ( 1 ... M ) ) )
177	166, 175, 176	syl2anc 654	. . . . 5 |- ( M e. NN -> ( ( # ` ( `' P " { 0 } ) ) <_ ( # ` ( 1 ... M ) ) <-> ( `' P " { 0 } ) ~<_ ( 1 ... M ) ) )
178	174, 177	mpbid 210	. . . 4 |- ( M e. NN -> ( `' P " { 0 } ) ~<_ ( 1 ... M ) )
179		sbth 7419	. . . 4 |- ( ( ( 1 ... M ) ~<_ ( `' P " { 0 } ) /\ ( `' P " { 0 } ) ~<_ ( 1 ... M ) ) -> ( 1 ... M ) ~~ ( `' P " { 0 } ) )
180	168, 178, 179	syl2anc 654	. . 3 |- ( M e. NN -> ( 1 ... M ) ~~ ( `' P " { 0 } ) )
181		f1finf1o 7527	. . 3 |- ( ( ( 1 ... M ) ~~ ( `' P " { 0 } ) /\ ( `' P " { 0 } ) e. Fin ) -> ( T : ( 1 ... M ) -1-1-> ( `' P " { 0 } ) <-> T : ( 1 ... M ) -1-1-onto-> ( `' P " { 0 } ) ) )
182	180, 166, 181	syl2anc 654	. 2 |- ( M e. NN -> ( T : ( 1 ... M ) -1-1-> ( `' P " { 0 } ) <-> T : ( 1 ... M ) -1-1-onto-> ( `' P " { 0 } ) ) )
183	154, 182	mpbid 210	1 |- ( M e. NN -> T : ( 1 ... M ) -1-1-onto-> ( `' P " { 0 } ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1362   e. wcel 1755   =/= wne 2596   A.wral 2705   C_ wss 3316   {csn 3865   class class class wbr 4280   e. cmpt 4338   `'ccnv 4826   "cima 4830   Fn wfn 5401   -->wf 5402   -1-1->wf1 5403   -1-1-onto->wf1o 5405   ` cfv 5406  (class class class)co 6080   ~~ cen 7295   ~<_ cdom 7296   Fincfn 7298   CCcc 9268   RRcr 9269   0cc0 9270   1c1 9271   + caddc 9273   x. cmul 9275   RR*cxr 9405   < clt 9406   <_ cle 9407   - cmin 9583   -ucneg 9584   / cdiv 9981   NNcn 10310   2c2 10359   NN0cn0 10567   ZZcz 10634   RR+crp 10979   (,)cioo 11288   ...cfz 11424   ^cexp 11849   _C cbc 12062   #chash 12087   sum_csu 13147   sincsin 13332   cosccos 13333   tanctan 13334   picpi 13335   0pc0p 20989  Polycply 21537  coeffccoe 21539  degcdgr 21540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-rep 4391  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-inf2 7835  ax-cnex 9326  ax-resscn 9327  ax-1cn 9328  ax-icn 9329  ax-addcl 9330  ax-addrcl 9331  ax-mulcl 9332  ax-mulrcl 9333  ax-mulcom 9334  ax-addass 9335  ax-mulass 9336  ax-distr 9337  ax-i2m1 9338  ax-1ne0 9339  ax-1rid 9340  ax-rnegex 9341  ax-rrecex 9342  ax-cnre 9343  ax-pre-lttri 9344  ax-pre-lttrn 9345  ax-pre-ltadd 9346  ax-pre-mulgt0 9347  ax-pre-sup 9348  ax-addf 9349  ax-mulf 9350

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-fal 1368  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-nel 2599  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-int 4117  df-iun 4161  df-iin 4162  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-se 4667  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-isom 5415  df-riota 6039  df-ov 6083  df-oprab 6084  df-mpt2 6085  df-of 6309  df-om 6466  df-1st 6566  df-2nd 6567  df-supp 6680  df-recs 6818  df-rdg 6852  df-1o 6908  df-2o 6909  df-oadd 6912  df-er 7089  df-map 7204  df-pm 7205  df-ixp 7252  df-en 7299  df-dom 7300  df-sdom 7301  df-fin 7302  df-fsupp 7609  df-fi 7649  df-sup 7679  df-oi 7712  df-card 8097  df-cda 8325  df-pnf 9408  df-mnf 9409  df-xr 9410  df-ltxr 9411  df-le 9412  df-sub 9585  df-neg 9586  df-div 9982  df-nn 10311  df-2 10368  df-3 10369  df-4 10370  df-5 10371  df-6 10372  df-7 10373  df-8 10374  df-9 10375  df-10 10376  df-n0 10568  df-z 10635  df-dec 10744  df-uz 10850  df-q 10942  df-rp 10980  df-xneg 11077  df-xadd 11078  df-xmul 11079  df-ioo 11292  df-ioc 11293  df-ico 11294  df-icc 11295  df-fz 11425  df-fzo 11533  df-fl 11626  df-mod 11693  df-seq 11791  df-exp 11850  df-fac 12036  df-bc 12063  df-hash 12088  df-shft 12540  df-cj 12572  df-re 12573  df-im 12574  df-sqr 12708  df-abs 12709  df-limsup 12933  df-clim 12950  df-rlim 12951  df-sum 13148  df-ef 13336  df-sin 13338  df-cos 13339  df-tan 13340  df-pi 13341  df-struct 14159  df-ndx 14160  df-slot 14161  df-base 14162  df-sets 14163  df-ress 14164  df-plusg 14234  df-mulr 14235  df-starv 14236  df-sca 14237  df-vsca 14238  df-ip 14239  df-tset 14240  df-ple 14241  df-ds 14243  df-unif 14244  df-hom 14245  df-cco 14246  df-rest 14344  df-topn 14345  df-0g 14363  df-gsum 14364  df-topgen 14365  df-pt 14366  df-prds 14369  df-xrs 14423  df-qtop 14428  df-imas 14429  df-xps 14431  df-mre 14507  df-mrc 14508  df-acs 14510  df-mnd 15398  df-submnd 15448  df-mulg 15528  df-cntz 15815  df-cmn 16259  df-psmet 17653  df-xmet 17654  df-met 17655  df-bl 17656  df-mopn 17657  df-fbas 17658  df-fg 17659  df-cnfld 17663  df-top 18345  df-bases 18347  df-topon 18348  df-topsp 18349  df-cld 18465  df-ntr 18466  df-cls 18467  df-nei 18544  df-lp 18582  df-perf 18583  df-cn 18673  df-cnp 18674  df-haus 18761  df-tx 18977  df-hmeo 19170  df-fil 19261  df-fm 19353  df-flim 19354  df-flf 19355  df-xms 19737  df-ms 19738  df-tms 19739  df-cncf 20296  df-0p 20990  df-limc 21183  df-dv 21184  df-ply 21541  df-idp 21542  df-coe 21543  df-dgr 21544  df-quot 21642

This theorem is referenced by:  basellem5  22307