axcontlem7 - Metamath Proof Explorer

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

Theorem axcontlem7 25650

Description: Lemma for axcont 25656. Given two points in 𝐷, one preceeds the other iff its scaling constant is less than the other point's. (Contributed by Scott Fenton, 18-Jun-2013.)

**Hypotheses**
Ref	Expression
axcontlem7.1	⊢ 𝐷 = {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)}
axcontlem7.2	⊢ 𝐹 = {⟨𝑥, 𝑡⟩ ∣ (𝑥 ∈ 𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))}

**Assertion**
Ref	Expression
axcontlem7	⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷)) → (𝑃 Btwn ⟨𝑍, 𝑄⟩ ↔ (𝐹‘𝑃) ≤ (𝐹‘𝑄)))

Distinct variable groups: 𝑡,𝐷,𝑥 𝑖,𝐹,𝑡 𝑖,𝑝,𝑥,𝑁,𝑡 𝑃,𝑖,𝑡,𝑥 𝑄,𝑖,𝑡,𝑥 𝑈,𝑖,𝑝,𝑡,𝑥 𝑖,𝑍,𝑝,𝑡,𝑥 Allowed substitution hints: 𝐷(𝑖,𝑝) 𝑃(𝑝) 𝑄(𝑝) 𝐹(𝑥,𝑝)

**Proof of Theorem axcontlem7**
Step	Hyp	Ref	Expression
1		axcontlem7.1	. . . . . 6 ⊢ 𝐷 = {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)}
2		ssrab2 3650	. . . . . 6 ⊢ {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)} ⊆ (𝔼‘𝑁)
3	1, 2	eqsstri 3598	. . . . 5 ⊢ 𝐷 ⊆ (𝔼‘𝑁)
4	3	sseli 3564	. . . 4 ⊢ (𝑃 ∈ 𝐷 → 𝑃 ∈ (𝔼‘𝑁))
5	4	ad2antrl 760	. . 3 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷)) → 𝑃 ∈ (𝔼‘𝑁))
6		simpll2 1094	. . 3 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷)) → 𝑍 ∈ (𝔼‘𝑁))
7	3	sseli 3564	. . . 4 ⊢ (𝑄 ∈ 𝐷 → 𝑄 ∈ (𝔼‘𝑁))
8	7	ad2antll 761	. . 3 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷)) → 𝑄 ∈ (𝔼‘𝑁))
9		brbtwn 25579	. . 3 ⊢ ((𝑃 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁)) → (𝑃 Btwn ⟨𝑍, 𝑄⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑄‘𝑖)))))
10	5, 6, 8, 9	syl3anc 1318	. 2 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷)) → (𝑃 Btwn ⟨𝑍, 𝑄⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑄‘𝑖)))))
11		axcontlem7.2	. . . . 5 ⊢ 𝐹 = {⟨𝑥, 𝑡⟩ ∣ (𝑥 ∈ 𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))}
12	1, 11	axcontlem6 25649	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑃 ∈ 𝐷) → ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))))
13	1, 11	axcontlem6 25649	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑄 ∈ 𝐷) → ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))))
14	12, 13	anim12dan 878	. . 3 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷)) → (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))))))
15		an4 861	. . . . 5 ⊢ ((((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))))) ↔ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ (∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))))))
16		r19.26 3046	. . . . . 6 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))))
17	16	anbi2i 726	. . . . 5 ⊢ ((((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ ∀𝑖 ∈ (1...𝑁)((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))))) ↔ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ (∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))))))
18	15, 17	bitr4i 266	. . . 4 ⊢ ((((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))))) ↔ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ ∀𝑖 ∈ (1...𝑁)((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))))))
19		id 22	. . . . . . . . . 10 ⊢ ((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) → (𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))
20		oveq2 6557	. . . . . . . . . . 11 ⊢ ((𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) → (𝑡 · (𝑄‘𝑖)) = (𝑡 · (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))))
21	20	oveq2d 6565	. . . . . . . . . 10 ⊢ ((𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) → (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑄‘𝑖))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))))))
22	19, 21	eqeqan12d 2626	. . . . . . . . 9 ⊢ (((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))) → ((𝑃‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑄‘𝑖))) ↔ (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))))))
23	22	ralimi 2936	. . . . . . . 8 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)((𝑃‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑄‘𝑖))) ↔ (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))))))
24		ralbi 3050	. . . . . . . 8 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑃‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑄‘𝑖))) ↔ (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))))) → (∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑄‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))))))
25	23, 24	syl 17	. . . . . . 7 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))) → (∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑄‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))))))
26	25	rexbidv 3034	. . . . . 6 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑄‘𝑖))) ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))))))
27		simpll2 1094	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → 𝑍 ∈ (𝔼‘𝑁))
28		fveecn 25582	. . . . . . . . . . . . 13 ⊢ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
29	27, 28	sylan 487	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
30		simpll3 1095	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → 𝑈 ∈ (𝔼‘𝑁))
31		fveecn 25582	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) ∈ ℂ)
32	30, 31	sylan 487	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) ∈ ℂ)
33		0re 9919	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ ℝ
34		1re 9918	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ
35	33, 34	elicc2i 12110	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ (0[,]1) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ∧ 𝑡 ≤ 1))
36	35	simp1bi 1069	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ (0[,]1) → 𝑡 ∈ ℝ)
37	36	recnd 9947	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ (0[,]1) → 𝑡 ∈ ℂ)
38	37	ad2antll 761	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → 𝑡 ∈ ℂ)
39	38	adantr 480	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
40		elrege0 12149	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑃) ∈ (0[,)+∞) ↔ ((𝐹‘𝑃) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑃)))
41	40	simplbi 475	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑃) ∈ (0[,)+∞) → (𝐹‘𝑃) ∈ ℝ)
42	41	recnd 9947	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑃) ∈ (0[,)+∞) → (𝐹‘𝑃) ∈ ℂ)
43	42	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) → (𝐹‘𝑃) ∈ ℂ)
44	43	ad2antrl 760	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → (𝐹‘𝑃) ∈ ℂ)
45	44	adantr 480	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) ∈ ℂ)
46		elrege0 12149	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑄) ∈ (0[,)+∞) ↔ ((𝐹‘𝑄) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑄)))
47	46	simplbi 475	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑄) ∈ (0[,)+∞) → (𝐹‘𝑄) ∈ ℝ)
48	47	recnd 9947	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑄) ∈ (0[,)+∞) → (𝐹‘𝑄) ∈ ℂ)
49	48	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) → (𝐹‘𝑄) ∈ ℂ)
50	49	ad2antrl 760	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → (𝐹‘𝑄) ∈ ℂ)
51	50	adantr 480	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑄) ∈ ℂ)
52		ax-1cn 9873	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℂ
53		simpr1 1060	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → 𝑡 ∈ ℂ)
54		simpr3 1062	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → (𝐹‘𝑄) ∈ ℂ)
55	53, 54	mulcld 9939	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → (𝑡 · (𝐹‘𝑄)) ∈ ℂ)
56		subcl 10159	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℂ ∧ (𝑡 · (𝐹‘𝑄)) ∈ ℂ) → (1 − (𝑡 · (𝐹‘𝑄))) ∈ ℂ)
57	52, 55, 56	sylancr 694	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → (1 − (𝑡 · (𝐹‘𝑄))) ∈ ℂ)
58		subcl 10159	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ) → (1 − (𝐹‘𝑃)) ∈ ℂ)
59	52, 58	mpan 702	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑃) ∈ ℂ → (1 − (𝐹‘𝑃)) ∈ ℂ)
60	59	3ad2ant2 1076	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ) → (1 − (𝐹‘𝑃)) ∈ ℂ)
61	60	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → (1 − (𝐹‘𝑃)) ∈ ℂ)
62		simpll 786	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → (𝑍‘𝑖) ∈ ℂ)
63	57, 61, 62	subdird 10366	. . . . . . . . . . . . . . 15 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → (((1 − (𝑡 · (𝐹‘𝑄))) − (1 − (𝐹‘𝑃))) · (𝑍‘𝑖)) = (((1 − (𝑡 · (𝐹‘𝑄))) · (𝑍‘𝑖)) − ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))))
64		simpr2 1061	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → (𝐹‘𝑃) ∈ ℂ)
65		nnncan1 10196	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℂ ∧ (𝑡 · (𝐹‘𝑄)) ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ) → ((1 − (𝑡 · (𝐹‘𝑄))) − (1 − (𝐹‘𝑃))) = ((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))))
66	52, 65	mp3an1 1403	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 · (𝐹‘𝑄)) ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ) → ((1 − (𝑡 · (𝐹‘𝑄))) − (1 − (𝐹‘𝑃))) = ((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))))
67	55, 64, 66	syl2anc 691	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → ((1 − (𝑡 · (𝐹‘𝑄))) − (1 − (𝐹‘𝑃))) = ((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))))
68	67	oveq1d 6564	. . . . . . . . . . . . . . 15 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → (((1 − (𝑡 · (𝐹‘𝑄))) − (1 − (𝐹‘𝑃))) · (𝑍‘𝑖)) = (((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) · (𝑍‘𝑖)))
69		subdi 10342	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ) → (𝑡 · (1 − (𝐹‘𝑄))) = ((𝑡 · 1) − (𝑡 · (𝐹‘𝑄))))
70	52, 69	mp3an2 1404	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ) → (𝑡 · (1 − (𝐹‘𝑄))) = ((𝑡 · 1) − (𝑡 · (𝐹‘𝑄))))
71		mulid1 9916	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 ∈ ℂ → (𝑡 · 1) = 𝑡)
72	71	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ) → (𝑡 · 1) = 𝑡)
73	72	oveq1d 6564	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ) → ((𝑡 · 1) − (𝑡 · (𝐹‘𝑄))) = (𝑡 − (𝑡 · (𝐹‘𝑄))))
74	70, 73	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ) → (𝑡 · (1 − (𝐹‘𝑄))) = (𝑡 − (𝑡 · (𝐹‘𝑄))))
75	53, 54, 74	syl2anc 691	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → (𝑡 · (1 − (𝐹‘𝑄))) = (𝑡 − (𝑡 · (𝐹‘𝑄))))
76	75	oveq2d 6565	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → ((1 − 𝑡) + (𝑡 · (1 − (𝐹‘𝑄)))) = ((1 − 𝑡) + (𝑡 − (𝑡 · (𝐹‘𝑄)))))
77		npncan 10181	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ (𝑡 · (𝐹‘𝑄)) ∈ ℂ) → ((1 − 𝑡) + (𝑡 − (𝑡 · (𝐹‘𝑄)))) = (1 − (𝑡 · (𝐹‘𝑄))))
78	52, 77	mp3an1 1403	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℂ ∧ (𝑡 · (𝐹‘𝑄)) ∈ ℂ) → ((1 − 𝑡) + (𝑡 − (𝑡 · (𝐹‘𝑄)))) = (1 − (𝑡 · (𝐹‘𝑄))))
79	53, 55, 78	syl2anc 691	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → ((1 − 𝑡) + (𝑡 − (𝑡 · (𝐹‘𝑄)))) = (1 − (𝑡 · (𝐹‘𝑄))))
80	76, 79	eqtr2d 2645	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → (1 − (𝑡 · (𝐹‘𝑄))) = ((1 − 𝑡) + (𝑡 · (1 − (𝐹‘𝑄)))))
81	80	oveq1d 6564	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → ((1 − (𝑡 · (𝐹‘𝑄))) · (𝑍‘𝑖)) = (((1 − 𝑡) + (𝑡 · (1 − (𝐹‘𝑄)))) · (𝑍‘𝑖)))
82		subcl 10159	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ∈ ℂ ∧ 𝑡 ∈ ℂ) → (1 − 𝑡) ∈ ℂ)
83	52, 82	mpan 702	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ ℂ → (1 − 𝑡) ∈ ℂ)
84	83	3ad2ant1 1075	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ) → (1 − 𝑡) ∈ ℂ)
85	84	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → (1 − 𝑡) ∈ ℂ)
86		subcl 10159	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ) → (1 − (𝐹‘𝑄)) ∈ ℂ)
87	52, 86	mpan 702	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑄) ∈ ℂ → (1 − (𝐹‘𝑄)) ∈ ℂ)
88	87	3ad2ant3 1077	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ) → (1 − (𝐹‘𝑄)) ∈ ℂ)
89	88	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → (1 − (𝐹‘𝑄)) ∈ ℂ)
90	53, 89	mulcld 9939	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → (𝑡 · (1 − (𝐹‘𝑄))) ∈ ℂ)
91	85, 90, 62	adddird 9944	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → (((1 − 𝑡) + (𝑡 · (1 − (𝐹‘𝑄)))) · (𝑍‘𝑖)) = (((1 − 𝑡) · (𝑍‘𝑖)) + ((𝑡 · (1 − (𝐹‘𝑄))) · (𝑍‘𝑖))))
92	53, 89, 62	mulassd 9942	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → ((𝑡 · (1 − (𝐹‘𝑄))) · (𝑍‘𝑖)) = (𝑡 · ((1 − (𝐹‘𝑄)) · (𝑍‘𝑖))))
93	92	oveq2d 6565	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → (((1 − 𝑡) · (𝑍‘𝑖)) + ((𝑡 · (1 − (𝐹‘𝑄))) · (𝑍‘𝑖))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · ((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)))))
94	81, 91, 93	3eqtrd 2648	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → ((1 − (𝑡 · (𝐹‘𝑄))) · (𝑍‘𝑖)) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · ((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)))))
95	94	oveq1d 6564	. . . . . . . . . . . . . . 15 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → (((1 − (𝑡 · (𝐹‘𝑄))) · (𝑍‘𝑖)) − ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) = ((((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · ((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)))) − ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))))
96	63, 68, 95	3eqtr3d 2652	. . . . . . . . . . . . . 14 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → (((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) · (𝑍‘𝑖)) = ((((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · ((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)))) − ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))))
97		simplr 788	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → (𝑈‘𝑖) ∈ ℂ)
98	64, 55, 97	subdird 10366	. . . . . . . . . . . . . . 15 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → (((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) · (𝑈‘𝑖)) = (((𝐹‘𝑃) · (𝑈‘𝑖)) − ((𝑡 · (𝐹‘𝑄)) · (𝑈‘𝑖))))
99	53, 54, 97	mulassd 9942	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → ((𝑡 · (𝐹‘𝑄)) · (𝑈‘𝑖)) = (𝑡 · ((𝐹‘𝑄) · (𝑈‘𝑖))))
100	99	oveq2d 6565	. . . . . . . . . . . . . . 15 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → (((𝐹‘𝑃) · (𝑈‘𝑖)) − ((𝑡 · (𝐹‘𝑄)) · (𝑈‘𝑖))) = (((𝐹‘𝑃) · (𝑈‘𝑖)) − (𝑡 · ((𝐹‘𝑄) · (𝑈‘𝑖)))))
101	98, 100	eqtrd 2644	. . . . . . . . . . . . . 14 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → (((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) · (𝑈‘𝑖)) = (((𝐹‘𝑃) · (𝑈‘𝑖)) − (𝑡 · ((𝐹‘𝑄) · (𝑈‘𝑖)))))
102	96, 101	eqeq12d 2625	. . . . . . . . . . . . 13 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → ((((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) · (𝑍‘𝑖)) = (((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) · (𝑈‘𝑖)) ↔ ((((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · ((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)))) − ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) = (((𝐹‘𝑃) · (𝑈‘𝑖)) − (𝑡 · ((𝐹‘𝑄) · (𝑈‘𝑖))))))
103	61, 62	mulcld 9939	. . . . . . . . . . . . . 14 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) ∈ ℂ)
104	64, 97	mulcld 9939	. . . . . . . . . . . . . 14 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → ((𝐹‘𝑃) · (𝑈‘𝑖)) ∈ ℂ)
105	85, 62	mulcld 9939	. . . . . . . . . . . . . . 15 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → ((1 − 𝑡) · (𝑍‘𝑖)) ∈ ℂ)
106	89, 62	mulcld 9939	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → ((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) ∈ ℂ)
107	53, 106	mulcld 9939	. . . . . . . . . . . . . . 15 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → (𝑡 · ((1 − (𝐹‘𝑄)) · (𝑍‘𝑖))) ∈ ℂ)
108	105, 107	addcld 9938	. . . . . . . . . . . . . 14 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · ((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)))) ∈ ℂ)
109	54, 97	mulcld 9939	. . . . . . . . . . . . . . 15 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → ((𝐹‘𝑄) · (𝑈‘𝑖)) ∈ ℂ)
110	53, 109	mulcld 9939	. . . . . . . . . . . . . 14 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → (𝑡 · ((𝐹‘𝑄) · (𝑈‘𝑖))) ∈ ℂ)
111	103, 104, 108, 110	addsubeq4d 10322	. . . . . . . . . . . . 13 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → ((((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = ((((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · ((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)))) + (𝑡 · ((𝐹‘𝑄) · (𝑈‘𝑖)))) ↔ ((((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · ((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)))) − ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) = (((𝐹‘𝑃) · (𝑈‘𝑖)) − (𝑡 · ((𝐹‘𝑄) · (𝑈‘𝑖))))))
112	105, 107, 110	addassd 9941	. . . . . . . . . . . . . . 15 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → ((((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · ((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)))) + (𝑡 · ((𝐹‘𝑄) · (𝑈‘𝑖)))) = (((1 − 𝑡) · (𝑍‘𝑖)) + ((𝑡 · ((1 − (𝐹‘𝑄)) · (𝑍‘𝑖))) + (𝑡 · ((𝐹‘𝑄) · (𝑈‘𝑖))))))
113	53, 106, 109	adddid 9943	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → (𝑡 · (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))) = ((𝑡 · ((1 − (𝐹‘𝑄)) · (𝑍‘𝑖))) + (𝑡 · ((𝐹‘𝑄) · (𝑈‘𝑖)))))
114	113	oveq2d 6565	. . . . . . . . . . . . . . 15 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))))) = (((1 − 𝑡) · (𝑍‘𝑖)) + ((𝑡 · ((1 − (𝐹‘𝑄)) · (𝑍‘𝑖))) + (𝑡 · ((𝐹‘𝑄) · (𝑈‘𝑖))))))
115	112, 114	eqtr4d 2647	. . . . . . . . . . . . . 14 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → ((((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · ((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)))) + (𝑡 · ((𝐹‘𝑄) · (𝑈‘𝑖)))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))))))
116	115	eqeq2d 2620	. . . . . . . . . . . . 13 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → ((((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = ((((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · ((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)))) + (𝑡 · ((𝐹‘𝑄) · (𝑈‘𝑖)))) ↔ (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))))))
117	102, 111, 116	3bitr2rd 296	. . . . . . . . . . . 12 ⊢ ((((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ)) → ((((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))))) ↔ (((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) · (𝑍‘𝑖)) = (((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) · (𝑈‘𝑖))))
118	29, 32, 39, 45, 51, 117	syl23anc 1325	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))))) ↔ (((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) · (𝑍‘𝑖)) = (((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) · (𝑈‘𝑖))))
119	118	ralbidva 2968	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) · (𝑍‘𝑖)) = (((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) · (𝑈‘𝑖))))
120	39, 51	mulcld 9939	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 · (𝐹‘𝑄)) ∈ ℂ)
121	45, 120	subcld 10271	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) ∈ ℂ)
122		mulcan1g 10559	. . . . . . . . . . . 12 ⊢ ((((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) → ((((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) · (𝑍‘𝑖)) = (((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) · (𝑈‘𝑖)) ↔ (((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖))))
123	121, 29, 32, 122	syl3anc 1318	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → ((((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) · (𝑍‘𝑖)) = (((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) · (𝑈‘𝑖)) ↔ (((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖))))
124	123	ralbidva 2968	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)(((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) · (𝑍‘𝑖)) = (((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) · (𝑈‘𝑖)) ↔ ∀𝑖 ∈ (1...𝑁)(((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖))))
125		r19.32v 3064	. . . . . . . . . . 11 ⊢ (∀𝑖 ∈ (1...𝑁)(((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖)) ↔ (((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)))
126		simplr 788	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → 𝑍 ≠ 𝑈)
127	126	neneqd 2787	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → ¬ 𝑍 = 𝑈)
128		biorf 419	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑍 = 𝑈 → (((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) = 0 ↔ (𝑍 = 𝑈 ∨ ((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) = 0)))
129		orcom 401	. . . . . . . . . . . . . 14 ⊢ ((𝑍 = 𝑈 ∨ ((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) = 0) ↔ (((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) = 0 ∨ 𝑍 = 𝑈))
130	128, 129	syl6bb 275	. . . . . . . . . . . . 13 ⊢ (¬ 𝑍 = 𝑈 → (((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) = 0 ↔ (((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) = 0 ∨ 𝑍 = 𝑈)))
131	127, 130	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → (((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) = 0 ↔ (((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) = 0 ∨ 𝑍 = 𝑈)))
132	38, 50	mulcld 9939	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → (𝑡 · (𝐹‘𝑄)) ∈ ℂ)
133	44, 132	subeq0ad 10281	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → (((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) = 0 ↔ (𝐹‘𝑃) = (𝑡 · (𝐹‘𝑄))))
134		eqeefv 25583	. . . . . . . . . . . . . . . 16 ⊢ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)))
135	134	3adant1 1072	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)))
136	135	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)))
137	136	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)))
138	137	orbi2d 734	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → ((((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) = 0 ∨ 𝑍 = 𝑈) ↔ (((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖))))
139	131, 133, 138	3bitr3rd 298	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → ((((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)) ↔ (𝐹‘𝑃) = (𝑡 · (𝐹‘𝑄))))
140	125, 139	syl5bb 271	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)(((𝐹‘𝑃) − (𝑡 · (𝐹‘𝑄))) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖)) ↔ (𝐹‘𝑃) = (𝑡 · (𝐹‘𝑄))))
141	119, 124, 140	3bitrd 293	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))))) ↔ (𝐹‘𝑃) = (𝑡 · (𝐹‘𝑄))))
142	141	anassrs 678	. . . . . . . 8 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞))) ∧ 𝑡 ∈ (0[,]1)) → (∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))))) ↔ (𝐹‘𝑃) = (𝑡 · (𝐹‘𝑄))))
143	142	rexbidva 3031	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞))) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))))) ↔ ∃𝑡 ∈ (0[,]1)(𝐹‘𝑃) = (𝑡 · (𝐹‘𝑄))))
144	36	adantl 481	. . . . . . . . . . . . 13 ⊢ ((((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1)) → 𝑡 ∈ ℝ)
145		1red 9934	. . . . . . . . . . . . 13 ⊢ ((((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1)) → 1 ∈ ℝ)
146	46	biimpi 205	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑄) ∈ (0[,)+∞) → ((𝐹‘𝑄) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑄)))
147	146	ad2antlr 759	. . . . . . . . . . . . 13 ⊢ ((((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1)) → ((𝐹‘𝑄) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑄)))
148	35	simp3bi 1071	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ (0[,]1) → 𝑡 ≤ 1)
149	148	adantl 481	. . . . . . . . . . . . 13 ⊢ ((((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1)) → 𝑡 ≤ 1)
150		lemul1a 10756	. . . . . . . . . . . . 13 ⊢ (((𝑡 ∈ ℝ ∧ 1 ∈ ℝ ∧ ((𝐹‘𝑄) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑄))) ∧ 𝑡 ≤ 1) → (𝑡 · (𝐹‘𝑄)) ≤ (1 · (𝐹‘𝑄)))
151	144, 145, 147, 149, 150	syl31anc 1321	. . . . . . . . . . . 12 ⊢ ((((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1)) → (𝑡 · (𝐹‘𝑄)) ≤ (1 · (𝐹‘𝑄)))
152	48	ad2antlr 759	. . . . . . . . . . . . 13 ⊢ ((((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1)) → (𝐹‘𝑄) ∈ ℂ)
153	152	mulid2d 9937	. . . . . . . . . . . 12 ⊢ ((((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1)) → (1 · (𝐹‘𝑄)) = (𝐹‘𝑄))
154	151, 153	breqtrd 4609	. . . . . . . . . . 11 ⊢ ((((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1)) → (𝑡 · (𝐹‘𝑄)) ≤ (𝐹‘𝑄))
155		breq1 4586	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑃) = (𝑡 · (𝐹‘𝑄)) → ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ↔ (𝑡 · (𝐹‘𝑄)) ≤ (𝐹‘𝑄)))
156	154, 155	syl5ibrcom 236	. . . . . . . . . 10 ⊢ ((((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1)) → ((𝐹‘𝑃) = (𝑡 · (𝐹‘𝑄)) → (𝐹‘𝑃) ≤ (𝐹‘𝑄)))
157	156	rexlimdva 3013	. . . . . . . . 9 ⊢ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) → (∃𝑡 ∈ (0[,]1)(𝐹‘𝑃) = (𝑡 · (𝐹‘𝑄)) → (𝐹‘𝑃) ≤ (𝐹‘𝑄)))
158		0elunit 12161	. . . . . . . . . . . . . 14 ⊢ 0 ∈ (0[,]1)
159		simpl 472	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) = 0 ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) → (𝐹‘𝑃) = 0)
160	48	mul02d 10113	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑄) ∈ (0[,)+∞) → (0 · (𝐹‘𝑄)) = 0)
161	160	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) = 0 ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) → (0 · (𝐹‘𝑄)) = 0)
162	159, 161	eqtr4d 2647	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) = 0 ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) → (𝐹‘𝑃) = (0 · (𝐹‘𝑄)))
163		oveq1 6556	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 0 → (𝑡 · (𝐹‘𝑄)) = (0 · (𝐹‘𝑄)))
164	163	eqeq2d 2620	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 0 → ((𝐹‘𝑃) = (𝑡 · (𝐹‘𝑄)) ↔ (𝐹‘𝑃) = (0 · (𝐹‘𝑄))))
165	164	rspcev 3282	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ (0[,]1) ∧ (𝐹‘𝑃) = (0 · (𝐹‘𝑄))) → ∃𝑡 ∈ (0[,]1)(𝐹‘𝑃) = (𝑡 · (𝐹‘𝑄)))
166	158, 162, 165	sylancr 694	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑃) = 0 ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) → ∃𝑡 ∈ (0[,]1)(𝐹‘𝑃) = (𝑡 · (𝐹‘𝑄)))
167	166	adantrl 748	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑃) = 0 ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞))) → ∃𝑡 ∈ (0[,]1)(𝐹‘𝑃) = (𝑡 · (𝐹‘𝑄)))
168	167	a1d 25	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑃) = 0 ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞))) → ((𝐹‘𝑃) ≤ (𝐹‘𝑄) → ∃𝑡 ∈ (0[,]1)(𝐹‘𝑃) = (𝑡 · (𝐹‘𝑄))))
169	168	ex 449	. . . . . . . . . 10 ⊢ ((𝐹‘𝑃) = 0 → (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) → ((𝐹‘𝑃) ≤ (𝐹‘𝑄) → ∃𝑡 ∈ (0[,]1)(𝐹‘𝑃) = (𝑡 · (𝐹‘𝑄)))))
170		simp3 1056	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑃) ≠ 0 ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ (𝐹‘𝑃) ≤ (𝐹‘𝑄)) → (𝐹‘𝑃) ≤ (𝐹‘𝑄))
171	41	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) → (𝐹‘𝑃) ∈ ℝ)
172	171	3ad2ant2 1076	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ 0 ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ (𝐹‘𝑃) ≤ (𝐹‘𝑄)) → (𝐹‘𝑃) ∈ ℝ)
173	40	simprbi 479	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑃) ∈ (0[,)+∞) → 0 ≤ (𝐹‘𝑃))
174	173	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) → 0 ≤ (𝐹‘𝑃))
175	174	3ad2ant2 1076	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ 0 ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ (𝐹‘𝑃) ≤ (𝐹‘𝑄)) → 0 ≤ (𝐹‘𝑃))
176	47	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) → (𝐹‘𝑄) ∈ ℝ)
177	176	3ad2ant2 1076	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ 0 ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ (𝐹‘𝑃) ≤ (𝐹‘𝑄)) → (𝐹‘𝑄) ∈ ℝ)
178		0red 9920	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ≠ 0 ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ (𝐹‘𝑃) ≤ (𝐹‘𝑄)) → 0 ∈ ℝ)
179		simp1 1054	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑃) ≠ 0 ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ (𝐹‘𝑃) ≤ (𝐹‘𝑄)) → (𝐹‘𝑃) ≠ 0)
180	172, 175, 179	ne0gt0d 10053	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ≠ 0 ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ (𝐹‘𝑃) ≤ (𝐹‘𝑄)) → 0 < (𝐹‘𝑃))
181	178, 172, 177, 180, 170	ltletrd 10076	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ 0 ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ (𝐹‘𝑃) ≤ (𝐹‘𝑄)) → 0 < (𝐹‘𝑄))
182		divelunit 12185	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑃)) ∧ ((𝐹‘𝑄) ∈ ℝ ∧ 0 < (𝐹‘𝑄))) → (((𝐹‘𝑃) / (𝐹‘𝑄)) ∈ (0[,]1) ↔ (𝐹‘𝑃) ≤ (𝐹‘𝑄)))
183	172, 175, 177, 181, 182	syl22anc 1319	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑃) ≠ 0 ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ (𝐹‘𝑃) ≤ (𝐹‘𝑄)) → (((𝐹‘𝑃) / (𝐹‘𝑄)) ∈ (0[,]1) ↔ (𝐹‘𝑃) ≤ (𝐹‘𝑄)))
184	170, 183	mpbird 246	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑃) ≠ 0 ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ (𝐹‘𝑃) ≤ (𝐹‘𝑄)) → ((𝐹‘𝑃) / (𝐹‘𝑄)) ∈ (0[,]1))
185	43	3ad2ant2 1076	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ 0 ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ (𝐹‘𝑃) ≤ (𝐹‘𝑄)) → (𝐹‘𝑃) ∈ ℂ)
186	49	3ad2ant2 1076	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ 0 ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ (𝐹‘𝑃) ≤ (𝐹‘𝑄)) → (𝐹‘𝑄) ∈ ℂ)
187	181	gt0ne0d 10471	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ 0 ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ (𝐹‘𝑃) ≤ (𝐹‘𝑄)) → (𝐹‘𝑄) ≠ 0)
188	185, 186, 187	divcan1d 10681	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑃) ≠ 0 ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ (𝐹‘𝑃) ≤ (𝐹‘𝑄)) → (((𝐹‘𝑃) / (𝐹‘𝑄)) · (𝐹‘𝑄)) = (𝐹‘𝑃))
189	188	eqcomd 2616	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑃) ≠ 0 ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ (𝐹‘𝑃) ≤ (𝐹‘𝑄)) → (𝐹‘𝑃) = (((𝐹‘𝑃) / (𝐹‘𝑄)) · (𝐹‘𝑄)))
190		oveq1 6556	. . . . . . . . . . . . . 14 ⊢ (𝑡 = ((𝐹‘𝑃) / (𝐹‘𝑄)) → (𝑡 · (𝐹‘𝑄)) = (((𝐹‘𝑃) / (𝐹‘𝑄)) · (𝐹‘𝑄)))
191	190	eqeq2d 2620	. . . . . . . . . . . . 13 ⊢ (𝑡 = ((𝐹‘𝑃) / (𝐹‘𝑄)) → ((𝐹‘𝑃) = (𝑡 · (𝐹‘𝑄)) ↔ (𝐹‘𝑃) = (((𝐹‘𝑃) / (𝐹‘𝑄)) · (𝐹‘𝑄))))
192	191	rspcev 3282	. . . . . . . . . . . 12 ⊢ ((((𝐹‘𝑃) / (𝐹‘𝑄)) ∈ (0[,]1) ∧ (𝐹‘𝑃) = (((𝐹‘𝑃) / (𝐹‘𝑄)) · (𝐹‘𝑄))) → ∃𝑡 ∈ (0[,]1)(𝐹‘𝑃) = (𝑡 · (𝐹‘𝑄)))
193	184, 189, 192	syl2anc 691	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑃) ≠ 0 ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ (𝐹‘𝑃) ≤ (𝐹‘𝑄)) → ∃𝑡 ∈ (0[,]1)(𝐹‘𝑃) = (𝑡 · (𝐹‘𝑄)))
194	193	3exp 1256	. . . . . . . . . 10 ⊢ ((𝐹‘𝑃) ≠ 0 → (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) → ((𝐹‘𝑃) ≤ (𝐹‘𝑄) → ∃𝑡 ∈ (0[,]1)(𝐹‘𝑃) = (𝑡 · (𝐹‘𝑄)))))
195	169, 194	pm2.61ine 2865	. . . . . . . . 9 ⊢ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) → ((𝐹‘𝑃) ≤ (𝐹‘𝑄) → ∃𝑡 ∈ (0[,]1)(𝐹‘𝑃) = (𝑡 · (𝐹‘𝑄))))
196	157, 195	impbid 201	. . . . . . . 8 ⊢ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) → (∃𝑡 ∈ (0[,]1)(𝐹‘𝑃) = (𝑡 · (𝐹‘𝑄)) ↔ (𝐹‘𝑃) ≤ (𝐹‘𝑄)))
197	196	adantl 481	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞))) → (∃𝑡 ∈ (0[,]1)(𝐹‘𝑃) = (𝑡 · (𝐹‘𝑄)) ↔ (𝐹‘𝑃) ≤ (𝐹‘𝑄)))
198	143, 197	bitrd 267	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞))) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))))) ↔ (𝐹‘𝑃) ≤ (𝐹‘𝑄)))
199	26, 198	sylan9bbr 733	. . . . 5 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))))) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑄‘𝑖))) ↔ (𝐹‘𝑃) ≤ (𝐹‘𝑄)))
200	199	anasss 677	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞)) ∧ ∀𝑖 ∈ (1...𝑁)((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))))) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑄‘𝑖))) ↔ (𝐹‘𝑃) ≤ (𝐹‘𝑄)))
201	18, 200	sylan2b 491	. . 3 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))))) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑄‘𝑖))) ↔ (𝐹‘𝑃) ≤ (𝐹‘𝑄)))
202	14, 201	syldan 486	. 2 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷)) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑄‘𝑖))) ↔ (𝐹‘𝑃) ≤ (𝐹‘𝑄)))
203	10, 202	bitrd 267	1 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷)) → (𝑃 Btwn ⟨𝑍, 𝑄⟩ ↔ (𝐹‘𝑃) ≤ (𝐹‘𝑄)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∨ wo 382 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ≠ wne 2780 ∀wral 2896 ∃wrex 2897 {crab 2900 ⟨cop 4131 class class class wbr 4583 {copab 4642 ‘cfv 5804 (class class class)co 6549 ℂcc 9813 ℝcr 9814 0cc0 9815 1c1 9816 + caddc 9818 · cmul 9820 +∞cpnf 9950 < clt 9953 ≤ cle 9954 − cmin 10145 / cdiv 10563 ℕcn 10897 [,)cico 12048 [,]cicc 12049 ...cfz 12197 𝔼cee 25568 Btwn cbtwn 25569

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-er 7629 df-map 7746 df-en 7842 df-dom 7843 df-sdom 7844 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-z 11255 df-uz 11564 df-ico 12052 df-icc 12053 df-fz 12198 df-ee 25571 df-btwn 25572

This theorem is referenced by: axcontlem9 25652

W3C validator