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