[GOAL]
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
⊢ FrobeniusNumber (m * n - m - n) {m, n}
[PROOFSTEP]
simp_rw [FrobeniusNumber, AddSubmonoid.mem_closure_pair]
[GOAL]
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)
[PROOFSTEP]
have hmn : m + n ≤ m * n := add_le_mul hm hn
[GOAL]
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)
[PROOFSTEP]
constructor
[GOAL]
case left
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
⊢ m * n - m - n ∈ {k | ¬∃ m_1 n_1, m_1 • m + n_1 • n = k}
[PROOFSTEP]
push_neg
[GOAL]
case left
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
⊢ m * n - m - n ∈ {k | ∀ (m_1 n_1 : ℕ), m_1 • m + n_1 • n ≠ k}
[PROOFSTEP]
intro a b h
[GOAL]
case left
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
⊢ False
[PROOFSTEP]
apply cop.mul_add_mul_ne_mul (add_one_ne_zero a) (add_one_ne_zero b)
[GOAL]
case left
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
⊢ (a + 1) * m + (b + 1) * n = m * n
[PROOFSTEP]
simp only [Nat.sub_sub, smul_eq_mul] at h 
[GOAL]
case left
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)
⊢ (a + 1) * m + (b + 1) * n = m * n
[PROOFSTEP]
zify [hmn] at h ⊢
[GOAL]
case left
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)
⊢ (↑a + 1) * ↑m + (↑b + 1) * ↑n = ↑m * ↑n
[PROOFSTEP]
rw [← sub_eq_zero] at h ⊢
[GOAL]
case left
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
⊢ (↑a + 1) * ↑m + (↑b + 1) * ↑n - ↑m * ↑n = 0
[PROOFSTEP]
rw [← h]
[GOAL]
case left
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
⊢ (↑a + 1) * ↑m + (↑b + 1) * ↑n - ↑m * ↑n = ↑a * ↑m + ↑b * ↑n - (↑m * ↑n - (↑m + ↑n))
[PROOFSTEP]
ring
[GOAL]
case right
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
⊢ m * n - m - n ∈ upperBounds {k | ¬∃ m_1 n_1, m_1 • m + n_1 • n = k}
[PROOFSTEP]
intro k hk
[GOAL]
case right
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}
⊢ k ≤ m * n - m - n
[PROOFSTEP]
dsimp at hk 
[GOAL]
case right
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
⊢ k ≤ m * n - m - n
[PROOFSTEP]
contrapose! hk
[GOAL]
case right
m n : ℕ
cop : coprime m n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
k : ℕ
hk : m * n - m - n < k
⊢ ∃ m_1 n_1, m_1 * m + n_1 * n = k
[PROOFSTEP]
let x := chineseRemainder cop 0 k
[GOAL]
case right
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 : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
⊢ ∃ m_1 n_1, m_1 * m + n_1 * n = k
[PROOFSTEP]
have hx : x.val < m * n := chineseRemainder_lt_mul cop 0 k (ne_bot_of_gt hm) (ne_bot_of_gt hn)
[GOAL]
case right
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 : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
hx : ↑x < m * n
⊢ ∃ m_1 n_1, m_1 * m + n_1 * n = k
[PROOFSTEP]
suffices key : x.1 ≤ k
[GOAL]
case right
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 : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
hx : ↑x < m * n
key : ↑x ≤ k
⊢ ∃ m_1 n_1, m_1 * m + n_1 * n = k
[PROOFSTEP]
obtain ⟨a, ha⟩ := modEq_zero_iff_dvd.mp x.2.1
[GOAL]
case right.intro
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 : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
hx : ↑x < m * n
key : ↑x ≤ k
a : ℕ
ha : ↑x = m * a
⊢ ∃ m_1 n_1, m_1 * m + n_1 * n = k
[PROOFSTEP]
obtain ⟨b, hb⟩ := (modEq_iff_dvd' key).mp x.2.2
[GOAL]
case right.intro.intro
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 : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
hx : ↑x < m * n
key : ↑x ≤ k
a : ℕ
ha : ↑x = m * a
b : ℕ
hb : k - ↑x = n * b
⊢ ∃ m_1 n_1, m_1 * m + n_1 * n = k
[PROOFSTEP]
exact ⟨a, b, by rw [mul_comm, ← ha, mul_comm, ← hb, Nat.add_sub_of_le key]⟩
[GOAL]
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 : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
hx : ↑x < m * n
key : ↑x ≤ k
a : ℕ
ha : ↑x = m * a
b : ℕ
hb : k - ↑x = n * b
⊢ a * m + b * n = k
[PROOFSTEP]
rw [mul_comm, ← ha, mul_comm, ← hb, Nat.add_sub_of_le key]
[GOAL]
case key
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 : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
hx : ↑x < m * n
⊢ ↑x ≤ k
[PROOFSTEP]
refine' ModEq.le_of_lt_add x.2.2 (lt_of_le_of_lt _ (add_lt_add_right hk n))
[GOAL]
case key
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 : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
hx : ↑x < m * n
⊢ ↑x ≤ m * n - m - n + n
[PROOFSTEP]
rw [Nat.sub_add_cancel (le_tsub_of_add_le_left hmn)]
[GOAL]
case key
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 : { k_1 // k_1 ≡ 0 [MOD m] ∧ k_1 ≡ k [MOD n] } := chineseRemainder cop 0 k
hx : ↑x < m * n
⊢ ↑x ≤ m * n - m
[PROOFSTEP]
exact
  ModEq.le_of_lt_add (x.2.1.trans (modEq_zero_iff_dvd.mpr (Nat.dvd_sub' (dvd_mul_right m n) dvd_rfl)).symm)
    (lt_of_lt_of_le hx le_tsub_add)
