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 28996

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 1251	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → 𝐴 ∈ (𝔼‘𝑁))
2		simpl22 1252	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → 𝐵 ∈ (𝔼‘𝑁))
3	1, 2	jca 511	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)))
4		simpl23 1253	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → 𝐶 ∈ (𝔼‘𝑁))
5		simpl3r 1229	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → 𝑇 ∈ (𝔼‘𝑁))
6	4, 5	jca 511	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁)))
7		simprll 778	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → 𝑝 ∈ (0[,]1))
8		simprlr 779	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → 𝑞 ∈ (0[,]1))
9		simp21 1206	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁))
10	9	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑝 = 0) → 𝐴 ∈ (𝔼‘𝑁))
11		fveecn 28935	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℂ)
12	10, 11	sylan 579	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑝 = 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℂ)
13		simp3r 1202	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → 𝑇 ∈ (𝔼‘𝑁))
14	13	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑝 = 0) → 𝑇 ∈ (𝔼‘𝑁))
15		fveecn 28935	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑇 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑇‘𝑖) ∈ ℂ)
16	14, 15	sylan 579	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑝 = 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑇‘𝑖) ∈ ℂ)
17		mullid 11289	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴‘𝑖) ∈ ℂ → (1 · (𝐴‘𝑖)) = (𝐴‘𝑖))
18		mul02 11468	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑇‘𝑖) ∈ ℂ → (0 · (𝑇‘𝑖)) = 0)
19	17, 18	oveqan12d 7467	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ) → ((1 · (𝐴‘𝑖)) + (0 · (𝑇‘𝑖))) = ((𝐴‘𝑖) + 0))
20		addrid 11470	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴‘𝑖) ∈ ℂ → ((𝐴‘𝑖) + 0) = (𝐴‘𝑖))
21	20	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ) → ((𝐴‘𝑖) + 0) = (𝐴‘𝑖))
22	19, 21	eqtrd 2780	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ) → ((1 · (𝐴‘𝑖)) + (0 · (𝑇‘𝑖))) = (𝐴‘𝑖))
23	12, 16, 22	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑝 = 0) ∧ 𝑖 ∈ (1...𝑁)) → ((1 · (𝐴‘𝑖)) + (0 · (𝑇‘𝑖))) = (𝐴‘𝑖))
24		oveq2 7456	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = 0 → (1 − 𝑝) = (1 − 0))
25		1m0e1 12414	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 − 0) = 1
26	24, 25	eqtrdi 2796	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = 0 → (1 − 𝑝) = 1)
27	26	oveq1d 7463	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 0 → ((1 − 𝑝) · (𝐴‘𝑖)) = (1 · (𝐴‘𝑖)))
28		oveq1 7455	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 0 → (𝑝 · (𝑇‘𝑖)) = (0 · (𝑇‘𝑖)))
29	27, 28	oveq12d 7466	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 0 → (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) = ((1 · (𝐴‘𝑖)) + (0 · (𝑇‘𝑖))))
30	29	eqeq1d 2742	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 0 → ((((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) = (𝐴‘𝑖) ↔ ((1 · (𝐴‘𝑖)) + (0 · (𝑇‘𝑖))) = (𝐴‘𝑖)))
31	30	ad2antlr 726	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑝 = 0) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) = (𝐴‘𝑖) ↔ ((1 · (𝐴‘𝑖)) + (0 · (𝑇‘𝑖))) = (𝐴‘𝑖)))
32	23, 31	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑝 = 0) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) = (𝐴‘𝑖))
33	32	eqeq2d 2751	. . . . . . . . . . . . . 14 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑝 = 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ↔ (𝐷‘𝑖) = (𝐴‘𝑖)))
34		eqcom 2747	. . . . . . . . . . . . . 14 ⊢ ((𝐷‘𝑖) = (𝐴‘𝑖) ↔ (𝐴‘𝑖) = (𝐷‘𝑖))
35	33, 34	bitrdi 287	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑝 = 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ↔ (𝐴‘𝑖) = (𝐷‘𝑖)))
36	35	biimpd 229	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑝 = 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) → (𝐴‘𝑖) = (𝐷‘𝑖)))
37	36	adantrd 491	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑝 = 0) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) → (𝐴‘𝑖) = (𝐷‘𝑖)))
38	37	ralimdva 3173	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑝 = 0) → (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (𝐷‘𝑖)))
39	38	impancom 451	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))))) → (𝑝 = 0 → ∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (𝐷‘𝑖)))
40	9	ad2antrr 725	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))))) → 𝐴 ∈ (𝔼‘𝑁))
41		simp3l 1201	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁))
42	41	ad2antrr 725	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))))) → 𝐷 ∈ (𝔼‘𝑁))
43		eqeefv 28936	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) → (𝐴 = 𝐷 ↔ ∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (𝐷‘𝑖)))
44	40, 42, 43	syl2anc 583	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))))) → (𝐴 = 𝐷 ↔ ∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (𝐷‘𝑖)))
45	39, 44	sylibrd 259	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))))) → (𝑝 = 0 → 𝐴 = 𝐷))
46	45	necon3d 2967	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))))) → (𝐴 ≠ 𝐷 → 𝑝 ≠ 0))
47	46	impr 454	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷)) → 𝑝 ≠ 0)
48	47	anasss 466	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → 𝑝 ≠ 0)
49		eqtr2 2764	. . . . . . . 8 ⊢ (((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) → (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))))
50	49	ralimi 3089	. . . . . . 7 ⊢ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))))
51	50	adantr 480	. . . . . 6 ⊢ ((∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))))
52	51	ad2antll 728	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))))
53		axeuclidlem 28995	. . . . 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 1390	. . . 4 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
55	54	exp32 420	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) → ((∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))))
56	55	rexlimdvv 3218	. 2 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → (∃𝑝 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
57		brbtwn 28932	. . . . 5 ⊢ ((𝐷 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁)) → (𝐷 Btwn ⟨𝐴, 𝑇⟩ ↔ ∃𝑝 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖)))))
58	41, 9, 13, 57	syl3anc 1371	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → (𝐷 Btwn ⟨𝐴, 𝑇⟩ ↔ ∃𝑝 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖)))))
59		simp22 1207	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁))
60		simp23 1208	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁))
61		brbtwn 28932	. . . . 5 ⊢ ((𝐷 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐷 Btwn ⟨𝐵, 𝐶⟩ ↔ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))))
62	41, 59, 60, 61	syl3anc 1371	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → (𝐷 Btwn ⟨𝐵, 𝐶⟩ ↔ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))))
63	58, 62	3anbi12d 1437	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn ⟨𝐴, 𝑇⟩ ∧ 𝐷 Btwn ⟨𝐵, 𝐶⟩ ∧ 𝐴 ≠ 𝐷) ↔ (∃𝑝 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))) ∧ 𝐴 ≠ 𝐷)))
64		r19.26 3117	. . . . . . 7 ⊢ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))))
65	64	2rexbii 3135	. . . . . 6 ⊢ (∃𝑝 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ↔ ∃𝑝 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))))
66		reeanv 3235	. . . . . 6 ⊢ (∃𝑝 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ↔ (∃𝑝 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))))
67	65, 66	bitri 275	. . . . 5 ⊢ (∃𝑝 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ↔ (∃𝑝 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))))
68	67	anbi1i 623	. . . 4 ⊢ ((∃𝑝 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷) ↔ ((∃𝑝 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))
69		r19.41vv 3233	. . . 4 ⊢ (∃𝑝 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷) ↔ (∃𝑝 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))
70		df-3an 1089	. . . 4 ⊢ ((∃𝑝 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))) ∧ 𝐴 ≠ 𝐷) ↔ ((∃𝑝 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))
71	68, 69, 70	3bitr4i 303	. . 3 ⊢ (∃𝑝 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷) ↔ (∃𝑝 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))) ∧ 𝐴 ≠ 𝐷))
72	63, 71	bitr4di 289	. 2 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn ⟨𝐴, 𝑇⟩ ∧ 𝐷 Btwn ⟨𝐵, 𝐶⟩ ∧ 𝐴 ≠ 𝐷) ↔ ∃𝑝 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷)))
73		simpl22 1252	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁))
74		simpl21 1251	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁))
75		simprl 770	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝑥 ∈ (𝔼‘𝑁))
76		brbtwn 28932	. . . . . 6 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝐵 Btwn ⟨𝐴, 𝑥⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖)))))
77	73, 74, 75, 76	syl3anc 1371	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (𝐵 Btwn ⟨𝐴, 𝑥⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖)))))
78		simpl23 1253	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁))
79		simprr 772	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝑦 ∈ (𝔼‘𝑁))
80		brbtwn 28932	. . . . . 6 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (𝐶 Btwn ⟨𝐴, 𝑦⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖)))))
81	78, 74, 79, 80	syl3anc 1371	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (𝐶 Btwn ⟨𝐴, 𝑦⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖)))))
82		simpl3r 1229	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝑇 ∈ (𝔼‘𝑁))
83		brbtwn 28932	. . . . . 6 ⊢ ((𝑇 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (𝑇 Btwn ⟨𝑥, 𝑦⟩ ↔ ∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
84	82, 75, 79, 83	syl3anc 1371	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (𝑇 Btwn ⟨𝑥, 𝑦⟩ ↔ ∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
85	77, 81, 84	3anbi123d 1436	. . . 4 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝑦⟩ ∧ 𝑇 Btwn ⟨𝑥, 𝑦⟩) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ ∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
86		r19.26-3 3118	. . . . . . 7 ⊢ (∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
87	86	rexbii 3100	. . . . . 6 ⊢ (∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑢 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
88	87	2rexbii 3135	. . . . 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 3236	. . . . 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 275	. . . 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	bitr4di 289	. . 3 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝑦⟩ ∧ 𝑇 Btwn ⟨𝑥, 𝑦⟩) ↔ ∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
92	91	2rexbidva 3226	. 2 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → (∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)(𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝑦⟩ ∧ 𝑇 Btwn ⟨𝑥, 𝑦⟩) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
93	56, 72, 92	3imtr4d 294	1 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn ⟨𝐴, 𝑇⟩ ∧ 𝐷 Btwn ⟨𝐵, 𝐶⟩ ∧ 𝐴 ≠ 𝐷) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)(𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝑦⟩ ∧ 𝑇 Btwn ⟨𝑥, 𝑦⟩)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1537 ∈ wcel 2108 ≠ wne 2946 ∀wral 3067 ∃wrex 3076 ⟨cop 4654 class class class wbr 5166 ‘cfv 6573 (class class class)co 7448 ℂcc 11182 0cc0 11184 1c1 11185 + caddc 11187 · cmul 11189 − cmin 11520 ℕcn 12293 [,]cicc 13410 ...cfz 13567 𝔼cee 28921 Btwn cbtwn 28922

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 ax-cnex 11240 ax-resscn 11241 ax-1cn 11242 ax-icn 11243 ax-addcl 11244 ax-addrcl 11245 ax-mulcl 11246 ax-mulrcl 11247 ax-mulcom 11248 ax-addass 11249 ax-mulass 11250 ax-distr 11251 ax-i2m1 11252 ax-1ne0 11253 ax-1rid 11254 ax-rnegex 11255 ax-rrecex 11256 ax-cnre 11257 ax-pre-lttri 11258 ax-pre-lttrn 11259 ax-pre-ltadd 11260 ax-pre-mulgt0 11261

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-iun 5017 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-pred 6332 df-ord 6398 df-on 6399 df-lim 6400 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-om 7904 df-1st 8030 df-2nd 8031 df-frecs 8322 df-wrecs 8353 df-recs 8427 df-rdg 8466 df-er 8763 df-map 8886 df-en 9004 df-dom 9005 df-sdom 9006 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11522 df-neg 11523 df-div 11948 df-nn 12294 df-z 12640 df-uz 12904 df-icc 13414 df-fz 13568 df-ee 28924 df-btwn 28925

This theorem is referenced by: eengtrkge 29020

W3C validator