FormalConjectures.Wikipedia.BealConjecture

FormalConjectures
Wikipedia
BealConjecture

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Beal conjecture

Reference: Wikipedia

namespace BealConjecture

def bealConjecture : Prop := ∀ {A B C x y z : ℕ},
    A ≠ 0 → B ≠ 0 → C ≠ 0 → 2 < x → 2 < y → 2 < z →
    A^x + B^y = C^z → 1 < Finset.gcd {A, B, C} id

The Beal Conjecture: if we are given positive integers $A, B, C, x, y, z$ such that $x, y, z > 2$ and $A^x + B^y = C^z$ then $A, B, C$ have a common divisor.

@[category research open, AMS 11]
theorem beal_conjecture : bealConjecture := by⊢ bealConjecture
  sorryAll goals completed! 🐙

The Beal Conjecture implies Fermat's last theorem


@[category textbook, AMS 11]
theorem flt_of_beal_conjecture (H : bealConjecture) :
    FermatLastTheorem := byH:bealConjecture⊢ FermatLastTheorem
  intro n hn x y z hx hy hzH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx:x ≠ 0hy:y ≠ 0hz:z ≠ 0⊢ x ^ n + y ^ n ≠ z ^ n
  by_contra hH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx:x ≠ 0hy:y ≠ 0hz:z ≠ 0h:x ^ n + y ^ n = z ^ n⊢ False
  apply mul_ne_zero (mul_ne_zero hx hy) hzH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx:x ≠ 0hy:y ≠ 0hz:z ≠ 0h:x ^ n + y ^ n = z ^ n⊢ x * y * z = 0
  by_contra H''H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx:x ≠ 0hy:y ≠ 0hz:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0⊢ False
  obtain ⟨hx, hy, hz⟩ : x ≠ 0 ∧ y ≠ 0 ∧ z ≠ 0 := byH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx:x ≠ 0hy:y ≠ 0hz:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0⊢ x ≠ 0 ∧ y ≠ 0 ∧ z ≠ 0H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0⊢ False aesopH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0⊢ FalseH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0⊢ False
  set G := Finset.gcd {x, y, z} idH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd id⊢ False
  set x' := (x / G : ℕ)H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / G⊢ False
  set y' := (y / G : ℕ)H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / G⊢ False
  set z' := (z / G : ℕ)H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / G⊢ False
  obtain ⟨hGx, hGy, hGz⟩ : G ∣ x ∧ G ∣ y ∧ G ∣ z := byH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / G⊢ G ∣ x ∧ G ∣ y ∧ G ∣ zH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ z⊢ False
    refine ⟨?_, ?_, ?_⟩refine_1H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / G⊢ G ∣ xrefine_2H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / G⊢ G ∣ yrefine_3H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / G⊢ G ∣ zH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ z⊢ False <;>refine_1H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / G⊢ G ∣ xrefine_2H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / G⊢ G ∣ yrefine_3H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / G⊢ G ∣ zH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ z⊢ False apply Finset.gcd_dvd (byH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / G⊢ z ∈ {x, y, z}H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ z⊢ False aesopAll goals completed! 🐙H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ z⊢ False)H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ z⊢ False
  obtain ⟨hx', hy', hz'⟩ : x' ≠ 0 ∧ y' ≠ 0 ∧ z' ≠ 0 := byH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ z⊢ x' ≠ 0 ∧ y' ≠ 0 ∧ z' ≠ 0H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ False
    refine ⟨?_, ?_, ?_⟩refine_1H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ z⊢ x' ≠ 0refine_2H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ z⊢ y' ≠ 0refine_3H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ z⊢ z' ≠ 0H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ False <;>refine_1H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ z⊢ x' ≠ 0refine_2H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ z⊢ y' ≠ 0refine_3H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ z⊢ z' ≠ 0H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ False
      apply Nat.div_ne_zero_iff_of_dvd (byH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ z⊢ G ∣ zH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ False assumptionAll goals completed! 🐙H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ False) |>.mpr ⟨(byH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ z⊢ z ≠ 0H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ False assumptionAll goals completed! 🐙H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ False), _⟩ <;>H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ z⊢ G ≠ 0H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ z⊢ G ≠ 0H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ z⊢ G ≠ 0H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ False aesopH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ FalseH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ False
  have Hxyz' : x'^n + y'^n = z'^n := byH:bealConjecture⊢ FermatLastTheoremH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0Hxyz':x' ^ n + y' ^ n = z' ^ n⊢ False
    rwa [Nat.div_pow hGx,H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ x ^ n / G ^ n + y' ^ n = z' ^ nH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0Hxyz':x' ^ n + y' ^ n = z' ^ n⊢ False Nat.div_pow hGy,H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ x ^ n / G ^ n + y ^ n / G ^ n = z' ^ nH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0Hxyz':x' ^ n + y' ^ n = z' ^ n⊢ False Nat.div_pow hGz,H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ x ^ n / G ^ n + y ^ n / G ^ n = z ^ n / G ^ nH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0Hxyz':x' ^ n + y' ^ n = z' ^ n⊢ False
      ←Nat.add_div_of_dvd_right,H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ (x ^ n + y ^ n) / G ^ n = z ^ n / G ^ nH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ G ^ n ∣ x ^ nH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0Hxyz':x' ^ n + y' ^ n = z' ^ n⊢ False Nat.div_left_inj (dvd_add _ _)H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ x ^ n + y ^ n = z ^ nH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ G ^ n ∣ z ^ nH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ G ^ n ∣ x ^ nH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ G ^ n ∣ y ^ nH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ G ^ n ∣ x ^ nH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0Hxyz':x' ^ n + y' ^ n = z' ^ n⊢ False]H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ x ^ n + y ^ n = z ^ nH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ G ^ n ∣ z ^ nH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ G ^ n ∣ x ^ nH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ G ^ n ∣ y ^ nH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ G ^ n ∣ x ^ nH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0Hxyz':x' ^ n + y' ^ n = z' ^ n⊢ False
    all_goals apply pow_dvd_pow_of_dvdH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0⊢ G ∣ xH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0Hxyz':x' ^ n + y' ^ n = z' ^ n⊢ False ; assumptionH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0Hxyz':x' ^ n + y' ^ n = z' ^ n⊢ FalseH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0Hxyz':x' ^ n + y' ^ n = z' ^ n⊢ False
  apply ne_of_lt <| H hx' hy' hz' hn hn hn Hxyz'H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0Hxyz':x' ^ n + y' ^ n = z' ^ n⊢ 1 = {x', y', z'}.gcd id
  rw [←Finset.gcd_div_id_eq_one (Finset.mem_insert_self x {y, z}) (byH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0Hxyz':x' ^ n + y' ^ n = z' ^ n⊢ x ≠ 0All goals completed! 🐙 trivialAll goals completed! 🐙All goals completed! 🐙),
    Finset.gcd_eq_gcd_image,H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0Hxyz':x' ^ n + y' ^ n = z' ^ n⊢ (Finset.image (fun b ↦ b / {x, y, z}.gcd id) {x, y, z}).gcd id = {x', y', z'}.gcd idAll goals completed! 🐙 Finset.image_insert,H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0Hxyz':x' ^ n + y' ^ n = z' ^ n⊢ (insert (x / {x, y, z}.gcd id) (Finset.image (fun b ↦ b / {x, y, z}.gcd id) {y, z})).gcd id = {x', y', z'}.gcd idAll goals completed! 🐙 Finset.image_insert,H:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0Hxyz':x' ^ n + y' ^ n = z' ^ n⊢ (insert (x / {x, y, z}.gcd id) (insert (y / {x, y, z}.gcd id) (Finset.image (fun b ↦ b / {x, y, z}.gcd id) {z}))).gcd
    id =
  {x', y', z'}.gcd idAll goals completed! 🐙
    Finset.image_singletonH:bealConjecturen:ℕhn:n ≥ 3x:ℕy:ℕz:ℕhx✝:x ≠ 0hy✝:y ≠ 0hz✝:z ≠ 0h:x ^ n + y ^ n = z ^ nH'':¬x * y * z = 0hx:x ≠ 0hy:y ≠ 0hz:z ≠ 0G:ℕ := {x, y, z}.gcd idx':ℕ := x / Gy':ℕ := y / Gz':ℕ := z / GhGx:G ∣ xhGy:G ∣ yhGz:G ∣ zhx':x' ≠ 0hy':y' ≠ 0hz':z' ≠ 0Hxyz':x' ^ n + y' ^ n = z' ^ n⊢ {x / {x, y, z}.gcd id, y / {x, y, z}.gcd id, z / {x, y, z}.gcd id}.gcd id = {x', y', z'}.gcd idAll goals completed! 🐙]All goals completed! 🐙

end BealConjecture