PA00FI

odd_half_of_mod4_one_exact

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

The half of a fixed odd number congruent to one modulo four is exactly even.

Exact expanded PA statement

forall p h a. p = 2 * h + 1 -> p = 4 * a + 1 -> h = 2 * a

Structural proof guide

Generated structural guide

The half of a fixed odd number congruent to one modulo four is exactly even.

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

The proof proceeds by intermediate claims (1).

Referenced ingredients

PA006R four_mul_eq_double_double PA006T odd_half_unique

Proof neighborhood

Direct dependencies

PA006R four_mul_eq_double_double PA006T odd_half_unique

Direct dependents

PA00FJ odd_half_even_iff_mod4_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 a
  4. 0004intro hp
  5. 0005intro hfour
  6. 0006have hcanonical : p = 2 * (2 * a) + 1
  7. 0007trans 4 * a + 1
  8. 0008exact hfour
  9. 0009congr
  10. 0010apply four_mul_eq_double_double
  11. 0011refl
  12. 0012specialize odd_half_unique p
  13. 0013specialize odd_half_unique h
  14. 0014specialize odd_half_unique (2 * a)
  15. 0015apply odd_half_unique
  16. 0016exact hp
  17. 0017exact hcanonical