axeuclid - Metamath Proof Explorer

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

Theorem axeuclid 26067

Description: Euclid's axiom. Take an angle 𝐵𝐴𝐶 and a point 𝐷 between 𝐵 and 𝐶. Now, if you extend the segment 𝐴𝐷 to a point 𝑇, then 𝑇 lies between two points 𝑥 and 𝑦 that lie on the angle. Axiom A10 of [Schwabhauser] p. 13. (Contributed by Scott Fenton, 9-Sep-2013.)

**Assertion**
Ref	Expression
axeuclid	⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn ⟨𝐴, 𝑇⟩ ∧ 𝐷 Btwn ⟨𝐵, 𝐶⟩ ∧ 𝐴 ≠ 𝐷) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)(𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝑦⟩ ∧ 𝑇 Btwn ⟨𝑥, 𝑦⟩)))

Distinct variable groups: 𝑥,𝐴,𝑦 𝑥,𝐵,𝑦 𝑥,𝐶,𝑦 𝑥,𝐷,𝑦 𝑥,𝑁,𝑦 𝑥,𝑇,𝑦

Proof of Theorem axeuclid Dummy variables 𝑖 𝑝 𝑞 𝑟 𝑠 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl21 1328	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → 𝐴 ∈ (𝔼‘𝑁))
2		simpl22 1330	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → 𝐵 ∈ (𝔼‘𝑁))
3	1, 2	jca 503	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)))
4		simpl23 1332	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → 𝐶 ∈ (𝔼‘𝑁))
5		simpl3r 1296	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → 𝑇 ∈ (𝔼‘𝑁))
6	4, 5	jca 503	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁)))
7		simprll 788	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → 𝑝 ∈ (0[,]1))
8		simprlr 789	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → 𝑞 ∈ (0[,]1))
9		simp21 1256	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁))
10	9	ad2antrr 708	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑝 = 0) → 𝐴 ∈ (𝔼‘𝑁))
11		fveecn 26006	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℂ)
12	10, 11	sylan 571	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑝 = 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℂ)
13		simp3r 1252	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → 𝑇 ∈ (𝔼‘𝑁))
14	13	ad2antrr 708	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑝 = 0) → 𝑇 ∈ (𝔼‘𝑁))
15		fveecn 26006	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑇 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑇‘𝑖) ∈ ℂ)
16	14, 15	sylan 571	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑝 = 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑇‘𝑖) ∈ ℂ)
17		mulid2 10331	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴‘𝑖) ∈ ℂ → (1 · (𝐴‘𝑖)) = (𝐴‘𝑖))
18		mul02 10506	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑇‘𝑖) ∈ ℂ → (0 · (𝑇‘𝑖)) = 0)
19	17, 18	oveqan12d 6900	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ) → ((1 · (𝐴‘𝑖)) + (0 · (𝑇‘𝑖))) = ((𝐴‘𝑖) + 0))
20		addid1 10508	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴‘𝑖) ∈ ℂ → ((𝐴‘𝑖) + 0) = (𝐴‘𝑖))
21	20	adantr 468	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ) → ((𝐴‘𝑖) + 0) = (𝐴‘𝑖))
22	19, 21	eqtrd 2851	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ) → ((1 · (𝐴‘𝑖)) + (0 · (𝑇‘𝑖))) = (𝐴‘𝑖))
23	12, 16, 22	syl2anc 575	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑝 = 0) ∧ 𝑖 ∈ (1...𝑁)) → ((1 · (𝐴‘𝑖)) + (0 · (𝑇‘𝑖))) = (𝐴‘𝑖))
24		oveq2 6889	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = 0 → (1 − 𝑝) = (1 − 0))
25		1m0e1 11420	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 − 0) = 1
26	24, 25	syl6eq 2867	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = 0 → (1 − 𝑝) = 1)
27	26	oveq1d 6896	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 0 → ((1 − 𝑝) · (𝐴‘𝑖)) = (1 · (𝐴‘𝑖)))
28		oveq1 6888	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 0 → (𝑝 · (𝑇‘𝑖)) = (0 · (𝑇‘𝑖)))
29	27, 28	oveq12d 6899	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 0 → (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) = ((1 · (𝐴‘𝑖)) + (0 · (𝑇‘𝑖))))
30	29	eqeq1d 2819	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 0 → ((((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) = (𝐴‘𝑖) ↔ ((1 · (𝐴‘𝑖)) + (0 · (𝑇‘𝑖))) = (𝐴‘𝑖)))
31	30	ad2antlr 709	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑝 = 0) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) = (𝐴‘𝑖) ↔ ((1 · (𝐴‘𝑖)) + (0 · (𝑇‘𝑖))) = (𝐴‘𝑖)))
32	23, 31	mpbird 248	. . . . . . . . . . . . . . 15 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑝 = 0) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) = (𝐴‘𝑖))
33	32	eqeq2d 2827	. . . . . . . . . . . . . 14 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑝 = 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ↔ (𝐷‘𝑖) = (𝐴‘𝑖)))
34		eqcom 2824	. . . . . . . . . . . . . 14 ⊢ ((𝐷‘𝑖) = (𝐴‘𝑖) ↔ (𝐴‘𝑖) = (𝐷‘𝑖))
35	33, 34	syl6bb 278	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑝 = 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ↔ (𝐴‘𝑖) = (𝐷‘𝑖)))
36	35	biimpd 220	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑝 = 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) → (𝐴‘𝑖) = (𝐷‘𝑖)))
37	36	adantrd 481	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑝 = 0) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) → (𝐴‘𝑖) = (𝐷‘𝑖)))
38	37	ralimdva 3161	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑝 = 0) → (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (𝐷‘𝑖)))
39	38	impancom 441	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))))) → (𝑝 = 0 → ∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (𝐷‘𝑖)))
40	9	ad2antrr 708	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))))) → 𝐴 ∈ (𝔼‘𝑁))
41		simp3l 1251	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁))
42	41	ad2antrr 708	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))))) → 𝐷 ∈ (𝔼‘𝑁))
43		eqeefv 26007	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) → (𝐴 = 𝐷 ↔ ∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (𝐷‘𝑖)))
44	40, 42, 43	syl2anc 575	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))))) → (𝐴 = 𝐷 ↔ ∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (𝐷‘𝑖)))
45	39, 44	sylibrd 250	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))))) → (𝑝 = 0 → 𝐴 = 𝐷))
46	45	necon3d 3010	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))))) → (𝐴 ≠ 𝐷 → 𝑝 ≠ 0))
47	46	impr 444	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷)) → 𝑝 ≠ 0)
48	47	anasss 454	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → 𝑝 ≠ 0)
49		eqtr2 2837	. . . . . . . 8 ⊢ (((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) → (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))))
50	49	ralimi 3151	. . . . . . 7 ⊢ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))))
51	50	adantr 468	. . . . . 6 ⊢ ((∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))))
52	51	ad2antll 711	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))))
53		axeuclidlem 26066	. . . . 5 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1) ∧ 𝑝 ≠ 0) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
54	3, 6, 7, 8, 48, 52, 53	syl231anc 1502	. . . 4 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
55	54	exp32 409	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) → ((∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))))
56	55	rexlimdvv 3236	. 2 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → (∃𝑝 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
57		brbtwn 26003	. . . . 5 ⊢ ((𝐷 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁)) → (𝐷 Btwn ⟨𝐴, 𝑇⟩ ↔ ∃𝑝 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖)))))
58	41, 9, 13, 57	syl3anc 1483	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → (𝐷 Btwn ⟨𝐴, 𝑇⟩ ↔ ∃𝑝 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖)))))
59		simp22 1257	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁))
60		simp23 1258	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁))
61		brbtwn 26003	. . . . 5 ⊢ ((𝐷 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐷 Btwn ⟨𝐵, 𝐶⟩ ↔ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))))
62	41, 59, 60, 61	syl3anc 1483	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → (𝐷 Btwn ⟨𝐵, 𝐶⟩ ↔ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))))
63	58, 62	3anbi12d 1554	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn ⟨𝐴, 𝑇⟩ ∧ 𝐷 Btwn ⟨𝐵, 𝐶⟩ ∧ 𝐴 ≠ 𝐷) ↔ (∃𝑝 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))) ∧ 𝐴 ≠ 𝐷)))
64		r19.26 3263	. . . . . . 7 ⊢ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))))
65	64	2rexbii 3241	. . . . . 6 ⊢ (∃𝑝 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ↔ ∃𝑝 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))))
66		reeanv 3306	. . . . . 6 ⊢ (∃𝑝 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ↔ (∃𝑝 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))))
67	65, 66	bitri 266	. . . . 5 ⊢ (∃𝑝 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ↔ (∃𝑝 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))))
68	67	anbi1i 612	. . . 4 ⊢ ((∃𝑝 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷) ↔ ((∃𝑝 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))
69		r19.41vv 3290	. . . 4 ⊢ (∃𝑝 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷) ↔ (∃𝑝 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))
70		df-3an 1102	. . . 4 ⊢ ((∃𝑝 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))) ∧ 𝐴 ≠ 𝐷) ↔ ((∃𝑝 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))
71	68, 69, 70	3bitr4i 294	. . 3 ⊢ (∃𝑝 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷) ↔ (∃𝑝 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))) ∧ 𝐴 ≠ 𝐷))
72	63, 71	syl6bbr 280	. 2 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn ⟨𝐴, 𝑇⟩ ∧ 𝐷 Btwn ⟨𝐵, 𝐶⟩ ∧ 𝐴 ≠ 𝐷) ↔ ∃𝑝 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷)))
73		simpl22 1330	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁))
74		simpl21 1328	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁))
75		simprl 778	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝑥 ∈ (𝔼‘𝑁))
76		brbtwn 26003	. . . . . 6 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝐵 Btwn ⟨𝐴, 𝑥⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖)))))
77	73, 74, 75, 76	syl3anc 1483	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (𝐵 Btwn ⟨𝐴, 𝑥⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖)))))
78		simpl23 1332	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁))
79		simprr 780	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝑦 ∈ (𝔼‘𝑁))
80		brbtwn 26003	. . . . . 6 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (𝐶 Btwn ⟨𝐴, 𝑦⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖)))))
81	78, 74, 79, 80	syl3anc 1483	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (𝐶 Btwn ⟨𝐴, 𝑦⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖)))))
82		simpl3r 1296	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝑇 ∈ (𝔼‘𝑁))
83		brbtwn 26003	. . . . . 6 ⊢ ((𝑇 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (𝑇 Btwn ⟨𝑥, 𝑦⟩ ↔ ∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
84	82, 75, 79, 83	syl3anc 1483	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (𝑇 Btwn ⟨𝑥, 𝑦⟩ ↔ ∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
85	77, 81, 84	3anbi123d 1553	. . . 4 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝑦⟩ ∧ 𝑇 Btwn ⟨𝑥, 𝑦⟩) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ ∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
86		r19.26-3 3265	. . . . . . 7 ⊢ (∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
87	86	rexbii 3240	. . . . . 6 ⊢ (∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑢 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
88	87	2rexbii 3241	. . . . 5 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
89		3reeanv 3307	. . . . 5 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ ∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
90	88, 89	bitri 266	. . . 4 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ ∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
91	85, 90	syl6bbr 280	. . 3 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝑦⟩ ∧ 𝑇 Btwn ⟨𝑥, 𝑦⟩) ↔ ∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
92	91	2rexbidva 3255	. 2 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → (∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)(𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝑦⟩ ∧ 𝑇 Btwn ⟨𝑥, 𝑦⟩) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
93	56, 72, 92	3imtr4d 285	1 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn ⟨𝐴, 𝑇⟩ ∧ 𝐷 Btwn ⟨𝐵, 𝐶⟩ ∧ 𝐴 ≠ 𝐷) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)(𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝑦⟩ ∧ 𝑇 Btwn ⟨𝑥, 𝑦⟩)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 197 ∧ wa 384 ∧ w3a 1100 = wceq 1637 ∈ wcel 2157 ≠ wne 2989 ∀wral 3107 ∃wrex 3108 ⟨cop 4387 class class class wbr 4855 ‘cfv 6108 (class class class)co 6881 ℂcc 10226 0cc0 10228 1c1 10229 + caddc 10231 · cmul 10233 − cmin 10558 ℕcn 11312 [,]cicc 12403 ...cfz 12556 𝔼cee 25992 Btwn cbtwn 25993

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1877 ax-4 1894 ax-5 2001 ax-6 2069 ax-7 2105 ax-8 2159 ax-9 2166 ax-10 2186 ax-11 2202 ax-12 2215 ax-13 2422 ax-ext 2795 ax-sep 4986 ax-nul 4994 ax-pow 5046 ax-pr 5107 ax-un 7186 ax-cnex 10284 ax-resscn 10285 ax-1cn 10286 ax-icn 10287 ax-addcl 10288 ax-addrcl 10289 ax-mulcl 10290 ax-mulrcl 10291 ax-mulcom 10292 ax-addass 10293 ax-mulass 10294 ax-distr 10295 ax-i2m1 10296 ax-1ne0 10297 ax-1rid 10298 ax-rnegex 10299 ax-rrecex 10300 ax-cnre 10301 ax-pre-lttri 10302 ax-pre-lttrn 10303 ax-pre-ltadd 10304 ax-pre-mulgt0 10305

This theorem depends on definitions: df-bi 198 df-an 385 df-or 866 df-3or 1101 df-3an 1102 df-tru 1641 df-ex 1860 df-nf 1864 df-sb 2062 df-mo 2635 df-eu 2642 df-clab 2804 df-cleq 2810 df-clel 2813 df-nfc 2948 df-ne 2990 df-nel 3093 df-ral 3112 df-rex 3113 df-reu 3114 df-rmo 3115 df-rab 3116 df-v 3404 df-sbc 3645 df-csb 3740 df-dif 3783 df-un 3785 df-in 3787 df-ss 3794 df-pss 3796 df-nul 4128 df-if 4291 df-pw 4364 df-sn 4382 df-pr 4384 df-tp 4386 df-op 4388 df-uni 4642 df-iun 4725 df-br 4856 df-opab 4918 df-mpt 4935 df-tr 4958 df-id 5230 df-eprel 5235 df-po 5243 df-so 5244 df-fr 5281 df-we 5283 df-xp 5328 df-rel 5329 df-cnv 5330 df-co 5331 df-dm 5332 df-rn 5333 df-res 5334 df-ima 5335 df-pred 5904 df-ord 5950 df-on 5951 df-lim 5952 df-suc 5953 df-iota 6071 df-fun 6110 df-fn 6111 df-f 6112 df-f1 6113 df-fo 6114 df-f1o 6115 df-fv 6116 df-riota 6842 df-ov 6884 df-oprab 6885 df-mpt2 6886 df-om 7303 df-1st 7405 df-2nd 7406 df-wrecs 7649 df-recs 7711 df-rdg 7749 df-er 7986 df-map 8101 df-en 8200 df-dom 8201 df-sdom 8202 df-pnf 10368 df-mnf 10369 df-xr 10370 df-ltxr 10371 df-le 10372 df-sub 10560 df-neg 10561 df-div 10977 df-nn 11313 df-z 11651 df-uz 11912 df-icc 12407 df-fz 12557 df-ee 25995 df-btwn 25996

This theorem is referenced by: eengtrkge 26090

W3C validator