Metamath Proof Explorer

Theorem mzpconst

Description: Constant functions are polynomial. See also mzpconstmpt . (Contributed by Stefan O'Rear, 4-Oct-2014)

Ref Expression
Assertion mzpconst 
|- ( ( V e. _V /\ C e. ZZ ) -> ( ( ZZ ^m V ) X. { C } ) e. ( mzPoly ` V ) )

Proof

Step Hyp Ref Expression
1 mzpincl 
 |-  ( V e. _V -> ( mzPoly ` V ) e. ( mzPolyCld ` V ) )
2 mzpcl1 
 |-  ( ( ( mzPoly ` V ) e. ( mzPolyCld ` V ) /\ C e. ZZ ) -> ( ( ZZ ^m V ) X. { C } ) e. ( mzPoly ` V ) )
3 1 2 sylan 
 |-  ( ( V e. _V /\ C e. ZZ ) -> ( ( ZZ ^m V ) X. { C } ) e. ( mzPoly ` V ) )