no goals
m x y : ℤ
h : ↑2 * m = x ^ 2 + y ^ 2
⊢ Even (x ^ 2 + y ^ 2)
simp [← h, even_mul]
no goals
m x y : ℤ
h : ↑2 * m = x ^ 2 + y ^ 2
this : Even (x ^ 2 + y ^ 2)
⊢ Even (x + y)
simpa [sq, parity_simps]
no goals
m x y : ℤ
h : ↑2 * m = x ^ 2 + y ^ 2
this : Even (x ^ 2 + y ^ 2)
hxaddy : Even (x + y)
⊢ Even (x - y)
simpa [sq, parity_simps]
no goals
m x y : ℤ
h : ↑2 * m = x ^ 2 + y ^ 2
this : Even (x ^ 2 + y ^ 2)
hxaddy : Even (x + y)
hxsuby : Even (x - y)
⊢ 2 * 2 ≠ 0
decide
m x y : ℤ
h : ↑2 * m = x ^ 2 + y ^ 2
this : Even (x ^ 2 + y ^ 2)
hxaddy : Even (x + y)
hxsuby : Even (x - y)
⊢ ↑2 * (x ^ 2 + y ^ 2) = (x - y) ^ 2 + (x + y) ^ 2
m x y : ℤ
h : ↑2 * m = x ^ 2 + y ^ 2
this : Even (x ^ 2 + y ^ 2)
hxaddy : Even (x + y)
hxsuby : Even (x - y)
⊢ ↑2 * ↑2 * m = (x - y) ^ 2 + (x + y) ^ 2
rw [mul_assoc, h]
no goals
m x y : ℤ
h : ↑2 * m = x ^ 2 + y ^ 2
this : Even (x ^ 2 + y ^ 2)
hxaddy : Even (x + y)
hxsuby : Even (x - y)
⊢ ↑2 * (x ^ 2 + y ^ 2) = (x - y) ^ 2 + (x + y) ^ 2
ring
m x y : ℤ
h : ↑2 * m = x ^ 2 + y ^ 2
this : Even (x ^ 2 + y ^ 2)
hxaddy : 2 ∣ x + y
hxsuby : 2 ∣ x - y
⊢ (x - y) ^ 2 + (x + y) ^ 2 = (2 * ((x - y) / 2)) ^ 2 + (2 * ((x + y) / 2)) ^ 2
m x y : ℤ
h : ↑2 * m = x ^ 2 + y ^ 2
this : Even (x ^ 2 + y ^ 2)
hxaddy : Even (x + y)
hxsuby : Even (x - y)
⊢ (x - y) ^ 2 + (x + y) ^ 2 = (2 * ((x - y) / 2)) ^ 2 + (2 * ((x + y) / 2)) ^ 2
rw [even_iff_two_dvd] at hxsuby hxaddy
no goals
m x y : ℤ
h : ↑2 * m = x ^ 2 + y ^ 2
this : Even (x ^ 2 + y ^ 2)
hxaddy : 2 ∣ x + y
hxsuby : 2 ∣ x - y
⊢ (x - y) ^ 2 + (x + y) ^ 2 = (2 * ((x - y) / 2)) ^ 2 + (2 * ((x + y) / 2)) ^ 2
rw [Int.mul_ediv_cancel' hxsuby, Int.mul_ediv_cancel' hxaddy]
no goals
m x y : ℤ
h : ↑2 * m = x ^ 2 + y ^ 2
this : Even (x ^ 2 + y ^ 2)
hxaddy : Even (x + y)
hxsuby : Even (x - y)
⊢ (2 * ((x - y) / 2)) ^ 2 + (2 * ((x + y) / 2)) ^ 2 = ↑2 * ↑2 * (((x - y) / 2) ^ 2 + ((x + y) / 2) ^ 2)
simp [mul_add, pow_succ, mul_comm, mul_assoc, mul_left_comm]