PA00DO

distinct_primes_bounded_scaled_remainder_nonzero

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

Distinct primes give the nondivisibility needed by the bounded scaled-remainder theorem.

Exact expanded PA statement

forall p q i d r. ((~(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_index_below_p. ern_lt_gap_remainder_nonzero_index_below_p + S (S i) = p) -> q * S i = p * d + r -> ~(r = 0)

Structural proof guide

Generated structural guide

Distinct primes give the nondivisibility needed by the bounded scaled-remainder theorem.

Use the direct prerequisites prime_divisor_eq_one_or_self, prime_nondivisor_bounded_scaled_remainder_nonzero as previously established PA formulas.

The proof proceeds by case analysis (2), intermediate claims (2).

Referenced ingredients

PA0003 prime_divisor_eq_one_or_self PA00DN prime_nondivisor_bounded_scaled_remainder_nonzero

Proof neighborhood

Direct dependencies

PA0003 prime_divisor_eq_one_or_self PA00DN prime_nondivisor_bounded_scaled_remainder_nonzero

Direct dependents

PA00DP distinct_primes_own_odd_half_scaled_remainder_nonzero

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 i
  4. 0004intro d
  5. 0005intro r
  6. 0006intro hp
  7. 0007intro hq
  8. 0008intro hpq
  9. 0009intro hip
  10. 0010intro hdivision
  11. 0011have hnotdiv : ~(exists factor. q = p * factor)
  12. 0012intro hdiv
  13. 0013have hfactor : p = 1 \/ q = p
  14. 0014specialize prime_divisor_eq_one_or_self q
  15. 0015specialize prime_divisor_eq_one_or_self p
  16. 0016apply prime_divisor_eq_one_or_self
  17. 0017exact hq
  18. 0018exact hdiv
  19. 0019cases hfactor
  20. 0020cases hp
  21. 0021apply hp_left
  22. 0022exact hfactor_left
  23. 0023apply hpq
  24. 0024symm
  25. 0025exact hfactor_right
  26. 0026intro hr0
  27. 0027specialize prime_nondivisor_bounded_scaled_remainder_nonzero p
  28. 0028specialize prime_nondivisor_bounded_scaled_remainder_nonzero q
  29. 0029specialize prime_nondivisor_bounded_scaled_remainder_nonzero i
  30. 0030specialize prime_nondivisor_bounded_scaled_remainder_nonzero d
  31. 0031specialize prime_nondivisor_bounded_scaled_remainder_nonzero r
  32. 0032apply prime_nondivisor_bounded_scaled_remainder_nonzero
  33. 0033exact hp
  34. 0034exact hnotdiv
  35. 0035exact hip
  36. 0036exact hdivision
  37. 0037exact hr0