Theorem mulcan1 ≪ | index | src | ≫ 

theorem mulcan1 (a b c: nat): $ c != 0 -> (a * c = b * c <-> a = b) $;
StepHypRefExpression
1 lt01 
0 < c <-> c != 0
2 lemul1 
0 < c -> (a <= b <-> a * c <= b * c)
3 2 anwl 
0 < c /\ a * c = b * c -> (a <= b <-> a * c <= b * c)
4 eqle 
a * c = b * c -> a * c <= b * c
5 4 anwr 
0 < c /\ a * c = b * c -> a * c <= b * c
6 3, 5 mpbird 
0 < c /\ a * c = b * c -> a <= b
7 lemul1 
0 < c -> (b <= a <-> b * c <= a * c)
8 7 anwl 
0 < c /\ a * c = b * c -> (b <= a <-> b * c <= a * c)
9 eqler 
a * c = b * c -> b * c <= a * c
10 9 anwr 
0 < c /\ a * c = b * c -> b * c <= a * c
11 8, 10 mpbird 
0 < c /\ a * c = b * c -> b <= a
12 6, 11 leasymd 
0 < c /\ a * c = b * c -> a = b
13 12 exp 
0 < c -> a * c = b * c -> a = b
14 1, 13 sylbir 
c != 0 -> a * c = b * c -> a = b
15 muleq1 
a = b -> a * c = b * c
16 15 a1i 
c != 0 -> a = b -> a * c = b * c
17 14, 16 ibid 
c != 0 -> (a * c = b * c <-> 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)