Metamath Proof Explorer

Definition df-btwn

Description: Define the Euclidean betweenness predicate. For details, see brbtwn . (Contributed by Scott Fenton, 3-Jun-2013)

Ref Expression
Assertion df-btwn ⊢ Btwn = x z y | ∃ n ∈ ℕ x ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ y ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n y ⁡ i = 1 − t ⁢ x ⁡ i + t ⁢ z ⁡ i -1

Detailed syntax breakdown

Step Hyp Ref Expression
0 cbtwn class Btwn
1 vx setvar x
2 vz setvar z
3 vy setvar y
4 vn setvar n
5 cn class ℕ
6 1 cv setvar x
7 cee class 𝔼
8 4 cv setvar n
9 8 7 cfv class 𝔼 ⁡ n
10 6 9 wcel wff x ∈ 𝔼 ⁡ n
11 2 cv setvar z
12 11 9 wcel wff z ∈ 𝔼 ⁡ n
13 3 cv setvar y
14 13 9 wcel wff y ∈ 𝔼 ⁡ n
15 10 12 14 w3a wff x ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ y ∈ 𝔼 ⁡ n
16 vt setvar t
17 cc0 class 0
18 cicc class .
19 c1 class 1
20 17 19 18 co class 0 1
21 vi setvar i
22 cfz class …
23 19 8 22 co class 1 … n
24 21 cv setvar i
25 24 13 cfv class y ⁡ i
26 cmin class −
27 16 cv setvar t
28 19 27 26 co class 1 − t
29 cmul class ×
30 24 6 cfv class x ⁡ i
31 28 30 29 co class 1 − t ⁢ x ⁡ i
32 caddc class +
33 24 11 cfv class z ⁡ i
34 27 33 29 co class t ⁢ z ⁡ i
35 31 34 32 co class 1 − t ⁢ x ⁡ i + t ⁢ z ⁡ i
36 25 35 wceq wff y ⁡ i = 1 − t ⁢ x ⁡ i + t ⁢ z ⁡ i
37 36 21 23 wral wff ∀ i ∈ 1 … n y ⁡ i = 1 − t ⁢ x ⁡ i + t ⁢ z ⁡ i
38 37 16 20 wrex wff ∃ t ∈ 0 1 ∀ i ∈ 1 … n y ⁡ i = 1 − t ⁢ x ⁡ i + t ⁢ z ⁡ i
39 15 38 wa wff x ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ y ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n y ⁡ i = 1 − t ⁢ x ⁡ i + t ⁢ z ⁡ i
40 39 4 5 wrex wff ∃ n ∈ ℕ x ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ y ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n y ⁡ i = 1 − t ⁢ x ⁡ i + t ⁢ z ⁡ i
41 40 1 2 3 coprab class x z y | ∃ n ∈ ℕ x ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ y ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n y ⁡ i = 1 − t ⁢ x ⁡ i + t ⁢ z ⁡ i
42 41 ccnv class x z y | ∃ n ∈ ℕ x ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ y ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n y ⁡ i = 1 − t ⁢ x ⁡ i + t ⁢ z ⁡ i -1
43 0 42 wceq wff Btwn = x z y | ∃ n ∈ ℕ x ∈ 𝔼 ⁡ n ∧ z ∈ 𝔼 ⁡ n ∧ y ∈ 𝔼 ⁡ n ∧ ∃ t ∈ 0 1 ∀ i ∈ 1 … n y ⁡ i = 1 − t ⁢ x ⁡ i + t ⁢ z ⁡ i -1