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	$⊢ P = {Base}_{G}$
	tgexta.m	$⊢ \underset{˙}{-} = dist (G)$
	tgexta.i	$⊢ I = Itv (G)$
	tgexta.l	$⊢ L = {Line}_{𝒢} (G)$
	tgexta.k	$⊢ K = {hl}_{𝒢} (G)$
	tgexta.s	$⊢ \underset{˙}{\leq} = \leq_{𝒢}^{∠} (G)$
	tgexta.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tgexta.a	$⊢ φ \to A \in P$
	tgexta.b	$⊢ φ \to B \in P$
	tgexta.c	$⊢ φ \to C \in P$
	tgexta.d	$⊢ φ \to D \in P$
	tgexta.1	$⊢ φ \to C \in (B I D)$
	tgexta.2	$⊢ φ \to \neg (A \in (B L C) \lor B = C)$
	tgexta.3	$⊢ φ \to C \neq D$
Assertion	tgexta	$⊢ φ \to ((⟨“ B A C ”⟩ \underset{˙}{\leq} ⟨“ A C D ”⟩ \land \neg ⟨“ B A C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A C D ”⟩) \land (⟨“ A B C ”⟩ \underset{˙}{\leq} ⟨“ A C D ”⟩ \land \neg ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A C D ”⟩))$

Proof

Step	Hyp	Ref	Expression
1		tgexta.p	$⊢ P = {Base}_{G}$
2		tgexta.m	$⊢ \underset{˙}{-} = dist (G)$
3		tgexta.i	$⊢ I = Itv (G)$
4		tgexta.l	$⊢ L = {Line}_{𝒢} (G)$
5		tgexta.k	$⊢ K = {hl}_{𝒢} (G)$
6		tgexta.s	$⊢ \underset{˙}{\leq} = \leq_{𝒢}^{∠} (G)$
7		tgexta.g	$⊢ φ \to G \in 𝒢_{Tarski}$
8		tgexta.a	$⊢ φ \to A \in P$
9		tgexta.b	$⊢ φ \to B \in P$
10		tgexta.c	$⊢ φ \to C \in P$
11		tgexta.d	$⊢ φ \to D \in P$
12		tgexta.1	$⊢ φ \to C \in (B I D)$
13		tgexta.2	$⊢ φ \to \neg (A \in (B L C) \lor B = C)$
14		tgexta.3	$⊢ φ \to C \neq D$
15	1 2 3 4 5 6 7 8 9 10 11 12 13 14	tgextalt1	$⊢ φ \to (⟨“ B A C ”⟩ \underset{˙}{\leq} ⟨“ A C D ”⟩ \land \neg ⟨“ B A C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A C D ”⟩)$
16	7	adantr	$⊢ (φ \land y \in P) \to G \in 𝒢_{Tarski}$
17	16	adantr	$⊢ ((φ \land y \in P) \land (C \in (A I y) \land C \underset{˙}{-} y = C \underset{˙}{-} A)) \to G \in 𝒢_{Tarski}$
18	8	adantr	$⊢ (φ \land y \in P) \to A \in P$
19	18	adantr	$⊢ ((φ \land y \in P) \land (C \in (A I y) \land C \underset{˙}{-} y = C \underset{˙}{-} A)) \to A \in P$
20	9	adantr	$⊢ (φ \land y \in P) \to B \in P$
21	20	adantr	$⊢ ((φ \land y \in P) \land (C \in (A I y) \land C \underset{˙}{-} y = C \underset{˙}{-} A)) \to B \in P$
22	10	adantr	$⊢ (φ \land y \in P) \to C \in P$
23	22	adantr	$⊢ ((φ \land y \in P) \land (C \in (A I y) \land C \underset{˙}{-} y = C \underset{˙}{-} A)) \to C \in P$
24	11	adantr	$⊢ (φ \land y \in P) \to D \in P$
25	24	adantr	$⊢ ((φ \land y \in P) \land (C \in (A I y) \land C \underset{˙}{-} y = C \underset{˙}{-} A)) \to D \in P$
26		simpl	$⊢ ((φ \land y \in P) \land (C \in (A I y) \land C \underset{˙}{-} y = C \underset{˙}{-} A)) \to (φ \land y \in P)$
27	26	simprd	$⊢ ((φ \land y \in P) \land (C \in (A I y) \land C \underset{˙}{-} y = C \underset{˙}{-} A)) \to y \in P$
28	12	adantr	$⊢ (φ \land y \in P) \to C \in (B I D)$
29	28	adantr	$⊢ ((φ \land y \in P) \land (C \in (A I y) \land C \underset{˙}{-} y = C \underset{˙}{-} A)) \to C \in (B I D)$
30		simpr	$⊢ ((φ \land y \in P) \land (C \in (A I y) \land C \underset{˙}{-} y = C \underset{˙}{-} A)) \to (C \in (A I y) \land C \underset{˙}{-} y = C \underset{˙}{-} A)$
31	30	simpld	$⊢ ((φ \land y \in P) \land (C \in (A I y) \land C \underset{˙}{-} y = C \underset{˙}{-} A)) \to C \in (A I y)$
32	13	adantr	$⊢ (φ \land y \in P) \to \neg (A \in (B L C) \lor B = C)$
33	32	adantr	$⊢ ((φ \land y \in P) \land (C \in (A I y) \land C \underset{˙}{-} y = C \underset{˙}{-} A)) \to \neg (A \in (B L C) \lor B = C)$
34	14	adantr	$⊢ (φ \land y \in P) \to C \neq D$
35	34	adantr	$⊢ ((φ \land y \in P) \land (C \in (A I y) \land C \underset{˙}{-} y = C \underset{˙}{-} A)) \to C \neq D$
36	30	simprd	$⊢ ((φ \land y \in P) \land (C \in (A I y) \land C \underset{˙}{-} y = C \underset{˙}{-} A)) \to C \underset{˙}{-} y = C \underset{˙}{-} A$
37	36	eqcomd	$⊢ ((φ \land y \in P) \land (C \in (A I y) \land C \underset{˙}{-} y = C \underset{˙}{-} A)) \to C \underset{˙}{-} A = C \underset{˙}{-} y$
38	1 3 4 7 8 9 10 13	ncolne2	$⊢ φ \to A \neq C$
39	38	necomd	$⊢ φ \to C \neq A$
40	39	adantr	$⊢ (φ \land y \in P) \to C \neq A$
41	40	adantr	$⊢ ((φ \land y \in P) \land (C \in (A I y) \land C \underset{˙}{-} y = C \underset{˙}{-} A)) \to C \neq A$
42	1 2 3 17 23 19 23 27 37 41	tgcgrneq	$⊢ ((φ \land y \in P) \land (C \in (A I y) \land C \underset{˙}{-} y = C \underset{˙}{-} A)) \to C \neq y$
43	1 2 3 4 5 6 17 19 21 23 25 27 29 31 33 35 42	tgextalt2	$⊢ ((φ \land y \in P) \land (C \in (A I y) \land C \underset{˙}{-} y = C \underset{˙}{-} A)) \to (⟨“ A B C ”⟩ \underset{˙}{\leq} ⟨“ A C D ”⟩ \land \neg ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A C D ”⟩)$
44	1 2 3 7 8 10 10 8	axtgsegcon	$⊢ φ \to \exists y \in P (C \in (A I y) \land C \underset{˙}{-} y = C \underset{˙}{-} A)$
45	43 44	r19.29a	$⊢ φ \to (⟨“ A B C ”⟩ \underset{˙}{\leq} ⟨“ A C D ”⟩ \land \neg ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A C D ”⟩)$
46	15 45	jca	$⊢ φ \to ((⟨“ B A C ”⟩ \underset{˙}{\leq} ⟨“ A C D ”⟩ \land \neg ⟨“ B A C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A C D ”⟩) \land (⟨“ A B C ”⟩ \underset{˙}{\leq} ⟨“ A C D ”⟩ \land \neg ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A C D ”⟩))$

Metamath Proof Explorer

Theorem tgexta

Proof