# Metamath Proof Explorer

## Theorem cgrtriv

Description: Degenerate segments are congruent. Theorem 2.8 of Schwabhauser p. 28. (Contributed by Scott Fenton, 12-Jun-2013)

Ref Expression
Assertion cgrtriv ${⊢}\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\to ⟨{A},{A}⟩\mathrm{Cgr}⟨{B},{B}⟩$

### Proof

Step Hyp Ref Expression
1 simp1 ${⊢}\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\to {N}\in ℕ$
2 simp2 ${⊢}\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\to {A}\in 𝔼\left({N}\right)$
3 simp3 ${⊢}\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\to {B}\in 𝔼\left({N}\right)$
4 axsegcon ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\right)\wedge \left({B}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\right)\to \exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\left({A}\mathrm{Btwn}⟨{A},{x}⟩\wedge ⟨{A},{x}⟩\mathrm{Cgr}⟨{B},{B}⟩\right)$
5 1 2 2 3 3 4 syl122anc ${⊢}\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\to \exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\left({A}\mathrm{Btwn}⟨{A},{x}⟩\wedge ⟨{A},{x}⟩\mathrm{Cgr}⟨{B},{B}⟩\right)$
6 simpl1 ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to {N}\in ℕ$
7 simpl2 ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to {A}\in 𝔼\left({N}\right)$
8 simpr ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to {x}\in 𝔼\left({N}\right)$
9 simpl3 ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to {B}\in 𝔼\left({N}\right)$
10 axcgrid ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {x}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{A},{x}⟩\mathrm{Cgr}⟨{B},{B}⟩\to {A}={x}\right)$
11 6 7 8 9 10 syl13anc ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to \left(⟨{A},{x}⟩\mathrm{Cgr}⟨{B},{B}⟩\to {A}={x}\right)$
12 opeq2 ${⊢}{A}={x}\to ⟨{A},{A}⟩=⟨{A},{x}⟩$
13 12 breq1d ${⊢}{A}={x}\to \left(⟨{A},{A}⟩\mathrm{Cgr}⟨{B},{B}⟩↔⟨{A},{x}⟩\mathrm{Cgr}⟨{B},{B}⟩\right)$
14 13 biimprd ${⊢}{A}={x}\to \left(⟨{A},{x}⟩\mathrm{Cgr}⟨{B},{B}⟩\to ⟨{A},{A}⟩\mathrm{Cgr}⟨{B},{B}⟩\right)$
15 11 14 syli ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to \left(⟨{A},{x}⟩\mathrm{Cgr}⟨{B},{B}⟩\to ⟨{A},{A}⟩\mathrm{Cgr}⟨{B},{B}⟩\right)$
16 15 adantld ${⊢}\left(\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\wedge {x}\in 𝔼\left({N}\right)\right)\to \left(\left({A}\mathrm{Btwn}⟨{A},{x}⟩\wedge ⟨{A},{x}⟩\mathrm{Cgr}⟨{B},{B}⟩\right)\to ⟨{A},{A}⟩\mathrm{Cgr}⟨{B},{B}⟩\right)$
17 16 rexlimdva ${⊢}\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\to \left(\exists {x}\in 𝔼\left({N}\right)\phantom{\rule{.4em}{0ex}}\left({A}\mathrm{Btwn}⟨{A},{x}⟩\wedge ⟨{A},{x}⟩\mathrm{Cgr}⟨{B},{B}⟩\right)\to ⟨{A},{A}⟩\mathrm{Cgr}⟨{B},{B}⟩\right)$
18 5 17 mpd ${⊢}\left({N}\in ℕ\wedge {A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\to ⟨{A},{A}⟩\mathrm{Cgr}⟨{B},{B}⟩$