Theorem shrmodadd2 | index | src |

theorem shrmodadd2 (a b c: nat): $ shr (a % 2 ^ (b + c)) c = shr a c % 2 ^ b $;
StepHypRefExpression
1 eqtr
shr (a % 2 ^ (b + c)) c = shr (a % 2 ^ (c + b)) c -> shr (a % 2 ^ (c + b)) c = shr a c % 2 ^ b -> shr (a % 2 ^ (b + c)) c = shr a c % 2 ^ b
2 shreq1
a % 2 ^ (b + c) = a % 2 ^ (c + b) -> shr (a % 2 ^ (b + c)) c = shr (a % 2 ^ (c + b)) c
3 modeq2
2 ^ (b + c) = 2 ^ (c + b) -> a % 2 ^ (b + c) = a % 2 ^ (c + b)
4 poweq2
b + c = c + b -> 2 ^ (b + c) = 2 ^ (c + b)
5 addcom
b + c = c + b
6 4, 5 ax_mp
2 ^ (b + c) = 2 ^ (c + b)
7 3, 6 ax_mp
a % 2 ^ (b + c) = a % 2 ^ (c + b)
8 2, 7 ax_mp
shr (a % 2 ^ (b + c)) c = shr (a % 2 ^ (c + b)) c
9 1, 8 ax_mp
shr (a % 2 ^ (c + b)) c = shr a c % 2 ^ b -> shr (a % 2 ^ (b + c)) c = shr a c % 2 ^ b
10 shrmodadd1
shr (a % 2 ^ (c + b)) c = shr a c % 2 ^ b
11 9, 10 ax_mp
shr (a % 2 ^ (b + c)) c = shr a c % 2 ^ 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)