PA00E0

distinct_odd_prime_row_bit_count_equals_division_quotient

Alpha v16 checked-use theorem · independently closed; not Stable

A semantic row BitCount is the quotient in its bounded nonzero division.

Exact expanded PA statement

forall p q h k i d r rb rc n. p = 2 * h + 1 -> q = 2 * k + 1 -> ((~(p = 1) /\ forall frp_prime_left_row_quotient_prime_p frp_prime_right_row_quotient_prime_p. p = frp_prime_left_row_quotient_prime_p * frp_prime_right_row_quotient_prime_p -> frp_prime_left_row_quotient_prime_p = 1 \/ frp_prime_right_row_quotient_prime_p = 1)) -> ((~(q = 1) /\ forall frp_prime_left_row_quotient_prime_q frp_prime_right_row_quotient_prime_q. q = frp_prime_left_row_quotient_prime_q * frp_prime_right_row_quotient_prime_q -> frp_prime_left_row_quotient_prime_q = 1 \/ frp_prime_right_row_quotient_prime_q = 1)) -> ~(p = q) -> (exists edt_lt_gap_row_quotient_row_bound. edt_lt_gap_row_quotient_row_bound + S (i) = h) -> (forall eri_column_row_quotient_source. (exists eri_gap_row_quotient_source_bound. eri_gap_row_quotient_source_bound + S (eri_column_row_quotient_source) = k) -> exists eri_bit_row_quotient_source. ((((exists ff_h_eri_row_quotient_source_decoded. ff_h_eri_row_quotient_source_decoded + S (eri_bit_row_quotient_source) = S ((S (eri_column_row_quotient_source)) * rc)) /\ exists ff_q_eri_row_quotient_source_decoded. rb = ff_q_eri_row_quotient_source_decoded * S ((S (eri_column_row_quotient_source)) * rc) + (eri_bit_row_quotient_source))) /\ (((eri_bit_row_quotient_source = 0 /\ ((exists eri_gap_row_quotient_source_choice_left. eri_gap_row_quotient_source_choice_left + S (q * S i) = p * S eri_column_row_quotient_source) /\ ~(exists eri_gap_row_quotient_source_choice_right. eri_gap_row_quotient_source_choice_right + S (p * S eri_column_row_quotient_source) = q * S i))) \/ (eri_bit_row_quotient_source = 1 /\ ((exists eri_gap_row_quotient_source_choice_right. eri_gap_row_quotient_source_choice_right + S (p * S eri_column_row_quotient_source) = q * S i) /\ ~(exists eri_gap_row_quotient_source_choice_left. eri_gap_row_quotient_source_choice_left + S (q * S i) = p * S eri_column_row_quotient_source))))))) -> (((exists ff_u_row_quotient_count_n_sum ff_v_row_quotient_count_n_sum. ((((exists ff_h_row_quotient_count_n_sum_start. ff_h_row_quotient_count_n_sum_start + S (0) = S ((S (0)) * ff_v_row_quotient_count_n_sum)) /\ exists ff_q_row_quotient_count_n_sum_start. ff_u_row_quotient_count_n_sum = ff_q_row_quotient_count_n_sum_start * S ((S (0)) * ff_v_row_quotient_count_n_sum) + (0))) /\ ((((exists ff_h_row_quotient_count_n_sum_terminal. ff_h_row_quotient_count_n_sum_terminal + S (n) = S ((S (k)) * ff_v_row_quotient_count_n_sum)) /\ exists ff_q_row_quotient_count_n_sum_terminal. ff_u_row_quotient_count_n_sum = ff_q_row_quotient_count_n_sum_terminal * S ((S (k)) * ff_v_row_quotient_count_n_sum) + (n))) /\ forall ff_i_row_quotient_count_n_sum. (exists ff_lt_row_quotient_count_n_sum_bound. ff_lt_row_quotient_count_n_sum_bound + S ff_i_row_quotient_count_n_sum = k) -> exists ff_a_row_quotient_count_n_sum ff_r_row_quotient_count_n_sum ff_s_row_quotient_count_n_sum. ((((exists ff_h_row_quotient_count_n_sum_summand. ff_h_row_quotient_count_n_sum_summand + S (ff_a_row_quotient_count_n_sum) = S ((S (ff_i_row_quotient_count_n_sum)) * rc)) /\ exists ff_q_row_quotient_count_n_sum_summand. rb = ff_q_row_quotient_count_n_sum_summand * S ((S (ff_i_row_quotient_count_n_sum)) * rc) + (ff_a_row_quotient_count_n_sum))) /\ ((((exists ff_h_row_quotient_count_n_sum_partial. ff_h_row_quotient_count_n_sum_partial + S (ff_r_row_quotient_count_n_sum) = S ((S (ff_i_row_quotient_count_n_sum)) * ff_v_row_quotient_count_n_sum)) /\ exists ff_q_row_quotient_count_n_sum_partial. ff_u_row_quotient_count_n_sum = ff_q_row_quotient_count_n_sum_partial * S ((S (ff_i_row_quotient_count_n_sum)) * ff_v_row_quotient_count_n_sum) + (ff_r_row_quotient_count_n_sum))) /\ ((((exists ff_h_row_quotient_count_n_sum_successor. ff_h_row_quotient_count_n_sum_successor + S (ff_s_row_quotient_count_n_sum) = S ((S (S ff_i_row_quotient_count_n_sum)) * ff_v_row_quotient_count_n_sum)) /\ exists ff_q_row_quotient_count_n_sum_successor. ff_u_row_quotient_count_n_sum = ff_q_row_quotient_count_n_sum_successor * S ((S (S ff_i_row_quotient_count_n_sum)) * ff_v_row_quotient_count_n_sum) + (ff_s_row_quotient_count_n_sum))) /\ ff_s_row_quotient_count_n_sum = ff_r_row_quotient_count_n_sum + ff_a_row_quotient_count_n_sum)))))) /\ (forall ff_i_row_quotient_count_n_bits. (exists ff_lt_row_quotient_count_n_bits_bound. ff_lt_row_quotient_count_n_bits_bound + S ff_i_row_quotient_count_n_bits = k) -> exists ff_bit_row_quotient_count_n_bits. ((((exists ff_h_row_quotient_count_n_bits_decoded. ff_h_row_quotient_count_n_bits_decoded + S (ff_bit_row_quotient_count_n_bits) = S ((S (ff_i_row_quotient_count_n_bits)) * rc)) /\ exists ff_q_row_quotient_count_n_bits_decoded. rb = ff_q_row_quotient_count_n_bits_decoded * S ((S (ff_i_row_quotient_count_n_bits)) * rc) + (ff_bit_row_quotient_count_n_bits))) /\ (ff_bit_row_quotient_count_n_bits = 0 \/ ff_bit_row_quotient_count_n_bits = 1))))) -> q * S i = p * d + r -> (exists edt_lt_gap_row_quotient_remainder_bound. edt_lt_gap_row_quotient_remainder_bound + S (r) = p) -> n = d

Structural proof guide

Generated structural guide

A semantic row BitCount is the quotient in its bounded nonzero division.

Use the direct prerequisites distinct_primes_own_odd_half_scaled_remainder_nonzero, odd_half_division_quotient_bounded, eisenstein_row_indicator_prefix_to_initial_segment, eisenstein_initial_segment_bit_count_exact, bit_count_functional as previously established PA formulas.

The proof proceeds by intermediate claims (4).

Referenced ingredients

PA00DP distinct_primes_own_odd_half_scaled_remainder_nonzero PA00DR odd_half_division_quotient_bounded PA00DT eisenstein_row_indicator_prefix_to_initial_segment PA00DY eisenstein_initial_segment_bit_count_exact PA006Q bit_count_functional

Proof neighborhood

Direct dependencies

PA00DP distinct_primes_own_odd_half_scaled_remainder_nonzero PA00DR odd_half_division_quotient_bounded PA00DT eisenstein_row_indicator_prefix_to_initial_segment PA00DY eisenstein_initial_segment_bit_count_exact PA006Q bit_count_functional

Direct dependents

PA00E1 distinct_odd_prime_row_bit_count_equals_decoded_quotient

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  1. 0001intro p
  2. 0002intro q
  3. 0003intro h
  4. 0004intro k
  5. 0005intro i
  6. 0006intro d
  7. 0007intro r
  8. 0008intro rb
  9. 0009intro rc
  10. 0010intro n
  11. 0011intro hpodd
  12. 0012intro hqodd
  13. 0013intro hp
  14. 0014intro hq
  15. 0015intro hpq
  16. 0016intro hi
  17. 0017intro hrow
  18. 0018intro hcount
  19. 0019intro hdivision
  20. 0020intro hrp
  21. 0021have hr0 : ~(r = 0)
  22. 0022intro hrzero
  23. 0023specialize distinct_primes_own_odd_half_scaled_remainder_nonzero p
  24. 0024specialize distinct_primes_own_odd_half_scaled_remainder_nonzero q
  25. 0025specialize distinct_primes_own_odd_half_scaled_remainder_nonzero h
  26. 0026specialize distinct_primes_own_odd_half_scaled_remainder_nonzero i
  27. 0027specialize distinct_primes_own_odd_half_scaled_remainder_nonzero d
  28. 0028specialize distinct_primes_own_odd_half_scaled_remainder_nonzero r
  29. 0029apply distinct_primes_own_odd_half_scaled_remainder_nonzero
  30. 0030exact hpodd
  31. 0031exact hp
  32. 0032exact hq
  33. 0033exact hpq
  34. 0034exact hi
  35. 0035exact hdivision
  36. 0036exact hrzero
  37. 0037have hdle : exists edt_le_gap_row_quotient_quotient_bound. edt_le_gap_row_quotient_quotient_bound + (d) = k
  38. 0038specialize odd_half_division_quotient_bounded p
  39. 0039specialize odd_half_division_quotient_bounded q
  40. 0040specialize odd_half_division_quotient_bounded h
  41. 0041specialize odd_half_division_quotient_bounded k
  42. 0042specialize odd_half_division_quotient_bounded i
  43. 0043specialize odd_half_division_quotient_bounded d
  44. 0044specialize odd_half_division_quotient_bounded r
  45. 0045apply odd_half_division_quotient_bounded
  46. 0046exact hpodd
  47. 0047exact hqodd
  48. 0048exact hi
  49. 0049exact hdivision
  50. 0050have hinitial : forall eis_index_row_quotient_initial. (exists eis_lt_gap_row_quotient_initial_bound. eis_lt_gap_row_quotient_initial_bound + S (eis_index_row_quotient_initial) = k) -> exists eis_bit_row_quotient_initial. ((((exists ff_h_eis_row_quotient_initial_decoded. ff_h_eis_row_quotient_initial_decoded + S (eis_bit_row_quotient_initial) = S ((S (eis_index_row_quotient_initial)) * rc)) /\ exists ff_q_eis_row_quotient_initial_decoded. rb = ff_q_eis_row_quotient_initial_decoded * S ((S (eis_index_row_quotient_initial)) * rc) + (eis_bit_row_quotient_initial))) /\ (((eis_bit_row_quotient_initial = 1 /\ (exists eis_le_gap_row_quotient_initial_choice_inside. eis_le_gap_row_quotient_initial_choice_inside + (S eis_index_row_quotient_initial) = d)) \/ (eis_bit_row_quotient_initial = 0 /\ (exists eis_lt_gap_row_quotient_initial_choice_outside. eis_lt_gap_row_quotient_initial_choice_outside + S (d) = S eis_index_row_quotient_initial)))))
  51. 0051specialize eisenstein_row_indicator_prefix_to_initial_segment p
  52. 0052specialize eisenstein_row_indicator_prefix_to_initial_segment q
  53. 0053specialize eisenstein_row_indicator_prefix_to_initial_segment i
  54. 0054specialize eisenstein_row_indicator_prefix_to_initial_segment d
  55. 0055specialize eisenstein_row_indicator_prefix_to_initial_segment r
  56. 0056specialize eisenstein_row_indicator_prefix_to_initial_segment rb
  57. 0057specialize eisenstein_row_indicator_prefix_to_initial_segment rc
  58. 0058specialize eisenstein_row_indicator_prefix_to_initial_segment k
  59. 0059apply eisenstein_row_indicator_prefix_to_initial_segment
  60. 0060exact hrow
  61. 0061exact hdivision
  62. 0062exact hr0
  63. 0063exact hrp
  64. 0064have hcountd : ((exists ff_u_row_quotient_count_d_sum ff_v_row_quotient_count_d_sum. ((((exists ff_h_row_quotient_count_d_sum_start. ff_h_row_quotient_count_d_sum_start + S (0) = S ((S (0)) * ff_v_row_quotient_count_d_sum)) /\ exists ff_q_row_quotient_count_d_sum_start. ff_u_row_quotient_count_d_sum = ff_q_row_quotient_count_d_sum_start * S ((S (0)) * ff_v_row_quotient_count_d_sum) + (0))) /\ ((((exists ff_h_row_quotient_count_d_sum_terminal. ff_h_row_quotient_count_d_sum_terminal + S (d) = S ((S (k)) * ff_v_row_quotient_count_d_sum)) /\ exists ff_q_row_quotient_count_d_sum_terminal. ff_u_row_quotient_count_d_sum = ff_q_row_quotient_count_d_sum_terminal * S ((S (k)) * ff_v_row_quotient_count_d_sum) + (d))) /\ forall ff_i_row_quotient_count_d_sum. (exists ff_lt_row_quotient_count_d_sum_bound. ff_lt_row_quotient_count_d_sum_bound + S ff_i_row_quotient_count_d_sum = k) -> exists ff_a_row_quotient_count_d_sum ff_r_row_quotient_count_d_sum ff_s_row_quotient_count_d_sum. ((((exists ff_h_row_quotient_count_d_sum_summand. ff_h_row_quotient_count_d_sum_summand + S (ff_a_row_quotient_count_d_sum) = S ((S (ff_i_row_quotient_count_d_sum)) * rc)) /\ exists ff_q_row_quotient_count_d_sum_summand. rb = ff_q_row_quotient_count_d_sum_summand * S ((S (ff_i_row_quotient_count_d_sum)) * rc) + (ff_a_row_quotient_count_d_sum))) /\ ((((exists ff_h_row_quotient_count_d_sum_partial. ff_h_row_quotient_count_d_sum_partial + S (ff_r_row_quotient_count_d_sum) = S ((S (ff_i_row_quotient_count_d_sum)) * ff_v_row_quotient_count_d_sum)) /\ exists ff_q_row_quotient_count_d_sum_partial. ff_u_row_quotient_count_d_sum = ff_q_row_quotient_count_d_sum_partial * S ((S (ff_i_row_quotient_count_d_sum)) * ff_v_row_quotient_count_d_sum) + (ff_r_row_quotient_count_d_sum))) /\ ((((exists ff_h_row_quotient_count_d_sum_successor. ff_h_row_quotient_count_d_sum_successor + S (ff_s_row_quotient_count_d_sum) = S ((S (S ff_i_row_quotient_count_d_sum)) * ff_v_row_quotient_count_d_sum)) /\ exists ff_q_row_quotient_count_d_sum_successor. ff_u_row_quotient_count_d_sum = ff_q_row_quotient_count_d_sum_successor * S ((S (S ff_i_row_quotient_count_d_sum)) * ff_v_row_quotient_count_d_sum) + (ff_s_row_quotient_count_d_sum))) /\ ff_s_row_quotient_count_d_sum = ff_r_row_quotient_count_d_sum + ff_a_row_quotient_count_d_sum)))))) /\ (forall ff_i_row_quotient_count_d_bits. (exists ff_lt_row_quotient_count_d_bits_bound. ff_lt_row_quotient_count_d_bits_bound + S ff_i_row_quotient_count_d_bits = k) -> exists ff_bit_row_quotient_count_d_bits. ((((exists ff_h_row_quotient_count_d_bits_decoded. ff_h_row_quotient_count_d_bits_decoded + S (ff_bit_row_quotient_count_d_bits) = S ((S (ff_i_row_quotient_count_d_bits)) * rc)) /\ exists ff_q_row_quotient_count_d_bits_decoded. rb = ff_q_row_quotient_count_d_bits_decoded * S ((S (ff_i_row_quotient_count_d_bits)) * rc) + (ff_bit_row_quotient_count_d_bits))) /\ (ff_bit_row_quotient_count_d_bits = 0 \/ ff_bit_row_quotient_count_d_bits = 1))))
  65. 0065specialize eisenstein_initial_segment_bit_count_exact d
  66. 0066specialize eisenstein_initial_segment_bit_count_exact rb
  67. 0067specialize eisenstein_initial_segment_bit_count_exact rc
  68. 0068specialize eisenstein_initial_segment_bit_count_exact k
  69. 0069apply eisenstein_initial_segment_bit_count_exact
  70. 0070exact hinitial
  71. 0071exact hdle
  72. 0072specialize bit_count_functional rb
  73. 0073specialize bit_count_functional rc
  74. 0074specialize bit_count_functional k
  75. 0075specialize bit_count_functional n
  76. 0076specialize bit_count_functional d
  77. 0077apply bit_count_functional
  78. 0078exact hcount
  79. 0079exact hcountd