Theorem shrmodadd1 | index | src |

theorem shrmodadd1 (a b c: nat): $ shr (a % 2 ^ (b + c)) b = shr a b % 2 ^ c $;
StepHypRefExpression
1 eqtr4
shr (a % 2 ^ (b + c)) b = shr (a % (2 ^ b * 2 ^ c)) b -> shr a b % 2 ^ c = shr (a % (2 ^ b * 2 ^ c)) b -> shr (a % 2 ^ (b + c)) b = shr a b % 2 ^ c
2 shreq1
a % 2 ^ (b + c) = a % (2 ^ b * 2 ^ c) -> shr (a % 2 ^ (b + c)) b = shr (a % (2 ^ b * 2 ^ c)) b
3 modeq2
2 ^ (b + c) = 2 ^ b * 2 ^ c -> a % 2 ^ (b + c) = a % (2 ^ b * 2 ^ c)
4 powadd
2 ^ (b + c) = 2 ^ b * 2 ^ c
5 3, 4 ax_mp
a % 2 ^ (b + c) = a % (2 ^ b * 2 ^ c)
6 2, 5 ax_mp
shr (a % 2 ^ (b + c)) b = shr (a % (2 ^ b * 2 ^ c)) b
7 1, 6 ax_mp
shr a b % 2 ^ c = shr (a % (2 ^ b * 2 ^ c)) b -> shr (a % 2 ^ (b + c)) b = shr a b % 2 ^ c
8 divmod1
a // 2 ^ b % 2 ^ c = a % (2 ^ b * 2 ^ c) // 2 ^ b
9 8 conv shr
shr a b % 2 ^ c = shr (a % (2 ^ b * 2 ^ c)) b
10 7, 9 ax_mp
shr (a % 2 ^ (b + c)) b = shr a b % 2 ^ c

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)