Proof of Theorem fourierdlem24
Step | Hyp | Ref
| Expression |
1 | | 0zd 11987 |
. . . . 5
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
0 ∈ ℤ) |
2 | | pire 25038 |
. . . . . . . . . 10
⊢ π
∈ ℝ |
3 | 2 | renegcli 10941 |
. . . . . . . . 9
⊢ -π
∈ ℝ |
4 | | iccssre 12812 |
. . . . . . . . 9
⊢ ((-π
∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆
ℝ) |
5 | 3, 2, 4 | mp2an 690 |
. . . . . . . 8
⊢
(-π[,]π) ⊆ ℝ |
6 | | eldifi 4103 |
. . . . . . . 8
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → 𝐴 ∈
(-π[,]π)) |
7 | 5, 6 | sseldi 3965 |
. . . . . . 7
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → 𝐴 ∈
ℝ) |
8 | 7 | adantr 483 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
𝐴 ∈
ℝ) |
9 | | 2re 11705 |
. . . . . . . 8
⊢ 2 ∈
ℝ |
10 | 9, 2 | remulcli 10651 |
. . . . . . 7
⊢ (2
· π) ∈ ℝ |
11 | 10 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
(2 · π) ∈ ℝ) |
12 | | simpr 487 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
0 < 𝐴) |
13 | | 2pos 11734 |
. . . . . . . 8
⊢ 0 <
2 |
14 | | pipos 25040 |
. . . . . . . 8
⊢ 0 <
π |
15 | 9, 2, 13, 14 | mulgt0ii 10767 |
. . . . . . 7
⊢ 0 < (2
· π) |
16 | 15 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
0 < (2 · π)) |
17 | 8, 11, 12, 16 | divgt0d 11569 |
. . . . 5
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
0 < (𝐴 / (2 ·
π))) |
18 | 11, 16 | elrpd 12422 |
. . . . . . . 8
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
(2 · π) ∈ ℝ+) |
19 | 2 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → π ∈ ℝ) |
20 | 10 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → (2 · π) ∈ ℝ) |
21 | 3 | rexri 10693 |
. . . . . . . . . . . 12
⊢ -π
∈ ℝ* |
22 | 21 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → -π ∈ ℝ*) |
23 | 19 | rexrd 10685 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → π ∈ ℝ*) |
24 | | iccleub 12786 |
. . . . . . . . . . 11
⊢ ((-π
∈ ℝ* ∧ π ∈ ℝ* ∧ 𝐴 ∈ (-π[,]π)) →
𝐴 ≤
π) |
25 | 22, 23, 6, 24 | syl3anc 1367 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → 𝐴 ≤
π) |
26 | | pirp 25041 |
. . . . . . . . . . 11
⊢ π
∈ ℝ+ |
27 | | 2timesgt 41546 |
. . . . . . . . . . 11
⊢ (π
∈ ℝ+ → π < (2 · π)) |
28 | 26, 27 | mp1i 13 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → π < (2 · π)) |
29 | 7, 19, 20, 25, 28 | lelttrd 10792 |
. . . . . . . . 9
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → 𝐴 < (2
· π)) |
30 | 29 | adantr 483 |
. . . . . . . 8
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
𝐴 < (2 ·
π)) |
31 | 8, 11, 18, 30 | ltdiv1dd 12482 |
. . . . . . 7
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
(𝐴 / (2 · π))
< ((2 · π) / (2 · π))) |
32 | 10 | recni 10649 |
. . . . . . . 8
⊢ (2
· π) ∈ ℂ |
33 | 10, 15 | gt0ne0ii 11170 |
. . . . . . . 8
⊢ (2
· π) ≠ 0 |
34 | 32, 33 | dividi 11367 |
. . . . . . 7
⊢ ((2
· π) / (2 · π)) = 1 |
35 | 31, 34 | breqtrdi 5100 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
(𝐴 / (2 · π))
< 1) |
36 | | 0p1e1 11753 |
. . . . . 6
⊢ (0 + 1) =
1 |
37 | 35, 36 | breqtrrdi 5101 |
. . . . 5
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
(𝐴 / (2 · π))
< (0 + 1)) |
38 | | btwnnz 12052 |
. . . . 5
⊢ ((0
∈ ℤ ∧ 0 < (𝐴 / (2 · π)) ∧ (𝐴 / (2 · π)) < (0 +
1)) → ¬ (𝐴 / (2
· π)) ∈ ℤ) |
39 | 1, 17, 37, 38 | syl3anc 1367 |
. . . 4
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 0 < 𝐴) →
¬ (𝐴 / (2 ·
π)) ∈ ℤ) |
40 | | simpl 485 |
. . . . 5
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ ¬ 0 < 𝐴)
→ 𝐴 ∈
((-π[,]π) ∖ {0})) |
41 | 7 | adantr 483 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ ¬ 0 < 𝐴)
→ 𝐴 ∈
ℝ) |
42 | | 0red 10638 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ ¬ 0 < 𝐴)
→ 0 ∈ ℝ) |
43 | | simpr 487 |
. . . . . . 7
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ ¬ 0 < 𝐴)
→ ¬ 0 < 𝐴) |
44 | 41, 42, 43 | nltled 10784 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ ¬ 0 < 𝐴)
→ 𝐴 ≤
0) |
45 | | eldifsni 4716 |
. . . . . . . 8
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → 𝐴 ≠
0) |
46 | 45 | necomd 3071 |
. . . . . . 7
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → 0 ≠ 𝐴) |
47 | 46 | adantr 483 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ ¬ 0 < 𝐴)
→ 0 ≠ 𝐴) |
48 | 41, 42, 44, 47 | leneltd 10788 |
. . . . 5
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ ¬ 0 < 𝐴)
→ 𝐴 <
0) |
49 | | neg1z 12012 |
. . . . . . 7
⊢ -1 ∈
ℤ |
50 | 49 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
-1 ∈ ℤ) |
51 | 33 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → (2 · π) ≠ 0) |
52 | 7, 20, 51 | redivcld 11462 |
. . . . . . . 8
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → (𝐴 / (2
· π)) ∈ ℝ) |
53 | 52 | adantr 483 |
. . . . . . 7
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
(𝐴 / (2 · π))
∈ ℝ) |
54 | | 1red 10636 |
. . . . . . 7
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
1 ∈ ℝ) |
55 | 7 | recnd 10663 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → 𝐴 ∈
ℂ) |
56 | 55 | adantr 483 |
. . . . . . . . 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 11423 |
. . . . . . . 8
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
-(𝐴 / (2 · π)) =
(-𝐴 / (2 ·
π))) |
60 | 7 | renegcld 11061 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → -𝐴 ∈
ℝ) |
61 | 60 | adantr 483 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
-𝐴 ∈
ℝ) |
62 | 10 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
(2 · π) ∈ ℝ) |
63 | | 2rp 12388 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ+ |
64 | | rpmulcl 12406 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℝ+ ∧ π ∈ ℝ+) → (2
· π) ∈ ℝ+) |
65 | 63, 26, 64 | mp2an 690 |
. . . . . . . . . . 11
⊢ (2
· π) ∈ ℝ+ |
66 | 65 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
(2 · π) ∈ ℝ+) |
67 | | iccgelb 12787 |
. . . . . . . . . . . . . 14
⊢ ((-π
∈ ℝ* ∧ π ∈ ℝ* ∧ 𝐴 ∈ (-π[,]π)) →
-π ≤ 𝐴) |
68 | 22, 23, 6, 67 | syl3anc 1367 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → -π ≤ 𝐴) |
69 | 19, 7, 68 | lenegcon1d 11216 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → -𝐴 ≤
π) |
70 | 60, 19, 20, 69, 28 | lelttrd 10792 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → -𝐴 < (2
· π)) |
71 | 70 | adantr 483 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
-𝐴 < (2 ·
π)) |
72 | 61, 62, 66, 71 | ltdiv1dd 12482 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
(-𝐴 / (2 · π))
< ((2 · π) / (2 · π))) |
73 | 72, 34 | breqtrdi 5100 |
. . . . . . . 8
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
(-𝐴 / (2 · π))
< 1) |
74 | 59, 73 | eqbrtrd 5081 |
. . . . . . 7
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
-(𝐴 / (2 · π))
< 1) |
75 | 53, 54, 74 | ltnegcon1d 11214 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
-1 < (𝐴 / (2 ·
π))) |
76 | 7 | adantr 483 |
. . . . . . . 8
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
𝐴 ∈
ℝ) |
77 | | simpr 487 |
. . . . . . . 8
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
𝐴 < 0) |
78 | 76, 66, 77 | divlt0gt0d 41544 |
. . . . . . 7
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
(𝐴 / (2 · π))
< 0) |
79 | | neg1cn 11745 |
. . . . . . . . 9
⊢ -1 ∈
ℂ |
80 | | ax-1cn 10589 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
81 | 79, 80 | addcomi 10825 |
. . . . . . . 8
⊢ (-1 + 1)
= (1 + -1) |
82 | | 1pneg1e0 11750 |
. . . . . . . 8
⊢ (1 + -1)
= 0 |
83 | 81, 82 | eqtr2i 2845 |
. . . . . . 7
⊢ 0 = (-1 +
1) |
84 | 78, 83 | breqtrdi 5100 |
. . . . . 6
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
(𝐴 / (2 · π))
< (-1 + 1)) |
85 | | btwnnz 12052 |
. . . . . 6
⊢ ((-1
∈ ℤ ∧ -1 < (𝐴 / (2 · π)) ∧ (𝐴 / (2 · π)) < (-1 +
1)) → ¬ (𝐴 / (2
· π)) ∈ ℤ) |
86 | 50, 75, 84, 85 | syl3anc 1367 |
. . . . 5
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ 𝐴 < 0) →
¬ (𝐴 / (2 ·
π)) ∈ ℤ) |
87 | 40, 48, 86 | syl2anc 586 |
. . . 4
⊢ ((𝐴 ∈ ((-π[,]π) ∖
{0}) ∧ ¬ 0 < 𝐴)
→ ¬ (𝐴 / (2
· π)) ∈ ℤ) |
88 | 39, 87 | pm2.61dan 811 |
. . 3
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → ¬ (𝐴 / (2
· π)) ∈ ℤ) |
89 | 65 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → (2 · π) ∈ ℝ+) |
90 | | mod0 13238 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ (2
· π) ∈ ℝ+) → ((𝐴 mod (2 · π)) = 0 ↔ (𝐴 / (2 · π)) ∈
ℤ)) |
91 | 7, 89, 90 | syl2anc 586 |
. . 3
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → ((𝐴 mod (2
· π)) = 0 ↔ (𝐴 / (2 · π)) ∈
ℤ)) |
92 | 88, 91 | mtbird 327 |
. 2
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → ¬ (𝐴 mod (2
· π)) = 0) |
93 | 92 | neqned 3023 |
1
⊢ (𝐴 ∈ ((-π[,]π) ∖
{0}) → (𝐴 mod (2
· π)) ≠ 0) |