PC0030

prime_count_chebyshev_lower

The exact effective Chebyshev lower bound N <= 8*pi(N)*BitLen(N), including every N at least two.

Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not Stable

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.

These are the exact finite integer inequalities with constant 8, for every N≥2. The proof uses constructive binomial and primorial infrastructure; it does not assume logarithms, asymptotic estimates, the prime number theorem, or a factorization oracle.

Exact theorem in conservative defined notation

∀ N. ∀ ell. ∀ k. Lt(1,N) → BitLen(N,ell) → PrimeCount(N,k) → Le(N,8 · k · ell)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

BitLen(n,ell) · 1PrimeCount(x,z) · 1Le(a,b) · 2Lt(a,b) · 4

Actual proof prerequisites

le_or_lt · checked external prerequisiteprime_count_chebyshev_lower_largeprime_count_positive_above_onebinary_length_positivele_mul_of_one_le_right · checked external prerequisitele_trans · checked external prerequisitemul_le_mul_left · checked external prerequisitemul_one · checked external prerequisitemul_assoc · checked external prerequisitelt_to_le · checked external prerequisite
Original expanded first-order statement 
forall N ell k. (exists pc_le_cheb_lower_positive. pc_le_cheb_lower_positive + (2) = (N)) -> ((((N) = 0 /\ (ell) = 1) \/ exists ff_exponent_bl_pc_cheb_lower_length ff_lower_bl_pc_cheb_lower_length ff_upper_bl_pc_cheb_lower_length. (((ell) = S ff_exponent_bl_pc_cheb_lower_length) /\ ((exists ff_positive_bl_pc_cheb_lower_length. ff_positive_bl_pc_cheb_lower_length + 1 = (N)) /\ ((exists pa_b_bl_pc_cheb_lower_length_lower pa_c_bl_pc_cheb_lower_length_lower. ((forall pa_i_bl_pc_cheb_lower_length_lower_repeat. (exists pa_lt_bl_pc_cheb_lower_length_lower_repeat_bound. pa_lt_bl_pc_cheb_lower_length_lower_repeat_bound + S pa_i_bl_pc_cheb_lower_length_lower_repeat = ff_exponent_bl_pc_cheb_lower_length) -> (((exists pa_h_bl_pc_cheb_lower_length_lower_repeat_decoded. pa_h_bl_pc_cheb_lower_length_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_pc_cheb_lower_length_lower_repeat)) * pa_c_bl_pc_cheb_lower_length_lower)) /\ exists pa_q_bl_pc_cheb_lower_length_lower_repeat_decoded. pa_b_bl_pc_cheb_lower_length_lower = pa_q_bl_pc_cheb_lower_length_lower_repeat_decoded * S ((S (pa_i_bl_pc_cheb_lower_length_lower_repeat)) * pa_c_bl_pc_cheb_lower_length_lower) + (2)))) /\ (exists pa_u_bl_pc_cheb_lower_length_lower_product pa_v_bl_pc_cheb_lower_length_lower_product. ((((exists pa_h_bl_pc_cheb_lower_length_lower_product_start. pa_h_bl_pc_cheb_lower_length_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_pc_cheb_lower_length_lower_product)) /\ exists pa_q_bl_pc_cheb_lower_length_lower_product_start. pa_u_bl_pc_cheb_lower_length_lower_product = pa_q_bl_pc_cheb_lower_length_lower_product_start * S ((S (0)) * pa_v_bl_pc_cheb_lower_length_lower_product) + (1))) /\ ((((exists pa_h_bl_pc_cheb_lower_length_lower_product_terminal. pa_h_bl_pc_cheb_lower_length_lower_product_terminal + S (ff_lower_bl_pc_cheb_lower_length) = S ((S (ff_exponent_bl_pc_cheb_lower_length)) * pa_v_bl_pc_cheb_lower_length_lower_product)) /\ exists pa_q_bl_pc_cheb_lower_length_lower_product_terminal. pa_u_bl_pc_cheb_lower_length_lower_product = pa_q_bl_pc_cheb_lower_length_lower_product_terminal * S ((S (ff_exponent_bl_pc_cheb_lower_length)) * pa_v_bl_pc_cheb_lower_length_lower_product) + (ff_lower_bl_pc_cheb_lower_length))) /\ forall pa_i_bl_pc_cheb_lower_length_lower_product. (exists pa_lt_bl_pc_cheb_lower_length_lower_product_bound. pa_lt_bl_pc_cheb_lower_length_lower_product_bound + S pa_i_bl_pc_cheb_lower_length_lower_product = ff_exponent_bl_pc_cheb_lower_length) -> exists pa_p_bl_pc_cheb_lower_length_lower_product pa_r_bl_pc_cheb_lower_length_lower_product pa_s_bl_pc_cheb_lower_length_lower_product. ((((exists pa_h_bl_pc_cheb_lower_length_lower_product_factor. pa_h_bl_pc_cheb_lower_length_lower_product_factor + S (pa_p_bl_pc_cheb_lower_length_lower_product) = S ((S (pa_i_bl_pc_cheb_lower_length_lower_product)) * pa_c_bl_pc_cheb_lower_length_lower)) /\ exists pa_q_bl_pc_cheb_lower_length_lower_product_factor. pa_b_bl_pc_cheb_lower_length_lower = pa_q_bl_pc_cheb_lower_length_lower_product_factor * S ((S (pa_i_bl_pc_cheb_lower_length_lower_product)) * pa_c_bl_pc_cheb_lower_length_lower) + (pa_p_bl_pc_cheb_lower_length_lower_product))) /\ ((((exists pa_h_bl_pc_cheb_lower_length_lower_product_partial. pa_h_bl_pc_cheb_lower_length_lower_product_partial + S (pa_r_bl_pc_cheb_lower_length_lower_product) = S ((S (pa_i_bl_pc_cheb_lower_length_lower_product)) * pa_v_bl_pc_cheb_lower_length_lower_product)) /\ exists pa_q_bl_pc_cheb_lower_length_lower_product_partial. pa_u_bl_pc_cheb_lower_length_lower_product = pa_q_bl_pc_cheb_lower_length_lower_product_partial * S ((S (pa_i_bl_pc_cheb_lower_length_lower_product)) * pa_v_bl_pc_cheb_lower_length_lower_product) + (pa_r_bl_pc_cheb_lower_length_lower_product))) /\ ((((exists pa_h_bl_pc_cheb_lower_length_lower_product_successor. pa_h_bl_pc_cheb_lower_length_lower_product_successor + S (pa_s_bl_pc_cheb_lower_length_lower_product) = S ((S (S pa_i_bl_pc_cheb_lower_length_lower_product)) * pa_v_bl_pc_cheb_lower_length_lower_product)) /\ exists pa_q_bl_pc_cheb_lower_length_lower_product_successor. pa_u_bl_pc_cheb_lower_length_lower_product = pa_q_bl_pc_cheb_lower_length_lower_product_successor * S ((S (S pa_i_bl_pc_cheb_lower_length_lower_product)) * pa_v_bl_pc_cheb_lower_length_lower_product) + (pa_s_bl_pc_cheb_lower_length_lower_product))) /\ pa_s_bl_pc_cheb_lower_length_lower_product = pa_r_bl_pc_cheb_lower_length_lower_product * pa_p_bl_pc_cheb_lower_length_lower_product)))))))) /\ ((exists pa_b_bl_pc_cheb_lower_length_upper pa_c_bl_pc_cheb_lower_length_upper. ((forall pa_i_bl_pc_cheb_lower_length_upper_repeat. (exists pa_lt_bl_pc_cheb_lower_length_upper_repeat_bound. pa_lt_bl_pc_cheb_lower_length_upper_repeat_bound + S pa_i_bl_pc_cheb_lower_length_upper_repeat = ell) -> (((exists pa_h_bl_pc_cheb_lower_length_upper_repeat_decoded. pa_h_bl_pc_cheb_lower_length_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_pc_cheb_lower_length_upper_repeat)) * pa_c_bl_pc_cheb_lower_length_upper)) /\ exists pa_q_bl_pc_cheb_lower_length_upper_repeat_decoded. pa_b_bl_pc_cheb_lower_length_upper = pa_q_bl_pc_cheb_lower_length_upper_repeat_decoded * S ((S (pa_i_bl_pc_cheb_lower_length_upper_repeat)) * pa_c_bl_pc_cheb_lower_length_upper) + (2)))) /\ (exists pa_u_bl_pc_cheb_lower_length_upper_product pa_v_bl_pc_cheb_lower_length_upper_product. ((((exists pa_h_bl_pc_cheb_lower_length_upper_product_start. pa_h_bl_pc_cheb_lower_length_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_pc_cheb_lower_length_upper_product)) /\ exists pa_q_bl_pc_cheb_lower_length_upper_product_start. pa_u_bl_pc_cheb_lower_length_upper_product = pa_q_bl_pc_cheb_lower_length_upper_product_start * S ((S (0)) * pa_v_bl_pc_cheb_lower_length_upper_product) + (1))) /\ ((((exists pa_h_bl_pc_cheb_lower_length_upper_product_terminal. pa_h_bl_pc_cheb_lower_length_upper_product_terminal + S (ff_upper_bl_pc_cheb_lower_length) = S ((S (ell)) * pa_v_bl_pc_cheb_lower_length_upper_product)) /\ exists pa_q_bl_pc_cheb_lower_length_upper_product_terminal. pa_u_bl_pc_cheb_lower_length_upper_product = pa_q_bl_pc_cheb_lower_length_upper_product_terminal * S ((S (ell)) * pa_v_bl_pc_cheb_lower_length_upper_product) + (ff_upper_bl_pc_cheb_lower_length))) /\ forall pa_i_bl_pc_cheb_lower_length_upper_product. (exists pa_lt_bl_pc_cheb_lower_length_upper_product_bound. pa_lt_bl_pc_cheb_lower_length_upper_product_bound + S pa_i_bl_pc_cheb_lower_length_upper_product = ell) -> exists pa_p_bl_pc_cheb_lower_length_upper_product pa_r_bl_pc_cheb_lower_length_upper_product pa_s_bl_pc_cheb_lower_length_upper_product. ((((exists pa_h_bl_pc_cheb_lower_length_upper_product_factor. pa_h_bl_pc_cheb_lower_length_upper_product_factor + S (pa_p_bl_pc_cheb_lower_length_upper_product) = S ((S (pa_i_bl_pc_cheb_lower_length_upper_product)) * pa_c_bl_pc_cheb_lower_length_upper)) /\ exists pa_q_bl_pc_cheb_lower_length_upper_product_factor. pa_b_bl_pc_cheb_lower_length_upper = pa_q_bl_pc_cheb_lower_length_upper_product_factor * S ((S (pa_i_bl_pc_cheb_lower_length_upper_product)) * pa_c_bl_pc_cheb_lower_length_upper) + (pa_p_bl_pc_cheb_lower_length_upper_product))) /\ ((((exists pa_h_bl_pc_cheb_lower_length_upper_product_partial. pa_h_bl_pc_cheb_lower_length_upper_product_partial + S (pa_r_bl_pc_cheb_lower_length_upper_product) = S ((S (pa_i_bl_pc_cheb_lower_length_upper_product)) * pa_v_bl_pc_cheb_lower_length_upper_product)) /\ exists pa_q_bl_pc_cheb_lower_length_upper_product_partial. pa_u_bl_pc_cheb_lower_length_upper_product = pa_q_bl_pc_cheb_lower_length_upper_product_partial * S ((S (pa_i_bl_pc_cheb_lower_length_upper_product)) * pa_v_bl_pc_cheb_lower_length_upper_product) + (pa_r_bl_pc_cheb_lower_length_upper_product))) /\ ((((exists pa_h_bl_pc_cheb_lower_length_upper_product_successor. pa_h_bl_pc_cheb_lower_length_upper_product_successor + S (pa_s_bl_pc_cheb_lower_length_upper_product) = S ((S (S pa_i_bl_pc_cheb_lower_length_upper_product)) * pa_v_bl_pc_cheb_lower_length_upper_product)) /\ exists pa_q_bl_pc_cheb_lower_length_upper_product_successor. pa_u_bl_pc_cheb_lower_length_upper_product = pa_q_bl_pc_cheb_lower_length_upper_product_successor * S ((S (S pa_i_bl_pc_cheb_lower_length_upper_product)) * pa_v_bl_pc_cheb_lower_length_upper_product) + (pa_s_bl_pc_cheb_lower_length_upper_product))) /\ pa_s_bl_pc_cheb_lower_length_upper_product = pa_r_bl_pc_cheb_lower_length_upper_product * pa_p_bl_pc_cheb_lower_length_upper_product)))))))) /\ ((exists ff_lower_gap_bl_pc_cheb_lower_length. ff_lower_gap_bl_pc_cheb_lower_length + (ff_lower_bl_pc_cheb_lower_length) = (N)) /\ (exists ff_upper_gap_bl_pc_cheb_lower_length. ff_upper_gap_bl_pc_cheb_lower_length + S (N) = (ff_upper_bl_pc_cheb_lower_length))))))))) -> (exists pc_code_cheb_lower_count pc_scale_cheb_lower_count. (forall pc_index_cheb_lower_count_mask. (exists pc_lt_cheb_lower_count_mask_bound. pc_lt_cheb_lower_count_mask_bound + S (pc_index_cheb_lower_count_mask) = (N)) -> exists pc_bit_cheb_lower_count_mask. (((exists fs_h_pc_cheb_lower_count_mask_entry. fs_h_pc_cheb_lower_count_mask_entry + S (pc_bit_cheb_lower_count_mask) = S ((S (pc_index_cheb_lower_count_mask)) * pc_scale_cheb_lower_count)) /\ exists fs_q_pc_cheb_lower_count_mask_entry. pc_code_cheb_lower_count = fs_q_pc_cheb_lower_count_mask_entry * S ((S (pc_index_cheb_lower_count_mask)) * pc_scale_cheb_lower_count) + (pc_bit_cheb_lower_count_mask))) /\ (((((~(S (pc_index_cheb_lower_count_mask) = 1) /\ forall bpr_left_pc_cheb_lower_count_mask_choice_prime bpr_right_pc_cheb_lower_count_mask_choice_prime. S (pc_index_cheb_lower_count_mask) = bpr_left_pc_cheb_lower_count_mask_choice_prime * bpr_right_pc_cheb_lower_count_mask_choice_prime -> bpr_left_pc_cheb_lower_count_mask_choice_prime = 1 \/ bpr_right_pc_cheb_lower_count_mask_choice_prime = 1)) /\ pc_bit_cheb_lower_count_mask = 1) \/ (~((~(S (pc_index_cheb_lower_count_mask) = 1) /\ forall bpr_left_pc_cheb_lower_count_mask_choice_prime bpr_right_pc_cheb_lower_count_mask_choice_prime. S (pc_index_cheb_lower_count_mask) = bpr_left_pc_cheb_lower_count_mask_choice_prime * bpr_right_pc_cheb_lower_count_mask_choice_prime -> bpr_left_pc_cheb_lower_count_mask_choice_prime = 1 \/ bpr_right_pc_cheb_lower_count_mask_choice_prime = 1)) /\ pc_bit_cheb_lower_count_mask = 0)))) /\ (exists fs_u_pc_cheb_lower_count_sum fs_v_pc_cheb_lower_count_sum. ((((exists fs_h_pc_cheb_lower_count_sum_body_start. fs_h_pc_cheb_lower_count_sum_body_start + S (0) = S ((S (0)) * fs_v_pc_cheb_lower_count_sum)) /\ exists fs_q_pc_cheb_lower_count_sum_body_start. fs_u_pc_cheb_lower_count_sum = fs_q_pc_cheb_lower_count_sum_body_start * S ((S (0)) * fs_v_pc_cheb_lower_count_sum) + (0))) /\ ((((exists fs_h_pc_cheb_lower_count_sum_body_terminal. fs_h_pc_cheb_lower_count_sum_body_terminal + S (k) = S ((S (N)) * fs_v_pc_cheb_lower_count_sum)) /\ exists fs_q_pc_cheb_lower_count_sum_body_terminal. fs_u_pc_cheb_lower_count_sum = fs_q_pc_cheb_lower_count_sum_body_terminal * S ((S (N)) * fs_v_pc_cheb_lower_count_sum) + (k))) /\ forall fs_i_pc_cheb_lower_count_sum_body_steps. (exists fs_lt_pc_cheb_lower_count_sum_body_steps_bound. fs_lt_pc_cheb_lower_count_sum_body_steps_bound + S fs_i_pc_cheb_lower_count_sum_body_steps = N) -> exists fs_a_pc_cheb_lower_count_sum_body_steps fs_r_pc_cheb_lower_count_sum_body_steps fs_s_pc_cheb_lower_count_sum_body_steps. ((((exists fs_h_pc_cheb_lower_count_sum_body_steps_summand. fs_h_pc_cheb_lower_count_sum_body_steps_summand + S (fs_a_pc_cheb_lower_count_sum_body_steps) = S ((S (fs_i_pc_cheb_lower_count_sum_body_steps)) * pc_scale_cheb_lower_count)) /\ exists fs_q_pc_cheb_lower_count_sum_body_steps_summand. pc_code_cheb_lower_count = fs_q_pc_cheb_lower_count_sum_body_steps_summand * S ((S (fs_i_pc_cheb_lower_count_sum_body_steps)) * pc_scale_cheb_lower_count) + (fs_a_pc_cheb_lower_count_sum_body_steps))) /\ ((((exists fs_h_pc_cheb_lower_count_sum_body_steps_partial. fs_h_pc_cheb_lower_count_sum_body_steps_partial + S (fs_r_pc_cheb_lower_count_sum_body_steps) = S ((S (fs_i_pc_cheb_lower_count_sum_body_steps)) * fs_v_pc_cheb_lower_count_sum)) /\ exists fs_q_pc_cheb_lower_count_sum_body_steps_partial. fs_u_pc_cheb_lower_count_sum = fs_q_pc_cheb_lower_count_sum_body_steps_partial * S ((S (fs_i_pc_cheb_lower_count_sum_body_steps)) * fs_v_pc_cheb_lower_count_sum) + (fs_r_pc_cheb_lower_count_sum_body_steps))) /\ ((((exists fs_h_pc_cheb_lower_count_sum_body_steps_successor. fs_h_pc_cheb_lower_count_sum_body_steps_successor + S (fs_s_pc_cheb_lower_count_sum_body_steps) = S ((S (S fs_i_pc_cheb_lower_count_sum_body_steps)) * fs_v_pc_cheb_lower_count_sum)) /\ exists fs_q_pc_cheb_lower_count_sum_body_steps_successor. fs_u_pc_cheb_lower_count_sum = fs_q_pc_cheb_lower_count_sum_body_steps_successor * S ((S (S fs_i_pc_cheb_lower_count_sum_body_steps)) * fs_v_pc_cheb_lower_count_sum) + (fs_s_pc_cheb_lower_count_sum_body_steps))) /\ fs_s_pc_cheb_lower_count_sum_body_steps = fs_r_pc_cheb_lower_count_sum_body_steps + fs_a_pc_cheb_lower_count_sum_body_steps))))))) -> (exists pc_le_cheb_lower_result. pc_le_cheb_lower_result + (N) = (8 * k * ell))

Complete tactic proof in conservative notation

All 56 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

56 script commands · 10 reading checkpoints · 5 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 (3)
prime count chebyshev lower largeprime count positive above onebinary length positive
01Fix variables and assumptionsL1–6

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

  1. L1
    intro N
  2. L2
    intro ell
  3. L3
    intro k
  4. L4
    intro hN
  5. L5
    intro hl
  6. L6
    intro hk
02Establish hcL7–10

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

  1. L7
    have hc : Lt(7,N) ∨ Lt(N,8)Definitions: Lt(7,N)Lt(N,8)Original native command in the exact edition
  2. L8
    specialize le_or_lt 8
  3. L9
    specialize le_or_lt N
  4. L10
    apply le_or_lt
03Separate the logical casesL11–11

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

  1. L11
    cases hc
04Use earlier factsL12–18

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

  1. L12
    specialize prime_count_chebyshev_lower_large N
  2. L13
    specialize prime_count_chebyshev_lower_large ell
  3. L14
    specialize prime_count_chebyshev_lower_large k
  4. L15
    apply prime_count_chebyshev_lower_large
  5. L16
    exact hc_left
  6. L17
    exact hl
  7. L18
    exact hk
05Establish hpositiveL19–28

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

  1. L19
    have hpositive : Lt(0,k · ell)Definitions: Lt(0,k · ell)Original native command in the exact edition
  2. L20
    specialize le_trans 1
  3. L21
    specialize le_trans k
  4. L22
    specialize le_trans (k * ell)
  5. L23
    apply le_trans
  6. L24
    specialize prime_count_positive_above_one N
  7. L25
    specialize prime_count_positive_above_one k
  8. L26
    apply prime_count_positive_above_one
  9. L27
    exact hN
  10. L28
    exact hk
06Use earlier factsL29–35

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

  1. L29
    specialize le_mul_of_one_le_right k
  2. L30
    specialize le_mul_of_one_le_right ell
  3. L31
    apply le_mul_of_one_le_right
  4. L32
    specialize binary_length_positive N
  5. L33
    specialize binary_length_positive ell
  6. L34
    apply binary_length_positive
  7. L35
    exact hl
07Establish hscaleL36–41

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

  1. L36
    have hscale : Le(8 · 1,8 · (k · ell))Definitions: Le(8 · 1,8 · (k · ell))Original native command in the exact edition
  2. L37
    specialize mul_le_mul_left 1
  3. L38
    specialize mul_le_mul_left (k * ell)
  4. L39
    specialize mul_le_mul_left 8
  5. L40
    apply mul_le_mul_left
  6. L41
    exact hpositive
08Establish honeL42–44

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

  1. L42
    have hone : 8 * 1 = 8
  2. L43
    apply mul_one
  3. L44
    rewrite hone at hscale
09Establish hassocL45–54

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

  1. L45
    have hassoc : (8 * k) * ell = 8 * (k * ell)
  2. L46
    apply mul_assoc
  3. L47
    rewrite hassoc
  4. L48
    specialize le_trans N
  5. L49
    specialize le_trans 8
  6. L50
    specialize le_trans (8 * (k * ell))
  7. L51
    apply le_trans
  8. L52
    specialize lt_to_le N
  9. L53
    specialize lt_to_le 8
  10. L54
    apply lt_to_le
10Use earlier factsL55–56

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

  1. L55
    exact hc_right
  2. L56
    exact hscale

Library-wide reading audit

Original defined command ledger · 56 lines
  1. 0001intro N
  2. 0002intro ell
  3. 0003intro k
  4. 0004intro hN
  5. 0005intro hl
  6. 0006intro hk
  7. 0007have hc : Lt(7,N) ∨ Lt(N,8)
  8. 0008specialize le_or_lt 8
  9. 0009specialize le_or_lt N
  10. 0010apply le_or_lt
  11. 0011cases hc
  12. 0012specialize prime_count_chebyshev_lower_large N
  13. 0013specialize prime_count_chebyshev_lower_large ell
  14. 0014specialize prime_count_chebyshev_lower_large k
  15. 0015apply prime_count_chebyshev_lower_large
  16. 0016exact hc_left
  17. 0017exact hl
  18. 0018exact hk
  19. 0019have hpositive : Lt(0,k · ell)
  20. 0020specialize le_trans 1
  21. 0021specialize le_trans k
  22. 0022specialize le_trans (k * ell)
  23. 0023apply le_trans
  24. 0024specialize prime_count_positive_above_one N
  25. 0025specialize prime_count_positive_above_one k
  26. 0026apply prime_count_positive_above_one
  27. 0027exact hN
  28. 0028exact hk
  29. 0029specialize le_mul_of_one_le_right k
  30. 0030specialize le_mul_of_one_le_right ell
  31. 0031apply le_mul_of_one_le_right
  32. 0032specialize binary_length_positive N
  33. 0033specialize binary_length_positive ell
  34. 0034apply binary_length_positive
  35. 0035exact hl
  36. 0036have hscale : Le(8 · 1,8 · (k · ell))
  37. 0037specialize mul_le_mul_left 1
  38. 0038specialize mul_le_mul_left (k * ell)
  39. 0039specialize mul_le_mul_left 8
  40. 0040apply mul_le_mul_left
  41. 0041exact hpositive
  42. 0042have hone : 8 * 1 = 8
  43. 0043apply mul_one
  44. 0044rewrite hone at hscale
  45. 0045have hassoc : (8 * k) * ell = 8 * (k * ell)
  46. 0046apply mul_assoc
  47. 0047rewrite hassoc
  48. 0048specialize le_trans N
  49. 0049specialize le_trans 8
  50. 0050specialize le_trans (8 * (k * ell))
  51. 0051apply le_trans
  52. 0052specialize lt_to_le N
  53. 0053specialize lt_to_le 8
  54. 0054apply lt_to_le
  55. 0055exact hc_right
  56. 0056exact hscale