Theorem dvdeqm ≪ | index | src | ≫ 

theorem dvdeqm (G: wff) (a b m n: nat):
  $ G -> m || n $ >
  $ G -> mod(n): a = b $ >
  $ G -> mod(m): a = b $;
StepHypRefExpression
1 leorle 
a <= b \/ b <= a
2 eqmdvdsub 
a <= b -> (mod(m): a = b <-> m || b - a)
3 2 anwr 
G /\ a <= b -> (mod(m): a = b <-> m || b - a)
4 dvdtr 
m || n -> n || b - a -> m || b - a
5 hyp h1 
G -> m || n
6 5 anwl 
G /\ a <= b -> m || n
7 eqmdvdsub 
a <= b -> (mod(n): a = b <-> n || b - a)
8 7 anwr 
G /\ a <= b -> (mod(n): a = b <-> n || b - a)
9 hyp h2 
G -> mod(n): a = b
10 9 anwl 
G /\ a <= b -> mod(n): a = b
11 8, 10 mpbid 
G /\ a <= b -> n || b - a
12 4, 6, 11 sylc 
G /\ a <= b -> m || b - a
13 3, 12 mpbird 
G /\ a <= b -> mod(m): a = b
14 eqmcom 
mod(m): b = a -> mod(m): a = b
15 eqmdvdsub 
b <= a -> (mod(m): b = a <-> m || a - b)
16 15 anwr 
G /\ b <= a -> (mod(m): b = a <-> m || a - b)
17 dvdtr 
m || n -> n || a - b -> m || a - b
18 5 anwl 
G /\ b <= a -> m || n
19 eqmdvdsub 
b <= a -> (mod(n): b = a <-> n || a - b)
20 19 anwr 
G /\ b <= a -> (mod(n): b = a <-> n || a - b)
21 eqmcom 
mod(n): a = b -> mod(n): b = a
22 21, 9 syl 
G -> mod(n): b = a
23 22 anwl 
G /\ b <= a -> mod(n): b = a
24 20, 23 mpbid 
G /\ b <= a -> n || a - b
25 17, 18, 24 sylc 
G /\ b <= a -> m || a - b
26 16, 25 mpbird 
G /\ b <= a -> mod(m): b = a
27 14, 26 syl 
G /\ b <= a -> mod(m): a = b
28 13, 27 eorda 
G -> a <= b \/ b <= a -> mod(m): a = b
29 1, 28 mpi 
G -> mod(m): 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)