BT00WJ · Bertrand theorem

pow_two_successor_double_le_pow_four_successor_from_total

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

An odd power of two is bounded by the next power of four.

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

∀ k. ∀ x. ∀ y. (∀ z. ∀ n. ∃ m. Pow(z,n,m)) → Pow(2,2 · k + 1,x) → Pow(4,k + 1,y) → Le(x,y)

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 PD0020 Pow

4 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0020 Pow

8 occurrences

Exact expanded native-PA statement
forall k x y. (forall bpt_a_hj32_two_odd bpt_e_hj32_two_odd. exists bpt_x_hj32_two_odd. (exists ff_b_bpt_value_hj32_two_odd ff_c_bpt_value_hj32_two_odd. ((forall ff_i_bpt_value_hj32_two_odd_repeat. (exists ff_lt_bpt_value_hj32_two_odd_repeat_bound. ff_lt_bpt_value_hj32_two_odd_repeat_bound + S ff_i_bpt_value_hj32_two_odd_repeat = bpt_e_hj32_two_odd) -> (((exists ff_h_bpt_value_hj32_two_odd_repeat_decoded. ff_h_bpt_value_hj32_two_odd_repeat_decoded + S (bpt_a_hj32_two_odd) = S ((S (ff_i_bpt_value_hj32_two_odd_repeat)) * ff_c_bpt_value_hj32_two_odd)) /\ exists ff_q_bpt_value_hj32_two_odd_repeat_decoded. ff_b_bpt_value_hj32_two_odd = ff_q_bpt_value_hj32_two_odd_repeat_decoded * S ((S (ff_i_bpt_value_hj32_two_odd_repeat)) * ff_c_bpt_value_hj32_two_odd) + (bpt_a_hj32_two_odd)))) /\ (exists ff_u_bpt_value_hj32_two_odd_product ff_v_bpt_value_hj32_two_odd_product. ((((exists ff_h_bpt_value_hj32_two_odd_product_start. ff_h_bpt_value_hj32_two_odd_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_hj32_two_odd_product)) /\ exists ff_q_bpt_value_hj32_two_odd_product_start. ff_u_bpt_value_hj32_two_odd_product = ff_q_bpt_value_hj32_two_odd_product_start * S ((S (0)) * ff_v_bpt_value_hj32_two_odd_product) + (1))) /\ ((((exists ff_h_bpt_value_hj32_two_odd_product_terminal. ff_h_bpt_value_hj32_two_odd_product_terminal + S (bpt_x_hj32_two_odd) = S ((S (bpt_e_hj32_two_odd)) * ff_v_bpt_value_hj32_two_odd_product)) /\ exists ff_q_bpt_value_hj32_two_odd_product_terminal. ff_u_bpt_value_hj32_two_odd_product = ff_q_bpt_value_hj32_two_odd_product_terminal * S ((S (bpt_e_hj32_two_odd)) * ff_v_bpt_value_hj32_two_odd_product) + (bpt_x_hj32_two_odd))) /\ forall ff_i_bpt_value_hj32_two_odd_product. (exists ff_lt_bpt_value_hj32_two_odd_product_bound. ff_lt_bpt_value_hj32_two_odd_product_bound + S ff_i_bpt_value_hj32_two_odd_product = bpt_e_hj32_two_odd) -> exists ff_p_bpt_value_hj32_two_odd_product ff_r_bpt_value_hj32_two_odd_product ff_s_bpt_value_hj32_two_odd_product. ((((exists ff_h_bpt_value_hj32_two_odd_product_factor. ff_h_bpt_value_hj32_two_odd_product_factor + S (ff_p_bpt_value_hj32_two_odd_product) = S ((S (ff_i_bpt_value_hj32_two_odd_product)) * ff_c_bpt_value_hj32_two_odd)) /\ exists ff_q_bpt_value_hj32_two_odd_product_factor. ff_b_bpt_value_hj32_two_odd = ff_q_bpt_value_hj32_two_odd_product_factor * S ((S (ff_i_bpt_value_hj32_two_odd_product)) * ff_c_bpt_value_hj32_two_odd) + (ff_p_bpt_value_hj32_two_odd_product))) /\ ((((exists ff_h_bpt_value_hj32_two_odd_product_partial. ff_h_bpt_value_hj32_two_odd_product_partial + S (ff_r_bpt_value_hj32_two_odd_product) = S ((S (ff_i_bpt_value_hj32_two_odd_product)) * ff_v_bpt_value_hj32_two_odd_product)) /\ exists ff_q_bpt_value_hj32_two_odd_product_partial. ff_u_bpt_value_hj32_two_odd_product = ff_q_bpt_value_hj32_two_odd_product_partial * S ((S (ff_i_bpt_value_hj32_two_odd_product)) * ff_v_bpt_value_hj32_two_odd_product) + (ff_r_bpt_value_hj32_two_odd_product))) /\ ((((exists ff_h_bpt_value_hj32_two_odd_product_successor. ff_h_bpt_value_hj32_two_odd_product_successor + S (ff_s_bpt_value_hj32_two_odd_product) = S ((S (S ff_i_bpt_value_hj32_two_odd_product)) * ff_v_bpt_value_hj32_two_odd_product)) /\ exists ff_q_bpt_value_hj32_two_odd_product_successor. ff_u_bpt_value_hj32_two_odd_product = ff_q_bpt_value_hj32_two_odd_product_successor * S ((S (S ff_i_bpt_value_hj32_two_odd_product)) * ff_v_bpt_value_hj32_two_odd_product) + (ff_s_bpt_value_hj32_two_odd_product))) /\ ff_s_bpt_value_hj32_two_odd_product = ff_r_bpt_value_hj32_two_odd_product * ff_p_bpt_value_hj32_two_odd_product))))))))) -> (exists pa_b_hj32_two_odd_left pa_c_hj32_two_odd_left. ((forall pa_i_hj32_two_odd_left_repeat. (exists pa_lt_hj32_two_odd_left_repeat_bound. pa_lt_hj32_two_odd_left_repeat_bound + S pa_i_hj32_two_odd_left_repeat = 2 * k + 1) -> (((exists pa_h_hj32_two_odd_left_repeat_decoded. pa_h_hj32_two_odd_left_repeat_decoded + S (2) = S ((S (pa_i_hj32_two_odd_left_repeat)) * pa_c_hj32_two_odd_left)) /\ exists pa_q_hj32_two_odd_left_repeat_decoded. pa_b_hj32_two_odd_left = pa_q_hj32_two_odd_left_repeat_decoded * S ((S (pa_i_hj32_two_odd_left_repeat)) * pa_c_hj32_two_odd_left) + (2)))) /\ (exists pa_u_hj32_two_odd_left_product pa_v_hj32_two_odd_left_product. ((((exists pa_h_hj32_two_odd_left_product_start. pa_h_hj32_two_odd_left_product_start + S (1) = S ((S (0)) * pa_v_hj32_two_odd_left_product)) /\ exists pa_q_hj32_two_odd_left_product_start. pa_u_hj32_two_odd_left_product = pa_q_hj32_two_odd_left_product_start * S ((S (0)) * pa_v_hj32_two_odd_left_product) + (1))) /\ ((((exists pa_h_hj32_two_odd_left_product_terminal. pa_h_hj32_two_odd_left_product_terminal + S (x) = S ((S (2 * k + 1)) * pa_v_hj32_two_odd_left_product)) /\ exists pa_q_hj32_two_odd_left_product_terminal. pa_u_hj32_two_odd_left_product = pa_q_hj32_two_odd_left_product_terminal * S ((S (2 * k + 1)) * pa_v_hj32_two_odd_left_product) + (x))) /\ forall pa_i_hj32_two_odd_left_product. (exists pa_lt_hj32_two_odd_left_product_bound. pa_lt_hj32_two_odd_left_product_bound + S pa_i_hj32_two_odd_left_product = 2 * k + 1) -> exists pa_p_hj32_two_odd_left_product pa_r_hj32_two_odd_left_product pa_s_hj32_two_odd_left_product. ((((exists pa_h_hj32_two_odd_left_product_factor. pa_h_hj32_two_odd_left_product_factor + S (pa_p_hj32_two_odd_left_product) = S ((S (pa_i_hj32_two_odd_left_product)) * pa_c_hj32_two_odd_left)) /\ exists pa_q_hj32_two_odd_left_product_factor. pa_b_hj32_two_odd_left = pa_q_hj32_two_odd_left_product_factor * S ((S (pa_i_hj32_two_odd_left_product)) * pa_c_hj32_two_odd_left) + (pa_p_hj32_two_odd_left_product))) /\ ((((exists pa_h_hj32_two_odd_left_product_partial. pa_h_hj32_two_odd_left_product_partial + S (pa_r_hj32_two_odd_left_product) = S ((S (pa_i_hj32_two_odd_left_product)) * pa_v_hj32_two_odd_left_product)) /\ exists pa_q_hj32_two_odd_left_product_partial. pa_u_hj32_two_odd_left_product = pa_q_hj32_two_odd_left_product_partial * S ((S (pa_i_hj32_two_odd_left_product)) * pa_v_hj32_two_odd_left_product) + (pa_r_hj32_two_odd_left_product))) /\ ((((exists pa_h_hj32_two_odd_left_product_successor. pa_h_hj32_two_odd_left_product_successor + S (pa_s_hj32_two_odd_left_product) = S ((S (S pa_i_hj32_two_odd_left_product)) * pa_v_hj32_two_odd_left_product)) /\ exists pa_q_hj32_two_odd_left_product_successor. pa_u_hj32_two_odd_left_product = pa_q_hj32_two_odd_left_product_successor * S ((S (S pa_i_hj32_two_odd_left_product)) * pa_v_hj32_two_odd_left_product) + (pa_s_hj32_two_odd_left_product))) /\ pa_s_hj32_two_odd_left_product = pa_r_hj32_two_odd_left_product * pa_p_hj32_two_odd_left_product)))))))) -> (exists pa_b_hj32_two_odd_right pa_c_hj32_two_odd_right. ((forall pa_i_hj32_two_odd_right_repeat. (exists pa_lt_hj32_two_odd_right_repeat_bound. pa_lt_hj32_two_odd_right_repeat_bound + S pa_i_hj32_two_odd_right_repeat = k + 1) -> (((exists pa_h_hj32_two_odd_right_repeat_decoded. pa_h_hj32_two_odd_right_repeat_decoded + S (4) = S ((S (pa_i_hj32_two_odd_right_repeat)) * pa_c_hj32_two_odd_right)) /\ exists pa_q_hj32_two_odd_right_repeat_decoded. pa_b_hj32_two_odd_right = pa_q_hj32_two_odd_right_repeat_decoded * S ((S (pa_i_hj32_two_odd_right_repeat)) * pa_c_hj32_two_odd_right) + (4)))) /\ (exists pa_u_hj32_two_odd_right_product pa_v_hj32_two_odd_right_product. ((((exists pa_h_hj32_two_odd_right_product_start. pa_h_hj32_two_odd_right_product_start + S (1) = S ((S (0)) * pa_v_hj32_two_odd_right_product)) /\ exists pa_q_hj32_two_odd_right_product_start. pa_u_hj32_two_odd_right_product = pa_q_hj32_two_odd_right_product_start * S ((S (0)) * pa_v_hj32_two_odd_right_product) + (1))) /\ ((((exists pa_h_hj32_two_odd_right_product_terminal. pa_h_hj32_two_odd_right_product_terminal + S (y) = S ((S (k + 1)) * pa_v_hj32_two_odd_right_product)) /\ exists pa_q_hj32_two_odd_right_product_terminal. pa_u_hj32_two_odd_right_product = pa_q_hj32_two_odd_right_product_terminal * S ((S (k + 1)) * pa_v_hj32_two_odd_right_product) + (y))) /\ forall pa_i_hj32_two_odd_right_product. (exists pa_lt_hj32_two_odd_right_product_bound. pa_lt_hj32_two_odd_right_product_bound + S pa_i_hj32_two_odd_right_product = k + 1) -> exists pa_p_hj32_two_odd_right_product pa_r_hj32_two_odd_right_product pa_s_hj32_two_odd_right_product. ((((exists pa_h_hj32_two_odd_right_product_factor. pa_h_hj32_two_odd_right_product_factor + S (pa_p_hj32_two_odd_right_product) = S ((S (pa_i_hj32_two_odd_right_product)) * pa_c_hj32_two_odd_right)) /\ exists pa_q_hj32_two_odd_right_product_factor. pa_b_hj32_two_odd_right = pa_q_hj32_two_odd_right_product_factor * S ((S (pa_i_hj32_two_odd_right_product)) * pa_c_hj32_two_odd_right) + (pa_p_hj32_two_odd_right_product))) /\ ((((exists pa_h_hj32_two_odd_right_product_partial. pa_h_hj32_two_odd_right_product_partial + S (pa_r_hj32_two_odd_right_product) = S ((S (pa_i_hj32_two_odd_right_product)) * pa_v_hj32_two_odd_right_product)) /\ exists pa_q_hj32_two_odd_right_product_partial. pa_u_hj32_two_odd_right_product = pa_q_hj32_two_odd_right_product_partial * S ((S (pa_i_hj32_two_odd_right_product)) * pa_v_hj32_two_odd_right_product) + (pa_r_hj32_two_odd_right_product))) /\ ((((exists pa_h_hj32_two_odd_right_product_successor. pa_h_hj32_two_odd_right_product_successor + S (pa_s_hj32_two_odd_right_product) = S ((S (S pa_i_hj32_two_odd_right_product)) * pa_v_hj32_two_odd_right_product)) /\ exists pa_q_hj32_two_odd_right_product_successor. pa_u_hj32_two_odd_right_product = pa_q_hj32_two_odd_right_product_successor * S ((S (S pa_i_hj32_two_odd_right_product)) * pa_v_hj32_two_odd_right_product) + (pa_s_hj32_two_odd_right_product))) /\ pa_s_hj32_two_odd_right_product = pa_r_hj32_two_odd_right_product * pa_p_hj32_two_odd_right_product)))))))) -> (exists bqb_le_gap_hj32_two_odd_result. bqb_le_gap_hj32_two_odd_result + (x) = (y))

Proof neighborhood

Direct theorem prerequisites

BT00WI pow_two_double_eq_pow_four_from_total BT00PY pow_base_monotone BT009X pow_add BT00PV mul_le_mul BT000E le_refl

Direct theorem dependents

BT00WM pow_eleven_double_block_le_pow_four_odd_from_total

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

88 script commands · 21 reading checkpoints · 11 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 (5)
pow two double eq pow four from totalpow base monotonepow addmul le mulle refl
01Fix variables and assumptionsL1–6

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

  1. L1
    intro k
  2. L2
    intro x
  3. L3
    intro y
  4. L4
    intro htotal
  5. L5
    intro hx
  6. L6
    intro hy
02Establish to_p2_evenL7–10

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

  1. L7
    have to_p2_even : ∃ hj32_local_value_to_p2_even. Pow(2,2 · k,hj32_local_value_to_p2_even)Definitions: Pow(2,2 · k,hj32_local_value_to_p2_even)Original native command in the exact edition
  2. L8
    specialize htotal 2
  3. L9
    specialize htotal 2 * k
  4. L10
    exact htotal
03Separate the logical casesL11–11

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

  1. L11
    cases to_p2_even
04Establish to_p2_oneL12–15

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

  1. L12
    have to_p2_one : ∃ hj32_local_value_to_p2_one. Pow(2,1,hj32_local_value_to_p2_one)Definitions: Pow(2,1,hj32_local_value_to_p2_one)Original native command in the exact edition
  2. L13
    specialize htotal 2
  3. L14
    specialize htotal 1
  4. L15
    exact htotal
05Separate the logical casesL16–16

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

  1. L16
    cases to_p2_one
06Establish to_p4_evenL17–20

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

  1. L17
    have to_p4_even : ∃ hj32_local_value_to_p4_even. Pow(4,k,hj32_local_value_to_p4_even)Definitions: Pow(4,k,hj32_local_value_to_p4_even)Original native command in the exact edition
  2. L18
    specialize htotal 4
  3. L19
    specialize htotal k
  4. L20
    exact htotal
07Separate the logical casesL21–21

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

  1. L21
    cases to_p4_even
08Establish to_p4_oneL22–25

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

  1. L22
    have to_p4_one : ∃ hj32_local_value_to_p4_one. Pow(4,1,hj32_local_value_to_p4_one)Definitions: Pow(4,1,hj32_local_value_to_p4_one)Original native command in the exact edition
  2. L23
    specialize htotal 4
  3. L24
    specialize htotal 1
  4. L25
    exact htotal
09Separate the logical casesL26–26

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

  1. L26
    cases to_p4_one
10Establish to_even_eqL27–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow two double eq pow four from total.

  1. L27
    have to_even_eq : x1 = x3
  2. L28
    specialize pow_two_double_eq_pow_four_from_total k
  3. L29
    specialize pow_two_double_eq_pow_four_from_total x1
  4. L30
    specialize pow_two_double_eq_pow_four_from_total x3
  5. L31
    apply pow_two_double_eq_pow_four_from_total
  6. L32
    exact htotal
  7. L33
    exact to_p2_even_witness
  8. L34
    exact to_p4_even_witness
11Establish to_even_boundL35–38

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

  1. L35
    have to_even_bound : Le(x1,x3)Definitions: Le(x1,x3)Original native command in the exact edition
  2. L36
    rewrite to_even_eq
  3. L37
    specialize le_refl x3
  4. L38
    exact le_refl
12Establish to_baseL39–39

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

  1. L39
    have to_base : Lt(1,4)Definitions: Lt(1,4)Original native command in the exact edition
13Construct an explicit witnessL40–40

Supply the displayed value, then prove that it has the required property.

  1. L40
    exists 2
14Calculate and transport equalitiesL41–41

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L41
    norm_num
15Establish to_one_boundL42–51

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow base monotone.

  1. L42
    have to_one_bound : Le(x2,x4)Definitions: Le(x2,x4)Original native command in the exact edition
  2. L43
    specialize pow_base_monotone 2
  3. L44
    specialize pow_base_monotone 4
  4. L45
    specialize pow_base_monotone 1
  5. L46
    specialize pow_base_monotone x2
  6. L47
    specialize pow_base_monotone x4
  7. L48
    apply pow_base_monotone
  8. L49
    exact to_base
  9. L50
    exact to_p2_one_witness
  10. L51
    exact to_p4_one_witness
16Establish to_left_productL52–61

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

  1. L52
    have to_left_product : x = x1 * x2
  2. L53
    specialize pow_add 2
  3. L54
    specialize pow_add 2 * k
  4. L55
    specialize pow_add 1
  5. L56
    specialize pow_add 2 * k + 1
  6. L57
    specialize pow_add x1
  7. L58
    specialize pow_add x2
  8. L59
    specialize pow_add x
  9. L60
    apply pow_add
  10. L61
    refl
17Use earlier factsL62–64

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

  1. L62
    exact to_p2_even_witness
  2. L63
    exact to_p2_one_witness
  3. L64
    exact hx
18Establish to_right_productL65–74

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

  1. L65
    have to_right_product : y = x3 * x4
  2. L66
    specialize pow_add 4
  3. L67
    specialize pow_add k
  4. L68
    specialize pow_add 1
  5. L69
    specialize pow_add k + 1
  6. L70
    specialize pow_add x3
  7. L71
    specialize pow_add x4
  8. L72
    specialize pow_add y
  9. L73
    apply pow_add
  10. L74
    refl
19Use earlier factsL75–77

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

  1. L75
    exact to_p4_even_witness
  2. L76
    exact to_p4_one_witness
  3. L77
    exact hy
20Establish to_resultL78–87

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

  1. L78
    have to_result : Le(x1 · x2,x3 · x4)Definitions: Le(x1 · x2,x3 · x4)Original native command in the exact edition
  2. L79
    specialize mul_le_mul x1
  3. L80
    specialize mul_le_mul x3
  4. L81
    specialize mul_le_mul x2
  5. L82
    specialize mul_le_mul x4
  6. L83
    apply mul_le_mul
  7. L84
    exact to_even_bound
  8. L85
    exact to_one_bound
  9. L86
    rewrite <- to_left_product at to_result
  10. L87
    rewrite <- to_right_product at to_result
21Use earlier factsL88–88

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

  1. L88
    exact to_result

Library-wide reading audit

Original defined command ledger · 88 lines
  1. 0001intro k
  2. 0002intro x
  3. 0003intro y
  4. 0004intro htotal
  5. 0005intro hx
  6. 0006intro hy
  7. 0007have to_p2_even : ∃ hj32_local_value_to_p2_even. Pow(2,2 · k,hj32_local_value_to_p2_even)
    Exact native replay linehave to_p2_even : exists hj32_local_value_to_p2_even. (exists pa_b_hj32_local_total_to_p2_even pa_c_hj32_local_total_to_p2_even. ((forall pa_i_hj32_local_total_to_p2_even_repeat. (exists pa_lt_hj32_local_total_to_p2_even_repeat_bound. pa_lt_hj32_local_total_to_p2_even_repeat_bound + S pa_i_hj32_local_total_to_p2_even_repeat = 2 * k) -> (((exists pa_h_hj32_local_total_to_p2_even_repeat_decoded. pa_h_hj32_local_total_to_p2_even_repeat_decoded + S (2) = S ((S (pa_i_hj32_local_total_to_p2_even_repeat)) * pa_c_hj32_local_total_to_p2_even)) /\ exists pa_q_hj32_local_total_to_p2_even_repeat_decoded. pa_b_hj32_local_total_to_p2_even = pa_q_hj32_local_total_to_p2_even_repeat_decoded * S ((S (pa_i_hj32_local_total_to_p2_even_repeat)) * pa_c_hj32_local_total_to_p2_even) + (2)))) /\ (exists pa_u_hj32_local_total_to_p2_even_product pa_v_hj32_local_total_to_p2_even_product. ((((exists pa_h_hj32_local_total_to_p2_even_product_start. pa_h_hj32_local_total_to_p2_even_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_to_p2_even_product)) /\ exists pa_q_hj32_local_total_to_p2_even_product_start. pa_u_hj32_local_total_to_p2_even_product = pa_q_hj32_local_total_to_p2_even_product_start * S ((S (0)) * pa_v_hj32_local_total_to_p2_even_product) + (1))) /\ ((((exists pa_h_hj32_local_total_to_p2_even_product_terminal. pa_h_hj32_local_total_to_p2_even_product_terminal + S (hj32_local_value_to_p2_even) = S ((S (2 * k)) * pa_v_hj32_local_total_to_p2_even_product)) /\ exists pa_q_hj32_local_total_to_p2_even_product_terminal. pa_u_hj32_local_total_to_p2_even_product = pa_q_hj32_local_total_to_p2_even_product_terminal * S ((S (2 * k)) * pa_v_hj32_local_total_to_p2_even_product) + (hj32_local_value_to_p2_even))) /\ forall pa_i_hj32_local_total_to_p2_even_product. (exists pa_lt_hj32_local_total_to_p2_even_product_bound. pa_lt_hj32_local_total_to_p2_even_product_bound + S pa_i_hj32_local_total_to_p2_even_product = 2 * k) -> exists pa_p_hj32_local_total_to_p2_even_product pa_r_hj32_local_total_to_p2_even_product pa_s_hj32_local_total_to_p2_even_product. ((((exists pa_h_hj32_local_total_to_p2_even_product_factor. pa_h_hj32_local_total_to_p2_even_product_factor + S (pa_p_hj32_local_total_to_p2_even_product) = S ((S (pa_i_hj32_local_total_to_p2_even_product)) * pa_c_hj32_local_total_to_p2_even)) /\ exists pa_q_hj32_local_total_to_p2_even_product_factor. pa_b_hj32_local_total_to_p2_even = pa_q_hj32_local_total_to_p2_even_product_factor * S ((S (pa_i_hj32_local_total_to_p2_even_product)) * pa_c_hj32_local_total_to_p2_even) + (pa_p_hj32_local_total_to_p2_even_product))) /\ ((((exists pa_h_hj32_local_total_to_p2_even_product_partial. pa_h_hj32_local_total_to_p2_even_product_partial + S (pa_r_hj32_local_total_to_p2_even_product) = S ((S (pa_i_hj32_local_total_to_p2_even_product)) * pa_v_hj32_local_total_to_p2_even_product)) /\ exists pa_q_hj32_local_total_to_p2_even_product_partial. pa_u_hj32_local_total_to_p2_even_product = pa_q_hj32_local_total_to_p2_even_product_partial * S ((S (pa_i_hj32_local_total_to_p2_even_product)) * pa_v_hj32_local_total_to_p2_even_product) + (pa_r_hj32_local_total_to_p2_even_product))) /\ ((((exists pa_h_hj32_local_total_to_p2_even_product_successor. pa_h_hj32_local_total_to_p2_even_product_successor + S (pa_s_hj32_local_total_to_p2_even_product) = S ((S (S pa_i_hj32_local_total_to_p2_even_product)) * pa_v_hj32_local_total_to_p2_even_product)) /\ exists pa_q_hj32_local_total_to_p2_even_product_successor. pa_u_hj32_local_total_to_p2_even_product = pa_q_hj32_local_total_to_p2_even_product_successor * S ((S (S pa_i_hj32_local_total_to_p2_even_product)) * pa_v_hj32_local_total_to_p2_even_product) + (pa_s_hj32_local_total_to_p2_even_product))) /\ pa_s_hj32_local_total_to_p2_even_product = pa_r_hj32_local_total_to_p2_even_product * pa_p_hj32_local_total_to_p2_even_product))))))))
  8. 0008specialize htotal 2
  9. 0009specialize htotal 2 * k
  10. 0010exact htotal
  11. 0011cases to_p2_even
  12. 0012have to_p2_one : ∃ hj32_local_value_to_p2_one. Pow(2,1,hj32_local_value_to_p2_one)
    Exact native replay linehave to_p2_one : exists hj32_local_value_to_p2_one. (exists pa_b_hj32_local_total_to_p2_one pa_c_hj32_local_total_to_p2_one. ((forall pa_i_hj32_local_total_to_p2_one_repeat. (exists pa_lt_hj32_local_total_to_p2_one_repeat_bound. pa_lt_hj32_local_total_to_p2_one_repeat_bound + S pa_i_hj32_local_total_to_p2_one_repeat = 1) -> (((exists pa_h_hj32_local_total_to_p2_one_repeat_decoded. pa_h_hj32_local_total_to_p2_one_repeat_decoded + S (2) = S ((S (pa_i_hj32_local_total_to_p2_one_repeat)) * pa_c_hj32_local_total_to_p2_one)) /\ exists pa_q_hj32_local_total_to_p2_one_repeat_decoded. pa_b_hj32_local_total_to_p2_one = pa_q_hj32_local_total_to_p2_one_repeat_decoded * S ((S (pa_i_hj32_local_total_to_p2_one_repeat)) * pa_c_hj32_local_total_to_p2_one) + (2)))) /\ (exists pa_u_hj32_local_total_to_p2_one_product pa_v_hj32_local_total_to_p2_one_product. ((((exists pa_h_hj32_local_total_to_p2_one_product_start. pa_h_hj32_local_total_to_p2_one_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_to_p2_one_product)) /\ exists pa_q_hj32_local_total_to_p2_one_product_start. pa_u_hj32_local_total_to_p2_one_product = pa_q_hj32_local_total_to_p2_one_product_start * S ((S (0)) * pa_v_hj32_local_total_to_p2_one_product) + (1))) /\ ((((exists pa_h_hj32_local_total_to_p2_one_product_terminal. pa_h_hj32_local_total_to_p2_one_product_terminal + S (hj32_local_value_to_p2_one) = S ((S (1)) * pa_v_hj32_local_total_to_p2_one_product)) /\ exists pa_q_hj32_local_total_to_p2_one_product_terminal. pa_u_hj32_local_total_to_p2_one_product = pa_q_hj32_local_total_to_p2_one_product_terminal * S ((S (1)) * pa_v_hj32_local_total_to_p2_one_product) + (hj32_local_value_to_p2_one))) /\ forall pa_i_hj32_local_total_to_p2_one_product. (exists pa_lt_hj32_local_total_to_p2_one_product_bound. pa_lt_hj32_local_total_to_p2_one_product_bound + S pa_i_hj32_local_total_to_p2_one_product = 1) -> exists pa_p_hj32_local_total_to_p2_one_product pa_r_hj32_local_total_to_p2_one_product pa_s_hj32_local_total_to_p2_one_product. ((((exists pa_h_hj32_local_total_to_p2_one_product_factor. pa_h_hj32_local_total_to_p2_one_product_factor + S (pa_p_hj32_local_total_to_p2_one_product) = S ((S (pa_i_hj32_local_total_to_p2_one_product)) * pa_c_hj32_local_total_to_p2_one)) /\ exists pa_q_hj32_local_total_to_p2_one_product_factor. pa_b_hj32_local_total_to_p2_one = pa_q_hj32_local_total_to_p2_one_product_factor * S ((S (pa_i_hj32_local_total_to_p2_one_product)) * pa_c_hj32_local_total_to_p2_one) + (pa_p_hj32_local_total_to_p2_one_product))) /\ ((((exists pa_h_hj32_local_total_to_p2_one_product_partial. pa_h_hj32_local_total_to_p2_one_product_partial + S (pa_r_hj32_local_total_to_p2_one_product) = S ((S (pa_i_hj32_local_total_to_p2_one_product)) * pa_v_hj32_local_total_to_p2_one_product)) /\ exists pa_q_hj32_local_total_to_p2_one_product_partial. pa_u_hj32_local_total_to_p2_one_product = pa_q_hj32_local_total_to_p2_one_product_partial * S ((S (pa_i_hj32_local_total_to_p2_one_product)) * pa_v_hj32_local_total_to_p2_one_product) + (pa_r_hj32_local_total_to_p2_one_product))) /\ ((((exists pa_h_hj32_local_total_to_p2_one_product_successor. pa_h_hj32_local_total_to_p2_one_product_successor + S (pa_s_hj32_local_total_to_p2_one_product) = S ((S (S pa_i_hj32_local_total_to_p2_one_product)) * pa_v_hj32_local_total_to_p2_one_product)) /\ exists pa_q_hj32_local_total_to_p2_one_product_successor. pa_u_hj32_local_total_to_p2_one_product = pa_q_hj32_local_total_to_p2_one_product_successor * S ((S (S pa_i_hj32_local_total_to_p2_one_product)) * pa_v_hj32_local_total_to_p2_one_product) + (pa_s_hj32_local_total_to_p2_one_product))) /\ pa_s_hj32_local_total_to_p2_one_product = pa_r_hj32_local_total_to_p2_one_product * pa_p_hj32_local_total_to_p2_one_product))))))))
  13. 0013specialize htotal 2
  14. 0014specialize htotal 1
  15. 0015exact htotal
  16. 0016cases to_p2_one
  17. 0017have to_p4_even : ∃ hj32_local_value_to_p4_even. Pow(4,k,hj32_local_value_to_p4_even)
    Exact native replay linehave to_p4_even : exists hj32_local_value_to_p4_even. (exists pa_b_hj32_local_total_to_p4_even pa_c_hj32_local_total_to_p4_even. ((forall pa_i_hj32_local_total_to_p4_even_repeat. (exists pa_lt_hj32_local_total_to_p4_even_repeat_bound. pa_lt_hj32_local_total_to_p4_even_repeat_bound + S pa_i_hj32_local_total_to_p4_even_repeat = k) -> (((exists pa_h_hj32_local_total_to_p4_even_repeat_decoded. pa_h_hj32_local_total_to_p4_even_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_to_p4_even_repeat)) * pa_c_hj32_local_total_to_p4_even)) /\ exists pa_q_hj32_local_total_to_p4_even_repeat_decoded. pa_b_hj32_local_total_to_p4_even = pa_q_hj32_local_total_to_p4_even_repeat_decoded * S ((S (pa_i_hj32_local_total_to_p4_even_repeat)) * pa_c_hj32_local_total_to_p4_even) + (4)))) /\ (exists pa_u_hj32_local_total_to_p4_even_product pa_v_hj32_local_total_to_p4_even_product. ((((exists pa_h_hj32_local_total_to_p4_even_product_start. pa_h_hj32_local_total_to_p4_even_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_to_p4_even_product)) /\ exists pa_q_hj32_local_total_to_p4_even_product_start. pa_u_hj32_local_total_to_p4_even_product = pa_q_hj32_local_total_to_p4_even_product_start * S ((S (0)) * pa_v_hj32_local_total_to_p4_even_product) + (1))) /\ ((((exists pa_h_hj32_local_total_to_p4_even_product_terminal. pa_h_hj32_local_total_to_p4_even_product_terminal + S (hj32_local_value_to_p4_even) = S ((S (k)) * pa_v_hj32_local_total_to_p4_even_product)) /\ exists pa_q_hj32_local_total_to_p4_even_product_terminal. pa_u_hj32_local_total_to_p4_even_product = pa_q_hj32_local_total_to_p4_even_product_terminal * S ((S (k)) * pa_v_hj32_local_total_to_p4_even_product) + (hj32_local_value_to_p4_even))) /\ forall pa_i_hj32_local_total_to_p4_even_product. (exists pa_lt_hj32_local_total_to_p4_even_product_bound. pa_lt_hj32_local_total_to_p4_even_product_bound + S pa_i_hj32_local_total_to_p4_even_product = k) -> exists pa_p_hj32_local_total_to_p4_even_product pa_r_hj32_local_total_to_p4_even_product pa_s_hj32_local_total_to_p4_even_product. ((((exists pa_h_hj32_local_total_to_p4_even_product_factor. pa_h_hj32_local_total_to_p4_even_product_factor + S (pa_p_hj32_local_total_to_p4_even_product) = S ((S (pa_i_hj32_local_total_to_p4_even_product)) * pa_c_hj32_local_total_to_p4_even)) /\ exists pa_q_hj32_local_total_to_p4_even_product_factor. pa_b_hj32_local_total_to_p4_even = pa_q_hj32_local_total_to_p4_even_product_factor * S ((S (pa_i_hj32_local_total_to_p4_even_product)) * pa_c_hj32_local_total_to_p4_even) + (pa_p_hj32_local_total_to_p4_even_product))) /\ ((((exists pa_h_hj32_local_total_to_p4_even_product_partial. pa_h_hj32_local_total_to_p4_even_product_partial + S (pa_r_hj32_local_total_to_p4_even_product) = S ((S (pa_i_hj32_local_total_to_p4_even_product)) * pa_v_hj32_local_total_to_p4_even_product)) /\ exists pa_q_hj32_local_total_to_p4_even_product_partial. pa_u_hj32_local_total_to_p4_even_product = pa_q_hj32_local_total_to_p4_even_product_partial * S ((S (pa_i_hj32_local_total_to_p4_even_product)) * pa_v_hj32_local_total_to_p4_even_product) + (pa_r_hj32_local_total_to_p4_even_product))) /\ ((((exists pa_h_hj32_local_total_to_p4_even_product_successor. pa_h_hj32_local_total_to_p4_even_product_successor + S (pa_s_hj32_local_total_to_p4_even_product) = S ((S (S pa_i_hj32_local_total_to_p4_even_product)) * pa_v_hj32_local_total_to_p4_even_product)) /\ exists pa_q_hj32_local_total_to_p4_even_product_successor. pa_u_hj32_local_total_to_p4_even_product = pa_q_hj32_local_total_to_p4_even_product_successor * S ((S (S pa_i_hj32_local_total_to_p4_even_product)) * pa_v_hj32_local_total_to_p4_even_product) + (pa_s_hj32_local_total_to_p4_even_product))) /\ pa_s_hj32_local_total_to_p4_even_product = pa_r_hj32_local_total_to_p4_even_product * pa_p_hj32_local_total_to_p4_even_product))))))))
  18. 0018specialize htotal 4
  19. 0019specialize htotal k
  20. 0020exact htotal
  21. 0021cases to_p4_even
  22. 0022have to_p4_one : ∃ hj32_local_value_to_p4_one. Pow(4,1,hj32_local_value_to_p4_one)
    Exact native replay linehave to_p4_one : exists hj32_local_value_to_p4_one. (exists pa_b_hj32_local_total_to_p4_one pa_c_hj32_local_total_to_p4_one. ((forall pa_i_hj32_local_total_to_p4_one_repeat. (exists pa_lt_hj32_local_total_to_p4_one_repeat_bound. pa_lt_hj32_local_total_to_p4_one_repeat_bound + S pa_i_hj32_local_total_to_p4_one_repeat = 1) -> (((exists pa_h_hj32_local_total_to_p4_one_repeat_decoded. pa_h_hj32_local_total_to_p4_one_repeat_decoded + S (4) = S ((S (pa_i_hj32_local_total_to_p4_one_repeat)) * pa_c_hj32_local_total_to_p4_one)) /\ exists pa_q_hj32_local_total_to_p4_one_repeat_decoded. pa_b_hj32_local_total_to_p4_one = pa_q_hj32_local_total_to_p4_one_repeat_decoded * S ((S (pa_i_hj32_local_total_to_p4_one_repeat)) * pa_c_hj32_local_total_to_p4_one) + (4)))) /\ (exists pa_u_hj32_local_total_to_p4_one_product pa_v_hj32_local_total_to_p4_one_product. ((((exists pa_h_hj32_local_total_to_p4_one_product_start. pa_h_hj32_local_total_to_p4_one_product_start + S (1) = S ((S (0)) * pa_v_hj32_local_total_to_p4_one_product)) /\ exists pa_q_hj32_local_total_to_p4_one_product_start. pa_u_hj32_local_total_to_p4_one_product = pa_q_hj32_local_total_to_p4_one_product_start * S ((S (0)) * pa_v_hj32_local_total_to_p4_one_product) + (1))) /\ ((((exists pa_h_hj32_local_total_to_p4_one_product_terminal. pa_h_hj32_local_total_to_p4_one_product_terminal + S (hj32_local_value_to_p4_one) = S ((S (1)) * pa_v_hj32_local_total_to_p4_one_product)) /\ exists pa_q_hj32_local_total_to_p4_one_product_terminal. pa_u_hj32_local_total_to_p4_one_product = pa_q_hj32_local_total_to_p4_one_product_terminal * S ((S (1)) * pa_v_hj32_local_total_to_p4_one_product) + (hj32_local_value_to_p4_one))) /\ forall pa_i_hj32_local_total_to_p4_one_product. (exists pa_lt_hj32_local_total_to_p4_one_product_bound. pa_lt_hj32_local_total_to_p4_one_product_bound + S pa_i_hj32_local_total_to_p4_one_product = 1) -> exists pa_p_hj32_local_total_to_p4_one_product pa_r_hj32_local_total_to_p4_one_product pa_s_hj32_local_total_to_p4_one_product. ((((exists pa_h_hj32_local_total_to_p4_one_product_factor. pa_h_hj32_local_total_to_p4_one_product_factor + S (pa_p_hj32_local_total_to_p4_one_product) = S ((S (pa_i_hj32_local_total_to_p4_one_product)) * pa_c_hj32_local_total_to_p4_one)) /\ exists pa_q_hj32_local_total_to_p4_one_product_factor. pa_b_hj32_local_total_to_p4_one = pa_q_hj32_local_total_to_p4_one_product_factor * S ((S (pa_i_hj32_local_total_to_p4_one_product)) * pa_c_hj32_local_total_to_p4_one) + (pa_p_hj32_local_total_to_p4_one_product))) /\ ((((exists pa_h_hj32_local_total_to_p4_one_product_partial. pa_h_hj32_local_total_to_p4_one_product_partial + S (pa_r_hj32_local_total_to_p4_one_product) = S ((S (pa_i_hj32_local_total_to_p4_one_product)) * pa_v_hj32_local_total_to_p4_one_product)) /\ exists pa_q_hj32_local_total_to_p4_one_product_partial. pa_u_hj32_local_total_to_p4_one_product = pa_q_hj32_local_total_to_p4_one_product_partial * S ((S (pa_i_hj32_local_total_to_p4_one_product)) * pa_v_hj32_local_total_to_p4_one_product) + (pa_r_hj32_local_total_to_p4_one_product))) /\ ((((exists pa_h_hj32_local_total_to_p4_one_product_successor. pa_h_hj32_local_total_to_p4_one_product_successor + S (pa_s_hj32_local_total_to_p4_one_product) = S ((S (S pa_i_hj32_local_total_to_p4_one_product)) * pa_v_hj32_local_total_to_p4_one_product)) /\ exists pa_q_hj32_local_total_to_p4_one_product_successor. pa_u_hj32_local_total_to_p4_one_product = pa_q_hj32_local_total_to_p4_one_product_successor * S ((S (S pa_i_hj32_local_total_to_p4_one_product)) * pa_v_hj32_local_total_to_p4_one_product) + (pa_s_hj32_local_total_to_p4_one_product))) /\ pa_s_hj32_local_total_to_p4_one_product = pa_r_hj32_local_total_to_p4_one_product * pa_p_hj32_local_total_to_p4_one_product))))))))
  23. 0023specialize htotal 4
  24. 0024specialize htotal 1
  25. 0025exact htotal
  26. 0026cases to_p4_one
  27. 0027have to_even_eq : x1 = x3
  28. 0028specialize pow_two_double_eq_pow_four_from_total k
  29. 0029specialize pow_two_double_eq_pow_four_from_total x1
  30. 0030specialize pow_two_double_eq_pow_four_from_total x3
  31. 0031apply pow_two_double_eq_pow_four_from_total
  32. 0032exact htotal
  33. 0033exact to_p2_even_witness
  34. 0034exact to_p4_even_witness
  35. 0035have to_even_bound : Le(x1,x3)
    Exact native replay linehave to_even_bound : exists bqb_le_gap_hj32_to_even_bound. bqb_le_gap_hj32_to_even_bound + (x1) = (x3)
  36. 0036rewrite to_even_eq
  37. 0037specialize le_refl x3
  38. 0038exact le_refl
  39. 0039have to_base : Lt(1,4)
    Exact native replay linehave to_base : exists bqb_le_gap_hj32_to_base. bqb_le_gap_hj32_to_base + (2) = (4)
  40. 0040exists 2
  41. 0041norm_num
  42. 0042have to_one_bound : Le(x2,x4)
    Exact native replay linehave to_one_bound : exists bqb_le_gap_hj32_local_base_bound_to_one_bound. bqb_le_gap_hj32_local_base_bound_to_one_bound + (x2) = (x4)
  43. 0043specialize pow_base_monotone 2
  44. 0044specialize pow_base_monotone 4
  45. 0045specialize pow_base_monotone 1
  46. 0046specialize pow_base_monotone x2
  47. 0047specialize pow_base_monotone x4
  48. 0048apply pow_base_monotone
  49. 0049exact to_base
  50. 0050exact to_p2_one_witness
  51. 0051exact to_p4_one_witness
  52. 0052have to_left_product : x = x1 * x2
  53. 0053specialize pow_add 2
  54. 0054specialize pow_add 2 * k
  55. 0055specialize pow_add 1
  56. 0056specialize pow_add 2 * k + 1
  57. 0057specialize pow_add x1
  58. 0058specialize pow_add x2
  59. 0059specialize pow_add x
  60. 0060apply pow_add
  61. 0061refl
  62. 0062exact to_p2_even_witness
  63. 0063exact to_p2_one_witness
  64. 0064exact hx
  65. 0065have to_right_product : y = x3 * x4
  66. 0066specialize pow_add 4
  67. 0067specialize pow_add k
  68. 0068specialize pow_add 1
  69. 0069specialize pow_add k + 1
  70. 0070specialize pow_add x3
  71. 0071specialize pow_add x4
  72. 0072specialize pow_add y
  73. 0073apply pow_add
  74. 0074refl
  75. 0075exact to_p4_even_witness
  76. 0076exact to_p4_one_witness
  77. 0077exact hy
  78. 0078have to_result : Le(x1 · x2,x3 · x4)
    Exact native replay linehave to_result : exists bqb_le_gap_hj32_local_product_bound_to_result. bqb_le_gap_hj32_local_product_bound_to_result + (x1 * x2) = (x3 * x4)
  79. 0079specialize mul_le_mul x1
  80. 0080specialize mul_le_mul x3
  81. 0081specialize mul_le_mul x2
  82. 0082specialize mul_le_mul x4
  83. 0083apply mul_le_mul
  84. 0084exact to_even_bound
  85. 0085exact to_one_bound
  86. 0086rewrite <- to_left_product at to_result
  87. 0087rewrite <- to_right_product at to_result
  88. 0088exact to_result