Theorem znsubodd | index | src |

theorem znsubodd (a b: nat): $ odd (a -ZN b) <-> a < b $;
StepHypRefExpression
1 ax_3
(~a < b -> ~odd (a -ZN b)) -> odd (a -ZN b) -> a < b
2 b0odd
~odd (b0 (a - b))
3 ifneg
~a < b -> if (a < b) (b1 (b - suc a)) (b0 (a - b)) = b0 (a - b)
4 3 conv znsub
~a < b -> a -ZN b = b0 (a - b)
5 4 oddeqd
~a < b -> (odd (a -ZN b) <-> odd (b0 (a - b)))
6 5 noteqd
~a < b -> (~odd (a -ZN b) <-> ~odd (b0 (a - b)))
7 2, 6 mpbiri
~a < b -> ~odd (a -ZN b)
8 1, 7 ax_mp
odd (a -ZN b) -> a < b
9 b1odd
odd (b1 (b - suc a))
10 ifpos
a < b -> if (a < b) (b1 (b - suc a)) (b0 (a - b)) = b1 (b - suc a)
11 10 conv znsub
a < b -> a -ZN b = b1 (b - suc a)
12 11 oddeqd
a < b -> (odd (a -ZN b) <-> odd (b1 (b - suc a)))
13 9, 12 mpbiri
a < b -> odd (a -ZN b)
14 8, 13 ibii
odd (a -ZN b) <-> a < 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)