Step | Hyp | Ref
| Expression |
1 | | ovoliun.t |
. . 3
β’ π = seq1( + , πΊ) |
2 | | ovoliun.g |
. . 3
β’ πΊ = (π β β β¦ (vol*βπ΄)) |
3 | | ovoliun.a |
. . 3
β’ ((π β§ π β β) β π΄ β β) |
4 | | ovoliun.v |
. . 3
β’ ((π β§ π β β) β (vol*βπ΄) β
β) |
5 | 1, 2, 3, 4 | ovoliun 25246 |
. 2
β’ (π β (vol*ββͺ π β β π΄) β€ sup(ran π, β*, <
)) |
6 | | nnuz 12869 |
. . . . . . . 8
β’ β =
(β€β₯β1) |
7 | | 1zzd 12597 |
. . . . . . . 8
β’ (π β 1 β
β€) |
8 | | fvex 6904 |
. . . . . . . . . . 11
β’
(vol*ββ¦π / πβ¦π΄) β V |
9 | | nfcv 2903 |
. . . . . . . . . . . . . 14
β’
β²π(vol*βπ΄) |
10 | | nfcv 2903 |
. . . . . . . . . . . . . . 15
β’
β²πvol* |
11 | | nfcsb1v 3918 |
. . . . . . . . . . . . . . 15
β’
β²πβ¦π / πβ¦π΄ |
12 | 10, 11 | nffv 6901 |
. . . . . . . . . . . . . 14
β’
β²π(vol*ββ¦π / πβ¦π΄) |
13 | | csbeq1a 3907 |
. . . . . . . . . . . . . . 15
β’ (π = π β π΄ = β¦π / πβ¦π΄) |
14 | 13 | fveq2d 6895 |
. . . . . . . . . . . . . 14
β’ (π = π β (vol*βπ΄) = (vol*ββ¦π / πβ¦π΄)) |
15 | 9, 12, 14 | cbvmpt 5259 |
. . . . . . . . . . . . 13
β’ (π β β β¦
(vol*βπ΄)) = (π β β β¦
(vol*ββ¦π / πβ¦π΄)) |
16 | 2, 15 | eqtri 2760 |
. . . . . . . . . . . 12
β’ πΊ = (π β β β¦
(vol*ββ¦π / πβ¦π΄)) |
17 | 16 | fvmpt2 7009 |
. . . . . . . . . . 11
β’ ((π β β β§
(vol*ββ¦π / πβ¦π΄) β V) β (πΊβπ) = (vol*ββ¦π / πβ¦π΄)) |
18 | 8, 17 | mpan2 689 |
. . . . . . . . . 10
β’ (π β β β (πΊβπ) = (vol*ββ¦π / πβ¦π΄)) |
19 | 18 | adantl 482 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πΊβπ) = (vol*ββ¦π / πβ¦π΄)) |
20 | 4 | ralrimiva 3146 |
. . . . . . . . . . 11
β’ (π β βπ β β (vol*βπ΄) β β) |
21 | 9 | nfel1 2919 |
. . . . . . . . . . . 12
β’
β²π(vol*βπ΄) β β |
22 | 12 | nfel1 2919 |
. . . . . . . . . . . 12
β’
β²π(vol*ββ¦π / πβ¦π΄) β β |
23 | 14 | eleq1d 2818 |
. . . . . . . . . . . 12
β’ (π = π β ((vol*βπ΄) β β β
(vol*ββ¦π / πβ¦π΄) β β)) |
24 | 21, 22, 23 | cbvralw 3303 |
. . . . . . . . . . 11
β’
(βπ β
β (vol*βπ΄)
β β β βπ β β
(vol*ββ¦π / πβ¦π΄) β β) |
25 | 20, 24 | sylib 217 |
. . . . . . . . . 10
β’ (π β βπ β β
(vol*ββ¦π / πβ¦π΄) β β) |
26 | 25 | r19.21bi 3248 |
. . . . . . . . 9
β’ ((π β§ π β β) β
(vol*ββ¦π / πβ¦π΄) β β) |
27 | 19, 26 | eqeltrd 2833 |
. . . . . . . 8
β’ ((π β§ π β β) β (πΊβπ) β β) |
28 | 6, 7, 27 | serfre 14001 |
. . . . . . 7
β’ (π β seq1( + , πΊ):ββΆβ) |
29 | 1 | feq1i 6708 |
. . . . . . 7
β’ (π:ββΆβ β
seq1( + , πΊ):ββΆβ) |
30 | 28, 29 | sylibr 233 |
. . . . . 6
β’ (π β π:ββΆβ) |
31 | 30 | frnd 6725 |
. . . . 5
β’ (π β ran π β β) |
32 | | 1nn 12227 |
. . . . . . . 8
β’ 1 β
β |
33 | 30 | fdmd 6728 |
. . . . . . . 8
β’ (π β dom π = β) |
34 | 32, 33 | eleqtrrid 2840 |
. . . . . . 7
β’ (π β 1 β dom π) |
35 | 34 | ne0d 4335 |
. . . . . 6
β’ (π β dom π β β
) |
36 | | dm0rn0 5924 |
. . . . . . 7
β’ (dom
π = β
β ran
π =
β
) |
37 | 36 | necon3bii 2993 |
. . . . . 6
β’ (dom
π β β
β ran
π β
β
) |
38 | 35, 37 | sylib 217 |
. . . . 5
β’ (π β ran π β β
) |
39 | | ovoliun2.t |
. . . . . . . . 9
β’ (π β π β dom β ) |
40 | 1, 39 | eqeltrrid 2838 |
. . . . . . . 8
β’ (π β seq1( + , πΊ) β dom β
) |
41 | 6, 7, 19, 26, 40 | isumrecl 15715 |
. . . . . . 7
β’ (π β Ξ£π β β
(vol*ββ¦π / πβ¦π΄) β β) |
42 | | elfznn 13534 |
. . . . . . . . . . . . 13
β’ (π β (1...π) β π β β) |
43 | 42 | adantl 482 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β (1...π)) β π β β) |
44 | 43, 18 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (1...π)) β (πΊβπ) = (vol*ββ¦π / πβ¦π΄)) |
45 | | simpr 485 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π β β) |
46 | 45, 6 | eleqtrdi 2843 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β π β
(β€β₯β1)) |
47 | | simpl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β π) |
48 | 47, 42, 26 | syl2an 596 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β (1...π)) β (vol*ββ¦π / πβ¦π΄) β β) |
49 | 48 | recnd 11246 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (1...π)) β (vol*ββ¦π / πβ¦π΄) β β) |
50 | 44, 46, 49 | fsumser 15680 |
. . . . . . . . . 10
β’ ((π β§ π β β) β Ξ£π β (1...π)(vol*ββ¦π / πβ¦π΄) = (seq1( + , πΊ)βπ)) |
51 | 1 | fveq1i 6892 |
. . . . . . . . . 10
β’ (πβπ) = (seq1( + , πΊ)βπ) |
52 | 50, 51 | eqtr4di 2790 |
. . . . . . . . 9
β’ ((π β§ π β β) β Ξ£π β (1...π)(vol*ββ¦π / πβ¦π΄) = (πβπ)) |
53 | | fzfid 13942 |
. . . . . . . . . . 11
β’ (π β (1...π) β Fin) |
54 | | fz1ssnn 13536 |
. . . . . . . . . . . 12
β’
(1...π) β
β |
55 | 54 | a1i 11 |
. . . . . . . . . . 11
β’ (π β (1...π) β β) |
56 | 3 | ralrimiva 3146 |
. . . . . . . . . . . . . 14
β’ (π β βπ β β π΄ β β) |
57 | | nfv 1917 |
. . . . . . . . . . . . . . 15
β’
β²π π΄ β
β |
58 | | nfcv 2903 |
. . . . . . . . . . . . . . . 16
β’
β²πβ |
59 | 11, 58 | nfss 3974 |
. . . . . . . . . . . . . . 15
β’
β²πβ¦π / πβ¦π΄ β β |
60 | 13 | sseq1d 4013 |
. . . . . . . . . . . . . . 15
β’ (π = π β (π΄ β β β β¦π / πβ¦π΄ β β)) |
61 | 57, 59, 60 | cbvralw 3303 |
. . . . . . . . . . . . . 14
β’
(βπ β
β π΄ β β
β βπ β
β β¦π /
πβ¦π΄ β
β) |
62 | 56, 61 | sylib 217 |
. . . . . . . . . . . . 13
β’ (π β βπ β β β¦π / πβ¦π΄ β β) |
63 | 62 | r19.21bi 3248 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β β¦π / πβ¦π΄ β β) |
64 | | ovolge0 25222 |
. . . . . . . . . . . 12
β’
(β¦π /
πβ¦π΄ β β β 0 β€
(vol*ββ¦π / πβ¦π΄)) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β 0 β€
(vol*ββ¦π / πβ¦π΄)) |
66 | 6, 7, 53, 55, 19, 26, 65, 40 | isumless 15795 |
. . . . . . . . . 10
β’ (π β Ξ£π β (1...π)(vol*ββ¦π / πβ¦π΄) β€ Ξ£π β β
(vol*ββ¦π / πβ¦π΄)) |
67 | 66 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β β) β Ξ£π β (1...π)(vol*ββ¦π / πβ¦π΄) β€ Ξ£π β β
(vol*ββ¦π / πβ¦π΄)) |
68 | 52, 67 | eqbrtrrd 5172 |
. . . . . . . 8
β’ ((π β§ π β β) β (πβπ) β€ Ξ£π β β
(vol*ββ¦π / πβ¦π΄)) |
69 | 68 | ralrimiva 3146 |
. . . . . . 7
β’ (π β βπ β β (πβπ) β€ Ξ£π β β
(vol*ββ¦π / πβ¦π΄)) |
70 | | brralrspcev 5208 |
. . . . . . 7
β’
((Ξ£π β
β (vol*ββ¦π / πβ¦π΄) β β β§ βπ β β (πβπ) β€ Ξ£π β β
(vol*ββ¦π / πβ¦π΄)) β βπ₯ β β βπ β β (πβπ) β€ π₯) |
71 | 41, 69, 70 | syl2anc 584 |
. . . . . 6
β’ (π β βπ₯ β β βπ β β (πβπ) β€ π₯) |
72 | 30 | ffnd 6718 |
. . . . . . . 8
β’ (π β π Fn β) |
73 | | breq1 5151 |
. . . . . . . . 9
β’ (π§ = (πβπ) β (π§ β€ π₯ β (πβπ) β€ π₯)) |
74 | 73 | ralrn 7089 |
. . . . . . . 8
β’ (π Fn β β
(βπ§ β ran π π§ β€ π₯ β βπ β β (πβπ) β€ π₯)) |
75 | 72, 74 | syl 17 |
. . . . . . 7
β’ (π β (βπ§ β ran π π§ β€ π₯ β βπ β β (πβπ) β€ π₯)) |
76 | 75 | rexbidv 3178 |
. . . . . 6
β’ (π β (βπ₯ β β βπ§ β ran π π§ β€ π₯ β βπ₯ β β βπ β β (πβπ) β€ π₯)) |
77 | 71, 76 | mpbird 256 |
. . . . 5
β’ (π β βπ₯ β β βπ§ β ran π π§ β€ π₯) |
78 | | supxrre 13310 |
. . . . 5
β’ ((ran
π β β β§ ran
π β β
β§
βπ₯ β β
βπ§ β ran π π§ β€ π₯) β sup(ran π, β*, < ) = sup(ran
π, β, <
)) |
79 | 31, 38, 77, 78 | syl3anc 1371 |
. . . 4
β’ (π β sup(ran π, β*, < ) = sup(ran
π, β, <
)) |
80 | 6, 1, 7, 19, 26, 65, 71 | isumsup 15797 |
. . . 4
β’ (π β Ξ£π β β
(vol*ββ¦π / πβ¦π΄) = sup(ran π, β, < )) |
81 | 79, 80 | eqtr4d 2775 |
. . 3
β’ (π β sup(ran π, β*, < ) = Ξ£π β β
(vol*ββ¦π / πβ¦π΄)) |
82 | 9, 12, 14 | cbvsumi 15647 |
. . 3
β’
Ξ£π β
β (vol*βπ΄) =
Ξ£π β β
(vol*ββ¦π / πβ¦π΄) |
83 | 81, 82 | eqtr4di 2790 |
. 2
β’ (π β sup(ran π, β*, < ) = Ξ£π β β
(vol*βπ΄)) |
84 | 5, 83 | breqtrd 5174 |
1
β’ (π β (vol*ββͺ π β β π΄) β€ Ξ£π β β (vol*βπ΄)) |