PA00FJ

odd_half_even_iff_mod4_one

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

For a fixed odd decomposition, a modulo-four-one modulus is equivalent to an even half.

Exact expanded PA statement

forall p h. p = 2 * h + 1 -> ((((exists poh_even_half. h = 2 * poh_even_half) -> (exists poh_one_modulus. p = 4 * poh_one_modulus + 1)) /\ ((exists poh_one_modulus. p = 4 * poh_one_modulus + 1) -> (exists poh_even_half. h = 2 * poh_even_half))))

Structural proof guide

Generated structural guide

For a fixed odd decomposition, a modulo-four-one modulus is equivalent to an even half.

Use the direct prerequisites four_mul_eq_double_double, odd_half_of_mod4_one_exact as previously established PA formulas.

The proof proceeds by case analysis (2), equality transport (2).

Referenced ingredients

PA006R four_mul_eq_double_double PA00FI odd_half_of_mod4_one_exact

Proof neighborhood

Direct dependencies

PA006R four_mul_eq_double_double PA00FI odd_half_of_mod4_one_exact

Direct dependents

PA00FO qres_same_status_from_mod_four_one

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 h
  3. 0003intro hp
  4. 0004split
  5. 0005intro heven
  6. 0006cases heven
  7. 0007exists x
  8. 0008rewrite hp
  9. 0009rewrite heven_witness
  10. 0010congr
  11. 0011symm
  12. 0012apply four_mul_eq_double_double
  13. 0013refl
  14. 0014intro hone
  15. 0015cases hone
  16. 0016exists x
  17. 0017specialize odd_half_of_mod4_one_exact p
  18. 0018specialize odd_half_of_mod4_one_exact h
  19. 0019specialize odd_half_of_mod4_one_exact x
  20. 0020apply odd_half_of_mod4_one_exact
  21. 0021exact hp
  22. 0022exact hone_witness