Metamath Proof Explorer

Theorem ovolshftlem1

Description: Lemma for ovolshft . (Contributed by Mario Carneiro, 22-Mar-2014)

Ref Expression
Hypotheses ovolshft.1 
|- ( ph -> A C_ RR )
ovolshft.2 
|- ( ph -> C e. RR )
ovolshft.3 
|- ( ph -> B = { x e. RR | ( x - C ) e. A } )
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* , < ) ) }
ovolshft.5 
|- S = seq 1 ( + , ( ( abs o. - ) o. F ) )
ovolshft.6 
|- G = ( n e. NN |-> <. ( ( 1st ` ( F ` n ) ) + C ) , ( ( 2nd ` ( F ` n ) ) + C ) >. )
ovolshft.7 
|- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
ovolshft.8 
|- ( ph -> A C_ U. ran ( (,) o. F ) )
Assertion ovolshftlem1 
|- ( ph -> sup ( ran S , RR* , < ) e. M )

Proof

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 )