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

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ∃ 𝑥 ∈ ℕ ( 𝐴 ≤ 𝑥 ∧ 𝐵 ≤ 𝑥 ) )