PA0083 · theorem

prime_half_range_product_coprime

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

The canonical half-range product is coprime to its odd prime modulus.

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. ∀ h. ∀ b. ∀ c. ∀ P. p = 2 · h + 1 → Prime(p) → Range(b,c,1,h) → Product(b,c,h,P) → Coprime(P,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

PD0004 Prime PD0005 Coprime PD0014 Product PD0018 Range

4 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0030 UnitResidue

3 occurrences

Exact expanded native-PA statement
forall p h b c P. p = 2 * h + 1 -> ((~(p = 1) /\ forall frp_prime_left_gauss_composition_prime frp_prime_right_gauss_composition_prime. p = frp_prime_left_gauss_composition_prime * frp_prime_right_gauss_composition_prime -> frp_prime_left_gauss_composition_prime = 1 \/ frp_prime_right_gauss_composition_prime = 1)) -> (forall gsp_range_index_gauss_composition_half_range. (exists gsp_lt_gap_gauss_composition_half_range_range_bound. gsp_lt_gap_gauss_composition_half_range_range_bound + S gsp_range_index_gauss_composition_half_range = h) -> (((exists gsp_beta_height_gauss_composition_half_range_range_entry. gsp_beta_height_gauss_composition_half_range_range_entry + S (1 + gsp_range_index_gauss_composition_half_range) = S ((S (gsp_range_index_gauss_composition_half_range)) * c)) /\ exists gsp_beta_quotient_gauss_composition_half_range_range_entry. b = gsp_beta_quotient_gauss_composition_half_range_range_entry * S ((S (gsp_range_index_gauss_composition_half_range)) * c) + (1 + gsp_range_index_gauss_composition_half_range)))) -> (exists ff_u_gauss_composition_canonical_product ff_v_gauss_composition_canonical_product. ((((exists ff_h_gauss_composition_canonical_product_start. ff_h_gauss_composition_canonical_product_start + S (1) = S ((S (0)) * ff_v_gauss_composition_canonical_product)) /\ exists ff_q_gauss_composition_canonical_product_start. ff_u_gauss_composition_canonical_product = ff_q_gauss_composition_canonical_product_start * S ((S (0)) * ff_v_gauss_composition_canonical_product) + (1))) /\ ((((exists ff_h_gauss_composition_canonical_product_terminal. ff_h_gauss_composition_canonical_product_terminal + S (P) = S ((S (h)) * ff_v_gauss_composition_canonical_product)) /\ exists ff_q_gauss_composition_canonical_product_terminal. ff_u_gauss_composition_canonical_product = ff_q_gauss_composition_canonical_product_terminal * S ((S (h)) * ff_v_gauss_composition_canonical_product) + (P))) /\ forall ff_i_gauss_composition_canonical_product. (exists ff_lt_gauss_composition_canonical_product_bound. ff_lt_gauss_composition_canonical_product_bound + S ff_i_gauss_composition_canonical_product = h) -> exists ff_p_gauss_composition_canonical_product ff_r_gauss_composition_canonical_product ff_s_gauss_composition_canonical_product. ((((exists ff_h_gauss_composition_canonical_product_factor. ff_h_gauss_composition_canonical_product_factor + S (ff_p_gauss_composition_canonical_product) = S ((S (ff_i_gauss_composition_canonical_product)) * c)) /\ exists ff_q_gauss_composition_canonical_product_factor. b = ff_q_gauss_composition_canonical_product_factor * S ((S (ff_i_gauss_composition_canonical_product)) * c) + (ff_p_gauss_composition_canonical_product))) /\ ((((exists ff_h_gauss_composition_canonical_product_partial. ff_h_gauss_composition_canonical_product_partial + S (ff_r_gauss_composition_canonical_product) = S ((S (ff_i_gauss_composition_canonical_product)) * ff_v_gauss_composition_canonical_product)) /\ exists ff_q_gauss_composition_canonical_product_partial. ff_u_gauss_composition_canonical_product = ff_q_gauss_composition_canonical_product_partial * S ((S (ff_i_gauss_composition_canonical_product)) * ff_v_gauss_composition_canonical_product) + (ff_r_gauss_composition_canonical_product))) /\ ((((exists ff_h_gauss_composition_canonical_product_successor. ff_h_gauss_composition_canonical_product_successor + S (ff_s_gauss_composition_canonical_product) = S ((S (S ff_i_gauss_composition_canonical_product)) * ff_v_gauss_composition_canonical_product)) /\ exists ff_q_gauss_composition_canonical_product_successor. ff_u_gauss_composition_canonical_product = ff_q_gauss_composition_canonical_product_successor * S ((S (S ff_i_gauss_composition_canonical_product)) * ff_v_gauss_composition_canonical_product) + (ff_s_gauss_composition_canonical_product))) /\ ff_s_gauss_composition_canonical_product = ff_r_gauss_composition_canonical_product * ff_p_gauss_composition_canonical_product)))))) -> (forall frp_divisor_gauss_composition_canonical_coprime. (exists frp_left_factor_gauss_composition_canonical_coprime. P = frp_divisor_gauss_composition_canonical_coprime * frp_left_factor_gauss_composition_canonical_coprime) -> (exists frp_right_factor_gauss_composition_canonical_coprime. p = frp_divisor_gauss_composition_canonical_coprime * frp_right_factor_gauss_composition_canonical_coprime) -> frp_divisor_gauss_composition_canonical_coprime = 1)

Proof neighborhood

Direct theorem prerequisites

PA0034 beta_half_range_entry_bounds PA0082 prime_positive_bounded_product_coprime

Direct theorem dependents

PA0084 gauss_signed_products_cancel_mod

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

34 script commands · 4 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 (2)
beta half range entry boundsprime positive bounded product coprime
01Fix variables and assumptionsL1–9

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

  1. L1
    intro p
  2. L2
    intro h
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro P
  6. L6
    intro hp
  7. L7
    intro hprime
  8. L8
    intro hhalf
  9. L9
    intro hproduct
02Establish hboundsL10–19

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

  1. L10
    have hbounds : ∀ fppc_index_gauss_composition_bounds. ∀ fppc_factor_gauss_composition_bounds. Lt(fppc_index_gauss_composition_bounds,h) → BetaAt(b,c,fppc_index_gauss_composition_bounds,fppc_factor_gauss_composition_bounds) → UnitResidue(p,fppc_factor_gauss_composition_bounds)Definitions: Lt(fppc_index_gauss_composition_bounds,h)BetaAt(b,c,fppc_index_gauss_composition_bounds,fppc_factor_gauss_composition_bounds)UnitResidue(p,fppc_factor_gauss_composition_bounds)Original native command in the exact edition
  2. L11
    intro i
  3. L12
    intro x
  4. L13
    intro hi
  5. L14
    intro hx
  6. L15
    specialize beta_half_range_entry_bounds p
  7. L16
    specialize beta_half_range_entry_bounds h
  8. L17
    specialize beta_half_range_entry_bounds b
  9. L18
    specialize beta_half_range_entry_bounds c
  10. L19
    specialize beta_half_range_entry_bounds i
03Use earlier factsL20–29

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

  1. L20
    specialize beta_half_range_entry_bounds x
  2. L21
    apply beta_half_range_entry_bounds
  3. L22
    exact hp
  4. L23
    exact hhalf
  5. L24
    exact hi
  6. L25
    exact hx
  7. L26
    specialize prime_positive_bounded_product_coprime p
  8. L27
    specialize prime_positive_bounded_product_coprime b
  9. L28
    specialize prime_positive_bounded_product_coprime c
  10. L29
    specialize prime_positive_bounded_product_coprime h
04Use earlier factsL30–34

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

  1. L30
    specialize prime_positive_bounded_product_coprime P
  2. L31
    apply prime_positive_bounded_product_coprime
  3. L32
    exact hprime
  4. L33
    exact hbounds
  5. L34
    exact hproduct

Library-wide reading audit

Original defined command ledger · 34 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro b
  4. 0004intro c
  5. 0005intro P
  6. 0006intro hp
  7. 0007intro hprime
  8. 0008intro hhalf
  9. 0009intro hproduct
  10. 0010have hbounds : ∀ fppc_index_gauss_composition_bounds. ∀ fppc_factor_gauss_composition_bounds. Lt(fppc_index_gauss_composition_bounds,h) → BetaAt(b,c,fppc_index_gauss_composition_bounds,fppc_factor_gauss_composition_bounds) → UnitResidue(p,fppc_factor_gauss_composition_bounds)
    Exact native replay linehave hbounds : forall fppc_index_gauss_composition_bounds fppc_factor_gauss_composition_bounds. (exists frp_gap_gauss_composition_bounds_index_bound. frp_gap_gauss_composition_bounds_index_bound + S fppc_index_gauss_composition_bounds = h) -> (((exists ff_h_fppc_gauss_composition_bounds_decoded. ff_h_fppc_gauss_composition_bounds_decoded + S (fppc_factor_gauss_composition_bounds) = S ((S (fppc_index_gauss_composition_bounds)) * c)) /\ exists ff_q_fppc_gauss_composition_bounds_decoded. b = ff_q_fppc_gauss_composition_bounds_decoded * S ((S (fppc_index_gauss_composition_bounds)) * c) + (fppc_factor_gauss_composition_bounds))) -> (~(fppc_factor_gauss_composition_bounds = 0) /\ (exists frp_gap_gauss_composition_bounds_factor_bound. frp_gap_gauss_composition_bounds_factor_bound + S fppc_factor_gauss_composition_bounds = p))
  11. 0011intro i
  12. 0012intro x
  13. 0013intro hi
  14. 0014intro hx
  15. 0015specialize beta_half_range_entry_bounds p
  16. 0016specialize beta_half_range_entry_bounds h
  17. 0017specialize beta_half_range_entry_bounds b
  18. 0018specialize beta_half_range_entry_bounds c
  19. 0019specialize beta_half_range_entry_bounds i
  20. 0020specialize beta_half_range_entry_bounds x
  21. 0021apply beta_half_range_entry_bounds
  22. 0022exact hp
  23. 0023exact hhalf
  24. 0024exact hi
  25. 0025exact hx
  26. 0026specialize prime_positive_bounded_product_coprime p
  27. 0027specialize prime_positive_bounded_product_coprime b
  28. 0028specialize prime_positive_bounded_product_coprime c
  29. 0029specialize prime_positive_bounded_product_coprime h
  30. 0030specialize prime_positive_bounded_product_coprime P
  31. 0031apply prime_positive_bounded_product_coprime
  32. 0032exact hprime
  33. 0033exact hbounds
  34. 0034exact hproduct