Metamath Proof Explorer

Theorem xrralrecnnle

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

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

Proof

Step Hyp Ref Expression
1 xrralrecnnle.n 
 |-  F/ n ph
2 xrralrecnnle.a 
 |-  ( ph -> A e. RR* )
3 xrralrecnnle.b 
 |-  ( ph -> B e. RR )
4 nfv 
 |-  F/ n A <_ B
5 1 4 nfan 
 |-  F/ n ( ph /\ A <_ B )
6 2 ad2antrr 
 |-  ( ( ( ph /\ A <_ B ) /\ n e. NN ) -> A e. RR* )
7 3 adantr 
 |-  ( ( ph /\ n e. NN ) -> B e. RR )
8 nnrecre 
 |-  ( n e. NN -> ( 1 / n ) e. RR )
9 8 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( 1 / n ) e. RR )
10 7 9 readdcld 
 |-  ( ( ph /\ n e. NN ) -> ( B + ( 1 / n ) ) e. RR )
11 10 rexrd 
 |-  ( ( ph /\ n e. NN ) -> ( B + ( 1 / n ) ) e. RR* )
12 11 adantlr 
 |-  ( ( ( ph /\ A <_ B ) /\ n e. NN ) -> ( B + ( 1 / n ) ) e. RR* )
13 rexr 
 |-  ( B e. RR -> B e. RR* )
14 3 13 syl 
 |-  ( ph -> B e. RR* )
15 14 ad2antrr 
 |-  ( ( ( ph /\ A <_ B ) /\ n e. NN ) -> B e. RR* )
16 simplr 
 |-  ( ( ( ph /\ A <_ B ) /\ n e. NN ) -> A <_ B )
17 nnrp 
 |-  ( n e. NN -> n e. RR+ )
18 rpreccl 
 |-  ( n e. RR+ -> ( 1 / n ) e. RR+ )
19 17 18 syl 
 |-  ( n e. NN -> ( 1 / n ) e. RR+ )
20 19 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( 1 / n ) e. RR+ )
21 7 20 ltaddrpd 
 |-  ( ( ph /\ n e. NN ) -> B < ( B + ( 1 / n ) ) )
22 21 adantlr 
 |-  ( ( ( ph /\ A <_ B ) /\ n e. NN ) -> B < ( B + ( 1 / n ) ) )
23 6 15 12 16 22 xrlelttrd 
 |-  ( ( ( ph /\ A <_ B ) /\ n e. NN ) -> A < ( B + ( 1 / n ) ) )
24 6 12 23 xrltled 
 |-  ( ( ( ph /\ A <_ B ) /\ n e. NN ) -> A <_ ( B + ( 1 / n ) ) )
25 24 ex 
 |-  ( ( ph /\ A <_ B ) -> ( n e. NN -> A <_ ( B + ( 1 / n ) ) ) )
26 5 25 ralrimi 
 |-  ( ( ph /\ A <_ B ) -> A. n e. NN A <_ ( B + ( 1 / n ) ) )
27 26 ex 
 |-  ( ph -> ( A <_ B -> A. n e. NN A <_ ( B + ( 1 / n ) ) ) )
28 rpgtrecnn 
 |-  ( x e. RR+ -> E. n e. NN ( 1 / n ) < x )
29 28 adantl 
 |-  ( ( ( ph /\ A. n e. NN A <_ ( B + ( 1 / n ) ) ) /\ x e. RR+ ) -> E. n e. NN ( 1 / n ) < x )
30 nfra1 
 |-  F/ n A. n e. NN A <_ ( B + ( 1 / n ) )
31 1 30 nfan 
 |-  F/ n ( ph /\ A. n e. NN A <_ ( B + ( 1 / n ) ) )
32 nfv 
 |-  F/ n x e. RR+
33 31 32 nfan 
 |-  F/ n ( ( ph /\ A. n e. NN A <_ ( B + ( 1 / n ) ) ) /\ x e. RR+ )
34 nfv 
 |-  F/ n A <_ ( B + x )
35 simpll 
 |-  ( ( ( ph /\ A. n e. NN A <_ ( B + ( 1 / n ) ) ) /\ n e. NN ) -> ph )
36 rspa 
 |-  ( ( A. n e. NN A <_ ( B + ( 1 / n ) ) /\ n e. NN ) -> A <_ ( B + ( 1 / n ) ) )
37 36 adantll 
 |-  ( ( ( ph /\ A. n e. NN A <_ ( B + ( 1 / n ) ) ) /\ n e. NN ) -> A <_ ( B + ( 1 / n ) ) )
38 35 37 jca 
 |-  ( ( ( ph /\ A. n e. NN A <_ ( B + ( 1 / n ) ) ) /\ n e. NN ) -> ( ph /\ A <_ ( B + ( 1 / n ) ) ) )
39 38 adantlr 
 |-  ( ( ( ( ph /\ A. n e. NN A <_ ( B + ( 1 / n ) ) ) /\ x e. RR+ ) /\ n e. NN ) -> ( ph /\ A <_ ( B + ( 1 / n ) ) ) )
40 simplr 
 |-  ( ( ( ( ph /\ A. n e. NN A <_ ( B + ( 1 / n ) ) ) /\ x e. RR+ ) /\ n e. NN ) -> x e. RR+ )
41 simpr 
 |-  ( ( ( ( ph /\ A. n e. NN A <_ ( B + ( 1 / n ) ) ) /\ x e. RR+ ) /\ n e. NN ) -> n e. NN )
42 2 ad4antr 
 |-  ( ( ( ( ( ph /\ A <_ ( B + ( 1 / n ) ) ) /\ x e. RR+ ) /\ n e. NN ) /\ ( 1 / n ) < x ) -> A e. RR* )
43 3 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> B e. RR )
44 rpre 
 |-  ( x e. RR+ -> x e. RR )
45 44 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR )
46 43 45 readdcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( B + x ) e. RR )
47 46 rexrd 
 |-  ( ( ph /\ x e. RR+ ) -> ( B + x ) e. RR* )
48 47 ad5ant13 
 |-  ( ( ( ( ( ph /\ A <_ ( B + ( 1 / n ) ) ) /\ x e. RR+ ) /\ n e. NN ) /\ ( 1 / n ) < x ) -> ( B + x ) e. RR* )
49 11 ad5ant14 
 |-  ( ( ( ( ( ph /\ A <_ ( B + ( 1 / n ) ) ) /\ x e. RR+ ) /\ n e. NN ) /\ ( 1 / n ) < x ) -> ( B + ( 1 / n ) ) e. RR* )
50 simp-4r 
 |-  ( ( ( ( ( ph /\ A <_ ( B + ( 1 / n ) ) ) /\ x e. RR+ ) /\ n e. NN ) /\ ( 1 / n ) < x ) -> A <_ ( B + ( 1 / n ) ) )
51 8 ad2antlr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. NN ) /\ ( 1 / n ) < x ) -> ( 1 / n ) e. RR )
52 45 ad2antrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. NN ) /\ ( 1 / n ) < x ) -> x e. RR )
53 43 ad2antrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. NN ) /\ ( 1 / n ) < x ) -> B e. RR )
54 simpr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. NN ) /\ ( 1 / n ) < x ) -> ( 1 / n ) < x )
55 51 52 53 54 ltadd2dd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. NN ) /\ ( 1 / n ) < x ) -> ( B + ( 1 / n ) ) < ( B + x ) )
56 55 adantl3r 
 |-  ( ( ( ( ( ph /\ A <_ ( B + ( 1 / n ) ) ) /\ x e. RR+ ) /\ n e. NN ) /\ ( 1 / n ) < x ) -> ( B + ( 1 / n ) ) < ( B + x ) )
57 42 49 48 50 56 xrlelttrd 
 |-  ( ( ( ( ( ph /\ A <_ ( B + ( 1 / n ) ) ) /\ x e. RR+ ) /\ n e. NN ) /\ ( 1 / n ) < x ) -> A < ( B + x ) )
58 42 48 57 xrltled 
 |-  ( ( ( ( ( ph /\ A <_ ( B + ( 1 / n ) ) ) /\ x e. RR+ ) /\ n e. NN ) /\ ( 1 / n ) < x ) -> A <_ ( B + x ) )
59 58 ex 
 |-  ( ( ( ( ph /\ A <_ ( B + ( 1 / n ) ) ) /\ x e. RR+ ) /\ n e. NN ) -> ( ( 1 / n ) < x -> A <_ ( B + x ) ) )
60 39 40 41 59 syl21anc 
 |-  ( ( ( ( ph /\ A. n e. NN A <_ ( B + ( 1 / n ) ) ) /\ x e. RR+ ) /\ n e. NN ) -> ( ( 1 / n ) < x -> A <_ ( B + x ) ) )
61 60 ex 
 |-  ( ( ( ph /\ A. n e. NN A <_ ( B + ( 1 / n ) ) ) /\ x e. RR+ ) -> ( n e. NN -> ( ( 1 / n ) < x -> A <_ ( B + x ) ) ) )
62 33 34 61 rexlimd 
 |-  ( ( ( ph /\ A. n e. NN A <_ ( B + ( 1 / n ) ) ) /\ x e. RR+ ) -> ( E. n e. NN ( 1 / n ) < x -> A <_ ( B + x ) ) )
63 29 62 mpd 
 |-  ( ( ( ph /\ A. n e. NN A <_ ( B + ( 1 / n ) ) ) /\ x e. RR+ ) -> A <_ ( B + x ) )
64 63 ralrimiva 
 |-  ( ( ph /\ A. n e. NN A <_ ( B + ( 1 / n ) ) ) -> A. x e. RR+ A <_ ( B + x ) )
65 xralrple 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( A <_ B <-> A. x e. RR+ A <_ ( B + x ) ) )
66 2 3 65 syl2anc 
 |-  ( ph -> ( A <_ B <-> A. x e. RR+ A <_ ( B + x ) ) )
67 66 adantr 
 |-  ( ( ph /\ A. n e. NN A <_ ( B + ( 1 / n ) ) ) -> ( A <_ B <-> A. x e. RR+ A <_ ( B + x ) ) )
68 64 67 mpbird 
 |-  ( ( ph /\ A. n e. NN A <_ ( B + ( 1 / n ) ) ) -> A <_ B )
69 68 ex 
 |-  ( ph -> ( A. n e. NN A <_ ( B + ( 1 / n ) ) -> A <_ B ) )
70 27 69 impbid 
 |-  ( ph -> ( A <_ B <-> A. n e. NN A <_ ( B + ( 1 / n ) ) ) )