PA0024 · theorem

mod_eq_trans

Stable checked-use theorem · independently closed

Balanced natural congruence is transitive.

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

3 occurrences

In local proof propositions

none

0 occurrences

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

Proof neighborhood

Direct theorem prerequisites

PA0009 add_assoc PA000F add_comm PA000A mul_add

Direct theorem dependents

PA0026 binary_crt PA0028 binary_crt_fold_step PA002V mod_eq_to_remainder_decomposition PA003Q coprime_mod_inverse PA003R mod_eq_cancel_coprime PA004E mod_eq_mul PA005E pow_predecessor_parity_mod PA005J mod_eq_decidable_from_remainders PA005R quadratic_residue_bounded_equiv PA0063 prime_bounded_nonzero_mod_inverse PA00AK bounded_mod_inverse_unique PA0070 gauss_pointwise_signed_half_representative PA0079 prime_scaled_same_target_unique PA007B gauss_mixed_sign_scaled_source_impossible PA0087 quadratic_residue_mod_equiv PA008E prime_mul_index_map_injective PA008M quadratic_residue_half_power_mod_one PA008O scaled_inverse_transport_right PA009C prime_scaled_inverse_unique PA00BK scaled_pair_order_terminal_power_mod_predecessor PA00BQ bounded_euler_criterion_residue_iff PA00BR arbitrary_euler_criterion_residue_iff PA00BS bounded_euler_criterion_nonresidue_iff PA00BT arbitrary_euler_criterion_nonresidue_iff PA00BV arbitrary_gauss_lemma_complete PA00C5 canonical_remainder_from_mod PA00C6 odd_signed_division_branch_exact PA00CJ matching_parity_mod_two PA00CN odd_scaled_division_signed_mod_two PA00FL mod_two_preserves_parity

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)
add assocadd commmul add
01Fix variables and assumptionsL1–6

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 hab
  6. L6
    intro hbc
02Separate the logical casesL7–10

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

  1. L7
    cases hab
  2. L8
    cases hab_witness
  3. L9
    cases hbc
  4. L10
    cases hbc_witness
03Construct an explicit witnessL11–12

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

  1. L11
    exists x + x2
  2. L12
    exists x3 + x1
04Calculate and transport equalitiesL13–15

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

  1. L13
    trans a + (m * x + m * x2)
  2. L14
    congr
  3. L15
    refl
05Use earlier factsL16–16

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

  1. L16
    apply mul_add
06Calculate and transport equalitiesL17–18

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

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

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

  1. L19
    apply add_assoc
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 (b + m * x1) + m * x2
  2. L21
    congr
09Use earlier factsL22–22

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

  1. L22
    exact hab_witness_witness
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 b + (m * x1 + m * x2)
11Use earlier factsL25–25

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

  1. L25
    apply add_assoc
12Calculate and transport equalitiesL26–28

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

  1. L26
    trans b + (m * x2 + m * x1)
  2. L27
    congr
  3. L28
    refl
13Use earlier factsL29–29

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

  1. L29
    apply add_comm
14Calculate and transport equalitiesL30–31

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

  1. L30
    trans (b + m * x2) + m * x1
  2. L31
    symm
15Use earlier factsL32–32

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

  1. L32
    apply add_assoc
16Calculate and transport equalitiesL33–34

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

  1. L33
    trans (c + m * x3) + m * x1
  2. L34
    congr
17Use earlier factsL35–35

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

  1. L35
    exact hbc_witness_witness
18Calculate and transport equalitiesL36–37

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

  1. L36
    refl
  2. L37
    trans c + (m * x3 + m * x1)
19Use earlier factsL38–38

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

  1. L38
    apply add_assoc
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 hab
  6. 0006intro hbc
  7. 0007cases hab
  8. 0008cases hab_witness
  9. 0009cases hbc
  10. 0010cases hbc_witness
  11. 0011exists x + x2
  12. 0012exists x3 + x1
  13. 0013trans a + (m * x + m * x2)
  14. 0014congr
  15. 0015refl
  16. 0016apply mul_add
  17. 0017trans (a + m * x) + m * x2
  18. 0018symm
  19. 0019apply add_assoc
  20. 0020trans (b + m * x1) + m * x2
  21. 0021congr
  22. 0022exact hab_witness_witness
  23. 0023refl
  24. 0024trans b + (m * x1 + m * x2)
  25. 0025apply add_assoc
  26. 0026trans b + (m * x2 + m * x1)
  27. 0027congr
  28. 0028refl
  29. 0029apply add_comm
  30. 0030trans (b + m * x2) + m * x1
  31. 0031symm
  32. 0032apply add_assoc
  33. 0033trans (c + m * x3) + m * x1
  34. 0034congr
  35. 0035exact hbc_witness_witness
  36. 0036refl
  37. 0037trans c + (m * x3 + m * x1)
  38. 0038apply add_assoc
  39. 0039congr
  40. 0040refl
  41. 0041symm
  42. 0042apply mul_add