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 = { ⟨ ⟨ 𝑥 , 𝑧 ⟩ , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑦𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥𝑖 ) ) + ( 𝑡 · ( 𝑧𝑖 ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cbtwn Btwn
1 vx 𝑥
2 vz 𝑧
3 vy 𝑦
4 vn 𝑛
5 cn
6 1 cv 𝑥
7 cee 𝔼
8 4 cv 𝑛
9 8 7 cfv ( 𝔼 ‘ 𝑛 )
10 6 9 wcel 𝑥 ∈ ( 𝔼 ‘ 𝑛 )
11 2 cv 𝑧
12 11 9 wcel 𝑧 ∈ ( 𝔼 ‘ 𝑛 )
13 3 cv 𝑦
14 13 9 wcel 𝑦 ∈ ( 𝔼 ‘ 𝑛 )
15 10 12 14 w3a ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) )
16 vt 𝑡
17 cc0 0
18 cicc [,]
19 c1 1
20 17 19 18 co ( 0 [,] 1 )
21 vi 𝑖
22 cfz ...
23 19 8 22 co ( 1 ... 𝑛 )
24 21 cv 𝑖
25 24 13 cfv ( 𝑦𝑖 )
26 cmin
27 16 cv 𝑡
28 19 27 26 co ( 1 − 𝑡 )
29 cmul ·
30 24 6 cfv ( 𝑥𝑖 )
31 28 30 29 co ( ( 1 − 𝑡 ) · ( 𝑥𝑖 ) )
32 caddc +
33 24 11 cfv ( 𝑧𝑖 )
34 27 33 29 co ( 𝑡 · ( 𝑧𝑖 ) )
35 31 34 32 co ( ( ( 1 − 𝑡 ) · ( 𝑥𝑖 ) ) + ( 𝑡 · ( 𝑧𝑖 ) ) )
36 25 35 wceq ( 𝑦𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥𝑖 ) ) + ( 𝑡 · ( 𝑧𝑖 ) ) )
37 36 21 23 wral 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑦𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥𝑖 ) ) + ( 𝑡 · ( 𝑧𝑖 ) ) )
38 37 16 20 wrex 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑦𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥𝑖 ) ) + ( 𝑡 · ( 𝑧𝑖 ) ) )
39 15 38 wa ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑦𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥𝑖 ) ) + ( 𝑡 · ( 𝑧𝑖 ) ) ) )
40 39 4 5 wrex 𝑛 ∈ ℕ ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑦𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥𝑖 ) ) + ( 𝑡 · ( 𝑧𝑖 ) ) ) )
41 40 1 2 3 coprab { ⟨ ⟨ 𝑥 , 𝑧 ⟩ , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑦𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥𝑖 ) ) + ( 𝑡 · ( 𝑧𝑖 ) ) ) ) }
42 41 ccnv { ⟨ ⟨ 𝑥 , 𝑧 ⟩ , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑦𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥𝑖 ) ) + ( 𝑡 · ( 𝑧𝑖 ) ) ) ) }
43 0 42 wceq Btwn = { ⟨ ⟨ 𝑥 , 𝑧 ⟩ , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑦𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥𝑖 ) ) + ( 𝑡 · ( 𝑧𝑖 ) ) ) ) }