Metamath Proof Explorer

Theorem nexple

Description: A lower bound for an exponentiation. (Contributed by Thierry Arnoux, 19-Aug-2017)

Ref Expression
Assertion nexple 
|- ( ( A e. NN0 /\ B e. RR /\ 2 <_ B ) -> A <_ ( B ^ A ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( ( A e. NN0 /\ B e. RR /\ 2 <_ B ) /\ A e. NN ) -> A e. NN )
2 simpl2 
 |-  ( ( ( A e. NN0 /\ B e. RR /\ 2 <_ B ) /\ A e. NN ) -> B e. RR )
3 simpl3 
 |-  ( ( ( A e. NN0 /\ B e. RR /\ 2 <_ B ) /\ A e. NN ) -> 2 <_ B )
4 id 
 |-  ( k = 1 -> k = 1 )
5 oveq2 
 |-  ( k = 1 -> ( B ^ k ) = ( B ^ 1 ) )
6 4 5 breq12d 
 |-  ( k = 1 -> ( k <_ ( B ^ k ) <-> 1 <_ ( B ^ 1 ) ) )
7 6 imbi2d 
 |-  ( k = 1 -> ( ( ( B e. RR /\ 2 <_ B ) -> k <_ ( B ^ k ) ) <-> ( ( B e. RR /\ 2 <_ B ) -> 1 <_ ( B ^ 1 ) ) ) )
8 id 
 |-  ( k = n -> k = n )
9 oveq2 
 |-  ( k = n -> ( B ^ k ) = ( B ^ n ) )
10 8 9 breq12d 
 |-  ( k = n -> ( k <_ ( B ^ k ) <-> n <_ ( B ^ n ) ) )
11 10 imbi2d 
 |-  ( k = n -> ( ( ( B e. RR /\ 2 <_ B ) -> k <_ ( B ^ k ) ) <-> ( ( B e. RR /\ 2 <_ B ) -> n <_ ( B ^ n ) ) ) )
12 id 
 |-  ( k = ( n + 1 ) -> k = ( n + 1 ) )
13 oveq2 
 |-  ( k = ( n + 1 ) -> ( B ^ k ) = ( B ^ ( n + 1 ) ) )
14 12 13 breq12d 
 |-  ( k = ( n + 1 ) -> ( k <_ ( B ^ k ) <-> ( n + 1 ) <_ ( B ^ ( n + 1 ) ) ) )
15 14 imbi2d 
 |-  ( k = ( n + 1 ) -> ( ( ( B e. RR /\ 2 <_ B ) -> k <_ ( B ^ k ) ) <-> ( ( B e. RR /\ 2 <_ B ) -> ( n + 1 ) <_ ( B ^ ( n + 1 ) ) ) ) )
16 id 
 |-  ( k = A -> k = A )
17 oveq2 
 |-  ( k = A -> ( B ^ k ) = ( B ^ A ) )
18 16 17 breq12d 
 |-  ( k = A -> ( k <_ ( B ^ k ) <-> A <_ ( B ^ A ) ) )
19 18 imbi2d 
 |-  ( k = A -> ( ( ( B e. RR /\ 2 <_ B ) -> k <_ ( B ^ k ) ) <-> ( ( B e. RR /\ 2 <_ B ) -> A <_ ( B ^ A ) ) ) )
20 simpl 
 |-  ( ( B e. RR /\ 2 <_ B ) -> B e. RR )
21 1nn0 
 |-  1 e. NN0
22 21 a1i 
 |-  ( ( B e. RR /\ 2 <_ B ) -> 1 e. NN0 )
23 1red 
 |-  ( ( B e. RR /\ 2 <_ B ) -> 1 e. RR )
24 2re 
 |-  2 e. RR
25 24 a1i 
 |-  ( ( B e. RR /\ 2 <_ B ) -> 2 e. RR )
26 1le2 
 |-  1 <_ 2
27 26 a1i 
 |-  ( ( B e. RR /\ 2 <_ B ) -> 1 <_ 2 )
28 simpr 
 |-  ( ( B e. RR /\ 2 <_ B ) -> 2 <_ B )
29 23 25 20 27 28 letrd 
 |-  ( ( B e. RR /\ 2 <_ B ) -> 1 <_ B )
30 20 22 29 expge1d 
 |-  ( ( B e. RR /\ 2 <_ B ) -> 1 <_ ( B ^ 1 ) )
31 simp1 
 |-  ( ( n e. NN /\ ( B e. RR /\ 2 <_ B ) /\ n <_ ( B ^ n ) ) -> n e. NN )
32 31 nnnn0d 
 |-  ( ( n e. NN /\ ( B e. RR /\ 2 <_ B ) /\ n <_ ( B ^ n ) ) -> n e. NN0 )
33 32 nn0red 
 |-  ( ( n e. NN /\ ( B e. RR /\ 2 <_ B ) /\ n <_ ( B ^ n ) ) -> n e. RR )
34 1red 
 |-  ( ( n e. NN /\ ( B e. RR /\ 2 <_ B ) /\ n <_ ( B ^ n ) ) -> 1 e. RR )
35 33 34 readdcld 
 |-  ( ( n e. NN /\ ( B e. RR /\ 2 <_ B ) /\ n <_ ( B ^ n ) ) -> ( n + 1 ) e. RR )
36 20 3ad2ant2 
 |-  ( ( n e. NN /\ ( B e. RR /\ 2 <_ B ) /\ n <_ ( B ^ n ) ) -> B e. RR )
37 33 36 remulcld 
 |-  ( ( n e. NN /\ ( B e. RR /\ 2 <_ B ) /\ n <_ ( B ^ n ) ) -> ( n x. B ) e. RR )
38 36 32 reexpcld 
 |-  ( ( n e. NN /\ ( B e. RR /\ 2 <_ B ) /\ n <_ ( B ^ n ) ) -> ( B ^ n ) e. RR )
39 38 36 remulcld 
 |-  ( ( n e. NN /\ ( B e. RR /\ 2 <_ B ) /\ n <_ ( B ^ n ) ) -> ( ( B ^ n ) x. B ) e. RR )
40 24 a1i 
 |-  ( ( n e. NN /\ ( B e. RR /\ 2 <_ B ) /\ n <_ ( B ^ n ) ) -> 2 e. RR )
41 33 40 remulcld 
 |-  ( ( n e. NN /\ ( B e. RR /\ 2 <_ B ) /\ n <_ ( B ^ n ) ) -> ( n x. 2 ) e. RR )
42 31 nnge1d 
 |-  ( ( n e. NN /\ ( B e. RR /\ 2 <_ B ) /\ n <_ ( B ^ n ) ) -> 1 <_ n )
43 34 33 33 42 leadd2dd 
 |-  ( ( n e. NN /\ ( B e. RR /\ 2 <_ B ) /\ n <_ ( B ^ n ) ) -> ( n + 1 ) <_ ( n + n ) )
44 33 recnd 
 |-  ( ( n e. NN /\ ( B e. RR /\ 2 <_ B ) /\ n <_ ( B ^ n ) ) -> n e. CC )
45 44 times2d 
 |-  ( ( n e. NN /\ ( B e. RR /\ 2 <_ B ) /\ n <_ ( B ^ n ) ) -> ( n x. 2 ) = ( n + n ) )
46 43 45 breqtrrd 
 |-  ( ( n e. NN /\ ( B e. RR /\ 2 <_ B ) /\ n <_ ( B ^ n ) ) -> ( n + 1 ) <_ ( n x. 2 ) )
47 32 nn0ge0d 
 |-  ( ( n e. NN /\ ( B e. RR /\ 2 <_ B ) /\ n <_ ( B ^ n ) ) -> 0 <_ n )
48 simp2r 
 |-  ( ( n e. NN /\ ( B e. RR /\ 2 <_ B ) /\ n <_ ( B ^ n ) ) -> 2 <_ B )
49 40 36 33 47 48 lemul2ad 
 |-  ( ( n e. NN /\ ( B e. RR /\ 2 <_ B ) /\ n <_ ( B ^ n ) ) -> ( n x. 2 ) <_ ( n x. B ) )
50 35 41 37 46 49 letrd 
 |-  ( ( n e. NN /\ ( B e. RR /\ 2 <_ B ) /\ n <_ ( B ^ n ) ) -> ( n + 1 ) <_ ( n x. B ) )
51 0red 
 |-  ( ( B e. RR /\ 2 <_ B ) -> 0 e. RR )
52 0le2 
 |-  0 <_ 2
53 52 a1i 
 |-  ( ( B e. RR /\ 2 <_ B ) -> 0 <_ 2 )
54 51 25 20 53 28 letrd 
 |-  ( ( B e. RR /\ 2 <_ B ) -> 0 <_ B )
55 54 3ad2ant2 
 |-  ( ( n e. NN /\ ( B e. RR /\ 2 <_ B ) /\ n <_ ( B ^ n ) ) -> 0 <_ B )
56 simp3 
 |-  ( ( n e. NN /\ ( B e. RR /\ 2 <_ B ) /\ n <_ ( B ^ n ) ) -> n <_ ( B ^ n ) )
57 33 38 36 55 56 lemul1ad 
 |-  ( ( n e. NN /\ ( B e. RR /\ 2 <_ B ) /\ n <_ ( B ^ n ) ) -> ( n x. B ) <_ ( ( B ^ n ) x. B ) )
58 35 37 39 50 57 letrd 
 |-  ( ( n e. NN /\ ( B e. RR /\ 2 <_ B ) /\ n <_ ( B ^ n ) ) -> ( n + 1 ) <_ ( ( B ^ n ) x. B ) )
59 36 recnd 
 |-  ( ( n e. NN /\ ( B e. RR /\ 2 <_ B ) /\ n <_ ( B ^ n ) ) -> B e. CC )
60 59 32 expp1d 
 |-  ( ( n e. NN /\ ( B e. RR /\ 2 <_ B ) /\ n <_ ( B ^ n ) ) -> ( B ^ ( n + 1 ) ) = ( ( B ^ n ) x. B ) )
61 58 60 breqtrrd 
 |-  ( ( n e. NN /\ ( B e. RR /\ 2 <_ B ) /\ n <_ ( B ^ n ) ) -> ( n + 1 ) <_ ( B ^ ( n + 1 ) ) )
62 61 3exp 
 |-  ( n e. NN -> ( ( B e. RR /\ 2 <_ B ) -> ( n <_ ( B ^ n ) -> ( n + 1 ) <_ ( B ^ ( n + 1 ) ) ) ) )
63 62 a2d 
 |-  ( n e. NN -> ( ( ( B e. RR /\ 2 <_ B ) -> n <_ ( B ^ n ) ) -> ( ( B e. RR /\ 2 <_ B ) -> ( n + 1 ) <_ ( B ^ ( n + 1 ) ) ) ) )
64 7 11 15 19 30 63 nnind 
 |-  ( A e. NN -> ( ( B e. RR /\ 2 <_ B ) -> A <_ ( B ^ A ) ) )
65 64 3impib 
 |-  ( ( A e. NN /\ B e. RR /\ 2 <_ B ) -> A <_ ( B ^ A ) )
66 1 2 3 65 syl3anc 
 |-  ( ( ( A e. NN0 /\ B e. RR /\ 2 <_ B ) /\ A e. NN ) -> A <_ ( B ^ A ) )
67 0le1 
 |-  0 <_ 1
68 67 a1i 
 |-  ( ( ( A e. NN0 /\ B e. RR /\ 2 <_ B ) /\ A = 0 ) -> 0 <_ 1 )
69 simpr 
 |-  ( ( ( A e. NN0 /\ B e. RR /\ 2 <_ B ) /\ A = 0 ) -> A = 0 )
70 69 oveq2d 
 |-  ( ( ( A e. NN0 /\ B e. RR /\ 2 <_ B ) /\ A = 0 ) -> ( B ^ A ) = ( B ^ 0 ) )
71 simpl2 
 |-  ( ( ( A e. NN0 /\ B e. RR /\ 2 <_ B ) /\ A = 0 ) -> B e. RR )
72 71 recnd 
 |-  ( ( ( A e. NN0 /\ B e. RR /\ 2 <_ B ) /\ A = 0 ) -> B e. CC )
73 72 exp0d 
 |-  ( ( ( A e. NN0 /\ B e. RR /\ 2 <_ B ) /\ A = 0 ) -> ( B ^ 0 ) = 1 )
74 70 73 eqtrd 
 |-  ( ( ( A e. NN0 /\ B e. RR /\ 2 <_ B ) /\ A = 0 ) -> ( B ^ A ) = 1 )
75 68 69 74 3brtr4d 
 |-  ( ( ( A e. NN0 /\ B e. RR /\ 2 <_ B ) /\ A = 0 ) -> A <_ ( B ^ A ) )
76 elnn0 
 |-  ( A e. NN0 <-> ( A e. NN \/ A = 0 ) )
77 76 biimpi 
 |-  ( A e. NN0 -> ( A e. NN \/ A = 0 ) )
78 77 3ad2ant1 
 |-  ( ( A e. NN0 /\ B e. RR /\ 2 <_ B ) -> ( A e. NN \/ A = 0 ) )
79 66 75 78 mpjaodan 
 |-  ( ( A e. NN0 /\ B e. RR /\ 2 <_ B ) -> A <_ ( B ^ A ) )