Theorem gcd-div-gcd

• 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: square-neq-any-pos-01, square-neq-any-pos-02, square-neq-pos,
• Used by units in proved state:
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 4
• Proof steps: 5
• Used lemmas: gcd-abs, gcd-zero-zero, gcd-zero-04, gcd-zero-03, gcd-div-gcd-pos, gcd-abs-rew-02,
• Used spec theorems:
  • Used simplifier rules:
    • int-abs/abs-06
    • int-abs/abs-01
    • int-abs/abs-07
    • int-div/zero
    • int-div/abs-01
    • int-div/div-same
    • int-div/abs