tgaasexc

Description: The contradiction branch of AAS, stated once for both orders of the two candidate points. S lies strictly between E and T , and D is off the line, so <" D S E "> is an exterior angle of triangle D T S and is STRICTLY greater than the remote interior angle at T -- while the hypothesis says the two are congruent. tgextan turns that into anything. (Contributed by JAG, 12-Aug-2026)

	Ref	Expression
Hypotheses	tgaasexc.p	\|- P = ( Base ` G )
	tgaasexc.m	\|- .- = ( dist ` G )
	tgaasexc.i	\|- I = ( Itv ` G )
	tgaasexc.l	\|- L = ( LineG ` G )
	tgaasexc.g	\|- ( ph -> G e. TarskiG )
	tgaasexc.d	\|- ( ph -> D e. P )
	tgaasexc.e	\|- ( ph -> E e. P )
	tgaasexc.s	\|- ( ph -> S e. P )
	tgaasexc.t	\|- ( ph -> T e. P )
	tgaasexc.1	\|- ( ph -> -. ( D e. ( E L T ) \/ E = T ) )
	tgaasexc.2	\|- ( ph -> S e. ( E I T ) )
	tgaasexc.3	\|- ( ph -> S =/= E )
	tgaasexc.4	\|- ( ph -> S =/= T )
	tgaasexc.5	\|- ( ph -> <" D T E "> ( cgrA ` G ) <" D S E "> )
Assertion	tgaasexc	\|- ( ph -> ps )

Proof

Step	Hyp	Ref	Expression
1		tgaasexc.p	\|- P = ( Base ` G )
2		tgaasexc.m	\|- .- = ( dist ` G )
3		tgaasexc.i	\|- I = ( Itv ` G )
4		tgaasexc.l	\|- L = ( LineG ` G )
5		tgaasexc.g	\|- ( ph -> G e. TarskiG )
6		tgaasexc.d	\|- ( ph -> D e. P )
7		tgaasexc.e	\|- ( ph -> E e. P )
8		tgaasexc.s	\|- ( ph -> S e. P )
9		tgaasexc.t	\|- ( ph -> T e. P )
10		tgaasexc.1	\|- ( ph -> -. ( D e. ( E L T ) \/ E = T ) )
11		tgaasexc.2	\|- ( ph -> S e. ( E I T ) )
12		tgaasexc.3	\|- ( ph -> S =/= E )
13		tgaasexc.4	\|- ( ph -> S =/= T )
14		tgaasexc.5	\|- ( ph -> <" D T E "> ( cgrA ` G ) <" D S E "> )
15		eqid	\|- ( hlG ` G ) = ( hlG ` G )
16		eqid	\|- ( leA ` G ) = ( leA ` G )
17	1 2 3 5 7 8 9 11	tgbtwncom	\|- ( ph -> S e. ( T I E ) )
18	1 4 3 5 9 7 8 17	btwncolg1	\|- ( ph -> ( S e. ( T L E ) \/ T = E ) )
19	1 3 4 5 6 7 9 8 10 18 13	tgaasncol	\|- ( ph -> -. ( D e. ( T L S ) \/ T = S ) )
20	1 3 4 5 6 7 9 10	ncolne2	\|- ( ph -> D =/= T )
21	1 4 3 5 7 9 6 10	ncolrot1	\|- ( ph -> -. ( E e. ( T L D ) \/ T = D ) )
22	1 3 4 5 7 9 6 21	ncolne1	\|- ( ph -> E =/= T )
23	22	necomd	\|- ( ph -> T =/= E )
24	1 3 5 15 6 9 7 20 23	cgraid	\|- ( ph -> <" D T E "> ( cgrA ` G ) <" D T E "> )
25	1 3 15 9 7 8 5 6 17 23 13	btwnhl1	\|- ( ph -> S ( ( hlG ` G ) ` T ) E )
26	1 3 15 5 6 9 7 6 9 7 24 8 25	cgrahl2	\|- ( ph -> <" D T E "> ( cgrA ` G ) <" D T S "> )
27	1 3 5 15 6 9 7 6 9 8 26	cgracom	\|- ( ph -> <" D T S "> ( cgrA ` G ) <" D T E "> )
28	1 3 5 15 6 9 8 6 9 7 27 6 8 7 14	cgratr	\|- ( ph -> <" D T S "> ( cgrA ` G ) <" D S E "> )
29	1 2 3 4 15 16 5 6 9 8 7 17 19 12 28	tgextan	\|- ( ph -> ps )

Metamath Proof Explorer

Theorem tgaasexc

Proof