Metamath Proof Explorer

Theorem imo72b2lem1

Description: Lemma for imo72b2 . (Contributed by Stanislas Polu, 9-Mar-2020)

Ref Expression
Hypotheses imo72b2lem1.1 
|- ( ph -> F : RR --> RR )
imo72b2lem1.7 
|- ( ph -> E. x e. RR ( F ` x ) =/= 0 )
imo72b2lem1.6 
|- ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ 1 )
Assertion imo72b2lem1 
|- ( ph -> 0 < sup ( ( abs " ( F " RR ) ) , RR , < ) )

Proof

Step Hyp Ref Expression
1 imo72b2lem1.1 
 |-  ( ph -> F : RR --> RR )
2 imo72b2lem1.7 
 |-  ( ph -> E. x e. RR ( F ` x ) =/= 0 )
3 imo72b2lem1.6 
 |-  ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ 1 )
4 imaco 
 |-  ( ( abs o. F ) " RR ) = ( abs " ( F " RR ) )
5 imassrn 
 |-  ( ( abs o. F ) " RR ) C_ ran ( abs o. F )
6 absf 
 |-  abs : CC --> RR
7 6 a1i 
 |-  ( ph -> abs : CC --> RR )
8 ax-resscn 
 |-  RR C_ CC
9 8 a1i 
 |-  ( ph -> RR C_ CC )
10 7 9 fssresd 
 |-  ( ph -> ( abs |` RR ) : RR --> RR )
11 1 10 fco2d 
 |-  ( ph -> ( abs o. F ) : RR --> RR )
12 11 frnd 
 |-  ( ph -> ran ( abs o. F ) C_ RR )
13 5 12 sstrid 
 |-  ( ph -> ( ( abs o. F ) " RR ) C_ RR )
14 4 13 eqsstrrid 
 |-  ( ph -> ( abs " ( F " RR ) ) C_ RR )
15 0re 
 |-  0 e. RR
16 15 ne0ii 
 |-  RR =/= (/)
17 16 a1i 
 |-  ( ph -> RR =/= (/) )
18 17 11 wnefimgd 
 |-  ( ph -> ( ( abs o. F ) " RR ) =/= (/) )
19 4 18 eqnetrrid 
 |-  ( ph -> ( abs " ( F " RR ) ) =/= (/) )
20 1red 
 |-  ( ph -> 1 e. RR )
21 simpr 
 |-  ( ( ph /\ c = 1 ) -> c = 1 )
22 21 breq2d 
 |-  ( ( ph /\ c = 1 ) -> ( t <_ c <-> t <_ 1 ) )
23 22 ralbidv 
 |-  ( ( ph /\ c = 1 ) -> ( A. t e. ( abs " ( F " RR ) ) t <_ c <-> A. t e. ( abs " ( F " RR ) ) t <_ 1 ) )
24 1 3 extoimad 
 |-  ( ph -> A. t e. ( abs " ( F " RR ) ) t <_ 1 )
25 20 23 24 rspcedvd 
 |-  ( ph -> E. c e. RR A. t e. ( abs " ( F " RR ) ) t <_ c )
26 0red 
 |-  ( ph -> 0 e. RR )
27 1 adantr 
 |-  ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> F : RR --> RR )
28 simprl 
 |-  ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> x e. RR )
29 27 28 fvco3d 
 |-  ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> ( ( abs o. F ) ` x ) = ( abs ` ( F ` x ) ) )
30 11 funfvima2d 
 |-  ( ( ph /\ x e. RR ) -> ( ( abs o. F ) ` x ) e. ( ( abs o. F ) " RR ) )
31 30 adantrr 
 |-  ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> ( ( abs o. F ) ` x ) e. ( ( abs o. F ) " RR ) )
32 31 4 eleqtrdi 
 |-  ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> ( ( abs o. F ) ` x ) e. ( abs " ( F " RR ) ) )
33 29 32 eqeltrrd 
 |-  ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> ( abs ` ( F ` x ) ) e. ( abs " ( F " RR ) ) )
34 simpr 
 |-  ( ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) /\ z = ( abs ` ( F ` x ) ) ) -> z = ( abs ` ( F ` x ) ) )
35 34 breq2d 
 |-  ( ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) /\ z = ( abs ` ( F ` x ) ) ) -> ( 0 < z <-> 0 < ( abs ` ( F ` x ) ) ) )
36 1 ffvelrnda 
 |-  ( ( ph /\ x e. RR ) -> ( F ` x ) e. RR )
37 36 adantrr 
 |-  ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> ( F ` x ) e. RR )
38 37 recnd 
 |-  ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> ( F ` x ) e. CC )
39 simprr 
 |-  ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> ( F ` x ) =/= 0 )
40 38 39 absrpcld 
 |-  ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> ( abs ` ( F ` x ) ) e. RR+ )
41 40 rpgt0d 
 |-  ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> 0 < ( abs ` ( F ` x ) ) )
42 33 35 41 rspcedvd 
 |-  ( ( ph /\ ( x e. RR /\ ( F ` x ) =/= 0 ) ) -> E. z e. ( abs " ( F " RR ) ) 0 < z )
43 2 42 rexlimddv 
 |-  ( ph -> E. z e. ( abs " ( F " RR ) ) 0 < z )
44 14 19 25 26 43 suprlubrd 
 |-  ( ph -> 0 < sup ( ( abs " ( F " RR ) ) , RR , < ) )