PA005N · theorem

square_decomp

Stable checked-use theorem · independently closed

Expand a square while retaining an explicit quotient and remainder.

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

forall a z q r. z = a * q + r -> z * z = a * (q * z + r * q) + r * r

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

none

0 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall a z q r. z = a * q + r -> z * z = a * (q * z + r * q) + r * r

Proof neighborhood

Direct theorem prerequisites

PA0009 add_assoc PA000H mul_comm PA000A mul_add PA0016 add_mul PA000B mul_assoc

Direct theorem dependents

PA005P square_residue_lift

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

45 script commands · 22 reading checkpoints · 0 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 (5)
add assocmul commmul addadd mulmul assoc
01Fix variables and assumptionsL1–5

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

  1. L1
    intro a
  2. L2
    intro z
  3. L3
    intro q
  4. L4
    intro r
  5. L5
    intro hz
02Calculate and transport equalitiesL6–7

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

  1. L6
    trans (a * q + r) * z
  2. L7
    congr
03Use earlier factsL8–8

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

  1. L8
    exact hz
04Calculate and transport equalitiesL9–10

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

  1. L9
    refl
  2. L10
    trans (a * q) * z + r * z
05Use earlier factsL11–11

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

  1. L11
    apply add_mul
06Calculate and transport equalitiesL12–13

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

  1. L12
    trans a * (q * z) + r * z
  2. L13
    congr
07Use earlier factsL14–14

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

  1. L14
    apply mul_assoc
08Calculate and transport equalitiesL15–20

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

  1. L15
    refl
  2. L16
    trans a * (q * z) + r * (a * q + r)
  3. L17
    congr
  4. L18
    refl
  5. L19
    congr
  6. L20
    refl
09Use earlier factsL21–21

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

  1. L21
    exact hz
10Calculate and transport equalitiesL22–24

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

  1. L22
    trans a * (q * z) + (r * (a * q) + r * r)
  2. L23
    congr
  3. L24
    refl
11Use earlier factsL25–25

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

  1. L25
    apply mul_add
12Calculate and transport equalitiesL26–31

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

  1. L26
    trans a * (q * z) + (a * (r * q) + r * r)
  2. L27
    congr
  3. L28
    refl
  4. L29
    congr
  5. L30
    trans (r * a) * q
  6. L31
    symm
13Use earlier factsL32–32

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

  1. L32
    apply mul_assoc
14Calculate and transport equalitiesL33–34

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

  1. L33
    trans (a * r) * q
  2. L34
    congr
15Use earlier factsL35–35

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

  1. L35
    apply mul_comm
16Calculate and transport equalitiesL36–36

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

  1. L36
    refl
17Use earlier factsL37–37

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

  1. L37
    apply mul_assoc
18Calculate and transport equalitiesL38–40

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

  1. L38
    refl
  2. L39
    trans (a * (q * z) + a * (r * q)) + r * r
  3. L40
    symm
19Use earlier factsL41–41

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

  1. L41
    apply add_assoc
20Calculate and transport equalitiesL42–43

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

  1. L42
    congr
  2. L43
    symm
21Use earlier factsL44–44

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

  1. L44
    apply mul_add
22Calculate and transport equalitiesL45–45

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

  1. L45
    refl

Library-wide reading audit

Original defined command ledger · 45 lines
  1. 0001intro a
  2. 0002intro z
  3. 0003intro q
  4. 0004intro r
  5. 0005intro hz
  6. 0006trans (a * q + r) * z
  7. 0007congr
  8. 0008exact hz
  9. 0009refl
  10. 0010trans (a * q) * z + r * z
  11. 0011apply add_mul
  12. 0012trans a * (q * z) + r * z
  13. 0013congr
  14. 0014apply mul_assoc
  15. 0015refl
  16. 0016trans a * (q * z) + r * (a * q + r)
  17. 0017congr
  18. 0018refl
  19. 0019congr
  20. 0020refl
  21. 0021exact hz
  22. 0022trans a * (q * z) + (r * (a * q) + r * r)
  23. 0023congr
  24. 0024refl
  25. 0025apply mul_add
  26. 0026trans a * (q * z) + (a * (r * q) + r * r)
  27. 0027congr
  28. 0028refl
  29. 0029congr
  30. 0030trans (r * a) * q
  31. 0031symm
  32. 0032apply mul_assoc
  33. 0033trans (a * r) * q
  34. 0034congr
  35. 0035apply mul_comm
  36. 0036refl
  37. 0037apply mul_assoc
  38. 0038refl
  39. 0039trans (a * (q * z) + a * (r * q)) + r * r
  40. 0040symm
  41. 0041apply add_assoc
  42. 0042congr
  43. 0043symm
  44. 0044apply mul_add
  45. 0045refl