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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	tgextalt1.m	⊢ − = ( dist ‘ 𝐺 )
	tgextalt1.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tgextalt1.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	tgextalt1.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
	tgextalt1.s	⊢ ≤ = ( ≤∠ ‘ 𝐺 )
	tgextalt1.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tgextalt1.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	tgextalt1.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	tgextalt1.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	tgextalt1.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
	tgextalt1.ext	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) )
	tgextalt1.ncol	⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
	tgextalt1.ne	⊢ ( 𝜑 → 𝐶 ≠ 𝐷 )
Assertion	tgextalt1	⊢ ( 𝜑 → ( ⟨“ 𝐵 𝐴 𝐶 ”⟩ ≤ ⟨“ 𝐴 𝐶 𝐷 ”⟩ ∧ ¬ ⟨“ 𝐵 𝐴 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		tgextalt1.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		tgextalt1.m	⊢ − = ( dist ‘ 𝐺 )
3		tgextalt1.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		tgextalt1.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
5		tgextalt1.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
6		tgextalt1.s	⊢ ≤ = ( ≤∠ ‘ 𝐺 )
7		tgextalt1.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
8		tgextalt1.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
9		tgextalt1.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
10		tgextalt1.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
11		tgextalt1.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
12		tgextalt1.ext	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) )
13		tgextalt1.ncol	⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
14		tgextalt1.ne	⊢ ( 𝜑 → 𝐶 ≠ 𝐷 )
15	1 2 3 4 5 7 8 9 10 11 12 13 14	tgextale	⊢ ( 𝜑 → ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ )
16	1 3 4 7 8 9 10 13	ncolne2	⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
17	16	necomd	⊢ ( 𝜑 → 𝐶 ≠ 𝐴 )
18	1 3 4 7 8 9 10 13	ncolne1	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
19	1 3 7 5 10 8 9 17 18	cgraswap	⊢ ( 𝜑 → ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐵 𝐴 𝐶 ”⟩ )
20	1 3 5 7 10 8 9 8 10 11 9 8 10 15 19	leacgra1	⊢ ( 𝜑 → ⟨“ 𝐵 𝐴 𝐶 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ )
21	6	breqi	⊢ ( ⟨“ 𝐵 𝐴 𝐶 ”⟩ ≤ ⟨“ 𝐴 𝐶 𝐷 ”⟩ ↔ ⟨“ 𝐵 𝐴 𝐶 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ )
22	20 21	sylibr	⊢ ( 𝜑 → ⟨“ 𝐵 𝐴 𝐶 ”⟩ ≤ ⟨“ 𝐴 𝐶 𝐷 ”⟩ )
23	1 2 3 4 5 7 8 9 10 11 12 13 14	tgextancgra	⊢ ( 𝜑 → ¬ ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ )
24	7	adantr	⊢ ( ( 𝜑 ∧ ⟨“ 𝐵 𝐴 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → 𝐺 ∈ TarskiG )
25	10	adantr	⊢ ( ( 𝜑 ∧ ⟨“ 𝐵 𝐴 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → 𝐶 ∈ 𝑃 )
26	8	adantr	⊢ ( ( 𝜑 ∧ ⟨“ 𝐵 𝐴 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → 𝐴 ∈ 𝑃 )
27	9	adantr	⊢ ( ( 𝜑 ∧ ⟨“ 𝐵 𝐴 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → 𝐵 ∈ 𝑃 )
28	19	adantr	⊢ ( ( 𝜑 ∧ ⟨“ 𝐵 𝐴 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐵 𝐴 𝐶 ”⟩ )
29	11	adantr	⊢ ( ( 𝜑 ∧ ⟨“ 𝐵 𝐴 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → 𝐷 ∈ 𝑃 )
30		simpr	⊢ ( ( 𝜑 ∧ ⟨“ 𝐵 𝐴 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → ⟨“ 𝐵 𝐴 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ )
31	1 3 24 5 25 26 27 27 26 25 28 26 25 29 30	cgratr	⊢ ( ( 𝜑 ∧ ⟨“ 𝐵 𝐴 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ )
32	23 31	mtand	⊢ ( 𝜑 → ¬ ⟨“ 𝐵 𝐴 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ )
33	22 32	jca	⊢ ( 𝜑 → ( ⟨“ 𝐵 𝐴 𝐶 ”⟩ ≤ ⟨“ 𝐴 𝐶 𝐷 ”⟩ ∧ ¬ ⟨“ 𝐵 𝐴 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) )