PA00D1 · theorem

mod_eq_add_cancel_left

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

Balanced congruence cancels a common additive left term constructively.

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

∀ d. ∀ a. ∀ b. ∀ c. ModEq(d,a + b,a + c) → ModEq(d,b,c)

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

none

0 occurrences

Exact expanded native-PA statement
forall d a b c. (exists fspm_u_cancel_input fspm_v_cancel_input. (a + b) + d * fspm_u_cancel_input = (a + c) + d * fspm_v_cancel_input) -> (exists fspm_u_cancel_result fspm_v_cancel_result. (b) + d * fspm_u_cancel_result = (c) + d * fspm_v_cancel_result)

Proof neighborhood

Direct theorem prerequisites

PA002B add_left_cancel PA0009 add_assoc

Direct theorem dependents

PA00D2 mod_two_cancel_middle

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 · 8 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 (2)
add left canceladd assoc
01Fix variables and assumptionsL1–5

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

  1. L1
    intro d
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro hmod
02Separate the logical casesL6–7

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

  1. L6
    cases hmod
  2. L7
    cases hmod_witness
03Construct an explicit witnessL8–9

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

  1. L8
    exists x
  2. L9
    exists x1
04Use earlier factsL10–13

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

  1. L10
    specialize add_left_cancel a
  2. L11
    specialize add_left_cancel (b + d * x)
  3. L12
    specialize add_left_cancel (c + d * x1)
  4. L13
    apply add_left_cancel
05Calculate and transport equalitiesL14–15

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

  1. L14
    trans (a + b) + d * x
  2. L15
    symm
06Use earlier factsL16–16

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

  1. L16
    apply add_assoc
07Calculate and transport equalitiesL17–17

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

  1. L17
    trans (a + c) + d * x1
08Use earlier factsL18–19

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

  1. L18
    exact hmod_witness_witness
  2. L19
    apply add_assoc

Library-wide reading audit

Original defined command ledger · 19 lines
  1. 0001intro d
  2. 0002intro a
  3. 0003intro b
  4. 0004intro c
  5. 0005intro hmod
  6. 0006cases hmod
  7. 0007cases hmod_witness
  8. 0008exists x
  9. 0009exists x1
  10. 0010specialize add_left_cancel a
  11. 0011specialize add_left_cancel (b + d * x)
  12. 0012specialize add_left_cancel (c + d * x1)
  13. 0013apply add_left_cancel
  14. 0014trans (a + b) + d * x
  15. 0015symm
  16. 0016apply add_assoc
  17. 0017trans (a + c) + d * x1
  18. 0018exact hmod_witness_witness
  19. 0019apply add_assoc