Step |
Hyp |
Ref |
Expression |
1 |
|
ovolshft.1 |
|- ( ph -> A C_ RR ) |
2 |
|
ovolshft.2 |
|- ( ph -> C e. RR ) |
3 |
|
ovolshft.3 |
|- ( ph -> B = { x e. RR | ( x - C ) e. A } ) |
4 |
|
ovolshft.4 |
|- M = { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } |
5 |
|
ovolshft.5 |
|- S = seq 1 ( + , ( ( abs o. - ) o. F ) ) |
6 |
|
ovolshft.6 |
|- G = ( n e. NN |-> <. ( ( 1st ` ( F ` n ) ) + C ) , ( ( 2nd ` ( F ` n ) ) + C ) >. ) |
7 |
|
ovolshft.7 |
|- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) ) |
8 |
|
ovolshft.8 |
|- ( ph -> A C_ U. ran ( (,) o. F ) ) |
9 |
|
ovolfcl |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) e. RR /\ ( 2nd ` ( F ` n ) ) e. RR /\ ( 1st ` ( F ` n ) ) <_ ( 2nd ` ( F ` n ) ) ) ) |
10 |
7 9
|
sylan |
|- ( ( ph /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) e. RR /\ ( 2nd ` ( F ` n ) ) e. RR /\ ( 1st ` ( F ` n ) ) <_ ( 2nd ` ( F ` n ) ) ) ) |
11 |
10
|
simp1d |
|- ( ( ph /\ n e. NN ) -> ( 1st ` ( F ` n ) ) e. RR ) |
12 |
10
|
simp2d |
|- ( ( ph /\ n e. NN ) -> ( 2nd ` ( F ` n ) ) e. RR ) |
13 |
2
|
adantr |
|- ( ( ph /\ n e. NN ) -> C e. RR ) |
14 |
10
|
simp3d |
|- ( ( ph /\ n e. NN ) -> ( 1st ` ( F ` n ) ) <_ ( 2nd ` ( F ` n ) ) ) |
15 |
11 12 13 14
|
leadd1dd |
|- ( ( ph /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) + C ) <_ ( ( 2nd ` ( F ` n ) ) + C ) ) |
16 |
|
df-br |
|- ( ( ( 1st ` ( F ` n ) ) + C ) <_ ( ( 2nd ` ( F ` n ) ) + C ) <-> <. ( ( 1st ` ( F ` n ) ) + C ) , ( ( 2nd ` ( F ` n ) ) + C ) >. e. <_ ) |
17 |
15 16
|
sylib |
|- ( ( ph /\ n e. NN ) -> <. ( ( 1st ` ( F ` n ) ) + C ) , ( ( 2nd ` ( F ` n ) ) + C ) >. e. <_ ) |
18 |
11 13
|
readdcld |
|- ( ( ph /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) + C ) e. RR ) |
19 |
12 13
|
readdcld |
|- ( ( ph /\ n e. NN ) -> ( ( 2nd ` ( F ` n ) ) + C ) e. RR ) |
20 |
18 19
|
opelxpd |
|- ( ( ph /\ n e. NN ) -> <. ( ( 1st ` ( F ` n ) ) + C ) , ( ( 2nd ` ( F ` n ) ) + C ) >. e. ( RR X. RR ) ) |
21 |
17 20
|
elind |
|- ( ( ph /\ n e. NN ) -> <. ( ( 1st ` ( F ` n ) ) + C ) , ( ( 2nd ` ( F ` n ) ) + C ) >. e. ( <_ i^i ( RR X. RR ) ) ) |
22 |
21 6
|
fmptd |
|- ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) ) |
23 |
|
eqid |
|- ( ( abs o. - ) o. G ) = ( ( abs o. - ) o. G ) |
24 |
23
|
ovolfsf |
|- ( G : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( abs o. - ) o. G ) : NN --> ( 0 [,) +oo ) ) |
25 |
|
ffn |
|- ( ( ( abs o. - ) o. G ) : NN --> ( 0 [,) +oo ) -> ( ( abs o. - ) o. G ) Fn NN ) |
26 |
22 24 25
|
3syl |
|- ( ph -> ( ( abs o. - ) o. G ) Fn NN ) |
27 |
|
eqid |
|- ( ( abs o. - ) o. F ) = ( ( abs o. - ) o. F ) |
28 |
27
|
ovolfsf |
|- ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( abs o. - ) o. F ) : NN --> ( 0 [,) +oo ) ) |
29 |
|
ffn |
|- ( ( ( abs o. - ) o. F ) : NN --> ( 0 [,) +oo ) -> ( ( abs o. - ) o. F ) Fn NN ) |
30 |
7 28 29
|
3syl |
|- ( ph -> ( ( abs o. - ) o. F ) Fn NN ) |
31 |
|
opex |
|- <. ( ( 1st ` ( F ` n ) ) + C ) , ( ( 2nd ` ( F ` n ) ) + C ) >. e. _V |
32 |
6
|
fvmpt2 |
|- ( ( n e. NN /\ <. ( ( 1st ` ( F ` n ) ) + C ) , ( ( 2nd ` ( F ` n ) ) + C ) >. e. _V ) -> ( G ` n ) = <. ( ( 1st ` ( F ` n ) ) + C ) , ( ( 2nd ` ( F ` n ) ) + C ) >. ) |
33 |
31 32
|
mpan2 |
|- ( n e. NN -> ( G ` n ) = <. ( ( 1st ` ( F ` n ) ) + C ) , ( ( 2nd ` ( F ` n ) ) + C ) >. ) |
34 |
33
|
fveq2d |
|- ( n e. NN -> ( 2nd ` ( G ` n ) ) = ( 2nd ` <. ( ( 1st ` ( F ` n ) ) + C ) , ( ( 2nd ` ( F ` n ) ) + C ) >. ) ) |
35 |
|
ovex |
|- ( ( 1st ` ( F ` n ) ) + C ) e. _V |
36 |
|
ovex |
|- ( ( 2nd ` ( F ` n ) ) + C ) e. _V |
37 |
35 36
|
op2nd |
|- ( 2nd ` <. ( ( 1st ` ( F ` n ) ) + C ) , ( ( 2nd ` ( F ` n ) ) + C ) >. ) = ( ( 2nd ` ( F ` n ) ) + C ) |
38 |
34 37
|
eqtrdi |
|- ( n e. NN -> ( 2nd ` ( G ` n ) ) = ( ( 2nd ` ( F ` n ) ) + C ) ) |
39 |
33
|
fveq2d |
|- ( n e. NN -> ( 1st ` ( G ` n ) ) = ( 1st ` <. ( ( 1st ` ( F ` n ) ) + C ) , ( ( 2nd ` ( F ` n ) ) + C ) >. ) ) |
40 |
35 36
|
op1st |
|- ( 1st ` <. ( ( 1st ` ( F ` n ) ) + C ) , ( ( 2nd ` ( F ` n ) ) + C ) >. ) = ( ( 1st ` ( F ` n ) ) + C ) |
41 |
39 40
|
eqtrdi |
|- ( n e. NN -> ( 1st ` ( G ` n ) ) = ( ( 1st ` ( F ` n ) ) + C ) ) |
42 |
38 41
|
oveq12d |
|- ( n e. NN -> ( ( 2nd ` ( G ` n ) ) - ( 1st ` ( G ` n ) ) ) = ( ( ( 2nd ` ( F ` n ) ) + C ) - ( ( 1st ` ( F ` n ) ) + C ) ) ) |
43 |
42
|
adantl |
|- ( ( ph /\ n e. NN ) -> ( ( 2nd ` ( G ` n ) ) - ( 1st ` ( G ` n ) ) ) = ( ( ( 2nd ` ( F ` n ) ) + C ) - ( ( 1st ` ( F ` n ) ) + C ) ) ) |
44 |
12
|
recnd |
|- ( ( ph /\ n e. NN ) -> ( 2nd ` ( F ` n ) ) e. CC ) |
45 |
11
|
recnd |
|- ( ( ph /\ n e. NN ) -> ( 1st ` ( F ` n ) ) e. CC ) |
46 |
13
|
recnd |
|- ( ( ph /\ n e. NN ) -> C e. CC ) |
47 |
44 45 46
|
pnpcan2d |
|- ( ( ph /\ n e. NN ) -> ( ( ( 2nd ` ( F ` n ) ) + C ) - ( ( 1st ` ( F ` n ) ) + C ) ) = ( ( 2nd ` ( F ` n ) ) - ( 1st ` ( F ` n ) ) ) ) |
48 |
43 47
|
eqtrd |
|- ( ( ph /\ n e. NN ) -> ( ( 2nd ` ( G ` n ) ) - ( 1st ` ( G ` n ) ) ) = ( ( 2nd ` ( F ` n ) ) - ( 1st ` ( F ` n ) ) ) ) |
49 |
23
|
ovolfsval |
|- ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( ( ( abs o. - ) o. G ) ` n ) = ( ( 2nd ` ( G ` n ) ) - ( 1st ` ( G ` n ) ) ) ) |
50 |
22 49
|
sylan |
|- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. G ) ` n ) = ( ( 2nd ` ( G ` n ) ) - ( 1st ` ( G ` n ) ) ) ) |
51 |
27
|
ovolfsval |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( ( ( abs o. - ) o. F ) ` n ) = ( ( 2nd ` ( F ` n ) ) - ( 1st ` ( F ` n ) ) ) ) |
52 |
7 51
|
sylan |
|- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. F ) ` n ) = ( ( 2nd ` ( F ` n ) ) - ( 1st ` ( F ` n ) ) ) ) |
53 |
48 50 52
|
3eqtr4d |
|- ( ( ph /\ n e. NN ) -> ( ( ( abs o. - ) o. G ) ` n ) = ( ( ( abs o. - ) o. F ) ` n ) ) |
54 |
26 30 53
|
eqfnfvd |
|- ( ph -> ( ( abs o. - ) o. G ) = ( ( abs o. - ) o. F ) ) |
55 |
54
|
seqeq3d |
|- ( ph -> seq 1 ( + , ( ( abs o. - ) o. G ) ) = seq 1 ( + , ( ( abs o. - ) o. F ) ) ) |
56 |
55 5
|
eqtr4di |
|- ( ph -> seq 1 ( + , ( ( abs o. - ) o. G ) ) = S ) |
57 |
56
|
rneqd |
|- ( ph -> ran seq 1 ( + , ( ( abs o. - ) o. G ) ) = ran S ) |
58 |
57
|
supeq1d |
|- ( ph -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. G ) ) , RR* , < ) = sup ( ran S , RR* , < ) ) |
59 |
3
|
eleq2d |
|- ( ph -> ( y e. B <-> y e. { x e. RR | ( x - C ) e. A } ) ) |
60 |
|
oveq1 |
|- ( x = y -> ( x - C ) = ( y - C ) ) |
61 |
60
|
eleq1d |
|- ( x = y -> ( ( x - C ) e. A <-> ( y - C ) e. A ) ) |
62 |
61
|
elrab |
|- ( y e. { x e. RR | ( x - C ) e. A } <-> ( y e. RR /\ ( y - C ) e. A ) ) |
63 |
59 62
|
bitrdi |
|- ( ph -> ( y e. B <-> ( y e. RR /\ ( y - C ) e. A ) ) ) |
64 |
63
|
biimpa |
|- ( ( ph /\ y e. B ) -> ( y e. RR /\ ( y - C ) e. A ) ) |
65 |
|
breq2 |
|- ( x = ( y - C ) -> ( ( 1st ` ( F ` n ) ) < x <-> ( 1st ` ( F ` n ) ) < ( y - C ) ) ) |
66 |
|
breq1 |
|- ( x = ( y - C ) -> ( x < ( 2nd ` ( F ` n ) ) <-> ( y - C ) < ( 2nd ` ( F ` n ) ) ) ) |
67 |
65 66
|
anbi12d |
|- ( x = ( y - C ) -> ( ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) <-> ( ( 1st ` ( F ` n ) ) < ( y - C ) /\ ( y - C ) < ( 2nd ` ( F ` n ) ) ) ) ) |
68 |
67
|
rexbidv |
|- ( x = ( y - C ) -> ( E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) <-> E. n e. NN ( ( 1st ` ( F ` n ) ) < ( y - C ) /\ ( y - C ) < ( 2nd ` ( F ` n ) ) ) ) ) |
69 |
|
ovolfioo |
|- ( ( A C_ RR /\ F : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( A C_ U. ran ( (,) o. F ) <-> A. x e. A E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) ) ) |
70 |
1 7 69
|
syl2anc |
|- ( ph -> ( A C_ U. ran ( (,) o. F ) <-> A. x e. A E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) ) ) |
71 |
8 70
|
mpbid |
|- ( ph -> A. x e. A E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) ) |
72 |
71
|
adantr |
|- ( ( ph /\ ( y e. RR /\ ( y - C ) e. A ) ) -> A. x e. A E. n e. NN ( ( 1st ` ( F ` n ) ) < x /\ x < ( 2nd ` ( F ` n ) ) ) ) |
73 |
|
simprr |
|- ( ( ph /\ ( y e. RR /\ ( y - C ) e. A ) ) -> ( y - C ) e. A ) |
74 |
68 72 73
|
rspcdva |
|- ( ( ph /\ ( y e. RR /\ ( y - C ) e. A ) ) -> E. n e. NN ( ( 1st ` ( F ` n ) ) < ( y - C ) /\ ( y - C ) < ( 2nd ` ( F ` n ) ) ) ) |
75 |
41
|
adantl |
|- ( ( ( ph /\ ( y e. RR /\ ( y - C ) e. A ) ) /\ n e. NN ) -> ( 1st ` ( G ` n ) ) = ( ( 1st ` ( F ` n ) ) + C ) ) |
76 |
75
|
breq1d |
|- ( ( ( ph /\ ( y e. RR /\ ( y - C ) e. A ) ) /\ n e. NN ) -> ( ( 1st ` ( G ` n ) ) < y <-> ( ( 1st ` ( F ` n ) ) + C ) < y ) ) |
77 |
11
|
adantlr |
|- ( ( ( ph /\ ( y e. RR /\ ( y - C ) e. A ) ) /\ n e. NN ) -> ( 1st ` ( F ` n ) ) e. RR ) |
78 |
2
|
ad2antrr |
|- ( ( ( ph /\ ( y e. RR /\ ( y - C ) e. A ) ) /\ n e. NN ) -> C e. RR ) |
79 |
|
simplrl |
|- ( ( ( ph /\ ( y e. RR /\ ( y - C ) e. A ) ) /\ n e. NN ) -> y e. RR ) |
80 |
77 78 79
|
ltaddsubd |
|- ( ( ( ph /\ ( y e. RR /\ ( y - C ) e. A ) ) /\ n e. NN ) -> ( ( ( 1st ` ( F ` n ) ) + C ) < y <-> ( 1st ` ( F ` n ) ) < ( y - C ) ) ) |
81 |
76 80
|
bitrd |
|- ( ( ( ph /\ ( y e. RR /\ ( y - C ) e. A ) ) /\ n e. NN ) -> ( ( 1st ` ( G ` n ) ) < y <-> ( 1st ` ( F ` n ) ) < ( y - C ) ) ) |
82 |
38
|
adantl |
|- ( ( ( ph /\ ( y e. RR /\ ( y - C ) e. A ) ) /\ n e. NN ) -> ( 2nd ` ( G ` n ) ) = ( ( 2nd ` ( F ` n ) ) + C ) ) |
83 |
82
|
breq2d |
|- ( ( ( ph /\ ( y e. RR /\ ( y - C ) e. A ) ) /\ n e. NN ) -> ( y < ( 2nd ` ( G ` n ) ) <-> y < ( ( 2nd ` ( F ` n ) ) + C ) ) ) |
84 |
12
|
adantlr |
|- ( ( ( ph /\ ( y e. RR /\ ( y - C ) e. A ) ) /\ n e. NN ) -> ( 2nd ` ( F ` n ) ) e. RR ) |
85 |
79 78 84
|
ltsubaddd |
|- ( ( ( ph /\ ( y e. RR /\ ( y - C ) e. A ) ) /\ n e. NN ) -> ( ( y - C ) < ( 2nd ` ( F ` n ) ) <-> y < ( ( 2nd ` ( F ` n ) ) + C ) ) ) |
86 |
83 85
|
bitr4d |
|- ( ( ( ph /\ ( y e. RR /\ ( y - C ) e. A ) ) /\ n e. NN ) -> ( y < ( 2nd ` ( G ` n ) ) <-> ( y - C ) < ( 2nd ` ( F ` n ) ) ) ) |
87 |
81 86
|
anbi12d |
|- ( ( ( ph /\ ( y e. RR /\ ( y - C ) e. A ) ) /\ n e. NN ) -> ( ( ( 1st ` ( G ` n ) ) < y /\ y < ( 2nd ` ( G ` n ) ) ) <-> ( ( 1st ` ( F ` n ) ) < ( y - C ) /\ ( y - C ) < ( 2nd ` ( F ` n ) ) ) ) ) |
88 |
87
|
rexbidva |
|- ( ( ph /\ ( y e. RR /\ ( y - C ) e. A ) ) -> ( E. n e. NN ( ( 1st ` ( G ` n ) ) < y /\ y < ( 2nd ` ( G ` n ) ) ) <-> E. n e. NN ( ( 1st ` ( F ` n ) ) < ( y - C ) /\ ( y - C ) < ( 2nd ` ( F ` n ) ) ) ) ) |
89 |
74 88
|
mpbird |
|- ( ( ph /\ ( y e. RR /\ ( y - C ) e. A ) ) -> E. n e. NN ( ( 1st ` ( G ` n ) ) < y /\ y < ( 2nd ` ( G ` n ) ) ) ) |
90 |
64 89
|
syldan |
|- ( ( ph /\ y e. B ) -> E. n e. NN ( ( 1st ` ( G ` n ) ) < y /\ y < ( 2nd ` ( G ` n ) ) ) ) |
91 |
90
|
ralrimiva |
|- ( ph -> A. y e. B E. n e. NN ( ( 1st ` ( G ` n ) ) < y /\ y < ( 2nd ` ( G ` n ) ) ) ) |
92 |
|
ssrab2 |
|- { x e. RR | ( x - C ) e. A } C_ RR |
93 |
3 92
|
eqsstrdi |
|- ( ph -> B C_ RR ) |
94 |
|
ovolfioo |
|- ( ( B C_ RR /\ G : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( B C_ U. ran ( (,) o. G ) <-> A. y e. B E. n e. NN ( ( 1st ` ( G ` n ) ) < y /\ y < ( 2nd ` ( G ` n ) ) ) ) ) |
95 |
93 22 94
|
syl2anc |
|- ( ph -> ( B C_ U. ran ( (,) o. G ) <-> A. y e. B E. n e. NN ( ( 1st ` ( G ` n ) ) < y /\ y < ( 2nd ` ( G ` n ) ) ) ) ) |
96 |
91 95
|
mpbird |
|- ( ph -> B C_ U. ran ( (,) o. G ) ) |
97 |
|
eqid |
|- seq 1 ( + , ( ( abs o. - ) o. G ) ) = seq 1 ( + , ( ( abs o. - ) o. G ) ) |
98 |
4 97
|
elovolmr |
|- ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ B C_ U. ran ( (,) o. G ) ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. G ) ) , RR* , < ) e. M ) |
99 |
22 96 98
|
syl2anc |
|- ( ph -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. G ) ) , RR* , < ) e. M ) |
100 |
58 99
|
eqeltrrd |
|- ( ph -> sup ( ran S , RR* , < ) e. M ) |