Metamath Proof Explorer


Theorem leagne3

Description: Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023)

Ref Expression
Hypotheses isleag.p P = Base G
isleag.g φ G 𝒢 Tarski
isleag.a φ A P
isleag.b φ B P
isleag.c φ C P
isleag.d φ D P
isleag.e φ E P
isleag.f φ F P
leagne.1 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩
Assertion leagne3 φ D E

Proof

Step Hyp Ref Expression
1 isleag.p P = Base G
2 isleag.g φ G 𝒢 Tarski
3 isleag.a φ A P
4 isleag.b φ B P
5 isleag.c φ C P
6 isleag.d φ D P
7 isleag.e φ E P
8 isleag.f φ F P
9 leagne.1 φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩
10 eqid Itv G = Itv G
11 eqid hl 𝒢 G = hl 𝒢 G
12 2 ad2antrr φ x P x 𝒢 G ⟨“ DEF ”⟩ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEx ”⟩ G 𝒢 Tarski
13 3 ad2antrr φ x P x 𝒢 G ⟨“ DEF ”⟩ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEx ”⟩ A P
14 4 ad2antrr φ x P x 𝒢 G ⟨“ DEF ”⟩ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEx ”⟩ B P
15 5 ad2antrr φ x P x 𝒢 G ⟨“ DEF ”⟩ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEx ”⟩ C P
16 6 ad2antrr φ x P x 𝒢 G ⟨“ DEF ”⟩ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEx ”⟩ D P
17 7 ad2antrr φ x P x 𝒢 G ⟨“ DEF ”⟩ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEx ”⟩ E P
18 simplr φ x P x 𝒢 G ⟨“ DEF ”⟩ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEx ”⟩ x P
19 simprr φ x P x 𝒢 G ⟨“ DEF ”⟩ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEx ”⟩ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEx ”⟩
20 1 10 11 12 13 14 15 16 17 18 19 cgrane3 φ x P x 𝒢 G ⟨“ DEF ”⟩ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEx ”⟩ E D
21 20 necomd φ x P x 𝒢 G ⟨“ DEF ”⟩ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEx ”⟩ D E
22 1 2 3 4 5 6 7 8 isleag φ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEF ”⟩ x P x 𝒢 G ⟨“ DEF ”⟩ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEx ”⟩
23 9 22 mpbid φ x P x 𝒢 G ⟨“ DEF ”⟩ ⟨“ ABC ”⟩ 𝒢 G ⟨“ DEx ”⟩
24 21 23 r19.29a φ D E