PC0030

prime_count_chebyshev_lower

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

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.

Exact expanded first-order arithmetic 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))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 10 declared prerequisites and contains 56 exact native proof lines.

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

Proof neighborhood

Direct dependencies

le_or_lt Stable theorem; checked-use authorized PC002F prime_count_chebyshev_lower_large PC000B prime_count_positive_above_one PC0024 binary_length_positive le_mul_of_one_le_right Alpha theorem; checked-use authorized le_trans Stable theorem; checked-use authorized mul_le_mul_left Stable theorem; checked-use authorized mul_one Stable theorem; checked-use authorized mul_assoc Stable theorem; checked-use authorized lt_to_le Stable theorem; checked-use authorized

Direct dependents

PC0031 prime_count_chebyshev_bounds

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

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 : (exists g. g + 8 = N) \/ (exists g. g + S N = 8)
  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 : exists g. g + 1 = k * ell
  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 : exists g. g + 8 * 1 = 8 * (k * ell)
  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 exact 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 : (exists g. g + 8 = N) \/ (exists g. g + S 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 : exists g. g + 1 = 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 : exists g. g + 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