Theorem brbtwn

Description: The binary relation form of the betweenness predicate. The statement A Btwn <. B , C >. should be informally read as " A lies on a line segment between B and C . This exact definition is abstracted away by Tarski's geometry axioms later on. (Contributed by Scott Fenton, 3-Jun-2013)

	Ref	Expression
Assertion	brbtwn	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-btwn	⊢ Btwn = ◡ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑥 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑦 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) ) }
2	1	breqi	⊢ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ↔ 𝐴 ◡ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑥 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑦 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) ) } ⟨ 𝐵 , 𝐶 ⟩ )
3		opex	⊢ ⟨ 𝐵 , 𝐶 ⟩ ∈ V
4		brcnvg	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ⟨ 𝐵 , 𝐶 ⟩ ∈ V ) → ( 𝐴 ◡ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑥 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑦 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) ) } ⟨ 𝐵 , 𝐶 ⟩ ↔ ⟨ 𝐵 , 𝐶 ⟩ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑥 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑦 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) ) } 𝐴 ) )
5	3 4	mpan2	⊢ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) → ( 𝐴 ◡ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑥 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑦 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) ) } ⟨ 𝐵 , 𝐶 ⟩ ↔ ⟨ 𝐵 , 𝐶 ⟩ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑥 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑦 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) ) } 𝐴 ) )
6	5	3ad2ant1	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 ◡ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑥 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑦 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) ) } ⟨ 𝐵 , 𝐶 ⟩ ↔ ⟨ 𝐵 , 𝐶 ⟩ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑥 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑦 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) ) } 𝐴 ) )
7		df-br	⊢ ( ⟨ 𝐵 , 𝐶 ⟩ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑥 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑦 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) ) } 𝐴 ↔ ⟨ ⟨ 𝐵 , 𝐶 ⟩ , 𝐴 ⟩ ∈ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑥 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑦 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) ) } )
8		eleq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ) )
9	8	3anbi1d	⊢ ( 𝑦 = 𝐵 → ( ( 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ) ↔ ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ) ) )
10		fveq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 ‘ 𝑖 ) = ( 𝐵 ‘ 𝑖 ) )
11	10	oveq2d	⊢ ( 𝑦 = 𝐵 → ( ( 1 − 𝑡 ) · ( 𝑦 ‘ 𝑖 ) ) = ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) )
12	11	oveq1d	⊢ ( 𝑦 = 𝐵 → ( ( ( 1 − 𝑡 ) · ( 𝑦 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) )
13	12	eqeq2d	⊢ ( 𝑦 = 𝐵 → ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑦 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) ↔ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) ) )
14	13	rexralbidv	⊢ ( 𝑦 = 𝐵 → ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑦 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) ) )
15	9 14	anbi12d	⊢ ( 𝑦 = 𝐵 → ( ( ( 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑦 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) ) ↔ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) ) ) )
16	15	rexbidv	⊢ ( 𝑦 = 𝐵 → ( ∃ 𝑛 ∈ ℕ ( ( 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑦 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑛 ∈ ℕ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) ) ) )
17		eleq1	⊢ ( 𝑧 = 𝐶 → ( 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ) )
18	17	3anbi2d	⊢ ( 𝑧 = 𝐶 → ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ) ↔ ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ) ) )
19		fveq1	⊢ ( 𝑧 = 𝐶 → ( 𝑧 ‘ 𝑖 ) = ( 𝐶 ‘ 𝑖 ) )
20	19	oveq2d	⊢ ( 𝑧 = 𝐶 → ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) = ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) )
21	20	oveq2d	⊢ ( 𝑧 = 𝐶 → ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) )
22	21	eqeq2d	⊢ ( 𝑧 = 𝐶 → ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) ↔ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
23	22	rexralbidv	⊢ ( 𝑧 = 𝐶 → ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
24	18 23	anbi12d	⊢ ( 𝑧 = 𝐶 → ( ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) ) ↔ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) )
25	24	rexbidv	⊢ ( 𝑧 = 𝐶 → ( ∃ 𝑛 ∈ ℕ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑛 ∈ ℕ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) )
26		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ) )
27	26	3anbi3d	⊢ ( 𝑥 = 𝐴 → ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ) ↔ ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ) ) )
28		fveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ‘ 𝑖 ) = ( 𝐴 ‘ 𝑖 ) )
29	28	eqeq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ↔ ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
30	29	rexralbidv	⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
31	27 30	anbi12d	⊢ ( 𝑥 = 𝐴 → ( ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) ↔ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) )
32	31	rexbidv	⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑛 ∈ ℕ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑛 ∈ ℕ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) )
33	16 25 32	eloprabg	⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ⟨ ⟨ 𝐵 , 𝐶 ⟩ , 𝐴 ⟩ ∈ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑥 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑦 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) ) } ↔ ∃ 𝑛 ∈ ℕ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) )
34		simp1	⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) )
35		simp1	⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
36		eedimeq	⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑛 = 𝑁 )
37	34 35 36	syl2anr	⊢ ( ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ) ) → 𝑛 = 𝑁 )
38		oveq2	⊢ ( 𝑛 = 𝑁 → ( 1 ... 𝑛 ) = ( 1 ... 𝑁 ) )
39	38	raleqdv	⊢ ( 𝑛 = 𝑁 → ( ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
40	39	rexbidv	⊢ ( 𝑛 = 𝑁 → ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
41	37 40	syl	⊢ ( ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ) ) → ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
42	41	biimpd	⊢ ( ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ) ) → ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) → ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
43	42	expimpd	⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) → ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
44	43	rexlimdvw	⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ∃ 𝑛 ∈ ℕ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) → ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
45		eleenn	⊢ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) → 𝑁 ∈ ℕ )
46	45	3ad2ant1	⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ )
47		fveq2	⊢ ( 𝑛 = 𝑁 → ( 𝔼 ‘ 𝑛 ) = ( 𝔼 ‘ 𝑁 ) )
48	47	eleq2d	⊢ ( 𝑛 = 𝑁 → ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) )
49	47	eleq2d	⊢ ( 𝑛 = 𝑁 → ( 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) )
50	47	eleq2d	⊢ ( 𝑛 = 𝑁 → ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) )
51	48 49 50	3anbi123d	⊢ ( 𝑛 = 𝑁 → ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ) ↔ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ) )
52	51 40	anbi12d	⊢ ( 𝑛 = 𝑁 → ( ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) ↔ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) )
53	52	rspcev	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → ∃ 𝑛 ∈ ℕ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
54	53	exp32	⊢ ( 𝑁 ∈ ℕ → ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) → ∃ 𝑛 ∈ ℕ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) ) )
55	46 54	mpcom	⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) → ∃ 𝑛 ∈ ℕ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) )
56	44 55	impbid	⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ∃ 𝑛 ∈ ℕ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
57	33 56	bitrd	⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ⟨ ⟨ 𝐵 , 𝐶 ⟩ , 𝐴 ⟩ ∈ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑥 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑦 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) ) } ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
58	57	3comr	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ⟨ ⟨ 𝐵 , 𝐶 ⟩ , 𝐴 ⟩ ∈ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑥 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑦 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) ) } ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
59	7 58	bitrid	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ⟨ 𝐵 , 𝐶 ⟩ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑥 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑦 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) ) } 𝐴 ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
60	6 59	bitrd	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 ◡ { ⟨ ⟨ 𝑦 , 𝑧 ⟩ , 𝑥 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑛 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑦 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑧 ‘ 𝑖 ) ) ) ) } ⟨ 𝐵 , 𝐶 ⟩ ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
61	2 60	bitrid	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) )