PA00BY

beta_division_prefix_exists

Alpha v16 checked-use theorem · independently closed; not Stable

Every finite beta source prefix has beta-coded quotients and bounded remainders for a nonzero modulus.

Exact expanded PA statement

forall p b c l. ~(p = 0) -> exists qb qc rb rc. (forall fdp_index_exists_result. (exists gsp_lt_gap_exists_result_index_bound. gsp_lt_gap_exists_result_index_bound + S fdp_index_exists_result = l) -> exists fdp_value_exists_result fdp_quotient_exists_result fdp_remainder_exists_result. (((exists ff_h_fdp_exists_result_source. ff_h_fdp_exists_result_source + S (fdp_value_exists_result) = S ((S (fdp_index_exists_result)) * c)) /\ exists ff_q_fdp_exists_result_source. b = ff_q_fdp_exists_result_source * S ((S (fdp_index_exists_result)) * c) + (fdp_value_exists_result))) /\ ((((exists ff_h_fdp_exists_result_quotient_entry. ff_h_fdp_exists_result_quotient_entry + S (fdp_quotient_exists_result) = S ((S (fdp_index_exists_result)) * qc)) /\ exists ff_q_fdp_exists_result_quotient_entry. qb = ff_q_fdp_exists_result_quotient_entry * S ((S (fdp_index_exists_result)) * qc) + (fdp_quotient_exists_result))) /\ ((((exists ff_h_fdp_exists_result_remainder_entry. ff_h_fdp_exists_result_remainder_entry + S (fdp_remainder_exists_result) = S ((S (fdp_index_exists_result)) * rc)) /\ exists ff_q_fdp_exists_result_remainder_entry. rb = ff_q_fdp_exists_result_remainder_entry * S ((S (fdp_index_exists_result)) * rc) + (fdp_remainder_exists_result))) /\ (fdp_value_exists_result = p * fdp_quotient_exists_result + fdp_remainder_exists_result /\ (exists gsp_lt_gap_exists_result_remainder_bound. gsp_lt_gap_exists_result_remainder_bound + S fdp_remainder_exists_result = p)))))

Structural proof guide

Generated structural guide

Every finite beta source prefix has beta-coded quotients and bounded remainders for a nonzero modulus.

Use the direct prerequisites add_eq_zero_right, succ_ne_zero, beta_at_exists, division_remainder_exists, beta_division_prefix_extend as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (8), intermediate claims (6).

Referenced ingredients

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA0029 beta_at_exists PA001D division_remainder_exists PA00BX beta_division_prefix_extend

Proof neighborhood

Direct dependencies

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA0029 beta_at_exists PA001D division_remainder_exists PA00BX beta_division_prefix_extend

Direct dependents

PA00C0 prime_scaled_half_division_prefix_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004induction l
  5. 0005intro hp0
  6. 0006exists 0
  7. 0007exists 0
  8. 0008exists 0
  9. 0009exists 0
  10. 0010intro i
  11. 0011intro hi
  12. 0012exfalso
  13. 0013cases hi
  14. 0014have hsi : S i = 0
  15. 0015specialize add_eq_zero_right x
  16. 0016specialize add_eq_zero_right (S i)
  17. 0017apply add_eq_zero_right
  18. 0018exact hi_witness
  19. 0019specialize succ_ne_zero i
  20. 0020apply succ_ne_zero
  21. 0021exact hsi
  22. 0022intro hp0
  23. 0023have hprevious : exists qb qc rb rc. (forall fdp_index_exists_previous. (exists gsp_lt_gap_exists_previous_index_bound. gsp_lt_gap_exists_previous_index_bound + S fdp_index_exists_previous = l) -> exists fdp_value_exists_previous fdp_quotient_exists_previous fdp_remainder_exists_previous. (((exists ff_h_fdp_exists_previous_source. ff_h_fdp_exists_previous_source + S (fdp_value_exists_previous) = S ((S (fdp_index_exists_previous)) * c)) /\ exists ff_q_fdp_exists_previous_source. b = ff_q_fdp_exists_previous_source * S ((S (fdp_index_exists_previous)) * c) + (fdp_value_exists_previous))) /\ ((((exists ff_h_fdp_exists_previous_quotient_entry. ff_h_fdp_exists_previous_quotient_entry + S (fdp_quotient_exists_previous) = S ((S (fdp_index_exists_previous)) * qc)) /\ exists ff_q_fdp_exists_previous_quotient_entry. qb = ff_q_fdp_exists_previous_quotient_entry * S ((S (fdp_index_exists_previous)) * qc) + (fdp_quotient_exists_previous))) /\ ((((exists ff_h_fdp_exists_previous_remainder_entry. ff_h_fdp_exists_previous_remainder_entry + S (fdp_remainder_exists_previous) = S ((S (fdp_index_exists_previous)) * rc)) /\ exists ff_q_fdp_exists_previous_remainder_entry. rb = ff_q_fdp_exists_previous_remainder_entry * S ((S (fdp_index_exists_previous)) * rc) + (fdp_remainder_exists_previous))) /\ (fdp_value_exists_previous = p * fdp_quotient_exists_previous + fdp_remainder_exists_previous /\ (exists gsp_lt_gap_exists_previous_remainder_bound. gsp_lt_gap_exists_previous_remainder_bound + S fdp_remainder_exists_previous = p)))))
  24. 0024apply IH
  25. 0025exact hp0
  26. 0026cases hprevious
  27. 0027cases hprevious_witness
  28. 0028cases hprevious_witness_witness
  29. 0029cases hprevious_witness_witness_witness
  30. 0030have hdecoded : exists x. (((exists ff_h_fdp_exists_last_source. ff_h_fdp_exists_last_source + S (x) = S ((S (l)) * c)) /\ exists ff_q_fdp_exists_last_source. b = ff_q_fdp_exists_last_source * S ((S (l)) * c) + (x)))
  31. 0031specialize beta_at_exists b
  32. 0032specialize beta_at_exists c
  33. 0033specialize beta_at_exists l
  34. 0034exact beta_at_exists
  35. 0035cases hdecoded
  36. 0036have hdivision : exists q r. x4 = p * q + r /\ (exists gsp_lt_gap_fdp_exists_last_remainder_bound. gsp_lt_gap_fdp_exists_last_remainder_bound + S r = p)
  37. 0037specialize division_remainder_exists p
  38. 0038specialize division_remainder_exists x4
  39. 0039apply division_remainder_exists
  40. 0040exact hp0
  41. 0041cases hdivision
  42. 0042cases hdivision_witness
  43. 0043have hchoice : exists x q r. (((exists ff_h_fdp_choice_source. ff_h_fdp_choice_source + S (x) = S ((S (l)) * c)) /\ exists ff_q_fdp_choice_source. b = ff_q_fdp_choice_source * S ((S (l)) * c) + (x))) /\ (x = p * q + r /\ (exists gsp_lt_gap_fdp_choice_remainder_bound. gsp_lt_gap_fdp_choice_remainder_bound + S r = p))
  44. 0044exists x4
  45. 0045exists x5
  46. 0046exists x6
  47. 0047split
  48. 0048exact hdecoded_witness
  49. 0049exact hdivision_witness_witness
  50. 0050have hnext : exists qb qc rb rc. (forall fdp_index_exists_next. (exists gsp_lt_gap_exists_next_index_bound. gsp_lt_gap_exists_next_index_bound + S fdp_index_exists_next = S l) -> exists fdp_value_exists_next fdp_quotient_exists_next fdp_remainder_exists_next. (((exists ff_h_fdp_exists_next_source. ff_h_fdp_exists_next_source + S (fdp_value_exists_next) = S ((S (fdp_index_exists_next)) * c)) /\ exists ff_q_fdp_exists_next_source. b = ff_q_fdp_exists_next_source * S ((S (fdp_index_exists_next)) * c) + (fdp_value_exists_next))) /\ ((((exists ff_h_fdp_exists_next_quotient_entry. ff_h_fdp_exists_next_quotient_entry + S (fdp_quotient_exists_next) = S ((S (fdp_index_exists_next)) * qc)) /\ exists ff_q_fdp_exists_next_quotient_entry. qb = ff_q_fdp_exists_next_quotient_entry * S ((S (fdp_index_exists_next)) * qc) + (fdp_quotient_exists_next))) /\ ((((exists ff_h_fdp_exists_next_remainder_entry. ff_h_fdp_exists_next_remainder_entry + S (fdp_remainder_exists_next) = S ((S (fdp_index_exists_next)) * rc)) /\ exists ff_q_fdp_exists_next_remainder_entry. rb = ff_q_fdp_exists_next_remainder_entry * S ((S (fdp_index_exists_next)) * rc) + (fdp_remainder_exists_next))) /\ (fdp_value_exists_next = p * fdp_quotient_exists_next + fdp_remainder_exists_next /\ (exists gsp_lt_gap_exists_next_remainder_bound. gsp_lt_gap_exists_next_remainder_bound + S fdp_remainder_exists_next = p)))))
  51. 0051specialize beta_division_prefix_extend p
  52. 0052specialize beta_division_prefix_extend b
  53. 0053specialize beta_division_prefix_extend c
  54. 0054specialize beta_division_prefix_extend x
  55. 0055specialize beta_division_prefix_extend x1
  56. 0056specialize beta_division_prefix_extend x2
  57. 0057specialize beta_division_prefix_extend x3
  58. 0058specialize beta_division_prefix_extend l
  59. 0059apply beta_division_prefix_extend
  60. 0060exact hprevious_witness_witness_witness_witness
  61. 0061exact hchoice
  62. 0062exact hnext