Metamath Proof Explorer

Theorem xralrple4

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 xralrple4.a 
|- ( ph -> A e. RR* )
xralrple4.b 
|- ( ph -> B e. RR )
xralrple4.n 
|- ( ph -> N e. NN )
Assertion xralrple4 
|- ( ph -> ( A <_ B <-> A. x e. RR+ A <_ ( B + ( x ^ N ) ) ) )

Proof

Step Hyp Ref Expression
1 xralrple4.a 
 |-  ( ph -> A e. RR* )
2 xralrple4.b 
 |-  ( ph -> B e. RR )
3 xralrple4.n 
 |-  ( ph -> N e. NN )
4 1 ad2antrr 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> A e. RR* )
5 2 rexrd 
 |-  ( ph -> B e. RR* )
6 5 ad2antrr 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> B e. RR* )
7 2 ad2antrr 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> B e. RR )
8 rpre 
 |-  ( x e. RR+ -> x e. RR )
9 8 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR )
10 3 nnnn0d 
 |-  ( ph -> N e. NN0 )
11 10 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> N e. NN0 )
12 9 11 reexpcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( x ^ N ) e. RR )
13 12 adantlr 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> ( x ^ N ) e. RR )
14 7 13 readdcld 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> ( B + ( x ^ N ) ) e. RR )
15 14 rexrd 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> ( B + ( x ^ N ) ) e. RR* )
16 simplr 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> A <_ B )
17 rpge0 
 |-  ( x e. RR+ -> 0 <_ x )
18 17 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> 0 <_ x )
19 9 11 18 expge0d 
 |-  ( ( ph /\ x e. RR+ ) -> 0 <_ ( x ^ N ) )
20 2 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> B e. RR )
21 20 12 addge01d 
 |-  ( ( ph /\ x e. RR+ ) -> ( 0 <_ ( x ^ N ) <-> B <_ ( B + ( x ^ N ) ) ) )
22 19 21 mpbid 
 |-  ( ( ph /\ x e. RR+ ) -> B <_ ( B + ( x ^ N ) ) )
23 22 adantlr 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> B <_ ( B + ( x ^ N ) ) )
24 4 6 15 16 23 xrletrd 
 |-  ( ( ( ph /\ A <_ B ) /\ x e. RR+ ) -> A <_ ( B + ( x ^ N ) ) )
25 24 ralrimiva 
 |-  ( ( ph /\ A <_ B ) -> A. x e. RR+ A <_ ( B + ( x ^ N ) ) )
26 25 ex 
 |-  ( ph -> ( A <_ B -> A. x e. RR+ A <_ ( B + ( x ^ N ) ) ) )
27 simpr 
 |-  ( ( ph /\ y e. RR+ ) -> y e. RR+ )
28 3 nnrpd 
 |-  ( ph -> N e. RR+ )
29 28 rpreccld 
 |-  ( ph -> ( 1 / N ) e. RR+ )
30 29 rpred 
 |-  ( ph -> ( 1 / N ) e. RR )
31 30 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> ( 1 / N ) e. RR )
32 27 31 rpcxpcld 
 |-  ( ( ph /\ y e. RR+ ) -> ( y ^c ( 1 / N ) ) e. RR+ )
33 32 adantlr 
 |-  ( ( ( ph /\ A. x e. RR+ A <_ ( B + ( x ^ N ) ) ) /\ y e. RR+ ) -> ( y ^c ( 1 / N ) ) e. RR+ )
34 simplr 
 |-  ( ( ( ph /\ A. x e. RR+ A <_ ( B + ( x ^ N ) ) ) /\ y e. RR+ ) -> A. x e. RR+ A <_ ( B + ( x ^ N ) ) )
35 oveq1 
 |-  ( x = ( y ^c ( 1 / N ) ) -> ( x ^ N ) = ( ( y ^c ( 1 / N ) ) ^ N ) )
36 35 oveq2d 
 |-  ( x = ( y ^c ( 1 / N ) ) -> ( B + ( x ^ N ) ) = ( B + ( ( y ^c ( 1 / N ) ) ^ N ) ) )
37 36 breq2d 
 |-  ( x = ( y ^c ( 1 / N ) ) -> ( A <_ ( B + ( x ^ N ) ) <-> A <_ ( B + ( ( y ^c ( 1 / N ) ) ^ N ) ) ) )
38 37 rspcva 
 |-  ( ( ( y ^c ( 1 / N ) ) e. RR+ /\ A. x e. RR+ A <_ ( B + ( x ^ N ) ) ) -> A <_ ( B + ( ( y ^c ( 1 / N ) ) ^ N ) ) )
39 33 34 38 syl2anc 
 |-  ( ( ( ph /\ A. x e. RR+ A <_ ( B + ( x ^ N ) ) ) /\ y e. RR+ ) -> A <_ ( B + ( ( y ^c ( 1 / N ) ) ^ N ) ) )
40 27 rpcnd 
 |-  ( ( ph /\ y e. RR+ ) -> y e. CC )
41 3 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> N e. NN )
42 cxproot 
 |-  ( ( y e. CC /\ N e. NN ) -> ( ( y ^c ( 1 / N ) ) ^ N ) = y )
43 40 41 42 syl2anc 
 |-  ( ( ph /\ y e. RR+ ) -> ( ( y ^c ( 1 / N ) ) ^ N ) = y )
44 43 oveq2d 
 |-  ( ( ph /\ y e. RR+ ) -> ( B + ( ( y ^c ( 1 / N ) ) ^ N ) ) = ( B + y ) )
45 44 adantlr 
 |-  ( ( ( ph /\ A. x e. RR+ A <_ ( B + ( x ^ N ) ) ) /\ y e. RR+ ) -> ( B + ( ( y ^c ( 1 / N ) ) ^ N ) ) = ( B + y ) )
46 39 45 breqtrd 
 |-  ( ( ( ph /\ A. x e. RR+ A <_ ( B + ( x ^ N ) ) ) /\ y e. RR+ ) -> A <_ ( B + y ) )
47 46 ralrimiva 
 |-  ( ( ph /\ A. x e. RR+ A <_ ( B + ( x ^ N ) ) ) -> A. y e. RR+ A <_ ( B + y ) )
48 xralrple 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( A <_ B <-> A. y e. RR+ A <_ ( B + y ) ) )
49 1 2 48 syl2anc 
 |-  ( ph -> ( A <_ B <-> A. y e. RR+ A <_ ( B + y ) ) )
50 49 adantr 
 |-  ( ( ph /\ A. x e. RR+ A <_ ( B + ( x ^ N ) ) ) -> ( A <_ B <-> A. y e. RR+ A <_ ( B + y ) ) )
51 47 50 mpbird 
 |-  ( ( ph /\ A. x e. RR+ A <_ ( B + ( x ^ N ) ) ) -> A <_ B )
52 51 ex 
 |-  ( ph -> ( A. x e. RR+ A <_ ( B + ( x ^ N ) ) -> A <_ B ) )
53 26 52 impbid 
 |-  ( ph -> ( A <_ B <-> A. x e. RR+ A <_ ( B + ( x ^ N ) ) ) )