PA00DP · theorem

distinct_primes_own_odd_half_scaled_remainder_nonzero

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

An index below the divisor's own odd half has nonzero scaled remainder for a distinct prime multiplier.

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

PD0002 Lt

2 occurrences

Exact expanded native-PA statement
forall p q k i d r. p = 2 * k + 1 -> ((~(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_own_half_bound. ern_lt_gap_remainder_nonzero_own_half_bound + S (i) = k) -> q * S i = p * d + r -> ~(r = 0)

Proof neighborhood

Direct theorem prerequisites

PA00C2 odd_half_strictly_below_modulus PA0033 lt_of_le_of_lt PA00DO distinct_primes_bounded_scaled_remainder_nonzero

Direct theorem dependents

PA00E0 distinct_odd_prime_row_bit_count_equals_division_quotient

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 · 5 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 (3)
odd half strictly below moduluslt of le of ltdistinct primes 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 k
  4. L4
    intro i
  5. L5
    intro d
  6. L6
    intro r
  7. L7
    intro hpodd
  8. L8
    intro hp
  9. L9
    intro hq
  10. L10
    intro hpq
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hik
  2. L12
    intro hdivision
  3. L13
    intro hr0
03Establish hkpL14–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 k
  4. L17
    apply odd_half_strictly_below_modulus
  5. L18
    exact hpodd
04Establish hipL19–28

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 k
  4. L22
    specialize lt_of_le_of_lt p
  5. L23
    apply lt_of_le_of_lt
  6. L24
    exact hik
  7. L25
    exact hkp
  8. L26
    specialize distinct_primes_bounded_scaled_remainder_nonzero p
  9. L27
    specialize distinct_primes_bounded_scaled_remainder_nonzero q
  10. L28
    specialize distinct_primes_bounded_scaled_remainder_nonzero i
05Use earlier factsL29–37

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

  1. L29
    specialize distinct_primes_bounded_scaled_remainder_nonzero d
  2. L30
    specialize distinct_primes_bounded_scaled_remainder_nonzero r
  3. L31
    apply distinct_primes_bounded_scaled_remainder_nonzero
  4. L32
    exact hp
  5. L33
    exact hq
  6. L34
    exact hpq
  7. L35
    exact hip
  8. L36
    exact hdivision
  9. L37
    exact hr0

Library-wide reading audit

Original defined command ledger · 37 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro k
  4. 0004intro i
  5. 0005intro d
  6. 0006intro r
  7. 0007intro hpodd
  8. 0008intro hp
  9. 0009intro hq
  10. 0010intro hpq
  11. 0011intro hik
  12. 0012intro hdivision
  13. 0013intro hr0
  14. 0014have hkp : Lt(k,p)
    Exact native replay linehave hkp : exists ern_lt_gap_remainder_nonzero_half_below_p. ern_lt_gap_remainder_nonzero_half_below_p + S (k) = p
  15. 0015specialize odd_half_strictly_below_modulus p
  16. 0016specialize odd_half_strictly_below_modulus k
  17. 0017apply odd_half_strictly_below_modulus
  18. 0018exact hpodd
  19. 0019have hip : Lt(S i,p)
    Exact native replay linehave hip : exists ern_lt_gap_remainder_nonzero_index_below_p. ern_lt_gap_remainder_nonzero_index_below_p + S (S i) = p
  20. 0020specialize lt_of_le_of_lt (S i)
  21. 0021specialize lt_of_le_of_lt k
  22. 0022specialize lt_of_le_of_lt p
  23. 0023apply lt_of_le_of_lt
  24. 0024exact hik
  25. 0025exact hkp
  26. 0026specialize distinct_primes_bounded_scaled_remainder_nonzero p
  27. 0027specialize distinct_primes_bounded_scaled_remainder_nonzero q
  28. 0028specialize distinct_primes_bounded_scaled_remainder_nonzero i
  29. 0029specialize distinct_primes_bounded_scaled_remainder_nonzero d
  30. 0030specialize distinct_primes_bounded_scaled_remainder_nonzero r
  31. 0031apply distinct_primes_bounded_scaled_remainder_nonzero
  32. 0032exact hp
  33. 0033exact hq
  34. 0034exact hpq
  35. 0035exact hip
  36. 0036exact hdivision
  37. 0037exact hr0