Metamath Proof Explorer

Theorem ovolval2lem

Description: The value of the Lebesgue outer measure for subsets of the reals, expressed using sum^ . (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypothesis ovolval2lem.1 
|- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
Assertion ovolval2lem 
|- ( ph -> ran seq 1 ( + , ( ( abs o. - ) o. F ) ) = ran ( n e. NN |-> sum_ k e. ( 1 ... n ) ( vol ` ( ( [,) o. F ) ` k ) ) ) )

Proof

Step Hyp Ref Expression
1 ovolval2lem.1 
 |-  ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
2 reex 
 |-  RR e. _V
3 2 2 xpex 
 |-  ( RR X. RR ) e. _V
4 inss2 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR )
5 mapss 
 |-  ( ( ( RR X. RR ) e. _V /\ ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR ) ) -> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) C_ ( ( RR X. RR ) ^m NN ) )
6 3 4 5 mp2an 
 |-  ( ( <_ i^i ( RR X. RR ) ) ^m NN ) C_ ( ( RR X. RR ) ^m NN )
7 3 inex2 
 |-  ( <_ i^i ( RR X. RR ) ) e. _V
8 7 a1i 
 |-  ( ph -> ( <_ i^i ( RR X. RR ) ) e. _V )
9 nnex 
 |-  NN e. _V
10 9 a1i 
 |-  ( ph -> NN e. _V )
11 8 10 elmapd 
 |-  ( ph -> ( F e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) <-> F : NN --> ( <_ i^i ( RR X. RR ) ) ) )
12 1 11 mpbird 
 |-  ( ph -> F e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
13 6 12 sselid 
 |-  ( ph -> F e. ( ( RR X. RR ) ^m NN ) )
14 1zzd 
 |-  ( F e. ( ( RR X. RR ) ^m NN ) -> 1 e. ZZ )
15 nnuz 
 |-  NN = ( ZZ>= ` 1 )
16 elmapi 
 |-  ( F e. ( ( RR X. RR ) ^m NN ) -> F : NN --> ( RR X. RR ) )
17 16 adantr 
 |-  ( ( F e. ( ( RR X. RR ) ^m NN ) /\ k e. NN ) -> F : NN --> ( RR X. RR ) )
18 simpr 
 |-  ( ( F e. ( ( RR X. RR ) ^m NN ) /\ k e. NN ) -> k e. NN )
19 17 18 fvovco 
 |-  ( ( F e. ( ( RR X. RR ) ^m NN ) /\ k e. NN ) -> ( ( [,) o. F ) ` k ) = ( ( 1st ` ( F ` k ) ) [,) ( 2nd ` ( F ` k ) ) ) )
20 19 fveq2d 
 |-  ( ( F e. ( ( RR X. RR ) ^m NN ) /\ k e. NN ) -> ( vol ` ( ( [,) o. F ) ` k ) ) = ( vol ` ( ( 1st ` ( F ` k ) ) [,) ( 2nd ` ( F ` k ) ) ) ) )
21 16 ffvelrnda 
 |-  ( ( F e. ( ( RR X. RR ) ^m NN ) /\ k e. NN ) -> ( F ` k ) e. ( RR X. RR ) )
22 xp1st 
 |-  ( ( F ` k ) e. ( RR X. RR ) -> ( 1st ` ( F ` k ) ) e. RR )
23 21 22 syl 
 |-  ( ( F e. ( ( RR X. RR ) ^m NN ) /\ k e. NN ) -> ( 1st ` ( F ` k ) ) e. RR )
24 xp2nd 
 |-  ( ( F ` k ) e. ( RR X. RR ) -> ( 2nd ` ( F ` k ) ) e. RR )
25 21 24 syl 
 |-  ( ( F e. ( ( RR X. RR ) ^m NN ) /\ k e. NN ) -> ( 2nd ` ( F ` k ) ) e. RR )
26 volicore 
 |-  ( ( ( 1st ` ( F ` k ) ) e. RR /\ ( 2nd ` ( F ` k ) ) e. RR ) -> ( vol ` ( ( 1st ` ( F ` k ) ) [,) ( 2nd ` ( F ` k ) ) ) ) e. RR )
27 23 25 26 syl2anc 
 |-  ( ( F e. ( ( RR X. RR ) ^m NN ) /\ k e. NN ) -> ( vol ` ( ( 1st ` ( F ` k ) ) [,) ( 2nd ` ( F ` k ) ) ) ) e. RR )
28 20 27 eqeltrd 
 |-  ( ( F e. ( ( RR X. RR ) ^m NN ) /\ k e. NN ) -> ( vol ` ( ( [,) o. F ) ` k ) ) e. RR )
29 28 recnd 
 |-  ( ( F e. ( ( RR X. RR ) ^m NN ) /\ k e. NN ) -> ( vol ` ( ( [,) o. F ) ` k ) ) e. CC )
30 eqid 
 |-  ( n e. NN |-> sum_ k e. ( 1 ... n ) ( vol ` ( ( [,) o. F ) ` k ) ) ) = ( n e. NN |-> sum_ k e. ( 1 ... n ) ( vol ` ( ( [,) o. F ) ` k ) ) )
31 eqid 
 |-  seq 1 ( + , ( k e. NN |-> ( vol ` ( ( [,) o. F ) ` k ) ) ) ) = seq 1 ( + , ( k e. NN |-> ( vol ` ( ( [,) o. F ) ` k ) ) ) )
32 14 15 29 30 31 fsumsermpt 
 |-  ( F e. ( ( RR X. RR ) ^m NN ) -> ( n e. NN |-> sum_ k e. ( 1 ... n ) ( vol ` ( ( [,) o. F ) ` k ) ) ) = seq 1 ( + , ( k e. NN |-> ( vol ` ( ( [,) o. F ) ` k ) ) ) ) )
33 13 32 syl 
 |-  ( ph -> ( n e. NN |-> sum_ k e. ( 1 ... n ) ( vol ` ( ( [,) o. F ) ` k ) ) ) = seq 1 ( + , ( k e. NN |-> ( vol ` ( ( [,) o. F ) ` k ) ) ) ) )
34 simpr 
 |-  ( ( ( ph /\ k e. NN ) /\ ( 1st ` ( F ` k ) ) < ( 2nd ` ( F ` k ) ) ) -> ( 1st ` ( F ` k ) ) < ( 2nd ` ( F ` k ) ) )
35 34 iftrued 
 |-  ( ( ( ph /\ k e. NN ) /\ ( 1st ` ( F ` k ) ) < ( 2nd ` ( F ` k ) ) ) -> if ( ( 1st ` ( F ` k ) ) < ( 2nd ` ( F ` k ) ) , ( ( 2nd ` ( F ` k ) ) - ( 1st ` ( F ` k ) ) ) , 0 ) = ( ( 2nd ` ( F ` k ) ) - ( 1st ` ( F ` k ) ) ) )
36 13 23 sylan 
 |-  ( ( ph /\ k e. NN ) -> ( 1st ` ( F ` k ) ) e. RR )
37 36 adantr 
 |-  ( ( ( ph /\ k e. NN ) /\ -. ( 1st ` ( F ` k ) ) < ( 2nd ` ( F ` k ) ) ) -> ( 1st ` ( F ` k ) ) e. RR )
38 13 25 sylan 
 |-  ( ( ph /\ k e. NN ) -> ( 2nd ` ( F ` k ) ) e. RR )
39 38 adantr 
 |-  ( ( ( ph /\ k e. NN ) /\ -. ( 1st ` ( F ` k ) ) < ( 2nd ` ( F ` k ) ) ) -> ( 2nd ` ( F ` k ) ) e. RR )
40 ressxr 
 |-  RR C_ RR*
41 40 37 sselid 
 |-  ( ( ( ph /\ k e. NN ) /\ -. ( 1st ` ( F ` k ) ) < ( 2nd ` ( F ` k ) ) ) -> ( 1st ` ( F ` k ) ) e. RR* )
42 40 39 sselid 
 |-  ( ( ( ph /\ k e. NN ) /\ -. ( 1st ` ( F ` k ) ) < ( 2nd ` ( F ` k ) ) ) -> ( 2nd ` ( F ` k ) ) e. RR* )
43 xpss 
 |-  ( RR X. RR ) C_ ( _V X. _V )
44 43 21 sselid 
 |-  ( ( F e. ( ( RR X. RR ) ^m NN ) /\ k e. NN ) -> ( F ` k ) e. ( _V X. _V ) )
45 1st2ndb 
 |-  ( ( F ` k ) e. ( _V X. _V ) <-> ( F ` k ) = <. ( 1st ` ( F ` k ) ) , ( 2nd ` ( F ` k ) ) >. )
46 44 45 sylib 
 |-  ( ( F e. ( ( RR X. RR ) ^m NN ) /\ k e. NN ) -> ( F ` k ) = <. ( 1st ` ( F ` k ) ) , ( 2nd ` ( F ` k ) ) >. )
47 13 46 sylan 
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) = <. ( 1st ` ( F ` k ) ) , ( 2nd ` ( F ` k ) ) >. )
48 47 eqcomd 
 |-  ( ( ph /\ k e. NN ) -> <. ( 1st ` ( F ` k ) ) , ( 2nd ` ( F ` k ) ) >. = ( F ` k ) )
49 inss1 
 |-  ( <_ i^i ( RR X. RR ) ) C_ <_
50 49 a1i 
 |-  ( ph -> ( <_ i^i ( RR X. RR ) ) C_ <_ )
51 1 50 fssd 
 |-  ( ph -> F : NN --> <_ )
52 51 ffvelrnda 
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) e. <_ )
53 48 52 eqeltrd 
 |-  ( ( ph /\ k e. NN ) -> <. ( 1st ` ( F ` k ) ) , ( 2nd ` ( F ` k ) ) >. e. <_ )
54 df-br 
 |-  ( ( 1st ` ( F ` k ) ) <_ ( 2nd ` ( F ` k ) ) <-> <. ( 1st ` ( F ` k ) ) , ( 2nd ` ( F ` k ) ) >. e. <_ )
55 53 54 sylibr 
 |-  ( ( ph /\ k e. NN ) -> ( 1st ` ( F ` k ) ) <_ ( 2nd ` ( F ` k ) ) )
56 55 adantr 
 |-  ( ( ( ph /\ k e. NN ) /\ -. ( 1st ` ( F ` k ) ) < ( 2nd ` ( F ` k ) ) ) -> ( 1st ` ( F ` k ) ) <_ ( 2nd ` ( F ` k ) ) )
57 simpr 
 |-  ( ( ( ph /\ k e. NN ) /\ -. ( 1st ` ( F ` k ) ) < ( 2nd ` ( F ` k ) ) ) -> -. ( 1st ` ( F ` k ) ) < ( 2nd ` ( F ` k ) ) )
58 39 37 lenltd 
 |-  ( ( ( ph /\ k e. NN ) /\ -. ( 1st ` ( F ` k ) ) < ( 2nd ` ( F ` k ) ) ) -> ( ( 2nd ` ( F ` k ) ) <_ ( 1st ` ( F ` k ) ) <-> -. ( 1st ` ( F ` k ) ) < ( 2nd ` ( F ` k ) ) ) )
59 57 58 mpbird 
 |-  ( ( ( ph /\ k e. NN ) /\ -. ( 1st ` ( F ` k ) ) < ( 2nd ` ( F ` k ) ) ) -> ( 2nd ` ( F ` k ) ) <_ ( 1st ` ( F ` k ) ) )
60 41 42 56 59 xrletrid 
 |-  ( ( ( ph /\ k e. NN ) /\ -. ( 1st ` ( F ` k ) ) < ( 2nd ` ( F ` k ) ) ) -> ( 1st ` ( F ` k ) ) = ( 2nd ` ( F ` k ) ) )
61 simp3 
 |-  ( ( ( 1st ` ( F ` k ) ) e. RR /\ ( 2nd ` ( F ` k ) ) e. RR /\ ( 1st ` ( F ` k ) ) = ( 2nd ` ( F ` k ) ) ) -> ( 1st ` ( F ` k ) ) = ( 2nd ` ( F ` k ) ) )
62 simp1 
 |-  ( ( ( 1st ` ( F ` k ) ) e. RR /\ ( 2nd ` ( F ` k ) ) e. RR /\ ( 1st ` ( F ` k ) ) = ( 2nd ` ( F ` k ) ) ) -> ( 1st ` ( F ` k ) ) e. RR )
63 simp2 
 |-  ( ( ( 1st ` ( F ` k ) ) e. RR /\ ( 2nd ` ( F ` k ) ) e. RR /\ ( 1st ` ( F ` k ) ) = ( 2nd ` ( F ` k ) ) ) -> ( 2nd ` ( F ` k ) ) e. RR )
64 62 63 eqleltd 
 |-  ( ( ( 1st ` ( F ` k ) ) e. RR /\ ( 2nd ` ( F ` k ) ) e. RR /\ ( 1st ` ( F ` k ) ) = ( 2nd ` ( F ` k ) ) ) -> ( ( 1st ` ( F ` k ) ) = ( 2nd ` ( F ` k ) ) <-> ( ( 1st ` ( F ` k ) ) <_ ( 2nd ` ( F ` k ) ) /\ -. ( 1st ` ( F ` k ) ) < ( 2nd ` ( F ` k ) ) ) ) )
65 61 64 mpbid 
 |-  ( ( ( 1st ` ( F ` k ) ) e. RR /\ ( 2nd ` ( F ` k ) ) e. RR /\ ( 1st ` ( F ` k ) ) = ( 2nd ` ( F ` k ) ) ) -> ( ( 1st ` ( F ` k ) ) <_ ( 2nd ` ( F ` k ) ) /\ -. ( 1st ` ( F ` k ) ) < ( 2nd ` ( F ` k ) ) ) )
66 65 simprd 
 |-  ( ( ( 1st ` ( F ` k ) ) e. RR /\ ( 2nd ` ( F ` k ) ) e. RR /\ ( 1st ` ( F ` k ) ) = ( 2nd ` ( F ` k ) ) ) -> -. ( 1st ` ( F ` k ) ) < ( 2nd ` ( F ` k ) ) )
67 66 iffalsed 
 |-  ( ( ( 1st ` ( F ` k ) ) e. RR /\ ( 2nd ` ( F ` k ) ) e. RR /\ ( 1st ` ( F ` k ) ) = ( 2nd ` ( F ` k ) ) ) -> if ( ( 1st ` ( F ` k ) ) < ( 2nd ` ( F ` k ) ) , ( ( 2nd ` ( F ` k ) ) - ( 1st ` ( F ` k ) ) ) , 0 ) = 0 )
68 63 recnd 
 |-  ( ( ( 1st ` ( F ` k ) ) e. RR /\ ( 2nd ` ( F ` k ) ) e. RR /\ ( 1st ` ( F ` k ) ) = ( 2nd ` ( F ` k ) ) ) -> ( 2nd ` ( F ` k ) ) e. CC )
69 61 eqcomd 
 |-  ( ( ( 1st ` ( F ` k ) ) e. RR /\ ( 2nd ` ( F ` k ) ) e. RR /\ ( 1st ` ( F ` k ) ) = ( 2nd ` ( F ` k ) ) ) -> ( 2nd ` ( F ` k ) ) = ( 1st ` ( F ` k ) ) )
70 68 69 subeq0bd 
 |-  ( ( ( 1st ` ( F ` k ) ) e. RR /\ ( 2nd ` ( F ` k ) ) e. RR /\ ( 1st ` ( F ` k ) ) = ( 2nd ` ( F ` k ) ) ) -> ( ( 2nd ` ( F ` k ) ) - ( 1st ` ( F ` k ) ) ) = 0 )
71 67 70 eqtr4d 
 |-  ( ( ( 1st ` ( F ` k ) ) e. RR /\ ( 2nd ` ( F ` k ) ) e. RR /\ ( 1st ` ( F ` k ) ) = ( 2nd ` ( F ` k ) ) ) -> if ( ( 1st ` ( F ` k ) ) < ( 2nd ` ( F ` k ) ) , ( ( 2nd ` ( F ` k ) ) - ( 1st ` ( F ` k ) ) ) , 0 ) = ( ( 2nd ` ( F ` k ) ) - ( 1st ` ( F ` k ) ) ) )
72 37 39 60 71 syl3anc 
 |-  ( ( ( ph /\ k e. NN ) /\ -. ( 1st ` ( F ` k ) ) < ( 2nd ` ( F ` k ) ) ) -> if ( ( 1st ` ( F ` k ) ) < ( 2nd ` ( F ` k ) ) , ( ( 2nd ` ( F ` k ) ) - ( 1st ` ( F ` k ) ) ) , 0 ) = ( ( 2nd ` ( F ` k ) ) - ( 1st ` ( F ` k ) ) ) )
73 35 72 pm2.61dan 
 |-  ( ( ph /\ k e. NN ) -> if ( ( 1st ` ( F ` k ) ) < ( 2nd ` ( F ` k ) ) , ( ( 2nd ` ( F ` k ) ) - ( 1st ` ( F ` k ) ) ) , 0 ) = ( ( 2nd ` ( F ` k ) ) - ( 1st ` ( F ` k ) ) ) )
74 volico 
 |-  ( ( ( 1st ` ( F ` k ) ) e. RR /\ ( 2nd ` ( F ` k ) ) e. RR ) -> ( vol ` ( ( 1st ` ( F ` k ) ) [,) ( 2nd ` ( F ` k ) ) ) ) = if ( ( 1st ` ( F ` k ) ) < ( 2nd ` ( F ` k ) ) , ( ( 2nd ` ( F ` k ) ) - ( 1st ` ( F ` k ) ) ) , 0 ) )
75 36 38 74 syl2anc 
 |-  ( ( ph /\ k e. NN ) -> ( vol ` ( ( 1st ` ( F ` k ) ) [,) ( 2nd ` ( F ` k ) ) ) ) = if ( ( 1st ` ( F ` k ) ) < ( 2nd ` ( F ` k ) ) , ( ( 2nd ` ( F ` k ) ) - ( 1st ` ( F ` k ) ) ) , 0 ) )
76 36 38 55 abssuble0d 
 |-  ( ( ph /\ k e. NN ) -> ( abs ` ( ( 1st ` ( F ` k ) ) - ( 2nd ` ( F ` k ) ) ) ) = ( ( 2nd ` ( F ` k ) ) - ( 1st ` ( F ` k ) ) ) )
77 73 75 76 3eqtr4d 
 |-  ( ( ph /\ k e. NN ) -> ( vol ` ( ( 1st ` ( F ` k ) ) [,) ( 2nd ` ( F ` k ) ) ) ) = ( abs ` ( ( 1st ` ( F ` k ) ) - ( 2nd ` ( F ` k ) ) ) ) )
78 13 adantr 
 |-  ( ( ph /\ k e. NN ) -> F e. ( ( RR X. RR ) ^m NN ) )
79 simpr 
 |-  ( ( ph /\ k e. NN ) -> k e. NN )
80 78 79 20 syl2anc 
 |-  ( ( ph /\ k e. NN ) -> ( vol ` ( ( [,) o. F ) ` k ) ) = ( vol ` ( ( 1st ` ( F ` k ) ) [,) ( 2nd ` ( F ` k ) ) ) ) )
81 46 fveq2d 
 |-  ( ( F e. ( ( RR X. RR ) ^m NN ) /\ k e. NN ) -> ( ( abs o. - ) ` ( F ` k ) ) = ( ( abs o. - ) ` <. ( 1st ` ( F ` k ) ) , ( 2nd ` ( F ` k ) ) >. ) )
82 df-ov 
 |-  ( ( 1st ` ( F ` k ) ) ( abs o. - ) ( 2nd ` ( F ` k ) ) ) = ( ( abs o. - ) ` <. ( 1st ` ( F ` k ) ) , ( 2nd ` ( F ` k ) ) >. )
83 82 eqcomi 
 |-  ( ( abs o. - ) ` <. ( 1st ` ( F ` k ) ) , ( 2nd ` ( F ` k ) ) >. ) = ( ( 1st ` ( F ` k ) ) ( abs o. - ) ( 2nd ` ( F ` k ) ) )
84 83 a1i 
 |-  ( ( F e. ( ( RR X. RR ) ^m NN ) /\ k e. NN ) -> ( ( abs o. - ) ` <. ( 1st ` ( F ` k ) ) , ( 2nd ` ( F ` k ) ) >. ) = ( ( 1st ` ( F ` k ) ) ( abs o. - ) ( 2nd ` ( F ` k ) ) ) )
85 23 recnd 
 |-  ( ( F e. ( ( RR X. RR ) ^m NN ) /\ k e. NN ) -> ( 1st ` ( F ` k ) ) e. CC )
86 25 recnd 
 |-  ( ( F e. ( ( RR X. RR ) ^m NN ) /\ k e. NN ) -> ( 2nd ` ( F ` k ) ) e. CC )
87 eqid 
 |-  ( abs o. - ) = ( abs o. - )
88 87 cnmetdval 
 |-  ( ( ( 1st ` ( F ` k ) ) e. CC /\ ( 2nd ` ( F ` k ) ) e. CC ) -> ( ( 1st ` ( F ` k ) ) ( abs o. - ) ( 2nd ` ( F ` k ) ) ) = ( abs ` ( ( 1st ` ( F ` k ) ) - ( 2nd ` ( F ` k ) ) ) ) )
89 85 86 88 syl2anc 
 |-  ( ( F e. ( ( RR X. RR ) ^m NN ) /\ k e. NN ) -> ( ( 1st ` ( F ` k ) ) ( abs o. - ) ( 2nd ` ( F ` k ) ) ) = ( abs ` ( ( 1st ` ( F ` k ) ) - ( 2nd ` ( F ` k ) ) ) ) )
90 81 84 89 3eqtrd 
 |-  ( ( F e. ( ( RR X. RR ) ^m NN ) /\ k e. NN ) -> ( ( abs o. - ) ` ( F ` k ) ) = ( abs ` ( ( 1st ` ( F ` k ) ) - ( 2nd ` ( F ` k ) ) ) ) )
91 78 79 90 syl2anc 
 |-  ( ( ph /\ k e. NN ) -> ( ( abs o. - ) ` ( F ` k ) ) = ( abs ` ( ( 1st ` ( F ` k ) ) - ( 2nd ` ( F ` k ) ) ) ) )
92 77 80 91 3eqtr4d 
 |-  ( ( ph /\ k e. NN ) -> ( vol ` ( ( [,) o. F ) ` k ) ) = ( ( abs o. - ) ` ( F ` k ) ) )
93 92 mpteq2dva 
 |-  ( ph -> ( k e. NN |-> ( vol ` ( ( [,) o. F ) ` k ) ) ) = ( k e. NN |-> ( ( abs o. - ) ` ( F ` k ) ) ) )
94 13 16 syl 
 |-  ( ph -> F : NN --> ( RR X. RR ) )
95 rr2sscn2 
 |-  ( RR X. RR ) C_ ( CC X. CC )
96 95 a1i 
 |-  ( ph -> ( RR X. RR ) C_ ( CC X. CC ) )
97 absf 
 |-  abs : CC --> RR
98 subf 
 |-  - : ( CC X. CC ) --> CC
99 fco 
 |-  ( ( abs : CC --> RR /\ - : ( CC X. CC ) --> CC ) -> ( abs o. - ) : ( CC X. CC ) --> RR )
100 97 98 99 mp2an 
 |-  ( abs o. - ) : ( CC X. CC ) --> RR
101 100 a1i 
 |-  ( ph -> ( abs o. - ) : ( CC X. CC ) --> RR )
102 94 96 101 fcomptss 
 |-  ( ph -> ( ( abs o. - ) o. F ) = ( k e. NN |-> ( ( abs o. - ) ` ( F ` k ) ) ) )
103 93 102 eqtr4d 
 |-  ( ph -> ( k e. NN |-> ( vol ` ( ( [,) o. F ) ` k ) ) ) = ( ( abs o. - ) o. F ) )
104 103 seqeq3d 
 |-  ( ph -> seq 1 ( + , ( k e. NN |-> ( vol ` ( ( [,) o. F ) ` k ) ) ) ) = seq 1 ( + , ( ( abs o. - ) o. F ) ) )
105 33 104 eqtr2d 
 |-  ( ph -> seq 1 ( + , ( ( abs o. - ) o. F ) ) = ( n e. NN |-> sum_ k e. ( 1 ... n ) ( vol ` ( ( [,) o. F ) ` k ) ) ) )
106 105 rneqd 
 |-  ( ph -> ran seq 1 ( + , ( ( abs o. - ) o. F ) ) = ran ( n e. NN |-> sum_ k e. ( 1 ... n ) ( vol ` ( ( [,) o. F ) ` k ) ) ) )