BT003E

factor_search_up_to

Stable · empty-context checked

Constructively decide whether a nonzero natural has a bounded nontrivial factor pair.

Exact expanded PA statement

forall B n. ~(n = 0) -> ((forall c d. (exists k. k + c = B) -> n = c * d -> c = 1 \/ d = 1) \/ exists c d. ((((exists k. k + c = B) /\ ~(c = 1)) /\ ~(d = 1)) /\ n = c * d))

Structural proof guide

Constructively decide whether a nonzero natural has a bounded nontrivial factor pair.

Direct prerequisites: mul_zero_left, succ_ne_zero, le_zero, le_refl, le_succ, mul_left_cancel_nonzero, eq_decidable, multiple_decidable_nonzero, factor_property_succ. The authored body proceeds by structural induction (1), case analysis (10), intermediate claims (6), equality transport (1).

Proof neighborhood

Direct dependencies

BT0004 mul_zero_left BT000C succ_ne_zero BT000Y le_zero BT000E le_refl BT0018 le_succ BT0022 mul_left_cancel_nonzero BT003A eq_decidable BT003B multiple_decidable_nonzero BT003D factor_property_succ

Direct dependents

BT003F prime_or_composite

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. 0002induction B
  3. 0003intro n
  4. 0004intro hn
  5. 0005left
  6. 0006intro c
  7. 0007intro d
  8. 0008intro hc
  9. 0009intro hfac
  10. 0010have hc0 : c = 0
  11. 0011apply le_zero
  12. 0012exact hc
  13. 0013exfalso
  14. 0014apply hn
  15. 0015trans c * d
  16. 0016exact hfac
  17. 0017rewrite hc0
  18. 0018apply mul_zero_left
  19. 0019intro n
  20. 0020intro hn
  21. 0021specialize IH n
  22. 0022have hprev : (forall c d. (exists k. k + c = B) -> n = c * d -> c = 1 \/ d = 1) \/ exists c d. ((((exists k. k + c = B) /\ ~(c = 1)) /\ ~(d = 1)) /\ n = c * d)
  23. 0023apply IH
  24. 0024exact hn
  25. 0025cases hprev
  26. 0026have hs0 : ~(S B = 0)
  27. 0027specialize succ_ne_zero B
  28. 0028exact succ_ne_zero
  29. 0029specialize multiple_decidable_nonzero (S B)
  30. 0030specialize multiple_decidable_nonzero n
  31. 0031have hdiv : (exists q. n = S B * q) \/ ~(exists q. n = S B * q)
  32. 0032apply multiple_decidable_nonzero
  33. 0033exact hs0
  34. 0034cases hdiv
  35. 0035cases hdiv_left
  36. 0036specialize eq_decidable (S B)
  37. 0037specialize eq_decidable 1
  38. 0038have hc1 : S B = 1 \/ ~(S B = 1)
  39. 0039apply eq_decidable
  40. 0040cases hc1
  41. 0041left
  42. 0042apply factor_property_succ
  43. 0043exact hprev_left
  44. 0044intro d
  45. 0045intro hboundary
  46. 0046left
  47. 0047exact hc1_left
  48. 0048specialize eq_decidable_before x
  49. 0049specialize eq_decidable_before 1
  50. 0050have hq1 : x = 1 \/ ~(x = 1)
  51. 0051apply eq_decidable_before
  52. 0052cases hq1
  53. 0053left
  54. 0054apply factor_property_succ
  55. 0055exact hprev_left
  56. 0056intro d
  57. 0057intro hboundary
  58. 0058right
  59. 0059trans x
  60. 0060apply mul_left_cancel_nonzero
  61. 0061exact hs0
  62. 0062trans n
  63. 0063symm
  64. 0064exact hboundary
  65. 0065exact hdiv_left_witness
  66. 0066exact hq1_left
  67. 0067right
  68. 0068exists S B
  69. 0069exists x
  70. 0070split
  71. 0071split
  72. 0072split
  73. 0073apply le_refl
  74. 0074exact hc1_right
  75. 0075exact hq1_right
  76. 0076exact hdiv_left_witness
  77. 0077left
  78. 0078apply factor_property_succ
  79. 0079exact hprev_left
  80. 0080intro d
  81. 0081intro hboundary
  82. 0082exfalso
  83. 0083apply hdiv_right
  84. 0084exists d
  85. 0085exact hboundary
  86. 0086right
  87. 0087cases hprev_right
  88. 0088cases hprev_right_witness
  89. 0089cases hprev_right_witness_witness
  90. 0090cases hprev_right_witness_witness_left
  91. 0091cases hprev_right_witness_witness_left_left
  92. 0092exists x
  93. 0093exists x1
  94. 0094split
  95. 0095split
  96. 0096split
  97. 0097apply le_succ
  98. 0098exact hprev_right_witness_witness_left_left_left
  99. 0099exact hprev_right_witness_witness_left_left_right
  100. 0100exact hprev_right_witness_witness_left_right
  101. 0101exact hprev_right_witness_witness_right