BT010B

floor_sqrt_two_le_of_two_lt

Alpha body-checked · checked-use disabled

The floor root of twice a natural above two is at least two.

Exact expanded PA statement

forall n s. (exists bcf_lt_gap_b5rbfstl_positive. bcf_lt_gap_b5rbfstl_positive + S (2) = n) -> (((exists bcs_sqrt_lower_gap_b5rbfstl_floor. bcs_sqrt_lower_gap_b5rbfstl_floor + (s) * (s) = (n + n)) /\ exists bcs_sqrt_upper_gap_b5rbfstl_floor. bcs_sqrt_upper_gap_b5rbfstl_floor + S (n + n) = S (s) * S (s))) -> (exists bcf_le_gap_b5rbfstl_result. bcf_le_gap_b5rbfstl_result + (2) = s)

Structural proof guide

The floor root of twice a natural above two is at least two.

Direct prerequisites: le_or_lt, le_refl, le_succ, lt_of_lt_of_le, lt_three_cases, floor_sqrt_strict_upper_bound, two_lt_double_lower_six, le_trans, lt_not_le, lt_irrefl_expanded. The authored body proceeds by case analysis (3), intermediate claims (10), equality transport (5), closed numeral normalization (2).

Proof neighborhood

Direct dependencies

BT001G le_or_lt BT000E le_refl BT0018 le_succ BT001D lt_of_lt_of_le BT0097 lt_three_cases BT00R7 floor_sqrt_strict_upper_bound BT010A two_lt_double_lower_six BT000F le_trans BT001I lt_not_le BT001B lt_irrefl_expanded

Direct dependents

BT010D floor_sqrt_three_mul_le_double

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 hcases : (exists bcf_le_gap_b5rbfstl_result. bcf_le_gap_b5rbfstl_result + (2) = s) \/ (exists bcf_lt_gap_b5rbfstl_reverse. bcf_lt_gap_b5rbfstl_reverse + S (s) = 2)
  6. 0006specialize le_or_lt 2
  7. 0007specialize le_or_lt s
  8. 0008exact le_or_lt
  9. 0009cases hcases
  10. 0010exact hcases_left
  11. 0011have htwo_three : exists k. k + 2 = 3
  12. 0012specialize le_refl 2
  13. 0013specialize le_succ 2
  14. 0014specialize le_succ 2
  15. 0015apply le_succ
  16. 0016exact le_refl
  17. 0017have hthree : exists bcf_lt_gap_b5rbfstl_three. bcf_lt_gap_b5rbfstl_three + S (s) = 3
  18. 0018specialize lt_of_lt_of_le s
  19. 0019specialize lt_of_lt_of_le 2
  20. 0020specialize lt_of_lt_of_le 3
  21. 0021apply lt_of_lt_of_le
  22. 0022exact hcases_right
  23. 0023exact htwo_three
  24. 0024have hsmall_cases : s = 0 \/ s = 1 \/ s = 2
  25. 0025specialize lt_three_cases s
  26. 0026apply lt_three_cases
  27. 0027exact hthree
  28. 0028have hupper : exists bcf_lt_gap_b5rbfstl_upper. bcf_lt_gap_b5rbfstl_upper + S (n + n) = S s * S s
  29. 0029specialize floor_sqrt_strict_upper_bound (n + n)
  30. 0030specialize floor_sqrt_strict_upper_bound s
  31. 0031apply floor_sqrt_strict_upper_bound
  32. 0032exact hfloor
  33. 0033have hlower : exists bcf_le_gap_b5rbfstl_lower_six. bcf_le_gap_b5rbfstl_lower_six + (3 + 3) = n + n
  34. 0034specialize two_lt_double_lower_six n
  35. 0035apply two_lt_double_lower_six
  36. 0036exact hpositive
  37. 0037cases hsmall_cases
  38. 0038cases hsmall_cases_left
  39. 0039rewrite hsmall_cases_left_left at hupper
  40. 0040rewrite hsmall_cases_left_left at hupper
  41. 0041have hsmall : exists bcf_le_gap_b5rbfstl_zero_small. bcf_le_gap_b5rbfstl_zero_small + (S 0 * S 0) = 3 + 3
  42. 0042exists 5
  43. 0043norm_num
  44. 0044have hreverse : exists bcf_le_gap_b5rbfstl_zero_reverse. bcf_le_gap_b5rbfstl_zero_reverse + (S 0 * S 0) = n + n
  45. 0045specialize le_trans (S 0 * S 0)
  46. 0046specialize le_trans (3 + 3)
  47. 0047specialize le_trans (n + n)
  48. 0048apply le_trans
  49. 0049exact hsmall
  50. 0050exact hlower
  51. 0051exfalso
  52. 0052specialize lt_not_le (n + n)
  53. 0053specialize lt_not_le (S 0 * S 0)
  54. 0054apply lt_not_le
  55. 0055exact hupper
  56. 0056exact hreverse
  57. 0057rewrite hsmall_cases_left_right at hupper
  58. 0058rewrite hsmall_cases_left_right at hupper
  59. 0059have hsmall : exists bcf_le_gap_b5rbfstl_one_small. bcf_le_gap_b5rbfstl_one_small + (S 1 * S 1) = 3 + 3
  60. 0060exists 2
  61. 0061norm_num
  62. 0062have hreverse : exists bcf_le_gap_b5rbfstl_one_reverse. bcf_le_gap_b5rbfstl_one_reverse + (S 1 * S 1) = n + n
  63. 0063specialize le_trans (S 1 * S 1)
  64. 0064specialize le_trans (3 + 3)
  65. 0065specialize le_trans (n + n)
  66. 0066apply le_trans
  67. 0067exact hsmall
  68. 0068exact hlower
  69. 0069exfalso
  70. 0070specialize lt_not_le (n + n)
  71. 0071specialize lt_not_le (S 1 * S 1)
  72. 0072apply lt_not_le
  73. 0073exact hupper
  74. 0074exact hreverse
  75. 0075rewrite hsmall_cases_right at hcases_right
  76. 0076exfalso
  77. 0077specialize lt_irrefl_expanded 2
  78. 0078apply lt_irrefl_expanded
  79. 0079exact hcases_right