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

Metamath Proof Explorer

Theorem declei

Description: Comparing a digit to a decimal integer. (Contributed by AV, 17-Aug-2021)

Ref Expression
Hypotheses declei.1 ⊢ 𝐴 ∈ ℕ
declei.2 ⊢ 𝐵 ∈ ℕ0
declei.3 ⊢ 𝐶 ∈ ℕ0
declei.4 ⊢ 𝐶 ≤ 9
Assertion declei 𝐶 ≤ 𝐴 𝐵

Proof

Step Hyp Ref Expression
1 declei.1 ⊢ 𝐴 ∈ ℕ
2 declei.2 ⊢ 𝐵 ∈ ℕ0
3 declei.3 ⊢ 𝐶 ∈ ℕ0
4 declei.4 ⊢ 𝐶 ≤ 9
5 3 dec0h ⊢ 𝐶 = 0 𝐶
6 0nn0 ⊢ 0 ∈ ℕ0
7 1 nnnn0i ⊢ 𝐴 ∈ ℕ0
8 1 nngt0i ⊢ 0 < 𝐴
9 6 7 3 2 4 8 decleh ⊢ 0 𝐶 ≤ 𝐴 𝐵
10 5 9 eqbrtri ⊢ 𝐶 ≤ 𝐴 𝐵