Metamath Proof Explorer

Theorem irrapxlem4

Description: Lemma for irrapx1 . Eliminate ranges, use positivity of the input to force positivity of the output by increasing B as needed. (Contributed by Stefan O'Rear, 13-Sep-2014)

Ref Expression
Assertion irrapxlem4 
|- ( ( A e. RR+ /\ B e. NN ) -> E. x e. NN E. y e. NN ( abs ` ( ( A x. x ) - y ) ) < ( 1 / if ( x <_ B , B , x ) ) )

Proof

Step Hyp Ref Expression
1 elfznn 
 |-  ( a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) -> a e. NN )
2 1 ad3antlr 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> a e. NN )
3 nn0z 
 |-  ( b e. NN0 -> b e. ZZ )
4 3 ad2antlr 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> b e. ZZ )
5 simpl 
 |-  ( ( A e. RR+ /\ B e. NN ) -> A e. RR+ )
6 5 ad3antrrr 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> A e. RR+ )
7 6 rpred 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> A e. RR )
8 2 nnred 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> a e. RR )
9 7 8 remulcld 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( A x. a ) e. RR )
10 nn0re 
 |-  ( b e. NN0 -> b e. RR )
11 10 ad2antlr 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> b e. RR )
12 9 11 resubcld 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( ( A x. a ) - b ) e. RR )
13 12 recnd 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( ( A x. a ) - b ) e. CC )
14 13 abscld 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( abs ` ( ( A x. a ) - b ) ) e. RR )
15 5 rpreccld 
 |-  ( ( A e. RR+ /\ B e. NN ) -> ( 1 / A ) e. RR+ )
16 15 rprege0d 
 |-  ( ( A e. RR+ /\ B e. NN ) -> ( ( 1 / A ) e. RR /\ 0 <_ ( 1 / A ) ) )
17 flge0nn0 
 |-  ( ( ( 1 / A ) e. RR /\ 0 <_ ( 1 / A ) ) -> ( |_ ` ( 1 / A ) ) e. NN0 )
18 nn0p1nn 
 |-  ( ( |_ ` ( 1 / A ) ) e. NN0 -> ( ( |_ ` ( 1 / A ) ) + 1 ) e. NN )
19 16 17 18 3syl 
 |-  ( ( A e. RR+ /\ B e. NN ) -> ( ( |_ ` ( 1 / A ) ) + 1 ) e. NN )
20 19 ad3antrrr 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( ( |_ ` ( 1 / A ) ) + 1 ) e. NN )
21 simpr 
 |-  ( ( A e. RR+ /\ B e. NN ) -> B e. NN )
22 21 ad3antrrr 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> B e. NN )
23 20 22 ifcld 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) e. NN )
24 23 nnrecred 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) e. RR )
25 0red 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> 0 e. RR )
26 9 25 resubcld 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( ( A x. a ) - 0 ) e. RR )
27 simpr 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) )
28 20 nnrecred 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( 1 / ( ( |_ ` ( 1 / A ) ) + 1 ) ) e. RR )
29 22 nnred 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> B e. RR )
30 6 rprecred 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( 1 / A ) e. RR )
31 30 flcld 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( |_ ` ( 1 / A ) ) e. ZZ )
32 31 zred 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( |_ ` ( 1 / A ) ) e. RR )
33 peano2re 
 |-  ( ( |_ ` ( 1 / A ) ) e. RR -> ( ( |_ ` ( 1 / A ) ) + 1 ) e. RR )
34 32 33 syl 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( ( |_ ` ( 1 / A ) ) + 1 ) e. RR )
35 max2 
 |-  ( ( B e. RR /\ ( ( |_ ` ( 1 / A ) ) + 1 ) e. RR ) -> ( ( |_ ` ( 1 / A ) ) + 1 ) <_ if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) )
36 29 34 35 syl2anc 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( ( |_ ` ( 1 / A ) ) + 1 ) <_ if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) )
37 20 nngt0d 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> 0 < ( ( |_ ` ( 1 / A ) ) + 1 ) )
38 23 nnred 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) e. RR )
39 23 nngt0d 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> 0 < if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) )
40 lerec 
 |-  ( ( ( ( ( |_ ` ( 1 / A ) ) + 1 ) e. RR /\ 0 < ( ( |_ ` ( 1 / A ) ) + 1 ) ) /\ ( if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) e. RR /\ 0 < if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( ( ( |_ ` ( 1 / A ) ) + 1 ) <_ if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) <-> ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) <_ ( 1 / ( ( |_ ` ( 1 / A ) ) + 1 ) ) ) )
41 34 37 38 39 40 syl22anc 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( ( ( |_ ` ( 1 / A ) ) + 1 ) <_ if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) <-> ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) <_ ( 1 / ( ( |_ ` ( 1 / A ) ) + 1 ) ) ) )
42 36 41 mpbid 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) <_ ( 1 / ( ( |_ ` ( 1 / A ) ) + 1 ) ) )
43 fllep1 
 |-  ( ( 1 / A ) e. RR -> ( 1 / A ) <_ ( ( |_ ` ( 1 / A ) ) + 1 ) )
44 30 43 syl 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( 1 / A ) <_ ( ( |_ ` ( 1 / A ) ) + 1 ) )
45 20 nncnd 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( ( |_ ` ( 1 / A ) ) + 1 ) e. CC )
46 20 nnne0d 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( ( |_ ` ( 1 / A ) ) + 1 ) =/= 0 )
47 45 46 recrecd 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( 1 / ( 1 / ( ( |_ ` ( 1 / A ) ) + 1 ) ) ) = ( ( |_ ` ( 1 / A ) ) + 1 ) )
48 44 47 breqtrrd 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( 1 / A ) <_ ( 1 / ( 1 / ( ( |_ ` ( 1 / A ) ) + 1 ) ) ) )
49 34 37 recgt0d 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> 0 < ( 1 / ( ( |_ ` ( 1 / A ) ) + 1 ) ) )
50 6 rpgt0d 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> 0 < A )
51 lerec 
 |-  ( ( ( ( 1 / ( ( |_ ` ( 1 / A ) ) + 1 ) ) e. RR /\ 0 < ( 1 / ( ( |_ ` ( 1 / A ) ) + 1 ) ) ) /\ ( A e. RR /\ 0 < A ) ) -> ( ( 1 / ( ( |_ ` ( 1 / A ) ) + 1 ) ) <_ A <-> ( 1 / A ) <_ ( 1 / ( 1 / ( ( |_ ` ( 1 / A ) ) + 1 ) ) ) ) )
52 28 49 7 50 51 syl22anc 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( ( 1 / ( ( |_ ` ( 1 / A ) ) + 1 ) ) <_ A <-> ( 1 / A ) <_ ( 1 / ( 1 / ( ( |_ ` ( 1 / A ) ) + 1 ) ) ) ) )
53 48 52 mpbird 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( 1 / ( ( |_ ` ( 1 / A ) ) + 1 ) ) <_ A )
54 24 28 7 42 53 letrd 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) <_ A )
55 7 recnd 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> A e. CC )
56 55 mulid1d 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( A x. 1 ) = A )
57 2 nnge1d 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> 1 <_ a )
58 1red 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> 1 e. RR )
59 58 8 6 lemul2d 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( 1 <_ a <-> ( A x. 1 ) <_ ( A x. a ) ) )
60 57 59 mpbid 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( A x. 1 ) <_ ( A x. a ) )
61 56 60 eqbrtrrd 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> A <_ ( A x. a ) )
62 9 recnd 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( A x. a ) e. CC )
63 62 subid1d 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( ( A x. a ) - 0 ) = ( A x. a ) )
64 61 63 breqtrrd 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> A <_ ( ( A x. a ) - 0 ) )
65 24 7 26 54 64 letrd 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) <_ ( ( A x. a ) - 0 ) )
66 14 24 26 27 65 ltletrd 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( abs ` ( ( A x. a ) - b ) ) < ( ( A x. a ) - 0 ) )
67 12 26 absltd 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( ( abs ` ( ( A x. a ) - b ) ) < ( ( A x. a ) - 0 ) <-> ( -u ( ( A x. a ) - 0 ) < ( ( A x. a ) - b ) /\ ( ( A x. a ) - b ) < ( ( A x. a ) - 0 ) ) ) )
68 66 67 mpbid 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( -u ( ( A x. a ) - 0 ) < ( ( A x. a ) - b ) /\ ( ( A x. a ) - b ) < ( ( A x. a ) - 0 ) ) )
69 68 simprd 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( ( A x. a ) - b ) < ( ( A x. a ) - 0 ) )
70 25 11 9 ltsub2d 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( 0 < b <-> ( ( A x. a ) - b ) < ( ( A x. a ) - 0 ) ) )
71 69 70 mpbird 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> 0 < b )
72 elnnz 
 |-  ( b e. NN <-> ( b e. ZZ /\ 0 < b ) )
73 4 71 72 sylanbrc 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> b e. NN )
74 22 2 ifcld 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> if ( a <_ B , B , a ) e. NN )
75 74 nnrecred 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( 1 / if ( a <_ B , B , a ) ) e. RR )
76 elfzle2 
 |-  ( a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) -> a <_ if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) )
77 76 ad3antlr 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> a <_ if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) )
78 max1 
 |-  ( ( B e. RR /\ ( ( |_ ` ( 1 / A ) ) + 1 ) e. RR ) -> B <_ if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) )
79 29 34 78 syl2anc 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> B <_ if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) )
80 maxle 
 |-  ( ( a e. RR /\ B e. RR /\ if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) e. RR ) -> ( if ( a <_ B , B , a ) <_ if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) <-> ( a <_ if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) /\ B <_ if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) )
81 8 29 38 80 syl3anc 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( if ( a <_ B , B , a ) <_ if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) <-> ( a <_ if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) /\ B <_ if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) )
82 77 79 81 mpbir2and 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> if ( a <_ B , B , a ) <_ if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) )
83 29 8 ifcld 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> if ( a <_ B , B , a ) e. RR )
84 22 nngt0d 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> 0 < B )
85 max2 
 |-  ( ( a e. RR /\ B e. RR ) -> B <_ if ( a <_ B , B , a ) )
86 8 29 85 syl2anc 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> B <_ if ( a <_ B , B , a ) )
87 25 29 83 84 86 ltletrd 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> 0 < if ( a <_ B , B , a ) )
88 lerec 
 |-  ( ( ( if ( a <_ B , B , a ) e. RR /\ 0 < if ( a <_ B , B , a ) ) /\ ( if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) e. RR /\ 0 < if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( if ( a <_ B , B , a ) <_ if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) <-> ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) <_ ( 1 / if ( a <_ B , B , a ) ) ) )
89 83 87 38 39 88 syl22anc 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( if ( a <_ B , B , a ) <_ if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) <-> ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) <_ ( 1 / if ( a <_ B , B , a ) ) ) )
90 82 89 mpbid 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) <_ ( 1 / if ( a <_ B , B , a ) ) )
91 14 24 75 27 90 ltletrd 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ B , B , a ) ) )
92 oveq2 
 |-  ( x = a -> ( A x. x ) = ( A x. a ) )
93 92 fvoveq1d 
 |-  ( x = a -> ( abs ` ( ( A x. x ) - y ) ) = ( abs ` ( ( A x. a ) - y ) ) )
94 breq1 
 |-  ( x = a -> ( x <_ B <-> a <_ B ) )
95 id 
 |-  ( x = a -> x = a )
96 94 95 ifbieq2d 
 |-  ( x = a -> if ( x <_ B , B , x ) = if ( a <_ B , B , a ) )
97 96 oveq2d 
 |-  ( x = a -> ( 1 / if ( x <_ B , B , x ) ) = ( 1 / if ( a <_ B , B , a ) ) )
98 93 97 breq12d 
 |-  ( x = a -> ( ( abs ` ( ( A x. x ) - y ) ) < ( 1 / if ( x <_ B , B , x ) ) <-> ( abs ` ( ( A x. a ) - y ) ) < ( 1 / if ( a <_ B , B , a ) ) ) )
99 oveq2 
 |-  ( y = b -> ( ( A x. a ) - y ) = ( ( A x. a ) - b ) )
100 99 fveq2d 
 |-  ( y = b -> ( abs ` ( ( A x. a ) - y ) ) = ( abs ` ( ( A x. a ) - b ) ) )
101 100 breq1d 
 |-  ( y = b -> ( ( abs ` ( ( A x. a ) - y ) ) < ( 1 / if ( a <_ B , B , a ) ) <-> ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ B , B , a ) ) ) )
102 98 101 rspc2ev 
 |-  ( ( a e. NN /\ b e. NN /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( a <_ B , B , a ) ) ) -> E. x e. NN E. y e. NN ( abs ` ( ( A x. x ) - y ) ) < ( 1 / if ( x <_ B , B , x ) ) )
103 2 73 91 102 syl3anc 
 |-  ( ( ( ( ( A e. RR+ /\ B e. NN ) /\ a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) /\ b e. NN0 ) /\ ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) ) -> E. x e. NN E. y e. NN ( abs ` ( ( A x. x ) - y ) ) < ( 1 / if ( x <_ B , B , x ) ) )
104 19 21 ifcld 
 |-  ( ( A e. RR+ /\ B e. NN ) -> if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) e. NN )
105 irrapxlem3 
 |-  ( ( A e. RR+ /\ if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) e. NN ) -> E. a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) E. b e. NN0 ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) )
106 5 104 105 syl2anc 
 |-  ( ( A e. RR+ /\ B e. NN ) -> E. a e. ( 1 ... if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) E. b e. NN0 ( abs ` ( ( A x. a ) - b ) ) < ( 1 / if ( B <_ ( ( |_ ` ( 1 / A ) ) + 1 ) , ( ( |_ ` ( 1 / A ) ) + 1 ) , B ) ) )
107 103 106 r19.29vva 
 |-  ( ( A e. RR+ /\ B e. NN ) -> E. x e. NN E. y e. NN ( abs ` ( ( A x. x ) - y ) ) < ( 1 / if ( x <_ B , B , x ) ) )