Metamath Proof Explorer

Theorem segcon2

Description: Generalization of axsegcon . This time, we generate an endpoint for a segment on the ray Q A congruent to B C and starting at Q , as opposed to axsegcon , where the segment starts at A (Contributed by Scott Fenton, 14-Oct-2013) Remove unneeded inequality. (Revised by Scott Fenton, 15-Oct-2013)

Ref Expression
Assertion segcon2 ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝐴 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑄 , 𝐴 ⟩ ) ∧ ⟨ 𝑄 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) )

Proof

Step Hyp Ref Expression
1 breq1 ⊢ ( 𝐴 = 𝑄 → ( 𝐴 Btwn ⟨ 𝑄 , 𝑥 ⟩ ↔ 𝑄 Btwn ⟨ 𝑄 , 𝑥 ⟩ ) )
2 1 orbi1d ⊢ ( 𝐴 = 𝑄 → ( ( 𝐴 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑄 , 𝐴 ⟩ ) ↔ ( 𝑄 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑄 , 𝐴 ⟩ ) ) )
3 2 anbi1d ⊢ ( 𝐴 = 𝑄 → ( ( ( 𝐴 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑄 , 𝐴 ⟩ ) ∧ ⟨ 𝑄 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ↔ ( ( 𝑄 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑄 , 𝐴 ⟩ ) ∧ ⟨ 𝑄 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) )
4 3 rexbidv ⊢ ( 𝐴 = 𝑄 → ( ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝐴 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑄 , 𝐴 ⟩ ) ∧ ⟨ 𝑄 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝑄 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑄 , 𝐴 ⟩ ) ∧ ⟨ 𝑄 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) )
5 simp1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
6 simp2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) )
7 6 ancomd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) )
8 axsegcon ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑄 Btwn ⟨ 𝐴 , 𝑎 ⟩ ∧ ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ) )
9 5 7 7 8 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑄 Btwn ⟨ 𝐴 , 𝑎 ⟩ ∧ ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ) )
10 9 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝐴 ≠ 𝑄 ) → ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑄 Btwn ⟨ 𝐴 , 𝑎 ⟩ ∧ ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ) )
11 simpl1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ )
12 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) )
13 simpl2l ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) )
14 simpl3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) )
15 axsegcon ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑄 Btwn ⟨ 𝑎 , 𝑥 ⟩ ∧ ⟨ 𝑄 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) )
16 11 12 13 14 15 syl121anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑄 Btwn ⟨ 𝑎 , 𝑥 ⟩ ∧ ⟨ 𝑄 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) )
17 16 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ≠ 𝑄 ∧ ( 𝑄 Btwn ⟨ 𝐴 , 𝑎 ⟩ ∧ ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑄 Btwn ⟨ 𝑎 , 𝑥 ⟩ ∧ ⟨ 𝑄 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) )
18 anass ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ↔ ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ) )
19 df-3an ⊢ ( ( 𝐴 ≠ 𝑄 ∧ ( 𝑄 Btwn ⟨ 𝐴 , 𝑎 ⟩ ∧ ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ) ∧ 𝑄 Btwn ⟨ 𝑎 , 𝑥 ⟩ ) ↔ ( ( 𝐴 ≠ 𝑄 ∧ ( 𝑄 Btwn ⟨ 𝐴 , 𝑎 ⟩ ∧ ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ) ) ∧ 𝑄 Btwn ⟨ 𝑎 , 𝑥 ⟩ ) )
20 simpr1 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝑄 ∧ ( 𝑄 Btwn ⟨ 𝐴 , 𝑎 ⟩ ∧ ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ) ∧ 𝑄 Btwn ⟨ 𝑎 , 𝑥 ⟩ ) ) → 𝐴 ≠ 𝑄 )
21 simpr2r ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝑄 ∧ ( 𝑄 Btwn ⟨ 𝐴 , 𝑎 ⟩ ∧ ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ) ∧ 𝑄 Btwn ⟨ 𝑎 , 𝑥 ⟩ ) ) → ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ )
22 simpl1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
23 simpl2l ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) )
24 simprl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) )
25 simpl2r ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
26 cgrdegen ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ → ( 𝑄 = 𝑎 ↔ 𝐴 = 𝑄 ) ) )
27 22 23 24 25 23 26 syl122anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ → ( 𝑄 = 𝑎 ↔ 𝐴 = 𝑄 ) ) )
28 27 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝑄 ∧ ( 𝑄 Btwn ⟨ 𝐴 , 𝑎 ⟩ ∧ ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ) ∧ 𝑄 Btwn ⟨ 𝑎 , 𝑥 ⟩ ) ) → ( ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ → ( 𝑄 = 𝑎 ↔ 𝐴 = 𝑄 ) ) )
29 21 28 mpd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝑄 ∧ ( 𝑄 Btwn ⟨ 𝐴 , 𝑎 ⟩ ∧ ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ) ∧ 𝑄 Btwn ⟨ 𝑎 , 𝑥 ⟩ ) ) → ( 𝑄 = 𝑎 ↔ 𝐴 = 𝑄 ) )
30 29 necon3bid ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝑄 ∧ ( 𝑄 Btwn ⟨ 𝐴 , 𝑎 ⟩ ∧ ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ) ∧ 𝑄 Btwn ⟨ 𝑎 , 𝑥 ⟩ ) ) → ( 𝑄 ≠ 𝑎 ↔ 𝐴 ≠ 𝑄 ) )
31 20 30 mpbird ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝑄 ∧ ( 𝑄 Btwn ⟨ 𝐴 , 𝑎 ⟩ ∧ ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ) ∧ 𝑄 Btwn ⟨ 𝑎 , 𝑥 ⟩ ) ) → 𝑄 ≠ 𝑎 )
32 31 necomd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝑄 ∧ ( 𝑄 Btwn ⟨ 𝐴 , 𝑎 ⟩ ∧ ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ) ∧ 𝑄 Btwn ⟨ 𝑎 , 𝑥 ⟩ ) ) → 𝑎 ≠ 𝑄 )
33 simpr2l ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝑄 ∧ ( 𝑄 Btwn ⟨ 𝐴 , 𝑎 ⟩ ∧ ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ) ∧ 𝑄 Btwn ⟨ 𝑎 , 𝑥 ⟩ ) ) → 𝑄 Btwn ⟨ 𝐴 , 𝑎 ⟩ )
34 22 23 25 24 33 btwncomand ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝑄 ∧ ( 𝑄 Btwn ⟨ 𝐴 , 𝑎 ⟩ ∧ ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ) ∧ 𝑄 Btwn ⟨ 𝑎 , 𝑥 ⟩ ) ) → 𝑄 Btwn ⟨ 𝑎 , 𝐴 ⟩ )
35 simpr3 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝑄 ∧ ( 𝑄 Btwn ⟨ 𝐴 , 𝑎 ⟩ ∧ ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ) ∧ 𝑄 Btwn ⟨ 𝑎 , 𝑥 ⟩ ) ) → 𝑄 Btwn ⟨ 𝑎 , 𝑥 ⟩ )
36 simprr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) )
37 btwnconn2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑎 ≠ 𝑄 ∧ 𝑄 Btwn ⟨ 𝑎 , 𝐴 ⟩ ∧ 𝑄 Btwn ⟨ 𝑎 , 𝑥 ⟩ ) → ( 𝐴 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑄 , 𝐴 ⟩ ) ) )
38 22 24 23 25 36 37 syl122anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑎 ≠ 𝑄 ∧ 𝑄 Btwn ⟨ 𝑎 , 𝐴 ⟩ ∧ 𝑄 Btwn ⟨ 𝑎 , 𝑥 ⟩ ) → ( 𝐴 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑄 , 𝐴 ⟩ ) ) )
39 38 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝑄 ∧ ( 𝑄 Btwn ⟨ 𝐴 , 𝑎 ⟩ ∧ ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ) ∧ 𝑄 Btwn ⟨ 𝑎 , 𝑥 ⟩ ) ) → ( ( 𝑎 ≠ 𝑄 ∧ 𝑄 Btwn ⟨ 𝑎 , 𝐴 ⟩ ∧ 𝑄 Btwn ⟨ 𝑎 , 𝑥 ⟩ ) → ( 𝐴 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑄 , 𝐴 ⟩ ) ) )
40 32 34 35 39 mp3and ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝑄 ∧ ( 𝑄 Btwn ⟨ 𝐴 , 𝑎 ⟩ ∧ ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ) ∧ 𝑄 Btwn ⟨ 𝑎 , 𝑥 ⟩ ) ) → ( 𝐴 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑄 , 𝐴 ⟩ ) )
41 19 40 sylan2br ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝑄 ∧ ( 𝑄 Btwn ⟨ 𝐴 , 𝑎 ⟩ ∧ ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ) ) ∧ 𝑄 Btwn ⟨ 𝑎 , 𝑥 ⟩ ) ) → ( 𝐴 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑄 , 𝐴 ⟩ ) )
42 41 expr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝑄 ∧ ( 𝑄 Btwn ⟨ 𝐴 , 𝑎 ⟩ ∧ ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ) ) ) → ( 𝑄 Btwn ⟨ 𝑎 , 𝑥 ⟩ → ( 𝐴 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑄 , 𝐴 ⟩ ) ) )
43 42 anim1d ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝑄 ∧ ( 𝑄 Btwn ⟨ 𝐴 , 𝑎 ⟩ ∧ ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ) ) ) → ( ( 𝑄 Btwn ⟨ 𝑎 , 𝑥 ⟩ ∧ ⟨ 𝑄 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) → ( ( 𝐴 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑄 , 𝐴 ⟩ ) ∧ ⟨ 𝑄 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) )
44 18 43 sylanb ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ≠ 𝑄 ∧ ( 𝑄 Btwn ⟨ 𝐴 , 𝑎 ⟩ ∧ ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ) ) ) → ( ( 𝑄 Btwn ⟨ 𝑎 , 𝑥 ⟩ ∧ ⟨ 𝑄 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) → ( ( 𝐴 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑄 , 𝐴 ⟩ ) ∧ ⟨ 𝑄 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) )
45 44 an32s ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ≠ 𝑄 ∧ ( 𝑄 Btwn ⟨ 𝐴 , 𝑎 ⟩ ∧ ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝑄 Btwn ⟨ 𝑎 , 𝑥 ⟩ ∧ ⟨ 𝑄 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) → ( ( 𝐴 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑄 , 𝐴 ⟩ ) ∧ ⟨ 𝑄 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) )
46 45 reximdva ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ≠ 𝑄 ∧ ( 𝑄 Btwn ⟨ 𝐴 , 𝑎 ⟩ ∧ ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ) ) ) → ( ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑄 Btwn ⟨ 𝑎 , 𝑥 ⟩ ∧ ⟨ 𝑄 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝐴 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑄 , 𝐴 ⟩ ) ∧ ⟨ 𝑄 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) )
47 17 46 mpd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ≠ 𝑄 ∧ ( 𝑄 Btwn ⟨ 𝐴 , 𝑎 ⟩ ∧ ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝐴 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑄 , 𝐴 ⟩ ) ∧ ⟨ 𝑄 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) )
48 47 expr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐴 ≠ 𝑄 ) → ( ( 𝑄 Btwn ⟨ 𝐴 , 𝑎 ⟩ ∧ ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝐴 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑄 , 𝐴 ⟩ ) ∧ ⟨ 𝑄 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) )
49 48 an32s ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝐴 ≠ 𝑄 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝑄 Btwn ⟨ 𝐴 , 𝑎 ⟩ ∧ ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝐴 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑄 , 𝐴 ⟩ ) ∧ ⟨ 𝑄 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) )
50 49 rexlimdva ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝐴 ≠ 𝑄 ) → ( ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑄 Btwn ⟨ 𝐴 , 𝑎 ⟩ ∧ ⟨ 𝑄 , 𝑎 ⟩ Cgr ⟨ 𝐴 , 𝑄 ⟩ ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝐴 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑄 , 𝐴 ⟩ ) ∧ ⟨ 𝑄 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) ) )
51 10 50 mpd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝐴 ≠ 𝑄 ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝐴 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑄 , 𝐴 ⟩ ) ∧ ⟨ 𝑄 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) )
52 simp2l ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) )
53 simp3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) )
54 axsegcon ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑄 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∧ ⟨ 𝑄 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) )
55 5 52 52 53 54 syl121anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑄 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∧ ⟨ 𝑄 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) )
56 orc ⊢ ( 𝑄 Btwn ⟨ 𝑄 , 𝑥 ⟩ → ( 𝑄 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑄 , 𝐴 ⟩ ) )
57 56 anim1i ⊢ ( ( 𝑄 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∧ ⟨ 𝑄 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) → ( ( 𝑄 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑄 , 𝐴 ⟩ ) ∧ ⟨ 𝑄 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) )
58 57 reximi ⊢ ( ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑄 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∧ ⟨ 𝑄 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝑄 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑄 , 𝐴 ⟩ ) ∧ ⟨ 𝑄 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) )
59 55 58 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝑄 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑄 , 𝐴 ⟩ ) ∧ ⟨ 𝑄 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) )
60 4 51 59 pm2.61ne ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝐴 Btwn ⟨ 𝑄 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑄 , 𝐴 ⟩ ) ∧ ⟨ 𝑄 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐶 ⟩ ) )