Metamath Proof Explorer

Theorem btwnexch3

Description: Exchange the first endpoint in betweenness. Left-hand side of Theorem 3.6 of Schwabhauser p. 30. (Contributed by Scott Fenton, 12-Jun-2013)

Ref Expression
Assertion btwnexch3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → B Btwn A C ∧ C Btwn A D → C Btwn B D

Proof

Step Hyp Ref Expression
1 simp1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → N ∈ ℕ
2 simp3l ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → C ∈ 𝔼 ⁡ N
3 simp2l ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N
4 simp3r ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → D ∈ 𝔼 ⁡ N
5 btwncom ⊢ N ∈ ℕ ∧ C ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → C Btwn A D ↔ C Btwn D A
6 1 2 3 4 5 syl13anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → C Btwn A D ↔ C Btwn D A
7 simp2r ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → B ∈ 𝔼 ⁡ N
8 btwncom ⊢ N ∈ ℕ ∧ B ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → B Btwn A C ↔ B Btwn C A
9 1 7 3 2 8 syl13anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → B Btwn A C ↔ B Btwn C A
10 6 9 anbi12d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → C Btwn A D ∧ B Btwn A C ↔ C Btwn D A ∧ B Btwn C A
11 axpasch ⊢ N ∈ ℕ ∧ D ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → C Btwn D A ∧ B Btwn C A → ∃ x ∈ 𝔼 ⁡ N x Btwn C C ∧ x Btwn B D
12 1 4 2 3 2 7 11 syl132anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → C Btwn D A ∧ B Btwn C A → ∃ x ∈ 𝔼 ⁡ N x Btwn C C ∧ x Btwn B D
13 10 12 sylbid ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → C Btwn A D ∧ B Btwn A C → ∃ x ∈ 𝔼 ⁡ N x Btwn C C ∧ x Btwn B D
14 13 ancomsd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → B Btwn A C ∧ C Btwn A D → ∃ x ∈ 𝔼 ⁡ N x Btwn C C ∧ x Btwn B D
15 simpl1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → N ∈ ℕ
16 simpr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → x ∈ 𝔼 ⁡ N
17 simpl3l ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → C ∈ 𝔼 ⁡ N
18 axbtwnid ⊢ N ∈ ℕ ∧ x ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → x Btwn C C → x = C
19 15 16 17 18 syl3anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → x Btwn C C → x = C
20 breq1 ⊢ x = C → x Btwn B D ↔ C Btwn B D
21 20 biimpd ⊢ x = C → x Btwn B D → C Btwn B D
22 19 21 syl6 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → x Btwn C C → x Btwn B D → C Btwn B D
23 22 impd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → x Btwn C C ∧ x Btwn B D → C Btwn B D
24 23 rexlimdva ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → ∃ x ∈ 𝔼 ⁡ N x Btwn C C ∧ x Btwn B D → C Btwn B D
25 14 24 syld ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → B Btwn A C ∧ C Btwn A D → C Btwn B D