Metamath Proof Explorer

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 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) )