Metamath Proof Explorer

Theorem tgexta

Description: The exterior-angle theorem, GeoCoq l11__41 -- BOTH remote interior angles of the triangle are STRICTLY less than the exterior angle at C . There is no ltA in set.mm , so strictness is carried inline as leA together with the non-congruence; the pair is what tgaas 's contradiction branch needs, since a bare leA conclusion is satisfied by a congruence and so contradicts nothing ( tgextan records that the pair is usable). The second conjunct is not a permutation of the first: axtgsegcon builds a second extension point y beyond C on line A C , tgextalt2 reruns the construction there, and the two exterior angles are identified as vertical by tgextaoa . (Contributed by JAG, 12-Aug-2026)

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

Proof

Step Hyp Ref Expression
1 tgexta.p 
 |-  P = ( Base ` G )
2 tgexta.m 
 |-  .- = ( dist ` G )
3 tgexta.i 
 |-  I = ( Itv ` G )
4 tgexta.l 
 |-  L = ( LineG ` G )
5 tgexta.k 
 |-  K = ( hlG ` G )
6 tgexta.s 
 |-  .<_ = ( leA ` G )
7 tgexta.g 
 |-  ( ph -> G e. TarskiG )
8 tgexta.a 
 |-  ( ph -> A e. P )
9 tgexta.b 
 |-  ( ph -> B e. P )
10 tgexta.c 
 |-  ( ph -> C e. P )
11 tgexta.d 
 |-  ( ph -> D e. P )
12 tgexta.1 
 |-  ( ph -> C e. ( B I D ) )
13 tgexta.2 
 |-  ( ph -> -. ( A e. ( B L C ) \/ B = C ) )
14 tgexta.3 
 |-  ( ph -> C =/= D )
15 1 2 3 4 5 6 7 8 9 10 11 12 13 14 tgextalt1 
 |-  ( ph -> ( <" B A C "> .<_ <" A C D "> /\ -. <" B A C "> ( cgrA ` G ) <" A C D "> ) )
16 7 adantr 
 |-  ( ( ph /\ y e. P ) -> G e. TarskiG )
17 16 adantr 
 |-  ( ( ( ph /\ y e. P ) /\ ( C e. ( A I y ) /\ ( C .- y ) = ( C .- A ) ) ) -> G e. TarskiG )
18 8 adantr 
 |-  ( ( ph /\ y e. P ) -> A e. P )
19 18 adantr 
 |-  ( ( ( ph /\ y e. P ) /\ ( C e. ( A I y ) /\ ( C .- y ) = ( C .- A ) ) ) -> A e. P )
20 9 adantr 
 |-  ( ( ph /\ y e. P ) -> B e. P )
21 20 adantr 
 |-  ( ( ( ph /\ y e. P ) /\ ( C e. ( A I y ) /\ ( C .- y ) = ( C .- A ) ) ) -> B e. P )
22 10 adantr 
 |-  ( ( ph /\ y e. P ) -> C e. P )
23 22 adantr 
 |-  ( ( ( ph /\ y e. P ) /\ ( C e. ( A I y ) /\ ( C .- y ) = ( C .- A ) ) ) -> C e. P )
24 11 adantr 
 |-  ( ( ph /\ y e. P ) -> D e. P )
25 24 adantr 
 |-  ( ( ( ph /\ y e. P ) /\ ( C e. ( A I y ) /\ ( C .- y ) = ( C .- A ) ) ) -> D e. P )
26 simpl 
 |-  ( ( ( ph /\ y e. P ) /\ ( C e. ( A I y ) /\ ( C .- y ) = ( C .- A ) ) ) -> ( ph /\ y e. P ) )
27 26 simprd 
 |-  ( ( ( ph /\ y e. P ) /\ ( C e. ( A I y ) /\ ( C .- y ) = ( C .- A ) ) ) -> y e. P )
28 12 adantr 
 |-  ( ( ph /\ y e. P ) -> C e. ( B I D ) )
29 28 adantr 
 |-  ( ( ( ph /\ y e. P ) /\ ( C e. ( A I y ) /\ ( C .- y ) = ( C .- A ) ) ) -> C e. ( B I D ) )
30 simpr 
 |-  ( ( ( ph /\ y e. P ) /\ ( C e. ( A I y ) /\ ( C .- y ) = ( C .- A ) ) ) -> ( C e. ( A I y ) /\ ( C .- y ) = ( C .- A ) ) )
31 30 simpld 
 |-  ( ( ( ph /\ y e. P ) /\ ( C e. ( A I y ) /\ ( C .- y ) = ( C .- A ) ) ) -> C e. ( A I y ) )
32 13 adantr 
 |-  ( ( ph /\ y e. P ) -> -. ( A e. ( B L C ) \/ B = C ) )
33 32 adantr 
 |-  ( ( ( ph /\ y e. P ) /\ ( C e. ( A I y ) /\ ( C .- y ) = ( C .- A ) ) ) -> -. ( A e. ( B L C ) \/ B = C ) )
34 14 adantr 
 |-  ( ( ph /\ y e. P ) -> C =/= D )
35 34 adantr 
 |-  ( ( ( ph /\ y e. P ) /\ ( C e. ( A I y ) /\ ( C .- y ) = ( C .- A ) ) ) -> C =/= D )
36 30 simprd 
 |-  ( ( ( ph /\ y e. P ) /\ ( C e. ( A I y ) /\ ( C .- y ) = ( C .- A ) ) ) -> ( C .- y ) = ( C .- A ) )
37 36 eqcomd 
 |-  ( ( ( ph /\ y e. P ) /\ ( C e. ( A I y ) /\ ( C .- y ) = ( C .- A ) ) ) -> ( C .- A ) = ( C .- y ) )
38 1 3 4 7 8 9 10 13 ncolne2 
 |-  ( ph -> A =/= C )
39 38 necomd 
 |-  ( ph -> C =/= A )
40 39 adantr 
 |-  ( ( ph /\ y e. P ) -> C =/= A )
41 40 adantr 
 |-  ( ( ( ph /\ y e. P ) /\ ( C e. ( A I y ) /\ ( C .- y ) = ( C .- A ) ) ) -> C =/= A )
42 1 2 3 17 23 19 23 27 37 41 tgcgrneq 
 |-  ( ( ( ph /\ y e. P ) /\ ( C e. ( A I y ) /\ ( C .- y ) = ( C .- A ) ) ) -> C =/= y )
43 1 2 3 4 5 6 17 19 21 23 25 27 29 31 33 35 42 tgextalt2 
 |-  ( ( ( ph /\ y e. P ) /\ ( C e. ( A I y ) /\ ( C .- y ) = ( C .- A ) ) ) -> ( <" A B C "> .<_ <" A C D "> /\ -. <" A B C "> ( cgrA ` G ) <" A C D "> ) )
44 1 2 3 7 8 10 10 8 axtgsegcon 
 |-  ( ph -> E. y e. P ( C e. ( A I y ) /\ ( C .- y ) = ( C .- A ) ) )
45 43 44 r19.29a 
 |-  ( ph -> ( <" A B C "> .<_ <" A C D "> /\ -. <" A B C "> ( cgrA ` G ) <" A C D "> ) )
46 15 45 jca 
 |-  ( ph -> ( ( <" B A C "> .<_ <" A C D "> /\ -. <" B A C "> ( cgrA ` G ) <" A C D "> ) /\ ( <" A B C "> .<_ <" A C D "> /\ -. <" A B C "> ( cgrA ` G ) <" A C D "> ) ) )