BT00QE

succ_le_mul_of_two_le_right

Alpha body-checked · checked-use disabled

Multiplying a nonzero natural by a factor at least two exceeds it.

Exact expanded PA statement

forall r p. ~(r = 0) -> (exists bpvl_gap_factor_two. bpvl_gap_factor_two + (2) = (p)) -> (exists bpvl_gap_factor_result. bpvl_gap_factor_result + (S r) = (r * p))

Structural proof guide

Multiplying a nonzero natural by a factor at least two exceeds it.

Direct prerequisites: mul_lt_mul_succ_left_nonzero, mul_le_mul_left, mul_one, le_trans. The authored body proceeds by intermediate claims (2), equality transport (1).

Proof neighborhood

Direct dependencies

BT001N mul_lt_mul_succ_left_nonzero BT001L mul_le_mul_left BT000A mul_one BT000F le_trans

Direct dependents

BT00QF prime_power_exponent_le

Formal native tactic body

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

  1. 0001intro r
  2. 0002intro p
  3. 0003intro hr
  4. 0004intro hp
  5. 0005have hstep : exists k. k + S (r * 1) = r * 2
  6. 0006specialize mul_lt_mul_succ_left_nonzero r
  7. 0007specialize mul_lt_mul_succ_left_nonzero 1
  8. 0008apply mul_lt_mul_succ_left_nonzero
  9. 0009exact hr
  10. 0010specialize mul_one r
  11. 0011rewrite mul_one at hstep
  12. 0012have hscaled : exists k. k + r * 2 = r * p
  13. 0013specialize mul_le_mul_left 2
  14. 0014specialize mul_le_mul_left p
  15. 0015specialize mul_le_mul_left r
  16. 0016apply mul_le_mul_left
  17. 0017exact hp
  18. 0018specialize le_trans (S r)
  19. 0019specialize le_trans (r * 2)
  20. 0020specialize le_trans (r * p)
  21. 0021apply le_trans
  22. 0022exact hstep
  23. 0023exact hscaled