| 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
|
sseldi |
⊢ ( 𝐴 ∈ ( ( - π [,] π ) ∖ { 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 ) |