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

Metamath Proof Explorer

Theorem expeqidd

Description: A nonnegative real number is zero or one if and only if it is itself when raised to an integer greater than one. (Contributed by SN, 3-Jul-2025)

Ref Expression
Hypotheses expeqidd.a 
|- ( ph -> A e. RR )
expeqidd.n 
|- ( ph -> N e. ( ZZ>= ` 2 ) )
expeqidd.0 
|- ( ph -> 0 <_ A )
Assertion expeqidd 
|- ( ph -> ( ( A ^ N ) = A <-> ( A = 0 \/ A = 1 ) ) )

Proof

Step Hyp Ref Expression
1 expeqidd.a 
 |-  ( ph -> A e. RR )
2 expeqidd.n 
 |-  ( ph -> N e. ( ZZ>= ` 2 ) )
3 expeqidd.0 
 |-  ( ph -> 0 <_ A )
4 df-ne 
 |-  ( A =/= 0 <-> -. A = 0 )
5 1 recnd 
 |-  ( ph -> A e. CC )
6 5 ad2antrr 
 |-  ( ( ( ph /\ A =/= 0 ) /\ ( A ^ N ) = A ) -> A e. CC )
7 simplr 
 |-  ( ( ( ph /\ A =/= 0 ) /\ ( A ^ N ) = A ) -> A =/= 0 )
8 eluz2nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN )
9 2 8 syl 
 |-  ( ph -> N e. NN )
10 9 nnzd 
 |-  ( ph -> N e. ZZ )
11 10 ad2antrr 
 |-  ( ( ( ph /\ A =/= 0 ) /\ ( A ^ N ) = A ) -> N e. ZZ )
12 6 7 11 expm1d 
 |-  ( ( ( ph /\ A =/= 0 ) /\ ( A ^ N ) = A ) -> ( A ^ ( N - 1 ) ) = ( ( A ^ N ) / A ) )
13 simpr 
 |-  ( ( ( ph /\ A =/= 0 ) /\ ( A ^ N ) = A ) -> ( A ^ N ) = A )
14 13 oveq1d 
 |-  ( ( ( ph /\ A =/= 0 ) /\ ( A ^ N ) = A ) -> ( ( A ^ N ) / A ) = ( A / A ) )
15 6 7 dividd 
 |-  ( ( ( ph /\ A =/= 0 ) /\ ( A ^ N ) = A ) -> ( A / A ) = 1 )
16 12 14 15 3eqtrd 
 |-  ( ( ( ph /\ A =/= 0 ) /\ ( A ^ N ) = A ) -> ( A ^ ( N - 1 ) ) = 1 )
17 1 adantr 
 |-  ( ( ph /\ A =/= 0 ) -> A e. RR )
18 uz2m1nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N - 1 ) e. NN )
19 2 18 syl 
 |-  ( ph -> ( N - 1 ) e. NN )
20 19 adantr 
 |-  ( ( ph /\ A =/= 0 ) -> ( N - 1 ) e. NN )
21 3 adantr 
 |-  ( ( ph /\ A =/= 0 ) -> 0 <_ A )
22 17 20 21 expeq1d 
 |-  ( ( ph /\ A =/= 0 ) -> ( ( A ^ ( N - 1 ) ) = 1 <-> A = 1 ) )
23 22 biimpa 
 |-  ( ( ( ph /\ A =/= 0 ) /\ ( A ^ ( N - 1 ) ) = 1 ) -> A = 1 )
24 16 23 syldan 
 |-  ( ( ( ph /\ A =/= 0 ) /\ ( A ^ N ) = A ) -> A = 1 )
25 24 an32s 
 |-  ( ( ( ph /\ ( A ^ N ) = A ) /\ A =/= 0 ) -> A = 1 )
26 25 ex 
 |-  ( ( ph /\ ( A ^ N ) = A ) -> ( A =/= 0 -> A = 1 ) )
27 4 26 biimtrrid 
 |-  ( ( ph /\ ( A ^ N ) = A ) -> ( -. A = 0 -> A = 1 ) )
28 27 orrd 
 |-  ( ( ph /\ ( A ^ N ) = A ) -> ( A = 0 \/ A = 1 ) )
29 28 ex 
 |-  ( ph -> ( ( A ^ N ) = A -> ( A = 0 \/ A = 1 ) ) )
30 9 0expd 
 |-  ( ph -> ( 0 ^ N ) = 0 )
31 oveq1 
 |-  ( A = 0 -> ( A ^ N ) = ( 0 ^ N ) )
32 id 
 |-  ( A = 0 -> A = 0 )
33 31 32 eqeq12d 
 |-  ( A = 0 -> ( ( A ^ N ) = A <-> ( 0 ^ N ) = 0 ) )
34 30 33 syl5ibrcom 
 |-  ( ph -> ( A = 0 -> ( A ^ N ) = A ) )
35 1exp 
 |-  ( N e. ZZ -> ( 1 ^ N ) = 1 )
36 10 35 syl 
 |-  ( ph -> ( 1 ^ N ) = 1 )
37 oveq1 
 |-  ( A = 1 -> ( A ^ N ) = ( 1 ^ N ) )
38 id 
 |-  ( A = 1 -> A = 1 )
39 37 38 eqeq12d 
 |-  ( A = 1 -> ( ( A ^ N ) = A <-> ( 1 ^ N ) = 1 ) )
40 36 39 syl5ibrcom 
 |-  ( ph -> ( A = 1 -> ( A ^ N ) = A ) )
41 34 40 jaod 
 |-  ( ph -> ( ( A = 0 \/ A = 1 ) -> ( A ^ N ) = A ) )
42 29 41 impbid 
 |-  ( ph -> ( ( A ^ N ) = A <-> ( A = 0 \/ A = 1 ) ) )