This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ ℤ → if M ≤ N N M ∈ ℤ
2 1 ancoms ⊢ M ∈ ℤ ∧ N ∈ ℤ → if M ≤ N N M ∈ ℤ
3 zre ⊢ M ∈ ℤ → M ∈ ℝ
4 zre ⊢ N ∈ ℤ → N ∈ ℝ
5 max1 ⊢ M ∈ ℝ ∧ N ∈ ℝ → M ≤ if M ≤ N N M
6 max2 ⊢ M ∈ ℝ ∧ N ∈ ℝ → N ≤ if M ≤ N N M
7 5 6 jca ⊢ M ∈ ℝ ∧ N ∈ ℝ → M ≤ if M ≤ N N M ∧ N ≤ if M ≤ N N M
8 3 4 7 syl2an ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ≤ if M ≤ N N M ∧ N ≤ if M ≤ N N M
9 breq2 ⊢ k = if M ≤ N N M → M ≤ k ↔ M ≤ if M ≤ N N M
10 breq2 ⊢ k = if M ≤ N N M → N ≤ k ↔ N ≤ if M ≤ N N M
11 9 10 anbi12d ⊢ k = if M ≤ N N M → M ≤ k ∧ N ≤ k ↔ M ≤ if M ≤ N N M ∧ N ≤ if M ≤ N N M
12 11 rspcev ⊢ if M ≤ N N M ∈ ℤ ∧ M ≤ if M ≤ N N M ∧ N ≤ if M ≤ N N M → ∃ k ∈ ℤ M ≤ k ∧ N ≤ k
13 2 8 12 syl2anc ⊢ M ∈ ℤ ∧ N ∈ ℤ → ∃ k ∈ ℤ M ≤ k ∧ N ≤ k