Step |
Hyp |
Ref |
Expression |
1 |
|
constrrtll.s |
⊢ ( 𝜑 → 𝑆 ⊆ ℂ ) |
2 |
|
constrrtll.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝑆 ) |
3 |
|
constrrtll.b |
⊢ ( 𝜑 → 𝐵 ∈ 𝑆 ) |
4 |
|
constrrtll.c |
⊢ ( 𝜑 → 𝐶 ∈ 𝑆 ) |
5 |
|
constrrtll.d |
⊢ ( 𝜑 → 𝐷 ∈ 𝑆 ) |
6 |
|
constrrtll.t |
⊢ ( 𝜑 → 𝑇 ∈ ℝ ) |
7 |
|
constrrtll.r |
⊢ ( 𝜑 → 𝑅 ∈ ℝ ) |
8 |
|
constrrtll.1 |
⊢ ( 𝜑 → 𝑋 = ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) ) |
9 |
|
constrrtll.2 |
⊢ ( 𝜑 → 𝑋 = ( 𝐶 + ( 𝑅 · ( 𝐷 − 𝐶 ) ) ) ) |
10 |
|
constrrtll.3 |
⊢ ( 𝜑 → ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ) ≠ 0 ) |
11 |
|
constrrtll.n |
⊢ 𝑁 = ( 𝐴 + ( ( ( ( ( 𝐴 − 𝐶 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) − ( ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) · ( 𝐷 − 𝐶 ) ) ) / ( ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) − ( ( 𝐵 − 𝐴 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) ) · ( 𝐵 − 𝐴 ) ) ) |
12 |
6
|
recnd |
⊢ ( 𝜑 → 𝑇 ∈ ℂ ) |
13 |
1 3
|
sseldd |
⊢ ( 𝜑 → 𝐵 ∈ ℂ ) |
14 |
1 2
|
sseldd |
⊢ ( 𝜑 → 𝐴 ∈ ℂ ) |
15 |
13 14
|
cjsubd |
⊢ ( 𝜑 → ( ∗ ‘ ( 𝐵 − 𝐴 ) ) = ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) |
16 |
13 14
|
subcld |
⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℂ ) |
17 |
16
|
cjcld |
⊢ ( 𝜑 → ( ∗ ‘ ( 𝐵 − 𝐴 ) ) ∈ ℂ ) |
18 |
15 17
|
eqeltrrd |
⊢ ( 𝜑 → ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ∈ ℂ ) |
19 |
1 5
|
sseldd |
⊢ ( 𝜑 → 𝐷 ∈ ℂ ) |
20 |
1 4
|
sseldd |
⊢ ( 𝜑 → 𝐶 ∈ ℂ ) |
21 |
19 20
|
subcld |
⊢ ( 𝜑 → ( 𝐷 − 𝐶 ) ∈ ℂ ) |
22 |
18 21
|
mulcld |
⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ∈ ℂ ) |
23 |
19 20
|
cjsubd |
⊢ ( 𝜑 → ( ∗ ‘ ( 𝐷 − 𝐶 ) ) = ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) |
24 |
21
|
cjcld |
⊢ ( 𝜑 → ( ∗ ‘ ( 𝐷 − 𝐶 ) ) ∈ ℂ ) |
25 |
23 24
|
eqeltrrd |
⊢ ( 𝜑 → ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ∈ ℂ ) |
26 |
16 25
|
mulcld |
⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ∈ ℂ ) |
27 |
12 22 26
|
subdid |
⊢ ( 𝜑 → ( 𝑇 · ( ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) − ( ( 𝐵 − 𝐴 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) ) = ( ( 𝑇 · ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ) − ( 𝑇 · ( ( 𝐵 − 𝐴 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) ) ) |
28 |
8
|
oveq1d |
⊢ ( 𝜑 → ( 𝑋 − 𝐶 ) = ( ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) − 𝐶 ) ) |
29 |
7
|
recnd |
⊢ ( 𝜑 → 𝑅 ∈ ℂ ) |
30 |
29 21
|
mulcld |
⊢ ( 𝜑 → ( 𝑅 · ( 𝐷 − 𝐶 ) ) ∈ ℂ ) |
31 |
20 30 9
|
mvrladdd |
⊢ ( 𝜑 → ( 𝑋 − 𝐶 ) = ( 𝑅 · ( 𝐷 − 𝐶 ) ) ) |
32 |
28 31
|
eqtr3d |
⊢ ( 𝜑 → ( ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) − 𝐶 ) = ( 𝑅 · ( 𝐷 − 𝐶 ) ) ) |
33 |
32 30
|
eqeltrd |
⊢ ( 𝜑 → ( ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) − 𝐶 ) ∈ ℂ ) |
34 |
|
fveq2 |
⊢ ( ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) = 0 → ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ) = ( ℑ ‘ 0 ) ) |
35 |
|
im0 |
⊢ ( ℑ ‘ 0 ) = 0 |
36 |
34 35
|
eqtrdi |
⊢ ( ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) = 0 → ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ) = 0 ) |
37 |
36
|
necon3i |
⊢ ( ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ) ≠ 0 → ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ≠ 0 ) |
38 |
10 37
|
syl |
⊢ ( 𝜑 → ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ≠ 0 ) |
39 |
17 21 38
|
mulne0bbd |
⊢ ( 𝜑 → ( 𝐷 − 𝐶 ) ≠ 0 ) |
40 |
33 29 21 39
|
divmul3d |
⊢ ( 𝜑 → ( ( ( ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) − 𝐶 ) / ( 𝐷 − 𝐶 ) ) = 𝑅 ↔ ( ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) − 𝐶 ) = ( 𝑅 · ( 𝐷 − 𝐶 ) ) ) ) |
41 |
32 40
|
mpbird |
⊢ ( 𝜑 → ( ( ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) − 𝐶 ) / ( 𝐷 − 𝐶 ) ) = 𝑅 ) |
42 |
41
|
fveq2d |
⊢ ( 𝜑 → ( ∗ ‘ ( ( ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) − 𝐶 ) / ( 𝐷 − 𝐶 ) ) ) = ( ∗ ‘ 𝑅 ) ) |
43 |
33 21 39
|
cjdivd |
⊢ ( 𝜑 → ( ∗ ‘ ( ( ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) − 𝐶 ) / ( 𝐷 − 𝐶 ) ) ) = ( ( ∗ ‘ ( ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) − 𝐶 ) ) / ( ∗ ‘ ( 𝐷 − 𝐶 ) ) ) ) |
44 |
12 16
|
mulcld |
⊢ ( 𝜑 → ( 𝑇 · ( 𝐵 − 𝐴 ) ) ∈ ℂ ) |
45 |
14 44
|
addcld |
⊢ ( 𝜑 → ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) ∈ ℂ ) |
46 |
45 20
|
cjsubd |
⊢ ( 𝜑 → ( ∗ ‘ ( ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) − 𝐶 ) ) = ( ( ∗ ‘ ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) ) − ( ∗ ‘ 𝐶 ) ) ) |
47 |
14 44
|
cjaddd |
⊢ ( 𝜑 → ( ∗ ‘ ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) ) = ( ( ∗ ‘ 𝐴 ) + ( ∗ ‘ ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) ) ) |
48 |
12 16
|
cjmuld |
⊢ ( 𝜑 → ( ∗ ‘ ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) = ( ( ∗ ‘ 𝑇 ) · ( ∗ ‘ ( 𝐵 − 𝐴 ) ) ) ) |
49 |
6
|
cjred |
⊢ ( 𝜑 → ( ∗ ‘ 𝑇 ) = 𝑇 ) |
50 |
49 15
|
oveq12d |
⊢ ( 𝜑 → ( ( ∗ ‘ 𝑇 ) · ( ∗ ‘ ( 𝐵 − 𝐴 ) ) ) = ( 𝑇 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) ) |
51 |
48 50
|
eqtrd |
⊢ ( 𝜑 → ( ∗ ‘ ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) = ( 𝑇 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) ) |
52 |
51
|
oveq2d |
⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) + ( ∗ ‘ ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) ) = ( ( ∗ ‘ 𝐴 ) + ( 𝑇 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) ) ) |
53 |
47 52
|
eqtrd |
⊢ ( 𝜑 → ( ∗ ‘ ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) ) = ( ( ∗ ‘ 𝐴 ) + ( 𝑇 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) ) ) |
54 |
53
|
oveq1d |
⊢ ( 𝜑 → ( ( ∗ ‘ ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) ) − ( ∗ ‘ 𝐶 ) ) = ( ( ( ∗ ‘ 𝐴 ) + ( 𝑇 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) ) − ( ∗ ‘ 𝐶 ) ) ) |
55 |
46 54
|
eqtrd |
⊢ ( 𝜑 → ( ∗ ‘ ( ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) − 𝐶 ) ) = ( ( ( ∗ ‘ 𝐴 ) + ( 𝑇 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) ) − ( ∗ ‘ 𝐶 ) ) ) |
56 |
55 23
|
oveq12d |
⊢ ( 𝜑 → ( ( ∗ ‘ ( ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) − 𝐶 ) ) / ( ∗ ‘ ( 𝐷 − 𝐶 ) ) ) = ( ( ( ( ∗ ‘ 𝐴 ) + ( 𝑇 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) ) − ( ∗ ‘ 𝐶 ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) |
57 |
43 56
|
eqtrd |
⊢ ( 𝜑 → ( ∗ ‘ ( ( ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) − 𝐶 ) / ( 𝐷 − 𝐶 ) ) ) = ( ( ( ( ∗ ‘ 𝐴 ) + ( 𝑇 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) ) − ( ∗ ‘ 𝐶 ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) |
58 |
7
|
cjred |
⊢ ( 𝜑 → ( ∗ ‘ 𝑅 ) = 𝑅 ) |
59 |
42 57 58
|
3eqtr3rd |
⊢ ( 𝜑 → 𝑅 = ( ( ( ( ∗ ‘ 𝐴 ) + ( 𝑇 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) ) − ( ∗ ‘ 𝐶 ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) |
60 |
41 59
|
eqtrd |
⊢ ( 𝜑 → ( ( ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) − 𝐶 ) / ( 𝐷 − 𝐶 ) ) = ( ( ( ( ∗ ‘ 𝐴 ) + ( 𝑇 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) ) − ( ∗ ‘ 𝐶 ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) |
61 |
14
|
cjcld |
⊢ ( 𝜑 → ( ∗ ‘ 𝐴 ) ∈ ℂ ) |
62 |
12 18
|
mulcld |
⊢ ( 𝜑 → ( 𝑇 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) ∈ ℂ ) |
63 |
61 62
|
addcld |
⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) + ( 𝑇 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) ) ∈ ℂ ) |
64 |
20
|
cjcld |
⊢ ( 𝜑 → ( ∗ ‘ 𝐶 ) ∈ ℂ ) |
65 |
63 64
|
subcld |
⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) + ( 𝑇 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) ) − ( ∗ ‘ 𝐶 ) ) ∈ ℂ ) |
66 |
21 39
|
cjne0d |
⊢ ( 𝜑 → ( ∗ ‘ ( 𝐷 − 𝐶 ) ) ≠ 0 ) |
67 |
23 66
|
eqnetrrd |
⊢ ( 𝜑 → ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ≠ 0 ) |
68 |
33 21 65 25 39 67
|
divmuleqd |
⊢ ( 𝜑 → ( ( ( ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) − 𝐶 ) / ( 𝐷 − 𝐶 ) ) = ( ( ( ( ∗ ‘ 𝐴 ) + ( 𝑇 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) ) − ( ∗ ‘ 𝐶 ) ) / ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ↔ ( ( ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) − 𝐶 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) = ( ( ( ( ∗ ‘ 𝐴 ) + ( 𝑇 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) ) − ( ∗ ‘ 𝐶 ) ) · ( 𝐷 − 𝐶 ) ) ) ) |
69 |
60 68
|
mpbid |
⊢ ( 𝜑 → ( ( ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) − 𝐶 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) = ( ( ( ( ∗ ‘ 𝐴 ) + ( 𝑇 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) ) − ( ∗ ‘ 𝐶 ) ) · ( 𝐷 − 𝐶 ) ) ) |
70 |
14 44 20
|
addsubassd |
⊢ ( 𝜑 → ( ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) − 𝐶 ) = ( 𝐴 + ( ( 𝑇 · ( 𝐵 − 𝐴 ) ) − 𝐶 ) ) ) |
71 |
44 14 20
|
addsub12d |
⊢ ( 𝜑 → ( ( 𝑇 · ( 𝐵 − 𝐴 ) ) + ( 𝐴 − 𝐶 ) ) = ( 𝐴 + ( ( 𝑇 · ( 𝐵 − 𝐴 ) ) − 𝐶 ) ) ) |
72 |
70 71
|
eqtr4d |
⊢ ( 𝜑 → ( ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) − 𝐶 ) = ( ( 𝑇 · ( 𝐵 − 𝐴 ) ) + ( 𝐴 − 𝐶 ) ) ) |
73 |
72
|
oveq1d |
⊢ ( 𝜑 → ( ( ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) − 𝐶 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) = ( ( ( 𝑇 · ( 𝐵 − 𝐴 ) ) + ( 𝐴 − 𝐶 ) ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) |
74 |
14 20
|
subcld |
⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) ∈ ℂ ) |
75 |
44 74 25
|
adddird |
⊢ ( 𝜑 → ( ( ( 𝑇 · ( 𝐵 − 𝐴 ) ) + ( 𝐴 − 𝐶 ) ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) = ( ( ( 𝑇 · ( 𝐵 − 𝐴 ) ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐴 − 𝐶 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) ) |
76 |
12 16 25
|
mulassd |
⊢ ( 𝜑 → ( ( 𝑇 · ( 𝐵 − 𝐴 ) ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) = ( 𝑇 · ( ( 𝐵 − 𝐴 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) ) |
77 |
76
|
oveq1d |
⊢ ( 𝜑 → ( ( ( 𝑇 · ( 𝐵 − 𝐴 ) ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) + ( ( 𝐴 − 𝐶 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) = ( ( 𝑇 · ( ( 𝐵 − 𝐴 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) + ( ( 𝐴 − 𝐶 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) ) |
78 |
73 75 77
|
3eqtrd |
⊢ ( 𝜑 → ( ( ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) − 𝐶 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) = ( ( 𝑇 · ( ( 𝐵 − 𝐴 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) + ( ( 𝐴 − 𝐶 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) ) |
79 |
61 62 64
|
addsubassd |
⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) + ( 𝑇 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) ) − ( ∗ ‘ 𝐶 ) ) = ( ( ∗ ‘ 𝐴 ) + ( ( 𝑇 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) − ( ∗ ‘ 𝐶 ) ) ) ) |
80 |
62 61 64
|
addsub12d |
⊢ ( 𝜑 → ( ( 𝑇 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) + ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) ) = ( ( ∗ ‘ 𝐴 ) + ( ( 𝑇 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) − ( ∗ ‘ 𝐶 ) ) ) ) |
81 |
79 80
|
eqtr4d |
⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) + ( 𝑇 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) ) − ( ∗ ‘ 𝐶 ) ) = ( ( 𝑇 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) + ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) ) ) |
82 |
81
|
oveq1d |
⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) + ( 𝑇 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) ) − ( ∗ ‘ 𝐶 ) ) · ( 𝐷 − 𝐶 ) ) = ( ( ( 𝑇 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) + ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) ) · ( 𝐷 − 𝐶 ) ) ) |
83 |
61 64
|
subcld |
⊢ ( 𝜑 → ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) ∈ ℂ ) |
84 |
62 83 21
|
adddird |
⊢ ( 𝜑 → ( ( ( 𝑇 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) + ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) ) · ( 𝐷 − 𝐶 ) ) = ( ( ( 𝑇 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) · ( 𝐷 − 𝐶 ) ) + ( ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) · ( 𝐷 − 𝐶 ) ) ) ) |
85 |
12 18 21
|
mulassd |
⊢ ( 𝜑 → ( ( 𝑇 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) · ( 𝐷 − 𝐶 ) ) = ( 𝑇 · ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ) ) |
86 |
85
|
oveq1d |
⊢ ( 𝜑 → ( ( ( 𝑇 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) · ( 𝐷 − 𝐶 ) ) + ( ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) · ( 𝐷 − 𝐶 ) ) ) = ( ( 𝑇 · ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ) + ( ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) · ( 𝐷 − 𝐶 ) ) ) ) |
87 |
82 84 86
|
3eqtrd |
⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐴 ) + ( 𝑇 · ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) ) ) − ( ∗ ‘ 𝐶 ) ) · ( 𝐷 − 𝐶 ) ) = ( ( 𝑇 · ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ) + ( ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) · ( 𝐷 − 𝐶 ) ) ) ) |
88 |
69 78 87
|
3eqtr3d |
⊢ ( 𝜑 → ( ( 𝑇 · ( ( 𝐵 − 𝐴 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) + ( ( 𝐴 − 𝐶 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) = ( ( 𝑇 · ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ) + ( ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) · ( 𝐷 − 𝐶 ) ) ) ) |
89 |
12 26
|
mulcld |
⊢ ( 𝜑 → ( 𝑇 · ( ( 𝐵 − 𝐴 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) ∈ ℂ ) |
90 |
74 25
|
mulcld |
⊢ ( 𝜑 → ( ( 𝐴 − 𝐶 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ∈ ℂ ) |
91 |
12 22
|
mulcld |
⊢ ( 𝜑 → ( 𝑇 · ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ) ∈ ℂ ) |
92 |
83 21
|
mulcld |
⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) · ( 𝐷 − 𝐶 ) ) ∈ ℂ ) |
93 |
89 90 91 92
|
addsubeq4d |
⊢ ( 𝜑 → ( ( ( 𝑇 · ( ( 𝐵 − 𝐴 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) + ( ( 𝐴 − 𝐶 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) = ( ( 𝑇 · ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ) + ( ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) · ( 𝐷 − 𝐶 ) ) ) ↔ ( ( 𝑇 · ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ) − ( 𝑇 · ( ( 𝐵 − 𝐴 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) ) = ( ( ( 𝐴 − 𝐶 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) − ( ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) · ( 𝐷 − 𝐶 ) ) ) ) ) |
94 |
88 93
|
mpbid |
⊢ ( 𝜑 → ( ( 𝑇 · ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ) − ( 𝑇 · ( ( 𝐵 − 𝐴 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) ) = ( ( ( 𝐴 − 𝐶 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) − ( ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) · ( 𝐷 − 𝐶 ) ) ) ) |
95 |
27 94
|
eqtrd |
⊢ ( 𝜑 → ( 𝑇 · ( ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) − ( ( 𝐵 − 𝐴 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) ) = ( ( ( 𝐴 − 𝐶 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) − ( ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) · ( 𝐷 − 𝐶 ) ) ) ) |
96 |
22 26
|
subcld |
⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) − ( ( 𝐵 − 𝐴 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) ∈ ℂ ) |
97 |
90 92
|
subcld |
⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐶 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) − ( ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) · ( 𝐷 − 𝐶 ) ) ) ∈ ℂ ) |
98 |
17 21
|
mulcld |
⊢ ( 𝜑 → ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ∈ ℂ ) |
99 |
|
reim0b |
⊢ ( ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ∈ ℂ → ( ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ∈ ℝ ↔ ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ) = 0 ) ) |
100 |
98 99
|
syl |
⊢ ( 𝜑 → ( ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ∈ ℝ ↔ ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ) = 0 ) ) |
101 |
100
|
necon3bbid |
⊢ ( 𝜑 → ( ¬ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ∈ ℝ ↔ ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ) ≠ 0 ) ) |
102 |
10 101
|
mpbird |
⊢ ( 𝜑 → ¬ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ∈ ℝ ) |
103 |
|
cjreb |
⊢ ( ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ∈ ℂ → ( ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ∈ ℝ ↔ ( ∗ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ) = ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ) ) |
104 |
98 103
|
syl |
⊢ ( 𝜑 → ( ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ∈ ℝ ↔ ( ∗ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ) = ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ) ) |
105 |
104
|
necon3bbid |
⊢ ( 𝜑 → ( ¬ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ∈ ℝ ↔ ( ∗ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ) ≠ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ) ) |
106 |
102 105
|
mpbid |
⊢ ( 𝜑 → ( ∗ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ) ≠ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ) |
107 |
17 21
|
cjmuld |
⊢ ( 𝜑 → ( ∗ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ) = ( ( ∗ ‘ ( ∗ ‘ ( 𝐵 − 𝐴 ) ) ) · ( ∗ ‘ ( 𝐷 − 𝐶 ) ) ) ) |
108 |
16
|
cjcjd |
⊢ ( 𝜑 → ( ∗ ‘ ( ∗ ‘ ( 𝐵 − 𝐴 ) ) ) = ( 𝐵 − 𝐴 ) ) |
109 |
108 23
|
oveq12d |
⊢ ( 𝜑 → ( ( ∗ ‘ ( ∗ ‘ ( 𝐵 − 𝐴 ) ) ) · ( ∗ ‘ ( 𝐷 − 𝐶 ) ) ) = ( ( 𝐵 − 𝐴 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) |
110 |
107 109
|
eqtrd |
⊢ ( 𝜑 → ( ∗ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ) = ( ( 𝐵 − 𝐴 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) |
111 |
15
|
oveq1d |
⊢ ( 𝜑 → ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) = ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ) |
112 |
106 110 111
|
3netr3d |
⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ≠ ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ) |
113 |
112
|
necomd |
⊢ ( 𝜑 → ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) ≠ ( ( 𝐵 − 𝐴 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) |
114 |
22 26 113
|
subne0d |
⊢ ( 𝜑 → ( ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) − ( ( 𝐵 − 𝐴 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) ≠ 0 ) |
115 |
12 96 97 114
|
ldiv |
⊢ ( 𝜑 → ( ( 𝑇 · ( ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) − ( ( 𝐵 − 𝐴 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) ) = ( ( ( 𝐴 − 𝐶 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) − ( ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) · ( 𝐷 − 𝐶 ) ) ) ↔ 𝑇 = ( ( ( ( 𝐴 − 𝐶 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) − ( ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) · ( 𝐷 − 𝐶 ) ) ) / ( ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) − ( ( 𝐵 − 𝐴 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) ) ) ) |
116 |
95 115
|
mpbid |
⊢ ( 𝜑 → 𝑇 = ( ( ( ( 𝐴 − 𝐶 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) − ( ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) · ( 𝐷 − 𝐶 ) ) ) / ( ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) − ( ( 𝐵 − 𝐴 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) ) ) |
117 |
116
|
oveq1d |
⊢ ( 𝜑 → ( 𝑇 · ( 𝐵 − 𝐴 ) ) = ( ( ( ( ( 𝐴 − 𝐶 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) − ( ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) · ( 𝐷 − 𝐶 ) ) ) / ( ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) − ( ( 𝐵 − 𝐴 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) ) · ( 𝐵 − 𝐴 ) ) ) |
118 |
117
|
oveq2d |
⊢ ( 𝜑 → ( 𝐴 + ( 𝑇 · ( 𝐵 − 𝐴 ) ) ) = ( 𝐴 + ( ( ( ( ( 𝐴 − 𝐶 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) − ( ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) · ( 𝐷 − 𝐶 ) ) ) / ( ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) − ( ( 𝐵 − 𝐴 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) ) · ( 𝐵 − 𝐴 ) ) ) ) |
119 |
8 118
|
eqtrd |
⊢ ( 𝜑 → 𝑋 = ( 𝐴 + ( ( ( ( ( 𝐴 − 𝐶 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) − ( ( ( ∗ ‘ 𝐴 ) − ( ∗ ‘ 𝐶 ) ) · ( 𝐷 − 𝐶 ) ) ) / ( ( ( ( ∗ ‘ 𝐵 ) − ( ∗ ‘ 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) − ( ( 𝐵 − 𝐴 ) · ( ( ∗ ‘ 𝐷 ) − ( ∗ ‘ 𝐶 ) ) ) ) ) · ( 𝐵 − 𝐴 ) ) ) ) |
120 |
119 11
|
eqtr4di |
⊢ ( 𝜑 → 𝑋 = 𝑁 ) |