Theorem modlt | index | src |

pub theorem modlt (a b: nat): $ b != 0 -> a % b < b $;
StepHypRefExpression
1 divlem3
b != 0 -> E. q E. r (r < b /\ b * q + r = a)
2 anrl
b != 0 /\ (r < b /\ b * q + r = a) -> r < b
3 anrr
b != 0 /\ (r < b /\ b * q + r = a) -> b * q + r = a
4 2, 3 eqdivmod
b != 0 /\ (r < b /\ b * q + r = a) -> a // b = q /\ a % b = r
5 4 anrd
b != 0 /\ (r < b /\ b * q + r = a) -> a % b = r
6 5 lteq1d
b != 0 /\ (r < b /\ b * q + r = a) -> (a % b < b <-> r < b)
7 6, 2 mpbird
b != 0 /\ (r < b /\ b * q + r = a) -> a % b < b
8 7 eexda
b != 0 -> E. r (r < b /\ b * q + r = a) -> a % b < b
9 8 eexd
b != 0 -> E. q E. r (r < b /\ b * q + r = a) -> a % b < b
10 1, 9 mpd
b != 0 -> a % b < 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), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)