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

Proof

Step	Hyp	Ref	Expression
1		tgextancd.p	\|- P = ( Base ` G )
2		tgextancd.m	\|- .- = ( dist ` G )
3		tgextancd.i	\|- I = ( Itv ` G )
4		tgextancd.l	\|- L = ( LineG ` G )
5		tgextancd.g	\|- ( ph -> G e. TarskiG )
6		tgextancd.a	\|- ( ph -> A e. P )
7		tgextancd.b	\|- ( ph -> B e. P )
8		tgextancd.c	\|- ( ph -> C e. P )
9		tgextancd.d	\|- ( ph -> D e. P )
10		tgextancd.ext	\|- ( ph -> C e. ( B I D ) )
11		tgextancd.ncol	\|- ( ph -> -. ( A e. ( B L C ) \/ B = C ) )
12		tgextancd.ne	\|- ( ph -> C =/= D )
13	1 4 3 5 7 8 6 11	ncolcom	\|- ( ph -> -. ( A e. ( C L B ) \/ C = B ) )
14		ioran	\|- ( -. ( A e. ( C L B ) \/ C = B ) <-> ( -. A e. ( C L B ) /\ -. C = B ) )
15	13 14	sylib	\|- ( ph -> ( -. A e. ( C L B ) /\ -. C = B ) )
16	15	simpld	\|- ( ph -> -. A e. ( C L B ) )
17	15	simprd	\|- ( ph -> -. C = B )
18	17	neqned	\|- ( ph -> C =/= B )
19	12	necomd	\|- ( ph -> D =/= C )
20	1 2 3 5 7 8 9 10	tgbtwncom	\|- ( ph -> C e. ( D I B ) )
21	1 4 3 5 8 7 9 20	btwncolg2	\|- ( ph -> ( D e. ( C L B ) \/ C = B ) )
22	21 17	olcnd	\|- ( ph -> D e. ( C L B ) )
23	1 3 4 5 8 7 18 9 19 22	tglineelsb2	\|- ( ph -> ( C L B ) = ( C L D ) )
24	23	eleq2d	\|- ( ph -> ( A e. ( C L B ) <-> A e. ( C L D ) ) )
25	16 24	mtbid	\|- ( ph -> -. A e. ( C L D ) )
26	12	neneqd	\|- ( ph -> -. C = D )
27	25 26	jca	\|- ( ph -> ( -. A e. ( C L D ) /\ -. C = D ) )
28		ioran	\|- ( -. ( A e. ( C L D ) \/ C = D ) <-> ( -. A e. ( C L D ) /\ -. C = D ) )
29	27 28	sylibr	\|- ( ph -> -. ( A e. ( C L D ) \/ C = D ) )

Metamath Proof Explorer

Theorem tgextancd

Proof