PA00DN · theorem

prime_nondivisor_bounded_scaled_remainder_nonzero

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

A bounded positive factor times a prime nondivisor cannot have zero remainder modulo that prime.

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) → ¬Dvd(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 PD0003 Dvd PD0004 Prime

3 occurrences

In local proof propositions

PD0001 Le PD0003 Dvd

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

PA0038 euclid_prime_dvd_product PA0005 succ_ne_zero PA0039 divisor_le_nonzero PA003A lt_not_le

Direct theorem dependents

PA00DO distinct_primes_bounded_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

40 script commands · 13 reading checkpoints · 4 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 (4)
euclid prime dvd productsucc 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 i
  4. L4
    intro d
  5. L5
    intro r
  6. L6
    intro hp
  7. L7
    intro hpq
  8. L8
    intro hip
  9. L9
    intro hdivision
  10. L10
    intro hr0
02Establish hmultipleL11–11

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

  1. L11
    have hmultiple : Dvd(p,q · S i)Definitions: Dvd(p,q · S i)Original native command in the exact edition
03Construct an explicit witnessL12–12

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

  1. L12
    exists d
04Calculate and transport equalitiesL13–13

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

  1. L13
    trans p * d + r
05Use earlier factsL14–14

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

  1. L14
    exact hdivision
06Calculate and transport equalitiesL15–15

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

  1. L15
    rewrite hr0
07Use earlier factsL16–16

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

  1. L16
    apply PA3
08Establish hsplitL17–23

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

  1. L17
    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. L18
    specialize euclid_prime_dvd_product p
  3. L19
    specialize euclid_prime_dvd_product q
  4. L20
    specialize euclid_prime_dvd_product (S i)
  5. L21
    apply euclid_prime_dvd_product
  6. L22
    exact hp
  7. L23
    exact hmultiple
09Separate the logical casesL24–24

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

  1. L24
    cases hsplit
10Use earlier factsL25–26

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

  1. L25
    apply hpq
  2. L26
    exact hsplit_left
11Establish hsi0L27–29

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

  1. L27
    have hsi0 : ~(S i = 0)
  2. L28
    specialize succ_ne_zero i
  3. L29
    exact succ_ne_zero
12Establish hleL30–39

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

  1. L30
  2. L31
    specialize divisor_le_nonzero p
  3. L32
    specialize divisor_le_nonzero (S i)
  4. L33
    apply divisor_le_nonzero
  5. L34
    exact hsi0
  6. L35
    exact hsplit_right
  7. L36
    specialize lt_not_le (S i)
  8. L37
    specialize lt_not_le p
  9. L38
    apply lt_not_le
  10. L39
    exact hip
13Use earlier factsL40–40

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

  1. L40
    exact hle

Library-wide reading audit

Original defined command ledger · 40 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro i
  4. 0004intro d
  5. 0005intro r
  6. 0006intro hp
  7. 0007intro hpq
  8. 0008intro hip
  9. 0009intro hdivision
  10. 0010intro hr0
  11. 0011have hmultiple : Dvd(p,q · S i)
    Exact native replay linehave hmultiple : exists t. q * S i = p * t
  12. 0012exists d
  13. 0013trans p * d + r
  14. 0014exact hdivision
  15. 0015rewrite hr0
  16. 0016apply PA3
  17. 0017have hsplit : Dvd(p,q) ∨ Dvd(p,S i)
    Exact native replay linehave hsplit : (exists u. q = p * u) \/ exists v. S i = p * v
  18. 0018specialize euclid_prime_dvd_product p
  19. 0019specialize euclid_prime_dvd_product q
  20. 0020specialize euclid_prime_dvd_product (S i)
  21. 0021apply euclid_prime_dvd_product
  22. 0022exact hp
  23. 0023exact hmultiple
  24. 0024cases hsplit
  25. 0025apply hpq
  26. 0026exact hsplit_left
  27. 0027have hsi0 : ~(S i = 0)
  28. 0028specialize succ_ne_zero i
  29. 0029exact succ_ne_zero
  30. 0030have hle : Le(p,S i)
    Exact native replay linehave hle : exists gap. gap + p = S i
  31. 0031specialize divisor_le_nonzero p
  32. 0032specialize divisor_le_nonzero (S i)
  33. 0033apply divisor_le_nonzero
  34. 0034exact hsi0
  35. 0035exact hsplit_right
  36. 0036specialize lt_not_le (S i)
  37. 0037specialize lt_not_le p
  38. 0038apply lt_not_le
  39. 0039exact hip
  40. 0040exact hle