Metamath Proof Explorer

Theorem z2ge

Description: There exists an integer greater than or equal to any two others. (Contributed by NM, 28-Aug-2005)

Ref Expression
Assertion z2ge ⊢M∈ℤ∧N∈ℤ→∃k∈ℤM≤k∧N≤k

Proof

Step Hyp Ref Expression
1 ifcl ⊢N∈ℤ∧M∈ℤ→ifM≤NNM∈ℤ
2 1 ancoms ⊢M∈ℤ∧N∈ℤ→ifM≤NNM∈ℤ
3 zre ⊢M∈ℤ→M∈ℝ
4 zre ⊢N∈ℤ→N∈ℝ
5 max1 ⊢M∈ℝ∧N∈ℝ→M≤ifM≤NNM
6 max2 ⊢M∈ℝ∧N∈ℝ→N≤ifM≤NNM
7 5 6 jca ⊢M∈ℝ∧N∈ℝ→M≤ifM≤NNM∧N≤ifM≤NNM
8 3 4 7 syl2an ⊢M∈ℤ∧N∈ℤ→M≤ifM≤NNM∧N≤ifM≤NNM
9 breq2 ⊢k=ifM≤NNM→M≤k↔M≤ifM≤NNM
10 breq2 ⊢k=ifM≤NNM→N≤k↔N≤ifM≤NNM
11 9 10 anbi12d ⊢k=ifM≤NNM→M≤k∧N≤k↔M≤ifM≤NNM∧N≤ifM≤NNM
12 11 rspcev ⊢ifM≤NNM∈ℤ∧M≤ifM≤NNM∧N≤ifM≤NNM→∃k∈ℤM≤k∧N≤k
13 2 8 12 syl2anc ⊢M∈ℤ∧N∈ℤ→∃k∈ℤM≤k∧N≤k