PA0022 · theorem

mod_eq_add

Stable checked-use theorem · independently closed

Balanced natural congruence respects addition.

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. ∀ a. ∀ b. ∀ c. ∀ d. ModEq(m,a,b) → ModEq(m,c,d) → ModEq(m,a + c,b + d)

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

3 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall m a b c d. (exists u v. a + m * u = b + m * v) -> (exists r s. c + m * r = d + m * s) -> exists x y. (a + c) + m * x = (b + d) + m * y

Proof neighborhood

Direct theorem prerequisites

PA000A mul_add PA000F add_comm PA001I add_permute_outer

Direct theorem dependents

PA0026 binary_crt PA003Q coprime_mod_inverse PA007B gauss_mixed_sign_scaled_source_impossible PA00CM signed_remainder_sum_mod_two PA00CQ beta_sum_pointwise_mod_three_add PA00FH gauss_count_sum_mod_two_from_quotient_sums

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

42 script commands · 21 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 (3)
mul addadd commadd permute outer
01Fix variables and assumptionsL1–7

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

  1. L1
    intro m
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro d
  6. L6
    intro hab
  7. L7
    intro hcd
02Separate the logical casesL8–11

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

  1. L8
    cases hab
  2. L9
    cases hab_witness
  3. L10
    cases hcd
  4. L11
    cases hcd_witness
03Construct an explicit witnessL12–13

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

  1. L12
    exists x2 + x
  2. L13
    exists x3 + x1
04Calculate and transport equalitiesL14–16

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

  1. L14
    trans (a + c) + (m * x2 + m * x)
  2. L15
    congr
  3. L16
    refl
05Use earlier factsL17–17

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

  1. L17
    apply mul_add
06Calculate and transport equalitiesL18–18

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

  1. L18
    trans (m * x2 + c) + (a + m * x)
07Use earlier factsL19–19

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

  1. L19
    apply add_permute_outer
08Calculate and transport equalitiesL20–21

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

  1. L20
    trans (c + m * x2) + (a + m * x)
  2. L21
    congr
09Use earlier factsL22–22

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

  1. L22
    apply add_comm
10Calculate and transport equalitiesL23–24

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

  1. L23
    refl
  2. L24
    trans (a + m * x) + (c + m * x2)
11Use earlier factsL25–25

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

  1. L25
    apply add_comm
12Calculate and transport equalitiesL26–27

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

  1. L26
    trans (b + m * x1) + (d + m * x3)
  2. L27
    congr
13Use earlier factsL28–29

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

  1. L28
    exact hab_witness_witness
  2. L29
    exact hcd_witness_witness
14Calculate and transport equalitiesL30–30

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

  1. L30
    trans (d + m * x3) + (b + m * x1)
15Use earlier factsL31–31

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

  1. L31
    apply add_comm
16Calculate and transport equalitiesL32–33

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

  1. L32
    trans (m * x3 + d) + (b + m * x1)
  2. L33
    congr
17Use earlier factsL34–34

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

  1. L34
    apply add_comm
18Calculate and transport equalitiesL35–37

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

  1. L35
    refl
  2. L36
    trans (b + d) + (m * x3 + m * x1)
  3. L37
    symm
19Use earlier factsL38–38

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

  1. L38
    apply add_permute_outer
20Calculate and transport equalitiesL39–41

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

  1. L39
    congr
  2. L40
    refl
  3. L41
    symm
21Use earlier factsL42–42

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

  1. L42
    apply mul_add

Library-wide reading audit

Original defined command ledger · 42 lines
  1. 0001intro m
  2. 0002intro a
  3. 0003intro b
  4. 0004intro c
  5. 0005intro d
  6. 0006intro hab
  7. 0007intro hcd
  8. 0008cases hab
  9. 0009cases hab_witness
  10. 0010cases hcd
  11. 0011cases hcd_witness
  12. 0012exists x2 + x
  13. 0013exists x3 + x1
  14. 0014trans (a + c) + (m * x2 + m * x)
  15. 0015congr
  16. 0016refl
  17. 0017apply mul_add
  18. 0018trans (m * x2 + c) + (a + m * x)
  19. 0019apply add_permute_outer
  20. 0020trans (c + m * x2) + (a + m * x)
  21. 0021congr
  22. 0022apply add_comm
  23. 0023refl
  24. 0024trans (a + m * x) + (c + m * x2)
  25. 0025apply add_comm
  26. 0026trans (b + m * x1) + (d + m * x3)
  27. 0027congr
  28. 0028exact hab_witness_witness
  29. 0029exact hcd_witness_witness
  30. 0030trans (d + m * x3) + (b + m * x1)
  31. 0031apply add_comm
  32. 0032trans (m * x3 + d) + (b + m * x1)
  33. 0033congr
  34. 0034apply add_comm
  35. 0035refl
  36. 0036trans (b + d) + (m * x3 + m * x1)
  37. 0037symm
  38. 0038apply add_permute_outer
  39. 0039congr
  40. 0040refl
  41. 0041symm
  42. 0042apply mul_add