This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fourierdlem24

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

Ref Expression
Assertion fourierdlem24 ( 𝐴 ∈ ( ( - π [,] π ) ∖ { 0 } ) → ( 𝐴 mod ( 2 · π ) ) ≠ 0 )

Proof

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