Metamath Proof Explorer

Theorem isosctrlem1

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

Ref Expression
Assertion isosctrlem1 ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( ℑ ‘ ( log ‘ ( 1 − 𝐴 ) ) ) ≠ π )

Proof

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