brsegle2 - Mathbox for Scott Fenton

	Mathbox for Scott Fenton		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > brsegle2		Structured version Visualization version GIF version

Theorem brsegle2 34148

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

**Assertion**
Ref	Expression
brsegle2	⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (⟨𝐴, 𝐵⟩ Seg_≤ ⟨𝐶, 𝐷⟩ ↔ ∃𝑥 ∈ (𝔼‘𝑁)(𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩)))

Distinct variable groups: 𝑥,𝑁 𝑥,𝐴 𝑥,𝐵 𝑥,𝐶 𝑥,𝐷

Proof of Theorem brsegle2 Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		brsegle 34147	. 2 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (⟨𝐴, 𝐵⟩ Seg_≤ ⟨𝐶, 𝐷⟩ ↔ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩)))
2		simprl 771	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩)) → 𝑦 Btwn ⟨𝐶, 𝐷⟩)
3		simpl1 1193	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ)
4		simpl3l 1230	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝐶 ∈ (𝔼‘𝑁))
5		simpl3r 1231	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝐷 ∈ (𝔼‘𝑁))
6		simpr 488	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝑦 ∈ (𝔼‘𝑁))
7		btwncolinear2 34109	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (𝑦 Btwn ⟨𝐶, 𝐷⟩ → 𝐶 Colinear ⟨𝑦, 𝐷⟩))
8	3, 4, 5, 6, 7	syl13anc 1374	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (𝑦 Btwn ⟨𝐶, 𝐷⟩ → 𝐶 Colinear ⟨𝑦, 𝐷⟩))
9	8	adantr 484	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩)) → (𝑦 Btwn ⟨𝐶, 𝐷⟩ → 𝐶 Colinear ⟨𝑦, 𝐷⟩))
10	2, 9	mpd 15	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩)) → 𝐶 Colinear ⟨𝑦, 𝐷⟩)
11		simpl2l 1228	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝐴 ∈ (𝔼‘𝑁))
12		simpl2r 1229	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝐵 ∈ (𝔼‘𝑁))
13		simprr 773	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩)) → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩)
14	3, 11, 12, 4, 6, 13	cgrcomand 34030	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩)) → ⟨𝐶, 𝑦⟩Cgr⟨𝐴, 𝐵⟩)
15		simpl2 1194	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)))
16		lineext 34115	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → ((𝐶 Colinear ⟨𝑦, 𝐷⟩ ∧ ⟨𝐶, 𝑦⟩Cgr⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ (𝔼‘𝑁)⟨𝐶, ⟨𝑦, 𝐷⟩⟩Cgr3⟨𝐴, ⟨𝐵, 𝑥⟩⟩))
17	3, 4, 6, 5, 15, 16	syl131anc 1385	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) → ((𝐶 Colinear ⟨𝑦, 𝐷⟩ ∧ ⟨𝐶, 𝑦⟩Cgr⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ (𝔼‘𝑁)⟨𝐶, ⟨𝑦, 𝐷⟩⟩Cgr3⟨𝐴, ⟨𝐵, 𝑥⟩⟩))
18	17	adantr 484	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩)) → ((𝐶 Colinear ⟨𝑦, 𝐷⟩ ∧ ⟨𝐶, 𝑦⟩Cgr⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ (𝔼‘𝑁)⟨𝐶, ⟨𝑦, 𝐷⟩⟩Cgr3⟨𝐴, ⟨𝐵, 𝑥⟩⟩))
19	10, 14, 18	mp2and 699	. . . . 5 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩)) → ∃𝑥 ∈ (𝔼‘𝑁)⟨𝐶, ⟨𝑦, 𝐷⟩⟩Cgr3⟨𝐴, ⟨𝐵, 𝑥⟩⟩)
20		an32 646	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ↔ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)))
21		simpll1 1214	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ)
22		simpl3l 1230	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐶 ∈ (𝔼‘𝑁))
23	22	adantr 484	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝐶 ∈ (𝔼‘𝑁))
24		simpr 488	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝑦 ∈ (𝔼‘𝑁))
25		simpl3r 1231	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐷 ∈ (𝔼‘𝑁))
26	25	adantr 484	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝐷 ∈ (𝔼‘𝑁))
27		simpl2l 1228	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐴 ∈ (𝔼‘𝑁))
28	27	adantr 484	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝐴 ∈ (𝔼‘𝑁))
29		simpl2r 1229	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐵 ∈ (𝔼‘𝑁))
30	29	adantr 484	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝐵 ∈ (𝔼‘𝑁))
31		simplr 769	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (𝔼‘𝑁))
32		brcgr3 34085	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → (⟨𝐶, ⟨𝑦, 𝐷⟩⟩Cgr3⟨𝐴, ⟨𝐵, 𝑥⟩⟩ ↔ (⟨𝐶, 𝑦⟩Cgr⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐴, 𝑥⟩ ∧ ⟨𝑦, 𝐷⟩Cgr⟨𝐵, 𝑥⟩)))
33	21, 23, 24, 26, 28, 30, 31, 32	syl133anc 1395	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (⟨𝐶, ⟨𝑦, 𝐷⟩⟩Cgr3⟨𝐴, ⟨𝐵, 𝑥⟩⟩ ↔ (⟨𝐶, 𝑦⟩Cgr⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐴, 𝑥⟩ ∧ ⟨𝑦, 𝐷⟩Cgr⟨𝐵, 𝑥⟩)))
34	33	adantr 484	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩)) → (⟨𝐶, ⟨𝑦, 𝐷⟩⟩Cgr3⟨𝐴, ⟨𝐵, 𝑥⟩⟩ ↔ (⟨𝐶, 𝑦⟩Cgr⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐴, 𝑥⟩ ∧ ⟨𝑦, 𝐷⟩Cgr⟨𝐵, 𝑥⟩)))
35		simp2l 1201	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩) ∧ (⟨𝐶, 𝑦⟩Cgr⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐴, 𝑥⟩ ∧ ⟨𝑦, 𝐷⟩Cgr⟨𝐵, 𝑥⟩)) → 𝑦 Btwn ⟨𝐶, 𝐷⟩)
36		simp3 1140	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩) ∧ (⟨𝐶, 𝑦⟩Cgr⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐴, 𝑥⟩ ∧ ⟨𝑦, 𝐷⟩Cgr⟨𝐵, 𝑥⟩)) → (⟨𝐶, 𝑦⟩Cgr⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐴, 𝑥⟩ ∧ ⟨𝑦, 𝐷⟩Cgr⟨𝐵, 𝑥⟩))
37	33	3ad2ant1 1135	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩) ∧ (⟨𝐶, 𝑦⟩Cgr⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐴, 𝑥⟩ ∧ ⟨𝑦, 𝐷⟩Cgr⟨𝐵, 𝑥⟩)) → (⟨𝐶, ⟨𝑦, 𝐷⟩⟩Cgr3⟨𝐴, ⟨𝐵, 𝑥⟩⟩ ↔ (⟨𝐶, 𝑦⟩Cgr⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐴, 𝑥⟩ ∧ ⟨𝑦, 𝐷⟩Cgr⟨𝐵, 𝑥⟩)))
38	36, 37	mpbird 260	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩) ∧ (⟨𝐶, 𝑦⟩Cgr⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐴, 𝑥⟩ ∧ ⟨𝑦, 𝐷⟩Cgr⟨𝐵, 𝑥⟩)) → ⟨𝐶, ⟨𝑦, 𝐷⟩⟩Cgr3⟨𝐴, ⟨𝐵, 𝑥⟩⟩)
39		btwnxfr 34095	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → ((𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐶, ⟨𝑦, 𝐷⟩⟩Cgr3⟨𝐴, ⟨𝐵, 𝑥⟩⟩) → 𝐵 Btwn ⟨𝐴, 𝑥⟩))
40	21, 23, 24, 26, 28, 30, 31, 39	syl133anc 1395	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → ((𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐶, ⟨𝑦, 𝐷⟩⟩Cgr3⟨𝐴, ⟨𝐵, 𝑥⟩⟩) → 𝐵 Btwn ⟨𝐴, 𝑥⟩))
41	40	3ad2ant1 1135	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩) ∧ (⟨𝐶, 𝑦⟩Cgr⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐴, 𝑥⟩ ∧ ⟨𝑦, 𝐷⟩Cgr⟨𝐵, 𝑥⟩)) → ((𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐶, ⟨𝑦, 𝐷⟩⟩Cgr3⟨𝐴, ⟨𝐵, 𝑥⟩⟩) → 𝐵 Btwn ⟨𝐴, 𝑥⟩))
42	35, 38, 41	mp2and 699	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩) ∧ (⟨𝐶, 𝑦⟩Cgr⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐴, 𝑥⟩ ∧ ⟨𝑦, 𝐷⟩Cgr⟨𝐵, 𝑥⟩)) → 𝐵 Btwn ⟨𝐴, 𝑥⟩)
43		simp32 1212	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩) ∧ (⟨𝐶, 𝑦⟩Cgr⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐴, 𝑥⟩ ∧ ⟨𝑦, 𝐷⟩Cgr⟨𝐵, 𝑥⟩)) → ⟨𝐶, 𝐷⟩Cgr⟨𝐴, 𝑥⟩)
44		cgrcom 34029	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) → (⟨𝐶, 𝐷⟩Cgr⟨𝐴, 𝑥⟩ ↔ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩))
45	21, 23, 26, 28, 31, 44	syl122anc 1381	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (⟨𝐶, 𝐷⟩Cgr⟨𝐴, 𝑥⟩ ↔ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩))
46	45	3ad2ant1 1135	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩) ∧ (⟨𝐶, 𝑦⟩Cgr⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐴, 𝑥⟩ ∧ ⟨𝑦, 𝐷⟩Cgr⟨𝐵, 𝑥⟩)) → (⟨𝐶, 𝐷⟩Cgr⟨𝐴, 𝑥⟩ ↔ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩))
47	43, 46	mpbid 235	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩) ∧ (⟨𝐶, 𝑦⟩Cgr⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐴, 𝑥⟩ ∧ ⟨𝑦, 𝐷⟩Cgr⟨𝐵, 𝑥⟩)) → ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩)
48	42, 47	jca 515	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩) ∧ (⟨𝐶, 𝑦⟩Cgr⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐴, 𝑥⟩ ∧ ⟨𝑦, 𝐷⟩Cgr⟨𝐵, 𝑥⟩)) → (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩))
49	48	3expia 1123	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩)) → ((⟨𝐶, 𝑦⟩Cgr⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐴, 𝑥⟩ ∧ ⟨𝑦, 𝐷⟩Cgr⟨𝐵, 𝑥⟩) → (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩)))
50	34, 49	sylbid 243	. . . . . . . 8 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩)) → (⟨𝐶, ⟨𝑦, 𝐷⟩⟩Cgr3⟨𝐴, ⟨𝐵, 𝑥⟩⟩ → (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩)))
51	20, 50	sylanb 584	. . . . . . 7 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩)) → (⟨𝐶, ⟨𝑦, 𝐷⟩⟩Cgr3⟨𝐴, ⟨𝐵, 𝑥⟩⟩ → (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩)))
52	51	an32s 652	. . . . . 6 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (⟨𝐶, ⟨𝑦, 𝐷⟩⟩Cgr3⟨𝐴, ⟨𝐵, 𝑥⟩⟩ → (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩)))
53	52	reximdva 3193	. . . . 5 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩)) → (∃𝑥 ∈ (𝔼‘𝑁)⟨𝐶, ⟨𝑦, 𝐷⟩⟩Cgr3⟨𝐴, ⟨𝐵, 𝑥⟩⟩ → ∃𝑥 ∈ (𝔼‘𝑁)(𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩)))
54	19, 53	mpd 15	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩)) → ∃𝑥 ∈ (𝔼‘𝑁)(𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩))
55	54	rexlimdva2 3206	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩) → ∃𝑥 ∈ (𝔼‘𝑁)(𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩)))
56		simprl 771	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩)) → 𝐵 Btwn ⟨𝐴, 𝑥⟩)
57		simpll1 1214	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩)) → 𝑁 ∈ ℕ)
58	27	adantr 484	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩)) → 𝐴 ∈ (𝔼‘𝑁))
59		simplr 769	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩)) → 𝑥 ∈ (𝔼‘𝑁))
60	29	adantr 484	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩)) → 𝐵 ∈ (𝔼‘𝑁))
61		btwncolinear1 34108	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝐵 Btwn ⟨𝐴, 𝑥⟩ → 𝐴 Colinear ⟨𝑥, 𝐵⟩))
62	57, 58, 59, 60, 61	syl13anc 1374	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩)) → (𝐵 Btwn ⟨𝐴, 𝑥⟩ → 𝐴 Colinear ⟨𝑥, 𝐵⟩))
63	56, 62	mpd 15	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩)) → 𝐴 Colinear ⟨𝑥, 𝐵⟩)
64		simprr 773	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩)) → ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩)
65		simpl1 1193	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ)
66		simpr 488	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (𝔼‘𝑁))
67		simpl3 1195	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))
68		lineext 34115	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐴 Colinear ⟨𝑥, 𝐵⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩) → ∃𝑦 ∈ (𝔼‘𝑁)⟨𝐴, ⟨𝑥, 𝐵⟩⟩Cgr3⟨𝐶, ⟨𝐷, 𝑦⟩⟩))
69	65, 27, 66, 29, 67, 68	syl131anc 1385	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝐴 Colinear ⟨𝑥, 𝐵⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩) → ∃𝑦 ∈ (𝔼‘𝑁)⟨𝐴, ⟨𝑥, 𝐵⟩⟩Cgr3⟨𝐶, ⟨𝐷, 𝑦⟩⟩))
70	69	adantr 484	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩)) → ((𝐴 Colinear ⟨𝑥, 𝐵⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩) → ∃𝑦 ∈ (𝔼‘𝑁)⟨𝐴, ⟨𝑥, 𝐵⟩⟩Cgr3⟨𝐶, ⟨𝐷, 𝑦⟩⟩))
71	63, 64, 70	mp2and 699	. . . . 5 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩)) → ∃𝑦 ∈ (𝔼‘𝑁)⟨𝐴, ⟨𝑥, 𝐵⟩⟩Cgr3⟨𝐶, ⟨𝐷, 𝑦⟩⟩)
72	27, 66, 29	3jca 1130	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)))
73	72	adantr 484	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)))
74		brcgr3 34085	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (⟨𝐴, ⟨𝑥, 𝐵⟩⟩Cgr3⟨𝐶, ⟨𝐷, 𝑦⟩⟩ ↔ (⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩ ∧ ⟨𝑥, 𝐵⟩Cgr⟨𝐷, 𝑦⟩)))
75	21, 73, 23, 26, 24, 74	syl113anc 1384	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (⟨𝐴, ⟨𝑥, 𝐵⟩⟩Cgr3⟨𝐶, ⟨𝐷, 𝑦⟩⟩ ↔ (⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩ ∧ ⟨𝑥, 𝐵⟩Cgr⟨𝐷, 𝑦⟩)))
76	75	adantr 484	. . . . . . . 8 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩)) → (⟨𝐴, ⟨𝑥, 𝐵⟩⟩Cgr3⟨𝐶, ⟨𝐷, 𝑦⟩⟩ ↔ (⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩ ∧ ⟨𝑥, 𝐵⟩Cgr⟨𝐷, 𝑦⟩)))
77		simp2l 1201	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩) ∧ (⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩ ∧ ⟨𝑥, 𝐵⟩Cgr⟨𝐷, 𝑦⟩)) → 𝐵 Btwn ⟨𝐴, 𝑥⟩)
78		simp32 1212	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩) ∧ (⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩ ∧ ⟨𝑥, 𝐵⟩Cgr⟨𝐷, 𝑦⟩)) → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩)
79		simp2r 1202	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩) ∧ (⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩ ∧ ⟨𝑥, 𝐵⟩Cgr⟨𝐷, 𝑦⟩)) → ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩)
80		simp33 1213	. . . . . . . . . . . . . 14 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩) ∧ (⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩ ∧ ⟨𝑥, 𝐵⟩Cgr⟨𝐷, 𝑦⟩)) → ⟨𝑥, 𝐵⟩Cgr⟨𝐷, 𝑦⟩)
81		cgrcomlr 34037	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (⟨𝑥, 𝐵⟩Cgr⟨𝐷, 𝑦⟩ ↔ ⟨𝐵, 𝑥⟩Cgr⟨𝑦, 𝐷⟩))
82	21, 31, 30, 26, 24, 81	syl122anc 1381	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (⟨𝑥, 𝐵⟩Cgr⟨𝐷, 𝑦⟩ ↔ ⟨𝐵, 𝑥⟩Cgr⟨𝑦, 𝐷⟩))
83	82	3ad2ant1 1135	. . . . . . . . . . . . . 14 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩) ∧ (⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩ ∧ ⟨𝑥, 𝐵⟩Cgr⟨𝐷, 𝑦⟩)) → (⟨𝑥, 𝐵⟩Cgr⟨𝐷, 𝑦⟩ ↔ ⟨𝐵, 𝑥⟩Cgr⟨𝑦, 𝐷⟩))
84	80, 83	mpbid 235	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩) ∧ (⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩ ∧ ⟨𝑥, 𝐵⟩Cgr⟨𝐷, 𝑦⟩)) → ⟨𝐵, 𝑥⟩Cgr⟨𝑦, 𝐷⟩)
85	78, 79, 84	3jca 1130	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩) ∧ (⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩ ∧ ⟨𝑥, 𝐵⟩Cgr⟨𝐷, 𝑦⟩)) → (⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩ ∧ ⟨𝐵, 𝑥⟩Cgr⟨𝑦, 𝐷⟩))
86		brcgr3 34085	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (⟨𝐴, ⟨𝐵, 𝑥⟩⟩Cgr3⟨𝐶, ⟨𝑦, 𝐷⟩⟩ ↔ (⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩ ∧ ⟨𝐵, 𝑥⟩Cgr⟨𝑦, 𝐷⟩)))
87	21, 28, 30, 31, 23, 24, 26, 86	syl133anc 1395	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (⟨𝐴, ⟨𝐵, 𝑥⟩⟩Cgr3⟨𝐶, ⟨𝑦, 𝐷⟩⟩ ↔ (⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩ ∧ ⟨𝐵, 𝑥⟩Cgr⟨𝑦, 𝐷⟩)))
88	87	3ad2ant1 1135	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩) ∧ (⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩ ∧ ⟨𝑥, 𝐵⟩Cgr⟨𝐷, 𝑦⟩)) → (⟨𝐴, ⟨𝐵, 𝑥⟩⟩Cgr3⟨𝐶, ⟨𝑦, 𝐷⟩⟩ ↔ (⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩ ∧ ⟨𝐵, 𝑥⟩Cgr⟨𝑦, 𝐷⟩)))
89	85, 88	mpbird 260	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩) ∧ (⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩ ∧ ⟨𝑥, 𝐵⟩Cgr⟨𝐷, 𝑦⟩)) → ⟨𝐴, ⟨𝐵, 𝑥⟩⟩Cgr3⟨𝐶, ⟨𝑦, 𝐷⟩⟩)
90		btwnxfr 34095	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, ⟨𝐵, 𝑥⟩⟩Cgr3⟨𝐶, ⟨𝑦, 𝐷⟩⟩) → 𝑦 Btwn ⟨𝐶, 𝐷⟩))
91	21, 28, 30, 31, 23, 24, 26, 90	syl133anc 1395	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → ((𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, ⟨𝐵, 𝑥⟩⟩Cgr3⟨𝐶, ⟨𝑦, 𝐷⟩⟩) → 𝑦 Btwn ⟨𝐶, 𝐷⟩))
92	91	3ad2ant1 1135	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩) ∧ (⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩ ∧ ⟨𝑥, 𝐵⟩Cgr⟨𝐷, 𝑦⟩)) → ((𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, ⟨𝐵, 𝑥⟩⟩Cgr3⟨𝐶, ⟨𝑦, 𝐷⟩⟩) → 𝑦 Btwn ⟨𝐶, 𝐷⟩))
93	77, 89, 92	mp2and 699	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩) ∧ (⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩ ∧ ⟨𝑥, 𝐵⟩Cgr⟨𝐷, 𝑦⟩)) → 𝑦 Btwn ⟨𝐶, 𝐷⟩)
94	93, 78	jca 515	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩) ∧ (⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩ ∧ ⟨𝑥, 𝐵⟩Cgr⟨𝐷, 𝑦⟩)) → (𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩))
95	94	3expia 1123	. . . . . . . 8 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩)) → ((⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩ ∧ ⟨𝑥, 𝐵⟩Cgr⟨𝐷, 𝑦⟩) → (𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩)))
96	76, 95	sylbid 243	. . . . . . 7 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩)) → (⟨𝐴, ⟨𝑥, 𝐵⟩⟩Cgr3⟨𝐶, ⟨𝐷, 𝑦⟩⟩ → (𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩)))
97	96	an32s 652	. . . . . 6 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩)) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (⟨𝐴, ⟨𝑥, 𝐵⟩⟩Cgr3⟨𝐶, ⟨𝐷, 𝑦⟩⟩ → (𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩)))
98	97	reximdva 3193	. . . . 5 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩)) → (∃𝑦 ∈ (𝔼‘𝑁)⟨𝐴, ⟨𝑥, 𝐵⟩⟩Cgr3⟨𝐶, ⟨𝐷, 𝑦⟩⟩ → ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩)))
99	71, 98	mpd 15	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩)) → ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩))
100	99	rexlimdva2 3206	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (∃𝑥 ∈ (𝔼‘𝑁)(𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩) → ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩)))
101	55, 100	impbid 215	. 2 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn ⟨𝐶, 𝐷⟩ ∧ ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝑦⟩) ↔ ∃𝑥 ∈ (𝔼‘𝑁)(𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩)))
102	1, 101	bitrd 282	1 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (⟨𝐴, 𝐵⟩ Seg_≤ ⟨𝐶, 𝐷⟩ ↔ ∃𝑥 ∈ (𝔼‘𝑁)(𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐶, 𝐷⟩)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1089 ∈ wcel 2110 ∃wrex 3062 ⟨cop 4547 class class class wbr 5053 ‘cfv 6380 ℕcn 11830 𝔼cee 26979 Btwn cbtwn 26980 Cgrccgr 26981 Cgr3ccgr3 34075 Colinear ccolin 34076 Seg_≤ csegle 34145

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 ax-rep 5179 ax-sep 5192 ax-nul 5199 ax-pow 5258 ax-pr 5322 ax-un 7523 ax-inf2 9256 ax-cnex 10785 ax-resscn 10786 ax-1cn 10787 ax-icn 10788 ax-addcl 10789 ax-addrcl 10790 ax-mulcl 10791 ax-mulrcl 10792 ax-mulcom 10793 ax-addass 10794 ax-mulass 10795 ax-distr 10796 ax-i2m1 10797 ax-1ne0 10798 ax-1rid 10799 ax-rnegex 10800 ax-rrecex 10801 ax-cnre 10802 ax-pre-lttri 10803 ax-pre-lttrn 10804 ax-pre-ltadd 10805 ax-pre-mulgt0 10806 ax-pre-sup 10807

This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2886 df-ne 2941 df-nel 3047 df-ral 3066 df-rex 3067 df-reu 3068 df-rmo 3069 df-rab 3070 df-v 3410 df-sbc 3695 df-csb 3812 df-dif 3869 df-un 3871 df-in 3873 df-ss 3883 df-pss 3885 df-nul 4238 df-if 4440 df-pw 4515 df-sn 4542 df-pr 4544 df-tp 4546 df-op 4548 df-uni 4820 df-int 4860 df-iun 4906 df-br 5054 df-opab 5116 df-mpt 5136 df-tr 5162 df-id 5455 df-eprel 5460 df-po 5468 df-so 5469 df-fr 5509 df-se 5510 df-we 5511 df-xp 5557 df-rel 5558 df-cnv 5559 df-co 5560 df-dm 5561 df-rn 5562 df-res 5563 df-ima 5564 df-pred 6160 df-ord 6216 df-on 6217 df-lim 6218 df-suc 6219 df-iota 6338 df-fun 6382 df-fn 6383 df-f 6384 df-f1 6385 df-fo 6386 df-f1o 6387 df-fv 6388 df-isom 6389 df-riota 7170 df-ov 7216 df-oprab 7217 df-mpo 7218 df-om 7645 df-1st 7761 df-2nd 7762 df-wrecs 8047 df-recs 8108 df-rdg 8146 df-1o 8202 df-er 8391 df-map 8510 df-en 8627 df-dom 8628 df-sdom 8629 df-fin 8630 df-sup 9058 df-oi 9126 df-card 9555 df-pnf 10869 df-mnf 10870 df-xr 10871 df-ltxr 10872 df-le 10873 df-sub 11064 df-neg 11065 df-div 11490 df-nn 11831 df-2 11893 df-3 11894 df-n0 12091 df-z 12177 df-uz 12439 df-rp 12587 df-ico 12941 df-icc 12942 df-fz 13096 df-fzo 13239 df-seq 13575 df-exp 13636 df-hash 13897 df-cj 14662 df-re 14663 df-im 14664 df-sqrt 14798 df-abs 14799 df-clim 15049 df-sum 15250 df-ee 26982 df-btwn 26983 df-cgr 26984 df-ofs 34022 df-colinear 34078 df-ifs 34079 df-cgr3 34080 df-segle 34146

This theorem is referenced by: segleantisym 34154 seglelin 34155 outsidele 34171

W3C validator