Step | Hyp | Ref
| Expression |
1 | | mnfxr 11220 |
. . . . . 6
β’ -β
β β* |
2 | 1 | a1i 11 |
. . . . 5
β’ (π β -β β
β*) |
3 | | nnuz 12814 |
. . . . . . . . 9
β’ β =
(β€β₯β1) |
4 | | 1zzd 12542 |
. . . . . . . . 9
β’ (π β 1 β
β€) |
5 | | ovoliun.v |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (vol*βπ΄) β
β) |
6 | | ovoliun.g |
. . . . . . . . . . 11
β’ πΊ = (π β β β¦ (vol*βπ΄)) |
7 | 5, 6 | fmptd 7066 |
. . . . . . . . . 10
β’ (π β πΊ:ββΆβ) |
8 | 7 | ffvelcdmda 7039 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πΊβπ) β β) |
9 | 3, 4, 8 | serfre 13946 |
. . . . . . . 8
β’ (π β seq1( + , πΊ):ββΆβ) |
10 | | ovoliun.t |
. . . . . . . . 9
β’ π = seq1( + , πΊ) |
11 | 10 | feq1i 6663 |
. . . . . . . 8
β’ (π:ββΆβ β
seq1( + , πΊ):ββΆβ) |
12 | 9, 11 | sylibr 233 |
. . . . . . 7
β’ (π β π:ββΆβ) |
13 | | 1nn 12172 |
. . . . . . 7
β’ 1 β
β |
14 | | ffvelcdm 7036 |
. . . . . . 7
β’ ((π:ββΆβ β§ 1
β β) β (πβ1) β β) |
15 | 12, 13, 14 | sylancl 587 |
. . . . . 6
β’ (π β (πβ1) β β) |
16 | 15 | rexrd 11213 |
. . . . 5
β’ (π β (πβ1) β
β*) |
17 | 12 | frnd 6680 |
. . . . . . 7
β’ (π β ran π β β) |
18 | | ressxr 11207 |
. . . . . . 7
β’ β
β β* |
19 | 17, 18 | sstrdi 3960 |
. . . . . 6
β’ (π β ran π β
β*) |
20 | | supxrcl 13243 |
. . . . . 6
β’ (ran
π β
β* β sup(ran π, β*, < ) β
β*) |
21 | 19, 20 | syl 17 |
. . . . 5
β’ (π β sup(ran π, β*, < ) β
β*) |
22 | 15 | mnfltd 13053 |
. . . . 5
β’ (π β -β < (πβ1)) |
23 | 12 | ffnd 6673 |
. . . . . . 7
β’ (π β π Fn β) |
24 | | fnfvelrn 7035 |
. . . . . . 7
β’ ((π Fn β β§ 1 β
β) β (πβ1)
β ran π) |
25 | 23, 13, 24 | sylancl 587 |
. . . . . 6
β’ (π β (πβ1) β ran π) |
26 | | supxrub 13252 |
. . . . . 6
β’ ((ran
π β
β* β§ (πβ1) β ran π) β (πβ1) β€ sup(ran π, β*, <
)) |
27 | 19, 25, 26 | syl2anc 585 |
. . . . 5
β’ (π β (πβ1) β€ sup(ran π, β*, <
)) |
28 | 2, 16, 21, 22, 27 | xrltletrd 13089 |
. . . 4
β’ (π β -β < sup(ran
π, β*,
< )) |
29 | | xrrebnd 13096 |
. . . . 5
β’ (sup(ran
π, β*,
< ) β β* β (sup(ran π, β*, < ) β β
β (-β < sup(ran π, β*, < ) β§ sup(ran
π, β*,
< ) < +β))) |
30 | 21, 29 | syl 17 |
. . . 4
β’ (π β (sup(ran π, β*, < ) β β
β (-β < sup(ran π, β*, < ) β§ sup(ran
π, β*,
< ) < +β))) |
31 | 28, 30 | mpbirand 706 |
. . 3
β’ (π β (sup(ran π, β*, < ) β β
β sup(ran π,
β*, < ) < +β)) |
32 | | nfcv 2904 |
. . . . . . . . 9
β’
β²ππ΄ |
33 | | nfcsb1v 3884 |
. . . . . . . . 9
β’
β²πβ¦π / πβ¦π΄ |
34 | | csbeq1a 3873 |
. . . . . . . . 9
β’ (π = π β π΄ = β¦π / πβ¦π΄) |
35 | 32, 33, 34 | cbviun 5000 |
. . . . . . . 8
β’ βͺ π β β π΄ = βͺ π β β
β¦π / πβ¦π΄ |
36 | 35 | fveq2i 6849 |
. . . . . . 7
β’
(vol*ββͺ π β β π΄) = (vol*ββͺ π β β β¦π / πβ¦π΄) |
37 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²π(vol*βπ΄) |
38 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²πvol* |
39 | 38, 33 | nffv 6856 |
. . . . . . . . . 10
β’
β²π(vol*ββ¦π / πβ¦π΄) |
40 | 34 | fveq2d 6850 |
. . . . . . . . . 10
β’ (π = π β (vol*βπ΄) = (vol*ββ¦π / πβ¦π΄)) |
41 | 37, 39, 40 | cbvmpt 5220 |
. . . . . . . . 9
β’ (π β β β¦
(vol*βπ΄)) = (π β β β¦
(vol*ββ¦π / πβ¦π΄)) |
42 | 6, 41 | eqtri 2761 |
. . . . . . . 8
β’ πΊ = (π β β β¦
(vol*ββ¦π / πβ¦π΄)) |
43 | | ovoliun.a |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π΄ β β) |
44 | 43 | ralrimiva 3140 |
. . . . . . . . . . 11
β’ (π β βπ β β π΄ β β) |
45 | | nfv 1918 |
. . . . . . . . . . . 12
β’
β²π π΄ β
β |
46 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²πβ |
47 | 33, 46 | nfss 3940 |
. . . . . . . . . . . 12
β’
β²πβ¦π / πβ¦π΄ β β |
48 | 34 | sseq1d 3979 |
. . . . . . . . . . . 12
β’ (π = π β (π΄ β β β β¦π / πβ¦π΄ β β)) |
49 | 45, 47, 48 | cbvralw 3288 |
. . . . . . . . . . 11
β’
(βπ β
β π΄ β β
β βπ β
β β¦π /
πβ¦π΄ β
β) |
50 | 44, 49 | sylib 217 |
. . . . . . . . . 10
β’ (π β βπ β β β¦π / πβ¦π΄ β β) |
51 | 50 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ sup(ran π, β*, < ) β
β) β§ π₯ β
β+) β βπ β β β¦π / πβ¦π΄ β β) |
52 | 51 | r19.21bi 3233 |
. . . . . . . 8
β’ ((((π β§ sup(ran π, β*, < ) β
β) β§ π₯ β
β+) β§ π β β) β β¦π / πβ¦π΄ β β) |
53 | 5 | ralrimiva 3140 |
. . . . . . . . . . 11
β’ (π β βπ β β (vol*βπ΄) β β) |
54 | 37 | nfel1 2920 |
. . . . . . . . . . . 12
β’
β²π(vol*βπ΄) β β |
55 | 39 | nfel1 2920 |
. . . . . . . . . . . 12
β’
β²π(vol*ββ¦π / πβ¦π΄) β β |
56 | 40 | eleq1d 2819 |
. . . . . . . . . . . 12
β’ (π = π β ((vol*βπ΄) β β β
(vol*ββ¦π / πβ¦π΄) β β)) |
57 | 54, 55, 56 | cbvralw 3288 |
. . . . . . . . . . 11
β’
(βπ β
β (vol*βπ΄)
β β β βπ β β
(vol*ββ¦π / πβ¦π΄) β β) |
58 | 53, 57 | sylib 217 |
. . . . . . . . . 10
β’ (π β βπ β β
(vol*ββ¦π / πβ¦π΄) β β) |
59 | 58 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ sup(ran π, β*, < ) β
β) β§ π₯ β
β+) β βπ β β
(vol*ββ¦π / πβ¦π΄) β β) |
60 | 59 | r19.21bi 3233 |
. . . . . . . 8
β’ ((((π β§ sup(ran π, β*, < ) β
β) β§ π₯ β
β+) β§ π β β) β
(vol*ββ¦π / πβ¦π΄) β β) |
61 | | simplr 768 |
. . . . . . . 8
β’ (((π β§ sup(ran π, β*, < ) β
β) β§ π₯ β
β+) β sup(ran π, β*, < ) β
β) |
62 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ sup(ran π, β*, < ) β
β) β§ π₯ β
β+) β π₯ β β+) |
63 | 10, 42, 52, 60, 61, 62 | ovoliunlem3 24891 |
. . . . . . 7
β’ (((π β§ sup(ran π, β*, < ) β
β) β§ π₯ β
β+) β (vol*ββͺ
π β β
β¦π / πβ¦π΄) β€ (sup(ran π, β*, < ) + π₯)) |
64 | 36, 63 | eqbrtrid 5144 |
. . . . . 6
β’ (((π β§ sup(ran π, β*, < ) β
β) β§ π₯ β
β+) β (vol*ββͺ
π β β π΄) β€ (sup(ran π, β*, < ) +
π₯)) |
65 | 64 | ralrimiva 3140 |
. . . . 5
β’ ((π β§ sup(ran π, β*, < ) β
β) β βπ₯
β β+ (vol*ββͺ
π β β π΄) β€ (sup(ran π, β*, < ) +
π₯)) |
66 | | iunss 5009 |
. . . . . . . 8
β’ (βͺ π β β π΄ β β β βπ β β π΄ β
β) |
67 | 44, 66 | sylibr 233 |
. . . . . . 7
β’ (π β βͺ π β β π΄ β β) |
68 | | ovolcl 24865 |
. . . . . . 7
β’ (βͺ π β β π΄ β β β (vol*ββͺ π β β π΄) β
β*) |
69 | 67, 68 | syl 17 |
. . . . . 6
β’ (π β (vol*ββͺ π β β π΄) β
β*) |
70 | | xralrple 13133 |
. . . . . 6
β’
(((vol*ββͺ π β β π΄) β β* β§ sup(ran
π, β*,
< ) β β) β ((vol*ββͺ
π β β π΄) β€ sup(ran π, β*, < ) β
βπ₯ β
β+ (vol*ββͺ π β β π΄) β€ (sup(ran π, β*, < ) +
π₯))) |
71 | 69, 70 | sylan 581 |
. . . . 5
β’ ((π β§ sup(ran π, β*, < ) β
β) β ((vol*ββͺ π β β π΄) β€ sup(ran π, β*, < ) β
βπ₯ β
β+ (vol*ββͺ π β β π΄) β€ (sup(ran π, β*, < ) +
π₯))) |
72 | 65, 71 | mpbird 257 |
. . . 4
β’ ((π β§ sup(ran π, β*, < ) β
β) β (vol*ββͺ π β β π΄) β€ sup(ran π, β*, <
)) |
73 | 72 | ex 414 |
. . 3
β’ (π β (sup(ran π, β*, < ) β β
β (vol*ββͺ π β β π΄) β€ sup(ran π, β*, <
))) |
74 | 31, 73 | sylbird 260 |
. 2
β’ (π β (sup(ran π, β*, < ) < +β
β (vol*ββͺ π β β π΄) β€ sup(ran π, β*, <
))) |
75 | | nltpnft 13092 |
. . . 4
β’ (sup(ran
π, β*,
< ) β β* β (sup(ran π, β*, < ) = +β
β Β¬ sup(ran π,
β*, < ) < +β)) |
76 | 21, 75 | syl 17 |
. . 3
β’ (π β (sup(ran π, β*, < ) = +β
β Β¬ sup(ran π,
β*, < ) < +β)) |
77 | | pnfge 13059 |
. . . . 5
β’
((vol*ββͺ π β β π΄) β β* β
(vol*ββͺ π β β π΄) β€ +β) |
78 | 69, 77 | syl 17 |
. . . 4
β’ (π β (vol*ββͺ π β β π΄) β€ +β) |
79 | | breq2 5113 |
. . . 4
β’ (sup(ran
π, β*,
< ) = +β β ((vol*ββͺ π β β π΄) β€ sup(ran π, β*, < ) β
(vol*ββͺ π β β π΄) β€ +β)) |
80 | 78, 79 | syl5ibrcom 247 |
. . 3
β’ (π β (sup(ran π, β*, < ) = +β
β (vol*ββͺ π β β π΄) β€ sup(ran π, β*, <
))) |
81 | 76, 80 | sylbird 260 |
. 2
β’ (π β (Β¬ sup(ran π, β*, < )
< +β β (vol*ββͺ π β β π΄) β€ sup(ran π, β*, <
))) |
82 | 74, 81 | pm2.61d 179 |
1
β’ (π β (vol*ββͺ π β β π΄) β€ sup(ran π, β*, <
)) |