BT00UE

primorial_positive

Alpha body-checked · checked-use disabled

Every relational primorial value is a successor.

Exact expanded PA statement

forall m z. (exists bpr_code_bp_positive_source bpr_scale_bp_positive_source. ((forall bpr_index_bp_positive_source_mask. (exists bpr_gap_bp_positive_source_mask_bound. bpr_gap_bp_positive_source_mask_bound + S (bpr_index_bp_positive_source_mask) = m) -> exists bpr_value_bp_positive_source_mask. ((((exists bpr_height_bp_positive_source_mask_decoded. bpr_height_bp_positive_source_mask_decoded + S (bpr_value_bp_positive_source_mask) = S ((S (bpr_index_bp_positive_source_mask)) * bpr_scale_bp_positive_source)) /\ exists bpr_quotient_bp_positive_source_mask_decoded. bpr_code_bp_positive_source = bpr_quotient_bp_positive_source_mask_decoded * S ((S (bpr_index_bp_positive_source_mask)) * bpr_scale_bp_positive_source) + (bpr_value_bp_positive_source_mask))) /\ (((((~(S (bpr_index_bp_positive_source_mask) = 1) /\ forall bpr_left_bp_positive_source_mask_choice_prime bpr_right_bp_positive_source_mask_choice_prime. S (bpr_index_bp_positive_source_mask) = bpr_left_bp_positive_source_mask_choice_prime * bpr_right_bp_positive_source_mask_choice_prime -> bpr_left_bp_positive_source_mask_choice_prime = 1 \/ bpr_right_bp_positive_source_mask_choice_prime = 1)) /\ bpr_value_bp_positive_source_mask = S (bpr_index_bp_positive_source_mask)) \/ (~((~(S (bpr_index_bp_positive_source_mask) = 1) /\ forall bpr_left_bp_positive_source_mask_choice_prime bpr_right_bp_positive_source_mask_choice_prime. S (bpr_index_bp_positive_source_mask) = bpr_left_bp_positive_source_mask_choice_prime * bpr_right_bp_positive_source_mask_choice_prime -> bpr_left_bp_positive_source_mask_choice_prime = 1 \/ bpr_right_bp_positive_source_mask_choice_prime = 1)) /\ bpr_value_bp_positive_source_mask = 1))))) /\ (exists ff_u_bp_positive_source_product ff_v_bp_positive_source_product. ((((exists ff_h_bp_positive_source_product_start. ff_h_bp_positive_source_product_start + S (1) = S ((S (0)) * ff_v_bp_positive_source_product)) /\ exists ff_q_bp_positive_source_product_start. ff_u_bp_positive_source_product = ff_q_bp_positive_source_product_start * S ((S (0)) * ff_v_bp_positive_source_product) + (1))) /\ ((((exists ff_h_bp_positive_source_product_terminal. ff_h_bp_positive_source_product_terminal + S (z) = S ((S (m)) * ff_v_bp_positive_source_product)) /\ exists ff_q_bp_positive_source_product_terminal. ff_u_bp_positive_source_product = ff_q_bp_positive_source_product_terminal * S ((S (m)) * ff_v_bp_positive_source_product) + (z))) /\ forall ff_i_bp_positive_source_product. (exists ff_lt_bp_positive_source_product_bound. ff_lt_bp_positive_source_product_bound + S ff_i_bp_positive_source_product = m) -> exists ff_p_bp_positive_source_product ff_r_bp_positive_source_product ff_s_bp_positive_source_product. ((((exists ff_h_bp_positive_source_product_factor. ff_h_bp_positive_source_product_factor + S (ff_p_bp_positive_source_product) = S ((S (ff_i_bp_positive_source_product)) * bpr_scale_bp_positive_source)) /\ exists ff_q_bp_positive_source_product_factor. bpr_code_bp_positive_source = ff_q_bp_positive_source_product_factor * S ((S (ff_i_bp_positive_source_product)) * bpr_scale_bp_positive_source) + (ff_p_bp_positive_source_product))) /\ ((((exists ff_h_bp_positive_source_product_partial. ff_h_bp_positive_source_product_partial + S (ff_r_bp_positive_source_product) = S ((S (ff_i_bp_positive_source_product)) * ff_v_bp_positive_source_product)) /\ exists ff_q_bp_positive_source_product_partial. ff_u_bp_positive_source_product = ff_q_bp_positive_source_product_partial * S ((S (ff_i_bp_positive_source_product)) * ff_v_bp_positive_source_product) + (ff_r_bp_positive_source_product))) /\ ((((exists ff_h_bp_positive_source_product_successor. ff_h_bp_positive_source_product_successor + S (ff_s_bp_positive_source_product) = S ((S (S ff_i_bp_positive_source_product)) * ff_v_bp_positive_source_product)) /\ exists ff_q_bp_positive_source_product_successor. ff_u_bp_positive_source_product = ff_q_bp_positive_source_product_successor * S ((S (S ff_i_bp_positive_source_product)) * ff_v_bp_positive_source_product) + (ff_s_bp_positive_source_product))) /\ ff_s_bp_positive_source_product = ff_r_bp_positive_source_product * ff_p_bp_positive_source_product)))))))) -> exists r. z = S r

Structural proof guide

Every relational primorial value is a successor.

Direct prerequisites: mul_succ_left, primorial_zero, primorial_succ_decompose. The authored body proceeds by structural induction (1), case analysis (8), intermediate claims (3), equality transport (4).

Proof neighborhood

Direct dependencies

BT0005 mul_succ_left BT00UC primorial_zero BT00UD primorial_succ_decompose

Direct dependents

BT0111 no_bertrand_middle_contribution_interval_le_four_pow

Formal native tactic body

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

  1. 0001induction m
  2. 0002intro z
  3. 0003intro hprimorial
  4. 0004have hz : z = 1
  5. 0005apply primorial_zero
  6. 0006exact hprimorial
  7. 0007exists 0
  8. 0008trans 1
  9. 0009exact hz
  10. 0010refl
  11. 0011intro z
  12. 0012intro hprimorial
  13. 0013have hdecomposition : exists p r. (((((~(S (m) = 1) /\ forall bpr_left_bp_succ_factor_prime bpr_right_bp_succ_factor_prime. S (m) = bpr_left_bp_succ_factor_prime * bpr_right_bp_succ_factor_prime -> bpr_left_bp_succ_factor_prime = 1 \/ bpr_right_bp_succ_factor_prime = 1)) /\ p = S (m)) \/ (~((~(S (m) = 1) /\ forall bpr_left_bp_succ_factor_prime bpr_right_bp_succ_factor_prime. S (m) = bpr_left_bp_succ_factor_prime * bpr_right_bp_succ_factor_prime -> bpr_left_bp_succ_factor_prime = 1 \/ bpr_right_bp_succ_factor_prime = 1)) /\ p = 1))) /\ ((exists bpr_code_bp_succ_predecessor bpr_scale_bp_succ_predecessor. ((forall bpr_index_bp_succ_predecessor_mask. (exists bpr_gap_bp_succ_predecessor_mask_bound. bpr_gap_bp_succ_predecessor_mask_bound + S (bpr_index_bp_succ_predecessor_mask) = m) -> exists bpr_value_bp_succ_predecessor_mask. ((((exists bpr_height_bp_succ_predecessor_mask_decoded. bpr_height_bp_succ_predecessor_mask_decoded + S (bpr_value_bp_succ_predecessor_mask) = S ((S (bpr_index_bp_succ_predecessor_mask)) * bpr_scale_bp_succ_predecessor)) /\ exists bpr_quotient_bp_succ_predecessor_mask_decoded. bpr_code_bp_succ_predecessor = bpr_quotient_bp_succ_predecessor_mask_decoded * S ((S (bpr_index_bp_succ_predecessor_mask)) * bpr_scale_bp_succ_predecessor) + (bpr_value_bp_succ_predecessor_mask))) /\ (((((~(S (bpr_index_bp_succ_predecessor_mask) = 1) /\ forall bpr_left_bp_succ_predecessor_mask_choice_prime bpr_right_bp_succ_predecessor_mask_choice_prime. S (bpr_index_bp_succ_predecessor_mask) = bpr_left_bp_succ_predecessor_mask_choice_prime * bpr_right_bp_succ_predecessor_mask_choice_prime -> bpr_left_bp_succ_predecessor_mask_choice_prime = 1 \/ bpr_right_bp_succ_predecessor_mask_choice_prime = 1)) /\ bpr_value_bp_succ_predecessor_mask = S (bpr_index_bp_succ_predecessor_mask)) \/ (~((~(S (bpr_index_bp_succ_predecessor_mask) = 1) /\ forall bpr_left_bp_succ_predecessor_mask_choice_prime bpr_right_bp_succ_predecessor_mask_choice_prime. S (bpr_index_bp_succ_predecessor_mask) = bpr_left_bp_succ_predecessor_mask_choice_prime * bpr_right_bp_succ_predecessor_mask_choice_prime -> bpr_left_bp_succ_predecessor_mask_choice_prime = 1 \/ bpr_right_bp_succ_predecessor_mask_choice_prime = 1)) /\ bpr_value_bp_succ_predecessor_mask = 1))))) /\ (exists ff_u_bp_succ_predecessor_product ff_v_bp_succ_predecessor_product. ((((exists ff_h_bp_succ_predecessor_product_start. ff_h_bp_succ_predecessor_product_start + S (1) = S ((S (0)) * ff_v_bp_succ_predecessor_product)) /\ exists ff_q_bp_succ_predecessor_product_start. ff_u_bp_succ_predecessor_product = ff_q_bp_succ_predecessor_product_start * S ((S (0)) * ff_v_bp_succ_predecessor_product) + (1))) /\ ((((exists ff_h_bp_succ_predecessor_product_terminal. ff_h_bp_succ_predecessor_product_terminal + S (r) = S ((S (m)) * ff_v_bp_succ_predecessor_product)) /\ exists ff_q_bp_succ_predecessor_product_terminal. ff_u_bp_succ_predecessor_product = ff_q_bp_succ_predecessor_product_terminal * S ((S (m)) * ff_v_bp_succ_predecessor_product) + (r))) /\ forall ff_i_bp_succ_predecessor_product. (exists ff_lt_bp_succ_predecessor_product_bound. ff_lt_bp_succ_predecessor_product_bound + S ff_i_bp_succ_predecessor_product = m) -> exists ff_p_bp_succ_predecessor_product ff_r_bp_succ_predecessor_product ff_s_bp_succ_predecessor_product. ((((exists ff_h_bp_succ_predecessor_product_factor. ff_h_bp_succ_predecessor_product_factor + S (ff_p_bp_succ_predecessor_product) = S ((S (ff_i_bp_succ_predecessor_product)) * bpr_scale_bp_succ_predecessor)) /\ exists ff_q_bp_succ_predecessor_product_factor. bpr_code_bp_succ_predecessor = ff_q_bp_succ_predecessor_product_factor * S ((S (ff_i_bp_succ_predecessor_product)) * bpr_scale_bp_succ_predecessor) + (ff_p_bp_succ_predecessor_product))) /\ ((((exists ff_h_bp_succ_predecessor_product_partial. ff_h_bp_succ_predecessor_product_partial + S (ff_r_bp_succ_predecessor_product) = S ((S (ff_i_bp_succ_predecessor_product)) * ff_v_bp_succ_predecessor_product)) /\ exists ff_q_bp_succ_predecessor_product_partial. ff_u_bp_succ_predecessor_product = ff_q_bp_succ_predecessor_product_partial * S ((S (ff_i_bp_succ_predecessor_product)) * ff_v_bp_succ_predecessor_product) + (ff_r_bp_succ_predecessor_product))) /\ ((((exists ff_h_bp_succ_predecessor_product_successor. ff_h_bp_succ_predecessor_product_successor + S (ff_s_bp_succ_predecessor_product) = S ((S (S ff_i_bp_succ_predecessor_product)) * ff_v_bp_succ_predecessor_product)) /\ exists ff_q_bp_succ_predecessor_product_successor. ff_u_bp_succ_predecessor_product = ff_q_bp_succ_predecessor_product_successor * S ((S (S ff_i_bp_succ_predecessor_product)) * ff_v_bp_succ_predecessor_product) + (ff_s_bp_succ_predecessor_product))) /\ ff_s_bp_succ_predecessor_product = ff_r_bp_succ_predecessor_product * ff_p_bp_succ_predecessor_product)))))))) /\ z = r * p)
  14. 0014apply primorial_succ_decompose
  15. 0015exact hprimorial
  16. 0016cases hdecomposition
  17. 0017cases hdecomposition_witness
  18. 0018cases hdecomposition_witness_witness
  19. 0019cases hdecomposition_witness_witness_right
  20. 0020have hprevious : exists t. x1 = S t
  21. 0021apply IH
  22. 0022exact hdecomposition_witness_witness_right_left
  23. 0023cases hprevious
  24. 0024cases hdecomposition_witness_witness_left
  25. 0025cases hdecomposition_witness_witness_left_left
  26. 0026exists x2 * S m + m
  27. 0027trans x1 * x
  28. 0028exact hdecomposition_witness_witness_right_right
  29. 0029rewrite hprevious_witness
  30. 0030rewrite hdecomposition_witness_witness_left_left_right
  31. 0031trans x2 * S m + S m
  32. 0032apply mul_succ_left
  33. 0033apply PA4
  34. 0034cases hdecomposition_witness_witness_left_right
  35. 0035exists x2 * 1 + 0
  36. 0036trans x1 * x
  37. 0037exact hdecomposition_witness_witness_right_right
  38. 0038rewrite hprevious_witness
  39. 0039rewrite hdecomposition_witness_witness_left_right_right
  40. 0040trans x2 * 1 + 1
  41. 0041apply mul_succ_left
  42. 0042apply PA4