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 ... 𝑁 ) × { 0 } ) : ( 3 ... 𝑁 ) ⟶ ℝ

Proof

Step	Hyp	Ref	Expression
1		0re	⊢ 0 ∈ ℝ
2	1	fconst6	⊢ ( ( 3 ... 𝑁 ) × { 0 } ) : ( 3 ... 𝑁 ) ⟶ ℝ