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