Proof of Theorem constrrtll
Step | Hyp | Ref
| Expression |
1 | | constrrtll.1 |
. . 3
⊢ (𝜑 → 𝑋 = (𝐴 + (𝑇 · (𝐵 − 𝐴)))) |
2 | | constrrtll.t |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ ℝ) |
3 | 2 | recnd 11314 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ ℂ) |
4 | | constrrtll.s |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
5 | | constrrtll.b |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ 𝑆) |
6 | 4, 5 | sseldd 4003 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℂ) |
7 | | constrrtll.a |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ 𝑆) |
8 | 4, 7 | sseldd 4003 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℂ) |
9 | 6, 8 | cjsubd 32747 |
. . . . . . . . . 10
⊢ (𝜑 → (∗‘(𝐵 − 𝐴)) = ((∗‘𝐵) − (∗‘𝐴))) |
10 | 6, 8 | subcld 11643 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℂ) |
11 | 10 | cjcld 15241 |
. . . . . . . . . 10
⊢ (𝜑 → (∗‘(𝐵 − 𝐴)) ∈ ℂ) |
12 | 9, 11 | eqeltrrd 2839 |
. . . . . . . . 9
⊢ (𝜑 → ((∗‘𝐵) − (∗‘𝐴)) ∈
ℂ) |
13 | | constrrtll.d |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ 𝑆) |
14 | 4, 13 | sseldd 4003 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ ℂ) |
15 | | constrrtll.c |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ 𝑆) |
16 | 4, 15 | sseldd 4003 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ ℂ) |
17 | 14, 16 | subcld 11643 |
. . . . . . . . 9
⊢ (𝜑 → (𝐷 − 𝐶) ∈ ℂ) |
18 | 12, 17 | mulcld 11306 |
. . . . . . . 8
⊢ (𝜑 → (((∗‘𝐵) − (∗‘𝐴)) · (𝐷 − 𝐶)) ∈ ℂ) |
19 | 14, 16 | cjsubd 32747 |
. . . . . . . . . 10
⊢ (𝜑 → (∗‘(𝐷 − 𝐶)) = ((∗‘𝐷) − (∗‘𝐶))) |
20 | 17 | cjcld 15241 |
. . . . . . . . . 10
⊢ (𝜑 → (∗‘(𝐷 − 𝐶)) ∈ ℂ) |
21 | 19, 20 | eqeltrrd 2839 |
. . . . . . . . 9
⊢ (𝜑 → ((∗‘𝐷) − (∗‘𝐶)) ∈
ℂ) |
22 | 10, 21 | mulcld 11306 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 − 𝐴) · ((∗‘𝐷) − (∗‘𝐶))) ∈
ℂ) |
23 | 3, 18, 22 | subdid 11742 |
. . . . . . 7
⊢ (𝜑 → (𝑇 · ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷 − 𝐶)) − ((𝐵 − 𝐴) · ((∗‘𝐷) − (∗‘𝐶))))) = ((𝑇 · (((∗‘𝐵) − (∗‘𝐴)) · (𝐷 − 𝐶))) − (𝑇 · ((𝐵 − 𝐴) · ((∗‘𝐷) − (∗‘𝐶)))))) |
24 | 1 | oveq1d 7460 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 − 𝐶) = ((𝐴 + (𝑇 · (𝐵 − 𝐴))) − 𝐶)) |
25 | | constrrtll.r |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑅 ∈ ℝ) |
26 | 25 | recnd 11314 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑅 ∈ ℂ) |
27 | 26, 17 | mulcld 11306 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑅 · (𝐷 − 𝐶)) ∈ ℂ) |
28 | | constrrtll.2 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑋 = (𝐶 + (𝑅 · (𝐷 − 𝐶)))) |
29 | 16, 27, 28 | mvrladdd 11699 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 − 𝐶) = (𝑅 · (𝐷 − 𝐶))) |
30 | 24, 29 | eqtr3d 2776 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴 + (𝑇 · (𝐵 − 𝐴))) − 𝐶) = (𝑅 · (𝐷 − 𝐶))) |
31 | 30, 27 | eqeltrd 2838 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴 + (𝑇 · (𝐵 − 𝐴))) − 𝐶) ∈ ℂ) |
32 | | constrrtll.3 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 →
(ℑ‘((∗‘(𝐵 − 𝐴)) · (𝐷 − 𝐶))) ≠ 0) |
33 | | fveq2 6919 |
. . . . . . . . . . . . . . . . 17
⊢
(((∗‘(𝐵
− 𝐴)) · (𝐷 − 𝐶)) = 0 →
(ℑ‘((∗‘(𝐵 − 𝐴)) · (𝐷 − 𝐶))) = (ℑ‘0)) |
34 | | im0 15198 |
. . . . . . . . . . . . . . . . 17
⊢
(ℑ‘0) = 0 |
35 | 33, 34 | eqtrdi 2790 |
. . . . . . . . . . . . . . . 16
⊢
(((∗‘(𝐵
− 𝐴)) · (𝐷 − 𝐶)) = 0 →
(ℑ‘((∗‘(𝐵 − 𝐴)) · (𝐷 − 𝐶))) = 0) |
36 | 35 | necon3i 2975 |
. . . . . . . . . . . . . . 15
⊢
((ℑ‘((∗‘(𝐵 − 𝐴)) · (𝐷 − 𝐶))) ≠ 0 → ((∗‘(𝐵 − 𝐴)) · (𝐷 − 𝐶)) ≠ 0) |
37 | 32, 36 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((∗‘(𝐵 − 𝐴)) · (𝐷 − 𝐶)) ≠ 0) |
38 | 11, 17, 37 | mulne0bbd 11942 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐷 − 𝐶) ≠ 0) |
39 | 31, 26, 17, 38 | divmul3d 12100 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((𝐴 + (𝑇 · (𝐵 − 𝐴))) − 𝐶) / (𝐷 − 𝐶)) = 𝑅 ↔ ((𝐴 + (𝑇 · (𝐵 − 𝐴))) − 𝐶) = (𝑅 · (𝐷 − 𝐶)))) |
40 | 30, 39 | mpbird 257 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐴 + (𝑇 · (𝐵 − 𝐴))) − 𝐶) / (𝐷 − 𝐶)) = 𝑅) |
41 | 40 | fveq2d 6923 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∗‘(((𝐴 + (𝑇 · (𝐵 − 𝐴))) − 𝐶) / (𝐷 − 𝐶))) = (∗‘𝑅)) |
42 | 31, 17, 38 | cjdivd 15268 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (∗‘(((𝐴 + (𝑇 · (𝐵 − 𝐴))) − 𝐶) / (𝐷 − 𝐶))) = ((∗‘((𝐴 + (𝑇 · (𝐵 − 𝐴))) − 𝐶)) / (∗‘(𝐷 − 𝐶)))) |
43 | 3, 10 | mulcld 11306 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑇 · (𝐵 − 𝐴)) ∈ ℂ) |
44 | 8, 43 | addcld 11305 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐴 + (𝑇 · (𝐵 − 𝐴))) ∈ ℂ) |
45 | 44, 16 | cjsubd 32747 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (∗‘((𝐴 + (𝑇 · (𝐵 − 𝐴))) − 𝐶)) = ((∗‘(𝐴 + (𝑇 · (𝐵 − 𝐴)))) − (∗‘𝐶))) |
46 | 8, 43 | cjaddd 15265 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (∗‘(𝐴 + (𝑇 · (𝐵 − 𝐴)))) = ((∗‘𝐴) + (∗‘(𝑇 · (𝐵 − 𝐴))))) |
47 | 3, 10 | cjmuld 15266 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (∗‘(𝑇 · (𝐵 − 𝐴))) = ((∗‘𝑇) · (∗‘(𝐵 − 𝐴)))) |
48 | 2 | cjred 15271 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (∗‘𝑇) = 𝑇) |
49 | 48, 9 | oveq12d 7463 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((∗‘𝑇) ·
(∗‘(𝐵 −
𝐴))) = (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) |
50 | 47, 49 | eqtrd 2774 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (∗‘(𝑇 · (𝐵 − 𝐴))) = (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) |
51 | 50 | oveq2d 7461 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((∗‘𝐴) + (∗‘(𝑇 · (𝐵 − 𝐴)))) = ((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴))))) |
52 | 46, 51 | eqtrd 2774 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (∗‘(𝐴 + (𝑇 · (𝐵 − 𝐴)))) = ((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴))))) |
53 | 52 | oveq1d 7460 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((∗‘(𝐴 + (𝑇 · (𝐵 − 𝐴)))) − (∗‘𝐶)) = (((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶))) |
54 | 45, 53 | eqtrd 2774 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (∗‘((𝐴 + (𝑇 · (𝐵 − 𝐴))) − 𝐶)) = (((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶))) |
55 | 54, 19 | oveq12d 7463 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((∗‘((𝐴 + (𝑇 · (𝐵 − 𝐴))) − 𝐶)) / (∗‘(𝐷 − 𝐶))) = ((((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) / ((∗‘𝐷) − (∗‘𝐶)))) |
56 | 42, 55 | eqtrd 2774 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∗‘(((𝐴 + (𝑇 · (𝐵 − 𝐴))) − 𝐶) / (𝐷 − 𝐶))) = ((((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) / ((∗‘𝐷) − (∗‘𝐶)))) |
57 | 25 | cjred 15271 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∗‘𝑅) = 𝑅) |
58 | 41, 56, 57 | 3eqtr3rd 2783 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 = ((((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) / ((∗‘𝐷) − (∗‘𝐶)))) |
59 | 40, 58 | eqtrd 2774 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐴 + (𝑇 · (𝐵 − 𝐴))) − 𝐶) / (𝐷 − 𝐶)) = ((((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) / ((∗‘𝐷) − (∗‘𝐶)))) |
60 | 8 | cjcld 15241 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (∗‘𝐴) ∈
ℂ) |
61 | 3, 12 | mulcld 11306 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑇 · ((∗‘𝐵) − (∗‘𝐴))) ∈ ℂ) |
62 | 60, 61 | addcld 11305 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) ∈ ℂ) |
63 | 16 | cjcld 15241 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∗‘𝐶) ∈
ℂ) |
64 | 62, 63 | subcld 11643 |
. . . . . . . . . . 11
⊢ (𝜑 → (((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) ∈
ℂ) |
65 | 17, 38 | cjne0d 15248 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∗‘(𝐷 − 𝐶)) ≠ 0) |
66 | 19, 65 | eqnetrrd 3011 |
. . . . . . . . . . 11
⊢ (𝜑 → ((∗‘𝐷) − (∗‘𝐶)) ≠ 0) |
67 | 31, 17, 64, 21, 38, 66 | divmuleqd 12112 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝐴 + (𝑇 · (𝐵 − 𝐴))) − 𝐶) / (𝐷 − 𝐶)) = ((((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) / ((∗‘𝐷) − (∗‘𝐶))) ↔ (((𝐴 + (𝑇 · (𝐵 − 𝐴))) − 𝐶) · ((∗‘𝐷) − (∗‘𝐶))) = ((((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) · (𝐷 − 𝐶)))) |
68 | 59, 67 | mpbid 232 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐴 + (𝑇 · (𝐵 − 𝐴))) − 𝐶) · ((∗‘𝐷) − (∗‘𝐶))) = ((((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) · (𝐷 − 𝐶))) |
69 | 8, 43, 16 | addsubassd 11663 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴 + (𝑇 · (𝐵 − 𝐴))) − 𝐶) = (𝐴 + ((𝑇 · (𝐵 − 𝐴)) − 𝐶))) |
70 | 43, 8, 16 | addsub12d 11666 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑇 · (𝐵 − 𝐴)) + (𝐴 − 𝐶)) = (𝐴 + ((𝑇 · (𝐵 − 𝐴)) − 𝐶))) |
71 | 69, 70 | eqtr4d 2777 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴 + (𝑇 · (𝐵 − 𝐴))) − 𝐶) = ((𝑇 · (𝐵 − 𝐴)) + (𝐴 − 𝐶))) |
72 | 71 | oveq1d 7460 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐴 + (𝑇 · (𝐵 − 𝐴))) − 𝐶) · ((∗‘𝐷) − (∗‘𝐶))) = (((𝑇 · (𝐵 − 𝐴)) + (𝐴 − 𝐶)) · ((∗‘𝐷) − (∗‘𝐶)))) |
73 | 8, 16 | subcld 11643 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 − 𝐶) ∈ ℂ) |
74 | 43, 73, 21 | adddird 11311 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑇 · (𝐵 − 𝐴)) + (𝐴 − 𝐶)) · ((∗‘𝐷) − (∗‘𝐶))) = (((𝑇 · (𝐵 − 𝐴)) · ((∗‘𝐷) − (∗‘𝐶))) + ((𝐴 − 𝐶) · ((∗‘𝐷) − (∗‘𝐶))))) |
75 | 3, 10, 21 | mulassd 11309 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑇 · (𝐵 − 𝐴)) · ((∗‘𝐷) − (∗‘𝐶))) = (𝑇 · ((𝐵 − 𝐴) · ((∗‘𝐷) − (∗‘𝐶))))) |
76 | 75 | oveq1d 7460 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑇 · (𝐵 − 𝐴)) · ((∗‘𝐷) − (∗‘𝐶))) + ((𝐴 − 𝐶) · ((∗‘𝐷) − (∗‘𝐶)))) = ((𝑇 · ((𝐵 − 𝐴) · ((∗‘𝐷) − (∗‘𝐶)))) + ((𝐴 − 𝐶) · ((∗‘𝐷) − (∗‘𝐶))))) |
77 | 72, 74, 76 | 3eqtrd 2778 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐴 + (𝑇 · (𝐵 − 𝐴))) − 𝐶) · ((∗‘𝐷) − (∗‘𝐶))) = ((𝑇 · ((𝐵 − 𝐴) · ((∗‘𝐷) − (∗‘𝐶)))) + ((𝐴 − 𝐶) · ((∗‘𝐷) − (∗‘𝐶))))) |
78 | 60, 61, 63 | addsubassd 11663 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) = ((∗‘𝐴) + ((𝑇 · ((∗‘𝐵) − (∗‘𝐴))) − (∗‘𝐶)))) |
79 | 61, 60, 63 | addsub12d 11666 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑇 · ((∗‘𝐵) − (∗‘𝐴))) + ((∗‘𝐴) − (∗‘𝐶))) = ((∗‘𝐴) + ((𝑇 · ((∗‘𝐵) − (∗‘𝐴))) − (∗‘𝐶)))) |
80 | 78, 79 | eqtr4d 2777 |
. . . . . . . . . . 11
⊢ (𝜑 → (((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) = ((𝑇 · ((∗‘𝐵) − (∗‘𝐴))) + ((∗‘𝐴) − (∗‘𝐶)))) |
81 | 80 | oveq1d 7460 |
. . . . . . . . . 10
⊢ (𝜑 → ((((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) · (𝐷 − 𝐶)) = (((𝑇 · ((∗‘𝐵) − (∗‘𝐴))) + ((∗‘𝐴) − (∗‘𝐶))) · (𝐷 − 𝐶))) |
82 | 60, 63 | subcld 11643 |
. . . . . . . . . . 11
⊢ (𝜑 → ((∗‘𝐴) − (∗‘𝐶)) ∈
ℂ) |
83 | 61, 82, 17 | adddird 11311 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑇 · ((∗‘𝐵) − (∗‘𝐴))) + ((∗‘𝐴) − (∗‘𝐶))) · (𝐷 − 𝐶)) = (((𝑇 · ((∗‘𝐵) − (∗‘𝐴))) · (𝐷 − 𝐶)) + (((∗‘𝐴) − (∗‘𝐶)) · (𝐷 − 𝐶)))) |
84 | 3, 12, 17 | mulassd 11309 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑇 · ((∗‘𝐵) − (∗‘𝐴))) · (𝐷 − 𝐶)) = (𝑇 · (((∗‘𝐵) − (∗‘𝐴)) · (𝐷 − 𝐶)))) |
85 | 84 | oveq1d 7460 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑇 · ((∗‘𝐵) − (∗‘𝐴))) · (𝐷 − 𝐶)) + (((∗‘𝐴) − (∗‘𝐶)) · (𝐷 − 𝐶))) = ((𝑇 · (((∗‘𝐵) − (∗‘𝐴)) · (𝐷 − 𝐶))) + (((∗‘𝐴) − (∗‘𝐶)) · (𝐷 − 𝐶)))) |
86 | 81, 83, 85 | 3eqtrd 2778 |
. . . . . . . . 9
⊢ (𝜑 → ((((∗‘𝐴) + (𝑇 · ((∗‘𝐵) − (∗‘𝐴)))) − (∗‘𝐶)) · (𝐷 − 𝐶)) = ((𝑇 · (((∗‘𝐵) − (∗‘𝐴)) · (𝐷 − 𝐶))) + (((∗‘𝐴) − (∗‘𝐶)) · (𝐷 − 𝐶)))) |
87 | 68, 77, 86 | 3eqtr3d 2782 |
. . . . . . . 8
⊢ (𝜑 → ((𝑇 · ((𝐵 − 𝐴) · ((∗‘𝐷) − (∗‘𝐶)))) + ((𝐴 − 𝐶) · ((∗‘𝐷) − (∗‘𝐶)))) = ((𝑇 · (((∗‘𝐵) − (∗‘𝐴)) · (𝐷 − 𝐶))) + (((∗‘𝐴) − (∗‘𝐶)) · (𝐷 − 𝐶)))) |
88 | 3, 22 | mulcld 11306 |
. . . . . . . . 9
⊢ (𝜑 → (𝑇 · ((𝐵 − 𝐴) · ((∗‘𝐷) − (∗‘𝐶)))) ∈
ℂ) |
89 | 73, 21 | mulcld 11306 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 − 𝐶) · ((∗‘𝐷) − (∗‘𝐶))) ∈
ℂ) |
90 | 3, 18 | mulcld 11306 |
. . . . . . . . 9
⊢ (𝜑 → (𝑇 · (((∗‘𝐵) − (∗‘𝐴)) · (𝐷 − 𝐶))) ∈ ℂ) |
91 | 82, 17 | mulcld 11306 |
. . . . . . . . 9
⊢ (𝜑 → (((∗‘𝐴) − (∗‘𝐶)) · (𝐷 − 𝐶)) ∈ ℂ) |
92 | 88, 89, 90, 91 | addsubeq4d 11694 |
. . . . . . . 8
⊢ (𝜑 → (((𝑇 · ((𝐵 − 𝐴) · ((∗‘𝐷) − (∗‘𝐶)))) + ((𝐴 − 𝐶) · ((∗‘𝐷) − (∗‘𝐶)))) = ((𝑇 · (((∗‘𝐵) − (∗‘𝐴)) · (𝐷 − 𝐶))) + (((∗‘𝐴) − (∗‘𝐶)) · (𝐷 − 𝐶))) ↔ ((𝑇 · (((∗‘𝐵) − (∗‘𝐴)) · (𝐷 − 𝐶))) − (𝑇 · ((𝐵 − 𝐴) · ((∗‘𝐷) − (∗‘𝐶))))) = (((𝐴 − 𝐶) · ((∗‘𝐷) − (∗‘𝐶))) −
(((∗‘𝐴)
− (∗‘𝐶))
· (𝐷 − 𝐶))))) |
93 | 87, 92 | mpbid 232 |
. . . . . . 7
⊢ (𝜑 → ((𝑇 · (((∗‘𝐵) − (∗‘𝐴)) · (𝐷 − 𝐶))) − (𝑇 · ((𝐵 − 𝐴) · ((∗‘𝐷) − (∗‘𝐶))))) = (((𝐴 − 𝐶) · ((∗‘𝐷) − (∗‘𝐶))) −
(((∗‘𝐴)
− (∗‘𝐶))
· (𝐷 − 𝐶)))) |
94 | 23, 93 | eqtrd 2774 |
. . . . . 6
⊢ (𝜑 → (𝑇 · ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷 − 𝐶)) − ((𝐵 − 𝐴) · ((∗‘𝐷) − (∗‘𝐶))))) = (((𝐴 − 𝐶) · ((∗‘𝐷) − (∗‘𝐶))) −
(((∗‘𝐴)
− (∗‘𝐶))
· (𝐷 − 𝐶)))) |
95 | 18, 22 | subcld 11643 |
. . . . . . 7
⊢ (𝜑 → ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷 − 𝐶)) − ((𝐵 − 𝐴) · ((∗‘𝐷) − (∗‘𝐶)))) ∈
ℂ) |
96 | 89, 91 | subcld 11643 |
. . . . . . 7
⊢ (𝜑 → (((𝐴 − 𝐶) · ((∗‘𝐷) − (∗‘𝐶))) −
(((∗‘𝐴)
− (∗‘𝐶))
· (𝐷 − 𝐶))) ∈
ℂ) |
97 | 11, 17 | mulcld 11306 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((∗‘(𝐵 − 𝐴)) · (𝐷 − 𝐶)) ∈ ℂ) |
98 | | reim0b 15164 |
. . . . . . . . . . . . . 14
⊢
(((∗‘(𝐵
− 𝐴)) · (𝐷 − 𝐶)) ∈ ℂ →
(((∗‘(𝐵
− 𝐴)) · (𝐷 − 𝐶)) ∈ ℝ ↔
(ℑ‘((∗‘(𝐵 − 𝐴)) · (𝐷 − 𝐶))) = 0)) |
99 | 97, 98 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((∗‘(𝐵 − 𝐴)) · (𝐷 − 𝐶)) ∈ ℝ ↔
(ℑ‘((∗‘(𝐵 − 𝐴)) · (𝐷 − 𝐶))) = 0)) |
100 | 99 | necon3bbid 2980 |
. . . . . . . . . . . 12
⊢ (𝜑 → (¬
((∗‘(𝐵 −
𝐴)) · (𝐷 − 𝐶)) ∈ ℝ ↔
(ℑ‘((∗‘(𝐵 − 𝐴)) · (𝐷 − 𝐶))) ≠ 0)) |
101 | 32, 100 | mpbird 257 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬
((∗‘(𝐵 −
𝐴)) · (𝐷 − 𝐶)) ∈ ℝ) |
102 | | cjreb 15168 |
. . . . . . . . . . . . 13
⊢
(((∗‘(𝐵
− 𝐴)) · (𝐷 − 𝐶)) ∈ ℂ →
(((∗‘(𝐵
− 𝐴)) · (𝐷 − 𝐶)) ∈ ℝ ↔
(∗‘((∗‘(𝐵 − 𝐴)) · (𝐷 − 𝐶))) = ((∗‘(𝐵 − 𝐴)) · (𝐷 − 𝐶)))) |
103 | 97, 102 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((∗‘(𝐵 − 𝐴)) · (𝐷 − 𝐶)) ∈ ℝ ↔
(∗‘((∗‘(𝐵 − 𝐴)) · (𝐷 − 𝐶))) = ((∗‘(𝐵 − 𝐴)) · (𝐷 − 𝐶)))) |
104 | 103 | necon3bbid 2980 |
. . . . . . . . . . 11
⊢ (𝜑 → (¬
((∗‘(𝐵 −
𝐴)) · (𝐷 − 𝐶)) ∈ ℝ ↔
(∗‘((∗‘(𝐵 − 𝐴)) · (𝐷 − 𝐶))) ≠ ((∗‘(𝐵 − 𝐴)) · (𝐷 − 𝐶)))) |
105 | 101, 104 | mpbid 232 |
. . . . . . . . . 10
⊢ (𝜑 →
(∗‘((∗‘(𝐵 − 𝐴)) · (𝐷 − 𝐶))) ≠ ((∗‘(𝐵 − 𝐴)) · (𝐷 − 𝐶))) |
106 | 11, 17 | cjmuld 15266 |
. . . . . . . . . . 11
⊢ (𝜑 →
(∗‘((∗‘(𝐵 − 𝐴)) · (𝐷 − 𝐶))) =
((∗‘(∗‘(𝐵 − 𝐴))) · (∗‘(𝐷 − 𝐶)))) |
107 | 10 | cjcjd 15244 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(∗‘(∗‘(𝐵 − 𝐴))) = (𝐵 − 𝐴)) |
108 | 107, 19 | oveq12d 7463 |
. . . . . . . . . . 11
⊢ (𝜑 →
((∗‘(∗‘(𝐵 − 𝐴))) · (∗‘(𝐷 − 𝐶))) = ((𝐵 − 𝐴) · ((∗‘𝐷) − (∗‘𝐶)))) |
109 | 106, 108 | eqtrd 2774 |
. . . . . . . . . 10
⊢ (𝜑 →
(∗‘((∗‘(𝐵 − 𝐴)) · (𝐷 − 𝐶))) = ((𝐵 − 𝐴) · ((∗‘𝐷) − (∗‘𝐶)))) |
110 | 9 | oveq1d 7460 |
. . . . . . . . . 10
⊢ (𝜑 → ((∗‘(𝐵 − 𝐴)) · (𝐷 − 𝐶)) = (((∗‘𝐵) − (∗‘𝐴)) · (𝐷 − 𝐶))) |
111 | 105, 109,
110 | 3netr3d 3019 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐵 − 𝐴) · ((∗‘𝐷) − (∗‘𝐶))) ≠ (((∗‘𝐵) − (∗‘𝐴)) · (𝐷 − 𝐶))) |
112 | 111 | necomd 2998 |
. . . . . . . 8
⊢ (𝜑 → (((∗‘𝐵) − (∗‘𝐴)) · (𝐷 − 𝐶)) ≠ ((𝐵 − 𝐴) · ((∗‘𝐷) − (∗‘𝐶)))) |
113 | 18, 22, 112 | subne0d 11652 |
. . . . . . 7
⊢ (𝜑 → ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷 − 𝐶)) − ((𝐵 − 𝐴) · ((∗‘𝐷) − (∗‘𝐶)))) ≠ 0) |
114 | 3, 95, 96, 113 | ldiv 12124 |
. . . . . 6
⊢ (𝜑 → ((𝑇 · ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷 − 𝐶)) − ((𝐵 − 𝐴) · ((∗‘𝐷) − (∗‘𝐶))))) = (((𝐴 − 𝐶) · ((∗‘𝐷) − (∗‘𝐶))) −
(((∗‘𝐴)
− (∗‘𝐶))
· (𝐷 − 𝐶))) ↔ 𝑇 = ((((𝐴 − 𝐶) · ((∗‘𝐷) − (∗‘𝐶))) −
(((∗‘𝐴)
− (∗‘𝐶))
· (𝐷 − 𝐶))) / ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷 − 𝐶)) − ((𝐵 − 𝐴) · ((∗‘𝐷) − (∗‘𝐶))))))) |
115 | 94, 114 | mpbid 232 |
. . . . 5
⊢ (𝜑 → 𝑇 = ((((𝐴 − 𝐶) · ((∗‘𝐷) − (∗‘𝐶))) −
(((∗‘𝐴)
− (∗‘𝐶))
· (𝐷 − 𝐶))) / ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷 − 𝐶)) − ((𝐵 − 𝐴) · ((∗‘𝐷) − (∗‘𝐶)))))) |
116 | 115 | oveq1d 7460 |
. . . 4
⊢ (𝜑 → (𝑇 · (𝐵 − 𝐴)) = (((((𝐴 − 𝐶) · ((∗‘𝐷) − (∗‘𝐶))) −
(((∗‘𝐴)
− (∗‘𝐶))
· (𝐷 − 𝐶))) / ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷 − 𝐶)) − ((𝐵 − 𝐴) · ((∗‘𝐷) − (∗‘𝐶))))) · (𝐵 − 𝐴))) |
117 | 116 | oveq2d 7461 |
. . 3
⊢ (𝜑 → (𝐴 + (𝑇 · (𝐵 − 𝐴))) = (𝐴 + (((((𝐴 − 𝐶) · ((∗‘𝐷) − (∗‘𝐶))) −
(((∗‘𝐴)
− (∗‘𝐶))
· (𝐷 − 𝐶))) / ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷 − 𝐶)) − ((𝐵 − 𝐴) · ((∗‘𝐷) − (∗‘𝐶))))) · (𝐵 − 𝐴)))) |
118 | 1, 117 | eqtrd 2774 |
. 2
⊢ (𝜑 → 𝑋 = (𝐴 + (((((𝐴 − 𝐶) · ((∗‘𝐷) − (∗‘𝐶))) −
(((∗‘𝐴)
− (∗‘𝐶))
· (𝐷 − 𝐶))) / ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷 − 𝐶)) − ((𝐵 − 𝐴) · ((∗‘𝐷) − (∗‘𝐶))))) · (𝐵 − 𝐴)))) |
119 | | constrrtll.n |
. 2
⊢ 𝑁 = (𝐴 + (((((𝐴 − 𝐶) · ((∗‘𝐷) − (∗‘𝐶))) −
(((∗‘𝐴)
− (∗‘𝐶))
· (𝐷 − 𝐶))) / ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷 − 𝐶)) − ((𝐵 − 𝐴) · ((∗‘𝐷) − (∗‘𝐶))))) · (𝐵 − 𝐴))) |
120 | 118, 119 | eqtr4di 2792 |
1
⊢ (𝜑 → 𝑋 = 𝑁) |