theorem proved term proof

`one_not_primeLedgerAtomLogic`

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

formal statement (Lean)

  42theorem one_not_primeLedgerAtomLogic :
  43    ¬ PrimeLedgerAtomLogic (fromNat 1) := by

proof body

Term-mode proof.

  44  intro h
  45  have hp : Nat.Prime (toNat (fromNat 1)) := ledger_atom_logic_is_prime h
  46  rw [toNat_fromNat] at hp
  47  exact Nat.not_prime_one hp
  48

used by (1)

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

primeLedgerLogicCert in IndisputableMonolith.NumberTheory.LogicPrimeLedgerAtom decl_use

depends on (8)

Lean names referenced from this declaration's body.

fromNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
toNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
toNat_fromNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
fromNat in IndisputableMonolith.LedgerUnits decl_use
ledger_atom_logic_is_prime in IndisputableMonolith.NumberTheory.LogicPrimeLedgerAtom decl_use
PrimeLedgerAtomLogic in IndisputableMonolith.NumberTheory.LogicPrimeLedgerAtom decl_use
not_prime_one in IndisputableMonolith.NumberTheory.Primes.Basic decl_use
Prime in IndisputableMonolith.NumberTheory.Primes.Basic decl_use