Metamath Proof Explorer

Theorem tgextalt1

Description: tgexta 's FIRST conjunct, strict -- the remote interior angle at A is strictly less than the exterior angle at C . tgextale and tgextancgra deliver both halves already, but stated about <" C A B "> ; tgexta wants <" B A C "> , the same angle read backwards. So this is cgraswap plus two transports: leacgra1 for the leA half, and cgratr under mtand for the negation -- if <" B A C "> were congruent to the exterior angle then so would <" C A B "> be, which tgextancgra forbids. (Contributed by JAG, 12-Aug-2026)

Ref Expression
Hypotheses tgextalt1.p 
|- P = ( Base ` G )
tgextalt1.m 
|- .- = ( dist ` G )
tgextalt1.i 
|- I = ( Itv ` G )
tgextalt1.l 
|- L = ( LineG ` G )
tgextalt1.k 
|- K = ( hlG ` G )
tgextalt1.s 
|- .<_ = ( leA ` G )
tgextalt1.g 
|- ( ph -> G e. TarskiG )
tgextalt1.a 
|- ( ph -> A e. P )
tgextalt1.b 
|- ( ph -> B e. P )
tgextalt1.c 
|- ( ph -> C e. P )
tgextalt1.d 
|- ( ph -> D e. P )
tgextalt1.ext 
|- ( ph -> C e. ( B I D ) )
tgextalt1.ncol 
|- ( ph -> -. ( A e. ( B L C ) \/ B = C ) )
tgextalt1.ne 
|- ( ph -> C =/= D )
Assertion tgextalt1 
|- ( ph -> ( <" B A C "> .<_ <" A C D "> /\ -. <" B A C "> ( cgrA ` G ) <" A C D "> ) )

Proof

Step Hyp Ref Expression
1 tgextalt1.p 
 |-  P = ( Base ` G )
2 tgextalt1.m 
 |-  .- = ( dist ` G )
3 tgextalt1.i 
 |-  I = ( Itv ` G )
4 tgextalt1.l 
 |-  L = ( LineG ` G )
5 tgextalt1.k 
 |-  K = ( hlG ` G )
6 tgextalt1.s 
 |-  .<_ = ( leA ` G )
7 tgextalt1.g 
 |-  ( ph -> G e. TarskiG )
8 tgextalt1.a 
 |-  ( ph -> A e. P )
9 tgextalt1.b 
 |-  ( ph -> B e. P )
10 tgextalt1.c 
 |-  ( ph -> C e. P )
11 tgextalt1.d 
 |-  ( ph -> D e. P )
12 tgextalt1.ext 
 |-  ( ph -> C e. ( B I D ) )
13 tgextalt1.ncol 
 |-  ( ph -> -. ( A e. ( B L C ) \/ B = C ) )
14 tgextalt1.ne 
 |-  ( ph -> C =/= D )
15 1 2 3 4 5 7 8 9 10 11 12 13 14 tgextale 
 |-  ( ph -> <" C A B "> ( leA ` G ) <" A C D "> )
16 1 3 4 7 8 9 10 13 ncolne2 
 |-  ( ph -> A =/= C )
17 16 necomd 
 |-  ( ph -> C =/= A )
18 1 3 4 7 8 9 10 13 ncolne1 
 |-  ( ph -> A =/= B )
19 1 3 7 5 10 8 9 17 18 cgraswap 
 |-  ( ph -> <" C A B "> ( cgrA ` G ) <" B A C "> )
20 1 3 5 7 10 8 9 8 10 11 9 8 10 15 19 leacgra1 
 |-  ( ph -> <" B A C "> ( leA ` G ) <" A C D "> )
21 6 breqi 
 |-  ( <" B A C "> .<_ <" A C D "> <-> <" B A C "> ( leA ` G ) <" A C D "> )
22 20 21 sylibr 
 |-  ( ph -> <" B A C "> .<_ <" A C D "> )
23 1 2 3 4 5 7 8 9 10 11 12 13 14 tgextancgra 
 |-  ( ph -> -. <" C A B "> ( cgrA ` G ) <" A C D "> )
24 7 adantr 
 |-  ( ( ph /\ <" B A C "> ( cgrA ` G ) <" A C D "> ) -> G e. TarskiG )
25 10 adantr 
 |-  ( ( ph /\ <" B A C "> ( cgrA ` G ) <" A C D "> ) -> C e. P )
26 8 adantr 
 |-  ( ( ph /\ <" B A C "> ( cgrA ` G ) <" A C D "> ) -> A e. P )
27 9 adantr 
 |-  ( ( ph /\ <" B A C "> ( cgrA ` G ) <" A C D "> ) -> B e. P )
28 19 adantr 
 |-  ( ( ph /\ <" B A C "> ( cgrA ` G ) <" A C D "> ) -> <" C A B "> ( cgrA ` G ) <" B A C "> )
29 11 adantr 
 |-  ( ( ph /\ <" B A C "> ( cgrA ` G ) <" A C D "> ) -> D e. P )
30 simpr 
 |-  ( ( ph /\ <" B A C "> ( cgrA ` G ) <" A C D "> ) -> <" B A C "> ( cgrA ` G ) <" A C D "> )
31 1 3 24 5 25 26 27 27 26 25 28 26 25 29 30 cgratr 
 |-  ( ( ph /\ <" B A C "> ( cgrA ` G ) <" A C D "> ) -> <" C A B "> ( cgrA ` G ) <" A C D "> )
32 23 31 mtand 
 |-  ( ph -> -. <" B A C "> ( cgrA ` G ) <" A C D "> )
33 22 32 jca 
 |-  ( ph -> ( <" B A C "> .<_ <" A C D "> /\ -. <" B A C "> ( cgrA ` G ) <" A C D "> ) )