Proof of Theorem eenglngeehlnmlem2
Step | Hyp | Ref
| Expression |
1 | | 0red 10979 |
. . . 4
⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ
↑m (1...𝑁))
∧ 𝑦 ∈ ((ℝ
↑m (1...𝑁))
∖ {𝑥})) ∧ 𝑝 ∈ (ℝ
↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → 0 ∈
ℝ) |
2 | | 1red 10977 |
. . . 4
⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ
↑m (1...𝑁))
∧ 𝑦 ∈ ((ℝ
↑m (1...𝑁))
∖ {𝑥})) ∧ 𝑝 ∈ (ℝ
↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → 1 ∈
ℝ) |
3 | | simpr 485 |
. . . 4
⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ
↑m (1...𝑁))
∧ 𝑦 ∈ ((ℝ
↑m (1...𝑁))
∖ {𝑥})) ∧ 𝑝 ∈ (ℝ
↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℝ) |
4 | | reorelicc 46025 |
. . . 4
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (𝑡 < 0 ∨ 𝑡 ∈ (0[,]1) ∨ 1 < 𝑡)) |
5 | 1, 2, 3, 4 | syl3anc 1370 |
. . 3
⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ
↑m (1...𝑁))
∧ 𝑦 ∈ ((ℝ
↑m (1...𝑁))
∖ {𝑥})) ∧ 𝑝 ∈ (ℝ
↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → (𝑡 < 0 ∨ 𝑡 ∈ (0[,]1) ∨ 1 < 𝑡)) |
6 | | 0xr 11023 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ* |
7 | 6 | a1i 11 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → 0 ∈
ℝ*) |
8 | | 1xr 11035 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ* |
9 | 8 | a1i 11 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → 1 ∈
ℝ*) |
10 | | simpl 483 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 ∈
ℝ) |
11 | 10 | recnd 11004 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 ∈
ℂ) |
12 | | 0red 10979 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 ∈
ℝ) |
13 | | 1red 10977 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 1 ∈
ℝ) |
14 | | simpr 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 < 0) |
15 | | 0lt1 11497 |
. . . . . . . . . . . . . . . . 17
⊢ 0 <
1 |
16 | 15 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 <
1) |
17 | 10, 12, 13, 14, 16 | lttrd 11136 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 < 1) |
18 | 10, 17 | ltned 11111 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 ≠ 1) |
19 | | 1subrec1sub 46020 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 1) → (1 − (1 /
(1 − 𝑡))) = (𝑡 / (𝑡 − 1))) |
20 | 11, 18, 19 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 /
(1 − 𝑡))) = (𝑡 / (𝑡 − 1))) |
21 | 10, 13 | resubcld 11403 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − 1) ∈
ℝ) |
22 | | 1cnd 10971 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 1 ∈
ℂ) |
23 | 11, 22, 18 | subne0d 11341 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − 1) ≠
0) |
24 | 10, 21, 23 | redivcld 11803 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 / (𝑡 − 1)) ∈ ℝ) |
25 | 24 | rexrd 11026 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 / (𝑡 − 1)) ∈
ℝ*) |
26 | 20, 25 | eqeltrd 2841 |
. . . . . . . . . . . 12
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 /
(1 − 𝑡))) ∈
ℝ*) |
27 | 26 | ad4ant23 750 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 − (1 / (1 − 𝑡))) ∈
ℝ*) |
28 | 10 | renegcld 11402 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → -𝑡 ∈
ℝ) |
29 | 10, 13 | sublt0d 11601 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − 1) < 0 ↔ 𝑡 < 1)) |
30 | 17, 29 | mpbird 256 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − 1) <
0) |
31 | 21, 30 | negelrpd 12763 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → -(𝑡 − 1) ∈
ℝ+) |
32 | 10, 12, 14 | ltled 11123 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 ≤ 0) |
33 | 10 | le0neg1d 11546 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 ≤ 0 ↔ 0 ≤ -𝑡)) |
34 | 32, 33 | mpbid 231 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 ≤ -𝑡) |
35 | 28, 31, 34 | divge0d 12811 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 ≤ (-𝑡 / -(𝑡 − 1))) |
36 | 21 | recnd 11004 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − 1) ∈
ℂ) |
37 | 11, 36, 23 | div2negd 11766 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (-𝑡 / -(𝑡 − 1)) = (𝑡 / (𝑡 − 1))) |
38 | 20, 37 | eqtr4d 2783 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 /
(1 − 𝑡))) = (-𝑡 / -(𝑡 − 1))) |
39 | 35, 38 | breqtrrd 5107 |
. . . . . . . . . . . 12
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 ≤ (1
− (1 / (1 − 𝑡)))) |
40 | 39 | ad4ant23 750 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → 0 ≤ (1 − (1 / (1 −
𝑡)))) |
41 | | 1red 10977 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → 1 ∈
ℝ) |
42 | 13, 10 | resubcld 11403 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − 𝑡) ∈
ℝ) |
43 | 10, 13 | posdifd 11562 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 < 1 ↔ 0 < (1 −
𝑡))) |
44 | 17, 43 | mpbid 231 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 < (1
− 𝑡)) |
45 | 42, 44 | elrpd 12768 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − 𝑡) ∈
ℝ+) |
46 | 45 | ad4ant23 750 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 − 𝑡) ∈
ℝ+) |
47 | 46 | rpreccld 12781 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 / (1 − 𝑡)) ∈
ℝ+) |
48 | 41, 47 | ltsubrpd 12803 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 − (1 / (1 − 𝑡))) < 1) |
49 | 7, 9, 27, 40, 48 | elicod 13128 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 − (1 / (1 − 𝑡))) ∈
(0[,)1)) |
50 | | oveq2 7279 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 = (1 − (1 / (1 −
𝑡))) → (1 −
𝑙) = (1 − (1 −
(1 / (1 − 𝑡))))) |
51 | 50 | oveq1d 7286 |
. . . . . . . . . . . . . 14
⊢ (𝑙 = (1 − (1 / (1 −
𝑡))) → ((1 −
𝑙) · (𝑝‘𝑖)) = ((1 − (1 − (1 / (1 −
𝑡)))) · (𝑝‘𝑖))) |
52 | | oveq1 7278 |
. . . . . . . . . . . . . 14
⊢ (𝑙 = (1 − (1 / (1 −
𝑡))) → (𝑙 · (𝑦‘𝑖)) = ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) |
53 | 51, 52 | oveq12d 7289 |
. . . . . . . . . . . . 13
⊢ (𝑙 = (1 − (1 / (1 −
𝑡))) → (((1 −
𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) = (((1 − (1 − (1 / (1 −
𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)))) |
54 | 53 | eqeq2d 2751 |
. . . . . . . . . . . 12
⊢ (𝑙 = (1 − (1 / (1 −
𝑡))) → ((𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − (1 − (1 / (1 −
𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))))) |
55 | 54 | ralbidv 3123 |
. . . . . . . . . . 11
⊢ (𝑙 = (1 − (1 / (1 −
𝑡))) → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − (1 − (1 / (1 −
𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))))) |
56 | 55 | adantl 482 |
. . . . . . . . . 10
⊢
(((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) ∧ 𝑙 = (1 − (1 / (1 − 𝑡)))) → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − (1 − (1 / (1 −
𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))))) |
57 | 22, 11 | subcld 11332 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − 𝑡) ∈
ℂ) |
58 | 10, 17 | gtned 11110 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 1 ≠ 𝑡) |
59 | 22, 11, 58 | subne0d 11341 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − 𝑡) ≠ 0) |
60 | 57, 59 | reccld 11744 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 / (1 −
𝑡)) ∈
ℂ) |
61 | 22, 60 | nncand 11337 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1
− (1 / (1 − 𝑡)))) = (1 / (1 − 𝑡))) |
62 | 61, 60 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1
− (1 / (1 − 𝑡)))) ∈ ℂ) |
63 | 22, 60 | subcld 11332 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 /
(1 − 𝑡))) ∈
ℂ) |
64 | 16 | gt0ne0d 11539 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 1 ≠
0) |
65 | 36, 11 | subeq0ad 11342 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 − 1) − 𝑡) = 0 ↔ (𝑡 − 1) = 𝑡)) |
66 | 11, 22, 11 | sub32d 11364 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − 1) − 𝑡) = ((𝑡 − 𝑡) − 1)) |
67 | 66 | eqeq1d 2742 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 − 1) − 𝑡) = 0 ↔ ((𝑡 − 𝑡) − 1) = 0)) |
68 | 11 | subidd 11320 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − 𝑡) = 0) |
69 | 68 | oveq1d 7286 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − 𝑡) − 1) = (0 −
1)) |
70 | 69 | eqeq1d 2742 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 − 𝑡) − 1) = 0 ↔ (0 − 1) =
0)) |
71 | | 0cnd 10969 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 0 ∈
ℂ) |
72 | 71, 22, 71 | subaddd 11350 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((0 − 1) =
0 ↔ (1 + 0) = 0)) |
73 | 22 | addid1d 11175 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 + 0) =
1) |
74 | 73 | eqeq1d 2742 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 + 0) = 0
↔ 1 = 0)) |
75 | 72, 74 | bitrd 278 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((0 − 1) =
0 ↔ 1 = 0)) |
76 | 67, 70, 75 | 3bitrd 305 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 − 1) − 𝑡) = 0 ↔ 1 =
0)) |
77 | 65, 76 | bitr3d 280 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − 1) = 𝑡 ↔ 1 = 0)) |
78 | 77 | necon3bid 2990 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − 1) ≠ 𝑡 ↔ 1 ≠
0)) |
79 | 64, 78 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − 1) ≠ 𝑡) |
80 | 20 | eqeq2d 2751 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 = (1 −
(1 / (1 − 𝑡))) ↔
1 = (𝑡 / (𝑡 − 1)))) |
81 | | eqcom 2747 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (1 =
(𝑡 / (𝑡 − 1)) ↔ (𝑡 / (𝑡 − 1)) = 1) |
82 | 11, 36, 22, 23 | divmuld 11773 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 / (𝑡 − 1)) = 1 ↔ ((𝑡 − 1) · 1) = 𝑡)) |
83 | 81, 82 | syl5bb 283 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 = (𝑡 / (𝑡 − 1)) ↔ ((𝑡 − 1) · 1) = 𝑡)) |
84 | 36 | mulid1d 10993 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − 1) · 1) = (𝑡 − 1)) |
85 | 84 | eqeq1d 2742 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 − 1) · 1) = 𝑡 ↔ (𝑡 − 1) = 𝑡)) |
86 | 80, 83, 85 | 3bitrd 305 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 = (1 −
(1 / (1 − 𝑡))) ↔
(𝑡 − 1) = 𝑡)) |
87 | 86 | necon3bid 2990 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 ≠ (1
− (1 / (1 − 𝑡))) ↔ (𝑡 − 1) ≠ 𝑡)) |
88 | 79, 87 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 1 ≠ (1
− (1 / (1 − 𝑡)))) |
89 | 22, 63, 88 | subne0d 11341 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1
− (1 / (1 − 𝑡)))) ≠ 0) |
90 | 61 | oveq1d 7286 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 − (1
− (1 / (1 − 𝑡)))) · (1 − 𝑡)) = ((1 / (1 − 𝑡)) · (1 − 𝑡))) |
91 | 57, 59 | recid2d 11747 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 / (1 −
𝑡)) · (1 −
𝑡)) = 1) |
92 | 90, 91 | eqtrd 2780 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 − (1
− (1 / (1 − 𝑡)))) · (1 − 𝑡)) = 1) |
93 | 62, 57, 89, 92 | mvllmuld 11807 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − 𝑡) = (1 / (1 − (1 −
(1 / (1 − 𝑡)))))) |
94 | 93 | ad4ant23 750 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑡) = (1 / (1 − (1 − (1 / (1
− 𝑡)))))) |
95 | 94 | oveq1d 7286 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑡) · (𝑥‘𝑖)) = ((1 / (1 − (1 − (1 / (1
− 𝑡))))) ·
(𝑥‘𝑖))) |
96 | 20 | oveq1d 7286 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 − (1 /
(1 − 𝑡))) − 1)
= ((𝑡 / (𝑡 − 1)) − 1)) |
97 | 20, 96 | oveq12d 7289 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 − (1 /
(1 − 𝑡))) / ((1
− (1 / (1 − 𝑡))) − 1)) = ((𝑡 / (𝑡 − 1)) / ((𝑡 / (𝑡 − 1)) − 1))) |
98 | | subdivcomb2 11671 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑡 ∈ ℂ ∧ 1 ∈
ℂ ∧ ((𝑡 −
1) ∈ ℂ ∧ (𝑡
− 1) ≠ 0)) → ((𝑡 − ((𝑡 − 1) · 1)) / (𝑡 − 1)) = ((𝑡 / (𝑡 − 1)) − 1)) |
99 | 11, 22, 36, 23, 98 | syl112anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − ((𝑡 − 1) · 1)) / (𝑡 − 1)) = ((𝑡 / (𝑡 − 1)) − 1)) |
100 | 84 | oveq2d 7287 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − ((𝑡 − 1) · 1)) = (𝑡 − (𝑡 − 1))) |
101 | 11, 22 | nncand 11337 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − (𝑡 − 1)) = 1) |
102 | 100, 101 | eqtrd 2780 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 − ((𝑡 − 1) · 1)) =
1) |
103 | 102 | oveq1d 7286 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 − ((𝑡 − 1) · 1)) / (𝑡 − 1)) = (1 / (𝑡 − 1))) |
104 | 99, 103 | eqtr3d 2782 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 / (𝑡 − 1)) − 1) = (1 / (𝑡 − 1))) |
105 | 104 | oveq1d 7286 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 / (𝑡 − 1)) − 1) · 𝑡) = ((1 / (𝑡 − 1)) · 𝑡)) |
106 | 11, 36, 23 | divrec2d 11755 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 / (𝑡 − 1)) = ((1 / (𝑡 − 1)) · 𝑡)) |
107 | 105, 106 | eqtr4d 2783 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 / (𝑡 − 1)) − 1) · 𝑡) = (𝑡 / (𝑡 − 1))) |
108 | 20, 63 | eqeltrrd 2842 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 / (𝑡 − 1)) ∈ ℂ) |
109 | 108, 22 | subcld 11332 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 / (𝑡 − 1)) − 1) ∈
ℂ) |
110 | 79 | necomd 3001 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 ≠ (𝑡 − 1)) |
111 | 11, 36, 23, 110 | divne1d 11762 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (𝑡 / (𝑡 − 1)) ≠ 1) |
112 | 108, 22, 111 | subne0d 11341 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 / (𝑡 − 1)) − 1) ≠
0) |
113 | 108, 109,
11, 112 | divmuld 11773 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (((𝑡 / (𝑡 − 1)) / ((𝑡 / (𝑡 − 1)) − 1)) = 𝑡 ↔ (((𝑡 / (𝑡 − 1)) − 1) · 𝑡) = (𝑡 / (𝑡 − 1)))) |
114 | 107, 113 | mpbird 256 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((𝑡 / (𝑡 − 1)) / ((𝑡 / (𝑡 − 1)) − 1)) = 𝑡) |
115 | 97, 114 | eqtr2d 2781 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → 𝑡 = ((1 − (1 / (1 −
𝑡))) / ((1 − (1 / (1
− 𝑡))) −
1))) |
116 | 115 | ad4ant23 750 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 = ((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1
− 𝑡))) −
1))) |
117 | 116 | oveq1d 7286 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 · (𝑦‘𝑖)) = (((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1
− 𝑡))) − 1))
· (𝑦‘𝑖))) |
118 | 95, 117 | oveq12d 7289 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) = (((1 / (1 − (1 − (1 / (1
− 𝑡))))) ·
(𝑥‘𝑖)) + (((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1
− 𝑡))) − 1))
· (𝑦‘𝑖)))) |
119 | 118 | eqeq2d 2751 |
. . . . . . . . . . . . . 14
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) ↔ (𝑝‘𝑖) = (((1 / (1 − (1 − (1 / (1
− 𝑡))))) ·
(𝑥‘𝑖)) + (((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1
− 𝑡))) − 1))
· (𝑦‘𝑖))))) |
120 | 119 | biimpd 228 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (𝑝‘𝑖) = (((1 / (1 − (1 − (1 / (1
− 𝑡))))) ·
(𝑥‘𝑖)) + (((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1
− 𝑡))) − 1))
· (𝑦‘𝑖))))) |
121 | | eqcom 2747 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥‘𝑖) = (((1 − (1 − (1 / (1 −
𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) ↔ (((1 − (1 − (1 / (1
− 𝑡)))) ·
(𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) = (𝑥‘𝑖)) |
122 | | elmapi 8620 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (ℝ
↑m (1...𝑁))
→ 𝑥:(1...𝑁)⟶ℝ) |
123 | 122 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ
↑m (1...𝑁))
∧ 𝑦 ∈ ((ℝ
↑m (1...𝑁))
∖ {𝑥})) → 𝑥:(1...𝑁)⟶ℝ) |
124 | 123 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ
↑m (1...𝑁))
∧ 𝑦 ∈ ((ℝ
↑m (1...𝑁))
∖ {𝑥})) ∧ 𝑝 ∈ (ℝ
↑m (1...𝑁))) → 𝑥:(1...𝑁)⟶ℝ) |
125 | 124 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) → 𝑥:(1...𝑁)⟶ℝ) |
126 | 125 | ffvelrnda 6958 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℝ) |
127 | 126 | recnd 11004 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℂ) |
128 | | 1cnd 10971 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → 1 ∈ ℂ) |
129 | 11 | ad4ant23 750 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ) |
130 | 128, 129 | subcld 11332 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑡) ∈ ℂ) |
131 | 58 | ad4ant23 750 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → 1 ≠ 𝑡) |
132 | 128, 129,
131 | subne0d 11341 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑡) ≠ 0) |
133 | 130, 132 | reccld 11744 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 / (1 − 𝑡)) ∈ ℂ) |
134 | 128, 133 | subcld 11332 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 − (1 / (1 − 𝑡))) ∈
ℂ) |
135 | | eldifi 4066 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ ((ℝ
↑m (1...𝑁))
∖ {𝑥}) → 𝑦 ∈ (ℝ
↑m (1...𝑁))) |
136 | | elmapi 8620 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ (ℝ
↑m (1...𝑁))
→ 𝑦:(1...𝑁)⟶ℝ) |
137 | 135, 136 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ ((ℝ
↑m (1...𝑁))
∖ {𝑥}) → 𝑦:(1...𝑁)⟶ℝ) |
138 | 137 | 3ad2ant3 1134 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ
↑m (1...𝑁))
∧ 𝑦 ∈ ((ℝ
↑m (1...𝑁))
∖ {𝑥})) → 𝑦:(1...𝑁)⟶ℝ) |
139 | 138 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ
↑m (1...𝑁))
∧ 𝑦 ∈ ((ℝ
↑m (1...𝑁))
∖ {𝑥})) ∧ 𝑝 ∈ (ℝ
↑m (1...𝑁))) → 𝑦:(1...𝑁)⟶ℝ) |
140 | 139 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) → 𝑦:(1...𝑁)⟶ℝ) |
141 | 140 | ffvelrnda 6958 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) ∈ ℝ) |
142 | 141 | recnd 11004 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) ∈ ℂ) |
143 | 134, 142 | mulcld 10996 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)) ∈ ℂ) |
144 | 62 | ad4ant23 750 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 − (1 − (1 / (1
− 𝑡)))) ∈
ℂ) |
145 | | elmapi 8620 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑝 ∈ (ℝ
↑m (1...𝑁))
→ 𝑝:(1...𝑁)⟶ℝ) |
146 | 145 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ
↑m (1...𝑁))
∧ 𝑦 ∈ ((ℝ
↑m (1...𝑁))
∖ {𝑥})) ∧ 𝑝 ∈ (ℝ
↑m (1...𝑁))) → 𝑝:(1...𝑁)⟶ℝ) |
147 | 146 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) → 𝑝:(1...𝑁)⟶ℝ) |
148 | 147 | ffvelrnda 6958 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑝‘𝑖) ∈ ℝ) |
149 | 148 | recnd 11004 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (𝑝‘𝑖) ∈ ℂ) |
150 | 144, 149 | mulcld 10996 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − (1 − (1 / (1
− 𝑡)))) ·
(𝑝‘𝑖)) ∈ ℂ) |
151 | 127, 143,
150 | subadd2d 11351 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) = ((1 − (1 − (1 / (1 −
𝑡)))) · (𝑝‘𝑖)) ↔ (((1 − (1 − (1 / (1
− 𝑡)))) ·
(𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) = (𝑥‘𝑖))) |
152 | 121, 151 | bitr4id 290 |
. . . . . . . . . . . . . 14
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) = (((1 − (1 − (1 / (1 −
𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) ↔ ((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) = ((1 − (1 − (1 / (1 −
𝑡)))) · (𝑝‘𝑖)))) |
153 | | eqcom 2747 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) = ((1 − (1 − (1 / (1 −
𝑡)))) · (𝑝‘𝑖)) ↔ ((1 − (1 − (1 / (1
− 𝑡)))) ·
(𝑝‘𝑖)) = ((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)))) |
154 | 127, 143 | subcld 11332 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) ∈ ℂ) |
155 | 89 | ad4ant23 750 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (1 − (1 − (1 / (1
− 𝑡)))) ≠
0) |
156 | 154, 144,
149, 155 | divmuld 11773 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) / (1 − (1 − (1 / (1 −
𝑡))))) = (𝑝‘𝑖) ↔ ((1 − (1 − (1 / (1
− 𝑡)))) ·
(𝑝‘𝑖)) = ((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))))) |
157 | | eqcom 2747 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) / (1 − (1 − (1 / (1 −
𝑡))))) = (𝑝‘𝑖) ↔ (𝑝‘𝑖) = (((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) / (1 − (1 − (1 / (1 −
𝑡)))))) |
158 | 127, 143,
144, 155 | divsubdird 11790 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) / (1 − (1 − (1 / (1 −
𝑡))))) = (((𝑥‘𝑖) / (1 − (1 − (1 / (1 −
𝑡))))) − (((1 −
(1 / (1 − 𝑡)))
· (𝑦‘𝑖)) / (1 − (1 − (1 /
(1 − 𝑡))))))) |
159 | 127, 144,
155 | divcld 11751 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) / (1 − (1 − (1 / (1 −
𝑡))))) ∈
ℂ) |
160 | 143, 144,
155 | divcld 11751 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)) / (1 − (1 − (1 / (1 −
𝑡))))) ∈
ℂ) |
161 | 159, 160 | negsubd 11338 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑥‘𝑖) / (1 − (1 − (1 / (1 −
𝑡))))) + -(((1 − (1 /
(1 − 𝑡))) ·
(𝑦‘𝑖)) / (1 − (1 − (1 / (1 −
𝑡)))))) = (((𝑥‘𝑖) / (1 − (1 − (1 / (1 −
𝑡))))) − (((1 −
(1 / (1 − 𝑡)))
· (𝑦‘𝑖)) / (1 − (1 − (1 /
(1 − 𝑡))))))) |
162 | 127, 144,
155 | divrec2d 11755 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) / (1 − (1 − (1 / (1 −
𝑡))))) = ((1 / (1 −
(1 − (1 / (1 − 𝑡))))) · (𝑥‘𝑖))) |
163 | 143, 144,
155 | divneg2d 11765 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → -(((1 − (1 / (1 −
𝑡))) · (𝑦‘𝑖)) / (1 − (1 − (1 / (1 −
𝑡))))) = (((1 − (1 /
(1 − 𝑡))) ·
(𝑦‘𝑖)) / -(1 − (1 − (1 / (1 −
𝑡)))))) |
164 | 128, 134 | negsubdi2d 11348 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → -(1 − (1 − (1 / (1
− 𝑡)))) = ((1 −
(1 / (1 − 𝑡)))
− 1)) |
165 | 164 | oveq2d 7287 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)) / -(1 − (1 − (1 / (1 −
𝑡))))) = (((1 − (1 /
(1 − 𝑡))) ·
(𝑦‘𝑖)) / ((1 − (1 / (1 − 𝑡))) −
1))) |
166 | 134, 128 | subcld 11332 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − (1 / (1 − 𝑡))) − 1) ∈
ℂ) |
167 | 88 | necomd 3001 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → (1 − (1 /
(1 − 𝑡))) ≠
1) |
168 | 63, 22, 167 | subne0d 11341 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑡 ∈ ℝ ∧ 𝑡 < 0) → ((1 − (1 /
(1 − 𝑡))) − 1)
≠ 0) |
169 | 168 | ad4ant23 750 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − (1 / (1 − 𝑡))) − 1) ≠
0) |
170 | 134, 142,
166, 169 | div23d 11788 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)) / ((1 − (1 / (1 − 𝑡))) − 1)) = (((1 −
(1 / (1 − 𝑡))) / ((1
− (1 / (1 − 𝑡))) − 1)) · (𝑦‘𝑖))) |
171 | 163, 165,
170 | 3eqtrd 2784 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → -(((1 − (1 / (1 −
𝑡))) · (𝑦‘𝑖)) / (1 − (1 − (1 / (1 −
𝑡))))) = (((1 − (1 /
(1 − 𝑡))) / ((1
− (1 / (1 − 𝑡))) − 1)) · (𝑦‘𝑖))) |
172 | 162, 171 | oveq12d 7289 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑥‘𝑖) / (1 − (1 − (1 / (1 −
𝑡))))) + -(((1 − (1 /
(1 − 𝑡))) ·
(𝑦‘𝑖)) / (1 − (1 − (1 / (1 −
𝑡)))))) = (((1 / (1 −
(1 − (1 / (1 − 𝑡))))) · (𝑥‘𝑖)) + (((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1
− 𝑡))) − 1))
· (𝑦‘𝑖)))) |
173 | 158, 161,
172 | 3eqtr2d 2786 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) / (1 − (1 − (1 / (1 −
𝑡))))) = (((1 / (1 −
(1 − (1 / (1 − 𝑡))))) · (𝑥‘𝑖)) + (((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1
− 𝑡))) − 1))
· (𝑦‘𝑖)))) |
174 | 173 | eqeq2d 2751 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) / (1 − (1 − (1 / (1 −
𝑡))))) ↔ (𝑝‘𝑖) = (((1 / (1 − (1 − (1 / (1
− 𝑡))))) ·
(𝑥‘𝑖)) + (((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1
− 𝑡))) − 1))
· (𝑦‘𝑖))))) |
175 | 157, 174 | syl5bb 283 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) / (1 − (1 − (1 / (1 −
𝑡))))) = (𝑝‘𝑖) ↔ (𝑝‘𝑖) = (((1 / (1 − (1 − (1 / (1
− 𝑡))))) ·
(𝑥‘𝑖)) + (((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1
− 𝑡))) − 1))
· (𝑦‘𝑖))))) |
176 | 156, 175 | bitr3d 280 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (1 − (1 / (1
− 𝑡)))) ·
(𝑝‘𝑖)) = ((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) ↔ (𝑝‘𝑖) = (((1 / (1 − (1 − (1 / (1
− 𝑡))))) ·
(𝑥‘𝑖)) + (((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1
− 𝑡))) − 1))
· (𝑦‘𝑖))))) |
177 | 153, 176 | syl5bb 283 |
. . . . . . . . . . . . . 14
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑥‘𝑖) − ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) = ((1 − (1 − (1 / (1 −
𝑡)))) · (𝑝‘𝑖)) ↔ (𝑝‘𝑖) = (((1 / (1 − (1 − (1 / (1
− 𝑡))))) ·
(𝑥‘𝑖)) + (((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1
− 𝑡))) − 1))
· (𝑦‘𝑖))))) |
178 | 152, 177 | bitrd 278 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) = (((1 − (1 − (1 / (1 −
𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))) ↔ (𝑝‘𝑖) = (((1 / (1 − (1 − (1 / (1
− 𝑡))))) ·
(𝑥‘𝑖)) + (((1 − (1 / (1 − 𝑡))) / ((1 − (1 / (1
− 𝑡))) − 1))
· (𝑦‘𝑖))))) |
179 | 120, 178 | sylibrd 258 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (𝑥‘𝑖) = (((1 − (1 − (1 / (1 −
𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))))) |
180 | 179 | ralimdva 3105 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) → (∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − (1 − (1 / (1 −
𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖))))) |
181 | 180 | imp 407 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − (1 − (1 / (1 −
𝑡)))) · (𝑝‘𝑖)) + ((1 − (1 / (1 − 𝑡))) · (𝑦‘𝑖)))) |
182 | 49, 56, 181 | rspcedvd 3564 |
. . . . . . . . 9
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖)))) |
183 | 182 | 3mix2d 1336 |
. . . . . . . 8
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 < 0) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))) |
184 | 183 | exp31 420 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ
↑m (1...𝑁))
∧ 𝑦 ∈ ((ℝ
↑m (1...𝑁))
∖ {𝑥})) ∧ 𝑝 ∈ (ℝ
↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → (𝑡 < 0 → (∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))))) |
185 | 184 | com23 86 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ
↑m (1...𝑁))
∧ 𝑦 ∈ ((ℝ
↑m (1...𝑁))
∖ {𝑥})) ∧ 𝑝 ∈ (ℝ
↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → (∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (𝑡 < 0 → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))))) |
186 | 185 | imp 407 |
. . . . 5
⊢
(((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧
∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (𝑡 < 0 → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖)))))) |
187 | | simpr 485 |
. . . . . . . 8
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧
∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) ∧ 𝑡 ∈ (0[,]1)) → 𝑡 ∈ (0[,]1)) |
188 | | oveq2 7279 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑡 → (1 − 𝑘) = (1 − 𝑡)) |
189 | 188 | oveq1d 7286 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑡 → ((1 − 𝑘) · (𝑥‘𝑖)) = ((1 − 𝑡) · (𝑥‘𝑖))) |
190 | | oveq1 7278 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑡 → (𝑘 · (𝑦‘𝑖)) = (𝑡 · (𝑦‘𝑖))) |
191 | 189, 190 | oveq12d 7289 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑡 → (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) |
192 | 191 | eqeq2d 2751 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑡 → ((𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ↔ (𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))))) |
193 | 192 | ralbidv 3123 |
. . . . . . . . 9
⊢ (𝑘 = 𝑡 → (∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))))) |
194 | 193 | adantl 482 |
. . . . . . . 8
⊢
(((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧
∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) ∧ 𝑡 ∈ (0[,]1)) ∧ 𝑘 = 𝑡) → (∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))))) |
195 | | simplr 766 |
. . . . . . . 8
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧
∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) ∧ 𝑡 ∈ (0[,]1)) → ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) |
196 | 187, 194,
195 | rspcedvd 3564 |
. . . . . . 7
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧
∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) ∧ 𝑡 ∈ (0[,]1)) → ∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖)))) |
197 | 196 | 3mix1d 1335 |
. . . . . 6
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧
∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) ∧ 𝑡 ∈ (0[,]1)) → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))) |
198 | 197 | ex 413 |
. . . . 5
⊢
(((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧
∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (𝑡 ∈ (0[,]1) → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖)))))) |
199 | | 1red 10977 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ ℝ ∧ 1 <
𝑡) → 1 ∈
ℝ) |
200 | | simpl 483 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ ℝ ∧ 1 <
𝑡) → 𝑡 ∈
ℝ) |
201 | | 0red 10979 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ ℝ ∧ 1 <
𝑡) → 0 ∈
ℝ) |
202 | 15 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ ℝ ∧ 1 <
𝑡) → 0 <
1) |
203 | | simpr 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ ℝ ∧ 1 <
𝑡) → 1 < 𝑡) |
204 | 201, 199,
200, 202, 203 | lttrd 11136 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ ℝ ∧ 1 <
𝑡) → 0 < 𝑡) |
205 | 204 | gt0ne0d 11539 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ ℝ ∧ 1 <
𝑡) → 𝑡 ≠ 0) |
206 | 199, 200,
205 | redivcld 11803 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ ℝ ∧ 1 <
𝑡) → (1 / 𝑡) ∈
ℝ) |
207 | 200, 204 | recgt0d 11909 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ ℝ ∧ 1 <
𝑡) → 0 < (1 / 𝑡)) |
208 | | recgt1i 11872 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ ℝ ∧ 1 <
𝑡) → (0 < (1 /
𝑡) ∧ (1 / 𝑡) < 1)) |
209 | 206 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑡 ∈ ℝ ∧ 1 <
𝑡) ∧ (0 < (1 / 𝑡) ∧ (1 / 𝑡) < 1)) → (1 / 𝑡) ∈ ℝ) |
210 | | 1red 10977 |
. . . . . . . . . . . . . . 15
⊢ (((𝑡 ∈ ℝ ∧ 1 <
𝑡) ∧ (0 < (1 / 𝑡) ∧ (1 / 𝑡) < 1)) → 1 ∈
ℝ) |
211 | | simprr 770 |
. . . . . . . . . . . . . . 15
⊢ (((𝑡 ∈ ℝ ∧ 1 <
𝑡) ∧ (0 < (1 / 𝑡) ∧ (1 / 𝑡) < 1)) → (1 / 𝑡) < 1) |
212 | 209, 210,
211 | ltled 11123 |
. . . . . . . . . . . . . 14
⊢ (((𝑡 ∈ ℝ ∧ 1 <
𝑡) ∧ (0 < (1 / 𝑡) ∧ (1 / 𝑡) < 1)) → (1 / 𝑡) ≤ 1) |
213 | 208, 212 | mpdan 684 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ ℝ ∧ 1 <
𝑡) → (1 / 𝑡) ≤ 1) |
214 | 206, 207,
213 | 3jca 1127 |
. . . . . . . . . . . 12
⊢ ((𝑡 ∈ ℝ ∧ 1 <
𝑡) → ((1 / 𝑡) ∈ ℝ ∧ 0 < (1
/ 𝑡) ∧ (1 / 𝑡) ≤ 1)) |
215 | | 1re 10976 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ |
216 | 6, 215 | pm3.2i 471 |
. . . . . . . . . . . . 13
⊢ (0 ∈
ℝ* ∧ 1 ∈ ℝ) |
217 | | elioc2 13141 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ) → ((1 / 𝑡) ∈ (0(,]1) ↔ ((1 /
𝑡) ∈ ℝ ∧ 0
< (1 / 𝑡) ∧ (1 /
𝑡) ≤
1))) |
218 | 216, 217 | mp1i 13 |
. . . . . . . . . . . 12
⊢ ((𝑡 ∈ ℝ ∧ 1 <
𝑡) → ((1 / 𝑡) ∈ (0(,]1) ↔ ((1 /
𝑡) ∈ ℝ ∧ 0
< (1 / 𝑡) ∧ (1 /
𝑡) ≤
1))) |
219 | 214, 218 | mpbird 256 |
. . . . . . . . . . 11
⊢ ((𝑡 ∈ ℝ ∧ 1 <
𝑡) → (1 / 𝑡) ∈
(0(,]1)) |
220 | 219 | ad4ant23 750 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 / 𝑡) ∈ (0(,]1)) |
221 | | oveq2 7279 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = (1 / 𝑡) → (1 − 𝑚) = (1 − (1 / 𝑡))) |
222 | 221 | oveq1d 7286 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (1 / 𝑡) → ((1 − 𝑚) · (𝑥‘𝑖)) = ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) |
223 | | oveq1 7278 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (1 / 𝑡) → (𝑚 · (𝑝‘𝑖)) = ((1 / 𝑡) · (𝑝‘𝑖))) |
224 | 222, 223 | oveq12d 7289 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (1 / 𝑡) → (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖)))) |
225 | 224 | eqeq2d 2751 |
. . . . . . . . . . . 12
⊢ (𝑚 = (1 / 𝑡) → ((𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) ↔ (𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))))) |
226 | 225 | ralbidv 3123 |
. . . . . . . . . . 11
⊢ (𝑚 = (1 / 𝑡) → (∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))))) |
227 | 226 | adantl 482 |
. . . . . . . . . 10
⊢
(((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) ∧ 𝑚 = (1 / 𝑡)) → (∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))))) |
228 | | simplr 766 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) → 𝑡 ∈
ℝ) |
229 | 228 | recnd 11004 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) → 𝑡 ∈
ℂ) |
230 | 229 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ) |
231 | 204 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 ∈ ℝ → (1 <
𝑡 → 0 < 𝑡)) |
232 | | gt0ne0 11440 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑡 ∈ ℝ ∧ 0 <
𝑡) → 𝑡 ≠ 0) |
233 | 232 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 ∈ ℝ → (0 <
𝑡 → 𝑡 ≠ 0)) |
234 | 231, 233 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 ∈ ℝ → (1 <
𝑡 → 𝑡 ≠ 0)) |
235 | 234 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ
↑m (1...𝑁))
∧ 𝑦 ∈ ((ℝ
↑m (1...𝑁))
∖ {𝑥})) ∧ 𝑝 ∈ (ℝ
↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → (1 < 𝑡 → 𝑡 ≠ 0)) |
236 | 235 | imp 407 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) → 𝑡 ≠ 0) |
237 | 236 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ≠ 0) |
238 | 230, 237 | reccld 11744 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (1 / 𝑡) ∈ ℂ) |
239 | | 1cnd 10971 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 1 ∈ ℂ) |
240 | 230, 237 | recne0d 11745 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (1 / 𝑡) ≠ 0) |
241 | 238, 239,
238, 240 | divsubdird 11790 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 / 𝑡) − 1) / (1 / 𝑡)) = (((1 / 𝑡) / (1 / 𝑡)) − (1 / (1 / 𝑡)))) |
242 | 238, 240 | dividd 11749 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((1 / 𝑡) / (1 / 𝑡)) = 1) |
243 | 230, 237 | recrecd 11748 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (1 / (1 / 𝑡)) = 𝑡) |
244 | 242, 243 | oveq12d 7289 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 / 𝑡) / (1 / 𝑡)) − (1 / (1 / 𝑡))) = (1 − 𝑡)) |
245 | 241, 244 | eqtr2d 2781 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑡) = (((1 / 𝑡) − 1) / (1 / 𝑡))) |
246 | 245 | oveq1d 7286 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑡) · (𝑥‘𝑖)) = ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖))) |
247 | 229, 236 | recrecd 11748 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) → (1 / (1 / 𝑡)) = 𝑡) |
248 | 247 | eqcomd 2746 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) → 𝑡 = (1 / (1 / 𝑡))) |
249 | 248 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 = (1 / (1 / 𝑡))) |
250 | 249 | oveq1d 7286 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 · (𝑦‘𝑖)) = ((1 / (1 / 𝑡)) · (𝑦‘𝑖))) |
251 | 246, 250 | oveq12d 7289 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖)))) |
252 | 251 | eqeq2d 2751 |
. . . . . . . . . . . . . 14
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) ↔ (𝑝‘𝑖) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖))))) |
253 | 252 | biimpd 228 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (𝑝‘𝑖) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖))))) |
254 | | eqcom 2747 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))) ↔ (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))) = (𝑦‘𝑖)) |
255 | 139 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) → 𝑦:(1...𝑁)⟶ℝ) |
256 | 255 | ffvelrnda 6958 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) ∈ ℝ) |
257 | 256 | recnd 11004 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) ∈ ℂ) |
258 | 239, 238 | subcld 11332 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (1 − (1 / 𝑡)) ∈ ℂ) |
259 | 124 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) → 𝑥:(1...𝑁)⟶ℝ) |
260 | 259 | ffvelrnda 6958 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℝ) |
261 | 260 | recnd 11004 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℂ) |
262 | 258, 261 | mulcld 10996 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − (1 / 𝑡)) · (𝑥‘𝑖)) ∈ ℂ) |
263 | 146 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) → 𝑝:(1...𝑁)⟶ℝ) |
264 | 263 | ffvelrnda 6958 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑝‘𝑖) ∈ ℝ) |
265 | 264 | recnd 11004 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (𝑝‘𝑖) ∈ ℂ) |
266 | 238, 265 | mulcld 10996 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((1 / 𝑡) · (𝑝‘𝑖)) ∈ ℂ) |
267 | 257, 262,
266 | subaddd 11350 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) = ((1 / 𝑡) · (𝑝‘𝑖)) ↔ (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))) = (𝑦‘𝑖))) |
268 | 254, 267 | bitr4id 290 |
. . . . . . . . . . . . . 14
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))) ↔ ((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) = ((1 / 𝑡) · (𝑝‘𝑖)))) |
269 | | eqcom 2747 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) = ((1 / 𝑡) · (𝑝‘𝑖)) ↔ ((1 / 𝑡) · (𝑝‘𝑖)) = ((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖)))) |
270 | 257, 262 | subcld 11332 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) ∈ ℂ) |
271 | 270, 238,
265, 240 | divmuld 11773 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) = (𝑝‘𝑖) ↔ ((1 / 𝑡) · (𝑝‘𝑖)) = ((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))))) |
272 | 269, 271 | bitr4id 290 |
. . . . . . . . . . . . . 14
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) = ((1 / 𝑡) · (𝑝‘𝑖)) ↔ (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) = (𝑝‘𝑖))) |
273 | | eqcom 2747 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) = (𝑝‘𝑖) ↔ (𝑝‘𝑖) = (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡))) |
274 | 257, 262,
238, 240 | divsubdird 11790 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) = (((𝑦‘𝑖) / (1 / 𝑡)) − (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)))) |
275 | 257, 238,
240 | divcld 11751 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑦‘𝑖) / (1 / 𝑡)) ∈ ℂ) |
276 | 262, 238,
240 | divcld 11751 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)) ∈ ℂ) |
277 | 275, 276 | negsubd 11338 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) / (1 / 𝑡)) + -(((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡))) = (((𝑦‘𝑖) / (1 / 𝑡)) − (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)))) |
278 | 262, 238,
240 | divnegd 11764 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → -(((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)) = (-((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡))) |
279 | 258, 261 | mulneg1d 11428 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (-(1 − (1 / 𝑡)) · (𝑥‘𝑖)) = -((1 − (1 / 𝑡)) · (𝑥‘𝑖))) |
280 | 279 | eqcomd 2746 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → -((1 − (1 / 𝑡)) · (𝑥‘𝑖)) = (-(1 − (1 / 𝑡)) · (𝑥‘𝑖))) |
281 | 280 | oveq1d 7286 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (-((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)) = ((-(1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡))) |
282 | 239, 238 | negsubdi2d 11348 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → -(1 − (1 / 𝑡)) = ((1 / 𝑡) − 1)) |
283 | 282 | oveq1d 7286 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (-(1 − (1 / 𝑡)) · (𝑥‘𝑖)) = (((1 / 𝑡) − 1) · (𝑥‘𝑖))) |
284 | 283 | oveq1d 7286 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((-(1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)) = ((((1 / 𝑡) − 1) · (𝑥‘𝑖)) / (1 / 𝑡))) |
285 | 238, 239 | subcld 11332 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((1 / 𝑡) − 1) ∈ ℂ) |
286 | 285, 261,
238, 240 | div23d 11788 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 / 𝑡) − 1) · (𝑥‘𝑖)) / (1 / 𝑡)) = ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖))) |
287 | 284, 286 | eqtrd 2780 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((-(1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)) = ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖))) |
288 | 278, 281,
287 | 3eqtrd 2784 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → -(((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡)) = ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖))) |
289 | 288 | oveq2d 7287 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) / (1 / 𝑡)) + -(((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡))) = (((𝑦‘𝑖) / (1 / 𝑡)) + ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)))) |
290 | 257, 238,
240 | divrec2d 11755 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑦‘𝑖) / (1 / 𝑡)) = ((1 / (1 / 𝑡)) · (𝑦‘𝑖))) |
291 | 290 | oveq1d 7286 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) / (1 / 𝑡)) + ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖))) = (((1 / (1 / 𝑡)) · (𝑦‘𝑖)) + ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)))) |
292 | 238, 240 | reccld 11744 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (1 / (1 / 𝑡)) ∈ ℂ) |
293 | 292, 257 | mulcld 10996 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((1 / (1 / 𝑡)) · (𝑦‘𝑖)) ∈ ℂ) |
294 | 285, 238,
240 | divcld 11751 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 / 𝑡) − 1) / (1 / 𝑡)) ∈ ℂ) |
295 | 294, 261 | mulcld 10996 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) ∈ ℂ) |
296 | 293, 295 | addcomd 11177 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((1 / (1 / 𝑡)) · (𝑦‘𝑖)) + ((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖))) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖)))) |
297 | 289, 291,
296 | 3eqtrd 2784 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) / (1 / 𝑡)) + -(((1 − (1 / 𝑡)) · (𝑥‘𝑖)) / (1 / 𝑡))) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖)))) |
298 | 274, 277,
297 | 3eqtr2d 2786 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖)))) |
299 | 298 | eqeq2d 2751 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) ↔ (𝑝‘𝑖) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖))))) |
300 | 273, 299 | syl5bb 283 |
. . . . . . . . . . . . . 14
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((((𝑦‘𝑖) − ((1 − (1 / 𝑡)) · (𝑥‘𝑖))) / (1 / 𝑡)) = (𝑝‘𝑖) ↔ (𝑝‘𝑖) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖))))) |
301 | 268, 272,
300 | 3bitrd 305 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))) ↔ (𝑝‘𝑖) = (((((1 / 𝑡) − 1) / (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / (1 / 𝑡)) · (𝑦‘𝑖))))) |
302 | 253, 301 | sylibrd 258 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))))) |
303 | 302 | ralimdva 3105 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) → (∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖))))) |
304 | 303 | imp 407 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − (1 / 𝑡)) · (𝑥‘𝑖)) + ((1 / 𝑡) · (𝑝‘𝑖)))) |
305 | 220, 227,
304 | rspcedvd 3564 |
. . . . . . . . 9
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖)))) |
306 | 305 | 3mix3d 1337 |
. . . . . . . 8
⊢
((((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧ 1 <
𝑡) ∧ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))) |
307 | 306 | exp31 420 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ
↑m (1...𝑁))
∧ 𝑦 ∈ ((ℝ
↑m (1...𝑁))
∖ {𝑥})) ∧ 𝑝 ∈ (ℝ
↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → (1 < 𝑡 → (∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))))) |
308 | 307 | com23 86 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ
↑m (1...𝑁))
∧ 𝑦 ∈ ((ℝ
↑m (1...𝑁))
∖ {𝑥})) ∧ 𝑝 ∈ (ℝ
↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → (∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (1 < 𝑡 → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))))) |
309 | 308 | imp 407 |
. . . . 5
⊢
(((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧
∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → (1 < 𝑡 → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖)))))) |
310 | 186, 198,
309 | 3jaod 1427 |
. . . 4
⊢
(((((𝑁 ∈
ℕ ∧ 𝑥 ∈
(ℝ ↑m (1...𝑁)) ∧ 𝑦 ∈ ((ℝ ↑m
(1...𝑁)) ∖ {𝑥})) ∧ 𝑝 ∈ (ℝ ↑m
(1...𝑁))) ∧ 𝑡 ∈ ℝ) ∧
∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖)))) → ((𝑡 < 0 ∨ 𝑡 ∈ (0[,]1) ∨ 1 < 𝑡) → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖)))))) |
311 | 310 | ex 413 |
. . 3
⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ
↑m (1...𝑁))
∧ 𝑦 ∈ ((ℝ
↑m (1...𝑁))
∖ {𝑥})) ∧ 𝑝 ∈ (ℝ
↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → (∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → ((𝑡 < 0 ∨ 𝑡 ∈ (0[,]1) ∨ 1 < 𝑡) → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))))) |
312 | 5, 311 | mpid 44 |
. 2
⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ
↑m (1...𝑁))
∧ 𝑦 ∈ ((ℝ
↑m (1...𝑁))
∖ {𝑥})) ∧ 𝑝 ∈ (ℝ
↑m (1...𝑁))) ∧ 𝑡 ∈ ℝ) → (∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖)))))) |
313 | 312 | rexlimdva 3215 |
1
⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ (ℝ
↑m (1...𝑁))
∧ 𝑦 ∈ ((ℝ
↑m (1...𝑁))
∖ {𝑥})) ∧ 𝑝 ∈ (ℝ
↑m (1...𝑁))) → (∃𝑡 ∈ ℝ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑦‘𝑖))) → (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖)))))) |