TS0030 · theorem body

prime_square_divisibility_forces_suffix_prime_divisor

dependency-curried kernel-checked candidate body; not enrolled in Alpha or Stable

If a prime square divides a product with one terminal prime factor, that same prime divides the remaining prefix product.

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. ∀ r. ∀ n. Prime(p) → n = r · p → Dvd(p · p,n) → Dvd(p,r)

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

PD0003 Dvd PD0004 Prime

In local proof propositions

none
Exact expanded first-order statement
forall p r n. ((~(p = 1) /\ forall frm_prime_left_ftsp_p frm_prime_right_ftsp_p. p = frm_prime_left_ftsp_p * frm_prime_right_ftsp_p -> frm_prime_left_ftsp_p = 1 \/ frm_prime_right_ftsp_p = 1)) -> n = r * p -> (exists ftcn_factor_ftsp_square. (n) = (p * p) * ftcn_factor_ftsp_square) -> (exists ftcn_factor_ftsp_suffix. (r) = (p) * ftcn_factor_ftsp_suffix)

Proof neighborhood

Direct theorem prerequisites

prime_nonzero · Stable closed mul_left_cancel_nonzero · Stable closed mul_comm · Stable closed mul_assoc · Stable closed

Direct theorem dependents

TS0032 even_valuation_sorted_terminal_prime_has_equal_predecessor

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

29 script commands · 6 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.

01Fix variables and assumptionsL1–6

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

  1. L1
    intro p
  2. L2
    intro r
  3. L3
    intro n
  4. L4
    intro hprime
  5. L5
    intro hproduct
  6. L6
    intro hsquare
02Separate the logical casesL7–7

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

  1. L7
    cases hsquare
03Establish hpnonzeroL8–13

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

  1. L8
    have hpnonzero : ~(p = 0)
  2. L9
    specialize prime_nonzero p
  3. L10
    intro hpzero
  4. L11
    apply prime_nonzero
  5. L12
    exact hprime
  6. L13
    exact hpzero
04Establish hbalanceL14–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul comm.

  1. L14
    have hbalance : p * r = p * (p * x)
  2. L15
    trans r * p
  3. L16
    apply mul_comm
  4. L17
    trans n
  5. L18
    symm
  6. L19
    exact hproduct
  7. L20
    trans (p * p) * x
  8. L21
    exact hsquare_witness
  9. L22
    apply mul_assoc
05Construct an explicit witnessL23–23

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

  1. L23
    exists x
06Use earlier factsL24–29

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

  1. L24
    specialize mul_left_cancel_nonzero p
  2. L25
    specialize mul_left_cancel_nonzero r
  3. L26
    specialize mul_left_cancel_nonzero (p * x)
  4. L27
    apply mul_left_cancel_nonzero
  5. L28
    exact hpnonzero
  6. L29
    exact hbalance

Library-wide reading audit

Original defined command ledger · 29 lines
  1. 0001intro p
  2. 0002intro r
  3. 0003intro n
  4. 0004intro hprime
  5. 0005intro hproduct
  6. 0006intro hsquare
  7. 0007cases hsquare
  8. 0008have hpnonzero : ~(p = 0)
  9. 0009specialize prime_nonzero p
  10. 0010intro hpzero
  11. 0011apply prime_nonzero
  12. 0012exact hprime
  13. 0013exact hpzero
  14. 0014have hbalance : p * r = p * (p * x)
  15. 0015trans r * p
  16. 0016apply mul_comm
  17. 0017trans n
  18. 0018symm
  19. 0019exact hproduct
  20. 0020trans (p * p) * x
  21. 0021exact hsquare_witness
  22. 0022apply mul_assoc
  23. 0023exists x
  24. 0024specialize mul_left_cancel_nonzero p
  25. 0025specialize mul_left_cancel_nonzero r
  26. 0026specialize mul_left_cancel_nonzero (p * x)
  27. 0027apply mul_left_cancel_nonzero
  28. 0028exact hpnonzero
  29. 0029exact hbalance