Theorem decltc

Description: Comparing two decimal integers (unequal higher places). (Contributed by Mario Carneiro, 18-Feb-2014) (Revised by AV, 6-Sep-2021)

	Ref	Expression
Hypotheses	declt.a	⊢ 𝐴 ∈ ℕ0
	declt.b	⊢ 𝐵 ∈ ℕ0
	decltc.c	⊢ 𝐶 ∈ ℕ0
	decltc.d	⊢ 𝐷 ∈ ℕ0
	decltc.s	⊢ 𝐶 < ; 1 0
	decltc.l	⊢ 𝐴 < 𝐵
Assertion	decltc	⊢ ; 𝐴 𝐶 < ; 𝐵 𝐷

Proof

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