Theorem elpset1 ≪ | index | src | ≫ 

theorem elpset1 (m n: nat): $ ~n e. pset (m, 1) $;
StepHypRefExpression
1 inot 
(n e. pset (m, 1) -> ~n e. pset (m, 1)) -> ~n e. pset (m, 1)
2 elpset 
n e. pset (m, 1) <-> 0 < m /\ 0 < 1 /\ A. x (0 < x /\ x <= n -> x || m) /\ suc (m * suc n) || 1
3 absurd 
~m * suc n < suc 0 -> m * suc n < suc 0 -> ~n e. pset (m, 1)
4 lenlt 
suc 0 <= m * suc n <-> ~m * suc n < suc 0
5 mulpos 
0 < m * suc n <-> 0 < m /\ 0 < suc n
6 5 conv lt 
suc 0 <= m * suc n <-> 0 < m /\ 0 < suc n
7 id 
0 < m -> 0 < m
8 lt01S 
0 < suc n
9 8 a1i 
0 < m -> 0 < suc n
10 7, 9 iand 
0 < m -> 0 < m /\ 0 < suc n
11 6, 10 sylibr 
0 < m -> suc 0 <= m * suc n
12 an3l 
0 < m /\ 0 < 1 /\ A. x (0 < x /\ x <= n -> x || m) /\ suc (m * suc n) || 1 -> 0 < m
13 11, 12 syl 
0 < m /\ 0 < 1 /\ A. x (0 < x /\ x <= n -> x || m) /\ suc (m * suc n) || 1 -> suc 0 <= m * suc n
14 4, 13 sylib 
0 < m /\ 0 < 1 /\ A. x (0 < x /\ x <= n -> x || m) /\ suc (m * suc n) || 1 -> ~m * suc n < suc 0
15 d1ne0 
1 != 0
16 15 conv d1 
suc 0 != 0
17 16 a1i 
0 < m /\ 0 < 1 /\ A. x (0 < x /\ x <= n -> x || m) /\ suc (m * suc n) || 1 -> suc 0 != 0
18 anr 
0 < m /\ 0 < 1 /\ A. x (0 < x /\ x <= n -> x || m) /\ suc (m * suc n) || 1 -> suc (m * suc n) || 1
19 18 conv d1 
0 < m /\ 0 < 1 /\ A. x (0 < x /\ x <= n -> x || m) /\ suc (m * suc n) || 1 -> suc (m * suc n) || suc 0
20 17, 19 dvdle 
0 < m /\ 0 < 1 /\ A. x (0 < x /\ x <= n -> x || m) /\ suc (m * suc n) || 1 -> suc (m * suc n) <= suc 0
21 20 conv lt 
0 < m /\ 0 < 1 /\ A. x (0 < x /\ x <= n -> x || m) /\ suc (m * suc n) || 1 -> m * suc n < suc 0
22 3, 14, 21 sylc 
0 < m /\ 0 < 1 /\ A. x (0 < x /\ x <= n -> x || m) /\ suc (m * suc n) || 1 -> ~n e. pset (m, 1)
23 2, 22 sylbi 
n e. pset (m, 1) -> ~n e. pset (m, 1)
24 1, 23 ax_mp 
~n e. pset (m, 1)

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)