Proof of Theorem axcontlem8
Step | Hyp | Ref
| Expression |
1 | | axcontlem8.1 |
. . . . . . . . 9
⊢ 𝐷 = {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn 〈𝑍, 𝑝〉 ∨ 𝑝 Btwn 〈𝑍, 𝑈〉)} |
2 | | axcontlem8.2 |
. . . . . . . . 9
⊢ 𝐹 = {〈𝑥, 𝑡〉 ∣ (𝑥 ∈ 𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))} |
3 | 1, 2 | axcontlem6 27065 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑃 ∈ 𝐷) → ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))) |
4 | 3 | ex 416 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → (𝑃 ∈ 𝐷 → ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))))) |
5 | 1, 2 | axcontlem6 27065 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑄 ∈ 𝐷) → ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))))) |
6 | 5 | ex 416 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → (𝑄 ∈ 𝐷 → ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))))) |
7 | 1, 2 | axcontlem6 27065 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑅 ∈ 𝐷) → ((𝐹‘𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) |
8 | 7 | ex 416 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → (𝑅 ∈ 𝐷 → ((𝐹‘𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) |
9 | 4, 6, 8 | 3anim123d 1445 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → ((𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷) → (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))) |
10 | 9 | imp 410 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) → (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) |
11 | 10 | adantr 484 |
. . . 4
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) |
12 | | 3an6 1448 |
. . . . 5
⊢ ((((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) ↔ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞)) ∧
(∀𝑖 ∈
(1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) |
13 | | 0elunit 13062 |
. . . . . . . . . . . 12
⊢ 0 ∈
(0[,]1) |
14 | | simplr1 1217 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → (𝐹‘𝑃) ∈ (0[,)+∞)) |
15 | 14 | ad2antlr 727 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) ∈ (0[,)+∞)) |
16 | | elrege0 13047 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑃) ∈ (0[,)+∞) ↔ ((𝐹‘𝑃) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑃))) |
17 | 16 | simplbi 501 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑃) ∈ (0[,)+∞) → (𝐹‘𝑃) ∈ ℝ) |
18 | 15, 17 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) ∈ ℝ) |
19 | 18 | recnd 10866 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) ∈ ℂ) |
20 | | simprrl 781 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) ≤ (𝐹‘𝑄)) |
21 | 20 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) ≤ (𝐹‘𝑄)) |
22 | | simprrr 782 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑄) ≤ (𝐹‘𝑅)) |
23 | | simpl 486 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) = (𝐹‘𝑅)) |
24 | 22, 23 | breqtrrd 5086 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑄) ≤ (𝐹‘𝑃)) |
25 | 24 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑄) ≤ (𝐹‘𝑃)) |
26 | | simplr2 1218 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → (𝐹‘𝑄) ∈ (0[,)+∞)) |
27 | 26 | ad2antlr 727 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑄) ∈ (0[,)+∞)) |
28 | | elrege0 13047 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑄) ∈ (0[,)+∞) ↔ ((𝐹‘𝑄) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑄))) |
29 | 28 | simplbi 501 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑄) ∈ (0[,)+∞) → (𝐹‘𝑄) ∈ ℝ) |
30 | 27, 29 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑄) ∈ ℝ) |
31 | 18, 30 | letri3d 10979 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐹‘𝑃) = (𝐹‘𝑄) ↔ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑃)))) |
32 | 21, 25, 31 | mpbir2and 713 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) = (𝐹‘𝑄)) |
33 | | simpll 767 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) = (𝐹‘𝑅)) |
34 | | simpll2 1215 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) → 𝑍 ∈ (𝔼‘𝑁)) |
35 | 34 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → 𝑍 ∈ (𝔼‘𝑁)) |
36 | 35 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁)) |
37 | | fveecn 26998 |
. . . . . . . . . . . . . . 15
⊢ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ) |
38 | 36, 37 | sylancom 591 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ) |
39 | | simpll3 1216 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) → 𝑈 ∈ (𝔼‘𝑁)) |
40 | 39 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → 𝑈 ∈ (𝔼‘𝑁)) |
41 | 40 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁)) |
42 | | fveecn 26998 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) ∈ ℂ) |
43 | 41, 42 | sylancom 591 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) ∈ ℂ) |
44 | | ax-1cn 10792 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ∈
ℂ |
45 | | simpl 486 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝐹‘𝑃) ∈ ℂ) |
46 | | subcl 11082 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1
∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ) → (1 − (𝐹‘𝑃)) ∈ ℂ) |
47 | 44, 45, 46 | sylancr 590 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − (𝐹‘𝑃)) ∈ ℂ) |
48 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑍‘𝑖) ∈ ℂ) |
49 | 47, 48 | mulcld 10858 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) ∈ ℂ) |
50 | | mulcl 10818 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐹‘𝑃) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) → ((𝐹‘𝑃) · (𝑈‘𝑖)) ∈ ℂ) |
51 | 50 | adantrl 716 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑃) · (𝑈‘𝑖)) ∈ ℂ) |
52 | 49, 51 | addcld 10857 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∈ ℂ) |
53 | 52 | mulid2d 10856 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 · (((1
− (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) |
54 | 52 | mul02d 11035 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (0 · (((1
− (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) = 0) |
55 | 53, 54 | oveq12d 7236 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 · (((1
− (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))) = ((((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) + 0)) |
56 | 52 | addid1d 11037 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 −
(𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) + 0) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) |
57 | 55, 56 | eqtr2d 2778 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))))) |
58 | 57 | 3adant2 1133 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝐹‘𝑃) = (𝐹‘𝑄) ∧ (𝐹‘𝑃) = (𝐹‘𝑅)) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))))) |
59 | | oveq2 7226 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑃) = (𝐹‘𝑄) → (1 − (𝐹‘𝑃)) = (1 − (𝐹‘𝑄))) |
60 | 59 | oveq1d 7233 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑃) = (𝐹‘𝑄) → ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) = ((1 − (𝐹‘𝑄)) · (𝑍‘𝑖))) |
61 | | oveq1 7225 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑃) = (𝐹‘𝑄) → ((𝐹‘𝑃) · (𝑈‘𝑖)) = ((𝐹‘𝑄) · (𝑈‘𝑖))) |
62 | 60, 61 | oveq12d 7236 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑃) = (𝐹‘𝑄) → (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))) |
63 | | oveq2 7226 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹‘𝑃) = (𝐹‘𝑅) → (1 − (𝐹‘𝑃)) = (1 − (𝐹‘𝑅))) |
64 | 63 | oveq1d 7233 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘𝑃) = (𝐹‘𝑅) → ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) = ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖))) |
65 | | oveq1 7225 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹‘𝑃) = (𝐹‘𝑅) → ((𝐹‘𝑃) · (𝑈‘𝑖)) = ((𝐹‘𝑅) · (𝑈‘𝑖))) |
66 | 64, 65 | oveq12d 7236 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑃) = (𝐹‘𝑅) → (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) |
67 | 66 | oveq2d 7234 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑃) = (𝐹‘𝑅) → (0 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) = (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) |
68 | 67 | oveq2d 7234 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑃) = (𝐹‘𝑅) → ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) |
69 | 62, 68 | eqeqan12d 2751 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹‘𝑃) = (𝐹‘𝑄) ∧ (𝐹‘𝑃) = (𝐹‘𝑅)) → ((((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))) ↔ (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))) |
70 | 69 | 3ad2ant2 1136 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝐹‘𝑃) = (𝐹‘𝑄) ∧ (𝐹‘𝑃) = (𝐹‘𝑅)) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 −
(𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))) ↔ (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))) |
71 | 58, 70 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝐹‘𝑃) = (𝐹‘𝑄) ∧ (𝐹‘𝑃) = (𝐹‘𝑅)) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) |
72 | 19, 32, 33, 38, 43, 71 | syl122anc 1381 |
. . . . . . . . . . . . 13
⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) |
73 | 72 | ralrimiva 3105 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) |
74 | | oveq2 7226 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = 0 → (1 − 𝑡) = (1 −
0)) |
75 | | 1m0e1 11956 |
. . . . . . . . . . . . . . . . . 18
⊢ (1
− 0) = 1 |
76 | 74, 75 | eqtrdi 2794 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = 0 → (1 − 𝑡) = 1) |
77 | 76 | oveq1d 7233 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 0 → ((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) = (1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))) |
78 | | oveq1 7225 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 0 → (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) = (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) |
79 | 77, 78 | oveq12d 7236 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 0 → (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) |
80 | 79 | eqeq2d 2748 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 0 → ((((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) ↔ (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))) |
81 | 80 | ralbidv 3118 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 0 → (∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))) |
82 | 81 | rspcev 3542 |
. . . . . . . . . . . 12
⊢ ((0
∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) |
83 | 13, 73, 82 | sylancr 590 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) |
84 | 83 | ex 416 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑃) = (𝐹‘𝑅) → (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))) |
85 | 26 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑄) ∈ (0[,)+∞)) |
86 | 85, 29 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑄) ∈ ℝ) |
87 | | simplr3 1219 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → (𝐹‘𝑅) ∈ (0[,)+∞)) |
88 | 87 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑅) ∈ (0[,)+∞)) |
89 | | elrege0 13047 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑅) ∈ (0[,)+∞) ↔ ((𝐹‘𝑅) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑅))) |
90 | 89 | simplbi 501 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑅) ∈ (0[,)+∞) → (𝐹‘𝑅) ∈ ℝ) |
91 | 88, 90 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑅) ∈ ℝ) |
92 | 14 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) ∈ (0[,)+∞)) |
93 | 92, 17 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) ∈ ℝ) |
94 | | simprrr 782 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑄) ≤ (𝐹‘𝑅)) |
95 | 86, 91, 93, 94 | lesub1dd 11453 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ((𝐹‘𝑄) − (𝐹‘𝑃)) ≤ ((𝐹‘𝑅) − (𝐹‘𝑃))) |
96 | 86, 93 | resubcld 11265 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ((𝐹‘𝑄) − (𝐹‘𝑃)) ∈ ℝ) |
97 | | simprrl 781 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) ≤ (𝐹‘𝑄)) |
98 | 86, 93 | subge0d 11427 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (0 ≤ ((𝐹‘𝑄) − (𝐹‘𝑃)) ↔ (𝐹‘𝑃) ≤ (𝐹‘𝑄))) |
99 | 97, 98 | mpbird 260 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → 0 ≤ ((𝐹‘𝑄) − (𝐹‘𝑃))) |
100 | 91, 93 | resubcld 11265 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ((𝐹‘𝑅) − (𝐹‘𝑃)) ∈ ℝ) |
101 | 93, 86, 91, 97, 94 | letrd 10994 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) ≤ (𝐹‘𝑅)) |
102 | | simpl 486 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) ≠ (𝐹‘𝑅)) |
103 | 102 | necomd 2996 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑅) ≠ (𝐹‘𝑃)) |
104 | 93, 91, 101, 103 | leneltd 10991 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) < (𝐹‘𝑅)) |
105 | 93, 91 | posdifd 11424 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ((𝐹‘𝑃) < (𝐹‘𝑅) ↔ 0 < ((𝐹‘𝑅) − (𝐹‘𝑃)))) |
106 | 104, 105 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → 0 < ((𝐹‘𝑅) − (𝐹‘𝑃))) |
107 | | divelunit 13087 |
. . . . . . . . . . . . . 14
⊢
(((((𝐹‘𝑄) − (𝐹‘𝑃)) ∈ ℝ ∧ 0 ≤ ((𝐹‘𝑄) − (𝐹‘𝑃))) ∧ (((𝐹‘𝑅) − (𝐹‘𝑃)) ∈ ℝ ∧ 0 < ((𝐹‘𝑅) − (𝐹‘𝑃)))) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) ∈ (0[,]1) ↔ ((𝐹‘𝑄) − (𝐹‘𝑃)) ≤ ((𝐹‘𝑅) − (𝐹‘𝑃)))) |
108 | 96, 99, 100, 106, 107 | syl22anc 839 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) ∈ (0[,]1) ↔ ((𝐹‘𝑄) − (𝐹‘𝑃)) ≤ ((𝐹‘𝑅) − (𝐹‘𝑃)))) |
109 | 95, 108 | mpbird 260 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) ∈ (0[,]1)) |
110 | 14 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) ∈ (0[,)+∞)) |
111 | 17 | recnd 10866 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑃) ∈ (0[,)+∞) → (𝐹‘𝑃) ∈ ℂ) |
112 | 110, 111 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) ∈ ℂ) |
113 | | simpll 767 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) ≠ (𝐹‘𝑅)) |
114 | 26 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑄) ∈ (0[,)+∞)) |
115 | 29 | recnd 10866 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑄) ∈ (0[,)+∞) → (𝐹‘𝑄) ∈ ℂ) |
116 | 114, 115 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑄) ∈ ℂ) |
117 | 87 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑅) ∈ (0[,)+∞)) |
118 | 90 | recnd 10866 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑅) ∈ (0[,)+∞) → (𝐹‘𝑅) ∈ ℂ) |
119 | 117, 118 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑅) ∈ ℂ) |
120 | 34 | ad2antrl 728 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → 𝑍 ∈ (𝔼‘𝑁)) |
121 | 120, 37 | sylan 583 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ) |
122 | 39 | ad2antrl 728 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → 𝑈 ∈ (𝔼‘𝑁)) |
123 | 122, 42 | sylan 583 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) ∈ ℂ) |
124 | | simp2r 1202 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝐹‘𝑅) ∈ ℂ) |
125 | | simp2l 1201 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝐹‘𝑄) ∈ ℂ) |
126 | 124, 125 | subcld 11194 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑅) − (𝐹‘𝑄)) ∈ ℂ) |
127 | | simp1l 1199 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝐹‘𝑃) ∈ ℂ) |
128 | 44, 127, 46 | sylancr 590 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − (𝐹‘𝑃)) ∈ ℂ) |
129 | 126, 128 | mulcld 10858 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) ∈ ℂ) |
130 | 125, 127 | subcld 11194 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑄) − (𝐹‘𝑃)) ∈ ℂ) |
131 | | subcl 11082 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((1
∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) → (1 − (𝐹‘𝑅)) ∈ ℂ) |
132 | 44, 124, 131 | sylancr 590 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − (𝐹‘𝑅)) ∈ ℂ) |
133 | 130, 132 | mulcld 10858 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) ∈ ℂ) |
134 | 124, 127 | subcld 11194 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑅) − (𝐹‘𝑃)) ∈ ℂ) |
135 | | simp1r 1200 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝐹‘𝑃) ≠ (𝐹‘𝑅)) |
136 | 135 | necomd 2996 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝐹‘𝑅) ≠ (𝐹‘𝑃)) |
137 | 124, 127,
136 | subne0d 11203 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑅) − (𝐹‘𝑃)) ≠ 0) |
138 | 129, 133,
134, 137 | divdird 11651 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅)))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) / ((𝐹‘𝑅) − (𝐹‘𝑃))))) |
139 | 134 | mulid1d 10855 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · 1) = ((𝐹‘𝑅) − (𝐹‘𝑃))) |
140 | 134, 125 | mulcomd 10859 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄)) = ((𝐹‘𝑄) · ((𝐹‘𝑅) − (𝐹‘𝑃)))) |
141 | 125, 124,
127 | subdid 11293 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑄) · ((𝐹‘𝑅) − (𝐹‘𝑃))) = (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃)))) |
142 | 140, 141 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄)) = (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃)))) |
143 | 139, 142 | oveq12d 7236 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄))) = (((𝐹‘𝑅) − (𝐹‘𝑃)) − (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))))) |
144 | | subdi 11270 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹‘𝑅) − (𝐹‘𝑃)) ∈ ℂ ∧ 1 ∈ ℂ
∧ (𝐹‘𝑄) ∈ ℂ) →
(((𝐹‘𝑅) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑄))) = ((((𝐹‘𝑅) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄)))) |
145 | 44, 144 | mp3an2 1451 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹‘𝑅) − (𝐹‘𝑃)) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑄))) = ((((𝐹‘𝑅) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄)))) |
146 | 134, 125,
145 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑄))) = ((((𝐹‘𝑅) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄)))) |
147 | | subdi 11270 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐹‘𝑅) − (𝐹‘𝑄)) ∈ ℂ ∧ 1 ∈ ℂ
∧ (𝐹‘𝑃) ∈ ℂ) →
(((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)))) |
148 | 44, 147 | mp3an2 1451 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐹‘𝑅) − (𝐹‘𝑄)) ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)))) |
149 | 126, 127,
148 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)))) |
150 | 126 | mulid1d 10855 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · 1) = ((𝐹‘𝑅) − (𝐹‘𝑄))) |
151 | 124, 125,
127 | subdird 11294 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) = (((𝐹‘𝑅) · (𝐹‘𝑃)) − ((𝐹‘𝑄) · (𝐹‘𝑃)))) |
152 | 124, 127 | mulcomd 10859 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑅) · (𝐹‘𝑃)) = ((𝐹‘𝑃) · (𝐹‘𝑅))) |
153 | 152 | oveq1d 7233 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) · (𝐹‘𝑃)) − ((𝐹‘𝑄) · (𝐹‘𝑃))) = (((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃)))) |
154 | 151, 153 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) = (((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃)))) |
155 | 150, 154 | oveq12d 7236 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃))) = (((𝐹‘𝑅) − (𝐹‘𝑄)) − (((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))))) |
156 | 149, 155 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) = (((𝐹‘𝑅) − (𝐹‘𝑄)) − (((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))))) |
157 | | subdi 11270 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐹‘𝑄) − (𝐹‘𝑃)) ∈ ℂ ∧ 1 ∈ ℂ
∧ (𝐹‘𝑅) ∈ ℂ) →
(((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅)))) |
158 | 44, 157 | mp3an2 1451 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐹‘𝑄) − (𝐹‘𝑃)) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅)))) |
159 | 130, 124,
158 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅)))) |
160 | 130 | mulid1d 10855 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · 1) = ((𝐹‘𝑄) − (𝐹‘𝑃))) |
161 | 125, 127,
124 | subdird 11294 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅)) = (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅)))) |
162 | 160, 161 | oveq12d 7236 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))) = (((𝐹‘𝑄) − (𝐹‘𝑃)) − (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅))))) |
163 | 159, 162 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) = (((𝐹‘𝑄) − (𝐹‘𝑃)) − (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅))))) |
164 | 156, 163 | oveq12d 7236 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅)))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) − (((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃)))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) − (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅)))))) |
165 | 127, 124 | mulcld 10858 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑃) · (𝐹‘𝑅)) ∈ ℂ) |
166 | 125, 127 | mulcld 10858 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑄) · (𝐹‘𝑃)) ∈ ℂ) |
167 | 165, 166 | subcld 11194 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))) ∈ ℂ) |
168 | | mulcl 10818 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) → ((𝐹‘𝑄) · (𝐹‘𝑅)) ∈ ℂ) |
169 | 168 | 3ad2ant2 1136 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑄) · (𝐹‘𝑅)) ∈ ℂ) |
170 | 169, 165 | subcld 11194 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅))) ∈ ℂ) |
171 | 126, 130,
167, 170 | addsub4d 11241 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) + ((𝐹‘𝑄) − (𝐹‘𝑃))) − ((((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))) + (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅))))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) − (((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃)))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) − (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅)))))) |
172 | 124, 125,
127 | npncand 11218 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) + ((𝐹‘𝑄) − (𝐹‘𝑃))) = ((𝐹‘𝑅) − (𝐹‘𝑃))) |
173 | 165, 166,
169 | npncan3d 11230 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))) + (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅)))) = (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃)))) |
174 | 172, 173 | oveq12d 7236 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) + ((𝐹‘𝑄) − (𝐹‘𝑃))) − ((((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))) + (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅))))) = (((𝐹‘𝑅) − (𝐹‘𝑃)) − (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))))) |
175 | 164, 171,
174 | 3eqtr2d 2783 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅)))) = (((𝐹‘𝑅) − (𝐹‘𝑃)) − (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))))) |
176 | 143, 146,
175 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑄))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))))) |
177 | 129, 133 | addcld 10857 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅)))) ∈ ℂ) |
178 | | subcl 11082 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((1
∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ) → (1 − (𝐹‘𝑄)) ∈ ℂ) |
179 | 44, 125, 178 | sylancr 590 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − (𝐹‘𝑄)) ∈ ℂ) |
180 | 177, 134,
179, 137 | divmuld 11635 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅)))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (1 − (𝐹‘𝑄)) ↔ (((𝐹‘𝑅) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑄))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅)))))) |
181 | 176, 180 | mpbird 260 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅)))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (1 − (𝐹‘𝑄))) |
182 | 126, 128,
134, 137 | div23d 11650 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑃)))) |
183 | 134, 130,
134, 137 | divsubdird 11652 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑃)) − ((𝐹‘𝑄) − (𝐹‘𝑃))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = ((((𝐹‘𝑅) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))))) |
184 | 124, 125,
127 | nnncan2d 11229 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) − ((𝐹‘𝑄) − (𝐹‘𝑃))) = ((𝐹‘𝑅) − (𝐹‘𝑄))) |
185 | 184 | oveq1d 7233 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑃)) − ((𝐹‘𝑄) − (𝐹‘𝑃))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (((𝐹‘𝑅) − (𝐹‘𝑄)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) |
186 | 134, 137 | dividd 11611 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = 1) |
187 | 186 | oveq1d 7233 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) = (1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))))) |
188 | 183, 185,
187 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))))) |
189 | 188 | oveq1d 7233 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑃))) = ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃)))) |
190 | 182, 189 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃)))) |
191 | 130, 132,
134, 137 | div23d 11650 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅)))) |
192 | 190, 191 | oveq12d 7236 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅))))) |
193 | 138, 181,
192 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − (𝐹‘𝑄)) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅))))) |
194 | 193 | oveq1d 7233 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) = ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅)))) · (𝑍‘𝑖))) |
195 | 126, 127 | mulcld 10858 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) ∈ ℂ) |
196 | 130, 124 | mulcld 10858 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅)) ∈ ℂ) |
197 | 195, 196,
134, 137 | divdird 11651 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅)) / ((𝐹‘𝑅) − (𝐹‘𝑃))))) |
198 | 154, 161 | oveq12d 7236 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))) = ((((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))) + (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅))))) |
199 | 173, 198,
142 | 3eqtr4rd 2788 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄)) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅)))) |
200 | 195, 196 | addcld 10857 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))) ∈ ℂ) |
201 | 200, 134,
125, 137 | divmuld 11635 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (𝐹‘𝑄) ↔ (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄)) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))))) |
202 | 199, 201 | mpbird 260 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (𝐹‘𝑄)) |
203 | 126, 127,
134, 137 | div23d 11650 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑃))) |
204 | 188 | oveq1d 7233 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑃)) = ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃))) |
205 | 203, 204 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃))) |
206 | 130, 124,
134, 137 | div23d 11650 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅))) |
207 | 205, 206 | oveq12d 7236 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅)))) |
208 | 197, 202,
207 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝐹‘𝑄) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅)))) |
209 | 208 | oveq1d 7233 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑄) · (𝑈‘𝑖)) = ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅))) · (𝑈‘𝑖))) |
210 | 194, 209 | oveq12d 7236 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅)))) · (𝑍‘𝑖)) + ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅))) · (𝑈‘𝑖)))) |
211 | 130, 134,
137 | divcld 11613 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) ∈ ℂ) |
212 | | subcl 11082 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1
∈ ℂ ∧ (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) ∈ ℂ) → (1 −
(((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) ∈ ℂ) |
213 | 44, 211, 212 | sylancr 590 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) ∈ ℂ) |
214 | | simp3l 1203 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑍‘𝑖) ∈ ℂ) |
215 | 128, 214 | mulcld 10858 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) ∈ ℂ) |
216 | 213, 215 | mulcld 10858 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 −
(((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) ∈ ℂ) |
217 | 132, 214 | mulcld 10858 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) ∈ ℂ) |
218 | 211, 217 | mulcld 10858 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖))) ∈ ℂ) |
219 | | simp3r 1204 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑈‘𝑖) ∈ ℂ) |
220 | 127, 219 | mulcld 10858 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑃) · (𝑈‘𝑖)) ∈ ℂ) |
221 | 213, 220 | mulcld 10858 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 −
(((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖))) ∈ ℂ) |
222 | 124, 219 | mulcld 10858 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑅) · (𝑈‘𝑖)) ∈ ℂ) |
223 | 211, 222 | mulcld 10858 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖))) ∈ ℂ) |
224 | 216, 218,
221, 223 | add4d 11065 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 −
(((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)))) + (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖))))) = ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) + ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖)))))) |
225 | 213, 128 | mulcld 10858 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 −
(((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) ∈ ℂ) |
226 | 211, 132 | mulcld 10858 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅))) ∈ ℂ) |
227 | 213, 128,
214 | mulassd 10861 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 −
(((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) · (𝑍‘𝑖)) = ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)))) |
228 | 211, 132,
214 | mulassd 10861 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅))) · (𝑍‘𝑖)) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)))) |
229 | 227, 228 | oveq12d 7236 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 −
(((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) · (𝑍‘𝑖)) + (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅))) · (𝑍‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖))))) |
230 | 225, 214,
226, 229 | joinlmuladdmuld 10865 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 −
(((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅)))) · (𝑍‘𝑖)) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖))))) |
231 | 213, 127 | mulcld 10858 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 −
(((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) ∈ ℂ) |
232 | 211, 124 | mulcld 10858 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅)) ∈ ℂ) |
233 | 213, 127,
219 | mulassd 10861 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 −
(((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) · (𝑈‘𝑖)) = ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖)))) |
234 | 211, 124,
219 | mulassd 10861 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅)) · (𝑈‘𝑖)) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖)))) |
235 | 233, 234 | oveq12d 7236 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 −
(((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) · (𝑈‘𝑖)) + (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅)) · (𝑈‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖))))) |
236 | 231, 219,
232, 235 | joinlmuladdmuld 10865 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 −
(((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅))) · (𝑈‘𝑖)) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖))))) |
237 | 230, 236 | oveq12d 7236 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((1 −
(((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅)))) · (𝑍‘𝑖)) + ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅))) · (𝑈‘𝑖))) = ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)))) + (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖)))))) |
238 | 213, 215,
220 | adddid 10862 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 −
(((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) + ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖))))) |
239 | 211, 217,
222 | adddid 10862 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) = (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖))))) |
240 | 238, 239 | oveq12d 7236 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 −
(((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) = ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) + ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖)))))) |
241 | 224, 237,
240 | 3eqtr4rd 2788 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 −
(((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) = (((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅)))) · (𝑍‘𝑖)) + ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅))) · (𝑈‘𝑖)))) |
242 | 210, 241 | eqtr4d 2780 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) |
243 | 112, 113,
116, 119, 121, 123, 242 | syl222anc 1388 |
. . . . . . . . . . . . 13
⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) |
244 | 243 | ralrimiva 3105 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) |
245 | | oveq2 7226 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) → (1 − 𝑡) = (1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))))) |
246 | 245 | oveq1d 7233 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) → ((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) = ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))) |
247 | | oveq1 7225 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) → (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) |
248 | 246, 247 | oveq12d 7236 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) → (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) |
249 | 248 | eqeq2d 2748 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) → ((((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) ↔ (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))) |
250 | 249 | ralbidv 3118 |
. . . . . . . . . . . . 13
⊢ (𝑡 = (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) → (∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))) |
251 | 250 | rspcev 3542 |
. . . . . . . . . . . 12
⊢
(((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) |
252 | 109, 244,
251 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) |
253 | 252 | ex 416 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑃) ≠ (𝐹‘𝑅) → (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))) |
254 | 84, 253 | pm2.61ine 3025 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) |
255 | | r19.26-3 3094 |
. . . . . . . . . 10
⊢
(∀𝑖 ∈
(1...𝑁)((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) |
256 | | simp2 1139 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))) |
257 | | oveq2 7226 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) → ((1 − 𝑡) · (𝑃‘𝑖)) = ((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))) |
258 | | oveq2 7226 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))) → (𝑡 · (𝑅‘𝑖)) = (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) |
259 | 257, 258 | oveqan12d 7237 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) |
260 | 259 | 3adant2 1133 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) |
261 | 256, 260 | eqeq12d 2753 |
. . . . . . . . . . . . . 14
⊢ (((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → ((𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))) ↔ (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))) |
262 | 261 | ralimi 3083 |
. . . . . . . . . . . . 13
⊢
(∀𝑖 ∈
(1...𝑁)((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)((𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))) ↔ (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))) |
263 | | ralbi 3090 |
. . . . . . . . . . . . 13
⊢
(∀𝑖 ∈
(1...𝑁)((𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))) ↔ (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) → (∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))) |
264 | 262, 263 | syl 17 |
. . . . . . . . . . . 12
⊢
(∀𝑖 ∈
(1...𝑁)((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → (∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))) |
265 | 264 | rexbidv 3221 |
. . . . . . . . . . 11
⊢
(∀𝑖 ∈
(1...𝑁)((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))) ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))) |
266 | 265 | biimprcd 253 |
. . . . . . . . . 10
⊢
(∃𝑡 ∈
(0[,]1)∀𝑖 ∈
(1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) → (∀𝑖 ∈ (1...𝑁)((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))))) |
267 | 255, 266 | syl5bir 246 |
. . . . . . . . 9
⊢
(∃𝑡 ∈
(0[,]1)∀𝑖 ∈
(1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) → ((∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))))) |
268 | 254, 267 | syl 17 |
. . . . . . . 8
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → ((∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))))) |
269 | 268 | an32s 652 |
. . . . . . 7
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) →
((∀𝑖 ∈
(1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))))) |
270 | 269 | expimpd 457 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → ((((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞)) ∧
(∀𝑖 ∈
(1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))))) |
271 | 270 | adantlr 715 |
. . . . 5
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → ((((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞)) ∧
(∀𝑖 ∈
(1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))))) |
272 | 12, 271 | syl5bi 245 |
. . . 4
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → ((((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))))) |
273 | 11, 272 | mpd 15 |
. . 3
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖)))) |
274 | | simpl1 1193 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → 𝑁 ∈ ℕ) |
275 | 1 | ssrab3 4000 |
. . . . . . . 8
⊢ 𝐷 ⊆ (𝔼‘𝑁) |
276 | 275 | sseli 3901 |
. . . . . . 7
⊢ (𝑄 ∈ 𝐷 → 𝑄 ∈ (𝔼‘𝑁)) |
277 | 275 | sseli 3901 |
. . . . . . 7
⊢ (𝑃 ∈ 𝐷 → 𝑃 ∈ (𝔼‘𝑁)) |
278 | 275 | sseli 3901 |
. . . . . . 7
⊢ (𝑅 ∈ 𝐷 → 𝑅 ∈ (𝔼‘𝑁)) |
279 | 276, 277,
278 | 3anim123i 1153 |
. . . . . 6
⊢ ((𝑄 ∈ 𝐷 ∧ 𝑃 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷) → (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) |
280 | 279 | 3com12 1125 |
. . . . 5
⊢ ((𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷) → (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) |
281 | | brbtwn 26995 |
. . . . . 6
⊢ ((𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) → (𝑄 Btwn 〈𝑃, 𝑅〉 ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))))) |
282 | 281 | adantl 485 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝑄 Btwn 〈𝑃, 𝑅〉 ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))))) |
283 | 274, 280,
282 | syl2an 599 |
. . . 4
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) → (𝑄 Btwn 〈𝑃, 𝑅〉 ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))))) |
284 | 283 | adantr 484 |
. . 3
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → (𝑄 Btwn 〈𝑃, 𝑅〉 ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))))) |
285 | 273, 284 | mpbird 260 |
. 2
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → 𝑄 Btwn 〈𝑃, 𝑅〉) |
286 | 285 | ex 416 |
1
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) → (((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)) → 𝑄 Btwn 〈𝑃, 𝑅〉)) |