dgreq0 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dgreq0		Structured version Visualization version GIF version

Theorem dgreq0 24229

Description: The leading coefficient of a polynomial is nonzero, unless the entire polynomial is zero. (Contributed by Mario Carneiro, 22-Jul-2014.) (Proof shortened by Fan Zheng, 21-Jun-2016.)

**Hypotheses**
Ref	Expression
dgreq0.1	⊢ 𝑁 = (deg‘𝐹)
dgreq0.2	⊢ 𝐴 = (coeff‘𝐹)

**Assertion**
Ref	Expression
dgreq0	⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0_𝑝 ↔ (𝐴‘𝑁) = 0))

Proof of Theorem dgreq0 Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dgreq0.2	. . . . . 6 ⊢ 𝐴 = (coeff‘𝐹)
2		fveq2 6402	. . . . . 6 ⊢ (𝐹 = 0_𝑝 → (coeff‘𝐹) = (coeff‘0_𝑝))
3	1, 2	syl5eq 2848	. . . . 5 ⊢ (𝐹 = 0_𝑝 → 𝐴 = (coeff‘0_𝑝))
4		coe0 24220	. . . . 5 ⊢ (coeff‘0_𝑝) = (ℕ₀ × {0})
5	3, 4	syl6eq 2852	. . . 4 ⊢ (𝐹 = 0_𝑝 → 𝐴 = (ℕ₀ × {0}))
6		dgreq0.1	. . . . . 6 ⊢ 𝑁 = (deg‘𝐹)
7		fveq2 6402	. . . . . 6 ⊢ (𝐹 = 0_𝑝 → (deg‘𝐹) = (deg‘0_𝑝))
8	6, 7	syl5eq 2848	. . . . 5 ⊢ (𝐹 = 0_𝑝 → 𝑁 = (deg‘0_𝑝))
9		dgr0 24226	. . . . 5 ⊢ (deg‘0_𝑝) = 0
10	8, 9	syl6eq 2852	. . . 4 ⊢ (𝐹 = 0_𝑝 → 𝑁 = 0)
11	5, 10	fveq12d 6409	. . 3 ⊢ (𝐹 = 0_𝑝 → (𝐴‘𝑁) = ((ℕ₀ × {0})‘0))
12		0nn0 11568	. . . 4 ⊢ 0 ∈ ℕ₀
13		fvconst2g 6686	. . . 4 ⊢ ((0 ∈ ℕ₀ ∧ 0 ∈ ℕ₀) → ((ℕ₀ × {0})‘0) = 0)
14	12, 12, 13	mp2an 675	. . 3 ⊢ ((ℕ₀ × {0})‘0) = 0
15	11, 14	syl6eq 2852	. 2 ⊢ (𝐹 = 0_𝑝 → (𝐴‘𝑁) = 0)
16	1	coefv0 24212	. . . . . . . 8 ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹‘0) = (𝐴‘0))
17	16	adantr 468	. . . . . . 7 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → (𝐹‘0) = (𝐴‘0))
18		simpr 473	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℕ)
19	18	nnred 11314	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℝ)
20	19	ltm1d 11235	. . . . . . . . . 10 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → (𝑁 − 1) < 𝑁)
21		simpll 774	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → 𝐹 ∈ (Poly‘𝑆))
22		nnm1nn0 11594	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
23	22	adantl 469	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → (𝑁 − 1) ∈ ℕ₀)
24	1, 6	dgrub 24198	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑘 ∈ ℕ₀ ∧ (𝐴‘𝑘) ≠ 0) → 𝑘 ≤ 𝑁)
25	24	3expia 1143	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑘 ∈ ℕ₀) → ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁))
26	25	ad2ant2rl 746	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ₀)) → ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ 𝑁))
27		simplr 776	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ₀)) → (𝐴‘𝑁) = 0)
28		fveqeq2 6411	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 = 𝑘 → ((𝐴‘𝑁) = 0 ↔ (𝐴‘𝑘) = 0))
29	27, 28	syl5ibcom 236	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ₀)) → (𝑁 = 𝑘 → (𝐴‘𝑘) = 0))
30	29	necon3d 2995	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ₀)) → ((𝐴‘𝑘) ≠ 0 → 𝑁 ≠ 𝑘))
31	26, 30	jcad 504	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ₀)) → ((𝐴‘𝑘) ≠ 0 → (𝑘 ≤ 𝑁 ∧ 𝑁 ≠ 𝑘)))
32		nn0re 11562	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℕ₀ → 𝑘 ∈ ℝ)
33	32	ad2antll 711	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ₀)) → 𝑘 ∈ ℝ)
34		nnre 11306	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
35	34	ad2antrl 710	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ₀)) → 𝑁 ∈ ℝ)
36	33, 35	ltlend 10461	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ₀)) → (𝑘 < 𝑁 ↔ (𝑘 ≤ 𝑁 ∧ 𝑁 ≠ 𝑘)))
37		nn0z 11660	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℕ₀ → 𝑘 ∈ ℤ)
38	37	ad2antll 711	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ₀)) → 𝑘 ∈ ℤ)
39		nnz 11659	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
40	39	ad2antrl 710	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ₀)) → 𝑁 ∈ ℤ)
41		zltlem1 11690	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 < 𝑁 ↔ 𝑘 ≤ (𝑁 − 1)))
42	38, 40, 41	syl2anc 575	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ₀)) → (𝑘 < 𝑁 ↔ 𝑘 ≤ (𝑁 − 1)))
43	36, 42	bitr3d 272	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ₀)) → ((𝑘 ≤ 𝑁 ∧ 𝑁 ≠ 𝑘) ↔ 𝑘 ≤ (𝑁 − 1)))
44	31, 43	sylibd 230	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ (𝑁 ∈ ℕ ∧ 𝑘 ∈ ℕ₀)) → ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ (𝑁 − 1)))
45	44	expr 446	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → (𝑘 ∈ ℕ₀ → ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ (𝑁 − 1))))
46	45	ralrimiv 3149	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → ∀𝑘 ∈ ℕ₀ ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ (𝑁 − 1)))
47	1	coef3 24196	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ₀⟶ℂ)
48	47	ad2antrr 708	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → 𝐴:ℕ₀⟶ℂ)
49		plyco0 24156	. . . . . . . . . . . . . 14 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ 𝐴:ℕ₀⟶ℂ) → ((𝐴 “ (ℤ_≥‘((𝑁 − 1) + 1))) = {0} ↔ ∀𝑘 ∈ ℕ₀ ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ (𝑁 − 1))))
50	23, 48, 49	syl2anc 575	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → ((𝐴 “ (ℤ_≥‘((𝑁 − 1) + 1))) = {0} ↔ ∀𝑘 ∈ ℕ₀ ((𝐴‘𝑘) ≠ 0 → 𝑘 ≤ (𝑁 − 1))))
51	46, 50	mpbird 248	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → (𝐴 “ (ℤ_≥‘((𝑁 − 1) + 1))) = {0})
52	1, 6	dgrlb 24200	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝑁 − 1) ∈ ℕ₀ ∧ (𝐴 “ (ℤ_≥‘((𝑁 − 1) + 1))) = {0}) → 𝑁 ≤ (𝑁 − 1))
53	21, 23, 51, 52	syl3anc 1483	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → 𝑁 ≤ (𝑁 − 1))
54	34	adantl 469	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℝ)
55		peano2rem 10627	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ)
56	54, 55	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → (𝑁 − 1) ∈ ℝ)
57	54, 56	lenltd 10462	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → (𝑁 ≤ (𝑁 − 1) ↔ ¬ (𝑁 − 1) < 𝑁))
58	53, 57	mpbid 223	. . . . . . . . . 10 ⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) ∧ 𝑁 ∈ ℕ) → ¬ (𝑁 − 1) < 𝑁)
59	20, 58	pm2.65da 842	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → ¬ 𝑁 ∈ ℕ)
60		dgrcl 24197	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈ ℕ₀)
61	6, 60	syl5eqel 2885	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (Poly‘𝑆) → 𝑁 ∈ ℕ₀)
62	61	adantr 468	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → 𝑁 ∈ ℕ₀)
63		elnn0 11555	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ₀ ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
64	62, 63	sylib 209	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → (𝑁 ∈ ℕ ∨ 𝑁 = 0))
65	64	ord 882	. . . . . . . . 9 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → (¬ 𝑁 ∈ ℕ → 𝑁 = 0))
66	59, 65	mpd 15	. . . . . . . 8 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → 𝑁 = 0)
67	66	fveq2d 6406	. . . . . . 7 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → (𝐴‘𝑁) = (𝐴‘0))
68		simpr 473	. . . . . . 7 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → (𝐴‘𝑁) = 0)
69	17, 67, 68	3eqtr2d 2842	. . . . . 6 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → (𝐹‘0) = 0)
70	69	sneqd 4376	. . . . 5 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → {(𝐹‘0)} = {0})
71	70	xpeq2d 5334	. . . 4 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → (ℂ × {(𝐹‘0)}) = (ℂ × {0}))
72	6, 66	syl5eqr 2850	. . . . 5 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → (deg‘𝐹) = 0)
73		0dgrb 24210	. . . . . 6 ⊢ (𝐹 ∈ (Poly‘𝑆) → ((deg‘𝐹) = 0 ↔ 𝐹 = (ℂ × {(𝐹‘0)})))
74	73	adantr 468	. . . . 5 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → ((deg‘𝐹) = 0 ↔ 𝐹 = (ℂ × {(𝐹‘0)})))
75	72, 74	mpbid 223	. . . 4 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → 𝐹 = (ℂ × {(𝐹‘0)}))
76		df-0p 23645	. . . . 5 ⊢ 0_𝑝 = (ℂ × {0})
77	76	a1i 11	. . . 4 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → 0_𝑝 = (ℂ × {0}))
78	71, 75, 77	3eqtr4d 2846	. . 3 ⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝐴‘𝑁) = 0) → 𝐹 = 0_𝑝)
79	78	ex 399	. 2 ⊢ (𝐹 ∈ (Poly‘𝑆) → ((𝐴‘𝑁) = 0 → 𝐹 = 0_𝑝))
80	15, 79	impbid2 217	1 ⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0_𝑝 ↔ (𝐴‘𝑁) = 0))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 197 ∧ wa 384 ∨ wo 865 = wceq 1637 ∈ wcel 2155 ≠ wne 2974 ∀wral 3092 {csn 4364 class class class wbr 4837 × cxp 5303 “ cima 5308 ⟶wf 6091 ‘cfv 6095 (class class class)co 6868 ℂcc 10213 ℝcr 10214 0cc0 10215 1c1 10216 + caddc 10218 < clt 10353 ≤ cle 10354 − cmin 10545 ℕcn 11299 ℕ₀cn0 11553 ℤcz 11637 ℤ_≥cuz 11898 0_𝑝c0p 23644 Polycply 24148 coeffccoe 24150 degcdgr 24151

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1877 ax-4 1894 ax-5 2001 ax-6 2067 ax-7 2103 ax-8 2157 ax-9 2164 ax-10 2184 ax-11 2200 ax-12 2213 ax-13 2419 ax-ext 2781 ax-rep 4957 ax-sep 4968 ax-nul 4977 ax-pow 5029 ax-pr 5090 ax-un 7173 ax-inf2 8779 ax-cnex 10271 ax-resscn 10272 ax-1cn 10273 ax-icn 10274 ax-addcl 10275 ax-addrcl 10276 ax-mulcl 10277 ax-mulrcl 10278 ax-mulcom 10279 ax-addass 10280 ax-mulass 10281 ax-distr 10282 ax-i2m1 10283 ax-1ne0 10284 ax-1rid 10285 ax-rnegex 10286 ax-rrecex 10287 ax-cnre 10288 ax-pre-lttri 10289 ax-pre-lttrn 10290 ax-pre-ltadd 10291 ax-pre-mulgt0 10292 ax-pre-sup 10293 ax-addf 10294

This theorem depends on definitions: df-bi 198 df-an 385 df-or 866 df-3or 1101 df-3an 1102 df-tru 1641 df-fal 1651 df-ex 1860 df-nf 1864 df-sb 2060 df-eu 2633 df-mo 2634 df-clab 2789 df-cleq 2795 df-clel 2798 df-nfc 2933 df-ne 2975 df-nel 3078 df-ral 3097 df-rex 3098 df-reu 3099 df-rmo 3100 df-rab 3101 df-v 3389 df-sbc 3628 df-csb 3723 df-dif 3766 df-un 3768 df-in 3770 df-ss 3777 df-pss 3779 df-nul 4111 df-if 4274 df-pw 4347 df-sn 4365 df-pr 4367 df-tp 4369 df-op 4371 df-uni 4624 df-int 4663 df-iun 4707 df-br 4838 df-opab 4900 df-mpt 4917 df-tr 4940 df-id 5213 df-eprel 5218 df-po 5226 df-so 5227 df-fr 5264 df-se 5265 df-we 5266 df-xp 5311 df-rel 5312 df-cnv 5313 df-co 5314 df-dm 5315 df-rn 5316 df-res 5317 df-ima 5318 df-pred 5887 df-ord 5933 df-on 5934 df-lim 5935 df-suc 5936 df-iota 6058 df-fun 6097 df-fn 6098 df-f 6099 df-f1 6100 df-fo 6101 df-f1o 6102 df-fv 6103 df-isom 6104 df-riota 6829 df-ov 6871 df-oprab 6872 df-mpt2 6873 df-of 7121 df-om 7290 df-1st 7392 df-2nd 7393 df-wrecs 7636 df-recs 7698 df-rdg 7736 df-1o 7790 df-oadd 7794 df-er 7973 df-map 8088 df-pm 8089 df-en 8187 df-dom 8188 df-sdom 8189 df-fin 8190 df-sup 8581 df-inf 8582 df-oi 8648 df-card 9042 df-pnf 10355 df-mnf 10356 df-xr 10357 df-ltxr 10358 df-le 10359 df-sub 10547 df-neg 10548 df-div 10964 df-nn 11300 df-2 11358 df-3 11359 df-n0 11554 df-z 11638 df-uz 11899 df-rp 12041 df-fz 12544 df-fzo 12684 df-fl 12811 df-seq 13019 df-exp 13078 df-hash 13332 df-cj 14056 df-re 14057 df-im 14058 df-sqrt 14192 df-abs 14193 df-clim 14436 df-rlim 14437 df-sum 14634 df-0p 23645 df-ply 24152 df-coe 24154 df-dgr 24155

This theorem is referenced by: dgrlt 24230 dgradd2 24232 dgrmul 24234 dgrcolem2 24238 plymul0or 24244 plydivlem4 24259 plydiveu 24261 vieta1lem2 24274 vieta1 24275 aareccl 24289 ftalem2 25008 ftalem4 25010 ftalem5 25011 signsply0 30947 mpaaeu 38215 elaa2lem 40923

W3C validator