TS003S · theorem body

prime_square_times_nonzero_strictly_increases

Alpha v34 checked-use · independently kernel and Lean verified; not Stable

Multiplication of a nonzero natural by a prime square is strictly increasing in witnessed constructive order.

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. Prime(p) → ¬q = 0 → Lt(q,p · p · q)

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

PD0002 Lt PD0004 Prime

In local proof propositions

PD0001 Le PD0002 Lt
Exact expanded first-order statement
forall p q. ((~(p = 1) /\ forall frm_prime_left_ftsv_prime frm_prime_right_ftsv_prime. p = frm_prime_left_ftsv_prime * frm_prime_right_ftsv_prime -> frm_prime_left_ftsv_prime = 1 \/ frm_prime_right_ftsv_prime = 1)) -> ~(q = 0) -> exists k. k + S q = (p * p) * q

Proof neighborhood

Direct theorem prerequisites

prime_two_le · Alpha closed succ_le_mul_of_two_le_right · Alpha closed prime_nonzero · Stable closed one_le_of_ne_zero · Stable closed mul_le_mul_left · Stable closed mul_one · Stable closed le_trans · Stable closed mul_assoc · Stable closed mul_comm · Stable closed

Direct theorem dependents

TS003C all_bad_prime_even_two_square_sufficiency_bounded TS003T three_mod_four_prime_two_square_norm_valuation_even_bounded

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

46 script commands · 13 reading checkpoints · 6 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–4

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

  1. L1
    intro p
  2. L2
    intro q
  3. L3
    intro hprime
  4. L4
    intro hquotient
02Establish htwoL5–8

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

  1. L5
  2. L6
    specialize prime_two_le p
  3. L7
    apply prime_two_le
  4. L8
    exact hprime
03Establish hfirstL9–14

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply succ le mul of two le right.

  1. L9
    have hfirst : Lt(q,q · p)Definitions: Lt(q,q · p)Original native command in the exact edition
  2. L10
    specialize succ_le_mul_of_two_le_right q
  3. L11
    specialize succ_le_mul_of_two_le_right p
  4. L12
    apply succ_le_mul_of_two_le_right
  5. L13
    exact hquotient
  6. L14
    exact htwo
04Establish hpnonzeroL15–20

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

  1. L15
    have hpnonzero : ~(p = 0)
  2. L16
    specialize prime_nonzero p
  3. L17
    intro hpzero
  4. L18
    apply prime_nonzero
  5. L19
    exact hprime
  6. L20
    exact hpzero
05Establish honeL21–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply one le of ne zero.

  1. L21
  2. L22
    specialize one_le_of_ne_zero p
  3. L23
    apply one_le_of_ne_zero
  4. L24
    exact hpnonzero
06Establish hsecondL25–32

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

  1. L25
    have hsecond : Le(q · p · 1,q · p · p)Definitions: Le(q · p · 1,q · p · p)Original native command in the exact edition
  2. L26
    specialize mul_le_mul_left 1
  3. L27
    specialize mul_le_mul_left p
  4. L28
    specialize mul_le_mul_left (q * p)
  5. L29
    apply mul_le_mul_left
  6. L30
    exact hone
  7. L31
    specialize mul_one (q * p)
  8. L32
    rewrite mul_one at hsecond
07Establish hcombinedL33–39

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

  1. L33
    have hcombined : Lt(q,q · p · p)Definitions: Lt(q,q · p · p)Original native command in the exact edition
  2. L34
    specialize le_trans (S q)
  3. L35
    specialize le_trans (q * p)
  4. L36
    specialize le_trans ((q * p) * p)
  5. L37
    apply le_trans
  6. L38
    exact hfirst
  7. L39
    exact hsecond
08Separate the logical casesL40–40

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

  1. L40
    cases hcombined
09Construct an explicit witnessL41–41

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

  1. L41
    exists x
10Calculate and transport equalitiesL42–42

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

  1. L42
    trans (q * p) * p
11Use earlier factsL43–43

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

  1. L43
    exact hcombined_witness
12Calculate and transport equalitiesL44–44

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

  1. L44
    trans q * (p * p)
13Use earlier factsL45–46

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

  1. L45
    apply mul_assoc
  2. L46
    apply mul_comm

Library-wide reading audit

Original defined command ledger · 46 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro hprime
  4. 0004intro hquotient
  5. 0005have htwo : Lt(1,p)
    Exact native replay linehave htwo : exists k. k + 2 = p
  6. 0006specialize prime_two_le p
  7. 0007apply prime_two_le
  8. 0008exact hprime
  9. 0009have hfirst : Lt(q,q · p)
    Exact native replay linehave hfirst : exists k. k + S q = q * p
  10. 0010specialize succ_le_mul_of_two_le_right q
  11. 0011specialize succ_le_mul_of_two_le_right p
  12. 0012apply succ_le_mul_of_two_le_right
  13. 0013exact hquotient
  14. 0014exact htwo
  15. 0015have hpnonzero : ~(p = 0)
  16. 0016specialize prime_nonzero p
  17. 0017intro hpzero
  18. 0018apply prime_nonzero
  19. 0019exact hprime
  20. 0020exact hpzero
  21. 0021have hone : Lt(0,p)
    Exact native replay linehave hone : exists k. k + 1 = p
  22. 0022specialize one_le_of_ne_zero p
  23. 0023apply one_le_of_ne_zero
  24. 0024exact hpnonzero
  25. 0025have hsecond : Le(q · p · 1,q · p · p)
    Exact native replay linehave hsecond : exists k. k + (q * p) * 1 = (q * p) * p
  26. 0026specialize mul_le_mul_left 1
  27. 0027specialize mul_le_mul_left p
  28. 0028specialize mul_le_mul_left (q * p)
  29. 0029apply mul_le_mul_left
  30. 0030exact hone
  31. 0031specialize mul_one (q * p)
  32. 0032rewrite mul_one at hsecond
  33. 0033have hcombined : Lt(q,q · p · p)
    Exact native replay linehave hcombined : exists k. k + S q = (q * p) * p
  34. 0034specialize le_trans (S q)
  35. 0035specialize le_trans (q * p)
  36. 0036specialize le_trans ((q * p) * p)
  37. 0037apply le_trans
  38. 0038exact hfirst
  39. 0039exact hsecond
  40. 0040cases hcombined
  41. 0041exists x
  42. 0042trans (q * p) * p
  43. 0043exact hcombined_witness
  44. 0044trans q * (p * p)
  45. 0045apply mul_assoc
  46. 0046apply mul_comm