brbtwn - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > brbtwn		Structured version Visualization version GIF version

Theorem brbtwn 26248

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

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

Distinct variable groups: 𝑖,𝑁,𝑡 𝐴,𝑖,𝑡 𝐵,𝑖,𝑡 𝐶,𝑖,𝑡

Proof of Theorem brbtwn Dummy variables 𝑥 𝑦 𝑧 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-btwn 26241	. . 3 ⊢ Btwn = ^◡{⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ ∃𝑛 ∈ ℕ ((𝑦 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑥 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑦‘𝑖)) + (𝑡 · (𝑧‘𝑖))))}
2	1	breqi 4892	. 2 ⊢ (𝐴 Btwn ⟨𝐵, 𝐶⟩ ↔ 𝐴^◡{⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ ∃𝑛 ∈ ℕ ((𝑦 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑥 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑦‘𝑖)) + (𝑡 · (𝑧‘𝑖))))}⟨𝐵, 𝐶⟩)
3		opex 5164	. . . . 5 ⊢ ⟨𝐵, 𝐶⟩ ∈ V
4		brcnvg 5547	. . . . 5 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ ⟨𝐵, 𝐶⟩ ∈ V) → (𝐴^◡{⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ ∃𝑛 ∈ ℕ ((𝑦 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑥 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑦‘𝑖)) + (𝑡 · (𝑧‘𝑖))))}⟨𝐵, 𝐶⟩ ↔ ⟨𝐵, 𝐶⟩{⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ ∃𝑛 ∈ ℕ ((𝑦 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑥 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑦‘𝑖)) + (𝑡 · (𝑧‘𝑖))))}𝐴))
5	3, 4	mpan2 681	. . . 4 ⊢ (𝐴 ∈ (𝔼‘𝑁) → (𝐴^◡{⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ ∃𝑛 ∈ ℕ ((𝑦 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑥 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑦‘𝑖)) + (𝑡 · (𝑧‘𝑖))))}⟨𝐵, 𝐶⟩ ↔ ⟨𝐵, 𝐶⟩{⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ ∃𝑛 ∈ ℕ ((𝑦 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑥 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑦‘𝑖)) + (𝑡 · (𝑧‘𝑖))))}𝐴))
6	5	3ad2ant1 1124	. . 3 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐴^◡{⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ ∃𝑛 ∈ ℕ ((𝑦 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑥 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑦‘𝑖)) + (𝑡 · (𝑧‘𝑖))))}⟨𝐵, 𝐶⟩ ↔ ⟨𝐵, 𝐶⟩{⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ ∃𝑛 ∈ ℕ ((𝑦 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑥 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑦‘𝑖)) + (𝑡 · (𝑧‘𝑖))))}𝐴))
7		df-br 4887	. . . 4 ⊢ (⟨𝐵, 𝐶⟩{⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ ∃𝑛 ∈ ℕ ((𝑦 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑥 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑦‘𝑖)) + (𝑡 · (𝑧‘𝑖))))}𝐴 ↔ ⟨⟨𝐵, 𝐶⟩, 𝐴⟩ ∈ {⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ ∃𝑛 ∈ ℕ ((𝑦 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑥 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑦‘𝑖)) + (𝑡 · (𝑧‘𝑖))))})
8		eleq1 2846	. . . . . . . . . 10 ⊢ (𝑦 = 𝐵 → (𝑦 ∈ (𝔼‘𝑛) ↔ 𝐵 ∈ (𝔼‘𝑛)))
9	8	3anbi1d 1513	. . . . . . . . 9 ⊢ (𝑦 = 𝐵 → ((𝑦 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑥 ∈ (𝔼‘𝑛)) ↔ (𝐵 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑥 ∈ (𝔼‘𝑛))))
10		fveq1 6445	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝐵 → (𝑦‘𝑖) = (𝐵‘𝑖))
11	10	oveq2d 6938	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐵 → ((1 − 𝑡) · (𝑦‘𝑖)) = ((1 − 𝑡) · (𝐵‘𝑖)))
12	11	oveq1d 6937	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐵 → (((1 − 𝑡) · (𝑦‘𝑖)) + (𝑡 · (𝑧‘𝑖))) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝑧‘𝑖))))
13	12	eqeq2d 2787	. . . . . . . . . 10 ⊢ (𝑦 = 𝐵 → ((𝑥‘𝑖) = (((1 − 𝑡) · (𝑦‘𝑖)) + (𝑡 · (𝑧‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝑧‘𝑖)))))
14	13	rexralbidv 3242	. . . . . . . . 9 ⊢ (𝑦 = 𝐵 → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑦‘𝑖)) + (𝑡 · (𝑧‘𝑖))) ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑥‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝑧‘𝑖)))))
15	9, 14	anbi12d 624	. . . . . . . 8 ⊢ (𝑦 = 𝐵 → (((𝑦 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑥 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑦‘𝑖)) + (𝑡 · (𝑧‘𝑖)))) ↔ ((𝐵 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑥 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑥‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝑧‘𝑖))))))
16	15	rexbidv 3236	. . . . . . 7 ⊢ (𝑦 = 𝐵 → (∃𝑛 ∈ ℕ ((𝑦 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑥 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑦‘𝑖)) + (𝑡 · (𝑧‘𝑖)))) ↔ ∃𝑛 ∈ ℕ ((𝐵 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑥 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑥‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝑧‘𝑖))))))
17		eleq1 2846	. . . . . . . . . 10 ⊢ (𝑧 = 𝐶 → (𝑧 ∈ (𝔼‘𝑛) ↔ 𝐶 ∈ (𝔼‘𝑛)))
18	17	3anbi2d 1514	. . . . . . . . 9 ⊢ (𝑧 = 𝐶 → ((𝐵 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑥 ∈ (𝔼‘𝑛)) ↔ (𝐵 ∈ (𝔼‘𝑛) ∧ 𝐶 ∈ (𝔼‘𝑛) ∧ 𝑥 ∈ (𝔼‘𝑛))))
19		fveq1 6445	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝐶 → (𝑧‘𝑖) = (𝐶‘𝑖))
20	19	oveq2d 6938	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝐶 → (𝑡 · (𝑧‘𝑖)) = (𝑡 · (𝐶‘𝑖)))
21	20	oveq2d 6938	. . . . . . . . . . 11 ⊢ (𝑧 = 𝐶 → (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝑧‘𝑖))) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖))))
22	21	eqeq2d 2787	. . . . . . . . . 10 ⊢ (𝑧 = 𝐶 → ((𝑥‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝑧‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
23	22	rexralbidv 3242	. . . . . . . . 9 ⊢ (𝑧 = 𝐶 → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑥‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝑧‘𝑖))) ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑥‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
24	18, 23	anbi12d 624	. . . . . . . 8 ⊢ (𝑧 = 𝐶 → (((𝐵 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑥 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑥‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝑧‘𝑖)))) ↔ ((𝐵 ∈ (𝔼‘𝑛) ∧ 𝐶 ∈ (𝔼‘𝑛) ∧ 𝑥 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑥‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖))))))
25	24	rexbidv 3236	. . . . . . 7 ⊢ (𝑧 = 𝐶 → (∃𝑛 ∈ ℕ ((𝐵 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑥 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑥‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝑧‘𝑖)))) ↔ ∃𝑛 ∈ ℕ ((𝐵 ∈ (𝔼‘𝑛) ∧ 𝐶 ∈ (𝔼‘𝑛) ∧ 𝑥 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑥‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖))))))
26		eleq1 2846	. . . . . . . . . 10 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ (𝔼‘𝑛) ↔ 𝐴 ∈ (𝔼‘𝑛)))
27	26	3anbi3d 1515	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → ((𝐵 ∈ (𝔼‘𝑛) ∧ 𝐶 ∈ (𝔼‘𝑛) ∧ 𝑥 ∈ (𝔼‘𝑛)) ↔ (𝐵 ∈ (𝔼‘𝑛) ∧ 𝐶 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛))))
28		fveq1 6445	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐴 → (𝑥‘𝑖) = (𝐴‘𝑖))
29	28	eqeq1d 2779	. . . . . . . . . 10 ⊢ (𝑥 = 𝐴 → ((𝑥‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ↔ (𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
30	29	rexralbidv 3242	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑥‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
31	27, 30	anbi12d 624	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (((𝐵 ∈ (𝔼‘𝑛) ∧ 𝐶 ∈ (𝔼‘𝑛) ∧ 𝑥 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑥‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) ↔ ((𝐵 ∈ (𝔼‘𝑛) ∧ 𝐶 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖))))))
32	31	rexbidv 3236	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (∃𝑛 ∈ ℕ ((𝐵 ∈ (𝔼‘𝑛) ∧ 𝐶 ∈ (𝔼‘𝑛) ∧ 𝑥 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑥‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) ↔ ∃𝑛 ∈ ℕ ((𝐵 ∈ (𝔼‘𝑛) ∧ 𝐶 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖))))))
33	16, 25, 32	eloprabg 7025	. . . . . 6 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (⟨⟨𝐵, 𝐶⟩, 𝐴⟩ ∈ {⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ ∃𝑛 ∈ ℕ ((𝑦 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑥 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑦‘𝑖)) + (𝑡 · (𝑧‘𝑖))))} ↔ ∃𝑛 ∈ ℕ ((𝐵 ∈ (𝔼‘𝑛) ∧ 𝐶 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖))))))
34		simp1 1127	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ (𝔼‘𝑛) ∧ 𝐶 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛)) → 𝐵 ∈ (𝔼‘𝑛))
35		simp1 1127	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → 𝐵 ∈ (𝔼‘𝑁))
36		eedimeq 26247	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 𝑛 = 𝑁)
37	34, 35, 36	syl2anr 590	. . . . . . . . . . 11 ⊢ (((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑛) ∧ 𝐶 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛))) → 𝑛 = 𝑁)
38		oveq2 6930	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑁 → (1...𝑛) = (1...𝑁))
39	38	raleqdv 3339	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑁 → (∀𝑖 ∈ (1...𝑛)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
40	39	rexbidv 3236	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑁 → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
41	37, 40	syl 17	. . . . . . . . . 10 ⊢ (((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑛) ∧ 𝐶 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛))) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
42	41	biimpd 221	. . . . . . . . 9 ⊢ (((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑛) ∧ 𝐶 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛))) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
43	42	expimpd 447	. . . . . . . 8 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (((𝐵 ∈ (𝔼‘𝑛) ∧ 𝐶 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
44	43	rexlimdvw 3216	. . . . . . 7 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (∃𝑛 ∈ ℕ ((𝐵 ∈ (𝔼‘𝑛) ∧ 𝐶 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
45		eleenn 26245	. . . . . . . . 9 ⊢ (𝐵 ∈ (𝔼‘𝑁) → 𝑁 ∈ ℕ)
46	45	3ad2ant1 1124	. . . . . . . 8 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ)
47		fveq2 6446	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑁 → (𝔼‘𝑛) = (𝔼‘𝑁))
48	47	eleq2d 2844	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑁 → (𝐵 ∈ (𝔼‘𝑛) ↔ 𝐵 ∈ (𝔼‘𝑁)))
49	47	eleq2d 2844	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑁 → (𝐶 ∈ (𝔼‘𝑛) ↔ 𝐶 ∈ (𝔼‘𝑁)))
50	47	eleq2d 2844	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑁 → (𝐴 ∈ (𝔼‘𝑛) ↔ 𝐴 ∈ (𝔼‘𝑁)))
51	48, 49, 50	3anbi123d 1509	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑁 → ((𝐵 ∈ (𝔼‘𝑛) ∧ 𝐶 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛)) ↔ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁))))
52	51, 40	anbi12d 624	. . . . . . . . . 10 ⊢ (𝑛 = 𝑁 → (((𝐵 ∈ (𝔼‘𝑛) ∧ 𝐶 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) ↔ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖))))))
53	52	rspcev 3510	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖))))) → ∃𝑛 ∈ ℕ ((𝐵 ∈ (𝔼‘𝑛) ∧ 𝐶 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
54	53	exp32 413	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖))) → ∃𝑛 ∈ ℕ ((𝐵 ∈ (𝔼‘𝑛) ∧ 𝐶 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))))
55	46, 54	mpcom 38	. . . . . . 7 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖))) → ∃𝑛 ∈ ℕ ((𝐵 ∈ (𝔼‘𝑛) ∧ 𝐶 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖))))))
56	44, 55	impbid 204	. . . . . 6 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (∃𝑛 ∈ ℕ ((𝐵 ∈ (𝔼‘𝑛) ∧ 𝐶 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
57	33, 56	bitrd 271	. . . . 5 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (⟨⟨𝐵, 𝐶⟩, 𝐴⟩ ∈ {⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ ∃𝑛 ∈ ℕ ((𝑦 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑥 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑦‘𝑖)) + (𝑡 · (𝑧‘𝑖))))} ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
58	57	3comr 1116	. . . 4 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (⟨⟨𝐵, 𝐶⟩, 𝐴⟩ ∈ {⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ ∃𝑛 ∈ ℕ ((𝑦 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑥 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑦‘𝑖)) + (𝑡 · (𝑧‘𝑖))))} ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
59	7, 58	syl5bb 275	. . 3 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (⟨𝐵, 𝐶⟩{⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ ∃𝑛 ∈ ℕ ((𝑦 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑥 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑦‘𝑖)) + (𝑡 · (𝑧‘𝑖))))}𝐴 ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
60	6, 59	bitrd 271	. 2 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐴^◡{⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ ∃𝑛 ∈ ℕ ((𝑦 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑥 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑦‘𝑖)) + (𝑡 · (𝑧‘𝑖))))}⟨𝐵, 𝐶⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
61	2, 60	syl5bb 275	1 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐴 Btwn ⟨𝐵, 𝐶⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (((1 − 𝑡) · (𝐵‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 ∧ w3a 1071 = wceq 1601 ∈ wcel 2106 ∀wral 3089 ∃wrex 3090 Vcvv 3397 ⟨cop 4403 class class class wbr 4886 ^◡ccnv 5354 ‘cfv 6135 (class class class)co 6922 {coprab 6923 0cc0 10272 1c1 10273 + caddc 10275 · cmul 10277 − cmin 10606 ℕcn 11374 [,]cicc 12490 ...cfz 12643 𝔼cee 26237 Btwn cbtwn 26238

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2054 ax-8 2108 ax-9 2115 ax-10 2134 ax-11 2149 ax-12 2162 ax-13 2333 ax-ext 2753 ax-sep 5017 ax-nul 5025 ax-pow 5077 ax-pr 5138 ax-un 7226 ax-cnex 10328 ax-resscn 10329 ax-1cn 10330 ax-icn 10331 ax-addcl 10332 ax-addrcl 10333 ax-mulcl 10334 ax-mulrcl 10335 ax-mulcom 10336 ax-addass 10337 ax-mulass 10338 ax-distr 10339 ax-i2m1 10340 ax-1ne0 10341 ax-1rid 10342 ax-rnegex 10343 ax-rrecex 10344 ax-cnre 10345 ax-pre-lttri 10346 ax-pre-lttrn 10347 ax-pre-ltadd 10348 ax-pre-mulgt0 10349

This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3or 1072 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2550 df-eu 2586 df-clab 2763 df-cleq 2769 df-clel 2773 df-nfc 2920 df-ne 2969 df-nel 3075 df-ral 3094 df-rex 3095 df-reu 3096 df-rab 3098 df-v 3399 df-sbc 3652 df-csb 3751 df-dif 3794 df-un 3796 df-in 3798 df-ss 3805 df-pss 3807 df-nul 4141 df-if 4307 df-pw 4380 df-sn 4398 df-pr 4400 df-tp 4402 df-op 4404 df-uni 4672 df-iun 4755 df-br 4887 df-opab 4949 df-mpt 4966 df-tr 4988 df-id 5261 df-eprel 5266 df-po 5274 df-so 5275 df-fr 5314 df-we 5316 df-xp 5361 df-rel 5362 df-cnv 5363 df-co 5364 df-dm 5365 df-rn 5366 df-res 5367 df-ima 5368 df-pred 5933 df-ord 5979 df-on 5980 df-lim 5981 df-suc 5982 df-iota 6099 df-fun 6137 df-fn 6138 df-f 6139 df-f1 6140 df-fo 6141 df-f1o 6142 df-fv 6143 df-riota 6883 df-ov 6925 df-oprab 6926 df-mpt2 6927 df-om 7344 df-1st 7445 df-2nd 7446 df-wrecs 7689 df-recs 7751 df-rdg 7789 df-er 8026 df-map 8142 df-en 8242 df-dom 8243 df-sdom 8244 df-pnf 10413 df-mnf 10414 df-xr 10415 df-ltxr 10416 df-le 10417 df-sub 10608 df-neg 10609 df-nn 11375 df-z 11729 df-uz 11993 df-fz 12644 df-ee 26240 df-btwn 26241

This theorem is referenced by: brbtwn2 26254 axsegcon 26276 ax5seg 26287 axbtwnid 26288 axpasch 26290 axeuclid 26312 axcontlem2 26314 axcontlem4 26316 axcontlem7 26319 axcontlem8 26320 elntg2 26334

W3C validator