Theorem elpow2 | index | src |

theorem elpow2 (a n: nat): $ a e. 2 ^ n <-> a = n $;
StepHypRefExpression
1 bitr3
(a e. shl 1 n <-> a e. 2 ^ n) -> (a e. shl 1 n <-> a = n) -> (a e. 2 ^ n <-> a = n)
2 elneq2
shl 1 n = 2 ^ n -> (a e. shl 1 n <-> a e. 2 ^ n)
3 shl11
shl 1 n = 2 ^ n
4 2, 3 ax_mp
a e. shl 1 n <-> a e. 2 ^ n
5 1, 4 ax_mp
(a e. shl 1 n <-> a = n) -> (a e. 2 ^ n <-> a = n)
6 bitr
(a e. shl 1 n <-> n <= a /\ a - n e. 1) -> (n <= a /\ a - n e. 1 <-> a = n) -> (a e. shl 1 n <-> a = n)
7 elshl
a e. shl 1 n <-> n <= a /\ a - n e. 1
8 6, 7 ax_mp
(n <= a /\ a - n e. 1 <-> a = n) -> (a e. shl 1 n <-> a = n)
9 bitr4
(n <= a /\ a - n e. 1 <-> n <= a /\ a <= n) -> (a = n <-> n <= a /\ a <= n) -> (n <= a /\ a - n e. 1 <-> a = n)
10 bitr4
(a - n e. 1 <-> a - n = 0) -> (a <= n <-> a - n = 0) -> (a - n e. 1 <-> a <= n)
11 el12
a - n e. 1 <-> a - n = 0
12 10, 11 ax_mp
(a <= n <-> a - n = 0) -> (a - n e. 1 <-> a <= n)
13 lesubeq0
a <= n <-> a - n = 0
14 12, 13 ax_mp
a - n e. 1 <-> a <= n
15 14 aneq2i
n <= a /\ a - n e. 1 <-> n <= a /\ a <= n
16 9, 15 ax_mp
(a = n <-> n <= a /\ a <= n) -> (n <= a /\ a - n e. 1 <-> a = n)
17 bitr
(a = n <-> n = a) -> (n = a <-> n <= a /\ a <= n) -> (a = n <-> n <= a /\ a <= n)
18 eqcomb
a = n <-> n = a
19 17, 18 ax_mp
(n = a <-> n <= a /\ a <= n) -> (a = n <-> n <= a /\ a <= n)
20 eqlele
n = a <-> n <= a /\ a <= n
21 19, 20 ax_mp
a = n <-> n <= a /\ a <= n
22 16, 21 ax_mp
n <= a /\ a - n e. 1 <-> a = n
23 8, 22 ax_mp
a e. shl 1 n <-> a = n
24 5, 23 ax_mp
a e. 2 ^ n <-> a = n

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)