Metamath Proof Explorer

Theorem brbtwn

Description: The binary relation form of the betweenness predicate. The statement A Btwn <. B , C >. should be informally read as " A lies on a line segment between B and C . This exact definition is abstracted away by Tarski's geometry axioms later on. (Contributed by Scott Fenton, 3-Jun-2013)

Ref Expression
Assertion brbtwn ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A Btwn B C ↔ ∃ t ∈ 0 1 ∀ i ∈ 1 … N A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i

Proof

Step Hyp Ref Expression
1 df-btwn ⊢ Btwn = y z x | ∃ n ∈ ℕ y ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ x ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n x ⁡ i = 1 − t ⁢ y ⁡ i + t ⁢ z ⁡ i -1
2 1 breqi ⊢ A Btwn B C ↔ A y z x | ∃ n ∈ ℕ y ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ x ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n x ⁡ i = 1 − t ⁢ y ⁡ i + t ⁢ z ⁡ i -1 B C
3 opex ⊢ B C ∈ V
4 brcnvg ⊢ A ∈ 𝔼 ⁡ N ∧ B C ∈ V → A y z x | ∃ n ∈ ℕ y ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ x ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n x ⁡ i = 1 − t ⁢ y ⁡ i + t ⁢ z ⁡ i -1 B C ↔ B C y z x | ∃ n ∈ ℕ y ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ x ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n x ⁡ i = 1 − t ⁢ y ⁡ i + t ⁢ z ⁡ i A
5 3 4 mpan2 ⊢ A ∈ 𝔼 ⁡ N → A y z x | ∃ n ∈ ℕ y ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ x ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n x ⁡ i = 1 − t ⁢ y ⁡ i + t ⁢ z ⁡ i -1 B C ↔ B C y z x | ∃ n ∈ ℕ y ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ x ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n x ⁡ i = 1 − t ⁢ y ⁡ i + t ⁢ z ⁡ i A
6 5 3ad2ant1 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A y z x | ∃ n ∈ ℕ y ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ x ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n x ⁡ i = 1 − t ⁢ y ⁡ i + t ⁢ z ⁡ i -1 B C ↔ B C y z x | ∃ n ∈ ℕ y ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ x ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n x ⁡ i = 1 − t ⁢ y ⁡ i + t ⁢ z ⁡ i A
7 df-br ⊢ B C y z x | ∃ n ∈ ℕ y ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ x ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n x ⁡ i = 1 − t ⁢ y ⁡ i + t ⁢ z ⁡ i A ↔ B C A ∈ y z x | ∃ n ∈ ℕ y ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ x ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n x ⁡ i = 1 − t ⁢ y ⁡ i + t ⁢ z ⁡ i
8 eleq1 ⊢ y = B → y ∈ 𝔼 ⁡ n ↔ B ∈ 𝔼 ⁡ n
9 8 3anbi1d ⊢ y = B → y ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ x ∈ 𝔼 ⁡ n ↔ B ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ x ∈ 𝔼 ⁡ n
10 fveq1 ⊢ y = B → y ⁡ i = B ⁡ i
11 10 oveq2d ⊢ y = B → 1 − t ⁢ y ⁡ i = 1 − t ⁢ B ⁡ i
12 11 oveq1d ⊢ y = B → 1 − t ⁢ y ⁡ i + t ⁢ z ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ z ⁡ i
13 12 eqeq2d ⊢ y = B → x ⁡ i = 1 − t ⁢ y ⁡ i + t ⁢ z ⁡ i ↔ x ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ z ⁡ i
14 13 rexralbidv ⊢ y = B → ∃ t ∈ 0 1 ∀ i ∈ 1 … n x ⁡ i = 1 − t ⁢ y ⁡ i + t ⁢ z ⁡ i ↔ ∃ t ∈ 0 1 ∀ i ∈ 1 … n x ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ z ⁡ i
15 9 14 anbi12d ⊢ y = B → y ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ x ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n x ⁡ i = 1 − t ⁢ y ⁡ i + t ⁢ z ⁡ i ↔ B ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ x ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n x ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ z ⁡ i
16 15 rexbidv ⊢ y = B → ∃ n ∈ ℕ y ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ x ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n x ⁡ i = 1 − t ⁢ y ⁡ i + t ⁢ z ⁡ i ↔ ∃ n ∈ ℕ B ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ x ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n x ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ z ⁡ i
17 eleq1 ⊢ z = C → z ∈ 𝔼 ⁡ n ↔ C ∈ 𝔼 ⁡ n
18 17 3anbi2d ⊢ z = C → B ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ x ∈ 𝔼 ⁡ n ↔ B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ x ∈ 𝔼 ⁡ n
19 fveq1 ⊢ z = C → z ⁡ i = C ⁡ i
20 19 oveq2d ⊢ z = C → t ⁢ z ⁡ i = t ⁢ C ⁡ i
21 20 oveq2d ⊢ z = C → 1 − t ⁢ B ⁡ i + t ⁢ z ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i
22 21 eqeq2d ⊢ z = C → x ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ z ⁡ i ↔ x ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i
23 22 rexralbidv ⊢ z = C → ∃ t ∈ 0 1 ∀ i ∈ 1 … n x ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ z ⁡ i ↔ ∃ t ∈ 0 1 ∀ i ∈ 1 … n x ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i
24 18 23 anbi12d ⊢ z = C → B ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ x ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n x ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ z ⁡ i ↔ B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ x ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n x ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i
25 24 rexbidv ⊢ z = C → ∃ n ∈ ℕ B ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ x ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n x ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ z ⁡ i ↔ ∃ n ∈ ℕ B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ x ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n x ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i
26 eleq1 ⊢ x = A → x ∈ 𝔼 ⁡ n ↔ A ∈ 𝔼 ⁡ n
27 26 3anbi3d ⊢ x = A → B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ x ∈ 𝔼 ⁡ n ↔ B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ A ∈ 𝔼 ⁡ n
28 fveq1 ⊢ x = A → x ⁡ i = A ⁡ i
29 28 eqeq1d ⊢ x = A → x ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i ↔ A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i
30 29 rexralbidv ⊢ x = A → ∃ t ∈ 0 1 ∀ i ∈ 1 … n x ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i ↔ ∃ t ∈ 0 1 ∀ i ∈ 1 … n A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i
31 27 30 anbi12d ⊢ x = A → B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ x ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n x ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i ↔ B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ A ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i
32 31 rexbidv ⊢ x = A → ∃ n ∈ ℕ B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ x ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n x ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i ↔ ∃ n ∈ ℕ B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ A ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i
33 16 25 32 eloprabg ⊢ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N → B C A ∈ y z x | ∃ n ∈ ℕ y ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ x ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n x ⁡ i = 1 − t ⁢ y ⁡ i + t ⁢ z ⁡ i ↔ ∃ n ∈ ℕ B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ A ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i
34 simp1 ⊢ B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ A ∈ 𝔼 ⁡ n → B ∈ 𝔼 ⁡ n
35 simp1 ⊢ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N → B ∈ 𝔼 ⁡ N
36 eedimeq ⊢ B ∈ 𝔼 ⁡ n ∧ B ∈ 𝔼 ⁡ N → n = N
37 34 35 36 syl2anr ⊢ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ A ∈ 𝔼 ⁡ n → n = N
38 oveq2 ⊢ n = N → 1 … n = 1 … N
39 38 raleqdv ⊢ n = N → ∀ i ∈ 1 … n A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i ↔ ∀ i ∈ 1 … N A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i
40 39 rexbidv ⊢ n = N → ∃ t ∈ 0 1 ∀ i ∈ 1 … n A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i ↔ ∃ t ∈ 0 1 ∀ i ∈ 1 … N A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i
41 37 40 syl ⊢ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ A ∈ 𝔼 ⁡ n → ∃ t ∈ 0 1 ∀ i ∈ 1 … n A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i ↔ ∃ t ∈ 0 1 ∀ i ∈ 1 … N A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i
42 41 biimpd ⊢ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ A ∈ 𝔼 ⁡ n → ∃ t ∈ 0 1 ∀ i ∈ 1 … n A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i → ∃ t ∈ 0 1 ∀ i ∈ 1 … N A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i
43 42 expimpd ⊢ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N → B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ A ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i → ∃ t ∈ 0 1 ∀ i ∈ 1 … N A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i
44 43 rexlimdvw ⊢ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N → ∃ n ∈ ℕ B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ A ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i → ∃ t ∈ 0 1 ∀ i ∈ 1 … N A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i
45 eleenn ⊢ B ∈ 𝔼 ⁡ N → N ∈ ℕ
46 45 3ad2ant1 ⊢ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N → N ∈ ℕ
47 fveq2 ⊢ n = N → 𝔼 ⁡ n = 𝔼 ⁡ N
48 47 eleq2d ⊢ n = N → B ∈ 𝔼 ⁡ n ↔ B ∈ 𝔼 ⁡ N
49 47 eleq2d ⊢ n = N → C ∈ 𝔼 ⁡ n ↔ C ∈ 𝔼 ⁡ N
50 47 eleq2d ⊢ n = N → A ∈ 𝔼 ⁡ n ↔ A ∈ 𝔼 ⁡ N
51 48 49 50 3anbi123d ⊢ n = N → B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ A ∈ 𝔼 ⁡ n ↔ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N
52 51 40 anbi12d ⊢ n = N → B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ A ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i ↔ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … N A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i
53 52 rspcev ⊢ N ∈ ℕ ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … N A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i → ∃ n ∈ ℕ B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ A ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i
54 53 exp32 ⊢ N ∈ ℕ → B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N → ∃ t ∈ 0 1 ∀ i ∈ 1 … N A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i → ∃ n ∈ ℕ B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ A ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i
55 46 54 mpcom ⊢ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N → ∃ t ∈ 0 1 ∀ i ∈ 1 … N A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i → ∃ n ∈ ℕ B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ A ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i
56 44 55 impbid ⊢ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N → ∃ n ∈ ℕ B ∈ 𝔼 ⁡ n ∧ C ∈ 𝔼 ⁡ n ∧ A ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i ↔ ∃ t ∈ 0 1 ∀ i ∈ 1 … N A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i
57 33 56 bitrd ⊢ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N → B C A ∈ y z x | ∃ n ∈ ℕ y ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ x ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n x ⁡ i = 1 − t ⁢ y ⁡ i + t ⁢ z ⁡ i ↔ ∃ t ∈ 0 1 ∀ i ∈ 1 … N A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i
58 57 3comr ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → B C A ∈ y z x | ∃ n ∈ ℕ y ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ x ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n x ⁡ i = 1 − t ⁢ y ⁡ i + t ⁢ z ⁡ i ↔ ∃ t ∈ 0 1 ∀ i ∈ 1 … N A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i
59 7 58 syl5bb ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → B C y z x | ∃ n ∈ ℕ y ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ x ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n x ⁡ i = 1 − t ⁢ y ⁡ i + t ⁢ z ⁡ i A ↔ ∃ t ∈ 0 1 ∀ i ∈ 1 … N A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i
60 6 59 bitrd ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A y z x | ∃ n ∈ ℕ y ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ x ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n x ⁡ i = 1 − t ⁢ y ⁡ i + t ⁢ z ⁡ i -1 B C ↔ ∃ t ∈ 0 1 ∀ i ∈ 1 … N A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i
61 2 60 syl5bb ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A Btwn B C ↔ ∃ t ∈ 0 1 ∀ i ∈ 1 … N A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ C ⁡ i