EU0002

euler_multiplier_coprime_iff

Multiplication by a coprime multiplier preserves and reflects precisely the unit predicate used by Phi.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

The exact G014 theorem covers m>1 and genuinely invertible a. Phi counts coprime residues independently of the conclusion. The broader coprime theorem handles m=1 by congruence, not by asserting that one is a canonical remainder. Multiplicative-order and RSA statements are not claimed.

Exact theorem in conservative defined notation

∀ a. ∀ m. ∀ i. ∀ r. Coprime(a,m) → ModEq(m,a · i,r) → (Coprime(i,m) → Coprime(r,m)) ∧ (Coprime(r,m) → Coprime(i,m))

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

Coprime(a,b) · 9ModEq(m,a,b) · 1

Actual proof prerequisites

euler_coprime_mod_transportcoprime_mul_left · checked external prerequisitetotient_coprime_cancel_unit_factor · checked external prerequisitemod_eq_symm · checked external prerequisite
Original expanded first-order statement 
forall a m i r. (forall eut_divisor_eu_multiplier_unit. (exists eut_left_eu_multiplier_unit. (a) = eut_divisor_eu_multiplier_unit * eut_left_eu_multiplier_unit) -> (exists eut_right_eu_multiplier_unit. (m) = eut_divisor_eu_multiplier_unit * eut_right_eu_multiplier_unit) -> eut_divisor_eu_multiplier_unit = 1) -> (exists eu_mod_left_multiplier_congruence eu_mod_right_multiplier_congruence. (a*i) + (m) * eu_mod_left_multiplier_congruence = (r) + (m) * eu_mod_right_multiplier_congruence) -> (((forall eut_divisor_eu_source_unit. (exists eut_left_eu_source_unit. (i) = eut_divisor_eu_source_unit * eut_left_eu_source_unit) -> (exists eut_right_eu_source_unit. (m) = eut_divisor_eu_source_unit * eut_right_eu_source_unit) -> eut_divisor_eu_source_unit = 1) -> (forall eut_divisor_eu_target_unit. (exists eut_left_eu_target_unit. (r) = eut_divisor_eu_target_unit * eut_left_eu_target_unit) -> (exists eut_right_eu_target_unit. (m) = eut_divisor_eu_target_unit * eut_right_eu_target_unit) -> eut_divisor_eu_target_unit = 1)) /\ ((forall eut_divisor_eu_target_unit_back. (exists eut_left_eu_target_unit_back. (r) = eut_divisor_eu_target_unit_back * eut_left_eu_target_unit_back) -> (exists eut_right_eu_target_unit_back. (m) = eut_divisor_eu_target_unit_back * eut_right_eu_target_unit_back) -> eut_divisor_eu_target_unit_back = 1) -> (forall eut_divisor_eu_source_unit_back. (exists eut_left_eu_source_unit_back. (i) = eut_divisor_eu_source_unit_back * eut_left_eu_source_unit_back) -> (exists eut_right_eu_source_unit_back. (m) = eut_divisor_eu_source_unit_back * eut_right_eu_source_unit_back) -> eut_divisor_eu_source_unit_back = 1)))

Complete tactic proof in conservative notation

All 38 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

38 script commands · 11 reading checkpoints · 1 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)
euler coprime mod transport
01Fix variables and assumptionsL1–6

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

  1. L1
    intro a
  2. L2
    intro m
  3. L3
    intro i
  4. L4
    intro r
  5. L5
    intro ha
  6. L6
    intro hmod
02Separate the logical casesL7–7

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

  1. L7
    split
03Fix variables and assumptionsL8–8

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

  1. L8
    intro hi
04Use earlier factsL9–18

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

  1. L9
    specialize euler_coprime_mod_transport (m)
  2. L10
    specialize euler_coprime_mod_transport (a*i)
  3. L11
    specialize euler_coprime_mod_transport (r)
  4. L12
    apply euler_coprime_mod_transport
  5. L13
    specialize coprime_mul_left (a)
  6. L14
    specialize coprime_mul_left (i)
  7. L15
    specialize coprime_mul_left (m)
  8. L16
    apply coprime_mul_left
  9. L17
    exact ha
  10. L18
    exact hi
05Use earlier factsL19–19

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

  1. L19
    exact hmod
06Fix variables and assumptionsL20–20

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

  1. L20
    intro hr
07Use earlier factsL21–23

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

  1. L21
    specialize totient_coprime_cancel_unit_factor a
  2. L22
    specialize totient_coprime_cancel_unit_factor m
  3. L23
    specialize totient_coprime_cancel_unit_factor i
08Establish hcL24–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply totient coprime cancel unit factor.

  1. L24
    have hc : (Coprime(a · i,m) → Coprime(i,m)) ∧ (Coprime(i,m) → Coprime(a · i,m))Definitions: Coprime(a · i,m)Coprime(i,m)Original native command in the exact edition
  2. L25
    apply totient_coprime_cancel_unit_factor
  3. L26
    exact ha
09Separate the logical casesL27–27

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

  1. L27
    cases hc
10Use earlier factsL28–37

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

  1. L28
    apply hc_left
  2. L29
    specialize euler_coprime_mod_transport (m)
  3. L30
    specialize euler_coprime_mod_transport (r)
  4. L31
    specialize euler_coprime_mod_transport (a*i)
  5. L32
    apply euler_coprime_mod_transport
  6. L33
    exact hr
  7. L34
    specialize mod_eq_symm (m)
  8. L35
    specialize mod_eq_symm (a*i)
  9. L36
    specialize mod_eq_symm (r)
  10. L37
    apply mod_eq_symm
11Use earlier factsL38–38

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

  1. L38
    exact hmod

Library-wide reading audit

Original defined command ledger · 38 lines
  1. 0001intro a
  2. 0002intro m
  3. 0003intro i
  4. 0004intro r
  5. 0005intro ha
  6. 0006intro hmod
  7. 0007split
  8. 0008intro hi
  9. 0009specialize euler_coprime_mod_transport (m)
  10. 0010specialize euler_coprime_mod_transport (a*i)
  11. 0011specialize euler_coprime_mod_transport (r)
  12. 0012apply euler_coprime_mod_transport
  13. 0013specialize coprime_mul_left (a)
  14. 0014specialize coprime_mul_left (i)
  15. 0015specialize coprime_mul_left (m)
  16. 0016apply coprime_mul_left
  17. 0017exact ha
  18. 0018exact hi
  19. 0019exact hmod
  20. 0020intro hr
  21. 0021specialize totient_coprime_cancel_unit_factor a
  22. 0022specialize totient_coprime_cancel_unit_factor m
  23. 0023specialize totient_coprime_cancel_unit_factor i
  24. 0024have hc : (Coprime(a · i,m) → Coprime(i,m)) ∧ (Coprime(i,m) → Coprime(a · i,m))
  25. 0025apply totient_coprime_cancel_unit_factor
  26. 0026exact ha
  27. 0027cases hc
  28. 0028apply hc_left
  29. 0029specialize euler_coprime_mod_transport (m)
  30. 0030specialize euler_coprime_mod_transport (r)
  31. 0031specialize euler_coprime_mod_transport (a*i)
  32. 0032apply euler_coprime_mod_transport
  33. 0033exact hr
  34. 0034specialize mod_eq_symm (m)
  35. 0035specialize mod_eq_symm (a*i)
  36. 0036specialize mod_eq_symm (r)
  37. 0037apply mod_eq_symm
  38. 0038exact hmod