PA002P

base_le_beta_modulus

Stable checked-use theorem · independently closed

A beta base is at most every beta modulus over that base.

Exact expanded PA statement

forall c i. exists h. h + c = S ((S i) * c)

Structural proof guide

Generated structural guide

A beta base is at most every beta modulus over that base.

Use the direct prerequisites le_add_left, mul_succ_left, le_succ as previously established PA formulas.

The proof proceeds by intermediate claims (1), equality transport (1).

Referenced ingredients

PA002J le_add_left PA000G mul_succ_left PA002O le_succ

Proof neighborhood

Direct dependencies

PA002J le_add_left PA000G mul_succ_left PA002O le_succ

Direct dependents

PA002Q new_value_lt_scaled_base PA002T beta_value_lt_scaled_base

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

  1. 0001intro c
  2. 0002intro i
  3. 0003have hproduct : exists h. h + c = S i * c
  4. 0004specialize mul_succ_left i
  5. 0005specialize mul_succ_left c
  6. 0006rewrite mul_succ_left
  7. 0007specialize le_add_left c
  8. 0008specialize le_add_left (i * c)
  9. 0009exact le_add_left
  10. 0010specialize le_succ c
  11. 0011specialize le_succ (S i * c)
  12. 0012apply le_succ
  13. 0013exact hproduct