Metamath Proof Explorer

Theorem isosctrlem1

Description: Lemma for isosctr . (Contributed by Saveliy Skresanov, 30-Dec-2016)

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

Proof

Step Hyp Ref Expression
1 ax-1cn ⊢ 1 ∈ ℂ
2 subcl ⊢ 1 ∈ ℂ ∧ A ∈ ℂ → 1 − A ∈ ℂ
3 1 2 mpan ⊢ A ∈ ℂ → 1 − A ∈ ℂ
4 3 adantr ⊢ A ∈ ℂ ∧ ¬ 1 = A → 1 − A ∈ ℂ
5 subeq0 ⊢ 1 ∈ ℂ ∧ A ∈ ℂ → 1 − A = 0 ↔ 1 = A
6 5 notbid ⊢ 1 ∈ ℂ ∧ A ∈ ℂ → ¬ 1 − A = 0 ↔ ¬ 1 = A
7 1 6 mpan ⊢ A ∈ ℂ → ¬ 1 − A = 0 ↔ ¬ 1 = A
8 7 biimpar ⊢ A ∈ ℂ ∧ ¬ 1 = A → ¬ 1 − A = 0
9 8 neqned ⊢ A ∈ ℂ ∧ ¬ 1 = A → 1 − A ≠ 0
10 4 9 logcld ⊢ A ∈ ℂ ∧ ¬ 1 = A → log ⁡ 1 − A ∈ ℂ
11 10 imcld ⊢ A ∈ ℂ ∧ ¬ 1 = A → ℑ ⁡ log ⁡ 1 − A ∈ ℝ
12 11 3adant2 ⊢ A ∈ ℂ ∧ A = 1 ∧ ¬ 1 = A → ℑ ⁡ log ⁡ 1 − A ∈ ℝ
13 3 3ad2ant1 ⊢ A ∈ ℂ ∧ A = 1 ∧ ¬ 1 = A → 1 − A ∈ ℂ
14 9 3adant2 ⊢ A ∈ ℂ ∧ A = 1 ∧ ¬ 1 = A → 1 − A ≠ 0
15 releabs ⊢ A ∈ ℂ → ℜ ⁡ A ≤ A
16 15 adantr ⊢ A ∈ ℂ ∧ A = 1 → ℜ ⁡ A ≤ A
17 breq2 ⊢ A = 1 → ℜ ⁡ A ≤ A ↔ ℜ ⁡ A ≤ 1
18 17 adantl ⊢ A ∈ ℂ ∧ A = 1 → ℜ ⁡ A ≤ A ↔ ℜ ⁡ A ≤ 1
19 16 18 mpbid ⊢ A ∈ ℂ ∧ A = 1 → ℜ ⁡ A ≤ 1
20 recl ⊢ A ∈ ℂ → ℜ ⁡ A ∈ ℝ
21 20 recnd ⊢ A ∈ ℂ → ℜ ⁡ A ∈ ℂ
22 21 subidd ⊢ A ∈ ℂ → ℜ ⁡ A − ℜ ⁡ A = 0
23 22 adantr ⊢ A ∈ ℂ ∧ ℜ ⁡ A ≤ 1 → ℜ ⁡ A − ℜ ⁡ A = 0
24 simpl ⊢ A ∈ ℂ ∧ ℜ ⁡ A ≤ 1 → A ∈ ℂ
25 24 recld ⊢ A ∈ ℂ ∧ ℜ ⁡ A ≤ 1 → ℜ ⁡ A ∈ ℝ
26 1red ⊢ A ∈ ℂ ∧ ℜ ⁡ A ≤ 1 → 1 ∈ ℝ
27 simpr ⊢ A ∈ ℂ ∧ ℜ ⁡ A ≤ 1 → ℜ ⁡ A ≤ 1
28 25 26 25 27 lesub1dd ⊢ A ∈ ℂ ∧ ℜ ⁡ A ≤ 1 → ℜ ⁡ A − ℜ ⁡ A ≤ 1 − ℜ ⁡ A
29 23 28 eqbrtrrd ⊢ A ∈ ℂ ∧ ℜ ⁡ A ≤ 1 → 0 ≤ 1 − ℜ ⁡ A
30 19 29 syldan ⊢ A ∈ ℂ ∧ A = 1 → 0 ≤ 1 − ℜ ⁡ A
31 resub ⊢ 1 ∈ ℂ ∧ A ∈ ℂ → ℜ ⁡ 1 − A = ℜ ⁡ 1 − ℜ ⁡ A
32 re1 ⊢ ℜ ⁡ 1 = 1
33 32 oveq1i ⊢ ℜ ⁡ 1 − ℜ ⁡ A = 1 − ℜ ⁡ A
34 31 33 eqtrdi ⊢ 1 ∈ ℂ ∧ A ∈ ℂ → ℜ ⁡ 1 − A = 1 − ℜ ⁡ A
35 1 34 mpan ⊢ A ∈ ℂ → ℜ ⁡ 1 − A = 1 − ℜ ⁡ A
36 35 adantr ⊢ A ∈ ℂ ∧ A = 1 → ℜ ⁡ 1 − A = 1 − ℜ ⁡ A
37 30 36 breqtrrd ⊢ A ∈ ℂ ∧ A = 1 → 0 ≤ ℜ ⁡ 1 − A
38 37 3adant3 ⊢ A ∈ ℂ ∧ A = 1 ∧ ¬ 1 = A → 0 ≤ ℜ ⁡ 1 − A
39 neghalfpirx ⊢ − π 2 ∈ ℝ *
40 halfpire ⊢ π 2 ∈ ℝ
41 40 rexri ⊢ π 2 ∈ ℝ *
42 argrege0 ⊢ 1 − A ∈ ℂ ∧ 1 − A ≠ 0 ∧ 0 ≤ ℜ ⁡ 1 − A → ℑ ⁡ log ⁡ 1 − A ∈ − π 2 π 2
43 iccleub ⊢ − π 2 ∈ ℝ * ∧ π 2 ∈ ℝ * ∧ ℑ ⁡ log ⁡ 1 − A ∈ − π 2 π 2 → ℑ ⁡ log ⁡ 1 − A ≤ π 2
44 39 41 42 43 mp3an12i ⊢ 1 − A ∈ ℂ ∧ 1 − A ≠ 0 ∧ 0 ≤ ℜ ⁡ 1 − A → ℑ ⁡ log ⁡ 1 − A ≤ π 2
45 13 14 38 44 syl3anc ⊢ A ∈ ℂ ∧ A = 1 ∧ ¬ 1 = A → ℑ ⁡ log ⁡ 1 − A ≤ π 2
46 pirp ⊢ π ∈ ℝ +
47 rphalflt ⊢ π ∈ ℝ + → π 2 < π
48 46 47 ax-mp ⊢ π 2 < π
49 45 48 jctir ⊢ A ∈ ℂ ∧ A = 1 ∧ ¬ 1 = A → ℑ ⁡ log ⁡ 1 − A ≤ π 2 ∧ π 2 < π
50 pire ⊢ π ∈ ℝ
51 50 a1i ⊢ A ∈ ℂ ∧ ¬ 1 = A → π ∈ ℝ
52 51 rehalfcld ⊢ A ∈ ℂ ∧ ¬ 1 = A → π 2 ∈ ℝ
53 lelttr ⊢ ℑ ⁡ log ⁡ 1 − A ∈ ℝ ∧ π 2 ∈ ℝ ∧ π ∈ ℝ → ℑ ⁡ log ⁡ 1 − A ≤ π 2 ∧ π 2 < π → ℑ ⁡ log ⁡ 1 − A < π
54 11 52 51 53 syl3anc ⊢ A ∈ ℂ ∧ ¬ 1 = A → ℑ ⁡ log ⁡ 1 − A ≤ π 2 ∧ π 2 < π → ℑ ⁡ log ⁡ 1 − A < π
55 54 3adant2 ⊢ A ∈ ℂ ∧ A = 1 ∧ ¬ 1 = A → ℑ ⁡ log ⁡ 1 − A ≤ π 2 ∧ π 2 < π → ℑ ⁡ log ⁡ 1 − A < π
56 49 55 mpd ⊢ A ∈ ℂ ∧ A = 1 ∧ ¬ 1 = A → ℑ ⁡ log ⁡ 1 − A < π
57 12 56 ltned ⊢ A ∈ ℂ ∧ A = 1 ∧ ¬ 1 = A → ℑ ⁡ log ⁡ 1 − A ≠ π