Theorem elshr | index | src |

theorem elshr (a b c: nat): $ a e. shr b c <-> a + c e. b $;
StepHypRefExpression
1 bitr
(a e. shr b c <-> odd (shr (shr b c) a)) -> (odd (shr (shr b c) a) <-> a + c e. b) -> (a e. shr b c <-> a + c e. b)
2 elnel
a e. shr b c <-> odd (shr (shr b c) a)
3 1, 2 ax_mp
(odd (shr (shr b c) a) <-> a + c e. b) -> (a e. shr b c <-> a + c e. b)
4 bitr4
(odd (shr (shr b c) a) <-> odd (shr b (a + c))) -> (a + c e. b <-> odd (shr b (a + c))) -> (odd (shr (shr b c) a) <-> a + c e. b)
5 oddeq
shr (shr b c) a = shr b (a + c) -> (odd (shr (shr b c) a) <-> odd (shr b (a + c)))
6 eqtr
shr (shr b c) a = shr b (c + a) -> shr b (c + a) = shr b (a + c) -> shr (shr b c) a = shr b (a + c)
7 shrshr
shr (shr b c) a = shr b (c + a)
8 6, 7 ax_mp
shr b (c + a) = shr b (a + c) -> shr (shr b c) a = shr b (a + c)
9 shreq2
c + a = a + c -> shr b (c + a) = shr b (a + c)
10 addcom
c + a = a + c
11 9, 10 ax_mp
shr b (c + a) = shr b (a + c)
12 8, 11 ax_mp
shr (shr b c) a = shr b (a + c)
13 5, 12 ax_mp
odd (shr (shr b c) a) <-> odd (shr b (a + c))
14 4, 13 ax_mp
(a + c e. b <-> odd (shr b (a + c))) -> (odd (shr (shr b c) a) <-> a + c e. b)
15 elnel
a + c e. b <-> odd (shr b (a + c))
16 14, 15 ax_mp
odd (shr (shr b c) a) <-> a + c e. b
17 3, 16 ax_mp
a e. shr b c <-> 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)