Proof of Theorem fourierdlem43
| Step | Hyp | Ref
| Expression |
| 1 | | fourierdlem43.1 |
. 2
⊢ 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) |
| 2 | | 1red 11262 |
. . 3
⊢ ((𝑠 ∈ (-π[,]π) ∧
𝑠 = 0) → 1 ∈
ℝ) |
| 3 | | pire 26500 |
. . . . . . . 8
⊢ π
∈ ℝ |
| 4 | 3 | a1i 11 |
. . . . . . 7
⊢ (𝑠 ∈ (-π[,]π) →
π ∈ ℝ) |
| 5 | 4 | renegcld 11690 |
. . . . . 6
⊢ (𝑠 ∈ (-π[,]π) →
-π ∈ ℝ) |
| 6 | | id 22 |
. . . . . 6
⊢ (𝑠 ∈ (-π[,]π) →
𝑠 ∈
(-π[,]π)) |
| 7 | | eliccre 45518 |
. . . . . 6
⊢ ((-π
∈ ℝ ∧ π ∈ ℝ ∧ 𝑠 ∈ (-π[,]π)) → 𝑠 ∈
ℝ) |
| 8 | 5, 4, 6, 7 | syl3anc 1373 |
. . . . 5
⊢ (𝑠 ∈ (-π[,]π) →
𝑠 ∈
ℝ) |
| 9 | 8 | adantr 480 |
. . . 4
⊢ ((𝑠 ∈ (-π[,]π) ∧
¬ 𝑠 = 0) → 𝑠 ∈
ℝ) |
| 10 | | 2re 12340 |
. . . . . 6
⊢ 2 ∈
ℝ |
| 11 | 10 | a1i 11 |
. . . . 5
⊢ ((𝑠 ∈ (-π[,]π) ∧
¬ 𝑠 = 0) → 2
∈ ℝ) |
| 12 | 9 | rehalfcld 12513 |
. . . . . 6
⊢ ((𝑠 ∈ (-π[,]π) ∧
¬ 𝑠 = 0) → (𝑠 / 2) ∈
ℝ) |
| 13 | 12 | resincld 16179 |
. . . . 5
⊢ ((𝑠 ∈ (-π[,]π) ∧
¬ 𝑠 = 0) →
(sin‘(𝑠 / 2)) ∈
ℝ) |
| 14 | 11, 13 | remulcld 11291 |
. . . 4
⊢ ((𝑠 ∈ (-π[,]π) ∧
¬ 𝑠 = 0) → (2
· (sin‘(𝑠 /
2))) ∈ ℝ) |
| 15 | | 2cnd 12344 |
. . . . 5
⊢ ((𝑠 ∈ (-π[,]π) ∧
¬ 𝑠 = 0) → 2
∈ ℂ) |
| 16 | 13 | recnd 11289 |
. . . . 5
⊢ ((𝑠 ∈ (-π[,]π) ∧
¬ 𝑠 = 0) →
(sin‘(𝑠 / 2)) ∈
ℂ) |
| 17 | | 2ne0 12370 |
. . . . . 6
⊢ 2 ≠
0 |
| 18 | 17 | a1i 11 |
. . . . 5
⊢ ((𝑠 ∈ (-π[,]π) ∧
¬ 𝑠 = 0) → 2 ≠
0) |
| 19 | | 0xr 11308 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ* |
| 20 | 19 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑠 ∈ (-π[,]π) ∧ 0
< 𝑠) → 0 ∈
ℝ*) |
| 21 | 10, 3 | remulcli 11277 |
. . . . . . . . . . 11
⊢ (2
· π) ∈ ℝ |
| 22 | 21 | rexri 11319 |
. . . . . . . . . 10
⊢ (2
· π) ∈ ℝ* |
| 23 | 22 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑠 ∈ (-π[,]π) ∧ 0
< 𝑠) → (2 ·
π) ∈ ℝ*) |
| 24 | 8 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑠 ∈ (-π[,]π) ∧ 0
< 𝑠) → 𝑠 ∈
ℝ) |
| 25 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝑠 ∈ (-π[,]π) ∧ 0
< 𝑠) → 0 < 𝑠) |
| 26 | 21 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (-π[,]π) → (2
· π) ∈ ℝ) |
| 27 | 5 | rexrd 11311 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ (-π[,]π) →
-π ∈ ℝ*) |
| 28 | 4 | rexrd 11311 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ (-π[,]π) →
π ∈ ℝ*) |
| 29 | | iccleub 13442 |
. . . . . . . . . . . 12
⊢ ((-π
∈ ℝ* ∧ π ∈ ℝ* ∧ 𝑠 ∈ (-π[,]π)) →
𝑠 ≤
π) |
| 30 | 27, 28, 6, 29 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (-π[,]π) →
𝑠 ≤
π) |
| 31 | | pirp 26503 |
. . . . . . . . . . . . 13
⊢ π
∈ ℝ+ |
| 32 | | 2timesgt 45300 |
. . . . . . . . . . . . 13
⊢ (π
∈ ℝ+ → π < (2 · π)) |
| 33 | 31, 32 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ π <
(2 · π) |
| 34 | 33 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (-π[,]π) →
π < (2 · π)) |
| 35 | 8, 4, 26, 30, 34 | lelttrd 11419 |
. . . . . . . . . 10
⊢ (𝑠 ∈ (-π[,]π) →
𝑠 < (2 ·
π)) |
| 36 | 35 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑠 ∈ (-π[,]π) ∧ 0
< 𝑠) → 𝑠 < (2 ·
π)) |
| 37 | 20, 23, 24, 25, 36 | eliood 45511 |
. . . . . . . 8
⊢ ((𝑠 ∈ (-π[,]π) ∧ 0
< 𝑠) → 𝑠 ∈ (0(,)(2 ·
π))) |
| 38 | | sinaover2ne0 45883 |
. . . . . . . 8
⊢ (𝑠 ∈ (0(,)(2 · π))
→ (sin‘(𝑠 / 2))
≠ 0) |
| 39 | 37, 38 | syl 17 |
. . . . . . 7
⊢ ((𝑠 ∈ (-π[,]π) ∧ 0
< 𝑠) →
(sin‘(𝑠 / 2)) ≠
0) |
| 40 | 39 | adantlr 715 |
. . . . . 6
⊢ (((𝑠 ∈ (-π[,]π) ∧
¬ 𝑠 = 0) ∧ 0 <
𝑠) → (sin‘(𝑠 / 2)) ≠ 0) |
| 41 | 8 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝑠 ∈ (-π[,]π) ∧
¬ 𝑠 = 0) ∧ ¬ 0
< 𝑠) → 𝑠 ∈
ℝ) |
| 42 | | iccgelb 13443 |
. . . . . . . . . 10
⊢ ((-π
∈ ℝ* ∧ π ∈ ℝ* ∧ 𝑠 ∈ (-π[,]π)) →
-π ≤ 𝑠) |
| 43 | 27, 28, 6, 42 | syl3anc 1373 |
. . . . . . . . 9
⊢ (𝑠 ∈ (-π[,]π) →
-π ≤ 𝑠) |
| 44 | 43 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝑠 ∈ (-π[,]π) ∧
¬ 𝑠 = 0) ∧ ¬ 0
< 𝑠) → -π ≤
𝑠) |
| 45 | | 0red 11264 |
. . . . . . . . 9
⊢ (((𝑠 ∈ (-π[,]π) ∧
¬ 𝑠 = 0) ∧ ¬ 0
< 𝑠) → 0 ∈
ℝ) |
| 46 | | neqne 2948 |
. . . . . . . . . 10
⊢ (¬
𝑠 = 0 → 𝑠 ≠ 0) |
| 47 | 46 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝑠 ∈ (-π[,]π) ∧
¬ 𝑠 = 0) ∧ ¬ 0
< 𝑠) → 𝑠 ≠ 0) |
| 48 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝑠 ∈ (-π[,]π) ∧
¬ 𝑠 = 0) ∧ ¬ 0
< 𝑠) → ¬ 0 <
𝑠) |
| 49 | 41, 45, 47, 48 | lttri5d 45311 |
. . . . . . . 8
⊢ (((𝑠 ∈ (-π[,]π) ∧
¬ 𝑠 = 0) ∧ ¬ 0
< 𝑠) → 𝑠 < 0) |
| 50 | 5 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝑠 ∈ (-π[,]π) ∧
¬ 𝑠 = 0) ∧ ¬ 0
< 𝑠) → -π ∈
ℝ) |
| 51 | | elico2 13451 |
. . . . . . . . 9
⊢ ((-π
∈ ℝ ∧ 0 ∈ ℝ*) → (𝑠 ∈ (-π[,)0) ↔ (𝑠 ∈ ℝ ∧ -π ≤
𝑠 ∧ 𝑠 < 0))) |
| 52 | 50, 19, 51 | sylancl 586 |
. . . . . . . 8
⊢ (((𝑠 ∈ (-π[,]π) ∧
¬ 𝑠 = 0) ∧ ¬ 0
< 𝑠) → (𝑠 ∈ (-π[,)0) ↔
(𝑠 ∈ ℝ ∧
-π ≤ 𝑠 ∧ 𝑠 < 0))) |
| 53 | 41, 44, 49, 52 | mpbir3and 1343 |
. . . . . . 7
⊢ (((𝑠 ∈ (-π[,]π) ∧
¬ 𝑠 = 0) ∧ ¬ 0
< 𝑠) → 𝑠 ∈
(-π[,)0)) |
| 54 | 3 | renegcli 11570 |
. . . . . . . . . . . . . . 15
⊢ -π
∈ ℝ |
| 55 | | elicore 13439 |
. . . . . . . . . . . . . . 15
⊢ ((-π
∈ ℝ ∧ 𝑠
∈ (-π[,)0)) → 𝑠 ∈ ℝ) |
| 56 | 54, 55 | mpan 690 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ (-π[,)0) → 𝑠 ∈
ℝ) |
| 57 | 56 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ (-π[,)0) → 𝑠 ∈
ℂ) |
| 58 | | 2cnd 12344 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ (-π[,)0) → 2
∈ ℂ) |
| 59 | 17 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ (-π[,)0) → 2
≠ 0) |
| 60 | 57, 58, 59 | divnegd 12056 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ (-π[,)0) →
-(𝑠 / 2) = (-𝑠 / 2)) |
| 61 | 60 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (-π[,)0) →
(-𝑠 / 2) = -(𝑠 / 2)) |
| 62 | 61 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑠 ∈ (-π[,)0) →
(sin‘(-𝑠 / 2)) =
(sin‘-(𝑠 /
2))) |
| 63 | 62 | negeqd 11502 |
. . . . . . . . 9
⊢ (𝑠 ∈ (-π[,)0) →
-(sin‘(-𝑠 / 2)) =
-(sin‘-(𝑠 /
2))) |
| 64 | 57 | halfcld 12511 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (-π[,)0) →
(𝑠 / 2) ∈
ℂ) |
| 65 | | sinneg 16182 |
. . . . . . . . . . 11
⊢ ((𝑠 / 2) ∈ ℂ →
(sin‘-(𝑠 / 2)) =
-(sin‘(𝑠 /
2))) |
| 66 | 64, 65 | syl 17 |
. . . . . . . . . 10
⊢ (𝑠 ∈ (-π[,)0) →
(sin‘-(𝑠 / 2)) =
-(sin‘(𝑠 /
2))) |
| 67 | 66 | negeqd 11502 |
. . . . . . . . 9
⊢ (𝑠 ∈ (-π[,)0) →
-(sin‘-(𝑠 / 2)) =
--(sin‘(𝑠 /
2))) |
| 68 | 64 | sincld 16166 |
. . . . . . . . . 10
⊢ (𝑠 ∈ (-π[,)0) →
(sin‘(𝑠 / 2)) ∈
ℂ) |
| 69 | 68 | negnegd 11611 |
. . . . . . . . 9
⊢ (𝑠 ∈ (-π[,)0) →
--(sin‘(𝑠 / 2)) =
(sin‘(𝑠 /
2))) |
| 70 | 63, 67, 69 | 3eqtrd 2781 |
. . . . . . . 8
⊢ (𝑠 ∈ (-π[,)0) →
-(sin‘(-𝑠 / 2)) =
(sin‘(𝑠 /
2))) |
| 71 | 57 | negcld 11607 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (-π[,)0) →
-𝑠 ∈
ℂ) |
| 72 | 71 | halfcld 12511 |
. . . . . . . . . 10
⊢ (𝑠 ∈ (-π[,)0) →
(-𝑠 / 2) ∈
ℂ) |
| 73 | 72 | sincld 16166 |
. . . . . . . . 9
⊢ (𝑠 ∈ (-π[,)0) →
(sin‘(-𝑠 / 2)) ∈
ℂ) |
| 74 | 19 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (-π[,)0) → 0
∈ ℝ*) |
| 75 | 22 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (-π[,)0) → (2
· π) ∈ ℝ*) |
| 76 | 56 | renegcld 11690 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (-π[,)0) →
-𝑠 ∈
ℝ) |
| 77 | 54 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ (-π[,)0) → -π
∈ ℝ) |
| 78 | 77 | rexrd 11311 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ (-π[,)0) → -π
∈ ℝ*) |
| 79 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ (-π[,)0) → 𝑠 ∈
(-π[,)0)) |
| 80 | | icoltub 45521 |
. . . . . . . . . . . . 13
⊢ ((-π
∈ ℝ* ∧ 0 ∈ ℝ* ∧ 𝑠 ∈ (-π[,)0)) →
𝑠 < 0) |
| 81 | 78, 74, 79, 80 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ (-π[,)0) → 𝑠 < 0) |
| 82 | 56 | lt0neg1d 11832 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ (-π[,)0) →
(𝑠 < 0 ↔ 0 <
-𝑠)) |
| 83 | 81, 82 | mpbid 232 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (-π[,)0) → 0
< -𝑠) |
| 84 | 3 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ (-π[,)0) → π
∈ ℝ) |
| 85 | 21 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ (-π[,)0) → (2
· π) ∈ ℝ) |
| 86 | | icogelb 13438 |
. . . . . . . . . . . . . 14
⊢ ((-π
∈ ℝ* ∧ 0 ∈ ℝ* ∧ 𝑠 ∈ (-π[,)0)) →
-π ≤ 𝑠) |
| 87 | 78, 74, 79, 86 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ (-π[,)0) → -π
≤ 𝑠) |
| 88 | 84, 56, 87 | lenegcon1d 11845 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ (-π[,)0) →
-𝑠 ≤
π) |
| 89 | 33 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ (-π[,)0) → π
< (2 · π)) |
| 90 | 76, 84, 85, 88, 89 | lelttrd 11419 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (-π[,)0) →
-𝑠 < (2 ·
π)) |
| 91 | 74, 75, 76, 83, 90 | eliood 45511 |
. . . . . . . . . 10
⊢ (𝑠 ∈ (-π[,)0) →
-𝑠 ∈ (0(,)(2 ·
π))) |
| 92 | | sinaover2ne0 45883 |
. . . . . . . . . 10
⊢ (-𝑠 ∈ (0(,)(2 · π))
→ (sin‘(-𝑠 / 2))
≠ 0) |
| 93 | 91, 92 | syl 17 |
. . . . . . . . 9
⊢ (𝑠 ∈ (-π[,)0) →
(sin‘(-𝑠 / 2)) ≠
0) |
| 94 | 73, 93 | negne0d 11618 |
. . . . . . . 8
⊢ (𝑠 ∈ (-π[,)0) →
-(sin‘(-𝑠 / 2)) ≠
0) |
| 95 | 70, 94 | eqnetrrd 3009 |
. . . . . . 7
⊢ (𝑠 ∈ (-π[,)0) →
(sin‘(𝑠 / 2)) ≠
0) |
| 96 | 53, 95 | syl 17 |
. . . . . 6
⊢ (((𝑠 ∈ (-π[,]π) ∧
¬ 𝑠 = 0) ∧ ¬ 0
< 𝑠) →
(sin‘(𝑠 / 2)) ≠
0) |
| 97 | 40, 96 | pm2.61dan 813 |
. . . . 5
⊢ ((𝑠 ∈ (-π[,]π) ∧
¬ 𝑠 = 0) →
(sin‘(𝑠 / 2)) ≠
0) |
| 98 | 15, 16, 18, 97 | mulne0d 11915 |
. . . 4
⊢ ((𝑠 ∈ (-π[,]π) ∧
¬ 𝑠 = 0) → (2
· (sin‘(𝑠 /
2))) ≠ 0) |
| 99 | 9, 14, 98 | redivcld 12095 |
. . 3
⊢ ((𝑠 ∈ (-π[,]π) ∧
¬ 𝑠 = 0) → (𝑠 / (2 · (sin‘(𝑠 / 2)))) ∈
ℝ) |
| 100 | 2, 99 | ifclda 4561 |
. 2
⊢ (𝑠 ∈ (-π[,]π) →
if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈
ℝ) |
| 101 | 1, 100 | fmpti 7132 |
1
⊢ 𝐾:(-π[,]π)⟶ℝ |