[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Mul α
a : α
x✝ : IsSquare (op a)
c : αᵐᵒᵖ
hc : op a = c * c
⊢ a = unop c * unop c
[PROOFSTEP]
rw [← unop_mul, ← hc, unop_op]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Mul α
a : α
x✝ : IsSquare a
c : α
hc : a = c * c
⊢ IsSquare (op a)
[PROOFSTEP]
simp [hc]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MonoidHomClass F α β
m : α
f : F
⊢ IsSquare m → IsSquare (↑f m)
[PROOFSTEP]
rintro ⟨m, rfl⟩
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MonoidHomClass F α β
f : F
m : α
⊢ IsSquare (↑f (m * m))
[PROOFSTEP]
exact ⟨f m, by simp⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MonoidHomClass F α β
f : F
m : α
⊢ ↑f (m * m) = ↑f m * ↑f m
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Monoid α
n : ℕ
a m : α
⊢ IsSquare m ↔ ∃ c, m = c ^ 2
[PROOFSTEP]
simp [IsSquare, pow_two]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Monoid α
n✝ : ℕ
a : α
n : ℕ
⊢ IsSquare a → IsSquare (a ^ n)
[PROOFSTEP]
rintro ⟨a, rfl⟩
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Monoid α
n✝ n : ℕ
a : α
⊢ IsSquare ((a * a) ^ n)
[PROOFSTEP]
exact ⟨a ^ n, (Commute.refl _).mul_pow _⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Monoid α
n : ℕ
a : α
⊢ Even n → ∀ (a : α), IsSquare (a ^ n)
[PROOFSTEP]
rintro ⟨n, rfl⟩ a
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Monoid α
a✝ : α
n : ℕ
a : α
⊢ IsSquare (a ^ (n + n))
[PROOFSTEP]
exact ⟨a ^ n, pow_add _ _ _⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Monoid α
n : ℕ
a : α
inst✝ : HasDistribNeg α
⊢ Even n → ∀ (a : α), (-a) ^ n = a ^ n
[PROOFSTEP]
rintro ⟨c, rfl⟩ a
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Monoid α
a✝ : α
inst✝ : HasDistribNeg α
c : ℕ
a : α
⊢ (-a) ^ (c + c) = a ^ (c + c)
[PROOFSTEP]
simp_rw [← two_mul, pow_mul, neg_sq]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Monoid α
n : ℕ
a : α
inst✝ : HasDistribNeg α
h : Even n
⊢ (-1) ^ n = 1
[PROOFSTEP]
rw [h.neg_pow, one_pow]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : CommSemigroup α
a b : α
⊢ IsSquare a → IsSquare b → IsSquare (a * b)
[PROOFSTEP]
rintro ⟨a, rfl⟩ ⟨b, rfl⟩
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : CommSemigroup α
a b : α
⊢ IsSquare (a * a * (b * b))
[PROOFSTEP]
exact ⟨a * b, mul_mul_mul_comm _ _ _ _⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : DivisionMonoid α
a : α
⊢ IsSquare a⁻¹ ↔ IsSquare a
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : DivisionMonoid α
a : α
h : IsSquare a⁻¹
⊢ IsSquare a
[PROOFSTEP]
rw [← isSquare_op_iff, ← inv_inv a]
[GOAL]
case refine'_1
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : DivisionMonoid α
a : α
h : IsSquare a⁻¹
⊢ IsSquare (op a⁻¹⁻¹)
[PROOFSTEP]
exact h.map (MulEquiv.inv' α)
[GOAL]
case refine'_2
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : DivisionMonoid α
a : α
h : IsSquare a
⊢ IsSquare a⁻¹
[PROOFSTEP]
exact ((isSquare_op_iff a).mpr h).map (MulEquiv.inv' α).symm
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : DivisionMonoid α
a : α
n : ℤ
⊢ IsSquare a → IsSquare (a ^ n)
[PROOFSTEP]
rintro ⟨a, rfl⟩
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : DivisionMonoid α
n : ℤ
a : α
⊢ IsSquare ((a * a) ^ n)
[PROOFSTEP]
exact ⟨a ^ n, (Commute.refl _).mul_zpow _⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : DivisionMonoid α
a : α
inst✝ : HasDistribNeg α
n : ℤ
⊢ Even n → ∀ (a : α), (-a) ^ n = a ^ n
[PROOFSTEP]
rintro ⟨c, rfl⟩ a
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : DivisionMonoid α
a✝ : α
inst✝ : HasDistribNeg α
c : ℤ
a : α
⊢ (-a) ^ (c + c) = a ^ (c + c)
[PROOFSTEP]
exact zpow_bit0_neg _ _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : DivisionMonoid α
a : α
inst✝ : HasDistribNeg α
n : ℤ
h : Even n
⊢ (-1) ^ n = 1
[PROOFSTEP]
rw [h.neg_zpow, one_zpow]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : SubtractionMonoid α
inst✝ : LinearOrder α
a : α
⊢ Even |a| ↔ Even a
[PROOFSTEP]
cases abs_choice a
[GOAL]
case inl
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : SubtractionMonoid α
inst✝ : LinearOrder α
a : α
h✝ : |a| = a
⊢ Even |a| ↔ Even a
[PROOFSTEP]
have h : abs a = a := by assumption
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : SubtractionMonoid α
inst✝ : LinearOrder α
a : α
h✝ : |a| = a
⊢ |a| = a
[PROOFSTEP]
assumption
[GOAL]
case inl
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : SubtractionMonoid α
inst✝ : LinearOrder α
a : α
h✝ h : |a| = a
⊢ Even |a| ↔ Even a
[PROOFSTEP]
simp only [h, even_neg]
[GOAL]
case inr
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : SubtractionMonoid α
inst✝ : LinearOrder α
a : α
h✝ : |a| = -a
⊢ Even |a| ↔ Even a
[PROOFSTEP]
have h : abs a = -a := by assumption
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : SubtractionMonoid α
inst✝ : LinearOrder α
a : α
h✝ : |a| = -a
⊢ |a| = -a
[PROOFSTEP]
assumption
[GOAL]
case inr
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : SubtractionMonoid α
inst✝ : LinearOrder α
a : α
h✝ h : |a| = -a
⊢ Even |a| ↔ Even a
[PROOFSTEP]
simp only [h, even_neg]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : DivisionCommMonoid α
a b : α
ha : IsSquare a
hb : IsSquare b
⊢ IsSquare (a / b)
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : DivisionCommMonoid α
a b : α
ha : IsSquare a
hb : IsSquare b
⊢ IsSquare (a * b⁻¹)
[PROOFSTEP]
exact ha.mul hb.inv
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Group α
n : ℤ
⊢ Even n → ∀ (a : α), IsSquare (a ^ n)
[PROOFSTEP]
rintro ⟨n, rfl⟩ a
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Group α
n : ℤ
a : α
⊢ IsSquare (a ^ (n + n))
[PROOFSTEP]
exact ⟨a ^ n, zpow_add _ _ _⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝³ : CanonicallyLinearOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
m n : α
hm : Even m
hn : Even n
⊢ Even (m - n)
[PROOFSTEP]
obtain ⟨a, rfl⟩ := hm
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝³ : CanonicallyLinearOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
n : α
hn : Even n
a : α
⊢ Even (a + a - n)
[PROOFSTEP]
obtain ⟨b, rfl⟩ := hn
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝³ : CanonicallyLinearOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ Even (a + a - (b + b))
[PROOFSTEP]
refine' ⟨a - b, _⟩
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝³ : CanonicallyLinearOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a + a - (b + b) = a - b + (a - b)
[PROOFSTEP]
obtain h | h := le_total a b
[GOAL]
case intro.intro.inl
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝³ : CanonicallyLinearOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
h : a ≤ b
⊢ a + a - (b + b) = a - b + (a - b)
[PROOFSTEP]
rw [tsub_eq_zero_of_le h, tsub_eq_zero_of_le (add_le_add h h), add_zero]
[GOAL]
case intro.intro.inr
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝³ : CanonicallyLinearOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
h : b ≤ a
⊢ a + a - (b + b) = a - b + (a - b)
[PROOFSTEP]
exact (tsub_add_tsub_comm h h).symm
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m✝ n m : α
⊢ Even m ↔ ∃ c, m = 2 * c
[PROOFSTEP]
simp [even_iff_exists_two_nsmul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n a : α
⊢ Even a ↔ 2 ∣ a
[PROOFSTEP]
simp [Even, Dvd.dvd, two_mul]
[GOAL]
F : Type u_1
α✝ : Type u_2
β : Type u_3
R : Type u_4
inst✝² : Semiring α✝
inst✝¹ : Semiring β
m n : α✝
α : Type u_5
inst✝ : Semiring α
⊢ (Set.range fun x => 2 * x) = {a | Even a}
[PROOFSTEP]
ext x
[GOAL]
case h
F : Type u_1
α✝ : Type u_2
β : Type u_3
R : Type u_4
inst✝² : Semiring α✝
inst✝¹ : Semiring β
m n : α✝
α : Type u_5
inst✝ : Semiring α
x : α
⊢ (x ∈ Set.range fun x => 2 * x) ↔ x ∈ {a | Even a}
[PROOFSTEP]
simp [eq_comm, two_mul, Even]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ 2 = 1 + 1
[PROOFSTEP]
rw [one_add_one_eq_two]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
hm : Even m
a : ℕ
x✝ : a + 1 ≠ 0
⊢ Even (m ^ (a + 1))
[PROOFSTEP]
rw [pow_succ]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
hm : Even m
a : ℕ
x✝ : a + 1 ≠ 0
⊢ Even (m * m ^ a)
[PROOFSTEP]
exact hm.mul_right _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n a b : α
⊢ a = 2 * b + 1 ↔ a = bit1 b
[PROOFSTEP]
rw [two_mul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n a b : α
⊢ a = b + b + 1 ↔ a = bit1 b
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α✝ : Type u_2
β : Type u_3
R : Type u_4
inst✝² : Semiring α✝
inst✝¹ : Semiring β
m n : α✝
α : Type u_5
inst✝ : Semiring α
⊢ (Set.range fun x => 2 * x + 1) = {a | Odd a}
[PROOFSTEP]
ext x
[GOAL]
case h
F : Type u_1
α✝ : Type u_2
β : Type u_3
R : Type u_4
inst✝² : Semiring α✝
inst✝¹ : Semiring β
m n : α✝
α : Type u_5
inst✝ : Semiring α
x : α
⊢ (x ∈ Set.range fun x => 2 * x + 1) ↔ x ∈ {a | Odd a}
[PROOFSTEP]
simp [Odd, eq_comm]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ Even m → Odd n → Odd (m + n)
[PROOFSTEP]
rintro ⟨m, rfl⟩ ⟨n, rfl⟩
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ Odd (m + m + (2 * n + 1))
[PROOFSTEP]
exact ⟨m + n, by rw [mul_add, ← two_mul, add_assoc]⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ m + m + (2 * n + 1) = 2 * (m + n) + 1
[PROOFSTEP]
rw [mul_add, ← two_mul, add_assoc]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
he : Even m
ho : Odd n
⊢ Odd (n + m)
[PROOFSTEP]
simp only [he.add_odd ho, add_comm n m]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
hm : Odd m
hn : Even n
⊢ Odd (m + n)
[PROOFSTEP]
rw [add_comm]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
hm : Odd m
hn : Even n
⊢ Odd (n + m)
[PROOFSTEP]
exact hn.add_odd hm
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ Odd m → Odd n → Even (m + n)
[PROOFSTEP]
rintro ⟨m, rfl⟩ ⟨n, rfl⟩
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ Even (2 * m + 1 + (2 * n + 1))
[PROOFSTEP]
refine' ⟨n + m + 1, _⟩
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ 2 * m + 1 + (2 * n + 1) = n + m + 1 + (n + m + 1)
[PROOFSTEP]
rw [two_mul, two_mul]
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ m + m + 1 + (n + n + 1) = n + m + 1 + (n + m + 1)
[PROOFSTEP]
ac_rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ Odd (m + (m + 1))
[PROOFSTEP]
simp [← add_assoc]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ Odd (m + 1 + m)
[PROOFSTEP]
simp [add_comm _ m]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ Odd (m + (1 + m))
[PROOFSTEP]
simp [add_comm 1 m]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ Odd (1 + m + m)
[PROOFSTEP]
simp [add_comm 1 m]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝² : Semiring α
inst✝¹ : Semiring β
m n : α
inst✝ : RingHomClass F α β
f : F
⊢ Odd m → Odd (↑f m)
[PROOFSTEP]
rintro ⟨m, rfl⟩
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝² : Semiring α
inst✝¹ : Semiring β
n : α
inst✝ : RingHomClass F α β
f : F
m : α
⊢ Odd (↑f (2 * m + 1))
[PROOFSTEP]
exact ⟨f m, by simp [two_mul]⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝² : Semiring α
inst✝¹ : Semiring β
n : α
inst✝ : RingHomClass F α β
f : F
m : α
⊢ ↑f (2 * m + 1) = 2 * ↑f m + 1
[PROOFSTEP]
simp [two_mul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ Odd m → Odd n → Odd (m * n)
[PROOFSTEP]
rintro ⟨m, rfl⟩ ⟨n, rfl⟩
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ Odd ((2 * m + 1) * (2 * n + 1))
[PROOFSTEP]
refine' ⟨2 * m * n + n + m, _⟩
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ (2 * m + 1) * (2 * n + 1) = 2 * (2 * m * n + n + m) + 1
[PROOFSTEP]
rw [mul_add, add_mul, mul_one, ← add_assoc, one_mul, mul_assoc, ← mul_add, ← mul_add, ← mul_assoc, ← Nat.cast_two, ←
  Nat.cast_comm]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
hm : Odd m
⊢ Odd (m ^ 0)
[PROOFSTEP]
rw [pow_zero]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
hm : Odd m
⊢ Odd 1
[PROOFSTEP]
exact odd_one
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
hm : Odd m
a : ℕ
⊢ Odd (m ^ (a + 1))
[PROOFSTEP]
rw [pow_succ]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
hm : Odd m
a : ℕ
⊢ Odd (m * m ^ a)
[PROOFSTEP]
exact hm.mul <| Odd.pow hm
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
a : α
n : ℕ
⊢ Odd n → ∀ (a : α), (-a) ^ n = -a ^ n
[PROOFSTEP]
rintro ⟨c, rfl⟩ a
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
a✝ : α
c : ℕ
a : α
⊢ (-a) ^ (2 * c + 1) = -a ^ (2 * c + 1)
[PROOFSTEP]
simp_rw [pow_add, pow_mul, neg_sq, pow_one, mul_neg]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
a : α
n : ℕ
h : Odd n
⊢ (-1) ^ n = -1
[PROOFSTEP]
rw [h.neg_pow, one_pow]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : CanonicallyOrderedCommSemiring α
inst✝ : Nontrivial α
n : α
hn : Odd n
⊢ 0 < n
[PROOFSTEP]
obtain ⟨k, rfl⟩ := hn
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : CanonicallyOrderedCommSemiring α
inst✝ : Nontrivial α
k : α
⊢ 0 < 2 * k + 1
[PROOFSTEP]
rw [pos_iff_ne_zero, Ne.def, add_eq_zero_iff, not_and']
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : CanonicallyOrderedCommSemiring α
inst✝ : Nontrivial α
k : α
⊢ 1 = 0 → ¬2 * k = 0
[PROOFSTEP]
exact fun h => (one_ne_zero h).elim
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Ring α
a b : α
n : ℕ
⊢ Even (-2)
[PROOFSTEP]
simp only [even_neg, even_two]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Ring α
a b : α
n : ℕ
hp : Odd a
⊢ Odd (-a)
[PROOFSTEP]
obtain ⟨k, hk⟩ := hp
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Ring α
a b : α
n : ℕ
k : α
hk : a = 2 * k + 1
⊢ Odd (-a)
[PROOFSTEP]
use-(k + 1)
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Ring α
a b : α
n : ℕ
k : α
hk : a = 2 * k + 1
⊢ -a = 2 * -(k + 1) + 1
[PROOFSTEP]
rw [mul_neg, mul_add, neg_add, add_assoc, two_mul (1 : α), neg_add, neg_add_cancel_right, ← neg_add, hk]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Ring α
a b : α
n : ℕ
⊢ Odd (-1)
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Ring α
a b : α
n : ℕ
ha : Odd a
hb : Even b
⊢ Odd (a - b)
[PROOFSTEP]
rw [sub_eq_add_neg]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Ring α
a b : α
n : ℕ
ha : Odd a
hb : Even b
⊢ Odd (a + -b)
[PROOFSTEP]
exact ha.add_even hb.neg
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Ring α
a b : α
n : ℕ
ha : Even a
hb : Odd b
⊢ Odd (a - b)
[PROOFSTEP]
rw [sub_eq_add_neg]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Ring α
a b : α
n : ℕ
ha : Even a
hb : Odd b
⊢ Odd (a + -b)
[PROOFSTEP]
exact ha.add_odd hb.neg
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Ring α
a b : α
n : ℕ
ha : Odd a
hb : Odd b
⊢ Even (a - b)
[PROOFSTEP]
rw [sub_eq_add_neg]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Ring α
a b : α
n : ℕ
ha : Odd a
hb : Odd b
⊢ Even (a + -b)
[PROOFSTEP]
exact ha.add_odd hb.neg
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Ring α
a b : α
n : ℕ
inst✝ : LinearOrder α
⊢ Odd |a| ↔ Odd a
[PROOFSTEP]
cases' abs_choice a with h h
[GOAL]
case inl
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Ring α
a b : α
n : ℕ
inst✝ : LinearOrder α
h : |a| = a
⊢ Odd |a| ↔ Odd a
[PROOFSTEP]
simp only [h, odd_neg]
[GOAL]
case inr
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Ring α
a b : α
n : ℕ
inst✝ : LinearOrder α
h : |a| = -a
⊢ Odd |a| ↔ Odd a
[PROOFSTEP]
simp only [h, odd_neg]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : LinearOrderedRing R
a✝ : R
n : ℕ
hn : Even n
a : R
⊢ 0 ≤ a ^ n
[PROOFSTEP]
cases' hn with k hk
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : LinearOrderedRing R
a✝ : R
n : ℕ
a : R
k : ℕ
hk : n = k + k
⊢ 0 ≤ a ^ n
[PROOFSTEP]
simpa only [hk, two_mul] using pow_bit0_nonneg a k
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : LinearOrderedRing R
a : R
n : ℕ
hn : Even n
ha : a ≠ 0
⊢ 0 < a ^ n
[PROOFSTEP]
cases' hn with k hk
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : LinearOrderedRing R
a : R
n : ℕ
ha : a ≠ 0
k : ℕ
hk : n = k + k
⊢ 0 < a ^ n
[PROOFSTEP]
simpa only [hk, two_mul] using pow_bit0_pos ha k
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : LinearOrderedRing R
a : R
n : ℕ
hn : Odd n
ha : a ≤ 0
⊢ a ^ n ≤ 0
[PROOFSTEP]
cases' hn with k hk
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : LinearOrderedRing R
a : R
n : ℕ
ha : a ≤ 0
k : ℕ
hk : n = 2 * k + 1
⊢ a ^ n ≤ 0
[PROOFSTEP]
simpa only [hk, two_mul] using pow_bit1_nonpos_iff.mpr ha
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : LinearOrderedRing R
a : R
n : ℕ
hn : Odd n
ha : a < 0
⊢ a ^ n < 0
[PROOFSTEP]
cases' hn with k hk
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : LinearOrderedRing R
a : R
n : ℕ
ha : a < 0
k : ℕ
hk : n = 2 * k + 1
⊢ a ^ n < 0
[PROOFSTEP]
simpa only [hk, two_mul] using pow_bit1_neg_iff.mpr ha
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : LinearOrderedRing R
a : R
n : ℕ
hn : Even n
h₀ : 0 < n
h : 0 < a ^ n
ha : a = 0
⊢ False
[PROOFSTEP]
rw [ha, zero_pow h₀] at h 
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : LinearOrderedRing R
a : R
n : ℕ
hn : Even n
h₀ : 0 < n
h : 0 < 0
ha : a = 0
⊢ False
[PROOFSTEP]
exact lt_irrefl 0 h
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : LinearOrderedRing R
a✝ : R
n p : ℕ
hp : Even p
a : R
⊢ |a| ^ p = a ^ p
[PROOFSTEP]
rw [← abs_pow, abs_eq_self]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : LinearOrderedRing R
a✝ : R
n p : ℕ
hp : Even p
a : R
⊢ 0 ≤ a ^ p
[PROOFSTEP]
exact hp.pow_nonneg _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : LinearOrderedRing R
a : R
n : ℕ
hn : Odd n
⊢ StrictMono fun a => a ^ n
[PROOFSTEP]
cases' hn with k hk
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : LinearOrderedRing R
a : R
n k : ℕ
hk : n = 2 * k + 1
⊢ StrictMono fun a => a ^ n
[PROOFSTEP]
simpa only [hk, two_mul] using strictMono_pow_bit1 _
