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