Theorem eqmdvdsub2 ≪ | index | src | ≫ 

theorem eqmdvdsub2 (a b n: nat): $ mod(n): a = b <-> n || zabs (b -ZN a) $;
StepHypRefExpression
1 eor 
(a <= b -> (mod(n): a = b <-> n || zabs (b -ZN a))) ->
  (b <= a -> (mod(n): a = b <-> n || zabs (b -ZN a))) ->
  a <= b \/ b <= a ->
  (mod(n): a = b <-> n || zabs (b -ZN a))
2 eqmdvdsub 
a <= b -> (mod(n): a = b <-> n || b - a)
3 lezabszn 
a <= b -> zabs (b -ZN a) = b - a
4 3 dvdeq2d 
a <= b -> (n || zabs (b -ZN a) <-> n || b - a)
5 2, 4 bitr4d 
a <= b -> (mod(n): a = b <-> n || zabs (b -ZN a))
6 1, 5 ax_mp 
(b <= a -> (mod(n): a = b <-> n || zabs (b -ZN a))) -> a <= b \/ b <= a -> (mod(n): a = b <-> n || zabs (b -ZN a))
7 eqmcomb 
mod(n): a = b <-> mod(n): b = a
8 eqmdvdsub 
b <= a -> (mod(n): b = a <-> n || a - b)
9 zabscom 
zabs (b -ZN a) = zabs (a -ZN b)
10 lezabszn 
b <= a -> zabs (a -ZN b) = a - b
11 9, 10 syl5eq 
b <= a -> zabs (b -ZN a) = a - b
12 11 dvdeq2d 
b <= a -> (n || zabs (b -ZN a) <-> n || a - b)
13 8, 12 bitr4d 
b <= a -> (mod(n): b = a <-> n || zabs (b -ZN a))
14 7, 13 syl5bb 
b <= a -> (mod(n): a = b <-> n || zabs (b -ZN a))
15 6, 14 ax_mp 
a <= b \/ b <= a -> (mod(n): a = b <-> n || zabs (b -ZN a))
16 leorle 
a <= b \/ b <= a
17 15, 16 ax_mp 
mod(n): a = b <-> n || zabs (b -ZN a)

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)