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

@[implicit_reducible]

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

@[implicit_reducible]

instance remark_2_15 : Decidable ψ

Equations

• remark_2_15 = decidable_of_iff φ remark_2_15._proof_1