tgextancd

Description: The target-side non-collinearity of the exterior angle. Line C D is line C B -- C lies between B and D , and C =/= D -- so A is off it exactly because the triangle is non-degenerate. This is acopyeu 's acopy.2 frame hypothesis in tgextancgra , and it is what excludes isinag 's x = C branch in tgextahp . (Contributed by JAG, 12-Aug-2026)

	Ref	Expression
Hypotheses	tgextancd.p	$⊢ P = {Base}_{G}$
	tgextancd.m	$⊢ \underset{˙}{-} = dist (G)$
	tgextancd.i	$⊢ I = Itv (G)$
	tgextancd.l	$⊢ L = {Line}_{𝒢} (G)$
	tgextancd.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tgextancd.a	$⊢ φ \to A \in P$
	tgextancd.b	$⊢ φ \to B \in P$
	tgextancd.c	$⊢ φ \to C \in P$
	tgextancd.d	$⊢ φ \to D \in P$
	tgextancd.ext	$⊢ φ \to C \in (B I D)$
	tgextancd.ncol	$⊢ φ \to \neg (A \in (B L C) \lor B = C)$
	tgextancd.ne	$⊢ φ \to C \neq D$
Assertion	tgextancd	$⊢ φ \to \neg (A \in (C L D) \lor C = D)$

Proof

Step	Hyp	Ref	Expression
1		tgextancd.p	$⊢ P = {Base}_{G}$
2		tgextancd.m	$⊢ \underset{˙}{-} = dist (G)$
3		tgextancd.i	$⊢ I = Itv (G)$
4		tgextancd.l	$⊢ L = {Line}_{𝒢} (G)$
5		tgextancd.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		tgextancd.a	$⊢ φ \to A \in P$
7		tgextancd.b	$⊢ φ \to B \in P$
8		tgextancd.c	$⊢ φ \to C \in P$
9		tgextancd.d	$⊢ φ \to D \in P$
10		tgextancd.ext	$⊢ φ \to C \in (B I D)$
11		tgextancd.ncol	$⊢ φ \to \neg (A \in (B L C) \lor B = C)$
12		tgextancd.ne	$⊢ φ \to C \neq D$
13	1 4 3 5 7 8 6 11	ncolcom	$⊢ φ \to \neg (A \in (C L B) \lor C = B)$
14		ioran	$⊢ \neg (A \in (C L B) \lor C = B) \leftrightarrow (\neg A \in (C L B) \land \neg C = B)$
15	13 14	sylib	$⊢ φ \to (\neg A \in (C L B) \land \neg C = B)$
16	15	simpld	$⊢ φ \to \neg A \in (C L B)$
17	15	simprd	$⊢ φ \to \neg C = B$
18	17	neqned	$⊢ φ \to C \neq B$
19	12	necomd	$⊢ φ \to D \neq C$
20	1 2 3 5 7 8 9 10	tgbtwncom	$⊢ φ \to C \in (D I B)$
21	1 4 3 5 8 7 9 20	btwncolg2	$⊢ φ \to (D \in (C L B) \lor C = B)$
22	21 17	olcnd	$⊢ φ \to D \in (C L B)$
23	1 3 4 5 8 7 18 9 19 22	tglineelsb2	$⊢ φ \to C L B = C L D$
24	23	eleq2d	$⊢ φ \to (A \in (C L B) \leftrightarrow A \in (C L D))$
25	16 24	mtbid	$⊢ φ \to \neg A \in (C L D)$
26	12	neneqd	$⊢ φ \to \neg C = D$
27	25 26	jca	$⊢ φ \to (\neg A \in (C L D) \land \neg C = D)$
28		ioran	$⊢ \neg (A \in (C L D) \lor C = D) \leftrightarrow (\neg A \in (C L D) \land \neg C = D)$
29	27 28	sylibr	$⊢ φ \to \neg (A \in (C L D) \lor C = D)$

Metamath Proof Explorer

Theorem tgextancd

Proof