PA00BI

mod_one_product_restore_predecessor

Alpha v16 checked-use theorem · independently closed; not Stable

Multiplying a residue-one product by n restores the predecessor residue n.

Exact expanded PA statement

forall p P n F. F = P * n -> (exists wpp_mod_left_wer_mod_left wpp_mod_right_wer_mod_left. (P) + p * wpp_mod_left_wer_mod_left = (1) + p * wpp_mod_right_wer_mod_left) -> (exists wpp_mod_left_wer_mod_result wpp_mod_right_wer_mod_result. (F) + p * wpp_mod_left_wer_mod_result = (n) + p * wpp_mod_right_wer_mod_result)

Structural proof guide

Generated structural guide

Multiplying a residue-one product by n restores the predecessor residue n.

Use the direct prerequisites mod_eq_mul_right, one_mul as previously established PA formulas.

The proof proceeds by intermediate claims (2), equality transport (2).

Referenced ingredients

PA001Y mod_eq_mul_right PA000M one_mul

Proof neighborhood

Direct dependencies

PA001Y mod_eq_mul_right PA000M one_mul

Direct dependents

PA00BJ prime_factorial_wilson_congruence

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  1. 0001intro p
  2. 0002intro P
  3. 0003intro n
  4. 0004intro F
  5. 0005intro hproduct
  6. 0006intro hmod
  7. 0007have hscaled : exists wpp_mod_left_wer_mod_scaled wpp_mod_right_wer_mod_scaled. (P * n) + p * wpp_mod_left_wer_mod_scaled = (1 * n) + p * wpp_mod_right_wer_mod_scaled
  8. 0008specialize mod_eq_mul_right p
  9. 0009specialize mod_eq_mul_right P
  10. 0010specialize mod_eq_mul_right 1
  11. 0011specialize mod_eq_mul_right n
  12. 0012apply mod_eq_mul_right
  13. 0013exact hmod
  14. 0014have hone : 1 * n = n
  15. 0015specialize one_mul n
  16. 0016exact one_mul
  17. 0017rewrite hone at hscaled
  18. 0018rewrite hproduct
  19. 0019exact hscaled