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

Metamath Proof Explorer

Theorem declt

Description: Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 17-Apr-2015) (Revised by AV, 6-Sep-2021)

Ref Expression
Hypotheses declt.a ⊢ 𝐴 ∈ ℕ0
declt.b ⊢ 𝐵 ∈ ℕ0
declt.c ⊢ 𝐶 ∈ ℕ
declt.l ⊢ 𝐵 < 𝐶
Assertion declt 𝐴 𝐵 < 𝐴 𝐶

Proof

Step Hyp Ref Expression
1 declt.a ⊢ 𝐴 ∈ ℕ0
2 declt.b ⊢ 𝐵 ∈ ℕ0
3 declt.c ⊢ 𝐶 ∈ ℕ
4 declt.l ⊢ 𝐵 < 𝐶
5 10nn ⊢ 1 0 ∈ ℕ
6 5 1 2 3 4 numlt ⊢ ( ( 1 0 · 𝐴 ) + 𝐵 ) < ( ( 1 0 · 𝐴 ) + 𝐶 )
7 dfdec10 ⊢ 𝐴 𝐵 = ( ( 1 0 · 𝐴 ) + 𝐵 )
8 dfdec10 ⊢ 𝐴 𝐶 = ( ( 1 0 · 𝐴 ) + 𝐶 )
9 6 7 8 3brtr4i ⊢ 𝐴 𝐵 < 𝐴 𝐶