a b c k : ℤ
hk0 : k ≠ 0
⊢ a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2 ↔ k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
a b c k : ℤ
hk0 : k ≠ 0
⊢ Fermat42 a b c ↔ Fermat42 (k * a) (k * b) (k ^ 2 * c)
delta Fermat42
case mp
a b c k : ℤ
hk0 : k ≠ 0
⊢ a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2 → k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2

case mpr
a b c k : ℤ
hk0 : k ≠ 0
⊢ k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2 → a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
a b c k : ℤ
hk0 : k ≠ 0
⊢ a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2 ↔ k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
constructor
case mp
a b c k : ℤ
hk0 : k ≠ 0
f42 : a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
⊢ k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
case mp
a b c k : ℤ
hk0 : k ≠ 0
⊢ a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2 → k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
intro f42
case mp.left
a b c k : ℤ
hk0 : k ≠ 0
f42 : a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
⊢ k * a ≠ 0

case mp.right
a b c k : ℤ
hk0 : k ≠ 0
f42 : a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
⊢ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
case mp
a b c k : ℤ
hk0 : k ≠ 0
f42 : a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
⊢ k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
constructor
case mp.right.left
a b c k : ℤ
hk0 : k ≠ 0
f42 : a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
⊢ k * b ≠ 0

case mp.right.right
a b c k : ℤ
hk0 : k ≠ 0
f42 : a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
⊢ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
case mp.right
a b c k : ℤ
hk0 : k ≠ 0
f42 : a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
⊢ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
constructor
no goals
case mp.left
a b c k : ℤ
hk0 : k ≠ 0
f42 : a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
⊢ k * a ≠ 0
exact mul_ne_zero hk0 f42.1
no goals
case mp.right.left
a b c k : ℤ
hk0 : k ≠ 0
f42 : a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
⊢ k * b ≠ 0
exact mul_ne_zero hk0 f42.2.1
case mp.right.right
a b c k : ℤ
hk0 : k ≠ 0
f42 : a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
H : a ^ 4 + b ^ 4 = c ^ 2
⊢ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
case mp.right.right
a b c k : ℤ
hk0 : k ≠ 0
f42 : a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
⊢ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
have H : a ^ 4 + b ^ 4 = c ^ 2 := f42.2.2
no goals
case mp.right.right
a b c k : ℤ
hk0 : k ≠ 0
f42 : a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
H : a ^ 4 + b ^ 4 = c ^ 2
⊢ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
linear_combination k ^ 4 * H
case mpr
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
case mpr
a b c k : ℤ
hk0 : k ≠ 0
⊢ k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2 → a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
intro f42
case mpr.left
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ a ≠ 0

case mpr.right
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
case mpr
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
constructor
case mpr.right.left
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ b ≠ 0

case mpr.right.right
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ a ^ 4 + b ^ 4 = c ^ 2
case mpr.right
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
constructor
case mpr.right.right
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ k ^ 4 * (a ^ 4 + b ^ 4) = k ^ 4 * c ^ 2
case mpr.right.right
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ a ^ 4 + b ^ 4 = c ^ 2
apply (mul_right_inj' (pow_ne_zero 4 hk0)).mp
no goals
case mpr.right.right
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ k ^ 4 * (a ^ 4 + b ^ 4) = k ^ 4 * c ^ 2
linear_combination f42.2.2
no goals
case mpr.left
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ a ≠ 0
exact right_ne_zero_of_mul f42.1
no goals
case mpr.right.left
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ b ≠ 0
exact right_ne_zero_of_mul f42.2.1