PA008K

prime_range_product_coprime

Alpha v34 checked-use theorem · independently closed; not Stable

The product 1*...*(p-1) is coprime to a prime p.

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.

Exact expanded PA statement

forall p n b c F. p = S n -> ((~(p = 1) /\ forall frp_prime_left_prime_p frp_prime_right_prime_p. p = frp_prime_left_prime_p * frp_prime_right_prime_p -> frp_prime_left_prime_p = 1 \/ frp_prime_right_prime_p = 1)) -> (forall ff_i_frp_range_prime_range. (exists ff_lt_frp_range_prime_range_bound. ff_lt_frp_range_prime_range_bound + S ff_i_frp_range_prime_range = n) -> (((exists ff_h_frp_range_prime_range_decoded. ff_h_frp_range_prime_range_decoded + S (1 + ff_i_frp_range_prime_range) = S ((S (ff_i_frp_range_prime_range)) * c)) /\ exists ff_q_frp_range_prime_range_decoded. b = ff_q_frp_range_prime_range_decoded * S ((S (ff_i_frp_range_prime_range)) * c) + (1 + ff_i_frp_range_prime_range)))) -> (exists ff_u_prime_product ff_v_prime_product. ((((exists ff_h_prime_product_start. ff_h_prime_product_start + S (1) = S ((S (0)) * ff_v_prime_product)) /\ exists ff_q_prime_product_start. ff_u_prime_product = ff_q_prime_product_start * S ((S (0)) * ff_v_prime_product) + (1))) /\ ((((exists ff_h_prime_product_terminal. ff_h_prime_product_terminal + S (F) = S ((S (n)) * ff_v_prime_product)) /\ exists ff_q_prime_product_terminal. ff_u_prime_product = ff_q_prime_product_terminal * S ((S (n)) * ff_v_prime_product) + (F))) /\ forall ff_i_prime_product. (exists ff_lt_prime_product_bound. ff_lt_prime_product_bound + S ff_i_prime_product = n) -> exists ff_p_prime_product ff_r_prime_product ff_s_prime_product. ((((exists ff_h_prime_product_factor. ff_h_prime_product_factor + S (ff_p_prime_product) = S ((S (ff_i_prime_product)) * c)) /\ exists ff_q_prime_product_factor. b = ff_q_prime_product_factor * S ((S (ff_i_prime_product)) * c) + (ff_p_prime_product))) /\ ((((exists ff_h_prime_product_partial. ff_h_prime_product_partial + S (ff_r_prime_product) = S ((S (ff_i_prime_product)) * ff_v_prime_product)) /\ exists ff_q_prime_product_partial. ff_u_prime_product = ff_q_prime_product_partial * S ((S (ff_i_prime_product)) * ff_v_prime_product) + (ff_r_prime_product))) /\ ((((exists ff_h_prime_product_successor. ff_h_prime_product_successor + S (ff_s_prime_product) = S ((S (S ff_i_prime_product)) * ff_v_prime_product)) /\ exists ff_q_prime_product_successor. ff_u_prime_product = ff_q_prime_product_successor * S ((S (S ff_i_prime_product)) * ff_v_prime_product) + (ff_s_prime_product))) /\ ff_s_prime_product = ff_r_prime_product * ff_p_prime_product)))))) -> (forall frp_divisor_prime_product_result. (exists frp_left_factor_prime_product_result. F = frp_divisor_prime_product_result * frp_left_factor_prime_product_result) -> (exists frp_right_factor_prime_product_result. p = frp_divisor_prime_product_result * frp_right_factor_prime_product_result) -> frp_divisor_prime_product_result = 1)

Structural proof guide

Generated structural guide

The product 1*...*(p-1) is coprime to a prime p.

Use the direct prerequisites beta_range_one_entry_eq_succ, beta_product_pointwise_coprime, succ_ne_zero, succ_le_succ, divisor_le_nonzero, lt_not_le, prime_not_divides_coprime, coprime_symm as previously established PA formulas.

The proof proceeds by intermediate claims (7), equality transport (2).

Referenced ingredients

PA008F beta_range_one_entry_eq_succ PA0081 beta_product_pointwise_coprime PA0005 succ_ne_zero PA002K succ_le_succ PA0039 divisor_le_nonzero PA003A lt_not_le PA003N prime_not_divides_coprime PA003O coprime_symm

Proof neighborhood

Direct dependencies

PA008F beta_range_one_entry_eq_succ PA0081 beta_product_pointwise_coprime PA0005 succ_ne_zero PA002K succ_le_succ PA0039 divisor_le_nonzero PA003A lt_not_le PA003N prime_not_divides_coprime PA003O coprime_symm

Direct dependents

PA008L fermat_predecessor_exponent_mod_one

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

Read the argument

Proof checkpoints

70 script commands · 10 reading checkpoints · 7 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.

Named ingredients (8)
beta range one entry eq succbeta product pointwise coprimesucc ne zerosucc le succdivisor le nonzerolt not leprime not divides coprimecoprime symm

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–9

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro F
  6. L6
    intro hpn
  7. L7
    intro hp
  8. L8
    intro hrange
  9. L9
    intro hproduct
02Establish hpointwiseL10–14

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

  1. L10
    have hpointwise : ∀ frp_index_prime_pointwise. ∀ frp_factor_prime_pointwise. Lt(frp_index_prime_pointwise,n) → BetaAt(b,c,frp_index_prime_pointwise,frp_factor_prime_pointwise) → Coprime(frp_factor_prime_pointwise,p)Definitions: LtCoprimeBetaAt
  2. L11
    intro i
  3. L12
    intro x
  4. L13
    intro hi
  5. L14
    intro hx
03Establish hvalueL15–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta range one entry eq succ.

  1. L15
    have hvalue : x = S i
  2. L16
    specialize beta_range_one_entry_eq_succ b
  3. L17
    specialize beta_range_one_entry_eq_succ c
  4. L18
    specialize beta_range_one_entry_eq_succ n
  5. L19
    specialize beta_range_one_entry_eq_succ i
  6. L20
    specialize beta_range_one_entry_eq_succ x
  7. L21
    apply beta_range_one_entry_eq_succ
  8. L22
    exact hrange
  9. L23
    exact hi
  10. L24
    exact hx
04Establish hx0L25–32

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

  1. L25
    have hx0 : ~(x = 0)
  2. L26
    intro hxzero
  3. L27
    specialize succ_ne_zero i
  4. L28
    apply succ_ne_zero
  5. L29
    trans x
  6. L30
    symm
  7. L31
    exact hvalue
  8. L32
    exact hxzero
05Establish hxltpL33–39

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

  1. L33
    have hxltp : exists h. h + S x = p
  2. L34
    rewrite hvalue
  3. L35
    rewrite hpn
  4. L36
    specialize succ_le_succ (S i)
  5. L37
    specialize succ_le_succ n
  6. L38
    apply succ_le_succ
  7. L39
    exact hi
06Establish hnotdivL40–41

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

  1. L40
    have hnotdiv : ~(exists k. x = p * k)
  2. L41
    intro hdiv
07Establish hleL42–51

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor le nonzero.

  1. L42
    have hle : exists k. k + p = x
  2. L43
    specialize divisor_le_nonzero p
  3. L44
    specialize divisor_le_nonzero x
  4. L45
    apply divisor_le_nonzero
  5. L46
    exact hx0
  6. L47
    exact hdiv
  7. L48
    specialize lt_not_le x
  8. L49
    specialize lt_not_le p
  9. L50
    apply lt_not_le
  10. L51
    exact hxltp
08Use earlier factsL52–52

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

  1. L52
    exact hle
09Establish hpxL53–62

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime not divides coprime.

  1. L53
    have hpx : forall frp_divisor_prime_factor. (exists frp_left_factor_prime_factor. p = frp_divisor_prime_factor * frp_left_factor_prime_factor) -> (exists frp_right_factor_prime_factor. x = frp_divisor_prime_factor * frp_right_factor_prime_factor) -> frp_divisor_prime_factor = 1
  2. L54
    specialize prime_not_divides_coprime p
  3. L55
    specialize prime_not_divides_coprime x
  4. L56
    apply prime_not_divides_coprime
  5. L57
    exact hp
  6. L58
    exact hnotdiv
  7. L59
    specialize coprime_symm p
  8. L60
    specialize coprime_symm x
  9. L61
    apply coprime_symm
  10. L62
    exact hpx
10Use earlier factsL63–70

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

  1. L63
    specialize beta_product_pointwise_coprime p
  2. L64
    specialize beta_product_pointwise_coprime b
  3. L65
    specialize beta_product_pointwise_coprime c
  4. L66
    specialize beta_product_pointwise_coprime n
  5. L67
    specialize beta_product_pointwise_coprime F
  6. L68
    apply beta_product_pointwise_coprime
  7. L69
    exact hpointwise
  8. L70
    exact hproduct

Library-wide reading audit

Original exact command ledger · 70 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro b
  4. 0004intro c
  5. 0005intro F
  6. 0006intro hpn
  7. 0007intro hp
  8. 0008intro hrange
  9. 0009intro hproduct
  10. 0010have hpointwise : forall frp_index_prime_pointwise frp_factor_prime_pointwise. (exists frp_gap_prime_pointwise_bound. frp_gap_prime_pointwise_bound + S frp_index_prime_pointwise = n) -> (((exists ff_h_frp_prime_pointwise_decoded. ff_h_frp_prime_pointwise_decoded + S (frp_factor_prime_pointwise) = S ((S (frp_index_prime_pointwise)) * c)) /\ exists ff_q_frp_prime_pointwise_decoded. b = ff_q_frp_prime_pointwise_decoded * S ((S (frp_index_prime_pointwise)) * c) + (frp_factor_prime_pointwise))) -> (forall frp_divisor_prime_pointwise_coprime. (exists frp_left_factor_prime_pointwise_coprime. frp_factor_prime_pointwise = frp_divisor_prime_pointwise_coprime * frp_left_factor_prime_pointwise_coprime) -> (exists frp_right_factor_prime_pointwise_coprime. p = frp_divisor_prime_pointwise_coprime * frp_right_factor_prime_pointwise_coprime) -> frp_divisor_prime_pointwise_coprime = 1)
  11. 0011intro i
  12. 0012intro x
  13. 0013intro hi
  14. 0014intro hx
  15. 0015have hvalue : x = S i
  16. 0016specialize beta_range_one_entry_eq_succ b
  17. 0017specialize beta_range_one_entry_eq_succ c
  18. 0018specialize beta_range_one_entry_eq_succ n
  19. 0019specialize beta_range_one_entry_eq_succ i
  20. 0020specialize beta_range_one_entry_eq_succ x
  21. 0021apply beta_range_one_entry_eq_succ
  22. 0022exact hrange
  23. 0023exact hi
  24. 0024exact hx
  25. 0025have hx0 : ~(x = 0)
  26. 0026intro hxzero
  27. 0027specialize succ_ne_zero i
  28. 0028apply succ_ne_zero
  29. 0029trans x
  30. 0030symm
  31. 0031exact hvalue
  32. 0032exact hxzero
  33. 0033have hxltp : exists h. h + S x = p
  34. 0034rewrite hvalue
  35. 0035rewrite hpn
  36. 0036specialize succ_le_succ (S i)
  37. 0037specialize succ_le_succ n
  38. 0038apply succ_le_succ
  39. 0039exact hi
  40. 0040have hnotdiv : ~(exists k. x = p * k)
  41. 0041intro hdiv
  42. 0042have hle : exists k. k + p = x
  43. 0043specialize divisor_le_nonzero p
  44. 0044specialize divisor_le_nonzero x
  45. 0045apply divisor_le_nonzero
  46. 0046exact hx0
  47. 0047exact hdiv
  48. 0048specialize lt_not_le x
  49. 0049specialize lt_not_le p
  50. 0050apply lt_not_le
  51. 0051exact hxltp
  52. 0052exact hle
  53. 0053have hpx : forall frp_divisor_prime_factor. (exists frp_left_factor_prime_factor. p = frp_divisor_prime_factor * frp_left_factor_prime_factor) -> (exists frp_right_factor_prime_factor. x = frp_divisor_prime_factor * frp_right_factor_prime_factor) -> frp_divisor_prime_factor = 1
  54. 0054specialize prime_not_divides_coprime p
  55. 0055specialize prime_not_divides_coprime x
  56. 0056apply prime_not_divides_coprime
  57. 0057exact hp
  58. 0058exact hnotdiv
  59. 0059specialize coprime_symm p
  60. 0060specialize coprime_symm x
  61. 0061apply coprime_symm
  62. 0062exact hpx
  63. 0063specialize beta_product_pointwise_coprime p
  64. 0064specialize beta_product_pointwise_coprime b
  65. 0065specialize beta_product_pointwise_coprime c
  66. 0066specialize beta_product_pointwise_coprime n
  67. 0067specialize beta_product_pointwise_coprime F
  68. 0068apply beta_product_pointwise_coprime
  69. 0069exact hpointwise
  70. 0070exact hproduct