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.
```/-
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 โ โ PropFrobeniusNumber (n: โn : โ: Typeโ) (s: Set โs : Set: Type ?u.4 โ Type ?u.4Set โ: Typeโ) : Prop: TypeProp :=
IsGreatest: {ฮฑ : Type ?u.10} โ [inst : Preorder ฮฑ] โ Set ฮฑ โ ฮฑ โ PropIsGreatest { k: ?m.18k | k: ?m.18k โ AddSubmonoid.closure: {M : Type ?u.25} โ [inst : AddZeroClass M] โ Set M โ AddSubmonoid MAddSubmonoid.closure s: Set โs } n: โn
#align is_frobenius_number FrobeniusNumber: โ โ Set โ โ PropFrobeniusNumber

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 ncop : coprime: โ โ โ โ Propcoprime m: โm n: โn) (hm: 1 < mhm : 1: ?m.2101 < m: โm) (hn: 1 < nhn : 1: ?m.2471 < n: โn) :
FrobeniusNumber: โ โ Set โ โ PropFrobeniusNumber (m: โm * n: โn - m: โm - n: โn) {m: โm, n: โn} := byGoals accomplished! ๐
m, n: โcop: coprime m nhm: 1 < mhn: 1 < nFrobeniusNumber (m * n - m - n) {m, n}simp_rw [m, n: โcop: coprime m nhm: 1 < mhn: 1 < nFrobeniusNumber (m * n - m - n) {m, n}FrobeniusNumber: โ โ Set โ โ PropFrobeniusNumber,m, n: โcop: coprime m nhm: 1 < mhn: 1 < nIsGreatest { k | ยฌk โ AddSubmonoid.closure {m, n} } (m * n - m - n) m, n: โcop: coprime m nhm: 1 < mhn: 1 < nFrobeniusNumber (m * n - m - n) {m, n}AddSubmonoid.mem_closure_pairm, n: โcop: coprime m nhm: 1 < mhn: 1 < nIsGreatest { k | ยฌโ m_1 n_1, m_1 โข m + n_1 โข n = k } (m * n - m - n)]m, n: โcop: coprime m nhm: 1 < mhn: 1 < nIsGreatest { k | ยฌโ m_1 n_1, m_1 โข m + n_1 โข n = k } (m * n - m - n)
m, n: โcop: coprime m nhm: 1 < mhn: 1 < nFrobeniusNumber (m * n - m - n) {m, n}have hmn: m + n โค m * nhmn : m: โm + n: โn โค m: โm * n: โn := add_le_mul: โ {ฮฑ : Type ?u.1199} [inst : LinearOrderedSemiring ฮฑ] {a b : ฮฑ}, 2 โค a โ 2 โค b โ a + b โค a * badd_le_mul hm: 1 < mhm hn: 1 < nhnm, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nIsGreatest { k | ยฌโ m_1 n_1, m_1 โข m + n_1 โข n = k } (m * n - m - n)
m, n: โcop: coprime m nhm: 1 < mhn: 1 < nFrobeniusNumber (m * n - m - n) {m, n}constructorm, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nleftm * n - m - n โ { k | ยฌโ m_1 n_1, m_1 โข m + n_1 โข n = k }m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nrightm * n - m - n โ upperBounds { k | ยฌโ m_1 n_1, m_1 โข m + n_1 โข n = k }
m, n: โcop: coprime m nhm: 1 < mhn: 1 < nFrobeniusNumber (m * n - m - n) {m, n}ยทm, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nleftm * n - m - n โ { k | ยฌโ m_1 n_1, m_1 โข m + n_1 โข n = k } m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nleftm * n - m - n โ { k | ยฌโ m_1 n_1, m_1 โข m + n_1 โข n = k }m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nrightm * n - m - n โ upperBounds { k | ยฌโ m_1 n_1, m_1 โข m + n_1 โข n = k }push_negm, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nleftm * n - m - n โ { k | โ (m_1 n_1 : โ), m_1 โข m + n_1 โข n โ  k }
m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nleftm * n - m - n โ { k | ยฌโ m_1 n_1, m_1 โข m + n_1 โข n = k }intro a: โa b: โb h: a โข m + b โข n = m * n - m - nhm, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * na, b: โh: a โข m + b โข n = m * n - m - nleftFalse
m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nleftm * n - m - n โ { k | ยฌโ m_1 n_1, m_1 โข m + n_1 โข n = k }apply cop: coprime m ncop.mul_add_mul_ne_mul: โ {m n a b : โ}, coprime m n โ a โ  0 โ b โ  0 โ a * m + b * n โ  m * nmul_add_mul_ne_mul (add_one_ne_zero: โ (n : โ), n + 1 โ  0add_one_ne_zero a: โa) (add_one_ne_zero: โ (n : โ), n + 1 โ  0add_one_ne_zero b: โb)m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * na, b: โh: a โข m + b โข n = m * n - m - nleft(a + 1) * m + (b + 1) * n = m * n
m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nleftm * n - m - n โ { k | ยฌโ m_1 n_1, m_1 โข m + n_1 โข n = k }simp only [Nat.sub_sub: โ (n m k : โ), n - m - k = n - (m + k)Nat.sub_sub, smul_eq_mul: โ (ฮฑ : Type ?u.1349) [inst : Mul ฮฑ] {a a' : ฮฑ}, a โข a' = a * a'smul_eq_mul] at h: a โข m + b โข n = m * n - m - nhm, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * na, b: โh: a * m + b * n = m * n - (m + n)left(a + 1) * m + (b + 1) * n = m * n
m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nleftm * n - m - n โ { k | ยฌโ m_1 n_1, m_1 โข m + n_1 โข n = k }zify [hmn: m + n โค m * nhmn] at h: a * m + b * n = m * n - (m + n)h โขm, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * na, b: โh: โa * โm + โb * โn = โm * โn - (โm + โn)left(โa + 1) * โm + (โb + 1) * โn = โm * โn
m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nleftm * n - m - n โ { k | ยฌโ m_1 n_1, m_1 โข m + n_1 โข n = k }rw [m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * na, b: โh: โa * โm + โb * โn = โm * โn - (โm + โn)left(โa + 1) * โm + (โb + 1) * โn = โm * โnโ sub_eq_zero: โ {G : Type ?u.2362} [inst : AddGroup G] {a b : G}, a - b = 0 โ a = bsub_eq_zerom, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * na, b: โhโ: โa * โm + โb * โn = โm * โn - (โm + โn)h: โa * โm + โb * โn - (โm * โn - (โm + โn)) = 0left(โa + 1) * โm + (โb + 1) * โn - โm * โn = 0]m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * na, b: โhโ: โa * โm + โb * โn = โm * โn - (โm + โn)h: โa * โm + โb * โn - (โm * โn - (โm + โn)) = 0left(โa + 1) * โm + (โb + 1) * โn - โm * โn = 0 at h: โa * โm + โb * โn = โm * โn - (โm + โn)h โขm, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * na, b: โhโ: โa * โm + โb * โn = โm * โn - (โm + โn)h: โa * โm + โb * โn - (โm * โn - (โm + โn)) = 0left(โa + 1) * โm + (โb + 1) * โn - โm * โn = 0
m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nleftm * n - m - n โ { k | ยฌโ m_1 n_1, m_1 โข m + n_1 โข n = k }rw [m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * na, b: โhโ: โa * โm + โb * โn = โm * โn - (โm + โn)h: โa * โm + โb * โn - (โm * โn - (โm + โn)) = 0left(โa + 1) * โm + (โb + 1) * โn - โm * โn = 0โ h: โa * โm + โb * โn - (โm * โn - (โm + โn)) = 0hm, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * na, b: โhโ: โa * โm + โb * โn = โm * โn - (โm + โn)h: โa * โm + โb * โn - (โm * โn - (โm + โn)) = 0left(โa + 1) * โm + (โb + 1) * โn - โm * โn = โa * โm + โb * โn - (โm * โn - (โm + โn))]m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * na, b: โhโ: โa * โm + โb * โn = โm * โn - (โm + โn)h: โa * โm + โb * โn - (โm * โn - (โm + โn)) = 0left(โa + 1) * โm + (โb + 1) * โn - โm * โn = โa * โm + โb * โn - (โm * โn - (โm + โn))
m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nleftm * n - m - n โ { k | ยฌโ m_1 n_1, m_1 โข m + n_1 โข n = k }ringGoals accomplished! ๐
m, n: โcop: coprime m nhm: 1 < mhn: 1 < nFrobeniusNumber (m * n - m - n) {m, n}ยทm, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nrightm * n - m - n โ upperBounds { k | ยฌโ m_1 n_1, m_1 โข m + n_1 โข n = k } m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nrightm * n - m - n โ upperBounds { k | ยฌโ m_1 n_1, m_1 โข m + n_1 โข n = k }intro k: โk hk: k โ { k | ยฌโ m_1 n_1, m_1 โข m + n_1 โข n = k }hkm, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nk: โhk: k โ { k | ยฌโ m_1 n_1, m_1 โข m + n_1 โข n = k }rightk โค m * n - m - n
m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nrightm * n - m - n โ upperBounds { k | ยฌโ m_1 n_1, m_1 โข m + n_1 โข n = k }dsimp at hk: k โ { k | ยฌโ m_1 n_1, m_1 โข m + n_1 โข n = k }hkm, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nk: โhk: ยฌโ m_1 n_1, m_1 * m + n_1 * n = krightk โค m * n - m - n
m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nrightm * n - m - n โ upperBounds { k | ยฌโ m_1 n_1, m_1 โข m + n_1 โข n = k }contrapose! hk: ยฌโ m_1 n_1, m_1 * m + n_1 * n = khkm, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nk: โhk: m * n - m - n < krightโ m_1 n_1, m_1 * m + n_1 * n = k
m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nrightm * n - m - n โ upperBounds { k | ยฌโ m_1 n_1, m_1 โข m + n_1 โข n = k }let x: ?m.2799x := chineseRemainder: {m n : โ} โ coprime n m โ (a b : โ) โ { k // k โก a [MOD n] โง k โก b [MOD m] }chineseRemainder cop: coprime m ncop 0: ?m.28050 k: โkm, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nk: โhk: m * n - m - n < kx:= 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 nhm: 1 < mhn: 1 < nhmn: m + n โค m * nrightm * n - m - n โ upperBounds { k | ยฌโ m_1 n_1, m_1 โข m + n_1 โข n = k }have hx: โx < m * nhx : x: ?m.2799x.val: {ฮฑ : Sort ?u.2822} โ {p : ฮฑ โ Prop} โ Subtype p โ ฮฑval < m: โm * n: โn := chineseRemainder_lt_mul: โ {m n : โ} (co : coprime n m) (a b : โ), n โ  0 โ m โ  0 โ โ(chineseRemainder co a b) < n * mchineseRemainder_lt_mul cop: coprime m ncop 0: ?m.28800 k: โk (ne_bot_of_gt: โ {ฮฑ : Type ?u.2913} [inst : Preorder ฮฑ] [inst_1 : OrderBot ฮฑ] {a b : ฮฑ}, a < b โ b โ  โฅne_bot_of_gt hm: 1 < mhm) (ne_bot_of_gt: โ {ฮฑ : Type ?u.3094} [inst : Preorder ฮฑ] [inst_1 : OrderBot ฮฑ] {a b : ฮฑ}, a < b โ b โ  โฅne_bot_of_gt hn: 1 < nhn)m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nk: โhk: m * n - m - n < kx:= chineseRemainder cop 0 k: { k_1 // k_1 โก 0 [MOD m] โง k_1 โก k [MOD n] }hx: โx < m * nrightโ m_1 n_1, m_1 * m + n_1 * n = k
m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nrightm * n - m - n โ upperBounds { k | ยฌโ m_1 n_1, m_1 โข m + n_1 โข n = k }suffices key: โx โค kkey : x: ?m.2799x.1: {ฮฑ : Sort ?u.3194} โ {p : ฮฑ โ Prop} โ Subtype p โ ฮฑ1 โค k: โkm, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nk: โhk: m * n - m - n < kx:= chineseRemainder cop 0 k: { k_1 // k_1 โก 0 [MOD m] โง k_1 โก k [MOD n] }hx: โx < m * nkey: โx โค krightโ m_1 n_1, m_1 * m + n_1 * n = km, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nk: โhk: m * n - m - n < kx:= chineseRemainder cop 0 k: { k_1 // k_1 โก 0 [MOD m] โง k_1 โก k [MOD n] }hx: โx < m * nkeyโx โค k
m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nrightm * n - m - n โ upperBounds { k | ยฌโ m_1 n_1, m_1 โข m + n_1 โข n = k }ยทm, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nk: โhk: m * n - m - n < kx:= chineseRemainder cop 0 k: { k_1 // k_1 โก 0 [MOD m] โง k_1 โก k [MOD n] }hx: โx < m * nkey: โx โค krightโ m_1 n_1, m_1 * m + n_1 * n = k m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nk: โhk: m * n - m - n < kx:= chineseRemainder cop 0 k: { k_1 // k_1 โก 0 [MOD m] โง k_1 โก k [MOD n] }hx: โx < m * nkey: โx โค krightโ m_1 n_1, m_1 * m + n_1 * n = km, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nk: โhk: m * n - m - n < kx:= chineseRemainder cop 0 k: { k_1 // k_1 โก 0 [MOD m] โง k_1 โก k [MOD n] }hx: โx < m * nkeyโx โค kobtain โจa, haโฉ: m โฃ โxโจa: โaโจa, haโฉ: m โฃ โx, ha: โx = m * ahaโจa, haโฉ: m โฃ โxโฉ := modEq_zero_iff_dvd: โ {n a : โ}, a โก 0 [MOD n] โ n โฃ amodEq_zero_iff_dvd.mp: โ {a b : Prop}, (a โ b) โ a โ bmp x: ?m.2799x.2: โ {ฮฑ : Sort ?u.3214} {p : ฮฑ โ Prop} (self : Subtype p), p โself2.1: โ {a b : Prop}, a โง b โ a1m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nk: โhk: m * n - m - n < kx:= chineseRemainder cop 0 k: { k_1 // k_1 โก 0 [MOD m] โง k_1 โก k [MOD n] }hx: โx < m * nkey: โx โค ka: โha: โx = m * aright.introโ m_1 n_1, m_1 * m + n_1 * n = k
m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nk: โhk: m * n - m - n < kx:= chineseRemainder cop 0 k: { k_1 // k_1 โก 0 [MOD m] โง k_1 โก k [MOD n] }hx: โx < m * nkey: โx โค krightโ m_1 n_1, m_1 * m + n_1 * n = kobtain โจb, hbโฉ: n โฃ k - โxโจb: โbโจb, hbโฉ: n โฃ k - โx, hb: k - โx = n * bhbโจb, hbโฉ: n โฃ k - โxโฉ := (modEq_iff_dvd': โ {n a b : โ}, a โค b โ (a โก b [MOD n] โ n โฃ b - a)modEq_iff_dvd' key: โx โค kkey).mp: โ {a b : Prop}, (a โ b) โ a โ bmp x: ?m.2799x.2: โ {ฮฑ : Sort ?u.3267} {p : ฮฑ โ Prop} (self : Subtype p), p โself2.2: โ {a b : Prop}, a โง b โ b2m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nk: โhk: m * n - m - n < kx:= chineseRemainder cop 0 k: { k_1 // k_1 โก 0 [MOD m] โง k_1 โก k [MOD n] }hx: โx < m * nkey: โx โค ka: โha: โx = m * ab: โhb: k - โx = n * bright.intro.introโ m_1 n_1, m_1 * m + n_1 * n = k
m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nk: โhk: m * n - m - n < kx:= chineseRemainder cop 0 k: { k_1 // k_1 โก 0 [MOD m] โง k_1 โก k [MOD n] }hx: โx < m * nkey: โx โค krightโ m_1 n_1, m_1 * m + n_1 * n = kexact โจa: โa, b: โb, m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nk: โhk: m * n - m - n < kx:= chineseRemainder cop 0 k: { k_1 // k_1 โก 0 [MOD m] โง k_1 โก k [MOD n] }hx: โx < m * nkey: โx โค ka: โha: โx = m * ab: โhb: k - โx = n * bright.intro.introโ m_1 n_1, m_1 * m + n_1 * n = kbyGoals accomplished! ๐ m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nk: โhk: m * n - m - n < kx:= chineseRemainder cop 0 k: { k_1 // k_1 โก 0 [MOD m] โง k_1 โก k [MOD n] }hx: โx < m * nkey: โx โค ka: โha: โx = m * ab: โhb: k - โx = n * ba * m + b * n = krw [m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nk: โhk: m * n - m - n < kx:= chineseRemainder cop 0 k: { k_1 // k_1 โก 0 [MOD m] โง k_1 โก k [MOD n] }hx: โx < m * nkey: โx โค ka: โha: โx = m * ab: โhb: k - โx = n * ba * m + b * n = kmul_comm: โ {G : Type ?u.3321} [inst : CommSemigroup G] (a b : G), a * b = b * amul_comm,m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nk: โhk: m * n - m - n < kx:= chineseRemainder cop 0 k: { k_1 // k_1 โก 0 [MOD m] โง k_1 โก k [MOD n] }hx: โx < m * nkey: โx โค ka: โha: โx = m * ab: โhb: k - โx = n * bm * a + b * n = k m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nk: โhk: m * n - m - n < kx:= chineseRemainder cop 0 k: { k_1 // k_1 โก 0 [MOD m] โง k_1 โก k [MOD n] }hx: โx < m * nkey: โx โค ka: โha: โx = m * ab: โhb: k - โx = n * ba * m + b * n = kโ ha: โx = m * aha,m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nk: โhk: m * n - m - n < kx:= chineseRemainder cop 0 k: { k_1 // k_1 โก 0 [MOD m] โง k_1 โก k [MOD n] }hx: โx < m * nkey: โx โค ka: โha: โx = m * ab: โhb: k - โx = n * bโx + b * n = k m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nk: โhk: m * n - m - n < kx:= chineseRemainder cop 0 k: { k_1 // k_1 โก 0 [MOD m] โง k_1 โก k [MOD n] }hx: โx < m * nkey: โx โค ka: โha: โx = m * ab: โhb: k - โx = n * ba * m + b * n = kmul_comm: โ {G : Type ?u.3379} [inst : CommSemigroup G] (a b : G), a * b = b * amul_comm,m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nk: โhk: m * n - m - n < kx:= chineseRemainder cop 0 k: { k_1 // k_1 โก 0 [MOD m] โง k_1 โก k [MOD n] }hx: โx < m * nkey: โx โค ka: โha: โx = m * ab: โhb: k - โx = n * bโx + n * b = k m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nk: โhk: m * n - m - n < kx:= chineseRemainder cop 0 k: { k_1 // k_1 โก 0 [MOD m] โง k_1 โก k [MOD n] }hx: โx < m * nkey: โx โค ka: โha: โx = m * ab: โhb: k - โx = n * ba * m + b * n = kโ hb: k - โx = n * bhb,m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nk: โhk: m * n - m - n < kx:= chineseRemainder cop 0 k: { k_1 // k_1 โก 0 [MOD m] โง k_1 โก k [MOD n] }hx: โx < m * nkey: โx โค ka: โha: โx = m * ab: โhb: k - โx = n * bโx + (k - โx) = k m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nk: โhk: m * n - m - n < kx:= chineseRemainder cop 0 k: { k_1 // k_1 โก 0 [MOD m] โง k_1 โก k [MOD n] }hx: โx < m * nkey: โx โค ka: โha: โx = m * ab: โhb: k - โx = n * ba * m + b * n = kNat.add_sub_of_le: โ {a b : โ}, a โค b โ a + (b - a) = bNat.add_sub_of_le key: โx โค kkeym, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nk: โhk: m * n - m - n < kx:= chineseRemainder cop 0 k: { k_1 // k_1 โก 0 [MOD m] โง k_1 โก k [MOD n] }hx: โx < m * nkey: โx โค ka: โha: โx = m * ab: โhb: k - โx = n * bk = k]Goals accomplished! ๐โฉGoals accomplished! ๐
m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nrightm * n - m - n โ upperBounds { k | ยฌโ m_1 n_1, m_1 โข m + n_1 โข n = k }refine' ModEq.le_of_lt_add: โ {m a b : โ}, a โก b [MOD m] โ a < b + m โ a โค bModEq.le_of_lt_add x: ?m.2799x.2: โ {ฮฑ : Sort ?u.3448} {p : ฮฑ โ Prop} (self : Subtype p), p โself2.2: โ {a b : Prop}, a โง b โ b2 (lt_of_le_of_lt: โ {ฮฑ : Type ?u.3454} [inst : Preorder ฮฑ] {a b c : ฮฑ}, a โค b โ b < c โ a < clt_of_le_of_lt _: ?m.3457 โค ?m.3458_ (add_lt_add_right: โ {ฮฑ : Type ?u.3485} [inst : Add ฮฑ] [inst_1 : LT ฮฑ]
[i : CovariantClass ฮฑ ฮฑ (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {b c : ฮฑ},
b < c โ โ (a : ฮฑ), b + a < c + aadd_lt_add_right hk: m * n - m - n < khk n: โn))m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nk: โhk: m * n - m - n < kx:= chineseRemainder cop 0 k: { k_1 // k_1 โก 0 [MOD m] โง k_1 โก k [MOD n] }hx: โx < m * nkeyโx โค m * n - m - n + n
m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nrightm * n - m - n โ upperBounds { k | ยฌโ m_1 n_1, m_1 โข m + n_1 โข n = k }rw [m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nk: โhk: m * n - m - n < kx:= chineseRemainder cop 0 k: { k_1 // k_1 โก 0 [MOD m] โง k_1 โก k [MOD n] }hx: โx < m * nkeyโx โค m * n - m - n + nNat.sub_add_cancel: โ {n m : โ}, m โค n โ n - m + m = nNat.sub_add_cancel (le_tsub_of_add_le_left: โ {ฮฑ : Type ?u.3866} [inst : Preorder ฮฑ] [inst_1 : AddCommSemigroup ฮฑ] [inst_2 : Sub ฮฑ] [inst_3 : OrderedSub ฮฑ]
{a b c : ฮฑ} [inst_4 : ContravariantClass ฮฑ ฮฑ (fun x x_1 => x + x_1) fun x x_1 => x โค x_1], a + b โค c โ b โค c - ale_tsub_of_add_le_left hmn: m + n โค m * nhmn)m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nk: โhk: m * n - m - n < kx:= chineseRemainder cop 0 k: { k_1 // k_1 โก 0 [MOD m] โง k_1 โก k [MOD n] }hx: โx < m * nkeyโx โค m * n - m]m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nk: โhk: m * n - m - n < kx:= chineseRemainder cop 0 k: { k_1 // k_1 โก 0 [MOD m] โง k_1 โก k [MOD n] }hx: โx < m * nkeyโx โค m * n - m
m, n: โcop: coprime m nhm: 1 < mhn: 1 < nhmn: m + n โค m * nrightm * n - m - n โ upperBounds { k | ยฌโ m_1 n_1, m_1 โข m + n_1 โข n = k }exact
ModEq.le_of_lt_add: โ {m a b : โ}, a โก b [MOD m] โ a < b + m โ a โค bModEq.le_of_lt_add
(x: ?m.2799x.2: โ {ฮฑ : Sort ?u.4153} {p : ฮฑ โ Prop} (self : Subtype p), p โself2.1: โ {a b : Prop}, a โง b โ a1.trans: โ {n a b c : โ}, a โก b [MOD n] โ b โก c [MOD n] โ a โก c [MOD n]trans (modEq_zero_iff_dvd: โ {n a : โ}, a โก 0 [MOD n] โ n โฃ amodEq_zero_iff_dvd.mpr: โ {a b : Prop}, (a โ b) โ b โ ampr (Nat.dvd_sub': โ {k m n : โ}, k โฃ m โ k โฃ n โ k โฃ m - nNat.dvd_sub' (dvd_mul_right: โ {ฮฑ : Type ?u.4180} [inst : Semigroup ฮฑ] (a b : ฮฑ), a โฃ a * bdvd_mul_right m: โm n: โn) dvd_rfl: โ {ฮฑ : Type ?u.4201} [inst : Monoid ฮฑ] {a : ฮฑ}, a โฃ advd_rfl)).symm: โ {n a b : โ}, a โก b [MOD n] โ b โก a [MOD n]symm)
(lt_of_lt_of_le: โ {ฮฑ : Type ?u.4250} [inst : Preorder ฮฑ] {a b c : ฮฑ}, a < b โ b โค c โ a < clt_of_lt_of_le hx: โx < m * nhx le_tsub_add: โ {ฮฑ : Type ?u.4280} [inst : Preorder ฮฑ] [inst_1 : Add ฮฑ] [inst_2 : Sub ฮฑ] [inst_3 : OrderedSub ฮฑ] {a b : ฮฑ},
b โค b - a + ale_tsub_add)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
```