def φ : Prop

Equations

• φ = ∀ (x : Fin 19) (y : Fin 30) (z : Fin 35), 143 * ↑x + 91 * ↑y + 77 * ↑z = 2692 ↔ ↑x = 6 ∧ ↑y = 10 ∧ ↑z = 12

def ψ : Prop

Equations

• ψ = ∀ (x y z : ℕ), 143 * x + 91 * y + 77 * z = 2692 ↔ x = 6 ∧ y = 10 ∧ z = 12

instance myφ : Decidable φ

Equations

• myφ = decidable_of_iff (∀ (x : Fin 19) (y : Fin 30) (z : Fin 35), 143 * ↑x + 91 * ↑y + 77 * ↑z = 2692 ↔ ↑x = 6 ∧ ↑y = 10 ∧ ↑z = 12) myφ.proof_1

theorem decide_diophantine3_1 {a : ℕ} {b : ℕ} {c : ℕ} {n : ℕ} {x : ℕ} {y : ℕ} {z : ℕ} (h : a * x + b * y + c * z = n) (ha : 0 < a) : x < n / a + 1

theorem decide_diophantine3_3 (a : ℕ) (b : ℕ) (c : ℕ) (n : ℕ) (x : ℕ) (y : ℕ) (z : ℕ) : a * x + b * y + c * z = n → 0 < a → 0 < b → 0 < c → x < n / a + 1 ∧ y < n / b + 1 ∧ z < n / c + 1

instance remark_2_15 : Decidable ψ

Equations

• remark_2_15 = decidable_of_iff φ remark_2_15.proof_1