BT0054

base_le_beta_modulus

Stable · empty-context checked

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

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

Direct prerequisites: le_add_left, mul_succ_left, le_succ. The authored body proceeds by intermediate claims (1), equality transport (1).

Proof neighborhood

Direct dependencies

BT0012 le_add_left BT0005 mul_succ_left BT0018 le_succ

Direct dependents

BT0057 beta_value_lt_scaled_base BT0058 new_value_lt_scaled_base

Formal native tactic body

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

  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