Metamath Proof Explorer

Theorem expnngt1b

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

Ref Expression
Assertion expnngt1b 
|- ( ( A e. ( ZZ>= ` 2 ) /\ B e. ZZ ) -> ( 1 < ( A ^ B ) <-> B e. NN ) )

Proof

Step Hyp Ref Expression
1 eluz2nn 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. NN )
2 1 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ B e. ZZ ) -> A e. NN )
3 2 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. ZZ ) /\ 1 < ( A ^ B ) ) -> A e. NN )
4 simplr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. ZZ ) /\ 1 < ( A ^ B ) ) -> B e. ZZ )
5 simpr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. ZZ ) /\ 1 < ( A ^ B ) ) -> 1 < ( A ^ B ) )
6 expnngt1 
 |-  ( ( A e. NN /\ B e. ZZ /\ 1 < ( A ^ B ) ) -> B e. NN )
7 3 4 5 6 syl3anc 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. ZZ ) /\ 1 < ( A ^ B ) ) -> B e. NN )
8 2 nnred 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ B e. ZZ ) -> A e. RR )
9 8 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. ZZ ) /\ B e. NN ) -> A e. RR )
10 simpr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. ZZ ) /\ B e. NN ) -> B e. NN )
11 eluz2gt1 
 |-  ( A e. ( ZZ>= ` 2 ) -> 1 < A )
12 11 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ B e. ZZ ) -> 1 < A )
13 12 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. ZZ ) /\ B e. NN ) -> 1 < A )
14 expgt1 
 |-  ( ( A e. RR /\ B e. NN /\ 1 < A ) -> 1 < ( A ^ B ) )
15 9 10 13 14 syl3anc 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. ZZ ) /\ B e. NN ) -> 1 < ( A ^ B ) )
16 7 15 impbida 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ B e. ZZ ) -> ( 1 < ( A ^ B ) <-> B e. NN ) )