EU001F

euler_coprime_totient_power_value

For every positive modulus and any actual Phi and Pow values, construct all finite permutation/product witnesses and prove the Euler congruence by coprime cancellation.

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. ∀ t. ∀ w. ¬m = 0 → Coprime(a,m) → Phi(m,t) → Pow(a,t,w) → ModEq(m,w,1)

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

Definition DAG

PermutationPrefix(b,c,l) · 1Phi(n,t) · 1UnitMultiplierPrefix(a,m,b,c,l) · 1UnitProductPrefix(m,b,c,l) · 1UnitScaledPrefix(a,m,b,c,d,e,l) · 1Lt(a,b) · 1Coprime(a,b) · 1ModEq(m,a,b) · 2BetaAt(b,c,i,x) · 3Product(b,c,l,z) · 2Pow(a,e,z) · 1

Actual proof prerequisites

euler_unit_product_prefix_existsbeta_product_exists · checked external prerequisiteeuler_multiplier_permutation_existsfinite_beta_composition_exists · checked external prerequisitebeta_product_permutation_invariant · checked external prerequisiteeuler_unit_product_reindex_scaleeuler_unit_count_product_balanceeuler_unit_product_coprimeeuler_coprime_weighted_product_cancel
Original expanded first-order statement 
forall a m t w. ~(m=0) -> (forall eut_divisor_eu_endpoint_coprime. (exists eut_left_eu_endpoint_coprime. (a) = eut_divisor_eu_endpoint_coprime * eut_left_eu_endpoint_coprime) -> (exists eut_right_eu_endpoint_coprime. (m) = eut_divisor_eu_endpoint_coprime * eut_right_eu_endpoint_coprime) -> eut_divisor_eu_endpoint_coprime = 1) -> ((~((m)=0) /\ (exists eut_code_eu_endpoint_phi_count eut_scale_eu_endpoint_phi_count. (forall eut_index_eu_endpoint_phi_count_mask. (exists eut_gap_eu_endpoint_phi_count_mask_bound. eut_gap_eu_endpoint_phi_count_mask_bound + S (eut_index_eu_endpoint_phi_count_mask) = (m)) -> exists eut_bit_eu_endpoint_phi_count_mask. (((exists fs_h_eut_eu_endpoint_phi_count_mask_entry. fs_h_eut_eu_endpoint_phi_count_mask_entry + S (eut_bit_eu_endpoint_phi_count_mask) = S ((S (eut_index_eu_endpoint_phi_count_mask)) * eut_scale_eu_endpoint_phi_count)) /\ exists fs_q_eut_eu_endpoint_phi_count_mask_entry. eut_code_eu_endpoint_phi_count = fs_q_eut_eu_endpoint_phi_count_mask_entry * S ((S (eut_index_eu_endpoint_phi_count_mask)) * eut_scale_eu_endpoint_phi_count) + (eut_bit_eu_endpoint_phi_count_mask))) /\ ((((forall eut_divisor_eu_endpoint_phi_count_mask_choice_coprime. (exists eut_left_eu_endpoint_phi_count_mask_choice_coprime. (eut_index_eu_endpoint_phi_count_mask) = eut_divisor_eu_endpoint_phi_count_mask_choice_coprime * eut_left_eu_endpoint_phi_count_mask_choice_coprime) -> (exists eut_right_eu_endpoint_phi_count_mask_choice_coprime. (m) = eut_divisor_eu_endpoint_phi_count_mask_choice_coprime * eut_right_eu_endpoint_phi_count_mask_choice_coprime) -> eut_divisor_eu_endpoint_phi_count_mask_choice_coprime = 1) /\ (eut_bit_eu_endpoint_phi_count_mask) = 1) \/ (~(forall eut_divisor_eu_endpoint_phi_count_mask_choice_coprime. (exists eut_left_eu_endpoint_phi_count_mask_choice_coprime. (eut_index_eu_endpoint_phi_count_mask) = eut_divisor_eu_endpoint_phi_count_mask_choice_coprime * eut_left_eu_endpoint_phi_count_mask_choice_coprime) -> (exists eut_right_eu_endpoint_phi_count_mask_choice_coprime. (m) = eut_divisor_eu_endpoint_phi_count_mask_choice_coprime * eut_right_eu_endpoint_phi_count_mask_choice_coprime) -> eut_divisor_eu_endpoint_phi_count_mask_choice_coprime = 1) /\ (eut_bit_eu_endpoint_phi_count_mask) = 0)))) /\ (exists fs_u_eut_eu_endpoint_phi_count_sum fs_v_eut_eu_endpoint_phi_count_sum. ((((exists fs_h_eut_eu_endpoint_phi_count_sum_body_start. fs_h_eut_eu_endpoint_phi_count_sum_body_start + S (0) = S ((S (0)) * fs_v_eut_eu_endpoint_phi_count_sum)) /\ exists fs_q_eut_eu_endpoint_phi_count_sum_body_start. fs_u_eut_eu_endpoint_phi_count_sum = fs_q_eut_eu_endpoint_phi_count_sum_body_start * S ((S (0)) * fs_v_eut_eu_endpoint_phi_count_sum) + (0))) /\ ((((exists fs_h_eut_eu_endpoint_phi_count_sum_body_terminal. fs_h_eut_eu_endpoint_phi_count_sum_body_terminal + S (t) = S ((S (m)) * fs_v_eut_eu_endpoint_phi_count_sum)) /\ exists fs_q_eut_eu_endpoint_phi_count_sum_body_terminal. fs_u_eut_eu_endpoint_phi_count_sum = fs_q_eut_eu_endpoint_phi_count_sum_body_terminal * S ((S (m)) * fs_v_eut_eu_endpoint_phi_count_sum) + (t))) /\ forall fs_i_eut_eu_endpoint_phi_count_sum_body_steps. (exists fs_lt_eut_eu_endpoint_phi_count_sum_body_steps_bound. fs_lt_eut_eu_endpoint_phi_count_sum_body_steps_bound + S fs_i_eut_eu_endpoint_phi_count_sum_body_steps = m) -> exists fs_a_eut_eu_endpoint_phi_count_sum_body_steps fs_r_eut_eu_endpoint_phi_count_sum_body_steps fs_s_eut_eu_endpoint_phi_count_sum_body_steps. ((((exists fs_h_eut_eu_endpoint_phi_count_sum_body_steps_summand. fs_h_eut_eu_endpoint_phi_count_sum_body_steps_summand + S (fs_a_eut_eu_endpoint_phi_count_sum_body_steps) = S ((S (fs_i_eut_eu_endpoint_phi_count_sum_body_steps)) * eut_scale_eu_endpoint_phi_count)) /\ exists fs_q_eut_eu_endpoint_phi_count_sum_body_steps_summand. eut_code_eu_endpoint_phi_count = fs_q_eut_eu_endpoint_phi_count_sum_body_steps_summand * S ((S (fs_i_eut_eu_endpoint_phi_count_sum_body_steps)) * eut_scale_eu_endpoint_phi_count) + (fs_a_eut_eu_endpoint_phi_count_sum_body_steps))) /\ ((((exists fs_h_eut_eu_endpoint_phi_count_sum_body_steps_partial. fs_h_eut_eu_endpoint_phi_count_sum_body_steps_partial + S (fs_r_eut_eu_endpoint_phi_count_sum_body_steps) = S ((S (fs_i_eut_eu_endpoint_phi_count_sum_body_steps)) * fs_v_eut_eu_endpoint_phi_count_sum)) /\ exists fs_q_eut_eu_endpoint_phi_count_sum_body_steps_partial. fs_u_eut_eu_endpoint_phi_count_sum = fs_q_eut_eu_endpoint_phi_count_sum_body_steps_partial * S ((S (fs_i_eut_eu_endpoint_phi_count_sum_body_steps)) * fs_v_eut_eu_endpoint_phi_count_sum) + (fs_r_eut_eu_endpoint_phi_count_sum_body_steps))) /\ ((((exists fs_h_eut_eu_endpoint_phi_count_sum_body_steps_successor. fs_h_eut_eu_endpoint_phi_count_sum_body_steps_successor + S (fs_s_eut_eu_endpoint_phi_count_sum_body_steps) = S ((S (S fs_i_eut_eu_endpoint_phi_count_sum_body_steps)) * fs_v_eut_eu_endpoint_phi_count_sum)) /\ exists fs_q_eut_eu_endpoint_phi_count_sum_body_steps_successor. fs_u_eut_eu_endpoint_phi_count_sum = fs_q_eut_eu_endpoint_phi_count_sum_body_steps_successor * S ((S (S fs_i_eut_eu_endpoint_phi_count_sum_body_steps)) * fs_v_eut_eu_endpoint_phi_count_sum) + (fs_s_eut_eu_endpoint_phi_count_sum_body_steps))) /\ fs_s_eut_eu_endpoint_phi_count_sum_body_steps = fs_r_eut_eu_endpoint_phi_count_sum_body_steps + fs_a_eut_eu_endpoint_phi_count_sum_body_steps))))))))) -> (exists pa_b_euta_eu_endpoint_power pa_c_euta_eu_endpoint_power. ((forall pa_i_euta_eu_endpoint_power_repeat. (exists pa_lt_euta_eu_endpoint_power_repeat_bound. pa_lt_euta_eu_endpoint_power_repeat_bound + S pa_i_euta_eu_endpoint_power_repeat = t) -> (((exists pa_h_euta_eu_endpoint_power_repeat_decoded. pa_h_euta_eu_endpoint_power_repeat_decoded + S (a) = S ((S (pa_i_euta_eu_endpoint_power_repeat)) * pa_c_euta_eu_endpoint_power)) /\ exists pa_q_euta_eu_endpoint_power_repeat_decoded. pa_b_euta_eu_endpoint_power = pa_q_euta_eu_endpoint_power_repeat_decoded * S ((S (pa_i_euta_eu_endpoint_power_repeat)) * pa_c_euta_eu_endpoint_power) + (a)))) /\ (exists pa_u_euta_eu_endpoint_power_product pa_v_euta_eu_endpoint_power_product. ((((exists pa_h_euta_eu_endpoint_power_product_start. pa_h_euta_eu_endpoint_power_product_start + S (1) = S ((S (0)) * pa_v_euta_eu_endpoint_power_product)) /\ exists pa_q_euta_eu_endpoint_power_product_start. pa_u_euta_eu_endpoint_power_product = pa_q_euta_eu_endpoint_power_product_start * S ((S (0)) * pa_v_euta_eu_endpoint_power_product) + (1))) /\ ((((exists pa_h_euta_eu_endpoint_power_product_terminal. pa_h_euta_eu_endpoint_power_product_terminal + S (w) = S ((S (t)) * pa_v_euta_eu_endpoint_power_product)) /\ exists pa_q_euta_eu_endpoint_power_product_terminal. pa_u_euta_eu_endpoint_power_product = pa_q_euta_eu_endpoint_power_product_terminal * S ((S (t)) * pa_v_euta_eu_endpoint_power_product) + (w))) /\ forall pa_i_euta_eu_endpoint_power_product. (exists pa_lt_euta_eu_endpoint_power_product_bound. pa_lt_euta_eu_endpoint_power_product_bound + S pa_i_euta_eu_endpoint_power_product = t) -> exists pa_p_euta_eu_endpoint_power_product pa_r_euta_eu_endpoint_power_product pa_s_euta_eu_endpoint_power_product. ((((exists pa_h_euta_eu_endpoint_power_product_factor. pa_h_euta_eu_endpoint_power_product_factor + S (pa_p_euta_eu_endpoint_power_product) = S ((S (pa_i_euta_eu_endpoint_power_product)) * pa_c_euta_eu_endpoint_power)) /\ exists pa_q_euta_eu_endpoint_power_product_factor. pa_b_euta_eu_endpoint_power = pa_q_euta_eu_endpoint_power_product_factor * S ((S (pa_i_euta_eu_endpoint_power_product)) * pa_c_euta_eu_endpoint_power) + (pa_p_euta_eu_endpoint_power_product))) /\ ((((exists pa_h_euta_eu_endpoint_power_product_partial. pa_h_euta_eu_endpoint_power_product_partial + S (pa_r_euta_eu_endpoint_power_product) = S ((S (pa_i_euta_eu_endpoint_power_product)) * pa_v_euta_eu_endpoint_power_product)) /\ exists pa_q_euta_eu_endpoint_power_product_partial. pa_u_euta_eu_endpoint_power_product = pa_q_euta_eu_endpoint_power_product_partial * S ((S (pa_i_euta_eu_endpoint_power_product)) * pa_v_euta_eu_endpoint_power_product) + (pa_r_euta_eu_endpoint_power_product))) /\ ((((exists pa_h_euta_eu_endpoint_power_product_successor. pa_h_euta_eu_endpoint_power_product_successor + S (pa_s_euta_eu_endpoint_power_product) = S ((S (S pa_i_euta_eu_endpoint_power_product)) * pa_v_euta_eu_endpoint_power_product)) /\ exists pa_q_euta_eu_endpoint_power_product_successor. pa_u_euta_eu_endpoint_power_product = pa_q_euta_eu_endpoint_power_product_successor * S ((S (S pa_i_euta_eu_endpoint_power_product)) * pa_v_euta_eu_endpoint_power_product) + (pa_s_euta_eu_endpoint_power_product))) /\ pa_s_euta_eu_endpoint_power_product = pa_r_euta_eu_endpoint_power_product * pa_p_euta_eu_endpoint_power_product)))))))) -> (exists eu_mod_left_endpoint_result eu_mod_right_endpoint_result. (w) + (m) * eu_mod_left_endpoint_result = (1) + (m) * eu_mod_right_endpoint_result)

Complete tactic proof in conservative notation

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

111 script commands · 21 reading checkpoints · 8 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 (6)
euler unit product prefix existseuler multiplier permutation existseuler unit product reindex scaleeuler unit count product balanceeuler coprime weighted product canceleuler unit product coprime
01Fix variables and assumptionsL1–8

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

  1. L1
    intro a
  2. L2
    intro m
  3. L3
    intro t
  4. L4
    intro w
  5. L5
    intro hm
  6. L6
    intro ha
  7. L7
    intro ht
  8. L8
    intro hw
02Separate the logical casesL9–9

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

  1. L9
    cases ht
03Establish hfL10–13

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply euler unit product prefix exists.

  1. L10
    have hf : ∃ b. ∃ c. UnitProductPrefix(m,b,c,m)Definitions: UnitProductPrefix(m,b,c,m)Original native command in the exact edition
  2. L11
    specialize euler_unit_product_prefix_exists (m)
  3. L12
    specialize euler_unit_product_prefix_exists (m)
  4. L13
    apply euler_unit_product_prefix_exists
04Separate the logical casesL14–15

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

  1. L14
    cases hf
  2. L15
    cases hf_witness
05Establish hPL16–20

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

  1. L16
    have hP : ∃ P. Product(x,x1,m,P)Definitions: Product(x,x1,m,P)Original native command in the exact edition
  2. L17
    specialize beta_product_exists (x)
  3. L18
    specialize beta_product_exists (x1)
  4. L19
    specialize beta_product_exists (m)
  5. L20
    apply beta_product_exists
06Separate the logical casesL21–21

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

  1. L21
    cases hP
07Establish hmapL22–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply euler multiplier permutation exists.

  1. L22
    have hmap : ∃ r. ∃ s. UnitMultiplierPrefix(a,m,r,s,m) ∧ PermutationPrefix(r,s,m)Definitions: UnitMultiplierPrefix(a,m,r,s,m)PermutationPrefix(r,s,m)Original native command in the exact edition
  2. L23
    specialize euler_multiplier_permutation_exists (a)
  3. L24
    specialize euler_multiplier_permutation_exists (m)
  4. L25
    apply euler_multiplier_permutation_exists
  5. L26
    exact hm
  6. L27
    exact ha
08Separate the logical casesL28–32

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

  1. L28
    cases hmap
  2. L29
    cases hmap_witness
  3. L30
    cases hmap_witness_witness
  4. L31
    cases hmap_witness_witness_right
  5. L32
    cases hmap_witness_witness_right_right
09Establish hcompL33–39

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

  1. L33
    have hcomp : ∃ z. ∃ d. ∀ y. ∀ n. ∀ k. Lt(y,m) → BetaAt(x3,x4,y,n) → BetaAt(x,x1,n,k) → BetaAt(z,d,y,k)Definitions: Lt(y,m)BetaAt(x3,x4,y,n)BetaAt(x,x1,n,k)BetaAt(z,d,y,k)Original native command in the exact edition
  2. L34
    specialize finite_beta_composition_exists (x3)
  3. L35
    specialize finite_beta_composition_exists (x4)
  4. L36
    specialize finite_beta_composition_exists (x)
  5. L37
    specialize finite_beta_composition_exists (x1)
  6. L38
    specialize finite_beta_composition_exists (m)
  7. L39
    apply finite_beta_composition_exists
10Separate the logical casesL40–41

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

  1. L40
    cases hcomp
  2. L41
    cases hcomp_witness
11Establish hQL42–46

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

  1. L42
    have hQ : ∃ Q. Product(x5,x6,m,Q)Definitions: Product(x5,x6,m,Q)Original native command in the exact edition
  2. L43
    specialize beta_product_exists (x5)
  3. L44
    specialize beta_product_exists (x6)
  4. L45
    specialize beta_product_exists (m)
  5. L46
    apply beta_product_exists
12Separate the logical casesL47–47

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

  1. L47
    cases hQ
13Establish heL48–57

Establish this local claim before using it. It is not an additional assumption.

  1. L48
    have he : x7=x2
  2. L49
    symm
  3. L50
    specialize beta_product_permutation_invariant (m)
  4. L51
    specialize beta_product_permutation_invariant (x3)
  5. L52
    specialize beta_product_permutation_invariant (x4)
  6. L53
    specialize beta_product_permutation_invariant (x)
  7. L54
    specialize beta_product_permutation_invariant (x1)
  8. L55
    specialize beta_product_permutation_invariant (x5)
  9. L56
    specialize beta_product_permutation_invariant (x6)
  10. L57
    specialize beta_product_permutation_invariant (x2)
14Use earlier factsL58–64

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

  1. L58
    specialize beta_product_permutation_invariant (x7)
  2. L59
    apply beta_product_permutation_invariant
  3. L60
    exact hmap_witness_witness_right_left
  4. L61
    exact hmap_witness_witness_right_right_left
  5. L62
    exact hcomp_witness_witness
  6. L63
    exact hP_witness
  7. L64
    exact hQ_witness
15Establish hsL65–74

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply euler unit product reindex scale.

  1. L65
    have hs : UnitScaledPrefix(a,m,x,x1,x5,x6,m)Definitions: UnitScaledPrefix(a,m,x,x1,x5,x6,m)Original native command in the exact edition
  2. L66
    specialize euler_unit_product_reindex_scale (a)
  3. L67
    specialize euler_unit_product_reindex_scale (m)
  4. L68
    specialize euler_unit_product_reindex_scale (x3)
  5. L69
    specialize euler_unit_product_reindex_scale (x4)
  6. L70
    specialize euler_unit_product_reindex_scale (x)
  7. L71
    specialize euler_unit_product_reindex_scale (x1)
  8. L72
    specialize euler_unit_product_reindex_scale (x5)
  9. L73
    specialize euler_unit_product_reindex_scale (x6)
  10. L74
    apply euler_unit_product_reindex_scale
16Use earlier factsL75–78

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

  1. L75
    exact ha
  2. L76
    exact hmap_witness_witness_left
  3. L77
    exact hf_witness_witness
  4. L78
    exact hcomp_witness_witness
17Establish hbalanceL79–88

Establish this local claim before using it. It is not an additional assumption.

  1. L79
    have hbalance : ModEq(m,w · x2,x7)Definitions: ModEq(m,w · x2,x7)Original native command in the exact edition
  2. L80
    specialize euler_unit_count_product_balance (m)
  3. L81
    specialize euler_unit_count_product_balance (a)
  4. L82
    specialize euler_unit_count_product_balance (m)
  5. L83
    specialize euler_unit_count_product_balance (x)
  6. L84
    specialize euler_unit_count_product_balance (x1)
  7. L85
    specialize euler_unit_count_product_balance (x5)
  8. L86
    specialize euler_unit_count_product_balance (x6)
  9. L87
    specialize euler_unit_count_product_balance (t)
  10. L88
    specialize euler_unit_count_product_balance (x2)
18Use earlier factsL89–96

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

  1. L89
    specialize euler_unit_count_product_balance (x7)
  2. L90
    specialize euler_unit_count_product_balance (w)
  3. L91
    apply euler_unit_count_product_balance
  4. L92
    exact ht_right
  5. L93
    exact hs
  6. L94
    exact hP_witness
  7. L95
    exact hQ_witness
  8. L96
    exact hw
19Calculate and transport equalitiesL97–97

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

  1. L97
    rewrite he at hbalance
20Use earlier factsL98–107

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

  1. L98
    specialize euler_coprime_weighted_product_cancel (m)
  2. L99
    specialize euler_coprime_weighted_product_cancel (x2)
  3. L100
    specialize euler_coprime_weighted_product_cancel (w)
  4. L101
    apply euler_coprime_weighted_product_cancel
  5. L102
    exact hm
  6. L103
    specialize euler_unit_product_coprime (m)
  7. L104
    specialize euler_unit_product_coprime (m)
  8. L105
    specialize euler_unit_product_coprime (x)
  9. L106
    specialize euler_unit_product_coprime (x1)
  10. L107
    specialize euler_unit_product_coprime (x2)
21Use earlier factsL108–111

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

  1. L108
    apply euler_unit_product_coprime
  2. L109
    exact hf_witness_witness
  3. L110
    exact hP_witness
  4. L111
    exact hbalance

Library-wide reading audit

Original defined command ledger · 111 lines
  1. 0001intro a
  2. 0002intro m
  3. 0003intro t
  4. 0004intro w
  5. 0005intro hm
  6. 0006intro ha
  7. 0007intro ht
  8. 0008intro hw
  9. 0009cases ht
  10. 0010have hf : ∃ b. ∃ c. UnitProductPrefix(m,b,c,m)
  11. 0011specialize euler_unit_product_prefix_exists (m)
  12. 0012specialize euler_unit_product_prefix_exists (m)
  13. 0013apply euler_unit_product_prefix_exists
  14. 0014cases hf
  15. 0015cases hf_witness
  16. 0016have hP : ∃ P. Product(x,x1,m,P)
  17. 0017specialize beta_product_exists (x)
  18. 0018specialize beta_product_exists (x1)
  19. 0019specialize beta_product_exists (m)
  20. 0020apply beta_product_exists
  21. 0021cases hP
  22. 0022have hmap : ∃ r. ∃ s. UnitMultiplierPrefix(a,m,r,s,m) ∧ PermutationPrefix(r,s,m)
  23. 0023specialize euler_multiplier_permutation_exists (a)
  24. 0024specialize euler_multiplier_permutation_exists (m)
  25. 0025apply euler_multiplier_permutation_exists
  26. 0026exact hm
  27. 0027exact ha
  28. 0028cases hmap
  29. 0029cases hmap_witness
  30. 0030cases hmap_witness_witness
  31. 0031cases hmap_witness_witness_right
  32. 0032cases hmap_witness_witness_right_right
  33. 0033have hcomp : ∃ z. ∃ d. ∀ y. ∀ n. ∀ k. Lt(y,m) → BetaAt(x3,x4,y,n) → BetaAt(x,x1,n,k) → BetaAt(z,d,y,k)
  34. 0034specialize finite_beta_composition_exists (x3)
  35. 0035specialize finite_beta_composition_exists (x4)
  36. 0036specialize finite_beta_composition_exists (x)
  37. 0037specialize finite_beta_composition_exists (x1)
  38. 0038specialize finite_beta_composition_exists (m)
  39. 0039apply finite_beta_composition_exists
  40. 0040cases hcomp
  41. 0041cases hcomp_witness
  42. 0042have hQ : ∃ Q. Product(x5,x6,m,Q)
  43. 0043specialize beta_product_exists (x5)
  44. 0044specialize beta_product_exists (x6)
  45. 0045specialize beta_product_exists (m)
  46. 0046apply beta_product_exists
  47. 0047cases hQ
  48. 0048have he : x7=x2
  49. 0049symm
  50. 0050specialize beta_product_permutation_invariant (m)
  51. 0051specialize beta_product_permutation_invariant (x3)
  52. 0052specialize beta_product_permutation_invariant (x4)
  53. 0053specialize beta_product_permutation_invariant (x)
  54. 0054specialize beta_product_permutation_invariant (x1)
  55. 0055specialize beta_product_permutation_invariant (x5)
  56. 0056specialize beta_product_permutation_invariant (x6)
  57. 0057specialize beta_product_permutation_invariant (x2)
  58. 0058specialize beta_product_permutation_invariant (x7)
  59. 0059apply beta_product_permutation_invariant
  60. 0060exact hmap_witness_witness_right_left
  61. 0061exact hmap_witness_witness_right_right_left
  62. 0062exact hcomp_witness_witness
  63. 0063exact hP_witness
  64. 0064exact hQ_witness
  65. 0065have hs : UnitScaledPrefix(a,m,x,x1,x5,x6,m)
  66. 0066specialize euler_unit_product_reindex_scale (a)
  67. 0067specialize euler_unit_product_reindex_scale (m)
  68. 0068specialize euler_unit_product_reindex_scale (x3)
  69. 0069specialize euler_unit_product_reindex_scale (x4)
  70. 0070specialize euler_unit_product_reindex_scale (x)
  71. 0071specialize euler_unit_product_reindex_scale (x1)
  72. 0072specialize euler_unit_product_reindex_scale (x5)
  73. 0073specialize euler_unit_product_reindex_scale (x6)
  74. 0074apply euler_unit_product_reindex_scale
  75. 0075exact ha
  76. 0076exact hmap_witness_witness_left
  77. 0077exact hf_witness_witness
  78. 0078exact hcomp_witness_witness
  79. 0079have hbalance : ModEq(m,w · x2,x7)
  80. 0080specialize euler_unit_count_product_balance (m)
  81. 0081specialize euler_unit_count_product_balance (a)
  82. 0082specialize euler_unit_count_product_balance (m)
  83. 0083specialize euler_unit_count_product_balance (x)
  84. 0084specialize euler_unit_count_product_balance (x1)
  85. 0085specialize euler_unit_count_product_balance (x5)
  86. 0086specialize euler_unit_count_product_balance (x6)
  87. 0087specialize euler_unit_count_product_balance (t)
  88. 0088specialize euler_unit_count_product_balance (x2)
  89. 0089specialize euler_unit_count_product_balance (x7)
  90. 0090specialize euler_unit_count_product_balance (w)
  91. 0091apply euler_unit_count_product_balance
  92. 0092exact ht_right
  93. 0093exact hs
  94. 0094exact hP_witness
  95. 0095exact hQ_witness
  96. 0096exact hw
  97. 0097rewrite he at hbalance
  98. 0098specialize euler_coprime_weighted_product_cancel (m)
  99. 0099specialize euler_coprime_weighted_product_cancel (x2)
  100. 0100specialize euler_coprime_weighted_product_cancel (w)
  101. 0101apply euler_coprime_weighted_product_cancel
  102. 0102exact hm
  103. 0103specialize euler_unit_product_coprime (m)
  104. 0104specialize euler_unit_product_coprime (m)
  105. 0105specialize euler_unit_product_coprime (x)
  106. 0106specialize euler_unit_product_coprime (x1)
  107. 0107specialize euler_unit_product_coprime (x2)
  108. 0108apply euler_unit_product_coprime
  109. 0109exact hf_witness_witness
  110. 0110exact hP_witness
  111. 0111exact hbalance