Metamath Proof Explorer


Theorem cgrane2

Description: Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020)

Ref Expression
Hypotheses iscgra.p P=BaseG
iscgra.i I=ItvG
iscgra.k K=hl𝒢G
iscgra.g φG𝒢Tarski
iscgra.a φAP
iscgra.b φBP
iscgra.c φCP
iscgra.d φDP
iscgra.e φEP
iscgra.f φFP
cgrahl1.2 φ⟨“ABC”⟩𝒢G⟨“DEF”⟩
Assertion cgrane2 φBC

Proof

Step Hyp Ref Expression
1 iscgra.p P=BaseG
2 iscgra.i I=ItvG
3 iscgra.k K=hl𝒢G
4 iscgra.g φG𝒢Tarski
5 iscgra.a φAP
6 iscgra.b φBP
7 iscgra.c φCP
8 iscgra.d φDP
9 iscgra.e φEP
10 iscgra.f φFP
11 cgrahl1.2 φ⟨“ABC”⟩𝒢G⟨“DEF”⟩
12 eqid distG=distG
13 4 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFG𝒢Tarski
14 9 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFEP
15 simplr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFyP
16 6 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFBP
17 7 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFCP
18 eqid 𝒢G=𝒢G
19 5 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFAP
20 simpllr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFxP
21 simpr1 φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEF⟨“ABC”⟩𝒢G⟨“xEy”⟩
22 1 12 2 18 13 19 16 17 20 14 15 21 cgr3simp2 φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFBdistGC=EdistGy
23 22 eqcomd φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFEdistGy=BdistGC
24 10 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFFP
25 simpr3 φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFyKEF
26 1 2 3 15 24 14 13 25 hlne1 φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFyE
27 26 necomd φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFEy
28 1 12 2 13 14 15 16 17 23 27 tgcgrneq φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFBC
29 1 2 3 4 5 6 7 8 9 10 iscgra φ⟨“ABC”⟩𝒢G⟨“DEF”⟩xPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEF
30 11 29 mpbid φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEF
31 28 30 r19.29vva φBC