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		elnelall	⊢ ( +∞ ∈ ℝ → ( +∞ ∉ ℝ → 𝑀 ∈ ℕ0 ) )
13	11 12	syl	⊢ ( +∞ ∈ ℕ0 → ( +∞ ∉ ℝ → 𝑀 ∈ ℕ0 ) )
14	10 13	syl6bi	⊢ ( 𝑁 = +∞ → ( 𝑁 ∈ ℕ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 )