Theorem isosctrlem1ALTVD
Description: Lemma for isosctr. The proof of isosctrlem1ALTVD is a Virtual Deduction proof based on Saveliy Skresanov's proof of isosctrlem1. The proof of isosctrlem1ALTVD is verified by automatically transforming it into the Metamath proof of isosctrlem1ALT using completeusersproof, which is verified by the Metamath program. The proof of isosctrlem1ALTRO is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. (Contributed by Alan Sare, 22-Apr-2018.)
Assertion
Ref Expression
isosctrlem1ALTVD (   (   𝐴 ∈ ℂ   ,   (abs‘𝐴) = 1   ,    ¬ 1 = 𝐴   )   ▶   (ℑ‘(log‘(1 − 𝐴))) ≠ 𝜋   )

Proof of Theorem isosctrlem1ALTVD
StepHypExpression
1  (   𝐴 ∈ ℂ   ▶   𝐴 ∈ ℂ   )
2  1 ∈ ℂ
31, 2 (   𝐴 ∈ ℂ   ▶   ((1 − 𝐴) = 0 → 1 = 𝐴)   )
43 (   𝐴 ∈ ℂ   ▶   (¬ 1 = 𝐴 → ¬ (1 − 𝐴) = 0)   )
5  (¬ (1 − 𝐴) = 0 → (1 − 𝐴) ≠ 0)
64, 5 (   𝐴 ∈ ℂ   ▶   (¬ 1 = 𝐴 → (1 − 𝐴) ≠ 0)   )
76 (   (   𝐴 ∈ ℂ   ,   ¬ 1 = 𝐴   )   ▶   (1 − 𝐴) ≠ 0   )
81 (   𝐴 ∈ ℂ   ▶   (ℜ‘𝐴) ≤ (abs‘𝐴)   )
9  (   (abs‘𝐴) = 1   ▶   (abs‘𝐴) = 1   )
108, 9 (   (   𝐴 ∈ ℂ   ,   (abs‘𝐴) = 1   )   ▶   (ℜ‘𝐴) ≤ 1   )
111 (   𝐴 ∈ ℂ   ▶   (ℜ‘𝐴) ∈ ℝ   )
122 1 ∈ ℝ
1311, 12, 10 (   (   𝐴 ∈ ℂ   ,   (abs‘𝐴) = 1   )   ▶   ((ℜ‘𝐴) − (ℜ‘𝐴)) ≤ (1 − (ℜ‘𝐴))   )
141 (   𝐴 ∈ ℂ   ▶   (ℜ‘𝐴) ∈ ℝ   )
1514 (   𝐴 ∈ ℂ   ▶   (ℜ‘𝐴) ∈ ℂ   )
1615 (   𝐴 ∈ ℂ   ▶   ((ℜ‘𝐴) − (ℜ‘𝐴)) = 0   )
1713, 16 (   (   𝐴 ∈ ℂ   ,   (abs‘𝐴) = 1   )   ▶   0 ≤ (1 − (ℜ‘𝐴))   )
1812 (ℜ‘1) = 1
1918 (1 − (ℜ‘𝐴)) = ((ℜ‘1) − (ℜ‘𝐴))
201, 2 (   𝐴 ∈ ℂ   ▶   ((ℜ‘1) − (ℜ‘𝐴)) = (ℜ‘(1 − 𝐴))   )
2119, 20 (   𝐴 ∈ ℂ   ▶   (1 − (ℜ‘𝐴)) = (ℜ‘(1 − 𝐴))   )
2217, 21 (   (   𝐴 ∈ ℂ   ,   (abs‘𝐴) = 1   )   ▶   0 ≤ (ℜ‘(1 − 𝐴))   )
231, 2 (   𝐴 ∈ ℂ   ▶   (1 − 𝐴) ∈ ℂ   )
2423, 7, 22 (   (   𝐴 ∈ ℂ   ,   (abs‘𝐴) = 1   ,   ¬ 1 = 𝐴   )   ▶   (ℑ‘(log‘(1 − 𝐴))) ∈ (-(𝜋 / 2)[,](𝜋 / 2))   )
25  𝜋 ∈ ℝ
26  2 ∈ ℝ
27  2 ≠ 0
2825, 26, 27 (𝜋 / 2) ∈ ℝ
2928 (𝜋 / 2) ∈ ℝ*
3028 -(𝜋 / 2) ∈ ℝ
3130 -(𝜋 / 2) ∈ ℝ*
3231, 29, 24 (   (   𝐴 ∈ ℂ   ,   (abs‘𝐴) = 1   ,   ¬ 1 = 𝐴   )   ▶   (ℑ‘(log‘(1 − 𝐴))) ≤ (𝜋 / 2)   )
33  0 < 𝜋
3433, 25 𝜋 ∈ ℝ+
3534 (𝜋 / 2) < 𝜋
367, 23 (   (   𝐴 ∈ ℂ   ,   ¬ 1 = 𝐴   )   ▶   (log‘(1 − 𝐴)) ∈ ℂ   )
3736 (   (   𝐴 ∈ ℂ   ,   ¬ 1 = 𝐴   )   ▶   (ℑ‘(log‘(1 − 𝐴))) ∈ ℝ   )
3837, 28, 25, 32, 35 (   (   𝐴 ∈ ℂ   ,   (abs‘𝐴) = 1   ,   ¬ 1 = 𝐴   )   ▶   (ℑ‘(log‘(1 − 𝐴))) < 𝜋   )
qed38, 37 (   (   𝐴 ∈ ℂ   ,   (abs‘𝐴) = 1   ,   ¬ 1 = 𝐴   )   ▶   (ℑ‘(log‘(1 − 𝐴))) ≠ 𝜋   )
 Copyright terms: Public domain W3C validator