BT00UA

primorial_exists

Alpha body-checked · checked-use disabled

Every natural index has a relational primorial value.

Exact expanded PA statement

forall m. exists z. (exists bpr_code_bp_exists bpr_scale_bp_exists. ((forall bpr_index_bp_exists_mask. (exists bpr_gap_bp_exists_mask_bound. bpr_gap_bp_exists_mask_bound + S (bpr_index_bp_exists_mask) = m) -> exists bpr_value_bp_exists_mask. ((((exists bpr_height_bp_exists_mask_decoded. bpr_height_bp_exists_mask_decoded + S (bpr_value_bp_exists_mask) = S ((S (bpr_index_bp_exists_mask)) * bpr_scale_bp_exists)) /\ exists bpr_quotient_bp_exists_mask_decoded. bpr_code_bp_exists = bpr_quotient_bp_exists_mask_decoded * S ((S (bpr_index_bp_exists_mask)) * bpr_scale_bp_exists) + (bpr_value_bp_exists_mask))) /\ (((((~(S (bpr_index_bp_exists_mask) = 1) /\ forall bpr_left_bp_exists_mask_choice_prime bpr_right_bp_exists_mask_choice_prime. S (bpr_index_bp_exists_mask) = bpr_left_bp_exists_mask_choice_prime * bpr_right_bp_exists_mask_choice_prime -> bpr_left_bp_exists_mask_choice_prime = 1 \/ bpr_right_bp_exists_mask_choice_prime = 1)) /\ bpr_value_bp_exists_mask = S (bpr_index_bp_exists_mask)) \/ (~((~(S (bpr_index_bp_exists_mask) = 1) /\ forall bpr_left_bp_exists_mask_choice_prime bpr_right_bp_exists_mask_choice_prime. S (bpr_index_bp_exists_mask) = bpr_left_bp_exists_mask_choice_prime * bpr_right_bp_exists_mask_choice_prime -> bpr_left_bp_exists_mask_choice_prime = 1 \/ bpr_right_bp_exists_mask_choice_prime = 1)) /\ bpr_value_bp_exists_mask = 1))))) /\ (exists ff_u_bp_exists_product ff_v_bp_exists_product. ((((exists ff_h_bp_exists_product_start. ff_h_bp_exists_product_start + S (1) = S ((S (0)) * ff_v_bp_exists_product)) /\ exists ff_q_bp_exists_product_start. ff_u_bp_exists_product = ff_q_bp_exists_product_start * S ((S (0)) * ff_v_bp_exists_product) + (1))) /\ ((((exists ff_h_bp_exists_product_terminal. ff_h_bp_exists_product_terminal + S (z) = S ((S (m)) * ff_v_bp_exists_product)) /\ exists ff_q_bp_exists_product_terminal. ff_u_bp_exists_product = ff_q_bp_exists_product_terminal * S ((S (m)) * ff_v_bp_exists_product) + (z))) /\ forall ff_i_bp_exists_product. (exists ff_lt_bp_exists_product_bound. ff_lt_bp_exists_product_bound + S ff_i_bp_exists_product = m) -> exists ff_p_bp_exists_product ff_r_bp_exists_product ff_s_bp_exists_product. ((((exists ff_h_bp_exists_product_factor. ff_h_bp_exists_product_factor + S (ff_p_bp_exists_product) = S ((S (ff_i_bp_exists_product)) * bpr_scale_bp_exists)) /\ exists ff_q_bp_exists_product_factor. bpr_code_bp_exists = ff_q_bp_exists_product_factor * S ((S (ff_i_bp_exists_product)) * bpr_scale_bp_exists) + (ff_p_bp_exists_product))) /\ ((((exists ff_h_bp_exists_product_partial. ff_h_bp_exists_product_partial + S (ff_r_bp_exists_product) = S ((S (ff_i_bp_exists_product)) * ff_v_bp_exists_product)) /\ exists ff_q_bp_exists_product_partial. ff_u_bp_exists_product = ff_q_bp_exists_product_partial * S ((S (ff_i_bp_exists_product)) * ff_v_bp_exists_product) + (ff_r_bp_exists_product))) /\ ((((exists ff_h_bp_exists_product_successor. ff_h_bp_exists_product_successor + S (ff_s_bp_exists_product) = S ((S (S ff_i_bp_exists_product)) * ff_v_bp_exists_product)) /\ exists ff_q_bp_exists_product_successor. ff_u_bp_exists_product = ff_q_bp_exists_product_successor * S ((S (S ff_i_bp_exists_product)) * ff_v_bp_exists_product) + (ff_s_bp_exists_product))) /\ ff_s_bp_exists_product = ff_r_bp_exists_product * ff_p_bp_exists_product))))))))

Structural proof guide

Every natural index has a relational primorial value.

Direct prerequisites: beta_product_exists, primorial_factor_prefix_exists. The authored body proceeds by case analysis (3), intermediate claims (2).

Proof neighborhood

Direct dependencies

BT005F beta_product_exists BT00U8 primorial_factor_prefix_exists

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. 0001intro m
  2. 0002have hprefix : exists b c. (forall bpr_index_bpfpx_result. (exists bpr_gap_bpfpx_result_bound. bpr_gap_bpfpx_result_bound + S (bpr_index_bpfpx_result) = m) -> exists bpr_value_bpfpx_result. ((((exists bpr_height_bpfpx_result_decoded. bpr_height_bpfpx_result_decoded + S (bpr_value_bpfpx_result) = S ((S (bpr_index_bpfpx_result)) * c)) /\ exists bpr_quotient_bpfpx_result_decoded. b = bpr_quotient_bpfpx_result_decoded * S ((S (bpr_index_bpfpx_result)) * c) + (bpr_value_bpfpx_result))) /\ (((((~(S (bpr_index_bpfpx_result) = 1) /\ forall bpr_left_bpfpx_result_choice_prime bpr_right_bpfpx_result_choice_prime. S (bpr_index_bpfpx_result) = bpr_left_bpfpx_result_choice_prime * bpr_right_bpfpx_result_choice_prime -> bpr_left_bpfpx_result_choice_prime = 1 \/ bpr_right_bpfpx_result_choice_prime = 1)) /\ bpr_value_bpfpx_result = S (bpr_index_bpfpx_result)) \/ (~((~(S (bpr_index_bpfpx_result) = 1) /\ forall bpr_left_bpfpx_result_choice_prime bpr_right_bpfpx_result_choice_prime. S (bpr_index_bpfpx_result) = bpr_left_bpfpx_result_choice_prime * bpr_right_bpfpx_result_choice_prime -> bpr_left_bpfpx_result_choice_prime = 1 \/ bpr_right_bpfpx_result_choice_prime = 1)) /\ bpr_value_bpfpx_result = 1)))))
  3. 0003apply primorial_factor_prefix_exists
  4. 0004cases hprefix
  5. 0005cases hprefix_witness
  6. 0006have hproduct : exists z. (exists ff_u_bp_exists_product_witness ff_v_bp_exists_product_witness. ((((exists ff_h_bp_exists_product_witness_start. ff_h_bp_exists_product_witness_start + S (1) = S ((S (0)) * ff_v_bp_exists_product_witness)) /\ exists ff_q_bp_exists_product_witness_start. ff_u_bp_exists_product_witness = ff_q_bp_exists_product_witness_start * S ((S (0)) * ff_v_bp_exists_product_witness) + (1))) /\ ((((exists ff_h_bp_exists_product_witness_terminal. ff_h_bp_exists_product_witness_terminal + S (z) = S ((S (m)) * ff_v_bp_exists_product_witness)) /\ exists ff_q_bp_exists_product_witness_terminal. ff_u_bp_exists_product_witness = ff_q_bp_exists_product_witness_terminal * S ((S (m)) * ff_v_bp_exists_product_witness) + (z))) /\ forall ff_i_bp_exists_product_witness. (exists ff_lt_bp_exists_product_witness_bound. ff_lt_bp_exists_product_witness_bound + S ff_i_bp_exists_product_witness = m) -> exists ff_p_bp_exists_product_witness ff_r_bp_exists_product_witness ff_s_bp_exists_product_witness. ((((exists ff_h_bp_exists_product_witness_factor. ff_h_bp_exists_product_witness_factor + S (ff_p_bp_exists_product_witness) = S ((S (ff_i_bp_exists_product_witness)) * x1)) /\ exists ff_q_bp_exists_product_witness_factor. x = ff_q_bp_exists_product_witness_factor * S ((S (ff_i_bp_exists_product_witness)) * x1) + (ff_p_bp_exists_product_witness))) /\ ((((exists ff_h_bp_exists_product_witness_partial. ff_h_bp_exists_product_witness_partial + S (ff_r_bp_exists_product_witness) = S ((S (ff_i_bp_exists_product_witness)) * ff_v_bp_exists_product_witness)) /\ exists ff_q_bp_exists_product_witness_partial. ff_u_bp_exists_product_witness = ff_q_bp_exists_product_witness_partial * S ((S (ff_i_bp_exists_product_witness)) * ff_v_bp_exists_product_witness) + (ff_r_bp_exists_product_witness))) /\ ((((exists ff_h_bp_exists_product_witness_successor. ff_h_bp_exists_product_witness_successor + S (ff_s_bp_exists_product_witness) = S ((S (S ff_i_bp_exists_product_witness)) * ff_v_bp_exists_product_witness)) /\ exists ff_q_bp_exists_product_witness_successor. ff_u_bp_exists_product_witness = ff_q_bp_exists_product_witness_successor * S ((S (S ff_i_bp_exists_product_witness)) * ff_v_bp_exists_product_witness) + (ff_s_bp_exists_product_witness))) /\ ff_s_bp_exists_product_witness = ff_r_bp_exists_product_witness * ff_p_bp_exists_product_witness))))))
  7. 0007apply beta_product_exists
  8. 0008cases hproduct
  9. 0009exists x2
  10. 0010exists x
  11. 0011exists x1
  12. 0012split
  13. 0013exact hprefix_witness_witness
  14. 0014exact hproduct_witness