Theorem gcd-div-gcd-pos

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: simp, localsimp,
• Comment: i / gcd(i,j) is the 'other' factor of i besides the gcd, analogous j / gcd(i, j). If those two would have a common divisor, it had to be part of the gcd of i and j, so their gcd is 1
• Used by: gcd-div-gcd,
• Used by units in proved state:
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 13
• Proof steps: 22
• Used lemmas: gcd-zero, div-mult, gcd-zero-04, gcd-max, divides, gcd-com, gcd-div-rest, gcd-zero-zero, gcd-less-eq-zero, gcd-one,
• Used spec theorems:
  • Used simplifier rules:
    • int-basic1/forward-pos
    • int-abs/gr-def
    • int-abs/absle
    • int-abs/lels
    • int-abs/lels-03
    • int-abs/lels-01
    • int-basic1/ls-01
    • int-div/div-elim-pospos
    • int-abs/forward-le-05
    • int-abs/forward-le-01
    • int-mult/zero-ge
    • int-mult/zero-gr
    • int-mult/le-same
    • int-abs/bet
    • int-basic1/lf-02
    • int-mult/zero-left
    • int-abs/lels-02
    • int-mult/zero-neq-01
    • int-mult/one-01
    • int-mult/eq-one
    • int-mult/eq-same-02
    • int-abs/abs-16
    • int-mult/commutativity
    • int-mult/associativity