Step | Hyp | Ref
| Expression |
1 | | itgulm.z |
. . . . 5
β’ π =
(β€β₯βπ) |
2 | | itgulm.m |
. . . . . 6
β’ (π β π β β€) |
3 | 2 | adantr 480 |
. . . . 5
β’ ((π β§ π β β+) β π β
β€) |
4 | | itgulm.f |
. . . . . . . 8
β’ (π β πΉ:πβΆπΏ1) |
5 | 4 | ffnd 6711 |
. . . . . . 7
β’ (π β πΉ Fn π) |
6 | | itgulm.u |
. . . . . . 7
β’ (π β πΉ(βπ’βπ)πΊ) |
7 | | ulmf2 26271 |
. . . . . . 7
β’ ((πΉ Fn π β§ πΉ(βπ’βπ)πΊ) β πΉ:πβΆ(β βm π)) |
8 | 5, 6, 7 | syl2anc 583 |
. . . . . 6
β’ (π β πΉ:πβΆ(β βm π)) |
9 | 8 | adantr 480 |
. . . . 5
β’ ((π β§ π β β+) β πΉ:πβΆ(β βm π)) |
10 | | eqidd 2727 |
. . . . 5
β’ (((π β§ π β β+) β§ (π β π β§ π§ β π)) β ((πΉβπ)βπ§) = ((πΉβπ)βπ§)) |
11 | | eqidd 2727 |
. . . . 5
β’ (((π β§ π β β+) β§ π§ β π) β (πΊβπ§) = (πΊβπ§)) |
12 | 6 | adantr 480 |
. . . . 5
β’ ((π β§ π β β+) β πΉ(βπ’βπ)πΊ) |
13 | | simpr 484 |
. . . . . 6
β’ ((π β§ π β β+) β π β
β+) |
14 | | itgulm.s |
. . . . . . . 8
β’ (π β (volβπ) β
β) |
15 | 14 | adantr 480 |
. . . . . . 7
β’ ((π β§ π β β+) β
(volβπ) β
β) |
16 | | ulmcl 26268 |
. . . . . . . . . . . 12
β’ (πΉ(βπ’βπ)πΊ β πΊ:πβΆβ) |
17 | | fdm 6719 |
. . . . . . . . . . . 12
β’ (πΊ:πβΆβ β dom πΊ = π) |
18 | 6, 16, 17 | 3syl 18 |
. . . . . . . . . . 11
β’ (π β dom πΊ = π) |
19 | 1, 2, 4, 6, 14 | iblulm 26294 |
. . . . . . . . . . . 12
β’ (π β πΊ β
πΏ1) |
20 | | iblmbf 25648 |
. . . . . . . . . . . 12
β’ (πΊ β πΏ1
β πΊ β
MblFn) |
21 | | mbfdm 25506 |
. . . . . . . . . . . 12
β’ (πΊ β MblFn β dom πΊ β dom
vol) |
22 | 19, 20, 21 | 3syl 18 |
. . . . . . . . . . 11
β’ (π β dom πΊ β dom vol) |
23 | 18, 22 | eqeltrrd 2828 |
. . . . . . . . . 10
β’ (π β π β dom vol) |
24 | | mblss 25411 |
. . . . . . . . . 10
β’ (π β dom vol β π β
β) |
25 | | ovolge0 25361 |
. . . . . . . . . 10
β’ (π β β β 0 β€
(vol*βπ)) |
26 | 23, 24, 25 | 3syl 18 |
. . . . . . . . 9
β’ (π β 0 β€ (vol*βπ)) |
27 | | mblvol 25410 |
. . . . . . . . . 10
β’ (π β dom vol β
(volβπ) =
(vol*βπ)) |
28 | 23, 27 | syl 17 |
. . . . . . . . 9
β’ (π β (volβπ) = (vol*βπ)) |
29 | 26, 28 | breqtrrd 5169 |
. . . . . . . 8
β’ (π β 0 β€ (volβπ)) |
30 | 29 | adantr 480 |
. . . . . . 7
β’ ((π β§ π β β+) β 0 β€
(volβπ)) |
31 | 15, 30 | ge0p1rpd 13049 |
. . . . . 6
β’ ((π β§ π β β+) β
((volβπ) + 1) β
β+) |
32 | 13, 31 | rpdivcld 13036 |
. . . . 5
β’ ((π β§ π β β+) β (π / ((volβπ) + 1)) β
β+) |
33 | 1, 3, 9, 10, 11, 12, 32 | ulmi 26273 |
. . . 4
β’ ((π β§ π β β+) β
βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1))) |
34 | 1 | uztrn2 12842 |
. . . . . . . 8
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
35 | 8 | ffvelcdmda 7079 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π) β (πΉβπ) β (β βm π)) |
36 | | elmapi 8842 |
. . . . . . . . . . . . . . . 16
β’ ((πΉβπ) β (β βm π) β (πΉβπ):πβΆβ) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π) β (πΉβπ):πβΆβ) |
38 | 37 | ffvelcdmda 7079 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π) β§ π₯ β π) β ((πΉβπ)βπ₯) β β) |
39 | 38 | adantllr 716 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β+) β§ π β π) β§ π₯ β π) β ((πΉβπ)βπ₯) β β) |
40 | 39 | adantlrr 718 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β§ π₯ β π) β ((πΉβπ)βπ₯) β β) |
41 | 37 | feqmptd 6953 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β (πΉβπ) = (π₯ β π β¦ ((πΉβπ)βπ₯))) |
42 | 4 | ffvelcdmda 7079 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β (πΉβπ) β
πΏ1) |
43 | 41, 42 | eqeltrrd 2828 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β (π₯ β π β¦ ((πΉβπ)βπ₯)) β
πΏ1) |
44 | 43 | ad2ant2r 744 |
. . . . . . . . . . . 12
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β (π₯ β π β¦ ((πΉβπ)βπ₯)) β
πΏ1) |
45 | 6, 16 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β πΊ:πβΆβ) |
46 | 45 | ffvelcdmda 7079 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π) β (πΊβπ₯) β β) |
47 | 46 | ad4ant14 749 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β§ π₯ β π) β (πΊβπ₯) β β) |
48 | 45 | feqmptd 6953 |
. . . . . . . . . . . . . 14
β’ (π β πΊ = (π₯ β π β¦ (πΊβπ₯))) |
49 | 48, 19 | eqeltrrd 2828 |
. . . . . . . . . . . . 13
β’ (π β (π₯ β π β¦ (πΊβπ₯)) β
πΏ1) |
50 | 49 | ad2antrr 723 |
. . . . . . . . . . . 12
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β (π₯ β π β¦ (πΊβπ₯)) β
πΏ1) |
51 | 40, 44, 47, 50 | itgsub 25706 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β β«π(((πΉβπ)βπ₯) β (πΊβπ₯)) dπ₯ = (β«π((πΉβπ)βπ₯) dπ₯ β β«π(πΊβπ₯) dπ₯)) |
52 | 51 | fveq2d 6888 |
. . . . . . . . . 10
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β (absββ«π(((πΉβπ)βπ₯) β (πΊβπ₯)) dπ₯) = (absβ(β«π((πΉβπ)βπ₯) dπ₯ β β«π(πΊβπ₯) dπ₯))) |
53 | 40, 47 | subcld 11572 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β§ π₯ β π) β (((πΉβπ)βπ₯) β (πΊβπ₯)) β β) |
54 | 40, 44, 47, 50 | iblsub 25702 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β (π₯ β π β¦ (((πΉβπ)βπ₯) β (πΊβπ₯))) β
πΏ1) |
55 | 53, 54 | itgcl 25664 |
. . . . . . . . . . . 12
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β β«π(((πΉβπ)βπ₯) β (πΊβπ₯)) dπ₯ β β) |
56 | 55 | abscld 15387 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β (absββ«π(((πΉβπ)βπ₯) β (πΊβπ₯)) dπ₯) β β) |
57 | 53 | abscld 15387 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β§ π₯ β π) β (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) β β) |
58 | 53, 54 | iblabs 25709 |
. . . . . . . . . . . 12
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β (π₯ β π β¦ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯)))) β
πΏ1) |
59 | 57, 58 | itgrecl 25678 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β β«π(absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) dπ₯ β β) |
60 | | rpre 12985 |
. . . . . . . . . . . 12
β’ (π β β+
β π β
β) |
61 | 60 | ad2antlr 724 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β π β β) |
62 | 53, 54 | itgabs 25715 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β (absββ«π(((πΉβπ)βπ₯) β (πΊβπ₯)) dπ₯) β€ β«π(absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) dπ₯) |
63 | 32 | adantr 480 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β (π / ((volβπ) + 1)) β
β+) |
64 | 63 | rpred 13019 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β (π / ((volβπ) + 1)) β β) |
65 | 14 | ad2antrr 723 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β (volβπ) β
β) |
66 | 64, 65 | remulcld 11245 |
. . . . . . . . . . . 12
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β ((π / ((volβπ) + 1)) Β· (volβπ)) β
β) |
67 | | fconstmpt 5731 |
. . . . . . . . . . . . . . 15
β’ (π Γ {(π / ((volβπ) + 1))}) = (π₯ β π β¦ (π / ((volβπ) + 1))) |
68 | 23 | ad2antrr 723 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β π β dom vol) |
69 | 63 | rpcnd 13021 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β (π / ((volβπ) + 1)) β β) |
70 | | iblconst 25698 |
. . . . . . . . . . . . . . . 16
β’ ((π β dom vol β§
(volβπ) β
β β§ (π /
((volβπ) + 1)) β
β) β (π Γ
{(π / ((volβπ) + 1))}) β
πΏ1) |
71 | 68, 65, 69, 70 | syl3anc 1368 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β (π Γ {(π / ((volβπ) + 1))}) β
πΏ1) |
72 | 67, 71 | eqeltrrid 2832 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β (π₯ β π β¦ (π / ((volβπ) + 1))) β
πΏ1) |
73 | 64 | adantr 480 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β§ π₯ β π) β (π / ((volβπ) + 1)) β β) |
74 | | simprr 770 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1))) |
75 | | fveq2 6884 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π§ = π₯ β ((πΉβπ)βπ§) = ((πΉβπ)βπ₯)) |
76 | | fveq2 6884 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π§ = π₯ β (πΊβπ§) = (πΊβπ₯)) |
77 | 75, 76 | oveq12d 7422 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ = π₯ β (((πΉβπ)βπ§) β (πΊβπ§)) = (((πΉβπ)βπ₯) β (πΊβπ₯))) |
78 | 77 | fveq2d 6888 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ = π₯ β (absβ(((πΉβπ)βπ§) β (πΊβπ§))) = (absβ(((πΉβπ)βπ₯) β (πΊβπ₯)))) |
79 | 78 | breq1d 5151 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = π₯ β ((absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)) β (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < (π / ((volβπ) + 1)))) |
80 | 79 | rspccva 3605 |
. . . . . . . . . . . . . . . 16
β’
((βπ§ β
π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)) β§ π₯ β π) β (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < (π / ((volβπ) + 1))) |
81 | 74, 80 | sylan 579 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β§ π₯ β π) β (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < (π / ((volβπ) + 1))) |
82 | 57, 73, 81 | ltled 11363 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β§ π₯ β π) β (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) β€ (π / ((volβπ) + 1))) |
83 | 58, 72, 57, 73, 82 | itgle 25690 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β β«π(absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) dπ₯ β€ β«π(π / ((volβπ) + 1)) dπ₯) |
84 | | itgconst 25699 |
. . . . . . . . . . . . . 14
β’ ((π β dom vol β§
(volβπ) β
β β§ (π /
((volβπ) + 1)) β
β) β β«π(π / ((volβπ) + 1)) dπ₯ = ((π / ((volβπ) + 1)) Β· (volβπ))) |
85 | 68, 65, 69, 84 | syl3anc 1368 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β β«π(π / ((volβπ) + 1)) dπ₯ = ((π / ((volβπ) + 1)) Β· (volβπ))) |
86 | 83, 85 | breqtrd 5167 |
. . . . . . . . . . . 12
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β β«π(absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) dπ₯ β€ ((π / ((volβπ) + 1)) Β· (volβπ))) |
87 | 61 | recnd 11243 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β π β β) |
88 | 65 | recnd 11243 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β (volβπ) β
β) |
89 | 31 | adantr 480 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β ((volβπ) + 1) β
β+) |
90 | 89 | rpcnd 13021 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β ((volβπ) + 1) β
β) |
91 | 89 | rpne0d 13024 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β ((volβπ) + 1) β 0) |
92 | 87, 88, 90, 91 | div23d 12028 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β ((π Β· (volβπ)) / ((volβπ) + 1)) = ((π / ((volβπ) + 1)) Β· (volβπ))) |
93 | 65 | ltp1d 12145 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β (volβπ) < ((volβπ) + 1)) |
94 | | peano2re 11388 |
. . . . . . . . . . . . . . . . 17
β’
((volβπ)
β β β ((volβπ) + 1) β β) |
95 | 65, 94 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β ((volβπ) + 1) β
β) |
96 | | rpgt0 12989 |
. . . . . . . . . . . . . . . . 17
β’ (π β β+
β 0 < π) |
97 | 96 | ad2antlr 724 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β 0 < π) |
98 | | ltmul2 12066 |
. . . . . . . . . . . . . . . 16
β’
(((volβπ)
β β β§ ((volβπ) + 1) β β β§ (π β β β§ 0 <
π)) β
((volβπ) <
((volβπ) + 1) β
(π Β·
(volβπ)) < (π Β· ((volβπ) + 1)))) |
99 | 65, 95, 61, 97, 98 | syl112anc 1371 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β ((volβπ) < ((volβπ) + 1) β (π Β· (volβπ)) < (π Β· ((volβπ) + 1)))) |
100 | 93, 99 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β (π Β· (volβπ)) < (π Β· ((volβπ) + 1))) |
101 | 61, 65 | remulcld 11245 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β (π Β· (volβπ)) β β) |
102 | 101, 61, 89 | ltdivmul2d 13071 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β (((π Β· (volβπ)) / ((volβπ) + 1)) < π β (π Β· (volβπ)) < (π Β· ((volβπ) + 1)))) |
103 | 100, 102 | mpbird 257 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β ((π Β· (volβπ)) / ((volβπ) + 1)) < π) |
104 | 92, 103 | eqbrtrrd 5165 |
. . . . . . . . . . . 12
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β ((π / ((volβπ) + 1)) Β· (volβπ)) < π) |
105 | 59, 66, 61, 86, 104 | lelttrd 11373 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β β«π(absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) dπ₯ < π) |
106 | 56, 59, 61, 62, 105 | lelttrd 11373 |
. . . . . . . . . 10
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β (absββ«π(((πΉβπ)βπ₯) β (πΊβπ₯)) dπ₯) < π) |
107 | 52, 106 | eqbrtrrd 5165 |
. . . . . . . . 9
β’ (((π β§ π β β+) β§ (π β π β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)))) β (absβ(β«π((πΉβπ)βπ₯) dπ₯ β β«π(πΊβπ₯) dπ₯)) < π) |
108 | 107 | expr 456 |
. . . . . . . 8
β’ (((π β§ π β β+) β§ π β π) β (βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)) β (absβ(β«π((πΉβπ)βπ₯) dπ₯ β β«π(πΊβπ₯) dπ₯)) < π)) |
109 | 34, 108 | sylan2 592 |
. . . . . . 7
β’ (((π β§ π β β+) β§ (π β π β§ π β (β€β₯βπ))) β (βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)) β (absβ(β«π((πΉβπ)βπ₯) dπ₯ β β«π(πΊβπ₯) dπ₯)) < π)) |
110 | 109 | anassrs 467 |
. . . . . 6
β’ ((((π β§ π β β+) β§ π β π) β§ π β (β€β₯βπ)) β (βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)) β (absβ(β«π((πΉβπ)βπ₯) dπ₯ β β«π(πΊβπ₯) dπ₯)) < π)) |
111 | 110 | ralimdva 3161 |
. . . . 5
β’ (((π β§ π β β+) β§ π β π) β (βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)) β βπ β (β€β₯βπ)(absβ(β«π((πΉβπ)βπ₯) dπ₯ β β«π(πΊβπ₯) dπ₯)) < π)) |
112 | 111 | reximdva 3162 |
. . . 4
β’ ((π β§ π β β+) β
(βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < (π / ((volβπ) + 1)) β βπ β π βπ β (β€β₯βπ)(absβ(β«π((πΉβπ)βπ₯) dπ₯ β β«π(πΊβπ₯) dπ₯)) < π)) |
113 | 33, 112 | mpd 15 |
. . 3
β’ ((π β§ π β β+) β
βπ β π βπ β (β€β₯βπ)(absβ(β«π((πΉβπ)βπ₯) dπ₯ β β«π(πΊβπ₯) dπ₯)) < π) |
114 | 113 | ralrimiva 3140 |
. 2
β’ (π β βπ β β+ βπ β π βπ β (β€β₯βπ)(absβ(β«π((πΉβπ)βπ₯) dπ₯ β β«π(πΊβπ₯) dπ₯)) < π) |
115 | 1 | fvexi 6898 |
. . . . 5
β’ π β V |
116 | 115 | mptex 7219 |
. . . 4
β’ (π β π β¦ β«π((πΉβπ)βπ₯) dπ₯) β V |
117 | 116 | a1i 11 |
. . 3
β’ (π β (π β π β¦ β«π((πΉβπ)βπ₯) dπ₯) β V) |
118 | | fveq2 6884 |
. . . . . . . 8
β’ (π = π β (πΉβπ) = (πΉβπ)) |
119 | 118 | fveq1d 6886 |
. . . . . . 7
β’ (π = π β ((πΉβπ)βπ₯) = ((πΉβπ)βπ₯)) |
120 | 119 | adantr 480 |
. . . . . 6
β’ ((π = π β§ π₯ β π) β ((πΉβπ)βπ₯) = ((πΉβπ)βπ₯)) |
121 | 120 | itgeq2dv 25662 |
. . . . 5
β’ (π = π β β«π((πΉβπ)βπ₯) dπ₯ = β«π((πΉβπ)βπ₯) dπ₯) |
122 | | eqid 2726 |
. . . . 5
β’ (π β π β¦ β«π((πΉβπ)βπ₯) dπ₯) = (π β π β¦ β«π((πΉβπ)βπ₯) dπ₯) |
123 | | itgex 25651 |
. . . . 5
β’
β«π((πΉβπ)βπ₯) dπ₯ β V |
124 | 121, 122,
123 | fvmpt 6991 |
. . . 4
β’ (π β π β ((π β π β¦ β«π((πΉβπ)βπ₯) dπ₯)βπ) = β«π((πΉβπ)βπ₯) dπ₯) |
125 | 124 | adantl 481 |
. . 3
β’ ((π β§ π β π) β ((π β π β¦ β«π((πΉβπ)βπ₯) dπ₯)βπ) = β«π((πΉβπ)βπ₯) dπ₯) |
126 | 46, 49 | itgcl 25664 |
. . 3
β’ (π β β«π(πΊβπ₯) dπ₯ β β) |
127 | 38, 43 | itgcl 25664 |
. . 3
β’ ((π β§ π β π) β β«π((πΉβπ)βπ₯) dπ₯ β β) |
128 | 1, 2, 117, 125, 126, 127 | clim2c 15453 |
. 2
β’ (π β ((π β π β¦ β«π((πΉβπ)βπ₯) dπ₯) β β«π(πΊβπ₯) dπ₯ β βπ β β+ βπ β π βπ β (β€β₯βπ)(absβ(β«π((πΉβπ)βπ₯) dπ₯ β β«π(πΊβπ₯) dπ₯)) < π)) |
129 | 114, 128 | mpbird 257 |
1
β’ (π β (π β π β¦ β«π((πΉβπ)βπ₯) dπ₯) β β«π(πΊβπ₯) dπ₯) |