Theorem nn2ge

Description: There exists a positive integer greater than or equal to any two others. (Contributed by NM, 18-Aug-1999)

	Ref	Expression
Assertion	nn2ge	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ∃ 𝑥 ∈ ℕ ( 𝐴 ≤ 𝑥 ∧ 𝐵 ≤ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		nnre	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℝ )
2	1	adantr	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → 𝐴 ∈ ℝ )
3		nnre	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ )
4	3	adantl	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → 𝐵 ∈ ℝ )
5		leid	⊢ ( 𝐵 ∈ ℝ → 𝐵 ≤ 𝐵 )
6	5	anim1ci	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐵 ) )
7	3 6	sylan	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐵 ) )
8		breq2	⊢ ( 𝑥 = 𝐵 → ( 𝐴 ≤ 𝑥 ↔ 𝐴 ≤ 𝐵 ) )
9		breq2	⊢ ( 𝑥 = 𝐵 → ( 𝐵 ≤ 𝑥 ↔ 𝐵 ≤ 𝐵 ) )
10	8 9	anbi12d	⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ≤ 𝑥 ∧ 𝐵 ≤ 𝑥 ) ↔ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐵 ) ) )
11	10	rspcev	⊢ ( ( 𝐵 ∈ ℕ ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐵 ) ) → ∃ 𝑥 ∈ ℕ ( 𝐴 ≤ 𝑥 ∧ 𝐵 ≤ 𝑥 ) )
12	7 11	syldan	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐴 ≤ 𝐵 ) → ∃ 𝑥 ∈ ℕ ( 𝐴 ≤ 𝑥 ∧ 𝐵 ≤ 𝑥 ) )
13	12	adantll	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝐴 ≤ 𝐵 ) → ∃ 𝑥 ∈ ℕ ( 𝐴 ≤ 𝑥 ∧ 𝐵 ≤ 𝑥 ) )
14		leid	⊢ ( 𝐴 ∈ ℝ → 𝐴 ≤ 𝐴 )
15	14	anim1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ≤ 𝐴 ) → ( 𝐴 ≤ 𝐴 ∧ 𝐵 ≤ 𝐴 ) )
16	1 15	sylan	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ≤ 𝐴 ) → ( 𝐴 ≤ 𝐴 ∧ 𝐵 ≤ 𝐴 ) )
17		breq2	⊢ ( 𝑥 = 𝐴 → ( 𝐴 ≤ 𝑥 ↔ 𝐴 ≤ 𝐴 ) )
18		breq2	⊢ ( 𝑥 = 𝐴 → ( 𝐵 ≤ 𝑥 ↔ 𝐵 ≤ 𝐴 ) )
19	17 18	anbi12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝐴 ≤ 𝑥 ∧ 𝐵 ≤ 𝑥 ) ↔ ( 𝐴 ≤ 𝐴 ∧ 𝐵 ≤ 𝐴 ) ) )
20	19	rspcev	⊢ ( ( 𝐴 ∈ ℕ ∧ ( 𝐴 ≤ 𝐴 ∧ 𝐵 ≤ 𝐴 ) ) → ∃ 𝑥 ∈ ℕ ( 𝐴 ≤ 𝑥 ∧ 𝐵 ≤ 𝑥 ) )
21	16 20	syldan	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ≤ 𝐴 ) → ∃ 𝑥 ∈ ℕ ( 𝐴 ≤ 𝑥 ∧ 𝐵 ≤ 𝑥 ) )
22	21	adantlr	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝐵 ≤ 𝐴 ) → ∃ 𝑥 ∈ ℕ ( 𝐴 ≤ 𝑥 ∧ 𝐵 ≤ 𝑥 ) )
23	2 4 13 22	lecasei	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ∃ 𝑥 ∈ ℕ ( 𝐴 ≤ 𝑥 ∧ 𝐵 ≤ 𝑥 ) )