Step |
Hyp |
Ref |
Expression |
1 |
|
ang.1 |
⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) ) |
2 |
|
simp2l |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → 𝐵 ∈ ℂ ) |
3 |
|
simp1l |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → 𝐴 ∈ ℂ ) |
4 |
|
simp3l |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → 𝐶 ∈ ℂ ) |
5 |
|
simp1r |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → 𝐴 ≠ 0 ) |
6 |
|
simp3r |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → 𝐶 ≠ 0 ) |
7 |
2 3 4 5 6
|
divcan5d |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐶 · 𝐵 ) / ( 𝐶 · 𝐴 ) ) = ( 𝐵 / 𝐴 ) ) |
8 |
7
|
fveq2d |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( log ‘ ( ( 𝐶 · 𝐵 ) / ( 𝐶 · 𝐴 ) ) ) = ( log ‘ ( 𝐵 / 𝐴 ) ) ) |
9 |
8
|
fveq2d |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ℑ ‘ ( log ‘ ( ( 𝐶 · 𝐵 ) / ( 𝐶 · 𝐴 ) ) ) ) = ( ℑ ‘ ( log ‘ ( 𝐵 / 𝐴 ) ) ) ) |
10 |
4 3
|
mulcld |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐶 · 𝐴 ) ∈ ℂ ) |
11 |
4 3 6 5
|
mulne0d |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐶 · 𝐴 ) ≠ 0 ) |
12 |
4 2
|
mulcld |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐶 · 𝐵 ) ∈ ℂ ) |
13 |
|
simp2r |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → 𝐵 ≠ 0 ) |
14 |
4 2 6 13
|
mulne0d |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐶 · 𝐵 ) ≠ 0 ) |
15 |
1
|
angval |
⊢ ( ( ( ( 𝐶 · 𝐴 ) ∈ ℂ ∧ ( 𝐶 · 𝐴 ) ≠ 0 ) ∧ ( ( 𝐶 · 𝐵 ) ∈ ℂ ∧ ( 𝐶 · 𝐵 ) ≠ 0 ) ) → ( ( 𝐶 · 𝐴 ) 𝐹 ( 𝐶 · 𝐵 ) ) = ( ℑ ‘ ( log ‘ ( ( 𝐶 · 𝐵 ) / ( 𝐶 · 𝐴 ) ) ) ) ) |
16 |
10 11 12 14 15
|
syl22anc |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐶 · 𝐴 ) 𝐹 ( 𝐶 · 𝐵 ) ) = ( ℑ ‘ ( log ‘ ( ( 𝐶 · 𝐵 ) / ( 𝐶 · 𝐴 ) ) ) ) ) |
17 |
1
|
angval |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 𝐹 𝐵 ) = ( ℑ ‘ ( log ‘ ( 𝐵 / 𝐴 ) ) ) ) |
18 |
17
|
3adant3 |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐴 𝐹 𝐵 ) = ( ℑ ‘ ( log ‘ ( 𝐵 / 𝐴 ) ) ) ) |
19 |
9 16 18
|
3eqtr4d |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐶 · 𝐴 ) 𝐹 ( 𝐶 · 𝐵 ) ) = ( 𝐴 𝐹 𝐵 ) ) |