Metamath Proof Explorer

Theorem axlowdimlem1

Description: Lemma for axlowdim . Establish a particular constant function as a function. (Contributed by Scott Fenton, 29-Jun-2013)

Ref Expression
Assertion axlowdimlem1 
|- ( ( 3 ... N ) X. { 0 } ) : ( 3 ... N ) --> RR

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 1 fconst6 
 |-  ( ( 3 ... N ) X. { 0 } ) : ( 3 ... N ) --> RR