PA00D8 · theorem

distinct_odd_prime_half_products_ne

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

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

∀ p. ∀ q. ∀ h. ∀ k. ∀ i. ∀ j. p = 2 · h + 1 → q = 2 · k + 1 → Prime(p) → Prime(q) → ¬p = q → Lt(i,h) → Lt(j,k) → ¬q · S i = p · S j

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0004 Prime

4 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0003 Dvd

6 occurrences

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

Proof neighborhood

Direct theorem prerequisites

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 theorem dependents

PA00D9 distinct_odd_prime_half_cell_oriented

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

64 script commands · 17 reading checkpoints · 7 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (7)
odd half strictly below moduluslt of le of lteuclid prime dvd productprime divisor eq one or selfsucc ne zerodivisor le nonzerolt not le
01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro q
  3. L3
    intro h
  4. L4
    intro k
  5. L5
    intro i
  6. L6
    intro j
  7. L7
    intro hpodd
  8. L8
    intro hqodd
  9. L9
    intro hp
  10. L10
    intro hq
02Fix variables and assumptionsL11–13

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro hpq
  2. L12
    intro hi
  3. L13
    intro hj
03Establish hhalfL14–18

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply odd half strictly below modulus.

  1. L14
  2. L15
    specialize odd_half_strictly_below_modulus p
  3. L16
    specialize odd_half_strictly_below_modulus h
  4. L17
    apply odd_half_strictly_below_modulus
  5. L18
    exact hpodd
04Establish hipL19–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lt of le of lt.

  1. L19
  2. L20
    specialize lt_of_le_of_lt (S i)
  3. L21
    specialize lt_of_le_of_lt h
  4. L22
    specialize lt_of_le_of_lt p
  5. L23
    apply lt_of_le_of_lt
  6. L24
    exact hi
  7. L25
    exact hhalf
  8. L26
    intro heq
05Establish hpdivL27–27

Establish this local claim before using it. It is not an additional assumption.

  1. L27
    have hpdiv : Dvd(p,q · S i)Definitions: Dvd(p,q · S i)Original native command in the exact edition
06Construct an explicit witnessL28–28

Supply the displayed value, then prove that it has the required property.

  1. L28
    exists S j
07Use earlier factsL29–29

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L29
    exact heq
08Establish hsplitL30–36

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply euclid prime dvd product.

  1. L30
    have hsplit : Dvd(p,q) ∨ Dvd(p,S i)Definitions: Dvd(p,q)Dvd(p,S i)Original native command in the exact edition
  2. L31
    specialize euclid_prime_dvd_product p
  3. L32
    specialize euclid_prime_dvd_product q
  4. L33
    specialize euclid_prime_dvd_product (S i)
  5. L34
    apply euclid_prime_dvd_product
  6. L35
    exact hp
  7. L36
    exact hpdiv
09Separate the logical casesL37–37

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L37
    cases hsplit
10Establish hfactorL38–43

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime divisor eq one or self.

  1. L38
    have hfactor : p = 1 \/ q = p
  2. L39
    specialize prime_divisor_eq_one_or_self q
  3. L40
    specialize prime_divisor_eq_one_or_self p
  4. L41
    apply prime_divisor_eq_one_or_self
  5. L42
    exact hq
  6. L43
    exact hsplit_left
11Separate the logical casesL44–45

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L44
    cases hfactor
  2. L45
    cases hp
12Use earlier factsL46–48

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L46
    apply hp_left
  2. L47
    exact hfactor_left
  3. L48
    apply hpq
13Calculate and transport equalitiesL49–49

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L49
    symm
14Use earlier factsL50–50

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L50
    exact hfactor_right
15Establish hsi0L51–53

Establish this local claim before using it. It is not an additional assumption.

  1. L51
    have hsi0 : ~(S i = 0)
  2. L52
    specialize succ_ne_zero i
  3. L53
    exact succ_ne_zero
16Establish hleL54–63

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor le nonzero.

  1. L54
  2. L55
    specialize divisor_le_nonzero p
  3. L56
    specialize divisor_le_nonzero (S i)
  4. L57
    apply divisor_le_nonzero
  5. L58
    exact hsi0
  6. L59
    exact hsplit_right
  7. L60
    specialize lt_not_le (S i)
  8. L61
    specialize lt_not_le p
  9. L62
    apply lt_not_le
  10. L63
    exact hip
17Use earlier factsL64–64

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L64
    exact hle

Library-wide reading audit

Original defined command ledger · 64 lines
  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 : Lt(h,p)
    Exact native replay linehave 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 : Lt(S i,p)
    Exact native replay linehave 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 : Dvd(p,q · S i)
    Exact native replay linehave hpdiv : exists t. q * S i = p * t
  28. 0028exists S j
  29. 0029exact heq
  30. 0030have hsplit : Dvd(p,q) ∨ Dvd(p,S i)
    Exact native replay linehave 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 : Le(p,S i)
    Exact native replay linehave 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