PA0082 · theorem

prime_positive_bounded_product_coprime

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

A product of positive residues below a prime is coprime to that prime.

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

∀ p. ∀ b. ∀ c. ∀ l. ∀ F. Prime(p) → (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → UnitResidue(p,y)) → Product(b,c,l,F) → Coprime(F,p)

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

PD0002 Lt PD0004 Prime PD0005 Coprime PD0013 BetaAt PD0014 Product PD0030 UnitResidue

6 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0003 Dvd PD0005 Coprime PD0013 BetaAt PD0030 UnitResidue

7 occurrences

Exact expanded native-PA statement
forall p b c l F. ((~(p = 1) /\ forall frp_prime_left_prime_product_prime frp_prime_right_prime_product_prime. p = frp_prime_left_prime_product_prime * frp_prime_right_prime_product_prime -> frp_prime_left_prime_product_prime = 1 \/ frp_prime_right_prime_product_prime = 1)) -> (forall fppc_index_prime_product_bounds fppc_factor_prime_product_bounds. (exists frp_gap_prime_product_bounds_index_bound. frp_gap_prime_product_bounds_index_bound + S fppc_index_prime_product_bounds = l) -> (((exists ff_h_fppc_prime_product_bounds_decoded. ff_h_fppc_prime_product_bounds_decoded + S (fppc_factor_prime_product_bounds) = S ((S (fppc_index_prime_product_bounds)) * c)) /\ exists ff_q_fppc_prime_product_bounds_decoded. b = ff_q_fppc_prime_product_bounds_decoded * S ((S (fppc_index_prime_product_bounds)) * c) + (fppc_factor_prime_product_bounds))) -> (~(fppc_factor_prime_product_bounds = 0) /\ (exists frp_gap_prime_product_bounds_factor_bound. frp_gap_prime_product_bounds_factor_bound + S fppc_factor_prime_product_bounds = p))) -> (exists ff_u_prime_product_product ff_v_prime_product_product. ((((exists ff_h_prime_product_product_start. ff_h_prime_product_product_start + S (1) = S ((S (0)) * ff_v_prime_product_product)) /\ exists ff_q_prime_product_product_start. ff_u_prime_product_product = ff_q_prime_product_product_start * S ((S (0)) * ff_v_prime_product_product) + (1))) /\ ((((exists ff_h_prime_product_product_terminal. ff_h_prime_product_product_terminal + S (F) = S ((S (l)) * ff_v_prime_product_product)) /\ exists ff_q_prime_product_product_terminal. ff_u_prime_product_product = ff_q_prime_product_product_terminal * S ((S (l)) * ff_v_prime_product_product) + (F))) /\ forall ff_i_prime_product_product. (exists ff_lt_prime_product_product_bound. ff_lt_prime_product_product_bound + S ff_i_prime_product_product = l) -> exists ff_p_prime_product_product ff_r_prime_product_product ff_s_prime_product_product. ((((exists ff_h_prime_product_product_factor. ff_h_prime_product_product_factor + S (ff_p_prime_product_product) = S ((S (ff_i_prime_product_product)) * c)) /\ exists ff_q_prime_product_product_factor. b = ff_q_prime_product_product_factor * S ((S (ff_i_prime_product_product)) * c) + (ff_p_prime_product_product))) /\ ((((exists ff_h_prime_product_product_partial. ff_h_prime_product_product_partial + S (ff_r_prime_product_product) = S ((S (ff_i_prime_product_product)) * ff_v_prime_product_product)) /\ exists ff_q_prime_product_product_partial. ff_u_prime_product_product = ff_q_prime_product_product_partial * S ((S (ff_i_prime_product_product)) * ff_v_prime_product_product) + (ff_r_prime_product_product))) /\ ((((exists ff_h_prime_product_product_successor. ff_h_prime_product_product_successor + S (ff_s_prime_product_product) = S ((S (S ff_i_prime_product_product)) * ff_v_prime_product_product)) /\ exists ff_q_prime_product_product_successor. ff_u_prime_product_product = ff_q_prime_product_product_successor * S ((S (S ff_i_prime_product_product)) * ff_v_prime_product_product) + (ff_s_prime_product_product))) /\ ff_s_prime_product_product = ff_r_prime_product_product * ff_p_prime_product_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)

Proof neighborhood

Direct theorem prerequisites

PA0039 divisor_le_nonzero PA003A lt_not_le PA003N prime_not_divides_coprime PA003O coprime_symm PA0081 beta_product_pointwise_coprime

Direct theorem dependents

PA0083 prime_half_range_product_coprime

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

51 script commands · 9 reading checkpoints · 5 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 (5)
divisor le nonzerolt not leprime not divides coprimecoprime symmbeta product pointwise coprime
01Fix variables and assumptionsL1–8

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

  1. L1
    intro p
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro l
  5. L5
    intro F
  6. L6
    intro hp
  7. L7
    intro hbounded
  8. L8
    intro hproduct
02Establish hpointwiseL9–13

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

  1. L9
    have hpointwise : ∀ frp_index_prime_product_pointwise. ∀ frp_factor_prime_product_pointwise. Lt(frp_index_prime_product_pointwise,l) → BetaAt(b,c,frp_index_prime_product_pointwise,frp_factor_prime_product_pointwise) → Coprime(frp_factor_prime_product_pointwise,p)Definitions: Lt(frp_index_prime_product_pointwise,l)BetaAt(b,c,frp_index_prime_product_pointwise,frp_factor_prime_product_pointwise)Coprime(frp_factor_prime_product_pointwise,p)Original native command in the exact edition
  2. L10
    intro i
  3. L11
    intro x
  4. L12
    intro hi
  5. L13
    intro hx
03Establish hboundsL14–19

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

  1. L14
    have hbounds : UnitResidue(p,x)Definitions: UnitResidue(p,x)Original native command in the exact edition
  2. L15
    specialize hbounded i
  3. L16
    specialize hbounded x
  4. L17
    apply hbounded
  5. L18
    exact hi
  6. L19
    exact hx
04Separate the logical casesL20–20

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

  1. L20
    cases hbounds
05Establish hnotdivL21–22

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

  1. L21
    have hnotdiv : ¬Dvd(p,x)Definitions: Dvd(p,x)Original native command in the exact edition
  2. L22
    intro hdiv
06Establish hleL23–32

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

  1. L23
  2. L24
    specialize divisor_le_nonzero p
  3. L25
    specialize divisor_le_nonzero x
  4. L26
    apply divisor_le_nonzero
  5. L27
    exact hbounds_left
  6. L28
    exact hdiv
  7. L29
    specialize lt_not_le x
  8. L30
    specialize lt_not_le p
  9. L31
    apply lt_not_le
  10. L32
    exact hbounds_right
07Use earlier factsL33–33

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

  1. L33
    exact hle
08Establish hprimecopL34–43

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

  1. L34
    have hprimecop : Coprime(p,x)Definitions: Coprime(p,x)Original native command in the exact edition
  2. L35
    specialize prime_not_divides_coprime p
  3. L36
    specialize prime_not_divides_coprime x
  4. L37
    apply prime_not_divides_coprime
  5. L38
    exact hp
  6. L39
    exact hnotdiv
  7. L40
    specialize coprime_symm p
  8. L41
    specialize coprime_symm x
  9. L42
    apply coprime_symm
  10. L43
    exact hprimecop
09Use earlier factsL44–51

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

  1. L44
    specialize beta_product_pointwise_coprime p
  2. L45
    specialize beta_product_pointwise_coprime b
  3. L46
    specialize beta_product_pointwise_coprime c
  4. L47
    specialize beta_product_pointwise_coprime l
  5. L48
    specialize beta_product_pointwise_coprime F
  6. L49
    apply beta_product_pointwise_coprime
  7. L50
    exact hpointwise
  8. L51
    exact hproduct

Library-wide reading audit

Original defined command ledger · 51 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro l
  5. 0005intro F
  6. 0006intro hp
  7. 0007intro hbounded
  8. 0008intro hproduct
  9. 0009have hpointwise : ∀ frp_index_prime_product_pointwise. ∀ frp_factor_prime_product_pointwise. Lt(frp_index_prime_product_pointwise,l) → BetaAt(b,c,frp_index_prime_product_pointwise,frp_factor_prime_product_pointwise) → Coprime(frp_factor_prime_product_pointwise,p)
    Exact native replay linehave hpointwise : forall frp_index_prime_product_pointwise frp_factor_prime_product_pointwise. (exists frp_gap_prime_product_pointwise_bound. frp_gap_prime_product_pointwise_bound + S frp_index_prime_product_pointwise = l) -> (((exists ff_h_frp_prime_product_pointwise_decoded. ff_h_frp_prime_product_pointwise_decoded + S (frp_factor_prime_product_pointwise) = S ((S (frp_index_prime_product_pointwise)) * c)) /\ exists ff_q_frp_prime_product_pointwise_decoded. b = ff_q_frp_prime_product_pointwise_decoded * S ((S (frp_index_prime_product_pointwise)) * c) + (frp_factor_prime_product_pointwise))) -> (forall frp_divisor_prime_product_pointwise_coprime. (exists frp_left_factor_prime_product_pointwise_coprime. frp_factor_prime_product_pointwise = frp_divisor_prime_product_pointwise_coprime * frp_left_factor_prime_product_pointwise_coprime) -> (exists frp_right_factor_prime_product_pointwise_coprime. p = frp_divisor_prime_product_pointwise_coprime * frp_right_factor_prime_product_pointwise_coprime) -> frp_divisor_prime_product_pointwise_coprime = 1)
  10. 0010intro i
  11. 0011intro x
  12. 0012intro hi
  13. 0013intro hx
  14. 0014have hbounds : UnitResidue(p,x)
    Exact native replay linehave hbounds : (~(x = 0) /\ (exists frp_gap_prime_product_local_bound. frp_gap_prime_product_local_bound + S x = p))
  15. 0015specialize hbounded i
  16. 0016specialize hbounded x
  17. 0017apply hbounded
  18. 0018exact hi
  19. 0019exact hx
  20. 0020cases hbounds
  21. 0021have hnotdiv : ¬Dvd(p,x)
    Exact native replay linehave hnotdiv : ~(exists k. x = p * k)
  22. 0022intro hdiv
  23. 0023have hle : Le(p,x)
    Exact native replay linehave hle : exists k. k + p = x
  24. 0024specialize divisor_le_nonzero p
  25. 0025specialize divisor_le_nonzero x
  26. 0026apply divisor_le_nonzero
  27. 0027exact hbounds_left
  28. 0028exact hdiv
  29. 0029specialize lt_not_le x
  30. 0030specialize lt_not_le p
  31. 0031apply lt_not_le
  32. 0032exact hbounds_right
  33. 0033exact hle
  34. 0034have hprimecop : Coprime(p,x)
    Exact native replay linehave hprimecop : forall frp_divisor_prime_product_factor. (exists frp_left_factor_prime_product_factor. p = frp_divisor_prime_product_factor * frp_left_factor_prime_product_factor) -> (exists frp_right_factor_prime_product_factor. x = frp_divisor_prime_product_factor * frp_right_factor_prime_product_factor) -> frp_divisor_prime_product_factor = 1
  35. 0035specialize prime_not_divides_coprime p
  36. 0036specialize prime_not_divides_coprime x
  37. 0037apply prime_not_divides_coprime
  38. 0038exact hp
  39. 0039exact hnotdiv
  40. 0040specialize coprime_symm p
  41. 0041specialize coprime_symm x
  42. 0042apply coprime_symm
  43. 0043exact hprimecop
  44. 0044specialize beta_product_pointwise_coprime p
  45. 0045specialize beta_product_pointwise_coprime b
  46. 0046specialize beta_product_pointwise_coprime c
  47. 0047specialize beta_product_pointwise_coprime l
  48. 0048specialize beta_product_pointwise_coprime F
  49. 0049apply beta_product_pointwise_coprime
  50. 0050exact hpointwise
  51. 0051exact hproduct