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 ⊢ A ∈ ℕ ∧ B ∈ ℕ → ∃ x ∈ ℕ A ≤ x ∧ B ≤ x

Proof

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