BT011P · Bertrand theorem

bertrand_add_six_permute

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

Normalize the six addends used by the 163-to-317 cover.

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 b c d e f. ((a + b) + (c + d)) + (e + f) = (a + e) + ((b + c) + (d + f))

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 a b c d e f. ((a + b) + (c + d)) + (e + f) = (a + e) + ((b + c) + (d + f))

Proof neighborhood

Direct theorem prerequisites

BT0003 add_assoc BT011O bertrand_add_swap_nested

Direct theorem dependents

BT0121 bertrand_cover_one_hundred_sixty_three_three_hundred_seventeen BT0122 bertrand_cover_three_hundred_seventeen_five_hundred_twenty_one

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

49 script commands · 20 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 (2)
add assocbertrand add swap nested
01Fix variables and assumptionsL1–6

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro d
  5. L5
    intro e
  6. L6
    intro f
02Calculate and transport equalitiesL7–8

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

  1. L7
    trans (a + (b + (c + d))) + (e + f)
  2. L8
    congr
03Use earlier factsL9–9

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

  1. L9
    apply add_assoc
04Calculate and transport equalitiesL10–11

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

  1. L10
    refl
  2. L11
    trans a + ((b + (c + d)) + (e + f))
05Use earlier factsL12–12

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

  1. L12
    apply add_assoc
06Calculate and transport equalitiesL13–15

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

  1. L13
    trans a + (b + ((c + d) + (e + f)))
  2. L14
    congr
  3. L15
    refl
07Use earlier factsL16–16

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

  1. L16
    apply add_assoc
08Calculate and transport equalitiesL17–21

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

  1. L17
    trans a + (b + (c + (d + (e + f))))
  2. L18
    congr
  3. L19
    refl
  4. L20
    congr
  5. L21
    refl
09Use earlier factsL22–22

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

  1. L22
    apply add_assoc
10Calculate and transport equalitiesL23–29

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

  1. L23
    trans a + (b + (c + (e + (d + f))))
  2. L24
    congr
  3. L25
    refl
  4. L26
    congr
  5. L27
    refl
  6. L28
    congr
  7. L29
    refl
11Use earlier factsL30–30

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

  1. L30
    apply bertrand_add_swap_nested
12Calculate and transport equalitiesL31–35

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

  1. L31
    trans a + (b + (e + (c + (d + f))))
  2. L32
    congr
  3. L33
    refl
  4. L34
    congr
  5. L35
    refl
13Use earlier factsL36–36

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

  1. L36
    apply bertrand_add_swap_nested
14Calculate and transport equalitiesL37–39

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

  1. L37
    trans a + (e + (b + (c + (d + f))))
  2. L38
    congr
  3. L39
    refl
15Use earlier factsL40–40

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

  1. L40
    apply bertrand_add_swap_nested
16Calculate and transport equalitiesL41–42

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

  1. L41
    trans (a + e) + (b + (c + (d + f)))
  2. L42
    symm
17Use earlier factsL43–43

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

  1. L43
    apply add_assoc
18Calculate and transport equalitiesL44–47

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

  1. L44
    trans (a + e) + ((b + c) + (d + f))
  2. L45
    congr
  3. L46
    refl
  4. L47
    symm
19Use earlier factsL48–48

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

  1. L48
    apply add_assoc
20Calculate and transport equalitiesL49–49

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

  1. L49
    refl

Library-wide reading audit

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