Metamath Proof Explorer

Theorem expeq0

Description: Positive integer exponentiation is 0 iff its mantissa is 0. (Contributed by NM, 23-Feb-2005)

Ref Expression
Assertion expeq0 
|- ( ( A e. CC /\ N e. NN ) -> ( ( A ^ N ) = 0 <-> A = 0 ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( j = 1 -> ( A ^ j ) = ( A ^ 1 ) )
2 1 eqeq1d 
 |-  ( j = 1 -> ( ( A ^ j ) = 0 <-> ( A ^ 1 ) = 0 ) )
3 2 bibi1d 
 |-  ( j = 1 -> ( ( ( A ^ j ) = 0 <-> A = 0 ) <-> ( ( A ^ 1 ) = 0 <-> A = 0 ) ) )
4 3 imbi2d 
 |-  ( j = 1 -> ( ( A e. CC -> ( ( A ^ j ) = 0 <-> A = 0 ) ) <-> ( A e. CC -> ( ( A ^ 1 ) = 0 <-> A = 0 ) ) ) )
5 oveq2 
 |-  ( j = k -> ( A ^ j ) = ( A ^ k ) )
6 5 eqeq1d 
 |-  ( j = k -> ( ( A ^ j ) = 0 <-> ( A ^ k ) = 0 ) )
7 6 bibi1d 
 |-  ( j = k -> ( ( ( A ^ j ) = 0 <-> A = 0 ) <-> ( ( A ^ k ) = 0 <-> A = 0 ) ) )
8 7 imbi2d 
 |-  ( j = k -> ( ( A e. CC -> ( ( A ^ j ) = 0 <-> A = 0 ) ) <-> ( A e. CC -> ( ( A ^ k ) = 0 <-> A = 0 ) ) ) )
9 oveq2 
 |-  ( j = ( k + 1 ) -> ( A ^ j ) = ( A ^ ( k + 1 ) ) )
10 9 eqeq1d 
 |-  ( j = ( k + 1 ) -> ( ( A ^ j ) = 0 <-> ( A ^ ( k + 1 ) ) = 0 ) )
11 10 bibi1d 
 |-  ( j = ( k + 1 ) -> ( ( ( A ^ j ) = 0 <-> A = 0 ) <-> ( ( A ^ ( k + 1 ) ) = 0 <-> A = 0 ) ) )
12 11 imbi2d 
 |-  ( j = ( k + 1 ) -> ( ( A e. CC -> ( ( A ^ j ) = 0 <-> A = 0 ) ) <-> ( A e. CC -> ( ( A ^ ( k + 1 ) ) = 0 <-> A = 0 ) ) ) )
13 oveq2 
 |-  ( j = N -> ( A ^ j ) = ( A ^ N ) )
14 13 eqeq1d 
 |-  ( j = N -> ( ( A ^ j ) = 0 <-> ( A ^ N ) = 0 ) )
15 14 bibi1d 
 |-  ( j = N -> ( ( ( A ^ j ) = 0 <-> A = 0 ) <-> ( ( A ^ N ) = 0 <-> A = 0 ) ) )
16 15 imbi2d 
 |-  ( j = N -> ( ( A e. CC -> ( ( A ^ j ) = 0 <-> A = 0 ) ) <-> ( A e. CC -> ( ( A ^ N ) = 0 <-> A = 0 ) ) ) )
17 exp1 
 |-  ( A e. CC -> ( A ^ 1 ) = A )
18 17 eqeq1d 
 |-  ( A e. CC -> ( ( A ^ 1 ) = 0 <-> A = 0 ) )
19 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
20 expp1 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( A ^ ( k + 1 ) ) = ( ( A ^ k ) x. A ) )
21 20 eqeq1d 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( ( A ^ ( k + 1 ) ) = 0 <-> ( ( A ^ k ) x. A ) = 0 ) )
22 expcl 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( A ^ k ) e. CC )
23 simpl 
 |-  ( ( A e. CC /\ k e. NN0 ) -> A e. CC )
24 22 23 mul0ord 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( ( ( A ^ k ) x. A ) = 0 <-> ( ( A ^ k ) = 0 \/ A = 0 ) ) )
25 21 24 bitrd 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( ( A ^ ( k + 1 ) ) = 0 <-> ( ( A ^ k ) = 0 \/ A = 0 ) ) )
26 19 25 sylan2 
 |-  ( ( A e. CC /\ k e. NN ) -> ( ( A ^ ( k + 1 ) ) = 0 <-> ( ( A ^ k ) = 0 \/ A = 0 ) ) )
27 biimp 
 |-  ( ( ( A ^ k ) = 0 <-> A = 0 ) -> ( ( A ^ k ) = 0 -> A = 0 ) )
28 idd 
 |-  ( ( ( A ^ k ) = 0 <-> A = 0 ) -> ( A = 0 -> A = 0 ) )
29 27 28 jaod 
 |-  ( ( ( A ^ k ) = 0 <-> A = 0 ) -> ( ( ( A ^ k ) = 0 \/ A = 0 ) -> A = 0 ) )
30 olc 
 |-  ( A = 0 -> ( ( A ^ k ) = 0 \/ A = 0 ) )
31 29 30 impbid1 
 |-  ( ( ( A ^ k ) = 0 <-> A = 0 ) -> ( ( ( A ^ k ) = 0 \/ A = 0 ) <-> A = 0 ) )
32 26 31 sylan9bb 
 |-  ( ( ( A e. CC /\ k e. NN ) /\ ( ( A ^ k ) = 0 <-> A = 0 ) ) -> ( ( A ^ ( k + 1 ) ) = 0 <-> A = 0 ) )
33 32 exp31 
 |-  ( A e. CC -> ( k e. NN -> ( ( ( A ^ k ) = 0 <-> A = 0 ) -> ( ( A ^ ( k + 1 ) ) = 0 <-> A = 0 ) ) ) )
34 33 com12 
 |-  ( k e. NN -> ( A e. CC -> ( ( ( A ^ k ) = 0 <-> A = 0 ) -> ( ( A ^ ( k + 1 ) ) = 0 <-> A = 0 ) ) ) )
35 34 a2d 
 |-  ( k e. NN -> ( ( A e. CC -> ( ( A ^ k ) = 0 <-> A = 0 ) ) -> ( A e. CC -> ( ( A ^ ( k + 1 ) ) = 0 <-> A = 0 ) ) ) )
36 4 8 12 16 18 35 nnind 
 |-  ( N e. NN -> ( A e. CC -> ( ( A ^ N ) = 0 <-> A = 0 ) ) )
37 36 impcom 
 |-  ( ( A e. CC /\ N e. NN ) -> ( ( A ^ N ) = 0 <-> A = 0 ) )