BT0010

one_le_of_ne_zero

Stable · empty-context checked

Every nonzero natural is at least one.

Exact expanded PA statement

forall n. ~(n = 0) -> 1 <= n

Structural proof guide

Every nonzero natural is at least one.

Direct prerequisites: none. The authored body proceeds by structural induction (1).

Proof neighborhood

Direct dependencies

none

Direct dependents

BT002D divisor_le_nonzero BT0055 le_scaled_nonzero BT00QF prime_power_exponent_le BT00QN prime_power_successor_cancel_cofactor BT00S0 prime_power_quotient_prefix_exists BT00W0 power_valuation_nonzero_exponent_divides_base BT00XG division_double_quotient_bit BT00Y5 central_binom_prime_power_contribution_le_double BT00Y6 central_binom_prime_square_tail_exponent_not_two_le BT00YE central_binom_prime_valuation_zero_two_thirds_range BT00YK no_bertrand_central_nonzero_valuation_factor_ranges

Formal native tactic body

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

  1. 0001induction n
  2. 0002intro h
  3. 0003exfalso
  4. 0004apply h
  5. 0005refl
  6. 0006intro h
  7. 0007exists n
  8. 0008simp