Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  numltc Unicode version

Theorem numltc 8583
 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 8582 . . . 4
61nnrei 8115 . . . . . . 7
76recni 7193 . . . . . 6
82nn0rei 8366 . . . . . . 7
98recni 7193 . . . . . 6
10 ax-1cn 7131 . . . . . 6
117, 9, 10adddii 7191 . . . . 5
127mulid1i 7183 . . . . . 6
1312oveq2i 5554 . . . . 5
1411, 13eqtri 2102 . . . 4
155, 14breqtrri 3818 . . 3
16 numltc.6 . . . . 5
17 numlt.3 . . . . . 6
18 nn0ltp1le 8494 . . . . . 6
192, 17, 18mp2an 417 . . . . 5
2016, 19mpbi 143 . . . 4
211nngt0i 8136 . . . . 5
22 peano2re 7311 . . . . . . 7
238, 22ax-mp 7 . . . . . 6
2417nn0rei 8366 . . . . . 6
2523, 24, 6lemul2i 8070 . . . . 5
2621, 25ax-mp 7 . . . 4
2720, 26mpbi 143 . . 3
286, 8remulcli 7195 . . . . 5
293nn0rei 8366 . . . . 5
3028, 29readdcli 7194 . . . 4
316, 23remulcli 7195 . . . 4
326, 24remulcli 7195 . . . 4
3330, 31, 32ltletri 7284 . . 3
3415, 27, 33mp2an 417 . 2
35 numltc.4 . . 3