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

Proof

Step	Hyp	Ref	Expression
1		tgexta.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		tgexta.m	⊢ − = ( dist ‘ 𝐺 )
3		tgexta.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		tgexta.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
5		tgexta.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
6		tgexta.s	⊢ ≤ = ( ≤∠ ‘ 𝐺 )
7		tgexta.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
8		tgexta.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
9		tgexta.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
10		tgexta.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
11		tgexta.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
12		tgexta.1	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) )
13		tgexta.2	⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
14		tgexta.3	⊢ ( 𝜑 → 𝐶 ≠ 𝐷 )
15	1 2 3 4 5 6 7 8 9 10 11 12 13 14	tgextalt1	⊢ ( 𝜑 → ( ⟨“ 𝐵 𝐴 𝐶 ”⟩ ≤ ⟨“ 𝐴 𝐶 𝐷 ”⟩ ∧ ¬ ⟨“ 𝐵 𝐴 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) )
16	7	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) → 𝐺 ∈ TarskiG )
17	16	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐶 − 𝐴 ) ) ) → 𝐺 ∈ TarskiG )
18	8	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) → 𝐴 ∈ 𝑃 )
19	18	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐶 − 𝐴 ) ) ) → 𝐴 ∈ 𝑃 )
20	9	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) → 𝐵 ∈ 𝑃 )
21	20	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐶 − 𝐴 ) ) ) → 𝐵 ∈ 𝑃 )
22	10	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) → 𝐶 ∈ 𝑃 )
23	22	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐶 − 𝐴 ) ) ) → 𝐶 ∈ 𝑃 )
24	11	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) → 𝐷 ∈ 𝑃 )
25	24	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐶 − 𝐴 ) ) ) → 𝐷 ∈ 𝑃 )
26		simpl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐶 − 𝐴 ) ) ) → ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) )
27	26	simprd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐶 − 𝐴 ) ) ) → 𝑦 ∈ 𝑃 )
28	12	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) → 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) )
29	28	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐶 − 𝐴 ) ) ) → 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) )
30		simpr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐶 − 𝐴 ) ) ) → ( 𝐶 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐶 − 𝐴 ) ) )
31	30	simpld	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐶 − 𝐴 ) ) ) → 𝐶 ∈ ( 𝐴 𝐼 𝑦 ) )
32	13	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
33	32	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐶 − 𝐴 ) ) ) → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
34	14	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) → 𝐶 ≠ 𝐷 )
35	34	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐶 − 𝐴 ) ) ) → 𝐶 ≠ 𝐷 )
36	30	simprd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐶 − 𝐴 ) ) ) → ( 𝐶 − 𝑦 ) = ( 𝐶 − 𝐴 ) )
37	36	eqcomd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐶 − 𝐴 ) ) ) → ( 𝐶 − 𝐴 ) = ( 𝐶 − 𝑦 ) )
38	1 3 4 7 8 9 10 13	ncolne2	⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
39	38	necomd	⊢ ( 𝜑 → 𝐶 ≠ 𝐴 )
40	39	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) → 𝐶 ≠ 𝐴 )
41	40	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐶 − 𝐴 ) ) ) → 𝐶 ≠ 𝐴 )
42	1 2 3 17 23 19 23 27 37 41	tgcgrneq	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐶 − 𝐴 ) ) ) → 𝐶 ≠ 𝑦 )
43	1 2 3 4 5 6 17 19 21 23 25 27 29 31 33 35 42	tgextalt2	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐶 − 𝐴 ) ) ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ≤ ⟨“ 𝐴 𝐶 𝐷 ”⟩ ∧ ¬ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) )
44	1 2 3 7 8 10 10 8	axtgsegcon	⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝑃 ( 𝐶 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐶 − 𝑦 ) = ( 𝐶 − 𝐴 ) ) )
45	43 44	r19.29a	⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ≤ ⟨“ 𝐴 𝐶 𝐷 ”⟩ ∧ ¬ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) )
46	15 45	jca	⊢ ( 𝜑 → ( ( ⟨“ 𝐵 𝐴 𝐶 ”⟩ ≤ ⟨“ 𝐴 𝐶 𝐷 ”⟩ ∧ ¬ ⟨“ 𝐵 𝐴 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ≤ ⟨“ 𝐴 𝐶 𝐷 ”⟩ ∧ ¬ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) ) )