Theorem cgranbtwn

Description: Null angle implies betweenness. (Contributed by SS, 4-Jun-2026)

	Ref	Expression
Hypotheses	cgranbtwn.p	|- P = ( Base ` G )
	cgranbtwn.i	|- I = ( Itv ` G )
	cgranbtwn.g	|- ( ph -> G e. TarskiG )
	cgranbtwn.a	|- ( ph -> A e. P )
	cgranbtwn.b	|- ( ph -> B e. P )
	cgranbtwn.c	|- ( ph -> C e. P )
	cgranbtwn.d	|- ( ph -> D e. P )
	cgranbtwn.e	|- ( ph -> E e. P )
	cgranbtwn.f	|- ( ph -> F e. P )
	cgranbtwn.1	|- ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
	cgranbtwn.2	|- ( ph -> A e. ( B I C ) )
Assertion	cgranbtwn	|- ( ph -> ( D e. ( E I F ) \/ F e. ( E I D ) ) )

Proof

Step	Hyp	Ref	Expression
1		cgranbtwn.p	|- P = ( Base ` G )
2		cgranbtwn.i	|- I = ( Itv ` G )
3		cgranbtwn.g	|- ( ph -> G e. TarskiG )
4		cgranbtwn.a	|- ( ph -> A e. P )
5		cgranbtwn.b	|- ( ph -> B e. P )
6		cgranbtwn.c	|- ( ph -> C e. P )
7		cgranbtwn.d	|- ( ph -> D e. P )
8		cgranbtwn.e	|- ( ph -> E e. P )
9		cgranbtwn.f	|- ( ph -> F e. P )
10		cgranbtwn.1	|- ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
11		cgranbtwn.2	|- ( ph -> A e. ( B I C ) )
12		eqid	|- ( dist ` G ) = ( dist ` G )
13		eqid	|- ( hlG ` G ) = ( hlG ` G )
14	1 2 13 3 4 5 6 7 8 9 10	cgrane2	|- ( ph -> B =/= C )
15	1 2 13 3 4 5 6 7 8 9 10	cgrane1	|- ( ph -> A =/= B )
16	1 2 13 5 6 4 3 4 11 14 15	btwnhl1	|- ( ph -> A ( ( hlG ` G ) ` B ) C )
17	1 2 12 3 4 5 6 7 8 9 10 13 16	cgrahl	|- ( ph -> D ( ( hlG ` G ) ` E ) F )
18	1 2 13 7 9 8 3	ishlg	|- ( ph -> ( D ( ( hlG ` G ) ` E ) F <-> ( D =/= E /\ F =/= E /\ ( D e. ( E I F ) \/ F e. ( E I D ) ) ) ) )
19	17 18	mpbid	|- ( ph -> ( D =/= E /\ F =/= E /\ ( D e. ( E I F ) \/ F e. ( E I D ) ) ) )
20	19	simp3d	|- ( ph -> ( D e. ( E I F ) \/ F e. ( E I D ) ) )