BT00X9

beta_product_pointwise_le

Alpha body-checked · checked-use disabled

Pointwise bounded decoded prefixes have ordered finite products.

Exact expanded PA statement

forall b c d e l n q. (forall i a z. (exists bppl_bound. bppl_bound + S i = l) -> (((exists ff_h_bppl_left. ff_h_bppl_left + S (a) = S ((S (i)) * c)) /\ exists ff_q_bppl_left. b = ff_q_bppl_left * S ((S (i)) * c) + (a))) -> (((exists ff_h_bppl_right. ff_h_bppl_right + S (z) = S ((S (i)) * e)) /\ exists ff_q_bppl_right. d = ff_q_bppl_right * S ((S (i)) * e) + (z))) -> exists bppl_factor_gap. bppl_factor_gap + a = z) -> (exists ff_u_bppl_left_product ff_v_bppl_left_product. ((((exists ff_h_bppl_left_product_start. ff_h_bppl_left_product_start + S (1) = S ((S (0)) * ff_v_bppl_left_product)) /\ exists ff_q_bppl_left_product_start. ff_u_bppl_left_product = ff_q_bppl_left_product_start * S ((S (0)) * ff_v_bppl_left_product) + (1))) /\ ((((exists ff_h_bppl_left_product_terminal. ff_h_bppl_left_product_terminal + S (n) = S ((S (l)) * ff_v_bppl_left_product)) /\ exists ff_q_bppl_left_product_terminal. ff_u_bppl_left_product = ff_q_bppl_left_product_terminal * S ((S (l)) * ff_v_bppl_left_product) + (n))) /\ forall ff_i_bppl_left_product. (exists ff_lt_bppl_left_product_bound. ff_lt_bppl_left_product_bound + S ff_i_bppl_left_product = l) -> exists ff_p_bppl_left_product ff_r_bppl_left_product ff_s_bppl_left_product. ((((exists ff_h_bppl_left_product_factor. ff_h_bppl_left_product_factor + S (ff_p_bppl_left_product) = S ((S (ff_i_bppl_left_product)) * c)) /\ exists ff_q_bppl_left_product_factor. b = ff_q_bppl_left_product_factor * S ((S (ff_i_bppl_left_product)) * c) + (ff_p_bppl_left_product))) /\ ((((exists ff_h_bppl_left_product_partial. ff_h_bppl_left_product_partial + S (ff_r_bppl_left_product) = S ((S (ff_i_bppl_left_product)) * ff_v_bppl_left_product)) /\ exists ff_q_bppl_left_product_partial. ff_u_bppl_left_product = ff_q_bppl_left_product_partial * S ((S (ff_i_bppl_left_product)) * ff_v_bppl_left_product) + (ff_r_bppl_left_product))) /\ ((((exists ff_h_bppl_left_product_successor. ff_h_bppl_left_product_successor + S (ff_s_bppl_left_product) = S ((S (S ff_i_bppl_left_product)) * ff_v_bppl_left_product)) /\ exists ff_q_bppl_left_product_successor. ff_u_bppl_left_product = ff_q_bppl_left_product_successor * S ((S (S ff_i_bppl_left_product)) * ff_v_bppl_left_product) + (ff_s_bppl_left_product))) /\ ff_s_bppl_left_product = ff_r_bppl_left_product * ff_p_bppl_left_product)))))) -> (exists ff_u_bppl_right_product ff_v_bppl_right_product. ((((exists ff_h_bppl_right_product_start. ff_h_bppl_right_product_start + S (1) = S ((S (0)) * ff_v_bppl_right_product)) /\ exists ff_q_bppl_right_product_start. ff_u_bppl_right_product = ff_q_bppl_right_product_start * S ((S (0)) * ff_v_bppl_right_product) + (1))) /\ ((((exists ff_h_bppl_right_product_terminal. ff_h_bppl_right_product_terminal + S (q) = S ((S (l)) * ff_v_bppl_right_product)) /\ exists ff_q_bppl_right_product_terminal. ff_u_bppl_right_product = ff_q_bppl_right_product_terminal * S ((S (l)) * ff_v_bppl_right_product) + (q))) /\ forall ff_i_bppl_right_product. (exists ff_lt_bppl_right_product_bound. ff_lt_bppl_right_product_bound + S ff_i_bppl_right_product = l) -> exists ff_p_bppl_right_product ff_r_bppl_right_product ff_s_bppl_right_product. ((((exists ff_h_bppl_right_product_factor. ff_h_bppl_right_product_factor + S (ff_p_bppl_right_product) = S ((S (ff_i_bppl_right_product)) * e)) /\ exists ff_q_bppl_right_product_factor. d = ff_q_bppl_right_product_factor * S ((S (ff_i_bppl_right_product)) * e) + (ff_p_bppl_right_product))) /\ ((((exists ff_h_bppl_right_product_partial. ff_h_bppl_right_product_partial + S (ff_r_bppl_right_product) = S ((S (ff_i_bppl_right_product)) * ff_v_bppl_right_product)) /\ exists ff_q_bppl_right_product_partial. ff_u_bppl_right_product = ff_q_bppl_right_product_partial * S ((S (ff_i_bppl_right_product)) * ff_v_bppl_right_product) + (ff_r_bppl_right_product))) /\ ((((exists ff_h_bppl_right_product_successor. ff_h_bppl_right_product_successor + S (ff_s_bppl_right_product) = S ((S (S ff_i_bppl_right_product)) * ff_v_bppl_right_product)) /\ exists ff_q_bppl_right_product_successor. ff_u_bppl_right_product = ff_q_bppl_right_product_successor * S ((S (S ff_i_bppl_right_product)) * ff_v_bppl_right_product) + (ff_s_bppl_right_product))) /\ ff_s_bppl_right_product = ff_r_bppl_right_product * ff_p_bppl_right_product)))))) -> exists bppl_result_gap. bppl_result_gap + n = q

Structural proof guide

Pointwise bounded decoded prefixes have ordered finite products.

Direct prerequisites: beta_product_zero, beta_product_succ_decompose, le_succ, le_refl, mul_le_mul. The authored body proceeds by structural induction (1), case analysis (8), intermediate claims (8), equality transport (4).

Proof neighborhood

Direct dependencies

BT005I beta_product_zero BT005J beta_product_succ_decompose BT0018 le_succ BT000E le_refl BT00PV mul_le_mul

Direct dependents

BT00XA beta_product_uniform_le_pow BT0110 no_bertrand_middle_contribution_interval_le_primorial_interval

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 c
  3. 0003intro d
  4. 0004intro e
  5. 0005induction l
  6. 0006intro n
  7. 0007intro q
  8. 0008intro hpw
  9. 0009intro hn
  10. 0010intro hq
  11. 0011have hn1 : n = 1
  12. 0012specialize beta_product_zero b
  13. 0013specialize beta_product_zero c
  14. 0014specialize beta_product_zero n
  15. 0015apply beta_product_zero
  16. 0016exact hn
  17. 0017have hq1 : q = 1
  18. 0018specialize beta_product_zero d
  19. 0019specialize beta_product_zero e
  20. 0020specialize beta_product_zero q
  21. 0021apply beta_product_zero
  22. 0022exact hq
  23. 0023rewrite hn1
  24. 0024rewrite hq1
  25. 0025specialize le_refl 1
  26. 0026exact le_refl
  27. 0027intro n
  28. 0028intro q
  29. 0029intro hpw
  30. 0030intro hn
  31. 0031intro hq
  32. 0032have hnd : exists a r. (((exists ff_h_bppl_left_decomposition_entry. ff_h_bppl_left_decomposition_entry + S (a) = S ((S (l)) * c)) /\ exists ff_q_bppl_left_decomposition_entry. b = ff_q_bppl_left_decomposition_entry * S ((S (l)) * c) + (a))) /\ ((exists ff_u_bppl_left_decomposition_product ff_v_bppl_left_decomposition_product. ((((exists ff_h_bppl_left_decomposition_product_start. ff_h_bppl_left_decomposition_product_start + S (1) = S ((S (0)) * ff_v_bppl_left_decomposition_product)) /\ exists ff_q_bppl_left_decomposition_product_start. ff_u_bppl_left_decomposition_product = ff_q_bppl_left_decomposition_product_start * S ((S (0)) * ff_v_bppl_left_decomposition_product) + (1))) /\ ((((exists ff_h_bppl_left_decomposition_product_terminal. ff_h_bppl_left_decomposition_product_terminal + S (r) = S ((S (l)) * ff_v_bppl_left_decomposition_product)) /\ exists ff_q_bppl_left_decomposition_product_terminal. ff_u_bppl_left_decomposition_product = ff_q_bppl_left_decomposition_product_terminal * S ((S (l)) * ff_v_bppl_left_decomposition_product) + (r))) /\ forall ff_i_bppl_left_decomposition_product. (exists ff_lt_bppl_left_decomposition_product_bound. ff_lt_bppl_left_decomposition_product_bound + S ff_i_bppl_left_decomposition_product = l) -> exists ff_p_bppl_left_decomposition_product ff_r_bppl_left_decomposition_product ff_s_bppl_left_decomposition_product. ((((exists ff_h_bppl_left_decomposition_product_factor. ff_h_bppl_left_decomposition_product_factor + S (ff_p_bppl_left_decomposition_product) = S ((S (ff_i_bppl_left_decomposition_product)) * c)) /\ exists ff_q_bppl_left_decomposition_product_factor. b = ff_q_bppl_left_decomposition_product_factor * S ((S (ff_i_bppl_left_decomposition_product)) * c) + (ff_p_bppl_left_decomposition_product))) /\ ((((exists ff_h_bppl_left_decomposition_product_partial. ff_h_bppl_left_decomposition_product_partial + S (ff_r_bppl_left_decomposition_product) = S ((S (ff_i_bppl_left_decomposition_product)) * ff_v_bppl_left_decomposition_product)) /\ exists ff_q_bppl_left_decomposition_product_partial. ff_u_bppl_left_decomposition_product = ff_q_bppl_left_decomposition_product_partial * S ((S (ff_i_bppl_left_decomposition_product)) * ff_v_bppl_left_decomposition_product) + (ff_r_bppl_left_decomposition_product))) /\ ((((exists ff_h_bppl_left_decomposition_product_successor. ff_h_bppl_left_decomposition_product_successor + S (ff_s_bppl_left_decomposition_product) = S ((S (S ff_i_bppl_left_decomposition_product)) * ff_v_bppl_left_decomposition_product)) /\ exists ff_q_bppl_left_decomposition_product_successor. ff_u_bppl_left_decomposition_product = ff_q_bppl_left_decomposition_product_successor * S ((S (S ff_i_bppl_left_decomposition_product)) * ff_v_bppl_left_decomposition_product) + (ff_s_bppl_left_decomposition_product))) /\ ff_s_bppl_left_decomposition_product = ff_r_bppl_left_decomposition_product * ff_p_bppl_left_decomposition_product)))))) /\ n = r * a)
  33. 0033specialize beta_product_succ_decompose b
  34. 0034specialize beta_product_succ_decompose c
  35. 0035specialize beta_product_succ_decompose l
  36. 0036specialize beta_product_succ_decompose n
  37. 0037apply beta_product_succ_decompose
  38. 0038exact hn
  39. 0039cases hnd
  40. 0040cases hnd_witness
  41. 0041cases hnd_witness_witness
  42. 0042cases hnd_witness_witness_right
  43. 0043have hqd : exists a r. (((exists ff_h_bppl_right_decomposition_entry. ff_h_bppl_right_decomposition_entry + S (a) = S ((S (l)) * e)) /\ exists ff_q_bppl_right_decomposition_entry. d = ff_q_bppl_right_decomposition_entry * S ((S (l)) * e) + (a))) /\ ((exists ff_u_bppl_right_decomposition_product ff_v_bppl_right_decomposition_product. ((((exists ff_h_bppl_right_decomposition_product_start. ff_h_bppl_right_decomposition_product_start + S (1) = S ((S (0)) * ff_v_bppl_right_decomposition_product)) /\ exists ff_q_bppl_right_decomposition_product_start. ff_u_bppl_right_decomposition_product = ff_q_bppl_right_decomposition_product_start * S ((S (0)) * ff_v_bppl_right_decomposition_product) + (1))) /\ ((((exists ff_h_bppl_right_decomposition_product_terminal. ff_h_bppl_right_decomposition_product_terminal + S (r) = S ((S (l)) * ff_v_bppl_right_decomposition_product)) /\ exists ff_q_bppl_right_decomposition_product_terminal. ff_u_bppl_right_decomposition_product = ff_q_bppl_right_decomposition_product_terminal * S ((S (l)) * ff_v_bppl_right_decomposition_product) + (r))) /\ forall ff_i_bppl_right_decomposition_product. (exists ff_lt_bppl_right_decomposition_product_bound. ff_lt_bppl_right_decomposition_product_bound + S ff_i_bppl_right_decomposition_product = l) -> exists ff_p_bppl_right_decomposition_product ff_r_bppl_right_decomposition_product ff_s_bppl_right_decomposition_product. ((((exists ff_h_bppl_right_decomposition_product_factor. ff_h_bppl_right_decomposition_product_factor + S (ff_p_bppl_right_decomposition_product) = S ((S (ff_i_bppl_right_decomposition_product)) * e)) /\ exists ff_q_bppl_right_decomposition_product_factor. d = ff_q_bppl_right_decomposition_product_factor * S ((S (ff_i_bppl_right_decomposition_product)) * e) + (ff_p_bppl_right_decomposition_product))) /\ ((((exists ff_h_bppl_right_decomposition_product_partial. ff_h_bppl_right_decomposition_product_partial + S (ff_r_bppl_right_decomposition_product) = S ((S (ff_i_bppl_right_decomposition_product)) * ff_v_bppl_right_decomposition_product)) /\ exists ff_q_bppl_right_decomposition_product_partial. ff_u_bppl_right_decomposition_product = ff_q_bppl_right_decomposition_product_partial * S ((S (ff_i_bppl_right_decomposition_product)) * ff_v_bppl_right_decomposition_product) + (ff_r_bppl_right_decomposition_product))) /\ ((((exists ff_h_bppl_right_decomposition_product_successor. ff_h_bppl_right_decomposition_product_successor + S (ff_s_bppl_right_decomposition_product) = S ((S (S ff_i_bppl_right_decomposition_product)) * ff_v_bppl_right_decomposition_product)) /\ exists ff_q_bppl_right_decomposition_product_successor. ff_u_bppl_right_decomposition_product = ff_q_bppl_right_decomposition_product_successor * S ((S (S ff_i_bppl_right_decomposition_product)) * ff_v_bppl_right_decomposition_product) + (ff_s_bppl_right_decomposition_product))) /\ ff_s_bppl_right_decomposition_product = ff_r_bppl_right_decomposition_product * ff_p_bppl_right_decomposition_product)))))) /\ q = r * a)
  44. 0044specialize beta_product_succ_decompose d
  45. 0045specialize beta_product_succ_decompose e
  46. 0046specialize beta_product_succ_decompose l
  47. 0047specialize beta_product_succ_decompose q
  48. 0048apply beta_product_succ_decompose
  49. 0049exact hq
  50. 0050cases hqd
  51. 0051cases hqd_witness
  52. 0052cases hqd_witness_witness
  53. 0053cases hqd_witness_witness_right
  54. 0054have hpw_prefix : forall i a z. (exists bppl_prefix_bound. bppl_prefix_bound + S i = l) -> (((exists ff_h_bppl_prefix_left. ff_h_bppl_prefix_left + S (a) = S ((S (i)) * c)) /\ exists ff_q_bppl_prefix_left. b = ff_q_bppl_prefix_left * S ((S (i)) * c) + (a))) -> (((exists ff_h_bppl_prefix_right. ff_h_bppl_prefix_right + S (z) = S ((S (i)) * e)) /\ exists ff_q_bppl_prefix_right. d = ff_q_bppl_prefix_right * S ((S (i)) * e) + (z))) -> exists bppl_prefix_factor_gap. bppl_prefix_factor_gap + a = z
  55. 0055intro i
  56. 0056intro a
  57. 0057intro z
  58. 0058intro hi
  59. 0059intro ha
  60. 0060intro hz
  61. 0061specialize hpw i
  62. 0062specialize hpw a
  63. 0063specialize hpw z
  64. 0064apply hpw
  65. 0065specialize le_succ (S i)
  66. 0066specialize le_succ l
  67. 0067apply le_succ
  68. 0068exact hi
  69. 0069exact ha
  70. 0070exact hz
  71. 0071have hprefix : exists k. k + x1 = x3
  72. 0072specialize IH x1
  73. 0073specialize IH x3
  74. 0074apply IH
  75. 0075exact hpw_prefix
  76. 0076exact hnd_witness_witness_right_left
  77. 0077exact hqd_witness_witness_right_left
  78. 0078have hentry : exists k. k + x = x2
  79. 0079specialize hpw l
  80. 0080specialize hpw x
  81. 0081specialize hpw x2
  82. 0082apply hpw
  83. 0083specialize le_refl (S l)
  84. 0084exact le_refl
  85. 0085exact hnd_witness_witness_left
  86. 0086exact hqd_witness_witness_left
  87. 0087have hfold : exists k. k + (x1 * x) = (x3 * x2)
  88. 0088specialize mul_le_mul x1
  89. 0089specialize mul_le_mul x3
  90. 0090specialize mul_le_mul x
  91. 0091specialize mul_le_mul x2
  92. 0092apply mul_le_mul
  93. 0093exact hprefix
  94. 0094exact hentry
  95. 0095rewrite hnd_witness_witness_right_right
  96. 0096rewrite hqd_witness_witness_right_right
  97. 0097exact hfold