This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bernneq3

Description: A corollary of bernneq . (Contributed by Mario Carneiro, 11-Mar-2014)

Ref Expression
Assertion bernneq3 
|- ( ( P e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> N < ( P ^ N ) )

Proof

Step Hyp Ref Expression
1 nn0re 
 |-  ( N e. NN0 -> N e. RR )
2 1 adantl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> N e. RR )
3 peano2re 
 |-  ( N e. RR -> ( N + 1 ) e. RR )
4 2 3 syl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( N + 1 ) e. RR )
5 eluzelre 
 |-  ( P e. ( ZZ>= ` 2 ) -> P e. RR )
6 reexpcl 
 |-  ( ( P e. RR /\ N e. NN0 ) -> ( P ^ N ) e. RR )
7 5 6 sylan 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( P ^ N ) e. RR )
8 2 ltp1d 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> N < ( N + 1 ) )
9 uz2m1nn 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( P - 1 ) e. NN )
10 9 adantr 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( P - 1 ) e. NN )
11 10 nnred 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( P - 1 ) e. RR )
12 11 2 remulcld 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( ( P - 1 ) x. N ) e. RR )
13 peano2re 
 |-  ( ( ( P - 1 ) x. N ) e. RR -> ( ( ( P - 1 ) x. N ) + 1 ) e. RR )
14 12 13 syl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( ( ( P - 1 ) x. N ) + 1 ) e. RR )
15 1red 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> 1 e. RR )
16 nn0ge0 
 |-  ( N e. NN0 -> 0 <_ N )
17 16 adantl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> 0 <_ N )
18 10 nnge1d 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> 1 <_ ( P - 1 ) )
19 2 11 17 18 lemulge12d 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> N <_ ( ( P - 1 ) x. N ) )
20 2 12 15 19 leadd1dd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( N + 1 ) <_ ( ( ( P - 1 ) x. N ) + 1 ) )
21 5 adantr 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> P e. RR )
22 simpr 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> N e. NN0 )
23 eluzge2nn0 
 |-  ( P e. ( ZZ>= ` 2 ) -> P e. NN0 )
24 nn0ge0 
 |-  ( P e. NN0 -> 0 <_ P )
25 23 24 syl 
 |-  ( P e. ( ZZ>= ` 2 ) -> 0 <_ P )
26 25 adantr 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> 0 <_ P )
27 bernneq2 
 |-  ( ( P e. RR /\ N e. NN0 /\ 0 <_ P ) -> ( ( ( P - 1 ) x. N ) + 1 ) <_ ( P ^ N ) )
28 21 22 26 27 syl3anc 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( ( ( P - 1 ) x. N ) + 1 ) <_ ( P ^ N ) )
29 4 14 7 20 28 letrd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( N + 1 ) <_ ( P ^ N ) )
30 2 4 7 8 29 ltletrd 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> N < ( P ^ N ) )