Theorem psetSlem2 ≪ | index | src | ≫ 

theorem psetSlem2 (G: wff) (a b m n: nat) {x: nat}:
  $ G -> A. x (0 < x /\ x < n -> x || m) $ >
  $ G -> a != b $ >
  $ G -> a < n $ >
  $ G -> b < n $ >
  $ G -> coprime (suc (m * suc a)) (suc (m * suc b)) $;
StepHypRefExpression
1 neltlt 
a != b <-> a < b \/ b < a
2 hyp h2 
G -> a != b
3 1, 2 sylib 
G -> a < b \/ b < a
4 hyp h1 
G -> A. x (0 < x /\ x < n -> x || m)
5 4 anwl 
G /\ a < b -> A. x (0 < x /\ x < n -> x || m)
6 anr 
G /\ a < b -> a < b
7 hyp h4 
G -> b < n
8 7 anwl 
G /\ a < b -> b < n
9 5, 6, 8 psetSlem1 
G /\ a < b -> coprime (suc (m * suc a)) (suc (m * suc b))
10 copcom 
coprime (suc (m * suc b)) (suc (m * suc a)) <-> coprime (suc (m * suc a)) (suc (m * suc b))
11 4 anwl 
G /\ b < a -> A. x (0 < x /\ x < n -> x || m)
12 anr 
G /\ b < a -> b < a
13 hyp h3 
G -> a < n
14 13 anwl 
G /\ b < a -> a < n
15 11, 12, 14 psetSlem1 
G /\ b < a -> coprime (suc (m * suc b)) (suc (m * suc a))
16 10, 15 sylib 
G /\ b < a -> coprime (suc (m * suc a)) (suc (m * suc b))
17 9, 16 eorda 
G -> a < b \/ b < a -> coprime (suc (m * suc a)) (suc (m * suc b))
18 3, 17 mpd 
G -> coprime (suc (m * suc a)) (suc (m * suc 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)