PA0083

prime_half_range_product_coprime

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

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

Exact expanded 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)

Structural proof guide

Generated structural guide

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

Use the direct prerequisites beta_half_range_entry_bounds, prime_positive_bounded_product_coprime as previously established PA formulas.

The proof proceeds by intermediate claims (1).

Referenced ingredients

PA0034 beta_half_range_entry_bounds PA0082 prime_positive_bounded_product_coprime

Proof neighborhood

Direct dependencies

PA0034 beta_half_range_entry_bounds PA0082 prime_positive_bounded_product_coprime

Direct dependents

PA0084 gauss_signed_products_cancel_mod

Formal native tactic body

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

  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 : 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