BT00X6 · Bertrand theorem

bertrand_main_inequality_factorized_from_total

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

The factorized threshold and all-root envelope imply the B6 power-product inequality under one supplied power-totality premise.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

∀ n. ∀ s. ∀ q. ∀ r. ∀ A. ∀ B. ∀ F. (∀ x. ∀ y. ∃ z. Pow(x,y,z)) → Le(16 · 32,n) → FloorSqrt(2 · n,s) → DivRem(2 · n,3,q,r) → Pow(2 · n,s,A) → Pow(4,q,B) → Pow(4,n,F) → Le(n · A · B,F)

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0001 Le PD0007 DivRem PD0020 Pow PD0051 FloorSqrt

8 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0020 Pow PD0052 CeilDivSix

16 occurrences

Exact expanded native-PA statement
forall n s q r A B F. (forall bpt_a_b6_main_factorized bpt_e_b6_main_factorized. exists bpt_x_b6_main_factorized. (exists ff_b_bpt_value_b6_main_factorized ff_c_bpt_value_b6_main_factorized. ((forall ff_i_bpt_value_b6_main_factorized_repeat. (exists ff_lt_bpt_value_b6_main_factorized_repeat_bound. ff_lt_bpt_value_b6_main_factorized_repeat_bound + S ff_i_bpt_value_b6_main_factorized_repeat = bpt_e_b6_main_factorized) -> (((exists ff_h_bpt_value_b6_main_factorized_repeat_decoded. ff_h_bpt_value_b6_main_factorized_repeat_decoded + S (bpt_a_b6_main_factorized) = S ((S (ff_i_bpt_value_b6_main_factorized_repeat)) * ff_c_bpt_value_b6_main_factorized)) /\ exists ff_q_bpt_value_b6_main_factorized_repeat_decoded. ff_b_bpt_value_b6_main_factorized = ff_q_bpt_value_b6_main_factorized_repeat_decoded * S ((S (ff_i_bpt_value_b6_main_factorized_repeat)) * ff_c_bpt_value_b6_main_factorized) + (bpt_a_b6_main_factorized)))) /\ (exists ff_u_bpt_value_b6_main_factorized_product ff_v_bpt_value_b6_main_factorized_product. ((((exists ff_h_bpt_value_b6_main_factorized_product_start. ff_h_bpt_value_b6_main_factorized_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_b6_main_factorized_product)) /\ exists ff_q_bpt_value_b6_main_factorized_product_start. ff_u_bpt_value_b6_main_factorized_product = ff_q_bpt_value_b6_main_factorized_product_start * S ((S (0)) * ff_v_bpt_value_b6_main_factorized_product) + (1))) /\ ((((exists ff_h_bpt_value_b6_main_factorized_product_terminal. ff_h_bpt_value_b6_main_factorized_product_terminal + S (bpt_x_b6_main_factorized) = S ((S (bpt_e_b6_main_factorized)) * ff_v_bpt_value_b6_main_factorized_product)) /\ exists ff_q_bpt_value_b6_main_factorized_product_terminal. ff_u_bpt_value_b6_main_factorized_product = ff_q_bpt_value_b6_main_factorized_product_terminal * S ((S (bpt_e_b6_main_factorized)) * ff_v_bpt_value_b6_main_factorized_product) + (bpt_x_b6_main_factorized))) /\ forall ff_i_bpt_value_b6_main_factorized_product. (exists ff_lt_bpt_value_b6_main_factorized_product_bound. ff_lt_bpt_value_b6_main_factorized_product_bound + S ff_i_bpt_value_b6_main_factorized_product = bpt_e_b6_main_factorized) -> exists ff_p_bpt_value_b6_main_factorized_product ff_r_bpt_value_b6_main_factorized_product ff_s_bpt_value_b6_main_factorized_product. ((((exists ff_h_bpt_value_b6_main_factorized_product_factor. ff_h_bpt_value_b6_main_factorized_product_factor + S (ff_p_bpt_value_b6_main_factorized_product) = S ((S (ff_i_bpt_value_b6_main_factorized_product)) * ff_c_bpt_value_b6_main_factorized)) /\ exists ff_q_bpt_value_b6_main_factorized_product_factor. ff_b_bpt_value_b6_main_factorized = ff_q_bpt_value_b6_main_factorized_product_factor * S ((S (ff_i_bpt_value_b6_main_factorized_product)) * ff_c_bpt_value_b6_main_factorized) + (ff_p_bpt_value_b6_main_factorized_product))) /\ ((((exists ff_h_bpt_value_b6_main_factorized_product_partial. ff_h_bpt_value_b6_main_factorized_product_partial + S (ff_r_bpt_value_b6_main_factorized_product) = S ((S (ff_i_bpt_value_b6_main_factorized_product)) * ff_v_bpt_value_b6_main_factorized_product)) /\ exists ff_q_bpt_value_b6_main_factorized_product_partial. ff_u_bpt_value_b6_main_factorized_product = ff_q_bpt_value_b6_main_factorized_product_partial * S ((S (ff_i_bpt_value_b6_main_factorized_product)) * ff_v_bpt_value_b6_main_factorized_product) + (ff_r_bpt_value_b6_main_factorized_product))) /\ ((((exists ff_h_bpt_value_b6_main_factorized_product_successor. ff_h_bpt_value_b6_main_factorized_product_successor + S (ff_s_bpt_value_b6_main_factorized_product) = S ((S (S ff_i_bpt_value_b6_main_factorized_product)) * ff_v_bpt_value_b6_main_factorized_product)) /\ exists ff_q_bpt_value_b6_main_factorized_product_successor. ff_u_bpt_value_b6_main_factorized_product = ff_q_bpt_value_b6_main_factorized_product_successor * S ((S (S ff_i_bpt_value_b6_main_factorized_product)) * ff_v_bpt_value_b6_main_factorized_product) + (ff_s_bpt_value_b6_main_factorized_product))) /\ ff_s_bpt_value_b6_main_factorized_product = ff_r_bpt_value_b6_main_factorized_product * ff_p_bpt_value_b6_main_factorized_product))))))))) -> (exists bqb_le_gap_b6_main_factorized_threshold. bqb_le_gap_b6_main_factorized_threshold + (16 * 32) = (n)) -> (((exists bcs_sqrt_lower_gap_b6_main_factorized_floor. bcs_sqrt_lower_gap_b6_main_factorized_floor + (s) * (s) = (2 * n)) /\ exists bcs_sqrt_upper_gap_b6_main_factorized_floor. bcs_sqrt_upper_gap_b6_main_factorized_floor + S (2 * n) = S (s) * S (s))) -> ((((2 * n) = 3 * (q) + (r)) /\ exists bmi_remainder_gap_b6_main_factorized_division. bmi_remainder_gap_b6_main_factorized_division + S (r) = 3)) -> (exists pa_b_b6_main_factorized_a pa_c_b6_main_factorized_a. ((forall pa_i_b6_main_factorized_a_repeat. (exists pa_lt_b6_main_factorized_a_repeat_bound. pa_lt_b6_main_factorized_a_repeat_bound + S pa_i_b6_main_factorized_a_repeat = s) -> (((exists pa_h_b6_main_factorized_a_repeat_decoded. pa_h_b6_main_factorized_a_repeat_decoded + S (2 * n) = S ((S (pa_i_b6_main_factorized_a_repeat)) * pa_c_b6_main_factorized_a)) /\ exists pa_q_b6_main_factorized_a_repeat_decoded. pa_b_b6_main_factorized_a = pa_q_b6_main_factorized_a_repeat_decoded * S ((S (pa_i_b6_main_factorized_a_repeat)) * pa_c_b6_main_factorized_a) + (2 * n)))) /\ (exists pa_u_b6_main_factorized_a_product pa_v_b6_main_factorized_a_product. ((((exists pa_h_b6_main_factorized_a_product_start. pa_h_b6_main_factorized_a_product_start + S (1) = S ((S (0)) * pa_v_b6_main_factorized_a_product)) /\ exists pa_q_b6_main_factorized_a_product_start. pa_u_b6_main_factorized_a_product = pa_q_b6_main_factorized_a_product_start * S ((S (0)) * pa_v_b6_main_factorized_a_product) + (1))) /\ ((((exists pa_h_b6_main_factorized_a_product_terminal. pa_h_b6_main_factorized_a_product_terminal + S (A) = S ((S (s)) * pa_v_b6_main_factorized_a_product)) /\ exists pa_q_b6_main_factorized_a_product_terminal. pa_u_b6_main_factorized_a_product = pa_q_b6_main_factorized_a_product_terminal * S ((S (s)) * pa_v_b6_main_factorized_a_product) + (A))) /\ forall pa_i_b6_main_factorized_a_product. (exists pa_lt_b6_main_factorized_a_product_bound. pa_lt_b6_main_factorized_a_product_bound + S pa_i_b6_main_factorized_a_product = s) -> exists pa_p_b6_main_factorized_a_product pa_r_b6_main_factorized_a_product pa_s_b6_main_factorized_a_product. ((((exists pa_h_b6_main_factorized_a_product_factor. pa_h_b6_main_factorized_a_product_factor + S (pa_p_b6_main_factorized_a_product) = S ((S (pa_i_b6_main_factorized_a_product)) * pa_c_b6_main_factorized_a)) /\ exists pa_q_b6_main_factorized_a_product_factor. pa_b_b6_main_factorized_a = pa_q_b6_main_factorized_a_product_factor * S ((S (pa_i_b6_main_factorized_a_product)) * pa_c_b6_main_factorized_a) + (pa_p_b6_main_factorized_a_product))) /\ ((((exists pa_h_b6_main_factorized_a_product_partial. pa_h_b6_main_factorized_a_product_partial + S (pa_r_b6_main_factorized_a_product) = S ((S (pa_i_b6_main_factorized_a_product)) * pa_v_b6_main_factorized_a_product)) /\ exists pa_q_b6_main_factorized_a_product_partial. pa_u_b6_main_factorized_a_product = pa_q_b6_main_factorized_a_product_partial * S ((S (pa_i_b6_main_factorized_a_product)) * pa_v_b6_main_factorized_a_product) + (pa_r_b6_main_factorized_a_product))) /\ ((((exists pa_h_b6_main_factorized_a_product_successor. pa_h_b6_main_factorized_a_product_successor + S (pa_s_b6_main_factorized_a_product) = S ((S (S pa_i_b6_main_factorized_a_product)) * pa_v_b6_main_factorized_a_product)) /\ exists pa_q_b6_main_factorized_a_product_successor. pa_u_b6_main_factorized_a_product = pa_q_b6_main_factorized_a_product_successor * S ((S (S pa_i_b6_main_factorized_a_product)) * pa_v_b6_main_factorized_a_product) + (pa_s_b6_main_factorized_a_product))) /\ pa_s_b6_main_factorized_a_product = pa_r_b6_main_factorized_a_product * pa_p_b6_main_factorized_a_product)))))))) -> (exists pa_b_b6_main_factorized_b pa_c_b6_main_factorized_b. ((forall pa_i_b6_main_factorized_b_repeat. (exists pa_lt_b6_main_factorized_b_repeat_bound. pa_lt_b6_main_factorized_b_repeat_bound + S pa_i_b6_main_factorized_b_repeat = q) -> (((exists pa_h_b6_main_factorized_b_repeat_decoded. pa_h_b6_main_factorized_b_repeat_decoded + S (4) = S ((S (pa_i_b6_main_factorized_b_repeat)) * pa_c_b6_main_factorized_b)) /\ exists pa_q_b6_main_factorized_b_repeat_decoded. pa_b_b6_main_factorized_b = pa_q_b6_main_factorized_b_repeat_decoded * S ((S (pa_i_b6_main_factorized_b_repeat)) * pa_c_b6_main_factorized_b) + (4)))) /\ (exists pa_u_b6_main_factorized_b_product pa_v_b6_main_factorized_b_product. ((((exists pa_h_b6_main_factorized_b_product_start. pa_h_b6_main_factorized_b_product_start + S (1) = S ((S (0)) * pa_v_b6_main_factorized_b_product)) /\ exists pa_q_b6_main_factorized_b_product_start. pa_u_b6_main_factorized_b_product = pa_q_b6_main_factorized_b_product_start * S ((S (0)) * pa_v_b6_main_factorized_b_product) + (1))) /\ ((((exists pa_h_b6_main_factorized_b_product_terminal. pa_h_b6_main_factorized_b_product_terminal + S (B) = S ((S (q)) * pa_v_b6_main_factorized_b_product)) /\ exists pa_q_b6_main_factorized_b_product_terminal. pa_u_b6_main_factorized_b_product = pa_q_b6_main_factorized_b_product_terminal * S ((S (q)) * pa_v_b6_main_factorized_b_product) + (B))) /\ forall pa_i_b6_main_factorized_b_product. (exists pa_lt_b6_main_factorized_b_product_bound. pa_lt_b6_main_factorized_b_product_bound + S pa_i_b6_main_factorized_b_product = q) -> exists pa_p_b6_main_factorized_b_product pa_r_b6_main_factorized_b_product pa_s_b6_main_factorized_b_product. ((((exists pa_h_b6_main_factorized_b_product_factor. pa_h_b6_main_factorized_b_product_factor + S (pa_p_b6_main_factorized_b_product) = S ((S (pa_i_b6_main_factorized_b_product)) * pa_c_b6_main_factorized_b)) /\ exists pa_q_b6_main_factorized_b_product_factor. pa_b_b6_main_factorized_b = pa_q_b6_main_factorized_b_product_factor * S ((S (pa_i_b6_main_factorized_b_product)) * pa_c_b6_main_factorized_b) + (pa_p_b6_main_factorized_b_product))) /\ ((((exists pa_h_b6_main_factorized_b_product_partial. pa_h_b6_main_factorized_b_product_partial + S (pa_r_b6_main_factorized_b_product) = S ((S (pa_i_b6_main_factorized_b_product)) * pa_v_b6_main_factorized_b_product)) /\ exists pa_q_b6_main_factorized_b_product_partial. pa_u_b6_main_factorized_b_product = pa_q_b6_main_factorized_b_product_partial * S ((S (pa_i_b6_main_factorized_b_product)) * pa_v_b6_main_factorized_b_product) + (pa_r_b6_main_factorized_b_product))) /\ ((((exists pa_h_b6_main_factorized_b_product_successor. pa_h_b6_main_factorized_b_product_successor + S (pa_s_b6_main_factorized_b_product) = S ((S (S pa_i_b6_main_factorized_b_product)) * pa_v_b6_main_factorized_b_product)) /\ exists pa_q_b6_main_factorized_b_product_successor. pa_u_b6_main_factorized_b_product = pa_q_b6_main_factorized_b_product_successor * S ((S (S pa_i_b6_main_factorized_b_product)) * pa_v_b6_main_factorized_b_product) + (pa_s_b6_main_factorized_b_product))) /\ pa_s_b6_main_factorized_b_product = pa_r_b6_main_factorized_b_product * pa_p_b6_main_factorized_b_product)))))))) -> (exists pa_b_b6_main_factorized_f pa_c_b6_main_factorized_f. ((forall pa_i_b6_main_factorized_f_repeat. (exists pa_lt_b6_main_factorized_f_repeat_bound. pa_lt_b6_main_factorized_f_repeat_bound + S pa_i_b6_main_factorized_f_repeat = n) -> (((exists pa_h_b6_main_factorized_f_repeat_decoded. pa_h_b6_main_factorized_f_repeat_decoded + S (4) = S ((S (pa_i_b6_main_factorized_f_repeat)) * pa_c_b6_main_factorized_f)) /\ exists pa_q_b6_main_factorized_f_repeat_decoded. pa_b_b6_main_factorized_f = pa_q_b6_main_factorized_f_repeat_decoded * S ((S (pa_i_b6_main_factorized_f_repeat)) * pa_c_b6_main_factorized_f) + (4)))) /\ (exists pa_u_b6_main_factorized_f_product pa_v_b6_main_factorized_f_product. ((((exists pa_h_b6_main_factorized_f_product_start. pa_h_b6_main_factorized_f_product_start + S (1) = S ((S (0)) * pa_v_b6_main_factorized_f_product)) /\ exists pa_q_b6_main_factorized_f_product_start. pa_u_b6_main_factorized_f_product = pa_q_b6_main_factorized_f_product_start * S ((S (0)) * pa_v_b6_main_factorized_f_product) + (1))) /\ ((((exists pa_h_b6_main_factorized_f_product_terminal. pa_h_b6_main_factorized_f_product_terminal + S (F) = S ((S (n)) * pa_v_b6_main_factorized_f_product)) /\ exists pa_q_b6_main_factorized_f_product_terminal. pa_u_b6_main_factorized_f_product = pa_q_b6_main_factorized_f_product_terminal * S ((S (n)) * pa_v_b6_main_factorized_f_product) + (F))) /\ forall pa_i_b6_main_factorized_f_product. (exists pa_lt_b6_main_factorized_f_product_bound. pa_lt_b6_main_factorized_f_product_bound + S pa_i_b6_main_factorized_f_product = n) -> exists pa_p_b6_main_factorized_f_product pa_r_b6_main_factorized_f_product pa_s_b6_main_factorized_f_product. ((((exists pa_h_b6_main_factorized_f_product_factor. pa_h_b6_main_factorized_f_product_factor + S (pa_p_b6_main_factorized_f_product) = S ((S (pa_i_b6_main_factorized_f_product)) * pa_c_b6_main_factorized_f)) /\ exists pa_q_b6_main_factorized_f_product_factor. pa_b_b6_main_factorized_f = pa_q_b6_main_factorized_f_product_factor * S ((S (pa_i_b6_main_factorized_f_product)) * pa_c_b6_main_factorized_f) + (pa_p_b6_main_factorized_f_product))) /\ ((((exists pa_h_b6_main_factorized_f_product_partial. pa_h_b6_main_factorized_f_product_partial + S (pa_r_b6_main_factorized_f_product) = S ((S (pa_i_b6_main_factorized_f_product)) * pa_v_b6_main_factorized_f_product)) /\ exists pa_q_b6_main_factorized_f_product_partial. pa_u_b6_main_factorized_f_product = pa_q_b6_main_factorized_f_product_partial * S ((S (pa_i_b6_main_factorized_f_product)) * pa_v_b6_main_factorized_f_product) + (pa_r_b6_main_factorized_f_product))) /\ ((((exists pa_h_b6_main_factorized_f_product_successor. pa_h_b6_main_factorized_f_product_successor + S (pa_s_b6_main_factorized_f_product) = S ((S (S pa_i_b6_main_factorized_f_product)) * pa_v_b6_main_factorized_f_product)) /\ exists pa_q_b6_main_factorized_f_product_successor. pa_u_b6_main_factorized_f_product = pa_q_b6_main_factorized_f_product_successor * S ((S (S pa_i_b6_main_factorized_f_product)) * pa_v_b6_main_factorized_f_product) + (pa_s_b6_main_factorized_f_product))) /\ pa_s_b6_main_factorized_f_product = pa_r_b6_main_factorized_f_product * pa_p_b6_main_factorized_f_product)))))))) -> (exists bqb_le_gap_b6_main_factorized_result. bqb_le_gap_b6_main_factorized_result + (n * A * B) = (F))

Proof neighborhood

Direct theorem prerequisites

BT00X0 floor_sqrt_factorized_threshold_thirty_two BT00R1 ceil_div_six_total BT00X3 bertrand_hj_envelope_thirty_two BT00RJ floor_ceil_division_budget BT00X4 bertrand_floor_power_product_le_h_from_total BT00X5 bertrand_four_power_product_le_of_sum_from_total BT001M mul_le_mul_right BT000F le_trans

Direct theorem dependents

BT00X7 bertrand_main_inequality_factorized

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

115 script commands · 23 reading checkpoints · 12 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (8)
floor sqrt factorized threshold thirty twoceil div six totalbertrand hj envelope thirty twofloor ceil division budgetbertrand floor power product le h from totalbertrand four power product le of sum from totalmul le mul rightle trans
01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro n
  2. L2
    intro s
  3. L3
    intro q
  4. L4
    intro r
  5. L5
    intro A
  6. L6
    intro B
  7. L7
    intro F
  8. L8
    intro htotal
  9. L9
    intro hthreshold
  10. L10
    intro hfloor
02Fix variables and assumptionsL11–14

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro hdiv
  2. L12
    intro hA
  3. L13
    intro hB
  4. L14
    intro hF
03Establish hsL15–20

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply floor sqrt factorized threshold thirty two.

  1. L15
  2. L16
    specialize floor_sqrt_factorized_threshold_thirty_two n
  3. L17
    specialize floor_sqrt_factorized_threshold_thirty_two s
  4. L18
    apply floor_sqrt_factorized_threshold_thirty_two
  5. L19
    exact hthreshold
  6. L20
    exact hfloor
04Establish he_existsL21–23

Establish this local claim before using it. It is not an additional assumption.

  1. L21
    have he_exists : ∃ e. CeilDivSix(s · s,e)Definitions: CeilDivSix(s · s,e)Original native command in the exact edition
  2. L22
    specialize ceil_div_six_total (s * s)
  3. L23
    exact ceil_div_six_total
05Separate the logical casesL24–24

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L24
    cases he_exists
06Establish hH_existsL25–28

Establish this local claim before using it. It is not an additional assumption.

  1. L25
    have hH_exists : ∃ H. Pow(s + 1,2 · s + 2,H)Definitions: Pow(s + 1,2 · s + 2,H)Original native command in the exact edition
  2. L26
    specialize htotal (s + 1)
  3. L27
    specialize htotal (2 * s + 2)
  4. L28
    exact htotal
07Separate the logical casesL29–29

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L29
    cases hH_exists
08Establish hU_existsL30–33

Establish this local claim before using it. It is not an additional assumption.

  1. L30
    have hU_exists : ∃ U. Pow(4,x,U)Definitions: Pow(4,x,U)Original native command in the exact edition
  2. L31
    specialize htotal 4
  3. L32
    specialize htotal x
  4. L33
    exact htotal
09Separate the logical casesL34–34

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L34
    cases hU_exists
10Establish hJ_existsL35–38

Establish this local claim before using it. It is not an additional assumption.

  1. L35
    have hJ_exists : ∃ J. Pow(s + 7,12,J)Definitions: Pow(s + 7,12,J)Original native command in the exact edition
  2. L36
    specialize htotal (s + 7)
  3. L37
    specialize htotal 12
  4. L38
    exact htotal
11Separate the logical casesL39–39

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L39
    cases hJ_exists
12Establish hG_existsL40–43

Establish this local claim before using it. It is not an additional assumption.

  1. L40
    have hG_exists : ∃ G. Pow(4,s + 5,G)Definitions: Pow(4,s + 5,G)Original native command in the exact edition
  2. L41
    specialize htotal 4
  3. L42
    specialize htotal (s + 5)
  4. L43
    exact htotal
13Separate the logical casesL44–44

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L44
    cases hG_exists
14Establish henvelopeL45–54

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bertrand hj envelope thirty two.

  1. L45
    have henvelope : Le(x1,x2) ∧ Le(x3,x4)Definitions: Le(x1,x2)Le(x3,x4)Original native command in the exact edition
  2. L46
    specialize bertrand_hj_envelope_thirty_two s
  3. L47
    specialize bertrand_hj_envelope_thirty_two x
  4. L48
    specialize bertrand_hj_envelope_thirty_two x1
  5. L49
    specialize bertrand_hj_envelope_thirty_two x2
  6. L50
    specialize bertrand_hj_envelope_thirty_two x3
  7. L51
    specialize bertrand_hj_envelope_thirty_two x4
  8. L52
    apply bertrand_hj_envelope_thirty_two
  9. L53
    exact hs
  10. L54
    exact he_exists_witness
15Use earlier factsL55–58

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L55
    exact hH_exists_witness
  2. L56
    exact hU_exists_witness
  3. L57
    exact hJ_exists_witness
  4. L58
    exact hG_exists_witness
16Separate the logical casesL59–59

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L59
    cases henvelope
17Establish hbudgetL60–69

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply floor ceil division budget.

  1. L60
    have hbudget : ∃ c. q + c = n ∧ Le(2 · n,6 · c) ∧ (Le(x,c) ∧ Le(q + x,n)) ∧ Lt(r,3)Definitions: Le(2 · n,6 · c)Le(x,c)Le(q + x,n)Lt(r,3)Original native command in the exact edition
  2. L61
    specialize floor_ceil_division_budget n
  3. L62
    specialize floor_ceil_division_budget q
  4. L63
    specialize floor_ceil_division_budget r
  5. L64
    specialize floor_ceil_division_budget s
  6. L65
    specialize floor_ceil_division_budget x
  7. L66
    apply floor_ceil_division_budget
  8. L67
    exact hfloor
  9. L68
    exact he_exists_witness
  10. L69
    exact hdiv
18Separate the logical casesL70–73

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L70
    cases hbudget
  2. L71
    cases hbudget_witness
  3. L72
    cases hbudget_witness_left
  4. L73
    cases hbudget_witness_left_right
19Establish hfloor_productL74–83

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bertrand floor power product le h from total.

  1. L74
    have hfloor_product : Le(n · A,x1)Definitions: Le(n · A,x1)Original native command in the exact edition
  2. L75
    specialize bertrand_floor_power_product_le_h_from_total n
  3. L76
    specialize bertrand_floor_power_product_le_h_from_total s
  4. L77
    specialize bertrand_floor_power_product_le_h_from_total A
  5. L78
    specialize bertrand_floor_power_product_le_h_from_total x1
  6. L79
    apply bertrand_floor_power_product_le_h_from_total
  7. L80
    exact htotal
  8. L81
    exact hfloor
  9. L82
    exact hA
  10. L83
    exact hH_exists_witness
20Establish hfloor_to_uL84–90

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le trans.

  1. L84
    have hfloor_to_u : Le(n · A,x2)Definitions: Le(n · A,x2)Original native command in the exact edition
  2. L85
    specialize le_trans (n * A)
  3. L86
    specialize le_trans x1
  4. L87
    specialize le_trans x2
  5. L88
    apply le_trans
  6. L89
    exact hfloor_product
  7. L90
    exact henvelope_left
21Establish hscaled_floorL91–96

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul le mul right.

  1. L91
    have hscaled_floor : Le(n · A · B,x2 · B)Definitions: Le(n · A · B,x2 · B)Original native command in the exact edition
  2. L92
    specialize mul_le_mul_right (n * A)
  3. L93
    specialize mul_le_mul_right x2
  4. L94
    specialize mul_le_mul_right B
  5. L95
    apply mul_le_mul_right
  6. L96
    exact hfloor_to_u
22Establish hubL97–106

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bertrand four power product le of sum from total.

  1. L97
  2. L98
    specialize bertrand_four_power_product_le_of_sum_from_total q
  3. L99
    specialize bertrand_four_power_product_le_of_sum_from_total x
  4. L100
    specialize bertrand_four_power_product_le_of_sum_from_total n
  5. L101
    specialize bertrand_four_power_product_le_of_sum_from_total B
  6. L102
    specialize bertrand_four_power_product_le_of_sum_from_total x2
  7. L103
    specialize bertrand_four_power_product_le_of_sum_from_total F
  8. L104
    apply bertrand_four_power_product_le_of_sum_from_total
  9. L105
    exact htotal
  10. L106
    exact hbudget_witness_left_right_right
23Use earlier factsL107–115

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L107
    exact hB
  2. L108
    exact hU_exists_witness
  3. L109
    exact hF
  4. L110
    specialize le_trans ((n * A) * B)
  5. L111
    specialize le_trans (x2 * B)
  6. L112
    specialize le_trans F
  7. L113
    apply le_trans
  8. L114
    exact hscaled_floor
  9. L115
    exact hub

Library-wide reading audit

Original defined command ledger · 115 lines
  1. 0001intro n
  2. 0002intro s
  3. 0003intro q
  4. 0004intro r
  5. 0005intro A
  6. 0006intro B
  7. 0007intro F
  8. 0008intro htotal
  9. 0009intro hthreshold
  10. 0010intro hfloor
  11. 0011intro hdiv
  12. 0012intro hA
  13. 0013intro hB
  14. 0014intro hF
  15. 0015have hs : Lt(31,s)
    Exact native replay linehave hs : exists bqb_le_gap_b6_main_root_lower. bqb_le_gap_b6_main_root_lower + (32) = (s)
  16. 0016specialize floor_sqrt_factorized_threshold_thirty_two n
  17. 0017specialize floor_sqrt_factorized_threshold_thirty_two s
  18. 0018apply floor_sqrt_factorized_threshold_thirty_two
  19. 0019exact hthreshold
  20. 0020exact hfloor
  21. 0021have he_exists : ∃ e. CeilDivSix(s · s,e)
    Exact native replay linehave he_exists : exists e. (((exists bcs_lower_gap_b6_main_ceiling. bcs_lower_gap_b6_main_ceiling + (s * s) = 6 * (e)) /\ exists bcs_upper_gap_b6_main_ceiling. bcs_upper_gap_b6_main_ceiling + S (6 * (e)) = (s * s) + 6))
  22. 0022specialize ceil_div_six_total (s * s)
  23. 0023exact ceil_div_six_total
  24. 0024cases he_exists
  25. 0025have hH_exists : ∃ H. Pow(s + 1,2 · s + 2,H)
    Exact native replay linehave hH_exists : exists H. (exists pa_b_b6_main_envelope_h pa_c_b6_main_envelope_h. ((forall pa_i_b6_main_envelope_h_repeat. (exists pa_lt_b6_main_envelope_h_repeat_bound. pa_lt_b6_main_envelope_h_repeat_bound + S pa_i_b6_main_envelope_h_repeat = 2 * s + 2) -> (((exists pa_h_b6_main_envelope_h_repeat_decoded. pa_h_b6_main_envelope_h_repeat_decoded + S (s + 1) = S ((S (pa_i_b6_main_envelope_h_repeat)) * pa_c_b6_main_envelope_h)) /\ exists pa_q_b6_main_envelope_h_repeat_decoded. pa_b_b6_main_envelope_h = pa_q_b6_main_envelope_h_repeat_decoded * S ((S (pa_i_b6_main_envelope_h_repeat)) * pa_c_b6_main_envelope_h) + (s + 1)))) /\ (exists pa_u_b6_main_envelope_h_product pa_v_b6_main_envelope_h_product. ((((exists pa_h_b6_main_envelope_h_product_start. pa_h_b6_main_envelope_h_product_start + S (1) = S ((S (0)) * pa_v_b6_main_envelope_h_product)) /\ exists pa_q_b6_main_envelope_h_product_start. pa_u_b6_main_envelope_h_product = pa_q_b6_main_envelope_h_product_start * S ((S (0)) * pa_v_b6_main_envelope_h_product) + (1))) /\ ((((exists pa_h_b6_main_envelope_h_product_terminal. pa_h_b6_main_envelope_h_product_terminal + S (H) = S ((S (2 * s + 2)) * pa_v_b6_main_envelope_h_product)) /\ exists pa_q_b6_main_envelope_h_product_terminal. pa_u_b6_main_envelope_h_product = pa_q_b6_main_envelope_h_product_terminal * S ((S (2 * s + 2)) * pa_v_b6_main_envelope_h_product) + (H))) /\ forall pa_i_b6_main_envelope_h_product. (exists pa_lt_b6_main_envelope_h_product_bound. pa_lt_b6_main_envelope_h_product_bound + S pa_i_b6_main_envelope_h_product = 2 * s + 2) -> exists pa_p_b6_main_envelope_h_product pa_r_b6_main_envelope_h_product pa_s_b6_main_envelope_h_product. ((((exists pa_h_b6_main_envelope_h_product_factor. pa_h_b6_main_envelope_h_product_factor + S (pa_p_b6_main_envelope_h_product) = S ((S (pa_i_b6_main_envelope_h_product)) * pa_c_b6_main_envelope_h)) /\ exists pa_q_b6_main_envelope_h_product_factor. pa_b_b6_main_envelope_h = pa_q_b6_main_envelope_h_product_factor * S ((S (pa_i_b6_main_envelope_h_product)) * pa_c_b6_main_envelope_h) + (pa_p_b6_main_envelope_h_product))) /\ ((((exists pa_h_b6_main_envelope_h_product_partial. pa_h_b6_main_envelope_h_product_partial + S (pa_r_b6_main_envelope_h_product) = S ((S (pa_i_b6_main_envelope_h_product)) * pa_v_b6_main_envelope_h_product)) /\ exists pa_q_b6_main_envelope_h_product_partial. pa_u_b6_main_envelope_h_product = pa_q_b6_main_envelope_h_product_partial * S ((S (pa_i_b6_main_envelope_h_product)) * pa_v_b6_main_envelope_h_product) + (pa_r_b6_main_envelope_h_product))) /\ ((((exists pa_h_b6_main_envelope_h_product_successor. pa_h_b6_main_envelope_h_product_successor + S (pa_s_b6_main_envelope_h_product) = S ((S (S pa_i_b6_main_envelope_h_product)) * pa_v_b6_main_envelope_h_product)) /\ exists pa_q_b6_main_envelope_h_product_successor. pa_u_b6_main_envelope_h_product = pa_q_b6_main_envelope_h_product_successor * S ((S (S pa_i_b6_main_envelope_h_product)) * pa_v_b6_main_envelope_h_product) + (pa_s_b6_main_envelope_h_product))) /\ pa_s_b6_main_envelope_h_product = pa_r_b6_main_envelope_h_product * pa_p_b6_main_envelope_h_product))))))))
  26. 0026specialize htotal (s + 1)
  27. 0027specialize htotal (2 * s + 2)
  28. 0028exact htotal
  29. 0029cases hH_exists
  30. 0030have hU_exists : ∃ U. Pow(4,x,U)
    Exact native replay linehave hU_exists : exists U. (exists pa_b_b6_main_envelope_u_witness pa_c_b6_main_envelope_u_witness. ((forall pa_i_b6_main_envelope_u_witness_repeat. (exists pa_lt_b6_main_envelope_u_witness_repeat_bound. pa_lt_b6_main_envelope_u_witness_repeat_bound + S pa_i_b6_main_envelope_u_witness_repeat = x) -> (((exists pa_h_b6_main_envelope_u_witness_repeat_decoded. pa_h_b6_main_envelope_u_witness_repeat_decoded + S (4) = S ((S (pa_i_b6_main_envelope_u_witness_repeat)) * pa_c_b6_main_envelope_u_witness)) /\ exists pa_q_b6_main_envelope_u_witness_repeat_decoded. pa_b_b6_main_envelope_u_witness = pa_q_b6_main_envelope_u_witness_repeat_decoded * S ((S (pa_i_b6_main_envelope_u_witness_repeat)) * pa_c_b6_main_envelope_u_witness) + (4)))) /\ (exists pa_u_b6_main_envelope_u_witness_product pa_v_b6_main_envelope_u_witness_product. ((((exists pa_h_b6_main_envelope_u_witness_product_start. pa_h_b6_main_envelope_u_witness_product_start + S (1) = S ((S (0)) * pa_v_b6_main_envelope_u_witness_product)) /\ exists pa_q_b6_main_envelope_u_witness_product_start. pa_u_b6_main_envelope_u_witness_product = pa_q_b6_main_envelope_u_witness_product_start * S ((S (0)) * pa_v_b6_main_envelope_u_witness_product) + (1))) /\ ((((exists pa_h_b6_main_envelope_u_witness_product_terminal. pa_h_b6_main_envelope_u_witness_product_terminal + S (U) = S ((S (x)) * pa_v_b6_main_envelope_u_witness_product)) /\ exists pa_q_b6_main_envelope_u_witness_product_terminal. pa_u_b6_main_envelope_u_witness_product = pa_q_b6_main_envelope_u_witness_product_terminal * S ((S (x)) * pa_v_b6_main_envelope_u_witness_product) + (U))) /\ forall pa_i_b6_main_envelope_u_witness_product. (exists pa_lt_b6_main_envelope_u_witness_product_bound. pa_lt_b6_main_envelope_u_witness_product_bound + S pa_i_b6_main_envelope_u_witness_product = x) -> exists pa_p_b6_main_envelope_u_witness_product pa_r_b6_main_envelope_u_witness_product pa_s_b6_main_envelope_u_witness_product. ((((exists pa_h_b6_main_envelope_u_witness_product_factor. pa_h_b6_main_envelope_u_witness_product_factor + S (pa_p_b6_main_envelope_u_witness_product) = S ((S (pa_i_b6_main_envelope_u_witness_product)) * pa_c_b6_main_envelope_u_witness)) /\ exists pa_q_b6_main_envelope_u_witness_product_factor. pa_b_b6_main_envelope_u_witness = pa_q_b6_main_envelope_u_witness_product_factor * S ((S (pa_i_b6_main_envelope_u_witness_product)) * pa_c_b6_main_envelope_u_witness) + (pa_p_b6_main_envelope_u_witness_product))) /\ ((((exists pa_h_b6_main_envelope_u_witness_product_partial. pa_h_b6_main_envelope_u_witness_product_partial + S (pa_r_b6_main_envelope_u_witness_product) = S ((S (pa_i_b6_main_envelope_u_witness_product)) * pa_v_b6_main_envelope_u_witness_product)) /\ exists pa_q_b6_main_envelope_u_witness_product_partial. pa_u_b6_main_envelope_u_witness_product = pa_q_b6_main_envelope_u_witness_product_partial * S ((S (pa_i_b6_main_envelope_u_witness_product)) * pa_v_b6_main_envelope_u_witness_product) + (pa_r_b6_main_envelope_u_witness_product))) /\ ((((exists pa_h_b6_main_envelope_u_witness_product_successor. pa_h_b6_main_envelope_u_witness_product_successor + S (pa_s_b6_main_envelope_u_witness_product) = S ((S (S pa_i_b6_main_envelope_u_witness_product)) * pa_v_b6_main_envelope_u_witness_product)) /\ exists pa_q_b6_main_envelope_u_witness_product_successor. pa_u_b6_main_envelope_u_witness_product = pa_q_b6_main_envelope_u_witness_product_successor * S ((S (S pa_i_b6_main_envelope_u_witness_product)) * pa_v_b6_main_envelope_u_witness_product) + (pa_s_b6_main_envelope_u_witness_product))) /\ pa_s_b6_main_envelope_u_witness_product = pa_r_b6_main_envelope_u_witness_product * pa_p_b6_main_envelope_u_witness_product))))))))
  31. 0031specialize htotal 4
  32. 0032specialize htotal x
  33. 0033exact htotal
  34. 0034cases hU_exists
  35. 0035have hJ_exists : ∃ J. Pow(s + 7,12,J)
    Exact native replay linehave hJ_exists : exists J. (exists pa_b_b6_main_envelope_j pa_c_b6_main_envelope_j. ((forall pa_i_b6_main_envelope_j_repeat. (exists pa_lt_b6_main_envelope_j_repeat_bound. pa_lt_b6_main_envelope_j_repeat_bound + S pa_i_b6_main_envelope_j_repeat = 12) -> (((exists pa_h_b6_main_envelope_j_repeat_decoded. pa_h_b6_main_envelope_j_repeat_decoded + S (s + 7) = S ((S (pa_i_b6_main_envelope_j_repeat)) * pa_c_b6_main_envelope_j)) /\ exists pa_q_b6_main_envelope_j_repeat_decoded. pa_b_b6_main_envelope_j = pa_q_b6_main_envelope_j_repeat_decoded * S ((S (pa_i_b6_main_envelope_j_repeat)) * pa_c_b6_main_envelope_j) + (s + 7)))) /\ (exists pa_u_b6_main_envelope_j_product pa_v_b6_main_envelope_j_product. ((((exists pa_h_b6_main_envelope_j_product_start. pa_h_b6_main_envelope_j_product_start + S (1) = S ((S (0)) * pa_v_b6_main_envelope_j_product)) /\ exists pa_q_b6_main_envelope_j_product_start. pa_u_b6_main_envelope_j_product = pa_q_b6_main_envelope_j_product_start * S ((S (0)) * pa_v_b6_main_envelope_j_product) + (1))) /\ ((((exists pa_h_b6_main_envelope_j_product_terminal. pa_h_b6_main_envelope_j_product_terminal + S (J) = S ((S (12)) * pa_v_b6_main_envelope_j_product)) /\ exists pa_q_b6_main_envelope_j_product_terminal. pa_u_b6_main_envelope_j_product = pa_q_b6_main_envelope_j_product_terminal * S ((S (12)) * pa_v_b6_main_envelope_j_product) + (J))) /\ forall pa_i_b6_main_envelope_j_product. (exists pa_lt_b6_main_envelope_j_product_bound. pa_lt_b6_main_envelope_j_product_bound + S pa_i_b6_main_envelope_j_product = 12) -> exists pa_p_b6_main_envelope_j_product pa_r_b6_main_envelope_j_product pa_s_b6_main_envelope_j_product. ((((exists pa_h_b6_main_envelope_j_product_factor. pa_h_b6_main_envelope_j_product_factor + S (pa_p_b6_main_envelope_j_product) = S ((S (pa_i_b6_main_envelope_j_product)) * pa_c_b6_main_envelope_j)) /\ exists pa_q_b6_main_envelope_j_product_factor. pa_b_b6_main_envelope_j = pa_q_b6_main_envelope_j_product_factor * S ((S (pa_i_b6_main_envelope_j_product)) * pa_c_b6_main_envelope_j) + (pa_p_b6_main_envelope_j_product))) /\ ((((exists pa_h_b6_main_envelope_j_product_partial. pa_h_b6_main_envelope_j_product_partial + S (pa_r_b6_main_envelope_j_product) = S ((S (pa_i_b6_main_envelope_j_product)) * pa_v_b6_main_envelope_j_product)) /\ exists pa_q_b6_main_envelope_j_product_partial. pa_u_b6_main_envelope_j_product = pa_q_b6_main_envelope_j_product_partial * S ((S (pa_i_b6_main_envelope_j_product)) * pa_v_b6_main_envelope_j_product) + (pa_r_b6_main_envelope_j_product))) /\ ((((exists pa_h_b6_main_envelope_j_product_successor. pa_h_b6_main_envelope_j_product_successor + S (pa_s_b6_main_envelope_j_product) = S ((S (S pa_i_b6_main_envelope_j_product)) * pa_v_b6_main_envelope_j_product)) /\ exists pa_q_b6_main_envelope_j_product_successor. pa_u_b6_main_envelope_j_product = pa_q_b6_main_envelope_j_product_successor * S ((S (S pa_i_b6_main_envelope_j_product)) * pa_v_b6_main_envelope_j_product) + (pa_s_b6_main_envelope_j_product))) /\ pa_s_b6_main_envelope_j_product = pa_r_b6_main_envelope_j_product * pa_p_b6_main_envelope_j_product))))))))
  36. 0036specialize htotal (s + 7)
  37. 0037specialize htotal 12
  38. 0038exact htotal
  39. 0039cases hJ_exists
  40. 0040have hG_exists : ∃ G. Pow(4,s + 5,G)
    Exact native replay linehave hG_exists : exists G. (exists pa_b_b6_main_envelope_g pa_c_b6_main_envelope_g. ((forall pa_i_b6_main_envelope_g_repeat. (exists pa_lt_b6_main_envelope_g_repeat_bound. pa_lt_b6_main_envelope_g_repeat_bound + S pa_i_b6_main_envelope_g_repeat = s + 5) -> (((exists pa_h_b6_main_envelope_g_repeat_decoded. pa_h_b6_main_envelope_g_repeat_decoded + S (4) = S ((S (pa_i_b6_main_envelope_g_repeat)) * pa_c_b6_main_envelope_g)) /\ exists pa_q_b6_main_envelope_g_repeat_decoded. pa_b_b6_main_envelope_g = pa_q_b6_main_envelope_g_repeat_decoded * S ((S (pa_i_b6_main_envelope_g_repeat)) * pa_c_b6_main_envelope_g) + (4)))) /\ (exists pa_u_b6_main_envelope_g_product pa_v_b6_main_envelope_g_product. ((((exists pa_h_b6_main_envelope_g_product_start. pa_h_b6_main_envelope_g_product_start + S (1) = S ((S (0)) * pa_v_b6_main_envelope_g_product)) /\ exists pa_q_b6_main_envelope_g_product_start. pa_u_b6_main_envelope_g_product = pa_q_b6_main_envelope_g_product_start * S ((S (0)) * pa_v_b6_main_envelope_g_product) + (1))) /\ ((((exists pa_h_b6_main_envelope_g_product_terminal. pa_h_b6_main_envelope_g_product_terminal + S (G) = S ((S (s + 5)) * pa_v_b6_main_envelope_g_product)) /\ exists pa_q_b6_main_envelope_g_product_terminal. pa_u_b6_main_envelope_g_product = pa_q_b6_main_envelope_g_product_terminal * S ((S (s + 5)) * pa_v_b6_main_envelope_g_product) + (G))) /\ forall pa_i_b6_main_envelope_g_product. (exists pa_lt_b6_main_envelope_g_product_bound. pa_lt_b6_main_envelope_g_product_bound + S pa_i_b6_main_envelope_g_product = s + 5) -> exists pa_p_b6_main_envelope_g_product pa_r_b6_main_envelope_g_product pa_s_b6_main_envelope_g_product. ((((exists pa_h_b6_main_envelope_g_product_factor. pa_h_b6_main_envelope_g_product_factor + S (pa_p_b6_main_envelope_g_product) = S ((S (pa_i_b6_main_envelope_g_product)) * pa_c_b6_main_envelope_g)) /\ exists pa_q_b6_main_envelope_g_product_factor. pa_b_b6_main_envelope_g = pa_q_b6_main_envelope_g_product_factor * S ((S (pa_i_b6_main_envelope_g_product)) * pa_c_b6_main_envelope_g) + (pa_p_b6_main_envelope_g_product))) /\ ((((exists pa_h_b6_main_envelope_g_product_partial. pa_h_b6_main_envelope_g_product_partial + S (pa_r_b6_main_envelope_g_product) = S ((S (pa_i_b6_main_envelope_g_product)) * pa_v_b6_main_envelope_g_product)) /\ exists pa_q_b6_main_envelope_g_product_partial. pa_u_b6_main_envelope_g_product = pa_q_b6_main_envelope_g_product_partial * S ((S (pa_i_b6_main_envelope_g_product)) * pa_v_b6_main_envelope_g_product) + (pa_r_b6_main_envelope_g_product))) /\ ((((exists pa_h_b6_main_envelope_g_product_successor. pa_h_b6_main_envelope_g_product_successor + S (pa_s_b6_main_envelope_g_product) = S ((S (S pa_i_b6_main_envelope_g_product)) * pa_v_b6_main_envelope_g_product)) /\ exists pa_q_b6_main_envelope_g_product_successor. pa_u_b6_main_envelope_g_product = pa_q_b6_main_envelope_g_product_successor * S ((S (S pa_i_b6_main_envelope_g_product)) * pa_v_b6_main_envelope_g_product) + (pa_s_b6_main_envelope_g_product))) /\ pa_s_b6_main_envelope_g_product = pa_r_b6_main_envelope_g_product * pa_p_b6_main_envelope_g_product))))))))
  41. 0041specialize htotal 4
  42. 0042specialize htotal (s + 5)
  43. 0043exact htotal
  44. 0044cases hG_exists
  45. 0045have henvelope : Le(x1,x2) ∧ Le(x3,x4)
    Exact native replay linehave henvelope : ((exists bqb_le_gap_b6_main_h_u_order. bqb_le_gap_b6_main_h_u_order + (x1) = (x2)) /\ (exists bqb_le_gap_b6_main_j_g_order. bqb_le_gap_b6_main_j_g_order + (x3) = (x4)))
  46. 0046specialize bertrand_hj_envelope_thirty_two s
  47. 0047specialize bertrand_hj_envelope_thirty_two x
  48. 0048specialize bertrand_hj_envelope_thirty_two x1
  49. 0049specialize bertrand_hj_envelope_thirty_two x2
  50. 0050specialize bertrand_hj_envelope_thirty_two x3
  51. 0051specialize bertrand_hj_envelope_thirty_two x4
  52. 0052apply bertrand_hj_envelope_thirty_two
  53. 0053exact hs
  54. 0054exact he_exists_witness
  55. 0055exact hH_exists_witness
  56. 0056exact hU_exists_witness
  57. 0057exact hJ_exists_witness
  58. 0058exact hG_exists_witness
  59. 0059cases henvelope
  60. 0060have hbudget : ∃ c. q + c = n ∧ Le(2 · n,6 · c) ∧ (Le(x,c) ∧ Le(q + x,n)) ∧ Lt(r,3)
    Exact native replay linehave hbudget : exists c. ((((((q) + (c) = (n)) /\ exists bqb_budget_gap_b6_main_budget_data. bqb_budget_gap_b6_main_budget_data + 2 * (n) = 6 * (c))) /\ (((exists bqb_le_gap_b6_main_budget_ec_witness. bqb_le_gap_b6_main_budget_ec_witness + (x) = (c)) /\ (exists bqb_le_gap_b6_main_budget_sum_witness. bqb_le_gap_b6_main_budget_sum_witness + (q + x) = (n))))) /\ exists bmi_remainder_gap_b6_main_budget_preserved. bmi_remainder_gap_b6_main_budget_preserved + S r = 3)
  61. 0061specialize floor_ceil_division_budget n
  62. 0062specialize floor_ceil_division_budget q
  63. 0063specialize floor_ceil_division_budget r
  64. 0064specialize floor_ceil_division_budget s
  65. 0065specialize floor_ceil_division_budget x
  66. 0066apply floor_ceil_division_budget
  67. 0067exact hfloor
  68. 0068exact he_exists_witness
  69. 0069exact hdiv
  70. 0070cases hbudget
  71. 0071cases hbudget_witness
  72. 0072cases hbudget_witness_left
  73. 0073cases hbudget_witness_left_right
  74. 0074have hfloor_product : Le(n · A,x1)
    Exact native replay linehave hfloor_product : exists bqb_le_gap_b6_main_floor_product_order. bqb_le_gap_b6_main_floor_product_order + (n * A) = (x1)
  75. 0075specialize bertrand_floor_power_product_le_h_from_total n
  76. 0076specialize bertrand_floor_power_product_le_h_from_total s
  77. 0077specialize bertrand_floor_power_product_le_h_from_total A
  78. 0078specialize bertrand_floor_power_product_le_h_from_total x1
  79. 0079apply bertrand_floor_power_product_le_h_from_total
  80. 0080exact htotal
  81. 0081exact hfloor
  82. 0082exact hA
  83. 0083exact hH_exists_witness
  84. 0084have hfloor_to_u : Le(n · A,x2)
    Exact native replay linehave hfloor_to_u : exists bqb_le_gap_b6_main_floor_to_u_order. bqb_le_gap_b6_main_floor_to_u_order + (n * A) = (x2)
  85. 0085specialize le_trans (n * A)
  86. 0086specialize le_trans x1
  87. 0087specialize le_trans x2
  88. 0088apply le_trans
  89. 0089exact hfloor_product
  90. 0090exact henvelope_left
  91. 0091have hscaled_floor : Le(n · A · B,x2 · B)
    Exact native replay linehave hscaled_floor : exists bqb_le_gap_b6_main_scaled_floor_order. bqb_le_gap_b6_main_scaled_floor_order + ((n * A) * B) = (x2 * B)
  92. 0092specialize mul_le_mul_right (n * A)
  93. 0093specialize mul_le_mul_right x2
  94. 0094specialize mul_le_mul_right B
  95. 0095apply mul_le_mul_right
  96. 0096exact hfloor_to_u
  97. 0097have hub : Le(x2 · B,F)
    Exact native replay linehave hub : exists bqb_le_gap_b6_main_u_b_order. bqb_le_gap_b6_main_u_b_order + (x2 * B) = (F)
  98. 0098specialize bertrand_four_power_product_le_of_sum_from_total q
  99. 0099specialize bertrand_four_power_product_le_of_sum_from_total x
  100. 0100specialize bertrand_four_power_product_le_of_sum_from_total n
  101. 0101specialize bertrand_four_power_product_le_of_sum_from_total B
  102. 0102specialize bertrand_four_power_product_le_of_sum_from_total x2
  103. 0103specialize bertrand_four_power_product_le_of_sum_from_total F
  104. 0104apply bertrand_four_power_product_le_of_sum_from_total
  105. 0105exact htotal
  106. 0106exact hbudget_witness_left_right_right
  107. 0107exact hB
  108. 0108exact hU_exists_witness
  109. 0109exact hF
  110. 0110specialize le_trans ((n * A) * B)
  111. 0111specialize le_trans (x2 * B)
  112. 0112specialize le_trans F
  113. 0113apply le_trans
  114. 0114exact hscaled_floor
  115. 0115exact hub