BT0117

factor_pair_has_small_member_below_square

Alpha body-checked · checked-use disabled

A factor pair below (B+1)^2 has a member at most B.

Exact expanded PA statement

forall B n a b. n = a * b -> (exists bpr_gap_bb8fps_bound. bpr_gap_bb8fps_bound + S (n) = S B * S B) -> (exists bpr_le_gap_bb8fps_left. bpr_le_gap_bb8fps_left + (a) = (B)) \/ (exists bpr_le_gap_bb8fps_right. bpr_le_gap_bb8fps_right + (b) = (B))

Structural proof guide

A factor pair below (B+1)^2 has a member at most B.

Direct prerequisites: le_total, le_or_lt, mul_le_mul_right, mul_le_mul_left, le_trans, lt_not_le. The authored body proceeds by case analysis (3), intermediate claims (11), equality transport (2).

Proof neighborhood

Direct dependencies

BT000K le_total BT001G le_or_lt BT001M mul_le_mul_right BT001L mul_le_mul_left BT000F le_trans BT001I lt_not_le

Direct dependents

BT0118 nonprime_has_small_prime_divisor_below_square

Formal native tactic body

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

  1. 0001intro B
  2. 0002intro n
  3. 0003intro a
  4. 0004intro b
  5. 0005intro hfactor
  6. 0006intro hbound
  7. 0007specialize le_total a
  8. 0008specialize le_total b
  9. 0009have horder : (exists k. k + a = b) \/ (exists k. k + b = a)
  10. 0010exact le_total
  11. 0011cases horder
  12. 0012specialize le_or_lt a
  13. 0013specialize le_or_lt B
  14. 0014have hsmall : (exists k. k + a = B) \/ (exists k. k + S B = a)
  15. 0015exact le_or_lt
  16. 0016cases hsmall
  17. 0017left
  18. 0018exact hsmall_left
  19. 0019exfalso
  20. 0020have hsb : exists k. k + S B = b
  21. 0021specialize le_trans (S B)
  22. 0022specialize le_trans a
  23. 0023specialize le_trans b
  24. 0024apply le_trans
  25. 0025exact hsmall_right
  26. 0026exact horder_left
  27. 0027have hfirst : exists k. k + S B * S B = a * S B
  28. 0028specialize mul_le_mul_right (S B)
  29. 0029specialize mul_le_mul_right a
  30. 0030specialize mul_le_mul_right (S B)
  31. 0031apply mul_le_mul_right
  32. 0032exact hsmall_right
  33. 0033have hsquare : exists k. k + S B * S B = a * b
  34. 0034specialize mul_le_mul_left (S B)
  35. 0035specialize mul_le_mul_left b
  36. 0036specialize mul_le_mul_left a
  37. 0037have hsecond : exists k. k + a * S B = a * b
  38. 0038apply mul_le_mul_left
  39. 0039exact hsb
  40. 0040specialize le_trans (S B * S B)
  41. 0041specialize le_trans (a * S B)
  42. 0042specialize le_trans (a * b)
  43. 0043apply le_trans
  44. 0044exact hfirst
  45. 0045exact hsecond
  46. 0046rewrite <- hfactor at hsquare
  47. 0047specialize lt_not_le n
  48. 0048specialize lt_not_le (S B * S B)
  49. 0049apply lt_not_le
  50. 0050exact hbound
  51. 0051exact hsquare
  52. 0052specialize le_or_lt b
  53. 0053specialize le_or_lt B
  54. 0054have hsmall : (exists k. k + b = B) \/ (exists k. k + S B = b)
  55. 0055exact le_or_lt
  56. 0056cases hsmall
  57. 0057right
  58. 0058exact hsmall_left
  59. 0059exfalso
  60. 0060have hsa : exists k. k + S B = a
  61. 0061specialize le_trans (S B)
  62. 0062specialize le_trans b
  63. 0063specialize le_trans a
  64. 0064apply le_trans
  65. 0065exact hsmall_right
  66. 0066exact horder_right
  67. 0067have hfirst : exists k. k + S B * S B = a * S B
  68. 0068specialize mul_le_mul_right (S B)
  69. 0069specialize mul_le_mul_right a
  70. 0070specialize mul_le_mul_right (S B)
  71. 0071apply mul_le_mul_right
  72. 0072exact hsa
  73. 0073have hsecond : exists k. k + a * S B = a * b
  74. 0074specialize mul_le_mul_left (S B)
  75. 0075specialize mul_le_mul_left b
  76. 0076specialize mul_le_mul_left a
  77. 0077apply mul_le_mul_left
  78. 0078exact hsmall_right
  79. 0079have hsquare : exists k. k + S B * S B = a * b
  80. 0080specialize le_trans (S B * S B)
  81. 0081specialize le_trans (a * S B)
  82. 0082specialize le_trans (a * b)
  83. 0083apply le_trans
  84. 0084exact hfirst
  85. 0085exact hsecond
  86. 0086rewrite <- hfactor at hsquare
  87. 0087specialize lt_not_le n
  88. 0088specialize lt_not_le (S B * S B)
  89. 0089apply lt_not_le
  90. 0090exact hbound
  91. 0091exact hsquare