Metamath Proof Explorer

Theorem expeq1d

Description: A nonnegative real number is one if and only if it is one when raised to a positive integer. (Contributed by SN, 3-Jul-2025)

Ref Expression
Hypotheses expeq1d.a 
|- ( ph -> A e. RR )
expeq1d.n 
|- ( ph -> N e. NN )
expeq1d.0 
|- ( ph -> 0 <_ A )
Assertion expeq1d 
|- ( ph -> ( ( A ^ N ) = 1 <-> A = 1 ) )

Proof

Step Hyp Ref Expression
1 expeq1d.a 
 |-  ( ph -> A e. RR )
2 expeq1d.n 
 |-  ( ph -> N e. NN )
3 expeq1d.0 
 |-  ( ph -> 0 <_ A )
4 2 nnzd 
 |-  ( ph -> N e. ZZ )
5 1exp 
 |-  ( N e. ZZ -> ( 1 ^ N ) = 1 )
6 4 5 syl 
 |-  ( ph -> ( 1 ^ N ) = 1 )
7 6 eqeq2d 
 |-  ( ph -> ( ( A ^ N ) = ( 1 ^ N ) <-> ( A ^ N ) = 1 ) )
8 1 adantr 
 |-  ( ( ph /\ ( A ^ N ) = ( 1 ^ N ) ) -> A e. RR )
9 3 adantr 
 |-  ( ( ph /\ ( A ^ N ) = ( 1 ^ N ) ) -> 0 <_ A )
10 0ne1 
 |-  0 =/= 1
11 10 a1i 
 |-  ( ph -> 0 =/= 1 )
12 2 0expd 
 |-  ( ph -> ( 0 ^ N ) = 0 )
13 11 12 6 3netr4d 
 |-  ( ph -> ( 0 ^ N ) =/= ( 1 ^ N ) )
14 13 adantr 
 |-  ( ( ph /\ ( A ^ N ) = ( 1 ^ N ) ) -> ( 0 ^ N ) =/= ( 1 ^ N ) )
15 oveq1 
 |-  ( A = 0 -> ( A ^ N ) = ( 0 ^ N ) )
16 15 eqeq1d 
 |-  ( A = 0 -> ( ( A ^ N ) = ( 1 ^ N ) <-> ( 0 ^ N ) = ( 1 ^ N ) ) )
17 16 biimpac 
 |-  ( ( ( A ^ N ) = ( 1 ^ N ) /\ A = 0 ) -> ( 0 ^ N ) = ( 1 ^ N ) )
18 17 adantll 
 |-  ( ( ( ph /\ ( A ^ N ) = ( 1 ^ N ) ) /\ A = 0 ) -> ( 0 ^ N ) = ( 1 ^ N ) )
19 14 18 mteqand 
 |-  ( ( ph /\ ( A ^ N ) = ( 1 ^ N ) ) -> A =/= 0 )
20 8 9 19 ne0gt0d 
 |-  ( ( ph /\ ( A ^ N ) = ( 1 ^ N ) ) -> 0 < A )
21 8 20 elrpd 
 |-  ( ( ph /\ ( A ^ N ) = ( 1 ^ N ) ) -> A e. RR+ )
22 1rp 
 |-  1 e. RR+
23 22 a1i 
 |-  ( ( ph /\ ( A ^ N ) = ( 1 ^ N ) ) -> 1 e. RR+ )
24 2 adantr 
 |-  ( ( ph /\ ( A ^ N ) = ( 1 ^ N ) ) -> N e. NN )
25 simpr 
 |-  ( ( ph /\ ( A ^ N ) = ( 1 ^ N ) ) -> ( A ^ N ) = ( 1 ^ N ) )
26 21 23 24 25 exp11nnd 
 |-  ( ( ph /\ ( A ^ N ) = ( 1 ^ N ) ) -> A = 1 )
27 26 ex 
 |-  ( ph -> ( ( A ^ N ) = ( 1 ^ N ) -> A = 1 ) )
28 7 27 sylbird 
 |-  ( ph -> ( ( A ^ N ) = 1 -> A = 1 ) )
29 oveq1 
 |-  ( A = 1 -> ( A ^ N ) = ( 1 ^ N ) )
30 29 eqeq1d 
 |-  ( A = 1 -> ( ( A ^ N ) = 1 <-> ( 1 ^ N ) = 1 ) )
31 6 30 syl5ibrcom 
 |-  ( ph -> ( A = 1 -> ( A ^ N ) = 1 ) )
32 28 31 impbid 
 |-  ( ph -> ( ( A ^ N ) = 1 <-> A = 1 ) )