Theorem tgextale

Description: The non-strict exterior-angle bound, a checkpoint only. tgmircgra gives the reflected copy of the interior angle, tgextalem1inag puts that copy inside the exterior angle; inaglea turns "inside" into leA and leacgra1 transports the bound along the congruence (flipped with cgracom ). No new geometry. This bound is deliberately too weak for tgaas , whose contradiction branch already holds an angle congruence and so satisfies leA for free -- strictness comes later, and only tgexta is the exterior-angle theorem. (Contributed by JAG, 12-Aug-2026)

	Ref	Expression
Hypotheses	tgextalem1inag.p	$$⊢P={\mathrm{Base}}_G$$
	tgextalem1inag.m	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	tgextalem1inag.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	tgextalem1inag.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	tgextalem1inag.k	$$⊢K={hl}_{𝒢}\left(G\right)$$
	tgextalem1inag.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	tgextalem1inag.a	$$⊢\phi \to A\in P$$
	tgextalem1inag.b	$$⊢\phi \to B\in P$$
	tgextalem1inag.c	$$⊢\phi \to C\in P$$
	tgextalem1inag.d	$$⊢\phi \to D\in P$$
	tgextalem1inag.ext	$$⊢\phi \to C\in \left(BID\right)$$
	tgextalem1inag.ncol	$$⊢\phi \to \neg \left(A\in \left(BLC\right)\vee B=C\right)$$
	tgextalem1inag.ne	$$⊢\phi \to C\ne D$$
Assertion	tgextale	$$⊢\phi \to ⟨“CAB”⟩{\le }_{𝒢}^{\angle }\left(G\right)⟨“ACD”⟩$$

Proof

Step	Hyp	Ref	Expression
1		tgextalem1inag.p	$$⊢P={\mathrm{Base}}_G$$
2		tgextalem1inag.m	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		tgextalem1inag.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		tgextalem1inag.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
5		tgextalem1inag.k	$$⊢K={hl}_{𝒢}\left(G\right)$$
6		tgextalem1inag.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
7		tgextalem1inag.a	$$⊢\phi \to A\in P$$
8		tgextalem1inag.b	$$⊢\phi \to B\in P$$
9		tgextalem1inag.c	$$⊢\phi \to C\in P$$
10		tgextalem1inag.d	$$⊢\phi \to D\in P$$
11		tgextalem1inag.ext	$$⊢\phi \to C\in \left(BID\right)$$
12		tgextalem1inag.ncol	$$⊢\phi \to \neg \left(A\in \left(BLC\right)\vee B=C\right)$$
13		tgextalem1inag.ne	$$⊢\phi \to C\ne D$$
14		eqid	$$⊢{pInv}_{𝒢}\left(G\right)={pInv}_{𝒢}\left(G\right)$$
15	1 4 3 6 8 9 7 12	ncoltgdim2	$$⊢\phi \to G{\mathrm{Dim}}_{𝒢}\ge 2$$
16	1 2 3 6 15 7 9	midcl	$$⊢\phi \to A{mid}_{𝒢}\left(G\right)C\in P$$
17		eqid	$$⊢{pInv}_{𝒢}\left(G\right)\left(A{mid}_{𝒢}\left(G\right)C\right)={pInv}_{𝒢}\left(G\right)\left(A{mid}_{𝒢}\left(G\right)C\right)$$
18	1 2 3 4 14 6 16 17 8	mircl	$$⊢\phi \to {pInv}_{𝒢}\left(G\right)\left(A{mid}_{𝒢}\left(G\right)C\right)\left(B\right)\in P$$
19	1 2 3 4 5 6 7 8 9 10 11 12 13	tgextalem1inag	$$⊢\phi \to {pInv}_{𝒢}\left(G\right)\left(A{mid}_{𝒢}\left(G\right)C\right)\left(B\right){\in }_{𝒢}^{\angle }\left(G\right)⟨“ACD”⟩$$
20	1 3 5 6 7 9 18 10 19	inaglea	$$⊢\phi \to ⟨“AC{pInv}_{𝒢}\left(G\right)\left(A{mid}_{𝒢}\left(G\right)C\right)\left(B\right)”⟩{\le }_{𝒢}^{\angle }\left(G\right)⟨“ACD”⟩$$
21	1 2 3 4 6 7 8 9 12	tgmircgra	$$⊢\phi \to ⟨“CAB”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“AC{pInv}_{𝒢}\left(G\right)\left(A{mid}_{𝒢}\left(G\right)C\right)\left(B\right)”⟩$$
22	1 3 6 5 9 7 8 7 9 18 21	cgracom	$$⊢\phi \to ⟨“AC{pInv}_{𝒢}\left(G\right)\left(A{mid}_{𝒢}\left(G\right)C\right)\left(B\right)”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“CAB”⟩$$
23	1 3 5 6 7 9 18 7 9 10 9 7 8 20 22	leacgra1	$$⊢\phi \to ⟨“CAB”⟩{\le }_{𝒢}^{\angle }\left(G\right)⟨“ACD”⟩$$