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 = ( Base ` G )
	tgextalem1inag.m	\|- .- = ( dist ` G )
	tgextalem1inag.i	\|- I = ( Itv ` G )
	tgextalem1inag.l	\|- L = ( LineG ` G )
	tgextalem1inag.k	\|- K = ( hlG ` G )
	tgextalem1inag.g	\|- ( ph -> G e. TarskiG )
	tgextalem1inag.a	\|- ( ph -> A e. P )
	tgextalem1inag.b	\|- ( ph -> B e. P )
	tgextalem1inag.c	\|- ( ph -> C e. P )
	tgextalem1inag.d	\|- ( ph -> D e. P )
	tgextalem1inag.ext	\|- ( ph -> C e. ( B I D ) )
	tgextalem1inag.ncol	\|- ( ph -> -. ( A e. ( B L C ) \/ B = C ) )
	tgextalem1inag.ne	\|- ( ph -> C =/= D )
Assertion	tgextale	\|- ( ph -> <" C A B "> ( leA ` G ) <" A C D "> )

Proof

Step	Hyp	Ref	Expression
1		tgextalem1inag.p	\|- P = ( Base ` G )
2		tgextalem1inag.m	\|- .- = ( dist ` G )
3		tgextalem1inag.i	\|- I = ( Itv ` G )
4		tgextalem1inag.l	\|- L = ( LineG ` G )
5		tgextalem1inag.k	\|- K = ( hlG ` G )
6		tgextalem1inag.g	\|- ( ph -> G e. TarskiG )
7		tgextalem1inag.a	\|- ( ph -> A e. P )
8		tgextalem1inag.b	\|- ( ph -> B e. P )
9		tgextalem1inag.c	\|- ( ph -> C e. P )
10		tgextalem1inag.d	\|- ( ph -> D e. P )
11		tgextalem1inag.ext	\|- ( ph -> C e. ( B I D ) )
12		tgextalem1inag.ncol	\|- ( ph -> -. ( A e. ( B L C ) \/ B = C ) )
13		tgextalem1inag.ne	\|- ( ph -> C =/= D )
14		eqid	\|- ( pInvG ` G ) = ( pInvG ` G )
15	1 4 3 6 8 9 7 12	ncoltgdim2	\|- ( ph -> G TarskiGDim>= 2 )
16	1 2 3 6 15 7 9	midcl	\|- ( ph -> ( A ( midG ` G ) C ) e. P )
17		eqid	\|- ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) = ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) )
18	1 2 3 4 14 6 16 17 8	mircl	\|- ( ph -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) e. P )
19	1 2 3 4 5 6 7 8 9 10 11 12 13	tgextalem1inag	\|- ( ph -> ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) ( inA ` G ) <" A C D "> )
20	1 3 5 6 7 9 18 10 19	inaglea	\|- ( ph -> <" A C ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) "> ( leA ` G ) <" A C D "> )
21	1 2 3 4 6 7 8 9 12	tgmircgra	\|- ( ph -> <" C A B "> ( cgrA ` G ) <" A C ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) "> )
22	1 3 6 5 9 7 8 7 9 18 21	cgracom	\|- ( ph -> <" A C ( ( ( pInvG ` G ) ` ( A ( midG ` G ) C ) ) ` B ) "> ( cgrA ` G ) <" C A B "> )
23	1 3 5 6 7 9 18 7 9 10 9 7 8 20 22	leacgra1	\|- ( ph -> <" C A B "> ( leA ` G ) <" A C D "> )

Metamath Proof Explorer

Theorem tgextale

Proof