PA00BI · theorem

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.

Statement with defined notation

∀ p. ∀ P. ∀ n. ∀ F. F = P · n → ModEq(p,P,1) → ModEq(p,F,n)

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0008 ModEq

2 occurrences

In local proof propositions

PD0008 ModEq

1 occurrences

Exact expanded native-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)

Proof neighborhood

Direct theorem prerequisites

PA001Y mod_eq_mul_right PA000M one_mul

Direct theorem dependents

PA00BJ prime_factorial_wilson_congruence

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 : ModEq(p,P · n,1 · n)Definitions: ModEq(p,P · n,1 · n)Original native command in the exact edition
  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 defined 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 : ModEq(p,P · n,1 · n)
    Exact native replay linehave 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