Proof of Theorem fourierdlem24
| Step | Hyp | Ref
| Expression |
| 1 | | 0zd 12625 |
. . . . 5
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
0 ∈ ℤ) |
| 2 | | pire 26500 |
. . . . . . . . . 10
⊢ π
∈ ℝ |
| 3 | 2 | renegcli 11570 |
. . . . . . . . 9
⊢ -π
∈ ℝ |
| 4 | | iccssre 13469 |
. . . . . . . . 9
⊢ ((-π
∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆
ℝ) |
| 5 | 3, 2, 4 | mp2an 692 |
. . . . . . . 8
⊢
(-π[,]π) ⊆ ℝ |
| 6 | | eldifi 4131 |
. . . . . . . 8
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → 𝐴 ∈
(-π[,]π)) |
| 7 | 5, 6 | sselid 3981 |
. . . . . . 7
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → 𝐴 ∈
ℝ) |
| 8 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
𝐴 ∈
ℝ) |
| 9 | | 2re 12340 |
. . . . . . . 8
⊢ 2 ∈
ℝ |
| 10 | 9, 2 | remulcli 11277 |
. . . . . . 7
⊢ (2
· π) ∈ ℝ |
| 11 | 10 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
(2 · π) ∈ ℝ) |
| 12 | | simpr 484 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
0 < 𝐴) |
| 13 | | 2pos 12369 |
. . . . . . . 8
⊢ 0 <
2 |
| 14 | | pipos 26502 |
. . . . . . . 8
⊢ 0 <
π |
| 15 | 9, 2, 13, 14 | mulgt0ii 11394 |
. . . . . . 7
⊢ 0 < (2
· π) |
| 16 | 15 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
0 < (2 · π)) |
| 17 | 8, 11, 12, 16 | divgt0d 12203 |
. . . . 5
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
0 < (𝐴 / (2 ·
π))) |
| 18 | 11, 16 | elrpd 13074 |
. . . . . . . 8
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
(2 · π) ∈ ℝ+) |
| 19 | 2 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → π ∈ ℝ) |
| 20 | 10 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → (2 · π) ∈ ℝ) |
| 21 | 3 | rexri 11319 |
. . . . . . . . . . . 12
⊢ -π
∈ ℝ* |
| 22 | 21 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → -π ∈ ℝ*) |
| 23 | 19 | rexrd 11311 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → π ∈ ℝ*) |
| 24 | | iccleub 13442 |
. . . . . . . . . . 11
⊢ ((-π
∈ ℝ* ∧ π ∈ ℝ* ∧ 𝐴 ∈ (-π[,]π)) →
𝐴 ≤
π) |
| 25 | 22, 23, 6, 24 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → 𝐴 ≤
π) |
| 26 | | pirp 26503 |
. . . . . . . . . . 11
⊢ π
∈ ℝ+ |
| 27 | | 2timesgt 45300 |
. . . . . . . . . . 11
⊢ (π
∈ ℝ+ → π < (2 · π)) |
| 28 | 26, 27 | mp1i 13 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → π < (2 · π)) |
| 29 | 7, 19, 20, 25, 28 | lelttrd 11419 |
. . . . . . . . 9
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → 𝐴 < (2
· π)) |
| 30 | 29 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
𝐴 < (2 ·
π)) |
| 31 | 8, 11, 18, 30 | ltdiv1dd 13134 |
. . . . . . 7
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
(𝐴 / (2 · π))
< ((2 · π) / (2 · π))) |
| 32 | 10 | recni 11275 |
. . . . . . . 8
⊢ (2
· π) ∈ ℂ |
| 33 | 10, 15 | gt0ne0ii 11799 |
. . . . . . . 8
⊢ (2
· π) ≠ 0 |
| 34 | 32, 33 | dividi 12000 |
. . . . . . 7
⊢ ((2
· π) / (2 · π)) = 1 |
| 35 | 31, 34 | breqtrdi 5184 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
(𝐴 / (2 · π))
< 1) |
| 36 | | 0p1e1 12388 |
. . . . . 6
⊢ (0 + 1) =
1 |
| 37 | 35, 36 | breqtrrdi 5185 |
. . . . 5
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
(𝐴 / (2 · π))
< (0 + 1)) |
| 38 | | btwnnz 12694 |
. . . . 5
⊢ ((0
∈ ℤ ∧ 0 < (𝐴 / (2 · π)) ∧ (𝐴 / (2 · π)) < (0 +
1)) → ¬ (𝐴 / (2
· π)) ∈ ℤ) |
| 39 | 1, 17, 37, 38 | syl3anc 1373 |
. . . 4
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
¬ (𝐴 / (2 ·
π)) ∈ ℤ) |
| 40 | | simpl 482 |
. . . . 5
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ ¬ 0 < 𝐴)
→ 𝐴 ∈
((-π[,]π) ∖ {0})) |
| 41 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ ¬ 0 < 𝐴)
→ 𝐴 ∈
ℝ) |
| 42 | | 0red 11264 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ ¬ 0 < 𝐴)
→ 0 ∈ ℝ) |
| 43 | | simpr 484 |
. . . . . . 7
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ ¬ 0 < 𝐴)
→ ¬ 0 < 𝐴) |
| 44 | 41, 42, 43 | nltled 11411 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ ¬ 0 < 𝐴)
→ 𝐴 ≤
0) |
| 45 | | eldifsni 4790 |
. . . . . . . 8
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → 𝐴 ≠
0) |
| 46 | 45 | necomd 2996 |
. . . . . . 7
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → 0 ≠ 𝐴) |
| 47 | 46 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ ¬ 0 < 𝐴)
→ 0 ≠ 𝐴) |
| 48 | 41, 42, 44, 47 | leneltd 11415 |
. . . . 5
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ ¬ 0 < 𝐴)
→ 𝐴 <
0) |
| 49 | | neg1z 12653 |
. . . . . . 7
⊢ -1 ∈
ℤ |
| 50 | 49 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
-1 ∈ ℤ) |
| 51 | 33 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → (2 · π) ≠ 0) |
| 52 | 7, 20, 51 | redivcld 12095 |
. . . . . . . 8
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → (𝐴 / (2
· π)) ∈ ℝ) |
| 53 | 52 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
(𝐴 / (2 · π))
∈ ℝ) |
| 54 | | 1red 11262 |
. . . . . . 7
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
1 ∈ ℝ) |
| 55 | 7 | recnd 11289 |
. . . . . . . . . 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 12056 |
. . . . . . . 8
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
-(𝐴 / (2 · π)) =
(-𝐴 / (2 ·
π))) |
| 60 | 7 | renegcld 11690 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → -𝐴 ∈
ℝ) |
| 61 | 60 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
-𝐴 ∈
ℝ) |
| 62 | 10 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
(2 · π) ∈ ℝ) |
| 63 | | 2rp 13039 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ+ |
| 64 | | rpmulcl 13058 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℝ+ ∧ π ∈ ℝ+) → (2
· π) ∈ ℝ+) |
| 65 | 63, 26, 64 | mp2an 692 |
. . . . . . . . . . 11
⊢ (2
· π) ∈ ℝ+ |
| 66 | 65 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
(2 · π) ∈ ℝ+) |
| 67 | | iccgelb 13443 |
. . . . . . . . . . . . . 14
⊢ ((-π
∈ ℝ* ∧ π ∈ ℝ* ∧ 𝐴 ∈ (-π[,]π)) →
-π ≤ 𝐴) |
| 68 | 22, 23, 6, 67 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → -π ≤ 𝐴) |
| 69 | 19, 7, 68 | lenegcon1d 11845 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → -𝐴 ≤
π) |
| 70 | 60, 19, 20, 69, 28 | lelttrd 11419 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → -𝐴 < (2
· π)) |
| 71 | 70 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
-𝐴 < (2 ·
π)) |
| 72 | 61, 62, 66, 71 | ltdiv1dd 13134 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
(-𝐴 / (2 · π))
< ((2 · π) / (2 · π))) |
| 73 | 72, 34 | breqtrdi 5184 |
. . . . . . . 8
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
(-𝐴 / (2 · π))
< 1) |
| 74 | 59, 73 | eqbrtrd 5165 |
. . . . . . 7
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
-(𝐴 / (2 · π))
< 1) |
| 75 | 53, 54, 74 | ltnegcon1d 11843 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
-1 < (𝐴 / (2 ·
π))) |
| 76 | 7 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
𝐴 ∈
ℝ) |
| 77 | | simpr 484 |
. . . . . . . 8
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
𝐴 < 0) |
| 78 | 76, 66, 77 | divlt0gt0d 45298 |
. . . . . . 7
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
(𝐴 / (2 · π))
< 0) |
| 79 | | neg1cn 12380 |
. . . . . . . . 9
⊢ -1 ∈
ℂ |
| 80 | | ax-1cn 11213 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
| 81 | 79, 80 | addcomi 11452 |
. . . . . . . 8
⊢ (-1 + 1)
= (1 + -1) |
| 82 | | 1pneg1e0 12385 |
. . . . . . . 8
⊢ (1 + -1)
= 0 |
| 83 | 81, 82 | eqtr2i 2766 |
. . . . . . 7
⊢ 0 = (-1 +
1) |
| 84 | 78, 83 | breqtrdi 5184 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
(𝐴 / (2 · π))
< (-1 + 1)) |
| 85 | | btwnnz 12694 |
. . . . . 6
⊢ ((-1
∈ ℤ ∧ -1 < (𝐴 / (2 · π)) ∧ (𝐴 / (2 · π)) < (-1 +
1)) → ¬ (𝐴 / (2
· π)) ∈ ℤ) |
| 86 | 50, 75, 84, 85 | syl3anc 1373 |
. . . . 5
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
¬ (𝐴 / (2 ·
π)) ∈ ℤ) |
| 87 | 40, 48, 86 | syl2anc 584 |
. . . 4
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ ¬ 0 < 𝐴)
→ ¬ (𝐴 / (2
· π)) ∈ ℤ) |
| 88 | 39, 87 | pm2.61dan 813 |
. . 3
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → ¬ (𝐴 / (2
· π)) ∈ ℤ) |
| 89 | 65 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → (2 · π) ∈ ℝ+) |
| 90 | | mod0 13916 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ (2
· π) ∈ ℝ+) → ((𝐴 mod (2 · π)) = 0 ↔ (𝐴 / (2 · π)) ∈
ℤ)) |
| 91 | 7, 89, 90 | syl2anc 584 |
. . 3
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → ((𝐴 mod (2
· π)) = 0 ↔ (𝐴 / (2 · π)) ∈
ℤ)) |
| 92 | 88, 91 | mtbird 325 |
. 2
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → ¬ (𝐴 mod (2
· π)) = 0) |
| 93 | 92 | neqned 2947 |
1
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → (𝐴 mod (2
· π)) ≠ 0) |