BT00PV

mul_le_mul

Alpha body-checked · checked-use disabled

Multiplication is monotone in both natural-number arguments.

Exact expanded PA statement

forall a b c d. (exists bpo_gap_mul_left. bpo_gap_mul_left + (a) = (b)) -> (exists bpo_gap_mul_right. bpo_gap_mul_right + (c) = (d)) -> (exists bpo_gap_mul_result. bpo_gap_mul_result + (a * c) = (b * d))

Structural proof guide

Multiplication is monotone in both natural-number arguments.

Direct prerequisites: mul_le_mul_right, mul_le_mul_left, le_trans. The authored body proceeds by intermediate claims (2).

Proof neighborhood

Direct dependencies

BT001M mul_le_mul_right BT001L mul_le_mul_left BT000F le_trans

Direct dependents

BT00PY pow_base_monotone BT00SW bertrand_h_six_step_transport_from_total BT00SX bertrand_j_six_step_transport_from_total BT00VV primorial_le_four_pow_bounded BT00W6 pow_six_ten_le_pow_four_thirteen_from_total BT00WF pow_six_six_le_pow_four_eight_from_total BT00WG pow_six_four_le_pow_four_six_from_total BT00WH pow_three_five_block_plus_one_le_pow_four_four_block_plus_one_from_total BT00WJ pow_two_successor_double_le_pow_four_successor_from_total BT00WP bertrand_h_root_32_from_total BT00WQ bertrand_h_root_33_from_total BT00WS bertrand_h_root_35_from_total BT00WT bertrand_h_root_36_from_total BT00WU bertrand_h_root_37_from_total BT00WV bertrand_j_base_thirty_two_window_from_total BT00X4 bertrand_floor_power_product_le_h_from_total BT00X9 beta_product_pointwise_le BT0114 central_binom_le_of_no_bertrand_prime

Formal native tactic body

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

  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro hab
  6. 0006intro hcd
  7. 0007have hacbc : exists k. k + a * c = b * c
  8. 0008specialize mul_le_mul_right a
  9. 0009specialize mul_le_mul_right b
  10. 0010specialize mul_le_mul_right c
  11. 0011apply mul_le_mul_right
  12. 0012exact hab
  13. 0013have hbcbd : exists k. k + b * c = b * d
  14. 0014specialize mul_le_mul_left c
  15. 0015specialize mul_le_mul_left d
  16. 0016specialize mul_le_mul_left b
  17. 0017apply mul_le_mul_left
  18. 0018exact hcd
  19. 0019specialize le_trans (a * c)
  20. 0020specialize le_trans (b * c)
  21. 0021specialize le_trans (b * d)
  22. 0022apply le_trans
  23. 0023exact hacbc
  24. 0024exact hbcbd