Metamath Proof Explorer

Theorem isosctrlem1ALT

Description: Lemma for isosctr . This proof was automatically derived by completeusersproof from its Virtual Deduction proof counterpart https://us.metamath.org/other/completeusersproof/isosctrlem1altvd.html . As it is verified by the Metamath program, isosctrlem1ALT verifies https://us.metamath.org/other/completeusersproof/isosctrlem1altvd.html . (Contributed by Alan Sare, 22-Apr-2018) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion isosctrlem1ALT ⊢ A ∈ ℂ ∧ A = 1 ∧ ¬ 1 = A → ℑ ⁡ log ⁡ 1 − A ≠ π

Proof

Step Hyp Ref Expression
1 ax-1cn ⊢ 1 ∈ ℂ
2 1 a1i ⊢ A ∈ ℂ → 1 ∈ ℂ
3 id ⊢ A ∈ ℂ → A ∈ ℂ
4 2 3 subcld ⊢ A ∈ ℂ → 1 − A ∈ ℂ
5 4 adantr ⊢ A ∈ ℂ ∧ ¬ 1 = A → 1 − A ∈ ℂ
6 subeq0 ⊢ 1 ∈ ℂ ∧ A ∈ ℂ → 1 − A = 0 ↔ 1 = A
7 6 biimpd ⊢ 1 ∈ ℂ ∧ A ∈ ℂ → 1 − A = 0 → 1 = A
8 7 idiALT ⊢ 1 ∈ ℂ ∧ A ∈ ℂ → 1 − A = 0 → 1 = A
9 1 3 8 sylancr ⊢ A ∈ ℂ → 1 − A = 0 → 1 = A
10 9 con3d ⊢ A ∈ ℂ → ¬ 1 = A → ¬ 1 − A = 0
11 df-ne ⊢ 1 − A ≠ 0 ↔ ¬ 1 − A = 0
12 11 biimpri ⊢ ¬ 1 − A = 0 → 1 − A ≠ 0
13 10 12 syl6 ⊢ A ∈ ℂ → ¬ 1 = A → 1 − A ≠ 0
14 13 imp ⊢ A ∈ ℂ ∧ ¬ 1 = A → 1 − A ≠ 0
15 5 14 logcld ⊢ A ∈ ℂ ∧ ¬ 1 = A → log ⁡ 1 − A ∈ ℂ
16 15 imcld ⊢ A ∈ ℂ ∧ ¬ 1 = A → ℑ ⁡ log ⁡ 1 − A ∈ ℝ
17 16 3adant2 ⊢ A ∈ ℂ ∧ A = 1 ∧ ¬ 1 = A → ℑ ⁡ log ⁡ 1 − A ∈ ℝ
18 pire ⊢ π ∈ ℝ
19 2re ⊢ 2 ∈ ℝ
20 2ne0 ⊢ 2 ≠ 0
21 18 19 20 redivcli ⊢ π 2 ∈ ℝ
22 21 a1i ⊢ A ∈ ℂ ∧ A = 1 ∧ ¬ 1 = A → π 2 ∈ ℝ
23 18 a1i ⊢ A ∈ ℂ ∧ A = 1 ∧ ¬ 1 = A → π ∈ ℝ
24 neghalfpirx ⊢ − π 2 ∈ ℝ *
25 21 rexri ⊢ π 2 ∈ ℝ *
26 3 recld ⊢ A ∈ ℂ → ℜ ⁡ A ∈ ℝ
27 26 recnd ⊢ A ∈ ℂ → ℜ ⁡ A ∈ ℂ
28 27 subidd ⊢ A ∈ ℂ → ℜ ⁡ A − ℜ ⁡ A = 0
29 28 adantr ⊢ A ∈ ℂ ∧ A = 1 → ℜ ⁡ A − ℜ ⁡ A = 0
30 1re ⊢ 1 ∈ ℝ
31 30 a1i ⊢ 1 ∈ ℂ → 1 ∈ ℝ
32 1 31 ax-mp ⊢ 1 ∈ ℝ
33 3 releabsd ⊢ A ∈ ℂ → ℜ ⁡ A ≤ A
34 33 adantr ⊢ A ∈ ℂ ∧ A = 1 → ℜ ⁡ A ≤ A
35 id ⊢ A = 1 → A = 1
36 35 adantl ⊢ A ∈ ℂ ∧ A = 1 → A = 1
37 34 36 breqtrd ⊢ A ∈ ℂ ∧ A = 1 → ℜ ⁡ A ≤ 1
38 lesub1 ⊢ ℜ ⁡ A ∈ ℝ ∧ 1 ∈ ℝ ∧ ℜ ⁡ A ∈ ℝ → ℜ ⁡ A ≤ 1 ↔ ℜ ⁡ A − ℜ ⁡ A ≤ 1 − ℜ ⁡ A
39 38 3impcombi ⊢ 1 ∈ ℝ ∧ ℜ ⁡ A ∈ ℝ ∧ ℜ ⁡ A ≤ 1 → ℜ ⁡ A − ℜ ⁡ A ≤ 1 − ℜ ⁡ A
40 39 idiALT ⊢ 1 ∈ ℝ ∧ ℜ ⁡ A ∈ ℝ ∧ ℜ ⁡ A ≤ 1 → ℜ ⁡ A − ℜ ⁡ A ≤ 1 − ℜ ⁡ A
41 32 26 37 40 mp3an2ani ⊢ A ∈ ℂ ∧ A = 1 → ℜ ⁡ A − ℜ ⁡ A ≤ 1 − ℜ ⁡ A
42 29 41 eqbrtrrd ⊢ A ∈ ℂ ∧ A = 1 → 0 ≤ 1 − ℜ ⁡ A
43 32 a1i ⊢ ⊤ → 1 ∈ ℝ
44 43 rered ⊢ ⊤ → ℜ ⁡ 1 = 1
45 44 mptru ⊢ ℜ ⁡ 1 = 1
46 oveq1 ⊢ ℜ ⁡ 1 = 1 → ℜ ⁡ 1 − ℜ ⁡ A = 1 − ℜ ⁡ A
47 46 eqcomd ⊢ ℜ ⁡ 1 = 1 → 1 − ℜ ⁡ A = ℜ ⁡ 1 − ℜ ⁡ A
48 45 47 ax-mp ⊢ 1 − ℜ ⁡ A = ℜ ⁡ 1 − ℜ ⁡ A
49 resub ⊢ 1 ∈ ℂ ∧ A ∈ ℂ → ℜ ⁡ 1 − A = ℜ ⁡ 1 − ℜ ⁡ A
50 49 eqcomd ⊢ 1 ∈ ℂ ∧ A ∈ ℂ → ℜ ⁡ 1 − ℜ ⁡ A = ℜ ⁡ 1 − A
51 50 idiALT ⊢ 1 ∈ ℂ ∧ A ∈ ℂ → ℜ ⁡ 1 − ℜ ⁡ A = ℜ ⁡ 1 − A
52 1 3 51 sylancr ⊢ A ∈ ℂ → ℜ ⁡ 1 − ℜ ⁡ A = ℜ ⁡ 1 − A
53 48 52 eqtrid ⊢ A ∈ ℂ → 1 − ℜ ⁡ A = ℜ ⁡ 1 − A
54 53 adantr ⊢ A ∈ ℂ ∧ A = 1 → 1 − ℜ ⁡ A = ℜ ⁡ 1 − A
55 42 54 breqtrd ⊢ A ∈ ℂ ∧ A = 1 → 0 ≤ ℜ ⁡ 1 − A
56 argrege0 ⊢ 1 − A ∈ ℂ ∧ 1 − A ≠ 0 ∧ 0 ≤ ℜ ⁡ 1 − A → ℑ ⁡ log ⁡ 1 − A ∈ − π 2 π 2
57 56 3coml ⊢ 1 − A ≠ 0 ∧ 0 ≤ ℜ ⁡ 1 − A ∧ 1 − A ∈ ℂ → ℑ ⁡ log ⁡ 1 − A ∈ − π 2 π 2
58 57 3com13 ⊢ 1 − A ∈ ℂ ∧ 0 ≤ ℜ ⁡ 1 − A ∧ 1 − A ≠ 0 → ℑ ⁡ log ⁡ 1 − A ∈ − π 2 π 2
59 4 55 14 58 eel12131 ⊢ A ∈ ℂ ∧ A = 1 ∧ ¬ 1 = A → ℑ ⁡ log ⁡ 1 − A ∈ − π 2 π 2
60 iccleub ⊢ − π 2 ∈ ℝ * ∧ π 2 ∈ ℝ * ∧ ℑ ⁡ log ⁡ 1 − A ∈ − π 2 π 2 → ℑ ⁡ log ⁡ 1 − A ≤ π 2
61 24 25 59 60 mp3an12i ⊢ A ∈ ℂ ∧ A = 1 ∧ ¬ 1 = A → ℑ ⁡ log ⁡ 1 − A ≤ π 2
62 pipos ⊢ 0 < π
63 18 62 elrpii ⊢ π ∈ ℝ +
64 rphalflt ⊢ π ∈ ℝ + → π 2 < π
65 63 64 ax-mp ⊢ π 2 < π
66 65 a1i ⊢ A ∈ ℂ ∧ A = 1 ∧ ¬ 1 = A → π 2 < π
67 17 22 23 61 66 lelttrd ⊢ A ∈ ℂ ∧ A = 1 ∧ ¬ 1 = A → ℑ ⁡ log ⁡ 1 − A < π
68 17 67 ltned ⊢ A ∈ ℂ ∧ A = 1 ∧ ¬ 1 = A → ℑ ⁡ log ⁡ 1 − A ≠ π