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 28993

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 1250	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → 𝐴 ∈ (𝔼‘𝑁))
2		simpl22 1251	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → 𝐵 ∈ (𝔼‘𝑁))
3	1, 2	jca 511	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)))
4		simpl23 1252	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → 𝐶 ∈ (𝔼‘𝑁))
5		simpl3r 1228	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → 𝑇 ∈ (𝔼‘𝑁))
6	4, 5	jca 511	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁)))
7		simprll 779	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → 𝑝 ∈ (0[,]1))
8		simprlr 780	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → 𝑞 ∈ (0[,]1))
9		simp21 1205	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁))
10	9	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑝 = 0) → 𝐴 ∈ (𝔼‘𝑁))
11		fveecn 28932	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℂ)
12	10, 11	sylan 580	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑝 = 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℂ)
13		simp3r 1201	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → 𝑇 ∈ (𝔼‘𝑁))
14	13	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑝 = 0) → 𝑇 ∈ (𝔼‘𝑁))
15		fveecn 28932	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑇 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑇‘𝑖) ∈ ℂ)
16	14, 15	sylan 580	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑝 = 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑇‘𝑖) ∈ ℂ)
17		mullid 11258	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴‘𝑖) ∈ ℂ → (1 · (𝐴‘𝑖)) = (𝐴‘𝑖))
18		mul02 11437	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑇‘𝑖) ∈ ℂ → (0 · (𝑇‘𝑖)) = 0)
19	17, 18	oveqan12d 7450	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ) → ((1 · (𝐴‘𝑖)) + (0 · (𝑇‘𝑖))) = ((𝐴‘𝑖) + 0))
20		addrid 11439	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴‘𝑖) ∈ ℂ → ((𝐴‘𝑖) + 0) = (𝐴‘𝑖))
21	20	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ) → ((𝐴‘𝑖) + 0) = (𝐴‘𝑖))
22	19, 21	eqtrd 2775	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ) → ((1 · (𝐴‘𝑖)) + (0 · (𝑇‘𝑖))) = (𝐴‘𝑖))
23	12, 16, 22	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑝 = 0) ∧ 𝑖 ∈ (1...𝑁)) → ((1 · (𝐴‘𝑖)) + (0 · (𝑇‘𝑖))) = (𝐴‘𝑖))
24		oveq2 7439	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = 0 → (1 − 𝑝) = (1 − 0))
25		1m0e1 12385	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 − 0) = 1
26	24, 25	eqtrdi 2791	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = 0 → (1 − 𝑝) = 1)
27	26	oveq1d 7446	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 0 → ((1 − 𝑝) · (𝐴‘𝑖)) = (1 · (𝐴‘𝑖)))
28		oveq1 7438	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 0 → (𝑝 · (𝑇‘𝑖)) = (0 · (𝑇‘𝑖)))
29	27, 28	oveq12d 7449	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 0 → (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) = ((1 · (𝐴‘𝑖)) + (0 · (𝑇‘𝑖))))
30	29	eqeq1d 2737	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 0 → ((((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) = (𝐴‘𝑖) ↔ ((1 · (𝐴‘𝑖)) + (0 · (𝑇‘𝑖))) = (𝐴‘𝑖)))
31	30	ad2antlr 727	. . . . . . . . . . . . . . . 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 2746	. . . . . . . . . . . . . 14 ⊢ (((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑝 = 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ↔ (𝐷‘𝑖) = (𝐴‘𝑖)))
34		eqcom 2742	. . . . . . . . . . . . . 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 3165	. . . . . . . . . 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 726	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))))) → 𝐴 ∈ (𝔼‘𝑁))
41		simp3l 1200	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁))
42	41	ad2antrr 726	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))))) → 𝐷 ∈ (𝔼‘𝑁))
43		eqeefv 28933	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) → (𝐴 = 𝐷 ↔ ∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (𝐷‘𝑖)))
44	40, 42, 43	syl2anc 584	. . . . . . . . 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 2959	. . . . . . 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 2759	. . . . . . . 8 ⊢ (((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) → (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))))
50	49	ralimi 3081	. . . . . . 7 ⊢ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))))
51	50	adantr 480	. . . . . 6 ⊢ ((∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))))
52	51	ad2antll 729	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ ((𝑝 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))))
53		axeuclidlem 28992	. . . . 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 1389	. . . 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 3210	. 2 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → (∃𝑝 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
57		brbtwn 28929	. . . . 5 ⊢ ((𝐷 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁)) → (𝐷 Btwn ⟨𝐴, 𝑇⟩ ↔ ∃𝑝 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖)))))
58	41, 9, 13, 57	syl3anc 1370	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → (𝐷 Btwn ⟨𝐴, 𝑇⟩ ↔ ∃𝑝 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖)))))
59		simp22 1206	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁))
60		simp23 1207	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁))
61		brbtwn 28929	. . . . 5 ⊢ ((𝐷 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐷 Btwn ⟨𝐵, 𝐶⟩ ↔ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))))
62	41, 59, 60, 61	syl3anc 1370	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → (𝐷 Btwn ⟨𝐵, 𝐶⟩ ↔ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))))
63	58, 62	3anbi12d 1436	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn ⟨𝐴, 𝑇⟩ ∧ 𝐷 Btwn ⟨𝐵, 𝐶⟩ ∧ 𝐴 ≠ 𝐷) ↔ (∃𝑝 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖))) ∧ 𝐴 ≠ 𝐷)))
64		r19.26 3109	. . . . . . 7 ⊢ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))))
65	64	2rexbii 3127	. . . . . 6 ⊢ (∃𝑝 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ↔ ∃𝑝 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))))
66		reeanv 3227	. . . . . 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 624	. . . 4 ⊢ ((∃𝑝 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷) ↔ ((∃𝑝 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))
69		r19.41vv 3225	. . . 4 ⊢ (∃𝑝 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷) ↔ (∃𝑝 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑝) · (𝐴‘𝑖)) + (𝑝 · (𝑇‘𝑖))) ∧ (𝐷‘𝑖) = (((1 − 𝑞) · (𝐵‘𝑖)) + (𝑞 · (𝐶‘𝑖)))) ∧ 𝐴 ≠ 𝐷))
70		df-3an 1088	. . . 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 1251	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁))
74		simpl21 1250	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁))
75		simprl 771	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝑥 ∈ (𝔼‘𝑁))
76		brbtwn 28929	. . . . . 6 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝐵 Btwn ⟨𝐴, 𝑥⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖)))))
77	73, 74, 75, 76	syl3anc 1370	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (𝐵 Btwn ⟨𝐴, 𝑥⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖)))))
78		simpl23 1252	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁))
79		simprr 773	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝑦 ∈ (𝔼‘𝑁))
80		brbtwn 28929	. . . . . 6 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (𝐶 Btwn ⟨𝐴, 𝑦⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖)))))
81	78, 74, 79, 80	syl3anc 1370	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (𝐶 Btwn ⟨𝐴, 𝑦⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖)))))
82		simpl3r 1228	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝑇 ∈ (𝔼‘𝑁))
83		brbtwn 28929	. . . . . 6 ⊢ ((𝑇 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (𝑇 Btwn ⟨𝑥, 𝑦⟩ ↔ ∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
84	82, 75, 79, 83	syl3anc 1370	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (𝑇 Btwn ⟨𝑥, 𝑦⟩ ↔ ∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
85	77, 81, 84	3anbi123d 1435	. . . 4 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn ⟨𝐴, 𝑥⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝑦⟩ ∧ 𝑇 Btwn ⟨𝑥, 𝑦⟩) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ ∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
86		r19.26-3 3110	. . . . . . 7 ⊢ (∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
87	86	rexbii 3092	. . . . . 6 ⊢ (∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑢 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
88	87	2rexbii 3127	. . . . 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 3228	. . . . 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 3218	. 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 1086 = wceq 1537 ∈ wcel 2106 ≠ wne 2938 ∀wral 3059 ∃wrex 3068 ⟨cop 4637 class class class wbr 5148 ‘cfv 6563 (class class class)co 7431 ℂcc 11151 0cc0 11153 1c1 11154 + caddc 11156 · cmul 11158 − cmin 11490 ℕcn 12264 [,]cicc 13387 ...cfz 13544 𝔼cee 28918 Btwn cbtwn 28919

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 ax-sep 5302 ax-nul 5312 ax-pow 5371 ax-pr 5438 ax-un 7754 ax-cnex 11209 ax-resscn 11210 ax-1cn 11211 ax-icn 11212 ax-addcl 11213 ax-addrcl 11214 ax-mulcl 11215 ax-mulrcl 11216 ax-mulcom 11217 ax-addass 11218 ax-mulass 11219 ax-distr 11220 ax-i2m1 11221 ax-1ne0 11222 ax-1rid 11223 ax-rnegex 11224 ax-rrecex 11225 ax-cnre 11226 ax-pre-lttri 11227 ax-pre-lttrn 11228 ax-pre-ltadd 11229 ax-pre-mulgt0 11230

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-nf 1781 df-sb 2063 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3378 df-reu 3379 df-rab 3434 df-v 3480 df-sbc 3792 df-csb 3909 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-pss 3983 df-nul 4340 df-if 4532 df-pw 4607 df-sn 4632 df-pr 4634 df-op 4638 df-uni 4913 df-iun 4998 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5583 df-eprel 5589 df-po 5597 df-so 5598 df-fr 5641 df-we 5643 df-xp 5695 df-rel 5696 df-cnv 5697 df-co 5698 df-dm 5699 df-rn 5700 df-res 5701 df-ima 5702 df-pred 6323 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6516 df-fun 6565 df-fn 6566 df-f 6567 df-f1 6568 df-fo 6569 df-f1o 6570 df-fv 6571 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8013 df-2nd 8014 df-frecs 8305 df-wrecs 8336 df-recs 8410 df-rdg 8449 df-er 8744 df-map 8867 df-en 8985 df-dom 8986 df-sdom 8987 df-pnf 11295 df-mnf 11296 df-xr 11297 df-ltxr 11298 df-le 11299 df-sub 11492 df-neg 11493 df-div 11919 df-nn 12265 df-z 12612 df-uz 12877 df-icc 13391 df-fz 13545 df-ee 28921 df-btwn 28922

This theorem is referenced by: eengtrkge 29017

W3C validator