BT0125

bertrand_closed_upper

Alpha body-checked · checked-use disabled

Every nonzero natural has a prime in its open-closed Bertrand interval.

Exact expanded PA statement

forall n. ~(n = 0) -> exists p. ((~(p = 1) /\ forall a b. p = a * b -> a = 1 \/ b = 1) /\ ((exists u. u + S n = p) /\ (exists v. v + p = n + n)))

Structural proof guide

Every nonzero natural has a prime in its open-closed Bertrand interval.

Direct prerequisites: le_or_lt, bertrand_eventually_closed_upper, bertrand_small_closed_upper. The authored body proceeds by case analysis (1).

Proof neighborhood

Direct dependencies

BT001G le_or_lt BT0115 bertrand_eventually_closed_upper BT0124 bertrand_small_closed_upper

Direct dependents

BT0127 bertrand_strict

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro n
  2. 0002intro hnonzero
  3. 0003specialize le_or_lt (16 * 32)
  4. 0004specialize le_or_lt n
  5. 0005cases le_or_lt
  6. 0006specialize bertrand_eventually_closed_upper n
  7. 0007apply bertrand_eventually_closed_upper
  8. 0008exact le_or_lt_left
  9. 0009specialize bertrand_small_closed_upper n
  10. 0010apply bertrand_small_closed_upper
  11. 0011exact hnonzero
  12. 0012exact le_or_lt_right