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 )