Metamath Proof Explorer

Theorem xrralrecnnge

Description: Show that A is less than B by showing that there is no positive bound on the difference. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses xrralrecnnge.n 
|- F/ n ph
xrralrecnnge.a 
|- ( ph -> A e. RR )
xrralrecnnge.b 
|- ( ph -> B e. RR* )
Assertion xrralrecnnge 
|- ( ph -> ( A <_ B <-> A. n e. NN ( A - ( 1 / n ) ) <_ B ) )

Proof

Step Hyp Ref Expression
1 xrralrecnnge.n 
 |-  F/ n ph
2 xrralrecnnge.a 
 |-  ( ph -> A e. RR )
3 xrralrecnnge.b 
 |-  ( ph -> B e. RR* )
4 nfv 
 |-  F/ n A <_ B
5 1 4 nfan 
 |-  F/ n ( ph /\ A <_ B )
6 2 adantr 
 |-  ( ( ph /\ n e. NN ) -> A e. RR )
7 nnrecre 
 |-  ( n e. NN -> ( 1 / n ) e. RR )
8 7 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( 1 / n ) e. RR )
9 6 8 resubcld 
 |-  ( ( ph /\ n e. NN ) -> ( A - ( 1 / n ) ) e. RR )
10 9 rexrd 
 |-  ( ( ph /\ n e. NN ) -> ( A - ( 1 / n ) ) e. RR* )
11 10 adantlr 
 |-  ( ( ( ph /\ A <_ B ) /\ n e. NN ) -> ( A - ( 1 / n ) ) e. RR* )
12 3 ad2antrr 
 |-  ( ( ( ph /\ A <_ B ) /\ n e. NN ) -> B e. RR* )
13 2 rexrd 
 |-  ( ph -> A e. RR* )
14 13 ad2antrr 
 |-  ( ( ( ph /\ A <_ B ) /\ n e. NN ) -> A e. RR* )
15 nnrp 
 |-  ( n e. NN -> n e. RR+ )
16 15 rpreccld 
 |-  ( n e. NN -> ( 1 / n ) e. RR+ )
17 16 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( 1 / n ) e. RR+ )
18 6 17 ltsubrpd 
 |-  ( ( ph /\ n e. NN ) -> ( A - ( 1 / n ) ) < A )
19 18 adantlr 
 |-  ( ( ( ph /\ A <_ B ) /\ n e. NN ) -> ( A - ( 1 / n ) ) < A )
20 simplr 
 |-  ( ( ( ph /\ A <_ B ) /\ n e. NN ) -> A <_ B )
21 11 14 12 19 20 xrltletrd 
 |-  ( ( ( ph /\ A <_ B ) /\ n e. NN ) -> ( A - ( 1 / n ) ) < B )
22 11 12 21 xrltled 
 |-  ( ( ( ph /\ A <_ B ) /\ n e. NN ) -> ( A - ( 1 / n ) ) <_ B )
23 22 ex 
 |-  ( ( ph /\ A <_ B ) -> ( n e. NN -> ( A - ( 1 / n ) ) <_ B ) )
24 5 23 ralrimi 
 |-  ( ( ph /\ A <_ B ) -> A. n e. NN ( A - ( 1 / n ) ) <_ B )
25 24 ex 
 |-  ( ph -> ( A <_ B -> A. n e. NN ( A - ( 1 / n ) ) <_ B ) )
26 pnfxr 
 |-  +oo e. RR*
27 26 a1i 
 |-  ( ph -> +oo e. RR* )
28 2 ltpnfd 
 |-  ( ph -> A < +oo )
29 13 27 28 xrltled 
 |-  ( ph -> A <_ +oo )
30 29 ad2antrr 
 |-  ( ( ( ph /\ A. n e. NN ( A - ( 1 / n ) ) <_ B ) /\ B = +oo ) -> A <_ +oo )
31 id 
 |-  ( B = +oo -> B = +oo )
32 31 eqcomd 
 |-  ( B = +oo -> +oo = B )
33 32 adantl 
 |-  ( ( ( ph /\ A. n e. NN ( A - ( 1 / n ) ) <_ B ) /\ B = +oo ) -> +oo = B )
34 30 33 breqtrd 
 |-  ( ( ( ph /\ A. n e. NN ( A - ( 1 / n ) ) <_ B ) /\ B = +oo ) -> A <_ B )
35 3 ad2antrr 
 |-  ( ( ( ph /\ A. n e. NN ( A - ( 1 / n ) ) <_ B ) /\ -. B = +oo ) -> B e. RR* )
36 1nn 
 |-  1 e. NN
37 36 a1i 
 |-  ( A. n e. NN ( A - ( 1 / n ) ) <_ B -> 1 e. NN )
38 id 
 |-  ( A. n e. NN ( A - ( 1 / n ) ) <_ B -> A. n e. NN ( A - ( 1 / n ) ) <_ B )
39 oveq2 
 |-  ( n = 1 -> ( 1 / n ) = ( 1 / 1 ) )
40 39 oveq2d 
 |-  ( n = 1 -> ( A - ( 1 / n ) ) = ( A - ( 1 / 1 ) ) )
41 40 breq1d 
 |-  ( n = 1 -> ( ( A - ( 1 / n ) ) <_ B <-> ( A - ( 1 / 1 ) ) <_ B ) )
42 41 rspcva 
 |-  ( ( 1 e. NN /\ A. n e. NN ( A - ( 1 / n ) ) <_ B ) -> ( A - ( 1 / 1 ) ) <_ B )
43 37 38 42 syl2anc 
 |-  ( A. n e. NN ( A - ( 1 / n ) ) <_ B -> ( A - ( 1 / 1 ) ) <_ B )
44 43 adantr 
 |-  ( ( A. n e. NN ( A - ( 1 / n ) ) <_ B /\ B = -oo ) -> ( A - ( 1 / 1 ) ) <_ B )
45 simpr 
 |-  ( ( A. n e. NN ( A - ( 1 / n ) ) <_ B /\ B = -oo ) -> B = -oo )
46 44 45 breqtrd 
 |-  ( ( A. n e. NN ( A - ( 1 / n ) ) <_ B /\ B = -oo ) -> ( A - ( 1 / 1 ) ) <_ -oo )
47 46 adantll 
 |-  ( ( ( ph /\ A. n e. NN ( A - ( 1 / n ) ) <_ B ) /\ B = -oo ) -> ( A - ( 1 / 1 ) ) <_ -oo )
48 1red 
 |-  ( ph -> 1 e. RR )
49 ax-1ne0 
 |-  1 =/= 0
50 49 a1i 
 |-  ( ph -> 1 =/= 0 )
51 48 48 50 redivcld 
 |-  ( ph -> ( 1 / 1 ) e. RR )
52 2 51 resubcld 
 |-  ( ph -> ( A - ( 1 / 1 ) ) e. RR )
53 52 mnfltd 
 |-  ( ph -> -oo < ( A - ( 1 / 1 ) ) )
54 mnfxr 
 |-  -oo e. RR*
55 54 a1i 
 |-  ( ph -> -oo e. RR* )
56 52 rexrd 
 |-  ( ph -> ( A - ( 1 / 1 ) ) e. RR* )
57 55 56 xrltnled 
 |-  ( ph -> ( -oo < ( A - ( 1 / 1 ) ) <-> -. ( A - ( 1 / 1 ) ) <_ -oo ) )
58 53 57 mpbid 
 |-  ( ph -> -. ( A - ( 1 / 1 ) ) <_ -oo )
59 58 ad2antrr 
 |-  ( ( ( ph /\ A. n e. NN ( A - ( 1 / n ) ) <_ B ) /\ B = -oo ) -> -. ( A - ( 1 / 1 ) ) <_ -oo )
60 47 59 pm2.65da 
 |-  ( ( ph /\ A. n e. NN ( A - ( 1 / n ) ) <_ B ) -> -. B = -oo )
61 60 neqned 
 |-  ( ( ph /\ A. n e. NN ( A - ( 1 / n ) ) <_ B ) -> B =/= -oo )
62 61 adantr 
 |-  ( ( ( ph /\ A. n e. NN ( A - ( 1 / n ) ) <_ B ) /\ -. B = +oo ) -> B =/= -oo )
63 neqne 
 |-  ( -. B = +oo -> B =/= +oo )
64 63 adantl 
 |-  ( ( ( ph /\ A. n e. NN ( A - ( 1 / n ) ) <_ B ) /\ -. B = +oo ) -> B =/= +oo )
65 35 62 64 xrred 
 |-  ( ( ( ph /\ A. n e. NN ( A - ( 1 / n ) ) <_ B ) /\ -. B = +oo ) -> B e. RR )
66 nfv 
 |-  F/ n B e. RR
67 1 66 nfan 
 |-  F/ n ( ph /\ B e. RR )
68 13 adantr 
 |-  ( ( ph /\ B e. RR ) -> A e. RR* )
69 simpr 
 |-  ( ( ph /\ B e. RR ) -> B e. RR )
70 67 68 69 xrralrecnnle 
 |-  ( ( ph /\ B e. RR ) -> ( A <_ B <-> A. n e. NN A <_ ( B + ( 1 / n ) ) ) )
71 6 adantlr 
 |-  ( ( ( ph /\ B e. RR ) /\ n e. NN ) -> A e. RR )
72 7 adantl 
 |-  ( ( ( ph /\ B e. RR ) /\ n e. NN ) -> ( 1 / n ) e. RR )
73 69 adantr 
 |-  ( ( ( ph /\ B e. RR ) /\ n e. NN ) -> B e. RR )
74 71 72 73 lesubaddd 
 |-  ( ( ( ph /\ B e. RR ) /\ n e. NN ) -> ( ( A - ( 1 / n ) ) <_ B <-> A <_ ( B + ( 1 / n ) ) ) )
75 74 bicomd 
 |-  ( ( ( ph /\ B e. RR ) /\ n e. NN ) -> ( A <_ ( B + ( 1 / n ) ) <-> ( A - ( 1 / n ) ) <_ B ) )
76 67 75 ralbida 
 |-  ( ( ph /\ B e. RR ) -> ( A. n e. NN A <_ ( B + ( 1 / n ) ) <-> A. n e. NN ( A - ( 1 / n ) ) <_ B ) )
77 70 76 bitr2d 
 |-  ( ( ph /\ B e. RR ) -> ( A. n e. NN ( A - ( 1 / n ) ) <_ B <-> A <_ B ) )
78 77 biimpd 
 |-  ( ( ph /\ B e. RR ) -> ( A. n e. NN ( A - ( 1 / n ) ) <_ B -> A <_ B ) )
79 78 imp 
 |-  ( ( ( ph /\ B e. RR ) /\ A. n e. NN ( A - ( 1 / n ) ) <_ B ) -> A <_ B )
80 79 an32s 
 |-  ( ( ( ph /\ A. n e. NN ( A - ( 1 / n ) ) <_ B ) /\ B e. RR ) -> A <_ B )
81 65 80 syldan 
 |-  ( ( ( ph /\ A. n e. NN ( A - ( 1 / n ) ) <_ B ) /\ -. B = +oo ) -> A <_ B )
82 34 81 pm2.61dan 
 |-  ( ( ph /\ A. n e. NN ( A - ( 1 / n ) ) <_ B ) -> A <_ B )
83 82 ex 
 |-  ( ph -> ( A. n e. NN ( A - ( 1 / n ) ) <_ B -> A <_ B ) )
84 25 83 impbid 
 |-  ( ph -> ( A <_ B <-> A. n e. NN ( A - ( 1 / n ) ) <_ B ) )