PA00D9

distinct_odd_prime_half_cell_oriented

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

Every bounded half-rectangle cell has one exclusive orientation.

Exact expanded PA statement

forall p q h k i j. p = 2 * h + 1 -> q = 2 * k + 1 -> ((~(p = 1) /\ forall frp_prime_left_lattice_prime_p frp_prime_right_lattice_prime_p. p = frp_prime_left_lattice_prime_p * frp_prime_right_lattice_prime_p -> frp_prime_left_lattice_prime_p = 1 \/ frp_prime_right_lattice_prime_p = 1)) -> ((~(q = 1) /\ forall frp_prime_left_lattice_prime_q frp_prime_right_lattice_prime_q. q = frp_prime_left_lattice_prime_q * frp_prime_right_lattice_prime_q -> frp_prime_left_lattice_prime_q = 1 \/ frp_prime_right_lattice_prime_q = 1)) -> ~(p = q) -> (exists elo_gap_lattice_i_bound. elo_gap_lattice_i_bound + S (i) = h) -> (exists elo_gap_lattice_j_bound. elo_gap_lattice_j_bound + S (j) = k) -> ((((exists elo_gap_lattice_cell_result_left. elo_gap_lattice_cell_result_left + S (q * S i) = p * S j) /\ ~(exists elo_gap_lattice_cell_result_right. elo_gap_lattice_cell_result_right + S (p * S j) = q * S i)) \/ ((exists elo_gap_lattice_cell_result_right. elo_gap_lattice_cell_result_right + S (p * S j) = q * S i) /\ ~(exists elo_gap_lattice_cell_result_left. elo_gap_lattice_cell_result_left + S (q * S i) = p * S j))))

Structural proof guide

Generated structural guide

Every bounded half-rectangle cell has one exclusive orientation.

Use the direct prerequisites distinct_odd_prime_half_products_ne, lt_trichotomy, lt_to_le, lt_not_le as previously established PA formulas.

The proof proceeds by case analysis (2), intermediate claims (3).

Referenced ingredients

PA00D8 distinct_odd_prime_half_products_ne PA0011 lt_trichotomy PA000X lt_to_le PA003A lt_not_le

Proof neighborhood

Direct dependencies

PA00D8 distinct_odd_prime_half_products_ne PA0011 lt_trichotomy PA000X lt_to_le PA003A lt_not_le

Direct dependents

PA00DA distinct_odd_prime_half_cell_indicator_choice

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 j
  7. 0007intro hpodd
  8. 0008intro hqodd
  9. 0009intro hp
  10. 0010intro hq
  11. 0011intro hpq
  12. 0012intro hi
  13. 0013intro hj
  14. 0014have hne : ~(q * S i = p * S j)
  15. 0015intro heq
  16. 0016specialize distinct_odd_prime_half_products_ne p
  17. 0017specialize distinct_odd_prime_half_products_ne q
  18. 0018specialize distinct_odd_prime_half_products_ne h
  19. 0019specialize distinct_odd_prime_half_products_ne k
  20. 0020specialize distinct_odd_prime_half_products_ne i
  21. 0021specialize distinct_odd_prime_half_products_ne j
  22. 0022apply distinct_odd_prime_half_products_ne
  23. 0023exact hpodd
  24. 0024exact hqodd
  25. 0025exact hp
  26. 0026exact hq
  27. 0027exact hpq
  28. 0028exact hi
  29. 0029exact hj
  30. 0030exact heq
  31. 0031specialize lt_trichotomy (q * S i)
  32. 0032specialize lt_trichotomy (p * S j)
  33. 0033cases lt_trichotomy
  34. 0034exfalso
  35. 0035apply hne
  36. 0036exact lt_trichotomy_left
  37. 0037cases lt_trichotomy_right
  38. 0038left
  39. 0039split
  40. 0040exact lt_trichotomy_right_left
  41. 0041intro hreverse
  42. 0042have hle : exists gap. gap + (p * S j) = q * S i
  43. 0043specialize lt_to_le (p * S j)
  44. 0044specialize lt_to_le (q * S i)
  45. 0045apply lt_to_le
  46. 0046exact hreverse
  47. 0047specialize lt_not_le (q * S i)
  48. 0048specialize lt_not_le (p * S j)
  49. 0049apply lt_not_le
  50. 0050exact lt_trichotomy_right_left
  51. 0051exact hle
  52. 0052right
  53. 0053split
  54. 0054exact lt_trichotomy_right_right
  55. 0055intro hreverse
  56. 0056have hle : exists gap. gap + (q * S i) = p * S j
  57. 0057specialize lt_to_le (q * S i)
  58. 0058specialize lt_to_le (p * S j)
  59. 0059apply lt_to_le
  60. 0060exact hreverse
  61. 0061specialize lt_not_le (p * S j)
  62. 0062specialize lt_not_le (q * S i)
  63. 0063apply lt_not_le
  64. 0064exact lt_trichotomy_right_right
  65. 0065exact hle