Step | Hyp | Ref
| Expression |
1 | | fourierdlem43.1 |
. 2
β’ πΎ = (π β (-Ο[,]Ο) β¦ if(π = 0, 1, (π / (2 Β· (sinβ(π / 2)))))) |
2 | | 1red 11220 |
. . 3
β’ ((π β (-Ο[,]Ο) β§
π = 0) β 1 β
β) |
3 | | pire 26205 |
. . . . . . . 8
β’ Ο
β β |
4 | 3 | a1i 11 |
. . . . . . 7
β’ (π β (-Ο[,]Ο) β
Ο β β) |
5 | 4 | renegcld 11646 |
. . . . . 6
β’ (π β (-Ο[,]Ο) β
-Ο β β) |
6 | | id 22 |
. . . . . 6
β’ (π β (-Ο[,]Ο) β
π β
(-Ο[,]Ο)) |
7 | | eliccre 44517 |
. . . . . 6
β’ ((-Ο
β β β§ Ο β β β§ π β (-Ο[,]Ο)) β π β
β) |
8 | 5, 4, 6, 7 | syl3anc 1370 |
. . . . 5
β’ (π β (-Ο[,]Ο) β
π β
β) |
9 | 8 | adantr 480 |
. . . 4
β’ ((π β (-Ο[,]Ο) β§
Β¬ π = 0) β π β
β) |
10 | | 2re 12291 |
. . . . . 6
β’ 2 β
β |
11 | 10 | a1i 11 |
. . . . 5
β’ ((π β (-Ο[,]Ο) β§
Β¬ π = 0) β 2
β β) |
12 | 9 | rehalfcld 12464 |
. . . . . 6
β’ ((π β (-Ο[,]Ο) β§
Β¬ π = 0) β (π / 2) β
β) |
13 | 12 | resincld 16091 |
. . . . 5
β’ ((π β (-Ο[,]Ο) β§
Β¬ π = 0) β
(sinβ(π / 2)) β
β) |
14 | 11, 13 | remulcld 11249 |
. . . 4
β’ ((π β (-Ο[,]Ο) β§
Β¬ π = 0) β (2
Β· (sinβ(π /
2))) β β) |
15 | | 2cnd 12295 |
. . . . 5
β’ ((π β (-Ο[,]Ο) β§
Β¬ π = 0) β 2
β β) |
16 | 13 | recnd 11247 |
. . . . 5
β’ ((π β (-Ο[,]Ο) β§
Β¬ π = 0) β
(sinβ(π / 2)) β
β) |
17 | | 2ne0 12321 |
. . . . . 6
β’ 2 β
0 |
18 | 17 | a1i 11 |
. . . . 5
β’ ((π β (-Ο[,]Ο) β§
Β¬ π = 0) β 2 β
0) |
19 | | 0xr 11266 |
. . . . . . . . . 10
β’ 0 β
β* |
20 | 19 | a1i 11 |
. . . . . . . . 9
β’ ((π β (-Ο[,]Ο) β§ 0
< π ) β 0 β
β*) |
21 | 10, 3 | remulcli 11235 |
. . . . . . . . . . 11
β’ (2
Β· Ο) β β |
22 | 21 | rexri 11277 |
. . . . . . . . . 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 11269 |
. . . . . . . . . . . 12
β’ (π β (-Ο[,]Ο) β
-Ο β β*) |
28 | 4 | rexrd 11269 |
. . . . . . . . . . . 12
β’ (π β (-Ο[,]Ο) β
Ο β β*) |
29 | | iccleub 13384 |
. . . . . . . . . . . 12
β’ ((-Ο
β β* β§ Ο β β* β§ π β (-Ο[,]Ο)) β
π β€
Ο) |
30 | 27, 28, 6, 29 | syl3anc 1370 |
. . . . . . . . . . 11
β’ (π β (-Ο[,]Ο) β
π β€
Ο) |
31 | | pirp 26208 |
. . . . . . . . . . . . 13
β’ Ο
β β+ |
32 | | 2timesgt 44297 |
. . . . . . . . . . . . 13
β’ (Ο
β β+ β Ο < (2 Β· Ο)) |
33 | 31, 32 | ax-mp 5 |
. . . . . . . . . . . 12
β’ Ο <
(2 Β· Ο) |
34 | 33 | a1i 11 |
. . . . . . . . . . 11
β’ (π β (-Ο[,]Ο) β
Ο < (2 Β· Ο)) |
35 | 8, 4, 26, 30, 34 | lelttrd 11377 |
. . . . . . . . . 10
β’ (π β (-Ο[,]Ο) β
π < (2 Β·
Ο)) |
36 | 35 | adantr 480 |
. . . . . . . . 9
β’ ((π β (-Ο[,]Ο) β§ 0
< π ) β π < (2 Β·
Ο)) |
37 | 20, 23, 24, 25, 36 | eliood 44510 |
. . . . . . . 8
β’ ((π β (-Ο[,]Ο) β§ 0
< π ) β π β (0(,)(2 Β·
Ο))) |
38 | | sinaover2ne0 44883 |
. . . . . . . 8
β’ (π β (0(,)(2 Β· Ο))
β (sinβ(π / 2))
β 0) |
39 | 37, 38 | syl 17 |
. . . . . . 7
β’ ((π β (-Ο[,]Ο) β§ 0
< π ) β
(sinβ(π / 2)) β
0) |
40 | 39 | adantlr 712 |
. . . . . 6
β’ (((π β (-Ο[,]Ο) β§
Β¬ π = 0) β§ 0 <
π ) β (sinβ(π / 2)) β 0) |
41 | 8 | ad2antrr 723 |
. . . . . . . 8
β’ (((π β (-Ο[,]Ο) β§
Β¬ π = 0) β§ Β¬ 0
< π ) β π β
β) |
42 | | iccgelb 13385 |
. . . . . . . . . 10
β’ ((-Ο
β β* β§ Ο β β* β§ π β (-Ο[,]Ο)) β
-Ο β€ π ) |
43 | 27, 28, 6, 42 | syl3anc 1370 |
. . . . . . . . 9
β’ (π β (-Ο[,]Ο) β
-Ο β€ π ) |
44 | 43 | ad2antrr 723 |
. . . . . . . 8
β’ (((π β (-Ο[,]Ο) β§
Β¬ π = 0) β§ Β¬ 0
< π ) β -Ο β€
π ) |
45 | | 0red 11222 |
. . . . . . . . 9
β’ (((π β (-Ο[,]Ο) β§
Β¬ π = 0) β§ Β¬ 0
< π ) β 0 β
β) |
46 | | neqne 2947 |
. . . . . . . . . 10
β’ (Β¬
π = 0 β π β 0) |
47 | 46 | ad2antlr 724 |
. . . . . . . . 9
β’ (((π β (-Ο[,]Ο) β§
Β¬ π = 0) β§ Β¬ 0
< π ) β π β 0) |
48 | | simpr 484 |
. . . . . . . . 9
β’ (((π β (-Ο[,]Ο) β§
Β¬ π = 0) β§ Β¬ 0
< π ) β Β¬ 0 <
π ) |
49 | 41, 45, 47, 48 | lttri5d 44308 |
. . . . . . . 8
β’ (((π β (-Ο[,]Ο) β§
Β¬ π = 0) β§ Β¬ 0
< π ) β π < 0) |
50 | 5 | ad2antrr 723 |
. . . . . . . . 9
β’ (((π β (-Ο[,]Ο) β§
Β¬ π = 0) β§ Β¬ 0
< π ) β -Ο β
β) |
51 | | elico2 13393 |
. . . . . . . . 9
β’ ((-Ο
β β β§ 0 β β*) β (π β (-Ο[,)0) β (π β β β§ -Ο β€
π β§ π < 0))) |
52 | 50, 19, 51 | sylancl 585 |
. . . . . . . 8
β’ (((π β (-Ο[,]Ο) β§
Β¬ π = 0) β§ Β¬ 0
< π ) β (π β (-Ο[,)0) β
(π β β β§
-Ο β€ π β§ π < 0))) |
53 | 41, 44, 49, 52 | mpbir3and 1341 |
. . . . . . 7
β’ (((π β (-Ο[,]Ο) β§
Β¬ π = 0) β§ Β¬ 0
< π ) β π β
(-Ο[,)0)) |
54 | 3 | renegcli 11526 |
. . . . . . . . . . . . . . 15
β’ -Ο
β β |
55 | | elicore 13381 |
. . . . . . . . . . . . . . 15
β’ ((-Ο
β β β§ π
β (-Ο[,)0)) β π β β) |
56 | 54, 55 | mpan 687 |
. . . . . . . . . . . . . 14
β’ (π β (-Ο[,)0) β π β
β) |
57 | 56 | recnd 11247 |
. . . . . . . . . . . . 13
β’ (π β (-Ο[,)0) β π β
β) |
58 | | 2cnd 12295 |
. . . . . . . . . . . . 13
β’ (π β (-Ο[,)0) β 2
β β) |
59 | 17 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β (-Ο[,)0) β 2
β 0) |
60 | 57, 58, 59 | divnegd 12008 |
. . . . . . . . . . . 12
β’ (π β (-Ο[,)0) β
-(π / 2) = (-π / 2)) |
61 | 60 | eqcomd 2737 |
. . . . . . . . . . 11
β’ (π β (-Ο[,)0) β
(-π / 2) = -(π / 2)) |
62 | 61 | fveq2d 6895 |
. . . . . . . . . 10
β’ (π β (-Ο[,)0) β
(sinβ(-π / 2)) =
(sinβ-(π /
2))) |
63 | 62 | negeqd 11459 |
. . . . . . . . 9
β’ (π β (-Ο[,)0) β
-(sinβ(-π / 2)) =
-(sinβ-(π /
2))) |
64 | 57 | halfcld 12462 |
. . . . . . . . . . 11
β’ (π β (-Ο[,)0) β
(π / 2) β
β) |
65 | | sinneg 16094 |
. . . . . . . . . . 11
β’ ((π / 2) β β β
(sinβ-(π / 2)) =
-(sinβ(π /
2))) |
66 | 64, 65 | syl 17 |
. . . . . . . . . 10
β’ (π β (-Ο[,)0) β
(sinβ-(π / 2)) =
-(sinβ(π /
2))) |
67 | 66 | negeqd 11459 |
. . . . . . . . 9
β’ (π β (-Ο[,)0) β
-(sinβ-(π / 2)) =
--(sinβ(π /
2))) |
68 | 64 | sincld 16078 |
. . . . . . . . . 10
β’ (π β (-Ο[,)0) β
(sinβ(π / 2)) β
β) |
69 | 68 | negnegd 11567 |
. . . . . . . . 9
β’ (π β (-Ο[,)0) β
--(sinβ(π / 2)) =
(sinβ(π /
2))) |
70 | 63, 67, 69 | 3eqtrd 2775 |
. . . . . . . 8
β’ (π β (-Ο[,)0) β
-(sinβ(-π / 2)) =
(sinβ(π /
2))) |
71 | 57 | negcld 11563 |
. . . . . . . . . . 11
β’ (π β (-Ο[,)0) β
-π β
β) |
72 | 71 | halfcld 12462 |
. . . . . . . . . 10
β’ (π β (-Ο[,)0) β
(-π / 2) β
β) |
73 | 72 | sincld 16078 |
. . . . . . . . 9
β’ (π β (-Ο[,)0) β
(sinβ(-π / 2)) β
β) |
74 | 19 | a1i 11 |
. . . . . . . . . . 11
β’ (π β (-Ο[,)0) β 0
β β*) |
75 | 22 | a1i 11 |
. . . . . . . . . . 11
β’ (π β (-Ο[,)0) β (2
Β· Ο) β β*) |
76 | 56 | renegcld 11646 |
. . . . . . . . . . 11
β’ (π β (-Ο[,)0) β
-π β
β) |
77 | 54 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β (-Ο[,)0) β -Ο
β β) |
78 | 77 | rexrd 11269 |
. . . . . . . . . . . . 13
β’ (π β (-Ο[,)0) β -Ο
β β*) |
79 | | id 22 |
. . . . . . . . . . . . 13
β’ (π β (-Ο[,)0) β π β
(-Ο[,)0)) |
80 | | icoltub 44520 |
. . . . . . . . . . . . 13
β’ ((-Ο
β β* β§ 0 β β* β§ π β (-Ο[,)0)) β
π < 0) |
81 | 78, 74, 79, 80 | syl3anc 1370 |
. . . . . . . . . . . 12
β’ (π β (-Ο[,)0) β π < 0) |
82 | 56 | lt0neg1d 11788 |
. . . . . . . . . . . 12
β’ (π β (-Ο[,)0) β
(π < 0 β 0 <
-π )) |
83 | 81, 82 | mpbid 231 |
. . . . . . . . . . 11
β’ (π β (-Ο[,)0) β 0
< -π ) |
84 | 3 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (-Ο[,)0) β Ο
β β) |
85 | 21 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (-Ο[,)0) β (2
Β· Ο) β β) |
86 | | icogelb 13380 |
. . . . . . . . . . . . . 14
β’ ((-Ο
β β* β§ 0 β β* β§ π β (-Ο[,)0)) β
-Ο β€ π ) |
87 | 78, 74, 79, 86 | syl3anc 1370 |
. . . . . . . . . . . . 13
β’ (π β (-Ο[,)0) β -Ο
β€ π ) |
88 | 84, 56, 87 | lenegcon1d 11801 |
. . . . . . . . . . . 12
β’ (π β (-Ο[,)0) β
-π β€
Ο) |
89 | 33 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (-Ο[,)0) β Ο
< (2 Β· Ο)) |
90 | 76, 84, 85, 88, 89 | lelttrd 11377 |
. . . . . . . . . . 11
β’ (π β (-Ο[,)0) β
-π < (2 Β·
Ο)) |
91 | 74, 75, 76, 83, 90 | eliood 44510 |
. . . . . . . . . 10
β’ (π β (-Ο[,)0) β
-π β (0(,)(2 Β·
Ο))) |
92 | | sinaover2ne0 44883 |
. . . . . . . . . 10
β’ (-π β (0(,)(2 Β· Ο))
β (sinβ(-π / 2))
β 0) |
93 | 91, 92 | syl 17 |
. . . . . . . . 9
β’ (π β (-Ο[,)0) β
(sinβ(-π / 2)) β
0) |
94 | 73, 93 | negne0d 11574 |
. . . . . . . 8
β’ (π β (-Ο[,)0) β
-(sinβ(-π / 2)) β
0) |
95 | 70, 94 | eqnetrrd 3008 |
. . . . . . 7
β’ (π β (-Ο[,)0) β
(sinβ(π / 2)) β
0) |
96 | 53, 95 | syl 17 |
. . . . . 6
β’ (((π β (-Ο[,]Ο) β§
Β¬ π = 0) β§ Β¬ 0
< π ) β
(sinβ(π / 2)) β
0) |
97 | 40, 96 | pm2.61dan 810 |
. . . . 5
β’ ((π β (-Ο[,]Ο) β§
Β¬ π = 0) β
(sinβ(π / 2)) β
0) |
98 | 15, 16, 18, 97 | mulne0d 11871 |
. . . 4
β’ ((π β (-Ο[,]Ο) β§
Β¬ π = 0) β (2
Β· (sinβ(π /
2))) β 0) |
99 | 9, 14, 98 | redivcld 12047 |
. . 3
β’ ((π β (-Ο[,]Ο) β§
Β¬ π = 0) β (π / (2 Β· (sinβ(π / 2)))) β
β) |
100 | 2, 99 | ifclda 4563 |
. 2
β’ (π β (-Ο[,]Ο) β
if(π = 0, 1, (π / (2 Β· (sinβ(π / 2))))) β
β) |
101 | 1, 100 | fmpti 7113 |
1
β’ πΎ:(-Ο[,]Ο)βΆβ |