pith. machine review for the scientific record. sign in
theorem proved term proof

middle_pairs_are_11_6

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  78theorem middle_pairs_are_11_6 :
  79    ∀ (b c : ℕ), b ∈ natural_invariants_D3 → c ∈ natural_invariants_D3 →
  80    b + c = 17 → b ≠ c →
  81    (b = 6 ∧ c = 11) ∨ (b = 11 ∧ c = 6) ∨
  82    -- Any other pair summing to 17 among our natural invariants
  83    (b = 17 ∧ c = 0) ∨ (b = 0 ∧ c = 17) := by

proof body

Term-mode proof.

  84  intro b c hb hc hsum _hne
  85  simp [natural_invariants_D3, List.mem_cons] at hb hc
  86  omega
  87
  88/-- Excluding zero (since 0 is not a "natural cube invariant"), only
  89    {11, 6} appears in the middle pair position. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.