PA003L · theorem

mod_eq_symm

Stable checked-use theorem · independently closed

Balanced natural congruence is symmetric.

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

PD0008 ModEq

2 occurrences

In local proof propositions

none

0 occurrences

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

Proof neighborhood

Direct theorem prerequisites

none

Direct theorem dependents

PA003R mod_eq_cancel_coprime PA005J mod_eq_decidable_from_remainders PA005R quadratic_residue_bounded_equiv PA0063 prime_bounded_nonzero_mod_inverse PA00AK bounded_mod_inverse_unique PA0079 prime_scaled_same_target_unique 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 PA00CJ matching_parity_mod_two PA00D5 mod_two_zero_sum_to_congruent PA00D7 odd_prime_gauss_eisenstein_orientation_data_exists 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

10 script commands · 5 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.

01Fix variables and assumptionsL1–4

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 h
02Separate the logical casesL5–6

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

  1. L5
    cases h
  2. L6
    cases h_witness
03Construct an explicit witnessL7–8

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

  1. L7
    exists x1
  2. L8
    exists x
04Calculate and transport equalitiesL9–9

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

  1. L9
    symm
05Use earlier factsL10–10

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

  1. L10
    exact h_witness_witness

Library-wide reading audit

Original defined command ledger · 10 lines
  1. 0001intro m
  2. 0002intro a
  3. 0003intro b
  4. 0004intro h
  5. 0005cases h
  6. 0006cases h_witness
  7. 0007exists x1
  8. 0008exists x
  9. 0009symm
  10. 0010exact h_witness_witness