PA00DN

prime_nondivisor_bounded_scaled_remainder_nonzero

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

A bounded positive factor times a prime nondivisor cannot have zero remainder modulo that prime.

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)) -> (~(exists factor. q = p * factor)) -> (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

A bounded positive factor times a prime nondivisor cannot have zero remainder modulo that prime.

Use the direct prerequisites euclid_prime_dvd_product, succ_ne_zero, divisor_le_nonzero, lt_not_le as previously established PA formulas.

The proof proceeds by case analysis (1), intermediate claims (4), equality transport (1).

Referenced ingredients

PA0038 euclid_prime_dvd_product PA0005 succ_ne_zero PA0039 divisor_le_nonzero PA003A lt_not_le

Proof neighborhood

Direct dependencies

PA0038 euclid_prime_dvd_product PA0005 succ_ne_zero PA0039 divisor_le_nonzero PA003A lt_not_le

Direct dependents

PA00DO distinct_primes_bounded_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 hpq
  8. 0008intro hip
  9. 0009intro hdivision
  10. 0010intro hr0
  11. 0011have hmultiple : exists t. q * S i = p * t
  12. 0012exists d
  13. 0013trans p * d + r
  14. 0014exact hdivision
  15. 0015rewrite hr0
  16. 0016apply PA3
  17. 0017have hsplit : (exists u. q = p * u) \/ exists v. S i = p * v
  18. 0018specialize euclid_prime_dvd_product p
  19. 0019specialize euclid_prime_dvd_product q
  20. 0020specialize euclid_prime_dvd_product (S i)
  21. 0021apply euclid_prime_dvd_product
  22. 0022exact hp
  23. 0023exact hmultiple
  24. 0024cases hsplit
  25. 0025apply hpq
  26. 0026exact hsplit_left
  27. 0027have hsi0 : ~(S i = 0)
  28. 0028specialize succ_ne_zero i
  29. 0029exact succ_ne_zero
  30. 0030have hle : exists gap. gap + p = S i
  31. 0031specialize divisor_le_nonzero p
  32. 0032specialize divisor_le_nonzero (S i)
  33. 0033apply divisor_le_nonzero
  34. 0034exact hsi0
  35. 0035exact hsplit_right
  36. 0036specialize lt_not_le (S i)
  37. 0037specialize lt_not_le p
  38. 0038apply lt_not_le
  39. 0039exact hip
  40. 0040exact hle