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

Metamath Proof Explorer

Theorem degltlem1

Description: Theorem on arithmetic of extended reals useful for degrees. (Contributed by Stefan O'Rear, 23-Mar-2015)

Ref Expression
Assertion degltlem1 ( ( 𝑋 ∈ ( ℕ0 ∪ { -∞ } ) ∧ 𝑌 ∈ ℤ ) → ( 𝑋 < 𝑌 ↔ 𝑋 ≤ ( 𝑌 − 1 ) ) )

Proof

Step Hyp Ref Expression
1 elun ⊢ ( 𝑋 ∈ ( ℕ0 ∪ { -∞ } ) ↔ ( 𝑋 ∈ ℕ0 ∨ 𝑋 ∈ { -∞ } ) )
2 nn0z ⊢ ( 𝑋 ∈ ℕ0 → 𝑋 ∈ ℤ )
3 zltlem1 ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( 𝑋 < 𝑌 ↔ 𝑋 ≤ ( 𝑌 − 1 ) ) )
4 2 3 sylan ⊢ ( ( 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) → ( 𝑋 < 𝑌 ↔ 𝑋 ≤ ( 𝑌 − 1 ) ) )
5 zre ⊢ ( 𝑌 ∈ ℤ → 𝑌 ∈ ℝ )
6 5 mnfltd ⊢ ( 𝑌 ∈ ℤ → -∞ < 𝑌 )
7 peano2zm ⊢ ( 𝑌 ∈ ℤ → ( 𝑌 − 1 ) ∈ ℤ )
8 7 zred ⊢ ( 𝑌 ∈ ℤ → ( 𝑌 − 1 ) ∈ ℝ )
9 8 rexrd ⊢ ( 𝑌 ∈ ℤ → ( 𝑌 − 1 ) ∈ ℝ* )
10 mnfle ⊢ ( ( 𝑌 − 1 ) ∈ ℝ* → -∞ ≤ ( 𝑌 − 1 ) )
11 9 10 syl ⊢ ( 𝑌 ∈ ℤ → -∞ ≤ ( 𝑌 − 1 ) )
12 6 11 2thd ⊢ ( 𝑌 ∈ ℤ → ( -∞ < 𝑌 ↔ -∞ ≤ ( 𝑌 − 1 ) ) )
13 elsni ⊢ ( 𝑋 ∈ { -∞ } → 𝑋 = -∞ )
14 breq1 ⊢ ( 𝑋 = -∞ → ( 𝑋 < 𝑌 ↔ -∞ < 𝑌 ) )
15 breq1 ⊢ ( 𝑋 = -∞ → ( 𝑋 ≤ ( 𝑌 − 1 ) ↔ -∞ ≤ ( 𝑌 − 1 ) ) )
16 14 15 bibi12d ⊢ ( 𝑋 = -∞ → ( ( 𝑋 < 𝑌 ↔ 𝑋 ≤ ( 𝑌 − 1 ) ) ↔ ( -∞ < 𝑌 ↔ -∞ ≤ ( 𝑌 − 1 ) ) ) )
17 13 16 syl ⊢ ( 𝑋 ∈ { -∞ } → ( ( 𝑋 < 𝑌 ↔ 𝑋 ≤ ( 𝑌 − 1 ) ) ↔ ( -∞ < 𝑌 ↔ -∞ ≤ ( 𝑌 − 1 ) ) ) )
18 12 17 syl5ibrcom ⊢ ( 𝑌 ∈ ℤ → ( 𝑋 ∈ { -∞ } → ( 𝑋 < 𝑌 ↔ 𝑋 ≤ ( 𝑌 − 1 ) ) ) )
19 18 impcom ⊢ ( ( 𝑋 ∈ { -∞ } ∧ 𝑌 ∈ ℤ ) → ( 𝑋 < 𝑌 ↔ 𝑋 ≤ ( 𝑌 − 1 ) ) )
20 4 19 jaoian ⊢ ( ( ( 𝑋 ∈ ℕ0 ∨ 𝑋 ∈ { -∞ } ) ∧ 𝑌 ∈ ℤ ) → ( 𝑋 < 𝑌 ↔ 𝑋 ≤ ( 𝑌 − 1 ) ) )
21 1 20 sylanb ⊢ ( ( 𝑋 ∈ ( ℕ0 ∪ { -∞ } ) ∧ 𝑌 ∈ ℤ ) → ( 𝑋 < 𝑌 ↔ 𝑋 ≤ ( 𝑌 − 1 ) ) )