Metamath Proof Explorer


Theorem expeq0

Description: Positive integer exponentiation is 0 iff its base 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 ) )