Metamath Proof Explorer

Theorem cgrdegen

Description: Two congruent segments are either both degenerate or both nondegenerate. (Contributed by Scott Fenton, 12-Jun-2013)

Ref Expression
Assertion cgrdegen ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→ABCgrCD→A=B↔C=D

Proof

Step Hyp Ref Expression
1 opeq1 ⊢A=B→AB=BB
2 1 breq1d ⊢A=B→ABCgrCD↔BBCgrCD
3 2 biimpac ⊢ABCgrCD∧A=B→BBCgrCD
4 simp1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→N∈ℕ
5 simp2r ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→B∈𝔼⁡N
6 simp3l ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→C∈𝔼⁡N
7 simp3r ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→D∈𝔼⁡N
8 cgrid2 ⊢N∈ℕ∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→BBCgrCD→C=D
9 4 5 6 7 8 syl13anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→BBCgrCD→C=D
10 3 9 syl5 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→ABCgrCD∧A=B→C=D
11 10 expdimp ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧ABCgrCD→A=B→C=D
12 opeq1 ⊢C=D→CD=DD
13 12 breq2d ⊢C=D→ABCgrCD↔ABCgrDD
14 13 biimpac ⊢ABCgrCD∧C=D→ABCgrDD
15 simp2l ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→A∈𝔼⁡N
16 axcgrid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧D∈𝔼⁡N→ABCgrDD→A=B
17 4 15 5 7 16 syl13anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→ABCgrDD→A=B
18 14 17 syl5 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→ABCgrCD∧C=D→A=B
19 18 expdimp ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧ABCgrCD→C=D→A=B
20 11 19 impbid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧ABCgrCD→A=B↔C=D
21 20 ex ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→ABCgrCD→A=B↔C=D