Theorem dvd01 ≪ | index | src | ≫ 

theorem dvd01 (a: nat): $ 0 || a <-> a = 0 $;
StepHypRefExpression
1 bi1 
(x * 0 = a <-> 0 = a) -> x * 0 = a -> 0 = a
2 eqeq1 
x * 0 = 0 -> (x * 0 = a <-> 0 = a)
3 mul02 
x * 0 = 0
4 2, 3 ax_mp 
x * 0 = a <-> 0 = a
5 1, 4 ax_mp 
x * 0 = a -> 0 = a
6 5 eqcomd 
x * 0 = a -> a = 0
7 6 eex 
E. x x * 0 = a -> a = 0
8 7 conv dvd 
0 || a -> a = 0
9 dvd02 
0 || 0
10 dvdeq2 
a = 0 -> (0 || a <-> 0 || 0)
11 9, 10 mpbiri 
a = 0 -> 0 || a
12 8, 11 ibii 
0 || a <-> a = 0

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 (peano2, peano5, muleq, add0, mul0, mulS)