Step | Hyp | Ref
| Expression |
1 | | itg2mulc.2 |
. . . . . . 7
β’ (π β πΉ:ββΆ(0[,)+β)) |
2 | | icossicc 13362 |
. . . . . . 7
β’
(0[,)+β) β (0[,]+β) |
3 | | fss 6689 |
. . . . . . 7
β’ ((πΉ:ββΆ(0[,)+β)
β§ (0[,)+β) β (0[,]+β)) β πΉ:ββΆ(0[,]+β)) |
4 | 1, 2, 3 | sylancl 587 |
. . . . . 6
β’ (π β πΉ:ββΆ(0[,]+β)) |
5 | 4 | adantr 482 |
. . . . 5
β’ ((π β§ π β dom β«1) β πΉ:ββΆ(0[,]+β)) |
6 | | simpr 486 |
. . . . . 6
β’ ((π β§ π β dom β«1) β π β dom
β«1) |
7 | | itg2mulclem.4 |
. . . . . . . . 9
β’ (π β π΄ β
β+) |
8 | 7 | rpreccld 12975 |
. . . . . . . 8
β’ (π β (1 / π΄) β
β+) |
9 | 8 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β dom β«1) β (1 /
π΄) β
β+) |
10 | 9 | rpred 12965 |
. . . . . 6
β’ ((π β§ π β dom β«1) β (1 /
π΄) β
β) |
11 | 6, 10 | i1fmulc 25091 |
. . . . 5
β’ ((π β§ π β dom β«1) β
((β Γ {(1 / π΄)}) βf Β· π) β dom
β«1) |
12 | | itg2ub 25121 |
. . . . . 6
β’ ((πΉ:ββΆ(0[,]+β)
β§ ((β Γ {(1 / π΄)}) βf Β· π) β dom β«1
β§ ((β Γ {(1 / π΄)}) βf Β· π) βr β€ πΉ) β
(β«1β((β Γ {(1 / π΄)}) βf Β· π)) β€
(β«2βπΉ)) |
13 | 12 | 3expia 1122 |
. . . . 5
β’ ((πΉ:ββΆ(0[,]+β)
β§ ((β Γ {(1 / π΄)}) βf Β· π) β dom β«1)
β (((β Γ {(1 / π΄)}) βf Β· π) βr β€ πΉ β
(β«1β((β Γ {(1 / π΄)}) βf Β· π)) β€
(β«2βπΉ))) |
14 | 5, 11, 13 | syl2anc 585 |
. . . 4
β’ ((π β§ π β dom β«1) β
(((β Γ {(1 / π΄)}) βf Β· π) βr β€ πΉ β
(β«1β((β Γ {(1 / π΄)}) βf Β· π)) β€
(β«2βπΉ))) |
15 | | i1ff 25063 |
. . . . . . . . . 10
β’ (π β dom β«1
β π:ββΆβ) |
16 | 15 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β dom β«1) β π:ββΆβ) |
17 | 16 | ffvelcdmda 7039 |
. . . . . . . 8
β’ (((π β§ π β dom β«1) β§ π¦ β β) β (πβπ¦) β β) |
18 | | rge0ssre 13382 |
. . . . . . . . . . 11
β’
(0[,)+β) β β |
19 | | fss 6689 |
. . . . . . . . . . 11
β’ ((πΉ:ββΆ(0[,)+β)
β§ (0[,)+β) β β) β πΉ:ββΆβ) |
20 | 1, 18, 19 | sylancl 587 |
. . . . . . . . . 10
β’ (π β πΉ:ββΆβ) |
21 | 20 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β dom β«1) β πΉ:ββΆβ) |
22 | 21 | ffvelcdmda 7039 |
. . . . . . . 8
β’ (((π β§ π β dom β«1) β§ π¦ β β) β (πΉβπ¦) β β) |
23 | 7 | rpred 12965 |
. . . . . . . . 9
β’ (π β π΄ β β) |
24 | 23 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β dom β«1) β§ π¦ β β) β π΄ β
β) |
25 | 7 | rpgt0d 12968 |
. . . . . . . . 9
β’ (π β 0 < π΄) |
26 | 25 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β dom β«1) β§ π¦ β β) β 0 <
π΄) |
27 | | ledivmul 12039 |
. . . . . . . 8
β’ (((πβπ¦) β β β§ (πΉβπ¦) β β β§ (π΄ β β β§ 0 < π΄)) β (((πβπ¦) / π΄) β€ (πΉβπ¦) β (πβπ¦) β€ (π΄ Β· (πΉβπ¦)))) |
28 | 17, 22, 24, 26, 27 | syl112anc 1375 |
. . . . . . 7
β’ (((π β§ π β dom β«1) β§ π¦ β β) β (((πβπ¦) / π΄) β€ (πΉβπ¦) β (πβπ¦) β€ (π΄ Β· (πΉβπ¦)))) |
29 | 17 | recnd 11191 |
. . . . . . . . 9
β’ (((π β§ π β dom β«1) β§ π¦ β β) β (πβπ¦) β β) |
30 | 24 | recnd 11191 |
. . . . . . . . 9
β’ (((π β§ π β dom β«1) β§ π¦ β β) β π΄ β
β) |
31 | 7 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β dom β«1) β π΄ β
β+) |
32 | 31 | rpne0d 12970 |
. . . . . . . . . 10
β’ ((π β§ π β dom β«1) β π΄ β 0) |
33 | 32 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β dom β«1) β§ π¦ β β) β π΄ β 0) |
34 | 29, 30, 33 | divrec2d 11943 |
. . . . . . . 8
β’ (((π β§ π β dom β«1) β§ π¦ β β) β ((πβπ¦) / π΄) = ((1 / π΄) Β· (πβπ¦))) |
35 | 34 | breq1d 5119 |
. . . . . . 7
β’ (((π β§ π β dom β«1) β§ π¦ β β) β (((πβπ¦) / π΄) β€ (πΉβπ¦) β ((1 / π΄) Β· (πβπ¦)) β€ (πΉβπ¦))) |
36 | 28, 35 | bitr3d 281 |
. . . . . 6
β’ (((π β§ π β dom β«1) β§ π¦ β β) β ((πβπ¦) β€ (π΄ Β· (πΉβπ¦)) β ((1 / π΄) Β· (πβπ¦)) β€ (πΉβπ¦))) |
37 | 36 | ralbidva 3169 |
. . . . 5
β’ ((π β§ π β dom β«1) β
(βπ¦ β β
(πβπ¦) β€ (π΄ Β· (πΉβπ¦)) β βπ¦ β β ((1 / π΄) Β· (πβπ¦)) β€ (πΉβπ¦))) |
38 | | reex 11150 |
. . . . . . 7
β’ β
β V |
39 | 38 | a1i 11 |
. . . . . 6
β’ ((π β§ π β dom β«1) β β
β V) |
40 | | ovexd 7396 |
. . . . . 6
β’ (((π β§ π β dom β«1) β§ π¦ β β) β (π΄ Β· (πΉβπ¦)) β V) |
41 | 16 | feqmptd 6914 |
. . . . . 6
β’ ((π β§ π β dom β«1) β π = (π¦ β β β¦ (πβπ¦))) |
42 | 7 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β dom β«1) β§ π¦ β β) β π΄ β
β+) |
43 | | fconstmpt 5698 |
. . . . . . . 8
β’ (β
Γ {π΄}) = (π¦ β β β¦ π΄) |
44 | 43 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β dom β«1) β
(β Γ {π΄}) =
(π¦ β β β¦
π΄)) |
45 | 1 | feqmptd 6914 |
. . . . . . . 8
β’ (π β πΉ = (π¦ β β β¦ (πΉβπ¦))) |
46 | 45 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β dom β«1) β πΉ = (π¦ β β β¦ (πΉβπ¦))) |
47 | 39, 42, 22, 44, 46 | offval2 7641 |
. . . . . 6
β’ ((π β§ π β dom β«1) β
((β Γ {π΄})
βf Β· πΉ) = (π¦ β β β¦ (π΄ Β· (πΉβπ¦)))) |
48 | 39, 17, 40, 41, 47 | ofrfval2 7642 |
. . . . 5
β’ ((π β§ π β dom β«1) β (π βr β€
((β Γ {π΄})
βf Β· πΉ) β βπ¦ β β (πβπ¦) β€ (π΄ Β· (πΉβπ¦)))) |
49 | | ovexd 7396 |
. . . . . 6
β’ (((π β§ π β dom β«1) β§ π¦ β β) β ((1 /
π΄) Β· (πβπ¦)) β V) |
50 | 8 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β dom β«1) β§ π¦ β β) β (1 /
π΄) β
β+) |
51 | | fconstmpt 5698 |
. . . . . . . 8
β’ (β
Γ {(1 / π΄)}) = (π¦ β β β¦ (1 /
π΄)) |
52 | 51 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β dom β«1) β
(β Γ {(1 / π΄)})
= (π¦ β β β¦
(1 / π΄))) |
53 | 39, 50, 17, 52, 41 | offval2 7641 |
. . . . . 6
β’ ((π β§ π β dom β«1) β
((β Γ {(1 / π΄)}) βf Β· π) = (π¦ β β β¦ ((1 / π΄) Β· (πβπ¦)))) |
54 | 39, 49, 22, 53, 46 | ofrfval2 7642 |
. . . . 5
β’ ((π β§ π β dom β«1) β
(((β Γ {(1 / π΄)}) βf Β· π) βr β€ πΉ β βπ¦ β β ((1 / π΄) Β· (πβπ¦)) β€ (πΉβπ¦))) |
55 | 37, 48, 54 | 3bitr4d 311 |
. . . 4
β’ ((π β§ π β dom β«1) β (π βr β€
((β Γ {π΄})
βf Β· πΉ) β ((β Γ {(1 / π΄)}) βf Β·
π) βr β€
πΉ)) |
56 | 6, 10 | itg1mulc 25092 |
. . . . . . 7
β’ ((π β§ π β dom β«1) β
(β«1β((β Γ {(1 / π΄)}) βf Β· π)) = ((1 / π΄) Β· (β«1βπ))) |
57 | | itg1cl 25072 |
. . . . . . . . . 10
β’ (π β dom β«1
β (β«1βπ) β β) |
58 | 57 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β dom β«1) β
(β«1βπ)
β β) |
59 | 58 | recnd 11191 |
. . . . . . . 8
β’ ((π β§ π β dom β«1) β
(β«1βπ)
β β) |
60 | 23 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β dom β«1) β π΄ β
β) |
61 | 60 | recnd 11191 |
. . . . . . . 8
β’ ((π β§ π β dom β«1) β π΄ β
β) |
62 | 59, 61, 32 | divrec2d 11943 |
. . . . . . 7
β’ ((π β§ π β dom β«1) β
((β«1βπ) / π΄) = ((1 / π΄) Β· (β«1βπ))) |
63 | 56, 62 | eqtr4d 2776 |
. . . . . 6
β’ ((π β§ π β dom β«1) β
(β«1β((β Γ {(1 / π΄)}) βf Β· π)) =
((β«1βπ) / π΄)) |
64 | 63 | breq1d 5119 |
. . . . 5
β’ ((π β§ π β dom β«1) β
((β«1β((β Γ {(1 / π΄)}) βf Β· π)) β€
(β«2βπΉ)
β ((β«1βπ) / π΄) β€ (β«2βπΉ))) |
65 | | itg2mulc.3 |
. . . . . . 7
β’ (π β
(β«2βπΉ)
β β) |
66 | 65 | adantr 482 |
. . . . . 6
β’ ((π β§ π β dom β«1) β
(β«2βπΉ)
β β) |
67 | 25 | adantr 482 |
. . . . . 6
β’ ((π β§ π β dom β«1) β 0 <
π΄) |
68 | | ledivmul 12039 |
. . . . . 6
β’
(((β«1βπ) β β β§
(β«2βπΉ)
β β β§ (π΄
β β β§ 0 < π΄)) β (((β«1βπ) / π΄) β€ (β«2βπΉ) β
(β«1βπ)
β€ (π΄ Β·
(β«2βπΉ)))) |
69 | 58, 66, 60, 67, 68 | syl112anc 1375 |
. . . . 5
β’ ((π β§ π β dom β«1) β
(((β«1βπ) / π΄) β€ (β«2βπΉ) β
(β«1βπ)
β€ (π΄ Β·
(β«2βπΉ)))) |
70 | 64, 69 | bitr2d 280 |
. . . 4
β’ ((π β§ π β dom β«1) β
((β«1βπ) β€ (π΄ Β· (β«2βπΉ)) β
(β«1β((β Γ {(1 / π΄)}) βf Β· π)) β€
(β«2βπΉ))) |
71 | 14, 55, 70 | 3imtr4d 294 |
. . 3
β’ ((π β§ π β dom β«1) β (π βr β€
((β Γ {π΄})
βf Β· πΉ) β (β«1βπ) β€ (π΄ Β· (β«2βπΉ)))) |
72 | 71 | ralrimiva 3140 |
. 2
β’ (π β βπ β dom β«1(π βr β€
((β Γ {π΄})
βf Β· πΉ) β (β«1βπ) β€ (π΄ Β· (β«2βπΉ)))) |
73 | | ge0mulcl 13387 |
. . . . . 6
β’ ((π₯ β (0[,)+β) β§
π¦ β (0[,)+β))
β (π₯ Β· π¦) β
(0[,)+β)) |
74 | 73 | adantl 483 |
. . . . 5
β’ ((π β§ (π₯ β (0[,)+β) β§ π¦ β (0[,)+β))) β
(π₯ Β· π¦) β
(0[,)+β)) |
75 | | fconstg 6733 |
. . . . . . 7
β’ (π΄ β β+
β (β Γ {π΄}):ββΆ{π΄}) |
76 | 7, 75 | syl 17 |
. . . . . 6
β’ (π β (β Γ {π΄}):ββΆ{π΄}) |
77 | | rpre 12931 |
. . . . . . . . 9
β’ (π΄ β β+
β π΄ β
β) |
78 | | rpge0 12936 |
. . . . . . . . 9
β’ (π΄ β β+
β 0 β€ π΄) |
79 | | elrege0 13380 |
. . . . . . . . 9
β’ (π΄ β (0[,)+β) β
(π΄ β β β§ 0
β€ π΄)) |
80 | 77, 78, 79 | sylanbrc 584 |
. . . . . . . 8
β’ (π΄ β β+
β π΄ β
(0[,)+β)) |
81 | 7, 80 | syl 17 |
. . . . . . 7
β’ (π β π΄ β (0[,)+β)) |
82 | 81 | snssd 4773 |
. . . . . 6
β’ (π β {π΄} β (0[,)+β)) |
83 | 76, 82 | fssd 6690 |
. . . . 5
β’ (π β (β Γ {π΄}):ββΆ(0[,)+β)) |
84 | 38 | a1i 11 |
. . . . 5
β’ (π β β β
V) |
85 | | inidm 4182 |
. . . . 5
β’ (β
β© β) = β |
86 | 74, 83, 1, 84, 84, 85 | off 7639 |
. . . 4
β’ (π β ((β Γ {π΄}) βf Β·
πΉ):ββΆ(0[,)+β)) |
87 | | fss 6689 |
. . . 4
β’
((((β Γ {π΄}) βf Β· πΉ):ββΆ(0[,)+β)
β§ (0[,)+β) β (0[,]+β)) β ((β Γ {π΄}) βf Β·
πΉ):ββΆ(0[,]+β)) |
88 | 86, 2, 87 | sylancl 587 |
. . 3
β’ (π β ((β Γ {π΄}) βf Β·
πΉ):ββΆ(0[,]+β)) |
89 | 23, 65 | remulcld 11193 |
. . . 4
β’ (π β (π΄ Β· (β«2βπΉ)) β
β) |
90 | 89 | rexrd 11213 |
. . 3
β’ (π β (π΄ Β· (β«2βπΉ)) β
β*) |
91 | | itg2leub 25122 |
. . 3
β’
((((β Γ {π΄}) βf Β· πΉ):ββΆ(0[,]+β)
β§ (π΄ Β·
(β«2βπΉ)) β β*) β
((β«2β((β Γ {π΄}) βf Β· πΉ)) β€ (π΄ Β· (β«2βπΉ)) β βπ β dom
β«1(π
βr β€ ((β Γ {π΄}) βf Β· πΉ) β
(β«1βπ)
β€ (π΄ Β·
(β«2βπΉ))))) |
92 | 88, 90, 91 | syl2anc 585 |
. 2
β’ (π β
((β«2β((β Γ {π΄}) βf Β· πΉ)) β€ (π΄ Β· (β«2βπΉ)) β βπ β dom
β«1(π
βr β€ ((β Γ {π΄}) βf Β· πΉ) β
(β«1βπ)
β€ (π΄ Β·
(β«2βπΉ))))) |
93 | 72, 92 | mpbird 257 |
1
β’ (π β
(β«2β((β Γ {π΄}) βf Β· πΉ)) β€ (π΄ Β· (β«2βπΉ))) |