Theorem powpos ≪ | index | src | ≫

theorem powpos (a b: nat): $ 0 < a -> 0 < a ^ b $;

Step	Hyp	Ref	Expression
1		id	_1 = b -> _1 = b
2	1	poweq2d	_1 = b -> a ^ _1 = a ^ b
3	2	lteq2d	_1 = b -> (0 < a ^ _1 <-> 0 < a ^ b)
4		id	_1 = 0 -> _1 = 0
5	4	poweq2d	_1 = 0 -> a ^ _1 = a ^ 0
6	5	lteq2d	_1 = 0 -> (0 < a ^ _1 <-> 0 < a ^ 0)
7		id	_1 = a1 -> _1 = a1
8	7	poweq2d	_1 = a1 -> a ^ _1 = a ^ a1
9	8	lteq2d	_1 = a1 -> (0 < a ^ _1 <-> 0 < a ^ a1)
10		id	_1 = suc a1 -> _1 = suc a1
11	10	poweq2d	_1 = suc a1 -> a ^ _1 = a ^ suc a1
12	11	lteq2d	_1 = suc a1 -> (0 < a ^ _1 <-> 0 < a ^ suc a1)
13		lteq2	a ^ 0 = 1 -> (0 < a ^ 0 <-> 0 < 1)
14		pow0	a ^ 0 = 1
15	13, 14	ax_mp	0 < a ^ 0 <-> 0 < 1
16		d0lt1	0 < 1
17	15, 16	mpbir	0 < a ^ 0
18	17	a1i	0 < a -> 0 < a ^ 0
19		lteq2	a ^ suc a1 = a * a ^ a1 -> (0 < a ^ suc a1 <-> 0 < a * a ^ a1)
20		powS	a ^ suc a1 = a * a ^ a1
21	19, 20	ax_mp	0 < a ^ suc a1 <-> 0 < a * a ^ a1
22		mulpos	0 < a * a ^ a1 <-> 0 < a /\ 0 < a ^ a1
23	22	bi2i	0 < a /\ 0 < a ^ a1 -> 0 < a * a ^ a1
24	21, 23	sylibr	0 < a /\ 0 < a ^ a1 -> 0 < a ^ suc a1
25	3, 6, 9, 12, 18, 24	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)