Metamath Proof Explorer

Theorem itg2i1fseqle

Description: Subject to the conditions coming from mbfi1fseq , the sequence of simple functions are all less than the target function F . (Contributed by Mario Carneiro, 17-Aug-2014)

Ref Expression
Hypotheses itg2i1fseq.1 
|- ( ph -> F e. MblFn )
itg2i1fseq.2 
|- ( ph -> F : RR --> ( 0 [,) +oo ) )
itg2i1fseq.3 
|- ( ph -> P : NN --> dom S.1 )
itg2i1fseq.4 
|- ( ph -> A. n e. NN ( 0p oR <_ ( P ` n ) /\ ( P ` n ) oR <_ ( P ` ( n + 1 ) ) ) )
itg2i1fseq.5 
|- ( ph -> A. x e. RR ( n e. NN |-> ( ( P ` n ) ` x ) ) ~~> ( F ` x ) )
Assertion itg2i1fseqle 
|- ( ( ph /\ M e. NN ) -> ( P ` M ) oR <_ F )

Proof

Step Hyp Ref Expression
1 itg2i1fseq.1 
 |-  ( ph -> F e. MblFn )
2 itg2i1fseq.2 
 |-  ( ph -> F : RR --> ( 0 [,) +oo ) )
3 itg2i1fseq.3 
 |-  ( ph -> P : NN --> dom S.1 )
4 itg2i1fseq.4 
 |-  ( ph -> A. n e. NN ( 0p oR <_ ( P ` n ) /\ ( P ` n ) oR <_ ( P ` ( n + 1 ) ) ) )
5 itg2i1fseq.5 
 |-  ( ph -> A. x e. RR ( n e. NN |-> ( ( P ` n ) ` x ) ) ~~> ( F ` x ) )
6 fveq2 
 |-  ( n = M -> ( P ` n ) = ( P ` M ) )
7 6 fveq1d 
 |-  ( n = M -> ( ( P ` n ) ` y ) = ( ( P ` M ) ` y ) )
8 eqid 
 |-  ( n e. NN |-> ( ( P ` n ) ` y ) ) = ( n e. NN |-> ( ( P ` n ) ` y ) )
9 fvex 
 |-  ( ( P ` M ) ` y ) e. _V
10 7 8 9 fvmpt 
 |-  ( M e. NN -> ( ( n e. NN |-> ( ( P ` n ) ` y ) ) ` M ) = ( ( P ` M ) ` y ) )
11 10 ad2antlr 
 |-  ( ( ( ph /\ M e. NN ) /\ y e. RR ) -> ( ( n e. NN |-> ( ( P ` n ) ` y ) ) ` M ) = ( ( P ` M ) ` y ) )
12 nnuz 
 |-  NN = ( ZZ>= ` 1 )
13 simplr 
 |-  ( ( ( ph /\ M e. NN ) /\ y e. RR ) -> M e. NN )
14 fveq2 
 |-  ( x = y -> ( ( P ` n ) ` x ) = ( ( P ` n ) ` y ) )
15 14 mpteq2dv 
 |-  ( x = y -> ( n e. NN |-> ( ( P ` n ) ` x ) ) = ( n e. NN |-> ( ( P ` n ) ` y ) ) )
16 fveq2 
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
17 15 16 breq12d 
 |-  ( x = y -> ( ( n e. NN |-> ( ( P ` n ) ` x ) ) ~~> ( F ` x ) <-> ( n e. NN |-> ( ( P ` n ) ` y ) ) ~~> ( F ` y ) ) )
18 17 rspccva 
 |-  ( ( A. x e. RR ( n e. NN |-> ( ( P ` n ) ` x ) ) ~~> ( F ` x ) /\ y e. RR ) -> ( n e. NN |-> ( ( P ` n ) ` y ) ) ~~> ( F ` y ) )
19 5 18 sylan 
 |-  ( ( ph /\ y e. RR ) -> ( n e. NN |-> ( ( P ` n ) ` y ) ) ~~> ( F ` y ) )
20 19 adantlr 
 |-  ( ( ( ph /\ M e. NN ) /\ y e. RR ) -> ( n e. NN |-> ( ( P ` n ) ` y ) ) ~~> ( F ` y ) )
21 fveq2 
 |-  ( n = k -> ( P ` n ) = ( P ` k ) )
22 21 fveq1d 
 |-  ( n = k -> ( ( P ` n ) ` y ) = ( ( P ` k ) ` y ) )
23 fvex 
 |-  ( ( P ` k ) ` y ) e. _V
24 22 8 23 fvmpt 
 |-  ( k e. NN -> ( ( n e. NN |-> ( ( P ` n ) ` y ) ) ` k ) = ( ( P ` k ) ` y ) )
25 24 adantl 
 |-  ( ( ( ph /\ y e. RR ) /\ k e. NN ) -> ( ( n e. NN |-> ( ( P ` n ) ` y ) ) ` k ) = ( ( P ` k ) ` y ) )
26 3 ffvelcdmda 
 |-  ( ( ph /\ k e. NN ) -> ( P ` k ) e. dom S.1 )
27 i1ff 
 |-  ( ( P ` k ) e. dom S.1 -> ( P ` k ) : RR --> RR )
28 26 27 syl 
 |-  ( ( ph /\ k e. NN ) -> ( P ` k ) : RR --> RR )
29 28 ffvelcdmda 
 |-  ( ( ( ph /\ k e. NN ) /\ y e. RR ) -> ( ( P ` k ) ` y ) e. RR )
30 29 an32s 
 |-  ( ( ( ph /\ y e. RR ) /\ k e. NN ) -> ( ( P ` k ) ` y ) e. RR )
31 25 30 eqeltrd 
 |-  ( ( ( ph /\ y e. RR ) /\ k e. NN ) -> ( ( n e. NN |-> ( ( P ` n ) ` y ) ) ` k ) e. RR )
32 31 adantllr 
 |-  ( ( ( ( ph /\ M e. NN ) /\ y e. RR ) /\ k e. NN ) -> ( ( n e. NN |-> ( ( P ` n ) ` y ) ) ` k ) e. RR )
33 simpr 
 |-  ( ( 0p oR <_ ( P ` n ) /\ ( P ` n ) oR <_ ( P ` ( n + 1 ) ) ) -> ( P ` n ) oR <_ ( P ` ( n + 1 ) ) )
34 33 ralimi 
 |-  ( A. n e. NN ( 0p oR <_ ( P ` n ) /\ ( P ` n ) oR <_ ( P ` ( n + 1 ) ) ) -> A. n e. NN ( P ` n ) oR <_ ( P ` ( n + 1 ) ) )
35 4 34 syl 
 |-  ( ph -> A. n e. NN ( P ` n ) oR <_ ( P ` ( n + 1 ) ) )
36 fvoveq1 
 |-  ( n = k -> ( P ` ( n + 1 ) ) = ( P ` ( k + 1 ) ) )
37 21 36 breq12d 
 |-  ( n = k -> ( ( P ` n ) oR <_ ( P ` ( n + 1 ) ) <-> ( P ` k ) oR <_ ( P ` ( k + 1 ) ) ) )
38 37 rspccva 
 |-  ( ( A. n e. NN ( P ` n ) oR <_ ( P ` ( n + 1 ) ) /\ k e. NN ) -> ( P ` k ) oR <_ ( P ` ( k + 1 ) ) )
39 35 38 sylan 
 |-  ( ( ph /\ k e. NN ) -> ( P ` k ) oR <_ ( P ` ( k + 1 ) ) )
40 ffn 
 |-  ( ( P ` k ) : RR --> RR -> ( P ` k ) Fn RR )
41 26 27 40 3syl 
 |-  ( ( ph /\ k e. NN ) -> ( P ` k ) Fn RR )
42 peano2nn 
 |-  ( k e. NN -> ( k + 1 ) e. NN )
43 ffvelcdm 
 |-  ( ( P : NN --> dom S.1 /\ ( k + 1 ) e. NN ) -> ( P ` ( k + 1 ) ) e. dom S.1 )
44 3 42 43 syl2an 
 |-  ( ( ph /\ k e. NN ) -> ( P ` ( k + 1 ) ) e. dom S.1 )
45 i1ff 
 |-  ( ( P ` ( k + 1 ) ) e. dom S.1 -> ( P ` ( k + 1 ) ) : RR --> RR )
46 ffn 
 |-  ( ( P ` ( k + 1 ) ) : RR --> RR -> ( P ` ( k + 1 ) ) Fn RR )
47 44 45 46 3syl 
 |-  ( ( ph /\ k e. NN ) -> ( P ` ( k + 1 ) ) Fn RR )
48 reex 
 |-  RR e. _V
49 48 a1i 
 |-  ( ( ph /\ k e. NN ) -> RR e. _V )
50 inidm 
 |-  ( RR i^i RR ) = RR
51 eqidd 
 |-  ( ( ( ph /\ k e. NN ) /\ y e. RR ) -> ( ( P ` k ) ` y ) = ( ( P ` k ) ` y ) )
52 eqidd 
 |-  ( ( ( ph /\ k e. NN ) /\ y e. RR ) -> ( ( P ` ( k + 1 ) ) ` y ) = ( ( P ` ( k + 1 ) ) ` y ) )
53 41 47 49 49 50 51 52 ofrfval 
 |-  ( ( ph /\ k e. NN ) -> ( ( P ` k ) oR <_ ( P ` ( k + 1 ) ) <-> A. y e. RR ( ( P ` k ) ` y ) <_ ( ( P ` ( k + 1 ) ) ` y ) ) )
54 39 53 mpbid 
 |-  ( ( ph /\ k e. NN ) -> A. y e. RR ( ( P ` k ) ` y ) <_ ( ( P ` ( k + 1 ) ) ` y ) )
55 54 r19.21bi 
 |-  ( ( ( ph /\ k e. NN ) /\ y e. RR ) -> ( ( P ` k ) ` y ) <_ ( ( P ` ( k + 1 ) ) ` y ) )
56 55 an32s 
 |-  ( ( ( ph /\ y e. RR ) /\ k e. NN ) -> ( ( P ` k ) ` y ) <_ ( ( P ` ( k + 1 ) ) ` y ) )
57 fveq2 
 |-  ( n = ( k + 1 ) -> ( P ` n ) = ( P ` ( k + 1 ) ) )
58 57 fveq1d 
 |-  ( n = ( k + 1 ) -> ( ( P ` n ) ` y ) = ( ( P ` ( k + 1 ) ) ` y ) )
59 fvex 
 |-  ( ( P ` ( k + 1 ) ) ` y ) e. _V
60 58 8 59 fvmpt 
 |-  ( ( k + 1 ) e. NN -> ( ( n e. NN |-> ( ( P ` n ) ` y ) ) ` ( k + 1 ) ) = ( ( P ` ( k + 1 ) ) ` y ) )
61 42 60 syl 
 |-  ( k e. NN -> ( ( n e. NN |-> ( ( P ` n ) ` y ) ) ` ( k + 1 ) ) = ( ( P ` ( k + 1 ) ) ` y ) )
62 61 adantl 
 |-  ( ( ( ph /\ y e. RR ) /\ k e. NN ) -> ( ( n e. NN |-> ( ( P ` n ) ` y ) ) ` ( k + 1 ) ) = ( ( P ` ( k + 1 ) ) ` y ) )
63 56 25 62 3brtr4d 
 |-  ( ( ( ph /\ y e. RR ) /\ k e. NN ) -> ( ( n e. NN |-> ( ( P ` n ) ` y ) ) ` k ) <_ ( ( n e. NN |-> ( ( P ` n ) ` y ) ) ` ( k + 1 ) ) )
64 63 adantllr 
 |-  ( ( ( ( ph /\ M e. NN ) /\ y e. RR ) /\ k e. NN ) -> ( ( n e. NN |-> ( ( P ` n ) ` y ) ) ` k ) <_ ( ( n e. NN |-> ( ( P ` n ) ` y ) ) ` ( k + 1 ) ) )
65 12 13 20 32 64 climub 
 |-  ( ( ( ph /\ M e. NN ) /\ y e. RR ) -> ( ( n e. NN |-> ( ( P ` n ) ` y ) ) ` M ) <_ ( F ` y ) )
66 11 65 eqbrtrrd 
 |-  ( ( ( ph /\ M e. NN ) /\ y e. RR ) -> ( ( P ` M ) ` y ) <_ ( F ` y ) )
67 66 ralrimiva 
 |-  ( ( ph /\ M e. NN ) -> A. y e. RR ( ( P ` M ) ` y ) <_ ( F ` y ) )
68 3 ffvelcdmda 
 |-  ( ( ph /\ M e. NN ) -> ( P ` M ) e. dom S.1 )
69 i1ff 
 |-  ( ( P ` M ) e. dom S.1 -> ( P ` M ) : RR --> RR )
70 ffn 
 |-  ( ( P ` M ) : RR --> RR -> ( P ` M ) Fn RR )
71 68 69 70 3syl 
 |-  ( ( ph /\ M e. NN ) -> ( P ` M ) Fn RR )
72 2 ffnd 
 |-  ( ph -> F Fn RR )
73 72 adantr 
 |-  ( ( ph /\ M e. NN ) -> F Fn RR )
74 48 a1i 
 |-  ( ( ph /\ M e. NN ) -> RR e. _V )
75 eqidd 
 |-  ( ( ( ph /\ M e. NN ) /\ y e. RR ) -> ( ( P ` M ) ` y ) = ( ( P ` M ) ` y ) )
76 eqidd 
 |-  ( ( ( ph /\ M e. NN ) /\ y e. RR ) -> ( F ` y ) = ( F ` y ) )
77 71 73 74 74 50 75 76 ofrfval 
 |-  ( ( ph /\ M e. NN ) -> ( ( P ` M ) oR <_ F <-> A. y e. RR ( ( P ` M ) ` y ) <_ ( F ` y ) ) )
78 67 77 mpbird 
 |-  ( ( ph /\ M e. NN ) -> ( P ` M ) oR <_ F )