Metamath Proof Explorer

Theorem ovolicc2lem2

Description: Lemma for ovolicc2 . (Contributed by Mario Carneiro, 14-Jun-2014)

Ref Expression
Hypotheses ovolicc.1 
|- ( ph -> A e. RR )
ovolicc.2 
|- ( ph -> B e. RR )
ovolicc.3 
|- ( ph -> A <_ B )
ovolicc2.4 
|- S = seq 1 ( + , ( ( abs o. - ) o. F ) )
ovolicc2.5 
|- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
ovolicc2.6 
|- ( ph -> U e. ( ~P ran ( (,) o. F ) i^i Fin ) )
ovolicc2.7 
|- ( ph -> ( A [,] B ) C_ U. U )
ovolicc2.8 
|- ( ph -> G : U --> NN )
ovolicc2.9 
|- ( ( ph /\ t e. U ) -> ( ( (,) o. F ) ` ( G ` t ) ) = t )
ovolicc2.10 
|- T = { u e. U | ( u i^i ( A [,] B ) ) =/= (/) }
ovolicc2.11 
|- ( ph -> H : T --> T )
ovolicc2.12 
|- ( ( ph /\ t e. T ) -> if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. ( H ` t ) )
ovolicc2.13 
|- ( ph -> A e. C )
ovolicc2.14 
|- ( ph -> C e. T )
ovolicc2.15 
|- K = seq 1 ( ( H o. 1st ) , ( NN X. { C } ) )
ovolicc2.16 
|- W = { n e. NN | B e. ( K ` n ) }
Assertion ovolicc2lem2 
|- ( ( ph /\ ( N e. NN /\ -. N e. W ) ) -> ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) <_ B )

Proof

Step Hyp Ref Expression
1 ovolicc.1 
 |-  ( ph -> A e. RR )
2 ovolicc.2 
 |-  ( ph -> B e. RR )
3 ovolicc.3 
 |-  ( ph -> A <_ B )
4 ovolicc2.4 
 |-  S = seq 1 ( + , ( ( abs o. - ) o. F ) )
5 ovolicc2.5 
 |-  ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
6 ovolicc2.6 
 |-  ( ph -> U e. ( ~P ran ( (,) o. F ) i^i Fin ) )
7 ovolicc2.7 
 |-  ( ph -> ( A [,] B ) C_ U. U )
8 ovolicc2.8 
 |-  ( ph -> G : U --> NN )
9 ovolicc2.9 
 |-  ( ( ph /\ t e. U ) -> ( ( (,) o. F ) ` ( G ` t ) ) = t )
10 ovolicc2.10 
 |-  T = { u e. U | ( u i^i ( A [,] B ) ) =/= (/) }
11 ovolicc2.11 
 |-  ( ph -> H : T --> T )
12 ovolicc2.12 
 |-  ( ( ph /\ t e. T ) -> if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. ( H ` t ) )
13 ovolicc2.13 
 |-  ( ph -> A e. C )
14 ovolicc2.14 
 |-  ( ph -> C e. T )
15 ovolicc2.15 
 |-  K = seq 1 ( ( H o. 1st ) , ( NN X. { C } ) )
16 ovolicc2.16 
 |-  W = { n e. NN | B e. ( K ` n ) }
17 2 adantr 
 |-  ( ( ph /\ N e. NN ) -> B e. RR )
18 inss2 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR )
19 fss 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR ) ) -> F : NN --> ( RR X. RR ) )
20 5 18 19 sylancl 
 |-  ( ph -> F : NN --> ( RR X. RR ) )
21 20 adantr 
 |-  ( ( ph /\ N e. NN ) -> F : NN --> ( RR X. RR ) )
22 8 adantr 
 |-  ( ( ph /\ N e. NN ) -> G : U --> NN )
23 nnuz 
 |-  NN = ( ZZ>= ` 1 )
24 1zzd 
 |-  ( ph -> 1 e. ZZ )
25 23 15 24 14 11 algrf 
 |-  ( ph -> K : NN --> T )
26 25 ffvelrnda 
 |-  ( ( ph /\ N e. NN ) -> ( K ` N ) e. T )
27 ineq1 
 |-  ( u = ( K ` N ) -> ( u i^i ( A [,] B ) ) = ( ( K ` N ) i^i ( A [,] B ) ) )
28 27 neeq1d 
 |-  ( u = ( K ` N ) -> ( ( u i^i ( A [,] B ) ) =/= (/) <-> ( ( K ` N ) i^i ( A [,] B ) ) =/= (/) ) )
29 28 10 elrab2 
 |-  ( ( K ` N ) e. T <-> ( ( K ` N ) e. U /\ ( ( K ` N ) i^i ( A [,] B ) ) =/= (/) ) )
30 26 29 sylib 
 |-  ( ( ph /\ N e. NN ) -> ( ( K ` N ) e. U /\ ( ( K ` N ) i^i ( A [,] B ) ) =/= (/) ) )
31 30 simpld 
 |-  ( ( ph /\ N e. NN ) -> ( K ` N ) e. U )
32 22 31 ffvelrnd 
 |-  ( ( ph /\ N e. NN ) -> ( G ` ( K ` N ) ) e. NN )
33 21 32 ffvelrnd 
 |-  ( ( ph /\ N e. NN ) -> ( F ` ( G ` ( K ` N ) ) ) e. ( RR X. RR ) )
34 xp2nd 
 |-  ( ( F ` ( G ` ( K ` N ) ) ) e. ( RR X. RR ) -> ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) e. RR )
35 33 34 syl 
 |-  ( ( ph /\ N e. NN ) -> ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) e. RR )
36 17 35 ltnled 
 |-  ( ( ph /\ N e. NN ) -> ( B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) <-> -. ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) <_ B ) )
37 simprl 
 |-  ( ( ph /\ ( N e. NN /\ B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) -> N e. NN )
38 2 adantr 
 |-  ( ( ph /\ ( N e. NN /\ B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) -> B e. RR )
39 30 adantrr 
 |-  ( ( ph /\ ( N e. NN /\ B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) -> ( ( K ` N ) e. U /\ ( ( K ` N ) i^i ( A [,] B ) ) =/= (/) ) )
40 39 simprd 
 |-  ( ( ph /\ ( N e. NN /\ B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) -> ( ( K ` N ) i^i ( A [,] B ) ) =/= (/) )
41 n0 
 |-  ( ( ( K ` N ) i^i ( A [,] B ) ) =/= (/) <-> E. x x e. ( ( K ` N ) i^i ( A [,] B ) ) )
42 40 41 sylib 
 |-  ( ( ph /\ ( N e. NN /\ B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) -> E. x x e. ( ( K ` N ) i^i ( A [,] B ) ) )
43 xp1st 
 |-  ( ( F ` ( G ` ( K ` N ) ) ) e. ( RR X. RR ) -> ( 1st ` ( F ` ( G ` ( K ` N ) ) ) ) e. RR )
44 33 43 syl 
 |-  ( ( ph /\ N e. NN ) -> ( 1st ` ( F ` ( G ` ( K ` N ) ) ) ) e. RR )
45 44 adantrr 
 |-  ( ( ph /\ ( N e. NN /\ B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) -> ( 1st ` ( F ` ( G ` ( K ` N ) ) ) ) e. RR )
46 45 adantr 
 |-  ( ( ( ph /\ ( N e. NN /\ B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) /\ x e. ( ( K ` N ) i^i ( A [,] B ) ) ) -> ( 1st ` ( F ` ( G ` ( K ` N ) ) ) ) e. RR )
47 simpr 
 |-  ( ( ( ph /\ ( N e. NN /\ B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) /\ x e. ( ( K ` N ) i^i ( A [,] B ) ) ) -> x e. ( ( K ` N ) i^i ( A [,] B ) ) )
48 elin 
 |-  ( x e. ( ( K ` N ) i^i ( A [,] B ) ) <-> ( x e. ( K ` N ) /\ x e. ( A [,] B ) ) )
49 47 48 sylib 
 |-  ( ( ( ph /\ ( N e. NN /\ B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) /\ x e. ( ( K ` N ) i^i ( A [,] B ) ) ) -> ( x e. ( K ` N ) /\ x e. ( A [,] B ) ) )
50 49 simprd 
 |-  ( ( ( ph /\ ( N e. NN /\ B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) /\ x e. ( ( K ` N ) i^i ( A [,] B ) ) ) -> x e. ( A [,] B ) )
51 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( x e. ( A [,] B ) <-> ( x e. RR /\ A <_ x /\ x <_ B ) ) )
52 1 2 51 syl2anc 
 |-  ( ph -> ( x e. ( A [,] B ) <-> ( x e. RR /\ A <_ x /\ x <_ B ) ) )
53 52 ad2antrr 
 |-  ( ( ( ph /\ ( N e. NN /\ B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) /\ x e. ( ( K ` N ) i^i ( A [,] B ) ) ) -> ( x e. ( A [,] B ) <-> ( x e. RR /\ A <_ x /\ x <_ B ) ) )
54 50 53 mpbid 
 |-  ( ( ( ph /\ ( N e. NN /\ B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) /\ x e. ( ( K ` N ) i^i ( A [,] B ) ) ) -> ( x e. RR /\ A <_ x /\ x <_ B ) )
55 54 simp1d 
 |-  ( ( ( ph /\ ( N e. NN /\ B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) /\ x e. ( ( K ` N ) i^i ( A [,] B ) ) ) -> x e. RR )
56 2 ad2antrr 
 |-  ( ( ( ph /\ ( N e. NN /\ B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) /\ x e. ( ( K ` N ) i^i ( A [,] B ) ) ) -> B e. RR )
57 49 simpld 
 |-  ( ( ( ph /\ ( N e. NN /\ B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) /\ x e. ( ( K ` N ) i^i ( A [,] B ) ) ) -> x e. ( K ` N ) )
58 39 simpld 
 |-  ( ( ph /\ ( N e. NN /\ B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) -> ( K ` N ) e. U )
59 1 2 3 4 5 6 7 8 9 ovolicc2lem1 
 |-  ( ( ph /\ ( K ` N ) e. U ) -> ( x e. ( K ` N ) <-> ( x e. RR /\ ( 1st ` ( F ` ( G ` ( K ` N ) ) ) ) < x /\ x < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) )
60 58 59 syldan 
 |-  ( ( ph /\ ( N e. NN /\ B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) -> ( x e. ( K ` N ) <-> ( x e. RR /\ ( 1st ` ( F ` ( G ` ( K ` N ) ) ) ) < x /\ x < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) )
61 60 adantr 
 |-  ( ( ( ph /\ ( N e. NN /\ B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) /\ x e. ( ( K ` N ) i^i ( A [,] B ) ) ) -> ( x e. ( K ` N ) <-> ( x e. RR /\ ( 1st ` ( F ` ( G ` ( K ` N ) ) ) ) < x /\ x < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) )
62 57 61 mpbid 
 |-  ( ( ( ph /\ ( N e. NN /\ B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) /\ x e. ( ( K ` N ) i^i ( A [,] B ) ) ) -> ( x e. RR /\ ( 1st ` ( F ` ( G ` ( K ` N ) ) ) ) < x /\ x < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) )
63 62 simp2d 
 |-  ( ( ( ph /\ ( N e. NN /\ B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) /\ x e. ( ( K ` N ) i^i ( A [,] B ) ) ) -> ( 1st ` ( F ` ( G ` ( K ` N ) ) ) ) < x )
64 54 simp3d 
 |-  ( ( ( ph /\ ( N e. NN /\ B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) /\ x e. ( ( K ` N ) i^i ( A [,] B ) ) ) -> x <_ B )
65 46 55 56 63 64 ltletrd 
 |-  ( ( ( ph /\ ( N e. NN /\ B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) /\ x e. ( ( K ` N ) i^i ( A [,] B ) ) ) -> ( 1st ` ( F ` ( G ` ( K ` N ) ) ) ) < B )
66 42 65 exlimddv 
 |-  ( ( ph /\ ( N e. NN /\ B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) -> ( 1st ` ( F ` ( G ` ( K ` N ) ) ) ) < B )
67 simprr 
 |-  ( ( ph /\ ( N e. NN /\ B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) -> B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) )
68 1 2 3 4 5 6 7 8 9 ovolicc2lem1 
 |-  ( ( ph /\ ( K ` N ) e. U ) -> ( B e. ( K ` N ) <-> ( B e. RR /\ ( 1st ` ( F ` ( G ` ( K ` N ) ) ) ) < B /\ B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) )
69 58 68 syldan 
 |-  ( ( ph /\ ( N e. NN /\ B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) -> ( B e. ( K ` N ) <-> ( B e. RR /\ ( 1st ` ( F ` ( G ` ( K ` N ) ) ) ) < B /\ B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) )
70 38 66 67 69 mpbir3and 
 |-  ( ( ph /\ ( N e. NN /\ B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) -> B e. ( K ` N ) )
71 fveq2 
 |-  ( n = N -> ( K ` n ) = ( K ` N ) )
72 71 eleq2d 
 |-  ( n = N -> ( B e. ( K ` n ) <-> B e. ( K ` N ) ) )
73 72 16 elrab2 
 |-  ( N e. W <-> ( N e. NN /\ B e. ( K ` N ) ) )
74 37 70 73 sylanbrc 
 |-  ( ( ph /\ ( N e. NN /\ B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) ) ) -> N e. W )
75 74 expr 
 |-  ( ( ph /\ N e. NN ) -> ( B < ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) -> N e. W ) )
76 36 75 sylbird 
 |-  ( ( ph /\ N e. NN ) -> ( -. ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) <_ B -> N e. W ) )
77 76 con1d 
 |-  ( ( ph /\ N e. NN ) -> ( -. N e. W -> ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) <_ B ) )
78 77 impr 
 |-  ( ( ph /\ ( N e. NN /\ -. N e. W ) ) -> ( 2nd ` ( F ` ( G ` ( K ` N ) ) ) ) <_ B )