Metamath Proof Explorer

Theorem cgranbtwn

Description: Null angle implies betweenness. (Contributed by SS, 4-Jun-2026)

Ref Expression
Hypotheses cgranbtwn.p ⊢ P = Base G
cgranbtwn.i ⊢ I = Itv ⁡ G
cgranbtwn.g ⊢ φ → G ∈ 𝒢 Tarski
cgranbtwn.a ⊢ φ → A ∈ P
cgranbtwn.b ⊢ φ → B ∈ P
cgranbtwn.c ⊢ φ → C ∈ P
cgranbtwn.d ⊢ φ → D ∈ P
cgranbtwn.e ⊢ φ → E ∈ P
cgranbtwn.f ⊢ φ → F ∈ P
cgranbtwn.1 ⊢ φ → ⟨“ ABC ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ DEF ”⟩
cgranbtwn.2 ⊢ φ → A ∈ B I C
Assertion cgranbtwn ⊢ φ → D ∈ E I F ∨ F ∈ E I D

Proof

Step Hyp Ref Expression
1 cgranbtwn.p ⊢ P = Base G
2 cgranbtwn.i ⊢ I = Itv ⁡ G
3 cgranbtwn.g ⊢ φ → G ∈ 𝒢 Tarski
4 cgranbtwn.a ⊢ φ → A ∈ P
5 cgranbtwn.b ⊢ φ → B ∈ P
6 cgranbtwn.c ⊢ φ → C ∈ P
7 cgranbtwn.d ⊢ φ → D ∈ P
8 cgranbtwn.e ⊢ φ → E ∈ P
9 cgranbtwn.f ⊢ φ → F ∈ P
10 cgranbtwn.1 ⊢ φ → ⟨“ ABC ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ DEF ”⟩
11 cgranbtwn.2 ⊢ φ → A ∈ B I C
12 eqid ⊢ dist ⁡ G = dist ⁡ G
13 eqid ⊢ hl 𝒢 ⁡ G = hl 𝒢 ⁡ G
14 1 2 13 3 4 5 6 7 8 9 10 cgrane2 ⊢ φ → B ≠ C
15 1 2 13 3 4 5 6 7 8 9 10 cgrane1 ⊢ φ → A ≠ B
16 1 2 13 5 6 4 3 4 11 14 15 btwnhl1 ⊢ φ → A hl 𝒢 ⁡ G ⁡ B C
17 1 2 12 3 4 5 6 7 8 9 10 13 16 cgrahl ⊢ φ → D hl 𝒢 ⁡ G ⁡ E F
18 1 2 13 7 9 8 3 ishlg ⊢ φ → D hl 𝒢 ⁡ G ⁡ E F ↔ D ≠ E ∧ F ≠ E ∧ D ∈ E I F ∨ F ∈ E I D
19 17 18 mpbid ⊢ φ → D ≠ E ∧ F ≠ E ∧ D ∈ E I F ∨ F ∈ E I D
20 19 simp3d ⊢ φ → D ∈ E I F ∨ F ∈ E I D