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 
|- ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( cos ` A ) =/= 0 )

Proof

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