# 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 ${⊢}\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\to \left({A}\mathrm{Btwn}⟨{B},{C}⟩↔\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)$

### Proof

Step Hyp Ref Expression
1 df-btwn ${⊢}\mathrm{Btwn}={\left\{⟨⟨{y},{z}⟩,{x}⟩|\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({y}\in 𝔼\left({n}\right)\wedge {z}\in 𝔼\left({n}\right)\wedge {x}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){y}\left({i}\right)+{t}{z}\left({i}\right)\right)\right\}}^{-1}$
2 1 breqi ${⊢}{A}\mathrm{Btwn}⟨{B},{C}⟩↔{A}{\left\{⟨⟨{y},{z}⟩,{x}⟩|\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({y}\in 𝔼\left({n}\right)\wedge {z}\in 𝔼\left({n}\right)\wedge {x}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){y}\left({i}\right)+{t}{z}\left({i}\right)\right)\right\}}^{-1}⟨{B},{C}⟩$
3 opex ${⊢}⟨{B},{C}⟩\in \mathrm{V}$
4 brcnvg ${⊢}\left({A}\in 𝔼\left({N}\right)\wedge ⟨{B},{C}⟩\in \mathrm{V}\right)\to \left({A}{\left\{⟨⟨{y},{z}⟩,{x}⟩|\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({y}\in 𝔼\left({n}\right)\wedge {z}\in 𝔼\left({n}\right)\wedge {x}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){y}\left({i}\right)+{t}{z}\left({i}\right)\right)\right\}}^{-1}⟨{B},{C}⟩↔⟨{B},{C}⟩\left\{⟨⟨{y},{z}⟩,{x}⟩|\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({y}\in 𝔼\left({n}\right)\wedge {z}\in 𝔼\left({n}\right)\wedge {x}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){y}\left({i}\right)+{t}{z}\left({i}\right)\right)\right\}{A}\right)$
5 3 4 mpan2 ${⊢}{A}\in 𝔼\left({N}\right)\to \left({A}{\left\{⟨⟨{y},{z}⟩,{x}⟩|\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({y}\in 𝔼\left({n}\right)\wedge {z}\in 𝔼\left({n}\right)\wedge {x}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){y}\left({i}\right)+{t}{z}\left({i}\right)\right)\right\}}^{-1}⟨{B},{C}⟩↔⟨{B},{C}⟩\left\{⟨⟨{y},{z}⟩,{x}⟩|\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({y}\in 𝔼\left({n}\right)\wedge {z}\in 𝔼\left({n}\right)\wedge {x}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){y}\left({i}\right)+{t}{z}\left({i}\right)\right)\right\}{A}\right)$
6 5 3ad2ant1 ${⊢}\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\to \left({A}{\left\{⟨⟨{y},{z}⟩,{x}⟩|\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({y}\in 𝔼\left({n}\right)\wedge {z}\in 𝔼\left({n}\right)\wedge {x}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){y}\left({i}\right)+{t}{z}\left({i}\right)\right)\right\}}^{-1}⟨{B},{C}⟩↔⟨{B},{C}⟩\left\{⟨⟨{y},{z}⟩,{x}⟩|\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({y}\in 𝔼\left({n}\right)\wedge {z}\in 𝔼\left({n}\right)\wedge {x}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){y}\left({i}\right)+{t}{z}\left({i}\right)\right)\right\}{A}\right)$
7 df-br ${⊢}⟨{B},{C}⟩\left\{⟨⟨{y},{z}⟩,{x}⟩|\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({y}\in 𝔼\left({n}\right)\wedge {z}\in 𝔼\left({n}\right)\wedge {x}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){y}\left({i}\right)+{t}{z}\left({i}\right)\right)\right\}{A}↔⟨⟨{B},{C}⟩,{A}⟩\in \left\{⟨⟨{y},{z}⟩,{x}⟩|\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({y}\in 𝔼\left({n}\right)\wedge {z}\in 𝔼\left({n}\right)\wedge {x}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){y}\left({i}\right)+{t}{z}\left({i}\right)\right)\right\}$
8 eleq1 ${⊢}{y}={B}\to \left({y}\in 𝔼\left({n}\right)↔{B}\in 𝔼\left({n}\right)\right)$
9 8 3anbi1d ${⊢}{y}={B}\to \left(\left({y}\in 𝔼\left({n}\right)\wedge {z}\in 𝔼\left({n}\right)\wedge {x}\in 𝔼\left({n}\right)\right)↔\left({B}\in 𝔼\left({n}\right)\wedge {z}\in 𝔼\left({n}\right)\wedge {x}\in 𝔼\left({n}\right)\right)\right)$
10 fveq1 ${⊢}{y}={B}\to {y}\left({i}\right)={B}\left({i}\right)$
11 10 oveq2d ${⊢}{y}={B}\to \left(1-{t}\right){y}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)$
12 11 oveq1d ${⊢}{y}={B}\to \left(1-{t}\right){y}\left({i}\right)+{t}{z}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{z}\left({i}\right)$
13 12 eqeq2d ${⊢}{y}={B}\to \left({x}\left({i}\right)=\left(1-{t}\right){y}\left({i}\right)+{t}{z}\left({i}\right)↔{x}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{z}\left({i}\right)\right)$
14 13 rexralbidv ${⊢}{y}={B}\to \left(\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){y}\left({i}\right)+{t}{z}\left({i}\right)↔\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{z}\left({i}\right)\right)$
15 9 14 anbi12d ${⊢}{y}={B}\to \left(\left(\left({y}\in 𝔼\left({n}\right)\wedge {z}\in 𝔼\left({n}\right)\wedge {x}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){y}\left({i}\right)+{t}{z}\left({i}\right)\right)↔\left(\left({B}\in 𝔼\left({n}\right)\wedge {z}\in 𝔼\left({n}\right)\wedge {x}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{z}\left({i}\right)\right)\right)$
16 15 rexbidv ${⊢}{y}={B}\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({y}\in 𝔼\left({n}\right)\wedge {z}\in 𝔼\left({n}\right)\wedge {x}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){y}\left({i}\right)+{t}{z}\left({i}\right)\right)↔\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({B}\in 𝔼\left({n}\right)\wedge {z}\in 𝔼\left({n}\right)\wedge {x}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{z}\left({i}\right)\right)\right)$
17 eleq1 ${⊢}{z}={C}\to \left({z}\in 𝔼\left({n}\right)↔{C}\in 𝔼\left({n}\right)\right)$
18 17 3anbi2d ${⊢}{z}={C}\to \left(\left({B}\in 𝔼\left({n}\right)\wedge {z}\in 𝔼\left({n}\right)\wedge {x}\in 𝔼\left({n}\right)\right)↔\left({B}\in 𝔼\left({n}\right)\wedge {C}\in 𝔼\left({n}\right)\wedge {x}\in 𝔼\left({n}\right)\right)\right)$
19 fveq1 ${⊢}{z}={C}\to {z}\left({i}\right)={C}\left({i}\right)$
20 19 oveq2d ${⊢}{z}={C}\to {t}{z}\left({i}\right)={t}{C}\left({i}\right)$
21 20 oveq2d ${⊢}{z}={C}\to \left(1-{t}\right){B}\left({i}\right)+{t}{z}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)$
22 21 eqeq2d ${⊢}{z}={C}\to \left({x}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{z}\left({i}\right)↔{x}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)$
23 22 rexralbidv ${⊢}{z}={C}\to \left(\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{z}\left({i}\right)↔\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)$
24 18 23 anbi12d ${⊢}{z}={C}\to \left(\left(\left({B}\in 𝔼\left({n}\right)\wedge {z}\in 𝔼\left({n}\right)\wedge {x}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{z}\left({i}\right)\right)↔\left(\left({B}\in 𝔼\left({n}\right)\wedge {C}\in 𝔼\left({n}\right)\wedge {x}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)\right)$
25 24 rexbidv ${⊢}{z}={C}\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({B}\in 𝔼\left({n}\right)\wedge {z}\in 𝔼\left({n}\right)\wedge {x}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{z}\left({i}\right)\right)↔\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({B}\in 𝔼\left({n}\right)\wedge {C}\in 𝔼\left({n}\right)\wedge {x}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)\right)$
26 eleq1 ${⊢}{x}={A}\to \left({x}\in 𝔼\left({n}\right)↔{A}\in 𝔼\left({n}\right)\right)$
27 26 3anbi3d ${⊢}{x}={A}\to \left(\left({B}\in 𝔼\left({n}\right)\wedge {C}\in 𝔼\left({n}\right)\wedge {x}\in 𝔼\left({n}\right)\right)↔\left({B}\in 𝔼\left({n}\right)\wedge {C}\in 𝔼\left({n}\right)\wedge {A}\in 𝔼\left({n}\right)\right)\right)$
28 fveq1 ${⊢}{x}={A}\to {x}\left({i}\right)={A}\left({i}\right)$
29 28 eqeq1d ${⊢}{x}={A}\to \left({x}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)↔{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)$
30 29 rexralbidv ${⊢}{x}={A}\to \left(\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)↔\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)$
31 27 30 anbi12d ${⊢}{x}={A}\to \left(\left(\left({B}\in 𝔼\left({n}\right)\wedge {C}\in 𝔼\left({n}\right)\wedge {x}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)↔\left(\left({B}\in 𝔼\left({n}\right)\wedge {C}\in 𝔼\left({n}\right)\wedge {A}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)\right)$
32 31 rexbidv ${⊢}{x}={A}\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({B}\in 𝔼\left({n}\right)\wedge {C}\in 𝔼\left({n}\right)\wedge {x}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)↔\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({B}\in 𝔼\left({n}\right)\wedge {C}\in 𝔼\left({n}\right)\wedge {A}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)\right)$
33 16 25 32 eloprabg ${⊢}\left({B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\right)\to \left(⟨⟨{B},{C}⟩,{A}⟩\in \left\{⟨⟨{y},{z}⟩,{x}⟩|\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({y}\in 𝔼\left({n}\right)\wedge {z}\in 𝔼\left({n}\right)\wedge {x}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){y}\left({i}\right)+{t}{z}\left({i}\right)\right)\right\}↔\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({B}\in 𝔼\left({n}\right)\wedge {C}\in 𝔼\left({n}\right)\wedge {A}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)\right)$
34 simp1 ${⊢}\left({B}\in 𝔼\left({n}\right)\wedge {C}\in 𝔼\left({n}\right)\wedge {A}\in 𝔼\left({n}\right)\right)\to {B}\in 𝔼\left({n}\right)$
35 simp1 ${⊢}\left({B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\right)\to {B}\in 𝔼\left({N}\right)$
36 eedimeq ${⊢}\left({B}\in 𝔼\left({n}\right)\wedge {B}\in 𝔼\left({N}\right)\right)\to {n}={N}$
37 34 35 36 syl2anr ${⊢}\left(\left({B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\right)\wedge \left({B}\in 𝔼\left({n}\right)\wedge {C}\in 𝔼\left({n}\right)\wedge {A}\in 𝔼\left({n}\right)\right)\right)\to {n}={N}$
38 oveq2 ${⊢}{n}={N}\to \left(1\dots {n}\right)=\left(1\dots {N}\right)$
39 38 raleqdv ${⊢}{n}={N}\to \left(\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)↔\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)$
40 39 rexbidv ${⊢}{n}={N}\to \left(\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)↔\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)$
41 37 40 syl ${⊢}\left(\left({B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\right)\wedge \left({B}\in 𝔼\left({n}\right)\wedge {C}\in 𝔼\left({n}\right)\wedge {A}\in 𝔼\left({n}\right)\right)\right)\to \left(\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)↔\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)$
42 41 biimpd ${⊢}\left(\left({B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\right)\wedge \left({B}\in 𝔼\left({n}\right)\wedge {C}\in 𝔼\left({n}\right)\wedge {A}\in 𝔼\left({n}\right)\right)\right)\to \left(\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\to \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)$
43 42 expimpd ${⊢}\left({B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\right)\to \left(\left(\left({B}\in 𝔼\left({n}\right)\wedge {C}\in 𝔼\left({n}\right)\wedge {A}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)\to \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)$
44 43 rexlimdvw ${⊢}\left({B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\right)\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({B}\in 𝔼\left({n}\right)\wedge {C}\in 𝔼\left({n}\right)\wedge {A}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)\to \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)$
45 eleenn ${⊢}{B}\in 𝔼\left({N}\right)\to {N}\in ℕ$
46 45 3ad2ant1 ${⊢}\left({B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\right)\to {N}\in ℕ$
47 fveq2 ${⊢}{n}={N}\to 𝔼\left({n}\right)=𝔼\left({N}\right)$
48 47 eleq2d ${⊢}{n}={N}\to \left({B}\in 𝔼\left({n}\right)↔{B}\in 𝔼\left({N}\right)\right)$
49 47 eleq2d ${⊢}{n}={N}\to \left({C}\in 𝔼\left({n}\right)↔{C}\in 𝔼\left({N}\right)\right)$
50 47 eleq2d ${⊢}{n}={N}\to \left({A}\in 𝔼\left({n}\right)↔{A}\in 𝔼\left({N}\right)\right)$
51 48 49 50 3anbi123d ${⊢}{n}={N}\to \left(\left({B}\in 𝔼\left({n}\right)\wedge {C}\in 𝔼\left({n}\right)\wedge {A}\in 𝔼\left({n}\right)\right)↔\left({B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\right)\right)$
52 51 40 anbi12d ${⊢}{n}={N}\to \left(\left(\left({B}\in 𝔼\left({n}\right)\wedge {C}\in 𝔼\left({n}\right)\wedge {A}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)↔\left(\left({B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)\right)$
53 52 rspcev ${⊢}\left({N}\in ℕ\wedge \left(\left({B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({B}\in 𝔼\left({n}\right)\wedge {C}\in 𝔼\left({n}\right)\wedge {A}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)$
54 53 exp32 ${⊢}{N}\in ℕ\to \left(\left({B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\right)\to \left(\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({B}\in 𝔼\left({n}\right)\wedge {C}\in 𝔼\left({n}\right)\wedge {A}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)\right)\right)$
55 46 54 mpcom ${⊢}\left({B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\right)\to \left(\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({B}\in 𝔼\left({n}\right)\wedge {C}\in 𝔼\left({n}\right)\wedge {A}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)\right)$
56 44 55 impbid ${⊢}\left({B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\right)\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({B}\in 𝔼\left({n}\right)\wedge {C}\in 𝔼\left({n}\right)\wedge {A}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)↔\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)$
57 33 56 bitrd ${⊢}\left({B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\wedge {A}\in 𝔼\left({N}\right)\right)\to \left(⟨⟨{B},{C}⟩,{A}⟩\in \left\{⟨⟨{y},{z}⟩,{x}⟩|\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({y}\in 𝔼\left({n}\right)\wedge {z}\in 𝔼\left({n}\right)\wedge {x}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){y}\left({i}\right)+{t}{z}\left({i}\right)\right)\right\}↔\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)$
58 57 3comr ${⊢}\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\to \left(⟨⟨{B},{C}⟩,{A}⟩\in \left\{⟨⟨{y},{z}⟩,{x}⟩|\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({y}\in 𝔼\left({n}\right)\wedge {z}\in 𝔼\left({n}\right)\wedge {x}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){y}\left({i}\right)+{t}{z}\left({i}\right)\right)\right\}↔\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)$
59 7 58 syl5bb ${⊢}\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\to \left(⟨{B},{C}⟩\left\{⟨⟨{y},{z}⟩,{x}⟩|\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({y}\in 𝔼\left({n}\right)\wedge {z}\in 𝔼\left({n}\right)\wedge {x}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){y}\left({i}\right)+{t}{z}\left({i}\right)\right)\right\}{A}↔\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)$
60 6 59 bitrd ${⊢}\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\to \left({A}{\left\{⟨⟨{y},{z}⟩,{x}⟩|\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\left(\left({y}\in 𝔼\left({n}\right)\wedge {z}\in 𝔼\left({n}\right)\wedge {x}\in 𝔼\left({n}\right)\right)\wedge \exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {n}\right)\phantom{\rule{.4em}{0ex}}{x}\left({i}\right)=\left(1-{t}\right){y}\left({i}\right)+{t}{z}\left({i}\right)\right)\right\}}^{-1}⟨{B},{C}⟩↔\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)$
61 2 60 syl5bb ${⊢}\left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\to \left({A}\mathrm{Btwn}⟨{B},{C}⟩↔\exists {t}\in \left[0,1\right]\phantom{\rule{.4em}{0ex}}\forall {i}\in \left(1\dots {N}\right)\phantom{\rule{.4em}{0ex}}{A}\left({i}\right)=\left(1-{t}\right){B}\left({i}\right)+{t}{C}\left({i}\right)\right)$