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 ) ) ) )