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	$$⊢\left(\left(3\dots N\right)\times \left\{0\right\}\right):\left(3\dots N\right)⟶ℝ$$

Proof

Step	Hyp	Ref	Expression
1		0re	$$⊢0\in ℝ$$
2	1	fconst6	$$⊢\left(\left(3\dots N\right)\times \left\{0\right\}\right):\left(3\dots N\right)⟶ℝ$$