axcontlem4 - Metamath Proof Explorer

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

Theorem axcontlem4 26316

Description: Lemma for axcont 26325. Given the separation assumption, 𝐴 is a subset of 𝐷. (Contributed by Scott Fenton, 18-Jun-2013.)

**Hypothesis**
Ref	Expression
axcontlem4.1	⊢ 𝐷 = {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)}

**Assertion**
Ref	Expression
axcontlem4	⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) ∧ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅) ∧ 𝑍 ≠ 𝑈)) → 𝐴 ⊆ 𝐷)

Distinct variable groups: 𝐴,𝑝,𝑥 𝐵,𝑝,𝑥,𝑦 𝑁,𝑝,𝑥,𝑦 𝑈,𝑝,𝑥,𝑦 𝑍,𝑝,𝑥,𝑦 Allowed substitution hints: 𝐴(𝑦) 𝐷(𝑥,𝑦,𝑝)

Proof of Theorem axcontlem4 Dummy variables 𝑏 𝑖 𝑟 𝑡 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simplr1 1232	. 2 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) ∧ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅) ∧ 𝑍 ≠ 𝑈)) → 𝐴 ⊆ (𝔼‘𝑁))
2		n0 4158	. . . . . 6 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑏 𝑏 ∈ 𝐵)
3		idd 24	. . . . . . . . . 10 ⊢ (𝑏 ∈ 𝐵 → (𝐴 ⊆ (𝔼‘𝑁) → 𝐴 ⊆ (𝔼‘𝑁)))
4		ssel 3814	. . . . . . . . . . 11 ⊢ (𝐵 ⊆ (𝔼‘𝑁) → (𝑏 ∈ 𝐵 → 𝑏 ∈ (𝔼‘𝑁)))
5	4	com12 32	. . . . . . . . . 10 ⊢ (𝑏 ∈ 𝐵 → (𝐵 ⊆ (𝔼‘𝑁) → 𝑏 ∈ (𝔼‘𝑁)))
6		opeq2 4637	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑏 → ⟨𝑍, 𝑦⟩ = ⟨𝑍, 𝑏⟩)
7	6	breq2d 4898	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑏 → (𝑥 Btwn ⟨𝑍, 𝑦⟩ ↔ 𝑥 Btwn ⟨𝑍, 𝑏⟩))
8	7	rspcv 3506	. . . . . . . . . . 11 ⊢ (𝑏 ∈ 𝐵 → (∀𝑦 ∈ 𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩ → 𝑥 Btwn ⟨𝑍, 𝑏⟩))
9	8	ralimdv 3144	. . . . . . . . . 10 ⊢ (𝑏 ∈ 𝐵 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩ → ∀𝑥 ∈ 𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩))
10	3, 5, 9	3anim123d 1516	. . . . . . . . 9 ⊢ (𝑏 ∈ 𝐵 → ((𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩) → (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)))
11	10	anim2d 605	. . . . . . . 8 ⊢ (𝑏 ∈ 𝐵 → ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → (𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩))))
12		simplr1 1232	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈)) → 𝐴 ⊆ (𝔼‘𝑁))
13	12	adantr 474	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈)) ∧ 𝑝 ∈ 𝐴) → 𝐴 ⊆ (𝔼‘𝑁))
14		simplr2 1234	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈)) ∧ 𝑝 ∈ 𝐴) → 𝑈 ∈ 𝐴)
15	13, 14	sseldd 3821	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈)) ∧ 𝑝 ∈ 𝐴) → 𝑈 ∈ (𝔼‘𝑁))
16		simpr3 1209	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) → ∀𝑥 ∈ 𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)
17		simp2 1128	. . . . . . . . . . . . . . . 16 ⊢ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈) → 𝑈 ∈ 𝐴)
18		breq1 4889	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑈 → (𝑥 Btwn ⟨𝑍, 𝑏⟩ ↔ 𝑈 Btwn ⟨𝑍, 𝑏⟩))
19	18	rspccva 3509	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑥 ∈ 𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑈 ∈ 𝐴) → 𝑈 Btwn ⟨𝑍, 𝑏⟩)
20	16, 17, 19	syl2an 589	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈)) → 𝑈 Btwn ⟨𝑍, 𝑏⟩)
21	20	adantr 474	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈)) ∧ 𝑝 ∈ 𝐴) → 𝑈 Btwn ⟨𝑍, 𝑏⟩)
22	15, 21	jca 507	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈)) ∧ 𝑝 ∈ 𝐴) → (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑈 Btwn ⟨𝑍, 𝑏⟩))
23	12	sselda 3820	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈)) ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ (𝔼‘𝑁))
24	16	adantr 474	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈)) → ∀𝑥 ∈ 𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)
25		breq1 4889	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑝 → (𝑥 Btwn ⟨𝑍, 𝑏⟩ ↔ 𝑝 Btwn ⟨𝑍, 𝑏⟩))
26	25	rspccva 3509	. . . . . . . . . . . . . 14 ⊢ ((∀𝑥 ∈ 𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 ∈ 𝐴) → 𝑝 Btwn ⟨𝑍, 𝑏⟩)
27	24, 26	sylan 575	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈)) ∧ 𝑝 ∈ 𝐴) → 𝑝 Btwn ⟨𝑍, 𝑏⟩)
28	22, 23, 27	jca32 511	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈)) ∧ 𝑝 ∈ 𝐴) → ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑈 Btwn ⟨𝑍, 𝑏⟩) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)))
29		an4 646	. . . . . . . . . . . 12 ⊢ (((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑈 Btwn ⟨𝑍, 𝑏⟩) ∧ (𝑝 ∈ (𝔼‘𝑁) ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)) ↔ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)))
30	28, 29	sylib 210	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈)) ∧ 𝑝 ∈ 𝐴) → ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)))
31		simp2 1128	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩) → 𝑏 ∈ (𝔼‘𝑁))
32		simpl2r 1256	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → 𝑍 ≠ 𝑈)
33	32	adantr 474	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ (𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))))) → 𝑍 ≠ 𝑈)
34		simpl 476	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ (𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))) → (𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))))
35	34	ralimi 3133	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ (𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))))
36		eqcom 2784	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ↔ (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) = (𝑈‘𝑖))
37		oveq2 6930	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑡 = 0 → (1 − 𝑡) = (1 − 0))
38		1m0e1 11503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (1 − 0) = 1
39	37, 38	syl6eq 2829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑡 = 0 → (1 − 𝑡) = 1)
40	39	oveq1d 6937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑡 = 0 → ((1 − 𝑡) · (𝑍‘𝑖)) = (1 · (𝑍‘𝑖)))
41		oveq1 6929	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑡 = 0 → (𝑡 · (𝑏‘𝑖)) = (0 · (𝑏‘𝑖)))
42	40, 41	oveq12d 6940	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑡 = 0 → (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) = ((1 · (𝑍‘𝑖)) + (0 · (𝑏‘𝑖))))
43	42	eqeq1d 2779	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑡 = 0 → ((((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) = (𝑈‘𝑖) ↔ ((1 · (𝑍‘𝑖)) + (0 · (𝑏‘𝑖))) = (𝑈‘𝑖)))
44	36, 43	syl5bb 275	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑡 = 0 → ((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ↔ ((1 · (𝑍‘𝑖)) + (0 · (𝑏‘𝑖))) = (𝑈‘𝑖)))
45	44	ralbidv 3167	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 = 0 → (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((1 · (𝑍‘𝑖)) + (0 · (𝑏‘𝑖))) = (𝑈‘𝑖)))
46	45	biimpac 472	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ 𝑡 = 0) → ∀𝑖 ∈ (1...𝑁)((1 · (𝑍‘𝑖)) + (0 · (𝑏‘𝑖))) = (𝑈‘𝑖))
47		simpl2l 1254	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → 𝑍 ∈ (𝔼‘𝑁))
48		simpl3l 1258	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → 𝑈 ∈ (𝔼‘𝑁))
49		eqeefv 26252	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)))
50	47, 48, 49	syl2anc 579	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)))
51		fveecn 26251	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
52	47, 51	sylan 575	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
53		simp1r 1212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → 𝑏 ∈ (𝔼‘𝑁))
54	53	ad2antrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑏 ∈ (𝔼‘𝑁))
55		fveecn 26251	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑏 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑏‘𝑖) ∈ ℂ)
56	54, 55	sylancom 582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑏‘𝑖) ∈ ℂ)
57		mulid2 10375	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑍‘𝑖) ∈ ℂ → (1 · (𝑍‘𝑖)) = (𝑍‘𝑖))
58		mul02 10554	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑏‘𝑖) ∈ ℂ → (0 · (𝑏‘𝑖)) = 0)
59	57, 58	oveqan12d 6941	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) → ((1 · (𝑍‘𝑖)) + (0 · (𝑏‘𝑖))) = ((𝑍‘𝑖) + 0))
60		addid1 10556	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑍‘𝑖) ∈ ℂ → ((𝑍‘𝑖) + 0) = (𝑍‘𝑖))
61	60	adantr 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) → ((𝑍‘𝑖) + 0) = (𝑍‘𝑖))
62	59, 61	eqtrd 2813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) → ((1 · (𝑍‘𝑖)) + (0 · (𝑏‘𝑖))) = (𝑍‘𝑖))
63	52, 56, 62	syl2anc 579	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 · (𝑍‘𝑖)) + (0 · (𝑏‘𝑖))) = (𝑍‘𝑖))
64	63	eqeq1d 2779	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 · (𝑍‘𝑖)) + (0 · (𝑏‘𝑖))) = (𝑈‘𝑖) ↔ (𝑍‘𝑖) = (𝑈‘𝑖)))
65	64	ralbidva 3166	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)((1 · (𝑍‘𝑖)) + (0 · (𝑏‘𝑖))) = (𝑈‘𝑖) ↔ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)))
66	50, 65	bitr4d 274	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)((1 · (𝑍‘𝑖)) + (0 · (𝑏‘𝑖))) = (𝑈‘𝑖)))
67	46, 66	syl5ibr 238	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → ((∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ 𝑡 = 0) → 𝑍 = 𝑈))
68	67	expdimp 446	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖)))) → (𝑡 = 0 → 𝑍 = 𝑈))
69	35, 68	sylan2 586	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ (𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))))) → (𝑡 = 0 → 𝑍 = 𝑈))
70	69	necon3d 2989	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ (𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))))) → (𝑍 ≠ 𝑈 → 𝑡 ≠ 0))
71	33, 70	mpd 15	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ (𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))))) → 𝑡 ≠ 0)
72		simp1l 1211	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ)
73		simp2l 1213	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → 𝑍 ∈ (𝔼‘𝑁))
74	72, 73, 53	3jca 1119	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)))
75		simp2l 1213	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑡 ∈ (0[,]1))
76		elicc01 12604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑡 ∈ (0[,]1) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ∧ 𝑡 ≤ 1))
77	76	simp1bi 1136	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑡 ∈ (0[,]1) → 𝑡 ∈ ℝ)
78	75, 77	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℝ)
79		simp2r 1214	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑠 ∈ (0[,]1))
80		elicc01 12604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑠 ∈ (0[,]1) ↔ (𝑠 ∈ ℝ ∧ 0 ≤ 𝑠 ∧ 𝑠 ≤ 1))
81	80	simp1bi 1136	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑠 ∈ (0[,]1) → 𝑠 ∈ ℝ)
82	79, 81	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑠 ∈ ℝ)
83	78, 82	letrid 10528	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → (𝑡 ≤ 𝑠 ∨ 𝑠 ≤ 𝑡))
84		simpr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡 ≤ 𝑠) → 𝑡 ≤ 𝑠)
85	78	adantr 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡 ≤ 𝑠) → 𝑡 ∈ ℝ)
86	76	simp2bi 1137	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑡 ∈ (0[,]1) → 0 ≤ 𝑡)
87	75, 86	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 0 ≤ 𝑡)
88	87	adantr 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡 ≤ 𝑠) → 0 ≤ 𝑡)
89	82	adantr 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡 ≤ 𝑠) → 𝑠 ∈ ℝ)
90		0red 10380	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡 ≤ 𝑠) → 0 ∈ ℝ)
91		simp3 1129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑡 ≠ 0)
92	78, 87, 91	ne0gt0d 10513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 0 < 𝑡)
93	92	adantr 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡 ≤ 𝑠) → 0 < 𝑡)
94	90, 85, 89, 93, 84	ltletrd 10536	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡 ≤ 𝑠) → 0 < 𝑠)
95		divelunit 12631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑡 ∈ ℝ ∧ 0 ≤ 𝑡) ∧ (𝑠 ∈ ℝ ∧ 0 < 𝑠)) → ((𝑡 / 𝑠) ∈ (0[,]1) ↔ 𝑡 ≤ 𝑠))
96	85, 88, 89, 94, 95	syl22anc 829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡 ≤ 𝑠) → ((𝑡 / 𝑠) ∈ (0[,]1) ↔ 𝑡 ≤ 𝑠))
97	84, 96	mpbird 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡 ≤ 𝑠) → (𝑡 / 𝑠) ∈ (0[,]1))
98		simp12 1218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑍 ∈ (𝔼‘𝑁))
99	98	ad2antrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡 ≤ 𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
100	99, 51	sylancom 582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡 ≤ 𝑠) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
101		simp13 1219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑏 ∈ (𝔼‘𝑁))
102	101	ad2antrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡 ≤ 𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑏 ∈ (𝔼‘𝑁))
103	102, 55	sylancom 582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡 ≤ 𝑠) ∧ 𝑖 ∈ (1...𝑁)) → (𝑏‘𝑖) ∈ ℂ)
104	77	recnd 10405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑡 ∈ (0[,]1) → 𝑡 ∈ ℂ)
105	75, 104	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℂ)
106	105	ad2antrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡 ≤ 𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
107	81	recnd 10405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑠 ∈ (0[,]1) → 𝑠 ∈ ℂ)
108	79, 107	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 𝑠 ∈ ℂ)
109	108	ad2antrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡 ≤ 𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℂ)
110		0red 10380	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡 ≤ 𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 0 ∈ ℝ)
111	78	ad2antrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡 ≤ 𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℝ)
112	82	ad2antrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡 ≤ 𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℝ)
113	87	ad2antrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡 ≤ 𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 0 ≤ 𝑡)
114		simpll3 1230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡 ≤ 𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ≠ 0)
115	111, 113, 114	ne0gt0d 10513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡 ≤ 𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 0 < 𝑡)
116		simplr 759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡 ≤ 𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ≤ 𝑠)
117	110, 111, 112, 115, 116	ltletrd 10536	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡 ≤ 𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 0 < 𝑠)
118	117	gt0ne0d 10939	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡 ≤ 𝑠) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ≠ 0)
119		divcl 11039	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (𝑡 / 𝑠) ∈ ℂ)
120	119	adantl 475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (𝑡 / 𝑠) ∈ ℂ)
121		ax-1cn 10330	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ 1 ∈ ℂ
122		simpr2 1207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → 𝑠 ∈ ℂ)
123		subcl 10621	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((1 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑠) ∈ ℂ)
124	121, 122, 123	sylancr 581	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (1 − 𝑠) ∈ ℂ)
125		simpll 757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (𝑍‘𝑖) ∈ ℂ)
126	124, 125	mulcld 10397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((1 − 𝑠) · (𝑍‘𝑖)) ∈ ℂ)
127		simplr 759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (𝑏‘𝑖) ∈ ℂ)
128	122, 127	mulcld 10397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (𝑠 · (𝑏‘𝑖)) ∈ ℂ)
129	120, 126, 128	adddid 10401	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))) = (((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖))) + ((𝑡 / 𝑠) · (𝑠 · (𝑏‘𝑖)))))
130	129	oveq2d 6938	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − (𝑡 / 𝑠)) · (𝑍‘𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))))) = (((1 − (𝑡 / 𝑠)) · (𝑍‘𝑖)) + (((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖))) + ((𝑡 / 𝑠) · (𝑠 · (𝑏‘𝑖))))))
131		subcl 10621	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((1 ∈ ℂ ∧ (𝑡 / 𝑠) ∈ ℂ) → (1 − (𝑡 / 𝑠)) ∈ ℂ)
132	121, 120, 131	sylancr 581	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (1 − (𝑡 / 𝑠)) ∈ ℂ)
133	132, 125	mulcld 10397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((1 − (𝑡 / 𝑠)) · (𝑍‘𝑖)) ∈ ℂ)
134	120, 126	mulcld 10397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖))) ∈ ℂ)
135	120, 128	mulcld 10397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · (𝑠 · (𝑏‘𝑖))) ∈ ℂ)
136	133, 134, 135	addassd 10399	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((((1 − (𝑡 / 𝑠)) · (𝑍‘𝑖)) + ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))) + ((𝑡 / 𝑠) · (𝑠 · (𝑏‘𝑖)))) = (((1 − (𝑡 / 𝑠)) · (𝑍‘𝑖)) + (((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖))) + ((𝑡 / 𝑠) · (𝑠 · (𝑏‘𝑖))))))
137	120, 124	mulcld 10397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · (1 − 𝑠)) ∈ ℂ)
138	132, 137, 125	adddird 10402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) · (1 − 𝑠))) · (𝑍‘𝑖)) = (((1 − (𝑡 / 𝑠)) · (𝑍‘𝑖)) + (((𝑡 / 𝑠) · (1 − 𝑠)) · (𝑍‘𝑖))))
139		simp2 1128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → 𝑠 ∈ ℂ)
140		subdi 10808	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((𝑡 / 𝑠) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((𝑡 / 𝑠) · (1 − 𝑠)) = (((𝑡 / 𝑠) · 1) − ((𝑡 / 𝑠) · 𝑠)))
141	121, 140	mp3an2 1522	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑡 / 𝑠) ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((𝑡 / 𝑠) · (1 − 𝑠)) = (((𝑡 / 𝑠) · 1) − ((𝑡 / 𝑠) · 𝑠)))
142	119, 139, 141	syl2anc 579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((𝑡 / 𝑠) · (1 − 𝑠)) = (((𝑡 / 𝑠) · 1) − ((𝑡 / 𝑠) · 𝑠)))
143	119	mulid1d 10394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((𝑡 / 𝑠) · 1) = (𝑡 / 𝑠))
144		divcan1 11042	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((𝑡 / 𝑠) · 𝑠) = 𝑡)
145	143, 144	oveq12d 6940	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((𝑡 / 𝑠) · 1) − ((𝑡 / 𝑠) · 𝑠)) = ((𝑡 / 𝑠) − 𝑡))
146	142, 145	eqtrd 2813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((𝑡 / 𝑠) · (1 − 𝑠)) = ((𝑡 / 𝑠) − 𝑡))
147	146	oveq2d 6938	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) · (1 − 𝑠))) = ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) − 𝑡)))
148		simp1 1127	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → 𝑡 ∈ ℂ)
149		npncan 10644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((1 ∈ ℂ ∧ (𝑡 / 𝑠) ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) − 𝑡)) = (1 − 𝑡))
150	121, 149	mp3an1 1521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝑡 / 𝑠) ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) − 𝑡)) = (1 − 𝑡))
151	119, 148, 150	syl2anc 579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) − 𝑡)) = (1 − 𝑡))
152	147, 151	eqtrd 2813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) · (1 − 𝑠))) = (1 − 𝑡))
153	152	adantl 475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) · (1 − 𝑠))) = (1 − 𝑡))
154	153	oveq1d 6937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − (𝑡 / 𝑠)) + ((𝑡 / 𝑠) · (1 − 𝑠))) · (𝑍‘𝑖)) = ((1 − 𝑡) · (𝑍‘𝑖)))
155	120, 124, 125	mulassd 10400	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((𝑡 / 𝑠) · (1 − 𝑠)) · (𝑍‘𝑖)) = ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖))))
156	155	oveq2d 6938	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − (𝑡 / 𝑠)) · (𝑍‘𝑖)) + (((𝑡 / 𝑠) · (1 − 𝑠)) · (𝑍‘𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍‘𝑖)) + ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))))
157	138, 154, 156	3eqtr3rd 2822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − (𝑡 / 𝑠)) · (𝑍‘𝑖)) + ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))) = ((1 − 𝑡) · (𝑍‘𝑖)))
158	120, 122, 127	mulassd 10400	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((𝑡 / 𝑠) · 𝑠) · (𝑏‘𝑖)) = ((𝑡 / 𝑠) · (𝑠 · (𝑏‘𝑖))))
159	144	adantl 475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · 𝑠) = 𝑡)
160	159	oveq1d 6937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((𝑡 / 𝑠) · 𝑠) · (𝑏‘𝑖)) = (𝑡 · (𝑏‘𝑖)))
161	158, 160	eqtr3d 2815	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((𝑡 / 𝑠) · (𝑠 · (𝑏‘𝑖))) = (𝑡 · (𝑏‘𝑖)))
162	157, 161	oveq12d 6940	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → ((((1 − (𝑡 / 𝑠)) · (𝑍‘𝑖)) + ((𝑡 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))) + ((𝑡 / 𝑠) · (𝑠 · (𝑏‘𝑖)))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))))
163	130, 136, 162	3eqtr2rd 2820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0)) → (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍‘𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))))))
164	100, 103, 106, 109, 118, 163	syl23anc 1445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡 ≤ 𝑠) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍‘𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))))))
165	164	ralrimiva 3147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡 ≤ 𝑠) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍‘𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))))))
166		oveq2 6930	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑟 = (𝑡 / 𝑠) → (1 − 𝑟) = (1 − (𝑡 / 𝑠)))
167	166	oveq1d 6937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑟 = (𝑡 / 𝑠) → ((1 − 𝑟) · (𝑍‘𝑖)) = ((1 − (𝑡 / 𝑠)) · (𝑍‘𝑖)))
168		oveq1 6929	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑟 = (𝑡 / 𝑠) → (𝑟 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))) = ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))))
169	167, 168	oveq12d 6940	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑟 = (𝑡 / 𝑠) → (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))))) = (((1 − (𝑡 / 𝑠)) · (𝑍‘𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))))))
170	169	eqeq2d 2787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑟 = (𝑡 / 𝑠) → ((((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))))) ↔ (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍‘𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))))))
171	170	ralbidv 3167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑟 = (𝑡 / 𝑠) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍‘𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))))))
172	171	rspcev 3510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑡 / 𝑠) ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) = (((1 − (𝑡 / 𝑠)) · (𝑍‘𝑖)) + ((𝑡 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))))) → ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))))))
173	97, 165, 172	syl2anc 579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑡 ≤ 𝑠) → ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))))))
174	173	ex 403	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → (𝑡 ≤ 𝑠 → ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))))))
175	80	simp2bi 1137	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑠 ∈ (0[,]1) → 0 ≤ 𝑠)
176	79, 175	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → 0 ≤ 𝑠)
177		divelunit 12631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑠 ∈ ℝ ∧ 0 ≤ 𝑠) ∧ (𝑡 ∈ ℝ ∧ 0 < 𝑡)) → ((𝑠 / 𝑡) ∈ (0[,]1) ↔ 𝑠 ≤ 𝑡))
178	82, 176, 78, 92, 177	syl22anc 829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → ((𝑠 / 𝑡) ∈ (0[,]1) ↔ 𝑠 ≤ 𝑡))
179	178	biimpar 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠 ≤ 𝑡) → (𝑠 / 𝑡) ∈ (0[,]1))
180		simp112 1359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠 ≤ 𝑡 ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
181		simp3 1129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠 ≤ 𝑡 ∧ 𝑖 ∈ (1...𝑁)) → 𝑖 ∈ (1...𝑁))
182	180, 181, 51	syl2anc 579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠 ≤ 𝑡 ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
183		simp113 1360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠 ≤ 𝑡 ∧ 𝑖 ∈ (1...𝑁)) → 𝑏 ∈ (𝔼‘𝑁))
184	183, 181, 55	syl2anc 579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠 ≤ 𝑡 ∧ 𝑖 ∈ (1...𝑁)) → (𝑏‘𝑖) ∈ ℂ)
185		simp12r 1343	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠 ≤ 𝑡 ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ (0[,]1))
186	185, 107	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠 ≤ 𝑡 ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℂ)
187		simp12l 1342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠 ≤ 𝑡 ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ (0[,]1))
188	187, 104	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠 ≤ 𝑡 ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
189		simp13 1219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠 ≤ 𝑡 ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ≠ 0)
190		divcl 11039	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (𝑠 / 𝑡) ∈ ℂ)
191	190	adantl 475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (𝑠 / 𝑡) ∈ ℂ)
192		simpr2 1207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → 𝑡 ∈ ℂ)
193		subcl 10621	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((1 ∈ ℂ ∧ 𝑡 ∈ ℂ) → (1 − 𝑡) ∈ ℂ)
194	121, 192, 193	sylancr 581	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (1 − 𝑡) ∈ ℂ)
195		simpll 757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (𝑍‘𝑖) ∈ ℂ)
196	194, 195	mulcld 10397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((1 − 𝑡) · (𝑍‘𝑖)) ∈ ℂ)
197		simplr 759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (𝑏‘𝑖) ∈ ℂ)
198	192, 197	mulcld 10397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (𝑡 · (𝑏‘𝑖)) ∈ ℂ)
199	191, 196, 198	adddid 10401	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖)))) = (((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖))) + ((𝑠 / 𝑡) · (𝑡 · (𝑏‘𝑖)))))
200	199	oveq2d 6938	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((1 − (𝑠 / 𝑡)) · (𝑍‘𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))))) = (((1 − (𝑠 / 𝑡)) · (𝑍‘𝑖)) + (((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖))) + ((𝑠 / 𝑡) · (𝑡 · (𝑏‘𝑖))))))
201		subcl 10621	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((1 ∈ ℂ ∧ (𝑠 / 𝑡) ∈ ℂ) → (1 − (𝑠 / 𝑡)) ∈ ℂ)
202	121, 191, 201	sylancr 581	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (1 − (𝑠 / 𝑡)) ∈ ℂ)
203	202, 195	mulcld 10397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((1 − (𝑠 / 𝑡)) · (𝑍‘𝑖)) ∈ ℂ)
204	191, 196	mulcld 10397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖))) ∈ ℂ)
205	191, 198	mulcld 10397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((𝑠 / 𝑡) · (𝑡 · (𝑏‘𝑖))) ∈ ℂ)
206	203, 204, 205	addassd 10399	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((((1 − (𝑠 / 𝑡)) · (𝑍‘𝑖)) + ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖)))) + ((𝑠 / 𝑡) · (𝑡 · (𝑏‘𝑖)))) = (((1 − (𝑠 / 𝑡)) · (𝑍‘𝑖)) + (((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖))) + ((𝑠 / 𝑡) · (𝑡 · (𝑏‘𝑖))))))
207		simp2 1128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → 𝑡 ∈ ℂ)
208		subdi 10808	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (((𝑠 / 𝑡) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((𝑠 / 𝑡) · (1 − 𝑡)) = (((𝑠 / 𝑡) · 1) − ((𝑠 / 𝑡) · 𝑡)))
209	121, 208	mp3an2 1522	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((𝑠 / 𝑡) ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((𝑠 / 𝑡) · (1 − 𝑡)) = (((𝑠 / 𝑡) · 1) − ((𝑠 / 𝑡) · 𝑡)))
210	190, 207, 209	syl2anc 579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((𝑠 / 𝑡) · (1 − 𝑡)) = (((𝑠 / 𝑡) · 1) − ((𝑠 / 𝑡) · 𝑡)))
211	190	mulid1d 10394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((𝑠 / 𝑡) · 1) = (𝑠 / 𝑡))
212		divcan1 11042	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((𝑠 / 𝑡) · 𝑡) = 𝑠)
213	211, 212	oveq12d 6940	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (((𝑠 / 𝑡) · 1) − ((𝑠 / 𝑡) · 𝑡)) = ((𝑠 / 𝑡) − 𝑠))
214	210, 213	eqtrd 2813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((𝑠 / 𝑡) · (1 − 𝑡)) = ((𝑠 / 𝑡) − 𝑠))
215	214	oveq2d 6938	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) · (1 − 𝑡))) = ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) − 𝑠)))
216		simp1 1127	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → 𝑠 ∈ ℂ)
217		npncan 10644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((1 ∈ ℂ ∧ (𝑠 / 𝑡) ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) − 𝑠)) = (1 − 𝑠))
218	121, 217	mp3an1 1521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝑠 / 𝑡) ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) − 𝑠)) = (1 − 𝑠))
219	190, 216, 218	syl2anc 579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) − 𝑠)) = (1 − 𝑠))
220	215, 219	eqtr2d 2814	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 − 𝑠) = ((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) · (1 − 𝑡))))
221	220	oveq1d 6937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − 𝑠) · (𝑍‘𝑖)) = (((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) · (1 − 𝑡))) · (𝑍‘𝑖)))
222	221	adantl 475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((1 − 𝑠) · (𝑍‘𝑖)) = (((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) · (1 − 𝑡))) · (𝑍‘𝑖)))
223	191, 194	mulcld 10397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((𝑠 / 𝑡) · (1 − 𝑡)) ∈ ℂ)
224	202, 223, 195	adddird 10402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((1 − (𝑠 / 𝑡)) + ((𝑠 / 𝑡) · (1 − 𝑡))) · (𝑍‘𝑖)) = (((1 − (𝑠 / 𝑡)) · (𝑍‘𝑖)) + (((𝑠 / 𝑡) · (1 − 𝑡)) · (𝑍‘𝑖))))
225	191, 194, 195	mulassd 10400	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((𝑠 / 𝑡) · (1 − 𝑡)) · (𝑍‘𝑖)) = ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖))))
226	225	oveq2d 6938	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((1 − (𝑠 / 𝑡)) · (𝑍‘𝑖)) + (((𝑠 / 𝑡) · (1 − 𝑡)) · (𝑍‘𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍‘𝑖)) + ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖)))))
227	222, 224, 226	3eqtrrd 2818	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((1 − (𝑠 / 𝑡)) · (𝑍‘𝑖)) + ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖)))) = ((1 − 𝑠) · (𝑍‘𝑖)))
228	191, 192, 197	mulassd 10400	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((𝑠 / 𝑡) · 𝑡) · (𝑏‘𝑖)) = ((𝑠 / 𝑡) · (𝑡 · (𝑏‘𝑖))))
229	212	oveq1d 6937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (((𝑠 / 𝑡) · 𝑡) · (𝑏‘𝑖)) = (𝑠 · (𝑏‘𝑖)))
230	229	adantl 475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((𝑠 / 𝑡) · 𝑡) · (𝑏‘𝑖)) = (𝑠 · (𝑏‘𝑖)))
231	228, 230	eqtr3d 2815	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((𝑠 / 𝑡) · (𝑡 · (𝑏‘𝑖))) = (𝑠 · (𝑏‘𝑖)))
232	227, 231	oveq12d 6940	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → ((((1 − (𝑠 / 𝑡)) · (𝑍‘𝑖)) + ((𝑠 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖)))) + ((𝑠 / 𝑡) · (𝑡 · (𝑏‘𝑖)))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))))
233	200, 206, 232	3eqtr2rd 2820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑏‘𝑖) ∈ ℂ) ∧ (𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) → (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍‘𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))))))
234	182, 184, 186, 188, 189, 233	syl23anc 1445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠 ≤ 𝑡 ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍‘𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))))))
235	234	3expa 1108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍‘𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))))))
236	235	ralrimiva 3147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠 ≤ 𝑡) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍‘𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))))))
237		oveq2 6930	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑟 = (𝑠 / 𝑡) → (1 − 𝑟) = (1 − (𝑠 / 𝑡)))
238	237	oveq1d 6937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑟 = (𝑠 / 𝑡) → ((1 − 𝑟) · (𝑍‘𝑖)) = ((1 − (𝑠 / 𝑡)) · (𝑍‘𝑖)))
239		oveq1 6929	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑟 = (𝑠 / 𝑡) → (𝑟 · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖)))) = ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖)))))
240	238, 239	oveq12d 6940	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑟 = (𝑠 / 𝑡) → (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))))) = (((1 − (𝑠 / 𝑡)) · (𝑍‘𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))))))
241	240	eqeq2d 2787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑟 = (𝑠 / 𝑡) → ((((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))))) ↔ (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍‘𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖)))))))
242	241	ralbidv 3167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑟 = (𝑠 / 𝑡) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍‘𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖)))))))
243	242	rspcev 3510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑠 / 𝑡) ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))) = (((1 − (𝑠 / 𝑡)) · (𝑍‘𝑖)) + ((𝑠 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖)))))) → ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))))))
244	179, 236, 243	syl2anc 579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) ∧ 𝑠 ≤ 𝑡) → ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))))))
245	244	ex 403	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → (𝑠 ≤ 𝑡 → ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖)))))))
246	174, 245	orim12d 950	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → ((𝑡 ≤ 𝑠 ∨ 𝑠 ≤ 𝑡) → (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))))) ∨ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))))))))
247		r19.43 3278	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))))) ∨ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖)))))) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))))) ∨ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖)))))))
248	246, 247	syl6ibr 244	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → ((𝑡 ≤ 𝑠 ∨ 𝑠 ≤ 𝑡) → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))))) ∨ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))))))))
249	83, 248	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))))) ∨ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖)))))))
250		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) → (𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))))
251		oveq2 6930	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))) → (𝑟 · (𝑝‘𝑖)) = (𝑟 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))))
252	251	oveq2d 6938	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))) → (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑝‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))))))
253	250, 252	eqeqan12d 2793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ (𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))) → ((𝑈‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑝‘𝑖))) ↔ (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))))))
254	253	ralimi 3133	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ (𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)((𝑈‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑝‘𝑖))) ↔ (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))))))
255		ralbi 3253	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑈‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑝‘𝑖))) ↔ (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))))) → (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑝‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))))))
256	254, 255	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ (𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))) → (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑝‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))))))
257		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))) → (𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))))
258		oveq2 6930	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) → (𝑟 · (𝑈‘𝑖)) = (𝑟 · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖)))))
259	258	oveq2d 6938	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) → (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑈‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))))))
260	257, 259	eqeqan12rd 2795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ (𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))) → ((𝑝‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑈‘𝑖))) ↔ (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖)))))))
261	260	ralimi 3133	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ (𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)((𝑝‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑈‘𝑖))) ↔ (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖)))))))
262		ralbi 3253	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑝‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑈‘𝑖))) ↔ (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖)))))) → (∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖)))))))
263	261, 262	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ (𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))) → (∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖)))))))
264	256, 263	orbi12d 905	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ (𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))) → ((∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑝‘𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑈‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))))) ∨ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))))))))
265	264	rexbidv 3236	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ (𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))) → (∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑝‘𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑈‘𝑖)))) ↔ ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))))) ∨ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))))))))
266	249, 265	syl5ibrcom 239	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑡 ≠ 0) → (∀𝑖 ∈ (1...𝑁)((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ (𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))) → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑝‘𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑈‘𝑖))))))
267	266	3expia 1111	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (𝑡 ≠ 0 → (∀𝑖 ∈ (1...𝑁)((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ (𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))) → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑝‘𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑈‘𝑖)))))))
268	267	com23 86	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ (𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))) → (𝑡 ≠ 0 → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑝‘𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑈‘𝑖)))))))
269	74, 268	sylan 575	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ (𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))) → (𝑡 ≠ 0 → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑝‘𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑈‘𝑖)))))))
270	269	imp 397	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ (𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))))) → (𝑡 ≠ 0 → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑝‘𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑈‘𝑖))))))
271	71, 270	mpd 15	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ (𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))))) → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑝‘𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑈‘𝑖)))))
272	271	ex 403	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ (𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))) → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑝‘𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑈‘𝑖))))))
273	272	rexlimdvva 3220	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ (𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))) → ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑝‘𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑈‘𝑖))))))
274		simp3l 1215	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → 𝑈 ∈ (𝔼‘𝑁))
275		brbtwn 26248	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, 𝑏⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖)))))
276	274, 73, 53, 275	syl3anc 1439	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (𝑈 Btwn ⟨𝑍, 𝑏⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖)))))
277		simp3r 1216	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → 𝑝 ∈ (𝔼‘𝑁))
278		brbtwn 26248	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑝 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁)) → (𝑝 Btwn ⟨𝑍, 𝑏⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))))
279	277, 73, 53, 278	syl3anc 1439	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (𝑝 Btwn ⟨𝑍, 𝑏⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))))
280	276, 279	anbi12d 624	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → ((𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩) ↔ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))))))
281		r19.26 3249	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ (𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))))
282	281	2rexbii 3224	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ (𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))) ↔ ∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))))
283		reeanv 3292	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))) ↔ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))))
284	282, 283	bitri 267	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ (𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))) ↔ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖)))))
285	280, 284	syl6bbr 281	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → ((𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩) ↔ ∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑈‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑏‘𝑖))) ∧ (𝑝‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑏‘𝑖))))))
286		brbtwn 26248	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑝‘𝑖)))))
287	274, 73, 277, 286	syl3anc 1439	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑝‘𝑖)))))
288		brbtwn 26248	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑝 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑝 Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑈‘𝑖)))))
289	277, 73, 274, 288	syl3anc 1439	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → (𝑝 Btwn ⟨𝑍, 𝑈⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑈‘𝑖)))))
290	287, 289	orbi12d 905	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → ((𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑝‘𝑖))) ∨ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑈‘𝑖))))))
291		r19.43 3278	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑝‘𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑈‘𝑖)))) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑝‘𝑖))) ∨ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑈‘𝑖)))))
292	290, 291	syl6bbr 281	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → ((𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩) ↔ ∃𝑟 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑝‘𝑖))) ∨ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑟) · (𝑍‘𝑖)) + (𝑟 · (𝑈‘𝑖))))))
293	273, 285, 292	3imtr4d 286	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈) ∧ (𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁))) → ((𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
294	293	3expia 1111	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈)) → ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) → ((𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))
295	294	impd 400	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈)) → (((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
296	31, 295	sylanl2 671	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑍 ≠ 𝑈)) → (((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
297	296	3adantr2 1172	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈)) → (((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
298	297	adantr 474	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈)) ∧ 𝑝 ∈ 𝐴) → (((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn ⟨𝑍, 𝑏⟩ ∧ 𝑝 Btwn ⟨𝑍, 𝑏⟩)) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
299	30, 298	mpd 15	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈)) ∧ 𝑝 ∈ 𝐴) → (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))
300	299	ralrimiva 3147	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) ∧ (𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈)) → ∀𝑝 ∈ 𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))
301	300	3exp2 1416	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 𝑥 Btwn ⟨𝑍, 𝑏⟩)) → (𝑍 ∈ (𝔼‘𝑁) → (𝑈 ∈ 𝐴 → (𝑍 ≠ 𝑈 → ∀𝑝 ∈ 𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))))
302	11, 301	syl6 35	. . . . . . 7 ⊢ (𝑏 ∈ 𝐵 → ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → (𝑍 ∈ (𝔼‘𝑁) → (𝑈 ∈ 𝐴 → (𝑍 ≠ 𝑈 → ∀𝑝 ∈ 𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))))
303	302	exlimiv 1973	. . . . . 6 ⊢ (∃𝑏 𝑏 ∈ 𝐵 → ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → (𝑍 ∈ (𝔼‘𝑁) → (𝑈 ∈ 𝐴 → (𝑍 ≠ 𝑈 → ∀𝑝 ∈ 𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))))
304	2, 303	sylbi 209	. . . . 5 ⊢ (𝐵 ≠ ∅ → ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → (𝑍 ∈ (𝔼‘𝑁) → (𝑈 ∈ 𝐴 → (𝑍 ≠ 𝑈 → ∀𝑝 ∈ 𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))))
305	304	com4l 92	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → (𝑍 ∈ (𝔼‘𝑁) → (𝑈 ∈ 𝐴 → (𝐵 ≠ ∅ → (𝑍 ≠ 𝑈 → ∀𝑝 ∈ 𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))))
306	305	3impd 1410	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) → ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅) → (𝑍 ≠ 𝑈 → ∀𝑝 ∈ 𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))))
307	306	imp32 411	. 2 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) ∧ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅) ∧ 𝑍 ≠ 𝑈)) → ∀𝑝 ∈ 𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩))
308		axcontlem4.1	. . . 4 ⊢ 𝐷 = {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)}
309	308	sseq2i 3848	. . 3 ⊢ (𝐴 ⊆ 𝐷 ↔ 𝐴 ⊆ {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)})
310		ssrab 3900	. . 3 ⊢ (𝐴 ⊆ {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)} ↔ (𝐴 ⊆ (𝔼‘𝑁) ∧ ∀𝑝 ∈ 𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
311	309, 310	bitri 267	. 2 ⊢ (𝐴 ⊆ 𝐷 ↔ (𝐴 ⊆ (𝔼‘𝑁) ∧ ∀𝑝 ∈ 𝐴 (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)))
312	1, 307, 311	sylanbrc 578	1 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ⊆ (𝔼‘𝑁) ∧ 𝐵 ⊆ (𝔼‘𝑁) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 Btwn ⟨𝑍, 𝑦⟩)) ∧ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅) ∧ 𝑍 ≠ 𝑈)) → 𝐴 ⊆ 𝐷)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 ∨ wo 836 ∧ w3a 1071 = wceq 1601 ∃wex 1823 ∈ wcel 2106 ≠ wne 2968 ∀wral 3089 ∃wrex 3090 {crab 3093 ⊆ wss 3791 ∅c0 4140 ⟨cop 4403 class class class wbr 4886 ‘cfv 6135 (class class class)co 6922 ℂcc 10270 ℝcr 10271 0cc0 10272 1c1 10273 + caddc 10275 · cmul 10277 < clt 10411 ≤ cle 10412 − cmin 10606 / cdiv 11032 ℕ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-rmo 3097 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-div 11033 df-nn 11375 df-z 11729 df-uz 11993 df-icc 12494 df-fz 12644 df-ee 26240 df-btwn 26241

This theorem is referenced by: axcontlem9 26321 axcontlem10 26322

W3C validator