EU0017

euler_unit_product_coprime

The entire actual unit-weighted product is coprime to m; this is the proved cancellation premise.

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

∀ l. ∀ m. ∀ b. ∀ c. ∀ P. UnitProductPrefix(m,b,c,l) → Product(b,c,l,P) → Coprime(P,m)

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

Definition DAG

UnitProductPrefix(m,b,c,l) · 1Coprime(a,b) · 1BetaAt(b,c,i,x) · 1Product(b,c,l,z) · 2

Actual proof prerequisites

beta_product_zero · checked external prerequisitecoprime_one_left · checked external prerequisitebeta_product_succ_decompose · checked external prerequisiteeuler_unit_product_prefix_drop_lasteuler_unit_product_prefix_entryeuler_unit_product_factor_coprimecoprime_mul_left · checked external prerequisitele_refl · checked external prerequisite
Original expanded first-order statement 
forall l m b c P. (forall eu_factor_index_product_coprime_factors. (exists eut_gap_eu_product_coprime_factors_index. eut_gap_eu_product_coprime_factors_index + S (eu_factor_index_product_coprime_factors) = (l)) -> exists eu_factor_value_product_coprime_factors. (((exists fs_h_eu_product_coprime_factors_at. fs_h_eu_product_coprime_factors_at + S (eu_factor_value_product_coprime_factors) = S ((S (eu_factor_index_product_coprime_factors)) * c)) /\ exists fs_q_eu_product_coprime_factors_at. b = fs_q_eu_product_coprime_factors_at * S ((S (eu_factor_index_product_coprime_factors)) * c) + (eu_factor_value_product_coprime_factors))) /\ ((((forall eut_divisor_eu_product_coprime_factors_choice_coprime. (exists eut_left_eu_product_coprime_factors_choice_coprime. (eu_factor_index_product_coprime_factors) = eut_divisor_eu_product_coprime_factors_choice_coprime * eut_left_eu_product_coprime_factors_choice_coprime) -> (exists eut_right_eu_product_coprime_factors_choice_coprime. (m) = eut_divisor_eu_product_coprime_factors_choice_coprime * eut_right_eu_product_coprime_factors_choice_coprime) -> eut_divisor_eu_product_coprime_factors_choice_coprime = 1) /\ (eu_factor_value_product_coprime_factors)=(eu_factor_index_product_coprime_factors)) \/ (~(forall eut_divisor_eu_product_coprime_factors_choice_coprime. (exists eut_left_eu_product_coprime_factors_choice_coprime. (eu_factor_index_product_coprime_factors) = eut_divisor_eu_product_coprime_factors_choice_coprime * eut_left_eu_product_coprime_factors_choice_coprime) -> (exists eut_right_eu_product_coprime_factors_choice_coprime. (m) = eut_divisor_eu_product_coprime_factors_choice_coprime * eut_right_eu_product_coprime_factors_choice_coprime) -> eut_divisor_eu_product_coprime_factors_choice_coprime = 1) /\ (eu_factor_value_product_coprime_factors)=1)))) -> (exists ff_u_fsat_eu_product_coprime ff_v_fsat_eu_product_coprime. ((((exists ff_h_fsat_eu_product_coprime_start. ff_h_fsat_eu_product_coprime_start + S (1) = S ((S (0)) * ff_v_fsat_eu_product_coprime)) /\ exists ff_q_fsat_eu_product_coprime_start. ff_u_fsat_eu_product_coprime = ff_q_fsat_eu_product_coprime_start * S ((S (0)) * ff_v_fsat_eu_product_coprime) + (1))) /\ ((((exists ff_h_fsat_eu_product_coprime_terminal. ff_h_fsat_eu_product_coprime_terminal + S (P) = S ((S (l)) * ff_v_fsat_eu_product_coprime)) /\ exists ff_q_fsat_eu_product_coprime_terminal. ff_u_fsat_eu_product_coprime = ff_q_fsat_eu_product_coprime_terminal * S ((S (l)) * ff_v_fsat_eu_product_coprime) + (P))) /\ forall ff_i_fsat_eu_product_coprime. (exists ff_lt_fsat_eu_product_coprime_bound. ff_lt_fsat_eu_product_coprime_bound + S ff_i_fsat_eu_product_coprime = l) -> exists ff_p_fsat_eu_product_coprime ff_r_fsat_eu_product_coprime ff_s_fsat_eu_product_coprime. ((((exists ff_h_fsat_eu_product_coprime_factor. ff_h_fsat_eu_product_coprime_factor + S (ff_p_fsat_eu_product_coprime) = S ((S (ff_i_fsat_eu_product_coprime)) * c)) /\ exists ff_q_fsat_eu_product_coprime_factor. b = ff_q_fsat_eu_product_coprime_factor * S ((S (ff_i_fsat_eu_product_coprime)) * c) + (ff_p_fsat_eu_product_coprime))) /\ ((((exists ff_h_fsat_eu_product_coprime_partial. ff_h_fsat_eu_product_coprime_partial + S (ff_r_fsat_eu_product_coprime) = S ((S (ff_i_fsat_eu_product_coprime)) * ff_v_fsat_eu_product_coprime)) /\ exists ff_q_fsat_eu_product_coprime_partial. ff_u_fsat_eu_product_coprime = ff_q_fsat_eu_product_coprime_partial * S ((S (ff_i_fsat_eu_product_coprime)) * ff_v_fsat_eu_product_coprime) + (ff_r_fsat_eu_product_coprime))) /\ ((((exists ff_h_fsat_eu_product_coprime_successor. ff_h_fsat_eu_product_coprime_successor + S (ff_s_fsat_eu_product_coprime) = S ((S (S ff_i_fsat_eu_product_coprime)) * ff_v_fsat_eu_product_coprime)) /\ exists ff_q_fsat_eu_product_coprime_successor. ff_u_fsat_eu_product_coprime = ff_q_fsat_eu_product_coprime_successor * S ((S (S ff_i_fsat_eu_product_coprime)) * ff_v_fsat_eu_product_coprime) + (ff_s_fsat_eu_product_coprime))) /\ ff_s_fsat_eu_product_coprime = ff_r_fsat_eu_product_coprime * ff_p_fsat_eu_product_coprime)))))) -> (forall eut_divisor_eu_product_coprime. (exists eut_left_eu_product_coprime. (P) = eut_divisor_eu_product_coprime * eut_left_eu_product_coprime) -> (exists eut_right_eu_product_coprime. (m) = eut_divisor_eu_product_coprime * eut_right_eu_product_coprime) -> eut_divisor_eu_product_coprime = 1)

Complete tactic proof in conservative notation

All 65 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

65 script commands · 10 reading checkpoints · 2 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)
euler unit product prefix drop lasteuler unit product factor coprimeeuler unit product prefix entry
01Induction on lL1–7

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L1
    induction l
  2. L2
    intro m
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro P
  6. L6
    intro hf
  7. L7
    intro hP
02Establish heL8–17

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta product zero.

  1. L8
    have he : P=1
  2. L9
    specialize beta_product_zero (b)
  3. L10
    specialize beta_product_zero (c)
  4. L11
    specialize beta_product_zero (P)
  5. L12
    apply beta_product_zero
  6. L13
    exact hP
  7. L14
    rewrite he
  8. L15
    specialize coprime_one_left (m)
  9. L16
    apply coprime_one_left
  10. L17
    intro m
03Fix variables and assumptionsL18–22

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

  1. L18
    intro b
  2. L19
    intro c
  3. L20
    intro P
  4. L21
    intro hf
  5. L22
    intro hP
04Establish hdL23–29

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta product succ decompose.

  1. L23
    have hd : ∃ v. ∃ Q. BetaAt(b,c,l,v) ∧ (Product(b,c,l,Q) ∧ P = Q · v)Definitions: BetaAt(b,c,l,v)Product(b,c,l,Q)Original native command in the exact edition
  2. L24
    specialize beta_product_succ_decompose (b)
  3. L25
    specialize beta_product_succ_decompose (c)
  4. L26
    specialize beta_product_succ_decompose (l)
  5. L27
    specialize beta_product_succ_decompose (P)
  6. L28
    apply beta_product_succ_decompose
  7. L29
    exact hP
05Separate the logical casesL30–33

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

  1. L30
    cases hd
  2. L31
    cases hd_witness
  3. L32
    cases hd_witness_witness
  4. L33
    cases hd_witness_witness_right
06Calculate and transport equalitiesL34–34

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

  1. L34
    rewrite hd_witness_witness_right_right
07Use earlier factsL35–44

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

  1. L35
    specialize coprime_mul_left (x1)
  2. L36
    specialize coprime_mul_left (x)
  3. L37
    specialize coprime_mul_left (m)
  4. L38
    apply coprime_mul_left
  5. L39
    specialize IH (m)
  6. L40
    specialize IH (b)
  7. L41
    specialize IH (c)
  8. L42
    specialize IH (x1)
  9. L43
    apply IH
  10. L44
    specialize euler_unit_product_prefix_drop_last (m)
08Use earlier factsL45–54

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

  1. L45
    specialize euler_unit_product_prefix_drop_last (b)
  2. L46
    specialize euler_unit_product_prefix_drop_last (c)
  3. L47
    specialize euler_unit_product_prefix_drop_last (l)
  4. L48
    apply euler_unit_product_prefix_drop_last
  5. L49
    exact hf
  6. L50
    exact hd_witness_witness_right_left
  7. L51
    specialize euler_unit_product_factor_coprime (m)
  8. L52
    specialize euler_unit_product_factor_coprime (l)
  9. L53
    specialize euler_unit_product_factor_coprime (x)
  10. L54
    apply euler_unit_product_factor_coprime
09Use earlier factsL55–64

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

  1. L55
    specialize euler_unit_product_prefix_entry (m)
  2. L56
    specialize euler_unit_product_prefix_entry (b)
  3. L57
    specialize euler_unit_product_prefix_entry (c)
  4. L58
    specialize euler_unit_product_prefix_entry (S l)
  5. L59
    specialize euler_unit_product_prefix_entry (l)
  6. L60
    specialize euler_unit_product_prefix_entry (x)
  7. L61
    apply euler_unit_product_prefix_entry
  8. L62
    exact hf
  9. L63
    specialize le_refl (S l)
  10. L64
    apply le_refl
10Use earlier factsL65–65

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

  1. L65
    exact hd_witness_witness_left

Library-wide reading audit

Original defined command ledger · 65 lines
  1. 0001induction l
  2. 0002intro m
  3. 0003intro b
  4. 0004intro c
  5. 0005intro P
  6. 0006intro hf
  7. 0007intro hP
  8. 0008have he : P=1
  9. 0009specialize beta_product_zero (b)
  10. 0010specialize beta_product_zero (c)
  11. 0011specialize beta_product_zero (P)
  12. 0012apply beta_product_zero
  13. 0013exact hP
  14. 0014rewrite he
  15. 0015specialize coprime_one_left (m)
  16. 0016apply coprime_one_left
  17. 0017intro m
  18. 0018intro b
  19. 0019intro c
  20. 0020intro P
  21. 0021intro hf
  22. 0022intro hP
  23. 0023have hd : ∃ v. ∃ Q. BetaAt(b,c,l,v) ∧ (Product(b,c,l,Q) ∧ P = Q · v)
  24. 0024specialize beta_product_succ_decompose (b)
  25. 0025specialize beta_product_succ_decompose (c)
  26. 0026specialize beta_product_succ_decompose (l)
  27. 0027specialize beta_product_succ_decompose (P)
  28. 0028apply beta_product_succ_decompose
  29. 0029exact hP
  30. 0030cases hd
  31. 0031cases hd_witness
  32. 0032cases hd_witness_witness
  33. 0033cases hd_witness_witness_right
  34. 0034rewrite hd_witness_witness_right_right
  35. 0035specialize coprime_mul_left (x1)
  36. 0036specialize coprime_mul_left (x)
  37. 0037specialize coprime_mul_left (m)
  38. 0038apply coprime_mul_left
  39. 0039specialize IH (m)
  40. 0040specialize IH (b)
  41. 0041specialize IH (c)
  42. 0042specialize IH (x1)
  43. 0043apply IH
  44. 0044specialize euler_unit_product_prefix_drop_last (m)
  45. 0045specialize euler_unit_product_prefix_drop_last (b)
  46. 0046specialize euler_unit_product_prefix_drop_last (c)
  47. 0047specialize euler_unit_product_prefix_drop_last (l)
  48. 0048apply euler_unit_product_prefix_drop_last
  49. 0049exact hf
  50. 0050exact hd_witness_witness_right_left
  51. 0051specialize euler_unit_product_factor_coprime (m)
  52. 0052specialize euler_unit_product_factor_coprime (l)
  53. 0053specialize euler_unit_product_factor_coprime (x)
  54. 0054apply euler_unit_product_factor_coprime
  55. 0055specialize euler_unit_product_prefix_entry (m)
  56. 0056specialize euler_unit_product_prefix_entry (b)
  57. 0057specialize euler_unit_product_prefix_entry (c)
  58. 0058specialize euler_unit_product_prefix_entry (S l)
  59. 0059specialize euler_unit_product_prefix_entry (l)
  60. 0060specialize euler_unit_product_prefix_entry (x)
  61. 0061apply euler_unit_product_prefix_entry
  62. 0062exact hf
  63. 0063specialize le_refl (S l)
  64. 0064apply le_refl
  65. 0065exact hd_witness_witness_left