Theorem declth

Description: Comparing two decimal integers (unequal higher places). (Contributed by AV, 8-Sep-2021)

	Ref	Expression
Hypotheses	declt.a	⊢ 𝐴 ∈ ℕ0
	declt.b	⊢ 𝐵 ∈ ℕ0
	declth.c	⊢ 𝐶 ∈ ℕ0
	declth.d	⊢ 𝐷 ∈ ℕ0
	declth.e	⊢ 𝐶 ≤ 9
	declth.l	⊢ 𝐴 < 𝐵
Assertion	declth	⊢ ; 𝐴 𝐶 < ; 𝐵 𝐷

Proof

Step	Hyp	Ref	Expression
1		declt.a	⊢ 𝐴 ∈ ℕ0
2		declt.b	⊢ 𝐵 ∈ ℕ0
3		declth.c	⊢ 𝐶 ∈ ℕ0
4		declth.d	⊢ 𝐷 ∈ ℕ0
5		declth.e	⊢ 𝐶 ≤ 9
6		declth.l	⊢ 𝐴 < 𝐵
7	3 5	le9lt10	⊢ 𝐶 < ; 1 0
8	1 2 3 4 7 6	decltc	⊢ ; 𝐴 𝐶 < ; 𝐵 𝐷