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 N 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 A j = 0 A = 0 A 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 A j = 0 A = 0 A 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 A j = 0 A = 0 A 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 A j = 0 A = 0 A A N = 0 A = 0
17 exp1 A A 1 = A
18 17 eqeq1d A A 1 = 0 A = 0
19 nnnn0 k k 0
20 expp1 A k 0 A k + 1 = A k A
21 20 eqeq1d A k 0 A k + 1 = 0 A k A = 0
22 expcl A k 0 A k
23 simpl A k 0 A
24 22 23 mul0ord A k 0 A k A = 0 A k = 0 A = 0
25 21 24 bitrd A k 0 A k + 1 = 0 A k = 0 A = 0
26 19 25 sylan2 A k 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 k A k = 0 A = 0 A k + 1 = 0 A = 0
33 32 exp31 A k A k = 0 A = 0 A k + 1 = 0 A = 0
34 33 com12 k A A k = 0 A = 0 A k + 1 = 0 A = 0
35 34 a2d k A A k = 0 A = 0 A A k + 1 = 0 A = 0
36 4 8 12 16 18 35 nnind N A A N = 0 A = 0
37 36 impcom A N A N = 0 A = 0