BT00R5

ceil_div_six_square_six_step

Alpha body-checked · checked-use disabled

Ceil((s+6)^2/6) is exactly Ceil(s^2/6)+2*s+6.

Exact expanded PA statement

forall s e f. (((exists bcs_lower_gap_square_source. bcs_lower_gap_square_source + (s * s) = 6 * (e)) /\ exists bcs_upper_gap_square_source. bcs_upper_gap_square_source + S (6 * (e)) = (s * s) + 6)) -> (((exists bcs_lower_gap_square_target. bcs_lower_gap_square_target + ((s + 6) * (s + 6)) = 6 * (f)) /\ exists bcs_upper_gap_square_target. bcs_upper_gap_square_target + S (6 * (f)) = ((s + 6) * (s + 6)) + 6)) -> f = e + (2 * s + 6)

Structural proof guide

Ceil((s+6)^2/6) is exactly Ceil(s^2/6)+2*s+6.

Direct prerequisites: ceil_div_six_shift, square_six_shift_identity, ceil_div_six_functional. The authored body proceeds by intermediate claims (3), equality transport (2).

Proof neighborhood

Direct dependencies

BT00R0 ceil_div_six_shift BT00R4 square_six_shift_identity BT00R2 ceil_div_six_functional

Direct dependents

BT00SW bertrand_h_six_step_transport_from_total

Formal native tactic body

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

  1. 0001intro s
  2. 0002intro e
  3. 0003intro f
  4. 0004intro he
  5. 0005intro hf
  6. 0006have hshift : ((exists bcs_lower_gap_square_shifted. bcs_lower_gap_square_shifted + (s * s + 6 * (2 * s + 6)) = 6 * (e + (2 * s + 6))) /\ exists bcs_upper_gap_square_shifted. bcs_upper_gap_square_shifted + S (6 * (e + (2 * s + 6))) = (s * s + 6 * (2 * s + 6)) + 6)
  7. 0007specialize ceil_div_six_shift (s * s)
  8. 0008specialize ceil_div_six_shift e
  9. 0009specialize ceil_div_six_shift (2 * s + 6)
  10. 0010apply ceil_div_six_shift
  11. 0011exact he
  12. 0012have hid : s * s + 6 * (2 * s + 6) = (s + 6) * (s + 6)
  13. 0013specialize square_six_shift_identity s
  14. 0014exact square_six_shift_identity
  15. 0015have hnext : ((exists bcs_lower_gap_square_rewritten. bcs_lower_gap_square_rewritten + ((s + 6) * (s + 6)) = 6 * (e + (2 * s + 6))) /\ exists bcs_upper_gap_square_rewritten. bcs_upper_gap_square_rewritten + S (6 * (e + (2 * s + 6))) = ((s + 6) * (s + 6)) + 6)
  16. 0016rewrite <- hid
  17. 0017rewrite <- hid
  18. 0018exact hshift
  19. 0019specialize ceil_div_six_functional ((s + 6) * (s + 6))
  20. 0020specialize ceil_div_six_functional f
  21. 0021specialize ceil_div_six_functional (e + (2 * s + 6))
  22. 0022apply ceil_div_six_functional
  23. 0023exact hf
  24. 0024exact hnext