Theorem elmodpow2 ≪ | index | src | ≫ 

theorem elmodpow2 (a n x: nat): $ x e. a % 2 ^ n <-> x < n /\ x e. a $;
StepHypRefExpression
1 bitr 
(x e. a % 2 ^ n <-> odd (shr (a % 2 ^ n) x)) -> (odd (shr (a % 2 ^ n) x) <-> x < n /\ x e. a) -> (x e. a % 2 ^ n <-> x < n /\ x e. a)
2 elnel 
x e. a % 2 ^ n <-> odd (shr (a % 2 ^ n) x)
3 1, 2 ax_mp 
(odd (shr (a % 2 ^ n) x) <-> x < n /\ x e. a) -> (x e. a % 2 ^ n <-> x < n /\ x e. a)
4 bitr3 
(x < n /\ odd (shr (a % 2 ^ n) x) <-> odd (shr (a % 2 ^ n) x)) ->
  (x < n /\ odd (shr (a % 2 ^ n) x) <-> x < n /\ x e. a) ->
  (odd (shr (a % 2 ^ n) x) <-> x < n /\ x e. a)
5 bian1a 
(odd (shr (a % 2 ^ n) x) -> x < n) -> (x < n /\ odd (shr (a % 2 ^ n) x) <-> odd (shr (a % 2 ^ n) x))
6 ax_3 
(~x < n -> ~odd (shr (a % 2 ^ n) x)) -> odd (shr (a % 2 ^ n) x) -> x < n
7 lenlt 
n <= x <-> ~x < n
8 odd0 
~odd 0
9 shreq0 
shr (a % 2 ^ n) x = 0 <-> a % 2 ^ n < 2 ^ x
10 ltletr 
a % 2 ^ n < 2 ^ n -> 2 ^ n <= 2 ^ x -> a % 2 ^ n < 2 ^ x
11 modlt 
2 ^ n != 0 -> a % 2 ^ n < 2 ^ n
12 pow2ne0 
2 ^ n != 0
13 11, 12 ax_mp 
a % 2 ^ n < 2 ^ n
14 10, 13 ax_mp 
2 ^ n <= 2 ^ x -> a % 2 ^ n < 2 ^ x
15 lepow2a 
2 != 0 -> n <= x -> 2 ^ n <= 2 ^ x
16 d2ne0 
2 != 0
17 15, 16 ax_mp 
n <= x -> 2 ^ n <= 2 ^ x
18 14, 17 syl 
n <= x -> a % 2 ^ n < 2 ^ x
19 9, 18 sylibr 
n <= x -> shr (a % 2 ^ n) x = 0
20 19 oddeqd 
n <= x -> (odd (shr (a % 2 ^ n) x) <-> odd 0)
21 20 noteqd 
n <= x -> (~odd (shr (a % 2 ^ n) x) <-> ~odd 0)
22 8, 21 mpbiri 
n <= x -> ~odd (shr (a % 2 ^ n) x)
23 7, 22 sylbir 
~x < n -> ~odd (shr (a % 2 ^ n) x)
24 6, 23 ax_mp 
odd (shr (a % 2 ^ n) x) -> x < n
25 5, 24 ax_mp 
x < n /\ odd (shr (a % 2 ^ n) x) <-> odd (shr (a % 2 ^ n) x)
26 4, 25 ax_mp 
(x < n /\ odd (shr (a % 2 ^ n) x) <-> x < n /\ x e. a) -> (odd (shr (a % 2 ^ n) x) <-> x < n /\ x e. a)
27 aneq2a 
(x < n -> (odd (shr (a % 2 ^ n) x) <-> x e. a)) -> (x < n /\ odd (shr (a % 2 ^ n) x) <-> x < n /\ x e. a)
28 elnel 
x e. a <-> odd (shr a x)
29 odddvd 
odd (shr (a % 2 ^ n) x) <-> ~2 || shr (a % 2 ^ n) x
30 odddvd 
odd (shr a x) <-> ~2 || shr a x
31 eqmdvd 
mod(2): shr (a % 2 ^ n) x = shr a x -> (2 || shr (a % 2 ^ n) x <-> 2 || shr a x)
32 shrmodsub 
x <= n -> shr (a % 2 ^ n) x = shr a x % 2 ^ (n - x)
33 ltle 
x < n -> x <= n
34 32, 33 syl 
x < n -> shr (a % 2 ^ n) x = shr a x % 2 ^ (n - x)
35 34 eqmeq2d 
x < n -> (mod(2): shr (a % 2 ^ n) x = shr a x <-> mod(2): shr a x % 2 ^ (n - x) = shr a x)
36 subpos 
x < n <-> 0 < n - x
37 powdvd1 
0 < n - x -> 2 || 2 ^ (n - x)
38 36, 37 sylbi 
x < n -> 2 || 2 ^ (n - x)
39 eqmmod 
mod(2 ^ (n - x)): shr a x % 2 ^ (n - x) = shr a x
40 39 a1i 
x < n -> mod(2 ^ (n - x)): shr a x % 2 ^ (n - x) = shr a x
41 38, 40 dvdeqm 
x < n -> mod(2): shr a x % 2 ^ (n - x) = shr a x
42 35, 41 mpbird 
x < n -> mod(2): shr (a % 2 ^ n) x = shr a x
43 31, 42 syl 
x < n -> (2 || shr (a % 2 ^ n) x <-> 2 || shr a x)
44 43 noteqd 
x < n -> (~2 || shr (a % 2 ^ n) x <-> ~2 || shr a x)
45 29, 30, 44 bitr4g 
x < n -> (odd (shr (a % 2 ^ n) x) <-> odd (shr a x))
46 28, 45 syl6bbr 
x < n -> (odd (shr (a % 2 ^ n) x) <-> x e. a)
47 27, 46 ax_mp 
x < n /\ odd (shr (a % 2 ^ n) x) <-> x < n /\ x e. a
48 26, 47 ax_mp 
odd (shr (a % 2 ^ n) x) <-> x < n /\ x e. a
49 3, 48 ax_mp 
x e. a % 2 ^ n <-> x < n /\ x e. a

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)