Metamath Proof Explorer


Theorem irrapxlem5

Description: Lemma for irrapx1 . Switching to real intervals and fraction syntax. (Contributed by Stefan O'Rear, 13-Sep-2014)

Ref Expression
Assertion irrapxlem5 ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โ†’ โˆƒ ๐‘ฅ โˆˆ โ„š ( 0 < ๐‘ฅ โˆง ( abs โ€˜ ( ๐‘ฅ โˆ’ ๐ด ) ) < ๐ต โˆง ( abs โ€˜ ( ๐‘ฅ โˆ’ ๐ด ) ) < ( ( denom โ€˜ ๐‘ฅ ) โ†‘ - 2 ) ) )

Proof

Step Hyp Ref Expression
1 simpr โŠข ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โ†’ ๐ต โˆˆ โ„+ )
2 1 rpreccld โŠข ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โ†’ ( 1 / ๐ต ) โˆˆ โ„+ )
3 2 rprege0d โŠข ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โ†’ ( ( 1 / ๐ต ) โˆˆ โ„ โˆง 0 โ‰ค ( 1 / ๐ต ) ) )
4 flge0nn0 โŠข ( ( ( 1 / ๐ต ) โˆˆ โ„ โˆง 0 โ‰ค ( 1 / ๐ต ) ) โ†’ ( โŒŠ โ€˜ ( 1 / ๐ต ) ) โˆˆ โ„•0 )
5 nn0p1nn โŠข ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) โˆˆ โ„•0 โ†’ ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) โˆˆ โ„• )
6 3 4 5 3syl โŠข ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โ†’ ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) โˆˆ โ„• )
7 irrapxlem4 โŠข ( ( ๐ด โˆˆ โ„+ โˆง ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) โˆˆ โ„• ) โ†’ โˆƒ ๐‘Ž โˆˆ โ„• โˆƒ ๐‘ โˆˆ โ„• ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) )
8 6 7 syldan โŠข ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โ†’ โˆƒ ๐‘Ž โˆˆ โ„• โˆƒ ๐‘ โˆˆ โ„• ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) )
9 simplrr โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ๐‘ โˆˆ โ„• )
10 nnq โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„š )
11 9 10 syl โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ๐‘ โˆˆ โ„š )
12 simplrl โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ๐‘Ž โˆˆ โ„• )
13 nnq โŠข ( ๐‘Ž โˆˆ โ„• โ†’ ๐‘Ž โˆˆ โ„š )
14 12 13 syl โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ๐‘Ž โˆˆ โ„š )
15 12 nnne0d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ๐‘Ž โ‰  0 )
16 qdivcl โŠข ( ( ๐‘ โˆˆ โ„š โˆง ๐‘Ž โˆˆ โ„š โˆง ๐‘Ž โ‰  0 ) โ†’ ( ๐‘ / ๐‘Ž ) โˆˆ โ„š )
17 11 14 15 16 syl3anc โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ๐‘ / ๐‘Ž ) โˆˆ โ„š )
18 9 nnrpd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ๐‘ โˆˆ โ„+ )
19 12 nnrpd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ๐‘Ž โˆˆ โ„+ )
20 18 19 rpdivcld โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ๐‘ / ๐‘Ž ) โˆˆ โ„+ )
21 20 rpgt0d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ 0 < ( ๐‘ / ๐‘Ž ) )
22 12 nnred โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ๐‘Ž โˆˆ โ„ )
23 12 nnnn0d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ๐‘Ž โˆˆ โ„•0 )
24 23 nn0ge0d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ 0 โ‰ค ๐‘Ž )
25 22 24 absidd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( abs โ€˜ ๐‘Ž ) = ๐‘Ž )
26 25 eqcomd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ๐‘Ž = ( abs โ€˜ ๐‘Ž ) )
27 26 oveq1d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ๐‘Ž ยท ( abs โ€˜ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) ) = ( ( abs โ€˜ ๐‘Ž ) ยท ( abs โ€˜ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) ) )
28 12 nncnd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ๐‘Ž โˆˆ โ„‚ )
29 qre โŠข ( ( ๐‘ / ๐‘Ž ) โˆˆ โ„š โ†’ ( ๐‘ / ๐‘Ž ) โˆˆ โ„ )
30 17 29 syl โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ๐‘ / ๐‘Ž ) โˆˆ โ„ )
31 rpre โŠข ( ๐ด โˆˆ โ„+ โ†’ ๐ด โˆˆ โ„ )
32 31 ad3antrrr โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ๐ด โˆˆ โ„ )
33 30 32 resubcld โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) โˆˆ โ„ )
34 33 recnd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) โˆˆ โ„‚ )
35 28 34 absmuld โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( abs โ€˜ ( ๐‘Ž ยท ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) ) = ( ( abs โ€˜ ๐‘Ž ) ยท ( abs โ€˜ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) ) )
36 27 35 eqtr4d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ๐‘Ž ยท ( abs โ€˜ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) ) = ( abs โ€˜ ( ๐‘Ž ยท ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) ) )
37 qcn โŠข ( ( ๐‘ / ๐‘Ž ) โˆˆ โ„š โ†’ ( ๐‘ / ๐‘Ž ) โˆˆ โ„‚ )
38 17 37 syl โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ๐‘ / ๐‘Ž ) โˆˆ โ„‚ )
39 rpcn โŠข ( ๐ด โˆˆ โ„+ โ†’ ๐ด โˆˆ โ„‚ )
40 39 ad3antrrr โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ๐ด โˆˆ โ„‚ )
41 28 38 40 subdid โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ๐‘Ž ยท ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) = ( ( ๐‘Ž ยท ( ๐‘ / ๐‘Ž ) ) โˆ’ ( ๐‘Ž ยท ๐ด ) ) )
42 9 nncnd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ๐‘ โˆˆ โ„‚ )
43 42 28 15 divcan2d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ๐‘Ž ยท ( ๐‘ / ๐‘Ž ) ) = ๐‘ )
44 28 40 mulcomd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ๐‘Ž ยท ๐ด ) = ( ๐ด ยท ๐‘Ž ) )
45 43 44 oveq12d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ( ๐‘Ž ยท ( ๐‘ / ๐‘Ž ) ) โˆ’ ( ๐‘Ž ยท ๐ด ) ) = ( ๐‘ โˆ’ ( ๐ด ยท ๐‘Ž ) ) )
46 41 45 eqtrd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ๐‘Ž ยท ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) = ( ๐‘ โˆ’ ( ๐ด ยท ๐‘Ž ) ) )
47 46 fveq2d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( abs โ€˜ ( ๐‘Ž ยท ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) ) = ( abs โ€˜ ( ๐‘ โˆ’ ( ๐ด ยท ๐‘Ž ) ) ) )
48 32 22 remulcld โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ๐ด ยท ๐‘Ž ) โˆˆ โ„ )
49 48 recnd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ๐ด ยท ๐‘Ž ) โˆˆ โ„‚ )
50 42 49 abssubd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( abs โ€˜ ( ๐‘ โˆ’ ( ๐ด ยท ๐‘Ž ) ) ) = ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) )
51 36 47 50 3eqtrd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ๐‘Ž ยท ( abs โ€˜ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) ) = ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) )
52 9 nnred โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ๐‘ โˆˆ โ„ )
53 48 52 resubcld โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) โˆˆ โ„ )
54 53 recnd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) โˆˆ โ„‚ )
55 54 abscld โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) โˆˆ โ„ )
56 simpllr โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ๐ต โˆˆ โ„+ )
57 56 rprecred โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( 1 / ๐ต ) โˆˆ โ„ )
58 56 rpreccld โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( 1 / ๐ต ) โˆˆ โ„+ )
59 58 rpge0d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ 0 โ‰ค ( 1 / ๐ต ) )
60 57 59 4 syl2anc โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( โŒŠ โ€˜ ( 1 / ๐ต ) ) โˆˆ โ„•0 )
61 60 5 syl โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) โˆˆ โ„• )
62 61 nnrpd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) โˆˆ โ„+ )
63 62 19 ifcld โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) โˆˆ โ„+ )
64 63 rprecred โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) โˆˆ โ„ )
65 56 rpred โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ๐ต โˆˆ โ„ )
66 22 65 remulcld โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ๐‘Ž ยท ๐ต ) โˆˆ โ„ )
67 simpr โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) )
68 58 rprecred โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( 1 / ( 1 / ๐ต ) ) โˆˆ โ„ )
69 61 nnred โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) โˆˆ โ„ )
70 69 22 ifcld โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) โˆˆ โ„ )
71 fllep1 โŠข ( ( 1 / ๐ต ) โˆˆ โ„ โ†’ ( 1 / ๐ต ) โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) )
72 57 71 syl โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( 1 / ๐ต ) โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) )
73 max2 โŠข ( ( ๐‘Ž โˆˆ โ„ โˆง ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) โˆˆ โ„ ) โ†’ ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) โ‰ค if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) )
74 22 69 73 syl2anc โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) โ‰ค if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) )
75 57 69 70 72 74 letrd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( 1 / ๐ต ) โ‰ค if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) )
76 58 63 lerecd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ( 1 / ๐ต ) โ‰ค if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) โ†” ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) โ‰ค ( 1 / ( 1 / ๐ต ) ) ) )
77 75 76 mpbid โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) โ‰ค ( 1 / ( 1 / ๐ต ) ) )
78 65 recnd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ๐ต โˆˆ โ„‚ )
79 56 rpne0d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ๐ต โ‰  0 )
80 78 79 recrecd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( 1 / ( 1 / ๐ต ) ) = ๐ต )
81 78 mulid2d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( 1 ยท ๐ต ) = ๐ต )
82 80 81 eqtr4d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( 1 / ( 1 / ๐ต ) ) = ( 1 ยท ๐ต ) )
83 12 nnge1d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ 1 โ‰ค ๐‘Ž )
84 1red โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ 1 โˆˆ โ„ )
85 84 22 56 lemul1d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( 1 โ‰ค ๐‘Ž โ†” ( 1 ยท ๐ต ) โ‰ค ( ๐‘Ž ยท ๐ต ) ) )
86 83 85 mpbid โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( 1 ยท ๐ต ) โ‰ค ( ๐‘Ž ยท ๐ต ) )
87 82 86 eqbrtrd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( 1 / ( 1 / ๐ต ) ) โ‰ค ( ๐‘Ž ยท ๐ต ) )
88 64 68 66 77 87 letrd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) โ‰ค ( ๐‘Ž ยท ๐ต ) )
89 55 64 66 67 88 ltletrd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( ๐‘Ž ยท ๐ต ) )
90 51 89 eqbrtrd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ๐‘Ž ยท ( abs โ€˜ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) ) < ( ๐‘Ž ยท ๐ต ) )
91 34 abscld โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( abs โ€˜ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) โˆˆ โ„ )
92 12 nngt0d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ 0 < ๐‘Ž )
93 ltmul2 โŠข ( ( ( abs โ€˜ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ( ๐‘Ž โˆˆ โ„ โˆง 0 < ๐‘Ž ) ) โ†’ ( ( abs โ€˜ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) < ๐ต โ†” ( ๐‘Ž ยท ( abs โ€˜ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) ) < ( ๐‘Ž ยท ๐ต ) ) )
94 91 65 22 92 93 syl112anc โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ( abs โ€˜ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) < ๐ต โ†” ( ๐‘Ž ยท ( abs โ€˜ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) ) < ( ๐‘Ž ยท ๐ต ) ) )
95 90 94 mpbird โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( abs โ€˜ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) < ๐ต )
96 22 22 remulcld โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ๐‘Ž ยท ๐‘Ž ) โˆˆ โ„ )
97 22 15 msqgt0d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ 0 < ( ๐‘Ž ยท ๐‘Ž ) )
98 97 gt0ne0d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ๐‘Ž ยท ๐‘Ž ) โ‰  0 )
99 96 98 rereccld โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( 1 / ( ๐‘Ž ยท ๐‘Ž ) ) โˆˆ โ„ )
100 qdencl โŠข ( ( ๐‘ / ๐‘Ž ) โˆˆ โ„š โ†’ ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) โˆˆ โ„• )
101 17 100 syl โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) โˆˆ โ„• )
102 101 nnred โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) โˆˆ โ„ )
103 102 102 remulcld โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ยท ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ) โˆˆ โ„ )
104 101 nnne0d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) โ‰  0 )
105 102 104 msqgt0d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ 0 < ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ยท ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ) )
106 105 gt0ne0d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ยท ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ) โ‰  0 )
107 103 106 rereccld โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( 1 / ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ยท ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ) ) โˆˆ โ„ )
108 22 15 rereccld โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( 1 / ๐‘Ž ) โˆˆ โ„ )
109 max1 โŠข ( ( ๐‘Ž โˆˆ โ„ โˆง ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) โˆˆ โ„ ) โ†’ ๐‘Ž โ‰ค if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) )
110 22 69 109 syl2anc โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ๐‘Ž โ‰ค if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) )
111 19 63 lerecd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ๐‘Ž โ‰ค if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) โ†” ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) โ‰ค ( 1 / ๐‘Ž ) ) )
112 110 111 mpbid โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) โ‰ค ( 1 / ๐‘Ž ) )
113 55 64 108 67 112 ltletrd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / ๐‘Ž ) )
114 28 28 28 15 15 divdiv1d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ( ๐‘Ž / ๐‘Ž ) / ๐‘Ž ) = ( ๐‘Ž / ( ๐‘Ž ยท ๐‘Ž ) ) )
115 28 15 dividd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ๐‘Ž / ๐‘Ž ) = 1 )
116 115 oveq1d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ( ๐‘Ž / ๐‘Ž ) / ๐‘Ž ) = ( 1 / ๐‘Ž ) )
117 96 recnd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ๐‘Ž ยท ๐‘Ž ) โˆˆ โ„‚ )
118 28 117 98 divrecd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ๐‘Ž / ( ๐‘Ž ยท ๐‘Ž ) ) = ( ๐‘Ž ยท ( 1 / ( ๐‘Ž ยท ๐‘Ž ) ) ) )
119 114 116 118 3eqtr3rd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ๐‘Ž ยท ( 1 / ( ๐‘Ž ยท ๐‘Ž ) ) ) = ( 1 / ๐‘Ž ) )
120 113 51 119 3brtr4d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ๐‘Ž ยท ( abs โ€˜ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) ) < ( ๐‘Ž ยท ( 1 / ( ๐‘Ž ยท ๐‘Ž ) ) ) )
121 ltmul2 โŠข ( ( ( abs โ€˜ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) โˆˆ โ„ โˆง ( 1 / ( ๐‘Ž ยท ๐‘Ž ) ) โˆˆ โ„ โˆง ( ๐‘Ž โˆˆ โ„ โˆง 0 < ๐‘Ž ) ) โ†’ ( ( abs โ€˜ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) < ( 1 / ( ๐‘Ž ยท ๐‘Ž ) ) โ†” ( ๐‘Ž ยท ( abs โ€˜ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) ) < ( ๐‘Ž ยท ( 1 / ( ๐‘Ž ยท ๐‘Ž ) ) ) ) )
122 91 99 22 92 121 syl112anc โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ( abs โ€˜ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) < ( 1 / ( ๐‘Ž ยท ๐‘Ž ) ) โ†” ( ๐‘Ž ยท ( abs โ€˜ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) ) < ( ๐‘Ž ยท ( 1 / ( ๐‘Ž ยท ๐‘Ž ) ) ) ) )
123 120 122 mpbird โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( abs โ€˜ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) < ( 1 / ( ๐‘Ž ยท ๐‘Ž ) ) )
124 9 nnzd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ๐‘ โˆˆ โ„ค )
125 divdenle โŠข ( ( ๐‘ โˆˆ โ„ค โˆง ๐‘Ž โˆˆ โ„• ) โ†’ ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) โ‰ค ๐‘Ž )
126 124 12 125 syl2anc โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) โ‰ค ๐‘Ž )
127 101 nnnn0d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) โˆˆ โ„•0 )
128 127 nn0ge0d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ 0 โ‰ค ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) )
129 le2msq โŠข ( ( ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) โˆˆ โ„ โˆง 0 โ‰ค ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ) โˆง ( ๐‘Ž โˆˆ โ„ โˆง 0 โ‰ค ๐‘Ž ) ) โ†’ ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) โ‰ค ๐‘Ž โ†” ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ยท ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ) โ‰ค ( ๐‘Ž ยท ๐‘Ž ) ) )
130 102 128 22 24 129 syl22anc โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) โ‰ค ๐‘Ž โ†” ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ยท ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ) โ‰ค ( ๐‘Ž ยท ๐‘Ž ) ) )
131 126 130 mpbid โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ยท ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ) โ‰ค ( ๐‘Ž ยท ๐‘Ž ) )
132 lerec โŠข ( ( ( ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ยท ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ) โˆˆ โ„ โˆง 0 < ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ยท ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ) ) โˆง ( ( ๐‘Ž ยท ๐‘Ž ) โˆˆ โ„ โˆง 0 < ( ๐‘Ž ยท ๐‘Ž ) ) ) โ†’ ( ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ยท ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ) โ‰ค ( ๐‘Ž ยท ๐‘Ž ) โ†” ( 1 / ( ๐‘Ž ยท ๐‘Ž ) ) โ‰ค ( 1 / ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ยท ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ) ) ) )
133 103 105 96 97 132 syl22anc โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ยท ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ) โ‰ค ( ๐‘Ž ยท ๐‘Ž ) โ†” ( 1 / ( ๐‘Ž ยท ๐‘Ž ) ) โ‰ค ( 1 / ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ยท ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ) ) ) )
134 131 133 mpbid โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( 1 / ( ๐‘Ž ยท ๐‘Ž ) ) โ‰ค ( 1 / ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ยท ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ) ) )
135 91 99 107 123 134 ltletrd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( abs โ€˜ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) < ( 1 / ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ยท ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ) ) )
136 101 nncnd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) โˆˆ โ„‚ )
137 2nn0 โŠข 2 โˆˆ โ„•0
138 expneg โŠข ( ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) โˆˆ โ„‚ โˆง 2 โˆˆ โ„•0 ) โ†’ ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) โ†‘ - 2 ) = ( 1 / ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) โ†‘ 2 ) ) )
139 136 137 138 sylancl โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) โ†‘ - 2 ) = ( 1 / ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) โ†‘ 2 ) ) )
140 136 sqvald โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) โ†‘ 2 ) = ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ยท ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ) )
141 140 oveq2d โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( 1 / ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) โ†‘ 2 ) ) = ( 1 / ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ยท ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ) ) )
142 139 141 eqtrd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) โ†‘ - 2 ) = ( 1 / ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ยท ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) ) ) )
143 135 142 breqtrrd โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ ( abs โ€˜ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) < ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) โ†‘ - 2 ) )
144 breq2 โŠข ( ๐‘ฅ = ( ๐‘ / ๐‘Ž ) โ†’ ( 0 < ๐‘ฅ โ†” 0 < ( ๐‘ / ๐‘Ž ) ) )
145 fvoveq1 โŠข ( ๐‘ฅ = ( ๐‘ / ๐‘Ž ) โ†’ ( abs โ€˜ ( ๐‘ฅ โˆ’ ๐ด ) ) = ( abs โ€˜ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) )
146 145 breq1d โŠข ( ๐‘ฅ = ( ๐‘ / ๐‘Ž ) โ†’ ( ( abs โ€˜ ( ๐‘ฅ โˆ’ ๐ด ) ) < ๐ต โ†” ( abs โ€˜ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) < ๐ต ) )
147 fveq2 โŠข ( ๐‘ฅ = ( ๐‘ / ๐‘Ž ) โ†’ ( denom โ€˜ ๐‘ฅ ) = ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) )
148 147 oveq1d โŠข ( ๐‘ฅ = ( ๐‘ / ๐‘Ž ) โ†’ ( ( denom โ€˜ ๐‘ฅ ) โ†‘ - 2 ) = ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) โ†‘ - 2 ) )
149 145 148 breq12d โŠข ( ๐‘ฅ = ( ๐‘ / ๐‘Ž ) โ†’ ( ( abs โ€˜ ( ๐‘ฅ โˆ’ ๐ด ) ) < ( ( denom โ€˜ ๐‘ฅ ) โ†‘ - 2 ) โ†” ( abs โ€˜ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) < ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) โ†‘ - 2 ) ) )
150 144 146 149 3anbi123d โŠข ( ๐‘ฅ = ( ๐‘ / ๐‘Ž ) โ†’ ( ( 0 < ๐‘ฅ โˆง ( abs โ€˜ ( ๐‘ฅ โˆ’ ๐ด ) ) < ๐ต โˆง ( abs โ€˜ ( ๐‘ฅ โˆ’ ๐ด ) ) < ( ( denom โ€˜ ๐‘ฅ ) โ†‘ - 2 ) ) โ†” ( 0 < ( ๐‘ / ๐‘Ž ) โˆง ( abs โ€˜ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) < ๐ต โˆง ( abs โ€˜ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) < ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) โ†‘ - 2 ) ) ) )
151 150 rspcev โŠข ( ( ( ๐‘ / ๐‘Ž ) โˆˆ โ„š โˆง ( 0 < ( ๐‘ / ๐‘Ž ) โˆง ( abs โ€˜ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) < ๐ต โˆง ( abs โ€˜ ( ( ๐‘ / ๐‘Ž ) โˆ’ ๐ด ) ) < ( ( denom โ€˜ ( ๐‘ / ๐‘Ž ) ) โ†‘ - 2 ) ) ) โ†’ โˆƒ ๐‘ฅ โˆˆ โ„š ( 0 < ๐‘ฅ โˆง ( abs โ€˜ ( ๐‘ฅ โˆ’ ๐ด ) ) < ๐ต โˆง ( abs โ€˜ ( ๐‘ฅ โˆ’ ๐ด ) ) < ( ( denom โ€˜ ๐‘ฅ ) โ†‘ - 2 ) ) )
152 17 21 95 143 151 syl13anc โŠข ( ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โˆง ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) ) โ†’ โˆƒ ๐‘ฅ โˆˆ โ„š ( 0 < ๐‘ฅ โˆง ( abs โ€˜ ( ๐‘ฅ โˆ’ ๐ด ) ) < ๐ต โˆง ( abs โ€˜ ( ๐‘ฅ โˆ’ ๐ด ) ) < ( ( denom โ€˜ ๐‘ฅ ) โ†‘ - 2 ) ) )
153 152 ex โŠข ( ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โˆง ( ๐‘Ž โˆˆ โ„• โˆง ๐‘ โˆˆ โ„• ) ) โ†’ ( ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) โ†’ โˆƒ ๐‘ฅ โˆˆ โ„š ( 0 < ๐‘ฅ โˆง ( abs โ€˜ ( ๐‘ฅ โˆ’ ๐ด ) ) < ๐ต โˆง ( abs โ€˜ ( ๐‘ฅ โˆ’ ๐ด ) ) < ( ( denom โ€˜ ๐‘ฅ ) โ†‘ - 2 ) ) ) )
154 153 rexlimdvva โŠข ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โ†’ ( โˆƒ ๐‘Ž โˆˆ โ„• โˆƒ ๐‘ โˆˆ โ„• ( abs โ€˜ ( ( ๐ด ยท ๐‘Ž ) โˆ’ ๐‘ ) ) < ( 1 / if ( ๐‘Ž โ‰ค ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ( ( โŒŠ โ€˜ ( 1 / ๐ต ) ) + 1 ) , ๐‘Ž ) ) โ†’ โˆƒ ๐‘ฅ โˆˆ โ„š ( 0 < ๐‘ฅ โˆง ( abs โ€˜ ( ๐‘ฅ โˆ’ ๐ด ) ) < ๐ต โˆง ( abs โ€˜ ( ๐‘ฅ โˆ’ ๐ด ) ) < ( ( denom โ€˜ ๐‘ฅ ) โ†‘ - 2 ) ) ) )
155 8 154 mpd โŠข ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โ†’ โˆƒ ๐‘ฅ โˆˆ โ„š ( 0 < ๐‘ฅ โˆง ( abs โ€˜ ( ๐‘ฅ โˆ’ ๐ด ) ) < ๐ต โˆง ( abs โ€˜ ( ๐‘ฅ โˆ’ ๐ด ) ) < ( ( denom โ€˜ ๐‘ฅ ) โ†‘ - 2 ) ) )