BT010D

floor_sqrt_three_mul_le_double

Alpha body-checked · checked-use disabled

Three times the floor root lies below the doubled input.

Exact expanded PA statement

forall n s. (exists bcf_lt_gap_b5rbfstmd_positive. bcf_lt_gap_b5rbfstmd_positive + S (2) = n) -> (((exists bcs_sqrt_lower_gap_b5rbfstmd_floor. bcs_sqrt_lower_gap_b5rbfstmd_floor + (s) * (s) = (n + n)) /\ exists bcs_sqrt_upper_gap_b5rbfstmd_floor. bcs_sqrt_upper_gap_b5rbfstmd_floor + S (n + n) = S (s) * S (s))) -> (exists bcf_le_gap_b5rbfstmd_result. bcf_le_gap_b5rbfstmd_result + (3 * s) = n + n)

Structural proof guide

Three times the floor root lies below the doubled input.

Direct prerequisites: two_lt_double_lower_six, floor_sqrt_two_le_of_two_lt, three_mul_le_square_of_three_le, le_eq_or_lt, floor_sqrt_lower_bound, le_trans. The authored body proceeds by case analysis (1), intermediate claims (7), equality transport (2), closed numeral normalization (1).

Proof neighborhood

Direct dependencies

BT010A two_lt_double_lower_six BT010B floor_sqrt_two_le_of_two_lt BT010C three_mul_le_square_of_three_le BT001C le_eq_or_lt BT00R6 floor_sqrt_lower_bound BT000F le_trans

Direct dependents

BT010F floor_sqrt_le_third_quotient

Formal native tactic body

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

  1. 0001intro n
  2. 0002intro s
  3. 0003intro hpositive
  4. 0004intro hfloor
  5. 0005have htwo : exists bcf_le_gap_b5rbfstmd_two. bcf_le_gap_b5rbfstmd_two + (2) = s
  6. 0006specialize floor_sqrt_two_le_of_two_lt n
  7. 0007specialize floor_sqrt_two_le_of_two_lt s
  8. 0008apply floor_sqrt_two_le_of_two_lt
  9. 0009exact hpositive
  10. 0010exact hfloor
  11. 0011have hsplit : 2 = s \/ (exists bcf_lt_gap_b5rbfstmd_strict. bcf_lt_gap_b5rbfstmd_strict + S (2) = s)
  12. 0012specialize le_eq_or_lt 2
  13. 0013specialize le_eq_or_lt s
  14. 0014apply le_eq_or_lt
  15. 0015exact htwo
  16. 0016cases hsplit
  17. 0017have hlower : exists bcf_le_gap_b5rbfstmd_lower_six. bcf_le_gap_b5rbfstmd_lower_six + (3 + 3) = n + n
  18. 0018specialize two_lt_double_lower_six n
  19. 0019apply two_lt_double_lower_six
  20. 0020exact hpositive
  21. 0021rewrite <- hsplit_left
  22. 0022have hcalc : 3 * 2 = 3 + 3
  23. 0023norm_num
  24. 0024rewrite hcalc
  25. 0025exact hlower
  26. 0026have hthree : exists bcf_le_gap_b5rbfstmd_three. bcf_le_gap_b5rbfstmd_three + (3) = s
  27. 0027exact hsplit_right
  28. 0028have hsquare : exists bcf_le_gap_b5rbfstmd_square. bcf_le_gap_b5rbfstmd_square + (3 * s) = s * s
  29. 0029specialize three_mul_le_square_of_three_le s
  30. 0030apply three_mul_le_square_of_three_le
  31. 0031exact hthree
  32. 0032have hfloor_lower : exists bcf_le_gap_b5rbfstmd_floor_lower. bcf_le_gap_b5rbfstmd_floor_lower + (s * s) = n + n
  33. 0033specialize floor_sqrt_lower_bound (n + n)
  34. 0034specialize floor_sqrt_lower_bound s
  35. 0035apply floor_sqrt_lower_bound
  36. 0036exact hfloor
  37. 0037specialize le_trans (3 * s)
  38. 0038specialize le_trans (s * s)
  39. 0039specialize le_trans (n + n)
  40. 0040apply le_trans
  41. 0041exact hsquare
  42. 0042exact hfloor_lower