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	⊢ ; 𝐴 𝐵 < ; 𝐴 𝐶