Metamath Proof Explorer

Theorem cosne0

Description: The cosine function has no zeroes within the vertical strip of the complex plane between real part -upi / 2 and pi / 2 . (Contributed by Mario Carneiro, 2-Apr-2015)

Ref Expression
Assertion cosne0 ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( cos ‘ 𝐴 ) ≠ 0 )

Proof

Step Hyp Ref Expression
1 halfpire ⊢ ( π / 2 ) ∈ ℝ
2 1 recni ⊢ ( π / 2 ) ∈ ℂ
3 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 𝐴 ∈ ℂ )
4 nncan ⊢ ( ( ( π / 2 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( π / 2 ) − ( ( π / 2 ) − 𝐴 ) ) = 𝐴 )
5 2 3 4 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( π / 2 ) − ( ( π / 2 ) − 𝐴 ) ) = 𝐴 )
6 5 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( cos ‘ ( ( π / 2 ) − ( ( π / 2 ) − 𝐴 ) ) ) = ( cos ‘ 𝐴 ) )
7 subcl ⊢ ( ( ( π / 2 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( π / 2 ) − 𝐴 ) ∈ ℂ )
8 2 3 7 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( π / 2 ) − 𝐴 ) ∈ ℂ )
9 coshalfpim ⊢ ( ( ( π / 2 ) − 𝐴 ) ∈ ℂ → ( cos ‘ ( ( π / 2 ) − ( ( π / 2 ) − 𝐴 ) ) ) = ( sin ‘ ( ( π / 2 ) − 𝐴 ) ) )
10 8 9 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( cos ‘ ( ( π / 2 ) − ( ( π / 2 ) − 𝐴 ) ) ) = ( sin ‘ ( ( π / 2 ) − 𝐴 ) ) )
11 6 10 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( cos ‘ 𝐴 ) = ( sin ‘ ( ( π / 2 ) − 𝐴 ) ) )
12 5 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ( ( π / 2 ) − 𝐴 ) / π ) ∈ ℤ ) → ( ( π / 2 ) − ( ( π / 2 ) − 𝐴 ) ) = 𝐴 )
13 picn ⊢ π ∈ ℂ
14 13 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → π ∈ ℂ )
15 pire ⊢ π ∈ ℝ
16 pipos ⊢ 0 < π
17 15 16 gt0ne0ii ⊢ π ≠ 0
18 17 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → π ≠ 0 )
19 8 14 18 divcan1d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ( ( π / 2 ) − 𝐴 ) / π ) · π ) = ( ( π / 2 ) − 𝐴 ) )
20 19 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ( ( π / 2 ) − 𝐴 ) / π ) ∈ ℤ ) → ( ( ( ( π / 2 ) − 𝐴 ) / π ) · π ) = ( ( π / 2 ) − 𝐴 ) )
21 zre ⊢ ( ( ( ( π / 2 ) − 𝐴 ) / π ) ∈ ℤ → ( ( ( π / 2 ) − 𝐴 ) / π ) ∈ ℝ )
22 21 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ( ( π / 2 ) − 𝐴 ) / π ) ∈ ℤ ) → ( ( ( π / 2 ) − 𝐴 ) / π ) ∈ ℝ )
23 remulcl ⊢ ( ( ( ( ( π / 2 ) − 𝐴 ) / π ) ∈ ℝ ∧ π ∈ ℝ ) → ( ( ( ( π / 2 ) − 𝐴 ) / π ) · π ) ∈ ℝ )
24 22 15 23 sylancl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ( ( π / 2 ) − 𝐴 ) / π ) ∈ ℤ ) → ( ( ( ( π / 2 ) − 𝐴 ) / π ) · π ) ∈ ℝ )
25 20 24 eqeltrrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ( ( π / 2 ) − 𝐴 ) / π ) ∈ ℤ ) → ( ( π / 2 ) − 𝐴 ) ∈ ℝ )
26 resubcl ⊢ ( ( ( π / 2 ) ∈ ℝ ∧ ( ( π / 2 ) − 𝐴 ) ∈ ℝ ) → ( ( π / 2 ) − ( ( π / 2 ) − 𝐴 ) ) ∈ ℝ )
27 1 25 26 sylancr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ( ( π / 2 ) − 𝐴 ) / π ) ∈ ℤ ) → ( ( π / 2 ) − ( ( π / 2 ) − 𝐴 ) ) ∈ ℝ )
28 12 27 eqeltrrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ( ( π / 2 ) − 𝐴 ) / π ) ∈ ℤ ) → 𝐴 ∈ ℝ )
29 28 rered ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ( ( π / 2 ) − 𝐴 ) / π ) ∈ ℤ ) → ( ℜ ‘ 𝐴 ) = 𝐴 )
30 simplr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ( ( π / 2 ) − 𝐴 ) / π ) ∈ ℤ ) → ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) )
31 29 30 eqeltrrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ( ( π / 2 ) − 𝐴 ) / π ) ∈ ℤ ) → 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) )
32 0zd ⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 0 ∈ ℤ )
33 elioore ⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 𝐴 ∈ ℝ )
34 resubcl ⊢ ( ( ( π / 2 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( π / 2 ) − 𝐴 ) ∈ ℝ )
35 1 33 34 sylancr ⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( ( π / 2 ) − 𝐴 ) ∈ ℝ )
36 15 a1i ⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → π ∈ ℝ )
37 eliooord ⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( - ( π / 2 ) < 𝐴 ∧ 𝐴 < ( π / 2 ) ) )
38 37 simprd ⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 𝐴 < ( π / 2 ) )
39 posdif ⊢ ( ( 𝐴 ∈ ℝ ∧ ( π / 2 ) ∈ ℝ ) → ( 𝐴 < ( π / 2 ) ↔ 0 < ( ( π / 2 ) − 𝐴 ) ) )
40 33 1 39 sylancl ⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( 𝐴 < ( π / 2 ) ↔ 0 < ( ( π / 2 ) − 𝐴 ) ) )
41 38 40 mpbid ⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 0 < ( ( π / 2 ) − 𝐴 ) )
42 16 a1i ⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 0 < π )
43 35 36 41 42 divgt0d ⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 0 < ( ( ( π / 2 ) − 𝐴 ) / π ) )
44 1 a1i ⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( π / 2 ) ∈ ℝ )
45 2 negcli ⊢ - ( π / 2 ) ∈ ℂ
46 13 2 negsubi ⊢ ( π + - ( π / 2 ) ) = ( π − ( π / 2 ) )
47 pidiv2halves ⊢ ( ( π / 2 ) + ( π / 2 ) ) = π
48 13 2 2 47 subaddrii ⊢ ( π − ( π / 2 ) ) = ( π / 2 )
49 46 48 eqtri ⊢ ( π + - ( π / 2 ) ) = ( π / 2 )
50 2 13 45 49 subaddrii ⊢ ( ( π / 2 ) − π ) = - ( π / 2 )
51 37 simpld ⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → - ( π / 2 ) < 𝐴 )
52 50 51 eqbrtrid ⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( ( π / 2 ) − π ) < 𝐴 )
53 44 36 33 52 ltsub23d ⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( ( π / 2 ) − 𝐴 ) < π )
54 13 mulid1i ⊢ ( π · 1 ) = π
55 53 54 breqtrrdi ⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( ( π / 2 ) − 𝐴 ) < ( π · 1 ) )
56 1red ⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 1 ∈ ℝ )
57 ltdivmul ⊢ ( ( ( ( π / 2 ) − 𝐴 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( π ∈ ℝ ∧ 0 < π ) ) → ( ( ( ( π / 2 ) − 𝐴 ) / π ) < 1 ↔ ( ( π / 2 ) − 𝐴 ) < ( π · 1 ) ) )
58 35 56 36 42 57 syl112anc ⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( ( ( ( π / 2 ) − 𝐴 ) / π ) < 1 ↔ ( ( π / 2 ) − 𝐴 ) < ( π · 1 ) ) )
59 55 58 mpbird ⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( ( ( π / 2 ) − 𝐴 ) / π ) < 1 )
60 1e0p1 ⊢ 1 = ( 0 + 1 )
61 59 60 breqtrdi ⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ( ( ( π / 2 ) − 𝐴 ) / π ) < ( 0 + 1 ) )
62 btwnnz ⊢ ( ( 0 ∈ ℤ ∧ 0 < ( ( ( π / 2 ) − 𝐴 ) / π ) ∧ ( ( ( π / 2 ) − 𝐴 ) / π ) < ( 0 + 1 ) ) → ¬ ( ( ( π / 2 ) − 𝐴 ) / π ) ∈ ℤ )
63 32 43 61 62 syl3anc ⊢ ( 𝐴 ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → ¬ ( ( ( π / 2 ) − 𝐴 ) / π ) ∈ ℤ )
64 31 63 syl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) ∧ ( ( ( π / 2 ) − 𝐴 ) / π ) ∈ ℤ ) → ¬ ( ( ( π / 2 ) − 𝐴 ) / π ) ∈ ℤ )
65 64 pm2.01da ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ¬ ( ( ( π / 2 ) − 𝐴 ) / π ) ∈ ℤ )
66 sineq0 ⊢ ( ( ( π / 2 ) − 𝐴 ) ∈ ℂ → ( ( sin ‘ ( ( π / 2 ) − 𝐴 ) ) = 0 ↔ ( ( ( π / 2 ) − 𝐴 ) / π ) ∈ ℤ ) )
67 8 66 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( sin ‘ ( ( π / 2 ) − 𝐴 ) ) = 0 ↔ ( ( ( π / 2 ) − 𝐴 ) / π ) ∈ ℤ ) )
68 67 necon3abid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( sin ‘ ( ( π / 2 ) − 𝐴 ) ) ≠ 0 ↔ ¬ ( ( ( π / 2 ) − 𝐴 ) / π ) ∈ ℤ ) )
69 65 68 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( sin ‘ ( ( π / 2 ) − 𝐴 ) ) ≠ 0 )
70 11 69 eqnetrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( cos ‘ 𝐴 ) ≠ 0 )