Theorem dvdle ≪ | index | src | ≫ 

theorem dvdle (G: wff) (a b: nat):
  $ G -> b != 0 $ >
  $ G -> a || b $ >
  $ G -> a <= b $;
StepHypRefExpression
1 hyp h2 
G -> a || b
2 mul11 
1 * a = a
3 2 a1i 
G /\ x * a = b -> 1 * a = a
4 anr 
G /\ x * a = b -> x * a = b
5 3, 4 leeqd 
G /\ x * a = b -> (1 * a <= x * a <-> a <= b)
6 lemul1a 
1 <= x -> 1 * a <= x * a
7 lt01 
0 < x <-> x != 0
8 7 conv d1, lt 
1 <= x <-> x != 0
9 hyp h1 
G -> b != 0
10 9 conv ne 
G -> ~b = 0
11 10 anwl 
G /\ x * a = b -> ~b = 0
12 anlr 
G /\ x * a = b /\ x = 0 -> x * a = b
13 mul01 
0 * a = 0
14 muleq1 
x = 0 -> x * a = 0 * a
15 14 anwr 
G /\ x * a = b /\ x = 0 -> x * a = 0 * a
16 13, 15 syl6eq 
G /\ x * a = b /\ x = 0 -> x * a = 0
17 12, 16 eqtr3d 
G /\ x * a = b /\ x = 0 -> b = 0
18 11, 17 mtand 
G /\ x * a = b -> ~x = 0
19 18 conv ne 
G /\ x * a = b -> x != 0
20 8, 19 sylibr 
G /\ x * a = b -> 1 <= x
21 6, 20 syl 
G /\ x * a = b -> 1 * a <= x * a
22 5, 21 mpbid 
G /\ x * a = b -> a <= b
23 22 eexda 
G -> E. x x * a = b -> a <= b
24 23 conv dvd 
G -> a || b -> a <= b
25 1, 24 mpd 
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)