Metamath Proof Explorer

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 ⊢ 𝑃 = ( Base ‘ 𝐺 )
tgaasexc.m ⊢ − = ( dist ‘ 𝐺 )
tgaasexc.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tgaasexc.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
tgaasexc.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tgaasexc.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
tgaasexc.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
tgaasexc.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑃 )
tgaasexc.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
tgaasexc.1 ⊢ ( 𝜑 → ¬ ( 𝐷 ∈ ( 𝐸 𝐿 𝑇 ) ∨ 𝐸 = 𝑇 ) )
tgaasexc.2 ⊢ ( 𝜑 → 𝑆 ∈ ( 𝐸 𝐼 𝑇 ) )
tgaasexc.3 ⊢ ( 𝜑 → 𝑆 ≠ 𝐸 )
tgaasexc.4 ⊢ ( 𝜑 → 𝑆 ≠ 𝑇 )
tgaasexc.5 ⊢ ( 𝜑 → ⟨“ 𝐷 𝑇 𝐸 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝑆 𝐸 ”⟩ )
Assertion tgaasexc ( 𝜑 → 𝜓 )

Proof

Step Hyp Ref Expression
1 tgaasexc.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tgaasexc.m ⊢ − = ( dist ‘ 𝐺 )
3 tgaasexc.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 tgaasexc.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
5 tgaasexc.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 tgaasexc.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
7 tgaasexc.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
8 tgaasexc.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑃 )
9 tgaasexc.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
10 tgaasexc.1 ⊢ ( 𝜑 → ¬ ( 𝐷 ∈ ( 𝐸 𝐿 𝑇 ) ∨ 𝐸 = 𝑇 ) )
11 tgaasexc.2 ⊢ ( 𝜑 → 𝑆 ∈ ( 𝐸 𝐼 𝑇 ) )
12 tgaasexc.3 ⊢ ( 𝜑 → 𝑆 ≠ 𝐸 )
13 tgaasexc.4 ⊢ ( 𝜑 → 𝑆 ≠ 𝑇 )
14 tgaasexc.5 ⊢ ( 𝜑 → ⟨“ 𝐷 𝑇 𝐸 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝑆 𝐸 ”⟩ )
15 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
16 eqid ⊢ ( ≤∠ ‘ 𝐺 ) = ( ≤∠ ‘ 𝐺 )
17 1 2 3 5 7 8 9 11 tgbtwncom ⊢ ( 𝜑 → 𝑆 ∈ ( 𝑇 𝐼 𝐸 ) )
18 1 4 3 5 9 7 8 17 btwncolg1 ⊢ ( 𝜑 → ( 𝑆 ∈ ( 𝑇 𝐿 𝐸 ) ∨ 𝑇 = 𝐸 ) )
19 1 3 4 5 6 7 9 8 10 18 13 tgaasncol ⊢ ( 𝜑 → ¬ ( 𝐷 ∈ ( 𝑇 𝐿 𝑆 ) ∨ 𝑇 = 𝑆 ) )
20 1 3 4 5 6 7 9 10 ncolne2 ⊢ ( 𝜑 → 𝐷 ≠ 𝑇 )
21 1 4 3 5 7 9 6 10 ncolrot1 ⊢ ( 𝜑 → ¬ ( 𝐸 ∈ ( 𝑇 𝐿 𝐷 ) ∨ 𝑇 = 𝐷 ) )
22 1 3 4 5 7 9 6 21 ncolne1 ⊢ ( 𝜑 → 𝐸 ≠ 𝑇 )
23 22 necomd ⊢ ( 𝜑 → 𝑇 ≠ 𝐸 )
24 1 3 5 15 6 9 7 20 23 cgraid ⊢ ( 𝜑 → ⟨“ 𝐷 𝑇 𝐸 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝑇 𝐸 ”⟩ )
25 1 3 15 9 7 8 5 6 17 23 13 btwnhl1 ⊢ ( 𝜑 → 𝑆 ( ( hlG ‘ 𝐺 ) ‘ 𝑇 ) 𝐸 )
26 1 3 15 5 6 9 7 6 9 7 24 8 25 cgrahl2 ⊢ ( 𝜑 → ⟨“ 𝐷 𝑇 𝐸 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝑇 𝑆 ”⟩ )
27 1 3 5 15 6 9 7 6 9 8 26 cgracom ⊢ ( 𝜑 → ⟨“ 𝐷 𝑇 𝑆 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝑇 𝐸 ”⟩ )
28 1 3 5 15 6 9 8 6 9 7 27 6 8 7 14 cgratr ⊢ ( 𝜑 → ⟨“ 𝐷 𝑇 𝑆 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝑆 𝐸 ”⟩ )
29 1 2 3 4 15 16 5 6 9 8 7 17 19 12 28 tgextan ⊢ ( 𝜑 → 𝜓 )