theorem
proved
tactic proof
jain_denominator_odd_minus
show as:
view Lean formalization →
formal statement (Lean)
110theorem jain_denominator_odd_minus (p m : ℕ) (h : 1 < 2 * m * p) :
111 (2 * m * p - 1) % 2 = 1 := by
proof body
Tactic-mode proof.
112 have hk : 2 * m * p = 2 * (m * p) := by ring
113 have hkge : 1 < 2 * (m * p) := by linarith [hk]
114 have : (2 * (m * p) - 1) % 2 = 1 := by omega
115 linarith [show (2 * m * p - 1) % 2 = (2 * (m * p) - 1) % 2 from by ring_nf]
116
117/-- **KEY THEOREM**: FQHE requires odd denominator. -/