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	⊢ 𝐴 ∈ ℝ
	axlowdimlem4.2	⊢ 𝐵 ∈ ℝ
Assertion	axlowdimlem5	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ∈ ( 𝔼 ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		axlowdimlem4.1	⊢ 𝐴 ∈ ℝ
2		axlowdimlem4.2	⊢ 𝐵 ∈ ℝ
3	1 2	axlowdimlem4	⊢ { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } : ( 1 ... 2 ) ⟶ ℝ
4		axlowdimlem1	⊢ ( ( 3 ... 𝑁 ) × { 0 } ) : ( 3 ... 𝑁 ) ⟶ ℝ
5	3 4	pm3.2i	⊢ ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } : ( 1 ... 2 ) ⟶ ℝ ∧ ( ( 3 ... 𝑁 ) × { 0 } ) : ( 3 ... 𝑁 ) ⟶ ℝ )
6		axlowdimlem2	⊢ ( ( 1 ... 2 ) ∩ ( 3 ... 𝑁 ) ) = ∅
7		fun2	⊢ ( ( ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } : ( 1 ... 2 ) ⟶ ℝ ∧ ( ( 3 ... 𝑁 ) × { 0 } ) : ( 3 ... 𝑁 ) ⟶ ℝ ) ∧ ( ( 1 ... 2 ) ∩ ( 3 ... 𝑁 ) ) = ∅ ) → ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) : ( ( 1 ... 2 ) ∪ ( 3 ... 𝑁 ) ) ⟶ ℝ )
8	5 6 7	mp2an	⊢ ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) : ( ( 1 ... 2 ) ∪ ( 3 ... 𝑁 ) ) ⟶ ℝ
9		axlowdimlem3	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 1 ... 𝑁 ) = ( ( 1 ... 2 ) ∪ ( 3 ... 𝑁 ) ) )
10	9	feq2d	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) : ( 1 ... 𝑁 ) ⟶ ℝ ↔ ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) : ( ( 1 ... 2 ) ∪ ( 3 ... 𝑁 ) ) ⟶ ℝ ) )
11	8 10	mpbiri	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) : ( 1 ... 𝑁 ) ⟶ ℝ )
12		eluz2nn	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ )
13		elee	⊢ ( 𝑁 ∈ ℕ → ( ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ∈ ( 𝔼 ‘ 𝑁 ) ↔ ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) : ( 1 ... 𝑁 ) ⟶ ℝ ) )
14	12 13	syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ∈ ( 𝔼 ‘ 𝑁 ) ↔ ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) : ( 1 ... 𝑁 ) ⟶ ℝ ) )
15	11 14	mpbird	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( { ⟨ 1 , 𝐴 ⟩ , ⟨ 2 , 𝐵 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ∈ ( 𝔼 ‘ 𝑁 ) )