Metamath Proof Explorer


Theorem cgrane3

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 cgrane3 φED

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 simpllr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFxP
13 8 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFDP
14 9 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFEP
15 4 ad3antrrr φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFG𝒢Tarski
16 simpr2 φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFxKED
17 1 2 3 12 13 14 15 16 hlne2 φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFDE
18 17 necomd φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEFED
19 1 2 3 4 5 6 7 8 9 10 iscgra φ⟨“ABC”⟩𝒢G⟨“DEF”⟩xPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEF
20 11 19 mpbid φxPyP⟨“ABC”⟩𝒢G⟨“xEy”⟩xKEDyKEF
21 18 20 r19.29vva φED