PA0027 · theorem

mod_eq_of_mod_eq_multiple

Stable checked-use theorem · independently closed

Balanced congruence descends from a multiple modulus to every divisor modulus.

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

∀ m. ∀ P. ∀ x. ∀ a. Dvd(m,P) → ModEq(P,x,a) → ModEq(m,x,a)

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

PD0003 Dvd PD0008 ModEq

3 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall m P x a. (exists k. P = m * k) -> (exists u v. x + P * u = a + P * v) -> exists r s. x + m * r = a + m * s

Proof neighborhood

Direct theorem prerequisites

PA000B mul_assoc

Direct theorem dependents

PA0028 binary_crt_fold_step

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

23 script commands · 10 reading checkpoints · 0 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 (1)
mul assoc
01Fix variables and assumptionsL1–6

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

  1. L1
    intro m
  2. L2
    intro P
  3. L3
    intro x
  4. L4
    intro a
  5. L5
    intro hdiv
  6. L6
    intro hmod
02Separate the logical casesL7–9

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L7
    cases hdiv
  2. L8
    cases hmod
  3. L9
    cases hmod_witness
03Calculate and transport equalitiesL10–11

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L10
    rewrite hdiv_witness at hmod_witness_witness
  2. L11
    rewrite hdiv_witness at hmod_witness_witness
04Construct an explicit witnessL12–13

Supply the displayed value, then prove that it has the required property.

  1. L12
    exists x1 * x2
  2. L13
    exists x1 * x3
05Calculate and transport equalitiesL14–17

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L14
    trans x + (m * x1) * x2
  2. L15
    congr
  3. L16
    refl
  4. L17
    symm
06Use earlier factsL18–18

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L18
    apply mul_assoc
07Calculate and transport equalitiesL19–19

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L19
    trans a + (m * x1) * x3
08Use earlier factsL20–20

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L20
    exact hmod_witness_witness
09Calculate and transport equalitiesL21–22

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L21
    congr
  2. L22
    refl
10Use earlier factsL23–23

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L23
    apply mul_assoc

Library-wide reading audit

Original defined command ledger · 23 lines
  1. 0001intro m
  2. 0002intro P
  3. 0003intro x
  4. 0004intro a
  5. 0005intro hdiv
  6. 0006intro hmod
  7. 0007cases hdiv
  8. 0008cases hmod
  9. 0009cases hmod_witness
  10. 0010rewrite hdiv_witness at hmod_witness_witness
  11. 0011rewrite hdiv_witness at hmod_witness_witness
  12. 0012exists x1 * x2
  13. 0013exists x1 * x3
  14. 0014trans x + (m * x1) * x2
  15. 0015congr
  16. 0016refl
  17. 0017symm
  18. 0018apply mul_assoc
  19. 0019trans a + (m * x1) * x3
  20. 0020exact hmod_witness_witness
  21. 0021congr
  22. 0022refl
  23. 0023apply mul_assoc