Theorem dvdasymd ≪ | index | src | ≫ 

theorem dvdasymd (G: wff) (a b: nat):
  $ G -> a || b $ >
  $ G -> b || a $ >
  $ G -> a = b $;
StepHypRefExpression
1 anr 
G /\ a = 0 -> a = 0
2 dvd01 
0 || b <-> b = 0
3 dvdeq1 
a = 0 -> (a || b <-> 0 || b)
4 3 anwr 
G /\ a = 0 -> (a || b <-> 0 || b)
5 hyp h1 
G -> a || b
6 5 anwl 
G /\ a = 0 -> a || b
7 4, 6 mpbid 
G /\ a = 0 -> 0 || b
8 2, 7 sylib 
G /\ a = 0 -> b = 0
9 1, 8 eqtr4d 
G /\ a = 0 -> a = b
10 dvd01 
0 || a <-> a = 0
11 dvdeq1 
b = 0 -> (b || a <-> 0 || a)
12 11 anwr 
G /\ ~a = 0 /\ b = 0 -> (b || a <-> 0 || a)
13 hyp h2 
G -> b || a
14 13 anwll 
G /\ ~a = 0 /\ b = 0 -> b || a
15 12, 14 mpbid 
G /\ ~a = 0 /\ b = 0 -> 0 || a
16 10, 15 sylib 
G /\ ~a = 0 /\ b = 0 -> a = 0
17 anr 
G /\ ~a = 0 /\ b = 0 -> b = 0
18 16, 17 eqtr4d 
G /\ ~a = 0 /\ b = 0 -> a = b
19 anr 
G /\ ~a = 0 /\ ~b = 0 -> ~b = 0
20 19 conv ne 
G /\ ~a = 0 /\ ~b = 0 -> b != 0
21 5 anwll 
G /\ ~a = 0 /\ ~b = 0 -> a || b
22 20, 21 dvdle 
G /\ ~a = 0 /\ ~b = 0 -> a <= b
23 anlr 
G /\ ~a = 0 /\ ~b = 0 -> ~a = 0
24 23 conv ne 
G /\ ~a = 0 /\ ~b = 0 -> a != 0
25 13 anwll 
G /\ ~a = 0 /\ ~b = 0 -> b || a
26 24, 25 dvdle 
G /\ ~a = 0 /\ ~b = 0 -> b <= a
27 22, 26 leasymd 
G /\ ~a = 0 /\ ~b = 0 -> a = b
28 18, 27 casesda 
G /\ ~a = 0 -> a = b
29 9, 28 casesda 
G -> 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_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)