Step | Hyp | Ref
| Expression |
1 | | mbfi1fseq.1 |
. . . 4
β’ (π β πΉ β MblFn) |
2 | | mbfi1fseq.2 |
. . . 4
β’ (π β πΉ:ββΆ(0[,)+β)) |
3 | | mbfi1fseq.3 |
. . . 4
β’ π½ = (π β β, π¦ β β β¦
((ββ((πΉβπ¦) Β· (2βπ))) / (2βπ))) |
4 | | mbfi1fseq.4 |
. . . 4
β’ πΊ = (π β β β¦ (π₯ β β β¦ if(π₯ β (-π[,]π), if((ππ½π₯) β€ π, (ππ½π₯), π), 0))) |
5 | 1, 2, 3, 4 | mbfi1fseqlem2 25104 |
. . 3
β’ (π΄ β β β (πΊβπ΄) = (π₯ β β β¦ if(π₯ β (-π΄[,]π΄), if((π΄π½π₯) β€ π΄, (π΄π½π₯), π΄), 0))) |
6 | 5 | adantl 483 |
. 2
β’ ((π β§ π΄ β β) β (πΊβπ΄) = (π₯ β β β¦ if(π₯ β (-π΄[,]π΄), if((π΄π½π₯) β€ π΄, (π΄π½π₯), π΄), 0))) |
7 | | rge0ssre 13382 |
. . . . . . . . . . . . . . . . . 18
β’
(0[,)+β) β β |
8 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ π¦ β β) β π¦ β
β) |
9 | | ffvelcdm 7036 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉ:ββΆ(0[,)+β)
β§ π¦ β β)
β (πΉβπ¦) β
(0[,)+β)) |
10 | 2, 8, 9 | syl2an 597 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π β β β§ π¦ β β)) β (πΉβπ¦) β (0[,)+β)) |
11 | 7, 10 | sselid 3946 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β β β§ π¦ β β)) β (πΉβπ¦) β β) |
12 | | 2nn 12234 |
. . . . . . . . . . . . . . . . . . . 20
β’ 2 β
β |
13 | | nnnn0 12428 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β π β
β0) |
14 | | nnexpcl 13989 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((2
β β β§ π
β β0) β (2βπ) β β) |
15 | 12, 13, 14 | sylancr 588 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β
(2βπ) β
β) |
16 | 15 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π β β β§ π¦ β β)) β (2βπ) β
β) |
17 | 16 | nnred 12176 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β β β§ π¦ β β)) β (2βπ) β
β) |
18 | 11, 17 | remulcld 11193 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β β β§ π¦ β β)) β ((πΉβπ¦) Β· (2βπ)) β β) |
19 | | reflcl 13710 |
. . . . . . . . . . . . . . . 16
β’ (((πΉβπ¦) Β· (2βπ)) β β β
(ββ((πΉβπ¦) Β· (2βπ))) β β) |
20 | 18, 19 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β β β§ π¦ β β)) β
(ββ((πΉβπ¦) Β· (2βπ))) β β) |
21 | 20, 16 | nndivred 12215 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β β§ π¦ β β)) β
((ββ((πΉβπ¦) Β· (2βπ))) / (2βπ)) β β) |
22 | 21 | ralrimivva 3194 |
. . . . . . . . . . . . 13
β’ (π β βπ β β βπ¦ β β ((ββ((πΉβπ¦) Β· (2βπ))) / (2βπ)) β β) |
23 | 3 | fmpo 8004 |
. . . . . . . . . . . . 13
β’
(βπ β
β βπ¦ β
β ((ββ((πΉβπ¦) Β· (2βπ))) / (2βπ)) β β β π½:(β Γ
β)βΆβ) |
24 | 22, 23 | sylib 217 |
. . . . . . . . . . . 12
β’ (π β π½:(β Γ
β)βΆβ) |
25 | | fovcdm 7528 |
. . . . . . . . . . . 12
β’ ((π½:(β Γ
β)βΆβ β§ π΄ β β β§ π₯ β β) β (π΄π½π₯) β β) |
26 | 24, 25 | syl3an1 1164 |
. . . . . . . . . . 11
β’ ((π β§ π΄ β β β§ π₯ β β) β (π΄π½π₯) β β) |
27 | 26 | 3expa 1119 |
. . . . . . . . . 10
β’ (((π β§ π΄ β β) β§ π₯ β β) β (π΄π½π₯) β β) |
28 | | nnre 12168 |
. . . . . . . . . . 11
β’ (π΄ β β β π΄ β
β) |
29 | 28 | ad2antlr 726 |
. . . . . . . . . 10
β’ (((π β§ π΄ β β) β§ π₯ β β) β π΄ β β) |
30 | | nnnn0 12428 |
. . . . . . . . . . . . 13
β’ (π΄ β β β π΄ β
β0) |
31 | | nnexpcl 13989 |
. . . . . . . . . . . . 13
β’ ((2
β β β§ π΄
β β0) β (2βπ΄) β β) |
32 | 12, 30, 31 | sylancr 588 |
. . . . . . . . . . . 12
β’ (π΄ β β β
(2βπ΄) β
β) |
33 | 32 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π β§ π΄ β β) β§ π₯ β β) β (2βπ΄) β
β) |
34 | | nnre 12168 |
. . . . . . . . . . . 12
β’
((2βπ΄) β
β β (2βπ΄)
β β) |
35 | | nngt0 12192 |
. . . . . . . . . . . 12
β’
((2βπ΄) β
β β 0 < (2βπ΄)) |
36 | 34, 35 | jca 513 |
. . . . . . . . . . 11
β’
((2βπ΄) β
β β ((2βπ΄)
β β β§ 0 < (2βπ΄))) |
37 | 33, 36 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π΄ β β) β§ π₯ β β) β ((2βπ΄) β β β§ 0 <
(2βπ΄))) |
38 | | lemul1 12015 |
. . . . . . . . . 10
β’ (((π΄π½π₯) β β β§ π΄ β β β§ ((2βπ΄) β β β§ 0 <
(2βπ΄))) β ((π΄π½π₯) β€ π΄ β ((π΄π½π₯) Β· (2βπ΄)) β€ (π΄ Β· (2βπ΄)))) |
39 | 27, 29, 37, 38 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β§ π΄ β β) β§ π₯ β β) β ((π΄π½π₯) β€ π΄ β ((π΄π½π₯) Β· (2βπ΄)) β€ (π΄ Β· (2βπ΄)))) |
40 | 39 | biimpa 478 |
. . . . . . . 8
β’ ((((π β§ π΄ β β) β§ π₯ β β) β§ (π΄π½π₯) β€ π΄) β ((π΄π½π₯) Β· (2βπ΄)) β€ (π΄ Β· (2βπ΄))) |
41 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π = π΄ β§ π¦ = π₯) β π¦ = π₯) |
42 | 41 | fveq2d 6850 |
. . . . . . . . . . . . . . . . . 18
β’ ((π = π΄ β§ π¦ = π₯) β (πΉβπ¦) = (πΉβπ₯)) |
43 | | simpl 484 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π = π΄ β§ π¦ = π₯) β π = π΄) |
44 | 43 | oveq2d 7377 |
. . . . . . . . . . . . . . . . . 18
β’ ((π = π΄ β§ π¦ = π₯) β (2βπ) = (2βπ΄)) |
45 | 42, 44 | oveq12d 7379 |
. . . . . . . . . . . . . . . . 17
β’ ((π = π΄ β§ π¦ = π₯) β ((πΉβπ¦) Β· (2βπ)) = ((πΉβπ₯) Β· (2βπ΄))) |
46 | 45 | fveq2d 6850 |
. . . . . . . . . . . . . . . 16
β’ ((π = π΄ β§ π¦ = π₯) β (ββ((πΉβπ¦) Β· (2βπ))) = (ββ((πΉβπ₯) Β· (2βπ΄)))) |
47 | 46, 44 | oveq12d 7379 |
. . . . . . . . . . . . . . 15
β’ ((π = π΄ β§ π¦ = π₯) β ((ββ((πΉβπ¦) Β· (2βπ))) / (2βπ)) = ((ββ((πΉβπ₯) Β· (2βπ΄))) / (2βπ΄))) |
48 | | ovex 7394 |
. . . . . . . . . . . . . . 15
β’
((ββ((πΉβπ₯) Β· (2βπ΄))) / (2βπ΄)) β V |
49 | 47, 3, 48 | ovmpoa 7514 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§ π₯ β β) β (π΄π½π₯) = ((ββ((πΉβπ₯) Β· (2βπ΄))) / (2βπ΄))) |
50 | 49 | ad4ant23 752 |
. . . . . . . . . . . . 13
β’ ((((π β§ π΄ β β) β§ π₯ β β) β§ (π΄π½π₯) β€ π΄) β (π΄π½π₯) = ((ββ((πΉβπ₯) Β· (2βπ΄))) / (2βπ΄))) |
51 | 50 | oveq1d 7376 |
. . . . . . . . . . . 12
β’ ((((π β§ π΄ β β) β§ π₯ β β) β§ (π΄π½π₯) β€ π΄) β ((π΄π½π₯) Β· (2βπ΄)) = (((ββ((πΉβπ₯) Β· (2βπ΄))) / (2βπ΄)) Β· (2βπ΄))) |
52 | 2 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π΄ β β) β πΉ:ββΆ(0[,)+β)) |
53 | 52 | ffvelcdmda 7039 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π΄ β β) β§ π₯ β β) β (πΉβπ₯) β (0[,)+β)) |
54 | | elrege0 13380 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉβπ₯) β (0[,)+β) β ((πΉβπ₯) β β β§ 0 β€ (πΉβπ₯))) |
55 | 53, 54 | sylib 217 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π΄ β β) β§ π₯ β β) β ((πΉβπ₯) β β β§ 0 β€ (πΉβπ₯))) |
56 | 55 | simpld 496 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π΄ β β) β§ π₯ β β) β (πΉβπ₯) β β) |
57 | 33 | nnred 12176 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π΄ β β) β§ π₯ β β) β (2βπ΄) β
β) |
58 | 56, 57 | remulcld 11193 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π΄ β β) β§ π₯ β β) β ((πΉβπ₯) Β· (2βπ΄)) β β) |
59 | 33 | nnnn0d 12481 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π΄ β β) β§ π₯ β β) β (2βπ΄) β
β0) |
60 | 59 | nn0ge0d 12484 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π΄ β β) β§ π₯ β β) β 0 β€ (2βπ΄)) |
61 | | mulge0 11681 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΉβπ₯) β β β§ 0 β€ (πΉβπ₯)) β§ ((2βπ΄) β β β§ 0 β€ (2βπ΄))) β 0 β€ ((πΉβπ₯) Β· (2βπ΄))) |
62 | 55, 57, 60, 61 | syl12anc 836 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π΄ β β) β§ π₯ β β) β 0 β€ ((πΉβπ₯) Β· (2βπ΄))) |
63 | | flge0nn0 13734 |
. . . . . . . . . . . . . . . 16
β’ ((((πΉβπ₯) Β· (2βπ΄)) β β β§ 0 β€ ((πΉβπ₯) Β· (2βπ΄))) β (ββ((πΉβπ₯) Β· (2βπ΄))) β
β0) |
64 | 58, 62, 63 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π΄ β β) β§ π₯ β β) β
(ββ((πΉβπ₯) Β· (2βπ΄))) β
β0) |
65 | 64 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π΄ β β) β§ π₯ β β) β§ (π΄π½π₯) β€ π΄) β (ββ((πΉβπ₯) Β· (2βπ΄))) β
β0) |
66 | 65 | nn0cnd 12483 |
. . . . . . . . . . . . 13
β’ ((((π β§ π΄ β β) β§ π₯ β β) β§ (π΄π½π₯) β€ π΄) β (ββ((πΉβπ₯) Β· (2βπ΄))) β β) |
67 | 33 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π΄ β β) β§ π₯ β β) β§ (π΄π½π₯) β€ π΄) β (2βπ΄) β β) |
68 | 67 | nncnd 12177 |
. . . . . . . . . . . . 13
β’ ((((π β§ π΄ β β) β§ π₯ β β) β§ (π΄π½π₯) β€ π΄) β (2βπ΄) β β) |
69 | 67 | nnne0d 12211 |
. . . . . . . . . . . . 13
β’ ((((π β§ π΄ β β) β§ π₯ β β) β§ (π΄π½π₯) β€ π΄) β (2βπ΄) β 0) |
70 | 66, 68, 69 | divcan1d 11940 |
. . . . . . . . . . . 12
β’ ((((π β§ π΄ β β) β§ π₯ β β) β§ (π΄π½π₯) β€ π΄) β (((ββ((πΉβπ₯) Β· (2βπ΄))) / (2βπ΄)) Β· (2βπ΄)) = (ββ((πΉβπ₯) Β· (2βπ΄)))) |
71 | 51, 70 | eqtrd 2773 |
. . . . . . . . . . 11
β’ ((((π β§ π΄ β β) β§ π₯ β β) β§ (π΄π½π₯) β€ π΄) β ((π΄π½π₯) Β· (2βπ΄)) = (ββ((πΉβπ₯) Β· (2βπ΄)))) |
72 | 71, 65 | eqeltrd 2834 |
. . . . . . . . . 10
β’ ((((π β§ π΄ β β) β§ π₯ β β) β§ (π΄π½π₯) β€ π΄) β ((π΄π½π₯) Β· (2βπ΄)) β
β0) |
73 | | nn0uz 12813 |
. . . . . . . . . 10
β’
β0 = (β€β₯β0) |
74 | 72, 73 | eleqtrdi 2844 |
. . . . . . . . 9
β’ ((((π β§ π΄ β β) β§ π₯ β β) β§ (π΄π½π₯) β€ π΄) β ((π΄π½π₯) Β· (2βπ΄)) β
(β€β₯β0)) |
75 | | nnmulcl 12185 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§
(2βπ΄) β β)
β (π΄ Β·
(2βπ΄)) β
β) |
76 | 32, 75 | mpdan 686 |
. . . . . . . . . . . 12
β’ (π΄ β β β (π΄ Β· (2βπ΄)) β
β) |
77 | 76 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π β§ π΄ β β) β§ π₯ β β) β (π΄ Β· (2βπ΄)) β β) |
78 | 77 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ π΄ β β) β§ π₯ β β) β§ (π΄π½π₯) β€ π΄) β (π΄ Β· (2βπ΄)) β β) |
79 | 78 | nnzd 12534 |
. . . . . . . . 9
β’ ((((π β§ π΄ β β) β§ π₯ β β) β§ (π΄π½π₯) β€ π΄) β (π΄ Β· (2βπ΄)) β β€) |
80 | | elfz5 13442 |
. . . . . . . . 9
β’ ((((π΄π½π₯) Β· (2βπ΄)) β (β€β₯β0)
β§ (π΄ Β·
(2βπ΄)) β β€)
β (((π΄π½π₯) Β· (2βπ΄)) β (0...(π΄ Β· (2βπ΄))) β ((π΄π½π₯) Β· (2βπ΄)) β€ (π΄ Β· (2βπ΄)))) |
81 | 74, 79, 80 | syl2anc 585 |
. . . . . . . 8
β’ ((((π β§ π΄ β β) β§ π₯ β β) β§ (π΄π½π₯) β€ π΄) β (((π΄π½π₯) Β· (2βπ΄)) β (0...(π΄ Β· (2βπ΄))) β ((π΄π½π₯) Β· (2βπ΄)) β€ (π΄ Β· (2βπ΄)))) |
82 | 40, 81 | mpbird 257 |
. . . . . . 7
β’ ((((π β§ π΄ β β) β§ π₯ β β) β§ (π΄π½π₯) β€ π΄) β ((π΄π½π₯) Β· (2βπ΄)) β (0...(π΄ Β· (2βπ΄)))) |
83 | | oveq1 7368 |
. . . . . . . 8
β’ (π = ((π΄π½π₯) Β· (2βπ΄)) β (π / (2βπ΄)) = (((π΄π½π₯) Β· (2βπ΄)) / (2βπ΄))) |
84 | | eqid 2733 |
. . . . . . . 8
β’ (π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄))) = (π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄))) |
85 | | ovex 7394 |
. . . . . . . 8
β’ (((π΄π½π₯) Β· (2βπ΄)) / (2βπ΄)) β V |
86 | 83, 84, 85 | fvmpt 6952 |
. . . . . . 7
β’ (((π΄π½π₯) Β· (2βπ΄)) β (0...(π΄ Β· (2βπ΄))) β ((π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))β((π΄π½π₯) Β· (2βπ΄))) = (((π΄π½π₯) Β· (2βπ΄)) / (2βπ΄))) |
87 | 82, 86 | syl 17 |
. . . . . 6
β’ ((((π β§ π΄ β β) β§ π₯ β β) β§ (π΄π½π₯) β€ π΄) β ((π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))β((π΄π½π₯) Β· (2βπ΄))) = (((π΄π½π₯) Β· (2βπ΄)) / (2βπ΄))) |
88 | 27 | adantr 482 |
. . . . . . . 8
β’ ((((π β§ π΄ β β) β§ π₯ β β) β§ (π΄π½π₯) β€ π΄) β (π΄π½π₯) β β) |
89 | 88 | recnd 11191 |
. . . . . . 7
β’ ((((π β§ π΄ β β) β§ π₯ β β) β§ (π΄π½π₯) β€ π΄) β (π΄π½π₯) β β) |
90 | 89, 68, 69 | divcan4d 11945 |
. . . . . 6
β’ ((((π β§ π΄ β β) β§ π₯ β β) β§ (π΄π½π₯) β€ π΄) β (((π΄π½π₯) Β· (2βπ΄)) / (2βπ΄)) = (π΄π½π₯)) |
91 | 87, 90 | eqtrd 2773 |
. . . . 5
β’ ((((π β§ π΄ β β) β§ π₯ β β) β§ (π΄π½π₯) β€ π΄) β ((π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))β((π΄π½π₯) Β· (2βπ΄))) = (π΄π½π₯)) |
92 | | elfznn0 13543 |
. . . . . . . . . . . 12
β’ (π β (0...(π΄ Β· (2βπ΄))) β π β β0) |
93 | 92 | nn0red 12482 |
. . . . . . . . . . 11
β’ (π β (0...(π΄ Β· (2βπ΄))) β π β β) |
94 | 32 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π΄ β β) β (2βπ΄) β
β) |
95 | | nndivre 12202 |
. . . . . . . . . . 11
β’ ((π β β β§
(2βπ΄) β β)
β (π / (2βπ΄)) β
β) |
96 | 93, 94, 95 | syl2anr 598 |
. . . . . . . . . 10
β’ (((π β§ π΄ β β) β§ π β (0...(π΄ Β· (2βπ΄)))) β (π / (2βπ΄)) β β) |
97 | 96 | fmpttd 7067 |
. . . . . . . . 9
β’ ((π β§ π΄ β β) β (π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄))):(0...(π΄ Β· (2βπ΄)))βΆβ) |
98 | 97 | ffnd 6673 |
. . . . . . . 8
β’ ((π β§ π΄ β β) β (π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄))) Fn (0...(π΄ Β· (2βπ΄)))) |
99 | 98 | adantr 482 |
. . . . . . 7
β’ (((π β§ π΄ β β) β§ π₯ β β) β (π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄))) Fn (0...(π΄ Β· (2βπ΄)))) |
100 | 99 | adantr 482 |
. . . . . 6
β’ ((((π β§ π΄ β β) β§ π₯ β β) β§ (π΄π½π₯) β€ π΄) β (π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄))) Fn (0...(π΄ Β· (2βπ΄)))) |
101 | | fnfvelrn 7035 |
. . . . . 6
β’ (((π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄))) Fn (0...(π΄ Β· (2βπ΄))) β§ ((π΄π½π₯) Β· (2βπ΄)) β (0...(π΄ Β· (2βπ΄)))) β ((π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))β((π΄π½π₯) Β· (2βπ΄))) β ran (π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))) |
102 | 100, 82, 101 | syl2anc 585 |
. . . . 5
β’ ((((π β§ π΄ β β) β§ π₯ β β) β§ (π΄π½π₯) β€ π΄) β ((π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))β((π΄π½π₯) Β· (2βπ΄))) β ran (π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))) |
103 | 91, 102 | eqeltrrd 2835 |
. . . 4
β’ ((((π β§ π΄ β β) β§ π₯ β β) β§ (π΄π½π₯) β€ π΄) β (π΄π½π₯) β ran (π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))) |
104 | 77 | nnnn0d 12481 |
. . . . . . . . . 10
β’ (((π β§ π΄ β β) β§ π₯ β β) β (π΄ Β· (2βπ΄)) β
β0) |
105 | 104, 73 | eleqtrdi 2844 |
. . . . . . . . 9
β’ (((π β§ π΄ β β) β§ π₯ β β) β (π΄ Β· (2βπ΄)) β
(β€β₯β0)) |
106 | | eluzfz2 13458 |
. . . . . . . . 9
β’ ((π΄ Β· (2βπ΄)) β
(β€β₯β0) β (π΄ Β· (2βπ΄)) β (0...(π΄ Β· (2βπ΄)))) |
107 | 105, 106 | syl 17 |
. . . . . . . 8
β’ (((π β§ π΄ β β) β§ π₯ β β) β (π΄ Β· (2βπ΄)) β (0...(π΄ Β· (2βπ΄)))) |
108 | | oveq1 7368 |
. . . . . . . . 9
β’ (π = (π΄ Β· (2βπ΄)) β (π / (2βπ΄)) = ((π΄ Β· (2βπ΄)) / (2βπ΄))) |
109 | | ovex 7394 |
. . . . . . . . 9
β’ ((π΄ Β· (2βπ΄)) / (2βπ΄)) β V |
110 | 108, 84, 109 | fvmpt 6952 |
. . . . . . . 8
β’ ((π΄ Β· (2βπ΄)) β (0...(π΄ Β· (2βπ΄))) β ((π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))β(π΄ Β· (2βπ΄))) = ((π΄ Β· (2βπ΄)) / (2βπ΄))) |
111 | 107, 110 | syl 17 |
. . . . . . 7
β’ (((π β§ π΄ β β) β§ π₯ β β) β ((π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))β(π΄ Β· (2βπ΄))) = ((π΄ Β· (2βπ΄)) / (2βπ΄))) |
112 | 29 | recnd 11191 |
. . . . . . . 8
β’ (((π β§ π΄ β β) β§ π₯ β β) β π΄ β β) |
113 | 33 | nncnd 12177 |
. . . . . . . 8
β’ (((π β§ π΄ β β) β§ π₯ β β) β (2βπ΄) β
β) |
114 | 33 | nnne0d 12211 |
. . . . . . . 8
β’ (((π β§ π΄ β β) β§ π₯ β β) β (2βπ΄) β 0) |
115 | 112, 113,
114 | divcan4d 11945 |
. . . . . . 7
β’ (((π β§ π΄ β β) β§ π₯ β β) β ((π΄ Β· (2βπ΄)) / (2βπ΄)) = π΄) |
116 | 111, 115 | eqtrd 2773 |
. . . . . 6
β’ (((π β§ π΄ β β) β§ π₯ β β) β ((π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))β(π΄ Β· (2βπ΄))) = π΄) |
117 | | fnfvelrn 7035 |
. . . . . . 7
β’ (((π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄))) Fn (0...(π΄ Β· (2βπ΄))) β§ (π΄ Β· (2βπ΄)) β (0...(π΄ Β· (2βπ΄)))) β ((π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))β(π΄ Β· (2βπ΄))) β ran (π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))) |
118 | 99, 107, 117 | syl2anc 585 |
. . . . . 6
β’ (((π β§ π΄ β β) β§ π₯ β β) β ((π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))β(π΄ Β· (2βπ΄))) β ran (π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))) |
119 | 116, 118 | eqeltrrd 2835 |
. . . . 5
β’ (((π β§ π΄ β β) β§ π₯ β β) β π΄ β ran (π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))) |
120 | 119 | adantr 482 |
. . . 4
β’ ((((π β§ π΄ β β) β§ π₯ β β) β§ Β¬ (π΄π½π₯) β€ π΄) β π΄ β ran (π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))) |
121 | 103, 120 | ifclda 4525 |
. . 3
β’ (((π β§ π΄ β β) β§ π₯ β β) β if((π΄π½π₯) β€ π΄, (π΄π½π₯), π΄) β ran (π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))) |
122 | | eluzfz1 13457 |
. . . . . . 7
β’ ((π΄ Β· (2βπ΄)) β
(β€β₯β0) β 0 β (0...(π΄ Β· (2βπ΄)))) |
123 | 105, 122 | syl 17 |
. . . . . 6
β’ (((π β§ π΄ β β) β§ π₯ β β) β 0 β (0...(π΄ Β· (2βπ΄)))) |
124 | | oveq1 7368 |
. . . . . . 7
β’ (π = 0 β (π / (2βπ΄)) = (0 / (2βπ΄))) |
125 | | ovex 7394 |
. . . . . . 7
β’ (0 /
(2βπ΄)) β
V |
126 | 124, 84, 125 | fvmpt 6952 |
. . . . . 6
β’ (0 β
(0...(π΄ Β·
(2βπ΄))) β ((π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))β0) = (0 / (2βπ΄))) |
127 | 123, 126 | syl 17 |
. . . . 5
β’ (((π β§ π΄ β β) β§ π₯ β β) β ((π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))β0) = (0 / (2βπ΄))) |
128 | | nncn 12169 |
. . . . . . 7
β’
((2βπ΄) β
β β (2βπ΄)
β β) |
129 | | nnne0 12195 |
. . . . . . 7
β’
((2βπ΄) β
β β (2βπ΄)
β 0) |
130 | 128, 129 | div0d 11938 |
. . . . . 6
β’
((2βπ΄) β
β β (0 / (2βπ΄)) = 0) |
131 | 33, 130 | syl 17 |
. . . . 5
β’ (((π β§ π΄ β β) β§ π₯ β β) β (0 / (2βπ΄)) = 0) |
132 | 127, 131 | eqtrd 2773 |
. . . 4
β’ (((π β§ π΄ β β) β§ π₯ β β) β ((π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))β0) = 0) |
133 | | fnfvelrn 7035 |
. . . . 5
β’ (((π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄))) Fn (0...(π΄ Β· (2βπ΄))) β§ 0 β (0...(π΄ Β· (2βπ΄)))) β ((π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))β0) β ran (π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))) |
134 | 99, 123, 133 | syl2anc 585 |
. . . 4
β’ (((π β§ π΄ β β) β§ π₯ β β) β ((π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))β0) β ran (π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))) |
135 | 132, 134 | eqeltrrd 2835 |
. . 3
β’ (((π β§ π΄ β β) β§ π₯ β β) β 0 β ran (π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))) |
136 | 121, 135 | ifcld 4536 |
. 2
β’ (((π β§ π΄ β β) β§ π₯ β β) β if(π₯ β (-π΄[,]π΄), if((π΄π½π₯) β€ π΄, (π΄π½π₯), π΄), 0) β ran (π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))) |
137 | 6, 136 | fmpt3d 7068 |
1
β’ ((π β§ π΄ β β) β (πΊβπ΄):ββΆran (π β (0...(π΄ Β· (2βπ΄))) β¦ (π / (2βπ΄)))) |