BT00X7

bertrand_main_inequality_factorized

Alpha body-checked · checked-use disabled

The factorized B6 inequality discharges relational-power totality exactly once.

Exact expanded PA statement

forall n s q r A B F. (exists bqb_le_gap_b6_main_thin_threshold. bqb_le_gap_b6_main_thin_threshold + (16 * 32) = (n)) -> (((exists bcs_sqrt_lower_gap_b6_main_thin_floor. bcs_sqrt_lower_gap_b6_main_thin_floor + (s) * (s) = (2 * n)) /\ exists bcs_sqrt_upper_gap_b6_main_thin_floor. bcs_sqrt_upper_gap_b6_main_thin_floor + S (2 * n) = S (s) * S (s))) -> ((((2 * n) = 3 * (q) + (r)) /\ exists bmi_remainder_gap_b6_main_thin_division. bmi_remainder_gap_b6_main_thin_division + S (r) = 3)) -> (exists pa_b_b6_main_thin_a pa_c_b6_main_thin_a. ((forall pa_i_b6_main_thin_a_repeat. (exists pa_lt_b6_main_thin_a_repeat_bound. pa_lt_b6_main_thin_a_repeat_bound + S pa_i_b6_main_thin_a_repeat = s) -> (((exists pa_h_b6_main_thin_a_repeat_decoded. pa_h_b6_main_thin_a_repeat_decoded + S (2 * n) = S ((S (pa_i_b6_main_thin_a_repeat)) * pa_c_b6_main_thin_a)) /\ exists pa_q_b6_main_thin_a_repeat_decoded. pa_b_b6_main_thin_a = pa_q_b6_main_thin_a_repeat_decoded * S ((S (pa_i_b6_main_thin_a_repeat)) * pa_c_b6_main_thin_a) + (2 * n)))) /\ (exists pa_u_b6_main_thin_a_product pa_v_b6_main_thin_a_product. ((((exists pa_h_b6_main_thin_a_product_start. pa_h_b6_main_thin_a_product_start + S (1) = S ((S (0)) * pa_v_b6_main_thin_a_product)) /\ exists pa_q_b6_main_thin_a_product_start. pa_u_b6_main_thin_a_product = pa_q_b6_main_thin_a_product_start * S ((S (0)) * pa_v_b6_main_thin_a_product) + (1))) /\ ((((exists pa_h_b6_main_thin_a_product_terminal. pa_h_b6_main_thin_a_product_terminal + S (A) = S ((S (s)) * pa_v_b6_main_thin_a_product)) /\ exists pa_q_b6_main_thin_a_product_terminal. pa_u_b6_main_thin_a_product = pa_q_b6_main_thin_a_product_terminal * S ((S (s)) * pa_v_b6_main_thin_a_product) + (A))) /\ forall pa_i_b6_main_thin_a_product. (exists pa_lt_b6_main_thin_a_product_bound. pa_lt_b6_main_thin_a_product_bound + S pa_i_b6_main_thin_a_product = s) -> exists pa_p_b6_main_thin_a_product pa_r_b6_main_thin_a_product pa_s_b6_main_thin_a_product. ((((exists pa_h_b6_main_thin_a_product_factor. pa_h_b6_main_thin_a_product_factor + S (pa_p_b6_main_thin_a_product) = S ((S (pa_i_b6_main_thin_a_product)) * pa_c_b6_main_thin_a)) /\ exists pa_q_b6_main_thin_a_product_factor. pa_b_b6_main_thin_a = pa_q_b6_main_thin_a_product_factor * S ((S (pa_i_b6_main_thin_a_product)) * pa_c_b6_main_thin_a) + (pa_p_b6_main_thin_a_product))) /\ ((((exists pa_h_b6_main_thin_a_product_partial. pa_h_b6_main_thin_a_product_partial + S (pa_r_b6_main_thin_a_product) = S ((S (pa_i_b6_main_thin_a_product)) * pa_v_b6_main_thin_a_product)) /\ exists pa_q_b6_main_thin_a_product_partial. pa_u_b6_main_thin_a_product = pa_q_b6_main_thin_a_product_partial * S ((S (pa_i_b6_main_thin_a_product)) * pa_v_b6_main_thin_a_product) + (pa_r_b6_main_thin_a_product))) /\ ((((exists pa_h_b6_main_thin_a_product_successor. pa_h_b6_main_thin_a_product_successor + S (pa_s_b6_main_thin_a_product) = S ((S (S pa_i_b6_main_thin_a_product)) * pa_v_b6_main_thin_a_product)) /\ exists pa_q_b6_main_thin_a_product_successor. pa_u_b6_main_thin_a_product = pa_q_b6_main_thin_a_product_successor * S ((S (S pa_i_b6_main_thin_a_product)) * pa_v_b6_main_thin_a_product) + (pa_s_b6_main_thin_a_product))) /\ pa_s_b6_main_thin_a_product = pa_r_b6_main_thin_a_product * pa_p_b6_main_thin_a_product)))))))) -> (exists pa_b_b6_main_thin_b pa_c_b6_main_thin_b. ((forall pa_i_b6_main_thin_b_repeat. (exists pa_lt_b6_main_thin_b_repeat_bound. pa_lt_b6_main_thin_b_repeat_bound + S pa_i_b6_main_thin_b_repeat = q) -> (((exists pa_h_b6_main_thin_b_repeat_decoded. pa_h_b6_main_thin_b_repeat_decoded + S (4) = S ((S (pa_i_b6_main_thin_b_repeat)) * pa_c_b6_main_thin_b)) /\ exists pa_q_b6_main_thin_b_repeat_decoded. pa_b_b6_main_thin_b = pa_q_b6_main_thin_b_repeat_decoded * S ((S (pa_i_b6_main_thin_b_repeat)) * pa_c_b6_main_thin_b) + (4)))) /\ (exists pa_u_b6_main_thin_b_product pa_v_b6_main_thin_b_product. ((((exists pa_h_b6_main_thin_b_product_start. pa_h_b6_main_thin_b_product_start + S (1) = S ((S (0)) * pa_v_b6_main_thin_b_product)) /\ exists pa_q_b6_main_thin_b_product_start. pa_u_b6_main_thin_b_product = pa_q_b6_main_thin_b_product_start * S ((S (0)) * pa_v_b6_main_thin_b_product) + (1))) /\ ((((exists pa_h_b6_main_thin_b_product_terminal. pa_h_b6_main_thin_b_product_terminal + S (B) = S ((S (q)) * pa_v_b6_main_thin_b_product)) /\ exists pa_q_b6_main_thin_b_product_terminal. pa_u_b6_main_thin_b_product = pa_q_b6_main_thin_b_product_terminal * S ((S (q)) * pa_v_b6_main_thin_b_product) + (B))) /\ forall pa_i_b6_main_thin_b_product. (exists pa_lt_b6_main_thin_b_product_bound. pa_lt_b6_main_thin_b_product_bound + S pa_i_b6_main_thin_b_product = q) -> exists pa_p_b6_main_thin_b_product pa_r_b6_main_thin_b_product pa_s_b6_main_thin_b_product. ((((exists pa_h_b6_main_thin_b_product_factor. pa_h_b6_main_thin_b_product_factor + S (pa_p_b6_main_thin_b_product) = S ((S (pa_i_b6_main_thin_b_product)) * pa_c_b6_main_thin_b)) /\ exists pa_q_b6_main_thin_b_product_factor. pa_b_b6_main_thin_b = pa_q_b6_main_thin_b_product_factor * S ((S (pa_i_b6_main_thin_b_product)) * pa_c_b6_main_thin_b) + (pa_p_b6_main_thin_b_product))) /\ ((((exists pa_h_b6_main_thin_b_product_partial. pa_h_b6_main_thin_b_product_partial + S (pa_r_b6_main_thin_b_product) = S ((S (pa_i_b6_main_thin_b_product)) * pa_v_b6_main_thin_b_product)) /\ exists pa_q_b6_main_thin_b_product_partial. pa_u_b6_main_thin_b_product = pa_q_b6_main_thin_b_product_partial * S ((S (pa_i_b6_main_thin_b_product)) * pa_v_b6_main_thin_b_product) + (pa_r_b6_main_thin_b_product))) /\ ((((exists pa_h_b6_main_thin_b_product_successor. pa_h_b6_main_thin_b_product_successor + S (pa_s_b6_main_thin_b_product) = S ((S (S pa_i_b6_main_thin_b_product)) * pa_v_b6_main_thin_b_product)) /\ exists pa_q_b6_main_thin_b_product_successor. pa_u_b6_main_thin_b_product = pa_q_b6_main_thin_b_product_successor * S ((S (S pa_i_b6_main_thin_b_product)) * pa_v_b6_main_thin_b_product) + (pa_s_b6_main_thin_b_product))) /\ pa_s_b6_main_thin_b_product = pa_r_b6_main_thin_b_product * pa_p_b6_main_thin_b_product)))))))) -> (exists pa_b_b6_main_thin_f pa_c_b6_main_thin_f. ((forall pa_i_b6_main_thin_f_repeat. (exists pa_lt_b6_main_thin_f_repeat_bound. pa_lt_b6_main_thin_f_repeat_bound + S pa_i_b6_main_thin_f_repeat = n) -> (((exists pa_h_b6_main_thin_f_repeat_decoded. pa_h_b6_main_thin_f_repeat_decoded + S (4) = S ((S (pa_i_b6_main_thin_f_repeat)) * pa_c_b6_main_thin_f)) /\ exists pa_q_b6_main_thin_f_repeat_decoded. pa_b_b6_main_thin_f = pa_q_b6_main_thin_f_repeat_decoded * S ((S (pa_i_b6_main_thin_f_repeat)) * pa_c_b6_main_thin_f) + (4)))) /\ (exists pa_u_b6_main_thin_f_product pa_v_b6_main_thin_f_product. ((((exists pa_h_b6_main_thin_f_product_start. pa_h_b6_main_thin_f_product_start + S (1) = S ((S (0)) * pa_v_b6_main_thin_f_product)) /\ exists pa_q_b6_main_thin_f_product_start. pa_u_b6_main_thin_f_product = pa_q_b6_main_thin_f_product_start * S ((S (0)) * pa_v_b6_main_thin_f_product) + (1))) /\ ((((exists pa_h_b6_main_thin_f_product_terminal. pa_h_b6_main_thin_f_product_terminal + S (F) = S ((S (n)) * pa_v_b6_main_thin_f_product)) /\ exists pa_q_b6_main_thin_f_product_terminal. pa_u_b6_main_thin_f_product = pa_q_b6_main_thin_f_product_terminal * S ((S (n)) * pa_v_b6_main_thin_f_product) + (F))) /\ forall pa_i_b6_main_thin_f_product. (exists pa_lt_b6_main_thin_f_product_bound. pa_lt_b6_main_thin_f_product_bound + S pa_i_b6_main_thin_f_product = n) -> exists pa_p_b6_main_thin_f_product pa_r_b6_main_thin_f_product pa_s_b6_main_thin_f_product. ((((exists pa_h_b6_main_thin_f_product_factor. pa_h_b6_main_thin_f_product_factor + S (pa_p_b6_main_thin_f_product) = S ((S (pa_i_b6_main_thin_f_product)) * pa_c_b6_main_thin_f)) /\ exists pa_q_b6_main_thin_f_product_factor. pa_b_b6_main_thin_f = pa_q_b6_main_thin_f_product_factor * S ((S (pa_i_b6_main_thin_f_product)) * pa_c_b6_main_thin_f) + (pa_p_b6_main_thin_f_product))) /\ ((((exists pa_h_b6_main_thin_f_product_partial. pa_h_b6_main_thin_f_product_partial + S (pa_r_b6_main_thin_f_product) = S ((S (pa_i_b6_main_thin_f_product)) * pa_v_b6_main_thin_f_product)) /\ exists pa_q_b6_main_thin_f_product_partial. pa_u_b6_main_thin_f_product = pa_q_b6_main_thin_f_product_partial * S ((S (pa_i_b6_main_thin_f_product)) * pa_v_b6_main_thin_f_product) + (pa_r_b6_main_thin_f_product))) /\ ((((exists pa_h_b6_main_thin_f_product_successor. pa_h_b6_main_thin_f_product_successor + S (pa_s_b6_main_thin_f_product) = S ((S (S pa_i_b6_main_thin_f_product)) * pa_v_b6_main_thin_f_product)) /\ exists pa_q_b6_main_thin_f_product_successor. pa_u_b6_main_thin_f_product = pa_q_b6_main_thin_f_product_successor * S ((S (S pa_i_b6_main_thin_f_product)) * pa_v_b6_main_thin_f_product) + (pa_s_b6_main_thin_f_product))) /\ pa_s_b6_main_thin_f_product = pa_r_b6_main_thin_f_product * pa_p_b6_main_thin_f_product)))))))) -> (exists bqb_le_gap_b6_main_thin_result. bqb_le_gap_b6_main_thin_result + (n * A * B) = (F))

Structural proof guide

The factorized B6 inequality discharges relational-power totality exactly once.

Direct prerequisites: pow_exists, bertrand_main_inequality_factorized_from_total. The authored body proceeds by intermediate claims (1).

Proof neighborhood

Direct dependencies

BT0080 pow_exists BT00X6 bertrand_main_inequality_factorized_from_total

Direct dependents

BT00X8 bertrand_main_inequality_nat

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 s
  3. 0003intro q
  4. 0004intro r
  5. 0005intro A
  6. 0006intro B
  7. 0007intro F
  8. 0008intro hthreshold
  9. 0009intro hfloor
  10. 0010intro hdiv
  11. 0011intro hA
  12. 0012intro hB
  13. 0013intro hF
  14. 0014have htotal : forall bpt_a_b6_main_thin_total bpt_e_b6_main_thin_total. exists bpt_x_b6_main_thin_total. (exists ff_b_bpt_value_b6_main_thin_total ff_c_bpt_value_b6_main_thin_total. ((forall ff_i_bpt_value_b6_main_thin_total_repeat. (exists ff_lt_bpt_value_b6_main_thin_total_repeat_bound. ff_lt_bpt_value_b6_main_thin_total_repeat_bound + S ff_i_bpt_value_b6_main_thin_total_repeat = bpt_e_b6_main_thin_total) -> (((exists ff_h_bpt_value_b6_main_thin_total_repeat_decoded. ff_h_bpt_value_b6_main_thin_total_repeat_decoded + S (bpt_a_b6_main_thin_total) = S ((S (ff_i_bpt_value_b6_main_thin_total_repeat)) * ff_c_bpt_value_b6_main_thin_total)) /\ exists ff_q_bpt_value_b6_main_thin_total_repeat_decoded. ff_b_bpt_value_b6_main_thin_total = ff_q_bpt_value_b6_main_thin_total_repeat_decoded * S ((S (ff_i_bpt_value_b6_main_thin_total_repeat)) * ff_c_bpt_value_b6_main_thin_total) + (bpt_a_b6_main_thin_total)))) /\ (exists ff_u_bpt_value_b6_main_thin_total_product ff_v_bpt_value_b6_main_thin_total_product. ((((exists ff_h_bpt_value_b6_main_thin_total_product_start. ff_h_bpt_value_b6_main_thin_total_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_b6_main_thin_total_product)) /\ exists ff_q_bpt_value_b6_main_thin_total_product_start. ff_u_bpt_value_b6_main_thin_total_product = ff_q_bpt_value_b6_main_thin_total_product_start * S ((S (0)) * ff_v_bpt_value_b6_main_thin_total_product) + (1))) /\ ((((exists ff_h_bpt_value_b6_main_thin_total_product_terminal. ff_h_bpt_value_b6_main_thin_total_product_terminal + S (bpt_x_b6_main_thin_total) = S ((S (bpt_e_b6_main_thin_total)) * ff_v_bpt_value_b6_main_thin_total_product)) /\ exists ff_q_bpt_value_b6_main_thin_total_product_terminal. ff_u_bpt_value_b6_main_thin_total_product = ff_q_bpt_value_b6_main_thin_total_product_terminal * S ((S (bpt_e_b6_main_thin_total)) * ff_v_bpt_value_b6_main_thin_total_product) + (bpt_x_b6_main_thin_total))) /\ forall ff_i_bpt_value_b6_main_thin_total_product. (exists ff_lt_bpt_value_b6_main_thin_total_product_bound. ff_lt_bpt_value_b6_main_thin_total_product_bound + S ff_i_bpt_value_b6_main_thin_total_product = bpt_e_b6_main_thin_total) -> exists ff_p_bpt_value_b6_main_thin_total_product ff_r_bpt_value_b6_main_thin_total_product ff_s_bpt_value_b6_main_thin_total_product. ((((exists ff_h_bpt_value_b6_main_thin_total_product_factor. ff_h_bpt_value_b6_main_thin_total_product_factor + S (ff_p_bpt_value_b6_main_thin_total_product) = S ((S (ff_i_bpt_value_b6_main_thin_total_product)) * ff_c_bpt_value_b6_main_thin_total)) /\ exists ff_q_bpt_value_b6_main_thin_total_product_factor. ff_b_bpt_value_b6_main_thin_total = ff_q_bpt_value_b6_main_thin_total_product_factor * S ((S (ff_i_bpt_value_b6_main_thin_total_product)) * ff_c_bpt_value_b6_main_thin_total) + (ff_p_bpt_value_b6_main_thin_total_product))) /\ ((((exists ff_h_bpt_value_b6_main_thin_total_product_partial. ff_h_bpt_value_b6_main_thin_total_product_partial + S (ff_r_bpt_value_b6_main_thin_total_product) = S ((S (ff_i_bpt_value_b6_main_thin_total_product)) * ff_v_bpt_value_b6_main_thin_total_product)) /\ exists ff_q_bpt_value_b6_main_thin_total_product_partial. ff_u_bpt_value_b6_main_thin_total_product = ff_q_bpt_value_b6_main_thin_total_product_partial * S ((S (ff_i_bpt_value_b6_main_thin_total_product)) * ff_v_bpt_value_b6_main_thin_total_product) + (ff_r_bpt_value_b6_main_thin_total_product))) /\ ((((exists ff_h_bpt_value_b6_main_thin_total_product_successor. ff_h_bpt_value_b6_main_thin_total_product_successor + S (ff_s_bpt_value_b6_main_thin_total_product) = S ((S (S ff_i_bpt_value_b6_main_thin_total_product)) * ff_v_bpt_value_b6_main_thin_total_product)) /\ exists ff_q_bpt_value_b6_main_thin_total_product_successor. ff_u_bpt_value_b6_main_thin_total_product = ff_q_bpt_value_b6_main_thin_total_product_successor * S ((S (S ff_i_bpt_value_b6_main_thin_total_product)) * ff_v_bpt_value_b6_main_thin_total_product) + (ff_s_bpt_value_b6_main_thin_total_product))) /\ ff_s_bpt_value_b6_main_thin_total_product = ff_r_bpt_value_b6_main_thin_total_product * ff_p_bpt_value_b6_main_thin_total_product))))))))
  15. 0015intro a
  16. 0016intro e
  17. 0017specialize pow_exists a
  18. 0018specialize pow_exists e
  19. 0019exact pow_exists
  20. 0020specialize bertrand_main_inequality_factorized_from_total n
  21. 0021specialize bertrand_main_inequality_factorized_from_total s
  22. 0022specialize bertrand_main_inequality_factorized_from_total q
  23. 0023specialize bertrand_main_inequality_factorized_from_total r
  24. 0024specialize bertrand_main_inequality_factorized_from_total A
  25. 0025specialize bertrand_main_inequality_factorized_from_total B
  26. 0026specialize bertrand_main_inequality_factorized_from_total F
  27. 0027apply bertrand_main_inequality_factorized_from_total
  28. 0028exact htotal
  29. 0029exact hthreshold
  30. 0030exact hfloor
  31. 0031exact hdiv
  32. 0032exact hA
  33. 0033exact hB
  34. 0034exact hF