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

Metamath Proof Explorer

Theorem 3declth

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

Ref Expression
Hypotheses 3decltc.a ⊢ A ∈ ℕ 0
3decltc.b ⊢ B ∈ ℕ 0
3decltc.c ⊢ C ∈ ℕ 0
3decltc.d ⊢ D ∈ ℕ 0
3decltc.e ⊢ E ∈ ℕ 0
3decltc.f ⊢ F ∈ ℕ 0
3decltc.3 ⊢ A < B
3declth.1 ⊢ C ≤ 9
3declth.2 ⊢ E ≤ 9
Assertion 3declth Could not format assertion : No typesetting found for |- ; ; A C E < ; ; B D F with typecode |-

Proof

Step Hyp Ref Expression
1 3decltc.a ⊢ A ∈ ℕ 0
2 3decltc.b ⊢ B ∈ ℕ 0
3 3decltc.c ⊢ C ∈ ℕ 0
4 3decltc.d ⊢ D ∈ ℕ 0
5 3decltc.e ⊢ E ∈ ℕ 0
6 3decltc.f ⊢ F ∈ ℕ 0
7 3decltc.3 ⊢ A < B
8 3declth.1 ⊢ C ≤ 9
9 3declth.2 ⊢ E ≤ 9
10 1 3 deccl Could not format ; A C e. NN0 : No typesetting found for |- ; A C e. NN0 with typecode |-
11 2 4 deccl Could not format ; B D e. NN0 : No typesetting found for |- ; B D e. NN0 with typecode |-
12 1 2 3 4 8 7 declth Could not format ; A C < ; B D : No typesetting found for |- ; A C < ; B D with typecode |-
13 10 11 5 6 9 12 declth Could not format ; ; A C E < ; ; B D F : No typesetting found for |- ; ; A C E < ; ; B D F with typecode |-