BT00X4 · Bertrand theorem

bertrand_floor_power_product_le_h_from_total

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

The floor-root power product is bounded by the H envelope using 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. ∀ A. ∀ H. (∀ x. ∀ y. ∃ z. Pow(x,y,z)) → FloorSqrt(2 · n,s) → Pow(2 · n,s,A) → Pow(s + 1,2 · s + 2,H) → Le(n · A,H)

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 PD0051 FloorSqrt

5 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0020 Pow

12 occurrences

Exact expanded native-PA statement
forall n s A H. (forall bpt_a_b6_floor_product bpt_e_b6_floor_product. exists bpt_x_b6_floor_product. (exists ff_b_bpt_value_b6_floor_product ff_c_bpt_value_b6_floor_product. ((forall ff_i_bpt_value_b6_floor_product_repeat. (exists ff_lt_bpt_value_b6_floor_product_repeat_bound. ff_lt_bpt_value_b6_floor_product_repeat_bound + S ff_i_bpt_value_b6_floor_product_repeat = bpt_e_b6_floor_product) -> (((exists ff_h_bpt_value_b6_floor_product_repeat_decoded. ff_h_bpt_value_b6_floor_product_repeat_decoded + S (bpt_a_b6_floor_product) = S ((S (ff_i_bpt_value_b6_floor_product_repeat)) * ff_c_bpt_value_b6_floor_product)) /\ exists ff_q_bpt_value_b6_floor_product_repeat_decoded. ff_b_bpt_value_b6_floor_product = ff_q_bpt_value_b6_floor_product_repeat_decoded * S ((S (ff_i_bpt_value_b6_floor_product_repeat)) * ff_c_bpt_value_b6_floor_product) + (bpt_a_b6_floor_product)))) /\ (exists ff_u_bpt_value_b6_floor_product_product ff_v_bpt_value_b6_floor_product_product. ((((exists ff_h_bpt_value_b6_floor_product_product_start. ff_h_bpt_value_b6_floor_product_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_b6_floor_product_product)) /\ exists ff_q_bpt_value_b6_floor_product_product_start. ff_u_bpt_value_b6_floor_product_product = ff_q_bpt_value_b6_floor_product_product_start * S ((S (0)) * ff_v_bpt_value_b6_floor_product_product) + (1))) /\ ((((exists ff_h_bpt_value_b6_floor_product_product_terminal. ff_h_bpt_value_b6_floor_product_product_terminal + S (bpt_x_b6_floor_product) = S ((S (bpt_e_b6_floor_product)) * ff_v_bpt_value_b6_floor_product_product)) /\ exists ff_q_bpt_value_b6_floor_product_product_terminal. ff_u_bpt_value_b6_floor_product_product = ff_q_bpt_value_b6_floor_product_product_terminal * S ((S (bpt_e_b6_floor_product)) * ff_v_bpt_value_b6_floor_product_product) + (bpt_x_b6_floor_product))) /\ forall ff_i_bpt_value_b6_floor_product_product. (exists ff_lt_bpt_value_b6_floor_product_product_bound. ff_lt_bpt_value_b6_floor_product_product_bound + S ff_i_bpt_value_b6_floor_product_product = bpt_e_b6_floor_product) -> exists ff_p_bpt_value_b6_floor_product_product ff_r_bpt_value_b6_floor_product_product ff_s_bpt_value_b6_floor_product_product. ((((exists ff_h_bpt_value_b6_floor_product_product_factor. ff_h_bpt_value_b6_floor_product_product_factor + S (ff_p_bpt_value_b6_floor_product_product) = S ((S (ff_i_bpt_value_b6_floor_product_product)) * ff_c_bpt_value_b6_floor_product)) /\ exists ff_q_bpt_value_b6_floor_product_product_factor. ff_b_bpt_value_b6_floor_product = ff_q_bpt_value_b6_floor_product_product_factor * S ((S (ff_i_bpt_value_b6_floor_product_product)) * ff_c_bpt_value_b6_floor_product) + (ff_p_bpt_value_b6_floor_product_product))) /\ ((((exists ff_h_bpt_value_b6_floor_product_product_partial. ff_h_bpt_value_b6_floor_product_product_partial + S (ff_r_bpt_value_b6_floor_product_product) = S ((S (ff_i_bpt_value_b6_floor_product_product)) * ff_v_bpt_value_b6_floor_product_product)) /\ exists ff_q_bpt_value_b6_floor_product_product_partial. ff_u_bpt_value_b6_floor_product_product = ff_q_bpt_value_b6_floor_product_product_partial * S ((S (ff_i_bpt_value_b6_floor_product_product)) * ff_v_bpt_value_b6_floor_product_product) + (ff_r_bpt_value_b6_floor_product_product))) /\ ((((exists ff_h_bpt_value_b6_floor_product_product_successor. ff_h_bpt_value_b6_floor_product_product_successor + S (ff_s_bpt_value_b6_floor_product_product) = S ((S (S ff_i_bpt_value_b6_floor_product_product)) * ff_v_bpt_value_b6_floor_product_product)) /\ exists ff_q_bpt_value_b6_floor_product_product_successor. ff_u_bpt_value_b6_floor_product_product = ff_q_bpt_value_b6_floor_product_product_successor * S ((S (S ff_i_bpt_value_b6_floor_product_product)) * ff_v_bpt_value_b6_floor_product_product) + (ff_s_bpt_value_b6_floor_product_product))) /\ ff_s_bpt_value_b6_floor_product_product = ff_r_bpt_value_b6_floor_product_product * ff_p_bpt_value_b6_floor_product_product))))))))) -> (((exists bcs_sqrt_lower_gap_b6_floor_product_root. bcs_sqrt_lower_gap_b6_floor_product_root + (s) * (s) = (2 * n)) /\ exists bcs_sqrt_upper_gap_b6_floor_product_root. bcs_sqrt_upper_gap_b6_floor_product_root + S (2 * n) = S (s) * S (s))) -> (exists pa_b_b6_floor_product_power pa_c_b6_floor_product_power. ((forall pa_i_b6_floor_product_power_repeat. (exists pa_lt_b6_floor_product_power_repeat_bound. pa_lt_b6_floor_product_power_repeat_bound + S pa_i_b6_floor_product_power_repeat = s) -> (((exists pa_h_b6_floor_product_power_repeat_decoded. pa_h_b6_floor_product_power_repeat_decoded + S (2 * n) = S ((S (pa_i_b6_floor_product_power_repeat)) * pa_c_b6_floor_product_power)) /\ exists pa_q_b6_floor_product_power_repeat_decoded. pa_b_b6_floor_product_power = pa_q_b6_floor_product_power_repeat_decoded * S ((S (pa_i_b6_floor_product_power_repeat)) * pa_c_b6_floor_product_power) + (2 * n)))) /\ (exists pa_u_b6_floor_product_power_product pa_v_b6_floor_product_power_product. ((((exists pa_h_b6_floor_product_power_product_start. pa_h_b6_floor_product_power_product_start + S (1) = S ((S (0)) * pa_v_b6_floor_product_power_product)) /\ exists pa_q_b6_floor_product_power_product_start. pa_u_b6_floor_product_power_product = pa_q_b6_floor_product_power_product_start * S ((S (0)) * pa_v_b6_floor_product_power_product) + (1))) /\ ((((exists pa_h_b6_floor_product_power_product_terminal. pa_h_b6_floor_product_power_product_terminal + S (A) = S ((S (s)) * pa_v_b6_floor_product_power_product)) /\ exists pa_q_b6_floor_product_power_product_terminal. pa_u_b6_floor_product_power_product = pa_q_b6_floor_product_power_product_terminal * S ((S (s)) * pa_v_b6_floor_product_power_product) + (A))) /\ forall pa_i_b6_floor_product_power_product. (exists pa_lt_b6_floor_product_power_product_bound. pa_lt_b6_floor_product_power_product_bound + S pa_i_b6_floor_product_power_product = s) -> exists pa_p_b6_floor_product_power_product pa_r_b6_floor_product_power_product pa_s_b6_floor_product_power_product. ((((exists pa_h_b6_floor_product_power_product_factor. pa_h_b6_floor_product_power_product_factor + S (pa_p_b6_floor_product_power_product) = S ((S (pa_i_b6_floor_product_power_product)) * pa_c_b6_floor_product_power)) /\ exists pa_q_b6_floor_product_power_product_factor. pa_b_b6_floor_product_power = pa_q_b6_floor_product_power_product_factor * S ((S (pa_i_b6_floor_product_power_product)) * pa_c_b6_floor_product_power) + (pa_p_b6_floor_product_power_product))) /\ ((((exists pa_h_b6_floor_product_power_product_partial. pa_h_b6_floor_product_power_product_partial + S (pa_r_b6_floor_product_power_product) = S ((S (pa_i_b6_floor_product_power_product)) * pa_v_b6_floor_product_power_product)) /\ exists pa_q_b6_floor_product_power_product_partial. pa_u_b6_floor_product_power_product = pa_q_b6_floor_product_power_product_partial * S ((S (pa_i_b6_floor_product_power_product)) * pa_v_b6_floor_product_power_product) + (pa_r_b6_floor_product_power_product))) /\ ((((exists pa_h_b6_floor_product_power_product_successor. pa_h_b6_floor_product_power_product_successor + S (pa_s_b6_floor_product_power_product) = S ((S (S pa_i_b6_floor_product_power_product)) * pa_v_b6_floor_product_power_product)) /\ exists pa_q_b6_floor_product_power_product_successor. pa_u_b6_floor_product_power_product = pa_q_b6_floor_product_power_product_successor * S ((S (S pa_i_b6_floor_product_power_product)) * pa_v_b6_floor_product_power_product) + (pa_s_b6_floor_product_power_product))) /\ pa_s_b6_floor_product_power_product = pa_r_b6_floor_product_power_product * pa_p_b6_floor_product_power_product)))))))) -> (exists pa_b_b6_floor_product_envelope pa_c_b6_floor_product_envelope. ((forall pa_i_b6_floor_product_envelope_repeat. (exists pa_lt_b6_floor_product_envelope_repeat_bound. pa_lt_b6_floor_product_envelope_repeat_bound + S pa_i_b6_floor_product_envelope_repeat = 2 * s + 2) -> (((exists pa_h_b6_floor_product_envelope_repeat_decoded. pa_h_b6_floor_product_envelope_repeat_decoded + S (s + 1) = S ((S (pa_i_b6_floor_product_envelope_repeat)) * pa_c_b6_floor_product_envelope)) /\ exists pa_q_b6_floor_product_envelope_repeat_decoded. pa_b_b6_floor_product_envelope = pa_q_b6_floor_product_envelope_repeat_decoded * S ((S (pa_i_b6_floor_product_envelope_repeat)) * pa_c_b6_floor_product_envelope) + (s + 1)))) /\ (exists pa_u_b6_floor_product_envelope_product pa_v_b6_floor_product_envelope_product. ((((exists pa_h_b6_floor_product_envelope_product_start. pa_h_b6_floor_product_envelope_product_start + S (1) = S ((S (0)) * pa_v_b6_floor_product_envelope_product)) /\ exists pa_q_b6_floor_product_envelope_product_start. pa_u_b6_floor_product_envelope_product = pa_q_b6_floor_product_envelope_product_start * S ((S (0)) * pa_v_b6_floor_product_envelope_product) + (1))) /\ ((((exists pa_h_b6_floor_product_envelope_product_terminal. pa_h_b6_floor_product_envelope_product_terminal + S (H) = S ((S (2 * s + 2)) * pa_v_b6_floor_product_envelope_product)) /\ exists pa_q_b6_floor_product_envelope_product_terminal. pa_u_b6_floor_product_envelope_product = pa_q_b6_floor_product_envelope_product_terminal * S ((S (2 * s + 2)) * pa_v_b6_floor_product_envelope_product) + (H))) /\ forall pa_i_b6_floor_product_envelope_product. (exists pa_lt_b6_floor_product_envelope_product_bound. pa_lt_b6_floor_product_envelope_product_bound + S pa_i_b6_floor_product_envelope_product = 2 * s + 2) -> exists pa_p_b6_floor_product_envelope_product pa_r_b6_floor_product_envelope_product pa_s_b6_floor_product_envelope_product. ((((exists pa_h_b6_floor_product_envelope_product_factor. pa_h_b6_floor_product_envelope_product_factor + S (pa_p_b6_floor_product_envelope_product) = S ((S (pa_i_b6_floor_product_envelope_product)) * pa_c_b6_floor_product_envelope)) /\ exists pa_q_b6_floor_product_envelope_product_factor. pa_b_b6_floor_product_envelope = pa_q_b6_floor_product_envelope_product_factor * S ((S (pa_i_b6_floor_product_envelope_product)) * pa_c_b6_floor_product_envelope) + (pa_p_b6_floor_product_envelope_product))) /\ ((((exists pa_h_b6_floor_product_envelope_product_partial. pa_h_b6_floor_product_envelope_product_partial + S (pa_r_b6_floor_product_envelope_product) = S ((S (pa_i_b6_floor_product_envelope_product)) * pa_v_b6_floor_product_envelope_product)) /\ exists pa_q_b6_floor_product_envelope_product_partial. pa_u_b6_floor_product_envelope_product = pa_q_b6_floor_product_envelope_product_partial * S ((S (pa_i_b6_floor_product_envelope_product)) * pa_v_b6_floor_product_envelope_product) + (pa_r_b6_floor_product_envelope_product))) /\ ((((exists pa_h_b6_floor_product_envelope_product_successor. pa_h_b6_floor_product_envelope_product_successor + S (pa_s_b6_floor_product_envelope_product) = S ((S (S pa_i_b6_floor_product_envelope_product)) * pa_v_b6_floor_product_envelope_product)) /\ exists pa_q_b6_floor_product_envelope_product_successor. pa_u_b6_floor_product_envelope_product = pa_q_b6_floor_product_envelope_product_successor * S ((S (S pa_i_b6_floor_product_envelope_product)) * pa_v_b6_floor_product_envelope_product) + (pa_s_b6_floor_product_envelope_product))) /\ pa_s_b6_floor_product_envelope_product = pa_r_b6_floor_product_envelope_product * pa_p_b6_floor_product_envelope_product)))))))) -> (exists bqb_le_gap_b6_floor_product_result. bqb_le_gap_b6_floor_product_result + (n * A) = (H))

Proof neighborhood

Direct theorem prerequisites

BT00R7 floor_sqrt_strict_upper_bound BT0019 lt_to_le BT0013 le_add_right BT00QU two_mul_eq_add_self BT000F le_trans BT009W pow_two BT00PY pow_base_monotone BT00SM pow_mul_exp_from_total BT009X pow_add BT00PV mul_le_mul BT0006 mul_comm

Direct theorem dependents

BT00X6 bertrand_main_inequality_factorized_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

121 script commands · 25 reading checkpoints · 18 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 (11)
floor sqrt strict upper boundlt to lele add righttwo mul eq add selfle transpow twopow base monotonepow mul exp from totalpow addmul le mulmul comm
01Fix variables and assumptionsL1–8

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

  1. L1
    intro n
  2. L2
    intro s
  3. L3
    intro A
  4. L4
    intro H
  5. L5
    intro htotal
  6. L6
    intro hfloor
  7. L7
    intro hA
  8. L8
    intro hH
02Establish hstrictL9–13

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply floor sqrt strict upper bound.

  1. L9
    have hstrict : Lt(2 · n,S s · S s)Definitions: Lt(2 · n,S s · S s)Original native command in the exact edition
  2. L10
    specialize floor_sqrt_strict_upper_bound (2 * n)
  3. L11
    specialize floor_sqrt_strict_upper_bound s
  4. L12
    apply floor_sqrt_strict_upper_bound
  5. L13
    exact hfloor
03Establish hweakL14–18

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

  1. L14
    have hweak : Le(2 · n,S s · S s)Definitions: Le(2 · n,S s · S s)Original native command in the exact edition
  2. L15
    specialize lt_to_le (2 * n)
  3. L16
    specialize lt_to_le (S s * S s)
  4. L17
    apply lt_to_le
  5. L18
    exact hstrict
04Establish hsuccL19–22

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

  1. L19
    have hsucc : s + 1 = S s
  2. L20
    rewrite PA4
  3. L21
    congr
  4. L22
    apply PA3
05Establish hv_existsL23–26

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

  1. L23
    have hv_exists : ∃ v. Pow(s + 1,2,v)Definitions: Pow(s + 1,2,v)Original native command in the exact edition
  2. L24
    specialize htotal (s + 1)
  3. L25
    specialize htotal 2
  4. L26
    exact htotal
06Separate the logical casesL27–27

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

  1. L27
    cases hv_exists
07Establish hv_squareL28–34

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

  1. L28
    have hv_square : x = (s + 1) * (s + 1)
  2. L29
    specialize pow_two (s + 1)
  3. L30
    specialize pow_two 2
  4. L31
    specialize pow_two x
  5. L32
    apply pow_two
  6. L33
    refl
  7. L34
    exact hv_exists_witness
08Establish hbaseL35–39

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

  1. L35
    have hbase : Le(2 · n,x)Definitions: Le(2 · n,x)Original native command in the exact edition
  2. L36
    rewrite hv_square
  3. L37
    rewrite hsucc
  4. L38
    rewrite hsucc
  5. L39
    exact hweak
09Establish hu_existsL40–43

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

  1. L40
    have hu_exists : ∃ u. Pow(x,s,u)Definitions: Pow(x,s,u)Original native command in the exact edition
  2. L41
    specialize htotal x
  3. L42
    specialize htotal s
  4. L43
    exact htotal
10Separate the logical casesL44–44

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

  1. L44
    cases hu_exists
11Establish hpowerL45–54

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

  1. L45
    have hpower : Le(A,x1)Definitions: Le(A,x1)Original native command in the exact edition
  2. L46
    specialize pow_base_monotone (2 * n)
  3. L47
    specialize pow_base_monotone x
  4. L48
    specialize pow_base_monotone s
  5. L49
    specialize pow_base_monotone A
  6. L50
    specialize pow_base_monotone x1
  7. L51
    apply pow_base_monotone
  8. L52
    exact hbase
  9. L53
    exact hA
  10. L54
    exact hu_exists_witness
12Establish hz_existsL55–58

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

  1. L55
    have hz_exists : ∃ z. Pow(s + 1,2 · s,z)Definitions: Pow(s + 1,2 · s,z)Original native command in the exact edition
  2. L56
    specialize htotal (s + 1)
  3. L57
    specialize htotal (2 * s)
  4. L58
    exact htotal
13Separate the logical casesL59–59

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

  1. L59
    cases hz_exists
14Establish huzL60–69

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

  1. L60
    have huz : x1 = x2
  2. L61
    specialize pow_mul_exp_from_total (s + 1)
  3. L62
    specialize pow_mul_exp_from_total 2
  4. L63
    specialize pow_mul_exp_from_total s
  5. L64
    specialize pow_mul_exp_from_total (2 * s)
  6. L65
    specialize pow_mul_exp_from_total x
  7. L66
    specialize pow_mul_exp_from_total x1
  8. L67
    specialize pow_mul_exp_from_total x2
  9. L68
    apply pow_mul_exp_from_total
  10. L69
    exact htotal
15Calculate and transport equalitiesL70–70

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

  1. L70
    refl
16Use earlier factsL71–73

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

  1. L71
    exact hv_exists_witness
  2. L72
    exact hu_exists_witness
  3. L73
    exact hz_exists_witness
17Establish hfactorL74–83

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

  1. L74
    have hfactor : H = x2 * x
  2. L75
    specialize pow_add (s + 1)
  3. L76
    specialize pow_add (2 * s)
  4. L77
    specialize pow_add 2
  5. L78
    specialize pow_add (2 * s + 2)
  6. L79
    specialize pow_add x2
  7. L80
    specialize pow_add x
  8. L81
    specialize pow_add H
  9. L82
    apply pow_add
  10. L83
    refl
18Use earlier factsL84–86

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

  1. L84
    exact hz_exists_witness
  2. L85
    exact hv_exists_witness
  3. L86
    exact hH
19Establish hn_double_sumL87–90

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

  1. L87
    have hn_double_sum : Le(n,n + n)Definitions: Le(n,n + n)Original native command in the exact edition
  2. L88
    specialize le_add_right n
  3. L89
    specialize le_add_right n
  4. L90
    exact le_add_right
20Establish hdoubleL91–93

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

  1. L91
    have hdouble : 2 * n = n + n
  2. L92
    specialize two_mul_eq_add_self n
  3. L93
    exact two_mul_eq_add_self
21Establish hn_doubleL94–96

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

  1. L94
    have hn_double : Le(n,2 · n)Definitions: Le(n,2 · n)Original native command in the exact edition
  2. L95
    rewrite hdouble
  3. L96
    exact hn_double_sum
22Establish hn_squareL97–103

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

  1. L97
    have hn_square : Le(n,x)Definitions: Le(n,x)Original native command in the exact edition
  2. L98
    specialize le_trans n
  3. L99
    specialize le_trans (2 * n)
  4. L100
    specialize le_trans x
  5. L101
    apply le_trans
  6. L102
    exact hn_double
  7. L103
    exact hbase
23Establish hAzL104–106

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

  1. L104
  2. L105
    rewrite <- huz
  3. L106
    exact hpower
24Establish hproductL107–114

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

  1. L107
    have hproduct : Le(n · A,x · x2)Definitions: Le(n · A,x · x2)Original native command in the exact edition
  2. L108
    specialize mul_le_mul n
  3. L109
    specialize mul_le_mul x
  4. L110
    specialize mul_le_mul A
  5. L111
    specialize mul_le_mul x2
  6. L112
    apply mul_le_mul
  7. L113
    exact hn_square
  8. L114
    exact hAz
25Establish hcommL115–121

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

  1. L115
    have hcomm : x * x2 = x2 * x
  2. L116
    specialize mul_comm x
  3. L117
    specialize mul_comm x2
  4. L118
    exact mul_comm
  5. L119
    rewrite hcomm at hproduct
  6. L120
    rewrite <- hfactor at hproduct
  7. L121
    exact hproduct

Library-wide reading audit

Original defined command ledger · 121 lines
  1. 0001intro n
  2. 0002intro s
  3. 0003intro A
  4. 0004intro H
  5. 0005intro htotal
  6. 0006intro hfloor
  7. 0007intro hA
  8. 0008intro hH
  9. 0009have hstrict : Lt(2 · n,S s · S s)
    Exact native replay linehave hstrict : exists k. k + S (2 * n) = S s * S s
  10. 0010specialize floor_sqrt_strict_upper_bound (2 * n)
  11. 0011specialize floor_sqrt_strict_upper_bound s
  12. 0012apply floor_sqrt_strict_upper_bound
  13. 0013exact hfloor
  14. 0014have hweak : Le(2 · n,S s · S s)
    Exact native replay linehave hweak : exists k. k + 2 * n = S s * S s
  15. 0015specialize lt_to_le (2 * n)
  16. 0016specialize lt_to_le (S s * S s)
  17. 0017apply lt_to_le
  18. 0018exact hstrict
  19. 0019have hsucc : s + 1 = S s
  20. 0020rewrite PA4
  21. 0021congr
  22. 0022apply PA3
  23. 0023have hv_exists : ∃ v. Pow(s + 1,2,v)
    Exact native replay linehave hv_exists : exists v. (exists pa_b_b6_floor_product_square pa_c_b6_floor_product_square. ((forall pa_i_b6_floor_product_square_repeat. (exists pa_lt_b6_floor_product_square_repeat_bound. pa_lt_b6_floor_product_square_repeat_bound + S pa_i_b6_floor_product_square_repeat = 2) -> (((exists pa_h_b6_floor_product_square_repeat_decoded. pa_h_b6_floor_product_square_repeat_decoded + S (s + 1) = S ((S (pa_i_b6_floor_product_square_repeat)) * pa_c_b6_floor_product_square)) /\ exists pa_q_b6_floor_product_square_repeat_decoded. pa_b_b6_floor_product_square = pa_q_b6_floor_product_square_repeat_decoded * S ((S (pa_i_b6_floor_product_square_repeat)) * pa_c_b6_floor_product_square) + (s + 1)))) /\ (exists pa_u_b6_floor_product_square_product pa_v_b6_floor_product_square_product. ((((exists pa_h_b6_floor_product_square_product_start. pa_h_b6_floor_product_square_product_start + S (1) = S ((S (0)) * pa_v_b6_floor_product_square_product)) /\ exists pa_q_b6_floor_product_square_product_start. pa_u_b6_floor_product_square_product = pa_q_b6_floor_product_square_product_start * S ((S (0)) * pa_v_b6_floor_product_square_product) + (1))) /\ ((((exists pa_h_b6_floor_product_square_product_terminal. pa_h_b6_floor_product_square_product_terminal + S (v) = S ((S (2)) * pa_v_b6_floor_product_square_product)) /\ exists pa_q_b6_floor_product_square_product_terminal. pa_u_b6_floor_product_square_product = pa_q_b6_floor_product_square_product_terminal * S ((S (2)) * pa_v_b6_floor_product_square_product) + (v))) /\ forall pa_i_b6_floor_product_square_product. (exists pa_lt_b6_floor_product_square_product_bound. pa_lt_b6_floor_product_square_product_bound + S pa_i_b6_floor_product_square_product = 2) -> exists pa_p_b6_floor_product_square_product pa_r_b6_floor_product_square_product pa_s_b6_floor_product_square_product. ((((exists pa_h_b6_floor_product_square_product_factor. pa_h_b6_floor_product_square_product_factor + S (pa_p_b6_floor_product_square_product) = S ((S (pa_i_b6_floor_product_square_product)) * pa_c_b6_floor_product_square)) /\ exists pa_q_b6_floor_product_square_product_factor. pa_b_b6_floor_product_square = pa_q_b6_floor_product_square_product_factor * S ((S (pa_i_b6_floor_product_square_product)) * pa_c_b6_floor_product_square) + (pa_p_b6_floor_product_square_product))) /\ ((((exists pa_h_b6_floor_product_square_product_partial. pa_h_b6_floor_product_square_product_partial + S (pa_r_b6_floor_product_square_product) = S ((S (pa_i_b6_floor_product_square_product)) * pa_v_b6_floor_product_square_product)) /\ exists pa_q_b6_floor_product_square_product_partial. pa_u_b6_floor_product_square_product = pa_q_b6_floor_product_square_product_partial * S ((S (pa_i_b6_floor_product_square_product)) * pa_v_b6_floor_product_square_product) + (pa_r_b6_floor_product_square_product))) /\ ((((exists pa_h_b6_floor_product_square_product_successor. pa_h_b6_floor_product_square_product_successor + S (pa_s_b6_floor_product_square_product) = S ((S (S pa_i_b6_floor_product_square_product)) * pa_v_b6_floor_product_square_product)) /\ exists pa_q_b6_floor_product_square_product_successor. pa_u_b6_floor_product_square_product = pa_q_b6_floor_product_square_product_successor * S ((S (S pa_i_b6_floor_product_square_product)) * pa_v_b6_floor_product_square_product) + (pa_s_b6_floor_product_square_product))) /\ pa_s_b6_floor_product_square_product = pa_r_b6_floor_product_square_product * pa_p_b6_floor_product_square_product))))))))
  24. 0024specialize htotal (s + 1)
  25. 0025specialize htotal 2
  26. 0026exact htotal
  27. 0027cases hv_exists
  28. 0028have hv_square : x = (s + 1) * (s + 1)
  29. 0029specialize pow_two (s + 1)
  30. 0030specialize pow_two 2
  31. 0031specialize pow_two x
  32. 0032apply pow_two
  33. 0033refl
  34. 0034exact hv_exists_witness
  35. 0035have hbase : Le(2 · n,x)
    Exact native replay linehave hbase : exists bqb_le_gap_b6_floor_product_base_order. bqb_le_gap_b6_floor_product_base_order + (2 * n) = (x)
  36. 0036rewrite hv_square
  37. 0037rewrite hsucc
  38. 0038rewrite hsucc
  39. 0039exact hweak
  40. 0040have hu_exists : ∃ u. Pow(x,s,u)
    Exact native replay linehave hu_exists : exists u. (exists pa_b_b6_floor_product_square_outer pa_c_b6_floor_product_square_outer. ((forall pa_i_b6_floor_product_square_outer_repeat. (exists pa_lt_b6_floor_product_square_outer_repeat_bound. pa_lt_b6_floor_product_square_outer_repeat_bound + S pa_i_b6_floor_product_square_outer_repeat = s) -> (((exists pa_h_b6_floor_product_square_outer_repeat_decoded. pa_h_b6_floor_product_square_outer_repeat_decoded + S (x) = S ((S (pa_i_b6_floor_product_square_outer_repeat)) * pa_c_b6_floor_product_square_outer)) /\ exists pa_q_b6_floor_product_square_outer_repeat_decoded. pa_b_b6_floor_product_square_outer = pa_q_b6_floor_product_square_outer_repeat_decoded * S ((S (pa_i_b6_floor_product_square_outer_repeat)) * pa_c_b6_floor_product_square_outer) + (x)))) /\ (exists pa_u_b6_floor_product_square_outer_product pa_v_b6_floor_product_square_outer_product. ((((exists pa_h_b6_floor_product_square_outer_product_start. pa_h_b6_floor_product_square_outer_product_start + S (1) = S ((S (0)) * pa_v_b6_floor_product_square_outer_product)) /\ exists pa_q_b6_floor_product_square_outer_product_start. pa_u_b6_floor_product_square_outer_product = pa_q_b6_floor_product_square_outer_product_start * S ((S (0)) * pa_v_b6_floor_product_square_outer_product) + (1))) /\ ((((exists pa_h_b6_floor_product_square_outer_product_terminal. pa_h_b6_floor_product_square_outer_product_terminal + S (u) = S ((S (s)) * pa_v_b6_floor_product_square_outer_product)) /\ exists pa_q_b6_floor_product_square_outer_product_terminal. pa_u_b6_floor_product_square_outer_product = pa_q_b6_floor_product_square_outer_product_terminal * S ((S (s)) * pa_v_b6_floor_product_square_outer_product) + (u))) /\ forall pa_i_b6_floor_product_square_outer_product. (exists pa_lt_b6_floor_product_square_outer_product_bound. pa_lt_b6_floor_product_square_outer_product_bound + S pa_i_b6_floor_product_square_outer_product = s) -> exists pa_p_b6_floor_product_square_outer_product pa_r_b6_floor_product_square_outer_product pa_s_b6_floor_product_square_outer_product. ((((exists pa_h_b6_floor_product_square_outer_product_factor. pa_h_b6_floor_product_square_outer_product_factor + S (pa_p_b6_floor_product_square_outer_product) = S ((S (pa_i_b6_floor_product_square_outer_product)) * pa_c_b6_floor_product_square_outer)) /\ exists pa_q_b6_floor_product_square_outer_product_factor. pa_b_b6_floor_product_square_outer = pa_q_b6_floor_product_square_outer_product_factor * S ((S (pa_i_b6_floor_product_square_outer_product)) * pa_c_b6_floor_product_square_outer) + (pa_p_b6_floor_product_square_outer_product))) /\ ((((exists pa_h_b6_floor_product_square_outer_product_partial. pa_h_b6_floor_product_square_outer_product_partial + S (pa_r_b6_floor_product_square_outer_product) = S ((S (pa_i_b6_floor_product_square_outer_product)) * pa_v_b6_floor_product_square_outer_product)) /\ exists pa_q_b6_floor_product_square_outer_product_partial. pa_u_b6_floor_product_square_outer_product = pa_q_b6_floor_product_square_outer_product_partial * S ((S (pa_i_b6_floor_product_square_outer_product)) * pa_v_b6_floor_product_square_outer_product) + (pa_r_b6_floor_product_square_outer_product))) /\ ((((exists pa_h_b6_floor_product_square_outer_product_successor. pa_h_b6_floor_product_square_outer_product_successor + S (pa_s_b6_floor_product_square_outer_product) = S ((S (S pa_i_b6_floor_product_square_outer_product)) * pa_v_b6_floor_product_square_outer_product)) /\ exists pa_q_b6_floor_product_square_outer_product_successor. pa_u_b6_floor_product_square_outer_product = pa_q_b6_floor_product_square_outer_product_successor * S ((S (S pa_i_b6_floor_product_square_outer_product)) * pa_v_b6_floor_product_square_outer_product) + (pa_s_b6_floor_product_square_outer_product))) /\ pa_s_b6_floor_product_square_outer_product = pa_r_b6_floor_product_square_outer_product * pa_p_b6_floor_product_square_outer_product))))))))
  41. 0041specialize htotal x
  42. 0042specialize htotal s
  43. 0043exact htotal
  44. 0044cases hu_exists
  45. 0045have hpower : Le(A,x1)
    Exact native replay linehave hpower : exists bqb_le_gap_b6_floor_product_power_order. bqb_le_gap_b6_floor_product_power_order + (A) = (x1)
  46. 0046specialize pow_base_monotone (2 * n)
  47. 0047specialize pow_base_monotone x
  48. 0048specialize pow_base_monotone s
  49. 0049specialize pow_base_monotone A
  50. 0050specialize pow_base_monotone x1
  51. 0051apply pow_base_monotone
  52. 0052exact hbase
  53. 0053exact hA
  54. 0054exact hu_exists_witness
  55. 0055have hz_exists : ∃ z. Pow(s + 1,2 · s,z)
    Exact native replay linehave hz_exists : exists z. (exists pa_b_b6_floor_product_square_flat pa_c_b6_floor_product_square_flat. ((forall pa_i_b6_floor_product_square_flat_repeat. (exists pa_lt_b6_floor_product_square_flat_repeat_bound. pa_lt_b6_floor_product_square_flat_repeat_bound + S pa_i_b6_floor_product_square_flat_repeat = 2 * s) -> (((exists pa_h_b6_floor_product_square_flat_repeat_decoded. pa_h_b6_floor_product_square_flat_repeat_decoded + S (s + 1) = S ((S (pa_i_b6_floor_product_square_flat_repeat)) * pa_c_b6_floor_product_square_flat)) /\ exists pa_q_b6_floor_product_square_flat_repeat_decoded. pa_b_b6_floor_product_square_flat = pa_q_b6_floor_product_square_flat_repeat_decoded * S ((S (pa_i_b6_floor_product_square_flat_repeat)) * pa_c_b6_floor_product_square_flat) + (s + 1)))) /\ (exists pa_u_b6_floor_product_square_flat_product pa_v_b6_floor_product_square_flat_product. ((((exists pa_h_b6_floor_product_square_flat_product_start. pa_h_b6_floor_product_square_flat_product_start + S (1) = S ((S (0)) * pa_v_b6_floor_product_square_flat_product)) /\ exists pa_q_b6_floor_product_square_flat_product_start. pa_u_b6_floor_product_square_flat_product = pa_q_b6_floor_product_square_flat_product_start * S ((S (0)) * pa_v_b6_floor_product_square_flat_product) + (1))) /\ ((((exists pa_h_b6_floor_product_square_flat_product_terminal. pa_h_b6_floor_product_square_flat_product_terminal + S (z) = S ((S (2 * s)) * pa_v_b6_floor_product_square_flat_product)) /\ exists pa_q_b6_floor_product_square_flat_product_terminal. pa_u_b6_floor_product_square_flat_product = pa_q_b6_floor_product_square_flat_product_terminal * S ((S (2 * s)) * pa_v_b6_floor_product_square_flat_product) + (z))) /\ forall pa_i_b6_floor_product_square_flat_product. (exists pa_lt_b6_floor_product_square_flat_product_bound. pa_lt_b6_floor_product_square_flat_product_bound + S pa_i_b6_floor_product_square_flat_product = 2 * s) -> exists pa_p_b6_floor_product_square_flat_product pa_r_b6_floor_product_square_flat_product pa_s_b6_floor_product_square_flat_product. ((((exists pa_h_b6_floor_product_square_flat_product_factor. pa_h_b6_floor_product_square_flat_product_factor + S (pa_p_b6_floor_product_square_flat_product) = S ((S (pa_i_b6_floor_product_square_flat_product)) * pa_c_b6_floor_product_square_flat)) /\ exists pa_q_b6_floor_product_square_flat_product_factor. pa_b_b6_floor_product_square_flat = pa_q_b6_floor_product_square_flat_product_factor * S ((S (pa_i_b6_floor_product_square_flat_product)) * pa_c_b6_floor_product_square_flat) + (pa_p_b6_floor_product_square_flat_product))) /\ ((((exists pa_h_b6_floor_product_square_flat_product_partial. pa_h_b6_floor_product_square_flat_product_partial + S (pa_r_b6_floor_product_square_flat_product) = S ((S (pa_i_b6_floor_product_square_flat_product)) * pa_v_b6_floor_product_square_flat_product)) /\ exists pa_q_b6_floor_product_square_flat_product_partial. pa_u_b6_floor_product_square_flat_product = pa_q_b6_floor_product_square_flat_product_partial * S ((S (pa_i_b6_floor_product_square_flat_product)) * pa_v_b6_floor_product_square_flat_product) + (pa_r_b6_floor_product_square_flat_product))) /\ ((((exists pa_h_b6_floor_product_square_flat_product_successor. pa_h_b6_floor_product_square_flat_product_successor + S (pa_s_b6_floor_product_square_flat_product) = S ((S (S pa_i_b6_floor_product_square_flat_product)) * pa_v_b6_floor_product_square_flat_product)) /\ exists pa_q_b6_floor_product_square_flat_product_successor. pa_u_b6_floor_product_square_flat_product = pa_q_b6_floor_product_square_flat_product_successor * S ((S (S pa_i_b6_floor_product_square_flat_product)) * pa_v_b6_floor_product_square_flat_product) + (pa_s_b6_floor_product_square_flat_product))) /\ pa_s_b6_floor_product_square_flat_product = pa_r_b6_floor_product_square_flat_product * pa_p_b6_floor_product_square_flat_product))))))))
  56. 0056specialize htotal (s + 1)
  57. 0057specialize htotal (2 * s)
  58. 0058exact htotal
  59. 0059cases hz_exists
  60. 0060have huz : x1 = x2
  61. 0061specialize pow_mul_exp_from_total (s + 1)
  62. 0062specialize pow_mul_exp_from_total 2
  63. 0063specialize pow_mul_exp_from_total s
  64. 0064specialize pow_mul_exp_from_total (2 * s)
  65. 0065specialize pow_mul_exp_from_total x
  66. 0066specialize pow_mul_exp_from_total x1
  67. 0067specialize pow_mul_exp_from_total x2
  68. 0068apply pow_mul_exp_from_total
  69. 0069exact htotal
  70. 0070refl
  71. 0071exact hv_exists_witness
  72. 0072exact hu_exists_witness
  73. 0073exact hz_exists_witness
  74. 0074have hfactor : H = x2 * x
  75. 0075specialize pow_add (s + 1)
  76. 0076specialize pow_add (2 * s)
  77. 0077specialize pow_add 2
  78. 0078specialize pow_add (2 * s + 2)
  79. 0079specialize pow_add x2
  80. 0080specialize pow_add x
  81. 0081specialize pow_add H
  82. 0082apply pow_add
  83. 0083refl
  84. 0084exact hz_exists_witness
  85. 0085exact hv_exists_witness
  86. 0086exact hH
  87. 0087have hn_double_sum : Le(n,n + n)
    Exact native replay linehave hn_double_sum : exists k. k + n = n + n
  88. 0088specialize le_add_right n
  89. 0089specialize le_add_right n
  90. 0090exact le_add_right
  91. 0091have hdouble : 2 * n = n + n
  92. 0092specialize two_mul_eq_add_self n
  93. 0093exact two_mul_eq_add_self
  94. 0094have hn_double : Le(n,2 · n)
    Exact native replay linehave hn_double : exists bqb_le_gap_b6_floor_product_n_double. bqb_le_gap_b6_floor_product_n_double + (n) = (2 * n)
  95. 0095rewrite hdouble
  96. 0096exact hn_double_sum
  97. 0097have hn_square : Le(n,x)
    Exact native replay linehave hn_square : exists bqb_le_gap_b6_floor_product_n_square. bqb_le_gap_b6_floor_product_n_square + (n) = (x)
  98. 0098specialize le_trans n
  99. 0099specialize le_trans (2 * n)
  100. 0100specialize le_trans x
  101. 0101apply le_trans
  102. 0102exact hn_double
  103. 0103exact hbase
  104. 0104have hAz : Le(A,x2)
    Exact native replay linehave hAz : exists k. k + A = x2
  105. 0105rewrite <- huz
  106. 0106exact hpower
  107. 0107have hproduct : Le(n · A,x · x2)
    Exact native replay linehave hproduct : exists bqb_le_gap_b6_floor_product_intermediate. bqb_le_gap_b6_floor_product_intermediate + (n * A) = (x * x2)
  108. 0108specialize mul_le_mul n
  109. 0109specialize mul_le_mul x
  110. 0110specialize mul_le_mul A
  111. 0111specialize mul_le_mul x2
  112. 0112apply mul_le_mul
  113. 0113exact hn_square
  114. 0114exact hAz
  115. 0115have hcomm : x * x2 = x2 * x
  116. 0116specialize mul_comm x
  117. 0117specialize mul_comm x2
  118. 0118exact mul_comm
  119. 0119rewrite hcomm at hproduct
  120. 0120rewrite <- hfactor at hproduct
  121. 0121exact hproduct