deg1tmle

Description: Limiting degree of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015)

	Ref	Expression
Hypotheses	deg1tm.d	$⊢ D = \deg_{1} (R)$
	deg1tm.k	$⊢ K = {Base}_{R}$
	deg1tm.p	$⊢ P = {Poly}_{1} (R)$
	deg1tm.x	$⊢ X = {var}_{1} (R)$
	deg1tm.m	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	deg1tm.n	$⊢ N = {mulGrp}_{P}$
	deg1tm.e	$⊢ \underset{˙}{\times} = \cdot_{N}$
Assertion	deg1tmle	$⊢ (R \in Ring \land C \in K \land F \in ℕ_{0}) \to D (C \underset{˙}{\cdot} (F \underset{˙}{\times} X)) \leq F$

Proof

Step	Hyp	Ref	Expression
1		deg1tm.d	$⊢ D = \deg_{1} (R)$
2		deg1tm.k	$⊢ K = {Base}_{R}$
3		deg1tm.p	$⊢ P = {Poly}_{1} (R)$
4		deg1tm.x	$⊢ X = {var}_{1} (R)$
5		deg1tm.m	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
6		deg1tm.n	$⊢ N = {mulGrp}_{P}$
7		deg1tm.e	$⊢ \underset{˙}{\times} = \cdot_{N}$
8		eqid	$⊢ 0_{R} = 0_{R}$
9		simpl1	$⊢ ((R \in Ring \land C \in K \land F \in ℕ_{0}) \land (x \in ℕ_{0} \land F < x)) \to R \in Ring$
10		simpl2	$⊢ ((R \in Ring \land C \in K \land F \in ℕ_{0}) \land (x \in ℕ_{0} \land F < x)) \to C \in K$
11		simpl3	$⊢ ((R \in Ring \land C \in K \land F \in ℕ_{0}) \land (x \in ℕ_{0} \land F < x)) \to F \in ℕ_{0}$
12		simprl	$⊢ ((R \in Ring \land C \in K \land F \in ℕ_{0}) \land (x \in ℕ_{0} \land F < x)) \to x \in ℕ_{0}$
13	11	nn0red	$⊢ ((R \in Ring \land C \in K \land F \in ℕ_{0}) \land (x \in ℕ_{0} \land F < x)) \to F \in ℝ$
14		simprr	$⊢ ((R \in Ring \land C \in K \land F \in ℕ_{0}) \land (x \in ℕ_{0} \land F < x)) \to F < x$
15	13 14	ltned	$⊢ ((R \in Ring \land C \in K \land F \in ℕ_{0}) \land (x \in ℕ_{0} \land F < x)) \to F \neq x$
16	8 2 3 4 5 6 7 9 10 11 12 15	coe1tmfv2	$⊢ ((R \in Ring \land C \in K \land F \in ℕ_{0}) \land (x \in ℕ_{0} \land F < x)) \to {coe}_{1} (C \underset{˙}{\cdot} (F \underset{˙}{\times} X)) (x) = 0_{R}$
17	16	expr	$⊢ ((R \in Ring \land C \in K \land F \in ℕ_{0}) \land x \in ℕ_{0}) \to (F < x \to {coe}_{1} (C \underset{˙}{\cdot} (F \underset{˙}{\times} X)) (x) = 0_{R})$
18	17	ralrimiva	$⊢ (R \in Ring \land C \in K \land F \in ℕ_{0}) \to \forall x \in ℕ_{0} (F < x \to {coe}_{1} (C \underset{˙}{\cdot} (F \underset{˙}{\times} X)) (x) = 0_{R})$
19		eqid	$⊢ {Base}_{P} = {Base}_{P}$
20	2 3 4 5 6 7 19	ply1tmcl	$⊢ (R \in Ring \land C \in K \land F \in ℕ_{0}) \to C \underset{˙}{\cdot} (F \underset{˙}{\times} X) \in {Base}_{P}$
21		nn0re	$⊢ F \in ℕ_{0} \to F \in ℝ$
22	21	rexrd	$⊢ F \in ℕ_{0} \to F \in ℝ^{*}$
23	22	3ad2ant3	$⊢ (R \in Ring \land C \in K \land F \in ℕ_{0}) \to F \in ℝ^{*}$
24		eqid	$⊢ {coe}_{1} (C \underset{˙}{\cdot} (F \underset{˙}{\times} X)) = {coe}_{1} (C \underset{˙}{\cdot} (F \underset{˙}{\times} X))$
25	1 3 19 8 24	deg1leb	$⊢ (C \underset{˙}{\cdot} (F \underset{˙}{\times} X) \in {Base}_{P} \land F \in ℝ^{*}) \to (D (C \underset{˙}{\cdot} (F \underset{˙}{\times} X)) \leq F \leftrightarrow \forall x \in ℕ_{0} (F < x \to {coe}_{1} (C \underset{˙}{\cdot} (F \underset{˙}{\times} X)) (x) = 0_{R}))$
26	20 23 25	syl2anc	$⊢ (R \in Ring \land C \in K \land F \in ℕ_{0}) \to (D (C \underset{˙}{\cdot} (F \underset{˙}{\times} X)) \leq F \leftrightarrow \forall x \in ℕ_{0} (F < x \to {coe}_{1} (C \underset{˙}{\cdot} (F \underset{˙}{\times} X)) (x) = 0_{R}))$
27	18 26	mpbird	$⊢ (R \in Ring \land C \in K \land F \in ℕ_{0}) \to D (C \underset{˙}{\cdot} (F \underset{˙}{\times} X)) \leq F$

Metamath Proof Explorer

Theorem deg1tmle

Proof