Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+โ†‘Ctrl+โ†“to navigate, Ctrl+๐Ÿ–ฑ๏ธto focus. On Mac, use Cmdinstead of Ctrl. 
/-
Copyright (c) 2021 Alex Zhao. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Alex Zhao

! This file was ported from Lean 3 source module number_theory.frobenius_number
! leanprover-community/mathlib commit 1126441d6bccf98c81214a0780c73d499f6721fe
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Nat.ModEq
import Mathlib.GroupTheory.Submonoid.Basic
import Mathlib.GroupTheory.Submonoid.Membership
import Mathlib.Tactic.Ring
import Mathlib.Tactic.Zify

/-!
# Frobenius Number in Two Variables

In this file we first define a predicate for Frobenius numbers, then solve the 2-variable variant
of this problem.

## Theorem Statement

Given a finite set of relatively prime integers all greater than 1, their Frobenius number is the
largest positive integer that cannot be expressed as a sum of nonnegative multiples of these
integers. Here we show the Frobenius number of two relatively prime integers `m` and `n` greater
than 1 is `m * n - m - n`. This result is also known as the Chicken McNugget Theorem.

## Implementation Notes

First we define Frobenius numbers in general using `IsGreatest` and `AddSubmonoid.closure`. Then
we proceed to compute the Frobenius number of `m` and `n`.

For the upper bound, we begin with an auxiliary lemma showing `m * n` is not attainable, then show
`m * n - m - n` is not attainable. Then for the construction, we create a `k_1` which is `k mod n`
and `0 mod m`, then show it is at most `k`. Then `k_1` is a multiple of `m`, so `(k-k_1)`
is a multiple of n, and we're done.

## Tags

frobenius number, chicken mcnugget, chinese remainder theorem, add_submonoid.closure
-/


open Nat

/-- A natural number `n` is the **Frobenius number** of a set of natural numbers `s` if it is an
upper bound on the complement of the additive submonoid generated by `s`.
In other words, it is the largest number that can not be expressed as a sum of numbers in `s`. -/
def 
FrobeniusNumber: โ„• โ†’ Set โ„• โ†’ Prop
FrobeniusNumber (
n: โ„•
n : 
โ„•: Type
โ„•) (
s: Set โ„•
s : 
Set: Type ?u.4 โ†’ Type ?u.4
Set 
โ„•: Type
โ„•) : 
Prop: Type
Prop :=
  
IsGreatest: {ฮฑ : Type ?u.10} โ†’ [inst : Preorder ฮฑ] โ†’ Set ฮฑ โ†’ ฮฑ โ†’ Prop
IsGreatest { 
k: ?m.18
k | 
k: ?m.18
k โˆ‰ 
AddSubmonoid.closure: {M : Type ?u.25} โ†’ [inst : AddZeroClass M] โ†’ Set M โ†’ AddSubmonoid M
AddSubmonoid.closure 
s: Set โ„•
s } 
n: โ„•
n
#align is_frobenius_number 
FrobeniusNumber: โ„• โ†’ Set โ„• โ†’ Prop
FrobeniusNumber

variable {
m: โ„•
m 
n: โ„•
n : 
โ„•: Type
โ„•}

/-- The **Chicken Mcnugget theorem** stating that the Frobenius number
  of positive numbers `m` and `n` is `m * n - m - n`. -/
theorem 
frobeniusNumber_pair: coprime m n โ†’ 1 < m โ†’ 1 < n โ†’ FrobeniusNumber (m * n - m - n) {m, n}
frobeniusNumber_pair (
cop: coprime m n
cop : 
coprime: โ„• โ†’ โ„• โ†’ Prop
coprime 
m: โ„•
m 
n: โ„•
n) (
hm: 1 < m
hm : 
1: ?m.210
1 < 
m: โ„•
m) (
hn: 1 < n
hn : 
1: ?m.247
1 < 
n: โ„•
n) :
    
FrobeniusNumber: โ„• โ†’ Set โ„• โ†’ Prop
FrobeniusNumber (
m: โ„•
m * 
n: โ„•
n - 
m: โ„•
m - 
n: โ„•
n) {
m: โ„•
m, 
n: โ„•
n} := 
Goals accomplished! ๐Ÿ™
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

FrobeniusNumber (m * n - m - n) {m, n}
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

FrobeniusNumber (m * n - m - n) {m, n}
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

IsGreatest { k | ยฌk โˆˆ AddSubmonoid.closure {m, n} } (m * n - m - n)
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

FrobeniusNumber (m * n - m - n) {m, n}
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

IsGreatest { k | ยฌโˆƒ m_1 n_1, m_1 โ€ข m + n_1 โ€ข n = k } (m * n - m - n)
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

IsGreatest { k | ยฌโˆƒ m_1 n_1, m_1 โ€ข m + n_1 โ€ข n = k } (m * n - m - n)
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

FrobeniusNumber (m * n - m - n) {m, n}
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

IsGreatest { k | ยฌโˆƒ m_1 n_1, m_1 โ€ข m + n_1 โ€ข n = k } (m * n - m - n)
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

FrobeniusNumber (m * n - m - n) {m, n}
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

left
m * n - m - n โˆˆ { k | ยฌโˆƒ m_1 n_1, m_1 โ€ข m + n_1 โ€ข n = k }
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

right
m * n - m - n โˆˆ upperBounds { k | ยฌโˆƒ m_1 n_1, m_1 โ€ข m + n_1 โ€ข n = k }
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

FrobeniusNumber (m * n - m - n) {m, n}
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

left
m * n - m - n โˆˆ { k | ยฌโˆƒ m_1 n_1, m_1 โ€ข m + n_1 โ€ข n = k }
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

left
m * n - m - n โˆˆ { k | ยฌโˆƒ m_1 n_1, m_1 โ€ข m + n_1 โ€ข n = k }
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

right
m * n - m - n โˆˆ upperBounds { k | ยฌโˆƒ m_1 n_1, m_1 โ€ข m + n_1 โ€ข n = k }
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

left
m * n - m - n โˆˆ { k | โˆ€ (m_1 n_1 : โ„•), m_1 โ€ข m + n_1 โ€ข n โ‰  k }
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

left
m * n - m - n โˆˆ { k | ยฌโˆƒ m_1 n_1, m_1 โ€ข m + n_1 โ€ข n = k }
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

a, b: โ„•

h: a โ€ข m + b โ€ข n = m * n - m - n

left
False
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

left
m * n - m - n โˆˆ { k | ยฌโˆƒ m_1 n_1, m_1 โ€ข m + n_1 โ€ข n = k }
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

a, b: โ„•

h: a โ€ข m + b โ€ข n = m * n - m - n

left
(a + 1) * m + (b + 1) * n = m * n
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

left
m * n - m - n โˆˆ { k | ยฌโˆƒ m_1 n_1, m_1 โ€ข m + n_1 โ€ข n = k }
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

a, b: โ„•

h: a * m + b * n = m * n - (m + n)

left
(a + 1) * m + (b + 1) * n = m * n
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

left
m * n - m - n โˆˆ { k | ยฌโˆƒ m_1 n_1, m_1 โ€ข m + n_1 โ€ข n = k }
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

a, b: โ„•

h: โ†‘a * โ†‘m + โ†‘b * โ†‘n = โ†‘m * โ†‘n - (โ†‘m + โ†‘n)

left
(โ†‘a + 1) * โ†‘m + (โ†‘b + 1) * โ†‘n = โ†‘m * โ†‘n
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

left
m * n - m - n โˆˆ { k | ยฌโˆƒ m_1 n_1, m_1 โ€ข m + n_1 โ€ข n = k }
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

a, b: โ„•

h: โ†‘a * โ†‘m + โ†‘b * โ†‘n = โ†‘m * โ†‘n - (โ†‘m + โ†‘n)

left
(โ†‘a + 1) * โ†‘m + (โ†‘b + 1) * โ†‘n = โ†‘m * โ†‘n
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

a, b: โ„•

hโœ: โ†‘a * โ†‘m + โ†‘b * โ†‘n = โ†‘m * โ†‘n - (โ†‘m + โ†‘n)

h: โ†‘a * โ†‘m + โ†‘b * โ†‘n - (โ†‘m * โ†‘n - (โ†‘m + โ†‘n)) = 0

left
(โ†‘a + 1) * โ†‘m + (โ†‘b + 1) * โ†‘n - โ†‘m * โ†‘n = 0
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

a, b: โ„•

hโœ: โ†‘a * โ†‘m + โ†‘b * โ†‘n = โ†‘m * โ†‘n - (โ†‘m + โ†‘n)

h: โ†‘a * โ†‘m + โ†‘b * โ†‘n - (โ†‘m * โ†‘n - (โ†‘m + โ†‘n)) = 0

left
(โ†‘a + 1) * โ†‘m + (โ†‘b + 1) * โ†‘n - โ†‘m * โ†‘n = 0
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

a, b: โ„•

hโœ: โ†‘a * โ†‘m + โ†‘b * โ†‘n = โ†‘m * โ†‘n - (โ†‘m + โ†‘n)

h: โ†‘a * โ†‘m + โ†‘b * โ†‘n - (โ†‘m * โ†‘n - (โ†‘m + โ†‘n)) = 0

left
(โ†‘a + 1) * โ†‘m + (โ†‘b + 1) * โ†‘n - โ†‘m * โ†‘n = 0
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

left
m * n - m - n โˆˆ { k | ยฌโˆƒ m_1 n_1, m_1 โ€ข m + n_1 โ€ข n = k }
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

a, b: โ„•

hโœ: โ†‘a * โ†‘m + โ†‘b * โ†‘n = โ†‘m * โ†‘n - (โ†‘m + โ†‘n)

h: โ†‘a * โ†‘m + โ†‘b * โ†‘n - (โ†‘m * โ†‘n - (โ†‘m + โ†‘n)) = 0

left
(โ†‘a + 1) * โ†‘m + (โ†‘b + 1) * โ†‘n - โ†‘m * โ†‘n = 0
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

a, b: โ„•

hโœ: โ†‘a * โ†‘m + โ†‘b * โ†‘n = โ†‘m * โ†‘n - (โ†‘m + โ†‘n)

h: โ†‘a * โ†‘m + โ†‘b * โ†‘n - (โ†‘m * โ†‘n - (โ†‘m + โ†‘n)) = 0

left
(โ†‘a + 1) * โ†‘m + (โ†‘b + 1) * โ†‘n - โ†‘m * โ†‘n = โ†‘a * โ†‘m + โ†‘b * โ†‘n - (โ†‘m * โ†‘n - (โ†‘m + โ†‘n))
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

a, b: โ„•

hโœ: โ†‘a * โ†‘m + โ†‘b * โ†‘n = โ†‘m * โ†‘n - (โ†‘m + โ†‘n)

h: โ†‘a * โ†‘m + โ†‘b * โ†‘n - (โ†‘m * โ†‘n - (โ†‘m + โ†‘n)) = 0

left
(โ†‘a + 1) * โ†‘m + (โ†‘b + 1) * โ†‘n - โ†‘m * โ†‘n = โ†‘a * โ†‘m + โ†‘b * โ†‘n - (โ†‘m * โ†‘n - (โ†‘m + โ†‘n))
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

left
m * n - m - n โˆˆ { k | ยฌโˆƒ m_1 n_1, m_1 โ€ข m + n_1 โ€ข n = k }
Goals accomplished! ๐Ÿ™
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

FrobeniusNumber (m * n - m - n) {m, n}
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

right
m * n - m - n โˆˆ upperBounds { k | ยฌโˆƒ m_1 n_1, m_1 โ€ข m + n_1 โ€ข n = k }
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

right
m * n - m - n โˆˆ upperBounds { k | ยฌโˆƒ m_1 n_1, m_1 โ€ข m + n_1 โ€ข n = k }
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

k: โ„•

hk: k โˆˆ { k | ยฌโˆƒ m_1 n_1, m_1 โ€ข m + n_1 โ€ข n = k }

right
k โ‰ค m * n - m - n
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

right
m * n - m - n โˆˆ upperBounds { k | ยฌโˆƒ m_1 n_1, m_1 โ€ข m + n_1 โ€ข n = k }
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

k: โ„•

hk: ยฌโˆƒ m_1 n_1, m_1 * m + n_1 * n = k

right
k โ‰ค m * n - m - n
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

right
m * n - m - n โˆˆ upperBounds { k | ยฌโˆƒ m_1 n_1, m_1 โ€ข m + n_1 โ€ข n = k }
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

k: โ„•

hk: m * n - m - n < k

right
โˆƒ m_1 n_1, m_1 * m + n_1 * n = k
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

right
m * n - m - n โˆˆ upperBounds { k | ยฌโˆƒ m_1 n_1, m_1 โ€ข m + n_1 โ€ข n = k }
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

k: โ„•

hk: m * n - m - n < k

x:= chineseRemainder cop 0 k: { k_1 // k_1 โ‰ก 0 [MOD m] โˆง k_1 โ‰ก k [MOD n] }

right
โˆƒ m_1 n_1, m_1 * m + n_1 * n = k
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

right
m * n - m - n โˆˆ upperBounds { k | ยฌโˆƒ m_1 n_1, m_1 โ€ข m + n_1 โ€ข n = k }
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

k: โ„•

hk: m * n - m - n < k

x:= chineseRemainder cop 0 k: { k_1 // k_1 โ‰ก 0 [MOD m] โˆง k_1 โ‰ก k [MOD n] }

hx: โ†‘x < m * n

right
โˆƒ m_1 n_1, m_1 * m + n_1 * n = k
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

right
m * n - m - n โˆˆ upperBounds { k | ยฌโˆƒ m_1 n_1, m_1 โ€ข m + n_1 โ€ข n = k }
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

k: โ„•

hk: m * n - m - n < k

x:= chineseRemainder cop 0 k: { k_1 // k_1 โ‰ก 0 [MOD m] โˆง k_1 โ‰ก k [MOD n] }

hx: โ†‘x < m * n

key: โ†‘x โ‰ค k

right
โˆƒ m_1 n_1, m_1 * m + n_1 * n = k
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

k: โ„•

hk: m * n - m - n < k

x:= chineseRemainder cop 0 k: { k_1 // k_1 โ‰ก 0 [MOD m] โˆง k_1 โ‰ก k [MOD n] }

hx: โ†‘x < m * n

key
โ†‘x โ‰ค k
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

right
m * n - m - n โˆˆ upperBounds { k | ยฌโˆƒ m_1 n_1, m_1 โ€ข m + n_1 โ€ข n = k }
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

k: โ„•

hk: m * n - m - n < k

x:= chineseRemainder cop 0 k: { k_1 // k_1 โ‰ก 0 [MOD m] โˆง k_1 โ‰ก k [MOD n] }

hx: โ†‘x < m * n

key: โ†‘x โ‰ค k

right
โˆƒ m_1 n_1, m_1 * m + n_1 * n = k
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

k: โ„•

hk: m * n - m - n < k

x:= chineseRemainder cop 0 k: { k_1 // k_1 โ‰ก 0 [MOD m] โˆง k_1 โ‰ก k [MOD n] }

hx: โ†‘x < m * n

key: โ†‘x โ‰ค k

right
โˆƒ m_1 n_1, m_1 * m + n_1 * n = k
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

k: โ„•

hk: m * n - m - n < k

x:= chineseRemainder cop 0 k: { k_1 // k_1 โ‰ก 0 [MOD m] โˆง k_1 โ‰ก k [MOD n] }

hx: โ†‘x < m * n

key
โ†‘x โ‰ค k
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

k: โ„•

hk: m * n - m - n < k

x:= chineseRemainder cop 0 k: { k_1 // k_1 โ‰ก 0 [MOD m] โˆง k_1 โ‰ก k [MOD n] }

hx: โ†‘x < m * n

key: โ†‘x โ‰ค k

a: โ„•

ha: โ†‘x = m * a

right.intro
โˆƒ m_1 n_1, m_1 * m + n_1 * n = k
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

k: โ„•

hk: m * n - m - n < k

x:= chineseRemainder cop 0 k: { k_1 // k_1 โ‰ก 0 [MOD m] โˆง k_1 โ‰ก k [MOD n] }

hx: โ†‘x < m * n

key: โ†‘x โ‰ค k

right
โˆƒ m_1 n_1, m_1 * m + n_1 * n = k
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

k: โ„•

hk: m * n - m - n < k

x:= chineseRemainder cop 0 k: { k_1 // k_1 โ‰ก 0 [MOD m] โˆง k_1 โ‰ก k [MOD n] }

hx: โ†‘x < m * n

key: โ†‘x โ‰ค k

a: โ„•

ha: โ†‘x = m * a

b: โ„•

hb: k - โ†‘x = n * b

right.intro.intro
โˆƒ m_1 n_1, m_1 * m + n_1 * n = k
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

k: โ„•

hk: m * n - m - n < k

x:= chineseRemainder cop 0 k: { k_1 // k_1 โ‰ก 0 [MOD m] โˆง k_1 โ‰ก k [MOD n] }

hx: โ†‘x < m * n

key: โ†‘x โ‰ค k

right
โˆƒ m_1 n_1, m_1 * m + n_1 * n = k
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

k: โ„•

hk: m * n - m - n < k

x:= chineseRemainder cop 0 k: { k_1 // k_1 โ‰ก 0 [MOD m] โˆง k_1 โ‰ก k [MOD n] }

hx: โ†‘x < m * n

key: โ†‘x โ‰ค k

a: โ„•

ha: โ†‘x = m * a

b: โ„•

hb: k - โ†‘x = n * b

right.intro.intro
โˆƒ m_1 n_1, m_1 * m + n_1 * n = k
Goals accomplished! ๐Ÿ™
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

k: โ„•

hk: m * n - m - n < k

x:= chineseRemainder cop 0 k: { k_1 // k_1 โ‰ก 0 [MOD m] โˆง k_1 โ‰ก k [MOD n] }

hx: โ†‘x < m * n

key: โ†‘x โ‰ค k

a: โ„•

ha: โ†‘x = m * a

b: โ„•

hb: k - โ†‘x = n * b

a * m + b * n = k
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

k: โ„•

hk: m * n - m - n < k

x:= chineseRemainder cop 0 k: { k_1 // k_1 โ‰ก 0 [MOD m] โˆง k_1 โ‰ก k [MOD n] }

hx: โ†‘x < m * n

key: โ†‘x โ‰ค k

a: โ„•

ha: โ†‘x = m * a

b: โ„•

hb: k - โ†‘x = n * b

a * m + b * n = k
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

k: โ„•

hk: m * n - m - n < k

x:= chineseRemainder cop 0 k: { k_1 // k_1 โ‰ก 0 [MOD m] โˆง k_1 โ‰ก k [MOD n] }

hx: โ†‘x < m * n

key: โ†‘x โ‰ค k

a: โ„•

ha: โ†‘x = m * a

b: โ„•

hb: k - โ†‘x = n * b

m * a + b * n = k
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

k: โ„•

hk: m * n - m - n < k

x:= chineseRemainder cop 0 k: { k_1 // k_1 โ‰ก 0 [MOD m] โˆง k_1 โ‰ก k [MOD n] }

hx: โ†‘x < m * n

key: โ†‘x โ‰ค k

a: โ„•

ha: โ†‘x = m * a

b: โ„•

hb: k - โ†‘x = n * b

a * m + b * n = k
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

k: โ„•

hk: m * n - m - n < k

x:= chineseRemainder cop 0 k: { k_1 // k_1 โ‰ก 0 [MOD m] โˆง k_1 โ‰ก k [MOD n] }

hx: โ†‘x < m * n

key: โ†‘x โ‰ค k

a: โ„•

ha: โ†‘x = m * a

b: โ„•

hb: k - โ†‘x = n * b

โ†‘x + b * n = k
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

k: โ„•

hk: m * n - m - n < k

x:= chineseRemainder cop 0 k: { k_1 // k_1 โ‰ก 0 [MOD m] โˆง k_1 โ‰ก k [MOD n] }

hx: โ†‘x < m * n

key: โ†‘x โ‰ค k

a: โ„•

ha: โ†‘x = m * a

b: โ„•

hb: k - โ†‘x = n * b

a * m + b * n = k
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

k: โ„•

hk: m * n - m - n < k

x:= chineseRemainder cop 0 k: { k_1 // k_1 โ‰ก 0 [MOD m] โˆง k_1 โ‰ก k [MOD n] }

hx: โ†‘x < m * n

key: โ†‘x โ‰ค k

a: โ„•

ha: โ†‘x = m * a

b: โ„•

hb: k - โ†‘x = n * b

โ†‘x + n * b = k
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

k: โ„•

hk: m * n - m - n < k

x:= chineseRemainder cop 0 k: { k_1 // k_1 โ‰ก 0 [MOD m] โˆง k_1 โ‰ก k [MOD n] }

hx: โ†‘x < m * n

key: โ†‘x โ‰ค k

a: โ„•

ha: โ†‘x = m * a

b: โ„•

hb: k - โ†‘x = n * b

a * m + b * n = k
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

k: โ„•

hk: m * n - m - n < k

x:= chineseRemainder cop 0 k: { k_1 // k_1 โ‰ก 0 [MOD m] โˆง k_1 โ‰ก k [MOD n] }

hx: โ†‘x < m * n

key: โ†‘x โ‰ค k

a: โ„•

ha: โ†‘x = m * a

b: โ„•

hb: k - โ†‘x = n * b

โ†‘x + (k - โ†‘x) = k
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

k: โ„•

hk: m * n - m - n < k

x:= chineseRemainder cop 0 k: { k_1 // k_1 โ‰ก 0 [MOD m] โˆง k_1 โ‰ก k [MOD n] }

hx: โ†‘x < m * n

key: โ†‘x โ‰ค k

a: โ„•

ha: โ†‘x = m * a

b: โ„•

hb: k - โ†‘x = n * b

a * m + b * n = k
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

k: โ„•

hk: m * n - m - n < k

x:= chineseRemainder cop 0 k: { k_1 // k_1 โ‰ก 0 [MOD m] โˆง k_1 โ‰ก k [MOD n] }

hx: โ†‘x < m * n

key: โ†‘x โ‰ค k

a: โ„•

ha: โ†‘x = m * a

b: โ„•

hb: k - โ†‘x = n * b

k = k
Goals accomplished! ๐Ÿ™
Goals accomplished! ๐Ÿ™
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

right
m * n - m - n โˆˆ upperBounds { k | ยฌโˆƒ m_1 n_1, m_1 โ€ข m + n_1 โ€ข n = k }
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

k: โ„•

hk: m * n - m - n < k

x:= chineseRemainder cop 0 k: { k_1 // k_1 โ‰ก 0 [MOD m] โˆง k_1 โ‰ก k [MOD n] }

hx: โ†‘x < m * n

key
โ†‘x โ‰ค m * n - m - n + n
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

right
m * n - m - n โˆˆ upperBounds { k | ยฌโˆƒ m_1 n_1, m_1 โ€ข m + n_1 โ€ข n = k }
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

k: โ„•

hk: m * n - m - n < k

x:= chineseRemainder cop 0 k: { k_1 // k_1 โ‰ก 0 [MOD m] โˆง k_1 โ‰ก k [MOD n] }

hx: โ†‘x < m * n

key
โ†‘x โ‰ค m * n - m - n + n
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

k: โ„•

hk: m * n - m - n < k

x:= chineseRemainder cop 0 k: { k_1 // k_1 โ‰ก 0 [MOD m] โˆง k_1 โ‰ก k [MOD n] }

hx: โ†‘x < m * n

key
โ†‘x โ‰ค m * n - m
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

k: โ„•

hk: m * n - m - n < k

x:= chineseRemainder cop 0 k: { k_1 // k_1 โ‰ก 0 [MOD m] โˆง k_1 โ‰ก k [MOD n] }

hx: โ†‘x < m * n

key
โ†‘x โ‰ค m * n - m
m, n: โ„•

cop: coprime m n

hm: 1 < m

hn: 1 < n

hmn: m + n โ‰ค m * n

right
m * n - m - n โˆˆ upperBounds { k | ยฌโˆƒ m_1 n_1, m_1 โ€ข m + n_1 โ€ข n = k }
Goals accomplished! ๐Ÿ™

#align is_frobenius_number_pair 
frobeniusNumber_pair: โˆ€ {m n : โ„•}, coprime m n โ†’ 1 < m โ†’ 1 < n โ†’ FrobeniusNumber (m * n - m - n) {m, n}
frobeniusNumber_pair