# 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 ${⊢}\left({A}\in ℂ\wedge \left|{A}\right|=1\wedge ¬1={A}\right)\to \Im \left(\mathrm{log}\left(1-{A}\right)\right)\ne \mathrm{\pi }$

### Proof

Step Hyp Ref Expression
1 ax-1cn ${⊢}1\in ℂ$
2 1 a1i ${⊢}{A}\in ℂ\to 1\in ℂ$
3 id ${⊢}{A}\in ℂ\to {A}\in ℂ$
4 2 3 subcld ${⊢}{A}\in ℂ\to 1-{A}\in ℂ$
5 4 adantr ${⊢}\left({A}\in ℂ\wedge ¬1={A}\right)\to 1-{A}\in ℂ$
6 subeq0 ${⊢}\left(1\in ℂ\wedge {A}\in ℂ\right)\to \left(1-{A}=0↔1={A}\right)$
7 6 biimpd ${⊢}\left(1\in ℂ\wedge {A}\in ℂ\right)\to \left(1-{A}=0\to 1={A}\right)$
8 7 idiALT ${⊢}\left(1\in ℂ\wedge {A}\in ℂ\right)\to \left(1-{A}=0\to 1={A}\right)$
9 1 3 8 sylancr ${⊢}{A}\in ℂ\to \left(1-{A}=0\to 1={A}\right)$
10 9 con3d ${⊢}{A}\in ℂ\to \left(¬1={A}\to ¬1-{A}=0\right)$
11 df-ne ${⊢}1-{A}\ne 0↔¬1-{A}=0$
12 11 biimpri ${⊢}¬1-{A}=0\to 1-{A}\ne 0$
13 10 12 syl6 ${⊢}{A}\in ℂ\to \left(¬1={A}\to 1-{A}\ne 0\right)$
14 13 imp ${⊢}\left({A}\in ℂ\wedge ¬1={A}\right)\to 1-{A}\ne 0$
15 5 14 logcld ${⊢}\left({A}\in ℂ\wedge ¬1={A}\right)\to \mathrm{log}\left(1-{A}\right)\in ℂ$
16 15 imcld ${⊢}\left({A}\in ℂ\wedge ¬1={A}\right)\to \Im \left(\mathrm{log}\left(1-{A}\right)\right)\in ℝ$
17 16 3adant2 ${⊢}\left({A}\in ℂ\wedge \left|{A}\right|=1\wedge ¬1={A}\right)\to \Im \left(\mathrm{log}\left(1-{A}\right)\right)\in ℝ$
18 pire ${⊢}\mathrm{\pi }\in ℝ$
19 2re ${⊢}2\in ℝ$
20 2ne0 ${⊢}2\ne 0$
21 18 19 20 redivcli ${⊢}\frac{\mathrm{\pi }}{2}\in ℝ$
22 21 a1i ${⊢}\left({A}\in ℂ\wedge \left|{A}\right|=1\wedge ¬1={A}\right)\to \frac{\mathrm{\pi }}{2}\in ℝ$
23 18 a1i ${⊢}\left({A}\in ℂ\wedge \left|{A}\right|=1\wedge ¬1={A}\right)\to \mathrm{\pi }\in ℝ$
24 neghalfpirx ${⊢}-\frac{\mathrm{\pi }}{2}\in {ℝ}^{*}$
25 21 rexri ${⊢}\frac{\mathrm{\pi }}{2}\in {ℝ}^{*}$
26 3 recld ${⊢}{A}\in ℂ\to \Re \left({A}\right)\in ℝ$
27 26 recnd ${⊢}{A}\in ℂ\to \Re \left({A}\right)\in ℂ$
28 27 subidd ${⊢}{A}\in ℂ\to \Re \left({A}\right)-\Re \left({A}\right)=0$
29 28 adantr ${⊢}\left({A}\in ℂ\wedge \left|{A}\right|=1\right)\to \Re \left({A}\right)-\Re \left({A}\right)=0$
30 1re ${⊢}1\in ℝ$
31 30 a1i ${⊢}1\in ℂ\to 1\in ℝ$
32 1 31 ax-mp ${⊢}1\in ℝ$
33 3 releabsd ${⊢}{A}\in ℂ\to \Re \left({A}\right)\le \left|{A}\right|$
34 33 adantr ${⊢}\left({A}\in ℂ\wedge \left|{A}\right|=1\right)\to \Re \left({A}\right)\le \left|{A}\right|$
35 id ${⊢}\left|{A}\right|=1\to \left|{A}\right|=1$
36 35 adantl ${⊢}\left({A}\in ℂ\wedge \left|{A}\right|=1\right)\to \left|{A}\right|=1$
37 34 36 breqtrd ${⊢}\left({A}\in ℂ\wedge \left|{A}\right|=1\right)\to \Re \left({A}\right)\le 1$
38 lesub1 ${⊢}\left(\Re \left({A}\right)\in ℝ\wedge 1\in ℝ\wedge \Re \left({A}\right)\in ℝ\right)\to \left(\Re \left({A}\right)\le 1↔\Re \left({A}\right)-\Re \left({A}\right)\le 1-\Re \left({A}\right)\right)$
39 38 3impcombi ${⊢}\left(1\in ℝ\wedge \Re \left({A}\right)\in ℝ\wedge \Re \left({A}\right)\le 1\right)\to \Re \left({A}\right)-\Re \left({A}\right)\le 1-\Re \left({A}\right)$
40 39 idiALT ${⊢}\left(1\in ℝ\wedge \Re \left({A}\right)\in ℝ\wedge \Re \left({A}\right)\le 1\right)\to \Re \left({A}\right)-\Re \left({A}\right)\le 1-\Re \left({A}\right)$
41 32 26 37 40 mp3an2ani ${⊢}\left({A}\in ℂ\wedge \left|{A}\right|=1\right)\to \Re \left({A}\right)-\Re \left({A}\right)\le 1-\Re \left({A}\right)$
42 29 41 eqbrtrrd ${⊢}\left({A}\in ℂ\wedge \left|{A}\right|=1\right)\to 0\le 1-\Re \left({A}\right)$
43 32 a1i ${⊢}\top \to 1\in ℝ$
44 43 rered ${⊢}\top \to \Re \left(1\right)=1$
45 44 mptru ${⊢}\Re \left(1\right)=1$
46 oveq1 ${⊢}\Re \left(1\right)=1\to \Re \left(1\right)-\Re \left({A}\right)=1-\Re \left({A}\right)$
47 46 eqcomd ${⊢}\Re \left(1\right)=1\to 1-\Re \left({A}\right)=\Re \left(1\right)-\Re \left({A}\right)$
48 45 47 ax-mp ${⊢}1-\Re \left({A}\right)=\Re \left(1\right)-\Re \left({A}\right)$
49 resub ${⊢}\left(1\in ℂ\wedge {A}\in ℂ\right)\to \Re \left(1-{A}\right)=\Re \left(1\right)-\Re \left({A}\right)$
50 49 eqcomd ${⊢}\left(1\in ℂ\wedge {A}\in ℂ\right)\to \Re \left(1\right)-\Re \left({A}\right)=\Re \left(1-{A}\right)$
51 50 idiALT ${⊢}\left(1\in ℂ\wedge {A}\in ℂ\right)\to \Re \left(1\right)-\Re \left({A}\right)=\Re \left(1-{A}\right)$
52 1 3 51 sylancr ${⊢}{A}\in ℂ\to \Re \left(1\right)-\Re \left({A}\right)=\Re \left(1-{A}\right)$
53 48 52 syl5eq ${⊢}{A}\in ℂ\to 1-\Re \left({A}\right)=\Re \left(1-{A}\right)$
54 53 adantr ${⊢}\left({A}\in ℂ\wedge \left|{A}\right|=1\right)\to 1-\Re \left({A}\right)=\Re \left(1-{A}\right)$
55 42 54 breqtrd ${⊢}\left({A}\in ℂ\wedge \left|{A}\right|=1\right)\to 0\le \Re \left(1-{A}\right)$
56 argrege0 ${⊢}\left(1-{A}\in ℂ\wedge 1-{A}\ne 0\wedge 0\le \Re \left(1-{A}\right)\right)\to \Im \left(\mathrm{log}\left(1-{A}\right)\right)\in \left[-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right]$
57 56 3coml ${⊢}\left(1-{A}\ne 0\wedge 0\le \Re \left(1-{A}\right)\wedge 1-{A}\in ℂ\right)\to \Im \left(\mathrm{log}\left(1-{A}\right)\right)\in \left[-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right]$
58 57 3com13 ${⊢}\left(1-{A}\in ℂ\wedge 0\le \Re \left(1-{A}\right)\wedge 1-{A}\ne 0\right)\to \Im \left(\mathrm{log}\left(1-{A}\right)\right)\in \left[-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right]$
59 4 55 14 58 eel12131 ${⊢}\left({A}\in ℂ\wedge \left|{A}\right|=1\wedge ¬1={A}\right)\to \Im \left(\mathrm{log}\left(1-{A}\right)\right)\in \left[-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right]$
60 iccleub ${⊢}\left(-\frac{\mathrm{\pi }}{2}\in {ℝ}^{*}\wedge \frac{\mathrm{\pi }}{2}\in {ℝ}^{*}\wedge \Im \left(\mathrm{log}\left(1-{A}\right)\right)\in \left[-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right]\right)\to \Im \left(\mathrm{log}\left(1-{A}\right)\right)\le \frac{\mathrm{\pi }}{2}$
61 24 25 59 60 mp3an12i ${⊢}\left({A}\in ℂ\wedge \left|{A}\right|=1\wedge ¬1={A}\right)\to \Im \left(\mathrm{log}\left(1-{A}\right)\right)\le \frac{\mathrm{\pi }}{2}$
62 pipos ${⊢}0<\mathrm{\pi }$
63 18 62 elrpii ${⊢}\mathrm{\pi }\in {ℝ}^{+}$
64 rphalflt ${⊢}\mathrm{\pi }\in {ℝ}^{+}\to \frac{\mathrm{\pi }}{2}<\mathrm{\pi }$
65 63 64 ax-mp ${⊢}\frac{\mathrm{\pi }}{2}<\mathrm{\pi }$
66 65 a1i ${⊢}\left({A}\in ℂ\wedge \left|{A}\right|=1\wedge ¬1={A}\right)\to \frac{\mathrm{\pi }}{2}<\mathrm{\pi }$
67 17 22 23 61 66 lelttrd ${⊢}\left({A}\in ℂ\wedge \left|{A}\right|=1\wedge ¬1={A}\right)\to \Im \left(\mathrm{log}\left(1-{A}\right)\right)<\mathrm{\pi }$
68 17 67 ltned ${⊢}\left({A}\in ℂ\wedge \left|{A}\right|=1\wedge ¬1={A}\right)\to \Im \left(\mathrm{log}\left(1-{A}\right)\right)\ne \mathrm{\pi }$