PA00BI

mod_one_product_restore_predecessor

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

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

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-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

Read the argument

Proof checkpoints

19 script commands · 3 reading checkpoints · 2 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (2)
mod eq mul rightone mul
01Fix variables and assumptionsL1–6

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro P
  3. L3
    intro n
  4. L4
    intro F
  5. L5
    intro hproduct
  6. L6
    intro hmod
02Establish hscaledL7–13

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq mul right.

  1. L7
    have 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
  2. L8
    specialize mod_eq_mul_right p
  3. L9
    specialize mod_eq_mul_right P
  4. L10
    specialize mod_eq_mul_right 1
  5. L11
    specialize mod_eq_mul_right n
  6. L12
    apply mod_eq_mul_right
  7. L13
    exact hmod
03Establish honeL14–19

Establish this local claim before using it. It is not an additional assumption.

  1. L14
    have hone : 1 * n = n
  2. L15
    specialize one_mul n
  3. L16
    exact one_mul
  4. L17
    rewrite hone at hscaled
  5. L18
    rewrite hproduct
  6. L19
    exact hscaled

Library-wide reading audit

Original exact command ledger · 19 lines
  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