PA00DO · theorem

distinct_primes_bounded_scaled_remainder_nonzero

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

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

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. ∀ i. ∀ d. ∀ r. Prime(p) → Prime(q) → ¬p = q → Lt(S i,p) → q · S i = p · d + r → ¬r = 0

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

3 occurrences

In local proof propositions

PD0003 Dvd

1 occurrences

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

Proof neighborhood

Direct theorem prerequisites

PA0003 prime_divisor_eq_one_or_self PA00DN prime_nondivisor_bounded_scaled_remainder_nonzero

Direct theorem dependents

PA00DP distinct_primes_own_odd_half_scaled_remainder_nonzero

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

37 script commands · 10 reading checkpoints · 2 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 (2)
prime divisor eq one or selfprime nondivisor bounded scaled remainder nonzero
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 i
  4. L4
    intro d
  5. L5
    intro r
  6. L6
    intro hp
  7. L7
    intro hq
  8. L8
    intro hpq
  9. L9
    intro hip
  10. L10
    intro hdivision
02Establish hnotdivL11–12

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

  1. L11
    have hnotdiv : ¬Dvd(p,q)Definitions: Dvd(p,q)Original native command in the exact edition
  2. L12
    intro hdiv
03Establish hfactorL13–18

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. L13
    have hfactor : p = 1 \/ q = p
  2. L14
    specialize prime_divisor_eq_one_or_self q
  3. L15
    specialize prime_divisor_eq_one_or_self p
  4. L16
    apply prime_divisor_eq_one_or_self
  5. L17
    exact hq
  6. L18
    exact hdiv
04Separate the logical casesL19–20

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

  1. L19
    cases hfactor
  2. L20
    cases hp
05Use earlier factsL21–23

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

  1. L21
    apply hp_left
  2. L22
    exact hfactor_left
  3. L23
    apply hpq
06Calculate and transport equalitiesL24–24

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

  1. L24
    symm
07Use earlier factsL25–25

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

  1. L25
    exact hfactor_right
08Fix variables and assumptionsL26–26

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

  1. L26
    intro hr0
09Use earlier factsL27–36

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

  1. L27
    specialize prime_nondivisor_bounded_scaled_remainder_nonzero p
  2. L28
    specialize prime_nondivisor_bounded_scaled_remainder_nonzero q
  3. L29
    specialize prime_nondivisor_bounded_scaled_remainder_nonzero i
  4. L30
    specialize prime_nondivisor_bounded_scaled_remainder_nonzero d
  5. L31
    specialize prime_nondivisor_bounded_scaled_remainder_nonzero r
  6. L32
    apply prime_nondivisor_bounded_scaled_remainder_nonzero
  7. L33
    exact hp
  8. L34
    exact hnotdiv
  9. L35
    exact hip
  10. L36
    exact hdivision
10Use earlier factsL37–37

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

  1. L37
    exact hr0

Library-wide reading audit

Original defined command ledger · 37 lines
  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 : ¬Dvd(p,q)
    Exact native replay linehave 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