theorem powne0 (a b: nat): $ a != 0 -> a ^ b != 0 $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | lt01 | 0 < a <-> a != 0 |
|
| 2 | lt01 | 0 < a ^ b <-> a ^ b != 0 |
|
| 3 | powpos | 0 < a -> 0 < a ^ b |
|
| 4 | 2, 3 | sylib | 0 < a -> a ^ b != 0 |
| 5 | 1, 4 | sylbir | a != 0 -> a ^ b != 0 |