Theorem mulpos | index | src |

theorem mulpos (a b: nat): $ 0 < a * b <-> 0 < a /\ 0 < b $;
StepHypRefExpression
1 lt01
0 < a * b <-> a * b != 0
2 lt01
0 < a <-> a != 0
3 con3
(a = 0 -> a * b = 0) -> ~a * b = 0 -> ~a = 0
4 3 conv ne
(a = 0 -> a * b = 0) -> a * b != 0 -> a != 0
5 mul01
0 * b = 0
6 muleq1
a = 0 -> a * b = 0 * b
7 5, 6 syl6eq
a = 0 -> a * b = 0
8 4, 7 ax_mp
a * b != 0 -> a != 0
9 2, 8 sylibr
a * b != 0 -> 0 < a
10 1, 9 sylbi
0 < a * b -> 0 < a
11 lt01
0 < b <-> b != 0
12 con3
(b = 0 -> a * b = 0) -> ~a * b = 0 -> ~b = 0
13 12 conv ne
(b = 0 -> a * b = 0) -> a * b != 0 -> b != 0
14 mul02
a * 0 = 0
15 muleq2
b = 0 -> a * b = a * 0
16 14, 15 syl6eq
b = 0 -> a * b = 0
17 13, 16 ax_mp
a * b != 0 -> b != 0
18 11, 17 sylibr
a * b != 0 -> 0 < b
19 1, 18 sylbi
0 < a * b -> 0 < b
20 10, 19 iand
0 < a * b -> 0 < a /\ 0 < b
21 lteq1
a * 0 = 0 -> (a * 0 < a * b <-> 0 < a * b)
22 mul0
a * 0 = 0
23 21, 22 ax_mp
a * 0 < a * b <-> 0 < a * b
24 ltmul2
0 < a -> (0 < b <-> a * 0 < a * b)
25 24 anwl
0 < a /\ 0 < b -> (0 < b <-> a * 0 < a * b)
26 anr
0 < a /\ 0 < b -> 0 < b
27 25, 26 mpbid
0 < a /\ 0 < b -> a * 0 < a * b
28 23, 27 sylib
0 < a /\ 0 < b -> 0 < a * b
29 20, 28 ibii
0 < a * b <-> 0 < a /\ 0 < 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)