Step |
Hyp |
Ref |
Expression |
1 |
|
sigar |
⊢ 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) ) |
2 |
|
sigardiv.a |
⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ) |
3 |
|
sigardiv.b |
⊢ ( 𝜑 → ¬ 𝐶 = 𝐴 ) |
4 |
|
sigardiv.c |
⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐶 − 𝐴 ) ) = 0 ) |
5 |
2
|
simp2d |
⊢ ( 𝜑 → 𝐵 ∈ ℂ ) |
6 |
2
|
simp1d |
⊢ ( 𝜑 → 𝐴 ∈ ℂ ) |
7 |
5 6
|
subcld |
⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℂ ) |
8 |
2
|
simp3d |
⊢ ( 𝜑 → 𝐶 ∈ ℂ ) |
9 |
8 6
|
subcld |
⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) ∈ ℂ ) |
10 |
3
|
neqned |
⊢ ( 𝜑 → 𝐶 ≠ 𝐴 ) |
11 |
8 6 10
|
subne0d |
⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) ≠ 0 ) |
12 |
7 9 11
|
cjdivd |
⊢ ( 𝜑 → ( ∗ ‘ ( ( 𝐵 − 𝐴 ) / ( 𝐶 − 𝐴 ) ) ) = ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) / ( ∗ ‘ ( 𝐶 − 𝐴 ) ) ) ) |
13 |
7
|
cjcld |
⊢ ( 𝜑 → ( ∗ ‘ ( 𝐵 − 𝐴 ) ) ∈ ℂ ) |
14 |
9
|
cjcld |
⊢ ( 𝜑 → ( ∗ ‘ ( 𝐶 − 𝐴 ) ) ∈ ℂ ) |
15 |
9 11
|
cjne0d |
⊢ ( 𝜑 → ( ∗ ‘ ( 𝐶 − 𝐴 ) ) ≠ 0 ) |
16 |
13 14 9 15 11
|
divcan5rd |
⊢ ( 𝜑 → ( ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐶 − 𝐴 ) ) / ( ( ∗ ‘ ( 𝐶 − 𝐴 ) ) · ( 𝐶 − 𝐴 ) ) ) = ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) / ( ∗ ‘ ( 𝐶 − 𝐴 ) ) ) ) |
17 |
13 9
|
mulcld |
⊢ ( 𝜑 → ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐶 − 𝐴 ) ) ∈ ℂ ) |
18 |
1
|
sigarval |
⊢ ( ( ( 𝐵 − 𝐴 ) ∈ ℂ ∧ ( 𝐶 − 𝐴 ) ∈ ℂ ) → ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐶 − 𝐴 ) ) = ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐶 − 𝐴 ) ) ) ) |
19 |
7 9 18
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) 𝐺 ( 𝐶 − 𝐴 ) ) = ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐶 − 𝐴 ) ) ) ) |
20 |
19 4
|
eqtr3d |
⊢ ( 𝜑 → ( ℑ ‘ ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐶 − 𝐴 ) ) ) = 0 ) |
21 |
17 20
|
reim0bd |
⊢ ( 𝜑 → ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐶 − 𝐴 ) ) ∈ ℝ ) |
22 |
9 14
|
mulcomd |
⊢ ( 𝜑 → ( ( 𝐶 − 𝐴 ) · ( ∗ ‘ ( 𝐶 − 𝐴 ) ) ) = ( ( ∗ ‘ ( 𝐶 − 𝐴 ) ) · ( 𝐶 − 𝐴 ) ) ) |
23 |
9
|
cjmulrcld |
⊢ ( 𝜑 → ( ( 𝐶 − 𝐴 ) · ( ∗ ‘ ( 𝐶 − 𝐴 ) ) ) ∈ ℝ ) |
24 |
22 23
|
eqeltrrd |
⊢ ( 𝜑 → ( ( ∗ ‘ ( 𝐶 − 𝐴 ) ) · ( 𝐶 − 𝐴 ) ) ∈ ℝ ) |
25 |
14 9 15 11
|
mulne0d |
⊢ ( 𝜑 → ( ( ∗ ‘ ( 𝐶 − 𝐴 ) ) · ( 𝐶 − 𝐴 ) ) ≠ 0 ) |
26 |
21 24 25
|
redivcld |
⊢ ( 𝜑 → ( ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) · ( 𝐶 − 𝐴 ) ) / ( ( ∗ ‘ ( 𝐶 − 𝐴 ) ) · ( 𝐶 − 𝐴 ) ) ) ∈ ℝ ) |
27 |
16 26
|
eqeltrrd |
⊢ ( 𝜑 → ( ( ∗ ‘ ( 𝐵 − 𝐴 ) ) / ( ∗ ‘ ( 𝐶 − 𝐴 ) ) ) ∈ ℝ ) |
28 |
12 27
|
eqeltrd |
⊢ ( 𝜑 → ( ∗ ‘ ( ( 𝐵 − 𝐴 ) / ( 𝐶 − 𝐴 ) ) ) ∈ ℝ ) |
29 |
28
|
cjred |
⊢ ( 𝜑 → ( ∗ ‘ ( ∗ ‘ ( ( 𝐵 − 𝐴 ) / ( 𝐶 − 𝐴 ) ) ) ) = ( ∗ ‘ ( ( 𝐵 − 𝐴 ) / ( 𝐶 − 𝐴 ) ) ) ) |
30 |
7 9 11
|
divcld |
⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) / ( 𝐶 − 𝐴 ) ) ∈ ℂ ) |
31 |
30
|
cjcjd |
⊢ ( 𝜑 → ( ∗ ‘ ( ∗ ‘ ( ( 𝐵 − 𝐴 ) / ( 𝐶 − 𝐴 ) ) ) ) = ( ( 𝐵 − 𝐴 ) / ( 𝐶 − 𝐴 ) ) ) |
32 |
29 31
|
eqtr3d |
⊢ ( 𝜑 → ( ∗ ‘ ( ( 𝐵 − 𝐴 ) / ( 𝐶 − 𝐴 ) ) ) = ( ( 𝐵 − 𝐴 ) / ( 𝐶 − 𝐴 ) ) ) |
33 |
32 28
|
eqeltrrd |
⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) / ( 𝐶 − 𝐴 ) ) ∈ ℝ ) |