Step | Hyp | Ref
| Expression |
1 | | opeq2 4341 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑥 → 〈𝑍, 𝑝〉 = 〈𝑍, 𝑥〉) |
2 | 1 | breq2d 4595 |
. . . . . . . . 9
⊢ (𝑝 = 𝑥 → (𝑈 Btwn 〈𝑍, 𝑝〉 ↔ 𝑈 Btwn 〈𝑍, 𝑥〉)) |
3 | | breq1 4586 |
. . . . . . . . 9
⊢ (𝑝 = 𝑥 → (𝑝 Btwn 〈𝑍, 𝑈〉 ↔ 𝑥 Btwn 〈𝑍, 𝑈〉)) |
4 | 2, 3 | orbi12d 742 |
. . . . . . . 8
⊢ (𝑝 = 𝑥 → ((𝑈 Btwn 〈𝑍, 𝑝〉 ∨ 𝑝 Btwn 〈𝑍, 𝑈〉) ↔ (𝑈 Btwn 〈𝑍, 𝑥〉 ∨ 𝑥 Btwn 〈𝑍, 𝑈〉))) |
5 | | axcontlem2.1 |
. . . . . . . 8
⊢ 𝐷 = {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn 〈𝑍, 𝑝〉 ∨ 𝑝 Btwn 〈𝑍, 𝑈〉)} |
6 | 4, 5 | elrab2 3333 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑈 Btwn 〈𝑍, 𝑥〉 ∨ 𝑥 Btwn 〈𝑍, 𝑈〉))) |
7 | | simpll3 1095 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑈 ∈ (𝔼‘𝑁)) |
8 | | simpll2 1094 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑍 ∈ (𝔼‘𝑁)) |
9 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (𝔼‘𝑁)) |
10 | | brbtwn 25579 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑈 Btwn 〈𝑍, 𝑥〉 ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))) |
11 | 7, 8, 9, 10 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑈 Btwn 〈𝑍, 𝑥〉 ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))) |
12 | 11 | biimpa 500 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑈 Btwn 〈𝑍, 𝑥〉) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) |
13 | | simp-4r 803 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) → 𝑍 ≠ 𝑈) |
14 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑠 = 0 → (1 − 𝑠) = (1 −
0)) |
15 | | 1m0e1 11008 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1
− 0) = 1 |
16 | 14, 15 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 = 0 → (1 − 𝑠) = 1) |
17 | 16 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 = 0 → ((1 − 𝑠) · (𝑍‘𝑖)) = (1 · (𝑍‘𝑖))) |
18 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 = 0 → (𝑠 · (𝑥‘𝑖)) = (0 · (𝑥‘𝑖))) |
19 | 17, 18 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 = 0 → (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖)))) |
20 | 19 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 = 0 → ((𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) ↔ (𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))))) |
21 | 20 | ralbidv 2969 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = 0 → (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))))) |
22 | 21 | biimpac 502 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑖 ∈
(1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) ∧ 𝑠 = 0) → ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖)))) |
23 | | eqcom 2617 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑍 = 𝑈 ↔ 𝑈 = 𝑍) |
24 | 7 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → 𝑈 ∈ (𝔼‘𝑁)) |
25 | 8 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → 𝑍 ∈ (𝔼‘𝑁)) |
26 | | eqeefv 25583 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁)) → (𝑈 = 𝑍 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (𝑍‘𝑖))) |
27 | 24, 25, 26 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (𝑈 = 𝑍 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (𝑍‘𝑖))) |
28 | 8 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁)) |
29 | | fveecn 25582 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ) |
30 | 28, 29 | sylancom 698 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ) |
31 | | simpllr 795 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑥 ∈ (𝔼‘𝑁)) |
32 | | fveecn 25582 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℂ) |
33 | 31, 32 | sylancom 698 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℂ) |
34 | | mulid2 9917 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑍‘𝑖) ∈ ℂ → (1 · (𝑍‘𝑖)) = (𝑍‘𝑖)) |
35 | | mul02 10093 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥‘𝑖) ∈ ℂ → (0 · (𝑥‘𝑖)) = 0) |
36 | 34, 35 | oveqan12d 6568 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑍‘𝑖) ∈ ℂ ∧ (𝑥‘𝑖) ∈ ℂ) → ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))) = ((𝑍‘𝑖) + 0)) |
37 | | addid1 10095 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑍‘𝑖) ∈ ℂ → ((𝑍‘𝑖) + 0) = (𝑍‘𝑖)) |
38 | 37 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑍‘𝑖) ∈ ℂ ∧ (𝑥‘𝑖) ∈ ℂ) → ((𝑍‘𝑖) + 0) = (𝑍‘𝑖)) |
39 | 36, 38 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑍‘𝑖) ∈ ℂ ∧ (𝑥‘𝑖) ∈ ℂ) → ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))) = (𝑍‘𝑖)) |
40 | 39 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑍‘𝑖) ∈ ℂ ∧ (𝑥‘𝑖) ∈ ℂ) → ((𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))) ↔ (𝑈‘𝑖) = (𝑍‘𝑖))) |
41 | 30, 33, 40 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))) ↔ (𝑈‘𝑖) = (𝑍‘𝑖))) |
42 | 41 | ralbidva 2968 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (𝑍‘𝑖))) |
43 | 27, 42 | bitr4d 270 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (𝑈 = 𝑍 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))))) |
44 | 23, 43 | syl5bb 271 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = ((1 · (𝑍‘𝑖)) + (0 · (𝑥‘𝑖))))) |
45 | 22, 44 | syl5ibr 235 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) → ((∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) ∧ 𝑠 = 0) → 𝑍 = 𝑈)) |
46 | 45 | expdimp 452 |
. . . . . . . . . . . . . 14
⊢
((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) → (𝑠 = 0 → 𝑍 = 𝑈)) |
47 | 46 | necon3d 2803 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) → (𝑍 ≠ 𝑈 → 𝑠 ≠ 0)) |
48 | 13, 47 | mpd 15 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) → 𝑠 ≠ 0) |
49 | | 0re 9919 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 ∈
ℝ |
50 | | 1re 9918 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℝ |
51 | 49, 50 | elicc2i 12110 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 ∈ (0[,]1) ↔ (𝑠 ∈ ℝ ∧ 0 ≤
𝑠 ∧ 𝑠 ≤ 1)) |
52 | 51 | simp1bi 1069 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ (0[,]1) → 𝑠 ∈
ℝ) |
53 | | rereccl 10622 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑠 ∈ ℝ ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈
ℝ) |
54 | 52, 53 | sylan 487 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈
ℝ) |
55 | 52 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 𝑠 ∈
ℝ) |
56 | 51 | simp2bi 1070 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 ∈ (0[,]1) → 0 ≤
𝑠) |
57 | 56 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 0 ≤ 𝑠) |
58 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 𝑠 ≠ 0) |
59 | 55, 57, 58 | ne0gt0d 10053 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 0 < 𝑠) |
60 | | 0le1 10430 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ≤
1 |
61 | | divge0 10771 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((1
∈ ℝ ∧ 0 ≤ 1) ∧ (𝑠 ∈ ℝ ∧ 0 < 𝑠)) → 0 ≤ (1 / 𝑠)) |
62 | 50, 60, 61 | mpanl12 714 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑠 ∈ ℝ ∧ 0 <
𝑠) → 0 ≤ (1 / 𝑠)) |
63 | 55, 59, 62 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → 0 ≤ (1 /
𝑠)) |
64 | | elrege0 12149 |
. . . . . . . . . . . . . . . . 17
⊢ ((1 /
𝑠) ∈ (0[,)+∞)
↔ ((1 / 𝑠) ∈
ℝ ∧ 0 ≤ (1 / 𝑠))) |
65 | 54, 63, 64 | sylanbrc 695 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑠 ∈ (0[,]1) ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈
(0[,)+∞)) |
66 | 65 | adantll 746 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈ (0[,)+∞)) |
67 | 52 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℝ) |
68 | 67 | recnd 9947 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℂ) |
69 | | simplr 788 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ≠ 0) |
70 | | simp-4r 803 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑥 ∈ (𝔼‘𝑁)) |
71 | 70, 32 | sylancom 698 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℂ) |
72 | 8 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁)) |
73 | 72, 29 | sylancom 698 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ) |
74 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 ∈
ℂ |
75 | | reccl 10571 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (1 / 𝑠) ∈
ℂ) |
76 | | subcl 10159 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((1
∈ ℂ ∧ (1 / 𝑠) ∈ ℂ) → (1 − (1 /
𝑠)) ∈
ℂ) |
77 | 74, 75, 76 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (1 − (1 /
𝑠)) ∈
ℂ) |
78 | 77 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (1 − (1 /
𝑠)) ∈
ℂ) |
79 | | subcl 10159 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((1
∈ ℂ ∧ 𝑠
∈ ℂ) → (1 − 𝑠) ∈ ℂ) |
80 | 74, 79 | mpan 702 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑠 ∈ ℂ → (1
− 𝑠) ∈
ℂ) |
81 | 80 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (1 − 𝑠) ∈
ℂ) |
82 | 75, 81 | mulcld 9939 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · (1 − 𝑠)) ∈
ℂ) |
83 | 82 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 / 𝑠) · (1 − 𝑠)) ∈
ℂ) |
84 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (𝑍‘𝑖) ∈ ℂ) |
85 | 78, 83, 84 | adddird 9944 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 − (1 /
𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) · (𝑍‘𝑖)) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + (((1 / 𝑠) · (1 − 𝑠)) · (𝑍‘𝑖)))) |
86 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → 𝑠 ∈
ℂ) |
87 | | subdi 10342 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((1 /
𝑠) ∈ ℂ ∧ 1
∈ ℂ ∧ 𝑠
∈ ℂ) → ((1 / 𝑠) · (1 − 𝑠)) = (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠))) |
88 | 74, 87 | mp3an2 1404 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((1 /
𝑠) ∈ ℂ ∧
𝑠 ∈ ℂ) →
((1 / 𝑠) · (1
− 𝑠)) = (((1 / 𝑠) · 1) − ((1 /
𝑠) · 𝑠))) |
89 | 75, 86, 88 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · (1 − 𝑠)) = (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠))) |
90 | 89 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 /
𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) = ((1 − (1 / 𝑠)) + (((1 / 𝑠) · 1) − ((1 / 𝑠) · 𝑠)))) |
91 | 75 | mulid1d 9936 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · 1) = (1 / 𝑠)) |
92 | | recid2 10579 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 / 𝑠) · 𝑠) = 1) |
93 | 91, 92 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 / 𝑠) · 1) − ((1 /
𝑠) · 𝑠)) = ((1 / 𝑠) − 1)) |
94 | 93 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 /
𝑠)) + (((1 / 𝑠) · 1) − ((1 /
𝑠) · 𝑠))) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1))) |
95 | | addsubass 10170 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((1
− (1 / 𝑠)) ∈
ℂ ∧ (1 / 𝑠)
∈ ℂ ∧ 1 ∈ ℂ) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1))) |
96 | 74, 95 | mp3an3 1405 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((1
− (1 / 𝑠)) ∈
ℂ ∧ (1 / 𝑠)
∈ ℂ) → (((1 − (1 / 𝑠)) + (1 / 𝑠)) − 1) = ((1 − (1 / 𝑠)) + ((1 / 𝑠) − 1))) |
97 | 77, 75, 96 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 − (1
/ 𝑠)) + (1 / 𝑠)) − 1) = ((1 − (1 /
𝑠)) + ((1 / 𝑠) − 1))) |
98 | 77, 75 | addcld 9938 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 /
𝑠)) + (1 / 𝑠)) ∈
ℂ) |
99 | | npcan 10169 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((1
∈ ℂ ∧ (1 / 𝑠) ∈ ℂ) → ((1 − (1 /
𝑠)) + (1 / 𝑠)) = 1) |
100 | 74, 75, 99 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 /
𝑠)) + (1 / 𝑠)) = 1) |
101 | 98, 100 | subeq0bd 10335 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 − (1
/ 𝑠)) + (1 / 𝑠)) − 1) =
0) |
102 | 94, 97, 101 | 3eqtr2d 2650 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 /
𝑠)) + (((1 / 𝑠) · 1) − ((1 /
𝑠) · 𝑠))) = 0) |
103 | 90, 102 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → ((1 − (1 /
𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) = 0) |
104 | 103 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 − (1 /
𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) = 0) |
105 | 104 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 − (1 /
𝑠)) + ((1 / 𝑠) · (1 − 𝑠))) · (𝑍‘𝑖)) = (0 · (𝑍‘𝑖))) |
106 | 75 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (1 / 𝑠) ∈
ℂ) |
107 | 80 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (1 − 𝑠) ∈
ℂ) |
108 | 106, 107,
84 | mulassd 9942 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 / 𝑠) · (1 − 𝑠)) · (𝑍‘𝑖)) = ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))) |
109 | 108 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 − (1 /
𝑠)) · (𝑍‘𝑖)) + (((1 / 𝑠) · (1 − 𝑠)) · (𝑍‘𝑖))) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖))))) |
110 | 85, 105, 109 | 3eqtr3rd 2653 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 − (1 /
𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))) = (0 · (𝑍‘𝑖))) |
111 | | mul02 10093 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑍‘𝑖) ∈ ℂ → (0 · (𝑍‘𝑖)) = 0) |
112 | 111 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (0 · (𝑍‘𝑖)) = 0) |
113 | 110, 112 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 − (1 /
𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))) = 0) |
114 | | simpll 786 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → 𝑠 ∈ ℂ) |
115 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (𝑥‘𝑖) ∈ ℂ) |
116 | 106, 114,
115 | mulassd 9942 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 / 𝑠) · 𝑠) · (𝑥‘𝑖)) = ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖)))) |
117 | 92 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) → (((1 / 𝑠) · 𝑠) · (𝑥‘𝑖)) = (1 · (𝑥‘𝑖))) |
118 | | mulid2 9917 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥‘𝑖) ∈ ℂ → (1 · (𝑥‘𝑖)) = (𝑥‘𝑖)) |
119 | 118 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ) → (1 · (𝑥‘𝑖)) = (𝑥‘𝑖)) |
120 | 117, 119 | sylan9eq 2664 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 / 𝑠) · 𝑠) · (𝑥‘𝑖)) = (𝑥‘𝑖)) |
121 | 116, 120 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖))) = (𝑥‘𝑖)) |
122 | 113, 121 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((((1 − (1 /
𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))) + ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖)))) = (0 + (𝑥‘𝑖))) |
123 | 78, 84 | mulcld 9939 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 − (1 /
𝑠)) · (𝑍‘𝑖)) ∈ ℂ) |
124 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ) → (𝑍‘𝑖) ∈ ℂ) |
125 | | mulcl 9899 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((1
− 𝑠) ∈ ℂ
∧ (𝑍‘𝑖) ∈ ℂ) → ((1
− 𝑠) · (𝑍‘𝑖)) ∈ ℂ) |
126 | 81, 124, 125 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 − 𝑠) · (𝑍‘𝑖)) ∈ ℂ) |
127 | 106, 126 | mulcld 9939 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖))) ∈ ℂ) |
128 | | mulcl 9899 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑠 ∈ ℂ ∧ (𝑥‘𝑖) ∈ ℂ) → (𝑠 · (𝑥‘𝑖)) ∈ ℂ) |
129 | 128 | ad2ant2r 779 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (𝑠 · (𝑥‘𝑖)) ∈ ℂ) |
130 | 106, 129 | mulcld 9939 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖))) ∈ ℂ) |
131 | 123, 127,
130 | addassd 9941 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((((1 − (1 /
𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))) + ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖)))) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + (((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖))) + ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖)))))) |
132 | 106, 126,
129 | adddid 9943 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) = (((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖))) + ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖))))) |
133 | 132 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (((1 − (1 /
𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + (((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖))) + ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖)))))) |
134 | 131, 133 | eqtr4d 2647 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → ((((1 − (1 /
𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · ((1 − 𝑠) · (𝑍‘𝑖)))) + ((1 / 𝑠) · (𝑠 · (𝑥‘𝑖)))) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))) |
135 | | addid2 10098 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥‘𝑖) ∈ ℂ → (0 + (𝑥‘𝑖)) = (𝑥‘𝑖)) |
136 | 135 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (0 + (𝑥‘𝑖)) = (𝑥‘𝑖)) |
137 | 122, 134,
136 | 3eqtr3rd 2653 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑠 ∈ ℂ ∧ 𝑠 ≠ 0) ∧ ((𝑥‘𝑖) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ)) → (𝑥‘𝑖) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))) |
138 | 68, 69, 71, 73, 137 | syl22anc 1319 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))) |
139 | 138 | ralrimiva 2949 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))) |
140 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = (1 / 𝑠) → (1 − 𝑡) = (1 − (1 / 𝑠))) |
141 | 140 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = (1 / 𝑠) → ((1 − 𝑡) · (𝑍‘𝑖)) = ((1 − (1 / 𝑠)) · (𝑍‘𝑖))) |
142 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = (1 / 𝑠) → (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) = ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))) |
143 | 141, 142 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = (1 / 𝑠) → (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))) |
144 | 143 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (1 / 𝑠) → ((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))) ↔ (𝑥‘𝑖) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))) |
145 | 144 | ralbidv 2969 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = (1 / 𝑠) → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))) |
146 | 145 | rspcev 3282 |
. . . . . . . . . . . . . . 15
⊢ (((1 /
𝑠) ∈ (0[,)+∞)
∧ ∀𝑖 ∈
(1...𝑁)(𝑥‘𝑖) = (((1 − (1 / 𝑠)) · (𝑍‘𝑖)) + ((1 / 𝑠) · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))) |
147 | 66, 139, 146 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢
((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))) |
148 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → (𝑡 · (𝑈‘𝑖)) = (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))) |
149 | 148 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))) |
150 | 149 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → ((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))) |
151 | 150 | ralimi 2936 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑖 ∈
(1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → ∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))) |
152 | | ralbi 3050 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑖 ∈
(1...𝑁)((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))))) → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))) |
153 | 151, 152 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑖 ∈
(1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))) |
154 | 153 | rexbidv 3034 |
. . . . . . . . . . . . . 14
⊢
(∀𝑖 ∈
(1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → (∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))))))) |
155 | 147, 154 | syl5ibrcom 236 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ 𝑠 ≠ 0) → (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) |
156 | 155 | impancom 455 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) → (𝑠 ≠ 0 → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) |
157 | 48, 156 | mpd 15 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑠 ∈ (0[,]1)) ∧ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) |
158 | 157 | r19.29an 3059 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑥‘𝑖)))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) |
159 | 12, 158 | syldan 486 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑈 Btwn 〈𝑍, 𝑥〉) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) |
160 | | 3simpa 1051 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥 ∧ 𝑥 ≤ 1) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) |
161 | 49, 50 | elicc2i 12110 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (0[,]1) ↔ (𝑥 ∈ ℝ ∧ 0 ≤
𝑥 ∧ 𝑥 ≤ 1)) |
162 | | elrege0 12149 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (0[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 0
≤ 𝑥)) |
163 | 160, 161,
162 | 3imtr4i 280 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (0[,]1) → 𝑥 ∈
(0[,)+∞)) |
164 | 163 | ssriv 3572 |
. . . . . . . . . 10
⊢ (0[,]1)
⊆ (0[,)+∞) |
165 | | brbtwn 25579 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑥 Btwn 〈𝑍, 𝑈〉 ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) |
166 | 9, 8, 7, 165 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn 〈𝑍, 𝑈〉 ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) |
167 | 166 | biimpa 500 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑥 Btwn 〈𝑍, 𝑈〉) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) |
168 | | ssrexv 3630 |
. . . . . . . . . 10
⊢ ((0[,]1)
⊆ (0[,)+∞) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) |
169 | 164, 167,
168 | mpsyl 66 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ 𝑥 Btwn 〈𝑍, 𝑈〉) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) |
170 | 159, 169 | jaodan 822 |
. . . . . . . 8
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑈 Btwn 〈𝑍, 𝑥〉 ∨ 𝑥 Btwn 〈𝑍, 𝑈〉)) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) |
171 | 170 | anasss 677 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ (𝑈 Btwn 〈𝑍, 𝑥〉 ∨ 𝑥 Btwn 〈𝑍, 𝑈〉))) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) |
172 | 6, 171 | sylan2b 491 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ 𝐷) → ∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) |
173 | | r19.26 3046 |
. . . . . . . . . 10
⊢
(∀𝑖 ∈
(1...𝑁)((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))) |
174 | | eqtr2 2630 |
. . . . . . . . . . 11
⊢ (((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) |
175 | 174 | ralimi 2936 |
. . . . . . . . . 10
⊢
(∀𝑖 ∈
(1...𝑁)((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) |
176 | 173, 175 | sylbir 224 |
. . . . . . . . 9
⊢
((∀𝑖 ∈
(1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) |
177 | | elrege0 12149 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ (0[,)+∞) ↔
(𝑡 ∈ ℝ ∧ 0
≤ 𝑡)) |
178 | 177 | simplbi 475 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ (0[,)+∞) →
𝑡 ∈
ℝ) |
179 | 178 | recnd 9947 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ (0[,)+∞) →
𝑡 ∈
ℂ) |
180 | | elrege0 12149 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ (0[,)+∞) ↔
(𝑠 ∈ ℝ ∧ 0
≤ 𝑠)) |
181 | 180 | simplbi 475 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ (0[,)+∞) →
𝑠 ∈
ℝ) |
182 | 181 | recnd 9947 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (0[,)+∞) →
𝑠 ∈
ℂ) |
183 | 179, 182 | anim12i 588 |
. . . . . . . . . 10
⊢ ((𝑡 ∈ (0[,)+∞) ∧
𝑠 ∈ (0[,)+∞))
→ (𝑡 ∈ ℂ
∧ 𝑠 ∈
ℂ)) |
184 | | simplr 788 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) |
185 | | simpl2 1058 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → 𝑍 ∈ (𝔼‘𝑁)) |
186 | 185 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁)) |
187 | 186, 29 | sylancom 698 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ) |
188 | | simpl3 1059 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → 𝑈 ∈ (𝔼‘𝑁)) |
189 | 188 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁)) |
190 | | fveecn 25582 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) ∈ ℂ) |
191 | 189, 190 | sylancom 698 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) ∈ ℂ) |
192 | | subcl 10159 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1
∈ ℂ ∧ 𝑡
∈ ℂ) → (1 − 𝑡) ∈ ℂ) |
193 | 74, 192 | mpan 702 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 ∈ ℂ → (1
− 𝑡) ∈
ℂ) |
194 | 193 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1
− 𝑡) ∈
ℂ) |
195 | | simpl 472 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) → (𝑍‘𝑖) ∈ ℂ) |
196 | | mulcl 9899 |
. . . . . . . . . . . . . . . 16
⊢ (((1
− 𝑡) ∈ ℂ
∧ (𝑍‘𝑖) ∈ ℂ) → ((1
− 𝑡) · (𝑍‘𝑖)) ∈ ℂ) |
197 | 194, 195,
196 | syl2an 493 |
. . . . . . . . . . . . . . 15
⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − 𝑡) · (𝑍‘𝑖)) ∈ ℂ) |
198 | | mulcl 9899 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) → (𝑡 · (𝑈‘𝑖)) ∈ ℂ) |
199 | 198 | ad2ant2rl 781 |
. . . . . . . . . . . . . . 15
⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑡 · (𝑈‘𝑖)) ∈ ℂ) |
200 | 80 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1
− 𝑠) ∈
ℂ) |
201 | 200, 195,
125 | syl2an 493 |
. . . . . . . . . . . . . . 15
⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − 𝑠) · (𝑍‘𝑖)) ∈ ℂ) |
202 | | mulcl 9899 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑠 ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) → (𝑠 · (𝑈‘𝑖)) ∈ ℂ) |
203 | 202 | ad2ant2l 778 |
. . . . . . . . . . . . . . 15
⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑠 · (𝑈‘𝑖)) ∈ ℂ) |
204 | 197, 199,
201, 203 | addsubeq4d 10322 |
. . . . . . . . . . . . . 14
⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ (((1 − 𝑠) · (𝑍‘𝑖)) − ((1 − 𝑡) · (𝑍‘𝑖))) = ((𝑡 · (𝑈‘𝑖)) − (𝑠 · (𝑈‘𝑖))))) |
205 | | nnncan1 10196 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((1
∈ ℂ ∧ 𝑠
∈ ℂ ∧ 𝑡
∈ ℂ) → ((1 − 𝑠) − (1 − 𝑡)) = (𝑡 − 𝑠)) |
206 | 74, 205 | mp3an1 1403 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ) → ((1
− 𝑠) − (1
− 𝑡)) = (𝑡 − 𝑠)) |
207 | 206 | ancoms 468 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((1
− 𝑠) − (1
− 𝑡)) = (𝑡 − 𝑠)) |
208 | 207 | oveq1d 6564 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (((1
− 𝑠) − (1
− 𝑡)) · (𝑍‘𝑖)) = ((𝑡 − 𝑠) · (𝑍‘𝑖))) |
209 | 208 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − 𝑠) − (1 − 𝑡)) · (𝑍‘𝑖)) = ((𝑡 − 𝑠) · (𝑍‘𝑖))) |
210 | 80 | ad2antlr 759 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − 𝑠) ∈
ℂ) |
211 | 193 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − 𝑡) ∈
ℂ) |
212 | | simprl 790 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑍‘𝑖) ∈ ℂ) |
213 | 210, 211,
212 | subdird 10366 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − 𝑠) − (1 − 𝑡)) · (𝑍‘𝑖)) = (((1 − 𝑠) · (𝑍‘𝑖)) − ((1 − 𝑡) · (𝑍‘𝑖)))) |
214 | 209, 213 | eqtr3d 2646 |
. . . . . . . . . . . . . . 15
⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝑡 − 𝑠) · (𝑍‘𝑖)) = (((1 − 𝑠) · (𝑍‘𝑖)) − ((1 − 𝑡) · (𝑍‘𝑖)))) |
215 | | simpll 786 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → 𝑡 ∈ ℂ) |
216 | | simplr 788 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → 𝑠 ∈ ℂ) |
217 | | simprr 792 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑈‘𝑖) ∈ ℂ) |
218 | 215, 216,
217 | subdird 10366 |
. . . . . . . . . . . . . . 15
⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝑡 − 𝑠) · (𝑈‘𝑖)) = ((𝑡 · (𝑈‘𝑖)) − (𝑠 · (𝑈‘𝑖)))) |
219 | 214, 218 | eqeq12d 2625 |
. . . . . . . . . . . . . 14
⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝑡 − 𝑠) · (𝑍‘𝑖)) = ((𝑡 − 𝑠) · (𝑈‘𝑖)) ↔ (((1 − 𝑠) · (𝑍‘𝑖)) − ((1 − 𝑡) · (𝑍‘𝑖))) = ((𝑡 · (𝑈‘𝑖)) − (𝑠 · (𝑈‘𝑖))))) |
220 | | subcl 10159 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (𝑡 − 𝑠) ∈ ℂ) |
221 | 220 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑡 − 𝑠) ∈ ℂ) |
222 | | mulcan1g 10559 |
. . . . . . . . . . . . . . 15
⊢ (((𝑡 − 𝑠) ∈ ℂ ∧ (𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) → (((𝑡 − 𝑠) · (𝑍‘𝑖)) = ((𝑡 − 𝑠) · (𝑈‘𝑖)) ↔ ((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖)))) |
223 | 221, 212,
217, 222 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝑡 − 𝑠) · (𝑍‘𝑖)) = ((𝑡 − 𝑠) · (𝑈‘𝑖)) ↔ ((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖)))) |
224 | 204, 219,
223 | 3bitr2d 295 |
. . . . . . . . . . . . 13
⊢ (((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ ((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖)))) |
225 | 184, 187,
191, 224 | syl12anc 1316 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ ((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖)))) |
226 | 225 | ralbidva 2968 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖)))) |
227 | | r19.32v 3064 |
. . . . . . . . . . . 12
⊢
(∀𝑖 ∈
(1...𝑁)((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖)) ↔ ((𝑡 − 𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖))) |
228 | | simplr 788 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → 𝑍 ≠ 𝑈) |
229 | 228 | neneqd 2787 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → ¬ 𝑍 = 𝑈) |
230 | | simpll2 1094 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → 𝑍 ∈ (𝔼‘𝑁)) |
231 | | simpll3 1095 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → 𝑈 ∈ (𝔼‘𝑁)) |
232 | | eqeefv 25583 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖))) |
233 | 230, 231,
232 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (𝑍 = 𝑈 ↔ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖))) |
234 | 229, 233 | mtbid 313 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → ¬ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)) |
235 | | orel2 397 |
. . . . . . . . . . . . . 14
⊢ (¬
∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖) → (((𝑡 − 𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)) → (𝑡 − 𝑠) = 0)) |
236 | 234, 235 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (((𝑡 − 𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)) → (𝑡 − 𝑠) = 0)) |
237 | | subeq0 10186 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ) → ((𝑡 − 𝑠) = 0 ↔ 𝑡 = 𝑠)) |
238 | 237 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → ((𝑡 − 𝑠) = 0 ↔ 𝑡 = 𝑠)) |
239 | 236, 238 | sylibd 228 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (((𝑡 − 𝑠) = 0 ∨ ∀𝑖 ∈ (1...𝑁)(𝑍‘𝑖) = (𝑈‘𝑖)) → 𝑡 = 𝑠)) |
240 | 227, 239 | syl5bi 231 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (∀𝑖 ∈ (1...𝑁)((𝑡 − 𝑠) = 0 ∨ (𝑍‘𝑖) = (𝑈‘𝑖)) → 𝑡 = 𝑠)) |
241 | 226, 240 | sylbid 229 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ)) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) → 𝑡 = 𝑠)) |
242 | 183, 241 | sylan2 490 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ (0[,)+∞) ∧ 𝑠 ∈ (0[,)+∞))) →
(∀𝑖 ∈
(1...𝑁)(((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) → 𝑡 = 𝑠)) |
243 | 176, 242 | syl5 33 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑡 ∈ (0[,)+∞) ∧ 𝑠 ∈ (0[,)+∞))) →
((∀𝑖 ∈
(1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → 𝑡 = 𝑠)) |
244 | 243 | ralrimivva 2954 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → ∀𝑡 ∈ (0[,)+∞)∀𝑠 ∈
(0[,)+∞)((∀𝑖
∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → 𝑡 = 𝑠)) |
245 | 244 | adantr 480 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ 𝐷) → ∀𝑡 ∈ (0[,)+∞)∀𝑠 ∈
(0[,)+∞)((∀𝑖
∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → 𝑡 = 𝑠)) |
246 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑠 → (1 − 𝑡) = (1 − 𝑠)) |
247 | 246 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑠 → ((1 − 𝑡) · (𝑍‘𝑖)) = ((1 − 𝑠) · (𝑍‘𝑖))) |
248 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑠 → (𝑡 · (𝑈‘𝑖)) = (𝑠 · (𝑈‘𝑖))) |
249 | 247, 248 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝑡 = 𝑠 → (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) |
250 | 249 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑡 = 𝑠 → ((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))) |
251 | 250 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑡 = 𝑠 → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))) |
252 | 251 | reu4 3367 |
. . . . . 6
⊢
(∃!𝑡 ∈
(0[,)+∞)∀𝑖
∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (∃𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑡 ∈ (0[,)+∞)∀𝑠 ∈
(0[,)+∞)((∀𝑖
∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) → 𝑡 = 𝑠))) |
253 | 172, 245,
252 | sylanbrc 695 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ 𝐷) → ∃!𝑡 ∈ (0[,)+∞)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) |
254 | | df-reu 2903 |
. . . . 5
⊢
(∃!𝑡 ∈
(0[,)+∞)∀𝑖
∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) |
255 | 253, 254 | sylib 207 |
. . . 4
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑥 ∈ 𝐷) → ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) |
256 | 255 | ralrimiva 2949 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → ∀𝑥 ∈ 𝐷 ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) |
257 | | axcontlem2.2 |
. . . 4
⊢ 𝐹 = {〈𝑥, 𝑡〉 ∣ (𝑥 ∈ 𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))} |
258 | 257 | fnopabg 5930 |
. . 3
⊢
(∀𝑥 ∈
𝐷 ∃!𝑡(𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) ↔ 𝐹 Fn 𝐷) |
259 | 256, 258 | sylib 207 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → 𝐹 Fn 𝐷) |
260 | 178 | ad2antlr 759 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → 𝑡 ∈ ℝ) |
261 | 185 | ad2antrr 758 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁)) |
262 | | fveere 25581 |
. . . . . . . . . . 11
⊢ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝑍‘𝑘) ∈ ℝ) |
263 | 261, 262 | sylancom 698 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → (𝑍‘𝑘) ∈ ℝ) |
264 | 188 | ad2antrr 758 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁)) |
265 | | fveere 25581 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝑈‘𝑘) ∈ ℝ) |
266 | 264, 265 | sylancom 698 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → (𝑈‘𝑘) ∈ ℝ) |
267 | | resubcl 10224 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ ℝ ∧ 𝑡
∈ ℝ) → (1 − 𝑡) ∈ ℝ) |
268 | 50, 267 | mpan 702 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ ℝ → (1
− 𝑡) ∈
ℝ) |
269 | | remulcl 9900 |
. . . . . . . . . . . . 13
⊢ (((1
− 𝑡) ∈ ℝ
∧ (𝑍‘𝑘) ∈ ℝ) → ((1
− 𝑡) · (𝑍‘𝑘)) ∈ ℝ) |
270 | 268, 269 | sylan 487 |
. . . . . . . . . . . 12
⊢ ((𝑡 ∈ ℝ ∧ (𝑍‘𝑘) ∈ ℝ) → ((1 − 𝑡) · (𝑍‘𝑘)) ∈ ℝ) |
271 | 270 | 3adant3 1074 |
. . . . . . . . . . 11
⊢ ((𝑡 ∈ ℝ ∧ (𝑍‘𝑘) ∈ ℝ ∧ (𝑈‘𝑘) ∈ ℝ) → ((1 − 𝑡) · (𝑍‘𝑘)) ∈ ℝ) |
272 | | remulcl 9900 |
. . . . . . . . . . . 12
⊢ ((𝑡 ∈ ℝ ∧ (𝑈‘𝑘) ∈ ℝ) → (𝑡 · (𝑈‘𝑘)) ∈ ℝ) |
273 | 272 | 3adant2 1073 |
. . . . . . . . . . 11
⊢ ((𝑡 ∈ ℝ ∧ (𝑍‘𝑘) ∈ ℝ ∧ (𝑈‘𝑘) ∈ ℝ) → (𝑡 · (𝑈‘𝑘)) ∈ ℝ) |
274 | 271, 273 | readdcld 9948 |
. . . . . . . . . 10
⊢ ((𝑡 ∈ ℝ ∧ (𝑍‘𝑘) ∈ ℝ ∧ (𝑈‘𝑘) ∈ ℝ) → (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))) ∈ ℝ) |
275 | 260, 263,
266, 274 | syl3anc 1318 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑘 ∈ (1...𝑁)) → (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))) ∈ ℝ) |
276 | 275 | ralrimiva 2949 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∀𝑘 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))) ∈ ℝ) |
277 | | simpll1 1093 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → 𝑁 ∈
ℕ) |
278 | | mptelee 25575 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))) ∈ ℝ)) |
279 | 277, 278 | syl 17 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))) ∈ ℝ)) |
280 | 276, 279 | mpbird 246 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁)) |
281 | | letric 10016 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ 𝑡
∈ ℝ) → (1 ≤ 𝑡 ∨ 𝑡 ≤ 1)) |
282 | 50, 178, 281 | sylancr 694 |
. . . . . . . . 9
⊢ (𝑡 ∈ (0[,)+∞) → (1
≤ 𝑡 ∨ 𝑡 ≤ 1)) |
283 | 282 | adantl 481 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (1 ≤ 𝑡 ∨ 𝑡 ≤ 1)) |
284 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1
≤ 𝑡) → 1 ≤ 𝑡) |
285 | 178 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1
≤ 𝑡) → 𝑡 ∈
ℝ) |
286 | | 0red 9920 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1
≤ 𝑡) → 0 ∈
ℝ) |
287 | | 1red 9934 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1
≤ 𝑡) → 1 ∈
ℝ) |
288 | | 0lt1 10429 |
. . . . . . . . . . . . . . . . 17
⊢ 0 <
1 |
289 | 288 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1
≤ 𝑡) → 0 <
1) |
290 | 286, 287,
285, 289, 284 | ltletrd 10076 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1
≤ 𝑡) → 0 < 𝑡) |
291 | | divelunit 12185 |
. . . . . . . . . . . . . . . 16
⊢ (((1
∈ ℝ ∧ 0 ≤ 1) ∧ (𝑡 ∈ ℝ ∧ 0 < 𝑡)) → ((1 / 𝑡) ∈ (0[,]1) ↔ 1 ≤
𝑡)) |
292 | 50, 60, 291 | mpanl12 714 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ ℝ ∧ 0 <
𝑡) → ((1 / 𝑡) ∈ (0[,]1) ↔ 1 ≤
𝑡)) |
293 | 285, 290,
292 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1
≤ 𝑡) → ((1 / 𝑡) ∈ (0[,]1) ↔ 1 ≤
𝑡)) |
294 | 284, 293 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1
≤ 𝑡) → (1 / 𝑡) ∈
(0[,]1)) |
295 | 294 | adantll 746 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → (1 / 𝑡) ∈ (0[,]1)) |
296 | 178 | ad3antlr 763 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℝ) |
297 | 296 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢
((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ) |
298 | 290 | gt0ne0d 10471 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ (0[,)+∞) ∧ 1
≤ 𝑡) → 𝑡 ≠ 0) |
299 | 298 | adantll 746 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑡 ≠ 0) |
300 | 299 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ≠ 0) |
301 | 185 | ad3antrrr 762 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁)) |
302 | 301, 29 | sylancom 698 |
. . . . . . . . . . . . . 14
⊢
((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ) |
303 | 188 | ad3antrrr 762 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁)) |
304 | 303, 190 | sylancom 698 |
. . . . . . . . . . . . . 14
⊢
((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) ∈ ℂ) |
305 | | reccl 10571 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 / 𝑡) ∈
ℂ) |
306 | 305 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 / 𝑡) ∈
ℂ) |
307 | 193 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 − 𝑡) ∈
ℂ) |
308 | 307, 195,
196 | syl2an 493 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − 𝑡) · (𝑍‘𝑖)) ∈ ℂ) |
309 | 198 | ad2ant2rl 781 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑡 · (𝑈‘𝑖)) ∈ ℂ) |
310 | 306, 308,
309 | adddid 9943 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) = (((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖))) + ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖))))) |
311 | 310 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (1 /
𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + (((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖))) + ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖)))))) |
312 | | subcl 10159 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1
∈ ℂ ∧ (1 / 𝑡) ∈ ℂ) → (1 − (1 /
𝑡)) ∈
ℂ) |
313 | 74, 305, 312 | sylancr 694 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 − (1 /
𝑡)) ∈
ℂ) |
314 | | mulcl 9899 |
. . . . . . . . . . . . . . . . 17
⊢ (((1
− (1 / 𝑡)) ∈
ℂ ∧ (𝑍‘𝑖) ∈ ℂ) → ((1 − (1 /
𝑡)) · (𝑍‘𝑖)) ∈ ℂ) |
315 | 313, 195,
314 | syl2an 493 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (1 /
𝑡)) · (𝑍‘𝑖)) ∈ ℂ) |
316 | 306, 308 | mulcld 9939 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖))) ∈ ℂ) |
317 | | recid2 10579 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · 𝑡) = 1) |
318 | 317 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (((1 / 𝑡) · 𝑡) · (𝑈‘𝑖)) = (1 · (𝑈‘𝑖))) |
319 | 318 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 / 𝑡) · 𝑡) · (𝑈‘𝑖)) = (1 · (𝑈‘𝑖))) |
320 | | simpll 786 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → 𝑡 ∈ ℂ) |
321 | | simprr 792 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑈‘𝑖) ∈ ℂ) |
322 | 306, 320,
321 | mulassd 9942 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 / 𝑡) · 𝑡) · (𝑈‘𝑖)) = ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖)))) |
323 | | mulid2 9917 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈‘𝑖) ∈ ℂ → (1 · (𝑈‘𝑖)) = (𝑈‘𝑖)) |
324 | 323 | ad2antll 761 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 · (𝑈‘𝑖)) = (𝑈‘𝑖)) |
325 | 319, 322,
324 | 3eqtr3d 2652 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖))) = (𝑈‘𝑖)) |
326 | 325, 321 | eqeltrd 2688 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖))) ∈ ℂ) |
327 | 315, 316,
326 | addassd 9941 |
. . . . . . . . . . . . . . 15
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (1 /
𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖)))) + ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖)))) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + (((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖))) + ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖)))))) |
328 | 313 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − (1 /
𝑡)) ∈
ℂ) |
329 | 305, 307 | mulcld 9939 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · (1 − 𝑡)) ∈
ℂ) |
330 | 329 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 / 𝑡) · (1 − 𝑡)) ∈
ℂ) |
331 | | simprl 790 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑍‘𝑖) ∈ ℂ) |
332 | 328, 330,
331 | adddird 9944 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (1 /
𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) · (𝑍‘𝑖)) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + (((1 / 𝑡) · (1 − 𝑡)) · (𝑍‘𝑖)))) |
333 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → 𝑡 ∈
ℂ) |
334 | | subdi 10342 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((1 /
𝑡) ∈ ℂ ∧ 1
∈ ℂ ∧ 𝑡
∈ ℂ) → ((1 / 𝑡) · (1 − 𝑡)) = (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡))) |
335 | 74, 334 | mp3an2 1404 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((1 /
𝑡) ∈ ℂ ∧
𝑡 ∈ ℂ) →
((1 / 𝑡) · (1
− 𝑡)) = (((1 / 𝑡) · 1) − ((1 /
𝑡) · 𝑡))) |
336 | 305, 333,
335 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · (1 − 𝑡)) = (((1 / 𝑡) · 1) − ((1 / 𝑡) · 𝑡))) |
337 | 305 | mulid1d 9936 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · 1) = (1 / 𝑡)) |
338 | 337, 317 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (((1 / 𝑡) · 1) − ((1 /
𝑡) · 𝑡)) = ((1 / 𝑡) − 1)) |
339 | 336, 338 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 / 𝑡) · (1 − 𝑡)) = ((1 / 𝑡) − 1)) |
340 | 339 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (1 /
𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) = ((1 − (1 / 𝑡)) + ((1 / 𝑡) − 1))) |
341 | | npncan2 10187 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
∈ ℂ ∧ (1 / 𝑡) ∈ ℂ) → ((1 − (1 /
𝑡)) + ((1 / 𝑡) − 1)) =
0) |
342 | 74, 305, 341 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (1 /
𝑡)) + ((1 / 𝑡) − 1)) =
0) |
343 | 340, 342 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → ((1 − (1 /
𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) = 0) |
344 | 343 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (1 /
𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) = 0) |
345 | 344 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (1 /
𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) · (𝑍‘𝑖)) = (0 · (𝑍‘𝑖))) |
346 | 111 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (0 · (𝑍‘𝑖)) = 0) |
347 | 345, 346 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (1 /
𝑡)) + ((1 / 𝑡) · (1 − 𝑡))) · (𝑍‘𝑖)) = 0) |
348 | 193 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − 𝑡) ∈
ℂ) |
349 | 306, 348,
331 | mulassd 9942 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 / 𝑡) · (1 − 𝑡)) · (𝑍‘𝑖)) = ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖)))) |
350 | 349 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (1 /
𝑡)) · (𝑍‘𝑖)) + (((1 / 𝑡) · (1 − 𝑡)) · (𝑍‘𝑖))) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖))))) |
351 | 332, 347,
350 | 3eqtr3rd 2653 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (1 /
𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖)))) = 0) |
352 | 351, 325 | oveq12d 6567 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (1 /
𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖)))) + ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖)))) = (0 + (𝑈‘𝑖))) |
353 | | addid2 10098 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈‘𝑖) ∈ ℂ → (0 + (𝑈‘𝑖)) = (𝑈‘𝑖)) |
354 | 353 | ad2antll 761 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (0 + (𝑈‘𝑖)) = (𝑈‘𝑖)) |
355 | 352, 354 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (1 /
𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((1 − 𝑡) · (𝑍‘𝑖)))) + ((1 / 𝑡) · (𝑡 · (𝑈‘𝑖)))) = (𝑈‘𝑖)) |
356 | 311, 327,
355 | 3eqtr2rd 2651 |
. . . . . . . . . . . . . 14
⊢ (((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))) |
357 | 297, 300,
302, 304, 356 | syl22anc 1319 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))) |
358 | 357 | ralrimiva 2949 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))) |
359 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 = (1 / 𝑡) → (1 − 𝑠) = (1 − (1 / 𝑡))) |
360 | 359 | oveq1d 6564 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = (1 / 𝑡) → ((1 − 𝑠) · (𝑍‘𝑖)) = ((1 − (1 / 𝑡)) · (𝑍‘𝑖))) |
361 | | oveq1 6556 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = (1 / 𝑡) → (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)) = ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) |
362 | 360, 361 | oveq12d 6567 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = (1 / 𝑡) → (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)))) |
363 | 362 | eqeq2d 2620 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 = (1 / 𝑡) → ((𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) ↔ (𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))))) |
364 | 363 | ralbidv 2969 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = (1 / 𝑡) → (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))))) |
365 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑖 → (𝑍‘𝑘) = (𝑍‘𝑖)) |
366 | 365 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑖 → ((1 − 𝑡) · (𝑍‘𝑘)) = ((1 − 𝑡) · (𝑍‘𝑖))) |
367 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑖 → (𝑈‘𝑘) = (𝑈‘𝑖)) |
368 | 367 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑖 → (𝑡 · (𝑈‘𝑘)) = (𝑡 · (𝑈‘𝑖))) |
369 | 366, 368 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑖 → (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) |
370 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) |
371 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((1
− 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∈ V |
372 | 369, 370,
371 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (1...𝑁) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) |
373 | 372 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (1...𝑁) → ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)) = ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) |
374 | 373 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (1...𝑁) → (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))) |
375 | 374 | eqeq2d 2620 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (1...𝑁) → ((𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) ↔ (𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))))) |
376 | 375 | ralbiia 2962 |
. . . . . . . . . . . . . 14
⊢
(∀𝑖 ∈
(1...𝑁)(𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))) |
377 | 364, 376 | syl6bb 275 |
. . . . . . . . . . . . 13
⊢ (𝑠 = (1 / 𝑡) → (∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))))) |
378 | 377 | rspcev 3282 |
. . . . . . . . . . . 12
⊢ (((1 /
𝑡) ∈ (0[,]1) ∧
∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − (1 / 𝑡)) · (𝑍‘𝑖)) + ((1 / 𝑡) · (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)))) |
379 | 295, 358,
378 | syl2anc 691 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)))) |
380 | 188 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑈 ∈ (𝔼‘𝑁)) |
381 | 185 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑍 ∈ (𝔼‘𝑁)) |
382 | 280 | adantr 480 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁)) |
383 | | brbtwn 25579 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁)) → (𝑈 Btwn 〈𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))〉 ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))))) |
384 | 380, 381,
382, 383 | syl3anc 1318 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → (𝑈 Btwn 〈𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))〉 ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑈‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖))))) |
385 | 379, 384 | mpbird 246 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 1 ≤ 𝑡) → 𝑈 Btwn 〈𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))〉) |
386 | 385 | ex 449 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (1 ≤ 𝑡 → 𝑈 Btwn 〈𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))〉)) |
387 | | simpll 786 |
. . . . . . . . . . . . . . 15
⊢ (((𝑡 ∈ ℝ ∧ 0 ≤
𝑡) ∧ 𝑡 ≤ 1) → 𝑡 ∈ ℝ) |
388 | | simplr 788 |
. . . . . . . . . . . . . . 15
⊢ (((𝑡 ∈ ℝ ∧ 0 ≤
𝑡) ∧ 𝑡 ≤ 1) → 0 ≤ 𝑡) |
389 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ (((𝑡 ∈ ℝ ∧ 0 ≤
𝑡) ∧ 𝑡 ≤ 1) → 𝑡 ≤ 1) |
390 | 387, 388,
389 | 3jca 1235 |
. . . . . . . . . . . . . 14
⊢ (((𝑡 ∈ ℝ ∧ 0 ≤
𝑡) ∧ 𝑡 ≤ 1) → (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ∧ 𝑡 ≤ 1)) |
391 | 177 | anbi1i 727 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ (0[,)+∞) ∧
𝑡 ≤ 1) ↔ ((𝑡 ∈ ℝ ∧ 0 ≤
𝑡) ∧ 𝑡 ≤ 1)) |
392 | 49, 50 | elicc2i 12110 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∈ (0[,]1) ↔ (𝑡 ∈ ℝ ∧ 0 ≤
𝑡 ∧ 𝑡 ≤ 1)) |
393 | 390, 391,
392 | 3imtr4i 280 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ (0[,)+∞) ∧
𝑡 ≤ 1) → 𝑡 ∈
(0[,]1)) |
394 | 393 | adantll 746 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → 𝑡 ∈
(0[,]1)) |
395 | 372 | rgen 2906 |
. . . . . . . . . . . 12
⊢
∀𝑖 ∈
(1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) |
396 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = 𝑡 → (1 − 𝑠) = (1 − 𝑡)) |
397 | 396 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = 𝑡 → ((1 − 𝑠) · (𝑍‘𝑖)) = ((1 − 𝑡) · (𝑍‘𝑖))) |
398 | | oveq1 6556 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = 𝑡 → (𝑠 · (𝑈‘𝑖)) = (𝑡 · (𝑈‘𝑖))) |
399 | 397, 398 | oveq12d 6567 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 = 𝑡 → (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) |
400 | 399 | eqeq2d 2620 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = 𝑡 → (((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) |
401 | 400 | ralbidv 2969 |
. . . . . . . . . . . . 13
⊢ (𝑠 = 𝑡 → (∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) |
402 | 401 | rspcev 3282 |
. . . . . . . . . . . 12
⊢ ((𝑡 ∈ (0[,]1) ∧
∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) |
403 | 394, 395,
402 | sylancl 693 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖)))) |
404 | 280 | adantr 480 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁)) |
405 | 185 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → 𝑍 ∈ (𝔼‘𝑁)) |
406 | 188 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → 𝑈 ∈ (𝔼‘𝑁)) |
407 | | brbtwn 25579 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁) ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn 〈𝑍, 𝑈〉 ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))) |
408 | 404, 405,
406, 407 | syl3anc 1318 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn 〈𝑍, 𝑈〉 ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑠) · (𝑍‘𝑖)) + (𝑠 · (𝑈‘𝑖))))) |
409 | 403, 408 | mpbird 246 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈
ℕ ∧ 𝑍 ∈
(𝔼‘𝑁) ∧
𝑈 ∈
(𝔼‘𝑁)) ∧
𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) ∧ 𝑡 ≤ 1) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn 〈𝑍, 𝑈〉) |
410 | 409 | ex 449 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑡 ≤ 1 → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn 〈𝑍, 𝑈〉)) |
411 | 386, 410 | orim12d 879 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ((1 ≤ 𝑡 ∨ 𝑡 ≤ 1) → (𝑈 Btwn 〈𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))〉 ∨ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn 〈𝑍, 𝑈〉))) |
412 | 283, 411 | mpd 15 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑈 Btwn 〈𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))〉 ∨ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn 〈𝑍, 𝑈〉)) |
413 | | opeq2 4341 |
. . . . . . . . . 10
⊢ (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → 〈𝑍, 𝑝〉 = 〈𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))〉) |
414 | 413 | breq2d 4595 |
. . . . . . . . 9
⊢ (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → (𝑈 Btwn 〈𝑍, 𝑝〉 ↔ 𝑈 Btwn 〈𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))〉)) |
415 | | breq1 4586 |
. . . . . . . . 9
⊢ (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → (𝑝 Btwn 〈𝑍, 𝑈〉 ↔ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn 〈𝑍, 𝑈〉)) |
416 | 414, 415 | orbi12d 742 |
. . . . . . . 8
⊢ (𝑝 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → ((𝑈 Btwn 〈𝑍, 𝑝〉 ∨ 𝑝 Btwn 〈𝑍, 𝑈〉) ↔ (𝑈 Btwn 〈𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))〉 ∨ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn 〈𝑍, 𝑈〉))) |
417 | 416, 5 | elrab2 3333 |
. . . . . . 7
⊢ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ 𝐷 ↔ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ (𝔼‘𝑁) ∧ (𝑈 Btwn 〈𝑍, (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))〉 ∨ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) Btwn 〈𝑍, 𝑈〉))) |
418 | 280, 412,
417 | sylanbrc 695 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ 𝐷) |
419 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → (𝑥‘𝑖) = ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖)) |
420 | 419 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → ((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) |
421 | 420 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) |
422 | 421 | rspcev 3282 |
. . . . . 6
⊢ (((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘)))) ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑡) · (𝑍‘𝑘)) + (𝑡 · (𝑈‘𝑘))))‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → ∃𝑥 ∈ 𝐷 ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) |
423 | 418, 395,
422 | sylancl 693 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∃𝑥 ∈ 𝐷 ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) |
424 | 6 | simplbi 475 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ (𝔼‘𝑁)) |
425 | | ssrab2 3650 |
. . . . . . . . . . 11
⊢ {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn 〈𝑍, 𝑝〉 ∨ 𝑝 Btwn 〈𝑍, 𝑈〉)} ⊆ (𝔼‘𝑁) |
426 | 5, 425 | eqsstri 3598 |
. . . . . . . . . 10
⊢ 𝐷 ⊆ (𝔼‘𝑁) |
427 | 426 | sseli 3564 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐷 → 𝑦 ∈ (𝔼‘𝑁)) |
428 | 424, 427 | anim12i 588 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) |
429 | | r19.26 3046 |
. . . . . . . . . 10
⊢
(∀𝑖 ∈
(1...𝑁)((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ (𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) |
430 | | eqtr3 2631 |
. . . . . . . . . . 11
⊢ (((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ (𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → (𝑥‘𝑖) = (𝑦‘𝑖)) |
431 | 430 | ralimi 2936 |
. . . . . . . . . 10
⊢
(∀𝑖 ∈
(1...𝑁)((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ (𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖)) |
432 | 429, 431 | sylbir 224 |
. . . . . . . . 9
⊢
((∀𝑖 ∈
(1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖)) |
433 | | eqeefv 25583 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (𝑥 = 𝑦 ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖))) |
434 | 433 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (𝑥 = 𝑦 ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖))) |
435 | 432, 434 | syl5ibr 235 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → 𝑥 = 𝑦)) |
436 | 428, 435 | sylan2 490 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → 𝑥 = 𝑦)) |
437 | 436 | ralrimivva 2954 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → 𝑥 = 𝑦)) |
438 | 437 | adantr 480 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → 𝑥 = 𝑦)) |
439 | | df-reu 2903 |
. . . . . 6
⊢
(∃!𝑥 ∈
𝐷 ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∃!𝑥(𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) |
440 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥‘𝑖) = (𝑦‘𝑖)) |
441 | 440 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) |
442 | 441 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) |
443 | 442 | reu4 3367 |
. . . . . 6
⊢
(∃!𝑥 ∈
𝐷 ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ↔ (∃𝑥 ∈ 𝐷 ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → 𝑥 = 𝑦))) |
444 | 439, 443 | bitr3i 265 |
. . . . 5
⊢
(∃!𝑥(𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) ↔ (∃𝑥 ∈ 𝐷 ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) → 𝑥 = 𝑦))) |
445 | 423, 438,
444 | sylanbrc 695 |
. . . 4
⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑡 ∈ (0[,)+∞)) → ∃!𝑥(𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) |
446 | 445 | ralrimiva 2949 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → ∀𝑡 ∈ (0[,)+∞)∃!𝑥(𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) |
447 | | an12 834 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖))))) ↔ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))) |
448 | 447 | opabbii 4649 |
. . . . . . 7
⊢
{〈𝑥, 𝑡〉 ∣ (𝑥 ∈ 𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))} = {〈𝑥, 𝑡〉 ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))} |
449 | 257, 448 | eqtri 2632 |
. . . . . 6
⊢ 𝐹 = {〈𝑥, 𝑡〉 ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))} |
450 | 449 | cnveqi 5219 |
. . . . 5
⊢ ◡𝐹 = ◡{〈𝑥, 𝑡〉 ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))} |
451 | | cnvopab 5452 |
. . . . 5
⊢ ◡{〈𝑥, 𝑡〉 ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))} = {〈𝑡, 𝑥〉 ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))} |
452 | 450, 451 | eqtri 2632 |
. . . 4
⊢ ◡𝐹 = {〈𝑡, 𝑥〉 ∣ (𝑡 ∈ (0[,)+∞) ∧ (𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))} |
453 | 452 | fnopabg 5930 |
. . 3
⊢
(∀𝑡 ∈
(0[,)+∞)∃!𝑥(𝑥 ∈ 𝐷 ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))) ↔ ◡𝐹 Fn (0[,)+∞)) |
454 | 446, 453 | sylib 207 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → ◡𝐹 Fn (0[,)+∞)) |
455 | | dff1o4 6058 |
. 2
⊢ (𝐹:𝐷–1-1-onto→(0[,)+∞) ↔ (𝐹 Fn 𝐷 ∧ ◡𝐹 Fn (0[,)+∞))) |
456 | 259, 454,
455 | sylanbrc 695 |
1
⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → 𝐹:𝐷–1-1-onto→(0[,)+∞)) |