TS000C · theorem body

prime_is_not_natural_square

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

No natural square satisfies the nonunit factor-pair definition of primality.

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. ∀ s. Prime(p) → ¬p = s · s

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

PD0004 Prime

In local proof propositions

none
Exact expanded first-order statement
forall p s. ((~(p = 1) /\ forall frm_prime_left_ftsp_prime frm_prime_right_ftsp_prime. p = frm_prime_left_ftsp_prime * frm_prime_right_ftsp_prime -> frm_prime_left_ftsp_prime = 1 \/ frm_prime_right_ftsp_prime = 1)) -> ~(p = s * s)

Proof neighborhood

Direct theorem prerequisites

none

Direct theorem dependents

TS000E prime_floor_square_strictly_below_prime

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

21 script commands · 8 reading checkpoints · 1 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 s
  3. L3
    intro hprime
  4. L4
    intro hsquare
02Separate the logical casesL5–5

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

  1. L5
    cases hprime
03Establish hfactorL6–10

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

  1. L6
    have hfactor : s = 1 \/ s = 1
  2. L7
    specialize hprime_right s
  3. L8
    specialize hprime_right s
  4. L9
    apply hprime_right
  5. L10
    exact hsquare
04Separate the logical casesL11–11

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

  1. L11
    cases hfactor
05Use earlier factsL12–12

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

  1. L12
    apply hprime_left
06Calculate and transport equalitiesL13–16

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

  1. L13
    rewrite hsquare
  2. L14
    rewrite hfactor_left
  3. L15
    rewrite hfactor_left
  4. L16
    norm_num
07Use earlier factsL17–17

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

  1. L17
    apply hprime_left
08Calculate and transport equalitiesL18–21

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

  1. L18
    rewrite hsquare
  2. L19
    rewrite hfactor_right
  3. L20
    rewrite hfactor_right
  4. L21
    norm_num

Library-wide reading audit

Original defined command ledger · 21 lines
  1. 0001intro p
  2. 0002intro s
  3. 0003intro hprime
  4. 0004intro hsquare
  5. 0005cases hprime
  6. 0006have hfactor : s = 1 \/ s = 1
  7. 0007specialize hprime_right s
  8. 0008specialize hprime_right s
  9. 0009apply hprime_right
  10. 0010exact hsquare
  11. 0011cases hfactor
  12. 0012apply hprime_left
  13. 0013rewrite hsquare
  14. 0014rewrite hfactor_left
  15. 0015rewrite hfactor_left
  16. 0016norm_num
  17. 0017apply hprime_left
  18. 0018rewrite hsquare
  19. 0019rewrite hfactor_right
  20. 0020rewrite hfactor_right
  21. 0021norm_num