Metamath Proof Explorer


Theorem cgrane1

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 cgrane1 φAB

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 simpllr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFxP
15 9 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFEP
16 5 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFAP
17 6 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFBP
18 eqid 𝒢G=𝒢G
19 7 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFCP
20 simplr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFyP
21 simpr1 φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEF⟨“ABC”⟩𝒢G⟨“xEy”⟩
22 1 12 2 18 13 16 17 19 14 15 20 21 cgr3simp1 φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFAdistGB=xdistGE
23 22 eqcomd φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFxdistGE=AdistGB
24 8 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFDP
25 simpr2 φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFxKED
26 1 2 3 14 24 15 13 25 hlne1 φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFxE
27 1 12 2 13 14 15 16 17 23 26 tgcgrneq φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFAB
28 1 2 3 4 5 6 7 8 9 10 iscgra φ⟨“ABC”⟩𝒢G⟨“DEF”⟩xPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEF
29 11 28 mpbid φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEF
30 27 29 r19.29vva φAB