Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  numltc Structured version   Unicode version

Theorem numltc 11004
 Description: Comparing two decimal integers (unequal higher places). (Contributed by Mario Carneiro, 18-Feb-2014.)
Hypotheses
Ref Expression
numlt.1
numlt.2
numlt.3
numltc.3
numltc.4
numltc.5
numltc.6
Assertion
Ref Expression
numltc

Proof of Theorem numltc
StepHypRef Expression
1 numlt.1 . . . . 5
2 numlt.2 . . . . 5
3 numltc.3 . . . . 5
4 numltc.5 . . . . 5
51, 2, 3, 1, 4numlt 11003 . . . 4
61nnrei 10551 . . . . . . 7
76recni 9611 . . . . . 6
82nn0rei 10812 . . . . . . 7
98recni 9611 . . . . . 6
10 ax-1cn 9553 . . . . . 6
117, 9, 10adddii 9609 . . . . 5
127mulid1i 9601 . . . . . 6
1312oveq2i 6292 . . . . 5
1411, 13eqtri 2472 . . . 4
155, 14breqtrri 4462 . . 3
16 numltc.6 . . . . 5
17 numlt.3 . . . . . 6
18 nn0ltp1le 10927 . . . . . 6
192, 17, 18mp2an 672 . . . . 5
2016, 19mpbi 208 . . . 4
211nngt0i 10575 . . . . 5
22 peano2re 9756 . . . . . . 7
238, 22ax-mp 5 . . . . . 6
2417nn0rei 10812 . . . . . 6
2523, 24, 6lemul2i 10475 . . . . 5
2621, 25ax-mp 5 . . . 4
2720, 26mpbi 208 . . 3
286, 8remulcli 9613 . . . . 5
293nn0rei 10812 . . . . 5
3028, 29readdcli 9612 . . . 4
316, 23remulcli 9613 . . . 4
326, 24remulcli 9613 . . . 4
3330, 31, 32ltletri 9715 . . 3
3415, 27, 33mp2an 672 . 2
35 numltc.4 . . 3