Metamath Proof Explorer

Theorem axeuclid

Description: Euclid's axiom. Take an angle B A C and a point D between B and C . Now, if you extend the segment A D to a point T , then T lies between two points x and y that lie on the angle. Axiom A10 of Schwabhauser p. 13. (Contributed by Scott Fenton, 9-Sep-2013)

Ref Expression
Assertion axeuclid ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N → D Btwn A T ∧ D Btwn B C ∧ A ≠ D → ∃ x ∈ 𝔼 ⁡ N ∃ y ∈ 𝔼 ⁡ N B Btwn A x ∧ C Btwn A y ∧ T Btwn x y

Proof

Step Hyp Ref Expression
1 simpl21 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i ∧ A ≠ D → A ∈ 𝔼 ⁡ N
2 simpl22 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i ∧ A ≠ D → B ∈ 𝔼 ⁡ N
3 1 2 jca ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i ∧ A ≠ D → A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N
4 simpl23 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i ∧ A ≠ D → C ∈ 𝔼 ⁡ N
5 simpl3r ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i ∧ A ≠ D → T ∈ 𝔼 ⁡ N
6 4 5 jca ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i ∧ A ≠ D → C ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N
7 simprll ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i ∧ A ≠ D → p ∈ 0 1
8 simprlr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i ∧ A ≠ D → q ∈ 0 1
9 simp21 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N
10 9 ad2antrr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ p = 0 → A ∈ 𝔼 ⁡ N
11 fveecn ⊢ A ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → A ⁡ i ∈ ℂ
12 10 11 sylan ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ p = 0 ∧ i ∈ 1 … N → A ⁡ i ∈ ℂ
13 simp3r ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N → T ∈ 𝔼 ⁡ N
14 13 ad2antrr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ p = 0 → T ∈ 𝔼 ⁡ N
15 fveecn ⊢ T ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → T ⁡ i ∈ ℂ
16 14 15 sylan ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ p = 0 ∧ i ∈ 1 … N → T ⁡ i ∈ ℂ
17 mulid2 ⊢ A ⁡ i ∈ ℂ → 1 ⁢ A ⁡ i = A ⁡ i
18 mul02 ⊢ T ⁡ i ∈ ℂ → 0 ⋅ T ⁡ i = 0
19 17 18 oveqan12d ⊢ A ⁡ i ∈ ℂ ∧ T ⁡ i ∈ ℂ → 1 ⁢ A ⁡ i + 0 ⋅ T ⁡ i = A ⁡ i + 0
20 addid1 ⊢ A ⁡ i ∈ ℂ → A ⁡ i + 0 = A ⁡ i
21 20 adantr ⊢ A ⁡ i ∈ ℂ ∧ T ⁡ i ∈ ℂ → A ⁡ i + 0 = A ⁡ i
22 19 21 eqtrd ⊢ A ⁡ i ∈ ℂ ∧ T ⁡ i ∈ ℂ → 1 ⁢ A ⁡ i + 0 ⋅ T ⁡ i = A ⁡ i
23 12 16 22 syl2anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ p = 0 ∧ i ∈ 1 … N → 1 ⁢ A ⁡ i + 0 ⋅ T ⁡ i = A ⁡ i
24 oveq2 ⊢ p = 0 → 1 − p = 1 − 0
25 1m0e1 ⊢ 1 − 0 = 1
26 24 25 eqtrdi ⊢ p = 0 → 1 − p = 1
27 26 oveq1d ⊢ p = 0 → 1 − p ⁢ A ⁡ i = 1 ⁢ A ⁡ i
28 oveq1 ⊢ p = 0 → p ⁢ T ⁡ i = 0 ⋅ T ⁡ i
29 27 28 oveq12d ⊢ p = 0 → 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i = 1 ⁢ A ⁡ i + 0 ⋅ T ⁡ i
30 29 eqeq1d ⊢ p = 0 → 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i = A ⁡ i ↔ 1 ⁢ A ⁡ i + 0 ⋅ T ⁡ i = A ⁡ i
31 30 ad2antlr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ p = 0 ∧ i ∈ 1 … N → 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i = A ⁡ i ↔ 1 ⁢ A ⁡ i + 0 ⋅ T ⁡ i = A ⁡ i
32 23 31 mpbird ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ p = 0 ∧ i ∈ 1 … N → 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i = A ⁡ i
33 32 eqeq2d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ p = 0 ∧ i ∈ 1 … N → D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ↔ D ⁡ i = A ⁡ i
34 eqcom ⊢ D ⁡ i = A ⁡ i ↔ A ⁡ i = D ⁡ i
35 33 34 bitrdi ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ p = 0 ∧ i ∈ 1 … N → D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ↔ A ⁡ i = D ⁡ i
36 35 biimpd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ p = 0 ∧ i ∈ 1 … N → D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i → A ⁡ i = D ⁡ i
37 36 adantrd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ p = 0 ∧ i ∈ 1 … N → D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i → A ⁡ i = D ⁡ i
38 37 ralimdva ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ p = 0 → ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i → ∀ i ∈ 1 … N A ⁡ i = D ⁡ i
39 38 impancom ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i → p = 0 → ∀ i ∈ 1 … N A ⁡ i = D ⁡ i
40 9 ad2antrr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i → A ∈ 𝔼 ⁡ N
41 simp3l ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N → D ∈ 𝔼 ⁡ N
42 41 ad2antrr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i → D ∈ 𝔼 ⁡ N
43 eqeefv ⊢ A ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → A = D ↔ ∀ i ∈ 1 … N A ⁡ i = D ⁡ i
44 40 42 43 syl2anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i → A = D ↔ ∀ i ∈ 1 … N A ⁡ i = D ⁡ i
45 39 44 sylibrd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i → p = 0 → A = D
46 45 necon3d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i → A ≠ D → p ≠ 0
47 46 impr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i ∧ A ≠ D → p ≠ 0
48 47 anasss ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i ∧ A ≠ D → p ≠ 0
49 eqtr2 ⊢ D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i → 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i
50 49 ralimi ⊢ ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i → ∀ i ∈ 1 … N 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i
51 50 adantr ⊢ ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i ∧ A ≠ D → ∀ i ∈ 1 … N 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i
52 51 ad2antll ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i ∧ A ≠ D → ∀ i ∈ 1 … N 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i
53 axeuclidlem ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ p ≠ 0 ∧ ∀ i ∈ 1 … N 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i → ∃ x ∈ 𝔼 ⁡ N ∃ y ∈ 𝔼 ⁡ N ∃ r ∈ 0 1 ∃ s ∈ 0 1 ∃ u ∈ 0 1 ∀ i ∈ 1 … N B ⁡ i = 1 − r ⁢ A ⁡ i + r ⁢ x ⁡ i ∧ C ⁡ i = 1 − s ⁢ A ⁡ i + s ⁢ y ⁡ i ∧ T ⁡ i = 1 − u ⁢ x ⁡ i + u ⁢ y ⁡ i
54 3 6 7 8 48 52 53 syl231anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ p ∈ 0 1 ∧ q ∈ 0 1 ∧ ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i ∧ A ≠ D → ∃ x ∈ 𝔼 ⁡ N ∃ y ∈ 𝔼 ⁡ N ∃ r ∈ 0 1 ∃ s ∈ 0 1 ∃ u ∈ 0 1 ∀ i ∈ 1 … N B ⁡ i = 1 − r ⁢ A ⁡ i + r ⁢ x ⁡ i ∧ C ⁡ i = 1 − s ⁢ A ⁡ i + s ⁢ y ⁡ i ∧ T ⁡ i = 1 − u ⁢ x ⁡ i + u ⁢ y ⁡ i
55 54 exp32 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N → p ∈ 0 1 ∧ q ∈ 0 1 → ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i ∧ A ≠ D → ∃ x ∈ 𝔼 ⁡ N ∃ y ∈ 𝔼 ⁡ N ∃ r ∈ 0 1 ∃ s ∈ 0 1 ∃ u ∈ 0 1 ∀ i ∈ 1 … N B ⁡ i = 1 − r ⁢ A ⁡ i + r ⁢ x ⁡ i ∧ C ⁡ i = 1 − s ⁢ A ⁡ i + s ⁢ y ⁡ i ∧ T ⁡ i = 1 − u ⁢ x ⁡ i + u ⁢ y ⁡ i
56 55 rexlimdvv ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N → ∃ p ∈ 0 1 ∃ q ∈ 0 1 ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i ∧ A ≠ D → ∃ x ∈ 𝔼 ⁡ N ∃ y ∈ 𝔼 ⁡ N ∃ r ∈ 0 1 ∃ s ∈ 0 1 ∃ u ∈ 0 1 ∀ i ∈ 1 … N B ⁡ i = 1 − r ⁢ A ⁡ i + r ⁢ x ⁡ i ∧ C ⁡ i = 1 − s ⁢ A ⁡ i + s ⁢ y ⁡ i ∧ T ⁡ i = 1 − u ⁢ x ⁡ i + u ⁢ y ⁡ i
57 brbtwn ⊢ D ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N → D Btwn A T ↔ ∃ p ∈ 0 1 ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i
58 41 9 13 57 syl3anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N → D Btwn A T ↔ ∃ p ∈ 0 1 ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i
59 simp22 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N → B ∈ 𝔼 ⁡ N
60 simp23 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N → C ∈ 𝔼 ⁡ N
61 brbtwn ⊢ D ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → D Btwn B C ↔ ∃ q ∈ 0 1 ∀ i ∈ 1 … N D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i
62 41 59 60 61 syl3anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N → D Btwn B C ↔ ∃ q ∈ 0 1 ∀ i ∈ 1 … N D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i
63 58 62 3anbi12d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N → D Btwn A T ∧ D Btwn B C ∧ A ≠ D ↔ ∃ p ∈ 0 1 ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ ∃ q ∈ 0 1 ∀ i ∈ 1 … N D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i ∧ A ≠ D
64 r19.26 ⊢ ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i ↔ ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ ∀ i ∈ 1 … N D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i
65 64 2rexbii ⊢ ∃ p ∈ 0 1 ∃ q ∈ 0 1 ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i ↔ ∃ p ∈ 0 1 ∃ q ∈ 0 1 ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ ∀ i ∈ 1 … N D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i
66 reeanv ⊢ ∃ p ∈ 0 1 ∃ q ∈ 0 1 ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ ∀ i ∈ 1 … N D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i ↔ ∃ p ∈ 0 1 ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ ∃ q ∈ 0 1 ∀ i ∈ 1 … N D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i
67 65 66 bitri ⊢ ∃ p ∈ 0 1 ∃ q ∈ 0 1 ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i ↔ ∃ p ∈ 0 1 ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ ∃ q ∈ 0 1 ∀ i ∈ 1 … N D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i
68 67 anbi1i ⊢ ∃ p ∈ 0 1 ∃ q ∈ 0 1 ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i ∧ A ≠ D ↔ ∃ p ∈ 0 1 ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ ∃ q ∈ 0 1 ∀ i ∈ 1 … N D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i ∧ A ≠ D
69 r19.41vv ⊢ ∃ p ∈ 0 1 ∃ q ∈ 0 1 ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i ∧ A ≠ D ↔ ∃ p ∈ 0 1 ∃ q ∈ 0 1 ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i ∧ A ≠ D
70 df-3an ⊢ ∃ p ∈ 0 1 ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ ∃ q ∈ 0 1 ∀ i ∈ 1 … N D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i ∧ A ≠ D ↔ ∃ p ∈ 0 1 ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ ∃ q ∈ 0 1 ∀ i ∈ 1 … N D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i ∧ A ≠ D
71 68 69 70 3bitr4i ⊢ ∃ p ∈ 0 1 ∃ q ∈ 0 1 ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i ∧ A ≠ D ↔ ∃ p ∈ 0 1 ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ ∃ q ∈ 0 1 ∀ i ∈ 1 … N D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i ∧ A ≠ D
72 63 71 bitr4di ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N → D Btwn A T ∧ D Btwn B C ∧ A ≠ D ↔ ∃ p ∈ 0 1 ∃ q ∈ 0 1 ∀ i ∈ 1 … N D ⁡ i = 1 − p ⁢ A ⁡ i + p ⁢ T ⁡ i ∧ D ⁡ i = 1 − q ⁢ B ⁡ i + q ⁢ C ⁡ i ∧ A ≠ D
73 simpl22 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N ∧ y ∈ 𝔼 ⁡ N → B ∈ 𝔼 ⁡ N
74 simpl21 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N ∧ y ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N
75 simprl ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N ∧ y ∈ 𝔼 ⁡ N → x ∈ 𝔼 ⁡ N
76 brbtwn ⊢ B ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → B Btwn A x ↔ ∃ r ∈ 0 1 ∀ i ∈ 1 … N B ⁡ i = 1 − r ⁢ A ⁡ i + r ⁢ x ⁡ i
77 73 74 75 76 syl3anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N ∧ y ∈ 𝔼 ⁡ N → B Btwn A x ↔ ∃ r ∈ 0 1 ∀ i ∈ 1 … N B ⁡ i = 1 − r ⁢ A ⁡ i + r ⁢ x ⁡ i
78 simpl23 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N ∧ y ∈ 𝔼 ⁡ N → C ∈ 𝔼 ⁡ N
79 simprr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N ∧ y ∈ 𝔼 ⁡ N → y ∈ 𝔼 ⁡ N
80 brbtwn ⊢ C ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ y ∈ 𝔼 ⁡ N → C Btwn A y ↔ ∃ s ∈ 0 1 ∀ i ∈ 1 … N C ⁡ i = 1 − s ⁢ A ⁡ i + s ⁢ y ⁡ i
81 78 74 79 80 syl3anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N ∧ y ∈ 𝔼 ⁡ N → C Btwn A y ↔ ∃ s ∈ 0 1 ∀ i ∈ 1 … N C ⁡ i = 1 − s ⁢ A ⁡ i + s ⁢ y ⁡ i
82 simpl3r ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N ∧ y ∈ 𝔼 ⁡ N → T ∈ 𝔼 ⁡ N
83 brbtwn ⊢ T ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N ∧ y ∈ 𝔼 ⁡ N → T Btwn x y ↔ ∃ u ∈ 0 1 ∀ i ∈ 1 … N T ⁡ i = 1 − u ⁢ x ⁡ i + u ⁢ y ⁡ i
84 82 75 79 83 syl3anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N ∧ y ∈ 𝔼 ⁡ N → T Btwn x y ↔ ∃ u ∈ 0 1 ∀ i ∈ 1 … N T ⁡ i = 1 − u ⁢ x ⁡ i + u ⁢ y ⁡ i
85 77 81 84 3anbi123d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N ∧ y ∈ 𝔼 ⁡ N → B Btwn A x ∧ C Btwn A y ∧ T Btwn x y ↔ ∃ r ∈ 0 1 ∀ i ∈ 1 … N B ⁡ i = 1 − r ⁢ A ⁡ i + r ⁢ x ⁡ i ∧ ∃ s ∈ 0 1 ∀ i ∈ 1 … N C ⁡ i = 1 − s ⁢ A ⁡ i + s ⁢ y ⁡ i ∧ ∃ u ∈ 0 1 ∀ i ∈ 1 … N T ⁡ i = 1 − u ⁢ x ⁡ i + u ⁢ y ⁡ i
86 r19.26-3 ⊢ ∀ i ∈ 1 … N B ⁡ i = 1 − r ⁢ A ⁡ i + r ⁢ x ⁡ i ∧ C ⁡ i = 1 − s ⁢ A ⁡ i + s ⁢ y ⁡ i ∧ T ⁡ i = 1 − u ⁢ x ⁡ i + u ⁢ y ⁡ i ↔ ∀ i ∈ 1 … N B ⁡ i = 1 − r ⁢ A ⁡ i + r ⁢ x ⁡ i ∧ ∀ i ∈ 1 … N C ⁡ i = 1 − s ⁢ A ⁡ i + s ⁢ y ⁡ i ∧ ∀ i ∈ 1 … N T ⁡ i = 1 − u ⁢ x ⁡ i + u ⁢ y ⁡ i
87 86 rexbii ⊢ ∃ u ∈ 0 1 ∀ i ∈ 1 … N B ⁡ i = 1 − r ⁢ A ⁡ i + r ⁢ x ⁡ i ∧ C ⁡ i = 1 − s ⁢ A ⁡ i + s ⁢ y ⁡ i ∧ T ⁡ i = 1 − u ⁢ x ⁡ i + u ⁢ y ⁡ i ↔ ∃ u ∈ 0 1 ∀ i ∈ 1 … N B ⁡ i = 1 − r ⁢ A ⁡ i + r ⁢ x ⁡ i ∧ ∀ i ∈ 1 … N C ⁡ i = 1 − s ⁢ A ⁡ i + s ⁢ y ⁡ i ∧ ∀ i ∈ 1 … N T ⁡ i = 1 − u ⁢ x ⁡ i + u ⁢ y ⁡ i
88 87 2rexbii ⊢ ∃ r ∈ 0 1 ∃ s ∈ 0 1 ∃ u ∈ 0 1 ∀ i ∈ 1 … N B ⁡ i = 1 − r ⁢ A ⁡ i + r ⁢ x ⁡ i ∧ C ⁡ i = 1 − s ⁢ A ⁡ i + s ⁢ y ⁡ i ∧ T ⁡ i = 1 − u ⁢ x ⁡ i + u ⁢ y ⁡ i ↔ ∃ r ∈ 0 1 ∃ s ∈ 0 1 ∃ u ∈ 0 1 ∀ i ∈ 1 … N B ⁡ i = 1 − r ⁢ A ⁡ i + r ⁢ x ⁡ i ∧ ∀ i ∈ 1 … N C ⁡ i = 1 − s ⁢ A ⁡ i + s ⁢ y ⁡ i ∧ ∀ i ∈ 1 … N T ⁡ i = 1 − u ⁢ x ⁡ i + u ⁢ y ⁡ i
89 3reeanv ⊢ ∃ r ∈ 0 1 ∃ s ∈ 0 1 ∃ u ∈ 0 1 ∀ i ∈ 1 … N B ⁡ i = 1 − r ⁢ A ⁡ i + r ⁢ x ⁡ i ∧ ∀ i ∈ 1 … N C ⁡ i = 1 − s ⁢ A ⁡ i + s ⁢ y ⁡ i ∧ ∀ i ∈ 1 … N T ⁡ i = 1 − u ⁢ x ⁡ i + u ⁢ y ⁡ i ↔ ∃ r ∈ 0 1 ∀ i ∈ 1 … N B ⁡ i = 1 − r ⁢ A ⁡ i + r ⁢ x ⁡ i ∧ ∃ s ∈ 0 1 ∀ i ∈ 1 … N C ⁡ i = 1 − s ⁢ A ⁡ i + s ⁢ y ⁡ i ∧ ∃ u ∈ 0 1 ∀ i ∈ 1 … N T ⁡ i = 1 − u ⁢ x ⁡ i + u ⁢ y ⁡ i
90 88 89 bitri ⊢ ∃ r ∈ 0 1 ∃ s ∈ 0 1 ∃ u ∈ 0 1 ∀ i ∈ 1 … N B ⁡ i = 1 − r ⁢ A ⁡ i + r ⁢ x ⁡ i ∧ C ⁡ i = 1 − s ⁢ A ⁡ i + s ⁢ y ⁡ i ∧ T ⁡ i = 1 − u ⁢ x ⁡ i + u ⁢ y ⁡ i ↔ ∃ r ∈ 0 1 ∀ i ∈ 1 … N B ⁡ i = 1 − r ⁢ A ⁡ i + r ⁢ x ⁡ i ∧ ∃ s ∈ 0 1 ∀ i ∈ 1 … N C ⁡ i = 1 − s ⁢ A ⁡ i + s ⁢ y ⁡ i ∧ ∃ u ∈ 0 1 ∀ i ∈ 1 … N T ⁡ i = 1 − u ⁢ x ⁡ i + u ⁢ y ⁡ i
91 85 90 bitr4di ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N ∧ y ∈ 𝔼 ⁡ N → B Btwn A x ∧ C Btwn A y ∧ T Btwn x y ↔ ∃ r ∈ 0 1 ∃ s ∈ 0 1 ∃ u ∈ 0 1 ∀ i ∈ 1 … N B ⁡ i = 1 − r ⁢ A ⁡ i + r ⁢ x ⁡ i ∧ C ⁡ i = 1 − s ⁢ A ⁡ i + s ⁢ y ⁡ i ∧ T ⁡ i = 1 − u ⁢ x ⁡ i + u ⁢ y ⁡ i
92 91 2rexbidva ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N → ∃ x ∈ 𝔼 ⁡ N ∃ y ∈ 𝔼 ⁡ N B Btwn A x ∧ C Btwn A y ∧ T Btwn x y ↔ ∃ x ∈ 𝔼 ⁡ N ∃ y ∈ 𝔼 ⁡ N ∃ r ∈ 0 1 ∃ s ∈ 0 1 ∃ u ∈ 0 1 ∀ i ∈ 1 … N B ⁡ i = 1 − r ⁢ A ⁡ i + r ⁢ x ⁡ i ∧ C ⁡ i = 1 − s ⁢ A ⁡ i + s ⁢ y ⁡ i ∧ T ⁡ i = 1 − u ⁢ x ⁡ i + u ⁢ y ⁡ i
93 56 72 92 3imtr4d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ T ∈ 𝔼 ⁡ N → D Btwn A T ∧ D Btwn B C ∧ A ≠ D → ∃ x ∈ 𝔼 ⁡ N ∃ y ∈ 𝔼 ⁡ N B Btwn A x ∧ C Btwn A y ∧ T Btwn x y