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 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) ) } |