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

Step	Hyp	Expression
1		⊢ (   𝐴 ∈ ℂ   ▶   𝐴 ∈ ℂ   )
2		⊢ 1 ∈ ℂ
3	1, 2	⊢ (   𝐴 ∈ ℂ   ▶   ((1 − 𝐴) = 0 → 1 = 𝐴)   )
4	3	⊢ (   𝐴 ∈ ℂ   ▶   (¬ 1 = 𝐴 → ¬ (1 − 𝐴) = 0)   )
5		⊢ (¬ (1 − 𝐴) = 0 → (1 − 𝐴) ≠ 0)
6	4, 5	⊢ (   𝐴 ∈ ℂ   ▶   (¬ 1 = 𝐴 → (1 − 𝐴) ≠ 0)   )
7	6	⊢ (   (   𝐴 ∈ ℂ   ,   ¬ 1 = 𝐴   )   ▶   (1 − 𝐴) ≠ 0   )
8	1	⊢ (   𝐴 ∈ ℂ   ▶   (ℜ‘𝐴) ≤ (abs‘𝐴)   )
9		⊢ (   (abs‘𝐴) = 1   ▶   (abs‘𝐴) = 1   )
10	8, 9	⊢ (   (   𝐴 ∈ ℂ   ,   (abs‘𝐴) = 1   )   ▶   (ℜ‘𝐴) ≤ 1   )
11	1	⊢ (   𝐴 ∈ ℂ   ▶   (ℜ‘𝐴) ∈ ℝ   )
12	2	⊢ 1 ∈ ℝ
13	11, 12, 10	⊢ (   (   𝐴 ∈ ℂ   ,   (abs‘𝐴) = 1   )   ▶   ((ℜ‘𝐴) − (ℜ‘𝐴)) ≤ (1 − (ℜ‘𝐴))   )
14	1	⊢ (   𝐴 ∈ ℂ   ▶   (ℜ‘𝐴) ∈ ℝ   )
15	14	⊢ (   𝐴 ∈ ℂ   ▶   (ℜ‘𝐴) ∈ ℂ   )
16	15	⊢ (   𝐴 ∈ ℂ   ▶   ((ℜ‘𝐴) − (ℜ‘𝐴)) = 0   )
17	13, 16	⊢ (   (   𝐴 ∈ ℂ   ,   (abs‘𝐴) = 1   )   ▶   0 ≤ (1 − (ℜ‘𝐴))   )
18	12	⊢ (ℜ‘1) = 1
19	18	⊢ (1 − (ℜ‘𝐴)) = ((ℜ‘1) − (ℜ‘𝐴))
20	1, 2	⊢ (   𝐴 ∈ ℂ   ▶   ((ℜ‘1) − (ℜ‘𝐴)) = (ℜ‘(1 − 𝐴))   )
21	19, 20	⊢ (   𝐴 ∈ ℂ   ▶   (1 − (ℜ‘𝐴)) = (ℜ‘(1 − 𝐴))   )
22	17, 21	⊢ (   (   𝐴 ∈ ℂ   ,   (abs‘𝐴) = 1   )   ▶   0 ≤ (ℜ‘(1 − 𝐴))   )
23	1, 2	⊢ (   𝐴 ∈ ℂ   ▶   (1 − 𝐴) ∈ ℂ   )
24	23, 7, 22	⊢ (   (   𝐴 ∈ ℂ   ,   (abs‘𝐴) = 1   ,   ¬ 1 = 𝐴   )   ▶   (ℑ‘(log‘(1 − 𝐴))) ∈ (-(𝜋 / 2)[,](𝜋 / 2))   )
25		⊢ 𝜋 ∈ ℝ
26		⊢ 2 ∈ ℝ
27		⊢ 2 ≠ 0
28	25, 26, 27	⊢ (𝜋 / 2) ∈ ℝ
29	28	⊢ (𝜋 / 2) ∈ ℝ*
30	28	⊢ -(𝜋 / 2) ∈ ℝ
31	30	⊢ -(𝜋 / 2) ∈ ℝ*
32	31, 29, 24	⊢ (   (   𝐴 ∈ ℂ   ,   (abs‘𝐴) = 1   ,   ¬ 1 = 𝐴   )   ▶   (ℑ‘(log‘(1 − 𝐴))) ≤ (𝜋 / 2)   )
33		⊢ 0 < 𝜋
34	33, 25	⊢ 𝜋 ∈ ℝ+
35	34	⊢ (𝜋 / 2) < 𝜋
36	7, 23	⊢ (   (   𝐴 ∈ ℂ   ,   ¬ 1 = 𝐴   )   ▶   (log‘(1 − 𝐴)) ∈ ℂ   )
37	36	⊢ (   (   𝐴 ∈ ℂ   ,   ¬ 1 = 𝐴   )   ▶   (ℑ‘(log‘(1 − 𝐴))) ∈ ℝ   )
38	37, 28, 25, 32, 35	⊢ (   (   𝐴 ∈ ℂ   ,   (abs‘𝐴) = 1   ,   ¬ 1 = 𝐴   )   ▶   (ℑ‘(log‘(1 − 𝐴))) < 𝜋   )
qed	38, 37	⊢ (   (   𝐴 ∈ ℂ   ,   (abs‘𝐴) = 1   ,   ¬ 1 = 𝐴   )   ▶   (ℑ‘(log‘(1 − 𝐴))) ≠ 𝜋   )