PA00D8

distinct_odd_prime_half_products_ne

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

Distinct odd primes have no bounded positive point on q*x=p*y.

Exact expanded PA statement

forall p q h k i j. p = 2 * h + 1 -> q = 2 * k + 1 -> ((~(p = 1) /\ forall frp_prime_left_lattice_prime_p frp_prime_right_lattice_prime_p. p = frp_prime_left_lattice_prime_p * frp_prime_right_lattice_prime_p -> frp_prime_left_lattice_prime_p = 1 \/ frp_prime_right_lattice_prime_p = 1)) -> ((~(q = 1) /\ forall frp_prime_left_lattice_prime_q frp_prime_right_lattice_prime_q. q = frp_prime_left_lattice_prime_q * frp_prime_right_lattice_prime_q -> frp_prime_left_lattice_prime_q = 1 \/ frp_prime_right_lattice_prime_q = 1)) -> ~(p = q) -> (exists elo_gap_lattice_i_bound. elo_gap_lattice_i_bound + S (i) = h) -> (exists elo_gap_lattice_j_bound. elo_gap_lattice_j_bound + S (j) = k) -> ~(q * S i = p * S j)

Structural proof guide

Generated structural guide

Distinct odd primes have no bounded positive point on q*x=p*y.

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

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

Referenced ingredients

PA00C2 odd_half_strictly_below_modulus PA0033 lt_of_le_of_lt PA0038 euclid_prime_dvd_product PA0003 prime_divisor_eq_one_or_self PA0005 succ_ne_zero PA0039 divisor_le_nonzero PA003A lt_not_le

Proof neighborhood

Direct dependencies

PA00C2 odd_half_strictly_below_modulus PA0033 lt_of_le_of_lt PA0038 euclid_prime_dvd_product PA0003 prime_divisor_eq_one_or_self PA0005 succ_ne_zero PA0039 divisor_le_nonzero PA003A lt_not_le

Direct dependents

PA00D9 distinct_odd_prime_half_cell_oriented

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 h
  4. 0004intro k
  5. 0005intro i
  6. 0006intro j
  7. 0007intro hpodd
  8. 0008intro hqodd
  9. 0009intro hp
  10. 0010intro hq
  11. 0011intro hpq
  12. 0012intro hi
  13. 0013intro hj
  14. 0014have hhalf : exists elo_gap_lattice_half_below_p. elo_gap_lattice_half_below_p + S (h) = p
  15. 0015specialize odd_half_strictly_below_modulus p
  16. 0016specialize odd_half_strictly_below_modulus h
  17. 0017apply odd_half_strictly_below_modulus
  18. 0018exact hpodd
  19. 0019have hip : exists elo_gap_lattice_i_below_p. elo_gap_lattice_i_below_p + S (S i) = p
  20. 0020specialize lt_of_le_of_lt (S i)
  21. 0021specialize lt_of_le_of_lt h
  22. 0022specialize lt_of_le_of_lt p
  23. 0023apply lt_of_le_of_lt
  24. 0024exact hi
  25. 0025exact hhalf
  26. 0026intro heq
  27. 0027have hpdiv : exists t. q * S i = p * t
  28. 0028exists S j
  29. 0029exact heq
  30. 0030have hsplit : (exists u. q = p * u) \/ exists v. S i = p * v
  31. 0031specialize euclid_prime_dvd_product p
  32. 0032specialize euclid_prime_dvd_product q
  33. 0033specialize euclid_prime_dvd_product (S i)
  34. 0034apply euclid_prime_dvd_product
  35. 0035exact hp
  36. 0036exact hpdiv
  37. 0037cases hsplit
  38. 0038have hfactor : p = 1 \/ q = p
  39. 0039specialize prime_divisor_eq_one_or_self q
  40. 0040specialize prime_divisor_eq_one_or_self p
  41. 0041apply prime_divisor_eq_one_or_self
  42. 0042exact hq
  43. 0043exact hsplit_left
  44. 0044cases hfactor
  45. 0045cases hp
  46. 0046apply hp_left
  47. 0047exact hfactor_left
  48. 0048apply hpq
  49. 0049symm
  50. 0050exact hfactor_right
  51. 0051have hsi0 : ~(S i = 0)
  52. 0052specialize succ_ne_zero i
  53. 0053exact succ_ne_zero
  54. 0054have hle : exists gap. gap + p = S i
  55. 0055specialize divisor_le_nonzero p
  56. 0056specialize divisor_le_nonzero (S i)
  57. 0057apply divisor_le_nonzero
  58. 0058exact hsi0
  59. 0059exact hsplit_right
  60. 0060specialize lt_not_le (S i)
  61. 0061specialize lt_not_le p
  62. 0062apply lt_not_le
  63. 0063exact hip
  64. 0064exact hle