brsegle2

Description: Alternate characterization of segment comparison. Theorem 5.5 of Schwabhauser p. 41-42. (Contributed by Scott Fenton, 11-Oct-2013)

		Ref	Expression
	Assertion	brsegle2	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩ \leftrightarrow \exists x \in 𝔼 (N) (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩))$

Proof

Step	Hyp	Ref	Expression
1		brsegle	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩ \leftrightarrow \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))$
2		simprl	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)) \to y Btwn ⟨C, D⟩$
3		simpl1	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land y \in 𝔼 (N)) \to N \in ℕ$
4		simpl3l	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land y \in 𝔼 (N)) \to C \in 𝔼 (N)$
5		simpl3r	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land y \in 𝔼 (N)) \to D \in 𝔼 (N)$
6		simpr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land y \in 𝔼 (N)) \to y \in 𝔼 (N)$
7		btwncolinear2	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land y \in 𝔼 (N))) \to (y Btwn ⟨C, D⟩ \to C Colinear ⟨y, D⟩)$
8	3 4 5 6 7	syl13anc	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land y \in 𝔼 (N)) \to (y Btwn ⟨C, D⟩ \to C Colinear ⟨y, D⟩)$
9	8	adantr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)) \to (y Btwn ⟨C, D⟩ \to C Colinear ⟨y, D⟩)$
10	2 9	mpd	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)) \to C Colinear ⟨y, D⟩$
11		simpl2l	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land y \in 𝔼 (N)) \to A \in 𝔼 (N)$
12		simpl2r	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land y \in 𝔼 (N)) \to B \in 𝔼 (N)$
13		simprr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)) \to ⟨A, B⟩ Cgr ⟨C, y⟩$
14	3 11 12 4 6 13	cgrcomand	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)) \to ⟨C, y⟩ Cgr ⟨A, B⟩$
15		simpl2	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land y \in 𝔼 (N)) \to (A \in 𝔼 (N) \land B \in 𝔼 (N))$
16		lineext	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land y \in 𝔼 (N) \land D \in 𝔼 (N)) \land (A \in 𝔼 (N) \land B \in 𝔼 (N))) \to ((C Colinear ⟨y, D⟩ \land ⟨C, y⟩ Cgr ⟨A, B⟩) \to \exists x \in 𝔼 (N) ⟨C, ⟨y, D⟩⟩ Cgr3 ⟨A, ⟨B, x⟩⟩)$
17	3 4 6 5 15 16	syl131anc	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land y \in 𝔼 (N)) \to ((C Colinear ⟨y, D⟩ \land ⟨C, y⟩ Cgr ⟨A, B⟩) \to \exists x \in 𝔼 (N) ⟨C, ⟨y, D⟩⟩ Cgr3 ⟨A, ⟨B, x⟩⟩)$
18	17	adantr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)) \to ((C Colinear ⟨y, D⟩ \land ⟨C, y⟩ Cgr ⟨A, B⟩) \to \exists x \in 𝔼 (N) ⟨C, ⟨y, D⟩⟩ Cgr3 ⟨A, ⟨B, x⟩⟩)$
19	10 14 18	mp2and	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)) \to \exists x \in 𝔼 (N) ⟨C, ⟨y, D⟩⟩ Cgr3 ⟨A, ⟨B, x⟩⟩$
20		an32	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land y \in 𝔼 (N)) \land x \in 𝔼 (N)) \leftrightarrow (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N))$
21		simpll1	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \to N \in ℕ$
22		simpl3l	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to C \in 𝔼 (N)$
23	22	adantr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \to C \in 𝔼 (N)$
24		simpr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \to y \in 𝔼 (N)$
25		simpl3r	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to D \in 𝔼 (N)$
26	25	adantr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \to D \in 𝔼 (N)$
27		simpl2l	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to A \in 𝔼 (N)$
28	27	adantr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \to A \in 𝔼 (N)$
29		simpl2r	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to B \in 𝔼 (N)$
30	29	adantr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \to B \in 𝔼 (N)$
31		simplr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \to x \in 𝔼 (N)$
32		brcgr3	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land y \in 𝔼 (N) \land D \in 𝔼 (N)) \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land x \in 𝔼 (N))) \to (⟨C, ⟨y, D⟩⟩ Cgr3 ⟨A, ⟨B, x⟩⟩ \leftrightarrow (⟨C, y⟩ Cgr ⟨A, B⟩ \land ⟨C, D⟩ Cgr ⟨A, x⟩ \land ⟨y, D⟩ Cgr ⟨B, x⟩))$
33	21 23 24 26 28 30 31 32	syl133anc	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \to (⟨C, ⟨y, D⟩⟩ Cgr3 ⟨A, ⟨B, x⟩⟩ \leftrightarrow (⟨C, y⟩ Cgr ⟨A, B⟩ \land ⟨C, D⟩ Cgr ⟨A, x⟩ \land ⟨y, D⟩ Cgr ⟨B, x⟩))$
34	33	adantr	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)) \to (⟨C, ⟨y, D⟩⟩ Cgr3 ⟨A, ⟨B, x⟩⟩ \leftrightarrow (⟨C, y⟩ Cgr ⟨A, B⟩ \land ⟨C, D⟩ Cgr ⟨A, x⟩ \land ⟨y, D⟩ Cgr ⟨B, x⟩))$
35		simp2l	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (⟨C, y⟩ Cgr ⟨A, B⟩ \land ⟨C, D⟩ Cgr ⟨A, x⟩ \land ⟨y, D⟩ Cgr ⟨B, x⟩)) \to y Btwn ⟨C, D⟩$
36		simp3	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (⟨C, y⟩ Cgr ⟨A, B⟩ \land ⟨C, D⟩ Cgr ⟨A, x⟩ \land ⟨y, D⟩ Cgr ⟨B, x⟩)) \to (⟨C, y⟩ Cgr ⟨A, B⟩ \land ⟨C, D⟩ Cgr ⟨A, x⟩ \land ⟨y, D⟩ Cgr ⟨B, x⟩)$
37	33	3ad2ant1	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (⟨C, y⟩ Cgr ⟨A, B⟩ \land ⟨C, D⟩ Cgr ⟨A, x⟩ \land ⟨y, D⟩ Cgr ⟨B, x⟩)) \to (⟨C, ⟨y, D⟩⟩ Cgr3 ⟨A, ⟨B, x⟩⟩ \leftrightarrow (⟨C, y⟩ Cgr ⟨A, B⟩ \land ⟨C, D⟩ Cgr ⟨A, x⟩ \land ⟨y, D⟩ Cgr ⟨B, x⟩))$
38	36 37	mpbird	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (⟨C, y⟩ Cgr ⟨A, B⟩ \land ⟨C, D⟩ Cgr ⟨A, x⟩ \land ⟨y, D⟩ Cgr ⟨B, x⟩)) \to ⟨C, ⟨y, D⟩⟩ Cgr3 ⟨A, ⟨B, x⟩⟩$
39		btwnxfr	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land y \in 𝔼 (N) \land D \in 𝔼 (N)) \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land x \in 𝔼 (N))) \to ((y Btwn ⟨C, D⟩ \land ⟨C, ⟨y, D⟩⟩ Cgr3 ⟨A, ⟨B, x⟩⟩) \to B Btwn ⟨A, x⟩)$
40	21 23 24 26 28 30 31 39	syl133anc	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \to ((y Btwn ⟨C, D⟩ \land ⟨C, ⟨y, D⟩⟩ Cgr3 ⟨A, ⟨B, x⟩⟩) \to B Btwn ⟨A, x⟩)$
41	40	3ad2ant1	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (⟨C, y⟩ Cgr ⟨A, B⟩ \land ⟨C, D⟩ Cgr ⟨A, x⟩ \land ⟨y, D⟩ Cgr ⟨B, x⟩)) \to ((y Btwn ⟨C, D⟩ \land ⟨C, ⟨y, D⟩⟩ Cgr3 ⟨A, ⟨B, x⟩⟩) \to B Btwn ⟨A, x⟩)$
42	35 38 41	mp2and	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (⟨C, y⟩ Cgr ⟨A, B⟩ \land ⟨C, D⟩ Cgr ⟨A, x⟩ \land ⟨y, D⟩ Cgr ⟨B, x⟩)) \to B Btwn ⟨A, x⟩$
43		simp32	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (⟨C, y⟩ Cgr ⟨A, B⟩ \land ⟨C, D⟩ Cgr ⟨A, x⟩ \land ⟨y, D⟩ Cgr ⟨B, x⟩)) \to ⟨C, D⟩ Cgr ⟨A, x⟩$
44		cgrcom	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land (A \in 𝔼 (N) \land x \in 𝔼 (N))) \to (⟨C, D⟩ Cgr ⟨A, x⟩ \leftrightarrow ⟨A, x⟩ Cgr ⟨C, D⟩)$
45	21 23 26 28 31 44	syl122anc	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \to (⟨C, D⟩ Cgr ⟨A, x⟩ \leftrightarrow ⟨A, x⟩ Cgr ⟨C, D⟩)$
46	45	3ad2ant1	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (⟨C, y⟩ Cgr ⟨A, B⟩ \land ⟨C, D⟩ Cgr ⟨A, x⟩ \land ⟨y, D⟩ Cgr ⟨B, x⟩)) \to (⟨C, D⟩ Cgr ⟨A, x⟩ \leftrightarrow ⟨A, x⟩ Cgr ⟨C, D⟩)$
47	43 46	mpbid	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (⟨C, y⟩ Cgr ⟨A, B⟩ \land ⟨C, D⟩ Cgr ⟨A, x⟩ \land ⟨y, D⟩ Cgr ⟨B, x⟩)) \to ⟨A, x⟩ Cgr ⟨C, D⟩$
48	42 47	jca	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (⟨C, y⟩ Cgr ⟨A, B⟩ \land ⟨C, D⟩ Cgr ⟨A, x⟩ \land ⟨y, D⟩ Cgr ⟨B, x⟩)) \to (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩)$
49	48	3expia	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)) \to ((⟨C, y⟩ Cgr ⟨A, B⟩ \land ⟨C, D⟩ Cgr ⟨A, x⟩ \land ⟨y, D⟩ Cgr ⟨B, x⟩) \to (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩))$
50	34 49	sylbid	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)) \to (⟨C, ⟨y, D⟩⟩ Cgr3 ⟨A, ⟨B, x⟩⟩ \to (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩))$
51	20 50	sylanb	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land y \in 𝔼 (N)) \land x \in 𝔼 (N)) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)) \to (⟨C, ⟨y, D⟩⟩ Cgr3 ⟨A, ⟨B, x⟩⟩ \to (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩))$
52	51	an32s	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)) \land x \in 𝔼 (N)) \to (⟨C, ⟨y, D⟩⟩ Cgr3 ⟨A, ⟨B, x⟩⟩ \to (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩))$
53	52	reximdva	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)) \to (\exists x \in 𝔼 (N) ⟨C, ⟨y, D⟩⟩ Cgr3 ⟨A, ⟨B, x⟩⟩ \to \exists x \in 𝔼 (N) (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩))$
54	19 53	mpd	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land y \in 𝔼 (N)) \land (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)) \to \exists x \in 𝔼 (N) (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩)$
55	54	rexlimdva2	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (\exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \to \exists x \in 𝔼 (N) (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩))$
56		simprl	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩)) \to B Btwn ⟨A, x⟩$
57		simpll1	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩)) \to N \in ℕ$
58	27	adantr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩)) \to A \in 𝔼 (N)$
59		simplr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩)) \to x \in 𝔼 (N)$
60	29	adantr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩)) \to B \in 𝔼 (N)$
61		btwncolinear1	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land x \in 𝔼 (N) \land B \in 𝔼 (N))) \to (B Btwn ⟨A, x⟩ \to A Colinear ⟨x, B⟩)$
62	57 58 59 60 61	syl13anc	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩)) \to (B Btwn ⟨A, x⟩ \to A Colinear ⟨x, B⟩)$
63	56 62	mpd	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩)) \to A Colinear ⟨x, B⟩$
64		simprr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩)) \to ⟨A, x⟩ Cgr ⟨C, D⟩$
65		simpl1	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to N \in ℕ$
66		simpr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to x \in 𝔼 (N)$
67		simpl3	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to (C \in 𝔼 (N) \land D \in 𝔼 (N))$
68		lineext	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land x \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((A Colinear ⟨x, B⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩) \to \exists y \in 𝔼 (N) ⟨A, ⟨x, B⟩⟩ Cgr3 ⟨C, ⟨D, y⟩⟩)$
69	65 27 66 29 67 68	syl131anc	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to ((A Colinear ⟨x, B⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩) \to \exists y \in 𝔼 (N) ⟨A, ⟨x, B⟩⟩ Cgr3 ⟨C, ⟨D, y⟩⟩)$
70	69	adantr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩)) \to ((A Colinear ⟨x, B⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩) \to \exists y \in 𝔼 (N) ⟨A, ⟨x, B⟩⟩ Cgr3 ⟨C, ⟨D, y⟩⟩)$
71	63 64 70	mp2and	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩)) \to \exists y \in 𝔼 (N) ⟨A, ⟨x, B⟩⟩ Cgr3 ⟨C, ⟨D, y⟩⟩$
72	27 66 29	3jca	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to (A \in 𝔼 (N) \land x \in 𝔼 (N) \land B \in 𝔼 (N))$
73	72	adantr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \to (A \in 𝔼 (N) \land x \in 𝔼 (N) \land B \in 𝔼 (N))$
74		brcgr3	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land x \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N) \land y \in 𝔼 (N))) \to (⟨A, ⟨x, B⟩⟩ Cgr3 ⟨C, ⟨D, y⟩⟩ \leftrightarrow (⟨A, x⟩ Cgr ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩ \land ⟨x, B⟩ Cgr ⟨D, y⟩))$
75	21 73 23 26 24 74	syl113anc	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \to (⟨A, ⟨x, B⟩⟩ Cgr3 ⟨C, ⟨D, y⟩⟩ \leftrightarrow (⟨A, x⟩ Cgr ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩ \land ⟨x, B⟩ Cgr ⟨D, y⟩))$
76	75	adantr	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \land (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩)) \to (⟨A, ⟨x, B⟩⟩ Cgr3 ⟨C, ⟨D, y⟩⟩ \leftrightarrow (⟨A, x⟩ Cgr ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩ \land ⟨x, B⟩ Cgr ⟨D, y⟩))$
77		simp2l	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \land (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩) \land (⟨A, x⟩ Cgr ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩ \land ⟨x, B⟩ Cgr ⟨D, y⟩)) \to B Btwn ⟨A, x⟩$
78		simp32	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \land (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩) \land (⟨A, x⟩ Cgr ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩ \land ⟨x, B⟩ Cgr ⟨D, y⟩)) \to ⟨A, B⟩ Cgr ⟨C, y⟩$
79		simp2r	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \land (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩) \land (⟨A, x⟩ Cgr ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩ \land ⟨x, B⟩ Cgr ⟨D, y⟩)) \to ⟨A, x⟩ Cgr ⟨C, D⟩$
80		simp33	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \land (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩) \land (⟨A, x⟩ Cgr ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩ \land ⟨x, B⟩ Cgr ⟨D, y⟩)) \to ⟨x, B⟩ Cgr ⟨D, y⟩$
81		cgrcomlr	$⊢ (N \in ℕ \land (x \in 𝔼 (N) \land B \in 𝔼 (N)) \land (D \in 𝔼 (N) \land y \in 𝔼 (N))) \to (⟨x, B⟩ Cgr ⟨D, y⟩ \leftrightarrow ⟨B, x⟩ Cgr ⟨y, D⟩)$
82	21 31 30 26 24 81	syl122anc	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \to (⟨x, B⟩ Cgr ⟨D, y⟩ \leftrightarrow ⟨B, x⟩ Cgr ⟨y, D⟩)$
83	82	3ad2ant1	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \land (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩) \land (⟨A, x⟩ Cgr ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩ \land ⟨x, B⟩ Cgr ⟨D, y⟩)) \to (⟨x, B⟩ Cgr ⟨D, y⟩ \leftrightarrow ⟨B, x⟩ Cgr ⟨y, D⟩)$
84	80 83	mpbid	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \land (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩) \land (⟨A, x⟩ Cgr ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩ \land ⟨x, B⟩ Cgr ⟨D, y⟩)) \to ⟨B, x⟩ Cgr ⟨y, D⟩$
85	78 79 84	3jca	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \land (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩) \land (⟨A, x⟩ Cgr ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩ \land ⟨x, B⟩ Cgr ⟨D, y⟩)) \to (⟨A, B⟩ Cgr ⟨C, y⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩ \land ⟨B, x⟩ Cgr ⟨y, D⟩)$
86		brcgr3	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land x \in 𝔼 (N)) \land (C \in 𝔼 (N) \land y \in 𝔼 (N) \land D \in 𝔼 (N))) \to (⟨A, ⟨B, x⟩⟩ Cgr3 ⟨C, ⟨y, D⟩⟩ \leftrightarrow (⟨A, B⟩ Cgr ⟨C, y⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩ \land ⟨B, x⟩ Cgr ⟨y, D⟩))$
87	21 28 30 31 23 24 26 86	syl133anc	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \to (⟨A, ⟨B, x⟩⟩ Cgr3 ⟨C, ⟨y, D⟩⟩ \leftrightarrow (⟨A, B⟩ Cgr ⟨C, y⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩ \land ⟨B, x⟩ Cgr ⟨y, D⟩))$
88	87	3ad2ant1	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \land (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩) \land (⟨A, x⟩ Cgr ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩ \land ⟨x, B⟩ Cgr ⟨D, y⟩)) \to (⟨A, ⟨B, x⟩⟩ Cgr3 ⟨C, ⟨y, D⟩⟩ \leftrightarrow (⟨A, B⟩ Cgr ⟨C, y⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩ \land ⟨B, x⟩ Cgr ⟨y, D⟩))$
89	85 88	mpbird	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \land (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩) \land (⟨A, x⟩ Cgr ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩ \land ⟨x, B⟩ Cgr ⟨D, y⟩)) \to ⟨A, ⟨B, x⟩⟩ Cgr3 ⟨C, ⟨y, D⟩⟩$
90		btwnxfr	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land x \in 𝔼 (N)) \land (C \in 𝔼 (N) \land y \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((B Btwn ⟨A, x⟩ \land ⟨A, ⟨B, x⟩⟩ Cgr3 ⟨C, ⟨y, D⟩⟩) \to y Btwn ⟨C, D⟩)$
91	21 28 30 31 23 24 26 90	syl133anc	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \to ((B Btwn ⟨A, x⟩ \land ⟨A, ⟨B, x⟩⟩ Cgr3 ⟨C, ⟨y, D⟩⟩) \to y Btwn ⟨C, D⟩)$
92	91	3ad2ant1	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \land (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩) \land (⟨A, x⟩ Cgr ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩ \land ⟨x, B⟩ Cgr ⟨D, y⟩)) \to ((B Btwn ⟨A, x⟩ \land ⟨A, ⟨B, x⟩⟩ Cgr3 ⟨C, ⟨y, D⟩⟩) \to y Btwn ⟨C, D⟩)$
93	77 89 92	mp2and	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \land (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩) \land (⟨A, x⟩ Cgr ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩ \land ⟨x, B⟩ Cgr ⟨D, y⟩)) \to y Btwn ⟨C, D⟩$
94	93 78	jca	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \land (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩) \land (⟨A, x⟩ Cgr ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩ \land ⟨x, B⟩ Cgr ⟨D, y⟩)) \to (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)$
95	94	3expia	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \land (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩)) \to ((⟨A, x⟩ Cgr ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩ \land ⟨x, B⟩ Cgr ⟨D, y⟩) \to (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))$
96	76 95	sylbid	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land y \in 𝔼 (N)) \land (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩)) \to (⟨A, ⟨x, B⟩⟩ Cgr3 ⟨C, ⟨D, y⟩⟩ \to (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))$
97	96	an32s	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩)) \land y \in 𝔼 (N)) \to (⟨A, ⟨x, B⟩⟩ Cgr3 ⟨C, ⟨D, y⟩⟩ \to (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))$
98	97	reximdva	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩)) \to (\exists y \in 𝔼 (N) ⟨A, ⟨x, B⟩⟩ Cgr3 ⟨C, ⟨D, y⟩⟩ \to \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))$
99	71 98	mpd	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩)) \to \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)$
100	99	rexlimdva2	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (\exists x \in 𝔼 (N) (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩) \to \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))$
101	55 100	impbid	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (\exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \leftrightarrow \exists x \in 𝔼 (N) (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩))$
102	1 101	bitrd	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩ \leftrightarrow \exists x \in 𝔼 (N) (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩))$

Metamath Proof Explorer

Theorem brsegle2

Proof