Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  deg1tmle Structured version   Unicode version

Theorem deg1tmle 22810
 Description: Limiting degree of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.)
Hypotheses
Ref Expression
deg1tm.d deg1
deg1tm.k
deg1tm.p Poly1
deg1tm.x var1
deg1tm.m
deg1tm.n mulGrp
deg1tm.e .g
Assertion
Ref Expression
deg1tmle

Proof of Theorem deg1tmle
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eqid 2402 . . . . 5
2 deg1tm.k . . . . 5
3 deg1tm.p . . . . 5 Poly1
4 deg1tm.x . . . . 5 var1
5 deg1tm.m . . . . 5
6 deg1tm.n . . . . 5 mulGrp
7 deg1tm.e . . . . 5 .g
8 simpl1 1000 . . . . 5
9 simpl2 1001 . . . . 5
10 simpl3 1002 . . . . 5
11 simprl 756 . . . . 5
1210nn0red 10894 . . . . . 6
13 simprr 758 . . . . . 6
1412, 13ltned 9753 . . . . 5
151, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 14coe1tmfv2 18636 . . . 4 coe1
1615expr 613 . . 3 coe1
1716ralrimiva 2818 . 2 coe1
18 eqid 2402 . . . 4
192, 3, 4, 5, 6, 7, 18ply1tmcl 18633 . . 3
20 nn0re 10845 . . . . 5
2120rexrd 9673 . . . 4