BT00VW

primorial_le_four_pow

Alpha body-checked · checked-use disabled

The inclusive Primorial is bounded by four to its index.

Exact expanded PA statement

forall n z q. (exists bpr_code_bplfp_primorial bpr_scale_bplfp_primorial. ((forall bpr_index_bplfp_primorial_mask. (exists bpr_gap_bplfp_primorial_mask_bound. bpr_gap_bplfp_primorial_mask_bound + S (bpr_index_bplfp_primorial_mask) = n) -> exists bpr_value_bplfp_primorial_mask. ((((exists bpr_height_bplfp_primorial_mask_decoded. bpr_height_bplfp_primorial_mask_decoded + S (bpr_value_bplfp_primorial_mask) = S ((S (bpr_index_bplfp_primorial_mask)) * bpr_scale_bplfp_primorial)) /\ exists bpr_quotient_bplfp_primorial_mask_decoded. bpr_code_bplfp_primorial = bpr_quotient_bplfp_primorial_mask_decoded * S ((S (bpr_index_bplfp_primorial_mask)) * bpr_scale_bplfp_primorial) + (bpr_value_bplfp_primorial_mask))) /\ (((((~(S (bpr_index_bplfp_primorial_mask) = 1) /\ forall bpr_left_bplfp_primorial_mask_choice_prime bpr_right_bplfp_primorial_mask_choice_prime. S (bpr_index_bplfp_primorial_mask) = bpr_left_bplfp_primorial_mask_choice_prime * bpr_right_bplfp_primorial_mask_choice_prime -> bpr_left_bplfp_primorial_mask_choice_prime = 1 \/ bpr_right_bplfp_primorial_mask_choice_prime = 1)) /\ bpr_value_bplfp_primorial_mask = S (bpr_index_bplfp_primorial_mask)) \/ (~((~(S (bpr_index_bplfp_primorial_mask) = 1) /\ forall bpr_left_bplfp_primorial_mask_choice_prime bpr_right_bplfp_primorial_mask_choice_prime. S (bpr_index_bplfp_primorial_mask) = bpr_left_bplfp_primorial_mask_choice_prime * bpr_right_bplfp_primorial_mask_choice_prime -> bpr_left_bplfp_primorial_mask_choice_prime = 1 \/ bpr_right_bplfp_primorial_mask_choice_prime = 1)) /\ bpr_value_bplfp_primorial_mask = 1))))) /\ (exists ff_u_bplfp_primorial_product ff_v_bplfp_primorial_product. ((((exists ff_h_bplfp_primorial_product_start. ff_h_bplfp_primorial_product_start + S (1) = S ((S (0)) * ff_v_bplfp_primorial_product)) /\ exists ff_q_bplfp_primorial_product_start. ff_u_bplfp_primorial_product = ff_q_bplfp_primorial_product_start * S ((S (0)) * ff_v_bplfp_primorial_product) + (1))) /\ ((((exists ff_h_bplfp_primorial_product_terminal. ff_h_bplfp_primorial_product_terminal + S (z) = S ((S (n)) * ff_v_bplfp_primorial_product)) /\ exists ff_q_bplfp_primorial_product_terminal. ff_u_bplfp_primorial_product = ff_q_bplfp_primorial_product_terminal * S ((S (n)) * ff_v_bplfp_primorial_product) + (z))) /\ forall ff_i_bplfp_primorial_product. (exists ff_lt_bplfp_primorial_product_bound. ff_lt_bplfp_primorial_product_bound + S ff_i_bplfp_primorial_product = n) -> exists ff_p_bplfp_primorial_product ff_r_bplfp_primorial_product ff_s_bplfp_primorial_product. ((((exists ff_h_bplfp_primorial_product_factor. ff_h_bplfp_primorial_product_factor + S (ff_p_bplfp_primorial_product) = S ((S (ff_i_bplfp_primorial_product)) * bpr_scale_bplfp_primorial)) /\ exists ff_q_bplfp_primorial_product_factor. bpr_code_bplfp_primorial = ff_q_bplfp_primorial_product_factor * S ((S (ff_i_bplfp_primorial_product)) * bpr_scale_bplfp_primorial) + (ff_p_bplfp_primorial_product))) /\ ((((exists ff_h_bplfp_primorial_product_partial. ff_h_bplfp_primorial_product_partial + S (ff_r_bplfp_primorial_product) = S ((S (ff_i_bplfp_primorial_product)) * ff_v_bplfp_primorial_product)) /\ exists ff_q_bplfp_primorial_product_partial. ff_u_bplfp_primorial_product = ff_q_bplfp_primorial_product_partial * S ((S (ff_i_bplfp_primorial_product)) * ff_v_bplfp_primorial_product) + (ff_r_bplfp_primorial_product))) /\ ((((exists ff_h_bplfp_primorial_product_successor. ff_h_bplfp_primorial_product_successor + S (ff_s_bplfp_primorial_product) = S ((S (S ff_i_bplfp_primorial_product)) * ff_v_bplfp_primorial_product)) /\ exists ff_q_bplfp_primorial_product_successor. ff_u_bplfp_primorial_product = ff_q_bplfp_primorial_product_successor * S ((S (S ff_i_bplfp_primorial_product)) * ff_v_bplfp_primorial_product) + (ff_s_bplfp_primorial_product))) /\ ff_s_bplfp_primorial_product = ff_r_bplfp_primorial_product * ff_p_bplfp_primorial_product)))))))) -> (exists pa_b_bplfp_power pa_c_bplfp_power. ((forall pa_i_bplfp_power_repeat. (exists pa_lt_bplfp_power_repeat_bound. pa_lt_bplfp_power_repeat_bound + S pa_i_bplfp_power_repeat = n) -> (((exists pa_h_bplfp_power_repeat_decoded. pa_h_bplfp_power_repeat_decoded + S (4) = S ((S (pa_i_bplfp_power_repeat)) * pa_c_bplfp_power)) /\ exists pa_q_bplfp_power_repeat_decoded. pa_b_bplfp_power = pa_q_bplfp_power_repeat_decoded * S ((S (pa_i_bplfp_power_repeat)) * pa_c_bplfp_power) + (4)))) /\ (exists pa_u_bplfp_power_product pa_v_bplfp_power_product. ((((exists pa_h_bplfp_power_product_start. pa_h_bplfp_power_product_start + S (1) = S ((S (0)) * pa_v_bplfp_power_product)) /\ exists pa_q_bplfp_power_product_start. pa_u_bplfp_power_product = pa_q_bplfp_power_product_start * S ((S (0)) * pa_v_bplfp_power_product) + (1))) /\ ((((exists pa_h_bplfp_power_product_terminal. pa_h_bplfp_power_product_terminal + S (q) = S ((S (n)) * pa_v_bplfp_power_product)) /\ exists pa_q_bplfp_power_product_terminal. pa_u_bplfp_power_product = pa_q_bplfp_power_product_terminal * S ((S (n)) * pa_v_bplfp_power_product) + (q))) /\ forall pa_i_bplfp_power_product. (exists pa_lt_bplfp_power_product_bound. pa_lt_bplfp_power_product_bound + S pa_i_bplfp_power_product = n) -> exists pa_p_bplfp_power_product pa_r_bplfp_power_product pa_s_bplfp_power_product. ((((exists pa_h_bplfp_power_product_factor. pa_h_bplfp_power_product_factor + S (pa_p_bplfp_power_product) = S ((S (pa_i_bplfp_power_product)) * pa_c_bplfp_power)) /\ exists pa_q_bplfp_power_product_factor. pa_b_bplfp_power = pa_q_bplfp_power_product_factor * S ((S (pa_i_bplfp_power_product)) * pa_c_bplfp_power) + (pa_p_bplfp_power_product))) /\ ((((exists pa_h_bplfp_power_product_partial. pa_h_bplfp_power_product_partial + S (pa_r_bplfp_power_product) = S ((S (pa_i_bplfp_power_product)) * pa_v_bplfp_power_product)) /\ exists pa_q_bplfp_power_product_partial. pa_u_bplfp_power_product = pa_q_bplfp_power_product_partial * S ((S (pa_i_bplfp_power_product)) * pa_v_bplfp_power_product) + (pa_r_bplfp_power_product))) /\ ((((exists pa_h_bplfp_power_product_successor. pa_h_bplfp_power_product_successor + S (pa_s_bplfp_power_product) = S ((S (S pa_i_bplfp_power_product)) * pa_v_bplfp_power_product)) /\ exists pa_q_bplfp_power_product_successor. pa_u_bplfp_power_product = pa_q_bplfp_power_product_successor * S ((S (S pa_i_bplfp_power_product)) * pa_v_bplfp_power_product) + (pa_s_bplfp_power_product))) /\ pa_s_bplfp_power_product = pa_r_bplfp_power_product * pa_p_bplfp_power_product)))))))) -> (exists bcf_le_gap_bplfp_result. bcf_le_gap_bplfp_result + (z) = q)

Structural proof guide

The inclusive Primorial is bounded by four to its index.

Direct prerequisites: le_refl, primorial_four_power_support_package, primorial_le_four_pow_bounded. The authored body proceeds by intermediate claims (1).

Proof neighborhood

Direct dependencies

BT000E le_refl BT00VU primorial_four_power_support_package BT00VV primorial_le_four_pow_bounded

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 n
  2. 0002intro z
  3. 0003intro q
  4. 0004intro hprimorial
  5. 0005intro hpower
  6. 0006have hbounded_all : forall N n z q. (exists bcf_le_gap_bplfpb_index. bcf_le_gap_bplfpb_index + (n) = N) -> (exists bpr_code_bplfpb_primorial bpr_scale_bplfpb_primorial. ((forall bpr_index_bplfpb_primorial_mask. (exists bpr_gap_bplfpb_primorial_mask_bound. bpr_gap_bplfpb_primorial_mask_bound + S (bpr_index_bplfpb_primorial_mask) = n) -> exists bpr_value_bplfpb_primorial_mask. ((((exists bpr_height_bplfpb_primorial_mask_decoded. bpr_height_bplfpb_primorial_mask_decoded + S (bpr_value_bplfpb_primorial_mask) = S ((S (bpr_index_bplfpb_primorial_mask)) * bpr_scale_bplfpb_primorial)) /\ exists bpr_quotient_bplfpb_primorial_mask_decoded. bpr_code_bplfpb_primorial = bpr_quotient_bplfpb_primorial_mask_decoded * S ((S (bpr_index_bplfpb_primorial_mask)) * bpr_scale_bplfpb_primorial) + (bpr_value_bplfpb_primorial_mask))) /\ (((((~(S (bpr_index_bplfpb_primorial_mask) = 1) /\ forall bpr_left_bplfpb_primorial_mask_choice_prime bpr_right_bplfpb_primorial_mask_choice_prime. S (bpr_index_bplfpb_primorial_mask) = bpr_left_bplfpb_primorial_mask_choice_prime * bpr_right_bplfpb_primorial_mask_choice_prime -> bpr_left_bplfpb_primorial_mask_choice_prime = 1 \/ bpr_right_bplfpb_primorial_mask_choice_prime = 1)) /\ bpr_value_bplfpb_primorial_mask = S (bpr_index_bplfpb_primorial_mask)) \/ (~((~(S (bpr_index_bplfpb_primorial_mask) = 1) /\ forall bpr_left_bplfpb_primorial_mask_choice_prime bpr_right_bplfpb_primorial_mask_choice_prime. S (bpr_index_bplfpb_primorial_mask) = bpr_left_bplfpb_primorial_mask_choice_prime * bpr_right_bplfpb_primorial_mask_choice_prime -> bpr_left_bplfpb_primorial_mask_choice_prime = 1 \/ bpr_right_bplfpb_primorial_mask_choice_prime = 1)) /\ bpr_value_bplfpb_primorial_mask = 1))))) /\ (exists ff_u_bplfpb_primorial_product ff_v_bplfpb_primorial_product. ((((exists ff_h_bplfpb_primorial_product_start. ff_h_bplfpb_primorial_product_start + S (1) = S ((S (0)) * ff_v_bplfpb_primorial_product)) /\ exists ff_q_bplfpb_primorial_product_start. ff_u_bplfpb_primorial_product = ff_q_bplfpb_primorial_product_start * S ((S (0)) * ff_v_bplfpb_primorial_product) + (1))) /\ ((((exists ff_h_bplfpb_primorial_product_terminal. ff_h_bplfpb_primorial_product_terminal + S (z) = S ((S (n)) * ff_v_bplfpb_primorial_product)) /\ exists ff_q_bplfpb_primorial_product_terminal. ff_u_bplfpb_primorial_product = ff_q_bplfpb_primorial_product_terminal * S ((S (n)) * ff_v_bplfpb_primorial_product) + (z))) /\ forall ff_i_bplfpb_primorial_product. (exists ff_lt_bplfpb_primorial_product_bound. ff_lt_bplfpb_primorial_product_bound + S ff_i_bplfpb_primorial_product = n) -> exists ff_p_bplfpb_primorial_product ff_r_bplfpb_primorial_product ff_s_bplfpb_primorial_product. ((((exists ff_h_bplfpb_primorial_product_factor. ff_h_bplfpb_primorial_product_factor + S (ff_p_bplfpb_primorial_product) = S ((S (ff_i_bplfpb_primorial_product)) * bpr_scale_bplfpb_primorial)) /\ exists ff_q_bplfpb_primorial_product_factor. bpr_code_bplfpb_primorial = ff_q_bplfpb_primorial_product_factor * S ((S (ff_i_bplfpb_primorial_product)) * bpr_scale_bplfpb_primorial) + (ff_p_bplfpb_primorial_product))) /\ ((((exists ff_h_bplfpb_primorial_product_partial. ff_h_bplfpb_primorial_product_partial + S (ff_r_bplfpb_primorial_product) = S ((S (ff_i_bplfpb_primorial_product)) * ff_v_bplfpb_primorial_product)) /\ exists ff_q_bplfpb_primorial_product_partial. ff_u_bplfpb_primorial_product = ff_q_bplfpb_primorial_product_partial * S ((S (ff_i_bplfpb_primorial_product)) * ff_v_bplfpb_primorial_product) + (ff_r_bplfpb_primorial_product))) /\ ((((exists ff_h_bplfpb_primorial_product_successor. ff_h_bplfpb_primorial_product_successor + S (ff_s_bplfpb_primorial_product) = S ((S (S ff_i_bplfpb_primorial_product)) * ff_v_bplfpb_primorial_product)) /\ exists ff_q_bplfpb_primorial_product_successor. ff_u_bplfpb_primorial_product = ff_q_bplfpb_primorial_product_successor * S ((S (S ff_i_bplfpb_primorial_product)) * ff_v_bplfpb_primorial_product) + (ff_s_bplfpb_primorial_product))) /\ ff_s_bplfpb_primorial_product = ff_r_bplfpb_primorial_product * ff_p_bplfpb_primorial_product)))))))) -> (exists pa_b_bplfpb_power pa_c_bplfpb_power. ((forall pa_i_bplfpb_power_repeat. (exists pa_lt_bplfpb_power_repeat_bound. pa_lt_bplfpb_power_repeat_bound + S pa_i_bplfpb_power_repeat = n) -> (((exists pa_h_bplfpb_power_repeat_decoded. pa_h_bplfpb_power_repeat_decoded + S (4) = S ((S (pa_i_bplfpb_power_repeat)) * pa_c_bplfpb_power)) /\ exists pa_q_bplfpb_power_repeat_decoded. pa_b_bplfpb_power = pa_q_bplfpb_power_repeat_decoded * S ((S (pa_i_bplfpb_power_repeat)) * pa_c_bplfpb_power) + (4)))) /\ (exists pa_u_bplfpb_power_product pa_v_bplfpb_power_product. ((((exists pa_h_bplfpb_power_product_start. pa_h_bplfpb_power_product_start + S (1) = S ((S (0)) * pa_v_bplfpb_power_product)) /\ exists pa_q_bplfpb_power_product_start. pa_u_bplfpb_power_product = pa_q_bplfpb_power_product_start * S ((S (0)) * pa_v_bplfpb_power_product) + (1))) /\ ((((exists pa_h_bplfpb_power_product_terminal. pa_h_bplfpb_power_product_terminal + S (q) = S ((S (n)) * pa_v_bplfpb_power_product)) /\ exists pa_q_bplfpb_power_product_terminal. pa_u_bplfpb_power_product = pa_q_bplfpb_power_product_terminal * S ((S (n)) * pa_v_bplfpb_power_product) + (q))) /\ forall pa_i_bplfpb_power_product. (exists pa_lt_bplfpb_power_product_bound. pa_lt_bplfpb_power_product_bound + S pa_i_bplfpb_power_product = n) -> exists pa_p_bplfpb_power_product pa_r_bplfpb_power_product pa_s_bplfpb_power_product. ((((exists pa_h_bplfpb_power_product_factor. pa_h_bplfpb_power_product_factor + S (pa_p_bplfpb_power_product) = S ((S (pa_i_bplfpb_power_product)) * pa_c_bplfpb_power)) /\ exists pa_q_bplfpb_power_product_factor. pa_b_bplfpb_power = pa_q_bplfpb_power_product_factor * S ((S (pa_i_bplfpb_power_product)) * pa_c_bplfpb_power) + (pa_p_bplfpb_power_product))) /\ ((((exists pa_h_bplfpb_power_product_partial. pa_h_bplfpb_power_product_partial + S (pa_r_bplfpb_power_product) = S ((S (pa_i_bplfpb_power_product)) * pa_v_bplfpb_power_product)) /\ exists pa_q_bplfpb_power_product_partial. pa_u_bplfpb_power_product = pa_q_bplfpb_power_product_partial * S ((S (pa_i_bplfpb_power_product)) * pa_v_bplfpb_power_product) + (pa_r_bplfpb_power_product))) /\ ((((exists pa_h_bplfpb_power_product_successor. pa_h_bplfpb_power_product_successor + S (pa_s_bplfpb_power_product) = S ((S (S pa_i_bplfpb_power_product)) * pa_v_bplfpb_power_product)) /\ exists pa_q_bplfpb_power_product_successor. pa_u_bplfpb_power_product = pa_q_bplfpb_power_product_successor * S ((S (S pa_i_bplfpb_power_product)) * pa_v_bplfpb_power_product) + (pa_s_bplfpb_power_product))) /\ pa_s_bplfpb_power_product = pa_r_bplfpb_power_product * pa_p_bplfpb_power_product)))))))) -> (exists bcf_le_gap_bplfpb_result. bcf_le_gap_bplfpb_result + (z) = q)
  7. 0007apply primorial_le_four_pow_bounded
  8. 0008exact primorial_four_power_support_package
  9. 0009specialize hbounded_all n
  10. 0010specialize hbounded_all n
  11. 0011specialize hbounded_all z
  12. 0012specialize hbounded_all q
  13. 0013apply hbounded_all
  14. 0014specialize le_refl n
  15. 0015exact le_refl
  16. 0016exact hprimorial
  17. 0017exact hpower