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