Metamath Proof Explorer

Theorem trisegint

Description: A line segment between two sides of a triange intersects a segment crossing from the remaining side to the opposite vertex. Theorem 3.17 of Schwabhauser p. 33. (Contributed by Scott Fenton, 24-Sep-2013)

Ref Expression
Assertion trisegint ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) → ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑞 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∧ 𝑞 Btwn ⟨ 𝐵 , 𝐸 ⟩ ) ) )

Proof

Step Hyp Ref Expression
1 simpl1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) → 𝑁 ∈ ℕ )
2 simpl23 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
3 simpl21 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
4 simpl31 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
5 2 3 4 3jca ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) → ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) )
6 simpl32 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) → 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) )
7 simpl33 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) → 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) )
8 6 7 jca ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) → ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) )
9 1 5 8 3jca ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) → ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) )
10 simpr2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) → 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ )
11 btwncom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ↔ 𝐸 Btwn ⟨ 𝐶 , 𝐷 ⟩ ) )
12 1 6 4 2 11 syl13anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) → ( 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ↔ 𝐸 Btwn ⟨ 𝐶 , 𝐷 ⟩ ) )
13 10 12 mpbid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) → 𝐸 Btwn ⟨ 𝐶 , 𝐷 ⟩ )
14 simpr3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) → 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ )
15 13 14 jca ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) → ( 𝐸 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) )
16 axpasch ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐸 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) → ∃ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) )
17 9 15 16 sylc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) → ∃ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) )
18 simp1l1 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) → 𝑁 ∈ ℕ )
19 6 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) → 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) )
20 2 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
21 3 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
22 19 20 21 3jca ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) → ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) )
23 simp2 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) → 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) )
24 simpl22 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
25 24 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
26 23 25 jca ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) → ( 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) )
27 18 22 26 3jca ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) → ( 𝑁 ∈ ℕ ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) )
28 simp3l ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) → 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ )
29 simp1r1 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ )
30 btwncom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ↔ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ) )
31 18 25 21 20 30 syl13anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ↔ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ) )
32 29 31 mpbid ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) → 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ )
33 28 32 jca ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) → ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ) )
34 axpasch ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ) → ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑞 Btwn ⟨ 𝑟 , 𝐶 ⟩ ∧ 𝑞 Btwn ⟨ 𝐵 , 𝐸 ⟩ ) ) )
35 27 33 34 sylc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) → ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑞 Btwn ⟨ 𝑟 , 𝐶 ⟩ ∧ 𝑞 Btwn ⟨ 𝐵 , 𝐸 ⟩ ) )
36 simpll1 ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑞 Btwn ⟨ 𝑟 , 𝐶 ⟩ ) → ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) )
37 36 1 syl ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑞 Btwn ⟨ 𝑟 , 𝐶 ⟩ ) → 𝑁 ∈ ℕ )
38 36 7 syl ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑞 Btwn ⟨ 𝑟 , 𝐶 ⟩ ) → 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) )
39 simpll2 ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑞 Btwn ⟨ 𝑟 , 𝐶 ⟩ ) → 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) )
40 38 39 jca ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑞 Btwn ⟨ 𝑟 , 𝐶 ⟩ ) → ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ) )
41 simplr ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑞 Btwn ⟨ 𝑟 , 𝐶 ⟩ ) → 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) )
42 36 2 syl ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑞 Btwn ⟨ 𝑟 , 𝐶 ⟩ ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
43 41 42 jca ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑞 Btwn ⟨ 𝑟 , 𝐶 ⟩ ) → ( 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) )
44 37 40 43 3jca ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑞 Btwn ⟨ 𝑟 , 𝐶 ⟩ ) → ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) )
45 simpl3r ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ )
46 45 anim1i ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑞 Btwn ⟨ 𝑟 , 𝐶 ⟩ ) → ( 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∧ 𝑞 Btwn ⟨ 𝑟 , 𝐶 ⟩ ) )
47 btwnexch2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∧ 𝑞 Btwn ⟨ 𝑟 , 𝐶 ⟩ ) → 𝑞 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) )
48 44 46 47 sylc ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑞 Btwn ⟨ 𝑟 , 𝐶 ⟩ ) → 𝑞 Btwn ⟨ 𝑃 , 𝐶 ⟩ )
49 48 ex ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑞 Btwn ⟨ 𝑟 , 𝐶 ⟩ → 𝑞 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) )
50 49 anim1d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝑞 Btwn ⟨ 𝑟 , 𝐶 ⟩ ∧ 𝑞 Btwn ⟨ 𝐵 , 𝐸 ⟩ ) → ( 𝑞 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∧ 𝑞 Btwn ⟨ 𝐵 , 𝐸 ⟩ ) ) )
51 50 reximdva ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) → ( ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑞 Btwn ⟨ 𝑟 , 𝐶 ⟩ ∧ 𝑞 Btwn ⟨ 𝐵 , 𝐸 ⟩ ) → ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑞 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∧ 𝑞 Btwn ⟨ 𝐵 , 𝐸 ⟩ ) ) )
52 35 51 mpd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) ) → ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑞 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∧ 𝑞 Btwn ⟨ 𝐵 , 𝐸 ⟩ ) )
53 52 rexlimdv3a ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) → ( ∃ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑟 Btwn ⟨ 𝐸 , 𝐴 ⟩ ∧ 𝑟 Btwn ⟨ 𝑃 , 𝐶 ⟩ ) → ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑞 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∧ 𝑞 Btwn ⟨ 𝐵 , 𝐸 ⟩ ) ) )
54 17 53 mpd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) → ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑞 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∧ 𝑞 Btwn ⟨ 𝐵 , 𝐸 ⟩ ) )
55 54 ex ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐷 , 𝐶 ⟩ ∧ 𝑃 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) → ∃ 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑞 Btwn ⟨ 𝑃 , 𝐶 ⟩ ∧ 𝑞 Btwn ⟨ 𝐵 , 𝐸 ⟩ ) ) )