Theorem elshl ≪ | index | src | ≫ 

theorem elshl (a b c: nat): $ a e. shl b c <-> c <= a /\ a - c e. b $;
StepHypRefExpression
1 bitr 
(a e. shl b c <-> odd (shr (shl b c) a)) -> (odd (shr (shl b c) a) <-> c <= a /\ a - c e. b) -> (a e. shl b c <-> c <= a /\ a - c e. b)
2 elnel 
a e. shl b c <-> odd (shr (shl b c) a)
3 1, 2 ax_mp 
(odd (shr (shl b c) a) <-> c <= a /\ a - c e. b) -> (a e. shl b c <-> c <= a /\ a - c e. b)
4 odddvd 
odd (shr (shl b c) a) <-> ~2 || shr (shl b c) a
5 con1 
(~c <= a -> 2 || shr (shl b c) a) -> ~2 || shr (shl b c) a -> c <= a
6 ltnle 
a < c <-> ~c <= a
7 ltle 
a < c -> a <= c
8 shrshl1 
a <= c -> shr (shl b c) a = shl b (c - a)
9 7, 8 rsyl 
a < c -> shr (shl b c) a = shl b (c - a)
10 9 dvdeq2d 
a < c -> (2 || shr (shl b c) a <-> 2 || shl b (c - a))
11 subpos 
a < c <-> 0 < c - a
12 shl2dvd 
0 < c - a -> 2 || shl b (c - a)
13 11, 12 sylbi 
a < c -> 2 || shl b (c - a)
14 10, 13 mpbird 
a < c -> 2 || shr (shl b c) a
15 6, 14 sylbir 
~c <= a -> 2 || shr (shl b c) a
16 5, 15 ax_mp 
~2 || shr (shl b c) a -> c <= a
17 4, 16 sylbi 
odd (shr (shl b c) a) -> c <= a
18 anl 
c <= a /\ a - c e. b -> c <= a
19 elnel 
a - c e. b <-> odd (shr b (a - c))
20 shrshl2 
c <= a -> shr (shl b c) a = shr b (a - c)
21 20 oddeqd 
c <= a -> (odd (shr (shl b c) a) <-> odd (shr b (a - c)))
22 19, 21 syl6bbr 
c <= a -> (odd (shr (shl b c) a) <-> a - c e. b)
23 bian1 
c <= a -> (c <= a /\ a - c e. b <-> a - c e. b)
24 22, 23 bitr4d 
c <= a -> (odd (shr (shl b c) a) <-> c <= a /\ a - c e. b)
25 17, 18, 24 rbid 
odd (shr (shl b c) a) <-> c <= a /\ a - c e. b
26 3, 25 ax_mp 
a e. shl b c <-> c <= a /\ a - c e. 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)