Metamath Proof Explorer

Theorem xnn0lem1lt

Description: Extended nonnegative integer ordering relation. (Contributed by Thierry Arnoux, 30-Jul-2023)

		Ref	Expression
	Assertion	xnn0lem1lt	⊢ ( ( 𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀^* ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝑀 − 1 ) < 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		nn0lem1lt	⊢ ( ( 𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝑀 − 1 ) < 𝑁 ) )
2	1	adantlr	⊢ ( ( ( 𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀^* ) ∧ 𝑁 ∈ ℕ₀ ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝑀 − 1 ) < 𝑁 ) )
3		nn0re	⊢ ( 𝑀 ∈ ℕ₀ → 𝑀 ∈ ℝ )
4	3	rexrd	⊢ ( 𝑀 ∈ ℕ₀ → 𝑀 ∈ ℝ^* )
5		pnfge	⊢ ( 𝑀 ∈ ℝ^* → 𝑀 ≤ +∞ )
6	4 5	syl	⊢ ( 𝑀 ∈ ℕ₀ → 𝑀 ≤ +∞ )
7	6	ad2antrr	⊢ ( ( ( 𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀^* ) ∧ ¬ 𝑁 ∈ ℕ₀ ) → 𝑀 ≤ +∞ )
8		simpll	⊢ ( ( ( 𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀^* ) ∧ ¬ 𝑁 ∈ ℕ₀ ) → 𝑀 ∈ ℕ₀ )
9		peano2rem	⊢ ( 𝑀 ∈ ℝ → ( 𝑀 − 1 ) ∈ ℝ )
10		ltpnf	⊢ ( ( 𝑀 − 1 ) ∈ ℝ → ( 𝑀 − 1 ) < +∞ )
11	8 3 9 10	4syl	⊢ ( ( ( 𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀^* ) ∧ ¬ 𝑁 ∈ ℕ₀ ) → ( 𝑀 − 1 ) < +∞ )
12	7 11	2thd	⊢ ( ( ( 𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀^* ) ∧ ¬ 𝑁 ∈ ℕ₀ ) → ( 𝑀 ≤ +∞ ↔ ( 𝑀 − 1 ) < +∞ ) )
13		xnn0nnn0pnf	⊢ ( ( 𝑁 ∈ ℕ₀^* ∧ ¬ 𝑁 ∈ ℕ₀ ) → 𝑁 = +∞ )
14	13	adantll	⊢ ( ( ( 𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀^* ) ∧ ¬ 𝑁 ∈ ℕ₀ ) → 𝑁 = +∞ )
15	14	breq2d	⊢ ( ( ( 𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀^* ) ∧ ¬ 𝑁 ∈ ℕ₀ ) → ( 𝑀 ≤ 𝑁 ↔ 𝑀 ≤ +∞ ) )
16	14	breq2d	⊢ ( ( ( 𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀^* ) ∧ ¬ 𝑁 ∈ ℕ₀ ) → ( ( 𝑀 − 1 ) < 𝑁 ↔ ( 𝑀 − 1 ) < +∞ ) )
17	12 15 16	3bitr4d	⊢ ( ( ( 𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀^* ) ∧ ¬ 𝑁 ∈ ℕ₀ ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝑀 − 1 ) < 𝑁 ) )
18	2 17	pm2.61dan	⊢ ( ( 𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀^* ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝑀 − 1 ) < 𝑁 ) )