Step | Hyp | Ref
| Expression |
1 | | nnuz 12813 |
. 2
β’ β =
(β€β₯β1) |
2 | | 1zzd 12541 |
. 2
β’ (π β 1 β
β€) |
3 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π₯ β β) β π₯ β β) |
4 | | readdcl 11141 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β β§ π¦ β β) β (π₯ + π¦) β β) |
5 | 4 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ (π₯ β β β§ π¦ β β)) β (π₯ + π¦) β β) |
6 | | itg2mono.3 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (πΉβπ):ββΆ(0[,)+β)) |
7 | | rge0ssre 13380 |
. . . . . . . . . . . . . . . 16
β’
(0[,)+β) β β |
8 | | fss 6690 |
. . . . . . . . . . . . . . . 16
β’ (((πΉβπ):ββΆ(0[,)+β) β§
(0[,)+β) β β) β (πΉβπ):ββΆβ) |
9 | 6, 7, 8 | sylancl 587 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (πΉβπ):ββΆβ) |
10 | | itg2mono.8 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π» β dom
β«1) |
11 | | itg2mono.7 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β (0(,)1)) |
12 | | 0xr 11209 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 0 β
β* |
13 | | 1xr 11221 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 1 β
β* |
14 | | elioo2 13312 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((0
β β* β§ 1 β β*) β (π β (0(,)1) β (π β β β§ 0 <
π β§ π < 1))) |
15 | 12, 13, 14 | mp2an 691 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (0(,)1) β (π β β β§ 0 <
π β§ π < 1)) |
16 | 11, 15 | sylib 217 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π β β β§ 0 < π β§ π < 1)) |
17 | 16 | simp1d 1143 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β β) |
18 | 17 | renegcld 11589 |
. . . . . . . . . . . . . . . . . 18
β’ (π β -π β β) |
19 | 10, 18 | i1fmulc 25084 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((β Γ {-π}) βf Β·
π») β dom
β«1) |
20 | 19 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β ((β Γ
{-π}) βf
Β· π») β dom
β«1) |
21 | | i1ff 25056 |
. . . . . . . . . . . . . . . 16
β’
(((β Γ {-π}) βf Β· π») β dom β«1
β ((β Γ {-π}) βf Β· π»):ββΆβ) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β ((β Γ
{-π}) βf
Β· π»):ββΆβ) |
23 | | reex 11149 |
. . . . . . . . . . . . . . . 16
β’ β
β V |
24 | 23 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β β β
V) |
25 | | inidm 4183 |
. . . . . . . . . . . . . . 15
β’ (β
β© β) = β |
26 | 5, 9, 22, 24, 24, 25 | off 7640 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β ((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»)):ββΆβ) |
27 | 26 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π₯ β β) β ((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»)):ββΆβ) |
28 | 27 | ffnd 6674 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π₯ β β) β ((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»)) Fn
β) |
29 | | elpreima 7013 |
. . . . . . . . . . . 12
β’ (((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»)) Fn β
β (π₯ β (β‘((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»)) β
(-β(,)0)) β (π₯
β β β§ (((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»))βπ₯) β
(-β(,)0)))) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π₯ β β) β (π₯ β (β‘((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»)) β
(-β(,)0)) β (π₯
β β β§ (((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»))βπ₯) β
(-β(,)0)))) |
31 | 3, 30 | mpbirand 706 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π₯ β β) β (π₯ β (β‘((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»)) β
(-β(,)0)) β (((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»))βπ₯) β
(-β(,)0))) |
32 | | elioomnf 13368 |
. . . . . . . . . . . 12
β’ (0 β
β* β ((((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»))βπ₯) β (-β(,)0) β
((((πΉβπ) βf +
((β Γ {-π})
βf Β· π»))βπ₯) β β β§ (((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»))βπ₯) < 0))) |
33 | 12, 32 | ax-mp 5 |
. . . . . . . . . . 11
β’ ((((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»))βπ₯) β (-β(,)0) β
((((πΉβπ) βf +
((β Γ {-π})
βf Β· π»))βπ₯) β β β§ (((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»))βπ₯) < 0)) |
34 | 26 | ffvelcdmda 7040 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π₯ β β) β (((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»))βπ₯) β
β) |
35 | 34 | biantrurd 534 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π₯ β β) β ((((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»))βπ₯) < 0 β ((((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»))βπ₯) β β β§ (((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»))βπ₯) < 0))) |
36 | 33, 35 | bitr4id 290 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π₯ β β) β ((((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»))βπ₯) β (-β(,)0) β
(((πΉβπ) βf +
((β Γ {-π})
βf Β· π»))βπ₯) < 0)) |
37 | 6 | ffnd 6674 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (πΉβπ) Fn β) |
38 | 22 | ffnd 6674 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β ((β Γ
{-π}) βf
Β· π») Fn
β) |
39 | | eqidd 2738 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π₯ β β) β ((πΉβπ)βπ₯) = ((πΉβπ)βπ₯)) |
40 | 18 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β -π β β) |
41 | | i1ff 25056 |
. . . . . . . . . . . . . . . . . . 19
β’ (π» β dom β«1
β π»:ββΆβ) |
42 | 10, 41 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π»:ββΆβ) |
43 | 42 | ffnd 6674 |
. . . . . . . . . . . . . . . . 17
β’ (π β π» Fn β) |
44 | 43 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β π» Fn β) |
45 | | eqidd 2738 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ π₯ β β) β (π»βπ₯) = (π»βπ₯)) |
46 | 24, 40, 44, 45 | ofc1 7648 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π₯ β β) β (((β Γ
{-π}) βf
Β· π»)βπ₯) = (-π Β· (π»βπ₯))) |
47 | 17 | recnd 11190 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β β) |
48 | 47 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ π₯ β β) β π β β) |
49 | 42 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β β) β (π»βπ₯) β β) |
50 | 49 | adantlr 714 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ π₯ β β) β (π»βπ₯) β β) |
51 | 50 | recnd 11190 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ π₯ β β) β (π»βπ₯) β β) |
52 | 48, 51 | mulneg1d 11615 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π₯ β β) β (-π Β· (π»βπ₯)) = -(π Β· (π»βπ₯))) |
53 | 46, 52 | eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π₯ β β) β (((β Γ
{-π}) βf
Β· π»)βπ₯) = -(π Β· (π»βπ₯))) |
54 | 37, 38, 24, 24, 25, 39, 53 | ofval 7633 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π₯ β β) β (((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»))βπ₯) = (((πΉβπ)βπ₯) + -(π Β· (π»βπ₯)))) |
55 | 9 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π₯ β β) β ((πΉβπ)βπ₯) β β) |
56 | 55 | recnd 11190 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π₯ β β) β ((πΉβπ)βπ₯) β β) |
57 | 17 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β β) β π β β) |
58 | 57, 49 | remulcld 11192 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β β) β (π Β· (π»βπ₯)) β β) |
59 | 58 | adantlr 714 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π₯ β β) β (π Β· (π»βπ₯)) β β) |
60 | 59 | recnd 11190 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π₯ β β) β (π Β· (π»βπ₯)) β β) |
61 | 56, 60 | negsubd 11525 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π₯ β β) β (((πΉβπ)βπ₯) + -(π Β· (π»βπ₯))) = (((πΉβπ)βπ₯) β (π Β· (π»βπ₯)))) |
62 | 54, 61 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π₯ β β) β (((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»))βπ₯) = (((πΉβπ)βπ₯) β (π Β· (π»βπ₯)))) |
63 | 62 | breq1d 5120 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π₯ β β) β ((((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»))βπ₯) < 0 β (((πΉβπ)βπ₯) β (π Β· (π»βπ₯))) < 0)) |
64 | | 0red 11165 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π₯ β β) β 0 β
β) |
65 | 55, 59, 64 | ltsubaddd 11758 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π₯ β β) β ((((πΉβπ)βπ₯) β (π Β· (π»βπ₯))) < 0 β ((πΉβπ)βπ₯) < (0 + (π Β· (π»βπ₯))))) |
66 | 60 | addid2d 11363 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π₯ β β) β (0 + (π Β· (π»βπ₯))) = (π Β· (π»βπ₯))) |
67 | 66 | breq2d 5122 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π₯ β β) β (((πΉβπ)βπ₯) < (0 + (π Β· (π»βπ₯))) β ((πΉβπ)βπ₯) < (π Β· (π»βπ₯)))) |
68 | 63, 65, 67 | 3bitrd 305 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π₯ β β) β ((((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»))βπ₯) < 0 β ((πΉβπ)βπ₯) < (π Β· (π»βπ₯)))) |
69 | 31, 36, 68 | 3bitrd 305 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π₯ β β) β (π₯ β (β‘((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»)) β
(-β(,)0)) β ((πΉβπ)βπ₯) < (π Β· (π»βπ₯)))) |
70 | 69 | notbid 318 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π₯ β β) β (Β¬ π₯ β (β‘((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»)) β
(-β(,)0)) β Β¬ ((πΉβπ)βπ₯) < (π Β· (π»βπ₯)))) |
71 | | eldif 3925 |
. . . . . . . . . 10
β’ (π₯ β (β β (β‘((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»)) β
(-β(,)0))) β (π₯
β β β§ Β¬ π₯ β (β‘((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»)) β
(-β(,)0)))) |
72 | 71 | baib 537 |
. . . . . . . . 9
β’ (π₯ β β β (π₯ β (β β (β‘((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»)) β
(-β(,)0))) β Β¬ π₯ β (β‘((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»)) β
(-β(,)0)))) |
73 | 72 | adantl 483 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π₯ β β) β (π₯ β (β β (β‘((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»)) β
(-β(,)0))) β Β¬ π₯ β (β‘((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»)) β
(-β(,)0)))) |
74 | 59, 55 | lenltd 11308 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π₯ β β) β ((π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯) β Β¬ ((πΉβπ)βπ₯) < (π Β· (π»βπ₯)))) |
75 | 70, 73, 74 | 3bitr4d 311 |
. . . . . . 7
β’ (((π β§ π β β) β§ π₯ β β) β (π₯ β (β β (β‘((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»)) β
(-β(,)0))) β (π
Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯))) |
76 | 75 | rabbi2dva 4182 |
. . . . . 6
β’ ((π β§ π β β) β (β β©
(β β (β‘((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»)) β
(-β(,)0)))) = {π₯
β β β£ (π
Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)}) |
77 | | rembl 24920 |
. . . . . . 7
β’ β
β dom vol |
78 | | itg2mono.2 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πΉβπ) β MblFn) |
79 | | i1fmbf 25055 |
. . . . . . . . . . 11
β’
(((β Γ {-π}) βf Β· π») β dom β«1
β ((β Γ {-π}) βf Β· π») β MblFn) |
80 | 20, 79 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((β Γ
{-π}) βf
Β· π») β
MblFn) |
81 | 78, 80 | mbfadd 25041 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»)) β
MblFn) |
82 | | mbfima 25010 |
. . . . . . . . 9
β’ ((((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»)) β MblFn
β§ ((πΉβπ) βf +
((β Γ {-π})
βf Β· π»)):ββΆβ) β (β‘((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»)) β
(-β(,)0)) β dom vol) |
83 | 81, 26, 82 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π β β) β (β‘((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»)) β
(-β(,)0)) β dom vol) |
84 | | cmmbl 24914 |
. . . . . . . 8
β’ ((β‘((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»)) β
(-β(,)0)) β dom vol β (β β (β‘((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»)) β
(-β(,)0))) β dom vol) |
85 | 83, 84 | syl 17 |
. . . . . . 7
β’ ((π β§ π β β) β (β β
(β‘((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»)) β
(-β(,)0))) β dom vol) |
86 | | inmbl 24922 |
. . . . . . 7
β’ ((β
β dom vol β§ (β β (β‘((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»)) β
(-β(,)0))) β dom vol) β (β β© (β β (β‘((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»)) β
(-β(,)0)))) β dom vol) |
87 | 77, 85, 86 | sylancr 588 |
. . . . . 6
β’ ((π β§ π β β) β (β β©
(β β (β‘((πΉβπ) βf + ((β Γ
{-π}) βf
Β· π»)) β
(-β(,)0)))) β dom vol) |
88 | 76, 87 | eqeltrrd 2839 |
. . . . 5
β’ ((π β§ π β β) β {π₯ β β β£ (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)} β dom vol) |
89 | | itg2mono.11 |
. . . . 5
β’ π΄ = (π β β β¦ {π₯ β β β£ (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)}) |
90 | 88, 89 | fmptd 7067 |
. . . 4
β’ (π β π΄:ββΆdom vol) |
91 | | itg2mono.4 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (πΉβπ) βr β€ (πΉβ(π + 1))) |
92 | 91 | ralrimiva 3144 |
. . . . . . . . . . 11
β’ (π β βπ β β (πΉβπ) βr β€ (πΉβ(π + 1))) |
93 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π = π β (πΉβπ) = (πΉβπ)) |
94 | | fvoveq1 7385 |
. . . . . . . . . . . . 13
β’ (π = π β (πΉβ(π + 1)) = (πΉβ(π + 1))) |
95 | 93, 94 | breq12d 5123 |
. . . . . . . . . . . 12
β’ (π = π β ((πΉβπ) βr β€ (πΉβ(π + 1)) β (πΉβπ) βr β€ (πΉβ(π + 1)))) |
96 | 95 | cbvralvw 3228 |
. . . . . . . . . . 11
β’
(βπ β
β (πΉβπ) βr β€
(πΉβ(π + 1)) β βπ β β (πΉβπ) βr β€ (πΉβ(π + 1))) |
97 | 92, 96 | sylib 217 |
. . . . . . . . . 10
β’ (π β βπ β β (πΉβπ) βr β€ (πΉβ(π + 1))) |
98 | 97 | r19.21bi 3237 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πΉβπ) βr β€ (πΉβ(π + 1))) |
99 | 6 | ralrimiva 3144 |
. . . . . . . . . . . . 13
β’ (π β βπ β β (πΉβπ):ββΆ(0[,)+β)) |
100 | 93 | feq1d 6658 |
. . . . . . . . . . . . . 14
β’ (π = π β ((πΉβπ):ββΆ(0[,)+β) β (πΉβπ):ββΆ(0[,)+β))) |
101 | 100 | cbvralvw 3228 |
. . . . . . . . . . . . 13
β’
(βπ β
β (πΉβπ):ββΆ(0[,)+β)
β βπ β
β (πΉβπ):ββΆ(0[,)+β)) |
102 | 99, 101 | sylib 217 |
. . . . . . . . . . . 12
β’ (π β βπ β β (πΉβπ):ββΆ(0[,)+β)) |
103 | 102 | r19.21bi 3237 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (πΉβπ):ββΆ(0[,)+β)) |
104 | 103 | ffnd 6674 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πΉβπ) Fn β) |
105 | | peano2nn 12172 |
. . . . . . . . . . . 12
β’ (π β β β (π + 1) β
β) |
106 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π = (π + 1) β (πΉβπ) = (πΉβ(π + 1))) |
107 | 106 | feq1d 6658 |
. . . . . . . . . . . . 13
β’ (π = (π + 1) β ((πΉβπ):ββΆ(0[,)+β) β (πΉβ(π +
1)):ββΆ(0[,)+β))) |
108 | 107 | rspccva 3583 |
. . . . . . . . . . . 12
β’
((βπ β
β (πΉβπ):ββΆ(0[,)+β)
β§ (π + 1) β
β) β (πΉβ(π +
1)):ββΆ(0[,)+β)) |
109 | 99, 105, 108 | syl2an 597 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (πΉβ(π +
1)):ββΆ(0[,)+β)) |
110 | 109 | ffnd 6674 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πΉβ(π + 1)) Fn β) |
111 | 23 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β β) β β β
V) |
112 | | eqidd 2738 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π₯ β β) β ((πΉβπ)βπ₯) = ((πΉβπ)βπ₯)) |
113 | | eqidd 2738 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π₯ β β) β ((πΉβ(π + 1))βπ₯) = ((πΉβ(π + 1))βπ₯)) |
114 | 104, 110,
111, 111, 25, 112, 113 | ofrfval 7632 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((πΉβπ) βr β€ (πΉβ(π + 1)) β βπ₯ β β ((πΉβπ)βπ₯) β€ ((πΉβ(π + 1))βπ₯))) |
115 | 98, 114 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ π β β) β βπ₯ β β ((πΉβπ)βπ₯) β€ ((πΉβ(π + 1))βπ₯)) |
116 | 115 | r19.21bi 3237 |
. . . . . . 7
β’ (((π β§ π β β) β§ π₯ β β) β ((πΉβπ)βπ₯) β€ ((πΉβ(π + 1))βπ₯)) |
117 | 17 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π₯ β β) β π β β) |
118 | 42 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β β) β π»:ββΆβ) |
119 | 118 | ffvelcdmda 7040 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π₯ β β) β (π»βπ₯) β β) |
120 | 117, 119 | remulcld 11192 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π₯ β β) β (π Β· (π»βπ₯)) β β) |
121 | | fss 6690 |
. . . . . . . . . 10
β’ (((πΉβπ):ββΆ(0[,)+β) β§
(0[,)+β) β β) β (πΉβπ):ββΆβ) |
122 | 103, 7, 121 | sylancl 587 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πΉβπ):ββΆβ) |
123 | 122 | ffvelcdmda 7040 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π₯ β β) β ((πΉβπ)βπ₯) β β) |
124 | | fss 6690 |
. . . . . . . . . 10
β’ (((πΉβ(π + 1)):ββΆ(0[,)+β) β§
(0[,)+β) β β) β (πΉβ(π +
1)):ββΆβ) |
125 | 109, 7, 124 | sylancl 587 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πΉβ(π +
1)):ββΆβ) |
126 | 125 | ffvelcdmda 7040 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π₯ β β) β ((πΉβ(π + 1))βπ₯) β β) |
127 | | letr 11256 |
. . . . . . . 8
β’ (((π Β· (π»βπ₯)) β β β§ ((πΉβπ)βπ₯) β β β§ ((πΉβ(π + 1))βπ₯) β β) β (((π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯) β§ ((πΉβπ)βπ₯) β€ ((πΉβ(π + 1))βπ₯)) β (π Β· (π»βπ₯)) β€ ((πΉβ(π + 1))βπ₯))) |
128 | 120, 123,
126, 127 | syl3anc 1372 |
. . . . . . 7
β’ (((π β§ π β β) β§ π₯ β β) β (((π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯) β§ ((πΉβπ)βπ₯) β€ ((πΉβ(π + 1))βπ₯)) β (π Β· (π»βπ₯)) β€ ((πΉβ(π + 1))βπ₯))) |
129 | 116, 128 | mpan2d 693 |
. . . . . 6
β’ (((π β§ π β β) β§ π₯ β β) β ((π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯) β (π Β· (π»βπ₯)) β€ ((πΉβ(π + 1))βπ₯))) |
130 | 129 | ss2rabdv 4038 |
. . . . 5
β’ ((π β§ π β β) β {π₯ β β β£ (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)} β {π₯ β β β£ (π Β· (π»βπ₯)) β€ ((πΉβ(π + 1))βπ₯)}) |
131 | 93 | fveq1d 6849 |
. . . . . . . . 9
β’ (π = π β ((πΉβπ)βπ₯) = ((πΉβπ)βπ₯)) |
132 | 131 | breq2d 5122 |
. . . . . . . 8
β’ (π = π β ((π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯) β (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯))) |
133 | 132 | rabbidv 3418 |
. . . . . . 7
β’ (π = π β {π₯ β β β£ (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)} = {π₯ β β β£ (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)}) |
134 | 23 | rabex 5294 |
. . . . . . 7
β’ {π₯ β β β£ (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)} β V |
135 | 133, 89, 134 | fvmpt 6953 |
. . . . . 6
β’ (π β β β (π΄βπ) = {π₯ β β β£ (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)}) |
136 | 135 | adantl 483 |
. . . . 5
β’ ((π β§ π β β) β (π΄βπ) = {π₯ β β β£ (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)}) |
137 | 105 | adantl 483 |
. . . . . 6
β’ ((π β§ π β β) β (π + 1) β β) |
138 | 106 | fveq1d 6849 |
. . . . . . . . 9
β’ (π = (π + 1) β ((πΉβπ)βπ₯) = ((πΉβ(π + 1))βπ₯)) |
139 | 138 | breq2d 5122 |
. . . . . . . 8
β’ (π = (π + 1) β ((π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯) β (π Β· (π»βπ₯)) β€ ((πΉβ(π + 1))βπ₯))) |
140 | 139 | rabbidv 3418 |
. . . . . . 7
β’ (π = (π + 1) β {π₯ β β β£ (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)} = {π₯ β β β£ (π Β· (π»βπ₯)) β€ ((πΉβ(π + 1))βπ₯)}) |
141 | 23 | rabex 5294 |
. . . . . . 7
β’ {π₯ β β β£ (π Β· (π»βπ₯)) β€ ((πΉβ(π + 1))βπ₯)} β V |
142 | 140, 89, 141 | fvmpt 6953 |
. . . . . 6
β’ ((π + 1) β β β
(π΄β(π + 1)) = {π₯ β β β£ (π Β· (π»βπ₯)) β€ ((πΉβ(π + 1))βπ₯)}) |
143 | 137, 142 | syl 17 |
. . . . 5
β’ ((π β§ π β β) β (π΄β(π + 1)) = {π₯ β β β£ (π Β· (π»βπ₯)) β€ ((πΉβ(π + 1))βπ₯)}) |
144 | 130, 136,
143 | 3sstr4d 3996 |
. . . 4
β’ ((π β§ π β β) β (π΄βπ) β (π΄β(π + 1))) |
145 | 58 | adantrr 716 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β β β§ 0 < (π»βπ₯))) β (π Β· (π»βπ₯)) β β) |
146 | 49 | adantrr 716 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β β β§ 0 < (π»βπ₯))) β (π»βπ₯) β β) |
147 | 55 | an32s 651 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β β) β§ π β β) β ((πΉβπ)βπ₯) β β) |
148 | 147 | fmpttd 7068 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β β) β (π β β β¦ ((πΉβπ)βπ₯)):ββΆβ) |
149 | 148 | frnd 6681 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β β) β ran (π β β β¦ ((πΉβπ)βπ₯)) β β) |
150 | | 1nn 12171 |
. . . . . . . . . . . . . . . . . . 19
β’ 1 β
β |
151 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β¦ ((πΉβπ)βπ₯)) = (π β β β¦ ((πΉβπ)βπ₯)) |
152 | 151, 147 | dmmptd 6651 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β β) β dom (π β β β¦ ((πΉβπ)βπ₯)) = β) |
153 | 150, 152 | eleqtrrid 2845 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β β) β 1 β dom (π β β β¦ ((πΉβπ)βπ₯))) |
154 | 153 | ne0d 4300 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β β) β dom (π β β β¦ ((πΉβπ)βπ₯)) β β
) |
155 | | dm0rn0 5885 |
. . . . . . . . . . . . . . . . . 18
β’ (dom
(π β β β¦
((πΉβπ)βπ₯)) = β
β ran (π β β β¦ ((πΉβπ)βπ₯)) = β
) |
156 | 155 | necon3bii 2997 |
. . . . . . . . . . . . . . . . 17
β’ (dom
(π β β β¦
((πΉβπ)βπ₯)) β β
β ran (π β β β¦ ((πΉβπ)βπ₯)) β β
) |
157 | 154, 156 | sylib 217 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β β) β ran (π β β β¦ ((πΉβπ)βπ₯)) β β
) |
158 | | itg2mono.5 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β β) β βπ¦ β β βπ β β ((πΉβπ)βπ₯) β€ π¦) |
159 | 148 | ffnd 6674 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β β) β (π β β β¦ ((πΉβπ)βπ₯)) Fn β) |
160 | | breq1 5113 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π§ = ((π β β β¦ ((πΉβπ)βπ₯))βπ) β (π§ β€ π¦ β ((π β β β¦ ((πΉβπ)βπ₯))βπ) β€ π¦)) |
161 | 160 | ralrn 7043 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β¦ ((πΉβπ)βπ₯)) Fn β β (βπ§ β ran (π β β β¦ ((πΉβπ)βπ₯))π§ β€ π¦ β βπ β β ((π β β β¦ ((πΉβπ)βπ₯))βπ) β€ π¦)) |
162 | 159, 161 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β β) β (βπ§ β ran (π β β β¦ ((πΉβπ)βπ₯))π§ β€ π¦ β βπ β β ((π β β β¦ ((πΉβπ)βπ₯))βπ) β€ π¦)) |
163 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = π β (πΉβπ) = (πΉβπ)) |
164 | 163 | fveq1d 6849 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β ((πΉβπ)βπ₯) = ((πΉβπ)βπ₯)) |
165 | | fvex 6860 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((πΉβπ)βπ₯) β V |
166 | 164, 151,
165 | fvmpt 6953 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β β ((π β β β¦ ((πΉβπ)βπ₯))βπ) = ((πΉβπ)βπ₯)) |
167 | 166 | breq1d 5120 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β (((π β β β¦ ((πΉβπ)βπ₯))βπ) β€ π¦ β ((πΉβπ)βπ₯) β€ π¦)) |
168 | 167 | ralbiia 3095 |
. . . . . . . . . . . . . . . . . . . 20
β’
(βπ β
β ((π β β
β¦ ((πΉβπ)βπ₯))βπ) β€ π¦ β βπ β β ((πΉβπ)βπ₯) β€ π¦) |
169 | 164 | breq1d 5120 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (((πΉβπ)βπ₯) β€ π¦ β ((πΉβπ)βπ₯) β€ π¦)) |
170 | 169 | cbvralvw 3228 |
. . . . . . . . . . . . . . . . . . . 20
β’
(βπ β
β ((πΉβπ)βπ₯) β€ π¦ β βπ β β ((πΉβπ)βπ₯) β€ π¦) |
171 | 168, 170 | bitr4i 278 |
. . . . . . . . . . . . . . . . . . 19
β’
(βπ β
β ((π β β
β¦ ((πΉβπ)βπ₯))βπ) β€ π¦ β βπ β β ((πΉβπ)βπ₯) β€ π¦) |
172 | 162, 171 | bitrdi 287 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β β) β (βπ§ β ran (π β β β¦ ((πΉβπ)βπ₯))π§ β€ π¦ β βπ β β ((πΉβπ)βπ₯) β€ π¦)) |
173 | 172 | rexbidv 3176 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β β) β (βπ¦ β β βπ§ β ran (π β β β¦ ((πΉβπ)βπ₯))π§ β€ π¦ β βπ¦ β β βπ β β ((πΉβπ)βπ₯) β€ π¦)) |
174 | 158, 173 | mpbird 257 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β β) β βπ¦ β β βπ§ β ran (π β β β¦ ((πΉβπ)βπ₯))π§ β€ π¦) |
175 | 149, 157,
174 | suprcld 12125 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β β) β sup(ran (π β β β¦ ((πΉβπ)βπ₯)), β, < ) β
β) |
176 | 175 | adantrr 716 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β β β§ 0 < (π»βπ₯))) β sup(ran (π β β β¦ ((πΉβπ)βπ₯)), β, < ) β
β) |
177 | 16 | simp3d 1145 |
. . . . . . . . . . . . . . . . 17
β’ (π β π < 1) |
178 | 177 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π₯ β β β§ 0 < (π»βπ₯))) β π < 1) |
179 | 17 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π₯ β β β§ 0 < (π»βπ₯))) β π β β) |
180 | | 1red 11163 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π₯ β β β§ 0 < (π»βπ₯))) β 1 β β) |
181 | | simprr 772 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π₯ β β β§ 0 < (π»βπ₯))) β 0 < (π»βπ₯)) |
182 | | ltmul1 12012 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ 1 β
β β§ ((π»βπ₯) β β β§ 0 < (π»βπ₯))) β (π < 1 β (π Β· (π»βπ₯)) < (1 Β· (π»βπ₯)))) |
183 | 179, 180,
146, 181, 182 | syl112anc 1375 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π₯ β β β§ 0 < (π»βπ₯))) β (π < 1 β (π Β· (π»βπ₯)) < (1 Β· (π»βπ₯)))) |
184 | 178, 183 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β β β§ 0 < (π»βπ₯))) β (π Β· (π»βπ₯)) < (1 Β· (π»βπ₯))) |
185 | 146 | recnd 11190 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π₯ β β β§ 0 < (π»βπ₯))) β (π»βπ₯) β β) |
186 | 185 | mulid2d 11180 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β β β§ 0 < (π»βπ₯))) β (1 Β· (π»βπ₯)) = (π»βπ₯)) |
187 | 184, 186 | breqtrd 5136 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β β β§ 0 < (π»βπ₯))) β (π Β· (π»βπ₯)) < (π»βπ₯)) |
188 | | itg2mono.9 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π» βr β€ πΊ) |
189 | | itg2mono.1 |
. . . . . . . . . . . . . . . . . . . . 21
β’ πΊ = (π₯ β β β¦ sup(ran (π β β β¦ ((πΉβπ)βπ₯)), β, < )) |
190 | 175, 189 | fmptd 7067 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β πΊ:ββΆβ) |
191 | 190 | ffnd 6674 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΊ Fn β) |
192 | 23 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β
V) |
193 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π¦ β β) β (π»βπ¦) = (π»βπ¦)) |
194 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π₯ = π¦ β ((πΉβπ)βπ₯) = ((πΉβπ)βπ¦)) |
195 | 194 | mpteq2dv 5212 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ = π¦ β (π β β β¦ ((πΉβπ)βπ₯)) = (π β β β¦ ((πΉβπ)βπ¦))) |
196 | 195 | rneqd 5898 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ = π¦ β ran (π β β β¦ ((πΉβπ)βπ₯)) = ran (π β β β¦ ((πΉβπ)βπ¦))) |
197 | 196 | supeq1d 9389 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π¦ β sup(ran (π β β β¦ ((πΉβπ)βπ₯)), β, < ) = sup(ran (π β β β¦ ((πΉβπ)βπ¦)), β, < )) |
198 | | ltso 11242 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ < Or
β |
199 | 198 | supex 9406 |
. . . . . . . . . . . . . . . . . . . . 21
β’ sup(ran
(π β β β¦
((πΉβπ)βπ¦)), β, < ) β V |
200 | 197, 189,
199 | fvmpt 6953 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ β β β (πΊβπ¦) = sup(ran (π β β β¦ ((πΉβπ)βπ¦)), β, < )) |
201 | 200 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π¦ β β) β (πΊβπ¦) = sup(ran (π β β β¦ ((πΉβπ)βπ¦)), β, < )) |
202 | 43, 191, 192, 192, 25, 193, 201 | ofrfval 7632 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π» βr β€ πΊ β βπ¦ β β (π»βπ¦) β€ sup(ran (π β β β¦ ((πΉβπ)βπ¦)), β, < ))) |
203 | 188, 202 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’ (π β βπ¦ β β (π»βπ¦) β€ sup(ran (π β β β¦ ((πΉβπ)βπ¦)), β, < )) |
204 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = π¦ β (π»βπ₯) = (π»βπ¦)) |
205 | 204, 197 | breq12d 5123 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π¦ β ((π»βπ₯) β€ sup(ran (π β β β¦ ((πΉβπ)βπ₯)), β, < ) β (π»βπ¦) β€ sup(ran (π β β β¦ ((πΉβπ)βπ¦)), β, < ))) |
206 | 205 | cbvralvw 3228 |
. . . . . . . . . . . . . . . . 17
β’
(βπ₯ β
β (π»βπ₯) β€ sup(ran (π β β β¦ ((πΉβπ)βπ₯)), β, < ) β βπ¦ β β (π»βπ¦) β€ sup(ran (π β β β¦ ((πΉβπ)βπ¦)), β, < )) |
207 | 203, 206 | sylibr 233 |
. . . . . . . . . . . . . . . 16
β’ (π β βπ₯ β β (π»βπ₯) β€ sup(ran (π β β β¦ ((πΉβπ)βπ₯)), β, < )) |
208 | 207 | r19.21bi 3237 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β β) β (π»βπ₯) β€ sup(ran (π β β β¦ ((πΉβπ)βπ₯)), β, < )) |
209 | 208 | adantrr 716 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β β β§ 0 < (π»βπ₯))) β (π»βπ₯) β€ sup(ran (π β β β¦ ((πΉβπ)βπ₯)), β, < )) |
210 | 145, 146,
176, 187, 209 | ltletrd 11322 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β β β§ 0 < (π»βπ₯))) β (π Β· (π»βπ₯)) < sup(ran (π β β β¦ ((πΉβπ)βπ₯)), β, < )) |
211 | 149 | adantrr 716 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β β β§ 0 < (π»βπ₯))) β ran (π β β β¦ ((πΉβπ)βπ₯)) β β) |
212 | 157 | adantrr 716 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β β β§ 0 < (π»βπ₯))) β ran (π β β β¦ ((πΉβπ)βπ₯)) β β
) |
213 | 174 | adantrr 716 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β β β§ 0 < (π»βπ₯))) β βπ¦ β β βπ§ β ran (π β β β¦ ((πΉβπ)βπ₯))π§ β€ π¦) |
214 | | suprlub 12126 |
. . . . . . . . . . . . . 14
β’ (((ran
(π β β β¦
((πΉβπ)βπ₯)) β β β§ ran (π β β β¦ ((πΉβπ)βπ₯)) β β
β§ βπ¦ β β βπ§ β ran (π β β β¦ ((πΉβπ)βπ₯))π§ β€ π¦) β§ (π Β· (π»βπ₯)) β β) β ((π Β· (π»βπ₯)) < sup(ran (π β β β¦ ((πΉβπ)βπ₯)), β, < ) β βπ€ β ran (π β β β¦ ((πΉβπ)βπ₯))(π Β· (π»βπ₯)) < π€)) |
215 | 211, 212,
213, 145, 214 | syl31anc 1374 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β β β§ 0 < (π»βπ₯))) β ((π Β· (π»βπ₯)) < sup(ran (π β β β¦ ((πΉβπ)βπ₯)), β, < ) β βπ€ β ran (π β β β¦ ((πΉβπ)βπ₯))(π Β· (π»βπ₯)) < π€)) |
216 | 210, 215 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β β β§ 0 < (π»βπ₯))) β βπ€ β ran (π β β β¦ ((πΉβπ)βπ₯))(π Β· (π»βπ₯)) < π€) |
217 | 159 | adantrr 716 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β β β§ 0 < (π»βπ₯))) β (π β β β¦ ((πΉβπ)βπ₯)) Fn β) |
218 | | breq2 5114 |
. . . . . . . . . . . . . . 15
β’ (π€ = ((π β β β¦ ((πΉβπ)βπ₯))βπ) β ((π Β· (π»βπ₯)) < π€ β (π Β· (π»βπ₯)) < ((π β β β¦ ((πΉβπ)βπ₯))βπ))) |
219 | 218 | rexrn 7042 |
. . . . . . . . . . . . . 14
β’ ((π β β β¦ ((πΉβπ)βπ₯)) Fn β β (βπ€ β ran (π β β β¦ ((πΉβπ)βπ₯))(π Β· (π»βπ₯)) < π€ β βπ β β (π Β· (π»βπ₯)) < ((π β β β¦ ((πΉβπ)βπ₯))βπ))) |
220 | 217, 219 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β β β§ 0 < (π»βπ₯))) β (βπ€ β ran (π β β β¦ ((πΉβπ)βπ₯))(π Β· (π»βπ₯)) < π€ β βπ β β (π Β· (π»βπ₯)) < ((π β β β¦ ((πΉβπ)βπ₯))βπ))) |
221 | | fvex 6860 |
. . . . . . . . . . . . . . . 16
β’ ((πΉβπ)βπ₯) β V |
222 | 131, 151,
221 | fvmpt 6953 |
. . . . . . . . . . . . . . 15
β’ (π β β β ((π β β β¦ ((πΉβπ)βπ₯))βπ) = ((πΉβπ)βπ₯)) |
223 | 222 | breq2d 5122 |
. . . . . . . . . . . . . 14
β’ (π β β β ((π Β· (π»βπ₯)) < ((π β β β¦ ((πΉβπ)βπ₯))βπ) β (π Β· (π»βπ₯)) < ((πΉβπ)βπ₯))) |
224 | 223 | rexbiia 3096 |
. . . . . . . . . . . . 13
β’
(βπ β
β (π Β· (π»βπ₯)) < ((π β β β¦ ((πΉβπ)βπ₯))βπ) β βπ β β (π Β· (π»βπ₯)) < ((πΉβπ)βπ₯)) |
225 | 220, 224 | bitrdi 287 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β β β§ 0 < (π»βπ₯))) β (βπ€ β ran (π β β β¦ ((πΉβπ)βπ₯))(π Β· (π»βπ₯)) < π€ β βπ β β (π Β· (π»βπ₯)) < ((πΉβπ)βπ₯))) |
226 | 216, 225 | mpbid 231 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β β β§ 0 < (π»βπ₯))) β βπ β β (π Β· (π»βπ₯)) < ((πΉβπ)βπ₯)) |
227 | 179, 146 | remulcld 11192 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β β β§ 0 < (π»βπ₯))) β (π Β· (π»βπ₯)) β β) |
228 | 103 | adantlr 714 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β β) β§ π β β) β (πΉβπ):ββΆ(0[,)+β)) |
229 | | simplr 768 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β β) β§ π β β) β π₯ β β) |
230 | 228, 229 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β β) β§ π β β) β ((πΉβπ)βπ₯) β (0[,)+β)) |
231 | | elrege0 13378 |
. . . . . . . . . . . . . . . 16
β’ (((πΉβπ)βπ₯) β (0[,)+β) β (((πΉβπ)βπ₯) β β β§ 0 β€ ((πΉβπ)βπ₯))) |
232 | 230, 231 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β) β§ π β β) β (((πΉβπ)βπ₯) β β β§ 0 β€ ((πΉβπ)βπ₯))) |
233 | 232 | simpld 496 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β) β§ π β β) β ((πΉβπ)βπ₯) β β) |
234 | 233 | adantlrr 720 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β β§ 0 < (π»βπ₯))) β§ π β β) β ((πΉβπ)βπ₯) β β) |
235 | | ltle 11250 |
. . . . . . . . . . . . 13
β’ (((π Β· (π»βπ₯)) β β β§ ((πΉβπ)βπ₯) β β) β ((π Β· (π»βπ₯)) < ((πΉβπ)βπ₯) β (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯))) |
236 | 227, 234,
235 | syl2an2r 684 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β β β§ 0 < (π»βπ₯))) β§ π β β) β ((π Β· (π»βπ₯)) < ((πΉβπ)βπ₯) β (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯))) |
237 | 236 | reximdva 3166 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β β β§ 0 < (π»βπ₯))) β (βπ β β (π Β· (π»βπ₯)) < ((πΉβπ)βπ₯) β βπ β β (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯))) |
238 | 226, 237 | mpd 15 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β β β§ 0 < (π»βπ₯))) β βπ β β (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)) |
239 | 238 | anassrs 469 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ 0 < (π»βπ₯)) β βπ β β (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)) |
240 | 150 | ne0ii 4302 |
. . . . . . . . . . 11
β’ β
β β
|
241 | 58 | adantrr 716 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β β β§ (π»βπ₯) β€ 0)) β (π Β· (π»βπ₯)) β β) |
242 | 241 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β β§ (π»βπ₯) β€ 0)) β§ π β β) β (π Β· (π»βπ₯)) β β) |
243 | | 0red 11165 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β β§ (π»βπ₯) β€ 0)) β§ π β β) β 0 β
β) |
244 | 232 | adantlrr 720 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β β β§ (π»βπ₯) β€ 0)) β§ π β β) β (((πΉβπ)βπ₯) β β β§ 0 β€ ((πΉβπ)βπ₯))) |
245 | 244 | simpld 496 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β β§ (π»βπ₯) β€ 0)) β§ π β β) β ((πΉβπ)βπ₯) β β) |
246 | | simplrr 777 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β β β§ (π»βπ₯) β€ 0)) β§ π β β) β (π»βπ₯) β€ 0) |
247 | 49 | adantrr 716 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π₯ β β β§ (π»βπ₯) β€ 0)) β (π»βπ₯) β β) |
248 | 247 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β β β§ (π»βπ₯) β€ 0)) β§ π β β) β (π»βπ₯) β β) |
249 | 17 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β β β§ (π»βπ₯) β€ 0)) β§ π β β) β π β β) |
250 | 16 | simp2d 1144 |
. . . . . . . . . . . . . . . . 17
β’ (π β 0 < π) |
251 | 250 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β β β§ (π»βπ₯) β€ 0)) β§ π β β) β 0 < π) |
252 | | lemul2 12015 |
. . . . . . . . . . . . . . . 16
β’ (((π»βπ₯) β β β§ 0 β β β§
(π β β β§ 0
< π)) β ((π»βπ₯) β€ 0 β (π Β· (π»βπ₯)) β€ (π Β· 0))) |
253 | 248, 243,
249, 251, 252 | syl112anc 1375 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β β β§ (π»βπ₯) β€ 0)) β§ π β β) β ((π»βπ₯) β€ 0 β (π Β· (π»βπ₯)) β€ (π Β· 0))) |
254 | 246, 253 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β β β§ (π»βπ₯) β€ 0)) β§ π β β) β (π Β· (π»βπ₯)) β€ (π Β· 0)) |
255 | 249 | recnd 11190 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β β β§ (π»βπ₯) β€ 0)) β§ π β β) β π β β) |
256 | 255 | mul01d 11361 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β β β§ (π»βπ₯) β€ 0)) β§ π β β) β (π Β· 0) = 0) |
257 | 254, 256 | breqtrd 5136 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β β§ (π»βπ₯) β€ 0)) β§ π β β) β (π Β· (π»βπ₯)) β€ 0) |
258 | 244 | simprd 497 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β β§ (π»βπ₯) β€ 0)) β§ π β β) β 0 β€ ((πΉβπ)βπ₯)) |
259 | 242, 243,
245, 257, 258 | letrd 11319 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β β β§ (π»βπ₯) β€ 0)) β§ π β β) β (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)) |
260 | 259 | ralrimiva 3144 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β β β§ (π»βπ₯) β€ 0)) β βπ β β (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)) |
261 | | r19.2z 4457 |
. . . . . . . . . . 11
β’ ((β
β β
β§ βπ β β (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)) β βπ β β (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)) |
262 | 240, 260,
261 | sylancr 588 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β β β§ (π»βπ₯) β€ 0)) β βπ β β (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)) |
263 | 262 | anassrs 469 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ (π»βπ₯) β€ 0) β βπ β β (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)) |
264 | | 0red 11165 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β 0 β
β) |
265 | 239, 263,
264, 49 | ltlecasei 11270 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β βπ β β (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)) |
266 | 265 | ralrimiva 3144 |
. . . . . . 7
β’ (π β βπ₯ β β βπ β β (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)) |
267 | | rabid2 3439 |
. . . . . . 7
β’ (β
= {π₯ β β β£
βπ β β
(π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)} β βπ₯ β β βπ β β (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)) |
268 | 266, 267 | sylibr 233 |
. . . . . 6
β’ (π β β = {π₯ β β β£
βπ β β
(π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)}) |
269 | | iunrab 5017 |
. . . . . 6
β’ βͺ π β β {π₯ β β β£ (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)} = {π₯ β β β£ βπ β β (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)} |
270 | 268, 269 | eqtr4di 2795 |
. . . . 5
β’ (π β β = βͺ π β β {π₯ β β β£ (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)}) |
271 | 136 | iuneq2dv 4983 |
. . . . 5
β’ (π β βͺ π β β (π΄βπ) = βͺ π β β {π₯ β β β£ (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)}) |
272 | 90 | ffnd 6674 |
. . . . . 6
β’ (π β π΄ Fn β) |
273 | | fniunfv 7199 |
. . . . . 6
β’ (π΄ Fn β β βͺ π β β (π΄βπ) = βͺ ran π΄) |
274 | 272, 273 | syl 17 |
. . . . 5
β’ (π β βͺ π β β (π΄βπ) = βͺ ran π΄) |
275 | 270, 271,
274 | 3eqtr2rd 2784 |
. . . 4
β’ (π β βͺ ran π΄ = β) |
276 | | eqid 2737 |
. . . 4
β’ (π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0)) = (π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0)) |
277 | 90, 144, 275, 10, 276 | itg1climres 25095 |
. . 3
β’ (π β (π β β β¦
(β«1β(π₯
β β β¦ if(π₯
β (π΄βπ), (π»βπ₯), 0)))) β
(β«1βπ»)) |
278 | | nnex 12166 |
. . . . 5
β’ β
β V |
279 | 278 | mptex 7178 |
. . . 4
β’ (π β β β¦ (π Β·
(β«1β(π₯
β β β¦ if(π₯
β (π΄βπ), (π»βπ₯), 0))))) β V |
280 | 279 | a1i 11 |
. . 3
β’ (π β (π β β β¦ (π Β· (β«1β(π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0))))) β V) |
281 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π = π β (π΄βπ) = (π΄βπ)) |
282 | 281 | eleq2d 2824 |
. . . . . . . . . 10
β’ (π = π β (π₯ β (π΄βπ) β π₯ β (π΄βπ))) |
283 | 282 | ifbid 4514 |
. . . . . . . . 9
β’ (π = π β if(π₯ β (π΄βπ), (π»βπ₯), 0) = if(π₯ β (π΄βπ), (π»βπ₯), 0)) |
284 | 283 | mpteq2dv 5212 |
. . . . . . . 8
β’ (π = π β (π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0)) = (π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0))) |
285 | 284 | fveq2d 6851 |
. . . . . . 7
β’ (π = π β (β«1β(π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0))) = (β«1β(π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0)))) |
286 | | eqid 2737 |
. . . . . . 7
β’ (π β β β¦
(β«1β(π₯
β β β¦ if(π₯
β (π΄βπ), (π»βπ₯), 0)))) = (π β β β¦
(β«1β(π₯
β β β¦ if(π₯
β (π΄βπ), (π»βπ₯), 0)))) |
287 | | fvex 6860 |
. . . . . . 7
β’
(β«1β(π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0))) β V |
288 | 285, 286,
287 | fvmpt 6953 |
. . . . . 6
β’ (π β β β ((π β β β¦
(β«1β(π₯
β β β¦ if(π₯
β (π΄βπ), (π»βπ₯), 0))))βπ) = (β«1β(π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0)))) |
289 | 288 | adantl 483 |
. . . . 5
β’ ((π β§ π β β) β ((π β β β¦
(β«1β(π₯
β β β¦ if(π₯
β (π΄βπ), (π»βπ₯), 0))))βπ) = (β«1β(π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0)))) |
290 | 90 | ffvelcdmda 7040 |
. . . . . . 7
β’ ((π β§ π β β) β (π΄βπ) β dom vol) |
291 | | eqid 2737 |
. . . . . . . 8
β’ (π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0)) = (π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0)) |
292 | 291 | i1fres 25086 |
. . . . . . 7
β’ ((π» β dom β«1
β§ (π΄βπ) β dom vol) β (π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0)) β dom
β«1) |
293 | 10, 290, 292 | syl2an2r 684 |
. . . . . 6
β’ ((π β§ π β β) β (π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0)) β dom
β«1) |
294 | | itg1cl 25065 |
. . . . . 6
β’ ((π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0)) β dom β«1 β
(β«1β(π₯
β β β¦ if(π₯
β (π΄βπ), (π»βπ₯), 0))) β β) |
295 | 293, 294 | syl 17 |
. . . . 5
β’ ((π β§ π β β) β
(β«1β(π₯
β β β¦ if(π₯
β (π΄βπ), (π»βπ₯), 0))) β β) |
296 | 289, 295 | eqeltrd 2838 |
. . . 4
β’ ((π β§ π β β) β ((π β β β¦
(β«1β(π₯
β β β¦ if(π₯
β (π΄βπ), (π»βπ₯), 0))))βπ) β β) |
297 | 296 | recnd 11190 |
. . 3
β’ ((π β§ π β β) β ((π β β β¦
(β«1β(π₯
β β β¦ if(π₯
β (π΄βπ), (π»βπ₯), 0))))βπ) β β) |
298 | 285 | oveq2d 7378 |
. . . . . 6
β’ (π = π β (π Β· (β«1β(π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0)))) = (π Β· (β«1β(π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0))))) |
299 | | eqid 2737 |
. . . . . 6
β’ (π β β β¦ (π Β·
(β«1β(π₯
β β β¦ if(π₯
β (π΄βπ), (π»βπ₯), 0))))) = (π β β β¦ (π Β· (β«1β(π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0))))) |
300 | | ovex 7395 |
. . . . . 6
β’ (π Β·
(β«1β(π₯
β β β¦ if(π₯
β (π΄βπ), (π»βπ₯), 0)))) β V |
301 | 298, 299,
300 | fvmpt 6953 |
. . . . 5
β’ (π β β β ((π β β β¦ (π Β·
(β«1β(π₯
β β β¦ if(π₯
β (π΄βπ), (π»βπ₯), 0)))))βπ) = (π Β· (β«1β(π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0))))) |
302 | 288 | oveq2d 7378 |
. . . . 5
β’ (π β β β (π Β· ((π β β β¦
(β«1β(π₯
β β β¦ if(π₯
β (π΄βπ), (π»βπ₯), 0))))βπ)) = (π Β· (β«1β(π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0))))) |
303 | 301, 302 | eqtr4d 2780 |
. . . 4
β’ (π β β β ((π β β β¦ (π Β·
(β«1β(π₯
β β β¦ if(π₯
β (π΄βπ), (π»βπ₯), 0)))))βπ) = (π Β· ((π β β β¦
(β«1β(π₯
β β β¦ if(π₯
β (π΄βπ), (π»βπ₯), 0))))βπ))) |
304 | 303 | adantl 483 |
. . 3
β’ ((π β§ π β β) β ((π β β β¦ (π Β· (β«1β(π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0)))))βπ) = (π Β· ((π β β β¦
(β«1β(π₯
β β β¦ if(π₯
β (π΄βπ), (π»βπ₯), 0))))βπ))) |
305 | 1, 2, 277, 47, 280, 297, 304 | climmulc2 15526 |
. 2
β’ (π β (π β β β¦ (π Β· (β«1β(π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0))))) β (π Β· (β«1βπ»))) |
306 | | icossicc 13360 |
. . . . . . 7
β’
(0[,)+β) β (0[,]+β) |
307 | | fss 6690 |
. . . . . . 7
β’ (((πΉβπ):ββΆ(0[,)+β) β§
(0[,)+β) β (0[,]+β)) β (πΉβπ):ββΆ(0[,]+β)) |
308 | 6, 306, 307 | sylancl 587 |
. . . . . 6
β’ ((π β§ π β β) β (πΉβπ):ββΆ(0[,]+β)) |
309 | | itg2mono.10 |
. . . . . . 7
β’ (π β π β β) |
310 | 309 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β) β π β β) |
311 | | itg2cl 25113 |
. . . . . . . . . . 11
β’ ((πΉβπ):ββΆ(0[,]+β) β
(β«2β(πΉβπ)) β
β*) |
312 | 308, 311 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β β) β
(β«2β(πΉβπ)) β
β*) |
313 | 312 | fmpttd 7068 |
. . . . . . . . 9
β’ (π β (π β β β¦
(β«2β(πΉβπ))):ββΆβ*) |
314 | 313 | frnd 6681 |
. . . . . . . 8
β’ (π β ran (π β β β¦
(β«2β(πΉβπ))) β
β*) |
315 | | fvex 6860 |
. . . . . . . . . . 11
β’
(β«2β(πΉβπ)) β V |
316 | 315 | elabrex 7195 |
. . . . . . . . . 10
β’ (π β β β
(β«2β(πΉβπ)) β {π₯ β£ βπ β β π₯ = (β«2β(πΉβπ))}) |
317 | 316 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β β) β
(β«2β(πΉβπ)) β {π₯ β£ βπ β β π₯ = (β«2β(πΉβπ))}) |
318 | | eqid 2737 |
. . . . . . . . . 10
β’ (π β β β¦
(β«2β(πΉβπ))) = (π β β β¦
(β«2β(πΉβπ))) |
319 | 318 | rnmpt 5915 |
. . . . . . . . 9
β’ ran
(π β β β¦
(β«2β(πΉβπ))) = {π₯ β£ βπ β β π₯ = (β«2β(πΉβπ))} |
320 | 317, 319 | eleqtrrdi 2849 |
. . . . . . . 8
β’ ((π β§ π β β) β
(β«2β(πΉβπ)) β ran (π β β β¦
(β«2β(πΉβπ)))) |
321 | | supxrub 13250 |
. . . . . . . 8
β’ ((ran
(π β β β¦
(β«2β(πΉβπ))) β β* β§
(β«2β(πΉβπ)) β ran (π β β β¦
(β«2β(πΉβπ)))) β (β«2β(πΉβπ)) β€ sup(ran (π β β β¦
(β«2β(πΉβπ))), β*, <
)) |
322 | 314, 320,
321 | syl2an2r 684 |
. . . . . . 7
β’ ((π β§ π β β) β
(β«2β(πΉβπ)) β€ sup(ran (π β β β¦
(β«2β(πΉβπ))), β*, <
)) |
323 | | itg2mono.6 |
. . . . . . 7
β’ π = sup(ran (π β β β¦
(β«2β(πΉβπ))), β*, <
) |
324 | 322, 323 | breqtrrdi 5152 |
. . . . . 6
β’ ((π β§ π β β) β
(β«2β(πΉβπ)) β€ π) |
325 | | itg2lecl 25119 |
. . . . . 6
β’ (((πΉβπ):ββΆ(0[,]+β) β§ π β β β§
(β«2β(πΉβπ)) β€ π) β (β«2β(πΉβπ)) β β) |
326 | 308, 310,
324, 325 | syl3anc 1372 |
. . . . 5
β’ ((π β§ π β β) β
(β«2β(πΉβπ)) β β) |
327 | 326 | fmpttd 7068 |
. . . 4
β’ (π β (π β β β¦
(β«2β(πΉβπ))):ββΆβ) |
328 | 308 | ralrimiva 3144 |
. . . . . . . . . 10
β’ (π β βπ β β (πΉβπ):ββΆ(0[,]+β)) |
329 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π = π β (πΉβπ) = (πΉβπ)) |
330 | 329 | feq1d 6658 |
. . . . . . . . . . 11
β’ (π = π β ((πΉβπ):ββΆ(0[,]+β) β (πΉβπ):ββΆ(0[,]+β))) |
331 | 330 | cbvralvw 3228 |
. . . . . . . . . 10
β’
(βπ β
β (πΉβπ):ββΆ(0[,]+β)
β βπ β
β (πΉβπ):ββΆ(0[,]+β)) |
332 | 328, 331 | sylib 217 |
. . . . . . . . 9
β’ (π β βπ β β (πΉβπ):ββΆ(0[,]+β)) |
333 | | peano2nn 12172 |
. . . . . . . . 9
β’ (π β β β (π + 1) β
β) |
334 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π = (π + 1) β (πΉβπ) = (πΉβ(π + 1))) |
335 | 334 | feq1d 6658 |
. . . . . . . . . 10
β’ (π = (π + 1) β ((πΉβπ):ββΆ(0[,]+β) β (πΉβ(π +
1)):ββΆ(0[,]+β))) |
336 | 335 | rspccva 3583 |
. . . . . . . . 9
β’
((βπ β
β (πΉβπ):ββΆ(0[,]+β)
β§ (π + 1) β
β) β (πΉβ(π +
1)):ββΆ(0[,]+β)) |
337 | 332, 333,
336 | syl2an 597 |
. . . . . . . 8
β’ ((π β§ π β β) β (πΉβ(π +
1)):ββΆ(0[,]+β)) |
338 | | itg2le 25120 |
. . . . . . . 8
β’ (((πΉβπ):ββΆ(0[,]+β) β§ (πΉβ(π + 1)):ββΆ(0[,]+β) β§
(πΉβπ) βr β€ (πΉβ(π + 1))) β
(β«2β(πΉβπ)) β€ (β«2β(πΉβ(π + 1)))) |
339 | 308, 337,
91, 338 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ π β β) β
(β«2β(πΉβπ)) β€ (β«2β(πΉβ(π + 1)))) |
340 | 339 | ralrimiva 3144 |
. . . . . 6
β’ (π β βπ β β
(β«2β(πΉβπ)) β€ (β«2β(πΉβ(π + 1)))) |
341 | | 2fveq3 6852 |
. . . . . . . . . 10
β’ (π = π β (β«2β(πΉβπ)) = (β«2β(πΉβπ))) |
342 | | fvex 6860 |
. . . . . . . . . 10
β’
(β«2β(πΉβπ)) β V |
343 | 341, 318,
342 | fvmpt 6953 |
. . . . . . . . 9
β’ (π β β β ((π β β β¦
(β«2β(πΉβπ)))βπ) = (β«2β(πΉβπ))) |
344 | | peano2nn 12172 |
. . . . . . . . . 10
β’ (π β β β (π + 1) β
β) |
345 | | 2fveq3 6852 |
. . . . . . . . . . 11
β’ (π = (π + 1) β (β«2β(πΉβπ)) = (β«2β(πΉβ(π + 1)))) |
346 | | fvex 6860 |
. . . . . . . . . . 11
β’
(β«2β(πΉβ(π + 1))) β V |
347 | 345, 318,
346 | fvmpt 6953 |
. . . . . . . . . 10
β’ ((π + 1) β β β
((π β β β¦
(β«2β(πΉβπ)))β(π + 1)) = (β«2β(πΉβ(π + 1)))) |
348 | 344, 347 | syl 17 |
. . . . . . . . 9
β’ (π β β β ((π β β β¦
(β«2β(πΉβπ)))β(π + 1)) = (β«2β(πΉβ(π + 1)))) |
349 | 343, 348 | breq12d 5123 |
. . . . . . . 8
β’ (π β β β (((π β β β¦
(β«2β(πΉβπ)))βπ) β€ ((π β β β¦
(β«2β(πΉβπ)))β(π + 1)) β (β«2β(πΉβπ)) β€ (β«2β(πΉβ(π + 1))))) |
350 | 349 | ralbiia 3095 |
. . . . . . 7
β’
(βπ β
β ((π β β
β¦ (β«2β(πΉβπ)))βπ) β€ ((π β β β¦
(β«2β(πΉβπ)))β(π + 1)) β βπ β β
(β«2β(πΉβπ)) β€ (β«2β(πΉβ(π + 1)))) |
351 | | fvoveq1 7385 |
. . . . . . . . . 10
β’ (π = π β (πΉβ(π + 1)) = (πΉβ(π + 1))) |
352 | 351 | fveq2d 6851 |
. . . . . . . . 9
β’ (π = π β (β«2β(πΉβ(π + 1))) = (β«2β(πΉβ(π + 1)))) |
353 | 341, 352 | breq12d 5123 |
. . . . . . . 8
β’ (π = π β ((β«2β(πΉβπ)) β€ (β«2β(πΉβ(π + 1))) β
(β«2β(πΉβπ)) β€ (β«2β(πΉβ(π + 1))))) |
354 | 353 | cbvralvw 3228 |
. . . . . . 7
β’
(βπ β
β (β«2β(πΉβπ)) β€ (β«2β(πΉβ(π + 1))) β βπ β β
(β«2β(πΉβπ)) β€ (β«2β(πΉβ(π + 1)))) |
355 | 350, 354 | bitr4i 278 |
. . . . . 6
β’
(βπ β
β ((π β β
β¦ (β«2β(πΉβπ)))βπ) β€ ((π β β β¦
(β«2β(πΉβπ)))β(π + 1)) β βπ β β
(β«2β(πΉβπ)) β€ (β«2β(πΉβ(π + 1)))) |
356 | 340, 355 | sylibr 233 |
. . . . 5
β’ (π β βπ β β ((π β β β¦
(β«2β(πΉβπ)))βπ) β€ ((π β β β¦
(β«2β(πΉβπ)))β(π + 1))) |
357 | 356 | r19.21bi 3237 |
. . . 4
β’ ((π β§ π β β) β ((π β β β¦
(β«2β(πΉβπ)))βπ) β€ ((π β β β¦
(β«2β(πΉβπ)))β(π + 1))) |
358 | 324 | ralrimiva 3144 |
. . . . 5
β’ (π β βπ β β
(β«2β(πΉβπ)) β€ π) |
359 | 343 | breq1d 5120 |
. . . . . . . . 9
β’ (π β β β (((π β β β¦
(β«2β(πΉβπ)))βπ) β€ π₯ β (β«2β(πΉβπ)) β€ π₯)) |
360 | 359 | ralbiia 3095 |
. . . . . . . 8
β’
(βπ β
β ((π β β
β¦ (β«2β(πΉβπ)))βπ) β€ π₯ β βπ β β
(β«2β(πΉβπ)) β€ π₯) |
361 | 341 | breq1d 5120 |
. . . . . . . . 9
β’ (π = π β ((β«2β(πΉβπ)) β€ π₯ β (β«2β(πΉβπ)) β€ π₯)) |
362 | 361 | cbvralvw 3228 |
. . . . . . . 8
β’
(βπ β
β (β«2β(πΉβπ)) β€ π₯ β βπ β β
(β«2β(πΉβπ)) β€ π₯) |
363 | 360, 362 | bitr4i 278 |
. . . . . . 7
β’
(βπ β
β ((π β β
β¦ (β«2β(πΉβπ)))βπ) β€ π₯ β βπ β β
(β«2β(πΉβπ)) β€ π₯) |
364 | | breq2 5114 |
. . . . . . . 8
β’ (π₯ = π β ((β«2β(πΉβπ)) β€ π₯ β (β«2β(πΉβπ)) β€ π)) |
365 | 364 | ralbidv 3175 |
. . . . . . 7
β’ (π₯ = π β (βπ β β
(β«2β(πΉβπ)) β€ π₯ β βπ β β
(β«2β(πΉβπ)) β€ π)) |
366 | 363, 365 | bitrid 283 |
. . . . . 6
β’ (π₯ = π β (βπ β β ((π β β β¦
(β«2β(πΉβπ)))βπ) β€ π₯ β βπ β β
(β«2β(πΉβπ)) β€ π)) |
367 | 366 | rspcev 3584 |
. . . . 5
β’ ((π β β β§
βπ β β
(β«2β(πΉβπ)) β€ π) β βπ₯ β β βπ β β ((π β β β¦
(β«2β(πΉβπ)))βπ) β€ π₯) |
368 | 309, 358,
367 | syl2anc 585 |
. . . 4
β’ (π β βπ₯ β β βπ β β ((π β β β¦
(β«2β(πΉβπ)))βπ) β€ π₯) |
369 | 1, 2, 327, 357, 368 | climsup 15561 |
. . 3
β’ (π β (π β β β¦
(β«2β(πΉβπ))) β sup(ran (π β β β¦
(β«2β(πΉβπ))), β, < )) |
370 | 327 | frnd 6681 |
. . . . 5
β’ (π β ran (π β β β¦
(β«2β(πΉβπ))) β β) |
371 | 318, 312 | dmmptd 6651 |
. . . . . . 7
β’ (π β dom (π β β β¦
(β«2β(πΉβπ))) = β) |
372 | 240 | a1i 11 |
. . . . . . 7
β’ (π β β β
β
) |
373 | 371, 372 | eqnetrd 3012 |
. . . . . 6
β’ (π β dom (π β β β¦
(β«2β(πΉβπ))) β β
) |
374 | | dm0rn0 5885 |
. . . . . . 7
β’ (dom
(π β β β¦
(β«2β(πΉβπ))) = β
β ran (π β β β¦
(β«2β(πΉβπ))) = β
) |
375 | 374 | necon3bii 2997 |
. . . . . 6
β’ (dom
(π β β β¦
(β«2β(πΉβπ))) β β
β ran (π β β β¦
(β«2β(πΉβπ))) β β
) |
376 | 373, 375 | sylib 217 |
. . . . 5
β’ (π β ran (π β β β¦
(β«2β(πΉβπ))) β β
) |
377 | 315, 318 | fnmpti 6649 |
. . . . . . . 8
β’ (π β β β¦
(β«2β(πΉβπ))) Fn β |
378 | | breq1 5113 |
. . . . . . . . 9
β’ (π§ = ((π β β β¦
(β«2β(πΉβπ)))βπ) β (π§ β€ π₯ β ((π β β β¦
(β«2β(πΉβπ)))βπ) β€ π₯)) |
379 | 378 | ralrn 7043 |
. . . . . . . 8
β’ ((π β β β¦
(β«2β(πΉβπ))) Fn β β (βπ§ β ran (π β β β¦
(β«2β(πΉβπ)))π§ β€ π₯ β βπ β β ((π β β β¦
(β«2β(πΉβπ)))βπ) β€ π₯)) |
380 | 377, 379 | mp1i 13 |
. . . . . . 7
β’ (π β (βπ§ β ran (π β β β¦
(β«2β(πΉβπ)))π§ β€ π₯ β βπ β β ((π β β β¦
(β«2β(πΉβπ)))βπ) β€ π₯)) |
381 | 380 | rexbidv 3176 |
. . . . . 6
β’ (π β (βπ₯ β β βπ§ β ran (π β β β¦
(β«2β(πΉβπ)))π§ β€ π₯ β βπ₯ β β βπ β β ((π β β β¦
(β«2β(πΉβπ)))βπ) β€ π₯)) |
382 | 368, 381 | mpbird 257 |
. . . . 5
β’ (π β βπ₯ β β βπ§ β ran (π β β β¦
(β«2β(πΉβπ)))π§ β€ π₯) |
383 | | supxrre 13253 |
. . . . 5
β’ ((ran
(π β β β¦
(β«2β(πΉβπ))) β β β§ ran (π β β β¦
(β«2β(πΉβπ))) β β
β§ βπ₯ β β βπ§ β ran (π β β β¦
(β«2β(πΉβπ)))π§ β€ π₯) β sup(ran (π β β β¦
(β«2β(πΉβπ))), β*, < ) = sup(ran
(π β β β¦
(β«2β(πΉβπ))), β, < )) |
384 | 370, 376,
382, 383 | syl3anc 1372 |
. . . 4
β’ (π β sup(ran (π β β β¦
(β«2β(πΉβπ))), β*, < ) = sup(ran
(π β β β¦
(β«2β(πΉβπ))), β, < )) |
385 | 323, 384 | eqtr2id 2790 |
. . 3
β’ (π β sup(ran (π β β β¦
(β«2β(πΉβπ))), β, < ) = π) |
386 | 369, 385 | breqtrd 5136 |
. 2
β’ (π β (π β β β¦
(β«2β(πΉβπ))) β π) |
387 | 17 | adantr 482 |
. . . . 5
β’ ((π β§ π β β) β π β β) |
388 | 90 | ffvelcdmda 7040 |
. . . . . . 7
β’ ((π β§ π β β) β (π΄βπ) β dom vol) |
389 | 276 | i1fres 25086 |
. . . . . . 7
β’ ((π» β dom β«1
β§ (π΄βπ) β dom vol) β (π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0)) β dom
β«1) |
390 | 10, 388, 389 | syl2an2r 684 |
. . . . . 6
β’ ((π β§ π β β) β (π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0)) β dom
β«1) |
391 | | itg1cl 25065 |
. . . . . 6
β’ ((π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0)) β dom β«1 β
(β«1β(π₯
β β β¦ if(π₯
β (π΄βπ), (π»βπ₯), 0))) β β) |
392 | 390, 391 | syl 17 |
. . . . 5
β’ ((π β§ π β β) β
(β«1β(π₯
β β β¦ if(π₯
β (π΄βπ), (π»βπ₯), 0))) β β) |
393 | 387, 392 | remulcld 11192 |
. . . 4
β’ ((π β§ π β β) β (π Β· (β«1β(π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0)))) β β) |
394 | 393 | fmpttd 7068 |
. . 3
β’ (π β (π β β β¦ (π Β· (β«1β(π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯),
0))))):ββΆβ) |
395 | 394 | ffvelcdmda 7040 |
. 2
β’ ((π β§ π β β) β ((π β β β¦ (π Β· (β«1β(π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0)))))βπ) β β) |
396 | 327 | ffvelcdmda 7040 |
. 2
β’ ((π β§ π β β) β ((π β β β¦
(β«2β(πΉβπ)))βπ) β β) |
397 | 329 | feq1d 6658 |
. . . . . . . 8
β’ (π = π β ((πΉβπ):ββΆ(0[,)+β) β (πΉβπ):ββΆ(0[,)+β))) |
398 | 397 | cbvralvw 3228 |
. . . . . . 7
β’
(βπ β
β (πΉβπ):ββΆ(0[,)+β)
β βπ β
β (πΉβπ):ββΆ(0[,)+β)) |
399 | 99, 398 | sylib 217 |
. . . . . 6
β’ (π β βπ β β (πΉβπ):ββΆ(0[,)+β)) |
400 | 399 | r19.21bi 3237 |
. . . . 5
β’ ((π β§ π β β) β (πΉβπ):ββΆ(0[,)+β)) |
401 | | fss 6690 |
. . . . 5
β’ (((πΉβπ):ββΆ(0[,)+β) β§
(0[,)+β) β (0[,]+β)) β (πΉβπ):ββΆ(0[,]+β)) |
402 | 400, 306,
401 | sylancl 587 |
. . . 4
β’ ((π β§ π β β) β (πΉβπ):ββΆ(0[,]+β)) |
403 | 23 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β β) β β β
V) |
404 | 17 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β) β π β β) |
405 | 404 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β β) β§ π₯ β β) β π β β) |
406 | | fvex 6860 |
. . . . . . . . 9
β’ (π»βπ₯) β V |
407 | | c0ex 11156 |
. . . . . . . . 9
β’ 0 β
V |
408 | 406, 407 | ifex 4541 |
. . . . . . . 8
β’ if(π₯ β (π΄βπ), (π»βπ₯), 0) β V |
409 | 408 | a1i 11 |
. . . . . . 7
β’ (((π β§ π β β) β§ π₯ β β) β if(π₯ β (π΄βπ), (π»βπ₯), 0) β V) |
410 | | fconstmpt 5699 |
. . . . . . . 8
β’ (β
Γ {π}) = (π₯ β β β¦ π) |
411 | 410 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β β) β (β Γ
{π}) = (π₯ β β β¦ π)) |
412 | | eqidd 2738 |
. . . . . . 7
β’ ((π β§ π β β) β (π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0)) = (π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0))) |
413 | 403, 405,
409, 411, 412 | offval2 7642 |
. . . . . 6
β’ ((π β§ π β β) β ((β Γ
{π}) βf
Β· (π₯ β β
β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0))) = (π₯ β β β¦ (π Β· if(π₯ β (π΄βπ), (π»βπ₯), 0)))) |
414 | | ovif2 7460 |
. . . . . . . 8
β’ (π Β· if(π₯ β (π΄βπ), (π»βπ₯), 0)) = if(π₯ β (π΄βπ), (π Β· (π»βπ₯)), (π Β· 0)) |
415 | 47 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β β) β π β β) |
416 | 415 | mul01d 11361 |
. . . . . . . . 9
β’ ((π β§ π β β) β (π Β· 0) = 0) |
417 | 416 | ifeq2d 4511 |
. . . . . . . 8
β’ ((π β§ π β β) β if(π₯ β (π΄βπ), (π Β· (π»βπ₯)), (π Β· 0)) = if(π₯ β (π΄βπ), (π Β· (π»βπ₯)), 0)) |
418 | 414, 417 | eqtrid 2789 |
. . . . . . 7
β’ ((π β§ π β β) β (π Β· if(π₯ β (π΄βπ), (π»βπ₯), 0)) = if(π₯ β (π΄βπ), (π Β· (π»βπ₯)), 0)) |
419 | 418 | mpteq2dv 5212 |
. . . . . 6
β’ ((π β§ π β β) β (π₯ β β β¦ (π Β· if(π₯ β (π΄βπ), (π»βπ₯), 0))) = (π₯ β β β¦ if(π₯ β (π΄βπ), (π Β· (π»βπ₯)), 0))) |
420 | 413, 419 | eqtrd 2777 |
. . . . 5
β’ ((π β§ π β β) β ((β Γ
{π}) βf
Β· (π₯ β β
β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0))) = (π₯ β β β¦ if(π₯ β (π΄βπ), (π Β· (π»βπ₯)), 0))) |
421 | 293, 404 | i1fmulc 25084 |
. . . . 5
β’ ((π β§ π β β) β ((β Γ
{π}) βf
Β· (π₯ β β
β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0))) β dom
β«1) |
422 | 420, 421 | eqeltrrd 2839 |
. . . 4
β’ ((π β§ π β β) β (π₯ β β β¦ if(π₯ β (π΄βπ), (π Β· (π»βπ₯)), 0)) β dom
β«1) |
423 | | iftrue 4497 |
. . . . . . . . 9
β’ (π₯ β (π΄βπ) β if(π₯ β (π΄βπ), (π Β· (π»βπ₯)), 0) = (π Β· (π»βπ₯))) |
424 | 423 | adantl 483 |
. . . . . . . 8
β’ ((((π β§ π β β) β§ π₯ β β) β§ π₯ β (π΄βπ)) β if(π₯ β (π΄βπ), (π Β· (π»βπ₯)), 0) = (π Β· (π»βπ₯))) |
425 | 329 | fveq1d 6849 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((πΉβπ)βπ₯) = ((πΉβπ)βπ₯)) |
426 | 425 | breq2d 5122 |
. . . . . . . . . . . . . 14
β’ (π = π β ((π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯) β (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯))) |
427 | 426 | rabbidv 3418 |
. . . . . . . . . . . . 13
β’ (π = π β {π₯ β β β£ (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)} = {π₯ β β β£ (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)}) |
428 | 23 | rabex 5294 |
. . . . . . . . . . . . 13
β’ {π₯ β β β£ (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)} β V |
429 | 427, 89, 428 | fvmpt 6953 |
. . . . . . . . . . . 12
β’ (π β β β (π΄βπ) = {π₯ β β β£ (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)}) |
430 | 429 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π₯ β β) β (π΄βπ) = {π₯ β β β£ (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)}) |
431 | 430 | eleq2d 2824 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π₯ β β) β (π₯ β (π΄βπ) β π₯ β {π₯ β β β£ (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)})) |
432 | 431 | biimpa 478 |
. . . . . . . . 9
β’ ((((π β§ π β β) β§ π₯ β β) β§ π₯ β (π΄βπ)) β π₯ β {π₯ β β β£ (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)}) |
433 | | rabid 3430 |
. . . . . . . . . 10
β’ (π₯ β {π₯ β β β£ (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)} β (π₯ β β β§ (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯))) |
434 | 433 | simprbi 498 |
. . . . . . . . 9
β’ (π₯ β {π₯ β β β£ (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)} β (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)) |
435 | 432, 434 | syl 17 |
. . . . . . . 8
β’ ((((π β§ π β β) β§ π₯ β β) β§ π₯ β (π΄βπ)) β (π Β· (π»βπ₯)) β€ ((πΉβπ)βπ₯)) |
436 | 424, 435 | eqbrtrd 5132 |
. . . . . . 7
β’ ((((π β§ π β β) β§ π₯ β β) β§ π₯ β (π΄βπ)) β if(π₯ β (π΄βπ), (π Β· (π»βπ₯)), 0) β€ ((πΉβπ)βπ₯)) |
437 | | iffalse 4500 |
. . . . . . . . 9
β’ (Β¬
π₯ β (π΄βπ) β if(π₯ β (π΄βπ), (π Β· (π»βπ₯)), 0) = 0) |
438 | 437 | adantl 483 |
. . . . . . . 8
β’ ((((π β§ π β β) β§ π₯ β β) β§ Β¬ π₯ β (π΄βπ)) β if(π₯ β (π΄βπ), (π Β· (π»βπ₯)), 0) = 0) |
439 | 400 | ffvelcdmda 7040 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π₯ β β) β ((πΉβπ)βπ₯) β (0[,)+β)) |
440 | | elrege0 13378 |
. . . . . . . . . . 11
β’ (((πΉβπ)βπ₯) β (0[,)+β) β (((πΉβπ)βπ₯) β β β§ 0 β€ ((πΉβπ)βπ₯))) |
441 | 440 | simprbi 498 |
. . . . . . . . . 10
β’ (((πΉβπ)βπ₯) β (0[,)+β) β 0 β€ ((πΉβπ)βπ₯)) |
442 | 439, 441 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π₯ β β) β 0 β€ ((πΉβπ)βπ₯)) |
443 | 442 | adantr 482 |
. . . . . . . 8
β’ ((((π β§ π β β) β§ π₯ β β) β§ Β¬ π₯ β (π΄βπ)) β 0 β€ ((πΉβπ)βπ₯)) |
444 | 438, 443 | eqbrtrd 5132 |
. . . . . . 7
β’ ((((π β§ π β β) β§ π₯ β β) β§ Β¬ π₯ β (π΄βπ)) β if(π₯ β (π΄βπ), (π Β· (π»βπ₯)), 0) β€ ((πΉβπ)βπ₯)) |
445 | 436, 444 | pm2.61dan 812 |
. . . . . 6
β’ (((π β§ π β β) β§ π₯ β β) β if(π₯ β (π΄βπ), (π Β· (π»βπ₯)), 0) β€ ((πΉβπ)βπ₯)) |
446 | 445 | ralrimiva 3144 |
. . . . 5
β’ ((π β§ π β β) β βπ₯ β β if(π₯ β (π΄βπ), (π Β· (π»βπ₯)), 0) β€ ((πΉβπ)βπ₯)) |
447 | | ovex 7395 |
. . . . . . . 8
β’ (π Β· (π»βπ₯)) β V |
448 | 447, 407 | ifex 4541 |
. . . . . . 7
β’ if(π₯ β (π΄βπ), (π Β· (π»βπ₯)), 0) β V |
449 | 448 | a1i 11 |
. . . . . 6
β’ (((π β§ π β β) β§ π₯ β β) β if(π₯ β (π΄βπ), (π Β· (π»βπ₯)), 0) β V) |
450 | | fvexd 6862 |
. . . . . 6
β’ (((π β§ π β β) β§ π₯ β β) β ((πΉβπ)βπ₯) β V) |
451 | | eqidd 2738 |
. . . . . 6
β’ ((π β§ π β β) β (π₯ β β β¦ if(π₯ β (π΄βπ), (π Β· (π»βπ₯)), 0)) = (π₯ β β β¦ if(π₯ β (π΄βπ), (π Β· (π»βπ₯)), 0))) |
452 | 400 | feqmptd 6915 |
. . . . . 6
β’ ((π β§ π β β) β (πΉβπ) = (π₯ β β β¦ ((πΉβπ)βπ₯))) |
453 | 403, 449,
450, 451, 452 | ofrfval2 7643 |
. . . . 5
β’ ((π β§ π β β) β ((π₯ β β β¦ if(π₯ β (π΄βπ), (π Β· (π»βπ₯)), 0)) βr β€ (πΉβπ) β βπ₯ β β if(π₯ β (π΄βπ), (π Β· (π»βπ₯)), 0) β€ ((πΉβπ)βπ₯))) |
454 | 446, 453 | mpbird 257 |
. . . 4
β’ ((π β§ π β β) β (π₯ β β β¦ if(π₯ β (π΄βπ), (π Β· (π»βπ₯)), 0)) βr β€ (πΉβπ)) |
455 | | itg2ub 25114 |
. . . 4
β’ (((πΉβπ):ββΆ(0[,]+β) β§ (π₯ β β β¦ if(π₯ β (π΄βπ), (π Β· (π»βπ₯)), 0)) β dom β«1 β§
(π₯ β β β¦
if(π₯ β (π΄βπ), (π Β· (π»βπ₯)), 0)) βr β€ (πΉβπ)) β (β«1β(π₯ β β β¦ if(π₯ β (π΄βπ), (π Β· (π»βπ₯)), 0))) β€ (β«2β(πΉβπ))) |
456 | 402, 422,
454, 455 | syl3anc 1372 |
. . 3
β’ ((π β§ π β β) β
(β«1β(π₯
β β β¦ if(π₯
β (π΄βπ), (π Β· (π»βπ₯)), 0))) β€ (β«2β(πΉβπ))) |
457 | 301 | adantl 483 |
. . . 4
β’ ((π β§ π β β) β ((π β β β¦ (π Β· (β«1β(π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0)))))βπ) = (π Β· (β«1β(π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0))))) |
458 | 293, 404 | itg1mulc 25085 |
. . . 4
β’ ((π β§ π β β) β
(β«1β((β Γ {π}) βf Β· (π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0)))) = (π Β· (β«1β(π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0))))) |
459 | 420 | fveq2d 6851 |
. . . 4
β’ ((π β§ π β β) β
(β«1β((β Γ {π}) βf Β· (π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0)))) = (β«1β(π₯ β β β¦ if(π₯ β (π΄βπ), (π Β· (π»βπ₯)), 0)))) |
460 | 457, 458,
459 | 3eqtr2d 2783 |
. . 3
β’ ((π β§ π β β) β ((π β β β¦ (π Β· (β«1β(π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0)))))βπ) = (β«1β(π₯ β β β¦ if(π₯ β (π΄βπ), (π Β· (π»βπ₯)), 0)))) |
461 | 343 | adantl 483 |
. . 3
β’ ((π β§ π β β) β ((π β β β¦
(β«2β(πΉβπ)))βπ) = (β«2β(πΉβπ))) |
462 | 456, 460,
461 | 3brtr4d 5142 |
. 2
β’ ((π β§ π β β) β ((π β β β¦ (π Β· (β«1β(π₯ β β β¦ if(π₯ β (π΄βπ), (π»βπ₯), 0)))))βπ) β€ ((π β β β¦
(β«2β(πΉβπ)))βπ)) |
463 | 1, 2, 305, 386, 395, 396, 462 | climle 15529 |
1
β’ (π β (π Β· (β«1βπ»)) β€ π) |