PA0034

beta_half_range_entry_bounds

Stable checked-use theorem · independently closed

Entries 1 through h in an odd half-range are nonzero and below p.

Exact expanded PA statement

forall p h b c i x. p = 2 * h + 1 -> (forall gh_i_half. (exists gh_lt_half_bound. gh_lt_half_bound + S gh_i_half = h) -> (((exists gh_h_half. gh_h_half + S (1 + gh_i_half) = S ((S gh_i_half) * c)) /\ exists gh_q_half. b = gh_q_half * S ((S gh_i_half) * c) + (1 + gh_i_half)))) -> (exists gh_lt_half_i. gh_lt_half_i + S i = h) -> (((exists ff_h_half_i. ff_h_half_i + S (x) = S ((S (i)) * c)) /\ exists ff_q_half_i. b = ff_q_half_i * S ((S (i)) * c) + (x))) -> (~(x = 0) /\ (exists gh_lt_half_value. gh_lt_half_value + S x = p))

Structural proof guide

Generated structural guide

Entries 1 through h in an odd half-range are nonzero and below p.

Use the direct prerequisites beta_range_entry_eq, zero_add, add_succ_left, mul_succ_left, mul_zero_left, add_assoc, lt_of_le_of_lt as previously established PA formulas.

The proof proceeds by intermediate claims (5), equality transport (2), certified simplification (1).

Referenced ingredients

PA0032 beta_range_entry_eq PA0001 zero_add PA000E add_succ_left PA000G mul_succ_left PA000D mul_zero_left PA0009 add_assoc PA0033 lt_of_le_of_lt

Proof neighborhood

Direct dependencies

PA0032 beta_range_entry_eq PA0001 zero_add PA000E add_succ_left PA000G mul_succ_left PA000D mul_zero_left PA0009 add_assoc PA0033 lt_of_le_of_lt

Direct dependents

PA0072 gauss_half_range_signed_choices PA007C gauss_signed_half_magnitude_injective PA0083 prime_half_range_product_coprime

Formal native tactic body

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

  1. 0001intro p
  2. 0002intro h
  3. 0003intro b
  4. 0004intro c
  5. 0005intro i
  6. 0006intro x
  7. 0007intro hp
  8. 0008intro hrange
  9. 0009intro hi
  10. 0010intro hxi
  11. 0011have hx : x = 1 + i
  12. 0012specialize beta_range_entry_eq b
  13. 0013specialize beta_range_entry_eq c
  14. 0014specialize beta_range_entry_eq 1
  15. 0015specialize beta_range_entry_eq h
  16. 0016specialize beta_range_entry_eq i
  17. 0017specialize beta_range_entry_eq x
  18. 0018apply beta_range_entry_eq
  19. 0019exact hrange
  20. 0020exact hi
  21. 0021exact hxi
  22. 0022have hone : 1 + i = S i
  23. 0023trans S (0 + i)
  24. 0024specialize add_succ_left 0
  25. 0025specialize add_succ_left i
  26. 0026exact add_succ_left
  27. 0027congr
  28. 0028specialize zero_add i
  29. 0029exact zero_add
  30. 0030have hxsi : x = S i
  31. 0031trans 1 + i
  32. 0032exact hx
  33. 0033exact hone
  34. 0034split
  35. 0035intro hx0
  36. 0036apply PA1
  37. 0037trans x
  38. 0038symm
  39. 0039exact hxsi
  40. 0040exact hx0
  41. 0041have hxh : exists k. k + x = h
  42. 0042rewrite hxsi
  43. 0043exact hi
  44. 0044have hhp : exists k. k + S h = p
  45. 0045exists h
  46. 0046rewrite hp
  47. 0047simp [mul_succ_left, mul_zero_left, add_succ_left, zero_add, add_assoc]
  48. 0048specialize lt_of_le_of_lt x
  49. 0049specialize lt_of_le_of_lt h
  50. 0050specialize lt_of_le_of_lt p
  51. 0051apply lt_of_le_of_lt
  52. 0052exact hxh
  53. 0053exact hhp