PA00DO

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.

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)) -> ((~(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)

Structural proof guide

Generated structural guide

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

Use the direct prerequisites prime_divisor_eq_one_or_self, prime_nondivisor_bounded_scaled_remainder_nonzero as previously established PA formulas.

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

Referenced ingredients

PA0003 prime_divisor_eq_one_or_self PA00DN prime_nondivisor_bounded_scaled_remainder_nonzero

Proof neighborhood

Direct dependencies

PA0003 prime_divisor_eq_one_or_self PA00DN prime_nondivisor_bounded_scaled_remainder_nonzero

Direct dependents

PA00DP distinct_primes_own_odd_half_scaled_remainder_nonzero

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

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.

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