Theorem psetSlem1 ≪ | index | src | ≫ 

theorem psetSlem1 (G: wff) (i j m n: nat) {x: nat}:
  $ G -> A. x (0 < x /\ x < n -> x || m) $ >
  $ G -> i < j $ >
  $ G -> j < n $ >
  $ G -> coprime (suc (m * suc i)) (suc (m * suc j)) $;
StepHypRefExpression
1 dfcop2 
coprime (suc (m * suc i)) (suc (m * suc j)) <-> A. u (u || suc (m * suc i) -> u || suc (m * suc j) -> u = 1)
2 dvd12 
u || 1 <-> u = 1
3 dvdadd1 
u || m * suc i -> (u || 1 <-> u || m * suc i + 1)
4 dvdmul11 
u || m -> u || m * suc i
5 dvdtr 
u || j - i -> j - i || m -> u || m
6 dvdadd1 
u || suc (m * suc j) * suc i -> (u || j - i <-> u || suc (m * suc j) * suc i + (j - i))
7 dvdmul11 
u || suc (m * suc j) -> u || suc (m * suc j) * suc i
8 7 anwr 
G /\ u || suc (m * suc i) /\ u || suc (m * suc j) -> u || suc (m * suc j) * suc i
9 6, 8 syl 
G /\ u || suc (m * suc i) /\ u || suc (m * suc j) -> (u || j - i <-> u || suc (m * suc j) * suc i + (j - i))
10 addeq1 
suc (m * suc j) * suc i = m * suc j * suc i + suc i -> suc (m * suc j) * suc i + (j - i) = m * suc j * suc i + suc i + (j - i)
11 mulS1 
suc (m * suc j) * suc i = m * suc j * suc i + suc i
12 10, 11 ax_mp 
suc (m * suc j) * suc i + (j - i) = m * suc j * suc i + suc i + (j - i)
13 addass 
m * suc j * suc i + suc i + (j - i) = m * suc j * suc i + (suc i + (j - i))
14 mulS1 
suc (m * suc i) * suc j = m * suc i * suc j + suc j
15 addeq1 
m * suc j * suc i = m * suc i * suc j -> m * suc j * suc i + suc j = m * suc i * suc j + suc j
16 mulrass 
m * suc j * suc i = m * suc i * suc j
17 15, 16 ax_mp 
m * suc j * suc i + suc j = m * suc i * suc j + suc j
18 addS1 
suc i + (j - i) = suc (i + (j - i))
19 pncan3 
i <= j -> i + (j - i) = j
20 ltle 
i < j -> i <= j
21 hyp h2 
G -> i < j
22 21 anwll 
G /\ u || suc (m * suc i) /\ u || suc (m * suc j) -> i < j
23 20, 22 syl 
G /\ u || suc (m * suc i) /\ u || suc (m * suc j) -> i <= j
24 19, 23 syl 
G /\ u || suc (m * suc i) /\ u || suc (m * suc j) -> i + (j - i) = j
25 24 suceqd 
G /\ u || suc (m * suc i) /\ u || suc (m * suc j) -> suc (i + (j - i)) = suc j
26 18, 25 syl5eq 
G /\ u || suc (m * suc i) /\ u || suc (m * suc j) -> suc i + (j - i) = suc j
27 26 addeq2d 
G /\ u || suc (m * suc i) /\ u || suc (m * suc j) -> m * suc j * suc i + (suc i + (j - i)) = m * suc j * suc i + suc j
28 17, 27 syl6eq 
G /\ u || suc (m * suc i) /\ u || suc (m * suc j) -> m * suc j * suc i + (suc i + (j - i)) = m * suc i * suc j + suc j
29 14, 28 syl6eqr 
G /\ u || suc (m * suc i) /\ u || suc (m * suc j) -> m * suc j * suc i + (suc i + (j - i)) = suc (m * suc i) * suc j
30 13, 29 syl5eq 
G /\ u || suc (m * suc i) /\ u || suc (m * suc j) -> m * suc j * suc i + suc i + (j - i) = suc (m * suc i) * suc j
31 12, 30 syl5eq 
G /\ u || suc (m * suc i) /\ u || suc (m * suc j) -> suc (m * suc j) * suc i + (j - i) = suc (m * suc i) * suc j
32 31 dvdeq2d 
G /\ u || suc (m * suc i) /\ u || suc (m * suc j) -> (u || suc (m * suc j) * suc i + (j - i) <-> u || suc (m * suc i) * suc j)
33 dvdmul11 
u || suc (m * suc i) -> u || suc (m * suc i) * suc j
34 anlr 
G /\ u || suc (m * suc i) /\ u || suc (m * suc j) -> u || suc (m * suc i)
35 33, 34 syl 
G /\ u || suc (m * suc i) /\ u || suc (m * suc j) -> u || suc (m * suc i) * suc j
36 32, 35 mpbird 
G /\ u || suc (m * suc i) /\ u || suc (m * suc j) -> u || suc (m * suc j) * suc i + (j - i)
37 9, 36 mpbird 
G /\ u || suc (m * suc i) /\ u || suc (m * suc j) -> u || j - i
38 lteq2 
x = j - i -> (0 < x <-> 0 < j - i)
39 lteq1 
x = j - i -> (x < n <-> j - i < n)
40 38, 39 aneqd 
x = j - i -> (0 < x /\ x < n <-> 0 < j - i /\ j - i < n)
41 dvdeq1 
x = j - i -> (x || m <-> j - i || m)
42 40, 41 imeqd 
x = j - i -> (0 < x /\ x < n -> x || m <-> 0 < j - i /\ j - i < n -> j - i || m)
43 42 eale 
A. x (0 < x /\ x < n -> x || m) -> 0 < j - i /\ j - i < n -> j - i || m
44 hyp h1 
G -> A. x (0 < x /\ x < n -> x || m)
45 44 anwll 
G /\ u || suc (m * suc i) /\ u || suc (m * suc j) -> A. x (0 < x /\ x < n -> x || m)
46 subpos 
i < j <-> 0 < j - i
47 46, 22 sylib 
G /\ u || suc (m * suc i) /\ u || suc (m * suc j) -> 0 < j - i
48 subleid 
j - i <= j
49 48 a1i 
G /\ u || suc (m * suc i) /\ u || suc (m * suc j) -> j - i <= j
50 hyp h3 
G -> j < n
51 50 anwll 
G /\ u || suc (m * suc i) /\ u || suc (m * suc j) -> j < n
52 49, 51 lelttrd 
G /\ u || suc (m * suc i) /\ u || suc (m * suc j) -> j - i < n
53 47, 52 iand 
G /\ u || suc (m * suc i) /\ u || suc (m * suc j) -> 0 < j - i /\ j - i < n
54 43, 45, 53 sylc 
G /\ u || suc (m * suc i) /\ u || suc (m * suc j) -> j - i || m
55 5, 37, 54 sylc 
G /\ u || suc (m * suc i) /\ u || suc (m * suc j) -> u || m
56 4, 55 syl 
G /\ u || suc (m * suc i) /\ u || suc (m * suc j) -> u || m * suc i
57 3, 56 syl 
G /\ u || suc (m * suc i) /\ u || suc (m * suc j) -> (u || 1 <-> u || m * suc i + 1)
58 dvdeq2 
m * suc i + 1 = suc (m * suc i) -> (u || m * suc i + 1 <-> u || suc (m * suc i))
59 add12 
m * suc i + 1 = suc (m * suc i)
60 58, 59 ax_mp 
u || m * suc i + 1 <-> u || suc (m * suc i)
61 60, 34 sylibr 
G /\ u || suc (m * suc i) /\ u || suc (m * suc j) -> u || m * suc i + 1
62 57, 61 mpbird 
G /\ u || suc (m * suc i) /\ u || suc (m * suc j) -> u || 1
63 2, 62 sylib 
G /\ u || suc (m * suc i) /\ u || suc (m * suc j) -> u = 1
64 63 exp 
G /\ u || suc (m * suc i) -> u || suc (m * suc j) -> u = 1
65 64 exp 
G -> u || suc (m * suc i) -> u || suc (m * suc j) -> u = 1
66 65 iald 
G -> A. u (u || suc (m * suc i) -> u || suc (m * suc j) -> u = 1)
67 1, 66 sylibr 
G -> coprime (suc (m * suc i)) (suc (m * suc j))

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)