Theorem psetS ≪ | index | src | ≫ 

theorem psetS (G: wff) (a m n v: nat) {x: nat}:
  $ G -> 0 < m $ >
  $ G -> 0 < v $ >
  $ G -> A. x (0 < x /\ x <= n -> x || m) $ >
  $ G -> (a e. pset (m, v * suc (m * suc n)) <-> a e. pset (m, v) \/ a = n) $;
StepHypRefExpression
1 elpset 
a e. pset (m, v * suc (m * suc n)) <-> 0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n)
2 elpset 
a e. pset (m, v) <-> 0 < m /\ 0 < v /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v
3 2 oreq1i 
a e. pset (m, v) \/ a = n <-> 0 < m /\ 0 < v /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v \/ a = n
4 orcom 
a = n \/ 0 < m /\ 0 < v /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v ->
  0 < m /\ 0 < v /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v \/ a = n
5 4 conv or 
(~a = n -> 0 < m /\ 0 < v /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v) ->
  0 < m /\ 0 < v /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v \/ a = n
6 hyp h1 
G -> 0 < m
7 6 anwll 
G /\ (0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n)) /\ ~a = n -> 0 < m
8 mulpos 
0 < v * suc (m * suc n) <-> 0 < v /\ 0 < suc (m * suc n)
9 anllr 
0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n) -> 0 < v * suc (m * suc n)
10 anlr 
G /\ (0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n)) /\ ~a = n ->
  0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n)
11 9, 10 syl 
G /\ (0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n)) /\ ~a = n -> 0 < v * suc (m * suc n)
12 8, 11 sylib 
G /\ (0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n)) /\ ~a = n -> 0 < v /\ 0 < suc (m * suc n)
13 12 anld 
G /\ (0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n)) /\ ~a = n -> 0 < v
14 7, 13 iand 
G /\ (0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n)) /\ ~a = n -> 0 < m /\ 0 < v
15 anlr 
0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n) -> A. x (0 < x /\ x <= a -> x || m)
16 15, 10 syl 
G /\ (0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n)) /\ ~a = n ->
  A. x (0 < x /\ x <= a -> x || m)
17 14, 16 iand 
G /\ (0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n)) /\ ~a = n ->
  0 < m /\ 0 < v /\ A. x (0 < x /\ x <= a -> x || m)
18 lteq2 
x = y -> (0 < x <-> 0 < y)
19 lteq1 
x = y -> (x < max (suc a) (suc n) <-> y < max (suc a) (suc n))
20 18, 19 aneqd 
x = y -> (0 < x /\ x < max (suc a) (suc n) <-> 0 < y /\ y < max (suc a) (suc n))
21 dvdeq1 
x = y -> (x || m <-> y || m)
22 20, 21 imeqd 
x = y -> (0 < x /\ x < max (suc a) (suc n) -> x || m <-> 0 < y /\ y < max (suc a) (suc n) -> y || m)
23 22 cbval 
A. x (0 < x /\ x < max (suc a) (suc n) -> x || m) <-> A. y (0 < y /\ y < max (suc a) (suc n) -> y || m)
24 andi 
0 < x /\ (x <= a \/ x <= n) <-> 0 < x /\ x <= a \/ 0 < x /\ x <= n
25 anim2 
(x < max (suc a) (suc n) -> x <= a \/ x <= n) -> 0 < x /\ x < max (suc a) (suc n) -> 0 < x /\ (x <= a \/ x <= n)
26 ltmax 
x < max (suc a) (suc n) <-> x < suc a \/ x < suc n
27 bi2 
(x <= a \/ x <= n <-> x < suc a \/ x < suc n) -> x < suc a \/ x < suc n -> x <= a \/ x <= n
28 leltsuc 
x <= a <-> x < suc a
29 leltsuc 
x <= n <-> x < suc n
30 28, 29 oreqi 
x <= a \/ x <= n <-> x < suc a \/ x < suc n
31 27, 30 ax_mp 
x < suc a \/ x < suc n -> x <= a \/ x <= n
32 26, 31 sylbi 
x < max (suc a) (suc n) -> x <= a \/ x <= n
33 25, 32 ax_mp 
0 < x /\ x < max (suc a) (suc n) -> 0 < x /\ (x <= a \/ x <= n)
34 24, 33 sylib 
0 < x /\ x < max (suc a) (suc n) -> 0 < x /\ x <= a \/ 0 < x /\ x <= n
35 34 imim1i 
(0 < x /\ x <= a \/ 0 < x /\ x <= n -> x || m) -> 0 < x /\ x < max (suc a) (suc n) -> x || m
36 eor 
(0 < x /\ x <= a -> x || m) -> (0 < x /\ x <= n -> x || m) -> 0 < x /\ x <= a \/ 0 < x /\ x <= n -> x || m
37 35, 36 syl6 
(0 < x /\ x <= a -> x || m) -> (0 < x /\ x <= n -> x || m) -> 0 < x /\ x < max (suc a) (suc n) -> x || m
38 37 al2imi 
A. x (0 < x /\ x <= a -> x || m) -> A. x (0 < x /\ x <= n -> x || m) -> A. x (0 < x /\ x < max (suc a) (suc n) -> x || m)
39 hyp h3 
G -> A. x (0 < x /\ x <= n -> x || m)
40 39 anwll 
G /\ (0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n)) /\ ~a = n ->
  A. x (0 < x /\ x <= n -> x || m)
41 38, 16, 40 sylc 
G /\ (0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n)) /\ ~a = n ->
  A. x (0 < x /\ x < max (suc a) (suc n) -> x || m)
42 23, 41 sylib 
G /\ (0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n)) /\ ~a = n ->
  A. y (0 < y /\ y < max (suc a) (suc n) -> y || m)
43 anr 
G /\ (0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n)) /\ ~a = n -> ~a = n
44 43 conv ne 
G /\ (0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n)) /\ ~a = n -> a != n
45 lemax1 
suc a <= max (suc a) (suc n)
46 45 conv lt 
a < max (suc a) (suc n)
47 46 a1i 
G /\ (0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n)) /\ ~a = n -> a < max (suc a) (suc n)
48 lemax2 
suc n <= max (suc a) (suc n)
49 48 conv lt 
n < max (suc a) (suc n)
50 49 a1i 
G /\ (0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n)) /\ ~a = n -> n < max (suc a) (suc n)
51 42, 44, 47, 50 psetSlem2 
G /\ (0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n)) /\ ~a = n ->
  coprime (suc (m * suc a)) (suc (m * suc n))
52 anrr 
G /\ (0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n)) -> suc (m * suc a) || v * suc (m * suc n)
53 52 anwl 
G /\ (0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n)) /\ ~a = n ->
  suc (m * suc a) || v * suc (m * suc n)
54 51, 53 copdvdmul1 
G /\ (0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n)) /\ ~a = n -> suc (m * suc a) || v
55 17, 54 iand 
G /\ (0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n)) /\ ~a = n ->
  0 < m /\ 0 < v /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v
56 5, 55 syla 
G /\ (0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n)) ->
  0 < m /\ 0 < v /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v \/ a = n
57 56 exp 
G ->
  0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n) ->
  0 < m /\ 0 < v /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v \/ a = n
58 anim1 
(0 < m /\ 0 < v -> 0 < m /\ 0 < v * suc (m * suc n)) ->
  0 < m /\ 0 < v /\ A. x (0 < x /\ x <= a -> x || m) ->
  0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m)
59 anim2 
(0 < v -> 0 < v * suc (m * suc n)) -> 0 < m /\ 0 < v -> 0 < m /\ 0 < v * suc (m * suc n)
60 id 
0 < v -> 0 < v
61 lt01S 
0 < suc (m * suc n)
62 61 a1i 
0 < v -> 0 < suc (m * suc n)
63 60, 62 iand 
0 < v -> 0 < v /\ 0 < suc (m * suc n)
64 8, 63 sylibr 
0 < v -> 0 < v * suc (m * suc n)
65 59, 64 ax_mp 
0 < m /\ 0 < v -> 0 < m /\ 0 < v * suc (m * suc n)
66 58, 65 ax_mp 
0 < m /\ 0 < v /\ A. x (0 < x /\ x <= a -> x || m) -> 0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m)
67 66 a1i 
G -> 0 < m /\ 0 < v /\ A. x (0 < x /\ x <= a -> x || m) -> 0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m)
68 dvdmul11 
suc (m * suc a) || v -> suc (m * suc a) || v * suc (m * suc n)
69 68 a1i 
G -> suc (m * suc a) || v -> suc (m * suc a) || v * suc (m * suc n)
70 67, 69 animd 
G ->
  0 < m /\ 0 < v /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v ->
  0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n)
71 leeq2 
a = n -> (x <= a <-> x <= n)
72 71 aneq2d 
a = n -> (0 < x /\ x <= a <-> 0 < x /\ x <= n)
73 72 imeq1d 
a = n -> (0 < x /\ x <= a -> x || m <-> 0 < x /\ x <= n -> x || m)
74 73 aleqd 
a = n -> (A. x (0 < x /\ x <= a -> x || m) <-> A. x (0 < x /\ x <= n -> x || m))
75 74 aneq2d 
a = n -> (0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) <-> 0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= n -> x || m))
76 suceq 
a = n -> suc a = suc n
77 76 muleq2d 
a = n -> m * suc a = m * suc n
78 77 suceqd 
a = n -> suc (m * suc a) = suc (m * suc n)
79 78 dvdeq1d 
a = n -> (suc (m * suc a) || v * suc (m * suc n) <-> suc (m * suc n) || v * suc (m * suc n))
80 75, 79 aneqd 
a = n ->
  (0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n) <->
    0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= n -> x || m) /\ suc (m * suc n) || v * suc (m * suc n))
81 hyp h2 
G -> 0 < v
82 61 a1i 
G -> 0 < suc (m * suc n)
83 81, 82 iand 
G -> 0 < v /\ 0 < suc (m * suc n)
84 8, 83 sylibr 
G -> 0 < v * suc (m * suc n)
85 6, 84 iand 
G -> 0 < m /\ 0 < v * suc (m * suc n)
86 85, 39 iand 
G -> 0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= n -> x || m)
87 dvdmul1 
suc (m * suc n) || v * suc (m * suc n)
88 87 a1i 
G -> suc (m * suc n) || v * suc (m * suc n)
89 86, 88 iand 
G -> 0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= n -> x || m) /\ suc (m * suc n) || v * suc (m * suc n)
90 80, 89 syl5ibrcom 
G -> a = n -> 0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n)
91 70, 90 eord 
G ->
  0 < m /\ 0 < v /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v \/ a = n ->
  0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n)
92 57, 91 ibid 
G ->
  (0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n) <->
    0 < m /\ 0 < v /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v \/ a = n)
93 3, 92 syl6bbr 
G -> (0 < m /\ 0 < v * suc (m * suc n) /\ A. x (0 < x /\ x <= a -> x || m) /\ suc (m * suc a) || v * suc (m * suc n) <-> a e. pset (m, v) \/ a = n)
94 1, 93 syl5bb 
G -> (a e. pset (m, v * suc (m * suc n)) <-> a e. pset (m, v) \/ a = n)

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)