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=xzy|∃n∈ℕx∈𝔼⁡n∧z∈𝔼⁡n∧y∈𝔼⁡n∧∃t∈01∀i∈1…ny⁡i=1−t⁢x⁡i+t⁢z⁡i-1

Detailed syntax breakdown

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