Theorem powpos ≪ | index | src | ≫ 

theorem powpos (a b: nat): $ 0 < a -> 0 < a ^ b $;
StepHypRefExpression
1 eqidd 
_1 = b -> 0 = 0
2 eqidd 
_1 = b -> a = a
3 id 
_1 = b -> _1 = b
4 2, 3 poweqd 
_1 = b -> a ^ _1 = a ^ b
5 1, 4 lteqd 
_1 = b -> (0 < a ^ _1 <-> 0 < a ^ b)
6 eqidd 
_1 = 0 -> 0 = 0
7 eqidd 
_1 = 0 -> a = a
8 id 
_1 = 0 -> _1 = 0
9 7, 8 poweqd 
_1 = 0 -> a ^ _1 = a ^ 0
10 6, 9 lteqd 
_1 = 0 -> (0 < a ^ _1 <-> 0 < a ^ 0)
11 eqidd 
_1 = a1 -> 0 = 0
12 eqidd 
_1 = a1 -> a = a
13 id 
_1 = a1 -> _1 = a1
14 12, 13 poweqd 
_1 = a1 -> a ^ _1 = a ^ a1
15 11, 14 lteqd 
_1 = a1 -> (0 < a ^ _1 <-> 0 < a ^ a1)
16 eqidd 
_1 = suc a1 -> 0 = 0
17 eqidd 
_1 = suc a1 -> a = a
18 id 
_1 = suc a1 -> _1 = suc a1
19 17, 18 poweqd 
_1 = suc a1 -> a ^ _1 = a ^ suc a1
20 16, 19 lteqd 
_1 = suc a1 -> (0 < a ^ _1 <-> 0 < a ^ suc a1)
21 lteq2 
a ^ 0 = 1 -> (0 < a ^ 0 <-> 0 < 1)
22 pow0 
a ^ 0 = 1
23 21, 22 ax_mp 
0 < a ^ 0 <-> 0 < 1
24 d0lt1 
0 < 1
25 23, 24 mpbir 
0 < a ^ 0
26 25 a1i 
0 < a -> 0 < a ^ 0
27 lteq2 
a ^ suc a1 = a * a ^ a1 -> (0 < a ^ suc a1 <-> 0 < a * a ^ a1)
28 powS 
a ^ suc a1 = a * a ^ a1
29 27, 28 ax_mp 
0 < a ^ suc a1 <-> 0 < a * a ^ a1
30 mulpos 
0 < a * a ^ a1 <-> 0 < a /\ 0 < a ^ a1
31 30 bi2i 
0 < a /\ 0 < a ^ a1 -> 0 < a * a ^ a1
32 29, 31 sylibr 
0 < a /\ 0 < a ^ a1 -> 0 < a ^ suc a1
33 5, 10, 15, 20, 26, 32 indd 
0 < a -> 0 < a ^ b

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)