Metamath Proof Explorer

Theorem axlowdimlem5

Description: Lemma for axlowdim . Show that a particular union is a point in Euclidean space. (Contributed by Scott Fenton, 29-Jun-2013)

		Ref	Expression
	Hypotheses	axlowdimlem4.1	$⊢ A \in ℝ$
		axlowdimlem4.2	$⊢ B \in ℝ$
	Assertion	axlowdimlem5	$⊢ N \in ℤ_{\geq 2} \to \{⟨1, A⟩, ⟨2, B⟩\} \cup ((3 \dots N) \times \{0\}) \in 𝔼 (N)$

Proof

Step	Hyp	Ref	Expression
1		axlowdimlem4.1	$⊢ A \in ℝ$
2		axlowdimlem4.2	$⊢ B \in ℝ$
3	1 2	axlowdimlem4	$⊢ \{⟨1, A⟩, ⟨2, B⟩\} : (1 \dots 2) ⟶ ℝ$
4		axlowdimlem1	$⊢ ((3 \dots N) \times \{0\}) : (3 \dots N) ⟶ ℝ$
5	3 4	pm3.2i	$⊢ (\{⟨1, A⟩, ⟨2, B⟩\} : (1 \dots 2) ⟶ ℝ \land ((3 \dots N) \times \{0\}) : (3 \dots N) ⟶ ℝ)$
6		axlowdimlem2	$⊢ (1 \dots 2) \cap (3 \dots N) = \emptyset$
7		fun2	$⊢ ((\{⟨1, A⟩, ⟨2, B⟩\} : (1 \dots 2) ⟶ ℝ \land ((3 \dots N) \times \{0\}) : (3 \dots N) ⟶ ℝ) \land (1 \dots 2) \cap (3 \dots N) = \emptyset) \to (\{⟨1, A⟩, ⟨2, B⟩\} \cup ((3 \dots N) \times \{0\})) : (1 \dots 2) \cup (3 \dots N) ⟶ ℝ$
8	5 6 7	mp2an	$⊢ (\{⟨1, A⟩, ⟨2, B⟩\} \cup ((3 \dots N) \times \{0\})) : (1 \dots 2) \cup (3 \dots N) ⟶ ℝ$
9		axlowdimlem3	$⊢ N \in ℤ_{\geq 2} \to (1 \dots N) = (1 \dots 2) \cup (3 \dots N)$
10	9	feq2d	$⊢ N \in ℤ_{\geq 2} \to ((\{⟨1, A⟩, ⟨2, B⟩\} \cup ((3 \dots N) \times \{0\})) : (1 \dots N) ⟶ ℝ \leftrightarrow (\{⟨1, A⟩, ⟨2, B⟩\} \cup ((3 \dots N) \times \{0\})) : (1 \dots 2) \cup (3 \dots N) ⟶ ℝ)$
11	8 10	mpbiri	$⊢ N \in ℤ_{\geq 2} \to (\{⟨1, A⟩, ⟨2, B⟩\} \cup ((3 \dots N) \times \{0\})) : (1 \dots N) ⟶ ℝ$
12		eluz2nn	$⊢ N \in ℤ_{\geq 2} \to N \in ℕ$
13		elee	$⊢ N \in ℕ \to (\{⟨1, A⟩, ⟨2, B⟩\} \cup ((3 \dots N) \times \{0\}) \in 𝔼 (N) \leftrightarrow (\{⟨1, A⟩, ⟨2, B⟩\} \cup ((3 \dots N) \times \{0\})) : (1 \dots N) ⟶ ℝ)$
14	12 13	syl	$⊢ N \in ℤ_{\geq 2} \to (\{⟨1, A⟩, ⟨2, B⟩\} \cup ((3 \dots N) \times \{0\}) \in 𝔼 (N) \leftrightarrow (\{⟨1, A⟩, ⟨2, B⟩\} \cup ((3 \dots N) \times \{0\})) : (1 \dots N) ⟶ ℝ)$
15	11 14	mpbird	$⊢ N \in ℤ_{\geq 2} \to \{⟨1, A⟩, ⟨2, B⟩\} \cup ((3 \dots N) \times \{0\}) \in 𝔼 (N)$