Proof of Theorem fourierdlem24
Step | Hyp | Ref
| Expression |
1 | | 0zd 12567 |
. . . . 5
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
0 ∈ ℤ) |
2 | | pire 26310 |
. . . . . . . . . 10
⊢ π
∈ ℝ |
3 | 2 | renegcli 11518 |
. . . . . . . . 9
⊢ -π
∈ ℝ |
4 | | iccssre 13403 |
. . . . . . . . 9
⊢ ((-π
∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆
ℝ) |
5 | 3, 2, 4 | mp2an 689 |
. . . . . . . 8
⊢
(-π[,]π) ⊆ ℝ |
6 | | eldifi 4118 |
. . . . . . . 8
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → 𝐴 ∈
(-π[,]π)) |
7 | 5, 6 | sselid 3972 |
. . . . . . 7
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → 𝐴 ∈
ℝ) |
8 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
𝐴 ∈
ℝ) |
9 | | 2re 12283 |
. . . . . . . 8
⊢ 2 ∈
ℝ |
10 | 9, 2 | remulcli 11227 |
. . . . . . 7
⊢ (2
· π) ∈ ℝ |
11 | 10 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
(2 · π) ∈ ℝ) |
12 | | simpr 484 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
0 < 𝐴) |
13 | | 2pos 12312 |
. . . . . . . 8
⊢ 0 <
2 |
14 | | pipos 26312 |
. . . . . . . 8
⊢ 0 <
π |
15 | 9, 2, 13, 14 | mulgt0ii 11344 |
. . . . . . 7
⊢ 0 < (2
· π) |
16 | 15 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
0 < (2 · π)) |
17 | 8, 11, 12, 16 | divgt0d 12146 |
. . . . 5
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
0 < (𝐴 / (2 ·
π))) |
18 | 11, 16 | elrpd 13010 |
. . . . . . . 8
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
(2 · π) ∈ ℝ+) |
19 | 2 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → π ∈ ℝ) |
20 | 10 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → (2 · π) ∈ ℝ) |
21 | 3 | rexri 11269 |
. . . . . . . . . . . 12
⊢ -π
∈ ℝ* |
22 | 21 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → -π ∈ ℝ*) |
23 | 19 | rexrd 11261 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → π ∈ ℝ*) |
24 | | iccleub 13376 |
. . . . . . . . . . 11
⊢ ((-π
∈ ℝ* ∧ π ∈ ℝ* ∧ 𝐴 ∈ (-π[,]π)) →
𝐴 ≤
π) |
25 | 22, 23, 6, 24 | syl3anc 1368 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → 𝐴 ≤
π) |
26 | | pirp 26313 |
. . . . . . . . . . 11
⊢ π
∈ ℝ+ |
27 | | 2timesgt 44483 |
. . . . . . . . . . 11
⊢ (π
∈ ℝ+ → π < (2 · π)) |
28 | 26, 27 | mp1i 13 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → π < (2 · π)) |
29 | 7, 19, 20, 25, 28 | lelttrd 11369 |
. . . . . . . . 9
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → 𝐴 < (2
· π)) |
30 | 29 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
𝐴 < (2 ·
π)) |
31 | 8, 11, 18, 30 | ltdiv1dd 13070 |
. . . . . . 7
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
(𝐴 / (2 · π))
< ((2 · π) / (2 · π))) |
32 | 10 | recni 11225 |
. . . . . . . 8
⊢ (2
· π) ∈ ℂ |
33 | 10, 15 | gt0ne0ii 11747 |
. . . . . . . 8
⊢ (2
· π) ≠ 0 |
34 | 32, 33 | dividi 11944 |
. . . . . . 7
⊢ ((2
· π) / (2 · π)) = 1 |
35 | 31, 34 | breqtrdi 5179 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
(𝐴 / (2 · π))
< 1) |
36 | | 0p1e1 12331 |
. . . . . 6
⊢ (0 + 1) =
1 |
37 | 35, 36 | breqtrrdi 5180 |
. . . . 5
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
(𝐴 / (2 · π))
< (0 + 1)) |
38 | | btwnnz 12635 |
. . . . 5
⊢ ((0
∈ ℤ ∧ 0 < (𝐴 / (2 · π)) ∧ (𝐴 / (2 · π)) < (0 +
1)) → ¬ (𝐴 / (2
· π)) ∈ ℤ) |
39 | 1, 17, 37, 38 | syl3anc 1368 |
. . . 4
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
¬ (𝐴 / (2 ·
π)) ∈ ℤ) |
40 | | simpl 482 |
. . . . 5
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ ¬ 0 < 𝐴)
→ 𝐴 ∈
((-π[,]π) ∖ {0})) |
41 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ ¬ 0 < 𝐴)
→ 𝐴 ∈
ℝ) |
42 | | 0red 11214 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ ¬ 0 < 𝐴)
→ 0 ∈ ℝ) |
43 | | simpr 484 |
. . . . . . 7
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ ¬ 0 < 𝐴)
→ ¬ 0 < 𝐴) |
44 | 41, 42, 43 | nltled 11361 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ ¬ 0 < 𝐴)
→ 𝐴 ≤
0) |
45 | | eldifsni 4785 |
. . . . . . . 8
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → 𝐴 ≠
0) |
46 | 45 | necomd 2988 |
. . . . . . 7
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → 0 ≠ 𝐴) |
47 | 46 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ ¬ 0 < 𝐴)
→ 0 ≠ 𝐴) |
48 | 41, 42, 44, 47 | leneltd 11365 |
. . . . 5
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ ¬ 0 < 𝐴)
→ 𝐴 <
0) |
49 | | neg1z 12595 |
. . . . . . 7
⊢ -1 ∈
ℤ |
50 | 49 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
-1 ∈ ℤ) |
51 | 33 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → (2 · π) ≠ 0) |
52 | 7, 20, 51 | redivcld 12039 |
. . . . . . . 8
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → (𝐴 / (2
· π)) ∈ ℝ) |
53 | 52 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
(𝐴 / (2 · π))
∈ ℝ) |
54 | | 1red 11212 |
. . . . . . 7
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
1 ∈ ℝ) |
55 | 7 | recnd 11239 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → 𝐴 ∈
ℂ) |
56 | 55 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
𝐴 ∈
ℂ) |
57 | 32 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
(2 · π) ∈ ℂ) |
58 | 33 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
(2 · π) ≠ 0) |
59 | 56, 57, 58 | divnegd 12000 |
. . . . . . . 8
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
-(𝐴 / (2 · π)) =
(-𝐴 / (2 ·
π))) |
60 | 7 | renegcld 11638 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → -𝐴 ∈
ℝ) |
61 | 60 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
-𝐴 ∈
ℝ) |
62 | 10 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
(2 · π) ∈ ℝ) |
63 | | 2rp 12976 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ+ |
64 | | rpmulcl 12994 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℝ+ ∧ π ∈ ℝ+) → (2
· π) ∈ ℝ+) |
65 | 63, 26, 64 | mp2an 689 |
. . . . . . . . . . 11
⊢ (2
· π) ∈ ℝ+ |
66 | 65 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
(2 · π) ∈ ℝ+) |
67 | | iccgelb 13377 |
. . . . . . . . . . . . . 14
⊢ ((-π
∈ ℝ* ∧ π ∈ ℝ* ∧ 𝐴 ∈ (-π[,]π)) →
-π ≤ 𝐴) |
68 | 22, 23, 6, 67 | syl3anc 1368 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → -π ≤ 𝐴) |
69 | 19, 7, 68 | lenegcon1d 11793 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → -𝐴 ≤
π) |
70 | 60, 19, 20, 69, 28 | lelttrd 11369 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → -𝐴 < (2
· π)) |
71 | 70 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
-𝐴 < (2 ·
π)) |
72 | 61, 62, 66, 71 | ltdiv1dd 13070 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
(-𝐴 / (2 · π))
< ((2 · π) / (2 · π))) |
73 | 72, 34 | breqtrdi 5179 |
. . . . . . . 8
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
(-𝐴 / (2 · π))
< 1) |
74 | 59, 73 | eqbrtrd 5160 |
. . . . . . 7
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
-(𝐴 / (2 · π))
< 1) |
75 | 53, 54, 74 | ltnegcon1d 11791 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
-1 < (𝐴 / (2 ·
π))) |
76 | 7 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
𝐴 ∈
ℝ) |
77 | | simpr 484 |
. . . . . . . 8
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
𝐴 < 0) |
78 | 76, 66, 77 | divlt0gt0d 44481 |
. . . . . . 7
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
(𝐴 / (2 · π))
< 0) |
79 | | neg1cn 12323 |
. . . . . . . . 9
⊢ -1 ∈
ℂ |
80 | | ax-1cn 11164 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
81 | 79, 80 | addcomi 11402 |
. . . . . . . 8
⊢ (-1 + 1)
= (1 + -1) |
82 | | 1pneg1e0 12328 |
. . . . . . . 8
⊢ (1 + -1)
= 0 |
83 | 81, 82 | eqtr2i 2753 |
. . . . . . 7
⊢ 0 = (-1 +
1) |
84 | 78, 83 | breqtrdi 5179 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
(𝐴 / (2 · π))
< (-1 + 1)) |
85 | | btwnnz 12635 |
. . . . . 6
⊢ ((-1
∈ ℤ ∧ -1 < (𝐴 / (2 · π)) ∧ (𝐴 / (2 · π)) < (-1 +
1)) → ¬ (𝐴 / (2
· π)) ∈ ℤ) |
86 | 50, 75, 84, 85 | syl3anc 1368 |
. . . . 5
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
¬ (𝐴 / (2 ·
π)) ∈ ℤ) |
87 | 40, 48, 86 | syl2anc 583 |
. . . 4
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ ¬ 0 < 𝐴)
→ ¬ (𝐴 / (2
· π)) ∈ ℤ) |
88 | 39, 87 | pm2.61dan 810 |
. . 3
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → ¬ (𝐴 / (2
· π)) ∈ ℤ) |
89 | 65 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → (2 · π) ∈ ℝ+) |
90 | | mod0 13838 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ (2
· π) ∈ ℝ+) → ((𝐴 mod (2 · π)) = 0 ↔ (𝐴 / (2 · π)) ∈
ℤ)) |
91 | 7, 89, 90 | syl2anc 583 |
. . 3
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → ((𝐴 mod (2
· π)) = 0 ↔ (𝐴 / (2 · π)) ∈
ℤ)) |
92 | 88, 91 | mtbird 325 |
. 2
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → ¬ (𝐴 mod (2
· π)) = 0) |
93 | 92 | neqned 2939 |
1
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → (𝐴 mod (2
· π)) ≠ 0) |