Theorem congmod-inverse

• Type: A user defined theorem
• Validity: The proof is valid.
• Features:
• Comment: i0 is the the multiplicative modulo inverse: z = x ^-1 mod n ⇔ z * x ≡ 1 mod n, i.e. ≡mod(z * x, 1, n).
• Used by: congmod-inverse-pos, fermat-2,
• Used by units in proved state:
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 19
• Proof steps: 36
• Used lemmas: congmod-def, cong-one-01, cong-one, cong-zero, cong-same,
• Used spec theorems:
  • int-gcd/gcd-mod-one-01
  • int-gcd/gcd-abs-rew-02
  • int-abs/sub-same-01
• Used simplifier rules:
  • int-abs/lels
  • int-mult/Mult-zero
  • int-mult/one
  • int-gcd/gcd-com
  • int-abs/lenls
  • int-abs/abs-01
  • int-mult/eq-one
  • int-abs/abs-one-01
  • int-gcd/gcd-one-01
  • int-abs/absle
  • int-mult/one-01
  • int-div/div-elim-pospos
  • int-abs/forward-le-01
  • int-mult/zero-ge
  • int-gcd/div-abs
  • int-abs/forward-le-02
  • oelem/intlista/transitivity
  • int-abs/lels-01
  • int-gcd/gcd-zero-04
  • int-abs/abs-08
  • int-gcd/div-zero-zero
  • int-mult/minus-one-01
  • int-abs/neg-02
  • int-basic2/zero-04
  • int-abs/mone-06
  • int-abs/zero-gels-04
  • int-abs/numadd-01
  • int-abs/negeq
  • int-div/mod-neg-01
  • int-abs/abs-07
  • int-mult/minus-left
  • int-gcd/div-abs-02
  • int-abs/abs-neg
  • int-abs/subsub
  • int-div/div-elim-negpos
  • int-abs/numlelsdel-01
  • int-abs/forward-le-04
  • int-abs/forward-lels
  • int-basic1/forward-pos
  • int-abs/forward-le-05
  • oelem/intlista/lel
  • int-mult/commutativity
  • int-mult/associativity
  • int-abs/zero-gels-01
  • int-mult/zero-ls
  • int-abs/abs-06
  • int-abs/sub-eq
  • int-basic2/add-c
  • int-basic2/add-a
  • int-abs/minus-add