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

Theorem axcontlem7 26141
Description: Lemma for axcont 26147. 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
StepHypRef Expression
1 axcontlem7.1 . . . . . 6 𝐷 = {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)}
2 ssrab2 3847 . . . . . 6 {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)} ⊆ (𝔼‘𝑁)
31, 2eqsstri 3795 . . . . 5 𝐷 ⊆ (𝔼‘𝑁)
43sseli 3757 . . . 4 (𝑃𝐷𝑃 ∈ (𝔼‘𝑁))
54ad2antrl 719 . . 3 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷)) → 𝑃 ∈ (𝔼‘𝑁))
6 simpll2 1271 . . 3 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷)) → 𝑍 ∈ (𝔼‘𝑁))
73sseli 3757 . . . 4 (𝑄𝐷𝑄 ∈ (𝔼‘𝑁))
87ad2antll 720 . . 3 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷)) → 𝑄 ∈ (𝔼‘𝑁))
9 brbtwn 26070 . . 3 ((𝑃 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁)) → (𝑃 Btwn ⟨𝑍, 𝑄⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑄𝑖)))))
105, 6, 8, 9syl3anc 1490 . 2 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷)) → (𝑃 Btwn ⟨𝑍, 𝑄⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑄𝑖)))))
11 axcontlem7.2 . . . . 5 𝐹 = {⟨𝑥, 𝑡⟩ ∣ (𝑥𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))}
121, 11axcontlem6 26140 . . . 4 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑃𝐷) → ((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))))
131, 11axcontlem6 26140 . . . 4 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑄𝐷) → ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))))
1412, 13anim12dan 612 . . 3 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷)) → (((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) ∧ ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))))
15 an4 646 . . . . 5 ((((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) ∧ ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))) ↔ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ (∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))))
16 r19.26 3211 . . . . . 6 (∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))))
1716anbi2i 616 . . . . 5 ((((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ ∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))) ↔ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ (∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))))
1815, 17bitr4i 269 . . . 4 ((((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) ∧ ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))) ↔ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ ∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))))
19 id 22 . . . . . . . . . 10 ((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) → (𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))
20 oveq2 6850 . . . . . . . . . . 11 ((𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) → (𝑡 · (𝑄𝑖)) = (𝑡 · (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))))
2120oveq2d 6858 . . . . . . . . . 10 ((𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑄𝑖))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))))
2219, 21eqeqan12d 2781 . . . . . . . . 9 (((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) → ((𝑃𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑄𝑖))) ↔ (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))))))
2322ralimi 3099 . . . . . . . 8 (∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) → ∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑄𝑖))) ↔ (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))))))
24 ralbi 3215 . . . . . . . 8 (∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑄𝑖))) ↔ (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))))) → (∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑄𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))))))
2523, 24syl 17 . . . . . . 7 (∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) → (∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑄𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))))))
2625rexbidv 3199 . . . . . 6 (∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑄𝑖))) ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))))))
27 simpll2 1271 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → 𝑍 ∈ (𝔼‘𝑁))
28 fveecn 26073 . . . . . . . . . . . . 13 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
2927, 28sylan 575 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
30 simpll3 1273 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → 𝑈 ∈ (𝔼‘𝑁))
31 fveecn 26073 . . . . . . . . . . . . 13 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) ∈ ℂ)
3230, 31sylan 575 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) ∈ ℂ)
33 elicc01 12494 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (0[,]1) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡𝑡 ≤ 1))
3433simp1bi 1175 . . . . . . . . . . . . . . 15 (𝑡 ∈ (0[,]1) → 𝑡 ∈ ℝ)
3534recnd 10322 . . . . . . . . . . . . . 14 (𝑡 ∈ (0[,]1) → 𝑡 ∈ ℂ)
3635ad2antll 720 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → 𝑡 ∈ ℂ)
3736adantr 472 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
38 elrege0 12482 . . . . . . . . . . . . . . . . 17 ((𝐹𝑃) ∈ (0[,)+∞) ↔ ((𝐹𝑃) ∈ ℝ ∧ 0 ≤ (𝐹𝑃)))
3938simplbi 491 . . . . . . . . . . . . . . . 16 ((𝐹𝑃) ∈ (0[,)+∞) → (𝐹𝑃) ∈ ℝ)
4039recnd 10322 . . . . . . . . . . . . . . 15 ((𝐹𝑃) ∈ (0[,)+∞) → (𝐹𝑃) ∈ ℂ)
4140adantr 472 . . . . . . . . . . . . . 14 (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) → (𝐹𝑃) ∈ ℂ)
4241ad2antrl 719 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → (𝐹𝑃) ∈ ℂ)
4342adantr 472 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ∈ ℂ)
44 elrege0 12482 . . . . . . . . . . . . . . . . 17 ((𝐹𝑄) ∈ (0[,)+∞) ↔ ((𝐹𝑄) ∈ ℝ ∧ 0 ≤ (𝐹𝑄)))
4544simplbi 491 . . . . . . . . . . . . . . . 16 ((𝐹𝑄) ∈ (0[,)+∞) → (𝐹𝑄) ∈ ℝ)
4645recnd 10322 . . . . . . . . . . . . . . 15 ((𝐹𝑄) ∈ (0[,)+∞) → (𝐹𝑄) ∈ ℂ)
4746adantl 473 . . . . . . . . . . . . . 14 (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) → (𝐹𝑄) ∈ ℂ)
4847ad2antrl 719 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → (𝐹𝑄) ∈ ℂ)
4948adantr 472 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑄) ∈ ℂ)
50 ax-1cn 10247 . . . . . . . . . . . . . . . . 17 1 ∈ ℂ
51 simpr1 1248 . . . . . . . . . . . . . . . . . 18 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → 𝑡 ∈ ℂ)
52 simpr3 1252 . . . . . . . . . . . . . . . . . 18 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → (𝐹𝑄) ∈ ℂ)
5351, 52mulcld 10314 . . . . . . . . . . . . . . . . 17 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → (𝑡 · (𝐹𝑄)) ∈ ℂ)
54 subcl 10534 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℂ ∧ (𝑡 · (𝐹𝑄)) ∈ ℂ) → (1 − (𝑡 · (𝐹𝑄))) ∈ ℂ)
5550, 53, 54sylancr 581 . . . . . . . . . . . . . . . 16 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → (1 − (𝑡 · (𝐹𝑄))) ∈ ℂ)
56 subcl 10534 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ) → (1 − (𝐹𝑃)) ∈ ℂ)
5750, 56mpan 681 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑃) ∈ ℂ → (1 − (𝐹𝑃)) ∈ ℂ)
58573ad2ant2 1164 . . . . . . . . . . . . . . . . 17 ((𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ) → (1 − (𝐹𝑃)) ∈ ℂ)
5958adantl 473 . . . . . . . . . . . . . . . 16 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → (1 − (𝐹𝑃)) ∈ ℂ)
60 simpll 783 . . . . . . . . . . . . . . . 16 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → (𝑍𝑖) ∈ ℂ)
6155, 59, 60subdird 10741 . . . . . . . . . . . . . . 15 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → (((1 − (𝑡 · (𝐹𝑄))) − (1 − (𝐹𝑃))) · (𝑍𝑖)) = (((1 − (𝑡 · (𝐹𝑄))) · (𝑍𝑖)) − ((1 − (𝐹𝑃)) · (𝑍𝑖))))
62 simpr2 1250 . . . . . . . . . . . . . . . . 17 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → (𝐹𝑃) ∈ ℂ)
63 nnncan1 10571 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℂ ∧ (𝑡 · (𝐹𝑄)) ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ) → ((1 − (𝑡 · (𝐹𝑄))) − (1 − (𝐹𝑃))) = ((𝐹𝑃) − (𝑡 · (𝐹𝑄))))
6450, 63mp3an1 1572 . . . . . . . . . . . . . . . . 17 (((𝑡 · (𝐹𝑄)) ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ) → ((1 − (𝑡 · (𝐹𝑄))) − (1 − (𝐹𝑃))) = ((𝐹𝑃) − (𝑡 · (𝐹𝑄))))
6553, 62, 64syl2anc 579 . . . . . . . . . . . . . . . 16 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → ((1 − (𝑡 · (𝐹𝑄))) − (1 − (𝐹𝑃))) = ((𝐹𝑃) − (𝑡 · (𝐹𝑄))))
6665oveq1d 6857 . . . . . . . . . . . . . . 15 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → (((1 − (𝑡 · (𝐹𝑄))) − (1 − (𝐹𝑃))) · (𝑍𝑖)) = (((𝐹𝑃) − (𝑡 · (𝐹𝑄))) · (𝑍𝑖)))
67 subdi 10717 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ) → (𝑡 · (1 − (𝐹𝑄))) = ((𝑡 · 1) − (𝑡 · (𝐹𝑄))))
6850, 67mp3an2 1573 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ) → (𝑡 · (1 − (𝐹𝑄))) = ((𝑡 · 1) − (𝑡 · (𝐹𝑄))))
69 mulid1 10291 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 ∈ ℂ → (𝑡 · 1) = 𝑡)
7069adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑡 ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ) → (𝑡 · 1) = 𝑡)
7170oveq1d 6857 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ) → ((𝑡 · 1) − (𝑡 · (𝐹𝑄))) = (𝑡 − (𝑡 · (𝐹𝑄))))
7268, 71eqtrd 2799 . . . . . . . . . . . . . . . . . . . . 21 ((𝑡 ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ) → (𝑡 · (1 − (𝐹𝑄))) = (𝑡 − (𝑡 · (𝐹𝑄))))
7351, 52, 72syl2anc 579 . . . . . . . . . . . . . . . . . . . 20 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → (𝑡 · (1 − (𝐹𝑄))) = (𝑡 − (𝑡 · (𝐹𝑄))))
7473oveq2d 6858 . . . . . . . . . . . . . . . . . . 19 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → ((1 − 𝑡) + (𝑡 · (1 − (𝐹𝑄)))) = ((1 − 𝑡) + (𝑡 − (𝑡 · (𝐹𝑄)))))
75 npncan 10556 . . . . . . . . . . . . . . . . . . . . 21 ((1 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ (𝑡 · (𝐹𝑄)) ∈ ℂ) → ((1 − 𝑡) + (𝑡 − (𝑡 · (𝐹𝑄)))) = (1 − (𝑡 · (𝐹𝑄))))
7650, 75mp3an1 1572 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ ℂ ∧ (𝑡 · (𝐹𝑄)) ∈ ℂ) → ((1 − 𝑡) + (𝑡 − (𝑡 · (𝐹𝑄)))) = (1 − (𝑡 · (𝐹𝑄))))
7751, 53, 76syl2anc 579 . . . . . . . . . . . . . . . . . . 19 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → ((1 − 𝑡) + (𝑡 − (𝑡 · (𝐹𝑄)))) = (1 − (𝑡 · (𝐹𝑄))))
7874, 77eqtr2d 2800 . . . . . . . . . . . . . . . . . 18 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → (1 − (𝑡 · (𝐹𝑄))) = ((1 − 𝑡) + (𝑡 · (1 − (𝐹𝑄)))))
7978oveq1d 6857 . . . . . . . . . . . . . . . . 17 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → ((1 − (𝑡 · (𝐹𝑄))) · (𝑍𝑖)) = (((1 − 𝑡) + (𝑡 · (1 − (𝐹𝑄)))) · (𝑍𝑖)))
80 subcl 10534 . . . . . . . . . . . . . . . . . . . . 21 ((1 ∈ ℂ ∧ 𝑡 ∈ ℂ) → (1 − 𝑡) ∈ ℂ)
8150, 80mpan 681 . . . . . . . . . . . . . . . . . . . 20 (𝑡 ∈ ℂ → (1 − 𝑡) ∈ ℂ)
82813ad2ant1 1163 . . . . . . . . . . . . . . . . . . 19 ((𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ) → (1 − 𝑡) ∈ ℂ)
8382adantl 473 . . . . . . . . . . . . . . . . . 18 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → (1 − 𝑡) ∈ ℂ)
84 subcl 10534 . . . . . . . . . . . . . . . . . . . . . 22 ((1 ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ) → (1 − (𝐹𝑄)) ∈ ℂ)
8550, 84mpan 681 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑄) ∈ ℂ → (1 − (𝐹𝑄)) ∈ ℂ)
86853ad2ant3 1165 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ) → (1 − (𝐹𝑄)) ∈ ℂ)
8786adantl 473 . . . . . . . . . . . . . . . . . . 19 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → (1 − (𝐹𝑄)) ∈ ℂ)
8851, 87mulcld 10314 . . . . . . . . . . . . . . . . . 18 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → (𝑡 · (1 − (𝐹𝑄))) ∈ ℂ)
8983, 88, 60adddird 10319 . . . . . . . . . . . . . . . . 17 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → (((1 − 𝑡) + (𝑡 · (1 − (𝐹𝑄)))) · (𝑍𝑖)) = (((1 − 𝑡) · (𝑍𝑖)) + ((𝑡 · (1 − (𝐹𝑄))) · (𝑍𝑖))))
9051, 87, 60mulassd 10317 . . . . . . . . . . . . . . . . . 18 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → ((𝑡 · (1 − (𝐹𝑄))) · (𝑍𝑖)) = (𝑡 · ((1 − (𝐹𝑄)) · (𝑍𝑖))))
9190oveq2d 6858 . . . . . . . . . . . . . . . . 17 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → (((1 − 𝑡) · (𝑍𝑖)) + ((𝑡 · (1 − (𝐹𝑄))) · (𝑍𝑖))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · ((1 − (𝐹𝑄)) · (𝑍𝑖)))))
9279, 89, 913eqtrd 2803 . . . . . . . . . . . . . . . 16 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → ((1 − (𝑡 · (𝐹𝑄))) · (𝑍𝑖)) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · ((1 − (𝐹𝑄)) · (𝑍𝑖)))))
9392oveq1d 6857 . . . . . . . . . . . . . . 15 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → (((1 − (𝑡 · (𝐹𝑄))) · (𝑍𝑖)) − ((1 − (𝐹𝑃)) · (𝑍𝑖))) = ((((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · ((1 − (𝐹𝑄)) · (𝑍𝑖)))) − ((1 − (𝐹𝑃)) · (𝑍𝑖))))
9461, 66, 933eqtr3d 2807 . . . . . . . . . . . . . 14 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → (((𝐹𝑃) − (𝑡 · (𝐹𝑄))) · (𝑍𝑖)) = ((((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · ((1 − (𝐹𝑄)) · (𝑍𝑖)))) − ((1 − (𝐹𝑃)) · (𝑍𝑖))))
95 simplr 785 . . . . . . . . . . . . . . . 16 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → (𝑈𝑖) ∈ ℂ)
9662, 53, 95subdird 10741 . . . . . . . . . . . . . . 15 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → (((𝐹𝑃) − (𝑡 · (𝐹𝑄))) · (𝑈𝑖)) = (((𝐹𝑃) · (𝑈𝑖)) − ((𝑡 · (𝐹𝑄)) · (𝑈𝑖))))
9751, 52, 95mulassd 10317 . . . . . . . . . . . . . . . 16 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → ((𝑡 · (𝐹𝑄)) · (𝑈𝑖)) = (𝑡 · ((𝐹𝑄) · (𝑈𝑖))))
9897oveq2d 6858 . . . . . . . . . . . . . . 15 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → (((𝐹𝑃) · (𝑈𝑖)) − ((𝑡 · (𝐹𝑄)) · (𝑈𝑖))) = (((𝐹𝑃) · (𝑈𝑖)) − (𝑡 · ((𝐹𝑄) · (𝑈𝑖)))))
9996, 98eqtrd 2799 . . . . . . . . . . . . . 14 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → (((𝐹𝑃) − (𝑡 · (𝐹𝑄))) · (𝑈𝑖)) = (((𝐹𝑃) · (𝑈𝑖)) − (𝑡 · ((𝐹𝑄) · (𝑈𝑖)))))
10094, 99eqeq12d 2780 . . . . . . . . . . . . 13 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → ((((𝐹𝑃) − (𝑡 · (𝐹𝑄))) · (𝑍𝑖)) = (((𝐹𝑃) − (𝑡 · (𝐹𝑄))) · (𝑈𝑖)) ↔ ((((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · ((1 − (𝐹𝑄)) · (𝑍𝑖)))) − ((1 − (𝐹𝑃)) · (𝑍𝑖))) = (((𝐹𝑃) · (𝑈𝑖)) − (𝑡 · ((𝐹𝑄) · (𝑈𝑖))))))
10159, 60mulcld 10314 . . . . . . . . . . . . . 14 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → ((1 − (𝐹𝑃)) · (𝑍𝑖)) ∈ ℂ)
10262, 95mulcld 10314 . . . . . . . . . . . . . 14 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → ((𝐹𝑃) · (𝑈𝑖)) ∈ ℂ)
10383, 60mulcld 10314 . . . . . . . . . . . . . . 15 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → ((1 − 𝑡) · (𝑍𝑖)) ∈ ℂ)
10487, 60mulcld 10314 . . . . . . . . . . . . . . . 16 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → ((1 − (𝐹𝑄)) · (𝑍𝑖)) ∈ ℂ)
10551, 104mulcld 10314 . . . . . . . . . . . . . . 15 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → (𝑡 · ((1 − (𝐹𝑄)) · (𝑍𝑖))) ∈ ℂ)
106103, 105addcld 10313 . . . . . . . . . . . . . 14 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · ((1 − (𝐹𝑄)) · (𝑍𝑖)))) ∈ ℂ)
10752, 95mulcld 10314 . . . . . . . . . . . . . . 15 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → ((𝐹𝑄) · (𝑈𝑖)) ∈ ℂ)
10851, 107mulcld 10314 . . . . . . . . . . . . . 14 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → (𝑡 · ((𝐹𝑄) · (𝑈𝑖))) ∈ ℂ)
109101, 102, 106, 108addsubeq4d 10697 . . . . . . . . . . . . 13 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → ((((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = ((((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · ((1 − (𝐹𝑄)) · (𝑍𝑖)))) + (𝑡 · ((𝐹𝑄) · (𝑈𝑖)))) ↔ ((((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · ((1 − (𝐹𝑄)) · (𝑍𝑖)))) − ((1 − (𝐹𝑃)) · (𝑍𝑖))) = (((𝐹𝑃) · (𝑈𝑖)) − (𝑡 · ((𝐹𝑄) · (𝑈𝑖))))))
110103, 105, 108addassd 10316 . . . . . . . . . . . . . . 15 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → ((((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · ((1 − (𝐹𝑄)) · (𝑍𝑖)))) + (𝑡 · ((𝐹𝑄) · (𝑈𝑖)))) = (((1 − 𝑡) · (𝑍𝑖)) + ((𝑡 · ((1 − (𝐹𝑄)) · (𝑍𝑖))) + (𝑡 · ((𝐹𝑄) · (𝑈𝑖))))))
11151, 104, 107adddid 10318 . . . . . . . . . . . . . . . 16 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → (𝑡 · (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) = ((𝑡 · ((1 − (𝐹𝑄)) · (𝑍𝑖))) + (𝑡 · ((𝐹𝑄) · (𝑈𝑖)))))
112111oveq2d 6858 . . . . . . . . . . . . . . 15 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))) = (((1 − 𝑡) · (𝑍𝑖)) + ((𝑡 · ((1 − (𝐹𝑄)) · (𝑍𝑖))) + (𝑡 · ((𝐹𝑄) · (𝑈𝑖))))))
113110, 112eqtr4d 2802 . . . . . . . . . . . . . 14 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → ((((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · ((1 − (𝐹𝑄)) · (𝑍𝑖)))) + (𝑡 · ((𝐹𝑄) · (𝑈𝑖)))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))))
114113eqeq2d 2775 . . . . . . . . . . . . 13 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → ((((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = ((((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · ((1 − (𝐹𝑄)) · (𝑍𝑖)))) + (𝑡 · ((𝐹𝑄) · (𝑈𝑖)))) ↔ (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))))))
115100, 109, 1143bitr2rd 299 . . . . . . . . . . . 12 ((((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) ∧ (𝑡 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ)) → ((((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))) ↔ (((𝐹𝑃) − (𝑡 · (𝐹𝑄))) · (𝑍𝑖)) = (((𝐹𝑃) − (𝑡 · (𝐹𝑄))) · (𝑈𝑖))))
11629, 32, 37, 43, 49, 115syl23anc 1496 . . . . . . . . . . 11 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))) ↔ (((𝐹𝑃) − (𝑡 · (𝐹𝑄))) · (𝑍𝑖)) = (((𝐹𝑃) − (𝑡 · (𝐹𝑄))) · (𝑈𝑖))))
117116ralbidva 3132 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((𝐹𝑃) − (𝑡 · (𝐹𝑄))) · (𝑍𝑖)) = (((𝐹𝑃) − (𝑡 · (𝐹𝑄))) · (𝑈𝑖))))
11837, 49mulcld 10314 . . . . . . . . . . . . 13 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 · (𝐹𝑄)) ∈ ℂ)
11943, 118subcld 10646 . . . . . . . . . . . 12 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐹𝑃) − (𝑡 · (𝐹𝑄))) ∈ ℂ)
120 mulcan1g 10934 . . . . . . . . . . . 12 ((((𝐹𝑃) − (𝑡 · (𝐹𝑄))) ∈ ℂ ∧ (𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) → ((((𝐹𝑃) − (𝑡 · (𝐹𝑄))) · (𝑍𝑖)) = (((𝐹𝑃) − (𝑡 · (𝐹𝑄))) · (𝑈𝑖)) ↔ (((𝐹𝑃) − (𝑡 · (𝐹𝑄))) = 0 ∨ (𝑍𝑖) = (𝑈𝑖))))
121119, 29, 32, 120syl3anc 1490 . . . . . . . . . . 11 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) ∧ 𝑖 ∈ (1...𝑁)) → ((((𝐹𝑃) − (𝑡 · (𝐹𝑄))) · (𝑍𝑖)) = (((𝐹𝑃) − (𝑡 · (𝐹𝑄))) · (𝑈𝑖)) ↔ (((𝐹𝑃) − (𝑡 · (𝐹𝑄))) = 0 ∨ (𝑍𝑖) = (𝑈𝑖))))
122121ralbidva 3132 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)(((𝐹𝑃) − (𝑡 · (𝐹𝑄))) · (𝑍𝑖)) = (((𝐹𝑃) − (𝑡 · (𝐹𝑄))) · (𝑈𝑖)) ↔ ∀𝑖 ∈ (1...𝑁)(((𝐹𝑃) − (𝑡 · (𝐹𝑄))) = 0 ∨ (𝑍𝑖) = (𝑈𝑖))))
123 r19.32v 3230 . . . . . . . . . . 11 (∀𝑖 ∈ (1...𝑁)(((𝐹𝑃) − (𝑡 · (𝐹𝑄))) = 0 ∨ (𝑍𝑖) = (𝑈𝑖)) ↔ (((𝐹𝑃) − (𝑡 · (𝐹𝑄))) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
124 simplr 785 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → 𝑍𝑈)
125124neneqd 2942 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → ¬ 𝑍 = 𝑈)
126 biorf 960 . . . . . . . . . . . . . 14 𝑍 = 𝑈 → (((𝐹𝑃) − (𝑡 · (𝐹𝑄))) = 0 ↔ (𝑍 = 𝑈 ∨ ((𝐹𝑃) − (𝑡 · (𝐹𝑄))) = 0)))
127 orcom 896 . . . . . . . . . . . . . 14 ((𝑍 = 𝑈 ∨ ((𝐹𝑃) − (𝑡 · (𝐹𝑄))) = 0) ↔ (((𝐹𝑃) − (𝑡 · (𝐹𝑄))) = 0 ∨ 𝑍 = 𝑈))
128126, 127syl6bb 278 . . . . . . . . . . . . 13 𝑍 = 𝑈 → (((𝐹𝑃) − (𝑡 · (𝐹𝑄))) = 0 ↔ (((𝐹𝑃) − (𝑡 · (𝐹𝑄))) = 0 ∨ 𝑍 = 𝑈)))
129125, 128syl 17 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → (((𝐹𝑃) − (𝑡 · (𝐹𝑄))) = 0 ↔ (((𝐹𝑃) − (𝑡 · (𝐹𝑄))) = 0 ∨ 𝑍 = 𝑈)))
13036, 48mulcld 10314 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → (𝑡 · (𝐹𝑄)) ∈ ℂ)
13142, 130subeq0ad 10656 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → (((𝐹𝑃) − (𝑡 · (𝐹𝑄))) = 0 ↔ (𝐹𝑃) = (𝑡 · (𝐹𝑄))))
132 eqeefv 26074 . . . . . . . . . . . . . . . 16 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
1331323adant1 1160 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
134133adantr 472 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
135134adantr 472 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)))
136135orbi2d 939 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → ((((𝐹𝑃) − (𝑡 · (𝐹𝑄))) = 0 ∨ 𝑍 = 𝑈) ↔ (((𝐹𝑃) − (𝑡 · (𝐹𝑄))) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖))))
137129, 131, 1363bitr3rd 301 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → ((((𝐹𝑃) − (𝑡 · (𝐹𝑄))) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍𝑖) = (𝑈𝑖)) ↔ (𝐹𝑃) = (𝑡 · (𝐹𝑄))))
138123, 137syl5bb 274 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)(((𝐹𝑃) − (𝑡 · (𝐹𝑄))) = 0 ∨ (𝑍𝑖) = (𝑈𝑖)) ↔ (𝐹𝑃) = (𝑡 · (𝐹𝑄))))
139117, 122, 1383bitrd 296 . . . . . . . . 9 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))) ↔ (𝐹𝑃) = (𝑡 · (𝐹𝑄))))
140139anassrs 459 . . . . . . . 8 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞))) ∧ 𝑡 ∈ (0[,]1)) → (∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))) ↔ (𝐹𝑃) = (𝑡 · (𝐹𝑄))))
141140rexbidva 3196 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞))) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))) ↔ ∃𝑡 ∈ (0[,]1)(𝐹𝑃) = (𝑡 · (𝐹𝑄))))
14234adantl 473 . . . . . . . . . . . . 13 ((((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1)) → 𝑡 ∈ ℝ)
143 1red 10294 . . . . . . . . . . . . 13 ((((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1)) → 1 ∈ ℝ)
14444biimpi 207 . . . . . . . . . . . . . 14 ((𝐹𝑄) ∈ (0[,)+∞) → ((𝐹𝑄) ∈ ℝ ∧ 0 ≤ (𝐹𝑄)))
145144ad2antlr 718 . . . . . . . . . . . . 13 ((((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1)) → ((𝐹𝑄) ∈ ℝ ∧ 0 ≤ (𝐹𝑄)))
14633simp3bi 1177 . . . . . . . . . . . . . 14 (𝑡 ∈ (0[,]1) → 𝑡 ≤ 1)
147146adantl 473 . . . . . . . . . . . . 13 ((((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1)) → 𝑡 ≤ 1)
148 lemul1a 11131 . . . . . . . . . . . . 13 (((𝑡 ∈ ℝ ∧ 1 ∈ ℝ ∧ ((𝐹𝑄) ∈ ℝ ∧ 0 ≤ (𝐹𝑄))) ∧ 𝑡 ≤ 1) → (𝑡 · (𝐹𝑄)) ≤ (1 · (𝐹𝑄)))
149142, 143, 145, 147, 148syl31anc 1492 . . . . . . . . . . . 12 ((((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1)) → (𝑡 · (𝐹𝑄)) ≤ (1 · (𝐹𝑄)))
15046ad2antlr 718 . . . . . . . . . . . . 13 ((((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1)) → (𝐹𝑄) ∈ ℂ)
151150mulid2d 10312 . . . . . . . . . . . 12 ((((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1)) → (1 · (𝐹𝑄)) = (𝐹𝑄))
152149, 151breqtrd 4835 . . . . . . . . . . 11 ((((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1)) → (𝑡 · (𝐹𝑄)) ≤ (𝐹𝑄))
153 breq1 4812 . . . . . . . . . . 11 ((𝐹𝑃) = (𝑡 · (𝐹𝑄)) → ((𝐹𝑃) ≤ (𝐹𝑄) ↔ (𝑡 · (𝐹𝑄)) ≤ (𝐹𝑄)))
154152, 153syl5ibrcom 238 . . . . . . . . . 10 ((((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ 𝑡 ∈ (0[,]1)) → ((𝐹𝑃) = (𝑡 · (𝐹𝑄)) → (𝐹𝑃) ≤ (𝐹𝑄)))
155154rexlimdva 3178 . . . . . . . . 9 (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) → (∃𝑡 ∈ (0[,]1)(𝐹𝑃) = (𝑡 · (𝐹𝑄)) → (𝐹𝑃) ≤ (𝐹𝑄)))
156 0elunit 12495 . . . . . . . . . . . . . 14 0 ∈ (0[,]1)
157 simpl 474 . . . . . . . . . . . . . . 15 (((𝐹𝑃) = 0 ∧ (𝐹𝑄) ∈ (0[,)+∞)) → (𝐹𝑃) = 0)
15846mul02d 10488 . . . . . . . . . . . . . . . 16 ((𝐹𝑄) ∈ (0[,)+∞) → (0 · (𝐹𝑄)) = 0)
159158adantl 473 . . . . . . . . . . . . . . 15 (((𝐹𝑃) = 0 ∧ (𝐹𝑄) ∈ (0[,)+∞)) → (0 · (𝐹𝑄)) = 0)
160157, 159eqtr4d 2802 . . . . . . . . . . . . . 14 (((𝐹𝑃) = 0 ∧ (𝐹𝑄) ∈ (0[,)+∞)) → (𝐹𝑃) = (0 · (𝐹𝑄)))
161 oveq1 6849 . . . . . . . . . . . . . . 15 (𝑡 = 0 → (𝑡 · (𝐹𝑄)) = (0 · (𝐹𝑄)))
162161rspceeqv 3479 . . . . . . . . . . . . . 14 ((0 ∈ (0[,]1) ∧ (𝐹𝑃) = (0 · (𝐹𝑄))) → ∃𝑡 ∈ (0[,]1)(𝐹𝑃) = (𝑡 · (𝐹𝑄)))
163156, 160, 162sylancr 581 . . . . . . . . . . . . 13 (((𝐹𝑃) = 0 ∧ (𝐹𝑄) ∈ (0[,)+∞)) → ∃𝑡 ∈ (0[,]1)(𝐹𝑃) = (𝑡 · (𝐹𝑄)))
164163adantrl 707 . . . . . . . . . . . 12 (((𝐹𝑃) = 0 ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞))) → ∃𝑡 ∈ (0[,]1)(𝐹𝑃) = (𝑡 · (𝐹𝑄)))
165164a1d 25 . . . . . . . . . . 11 (((𝐹𝑃) = 0 ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞))) → ((𝐹𝑃) ≤ (𝐹𝑄) → ∃𝑡 ∈ (0[,]1)(𝐹𝑃) = (𝑡 · (𝐹𝑄))))
166165ex 401 . . . . . . . . . 10 ((𝐹𝑃) = 0 → (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) → ((𝐹𝑃) ≤ (𝐹𝑄) → ∃𝑡 ∈ (0[,]1)(𝐹𝑃) = (𝑡 · (𝐹𝑄)))))
167 simp3 1168 . . . . . . . . . . . . 13 (((𝐹𝑃) ≠ 0 ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ (𝐹𝑃) ≤ (𝐹𝑄)) → (𝐹𝑃) ≤ (𝐹𝑄))
16839adantr 472 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) → (𝐹𝑃) ∈ ℝ)
1691683ad2ant2 1164 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ 0 ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ (𝐹𝑃) ≤ (𝐹𝑄)) → (𝐹𝑃) ∈ ℝ)
17038simprbi 490 . . . . . . . . . . . . . . . 16 ((𝐹𝑃) ∈ (0[,)+∞) → 0 ≤ (𝐹𝑃))
171170adantr 472 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) → 0 ≤ (𝐹𝑃))
1721713ad2ant2 1164 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ 0 ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ (𝐹𝑃) ≤ (𝐹𝑄)) → 0 ≤ (𝐹𝑃))
17345adantl 473 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) → (𝐹𝑄) ∈ ℝ)
1741733ad2ant2 1164 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ 0 ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ (𝐹𝑃) ≤ (𝐹𝑄)) → (𝐹𝑄) ∈ ℝ)
175 0red 10297 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ 0 ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ (𝐹𝑃) ≤ (𝐹𝑄)) → 0 ∈ ℝ)
176 simp1 1166 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) ≠ 0 ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ (𝐹𝑃) ≤ (𝐹𝑄)) → (𝐹𝑃) ≠ 0)
177169, 172, 176ne0gt0d 10428 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ 0 ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ (𝐹𝑃) ≤ (𝐹𝑄)) → 0 < (𝐹𝑃))
178175, 169, 174, 177, 167ltletrd 10451 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ 0 ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ (𝐹𝑃) ≤ (𝐹𝑄)) → 0 < (𝐹𝑄))
179 divelunit 12521 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ∈ ℝ ∧ 0 ≤ (𝐹𝑃)) ∧ ((𝐹𝑄) ∈ ℝ ∧ 0 < (𝐹𝑄))) → (((𝐹𝑃) / (𝐹𝑄)) ∈ (0[,]1) ↔ (𝐹𝑃) ≤ (𝐹𝑄)))
180169, 172, 174, 178, 179syl22anc 867 . . . . . . . . . . . . 13 (((𝐹𝑃) ≠ 0 ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ (𝐹𝑃) ≤ (𝐹𝑄)) → (((𝐹𝑃) / (𝐹𝑄)) ∈ (0[,]1) ↔ (𝐹𝑃) ≤ (𝐹𝑄)))
181167, 180mpbird 248 . . . . . . . . . . . 12 (((𝐹𝑃) ≠ 0 ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ (𝐹𝑃) ≤ (𝐹𝑄)) → ((𝐹𝑃) / (𝐹𝑄)) ∈ (0[,]1))
182413ad2ant2 1164 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ 0 ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ (𝐹𝑃) ≤ (𝐹𝑄)) → (𝐹𝑃) ∈ ℂ)
183473ad2ant2 1164 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ 0 ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ (𝐹𝑃) ≤ (𝐹𝑄)) → (𝐹𝑄) ∈ ℂ)
184178gt0ne0d 10846 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ 0 ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ (𝐹𝑃) ≤ (𝐹𝑄)) → (𝐹𝑄) ≠ 0)
185182, 183, 184divcan1d 11056 . . . . . . . . . . . . 13 (((𝐹𝑃) ≠ 0 ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ (𝐹𝑃) ≤ (𝐹𝑄)) → (((𝐹𝑃) / (𝐹𝑄)) · (𝐹𝑄)) = (𝐹𝑃))
186185eqcomd 2771 . . . . . . . . . . . 12 (((𝐹𝑃) ≠ 0 ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ (𝐹𝑃) ≤ (𝐹𝑄)) → (𝐹𝑃) = (((𝐹𝑃) / (𝐹𝑄)) · (𝐹𝑄)))
187 oveq1 6849 . . . . . . . . . . . . 13 (𝑡 = ((𝐹𝑃) / (𝐹𝑄)) → (𝑡 · (𝐹𝑄)) = (((𝐹𝑃) / (𝐹𝑄)) · (𝐹𝑄)))
188187rspceeqv 3479 . . . . . . . . . . . 12 ((((𝐹𝑃) / (𝐹𝑄)) ∈ (0[,]1) ∧ (𝐹𝑃) = (((𝐹𝑃) / (𝐹𝑄)) · (𝐹𝑄))) → ∃𝑡 ∈ (0[,]1)(𝐹𝑃) = (𝑡 · (𝐹𝑄)))
189181, 186, 188syl2anc 579 . . . . . . . . . . 11 (((𝐹𝑃) ≠ 0 ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ (𝐹𝑃) ≤ (𝐹𝑄)) → ∃𝑡 ∈ (0[,]1)(𝐹𝑃) = (𝑡 · (𝐹𝑄)))
1901893exp 1148 . . . . . . . . . 10 ((𝐹𝑃) ≠ 0 → (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) → ((𝐹𝑃) ≤ (𝐹𝑄) → ∃𝑡 ∈ (0[,]1)(𝐹𝑃) = (𝑡 · (𝐹𝑄)))))
191166, 190pm2.61ine 3020 . . . . . . . . 9 (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) → ((𝐹𝑃) ≤ (𝐹𝑄) → ∃𝑡 ∈ (0[,]1)(𝐹𝑃) = (𝑡 · (𝐹𝑄))))
192155, 191impbid 203 . . . . . . . 8 (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) → (∃𝑡 ∈ (0[,]1)(𝐹𝑃) = (𝑡 · (𝐹𝑄)) ↔ (𝐹𝑃) ≤ (𝐹𝑄)))
193192adantl 473 . . . . . . 7 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞))) → (∃𝑡 ∈ (0[,]1)(𝐹𝑃) = (𝑡 · (𝐹𝑄)) ↔ (𝐹𝑃) ≤ (𝐹𝑄)))
194141, 193bitrd 270 . . . . . 6 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞))) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))) ↔ (𝐹𝑃) ≤ (𝐹𝑄)))
19526, 194sylan9bbr 506 . . . . 5 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞))) ∧ ∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑄𝑖))) ↔ (𝐹𝑃) ≤ (𝐹𝑄)))
196195anasss 458 . . . 4 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞)) ∧ ∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))))) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑄𝑖))) ↔ (𝐹𝑃) ≤ (𝐹𝑄)))
19718, 196sylan2b 587 . . 3 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) ∧ ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))))) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑄𝑖))) ↔ (𝐹𝑃) ≤ (𝐹𝑄)))
19814, 197syldan 585 . 2 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷)) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑄𝑖))) ↔ (𝐹𝑃) ≤ (𝐹𝑄)))
19910, 198bitrd 270 1 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷)) → (𝑃 Btwn ⟨𝑍, 𝑄⟩ ↔ (𝐹𝑃) ≤ (𝐹𝑄)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 873  w3a 1107   = wceq 1652  wcel 2155  wne 2937  wral 3055  wrex 3056  {crab 3059  cop 4340   class class class wbr 4809  {copab 4871  cfv 6068  (class class class)co 6842  cc 10187  cr 10188  0cc0 10189  1c1 10190   + caddc 10192   · cmul 10194  +∞cpnf 10325   < clt 10328  cle 10329  cmin 10520   / cdiv 10938  cn 11274  [,)cico 12379  [,]cicc 12380  ...cfz 12533  𝔼cee 26059   Btwn cbtwn 26060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-er 7947  df-map 8062  df-en 8161  df-dom 8162  df-sdom 8163  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-z 11625  df-uz 11887  df-ico 12383  df-icc 12384  df-fz 12534  df-ee 26062  df-btwn 26063
This theorem is referenced by:  axcontlem9  26143
  Copyright terms: Public domain W3C validator