Metamath Proof Explorer

Theorem angcan

Description: Cancel a constant multiplier in the angle function. (Contributed by Mario Carneiro, 23-Sep-2014)

Ref Expression
Hypothesis ang.1 ⊢ F = x ∈ ℂ ∖ 0 , y ∈ ℂ ∖ 0 ⟼ ℑ ⁡ log ⁡ y x
Assertion angcan ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A F C ⁢ B = A F B

Proof

Step Hyp Ref Expression
1 ang.1 ⊢ F = x ∈ ℂ ∖ 0 , y ∈ ℂ ∖ 0 ⟼ ℑ ⁡ log ⁡ y x
2 simp2l ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → B ∈ ℂ
3 simp1l ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A ∈ ℂ
4 simp3l ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → C ∈ ℂ
5 simp1r ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A ≠ 0
6 simp3r ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → C ≠ 0
7 2 3 4 5 6 divcan5d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ B C ⁢ A = B A
8 7 fveq2d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → log ⁡ C ⁢ B C ⁢ A = log ⁡ B A
9 8 fveq2d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → ℑ ⁡ log ⁡ C ⁢ B C ⁢ A = ℑ ⁡ log ⁡ B A
10 4 3 mulcld ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A ∈ ℂ
11 4 3 6 5 mulne0d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A ≠ 0
12 4 2 mulcld ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ B ∈ ℂ
13 simp2r ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → B ≠ 0
14 4 2 6 13 mulne0d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ B ≠ 0
15 1 angval ⊢ C ⁢ A ∈ ℂ ∧ C ⁢ A ≠ 0 ∧ C ⁢ B ∈ ℂ ∧ C ⁢ B ≠ 0 → C ⁢ A F C ⁢ B = ℑ ⁡ log ⁡ C ⁢ B C ⁢ A
16 10 11 12 14 15 syl22anc ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A F C ⁢ B = ℑ ⁡ log ⁡ C ⁢ B C ⁢ A
17 1 angval ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → A F B = ℑ ⁡ log ⁡ B A
18 17 3adant3 ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A F B = ℑ ⁡ log ⁡ B A
19 9 16 18 3eqtr4d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A F C ⁢ B = A F B