Metamath Proof Explorer

Theorem expnngt1

Description: If an integer power with a positive integer base is greater than 1, then the exponent is positive. (Contributed by AV, 28-Dec-2022)

Ref Expression
Assertion expnngt1 
|- ( ( A e. NN /\ B e. ZZ /\ 1 < ( A ^ B ) ) -> B e. NN )

Proof

Step Hyp Ref Expression
1 elznn 
 |-  ( B e. ZZ <-> ( B e. RR /\ ( B e. NN \/ -u B e. NN0 ) ) )
2 2a1 
 |-  ( B e. NN -> ( A e. NN -> ( 1 < ( A ^ B ) -> B e. NN ) ) )
3 2 a1d 
 |-  ( B e. NN -> ( B e. RR -> ( A e. NN -> ( 1 < ( A ^ B ) -> B e. NN ) ) ) )
4 nncn 
 |-  ( A e. NN -> A e. CC )
5 4 3ad2ant3 
 |-  ( ( -u B e. NN0 /\ B e. RR /\ A e. NN ) -> A e. CC )
6 recn 
 |-  ( B e. RR -> B e. CC )
7 6 3ad2ant2 
 |-  ( ( -u B e. NN0 /\ B e. RR /\ A e. NN ) -> B e. CC )
8 simp1 
 |-  ( ( -u B e. NN0 /\ B e. RR /\ A e. NN ) -> -u B e. NN0 )
9 expneg2 
 |-  ( ( A e. CC /\ B e. CC /\ -u B e. NN0 ) -> ( A ^ B ) = ( 1 / ( A ^ -u B ) ) )
10 5 7 8 9 syl3anc 
 |-  ( ( -u B e. NN0 /\ B e. RR /\ A e. NN ) -> ( A ^ B ) = ( 1 / ( A ^ -u B ) ) )
11 10 breq2d 
 |-  ( ( -u B e. NN0 /\ B e. RR /\ A e. NN ) -> ( 1 < ( A ^ B ) <-> 1 < ( 1 / ( A ^ -u B ) ) ) )
12 nnre 
 |-  ( A e. NN -> A e. RR )
13 reexpcl 
 |-  ( ( A e. RR /\ -u B e. NN0 ) -> ( A ^ -u B ) e. RR )
14 12 13 sylan 
 |-  ( ( A e. NN /\ -u B e. NN0 ) -> ( A ^ -u B ) e. RR )
15 14 ancoms 
 |-  ( ( -u B e. NN0 /\ A e. NN ) -> ( A ^ -u B ) e. RR )
16 12 adantl 
 |-  ( ( -u B e. NN0 /\ A e. NN ) -> A e. RR )
17 nn0z 
 |-  ( -u B e. NN0 -> -u B e. ZZ )
18 17 adantr 
 |-  ( ( -u B e. NN0 /\ A e. NN ) -> -u B e. ZZ )
19 nngt0 
 |-  ( A e. NN -> 0 < A )
20 19 adantl 
 |-  ( ( -u B e. NN0 /\ A e. NN ) -> 0 < A )
21 expgt0 
 |-  ( ( A e. RR /\ -u B e. ZZ /\ 0 < A ) -> 0 < ( A ^ -u B ) )
22 16 18 20 21 syl3anc 
 |-  ( ( -u B e. NN0 /\ A e. NN ) -> 0 < ( A ^ -u B ) )
23 15 22 jca 
 |-  ( ( -u B e. NN0 /\ A e. NN ) -> ( ( A ^ -u B ) e. RR /\ 0 < ( A ^ -u B ) ) )
24 23 3adant2 
 |-  ( ( -u B e. NN0 /\ B e. RR /\ A e. NN ) -> ( ( A ^ -u B ) e. RR /\ 0 < ( A ^ -u B ) ) )
25 reclt1 
 |-  ( ( ( A ^ -u B ) e. RR /\ 0 < ( A ^ -u B ) ) -> ( ( A ^ -u B ) < 1 <-> 1 < ( 1 / ( A ^ -u B ) ) ) )
26 24 25 syl 
 |-  ( ( -u B e. NN0 /\ B e. RR /\ A e. NN ) -> ( ( A ^ -u B ) < 1 <-> 1 < ( 1 / ( A ^ -u B ) ) ) )
27 12 3ad2ant3 
 |-  ( ( -u B e. NN0 /\ B e. RR /\ A e. NN ) -> A e. RR )
28 nnge1 
 |-  ( A e. NN -> 1 <_ A )
29 28 3ad2ant3 
 |-  ( ( -u B e. NN0 /\ B e. RR /\ A e. NN ) -> 1 <_ A )
30 27 8 29 expge1d 
 |-  ( ( -u B e. NN0 /\ B e. RR /\ A e. NN ) -> 1 <_ ( A ^ -u B ) )
31 1red 
 |-  ( ( -u B e. NN0 /\ B e. RR /\ A e. NN ) -> 1 e. RR )
32 15 3adant2 
 |-  ( ( -u B e. NN0 /\ B e. RR /\ A e. NN ) -> ( A ^ -u B ) e. RR )
33 31 32 lenltd 
 |-  ( ( -u B e. NN0 /\ B e. RR /\ A e. NN ) -> ( 1 <_ ( A ^ -u B ) <-> -. ( A ^ -u B ) < 1 ) )
34 pm2.21 
 |-  ( -. ( A ^ -u B ) < 1 -> ( ( A ^ -u B ) < 1 -> B e. NN ) )
35 33 34 syl6bi 
 |-  ( ( -u B e. NN0 /\ B e. RR /\ A e. NN ) -> ( 1 <_ ( A ^ -u B ) -> ( ( A ^ -u B ) < 1 -> B e. NN ) ) )
36 30 35 mpd 
 |-  ( ( -u B e. NN0 /\ B e. RR /\ A e. NN ) -> ( ( A ^ -u B ) < 1 -> B e. NN ) )
37 26 36 sylbird 
 |-  ( ( -u B e. NN0 /\ B e. RR /\ A e. NN ) -> ( 1 < ( 1 / ( A ^ -u B ) ) -> B e. NN ) )
38 11 37 sylbid 
 |-  ( ( -u B e. NN0 /\ B e. RR /\ A e. NN ) -> ( 1 < ( A ^ B ) -> B e. NN ) )
39 38 3exp 
 |-  ( -u B e. NN0 -> ( B e. RR -> ( A e. NN -> ( 1 < ( A ^ B ) -> B e. NN ) ) ) )
40 3 39 jaoi 
 |-  ( ( B e. NN \/ -u B e. NN0 ) -> ( B e. RR -> ( A e. NN -> ( 1 < ( A ^ B ) -> B e. NN ) ) ) )
41 40 impcom 
 |-  ( ( B e. RR /\ ( B e. NN \/ -u B e. NN0 ) ) -> ( A e. NN -> ( 1 < ( A ^ B ) -> B e. NN ) ) )
42 1 41 sylbi 
 |-  ( B e. ZZ -> ( A e. NN -> ( 1 < ( A ^ B ) -> B e. NN ) ) )
43 42 3imp21 
 |-  ( ( A e. NN /\ B e. ZZ /\ 1 < ( A ^ B ) ) -> B e. NN )