MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-btwn Structured version   Visualization version   GIF version

Definition df-btwn 25572
Description: Define the Euclidean betweenness predicate. For details, see brbtwn 25579. (Contributed by Scott Fenton, 3-Jun-2013.)
Assertion
Ref Expression
df-btwn Btwn = {⟨⟨𝑥, 𝑧⟩, 𝑦⟩ ∣ ∃𝑛 ∈ ℕ ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑦𝑖) = (((1 − 𝑡) · (𝑥𝑖)) + (𝑡 · (𝑧𝑖))))}
Distinct variable group:   𝑥,𝑛,𝑦,𝑧,𝑡,𝑖

Detailed syntax breakdown of Definition df-btwn
StepHypRef Expression
1 cbtwn 25569 . 2 class Btwn
2 vx . . . . . . . . 9 setvar 𝑥
32cv 1474 . . . . . . . 8 class 𝑥
4 vn . . . . . . . . . 10 setvar 𝑛
54cv 1474 . . . . . . . . 9 class 𝑛
6 cee 25568 . . . . . . . . 9 class 𝔼
75, 6cfv 5804 . . . . . . . 8 class (𝔼‘𝑛)
83, 7wcel 1977 . . . . . . 7 wff 𝑥 ∈ (𝔼‘𝑛)
9 vz . . . . . . . . 9 setvar 𝑧
109cv 1474 . . . . . . . 8 class 𝑧
1110, 7wcel 1977 . . . . . . 7 wff 𝑧 ∈ (𝔼‘𝑛)
12 vy . . . . . . . . 9 setvar 𝑦
1312cv 1474 . . . . . . . 8 class 𝑦
1413, 7wcel 1977 . . . . . . 7 wff 𝑦 ∈ (𝔼‘𝑛)
158, 11, 14w3a 1031 . . . . . 6 wff (𝑥 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛))
16 vi . . . . . . . . . . 11 setvar 𝑖
1716cv 1474 . . . . . . . . . 10 class 𝑖
1817, 13cfv 5804 . . . . . . . . 9 class (𝑦𝑖)
19 c1 9816 . . . . . . . . . . . 12 class 1
20 vt . . . . . . . . . . . . 13 setvar 𝑡
2120cv 1474 . . . . . . . . . . . 12 class 𝑡
22 cmin 10145 . . . . . . . . . . . 12 class
2319, 21, 22co 6549 . . . . . . . . . . 11 class (1 − 𝑡)
2417, 3cfv 5804 . . . . . . . . . . 11 class (𝑥𝑖)
25 cmul 9820 . . . . . . . . . . 11 class ·
2623, 24, 25co 6549 . . . . . . . . . 10 class ((1 − 𝑡) · (𝑥𝑖))
2717, 10cfv 5804 . . . . . . . . . . 11 class (𝑧𝑖)
2821, 27, 25co 6549 . . . . . . . . . 10 class (𝑡 · (𝑧𝑖))
29 caddc 9818 . . . . . . . . . 10 class +
3026, 28, 29co 6549 . . . . . . . . 9 class (((1 − 𝑡) · (𝑥𝑖)) + (𝑡 · (𝑧𝑖)))
3118, 30wceq 1475 . . . . . . . 8 wff (𝑦𝑖) = (((1 − 𝑡) · (𝑥𝑖)) + (𝑡 · (𝑧𝑖)))
32 cfz 12197 . . . . . . . . 9 class ...
3319, 5, 32co 6549 . . . . . . . 8 class (1...𝑛)
3431, 16, 33wral 2896 . . . . . . 7 wff 𝑖 ∈ (1...𝑛)(𝑦𝑖) = (((1 − 𝑡) · (𝑥𝑖)) + (𝑡 · (𝑧𝑖)))
35 cc0 9815 . . . . . . . 8 class 0
36 cicc 12049 . . . . . . . 8 class [,]
3735, 19, 36co 6549 . . . . . . 7 class (0[,]1)
3834, 20, 37wrex 2897 . . . . . 6 wff 𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑦𝑖) = (((1 − 𝑡) · (𝑥𝑖)) + (𝑡 · (𝑧𝑖)))
3915, 38wa 383 . . . . 5 wff ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑦𝑖) = (((1 − 𝑡) · (𝑥𝑖)) + (𝑡 · (𝑧𝑖))))
40 cn 10897 . . . . 5 class
4139, 4, 40wrex 2897 . . . 4 wff 𝑛 ∈ ℕ ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑦𝑖) = (((1 − 𝑡) · (𝑥𝑖)) + (𝑡 · (𝑧𝑖))))
4241, 2, 9, 12coprab 6550 . . 3 class {⟨⟨𝑥, 𝑧⟩, 𝑦⟩ ∣ ∃𝑛 ∈ ℕ ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑦𝑖) = (((1 − 𝑡) · (𝑥𝑖)) + (𝑡 · (𝑧𝑖))))}
4342ccnv 5037 . 2 class {⟨⟨𝑥, 𝑧⟩, 𝑦⟩ ∣ ∃𝑛 ∈ ℕ ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑦𝑖) = (((1 − 𝑡) · (𝑥𝑖)) + (𝑡 · (𝑧𝑖))))}
441, 43wceq 1475 1 wff Btwn = {⟨⟨𝑥, 𝑧⟩, 𝑦⟩ ∣ ∃𝑛 ∈ ℕ ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑦𝑖) = (((1 − 𝑡) · (𝑥𝑖)) + (𝑡 · (𝑧𝑖))))}
Colors of variables: wff setvar class
This definition is referenced by:  brbtwn  25579
  Copyright terms: Public domain W3C validator