Step | Hyp | Ref
| Expression |
1 | | itg2gt0.2 |
. 2
β’ (π β 0 < (volβπ΄)) |
2 | | itg2gt0.1 |
. . . . . . 7
β’ (π β π΄ β dom vol) |
3 | | iccssxr 13276 |
. . . . . . . 8
β’
(0[,]+β) β β* |
4 | | volf 24815 |
. . . . . . . . 9
β’ vol:dom
volβΆ(0[,]+β) |
5 | 4 | ffvelcdmi 7029 |
. . . . . . . 8
β’ (π΄ β dom vol β
(volβπ΄) β
(0[,]+β)) |
6 | 3, 5 | sselid 3941 |
. . . . . . 7
β’ (π΄ β dom vol β
(volβπ΄) β
β*) |
7 | 2, 6 | syl 17 |
. . . . . 6
β’ (π β (volβπ΄) β
β*) |
8 | 7 | adantr 482 |
. . . . 5
β’ ((π β§ Β¬ 0 <
(β«2βπΉ)) β (volβπ΄) β
β*) |
9 | | itg2gt0.4 |
. . . . . . . . . . . . . . . 16
β’ (π β πΉ β MblFn) |
10 | 9 | elexd 3464 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ β V) |
11 | | cnvexg 7852 |
. . . . . . . . . . . . . . 15
β’ (πΉ β V β β‘πΉ β V) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β β‘πΉ β V) |
13 | | imaexg 7843 |
. . . . . . . . . . . . . 14
β’ (β‘πΉ β V β (β‘πΉ β ((1 / π)(,)+β)) β V) |
14 | 12, 13 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (β‘πΉ β ((1 / π)(,)+β)) β V) |
15 | 14 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (β‘πΉ β ((1 / π)(,)+β)) β V) |
16 | 15 | fmpttd 7058 |
. . . . . . . . . . 11
β’ (π β (π β β β¦ (β‘πΉ β ((1 / π)(,)+β))):ββΆV) |
17 | 16 | ffnd 6665 |
. . . . . . . . . 10
β’ (π β (π β β β¦ (β‘πΉ β ((1 / π)(,)+β))) Fn β) |
18 | | fniunfv 7189 |
. . . . . . . . . 10
β’ ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β))) Fn β β βͺ π β β ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ) = βͺ ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))) |
19 | 17, 18 | syl 17 |
. . . . . . . . 9
β’ (π β βͺ π β β ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ) = βͺ ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))) |
20 | | itg2gt0.3 |
. . . . . . . . . . . . . . . 16
β’ (π β πΉ:ββΆ(0[,)+β)) |
21 | | rge0ssre 13302 |
. . . . . . . . . . . . . . . 16
β’
(0[,)+β) β β |
22 | | fss 6681 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ:ββΆ(0[,)+β)
β§ (0[,)+β) β β) β πΉ:ββΆβ) |
23 | 20, 21, 22 | sylancl 587 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ:ββΆβ) |
24 | | mbfima 24916 |
. . . . . . . . . . . . . . 15
β’ ((πΉ β MblFn β§ πΉ:ββΆβ) β
(β‘πΉ β ((1 / π)(,)+β)) β dom
vol) |
25 | 9, 23, 24 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β (β‘πΉ β ((1 / π)(,)+β)) β dom
vol) |
26 | 25 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (β‘πΉ β ((1 / π)(,)+β)) β dom
vol) |
27 | 26 | fmpttd 7058 |
. . . . . . . . . . . 12
β’ (π β (π β β β¦ (β‘πΉ β ((1 / π)(,)+β))):ββΆdom
vol) |
28 | 27 | ffvelcdmda 7030 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ) β dom vol) |
29 | 28 | ralrimiva 3142 |
. . . . . . . . . 10
β’ (π β βπ β β ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ) β dom vol) |
30 | | iunmbl 24839 |
. . . . . . . . . 10
β’
(βπ β
β ((π β β
β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ) β dom vol β βͺ π β β ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ) β dom vol) |
31 | 29, 30 | syl 17 |
. . . . . . . . 9
β’ (π β βͺ π β β ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ) β dom vol) |
32 | 19, 31 | eqeltrrd 2840 |
. . . . . . . 8
β’ (π β βͺ ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β))) β dom
vol) |
33 | | mblss 24817 |
. . . . . . . 8
β’ (βͺ ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β))) β dom vol β βͺ ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β))) β
β) |
34 | 32, 33 | syl 17 |
. . . . . . 7
β’ (π β βͺ ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β))) β
β) |
35 | | ovolcl 24764 |
. . . . . . 7
β’ (βͺ ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β))) β β β
(vol*ββͺ ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))) β
β*) |
36 | 34, 35 | syl 17 |
. . . . . 6
β’ (π β (vol*ββͺ ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))) β
β*) |
37 | 36 | adantr 482 |
. . . . 5
β’ ((π β§ Β¬ 0 <
(β«2βπΉ)) β (vol*ββͺ ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))) β
β*) |
38 | | 0xr 11136 |
. . . . . 6
β’ 0 β
β* |
39 | 38 | a1i 11 |
. . . . 5
β’ ((π β§ Β¬ 0 <
(β«2βπΉ)) β 0 β
β*) |
40 | | mblvol 24816 |
. . . . . . . 8
β’ (π΄ β dom vol β
(volβπ΄) =
(vol*βπ΄)) |
41 | 2, 40 | syl 17 |
. . . . . . 7
β’ (π β (volβπ΄) = (vol*βπ΄)) |
42 | | mblss 24817 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β dom vol β π΄ β
β) |
43 | 2, 42 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β π΄ β β) |
44 | 43 | sselda 3943 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β π΄) β π₯ β β) |
45 | 20 | ffvelcdmda 7030 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β β) β (πΉβπ₯) β (0[,)+β)) |
46 | | elrege0 13300 |
. . . . . . . . . . . . . . . 16
β’ ((πΉβπ₯) β (0[,)+β) β ((πΉβπ₯) β β β§ 0 β€ (πΉβπ₯))) |
47 | 45, 46 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β β) β ((πΉβπ₯) β β β§ 0 β€ (πΉβπ₯))) |
48 | 47 | simpld 496 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β) β (πΉβπ₯) β β) |
49 | 44, 48 | syldan 592 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π΄) β (πΉβπ₯) β β) |
50 | | itg2gt0.5 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π΄) β 0 < (πΉβπ₯)) |
51 | | nnrecl 12345 |
. . . . . . . . . . . . 13
β’ (((πΉβπ₯) β β β§ 0 < (πΉβπ₯)) β βπ β β (1 / π) < (πΉβπ₯)) |
52 | 49, 50, 51 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β βπ β β (1 / π) < (πΉβπ₯)) |
53 | 20 | ffnd 6665 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΉ Fn β) |
54 | 53 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β π΄) β§ π β β) β πΉ Fn β) |
55 | | elpreima 7004 |
. . . . . . . . . . . . . . . 16
β’ (πΉ Fn β β (π₯ β (β‘πΉ β ((1 / π)(,)+β)) β (π₯ β β β§ (πΉβπ₯) β ((1 / π)(,)+β)))) |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β π΄) β§ π β β) β (π₯ β (β‘πΉ β ((1 / π)(,)+β)) β (π₯ β β β§ (πΉβπ₯) β ((1 / π)(,)+β)))) |
57 | 44 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β π΄) β§ π β β) β π₯ β β) |
58 | 57 | biantrurd 534 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β π΄) β§ π β β) β ((πΉβπ₯) β ((1 / π)(,)+β) β (π₯ β β β§ (πΉβπ₯) β ((1 / π)(,)+β)))) |
59 | | nnrecre 12129 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β (1 /
π) β
β) |
60 | 59 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β (1 / π) β
β) |
61 | 60 | rexrd 11139 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β (1 / π) β
β*) |
62 | 61 | adantlr 714 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β π΄) β§ π β β) β (1 / π) β
β*) |
63 | | elioopnf 13289 |
. . . . . . . . . . . . . . . 16
β’ ((1 /
π) β
β* β ((πΉβπ₯) β ((1 / π)(,)+β) β ((πΉβπ₯) β β β§ (1 / π) < (πΉβπ₯)))) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β π΄) β§ π β β) β ((πΉβπ₯) β ((1 / π)(,)+β) β ((πΉβπ₯) β β β§ (1 / π) < (πΉβπ₯)))) |
65 | 56, 58, 64 | 3bitr2d 307 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β π΄) β§ π β β) β (π₯ β (β‘πΉ β ((1 / π)(,)+β)) β ((πΉβπ₯) β β β§ (1 / π) < (πΉβπ₯)))) |
66 | | id 22 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β
β) |
67 | | imaexg 7843 |
. . . . . . . . . . . . . . . . . 18
β’ (β‘πΉ β V β (β‘πΉ β ((1 / π)(,)+β)) β V) |
68 | 12, 67 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β (β‘πΉ β ((1 / π)(,)+β)) β V) |
69 | 68 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β π΄) β (β‘πΉ β ((1 / π)(,)+β)) β V) |
70 | | oveq2 7358 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (1 / π) = (1 / π)) |
71 | 70 | oveq1d 7365 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β ((1 / π)(,)+β) = ((1 / π)(,)+β)) |
72 | 71 | imaeq2d 6010 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (β‘πΉ β ((1 / π)(,)+β)) = (β‘πΉ β ((1 / π)(,)+β))) |
73 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β¦ (β‘πΉ β ((1 / π)(,)+β))) = (π β β β¦ (β‘πΉ β ((1 / π)(,)+β))) |
74 | 72, 73 | fvmptg 6942 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ (β‘πΉ β ((1 / π)(,)+β)) β V) β ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ) = (β‘πΉ β ((1 / π)(,)+β))) |
75 | 66, 69, 74 | syl2anr 598 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β π΄) β§ π β β) β ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ) = (β‘πΉ β ((1 / π)(,)+β))) |
76 | 75 | eleq2d 2824 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β π΄) β§ π β β) β (π₯ β ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ) β π₯ β (β‘πΉ β ((1 / π)(,)+β)))) |
77 | 49 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β π΄) β§ π β β) β (πΉβπ₯) β β) |
78 | 77 | biantrurd 534 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β π΄) β§ π β β) β ((1 / π) < (πΉβπ₯) β ((πΉβπ₯) β β β§ (1 / π) < (πΉβπ₯)))) |
79 | 65, 76, 78 | 3bitr4rd 312 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β π΄) β§ π β β) β ((1 / π) < (πΉβπ₯) β π₯ β ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ))) |
80 | 79 | rexbidva 3172 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β (βπ β β (1 / π) < (πΉβπ₯) β βπ β β π₯ β ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ))) |
81 | 52, 80 | mpbid 231 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β βπ β β π₯ β ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ)) |
82 | 81 | ex 414 |
. . . . . . . . . 10
β’ (π β (π₯ β π΄ β βπ β β π₯ β ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ))) |
83 | | eluni2 4868 |
. . . . . . . . . . 11
β’ (π₯ β βͺ ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β))) β βπ§ β ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))π₯ β π§) |
84 | | eleq2 2827 |
. . . . . . . . . . . . 13
β’ (π§ = ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ) β (π₯ β π§ β π₯ β ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ))) |
85 | 84 | rexrn 7032 |
. . . . . . . . . . . 12
β’ ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β))) Fn β β
(βπ§ β ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))π₯ β π§ β βπ β β π₯ β ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ))) |
86 | 17, 85 | syl 17 |
. . . . . . . . . . 11
β’ (π β (βπ§ β ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))π₯ β π§ β βπ β β π₯ β ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ))) |
87 | 83, 86 | bitrid 283 |
. . . . . . . . . 10
β’ (π β (π₯ β βͺ ran
(π β β β¦
(β‘πΉ β ((1 / π)(,)+β))) β βπ β β π₯ β ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ))) |
88 | 82, 87 | sylibrd 259 |
. . . . . . . . 9
β’ (π β (π₯ β π΄ β π₯ β βͺ ran
(π β β β¦
(β‘πΉ β ((1 / π)(,)+β))))) |
89 | 88 | ssrdv 3949 |
. . . . . . . 8
β’ (π β π΄ β βͺ ran
(π β β β¦
(β‘πΉ β ((1 / π)(,)+β)))) |
90 | | ovolss 24771 |
. . . . . . . 8
β’ ((π΄ β βͺ ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β))) β§ βͺ ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β))) β β) β
(vol*βπ΄) β€
(vol*ββͺ ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β))))) |
91 | 89, 34, 90 | syl2anc 585 |
. . . . . . 7
β’ (π β (vol*βπ΄) β€ (vol*ββͺ ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β))))) |
92 | 41, 91 | eqbrtrd 5126 |
. . . . . 6
β’ (π β (volβπ΄) β€ (vol*ββͺ ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β))))) |
93 | 92 | adantr 482 |
. . . . 5
β’ ((π β§ Β¬ 0 <
(β«2βπΉ)) β (volβπ΄) β€ (vol*ββͺ ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β))))) |
94 | | mblvol 24816 |
. . . . . . . . 9
β’ (βͺ ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β))) β dom vol β
(volββͺ ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))) = (vol*ββͺ ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β))))) |
95 | 32, 94 | syl 17 |
. . . . . . . 8
β’ (π β (volββͺ ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))) = (vol*ββͺ ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β))))) |
96 | | peano2nn 12099 |
. . . . . . . . . . . . . . . 16
β’ (π β β β (π + 1) β
β) |
97 | 96 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (π + 1) β β) |
98 | | nnrecre 12129 |
. . . . . . . . . . . . . . 15
β’ ((π + 1) β β β (1 /
(π + 1)) β
β) |
99 | 97, 98 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (1 / (π + 1)) β
β) |
100 | 99 | rexrd 11139 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (1 / (π + 1)) β
β*) |
101 | | nnre 12094 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β
β) |
102 | 101 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β π β β) |
103 | 102 | lep1d 12020 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β π β€ (π + 1)) |
104 | | nngt0 12118 |
. . . . . . . . . . . . . . . 16
β’ (π β β β 0 <
π) |
105 | 104 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β 0 < π) |
106 | 97 | nnred 12102 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (π + 1) β β) |
107 | 97 | nngt0d 12136 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β 0 < (π + 1)) |
108 | | lerec 11972 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ 0 <
π) β§ ((π + 1) β β β§ 0
< (π + 1))) β
(π β€ (π + 1) β (1 / (π + 1)) β€ (1 / π))) |
109 | 102, 105,
106, 107, 108 | syl22anc 838 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (π β€ (π + 1) β (1 / (π + 1)) β€ (1 / π))) |
110 | 103, 109 | mpbid 231 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (1 / (π + 1)) β€ (1 / π)) |
111 | | iooss1 13228 |
. . . . . . . . . . . . 13
β’ (((1 /
(π + 1)) β
β* β§ (1 / (π + 1)) β€ (1 / π)) β ((1 / π)(,)+β) β ((1 / (π +
1))(,)+β)) |
112 | 100, 110,
111 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((1 / π)(,)+β) β ((1 /
(π +
1))(,)+β)) |
113 | | imass2 6051 |
. . . . . . . . . . . 12
β’ (((1 /
π)(,)+β) β ((1
/ (π + 1))(,)+β)
β (β‘πΉ β ((1 / π)(,)+β)) β (β‘πΉ β ((1 / (π + 1))(,)+β))) |
114 | 112, 113 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (β‘πΉ β ((1 / π)(,)+β)) β (β‘πΉ β ((1 / (π + 1))(,)+β))) |
115 | 66, 68, 74 | syl2anr 598 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ) = (β‘πΉ β ((1 / π)(,)+β))) |
116 | | imaexg 7843 |
. . . . . . . . . . . . 13
β’ (β‘πΉ β V β (β‘πΉ β ((1 / (π + 1))(,)+β)) β
V) |
117 | 12, 116 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (β‘πΉ β ((1 / (π + 1))(,)+β)) β
V) |
118 | | oveq2 7358 |
. . . . . . . . . . . . . . 15
β’ (π = (π + 1) β (1 / π) = (1 / (π + 1))) |
119 | 118 | oveq1d 7365 |
. . . . . . . . . . . . . 14
β’ (π = (π + 1) β ((1 / π)(,)+β) = ((1 / (π + 1))(,)+β)) |
120 | 119 | imaeq2d 6010 |
. . . . . . . . . . . . 13
β’ (π = (π + 1) β (β‘πΉ β ((1 / π)(,)+β)) = (β‘πΉ β ((1 / (π + 1))(,)+β))) |
121 | 120, 73 | fvmptg 6942 |
. . . . . . . . . . . 12
β’ (((π + 1) β β β§
(β‘πΉ β ((1 / (π + 1))(,)+β)) β V) β ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))β(π + 1)) = (β‘πΉ β ((1 / (π + 1))(,)+β))) |
122 | 96, 117, 121 | syl2anr 598 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))β(π + 1)) = (β‘πΉ β ((1 / (π + 1))(,)+β))) |
123 | 114, 115,
122 | 3sstr4d 3990 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ) β ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))β(π + 1))) |
124 | 123 | ralrimiva 3142 |
. . . . . . . . 9
β’ (π β βπ β β ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ) β ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))β(π + 1))) |
125 | | volsup 24842 |
. . . . . . . . 9
β’ (((π β β β¦ (β‘πΉ β ((1 / π)(,)+β))):ββΆdom vol β§
βπ β β
((π β β β¦
(β‘πΉ β ((1 / π)(,)+β)))βπ) β ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))β(π + 1))) β (volββͺ ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))) = sup((vol β ran
(π β β β¦
(β‘πΉ β ((1 / π)(,)+β)))), β*, <
)) |
126 | 27, 124, 125 | syl2anc 585 |
. . . . . . . 8
β’ (π β (volββͺ ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))) = sup((vol β ran
(π β β β¦
(β‘πΉ β ((1 / π)(,)+β)))), β*, <
)) |
127 | 95, 126 | eqtr3d 2780 |
. . . . . . 7
β’ (π β (vol*ββͺ ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))) = sup((vol β ran
(π β β β¦
(β‘πΉ β ((1 / π)(,)+β)))), β*, <
)) |
128 | 127 | adantr 482 |
. . . . . 6
β’ ((π β§ Β¬ 0 <
(β«2βπΉ)) β (vol*ββͺ ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))) = sup((vol β ran
(π β β β¦
(β‘πΉ β ((1 / π)(,)+β)))), β*, <
)) |
129 | 68 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ Β¬ 0 <
(β«2βπΉ)) β (β‘πΉ β ((1 / π)(,)+β)) β V) |
130 | 66, 129, 74 | syl2anr 598 |
. . . . . . . . . . . 12
β’ (((π β§ Β¬ 0 <
(β«2βπΉ)) β§ π β β) β ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ) = (β‘πΉ β ((1 / π)(,)+β))) |
131 | 130 | fveq2d 6842 |
. . . . . . . . . . 11
β’ (((π β§ Β¬ 0 <
(β«2βπΉ)) β§ π β β) β (volβ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ)) = (volβ(β‘πΉ β ((1 / π)(,)+β)))) |
132 | 38 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β 0 β
β*) |
133 | | nnrecgt0 12130 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β β 0 < (1
/ π)) |
134 | 133 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β β) β 0 < (1 / π)) |
135 | | 0re 11091 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ 0 β
β |
136 | | ltle 11177 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((0
β β β§ (1 / π) β β) β (0 < (1 / π) β 0 β€ (1 / π))) |
137 | 135, 60, 136 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β β) β (0 < (1 / π) β 0 β€ (1 / π))) |
138 | 134, 137 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β β) β 0 β€ (1 / π)) |
139 | | elxrge0 13303 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((1 /
π) β (0[,]+β)
β ((1 / π) β
β* β§ 0 β€ (1 / π))) |
140 | 61, 138, 139 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β β) β (1 / π) β
(0[,]+β)) |
141 | | 0e0iccpnf 13305 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 0 β
(0[,]+β) |
142 | | ifcl 4530 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((1 /
π) β (0[,]+β)
β§ 0 β (0[,]+β)) β if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0) β (0[,]+β)) |
143 | 140, 141,
142 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β β) β if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0) β (0[,]+β)) |
144 | 143 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β) β§ π₯ β β) β if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0) β (0[,]+β)) |
145 | 144 | fmpttd 7058 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β (π₯ β β β¦ if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π),
0)):ββΆ(0[,]+β)) |
146 | 145 | adantrr 716 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β (π₯ β β β¦ if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π),
0)):ββΆ(0[,]+β)) |
147 | | itg2cl 25019 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β β β¦ if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0)):ββΆ(0[,]+β) β
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0))) β
β*) |
148 | 146, 147 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0))) β
β*) |
149 | | icossicc 13282 |
. . . . . . . . . . . . . . . . . . . 20
β’
(0[,)+β) β (0[,]+β) |
150 | | fss 6681 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΉ:ββΆ(0[,)+β)
β§ (0[,)+β) β (0[,]+β)) β πΉ:ββΆ(0[,]+β)) |
151 | 20, 149, 150 | sylancl 587 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΉ:ββΆ(0[,]+β)) |
152 | | itg2cl 25019 |
. . . . . . . . . . . . . . . . . . 19
β’ (πΉ:ββΆ(0[,]+β)
β (β«2βπΉ) β
β*) |
153 | 151, 152 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β
(β«2βπΉ)
β β*) |
154 | 153 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β
(β«2βπΉ)
β β*) |
155 | | 0nrp 12879 |
. . . . . . . . . . . . . . . . . . 19
β’ Β¬ 0
β β+ |
156 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β§ 0 =
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0)))) β 0 =
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0)))) |
157 | 115, 28 | eqeltrrd 2840 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β β) β (β‘πΉ β ((1 / π)(,)+β)) β dom
vol) |
158 | 157 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β (β‘πΉ β ((1 / π)(,)+β)) β dom
vol) |
159 | 158 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β§ 0 =
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0)))) β (β‘πΉ β ((1 / π)(,)+β)) β dom
vol) |
160 | 156, 135 | eqeltrrdi 2848 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β§ 0 =
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0)))) β
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0))) β β) |
161 | 60, 134 | elrpd 12883 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π β β) β (1 / π) β
β+) |
162 | 161 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β (1 / π) β
β+) |
163 | 162 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β§ 0 =
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0)))) β (1 / π) β
β+) |
164 | | itg2const2 25028 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((β‘πΉ β ((1 / π)(,)+β)) β dom vol β§ (1 /
π) β
β+) β ((volβ(β‘πΉ β ((1 / π)(,)+β))) β β β
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0))) β β)) |
165 | 159, 163,
164 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β§ 0 =
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0)))) β ((volβ(β‘πΉ β ((1 / π)(,)+β))) β β β
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0))) β β)) |
166 | 160, 165 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β§ 0 =
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0)))) β (volβ(β‘πΉ β ((1 / π)(,)+β))) β
β) |
167 | | elrege0 13300 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((1 /
π) β (0[,)+β)
β ((1 / π) β
β β§ 0 β€ (1 / π))) |
168 | 60, 138, 167 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β β) β (1 / π) β
(0[,)+β)) |
169 | 168 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β (1 / π) β
(0[,)+β)) |
170 | 169 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β§ 0 =
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0)))) β (1 / π) β (0[,)+β)) |
171 | | itg2const 25027 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((β‘πΉ β ((1 / π)(,)+β)) β dom vol β§
(volβ(β‘πΉ β ((1 / π)(,)+β))) β β β§ (1 /
π) β (0[,)+β))
β (β«2β(π₯ β β β¦ if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0))) = ((1 / π) Β· (volβ(β‘πΉ β ((1 / π)(,)+β))))) |
172 | 159, 166,
170, 171 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β§ 0 =
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0)))) β
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0))) = ((1 / π) Β· (volβ(β‘πΉ β ((1 / π)(,)+β))))) |
173 | 156, 172 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β§ 0 =
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0)))) β 0 = ((1 / π) Β· (volβ(β‘πΉ β ((1 / π)(,)+β))))) |
174 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β§ 0 =
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0)))) β 0 < (volβ(β‘πΉ β ((1 / π)(,)+β)))) |
175 | 166, 174 | elrpd 12883 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β§ 0 =
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0)))) β (volβ(β‘πΉ β ((1 / π)(,)+β))) β
β+) |
176 | 163, 175 | rpmulcld 12902 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β§ 0 =
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0)))) β ((1 / π) Β· (volβ(β‘πΉ β ((1 / π)(,)+β)))) β
β+) |
177 | 173, 176 | eqeltrd 2839 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β§ 0 =
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0)))) β 0 β
β+) |
178 | 177 | ex 414 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β (0 =
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0))) β 0 β
β+)) |
179 | 155, 178 | mtoi 198 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β Β¬ 0 =
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0)))) |
180 | | itg2ge0 25022 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π₯ β β β¦ if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0)):ββΆ(0[,]+β) β 0
β€ (β«2β(π₯ β β β¦ if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0)))) |
181 | 146, 180 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β 0 β€
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0)))) |
182 | | xrleloe 12992 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((0
β β* β§ (β«2β(π₯ β β β¦ if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0))) β β*) β (0
β€ (β«2β(π₯ β β β¦ if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0))) β (0 <
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0))) β¨ 0 =
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0)))))) |
183 | 38, 148, 182 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β (0 β€
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0))) β (0 <
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0))) β¨ 0 =
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0)))))) |
184 | 181, 183 | mpbid 231 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β (0 <
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0))) β¨ 0 =
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0))))) |
185 | 184 | ord 863 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β (Β¬ 0 <
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0))) β 0 =
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0))))) |
186 | 179, 185 | mt3d 148 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β 0 <
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0)))) |
187 | 151 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β πΉ:ββΆ(0[,]+β)) |
188 | 60 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β β) β§ π₯ β (β‘πΉ β ((1 / π)(,)+β))) β (1 / π) β
β) |
189 | 53 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ π β β) β πΉ Fn β) |
190 | 189, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π β β) β (π₯ β (β‘πΉ β ((1 / π)(,)+β)) β (π₯ β β β§ (πΉβπ₯) β ((1 / π)(,)+β)))) |
191 | 190 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π β β) β§ π₯ β (β‘πΉ β ((1 / π)(,)+β))) β (π₯ β β β§ (πΉβπ₯) β ((1 / π)(,)+β))) |
192 | 191 | simpld 496 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β β) β§ π₯ β (β‘πΉ β ((1 / π)(,)+β))) β π₯ β β) |
193 | 48 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β β) β§ π₯ β β) β (πΉβπ₯) β β) |
194 | 192, 193 | syldan 592 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β β) β§ π₯ β (β‘πΉ β ((1 / π)(,)+β))) β (πΉβπ₯) β β) |
195 | 61 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β β) β§ π₯ β (β‘πΉ β ((1 / π)(,)+β))) β (1 / π) β
β*) |
196 | 191 | simprd 497 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β β) β§ π₯ β (β‘πΉ β ((1 / π)(,)+β))) β (πΉβπ₯) β ((1 / π)(,)+β)) |
197 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((πΉβπ₯) β β β§ (1 / π) < (πΉβπ₯)) β (1 / π) < (πΉβπ₯)) |
198 | 63, 197 | syl6bi 253 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((1 /
π) β
β* β ((πΉβπ₯) β ((1 / π)(,)+β) β (1 / π) < (πΉβπ₯))) |
199 | 195, 196,
198 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β β) β§ π₯ β (β‘πΉ β ((1 / π)(,)+β))) β (1 / π) < (πΉβπ₯)) |
200 | 188, 194,
199 | ltled 11237 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β β) β§ π₯ β (β‘πΉ β ((1 / π)(,)+β))) β (1 / π) β€ (πΉβπ₯)) |
201 | 47 | simprd 497 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π₯ β β) β 0 β€ (πΉβπ₯)) |
202 | 201 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β β) β§ π₯ β β) β 0 β€ (πΉβπ₯)) |
203 | 192, 202 | syldan 592 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β β) β§ π₯ β (β‘πΉ β ((1 / π)(,)+β))) β 0 β€ (πΉβπ₯)) |
204 | | breq1 5107 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((1 /
π) = if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0) β ((1 / π) β€ (πΉβπ₯) β if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0) β€ (πΉβπ₯))) |
205 | | breq1 5107 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (0 =
if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0) β (0 β€ (πΉβπ₯) β if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0) β€ (πΉβπ₯))) |
206 | 204, 205 | ifboth 4524 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((1 /
π) β€ (πΉβπ₯) β§ 0 β€ (πΉβπ₯)) β if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0) β€ (πΉβπ₯)) |
207 | 200, 203,
206 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β β) β§ π₯ β (β‘πΉ β ((1 / π)(,)+β))) β if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0) β€ (πΉβπ₯)) |
208 | 207 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β β) β§ π₯ β β) β§ π₯ β (β‘πΉ β ((1 / π)(,)+β))) β if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0) β€ (πΉβπ₯)) |
209 | | iffalse 4494 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (Β¬
π₯ β (β‘πΉ β ((1 / π)(,)+β)) β if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0) = 0) |
210 | 209 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β β) β§ π₯ β β) β§ Β¬ π₯ β (β‘πΉ β ((1 / π)(,)+β))) β if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0) = 0) |
211 | 202 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β β) β§ π₯ β β) β§ Β¬ π₯ β (β‘πΉ β ((1 / π)(,)+β))) β 0 β€ (πΉβπ₯)) |
212 | 210, 211 | eqbrtrd 5126 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β β) β§ π₯ β β) β§ Β¬ π₯ β (β‘πΉ β ((1 / π)(,)+β))) β if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0) β€ (πΉβπ₯)) |
213 | 208, 212 | pm2.61dan 812 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β) β§ π₯ β β) β if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0) β€ (πΉβπ₯)) |
214 | 213 | ralrimiva 3142 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β β) β βπ₯ β β if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0) β€ (πΉβπ₯)) |
215 | 214 | adantrr 716 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β βπ₯ β β if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0) β€ (πΉβπ₯)) |
216 | | reex 11076 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ β
β V |
217 | 216 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β
V) |
218 | | ovex 7383 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (1 /
π) β
V |
219 | | c0ex 11083 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ 0 β
V |
220 | 218, 219 | ifex 4535 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0) β V |
221 | 220 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π₯ β β) β if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0) β V) |
222 | | fvexd 6853 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π₯ β β) β (πΉβπ₯) β V) |
223 | | eqidd 2739 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π₯ β β β¦ if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0)) = (π₯ β β β¦ if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0))) |
224 | 20 | feqmptd 6906 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β πΉ = (π₯ β β β¦ (πΉβπ₯))) |
225 | 217, 221,
222, 223, 224 | ofrfval2 7629 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((π₯ β β β¦ if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0)) βr β€ πΉ β βπ₯ β β if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0) β€ (πΉβπ₯))) |
226 | 225 | biimpar 479 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ βπ₯ β β if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0) β€ (πΉβπ₯)) β (π₯ β β β¦ if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0)) βr β€ πΉ) |
227 | 215, 226 | syldan 592 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β (π₯ β β β¦ if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0)) βr β€ πΉ) |
228 | | itg2le 25026 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ β β β¦ if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0)):ββΆ(0[,]+β) β§
πΉ:ββΆ(0[,]+β) β§ (π₯ β β β¦ if(π₯ β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0)) βr β€ πΉ) β
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0))) β€ (β«2βπΉ)) |
229 | 146, 187,
227, 228 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β
(β«2β(π₯
β β β¦ if(π₯
β (β‘πΉ β ((1 / π)(,)+β)), (1 / π), 0))) β€ (β«2βπΉ)) |
230 | 132, 148,
154, 186, 229 | xrltletrd 13009 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β β β§ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) β 0 <
(β«2βπΉ)) |
231 | 230 | expr 458 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))) β 0 <
(β«2βπΉ))) |
232 | 231 | con3d 152 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (Β¬ 0 <
(β«2βπΉ)
β Β¬ 0 < (volβ(β‘πΉ β ((1 / π)(,)+β))))) |
233 | 4 | ffvelcdmi 7029 |
. . . . . . . . . . . . . . . . 17
β’ ((β‘πΉ β ((1 / π)(,)+β)) β dom vol β
(volβ(β‘πΉ β ((1 / π)(,)+β))) β
(0[,]+β)) |
234 | 3, 233 | sselid 3941 |
. . . . . . . . . . . . . . . 16
β’ ((β‘πΉ β ((1 / π)(,)+β)) β dom vol β
(volβ(β‘πΉ β ((1 / π)(,)+β))) β
β*) |
235 | 157, 234 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (volβ(β‘πΉ β ((1 / π)(,)+β))) β
β*) |
236 | | xrlenlt 11154 |
. . . . . . . . . . . . . . 15
β’
(((volβ(β‘πΉ β ((1 / π)(,)+β))) β β*
β§ 0 β β*) β ((volβ(β‘πΉ β ((1 / π)(,)+β))) β€ 0 β Β¬ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) |
237 | 235, 38, 236 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β ((volβ(β‘πΉ β ((1 / π)(,)+β))) β€ 0 β Β¬ 0 <
(volβ(β‘πΉ β ((1 / π)(,)+β))))) |
238 | 232, 237 | sylibrd 259 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (Β¬ 0 <
(β«2βπΉ)
β (volβ(β‘πΉ β ((1 / π)(,)+β))) β€ 0)) |
239 | 238 | imp 408 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ Β¬ 0 <
(β«2βπΉ)) β (volβ(β‘πΉ β ((1 / π)(,)+β))) β€ 0) |
240 | 239 | an32s 651 |
. . . . . . . . . . 11
β’ (((π β§ Β¬ 0 <
(β«2βπΉ)) β§ π β β) β (volβ(β‘πΉ β ((1 / π)(,)+β))) β€ 0) |
241 | 131, 240 | eqbrtrd 5126 |
. . . . . . . . . 10
β’ (((π β§ Β¬ 0 <
(β«2βπΉ)) β§ π β β) β (volβ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ)) β€ 0) |
242 | 241 | ralrimiva 3142 |
. . . . . . . . 9
β’ ((π β§ Β¬ 0 <
(β«2βπΉ)) β βπ β β (volβ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ)) β€ 0) |
243 | | ffn 6664 |
. . . . . . . . . . 11
β’ ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β))):ββΆV β
(π β β β¦
(β‘πΉ β ((1 / π)(,)+β))) Fn β) |
244 | | fveq2 6838 |
. . . . . . . . . . . . 13
β’ (π§ = ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ) β (volβπ§) = (volβ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ))) |
245 | 244 | breq1d 5114 |
. . . . . . . . . . . 12
β’ (π§ = ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ) β ((volβπ§) β€ 0 β (volβ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ)) β€ 0)) |
246 | 245 | ralrn 7033 |
. . . . . . . . . . 11
β’ ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β))) Fn β β
(βπ§ β ran
(π β β β¦
(β‘πΉ β ((1 / π)(,)+β)))(volβπ§) β€ 0 β βπ β β (volβ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ)) β€ 0)) |
247 | 16, 243, 246 | 3syl 18 |
. . . . . . . . . 10
β’ (π β (βπ§ β ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))(volβπ§) β€ 0 β βπ β β (volβ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ)) β€ 0)) |
248 | 247 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ Β¬ 0 <
(β«2βπΉ)) β (βπ§ β ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))(volβπ§) β€ 0 β βπ β β (volβ((π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))βπ)) β€ 0)) |
249 | 242, 248 | mpbird 257 |
. . . . . . . 8
β’ ((π β§ Β¬ 0 <
(β«2βπΉ)) β βπ§ β ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))(volβπ§) β€ 0) |
250 | | ffn 6664 |
. . . . . . . . . 10
β’ (vol:dom
volβΆ(0[,]+β) β vol Fn dom vol) |
251 | 4, 250 | ax-mp 5 |
. . . . . . . . 9
β’ vol Fn
dom vol |
252 | 27 | frnd 6672 |
. . . . . . . . . 10
β’ (π β ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β))) β dom
vol) |
253 | 252 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ Β¬ 0 <
(β«2βπΉ)) β ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β))) β dom
vol) |
254 | | breq1 5107 |
. . . . . . . . . 10
β’ (π₯ = (volβπ§) β (π₯ β€ 0 β (volβπ§) β€ 0)) |
255 | 254 | ralima 7183 |
. . . . . . . . 9
β’ ((vol Fn
dom vol β§ ran (π β
β β¦ (β‘πΉ β ((1 / π)(,)+β))) β dom vol) β
(βπ₯ β (vol
β ran (π β
β β¦ (β‘πΉ β ((1 / π)(,)+β))))π₯ β€ 0 β βπ§ β ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))(volβπ§) β€ 0)) |
256 | 251, 253,
255 | sylancr 588 |
. . . . . . . 8
β’ ((π β§ Β¬ 0 <
(β«2βπΉ)) β (βπ₯ β (vol β ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β))))π₯ β€ 0 β βπ§ β ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))(volβπ§) β€ 0)) |
257 | 249, 256 | mpbird 257 |
. . . . . . 7
β’ ((π β§ Β¬ 0 <
(β«2βπΉ)) β βπ₯ β (vol β ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β))))π₯ β€ 0) |
258 | | imassrn 6021 |
. . . . . . . . 9
β’ (vol
β ran (π β
β β¦ (β‘πΉ β ((1 / π)(,)+β)))) β ran
vol |
259 | | frn 6671 |
. . . . . . . . . . 11
β’ (vol:dom
volβΆ(0[,]+β) β ran vol β
(0[,]+β)) |
260 | 4, 259 | ax-mp 5 |
. . . . . . . . . 10
β’ ran vol
β (0[,]+β) |
261 | 260, 3 | sstri 3952 |
. . . . . . . . 9
β’ ran vol
β β* |
262 | 258, 261 | sstri 3952 |
. . . . . . . 8
β’ (vol
β ran (π β
β β¦ (β‘πΉ β ((1 / π)(,)+β)))) β
β* |
263 | | supxrleub 13174 |
. . . . . . . 8
β’ (((vol
β ran (π β
β β¦ (β‘πΉ β ((1 / π)(,)+β)))) β β*
β§ 0 β β*) β (sup((vol β ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))), β*, < )
β€ 0 β βπ₯
β (vol β ran (π
β β β¦ (β‘πΉ β ((1 / π)(,)+β))))π₯ β€ 0)) |
264 | 262, 38, 263 | mp2an 691 |
. . . . . . 7
β’ (sup((vol
β ran (π β
β β¦ (β‘πΉ β ((1 / π)(,)+β)))), β*, < )
β€ 0 β βπ₯
β (vol β ran (π
β β β¦ (β‘πΉ β ((1 / π)(,)+β))))π₯ β€ 0) |
265 | 257, 264 | sylibr 233 |
. . . . . 6
β’ ((π β§ Β¬ 0 <
(β«2βπΉ)) β sup((vol β ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))), β*, < )
β€ 0) |
266 | 128, 265 | eqbrtrd 5126 |
. . . . 5
β’ ((π β§ Β¬ 0 <
(β«2βπΉ)) β (vol*ββͺ ran (π β β β¦ (β‘πΉ β ((1 / π)(,)+β)))) β€ 0) |
267 | 8, 37, 39, 93, 266 | xrletrd 13010 |
. . . 4
β’ ((π β§ Β¬ 0 <
(β«2βπΉ)) β (volβπ΄) β€ 0) |
268 | 267 | ex 414 |
. . 3
β’ (π β (Β¬ 0 <
(β«2βπΉ)
β (volβπ΄) β€
0)) |
269 | | xrlenlt 11154 |
. . . 4
β’
(((volβπ΄)
β β* β§ 0 β β*) β
((volβπ΄) β€ 0
β Β¬ 0 < (volβπ΄))) |
270 | 7, 38, 269 | sylancl 587 |
. . 3
β’ (π β ((volβπ΄) β€ 0 β Β¬ 0 <
(volβπ΄))) |
271 | 268, 270 | sylibd 238 |
. 2
β’ (π β (Β¬ 0 <
(β«2βπΉ)
β Β¬ 0 < (volβπ΄))) |
272 | 1, 271 | mt4d 117 |
1
β’ (π β 0 <
(β«2βπΉ)) |