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 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ABtwnBC↔∃t∈01∀i∈1…NA⁡i=1−t⁢B⁡i+t⁢C⁡i

Proof

Step Hyp Ref Expression
1 df-btwn ⊢Btwn=yzx|∃n∈ℕy∈𝔼⁡n∧z∈𝔼⁡n∧x∈𝔼⁡n∧∃t∈01∀i∈1…nx⁡i=1−t⁢y⁡i+t⁢z⁡i-1
2 1 breqi ⊢ABtwnBC↔Ayzx|∃n∈ℕy∈𝔼⁡n∧z∈𝔼⁡n∧x∈𝔼⁡n∧∃t∈01∀i∈1…nx⁡i=1−t⁢y⁡i+t⁢z⁡i-1BC
3 opex ⊢BC∈V
4 brcnvg ⊢A∈𝔼⁡N∧BC∈V→Ayzx|∃n∈ℕy∈𝔼⁡n∧z∈𝔼⁡n∧x∈𝔼⁡n∧∃t∈01∀i∈1…nx⁡i=1−t⁢y⁡i+t⁢z⁡i-1BC↔BCyzx|∃n∈ℕy∈𝔼⁡n∧z∈𝔼⁡n∧x∈𝔼⁡n∧∃t∈01∀i∈1…nx⁡i=1−t⁢y⁡i+t⁢z⁡iA
5 3 4 mpan2 ⊢A∈𝔼⁡N→Ayzx|∃n∈ℕy∈𝔼⁡n∧z∈𝔼⁡n∧x∈𝔼⁡n∧∃t∈01∀i∈1…nx⁡i=1−t⁢y⁡i+t⁢z⁡i-1BC↔BCyzx|∃n∈ℕy∈𝔼⁡n∧z∈𝔼⁡n∧x∈𝔼⁡n∧∃t∈01∀i∈1…nx⁡i=1−t⁢y⁡i+t⁢z⁡iA
6 5 3ad2ant1 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→Ayzx|∃n∈ℕy∈𝔼⁡n∧z∈𝔼⁡n∧x∈𝔼⁡n∧∃t∈01∀i∈1…nx⁡i=1−t⁢y⁡i+t⁢z⁡i-1BC↔BCyzx|∃n∈ℕy∈𝔼⁡n∧z∈𝔼⁡n∧x∈𝔼⁡n∧∃t∈01∀i∈1…nx⁡i=1−t⁢y⁡i+t⁢z⁡iA
7 df-br ⊢BCyzx|∃n∈ℕy∈𝔼⁡n∧z∈𝔼⁡n∧x∈𝔼⁡n∧∃t∈01∀i∈1…nx⁡i=1−t⁢y⁡i+t⁢z⁡iA↔BCA∈yzx|∃n∈ℕy∈𝔼⁡n∧z∈𝔼⁡n∧x∈𝔼⁡n∧∃t∈01∀i∈1…nx⁡i=1−t⁢y⁡i+t⁢z⁡i
8 eleq1 ⊢y=B→y∈𝔼⁡n↔B∈𝔼⁡n
9 8 3anbi1d ⊢y=B→y∈𝔼⁡n∧z∈𝔼⁡n∧x∈𝔼⁡n↔B∈𝔼⁡n∧z∈𝔼⁡n∧x∈𝔼⁡n
10 fveq1 ⊢y=B→y⁡i=B⁡i
11 10 oveq2d ⊢y=B→1−t⁢y⁡i=1−t⁢B⁡i
12 11 oveq1d ⊢y=B→1−t⁢y⁡i+t⁢z⁡i=1−t⁢B⁡i+t⁢z⁡i
13 12 eqeq2d ⊢y=B→x⁡i=1−t⁢y⁡i+t⁢z⁡i↔x⁡i=1−t⁢B⁡i+t⁢z⁡i
14 13 rexralbidv ⊢y=B→∃t∈01∀i∈1…nx⁡i=1−t⁢y⁡i+t⁢z⁡i↔∃t∈01∀i∈1…nx⁡i=1−t⁢B⁡i+t⁢z⁡i
15 9 14 anbi12d ⊢y=B→y∈𝔼⁡n∧z∈𝔼⁡n∧x∈𝔼⁡n∧∃t∈01∀i∈1…nx⁡i=1−t⁢y⁡i+t⁢z⁡i↔B∈𝔼⁡n∧z∈𝔼⁡n∧x∈𝔼⁡n∧∃t∈01∀i∈1…nx⁡i=1−t⁢B⁡i+t⁢z⁡i
16 15 rexbidv ⊢y=B→∃n∈ℕy∈𝔼⁡n∧z∈𝔼⁡n∧x∈𝔼⁡n∧∃t∈01∀i∈1…nx⁡i=1−t⁢y⁡i+t⁢z⁡i↔∃n∈ℕB∈𝔼⁡n∧z∈𝔼⁡n∧x∈𝔼⁡n∧∃t∈01∀i∈1…nx⁡i=1−t⁢B⁡i+t⁢z⁡i
17 eleq1 ⊢z=C→z∈𝔼⁡n↔C∈𝔼⁡n
18 17 3anbi2d ⊢z=C→B∈𝔼⁡n∧z∈𝔼⁡n∧x∈𝔼⁡n↔B∈𝔼⁡n∧C∈𝔼⁡n∧x∈𝔼⁡n
19 fveq1 ⊢z=C→z⁡i=C⁡i
20 19 oveq2d ⊢z=C→t⁢z⁡i=t⁢C⁡i
21 20 oveq2d ⊢z=C→1−t⁢B⁡i+t⁢z⁡i=1−t⁢B⁡i+t⁢C⁡i
22 21 eqeq2d ⊢z=C→x⁡i=1−t⁢B⁡i+t⁢z⁡i↔x⁡i=1−t⁢B⁡i+t⁢C⁡i
23 22 rexralbidv ⊢z=C→∃t∈01∀i∈1…nx⁡i=1−t⁢B⁡i+t⁢z⁡i↔∃t∈01∀i∈1…nx⁡i=1−t⁢B⁡i+t⁢C⁡i
24 18 23 anbi12d ⊢z=C→B∈𝔼⁡n∧z∈𝔼⁡n∧x∈𝔼⁡n∧∃t∈01∀i∈1…nx⁡i=1−t⁢B⁡i+t⁢z⁡i↔B∈𝔼⁡n∧C∈𝔼⁡n∧x∈𝔼⁡n∧∃t∈01∀i∈1…nx⁡i=1−t⁢B⁡i+t⁢C⁡i
25 24 rexbidv ⊢z=C→∃n∈ℕB∈𝔼⁡n∧z∈𝔼⁡n∧x∈𝔼⁡n∧∃t∈01∀i∈1…nx⁡i=1−t⁢B⁡i+t⁢z⁡i↔∃n∈ℕB∈𝔼⁡n∧C∈𝔼⁡n∧x∈𝔼⁡n∧∃t∈01∀i∈1…nx⁡i=1−t⁢B⁡i+t⁢C⁡i
26 eleq1 ⊢x=A→x∈𝔼⁡n↔A∈𝔼⁡n
27 26 3anbi3d ⊢x=A→B∈𝔼⁡n∧C∈𝔼⁡n∧x∈𝔼⁡n↔B∈𝔼⁡n∧C∈𝔼⁡n∧A∈𝔼⁡n
28 fveq1 ⊢x=A→x⁡i=A⁡i
29 28 eqeq1d ⊢x=A→x⁡i=1−t⁢B⁡i+t⁢C⁡i↔A⁡i=1−t⁢B⁡i+t⁢C⁡i
30 29 rexralbidv ⊢x=A→∃t∈01∀i∈1…nx⁡i=1−t⁢B⁡i+t⁢C⁡i↔∃t∈01∀i∈1…nA⁡i=1−t⁢B⁡i+t⁢C⁡i
31 27 30 anbi12d ⊢x=A→B∈𝔼⁡n∧C∈𝔼⁡n∧x∈𝔼⁡n∧∃t∈01∀i∈1…nx⁡i=1−t⁢B⁡i+t⁢C⁡i↔B∈𝔼⁡n∧C∈𝔼⁡n∧A∈𝔼⁡n∧∃t∈01∀i∈1…nA⁡i=1−t⁢B⁡i+t⁢C⁡i
32 31 rexbidv ⊢x=A→∃n∈ℕB∈𝔼⁡n∧C∈𝔼⁡n∧x∈𝔼⁡n∧∃t∈01∀i∈1…nx⁡i=1−t⁢B⁡i+t⁢C⁡i↔∃n∈ℕB∈𝔼⁡n∧C∈𝔼⁡n∧A∈𝔼⁡n∧∃t∈01∀i∈1…nA⁡i=1−t⁢B⁡i+t⁢C⁡i
33 16 25 32 eloprabg ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N→BCA∈yzx|∃n∈ℕy∈𝔼⁡n∧z∈𝔼⁡n∧x∈𝔼⁡n∧∃t∈01∀i∈1…nx⁡i=1−t⁢y⁡i+t⁢z⁡i↔∃n∈ℕB∈𝔼⁡n∧C∈𝔼⁡n∧A∈𝔼⁡n∧∃t∈01∀i∈1…nA⁡i=1−t⁢B⁡i+t⁢C⁡i
34 simp1 ⊢B∈𝔼⁡n∧C∈𝔼⁡n∧A∈𝔼⁡n→B∈𝔼⁡n
35 simp1 ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N→B∈𝔼⁡N
36 eedimeq ⊢B∈𝔼⁡n∧B∈𝔼⁡N→n=N
37 34 35 36 syl2anr ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N∧B∈𝔼⁡n∧C∈𝔼⁡n∧A∈𝔼⁡n→n=N
38 oveq2 ⊢n=N→1…n=1…N
39 38 raleqdv ⊢n=N→∀i∈1…nA⁡i=1−t⁢B⁡i+t⁢C⁡i↔∀i∈1…NA⁡i=1−t⁢B⁡i+t⁢C⁡i
40 39 rexbidv ⊢n=N→∃t∈01∀i∈1…nA⁡i=1−t⁢B⁡i+t⁢C⁡i↔∃t∈01∀i∈1…NA⁡i=1−t⁢B⁡i+t⁢C⁡i
41 37 40 syl ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N∧B∈𝔼⁡n∧C∈𝔼⁡n∧A∈𝔼⁡n→∃t∈01∀i∈1…nA⁡i=1−t⁢B⁡i+t⁢C⁡i↔∃t∈01∀i∈1…NA⁡i=1−t⁢B⁡i+t⁢C⁡i
42 41 biimpd ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N∧B∈𝔼⁡n∧C∈𝔼⁡n∧A∈𝔼⁡n→∃t∈01∀i∈1…nA⁡i=1−t⁢B⁡i+t⁢C⁡i→∃t∈01∀i∈1…NA⁡i=1−t⁢B⁡i+t⁢C⁡i
43 42 expimpd ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N→B∈𝔼⁡n∧C∈𝔼⁡n∧A∈𝔼⁡n∧∃t∈01∀i∈1…nA⁡i=1−t⁢B⁡i+t⁢C⁡i→∃t∈01∀i∈1…NA⁡i=1−t⁢B⁡i+t⁢C⁡i
44 43 rexlimdvw ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N→∃n∈ℕB∈𝔼⁡n∧C∈𝔼⁡n∧A∈𝔼⁡n∧∃t∈01∀i∈1…nA⁡i=1−t⁢B⁡i+t⁢C⁡i→∃t∈01∀i∈1…NA⁡i=1−t⁢B⁡i+t⁢C⁡i
45 eleenn ⊢B∈𝔼⁡N→N∈ℕ
46 45 3ad2ant1 ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N→N∈ℕ
47 fveq2 ⊢n=N→𝔼⁡n=𝔼⁡N
48 47 eleq2d ⊢n=N→B∈𝔼⁡n↔B∈𝔼⁡N
49 47 eleq2d ⊢n=N→C∈𝔼⁡n↔C∈𝔼⁡N
50 47 eleq2d ⊢n=N→A∈𝔼⁡n↔A∈𝔼⁡N
51 48 49 50 3anbi123d ⊢n=N→B∈𝔼⁡n∧C∈𝔼⁡n∧A∈𝔼⁡n↔B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N
52 51 40 anbi12d ⊢n=N→B∈𝔼⁡n∧C∈𝔼⁡n∧A∈𝔼⁡n∧∃t∈01∀i∈1…nA⁡i=1−t⁢B⁡i+t⁢C⁡i↔B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N∧∃t∈01∀i∈1…NA⁡i=1−t⁢B⁡i+t⁢C⁡i
53 52 rspcev ⊢N∈ℕ∧B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N∧∃t∈01∀i∈1…NA⁡i=1−t⁢B⁡i+t⁢C⁡i→∃n∈ℕB∈𝔼⁡n∧C∈𝔼⁡n∧A∈𝔼⁡n∧∃t∈01∀i∈1…nA⁡i=1−t⁢B⁡i+t⁢C⁡i
54 53 exp32 ⊢N∈ℕ→B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N→∃t∈01∀i∈1…NA⁡i=1−t⁢B⁡i+t⁢C⁡i→∃n∈ℕB∈𝔼⁡n∧C∈𝔼⁡n∧A∈𝔼⁡n∧∃t∈01∀i∈1…nA⁡i=1−t⁢B⁡i+t⁢C⁡i
55 46 54 mpcom ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N→∃t∈01∀i∈1…NA⁡i=1−t⁢B⁡i+t⁢C⁡i→∃n∈ℕB∈𝔼⁡n∧C∈𝔼⁡n∧A∈𝔼⁡n∧∃t∈01∀i∈1…nA⁡i=1−t⁢B⁡i+t⁢C⁡i
56 44 55 impbid ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N→∃n∈ℕB∈𝔼⁡n∧C∈𝔼⁡n∧A∈𝔼⁡n∧∃t∈01∀i∈1…nA⁡i=1−t⁢B⁡i+t⁢C⁡i↔∃t∈01∀i∈1…NA⁡i=1−t⁢B⁡i+t⁢C⁡i
57 33 56 bitrd ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N→BCA∈yzx|∃n∈ℕy∈𝔼⁡n∧z∈𝔼⁡n∧x∈𝔼⁡n∧∃t∈01∀i∈1…nx⁡i=1−t⁢y⁡i+t⁢z⁡i↔∃t∈01∀i∈1…NA⁡i=1−t⁢B⁡i+t⁢C⁡i
58 57 3comr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→BCA∈yzx|∃n∈ℕy∈𝔼⁡n∧z∈𝔼⁡n∧x∈𝔼⁡n∧∃t∈01∀i∈1…nx⁡i=1−t⁢y⁡i+t⁢z⁡i↔∃t∈01∀i∈1…NA⁡i=1−t⁢B⁡i+t⁢C⁡i
59 7 58 bitrid ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→BCyzx|∃n∈ℕy∈𝔼⁡n∧z∈𝔼⁡n∧x∈𝔼⁡n∧∃t∈01∀i∈1…nx⁡i=1−t⁢y⁡i+t⁢z⁡iA↔∃t∈01∀i∈1…NA⁡i=1−t⁢B⁡i+t⁢C⁡i
60 6 59 bitrd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→Ayzx|∃n∈ℕy∈𝔼⁡n∧z∈𝔼⁡n∧x∈𝔼⁡n∧∃t∈01∀i∈1…nx⁡i=1−t⁢y⁡i+t⁢z⁡i-1BC↔∃t∈01∀i∈1…NA⁡i=1−t⁢B⁡i+t⁢C⁡i
61 2 60 bitrid ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ABtwnBC↔∃t∈01∀i∈1…NA⁡i=1−t⁢B⁡i+t⁢C⁡i