Metamath Proof Explorer
Description: Positive integer ordering relation. (Contributed by BTernaryTau, 24-Sep-2023)
|
|
Ref |
Expression |
|
Assertion |
nnltp1ne |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 + 1 ) < 𝐵 ↔ ( 𝐴 < 𝐵 ∧ 𝐵 ≠ ( 𝐴 + 1 ) ) ) ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
nnz |
⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ ) |
2 |
|
nnz |
⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ ) |
3 |
|
zltp1ne |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 + 1 ) < 𝐵 ↔ ( 𝐴 < 𝐵 ∧ 𝐵 ≠ ( 𝐴 + 1 ) ) ) ) |
4 |
1 2 3
|
syl2an |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 + 1 ) < 𝐵 ↔ ( 𝐴 < 𝐵 ∧ 𝐵 ≠ ( 𝐴 + 1 ) ) ) ) |