Theorem ledivmul1 ≪ | index | src | ≫ 

theorem ledivmul1 (a b c: nat): $ c != 0 -> (a <= b // c <-> c * a <= b) $;
StepHypRefExpression
1 lemul2a 
a <= b // c -> c * a <= c * (b // c)
2 1 anwr 
c != 0 /\ a <= b // c -> c * a <= c * (b // c)
3 muldivle 
c * (b // c) <= b
4 3 a1i 
c != 0 /\ a <= b // c -> c * (b // c) <= b
5 2, 4 letrd 
c != 0 /\ a <= b // c -> c * a <= b
6 leltsuc 
a <= b // c <-> a < suc (b // c)
7 ltmul2 
0 < c -> (a < suc (b // c) <-> c * a < c * suc (b // c))
8 lt01 
0 < c <-> c != 0
9 anl 
c != 0 /\ c * a <= b -> c != 0
10 8, 9 sylibr 
c != 0 /\ c * a <= b -> 0 < c
11 7, 10 syl 
c != 0 /\ c * a <= b -> (a < suc (b // c) <-> c * a < c * suc (b // c))
12 anr 
c != 0 /\ c * a <= b -> c * a <= b
13 lteq2 
c * suc (b // c) = c * (b // c) + c -> (b < c * suc (b // c) <-> b < c * (b // c) + c)
14 mulS 
c * suc (b // c) = c * (b // c) + c
15 13, 14 ax_mp 
b < c * suc (b // c) <-> b < c * (b // c) + c
16 lteq1 
c * (b // c) + b % c = b -> (c * (b // c) + b % c < c * (b // c) + c <-> b < c * (b // c) + c)
17 divmod 
c * (b // c) + b % c = b
18 16, 17 ax_mp 
c * (b // c) + b % c < c * (b // c) + c <-> b < c * (b // c) + c
19 ltadd2 
b % c < c <-> c * (b // c) + b % c < c * (b // c) + c
20 modlt 
c != 0 -> b % c < c
21 19, 20 sylib 
c != 0 -> c * (b // c) + b % c < c * (b // c) + c
22 18, 21 sylib 
c != 0 -> b < c * (b // c) + c
23 15, 22 sylibr 
c != 0 -> b < c * suc (b // c)
24 23 anwl 
c != 0 /\ c * a <= b -> b < c * suc (b // c)
25 12, 24 lelttrd 
c != 0 /\ c * a <= b -> c * a < c * suc (b // c)
26 11, 25 mpbird 
c != 0 /\ c * a <= b -> a < suc (b // c)
27 6, 26 sylibr 
c != 0 /\ c * a <= b -> a <= b // c
28 5, 27 ibida 
c != 0 -> (a <= b // c <-> 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_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)