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

Metamath Proof Explorer

Theorem xnn0lenn0nn0

Description: An extended nonnegative integer which is less than or equal to a nonnegative integer is a nonnegative integer. (Contributed by AV, 24-Nov-2021)

Ref Expression
Assertion xnn0lenn0nn0 ( ( 𝑀 ∈ ℕ0* ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) → 𝑀 ∈ ℕ0 )

Proof

Step Hyp Ref Expression
1 elxnn0 ⊢ ( 𝑀 ∈ ℕ0* ↔ ( 𝑀 ∈ ℕ0 ∨ 𝑀 = +∞ ) )
2 2a1 ⊢ ( 𝑀 ∈ ℕ0 → ( 𝑁 ∈ ℕ0 → ( 𝑀 ≤ 𝑁 → 𝑀 ∈ ℕ0 ) ) )
3 breq1 ⊢ ( 𝑀 = +∞ → ( 𝑀 ≤ 𝑁 ↔ +∞ ≤ 𝑁 ) )
4 3 adantr ⊢ ( ( 𝑀 = +∞ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ≤ 𝑁 ↔ +∞ ≤ 𝑁 ) )
5 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
6 5 rexrd ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ* )
7 xgepnf ⊢ ( 𝑁 ∈ ℝ* → ( +∞ ≤ 𝑁 ↔ 𝑁 = +∞ ) )
8 6 7 syl ⊢ ( 𝑁 ∈ ℕ0 → ( +∞ ≤ 𝑁 ↔ 𝑁 = +∞ ) )
9 pnfnre ⊢ +∞ ∉ ℝ
10 eleq1 ⊢ ( 𝑁 = +∞ → ( 𝑁 ∈ ℕ0 ↔ +∞ ∈ ℕ0 ) )
11 nn0re ⊢ ( +∞ ∈ ℕ0 → +∞ ∈ ℝ )
12 pm2.24nel ⊢ ( +∞ ∈ ℝ → ( +∞ ∉ ℝ → 𝑀 ∈ ℕ0 ) )
13 11 12 syl ⊢ ( +∞ ∈ ℕ0 → ( +∞ ∉ ℝ → 𝑀 ∈ ℕ0 ) )
14 10 13 biimtrdi ⊢ ( 𝑁 = +∞ → ( 𝑁 ∈ ℕ0 → ( +∞ ∉ ℝ → 𝑀 ∈ ℕ0 ) ) )
15 14 com13 ⊢ ( +∞ ∉ ℝ → ( 𝑁 ∈ ℕ0 → ( 𝑁 = +∞ → 𝑀 ∈ ℕ0 ) ) )
16 9 15 ax-mp ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 = +∞ → 𝑀 ∈ ℕ0 ) )
17 8 16 sylbid ⊢ ( 𝑁 ∈ ℕ0 → ( +∞ ≤ 𝑁 → 𝑀 ∈ ℕ0 ) )
18 17 adantl ⊢ ( ( 𝑀 = +∞ ∧ 𝑁 ∈ ℕ0 ) → ( +∞ ≤ 𝑁 → 𝑀 ∈ ℕ0 ) )
19 4 18 sylbid ⊢ ( ( 𝑀 = +∞ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ≤ 𝑁 → 𝑀 ∈ ℕ0 ) )
20 19 ex ⊢ ( 𝑀 = +∞ → ( 𝑁 ∈ ℕ0 → ( 𝑀 ≤ 𝑁 → 𝑀 ∈ ℕ0 ) ) )
21 2 20 jaoi ⊢ ( ( 𝑀 ∈ ℕ0 ∨ 𝑀 = +∞ ) → ( 𝑁 ∈ ℕ0 → ( 𝑀 ≤ 𝑁 → 𝑀 ∈ ℕ0 ) ) )
22 1 21 sylbi ⊢ ( 𝑀 ∈ ℕ0* → ( 𝑁 ∈ ℕ0 → ( 𝑀 ≤ 𝑁 → 𝑀 ∈ ℕ0 ) ) )
23 22 3imp ⊢ ( ( 𝑀 ∈ ℕ0* ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) → 𝑀 ∈ ℕ0 )