PA00DP

distinct_primes_own_odd_half_scaled_remainder_nonzero

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

An index below the divisor's own odd half has nonzero scaled remainder for a distinct prime multiplier.

Exact expanded PA statement

forall p q k i d r. p = 2 * k + 1 -> ((~(p = 1) /\ forall frp_prime_left_remainder_nonzero_prime_p frp_prime_right_remainder_nonzero_prime_p. p = frp_prime_left_remainder_nonzero_prime_p * frp_prime_right_remainder_nonzero_prime_p -> frp_prime_left_remainder_nonzero_prime_p = 1 \/ frp_prime_right_remainder_nonzero_prime_p = 1)) -> ((~(q = 1) /\ forall frp_prime_left_remainder_nonzero_prime_q frp_prime_right_remainder_nonzero_prime_q. q = frp_prime_left_remainder_nonzero_prime_q * frp_prime_right_remainder_nonzero_prime_q -> frp_prime_left_remainder_nonzero_prime_q = 1 \/ frp_prime_right_remainder_nonzero_prime_q = 1)) -> ~(p = q) -> (exists ern_lt_gap_remainder_nonzero_own_half_bound. ern_lt_gap_remainder_nonzero_own_half_bound + S (i) = k) -> q * S i = p * d + r -> ~(r = 0)

Structural proof guide

Generated structural guide

An index below the divisor's own odd half has nonzero scaled remainder for a distinct prime multiplier.

Use the direct prerequisites odd_half_strictly_below_modulus, lt_of_le_of_lt, distinct_primes_bounded_scaled_remainder_nonzero as previously established PA formulas.

The proof proceeds by intermediate claims (2).

Referenced ingredients

PA00C2 odd_half_strictly_below_modulus PA0033 lt_of_le_of_lt PA00DO distinct_primes_bounded_scaled_remainder_nonzero

Proof neighborhood

Direct dependencies

PA00C2 odd_half_strictly_below_modulus PA0033 lt_of_le_of_lt PA00DO distinct_primes_bounded_scaled_remainder_nonzero

Direct dependents

PA00E0 distinct_odd_prime_row_bit_count_equals_division_quotient

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 q
  3. 0003intro k
  4. 0004intro i
  5. 0005intro d
  6. 0006intro r
  7. 0007intro hpodd
  8. 0008intro hp
  9. 0009intro hq
  10. 0010intro hpq
  11. 0011intro hik
  12. 0012intro hdivision
  13. 0013intro hr0
  14. 0014have hkp : exists ern_lt_gap_remainder_nonzero_half_below_p. ern_lt_gap_remainder_nonzero_half_below_p + S (k) = p
  15. 0015specialize odd_half_strictly_below_modulus p
  16. 0016specialize odd_half_strictly_below_modulus k
  17. 0017apply odd_half_strictly_below_modulus
  18. 0018exact hpodd
  19. 0019have hip : exists ern_lt_gap_remainder_nonzero_index_below_p. ern_lt_gap_remainder_nonzero_index_below_p + S (S i) = p
  20. 0020specialize lt_of_le_of_lt (S i)
  21. 0021specialize lt_of_le_of_lt k
  22. 0022specialize lt_of_le_of_lt p
  23. 0023apply lt_of_le_of_lt
  24. 0024exact hik
  25. 0025exact hkp
  26. 0026specialize distinct_primes_bounded_scaled_remainder_nonzero p
  27. 0027specialize distinct_primes_bounded_scaled_remainder_nonzero q
  28. 0028specialize distinct_primes_bounded_scaled_remainder_nonzero i
  29. 0029specialize distinct_primes_bounded_scaled_remainder_nonzero d
  30. 0030specialize distinct_primes_bounded_scaled_remainder_nonzero r
  31. 0031apply distinct_primes_bounded_scaled_remainder_nonzero
  32. 0032exact hp
  33. 0033exact hq
  34. 0034exact hpq
  35. 0035exact hip
  36. 0036exact hdivision
  37. 0037exact hr0