Metamath Proof Explorer

Theorem decle

Description: Comparing two decimal integers (equal higher places). (Contributed by AV, 17-Aug-2021) (Revised by AV, 8-Sep-2021)

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

Proof

Step Hyp Ref Expression
1 decle.1 ⊢ 𝐴 ∈ ℕ0
2 decle.2 ⊢ 𝐵 ∈ ℕ0
3 decle.3 ⊢ 𝐶 ∈ ℕ0
4 decle.4 ⊢ 𝐵 ≤ 𝐶
5 2 nn0rei ⊢ 𝐵 ∈ ℝ
6 3 nn0rei ⊢ 𝐶 ∈ ℝ
7 10nn0 ⊢ 1 0 ∈ ℕ0
8 7 1 nn0mulcli ⊢ ( 1 0 · 𝐴 ) ∈ ℕ0
9 8 nn0rei ⊢ ( 1 0 · 𝐴 ) ∈ ℝ
10 5 6 9 leadd2i ⊢ ( 𝐵 ≤ 𝐶 ↔ ( ( 1 0 · 𝐴 ) + 𝐵 ) ≤ ( ( 1 0 · 𝐴 ) + 𝐶 ) )
11 4 10 mpbi ⊢ ( ( 1 0 · 𝐴 ) + 𝐵 ) ≤ ( ( 1 0 · 𝐴 ) + 𝐶 )
12 dfdec10 ⊢ 𝐴 𝐵 = ( ( 1 0 · 𝐴 ) + 𝐵 )
13 dfdec10 ⊢ 𝐴 𝐶 = ( ( 1 0 · 𝐴 ) + 𝐶 )
14 11 12 13 3brtr4i ⊢ 𝐴 𝐵 ≤ 𝐴 𝐶