tgextancgra

Description: The exterior angle is NOT congruent to the remote interior angle -- the strictness tgextale cannot give, and what tgaas 's contradiction branch needs. The exterior angle is <" A C D "> , at the extension of B C beyond C . The tail of GeoCoq's l11__41__aux , run through acopyeu rather than conga__cop__or__out__ts : a congruent exterior angle would, by angle-construction uniqueness, put the midpoint-reflected point of tgmircgra on the ray C D -- the two rays make congruent angles with the shared base ray C A and, by tgextahp and hpgid , lie on the same open half-plane of line A C -- which tgextamirnhl forbids. Both of acopyeu 's non-collinearity hypotheses are discharged, not assumed: source side by rotating the triangle's own ncol , target side by tgextancd . (Contributed by JAG, 12-Aug-2026)

	Ref	Expression
Hypotheses	tgextalem1inag.p	$⊢ P = {Base}_{G}$
	tgextalem1inag.m	$⊢ \underset{˙}{-} = dist (G)$
	tgextalem1inag.i	$⊢ I = Itv (G)$
	tgextalem1inag.l	$⊢ L = {Line}_{𝒢} (G)$
	tgextalem1inag.k	$⊢ K = {hl}_{𝒢} (G)$
	tgextalem1inag.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tgextalem1inag.a	$⊢ φ \to A \in P$
	tgextalem1inag.b	$⊢ φ \to B \in P$
	tgextalem1inag.c	$⊢ φ \to C \in P$
	tgextalem1inag.d	$⊢ φ \to D \in P$
	tgextalem1inag.ext	$⊢ φ \to C \in (B I D)$
	tgextalem1inag.ncol	$⊢ φ \to \neg (A \in (B L C) \lor B = C)$
	tgextalem1inag.ne	$⊢ φ \to C \neq D$
Assertion	tgextancgra	$⊢ φ \to \neg ⟨“ C A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A C D ”⟩$

Proof

Step	Hyp	Ref	Expression
1		tgextalem1inag.p	$⊢ P = {Base}_{G}$
2		tgextalem1inag.m	$⊢ \underset{˙}{-} = dist (G)$
3		tgextalem1inag.i	$⊢ I = Itv (G)$
4		tgextalem1inag.l	$⊢ L = {Line}_{𝒢} (G)$
5		tgextalem1inag.k	$⊢ K = {hl}_{𝒢} (G)$
6		tgextalem1inag.g	$⊢ φ \to G \in 𝒢_{Tarski}$
7		tgextalem1inag.a	$⊢ φ \to A \in P$
8		tgextalem1inag.b	$⊢ φ \to B \in P$
9		tgextalem1inag.c	$⊢ φ \to C \in P$
10		tgextalem1inag.d	$⊢ φ \to D \in P$
11		tgextalem1inag.ext	$⊢ φ \to C \in (B I D)$
12		tgextalem1inag.ncol	$⊢ φ \to \neg (A \in (B L C) \lor B = C)$
13		tgextalem1inag.ne	$⊢ φ \to C \neq D$
14	1 2 3 4 5 6 7 8 9 10 11 12 13	tgextamirnhl	$⊢ φ \to \neg D K (C) {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) C) (B)$
15	6	adantr	$⊢ (φ \land ⟨“ C A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A C D ”⟩) \to G \in 𝒢_{Tarski}$
16	9	adantr	$⊢ (φ \land ⟨“ C A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A C D ”⟩) \to C \in P$
17	7	adantr	$⊢ (φ \land ⟨“ C A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A C D ”⟩) \to A \in P$
18	8	adantr	$⊢ (φ \land ⟨“ C A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A C D ”⟩) \to B \in P$
19	10	adantr	$⊢ (φ \land ⟨“ C A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A C D ”⟩) \to D \in P$
20	1 4 3 6 8 9 7 12	ncolrot1	$⊢ φ \to \neg (B \in (C L A) \lor C = A)$
21	1 4 3 6 9 7 8 20	ncolrot1	$⊢ φ \to \neg (C \in (A L B) \lor A = B)$
22	21	adantr	$⊢ (φ \land ⟨“ C A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A C D ”⟩) \to \neg (C \in (A L B) \lor A = B)$
23	1 2 3 4 6 7 8 9 10 11 12 13	tgextancd	$⊢ φ \to \neg (A \in (C L D) \lor C = D)$
24	23	adantr	$⊢ (φ \land ⟨“ C A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A C D ”⟩) \to \neg (A \in (C L D) \lor C = D)$
25		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
26	1 4 3 6 8 9 7 12	ncoltgdim2	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
27	1 2 3 6 26 7 9	midcl	$⊢ φ \to A {mid}_{𝒢} (G) C \in P$
28		eqid	$⊢ {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) C) = {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) C)$
29	1 2 3 4 25 6 27 28 8	mircl	$⊢ φ \to {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) C) (B) \in P$
30	29	adantr	$⊢ (φ \land ⟨“ C A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A C D ”⟩) \to {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) C) (B) \in P$
31		simpr	$⊢ (φ \land ⟨“ C A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A C D ”⟩) \to ⟨“ C A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A C D ”⟩$
32	1 2 3 4 6 7 8 9 12	tgmircgra	$⊢ φ \to ⟨“ C A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A C {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) C) (B) ”⟩$
33	32	adantr	$⊢ (φ \land ⟨“ C A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A C D ”⟩) \to ⟨“ C A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A C {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) C) (B) ”⟩$
34	1 3 4 6 7 8 9 12	ncolne2	$⊢ φ \to A \neq C$
35	1 3 4 6 7 9 34	tgelrnln	$⊢ φ \to A L C \in ran L$
36		simpl	$⊢ (u = a \land v = b) \to u = a$
37	36	eleq1d	$⊢ (u = a \land v = b) \to (u \in (P ∖ (A L C)) \leftrightarrow a \in (P ∖ (A L C)))$
38		simpr	$⊢ (u = a \land v = b) \to v = b$
39	38	eleq1d	$⊢ (u = a \land v = b) \to (v \in (P ∖ (A L C)) \leftrightarrow b \in (P ∖ (A L C)))$
40	37 39	anbi12d	$⊢ (u = a \land v = b) \to ((u \in (P ∖ (A L C)) \land v \in (P ∖ (A L C))) \leftrightarrow (a \in (P ∖ (A L C)) \land b \in (P ∖ (A L C))))$
41		simpr	$⊢ ((u = a \land v = b) \land w = t) \to w = t$
42		simpll	$⊢ ((u = a \land v = b) \land w = t) \to u = a$
43		simplr	$⊢ ((u = a \land v = b) \land w = t) \to v = b$
44	42 43	oveq12d	$⊢ ((u = a \land v = b) \land w = t) \to u I v = a I b$
45	41 44	eleq12d	$⊢ ((u = a \land v = b) \land w = t) \to (w \in (u I v) \leftrightarrow t \in (a I b))$
46	45	cbvrexdva	$⊢ (u = a \land v = b) \to (\exists w \in (A L C) w \in (u I v) \leftrightarrow \exists t \in (A L C) t \in (a I b))$
47	40 46	anbi12d	$⊢ (u = a \land v = b) \to (((u \in (P ∖ (A L C)) \land v \in (P ∖ (A L C))) \land \exists w \in (A L C) w \in (u I v)) \leftrightarrow ((a \in (P ∖ (A L C)) \land b \in (P ∖ (A L C))) \land \exists t \in (A L C) t \in (a I b)))$
48	47	cbvopabv	$⊢ \{⟨u, v⟩ \| ((u \in (P ∖ (A L C)) \land v \in (P ∖ (A L C))) \land \exists w \in (A L C) w \in (u I v))\} = \{⟨a, b⟩ \| ((a \in (P ∖ (A L C)) \land b \in (P ∖ (A L C))) \land \exists t \in (A L C) t \in (a I b))\}$
49		ioran	$⊢ \neg (A \in (C L D) \lor C = D) \leftrightarrow (\neg A \in (C L D) \land \neg C = D)$
50	23 49	sylib	$⊢ φ \to (\neg A \in (C L D) \land \neg C = D)$
51	50	simpld	$⊢ φ \to \neg A \in (C L D)$
52	34	necomd	$⊢ φ \to C \neq A$
53	1 3 4 6 9 7 52	tglinerflx2	$⊢ φ \to A \in (C L A)$
54	53	adantr	$⊢ (φ \land D \in (A L C)) \to A \in (C L A)$
55	6	adantr	$⊢ (φ \land D \in (A L C)) \to G \in 𝒢_{Tarski}$
56	9	adantr	$⊢ (φ \land D \in (A L C)) \to C \in P$
57	7	adantr	$⊢ (φ \land D \in (A L C)) \to A \in P$
58	52	adantr	$⊢ (φ \land D \in (A L C)) \to C \neq A$
59	10	adantr	$⊢ (φ \land D \in (A L C)) \to D \in P$
60	13	necomd	$⊢ φ \to D \neq C$
61	60	adantr	$⊢ (φ \land D \in (A L C)) \to D \neq C$
62		simpr	$⊢ (φ \land D \in (A L C)) \to D \in (A L C)$
63	34	adantr	$⊢ (φ \land D \in (A L C)) \to A \neq C$
64	1 3 4 55 57 56 63	tglinecom	$⊢ (φ \land D \in (A L C)) \to A L C = C L A$
65	62 64	eleqtrd	$⊢ (φ \land D \in (A L C)) \to D \in (C L A)$
66	1 3 4 55 56 57 58 59 61 65	tglineelsb2	$⊢ (φ \land D \in (A L C)) \to C L A = C L D$
67	54 66	eleqtrd	$⊢ (φ \land D \in (A L C)) \to A \in (C L D)$
68	51 67	mtand	$⊢ φ \to \neg D \in (A L C)$
69	1 3 4 6 35 10 48 68	hpgid	$⊢ φ \to D {hp}_{𝒢} (G) (A L C) D$
70	69	adantr	$⊢ (φ \land ⟨“ C A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A C D ”⟩) \to D {hp}_{𝒢} (G) (A L C) D$
71	1 2 3 4 5 6 7 8 9 10 11 12 13	tgextahp	$⊢ φ \to {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) C) (B) {hp}_{𝒢} (G) (A L C) D$
72	71	adantr	$⊢ (φ \land ⟨“ C A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A C D ”⟩) \to {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) C) (B) {hp}_{𝒢} (G) (A L C) D$
73	1 3 2 15 16 17 18 17 16 19 4 22 24 19 30 5 31 33 70 72	acopyeu	$⊢ (φ \land ⟨“ C A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A C D ”⟩) \to D K (C) {pInv}_{𝒢} (G) (A {mid}_{𝒢} (G) C) (B)$
74	14 73	mtand	$⊢ φ \to \neg ⟨“ C A B ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A C D ”⟩$

Metamath Proof Explorer

Theorem tgextancgra

Proof