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	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ∃ 𝑘 ∈ ℤ ( 𝑀 ≤ 𝑘 ∧ 𝑁 ≤ 𝑘 ) )

Proof

Step	Hyp	Ref	Expression
1		ifcl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ℤ )
2	1	ancoms	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ℤ )
3		zre	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
4		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
5		max1	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 𝑀 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) )
6		max2	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 𝑁 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) )
7	5 6	jca	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∧ 𝑁 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
8	3 4 7	syl2an	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∧ 𝑁 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
9		breq2	⊢ ( 𝑘 = if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) → ( 𝑀 ≤ 𝑘 ↔ 𝑀 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
10		breq2	⊢ ( 𝑘 = if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) → ( 𝑁 ≤ 𝑘 ↔ 𝑁 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
11	9 10	anbi12d	⊢ ( 𝑘 = if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) → ( ( 𝑀 ≤ 𝑘 ∧ 𝑁 ≤ 𝑘 ) ↔ ( 𝑀 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∧ 𝑁 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) )
12	11	rspcev	⊢ ( ( if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ℤ ∧ ( 𝑀 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∧ 𝑁 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) → ∃ 𝑘 ∈ ℤ ( 𝑀 ≤ 𝑘 ∧ 𝑁 ≤ 𝑘 ) )
13	2 8 12	syl2anc	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ∃ 𝑘 ∈ ℤ ( 𝑀 ≤ 𝑘 ∧ 𝑁 ≤ 𝑘 ) )