Step | Hyp | Ref
| Expression |
1 | | oveq1 7418 |
. . . . . . . . . . 11
β’ (π = 0 β (π Β· π₯) = (0 Β· π₯)) |
2 | 1 | oveq2d 7427 |
. . . . . . . . . 10
β’ (π = 0 β ((i Β· (2
Β· Ο)) Β· (π
Β· π₯)) = ((i Β·
(2 Β· Ο)) Β· (0 Β· π₯))) |
3 | 2 | fveq2d 6895 |
. . . . . . . . 9
β’ (π = 0 β (expβ((i
Β· (2 Β· Ο)) Β· (π Β· π₯))) = (expβ((i Β· (2 Β·
Ο)) Β· (0 Β· π₯)))) |
4 | | ioossre 13389 |
. . . . . . . . . . . . . . . 16
β’ (0(,)1)
β β |
5 | | ax-resscn 11169 |
. . . . . . . . . . . . . . . 16
β’ β
β β |
6 | 4, 5 | sstri 3991 |
. . . . . . . . . . . . . . 15
β’ (0(,)1)
β β |
7 | 6 | sseli 3978 |
. . . . . . . . . . . . . 14
β’ (π₯ β (0(,)1) β π₯ β
β) |
8 | 7 | mul02d 11416 |
. . . . . . . . . . . . 13
β’ (π₯ β (0(,)1) β (0
Β· π₯) =
0) |
9 | 8 | oveq2d 7427 |
. . . . . . . . . . . 12
β’ (π₯ β (0(,)1) β ((i
Β· (2 Β· Ο)) Β· (0 Β· π₯)) = ((i Β· (2 Β· Ο)) Β·
0)) |
10 | | ax-icn 11171 |
. . . . . . . . . . . . . 14
β’ i β
β |
11 | | 2cn 12291 |
. . . . . . . . . . . . . . 15
β’ 2 β
β |
12 | | picn 26193 |
. . . . . . . . . . . . . . 15
β’ Ο
β β |
13 | 11, 12 | mulcli 11225 |
. . . . . . . . . . . . . 14
β’ (2
Β· Ο) β β |
14 | 10, 13 | mulcli 11225 |
. . . . . . . . . . . . 13
β’ (i
Β· (2 Β· Ο)) β β |
15 | 14 | mul01i 11408 |
. . . . . . . . . . . 12
β’ ((i
Β· (2 Β· Ο)) Β· 0) = 0 |
16 | 9, 15 | eqtrdi 2788 |
. . . . . . . . . . 11
β’ (π₯ β (0(,)1) β ((i
Β· (2 Β· Ο)) Β· (0 Β· π₯)) = 0) |
17 | 16 | fveq2d 6895 |
. . . . . . . . . 10
β’ (π₯ β (0(,)1) β
(expβ((i Β· (2 Β· Ο)) Β· (0 Β· π₯))) =
(expβ0)) |
18 | | ef0 16038 |
. . . . . . . . . 10
β’
(expβ0) = 1 |
19 | 17, 18 | eqtrdi 2788 |
. . . . . . . . 9
β’ (π₯ β (0(,)1) β
(expβ((i Β· (2 Β· Ο)) Β· (0 Β· π₯))) = 1) |
20 | 3, 19 | sylan9eq 2792 |
. . . . . . . 8
β’ ((π = 0 β§ π₯ β (0(,)1)) β (expβ((i
Β· (2 Β· Ο)) Β· (π Β· π₯))) = 1) |
21 | 20 | ralrimiva 3146 |
. . . . . . 7
β’ (π = 0 β βπ₯ β (0(,)1)(expβ((i
Β· (2 Β· Ο)) Β· (π Β· π₯))) = 1) |
22 | | itgeq2 25519 |
. . . . . . 7
β’
(βπ₯ β
(0(,)1)(expβ((i Β· (2 Β· Ο)) Β· (π Β· π₯))) = 1 β β«(0(,)1)(expβ((i
Β· (2 Β· Ο)) Β· (π Β· π₯))) dπ₯ = β«(0(,)1)1 dπ₯) |
23 | 21, 22 | syl 17 |
. . . . . 6
β’ (π = 0 β
β«(0(,)1)(expβ((i Β· (2 Β· Ο)) Β· (π Β· π₯))) dπ₯ = β«(0(,)1)1 dπ₯) |
24 | | ioombl 25306 |
. . . . . . . 8
β’ (0(,)1)
β dom vol |
25 | | 0re 11220 |
. . . . . . . . 9
β’ 0 β
β |
26 | | 1re 11218 |
. . . . . . . . 9
β’ 1 β
β |
27 | | ioovolcl 25311 |
. . . . . . . . 9
β’ ((0
β β β§ 1 β β) β (volβ(0(,)1)) β
β) |
28 | 25, 26, 27 | mp2an 690 |
. . . . . . . 8
β’
(volβ(0(,)1)) β β |
29 | | ax-1cn 11170 |
. . . . . . . 8
β’ 1 β
β |
30 | | itgconst 25560 |
. . . . . . . 8
β’ (((0(,)1)
β dom vol β§ (volβ(0(,)1)) β β β§ 1 β β)
β β«(0(,)1)1 dπ₯ =
(1 Β· (volβ(0(,)1)))) |
31 | 24, 28, 29, 30 | mp3an 1461 |
. . . . . . 7
β’
β«(0(,)1)1 dπ₯ =
(1 Β· (volβ(0(,)1))) |
32 | | 0le1 11741 |
. . . . . . . . . 10
β’ 0 β€
1 |
33 | | volioo 25310 |
. . . . . . . . . 10
β’ ((0
β β β§ 1 β β β§ 0 β€ 1) β
(volβ(0(,)1)) = (1 β 0)) |
34 | 25, 26, 32, 33 | mp3an 1461 |
. . . . . . . . 9
β’
(volβ(0(,)1)) = (1 β 0) |
35 | 29 | subid1i 11536 |
. . . . . . . . 9
β’ (1
β 0) = 1 |
36 | 34, 35 | eqtri 2760 |
. . . . . . . 8
β’
(volβ(0(,)1)) = 1 |
37 | 36 | oveq2i 7422 |
. . . . . . 7
β’ (1
Β· (volβ(0(,)1))) = (1 Β· 1) |
38 | 29 | mulridi 11222 |
. . . . . . 7
β’ (1
Β· 1) = 1 |
39 | 31, 37, 38 | 3eqtri 2764 |
. . . . . 6
β’
β«(0(,)1)1 dπ₯ =
1 |
40 | 23, 39 | eqtrdi 2788 |
. . . . 5
β’ (π = 0 β
β«(0(,)1)(expβ((i Β· (2 Β· Ο)) Β· (π Β· π₯))) dπ₯ = 1) |
41 | 40 | adantl 482 |
. . . 4
β’ ((π β β€ β§ π = 0) β
β«(0(,)1)(expβ((i Β· (2 Β· Ο)) Β· (π Β· π₯))) dπ₯ = 1) |
42 | 41 | eqcomd 2738 |
. . 3
β’ ((π β β€ β§ π = 0) β 1 =
β«(0(,)1)(expβ((i Β· (2 Β· Ο)) Β· (π Β· π₯))) dπ₯) |
43 | | ioomax 13403 |
. . . . . . 7
β’
(-β(,)+β) = β |
44 | 43 | eqcomi 2741 |
. . . . . 6
β’ β =
(-β(,)+β) |
45 | | 0red 11221 |
. . . . . 6
β’ ((π β β€ β§ Β¬
π = 0) β 0 β
β) |
46 | | 1red 11219 |
. . . . . 6
β’ ((π β β€ β§ Β¬
π = 0) β 1 β
β) |
47 | 32 | a1i 11 |
. . . . . 6
β’ ((π β β€ β§ Β¬
π = 0) β 0 β€
1) |
48 | 5 | a1i 11 |
. . . . . . . . . 10
β’ ((π β β€ β§ Β¬
π = 0) β β
β β) |
49 | 48 | sselda 3982 |
. . . . . . . . 9
β’ (((π β β€ β§ Β¬
π = 0) β§ π¦ β β) β π¦ β
β) |
50 | 10 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β β€ β§ Β¬
π = 0) β i β
β) |
51 | | 2cnd 12294 |
. . . . . . . . . . . . . . 15
β’ ((π β β€ β§ Β¬
π = 0) β 2 β
β) |
52 | 12 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β β€ β§ Β¬
π = 0) β Ο β
β) |
53 | 51, 52 | mulcld 11238 |
. . . . . . . . . . . . . 14
β’ ((π β β€ β§ Β¬
π = 0) β (2 Β·
Ο) β β) |
54 | 50, 53 | mulcld 11238 |
. . . . . . . . . . . . 13
β’ ((π β β€ β§ Β¬
π = 0) β (i Β·
(2 Β· Ο)) β β) |
55 | | simpl 483 |
. . . . . . . . . . . . . 14
β’ ((π β β€ β§ Β¬
π = 0) β π β
β€) |
56 | 55 | zcnd 12671 |
. . . . . . . . . . . . 13
β’ ((π β β€ β§ Β¬
π = 0) β π β
β) |
57 | 54, 56 | mulcld 11238 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ Β¬
π = 0) β ((i Β·
(2 Β· Ο)) Β· π) β β) |
58 | 57 | adantr 481 |
. . . . . . . . . . 11
β’ (((π β β€ β§ Β¬
π = 0) β§ π¦ β β) β ((i
Β· (2 Β· Ο)) Β· π) β β) |
59 | | simpr 485 |
. . . . . . . . . . 11
β’ (((π β β€ β§ Β¬
π = 0) β§ π¦ β β) β π¦ β
β) |
60 | 58, 59 | mulcld 11238 |
. . . . . . . . . 10
β’ (((π β β€ β§ Β¬
π = 0) β§ π¦ β β) β (((i
Β· (2 Β· Ο)) Β· π) Β· π¦) β β) |
61 | 60 | efcld 33889 |
. . . . . . . . 9
β’ (((π β β€ β§ Β¬
π = 0) β§ π¦ β β) β
(expβ(((i Β· (2 Β· Ο)) Β· π) Β· π¦)) β β) |
62 | 49, 61 | syldan 591 |
. . . . . . . 8
β’ (((π β β€ β§ Β¬
π = 0) β§ π¦ β β) β
(expβ(((i Β· (2 Β· Ο)) Β· π) Β· π¦)) β β) |
63 | 57 | adantr 481 |
. . . . . . . 8
β’ (((π β β€ β§ Β¬
π = 0) β§ π¦ β β) β ((i
Β· (2 Β· Ο)) Β· π) β β) |
64 | | ine0 11653 |
. . . . . . . . . . . 12
β’ i β
0 |
65 | | 2ne0 12320 |
. . . . . . . . . . . . 13
β’ 2 β
0 |
66 | | pipos 26194 |
. . . . . . . . . . . . . 14
β’ 0 <
Ο |
67 | 25, 66 | gtneii 11330 |
. . . . . . . . . . . . 13
β’ Ο β
0 |
68 | 11, 12, 65, 67 | mulne0i 11861 |
. . . . . . . . . . . 12
β’ (2
Β· Ο) β 0 |
69 | 10, 13, 64, 68 | mulne0i 11861 |
. . . . . . . . . . 11
β’ (i
Β· (2 Β· Ο)) β 0 |
70 | 69 | a1i 11 |
. . . . . . . . . 10
β’ ((π β β€ β§ Β¬
π = 0) β (i Β·
(2 Β· Ο)) β 0) |
71 | | simpr 485 |
. . . . . . . . . . 11
β’ ((π β β€ β§ Β¬
π = 0) β Β¬ π = 0) |
72 | 71 | neqned 2947 |
. . . . . . . . . 10
β’ ((π β β€ β§ Β¬
π = 0) β π β 0) |
73 | 54, 56, 70, 72 | mulne0d 11870 |
. . . . . . . . 9
β’ ((π β β€ β§ Β¬
π = 0) β ((i Β·
(2 Β· Ο)) Β· π) β 0) |
74 | 73 | adantr 481 |
. . . . . . . 8
β’ (((π β β€ β§ Β¬
π = 0) β§ π¦ β β) β ((i
Β· (2 Β· Ο)) Β· π) β 0) |
75 | 62, 63, 74 | divcld 11994 |
. . . . . . 7
β’ (((π β β€ β§ Β¬
π = 0) β§ π¦ β β) β
((expβ(((i Β· (2 Β· Ο)) Β· π) Β· π¦)) / ((i Β· (2 Β· Ο)) Β·
π)) β
β) |
76 | 75 | fmpttd 7116 |
. . . . . 6
β’ ((π β β€ β§ Β¬
π = 0) β (π¦ β β β¦
((expβ(((i Β· (2 Β· Ο)) Β· π) Β· π¦)) / ((i Β· (2 Β· Ο)) Β·
π))):ββΆβ) |
77 | | reelprrecn 11204 |
. . . . . . . . . 10
β’ β
β {β, β} |
78 | 77 | a1i 11 |
. . . . . . . . 9
β’ ((π β β€ β§ Β¬
π = 0) β β
β {β, β}) |
79 | | cnelprrecn 11205 |
. . . . . . . . . 10
β’ β
β {β, β} |
80 | 79 | a1i 11 |
. . . . . . . . 9
β’ ((π β β€ β§ Β¬
π = 0) β β
β {β, β}) |
81 | 63, 49 | mulcld 11238 |
. . . . . . . . 9
β’ (((π β β€ β§ Β¬
π = 0) β§ π¦ β β) β (((i
Β· (2 Β· Ο)) Β· π) Β· π¦) β β) |
82 | | simpr 485 |
. . . . . . . . . . 11
β’ (((π β β€ β§ Β¬
π = 0) β§ π§ β β) β π§ β
β) |
83 | 82 | efcld 33889 |
. . . . . . . . . 10
β’ (((π β β€ β§ Β¬
π = 0) β§ π§ β β) β
(expβπ§) β
β) |
84 | 57 | adantr 481 |
. . . . . . . . . 10
β’ (((π β β€ β§ Β¬
π = 0) β§ π§ β β) β ((i
Β· (2 Β· Ο)) Β· π) β β) |
85 | 73 | adantr 481 |
. . . . . . . . . 10
β’ (((π β β€ β§ Β¬
π = 0) β§ π§ β β) β ((i
Β· (2 Β· Ο)) Β· π) β 0) |
86 | 83, 84, 85 | divcld 11994 |
. . . . . . . . 9
β’ (((π β β€ β§ Β¬
π = 0) β§ π§ β β) β
((expβπ§) / ((i
Β· (2 Β· Ο)) Β· π)) β β) |
87 | 26 | a1i 11 |
. . . . . . . . . . 11
β’ (((π β β€ β§ Β¬
π = 0) β§ π¦ β β) β 1 β
β) |
88 | 78 | dvmptid 25698 |
. . . . . . . . . . 11
β’ ((π β β€ β§ Β¬
π = 0) β (β D
(π¦ β β β¦
π¦)) = (π¦ β β β¦ 1)) |
89 | 78, 49, 87, 88, 57 | dvmptcmul 25705 |
. . . . . . . . . 10
β’ ((π β β€ β§ Β¬
π = 0) β (β D
(π¦ β β β¦
(((i Β· (2 Β· Ο)) Β· π) Β· π¦))) = (π¦ β β β¦ (((i Β· (2
Β· Ο)) Β· π)
Β· 1))) |
90 | 63 | mulridd 11235 |
. . . . . . . . . . 11
β’ (((π β β€ β§ Β¬
π = 0) β§ π¦ β β) β (((i
Β· (2 Β· Ο)) Β· π) Β· 1) = ((i Β· (2 Β·
Ο)) Β· π)) |
91 | 90 | mpteq2dva 5248 |
. . . . . . . . . 10
β’ ((π β β€ β§ Β¬
π = 0) β (π¦ β β β¦ (((i
Β· (2 Β· Ο)) Β· π) Β· 1)) = (π¦ β β β¦ ((i Β· (2
Β· Ο)) Β· π))) |
92 | 89, 91 | eqtrd 2772 |
. . . . . . . . 9
β’ ((π β β€ β§ Β¬
π = 0) β (β D
(π¦ β β β¦
(((i Β· (2 Β· Ο)) Β· π) Β· π¦))) = (π¦ β β β¦ ((i Β· (2
Β· Ο)) Β· π))) |
93 | | dvef 25721 |
. . . . . . . . . . 11
β’ (β
D exp) = exp |
94 | | eff 16029 |
. . . . . . . . . . . . . 14
β’
exp:ββΆβ |
95 | 94 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β β€ β§ Β¬
π = 0) β
exp:ββΆβ) |
96 | 95 | feqmptd 6960 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ Β¬
π = 0) β exp = (π§ β β β¦
(expβπ§))) |
97 | 96 | oveq2d 7427 |
. . . . . . . . . . 11
β’ ((π β β€ β§ Β¬
π = 0) β (β D
exp) = (β D (π§ β
β β¦ (expβπ§)))) |
98 | 93, 97, 96 | 3eqtr3a 2796 |
. . . . . . . . . 10
β’ ((π β β€ β§ Β¬
π = 0) β (β D
(π§ β β β¦
(expβπ§))) = (π§ β β β¦
(expβπ§))) |
99 | 80, 83, 83, 98, 57, 73 | dvmptdivc 25706 |
. . . . . . . . 9
β’ ((π β β€ β§ Β¬
π = 0) β (β D
(π§ β β β¦
((expβπ§) / ((i
Β· (2 Β· Ο)) Β· π)))) = (π§ β β β¦ ((expβπ§) / ((i Β· (2 Β·
Ο)) Β· π)))) |
100 | | fveq2 6891 |
. . . . . . . . . 10
β’ (π§ = (((i Β· (2 Β·
Ο)) Β· π) Β·
π¦) β (expβπ§) = (expβ(((i Β· (2
Β· Ο)) Β· π)
Β· π¦))) |
101 | 100 | oveq1d 7426 |
. . . . . . . . 9
β’ (π§ = (((i Β· (2 Β·
Ο)) Β· π) Β·
π¦) β ((expβπ§) / ((i Β· (2 Β·
Ο)) Β· π)) =
((expβ(((i Β· (2 Β· Ο)) Β· π) Β· π¦)) / ((i Β· (2 Β· Ο)) Β·
π))) |
102 | 78, 80, 81, 63, 86, 86, 92, 99, 101, 101 | dvmptco 25713 |
. . . . . . . 8
β’ ((π β β€ β§ Β¬
π = 0) β (β D
(π¦ β β β¦
((expβ(((i Β· (2 Β· Ο)) Β· π) Β· π¦)) / ((i Β· (2 Β· Ο)) Β·
π)))) = (π¦ β β β¦ (((expβ(((i
Β· (2 Β· Ο)) Β· π) Β· π¦)) / ((i Β· (2 Β· Ο)) Β·
π)) Β· ((i Β·
(2 Β· Ο)) Β· π)))) |
103 | 62, 63, 74 | divcan1d 11995 |
. . . . . . . . 9
β’ (((π β β€ β§ Β¬
π = 0) β§ π¦ β β) β
(((expβ(((i Β· (2 Β· Ο)) Β· π) Β· π¦)) / ((i Β· (2 Β· Ο)) Β·
π)) Β· ((i Β·
(2 Β· Ο)) Β· π)) = (expβ(((i Β· (2 Β·
Ο)) Β· π) Β·
π¦))) |
104 | 103 | mpteq2dva 5248 |
. . . . . . . 8
β’ ((π β β€ β§ Β¬
π = 0) β (π¦ β β β¦
(((expβ(((i Β· (2 Β· Ο)) Β· π) Β· π¦)) / ((i Β· (2 Β· Ο)) Β·
π)) Β· ((i Β·
(2 Β· Ο)) Β· π))) = (π¦ β β β¦ (expβ(((i
Β· (2 Β· Ο)) Β· π) Β· π¦)))) |
105 | 102, 104 | eqtrd 2772 |
. . . . . . 7
β’ ((π β β€ β§ Β¬
π = 0) β (β D
(π¦ β β β¦
((expβ(((i Β· (2 Β· Ο)) Β· π) Β· π¦)) / ((i Β· (2 Β· Ο)) Β·
π)))) = (π¦ β β β¦ (expβ(((i
Β· (2 Β· Ο)) Β· π) Β· π¦)))) |
106 | | efcn 26179 |
. . . . . . . . 9
β’ exp
β (ββcnββ) |
107 | 106 | a1i 11 |
. . . . . . . 8
β’ ((π β β€ β§ Β¬
π = 0) β exp β
(ββcnββ)) |
108 | | resmpt 6037 |
. . . . . . . . . 10
β’ (β
β β β ((π¦
β β β¦ (((i Β· (2 Β· Ο)) Β· π) Β· π¦)) βΎ β) = (π¦ β β β¦ (((i Β· (2
Β· Ο)) Β· π)
Β· π¦))) |
109 | 5, 108 | mp1i 13 |
. . . . . . . . 9
β’ ((π β β€ β§ Β¬
π = 0) β ((π¦ β β β¦ (((i
Β· (2 Β· Ο)) Β· π) Β· π¦)) βΎ β) = (π¦ β β β¦ (((i Β· (2
Β· Ο)) Β· π)
Β· π¦))) |
110 | | eqid 2732 |
. . . . . . . . . . . 12
β’ (π¦ β β β¦ (((i
Β· (2 Β· Ο)) Β· π) Β· π¦)) = (π¦ β β β¦ (((i Β· (2
Β· Ο)) Β· π)
Β· π¦)) |
111 | 110 | mulc1cncf 24645 |
. . . . . . . . . . 11
β’ (((i
Β· (2 Β· Ο)) Β· π) β β β (π¦ β β β¦ (((i Β· (2
Β· Ο)) Β· π)
Β· π¦)) β
(ββcnββ)) |
112 | 57, 111 | syl 17 |
. . . . . . . . . 10
β’ ((π β β€ β§ Β¬
π = 0) β (π¦ β β β¦ (((i
Β· (2 Β· Ο)) Β· π) Β· π¦)) β (ββcnββ)) |
113 | | rescncf 24637 |
. . . . . . . . . . 11
β’ (β
β β β ((π¦
β β β¦ (((i Β· (2 Β· Ο)) Β· π) Β· π¦)) β (ββcnββ) β ((π¦ β β β¦ (((i Β· (2
Β· Ο)) Β· π)
Β· π¦)) βΎ
β) β (ββcnββ))) |
114 | 5, 113 | mp1i 13 |
. . . . . . . . . 10
β’ ((π β β€ β§ Β¬
π = 0) β ((π¦ β β β¦ (((i
Β· (2 Β· Ο)) Β· π) Β· π¦)) β (ββcnββ) β ((π¦ β β β¦ (((i Β· (2
Β· Ο)) Β· π)
Β· π¦)) βΎ
β) β (ββcnββ))) |
115 | 112, 114 | mpd 15 |
. . . . . . . . 9
β’ ((π β β€ β§ Β¬
π = 0) β ((π¦ β β β¦ (((i
Β· (2 Β· Ο)) Β· π) Β· π¦)) βΎ β) β
(ββcnββ)) |
116 | 109, 115 | eqeltrrd 2834 |
. . . . . . . 8
β’ ((π β β€ β§ Β¬
π = 0) β (π¦ β β β¦ (((i
Β· (2 Β· Ο)) Β· π) Β· π¦)) β (ββcnββ)) |
117 | 107, 116 | cncfmpt1f 24654 |
. . . . . . 7
β’ ((π β β€ β§ Β¬
π = 0) β (π¦ β β β¦
(expβ(((i Β· (2 Β· Ο)) Β· π) Β· π¦))) β (ββcnββ)) |
118 | 105, 117 | eqeltrd 2833 |
. . . . . 6
β’ ((π β β€ β§ Β¬
π = 0) β (β D
(π¦ β β β¦
((expβ(((i Β· (2 Β· Ο)) Β· π) Β· π¦)) / ((i Β· (2 Β· Ο)) Β·
π)))) β
(ββcnββ)) |
119 | 44, 45, 46, 47, 76, 118 | ftc2re 33896 |
. . . . 5
β’ ((π β β€ β§ Β¬
π = 0) β
β«(0(,)1)((β D (π¦
β β β¦ ((expβ(((i Β· (2 Β· Ο)) Β·
π) Β· π¦)) / ((i Β· (2 Β·
Ο)) Β· π))))βπ₯) dπ₯ = (((π¦ β β β¦ ((expβ(((i
Β· (2 Β· Ο)) Β· π) Β· π¦)) / ((i Β· (2 Β· Ο)) Β·
π)))β1) β
((π¦ β β β¦
((expβ(((i Β· (2 Β· Ο)) Β· π) Β· π¦)) / ((i Β· (2 Β· Ο)) Β·
π)))β0))) |
120 | 4 | sseli 3978 |
. . . . . . . 8
β’ (π₯ β (0(,)1) β π₯ β
β) |
121 | 105 | adantr 481 |
. . . . . . . . . 10
β’ (((π β β€ β§ Β¬
π = 0) β§ π₯ β β) β (β
D (π¦ β β β¦
((expβ(((i Β· (2 Β· Ο)) Β· π) Β· π¦)) / ((i Β· (2 Β· Ο)) Β·
π)))) = (π¦ β β β¦ (expβ(((i
Β· (2 Β· Ο)) Β· π) Β· π¦)))) |
122 | 121 | fveq1d 6893 |
. . . . . . . . 9
β’ (((π β β€ β§ Β¬
π = 0) β§ π₯ β β) β
((β D (π¦ β
β β¦ ((expβ(((i Β· (2 Β· Ο)) Β· π) Β· π¦)) / ((i Β· (2 Β· Ο)) Β·
π))))βπ₯) = ((π¦ β β β¦ (expβ(((i
Β· (2 Β· Ο)) Β· π) Β· π¦)))βπ₯)) |
123 | | oveq2 7419 |
. . . . . . . . . . . . . 14
β’ (π¦ = π₯ β (((i Β· (2 Β· Ο))
Β· π) Β· π¦) = (((i Β· (2 Β·
Ο)) Β· π) Β·
π₯)) |
124 | 123 | fveq2d 6895 |
. . . . . . . . . . . . 13
β’ (π¦ = π₯ β (expβ(((i Β· (2 Β·
Ο)) Β· π) Β·
π¦)) = (expβ(((i
Β· (2 Β· Ο)) Β· π) Β· π₯))) |
125 | 124 | cbvmptv 5261 |
. . . . . . . . . . . 12
β’ (π¦ β β β¦
(expβ(((i Β· (2 Β· Ο)) Β· π) Β· π¦))) = (π₯ β β β¦ (expβ(((i
Β· (2 Β· Ο)) Β· π) Β· π₯))) |
126 | 125 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β β€ β§ Β¬
π = 0) β (π¦ β β β¦
(expβ(((i Β· (2 Β· Ο)) Β· π) Β· π¦))) = (π₯ β β β¦ (expβ(((i
Β· (2 Β· Ο)) Β· π) Β· π₯)))) |
127 | 57 | adantr 481 |
. . . . . . . . . . . . 13
β’ (((π β β€ β§ Β¬
π = 0) β§ π₯ β β) β ((i
Β· (2 Β· Ο)) Β· π) β β) |
128 | 48 | sselda 3982 |
. . . . . . . . . . . . 13
β’ (((π β β€ β§ Β¬
π = 0) β§ π₯ β β) β π₯ β
β) |
129 | 127, 128 | mulcld 11238 |
. . . . . . . . . . . 12
β’ (((π β β€ β§ Β¬
π = 0) β§ π₯ β β) β (((i
Β· (2 Β· Ο)) Β· π) Β· π₯) β β) |
130 | 129 | efcld 33889 |
. . . . . . . . . . 11
β’ (((π β β€ β§ Β¬
π = 0) β§ π₯ β β) β
(expβ(((i Β· (2 Β· Ο)) Β· π) Β· π₯)) β β) |
131 | 126, 130 | fvmpt2d 7011 |
. . . . . . . . . 10
β’ (((π β β€ β§ Β¬
π = 0) β§ π₯ β β) β ((π¦ β β β¦
(expβ(((i Β· (2 Β· Ο)) Β· π) Β· π¦)))βπ₯) = (expβ(((i Β· (2 Β·
Ο)) Β· π) Β·
π₯))) |
132 | 14 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β β€ β§ Β¬
π = 0) β§ π₯ β β) β (i
Β· (2 Β· Ο)) β β) |
133 | 56 | adantr 481 |
. . . . . . . . . . . 12
β’ (((π β β€ β§ Β¬
π = 0) β§ π₯ β β) β π β
β) |
134 | 132, 133,
128 | mulassd 11241 |
. . . . . . . . . . 11
β’ (((π β β€ β§ Β¬
π = 0) β§ π₯ β β) β (((i
Β· (2 Β· Ο)) Β· π) Β· π₯) = ((i Β· (2 Β· Ο)) Β·
(π Β· π₯))) |
135 | 134 | fveq2d 6895 |
. . . . . . . . . 10
β’ (((π β β€ β§ Β¬
π = 0) β§ π₯ β β) β
(expβ(((i Β· (2 Β· Ο)) Β· π) Β· π₯)) = (expβ((i Β· (2 Β·
Ο)) Β· (π Β·
π₯)))) |
136 | 131, 135 | eqtrd 2772 |
. . . . . . . . 9
β’ (((π β β€ β§ Β¬
π = 0) β§ π₯ β β) β ((π¦ β β β¦
(expβ(((i Β· (2 Β· Ο)) Β· π) Β· π¦)))βπ₯) = (expβ((i Β· (2 Β·
Ο)) Β· (π Β·
π₯)))) |
137 | 122, 136 | eqtrd 2772 |
. . . . . . . 8
β’ (((π β β€ β§ Β¬
π = 0) β§ π₯ β β) β
((β D (π¦ β
β β¦ ((expβ(((i Β· (2 Β· Ο)) Β· π) Β· π¦)) / ((i Β· (2 Β· Ο)) Β·
π))))βπ₯) = (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π₯)))) |
138 | 120, 137 | sylan2 593 |
. . . . . . 7
β’ (((π β β€ β§ Β¬
π = 0) β§ π₯ β (0(,)1)) β
((β D (π¦ β
β β¦ ((expβ(((i Β· (2 Β· Ο)) Β· π) Β· π¦)) / ((i Β· (2 Β· Ο)) Β·
π))))βπ₯) = (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π₯)))) |
139 | 138 | ralrimiva 3146 |
. . . . . 6
β’ ((π β β€ β§ Β¬
π = 0) β βπ₯ β (0(,)1)((β D
(π¦ β β β¦
((expβ(((i Β· (2 Β· Ο)) Β· π) Β· π¦)) / ((i Β· (2 Β· Ο)) Β·
π))))βπ₯) = (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π₯)))) |
140 | | itgeq2 25519 |
. . . . . 6
β’
(βπ₯ β
(0(,)1)((β D (π¦
β β β¦ ((expβ(((i Β· (2 Β· Ο)) Β·
π) Β· π¦)) / ((i Β· (2 Β·
Ο)) Β· π))))βπ₯) = (expβ((i Β· (2 Β·
Ο)) Β· (π Β·
π₯))) β
β«(0(,)1)((β D (π¦
β β β¦ ((expβ(((i Β· (2 Β· Ο)) Β·
π) Β· π¦)) / ((i Β· (2 Β·
Ο)) Β· π))))βπ₯) dπ₯ = β«(0(,)1)(expβ((i Β· (2
Β· Ο)) Β· (π
Β· π₯))) dπ₯) |
141 | 139, 140 | syl 17 |
. . . . 5
β’ ((π β β€ β§ Β¬
π = 0) β
β«(0(,)1)((β D (π¦
β β β¦ ((expβ(((i Β· (2 Β· Ο)) Β·
π) Β· π¦)) / ((i Β· (2 Β·
Ο)) Β· π))))βπ₯) dπ₯ = β«(0(,)1)(expβ((i Β· (2
Β· Ο)) Β· (π
Β· π₯))) dπ₯) |
142 | | eqidd 2733 |
. . . . . . . . 9
β’ ((π β β€ β§ Β¬
π = 0) β (π¦ β β β¦
((expβ(((i Β· (2 Β· Ο)) Β· π) Β· π¦)) / ((i Β· (2 Β· Ο)) Β·
π))) = (π¦ β β β¦ ((expβ(((i
Β· (2 Β· Ο)) Β· π) Β· π¦)) / ((i Β· (2 Β· Ο)) Β·
π)))) |
143 | | simpr 485 |
. . . . . . . . . . . 12
β’ (((π β β€ β§ Β¬
π = 0) β§ π¦ = 1) β π¦ = 1) |
144 | 143 | oveq2d 7427 |
. . . . . . . . . . 11
β’ (((π β β€ β§ Β¬
π = 0) β§ π¦ = 1) β (((i Β· (2
Β· Ο)) Β· π)
Β· π¦) = (((i Β·
(2 Β· Ο)) Β· π) Β· 1)) |
145 | 144 | fveq2d 6895 |
. . . . . . . . . 10
β’ (((π β β€ β§ Β¬
π = 0) β§ π¦ = 1) β (expβ(((i
Β· (2 Β· Ο)) Β· π) Β· π¦)) = (expβ(((i Β· (2 Β·
Ο)) Β· π) Β·
1))) |
146 | 145 | oveq1d 7426 |
. . . . . . . . 9
β’ (((π β β€ β§ Β¬
π = 0) β§ π¦ = 1) β ((expβ(((i
Β· (2 Β· Ο)) Β· π) Β· π¦)) / ((i Β· (2 Β· Ο)) Β·
π)) = ((expβ(((i
Β· (2 Β· Ο)) Β· π) Β· 1)) / ((i Β· (2 Β·
Ο)) Β· π))) |
147 | 29 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ Β¬
π = 0) β 1 β
β) |
148 | 57, 147 | mulcld 11238 |
. . . . . . . . . . 11
β’ ((π β β€ β§ Β¬
π = 0) β (((i Β·
(2 Β· Ο)) Β· π) Β· 1) β
β) |
149 | 148 | efcld 33889 |
. . . . . . . . . 10
β’ ((π β β€ β§ Β¬
π = 0) β
(expβ(((i Β· (2 Β· Ο)) Β· π) Β· 1)) β
β) |
150 | 149, 57, 73 | divcld 11994 |
. . . . . . . . 9
β’ ((π β β€ β§ Β¬
π = 0) β
((expβ(((i Β· (2 Β· Ο)) Β· π) Β· 1)) / ((i Β· (2 Β·
Ο)) Β· π)) β
β) |
151 | 142, 146,
46, 150 | fvmptd 7005 |
. . . . . . . 8
β’ ((π β β€ β§ Β¬
π = 0) β ((π¦ β β β¦
((expβ(((i Β· (2 Β· Ο)) Β· π) Β· π¦)) / ((i Β· (2 Β· Ο)) Β·
π)))β1) =
((expβ(((i Β· (2 Β· Ο)) Β· π) Β· 1)) / ((i Β· (2 Β·
Ο)) Β· π))) |
152 | 57 | mulridd 11235 |
. . . . . . . . . . 11
β’ ((π β β€ β§ Β¬
π = 0) β (((i Β·
(2 Β· Ο)) Β· π) Β· 1) = ((i Β· (2 Β·
Ο)) Β· π)) |
153 | 152 | fveq2d 6895 |
. . . . . . . . . 10
β’ ((π β β€ β§ Β¬
π = 0) β
(expβ(((i Β· (2 Β· Ο)) Β· π) Β· 1)) = (expβ((i Β· (2
Β· Ο)) Β· π))) |
154 | | ef2kpi 26212 |
. . . . . . . . . . 11
β’ (π β β€ β
(expβ((i Β· (2 Β· Ο)) Β· π)) = 1) |
155 | 55, 154 | syl 17 |
. . . . . . . . . 10
β’ ((π β β€ β§ Β¬
π = 0) β
(expβ((i Β· (2 Β· Ο)) Β· π)) = 1) |
156 | 153, 155 | eqtrd 2772 |
. . . . . . . . 9
β’ ((π β β€ β§ Β¬
π = 0) β
(expβ(((i Β· (2 Β· Ο)) Β· π) Β· 1)) = 1) |
157 | 156 | oveq1d 7426 |
. . . . . . . 8
β’ ((π β β€ β§ Β¬
π = 0) β
((expβ(((i Β· (2 Β· Ο)) Β· π) Β· 1)) / ((i Β· (2 Β·
Ο)) Β· π)) = (1 /
((i Β· (2 Β· Ο)) Β· π))) |
158 | 151, 157 | eqtrd 2772 |
. . . . . . 7
β’ ((π β β€ β§ Β¬
π = 0) β ((π¦ β β β¦
((expβ(((i Β· (2 Β· Ο)) Β· π) Β· π¦)) / ((i Β· (2 Β· Ο)) Β·
π)))β1) = (1 / ((i
Β· (2 Β· Ο)) Β· π))) |
159 | | simpr 485 |
. . . . . . . . . . . 12
β’ (((π β β€ β§ Β¬
π = 0) β§ π¦ = 0) β π¦ = 0) |
160 | 159 | oveq2d 7427 |
. . . . . . . . . . 11
β’ (((π β β€ β§ Β¬
π = 0) β§ π¦ = 0) β (((i Β· (2
Β· Ο)) Β· π)
Β· π¦) = (((i Β·
(2 Β· Ο)) Β· π) Β· 0)) |
161 | 160 | fveq2d 6895 |
. . . . . . . . . 10
β’ (((π β β€ β§ Β¬
π = 0) β§ π¦ = 0) β (expβ(((i
Β· (2 Β· Ο)) Β· π) Β· π¦)) = (expβ(((i Β· (2 Β·
Ο)) Β· π) Β·
0))) |
162 | 161 | oveq1d 7426 |
. . . . . . . . 9
β’ (((π β β€ β§ Β¬
π = 0) β§ π¦ = 0) β ((expβ(((i
Β· (2 Β· Ο)) Β· π) Β· π¦)) / ((i Β· (2 Β· Ο)) Β·
π)) = ((expβ(((i
Β· (2 Β· Ο)) Β· π) Β· 0)) / ((i Β· (2 Β·
Ο)) Β· π))) |
163 | 5, 45 | sselid 3980 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ Β¬
π = 0) β 0 β
β) |
164 | 57, 163 | mulcld 11238 |
. . . . . . . . . . 11
β’ ((π β β€ β§ Β¬
π = 0) β (((i Β·
(2 Β· Ο)) Β· π) Β· 0) β
β) |
165 | 164 | efcld 33889 |
. . . . . . . . . 10
β’ ((π β β€ β§ Β¬
π = 0) β
(expβ(((i Β· (2 Β· Ο)) Β· π) Β· 0)) β
β) |
166 | 165, 57, 73 | divcld 11994 |
. . . . . . . . 9
β’ ((π β β€ β§ Β¬
π = 0) β
((expβ(((i Β· (2 Β· Ο)) Β· π) Β· 0)) / ((i Β· (2 Β·
Ο)) Β· π)) β
β) |
167 | 142, 162,
45, 166 | fvmptd 7005 |
. . . . . . . 8
β’ ((π β β€ β§ Β¬
π = 0) β ((π¦ β β β¦
((expβ(((i Β· (2 Β· Ο)) Β· π) Β· π¦)) / ((i Β· (2 Β· Ο)) Β·
π)))β0) =
((expβ(((i Β· (2 Β· Ο)) Β· π) Β· 0)) / ((i Β· (2 Β·
Ο)) Β· π))) |
168 | 57 | mul01d 11417 |
. . . . . . . . . . 11
β’ ((π β β€ β§ Β¬
π = 0) β (((i Β·
(2 Β· Ο)) Β· π) Β· 0) = 0) |
169 | 168 | fveq2d 6895 |
. . . . . . . . . 10
β’ ((π β β€ β§ Β¬
π = 0) β
(expβ(((i Β· (2 Β· Ο)) Β· π) Β· 0)) =
(expβ0)) |
170 | 169, 18 | eqtrdi 2788 |
. . . . . . . . 9
β’ ((π β β€ β§ Β¬
π = 0) β
(expβ(((i Β· (2 Β· Ο)) Β· π) Β· 0)) = 1) |
171 | 170 | oveq1d 7426 |
. . . . . . . 8
β’ ((π β β€ β§ Β¬
π = 0) β
((expβ(((i Β· (2 Β· Ο)) Β· π) Β· 0)) / ((i Β· (2 Β·
Ο)) Β· π)) = (1 /
((i Β· (2 Β· Ο)) Β· π))) |
172 | 167, 171 | eqtrd 2772 |
. . . . . . 7
β’ ((π β β€ β§ Β¬
π = 0) β ((π¦ β β β¦
((expβ(((i Β· (2 Β· Ο)) Β· π) Β· π¦)) / ((i Β· (2 Β· Ο)) Β·
π)))β0) = (1 / ((i
Β· (2 Β· Ο)) Β· π))) |
173 | 158, 172 | oveq12d 7429 |
. . . . . 6
β’ ((π β β€ β§ Β¬
π = 0) β (((π¦ β β β¦
((expβ(((i Β· (2 Β· Ο)) Β· π) Β· π¦)) / ((i Β· (2 Β· Ο)) Β·
π)))β1) β
((π¦ β β β¦
((expβ(((i Β· (2 Β· Ο)) Β· π) Β· π¦)) / ((i Β· (2 Β· Ο)) Β·
π)))β0)) = ((1 / ((i
Β· (2 Β· Ο)) Β· π)) β (1 / ((i Β· (2 Β·
Ο)) Β· π)))) |
174 | 157, 150 | eqeltrrd 2834 |
. . . . . . 7
β’ ((π β β€ β§ Β¬
π = 0) β (1 / ((i
Β· (2 Β· Ο)) Β· π)) β β) |
175 | 174 | subidd 11563 |
. . . . . 6
β’ ((π β β€ β§ Β¬
π = 0) β ((1 / ((i
Β· (2 Β· Ο)) Β· π)) β (1 / ((i Β· (2 Β·
Ο)) Β· π))) =
0) |
176 | 173, 175 | eqtrd 2772 |
. . . . 5
β’ ((π β β€ β§ Β¬
π = 0) β (((π¦ β β β¦
((expβ(((i Β· (2 Β· Ο)) Β· π) Β· π¦)) / ((i Β· (2 Β· Ο)) Β·
π)))β1) β
((π¦ β β β¦
((expβ(((i Β· (2 Β· Ο)) Β· π) Β· π¦)) / ((i Β· (2 Β· Ο)) Β·
π)))β0)) =
0) |
177 | 119, 141,
176 | 3eqtr3d 2780 |
. . . 4
β’ ((π β β€ β§ Β¬
π = 0) β
β«(0(,)1)(expβ((i Β· (2 Β· Ο)) Β· (π Β· π₯))) dπ₯ = 0) |
178 | 177 | eqcomd 2738 |
. . 3
β’ ((π β β€ β§ Β¬
π = 0) β 0 =
β«(0(,)1)(expβ((i Β· (2 Β· Ο)) Β· (π Β· π₯))) dπ₯) |
179 | 42, 178 | ifeqda 4564 |
. 2
β’ (π β β€ β if(π = 0, 1, 0) =
β«(0(,)1)(expβ((i Β· (2 Β· Ο)) Β· (π Β· π₯))) dπ₯) |
180 | 179 | eqcomd 2738 |
1
β’ (π β β€ β
β«(0(,)1)(expβ((i Β· (2 Β· Ο)) Β· (π Β· π₯))) dπ₯ = if(π = 0, 1, 0)) |