BT00SS

prime_power_quotient_prefix_last_zero

Alpha body-checked · checked-use disabled

The final entry of a length-(n+1) old quotient prefix is zero.

Exact expanded PA statement

forall p n b c. ((~(p = 1) /\ forall frm_prime_left_blrr_tail_prime frm_prime_right_blrr_tail_prime. p = frm_prime_left_blrr_tail_prime * frm_prime_right_blrr_tail_prime -> frm_prime_left_blrr_tail_prime = 1 \/ frm_prime_right_blrr_tail_prime = 1)) -> (forall bls_index_blrr_tail_prefix. (exists bls_gap_blrr_tail_prefix_bound. bls_gap_blrr_tail_prefix_bound + S (bls_index_blrr_tail_prefix) = (S n)) -> exists bls_power_blrr_tail_prefix bls_quotient_blrr_tail_prefix bls_remainder_blrr_tail_prefix. ((exists bpvi_b_bls_blrr_tail_prefix_power bpvi_c_bls_blrr_tail_prefix_power. ((forall bpvi_i_bls_blrr_tail_prefix_power. (exists bpvi_repeat_gap_bls_blrr_tail_prefix_power. bpvi_repeat_gap_bls_blrr_tail_prefix_power + S bpvi_i_bls_blrr_tail_prefix_power = S bls_index_blrr_tail_prefix) -> (((exists bpvi_h_bls_blrr_tail_prefix_power_repeat. bpvi_h_bls_blrr_tail_prefix_power_repeat + S (p) = S ((S (bpvi_i_bls_blrr_tail_prefix_power)) * bpvi_c_bls_blrr_tail_prefix_power)) /\ exists bpvi_q_bls_blrr_tail_prefix_power_repeat. bpvi_b_bls_blrr_tail_prefix_power = bpvi_q_bls_blrr_tail_prefix_power_repeat * S ((S (bpvi_i_bls_blrr_tail_prefix_power)) * bpvi_c_bls_blrr_tail_prefix_power) + (p)))) /\ (exists bpvi_u_bls_blrr_tail_prefix_power bpvi_v_bls_blrr_tail_prefix_power. ((((exists bpvi_h_bls_blrr_tail_prefix_power_start. bpvi_h_bls_blrr_tail_prefix_power_start + S (1) = S ((S (0)) * bpvi_v_bls_blrr_tail_prefix_power)) /\ exists bpvi_q_bls_blrr_tail_prefix_power_start. bpvi_u_bls_blrr_tail_prefix_power = bpvi_q_bls_blrr_tail_prefix_power_start * S ((S (0)) * bpvi_v_bls_blrr_tail_prefix_power) + (1))) /\ ((((exists bpvi_h_bls_blrr_tail_prefix_power_terminal. bpvi_h_bls_blrr_tail_prefix_power_terminal + S (bls_power_blrr_tail_prefix) = S ((S (S bls_index_blrr_tail_prefix)) * bpvi_v_bls_blrr_tail_prefix_power)) /\ exists bpvi_q_bls_blrr_tail_prefix_power_terminal. bpvi_u_bls_blrr_tail_prefix_power = bpvi_q_bls_blrr_tail_prefix_power_terminal * S ((S (S bls_index_blrr_tail_prefix)) * bpvi_v_bls_blrr_tail_prefix_power) + (bls_power_blrr_tail_prefix))) /\ forall bpvi_j_bls_blrr_tail_prefix_power. (exists bpvi_product_gap_bls_blrr_tail_prefix_power. bpvi_product_gap_bls_blrr_tail_prefix_power + S bpvi_j_bls_blrr_tail_prefix_power = S bls_index_blrr_tail_prefix) -> exists bpvi_factor_bls_blrr_tail_prefix_power bpvi_partial_bls_blrr_tail_prefix_power bpvi_successor_bls_blrr_tail_prefix_power. ((((exists bpvi_h_bls_blrr_tail_prefix_power_factor. bpvi_h_bls_blrr_tail_prefix_power_factor + S (bpvi_factor_bls_blrr_tail_prefix_power) = S ((S (bpvi_j_bls_blrr_tail_prefix_power)) * bpvi_c_bls_blrr_tail_prefix_power)) /\ exists bpvi_q_bls_blrr_tail_prefix_power_factor. bpvi_b_bls_blrr_tail_prefix_power = bpvi_q_bls_blrr_tail_prefix_power_factor * S ((S (bpvi_j_bls_blrr_tail_prefix_power)) * bpvi_c_bls_blrr_tail_prefix_power) + (bpvi_factor_bls_blrr_tail_prefix_power))) /\ ((((exists bpvi_h_bls_blrr_tail_prefix_power_partial. bpvi_h_bls_blrr_tail_prefix_power_partial + S (bpvi_partial_bls_blrr_tail_prefix_power) = S ((S (bpvi_j_bls_blrr_tail_prefix_power)) * bpvi_v_bls_blrr_tail_prefix_power)) /\ exists bpvi_q_bls_blrr_tail_prefix_power_partial. bpvi_u_bls_blrr_tail_prefix_power = bpvi_q_bls_blrr_tail_prefix_power_partial * S ((S (bpvi_j_bls_blrr_tail_prefix_power)) * bpvi_v_bls_blrr_tail_prefix_power) + (bpvi_partial_bls_blrr_tail_prefix_power))) /\ ((((exists bpvi_h_bls_blrr_tail_prefix_power_successor. bpvi_h_bls_blrr_tail_prefix_power_successor + S (bpvi_successor_bls_blrr_tail_prefix_power) = S ((S (S bpvi_j_bls_blrr_tail_prefix_power)) * bpvi_v_bls_blrr_tail_prefix_power)) /\ exists bpvi_q_bls_blrr_tail_prefix_power_successor. bpvi_u_bls_blrr_tail_prefix_power = bpvi_q_bls_blrr_tail_prefix_power_successor * S ((S (S bpvi_j_bls_blrr_tail_prefix_power)) * bpvi_v_bls_blrr_tail_prefix_power) + (bpvi_successor_bls_blrr_tail_prefix_power))) /\ bpvi_successor_bls_blrr_tail_prefix_power = bpvi_partial_bls_blrr_tail_prefix_power * bpvi_factor_bls_blrr_tail_prefix_power)))))))) /\ ((((exists ff_h_bls_blrr_tail_prefix_quotient_entry. ff_h_bls_blrr_tail_prefix_quotient_entry + S (bls_quotient_blrr_tail_prefix) = S ((S (bls_index_blrr_tail_prefix)) * c)) /\ exists ff_q_bls_blrr_tail_prefix_quotient_entry. b = ff_q_bls_blrr_tail_prefix_quotient_entry * S ((S (bls_index_blrr_tail_prefix)) * c) + (bls_quotient_blrr_tail_prefix))) /\ ((n = bls_power_blrr_tail_prefix * bls_quotient_blrr_tail_prefix + bls_remainder_blrr_tail_prefix /\ exists bls_remainder_gap_blrr_tail_prefix_division. bls_remainder_gap_blrr_tail_prefix_division + S (bls_remainder_blrr_tail_prefix) = bls_power_blrr_tail_prefix))))) -> (((exists fs_h_blrr_tail_zero. fs_h_blrr_tail_zero + S (0) = S ((S (n)) * c)) /\ exists fs_q_blrr_tail_zero. b = fs_q_blrr_tail_zero * S ((S (n)) * c) + (0)))

Structural proof guide

The final entry of a length-(n+1) old quotient prefix is zero.

Direct prerequisites: prime_power_quotient_tail_zero, division_remainder_unique, zero_add. The authored body proceeds by case analysis (8), intermediate claims (3), equality transport (2).

Proof neighborhood

Direct dependencies

BT00SA prime_power_quotient_tail_zero BT001U division_remainder_unique BT0000 zero_add

Direct dependents

BT00ST legendre_sum_zero_extended_prefix

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro p
  2. 0002intro n
  3. 0003intro b
  4. 0004intro c
  5. 0005intro hp
  6. 0006intro hprefix
  7. 0007have hdata : exists D q r. ((exists bpvi_b_blrr_tail_stored_power bpvi_c_blrr_tail_stored_power. ((forall bpvi_i_blrr_tail_stored_power. (exists bpvi_repeat_gap_blrr_tail_stored_power. bpvi_repeat_gap_blrr_tail_stored_power + S bpvi_i_blrr_tail_stored_power = S n) -> (((exists bpvi_h_blrr_tail_stored_power_repeat. bpvi_h_blrr_tail_stored_power_repeat + S (p) = S ((S (bpvi_i_blrr_tail_stored_power)) * bpvi_c_blrr_tail_stored_power)) /\ exists bpvi_q_blrr_tail_stored_power_repeat. bpvi_b_blrr_tail_stored_power = bpvi_q_blrr_tail_stored_power_repeat * S ((S (bpvi_i_blrr_tail_stored_power)) * bpvi_c_blrr_tail_stored_power) + (p)))) /\ (exists bpvi_u_blrr_tail_stored_power bpvi_v_blrr_tail_stored_power. ((((exists bpvi_h_blrr_tail_stored_power_start. bpvi_h_blrr_tail_stored_power_start + S (1) = S ((S (0)) * bpvi_v_blrr_tail_stored_power)) /\ exists bpvi_q_blrr_tail_stored_power_start. bpvi_u_blrr_tail_stored_power = bpvi_q_blrr_tail_stored_power_start * S ((S (0)) * bpvi_v_blrr_tail_stored_power) + (1))) /\ ((((exists bpvi_h_blrr_tail_stored_power_terminal. bpvi_h_blrr_tail_stored_power_terminal + S (D) = S ((S (S n)) * bpvi_v_blrr_tail_stored_power)) /\ exists bpvi_q_blrr_tail_stored_power_terminal. bpvi_u_blrr_tail_stored_power = bpvi_q_blrr_tail_stored_power_terminal * S ((S (S n)) * bpvi_v_blrr_tail_stored_power) + (D))) /\ forall bpvi_j_blrr_tail_stored_power. (exists bpvi_product_gap_blrr_tail_stored_power. bpvi_product_gap_blrr_tail_stored_power + S bpvi_j_blrr_tail_stored_power = S n) -> exists bpvi_factor_blrr_tail_stored_power bpvi_partial_blrr_tail_stored_power bpvi_successor_blrr_tail_stored_power. ((((exists bpvi_h_blrr_tail_stored_power_factor. bpvi_h_blrr_tail_stored_power_factor + S (bpvi_factor_blrr_tail_stored_power) = S ((S (bpvi_j_blrr_tail_stored_power)) * bpvi_c_blrr_tail_stored_power)) /\ exists bpvi_q_blrr_tail_stored_power_factor. bpvi_b_blrr_tail_stored_power = bpvi_q_blrr_tail_stored_power_factor * S ((S (bpvi_j_blrr_tail_stored_power)) * bpvi_c_blrr_tail_stored_power) + (bpvi_factor_blrr_tail_stored_power))) /\ ((((exists bpvi_h_blrr_tail_stored_power_partial. bpvi_h_blrr_tail_stored_power_partial + S (bpvi_partial_blrr_tail_stored_power) = S ((S (bpvi_j_blrr_tail_stored_power)) * bpvi_v_blrr_tail_stored_power)) /\ exists bpvi_q_blrr_tail_stored_power_partial. bpvi_u_blrr_tail_stored_power = bpvi_q_blrr_tail_stored_power_partial * S ((S (bpvi_j_blrr_tail_stored_power)) * bpvi_v_blrr_tail_stored_power) + (bpvi_partial_blrr_tail_stored_power))) /\ ((((exists bpvi_h_blrr_tail_stored_power_successor. bpvi_h_blrr_tail_stored_power_successor + S (bpvi_successor_blrr_tail_stored_power) = S ((S (S bpvi_j_blrr_tail_stored_power)) * bpvi_v_blrr_tail_stored_power)) /\ exists bpvi_q_blrr_tail_stored_power_successor. bpvi_u_blrr_tail_stored_power = bpvi_q_blrr_tail_stored_power_successor * S ((S (S bpvi_j_blrr_tail_stored_power)) * bpvi_v_blrr_tail_stored_power) + (bpvi_successor_blrr_tail_stored_power))) /\ bpvi_successor_blrr_tail_stored_power = bpvi_partial_blrr_tail_stored_power * bpvi_factor_blrr_tail_stored_power)))))))) /\ ((((exists ff_h_blrr_tail_stored_entry. ff_h_blrr_tail_stored_entry + S (q) = S ((S (n)) * c)) /\ exists ff_q_blrr_tail_stored_entry. b = ff_q_blrr_tail_stored_entry * S ((S (n)) * c) + (q))) /\ ((n = D * q + r /\ exists gap. gap + S r = D))))
  8. 0008specialize hprefix n
  9. 0009apply hprefix
  10. 0010exists 0
  11. 0011specialize zero_add (S n)
  12. 0012exact zero_add
  13. 0013cases hdata
  14. 0014cases hdata_witness
  15. 0015cases hdata_witness_witness
  16. 0016cases hdata_witness_witness_witness
  17. 0017cases hdata_witness_witness_witness_right
  18. 0018cases hdata_witness_witness_witness_right_right
  19. 0019have htail : ((n = x * 0 + n /\ exists gap. gap + S n = x))
  20. 0020specialize prime_power_quotient_tail_zero p
  21. 0021specialize prime_power_quotient_tail_zero n
  22. 0022specialize prime_power_quotient_tail_zero x
  23. 0023apply prime_power_quotient_tail_zero
  24. 0024exact hp
  25. 0025exact hdata_witness_witness_witness_left
  26. 0026cases htail
  27. 0027have hunique : x1 = 0 /\ x2 = n
  28. 0028specialize division_remainder_unique x
  29. 0029specialize division_remainder_unique n
  30. 0030specialize division_remainder_unique x1
  31. 0031specialize division_remainder_unique x2
  32. 0032specialize division_remainder_unique 0
  33. 0033specialize division_remainder_unique n
  34. 0034apply division_remainder_unique
  35. 0035exact hdata_witness_witness_witness_right_right_left
  36. 0036exact hdata_witness_witness_witness_right_right_right
  37. 0037exact htail_left
  38. 0038exact htail_right
  39. 0039cases hunique
  40. 0040rewrite <- hunique_left
  41. 0041rewrite <- hunique_left
  42. 0042exact hdata_witness_witness_witness_right_left