Theorem 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={\mathrm{Base}}_G$$
	tgaasexc.m	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	tgaasexc.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	tgaasexc.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	tgaasexc.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	tgaasexc.d	$$⊢\phi \to D\in P$$
	tgaasexc.e	$$⊢\phi \to E\in P$$
	tgaasexc.s	$$⊢\phi \to S\in P$$
	tgaasexc.t	$$⊢\phi \to T\in P$$
	tgaasexc.1	$$⊢\phi \to \neg \left(D\in \left(ELT\right)\vee E=T\right)$$
	tgaasexc.2	$$⊢\phi \to S\in \left(EIT\right)$$
	tgaasexc.3	$$⊢\phi \to S\ne E$$
	tgaasexc.4	$$⊢\phi \to S\ne T$$
	tgaasexc.5	$$⊢\phi \to ⟨“DTE”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DSE”⟩$$
Assertion	tgaasexc	$$⊢\phi \to \psi$$

Proof

Step	Hyp	Ref	Expression
1		tgaasexc.p	$$⊢P={\mathrm{Base}}_G$$
2		tgaasexc.m	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		tgaasexc.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		tgaasexc.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
5		tgaasexc.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
6		tgaasexc.d	$$⊢\phi \to D\in P$$
7		tgaasexc.e	$$⊢\phi \to E\in P$$
8		tgaasexc.s	$$⊢\phi \to S\in P$$
9		tgaasexc.t	$$⊢\phi \to T\in P$$
10		tgaasexc.1	$$⊢\phi \to \neg \left(D\in \left(ELT\right)\vee E=T\right)$$
11		tgaasexc.2	$$⊢\phi \to S\in \left(EIT\right)$$
12		tgaasexc.3	$$⊢\phi \to S\ne E$$
13		tgaasexc.4	$$⊢\phi \to S\ne T$$
14		tgaasexc.5	$$⊢\phi \to ⟨“DTE”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DSE”⟩$$
15		eqid	$$⊢{hl}_{𝒢}\left(G\right)={hl}_{𝒢}\left(G\right)$$
16		eqid	$$⊢{\le }_{𝒢}^{\angle }\left(G\right)={\le }_{𝒢}^{\angle }\left(G\right)$$
17	1 2 3 5 7 8 9 11	tgbtwncom	$$⊢\phi \to S\in \left(TIE\right)$$
18	1 4 3 5 9 7 8 17	btwncolg1	$$⊢\phi \to \left(S\in \left(TLE\right)\vee T=E\right)$$
19	1 3 4 5 6 7 9 8 10 18 13	tgaasncol	$$⊢\phi \to \neg \left(D\in \left(TLS\right)\vee T=S\right)$$
20	1 3 4 5 6 7 9 10	ncolne2	$$⊢\phi \to D\ne T$$
21	1 4 3 5 7 9 6 10	ncolrot1	$$⊢\phi \to \neg \left(E\in \left(TLD\right)\vee T=D\right)$$
22	1 3 4 5 7 9 6 21	ncolne1	$$⊢\phi \to E\ne T$$
23	22	necomd	$$⊢\phi \to T\ne E$$
24	1 3 5 15 6 9 7 20 23	cgraid	$$⊢\phi \to ⟨“DTE”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DTE”⟩$$
25	1 3 15 9 7 8 5 6 17 23 13	btwnhl1	$$⊢\phi \to S{hl}_{𝒢}\left(G\right)\left(T\right)E$$
26	1 3 15 5 6 9 7 6 9 7 24 8 25	cgrahl2	$$⊢\phi \to ⟨“DTE”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DTS”⟩$$
27	1 3 5 15 6 9 7 6 9 8 26	cgracom	$$⊢\phi \to ⟨“DTS”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DTE”⟩$$
28	1 3 5 15 6 9 8 6 9 7 27 6 8 7 14	cgratr	$$⊢\phi \to ⟨“DTS”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DSE”⟩$$
29	1 2 3 4 15 16 5 6 9 8 7 17 19 12 28	tgextan	$$⊢\phi \to \psi$$