BT00R4 · Bertrand theorem

square_six_shift_identity

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

The six-step square increment is exactly six times 2*s+6.

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 s. s * s + 6 * (2 * s + 6) = (s + 6) * (s + 6)

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

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 s. s * s + 6 * (2 * s + 6) = (s + 6) * (s + 6)

Proof neighborhood

Direct theorem prerequisites

BT00QU two_mul_eq_add_self BT0007 mul_add BT000B add_mul BT0006 mul_comm BT0003 add_assoc

Direct theorem dependents

BT00R5 ceil_div_six_square_six_step

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

39 script commands · 14 reading checkpoints · 3 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)
two mul eq add selfmul addadd mulmul commadd assoc
01Fix variables and assumptionsL1–1

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

  1. L1
    intro s
02Establish htwoL2–3

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

  1. L2
    have htwo : 2 * s = s + s
  2. L3
    apply two_mul_eq_add_self
03Establish hleftL4–12

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

  1. L4
    have hleft : 6 * (2 * s + 6) = (6 * s + 6 * s) + 6 * 6
  2. L5
    trans 6 * (2 * s) + 6 * 6
  3. L6
    apply mul_add
  4. L7
    rewrite htwo
  5. L8
    trans (6 * s + 6 * s) + 6 * 6
  6. L9
    congr
  7. L10
    apply mul_add
  8. L11
    refl
  9. L12
    refl
04Establish hrightL13–22

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

  1. L13
    have hright : (s + 6) * (s + 6) = (s * s + 6 * s) + (6 * s + 6 * 6)
  2. L14
    trans s * (s + 6) + 6 * (s + 6)
  3. L15
    apply add_mul
  4. L16
    trans (s * s + s * 6) + (6 * s + 6 * 6)
  5. L17
    congr
  6. L18
    apply mul_add
  7. L19
    apply mul_add
  8. L20
    trans (s * s + 6 * s) + (6 * s + 6 * 6)
  9. L21
    congr
  10. L22
    congr
05Calculate and transport equalitiesL23–23

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

  1. L23
    refl
06Use earlier factsL24–24

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

  1. L24
    apply mul_comm
07Calculate and transport equalitiesL25–29

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

  1. L25
    refl
  2. L26
    refl
  3. L27
    trans s * s + ((6 * s + 6 * s) + 6 * 6)
  4. L28
    congr
  5. L29
    refl
08Use earlier factsL30–30

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

  1. L30
    exact hleft
09Calculate and transport equalitiesL31–33

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

  1. L31
    trans s * s + (6 * s + (6 * s + 6 * 6))
  2. L32
    congr
  3. L33
    refl
10Use earlier factsL34–34

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

  1. L34
    apply add_assoc
11Calculate and transport equalitiesL35–36

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

  1. L35
    trans (s * s + 6 * s) + (6 * s + 6 * 6)
  2. L36
    symm
12Use earlier factsL37–37

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

  1. L37
    apply add_assoc
13Calculate and transport equalitiesL38–38

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

  1. L38
    symm
14Use earlier factsL39–39

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

  1. L39
    exact hright

Library-wide reading audit

Original defined command ledger · 39 lines
  1. 0001intro s
  2. 0002have htwo : 2 * s = s + s
  3. 0003apply two_mul_eq_add_self
  4. 0004have hleft : 6 * (2 * s + 6) = (6 * s + 6 * s) + 6 * 6
  5. 0005trans 6 * (2 * s) + 6 * 6
  6. 0006apply mul_add
  7. 0007rewrite htwo
  8. 0008trans (6 * s + 6 * s) + 6 * 6
  9. 0009congr
  10. 0010apply mul_add
  11. 0011refl
  12. 0012refl
  13. 0013have hright : (s + 6) * (s + 6) = (s * s + 6 * s) + (6 * s + 6 * 6)
  14. 0014trans s * (s + 6) + 6 * (s + 6)
  15. 0015apply add_mul
  16. 0016trans (s * s + s * 6) + (6 * s + 6 * 6)
  17. 0017congr
  18. 0018apply mul_add
  19. 0019apply mul_add
  20. 0020trans (s * s + 6 * s) + (6 * s + 6 * 6)
  21. 0021congr
  22. 0022congr
  23. 0023refl
  24. 0024apply mul_comm
  25. 0025refl
  26. 0026refl
  27. 0027trans s * s + ((6 * s + 6 * s) + 6 * 6)
  28. 0028congr
  29. 0029refl
  30. 0030exact hleft
  31. 0031trans s * s + (6 * s + (6 * s + 6 * 6))
  32. 0032congr
  33. 0033refl
  34. 0034apply add_assoc
  35. 0035trans (s * s + 6 * s) + (6 * s + 6 * 6)
  36. 0036symm
  37. 0037apply add_assoc
  38. 0038symm
  39. 0039exact hright