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

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 ⊢ A ∈ ℕ 0
decle.2 ⊢ B ∈ ℕ 0
decle.3 ⊢ C ∈ ℕ 0
decle.4 ⊢ B ≤ C
Assertion decle Could not format assertion : No typesetting found for |- ; A B <_ ; A C with typecode |-

Proof

Step Hyp Ref Expression
1 decle.1 ⊢ A ∈ ℕ 0
2 decle.2 ⊢ B ∈ ℕ 0
3 decle.3 ⊢ C ∈ ℕ 0
4 decle.4 ⊢ B ≤ C
5 2 nn0rei ⊢ B ∈ ℝ
6 3 nn0rei ⊢ C ∈ ℝ
7 10nn0 ⊢ 10 ∈ ℕ 0
8 7 1 nn0mulcli ⊢ 10 ⁢ A ∈ ℕ 0
9 8 nn0rei ⊢ 10 ⁢ A ∈ ℝ
10 5 6 9 leadd2i ⊢ B ≤ C ↔ 10 ⁢ A + B ≤ 10 ⁢ A + C
11 4 10 mpbi ⊢ 10 ⁢ A + B ≤ 10 ⁢ A + C
12 dfdec10 Could not format ; A B = ( ( ; 1 0 x. A ) + B ) : No typesetting found for |- ; A B = ( ( ; 1 0 x. A ) + B ) with typecode |-
13 dfdec10 Could not format ; A C = ( ( ; 1 0 x. A ) + C ) : No typesetting found for |- ; A C = ( ( ; 1 0 x. A ) + C ) with typecode |-
14 11 12 13 3brtr4i Could not format ; A B <_ ; A C : No typesetting found for |- ; A B <_ ; A C with typecode |-