| Step | Hyp | Ref | Expression | 
						
							| 1 |  | imo72b2lem0.1 |  |-  ( ph -> F : RR --> RR ) | 
						
							| 2 |  | imo72b2lem0.2 |  |-  ( ph -> G : RR --> RR ) | 
						
							| 3 |  | imo72b2lem0.3 |  |-  ( ph -> A e. RR ) | 
						
							| 4 |  | imo72b2lem0.4 |  |-  ( ph -> B e. RR ) | 
						
							| 5 |  | imo72b2lem0.5 |  |-  ( ph -> ( ( F ` ( A + B ) ) + ( F ` ( A - B ) ) ) = ( 2 x. ( ( F ` A ) x. ( G ` B ) ) ) ) | 
						
							| 6 |  | imo72b2lem0.6 |  |-  ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ 1 ) | 
						
							| 7 | 1 3 | ffvelcdmd |  |-  ( ph -> ( F ` A ) e. RR ) | 
						
							| 8 | 7 | recnd |  |-  ( ph -> ( F ` A ) e. CC ) | 
						
							| 9 | 2 4 | ffvelcdmd |  |-  ( ph -> ( G ` B ) e. RR ) | 
						
							| 10 | 9 | recnd |  |-  ( ph -> ( G ` B ) e. CC ) | 
						
							| 11 | 8 10 | absmuld |  |-  ( ph -> ( abs ` ( ( F ` A ) x. ( G ` B ) ) ) = ( ( abs ` ( F ` A ) ) x. ( abs ` ( G ` B ) ) ) ) | 
						
							| 12 | 8 10 | mulcld |  |-  ( ph -> ( ( F ` A ) x. ( G ` B ) ) e. CC ) | 
						
							| 13 | 12 | abscld |  |-  ( ph -> ( abs ` ( ( F ` A ) x. ( G ` B ) ) ) e. RR ) | 
						
							| 14 |  | absf |  |-  abs : CC --> RR | 
						
							| 15 | 14 | a1i |  |-  ( ph -> abs : CC --> RR ) | 
						
							| 16 | 15 | fimassd |  |-  ( ph -> ( abs " ( F " RR ) ) C_ RR ) | 
						
							| 17 |  | imaco |  |-  ( ( abs o. F ) " RR ) = ( abs " ( F " RR ) ) | 
						
							| 18 | 3 | ne0d |  |-  ( ph -> RR =/= (/) ) | 
						
							| 19 |  | ax-resscn |  |-  RR C_ CC | 
						
							| 20 | 19 | a1i |  |-  ( ph -> RR C_ CC ) | 
						
							| 21 | 15 20 | fssresd |  |-  ( ph -> ( abs |` RR ) : RR --> RR ) | 
						
							| 22 | 1 21 | fco2d |  |-  ( ph -> ( abs o. F ) : RR --> RR ) | 
						
							| 23 | 18 22 | wnefimgd |  |-  ( ph -> ( ( abs o. F ) " RR ) =/= (/) ) | 
						
							| 24 | 17 23 | eqnetrrid |  |-  ( ph -> ( abs " ( F " RR ) ) =/= (/) ) | 
						
							| 25 |  | 1red |  |-  ( ph -> 1 e. RR ) | 
						
							| 26 |  | simpr |  |-  ( ( ph /\ c = 1 ) -> c = 1 ) | 
						
							| 27 | 26 | breq2d |  |-  ( ( ph /\ c = 1 ) -> ( x <_ c <-> x <_ 1 ) ) | 
						
							| 28 | 27 | ralbidv |  |-  ( ( ph /\ c = 1 ) -> ( A. x e. ( abs " ( F " RR ) ) x <_ c <-> A. x e. ( abs " ( F " RR ) ) x <_ 1 ) ) | 
						
							| 29 | 1 6 | extoimad |  |-  ( ph -> A. x e. ( abs " ( F " RR ) ) x <_ 1 ) | 
						
							| 30 | 25 28 29 | rspcedvd |  |-  ( ph -> E. c e. RR A. x e. ( abs " ( F " RR ) ) x <_ c ) | 
						
							| 31 | 16 24 30 | suprcld |  |-  ( ph -> sup ( ( abs " ( F " RR ) ) , RR , < ) e. RR ) | 
						
							| 32 |  | 2re |  |-  2 e. RR | 
						
							| 33 | 32 | a1i |  |-  ( ph -> 2 e. RR ) | 
						
							| 34 |  | 0le2 |  |-  0 <_ 2 | 
						
							| 35 | 34 | a1i |  |-  ( ph -> 0 <_ 2 ) | 
						
							| 36 | 7 9 | remulcld |  |-  ( ph -> ( ( F ` A ) x. ( G ` B ) ) e. RR ) | 
						
							| 37 | 35 33 36 | absmulrposd |  |-  ( ph -> ( abs ` ( 2 x. ( ( F ` A ) x. ( G ` B ) ) ) ) = ( 2 x. ( abs ` ( ( F ` A ) x. ( G ` B ) ) ) ) ) | 
						
							| 38 | 5 | fveq2d |  |-  ( ph -> ( abs ` ( ( F ` ( A + B ) ) + ( F ` ( A - B ) ) ) ) = ( abs ` ( 2 x. ( ( F ` A ) x. ( G ` B ) ) ) ) ) | 
						
							| 39 |  | 2cnd |  |-  ( ph -> 2 e. CC ) | 
						
							| 40 | 39 12 | mulcld |  |-  ( ph -> ( 2 x. ( ( F ` A ) x. ( G ` B ) ) ) e. CC ) | 
						
							| 41 | 40 | abscld |  |-  ( ph -> ( abs ` ( 2 x. ( ( F ` A ) x. ( G ` B ) ) ) ) e. RR ) | 
						
							| 42 | 38 41 | eqeltrd |  |-  ( ph -> ( abs ` ( ( F ` ( A + B ) ) + ( F ` ( A - B ) ) ) ) e. RR ) | 
						
							| 43 | 3 4 | readdcld |  |-  ( ph -> ( A + B ) e. RR ) | 
						
							| 44 | 1 43 | ffvelcdmd |  |-  ( ph -> ( F ` ( A + B ) ) e. RR ) | 
						
							| 45 | 44 | recnd |  |-  ( ph -> ( F ` ( A + B ) ) e. CC ) | 
						
							| 46 | 45 | abscld |  |-  ( ph -> ( abs ` ( F ` ( A + B ) ) ) e. RR ) | 
						
							| 47 | 3 4 | resubcld |  |-  ( ph -> ( A - B ) e. RR ) | 
						
							| 48 | 1 47 | ffvelcdmd |  |-  ( ph -> ( F ` ( A - B ) ) e. RR ) | 
						
							| 49 | 48 | recnd |  |-  ( ph -> ( F ` ( A - B ) ) e. CC ) | 
						
							| 50 | 49 | abscld |  |-  ( ph -> ( abs ` ( F ` ( A - B ) ) ) e. RR ) | 
						
							| 51 | 46 50 | readdcld |  |-  ( ph -> ( ( abs ` ( F ` ( A + B ) ) ) + ( abs ` ( F ` ( A - B ) ) ) ) e. RR ) | 
						
							| 52 | 33 31 | remulcld |  |-  ( ph -> ( 2 x. sup ( ( abs " ( F " RR ) ) , RR , < ) ) e. RR ) | 
						
							| 53 | 45 49 | abstrid |  |-  ( ph -> ( abs ` ( ( F ` ( A + B ) ) + ( F ` ( A - B ) ) ) ) <_ ( ( abs ` ( F ` ( A + B ) ) ) + ( abs ` ( F ` ( A - B ) ) ) ) ) | 
						
							| 54 | 1 43 | fvco3d |  |-  ( ph -> ( ( abs o. F ) ` ( A + B ) ) = ( abs ` ( F ` ( A + B ) ) ) ) | 
						
							| 55 | 43 22 | wfximgfd |  |-  ( ph -> ( ( abs o. F ) ` ( A + B ) ) e. ( ( abs o. F ) " RR ) ) | 
						
							| 56 | 55 17 | eleqtrdi |  |-  ( ph -> ( ( abs o. F ) ` ( A + B ) ) e. ( abs " ( F " RR ) ) ) | 
						
							| 57 | 54 56 | eqeltrrd |  |-  ( ph -> ( abs ` ( F ` ( A + B ) ) ) e. ( abs " ( F " RR ) ) ) | 
						
							| 58 | 16 24 30 57 | suprubd |  |-  ( ph -> ( abs ` ( F ` ( A + B ) ) ) <_ sup ( ( abs " ( F " RR ) ) , RR , < ) ) | 
						
							| 59 | 1 47 | fvco3d |  |-  ( ph -> ( ( abs o. F ) ` ( A - B ) ) = ( abs ` ( F ` ( A - B ) ) ) ) | 
						
							| 60 | 47 22 | wfximgfd |  |-  ( ph -> ( ( abs o. F ) ` ( A - B ) ) e. ( ( abs o. F ) " RR ) ) | 
						
							| 61 | 60 17 | eleqtrdi |  |-  ( ph -> ( ( abs o. F ) ` ( A - B ) ) e. ( abs " ( F " RR ) ) ) | 
						
							| 62 | 59 61 | eqeltrrd |  |-  ( ph -> ( abs ` ( F ` ( A - B ) ) ) e. ( abs " ( F " RR ) ) ) | 
						
							| 63 | 16 24 30 62 | suprubd |  |-  ( ph -> ( abs ` ( F ` ( A - B ) ) ) <_ sup ( ( abs " ( F " RR ) ) , RR , < ) ) | 
						
							| 64 | 46 50 31 31 58 63 | le2addd |  |-  ( ph -> ( ( abs ` ( F ` ( A + B ) ) ) + ( abs ` ( F ` ( A - B ) ) ) ) <_ ( sup ( ( abs " ( F " RR ) ) , RR , < ) + sup ( ( abs " ( F " RR ) ) , RR , < ) ) ) | 
						
							| 65 | 31 | recnd |  |-  ( ph -> sup ( ( abs " ( F " RR ) ) , RR , < ) e. CC ) | 
						
							| 66 | 65 | 2timesd |  |-  ( ph -> ( 2 x. sup ( ( abs " ( F " RR ) ) , RR , < ) ) = ( sup ( ( abs " ( F " RR ) ) , RR , < ) + sup ( ( abs " ( F " RR ) ) , RR , < ) ) ) | 
						
							| 67 | 64 66 | breqtrrd |  |-  ( ph -> ( ( abs ` ( F ` ( A + B ) ) ) + ( abs ` ( F ` ( A - B ) ) ) ) <_ ( 2 x. sup ( ( abs " ( F " RR ) ) , RR , < ) ) ) | 
						
							| 68 | 42 51 52 53 67 | letrd |  |-  ( ph -> ( abs ` ( ( F ` ( A + B ) ) + ( F ` ( A - B ) ) ) ) <_ ( 2 x. sup ( ( abs " ( F " RR ) ) , RR , < ) ) ) | 
						
							| 69 | 38 68 | eqbrtrrd |  |-  ( ph -> ( abs ` ( 2 x. ( ( F ` A ) x. ( G ` B ) ) ) ) <_ ( 2 x. sup ( ( abs " ( F " RR ) ) , RR , < ) ) ) | 
						
							| 70 | 37 69 | eqbrtrrd |  |-  ( ph -> ( 2 x. ( abs ` ( ( F ` A ) x. ( G ` B ) ) ) ) <_ ( 2 x. sup ( ( abs " ( F " RR ) ) , RR , < ) ) ) | 
						
							| 71 |  | 2pos |  |-  0 < 2 | 
						
							| 72 | 71 | a1i |  |-  ( ph -> 0 < 2 ) | 
						
							| 73 | 13 31 33 70 72 | wwlemuld |  |-  ( ph -> ( abs ` ( ( F ` A ) x. ( G ` B ) ) ) <_ sup ( ( abs " ( F " RR ) ) , RR , < ) ) | 
						
							| 74 | 11 73 | eqbrtrrd |  |-  ( ph -> ( ( abs ` ( F ` A ) ) x. ( abs ` ( G ` B ) ) ) <_ sup ( ( abs " ( F " RR ) ) , RR , < ) ) |