Metamath Proof Explorer

Theorem angpieqvdlem2

Description: Equivalence used in angpieqvd . (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypotheses angpieqvd.angdef ⊢ F = x ∈ ℂ ∖ 0 , y ∈ ℂ ∖ 0 ⟼ ℑ ⁡ log ⁡ y x
angpieqvd.A ⊢ φ → A ∈ ℂ
angpieqvd.B ⊢ φ → B ∈ ℂ
angpieqvd.C ⊢ φ → C ∈ ℂ
angpieqvd.AneB ⊢ φ → A ≠ B
angpieqvd.BneC ⊢ φ → B ≠ C
Assertion angpieqvdlem2 ⊢ φ → − C − B A − B ∈ ℝ + ↔ A − B F C − B = π

Proof

Step Hyp Ref Expression
1 angpieqvd.angdef ⊢ F = x ∈ ℂ ∖ 0 , y ∈ ℂ ∖ 0 ⟼ ℑ ⁡ log ⁡ y x
2 angpieqvd.A ⊢ φ → A ∈ ℂ
3 angpieqvd.B ⊢ φ → B ∈ ℂ
4 angpieqvd.C ⊢ φ → C ∈ ℂ
5 angpieqvd.AneB ⊢ φ → A ≠ B
6 angpieqvd.BneC ⊢ φ → B ≠ C
7 4 3 subcld ⊢ φ → C − B ∈ ℂ
8 2 3 subcld ⊢ φ → A − B ∈ ℂ
9 2 3 5 subne0d ⊢ φ → A − B ≠ 0
10 7 8 9 divcld ⊢ φ → C − B A − B ∈ ℂ
11 6 necomd ⊢ φ → C ≠ B
12 4 3 11 subne0d ⊢ φ → C − B ≠ 0
13 7 8 12 9 divne0d ⊢ φ → C − B A − B ≠ 0
14 lognegb ⊢ C − B A − B ∈ ℂ ∧ C − B A − B ≠ 0 → − C − B A − B ∈ ℝ + ↔ ℑ ⁡ log ⁡ C − B A − B = π
15 10 13 14 syl2anc ⊢ φ → − C − B A − B ∈ ℝ + ↔ ℑ ⁡ log ⁡ C − B A − B = π
16 1 8 9 7 12 angvald ⊢ φ → A − B F C − B = ℑ ⁡ log ⁡ C − B A − B
17 16 eqeq1d ⊢ φ → A − B F C − B = π ↔ ℑ ⁡ log ⁡ C − B A − B = π
18 15 17 bitr4d ⊢ φ → − C − B A − B ∈ ℝ + ↔ A − B F C − B = π