Metamath Proof Explorer

Theorem eengstr

Description: The Euclidean geometry as a structure. (Contributed by Thierry Arnoux, 15-Mar-2019)

Ref Expression
Assertion eengstr ⊢ N ∈ ℕ → 𝔼 𝒢 ⁡ N Struct 1 17

Proof

Step Hyp Ref Expression
1 eengv ⊢ N ∈ ℕ → 𝔼 𝒢 ⁡ N = Base ndx 𝔼 ⁡ N dist ⁡ ndx x ∈ 𝔼 ⁡ N , y ∈ 𝔼 ⁡ N ⟼ ∑ i = 1 N x ⁡ i − y ⁡ i 2 ∪ Itv ⁡ ndx x ∈ 𝔼 ⁡ N , y ∈ 𝔼 ⁡ N ⟼ z ∈ 𝔼 ⁡ N | z Btwn x y Line 𝒢 ⁡ ndx x ∈ 𝔼 ⁡ N , y ∈ 𝔼 ⁡ N ∖ x ⟼ z ∈ 𝔼 ⁡ N | z Btwn x y ∨ x Btwn z y ∨ y Btwn x z
2 1nn ⊢ 1 ∈ ℕ
3 basendx ⊢ Base ndx = 1
4 2nn0 ⊢ 2 ∈ ℕ 0
5 1nn0 ⊢ 1 ∈ ℕ 0
6 1lt10 ⊢ 1 < 10
7 2 4 5 6 declti ⊢ 1 < 12
8 2nn ⊢ 2 ∈ ℕ
9 5 8 decnncl ⊢ 12 ∈ ℕ
10 dsndx ⊢ dist ⁡ ndx = 12
11 2 3 7 9 10 strle2 ⊢ Base ndx 𝔼 ⁡ N dist ⁡ ndx x ∈ 𝔼 ⁡ N , y ∈ 𝔼 ⁡ N ⟼ ∑ i = 1 N x ⁡ i − y ⁡ i 2 Struct 1 12
12 6nn ⊢ 6 ∈ ℕ
13 5 12 decnncl ⊢ 16 ∈ ℕ
14 itvndx ⊢ Itv ⁡ ndx = 16
15 6nn0 ⊢ 6 ∈ ℕ 0
16 7nn ⊢ 7 ∈ ℕ
17 6lt7 ⊢ 6 < 7
18 5 15 16 17 declt ⊢ 16 < 17
19 5 16 decnncl ⊢ 17 ∈ ℕ
20 lngndx ⊢ Line 𝒢 ⁡ ndx = 17
21 13 14 18 19 20 strle2 ⊢ Itv ⁡ ndx x ∈ 𝔼 ⁡ N , y ∈ 𝔼 ⁡ N ⟼ z ∈ 𝔼 ⁡ N | z Btwn x y Line 𝒢 ⁡ ndx x ∈ 𝔼 ⁡ N , y ∈ 𝔼 ⁡ N ∖ x ⟼ z ∈ 𝔼 ⁡ N | z Btwn x y ∨ x Btwn z y ∨ y Btwn x z Struct 16 17
22 2lt6 ⊢ 2 < 6
23 5 4 12 22 declt ⊢ 12 < 16
24 11 21 23 strleun ⊢ Base ndx 𝔼 ⁡ N dist ⁡ ndx x ∈ 𝔼 ⁡ N , y ∈ 𝔼 ⁡ N ⟼ ∑ i = 1 N x ⁡ i − y ⁡ i 2 ∪ Itv ⁡ ndx x ∈ 𝔼 ⁡ N , y ∈ 𝔼 ⁡ N ⟼ z ∈ 𝔼 ⁡ N | z Btwn x y Line 𝒢 ⁡ ndx x ∈ 𝔼 ⁡ N , y ∈ 𝔼 ⁡ N ∖ x ⟼ z ∈ 𝔼 ⁡ N | z Btwn x y ∨ x Btwn z y ∨ y Btwn x z Struct 1 17
25 1 24 eqbrtrdi ⊢ N ∈ ℕ → 𝔼 𝒢 ⁡ N Struct 1 17