Metamath Proof Explorer

Theorem fourierdlem24

Description: A sufficient condition for module being nonzero. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion fourierdlem24 
|- ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> ( A mod ( 2 x. _pi ) ) =/= 0 )

Proof

Step Hyp Ref Expression
1 0zd 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ 0 < A ) -> 0 e. ZZ )
2 pire 
 |-  _pi e. RR
3 2 renegcli 
 |-  -u _pi e. RR
4 iccssre 
 |-  ( ( -u _pi e. RR /\ _pi e. RR ) -> ( -u _pi [,] _pi ) C_ RR )
5 3 2 4 mp2an 
 |-  ( -u _pi [,] _pi ) C_ RR
6 eldifi 
 |-  ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> A e. ( -u _pi [,] _pi ) )
7 5 6 sseldi 
 |-  ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> A e. RR )
8 7 adantr 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ 0 < A ) -> A e. RR )
9 2re 
 |-  2 e. RR
10 9 2 remulcli 
 |-  ( 2 x. _pi ) e. RR
11 10 a1i 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ 0 < A ) -> ( 2 x. _pi ) e. RR )
12 simpr 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ 0 < A ) -> 0 < A )
13 2pos 
 |-  0 < 2
14 pipos 
 |-  0 < _pi
15 9 2 13 14 mulgt0ii 
 |-  0 < ( 2 x. _pi )
16 15 a1i 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ 0 < A ) -> 0 < ( 2 x. _pi ) )
17 8 11 12 16 divgt0d 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ 0 < A ) -> 0 < ( A / ( 2 x. _pi ) ) )
18 11 16 elrpd 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ 0 < A ) -> ( 2 x. _pi ) e. RR+ )
19 2 a1i 
 |-  ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> _pi e. RR )
20 10 a1i 
 |-  ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> ( 2 x. _pi ) e. RR )
21 3 rexri 
 |-  -u _pi e. RR*
22 21 a1i 
 |-  ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> -u _pi e. RR* )
23 19 rexrd 
 |-  ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> _pi e. RR* )
24 iccleub 
 |-  ( ( -u _pi e. RR* /\ _pi e. RR* /\ A e. ( -u _pi [,] _pi ) ) -> A <_ _pi )
25 22 23 6 24 syl3anc 
 |-  ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> A <_ _pi )
26 pirp 
 |-  _pi e. RR+
27 2timesgt 
 |-  ( _pi e. RR+ -> _pi < ( 2 x. _pi ) )
28 26 27 mp1i 
 |-  ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> _pi < ( 2 x. _pi ) )
29 7 19 20 25 28 lelttrd 
 |-  ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> A < ( 2 x. _pi ) )
30 29 adantr 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ 0 < A ) -> A < ( 2 x. _pi ) )
31 8 11 18 30 ltdiv1dd 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ 0 < A ) -> ( A / ( 2 x. _pi ) ) < ( ( 2 x. _pi ) / ( 2 x. _pi ) ) )
32 10 recni 
 |-  ( 2 x. _pi ) e. CC
33 10 15 gt0ne0ii 
 |-  ( 2 x. _pi ) =/= 0
34 32 33 dividi 
 |-  ( ( 2 x. _pi ) / ( 2 x. _pi ) ) = 1
35 31 34 breqtrdi 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ 0 < A ) -> ( A / ( 2 x. _pi ) ) < 1 )
36 0p1e1 
 |-  ( 0 + 1 ) = 1
37 35 36 breqtrrdi 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ 0 < A ) -> ( A / ( 2 x. _pi ) ) < ( 0 + 1 ) )
38 btwnnz 
 |-  ( ( 0 e. ZZ /\ 0 < ( A / ( 2 x. _pi ) ) /\ ( A / ( 2 x. _pi ) ) < ( 0 + 1 ) ) -> -. ( A / ( 2 x. _pi ) ) e. ZZ )
39 1 17 37 38 syl3anc 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ 0 < A ) -> -. ( A / ( 2 x. _pi ) ) e. ZZ )
40 simpl 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ -. 0 < A ) -> A e. ( ( -u _pi [,] _pi ) \ { 0 } ) )
41 7 adantr 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ -. 0 < A ) -> A e. RR )
42 0red 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ -. 0 < A ) -> 0 e. RR )
43 simpr 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ -. 0 < A ) -> -. 0 < A )
44 41 42 43 nltled 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ -. 0 < A ) -> A <_ 0 )
45 eldifsni 
 |-  ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> A =/= 0 )
46 45 necomd 
 |-  ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> 0 =/= A )
47 46 adantr 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ -. 0 < A ) -> 0 =/= A )
48 41 42 44 47 leneltd 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ -. 0 < A ) -> A < 0 )
49 neg1z 
 |-  -u 1 e. ZZ
50 49 a1i 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ A < 0 ) -> -u 1 e. ZZ )
51 33 a1i 
 |-  ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> ( 2 x. _pi ) =/= 0 )
52 7 20 51 redivcld 
 |-  ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> ( A / ( 2 x. _pi ) ) e. RR )
53 52 adantr 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ A < 0 ) -> ( A / ( 2 x. _pi ) ) e. RR )
54 1red 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ A < 0 ) -> 1 e. RR )
55 7 recnd 
 |-  ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> A e. CC )
56 55 adantr 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ A < 0 ) -> A e. CC )
57 32 a1i 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ A < 0 ) -> ( 2 x. _pi ) e. CC )
58 33 a1i 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ A < 0 ) -> ( 2 x. _pi ) =/= 0 )
59 56 57 58 divnegd 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ A < 0 ) -> -u ( A / ( 2 x. _pi ) ) = ( -u A / ( 2 x. _pi ) ) )
60 7 renegcld 
 |-  ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> -u A e. RR )
61 60 adantr 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ A < 0 ) -> -u A e. RR )
62 10 a1i 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ A < 0 ) -> ( 2 x. _pi ) e. RR )
63 2rp 
 |-  2 e. RR+
64 rpmulcl 
 |-  ( ( 2 e. RR+ /\ _pi e. RR+ ) -> ( 2 x. _pi ) e. RR+ )
65 63 26 64 mp2an 
 |-  ( 2 x. _pi ) e. RR+
66 65 a1i 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ A < 0 ) -> ( 2 x. _pi ) e. RR+ )
67 iccgelb 
 |-  ( ( -u _pi e. RR* /\ _pi e. RR* /\ A e. ( -u _pi [,] _pi ) ) -> -u _pi <_ A )
68 22 23 6 67 syl3anc 
 |-  ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> -u _pi <_ A )
69 19 7 68 lenegcon1d 
 |-  ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> -u A <_ _pi )
70 60 19 20 69 28 lelttrd 
 |-  ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> -u A < ( 2 x. _pi ) )
71 70 adantr 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ A < 0 ) -> -u A < ( 2 x. _pi ) )
72 61 62 66 71 ltdiv1dd 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ A < 0 ) -> ( -u A / ( 2 x. _pi ) ) < ( ( 2 x. _pi ) / ( 2 x. _pi ) ) )
73 72 34 breqtrdi 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ A < 0 ) -> ( -u A / ( 2 x. _pi ) ) < 1 )
74 59 73 eqbrtrd 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ A < 0 ) -> -u ( A / ( 2 x. _pi ) ) < 1 )
75 53 54 74 ltnegcon1d 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ A < 0 ) -> -u 1 < ( A / ( 2 x. _pi ) ) )
76 7 adantr 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ A < 0 ) -> A e. RR )
77 simpr 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ A < 0 ) -> A < 0 )
78 76 66 77 divlt0gt0d 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ A < 0 ) -> ( A / ( 2 x. _pi ) ) < 0 )
79 neg1cn 
 |-  -u 1 e. CC
80 ax-1cn 
 |-  1 e. CC
81 79 80 addcomi 
 |-  ( -u 1 + 1 ) = ( 1 + -u 1 )
82 1pneg1e0 
 |-  ( 1 + -u 1 ) = 0
83 81 82 eqtr2i 
 |-  0 = ( -u 1 + 1 )
84 78 83 breqtrdi 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ A < 0 ) -> ( A / ( 2 x. _pi ) ) < ( -u 1 + 1 ) )
85 btwnnz 
 |-  ( ( -u 1 e. ZZ /\ -u 1 < ( A / ( 2 x. _pi ) ) /\ ( A / ( 2 x. _pi ) ) < ( -u 1 + 1 ) ) -> -. ( A / ( 2 x. _pi ) ) e. ZZ )
86 50 75 84 85 syl3anc 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ A < 0 ) -> -. ( A / ( 2 x. _pi ) ) e. ZZ )
87 40 48 86 syl2anc 
 |-  ( ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) /\ -. 0 < A ) -> -. ( A / ( 2 x. _pi ) ) e. ZZ )
88 39 87 pm2.61dan 
 |-  ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> -. ( A / ( 2 x. _pi ) ) e. ZZ )
89 65 a1i 
 |-  ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> ( 2 x. _pi ) e. RR+ )
90 mod0 
 |-  ( ( A e. RR /\ ( 2 x. _pi ) e. RR+ ) -> ( ( A mod ( 2 x. _pi ) ) = 0 <-> ( A / ( 2 x. _pi ) ) e. ZZ ) )
91 7 89 90 syl2anc 
 |-  ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> ( ( A mod ( 2 x. _pi ) ) = 0 <-> ( A / ( 2 x. _pi ) ) e. ZZ ) )
92 88 91 mtbird 
 |-  ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> -. ( A mod ( 2 x. _pi ) ) = 0 )
93 92 neqned 
 |-  ( A e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> ( A mod ( 2 x. _pi ) ) =/= 0 )