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

Theorem numltc 9380
Description: Comparing two decimal integers (unequal higher places). (Contributed by Mario Carneiro, 18-Feb-2014.)
Hypotheses
Ref Expression
numlt.1 ๐‘‡ โˆˆ โ„•
numlt.2 ๐ด โˆˆ โ„•0
numlt.3 ๐ต โˆˆ โ„•0
numltc.3 ๐ถ โˆˆ โ„•0
numltc.4 ๐ท โˆˆ โ„•0
numltc.5 ๐ถ < ๐‘‡
numltc.6 ๐ด < ๐ต
Assertion
Ref Expression
numltc ((๐‘‡ ยท ๐ด) + ๐ถ) < ((๐‘‡ ยท ๐ต) + ๐ท)

Proof of Theorem numltc
StepHypRef Expression
1 numlt.1 . . . . 5 ๐‘‡ โˆˆ โ„•
2 numlt.2 . . . . 5 ๐ด โˆˆ โ„•0
3 numltc.3 . . . . 5 ๐ถ โˆˆ โ„•0
4 numltc.5 . . . . 5 ๐ถ < ๐‘‡
51, 2, 3, 1, 4numlt 9379 . . . 4 ((๐‘‡ ยท ๐ด) + ๐ถ) < ((๐‘‡ ยท ๐ด) + ๐‘‡)
61nnrei 8899 . . . . . . 7 ๐‘‡ โˆˆ โ„
76recni 7944 . . . . . 6 ๐‘‡ โˆˆ โ„‚
82nn0rei 9158 . . . . . . 7 ๐ด โˆˆ โ„
98recni 7944 . . . . . 6 ๐ด โˆˆ โ„‚
10 ax-1cn 7879 . . . . . 6 1 โˆˆ โ„‚
117, 9, 10adddii 7942 . . . . 5 (๐‘‡ ยท (๐ด + 1)) = ((๐‘‡ ยท ๐ด) + (๐‘‡ ยท 1))
127mulid1i 7934 . . . . . 6 (๐‘‡ ยท 1) = ๐‘‡
1312oveq2i 5876 . . . . 5 ((๐‘‡ ยท ๐ด) + (๐‘‡ ยท 1)) = ((๐‘‡ ยท ๐ด) + ๐‘‡)
1411, 13eqtri 2196 . . . 4 (๐‘‡ ยท (๐ด + 1)) = ((๐‘‡ ยท ๐ด) + ๐‘‡)
155, 14breqtrri 4025 . . 3 ((๐‘‡ ยท ๐ด) + ๐ถ) < (๐‘‡ ยท (๐ด + 1))
16 numltc.6 . . . . 5 ๐ด < ๐ต
17 numlt.3 . . . . . 6 ๐ต โˆˆ โ„•0
18 nn0ltp1le 9286 . . . . . 6 ((๐ด โˆˆ โ„•0 โˆง ๐ต โˆˆ โ„•0) โ†’ (๐ด < ๐ต โ†” (๐ด + 1) โ‰ค ๐ต))
192, 17, 18mp2an 426 . . . . 5 (๐ด < ๐ต โ†” (๐ด + 1) โ‰ค ๐ต)
2016, 19mpbi 145 . . . 4 (๐ด + 1) โ‰ค ๐ต
211nngt0i 8920 . . . . 5 0 < ๐‘‡
22 peano2re 8067 . . . . . . 7 (๐ด โˆˆ โ„ โ†’ (๐ด + 1) โˆˆ โ„)
238, 22ax-mp 5 . . . . . 6 (๐ด + 1) โˆˆ โ„
2417nn0rei 9158 . . . . . 6 ๐ต โˆˆ โ„
2523, 24, 6lemul2i 8853 . . . . 5 (0 < ๐‘‡ โ†’ ((๐ด + 1) โ‰ค ๐ต โ†” (๐‘‡ ยท (๐ด + 1)) โ‰ค (๐‘‡ ยท ๐ต)))
2621, 25ax-mp 5 . . . 4 ((๐ด + 1) โ‰ค ๐ต โ†” (๐‘‡ ยท (๐ด + 1)) โ‰ค (๐‘‡ ยท ๐ต))
2720, 26mpbi 145 . . 3 (๐‘‡ ยท (๐ด + 1)) โ‰ค (๐‘‡ ยท ๐ต)
286, 8remulcli 7946 . . . . 5 (๐‘‡ ยท ๐ด) โˆˆ โ„
293nn0rei 9158 . . . . 5 ๐ถ โˆˆ โ„
3028, 29readdcli 7945 . . . 4 ((๐‘‡ ยท ๐ด) + ๐ถ) โˆˆ โ„
316, 23remulcli 7946 . . . 4 (๐‘‡ ยท (๐ด + 1)) โˆˆ โ„
326, 24remulcli 7946 . . . 4 (๐‘‡ ยท ๐ต) โˆˆ โ„
3330, 31, 32ltletri 8038 . . 3 ((((๐‘‡ ยท ๐ด) + ๐ถ) < (๐‘‡ ยท (๐ด + 1)) โˆง (๐‘‡ ยท (๐ด + 1)) โ‰ค (๐‘‡ ยท ๐ต)) โ†’ ((๐‘‡ ยท ๐ด) + ๐ถ) < (๐‘‡ ยท ๐ต))
3415, 27, 33mp2an 426 . 2 ((๐‘‡ ยท ๐ด) + ๐ถ) < (๐‘‡ ยท ๐ต)
35 numltc.4 . . 3 ๐ท โˆˆ โ„•0
3632, 35nn0addge1i 9195 . 2 (๐‘‡ ยท ๐ต) โ‰ค ((๐‘‡ ยท ๐ต) + ๐ท)
3735nn0rei 9158 . . . 4 ๐ท โˆˆ โ„
3832, 37readdcli 7945 . . 3 ((๐‘‡ ยท ๐ต) + ๐ท) โˆˆ โ„
3930, 32, 38ltletri 8038 . 2 ((((๐‘‡ ยท ๐ด) + ๐ถ) < (๐‘‡ ยท ๐ต) โˆง (๐‘‡ ยท ๐ต) โ‰ค ((๐‘‡ ยท ๐ต) + ๐ท)) โ†’ ((๐‘‡ ยท ๐ด) + ๐ถ) < ((๐‘‡ ยท ๐ต) + ๐ท))
4034, 36, 39mp2an 426 1 ((๐‘‡ ยท ๐ด) + ๐ถ) < ((๐‘‡ ยท ๐ต) + ๐ท)
Colors of variables: wff set class
Syntax hints:   โ†” wb 105   โˆˆ wcel 2146   class class class wbr 3998  (class class class)co 5865  โ„cr 7785  0cc0 7786  1c1 7787   + caddc 7789   ยท cmul 7791   < clt 7966   โ‰ค cle 7967  โ„•cn 8890  โ„•0cn0 9147
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-13 2148  ax-14 2149  ax-ext 2157  ax-sep 4116  ax-pow 4169  ax-pr 4203  ax-un 4427  ax-setind 4530  ax-cnex 7877  ax-resscn 7878  ax-1cn 7879  ax-1re 7880  ax-icn 7881  ax-addcl 7882  ax-addrcl 7883  ax-mulcl 7884  ax-mulrcl 7885  ax-addcom 7886  ax-mulcom 7887  ax-addass 7888  ax-mulass 7889  ax-distr 7890  ax-i2m1 7891  ax-0lt1 7892  ax-1rid 7893  ax-0id 7894  ax-rnegex 7895  ax-precex 7896  ax-cnre 7897  ax-pre-ltirr 7898  ax-pre-ltwlin 7899  ax-pre-lttrn 7900  ax-pre-ltadd 7902  ax-pre-mulgt0 7903
This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1459  df-sb 1761  df-eu 2027  df-mo 2028  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ne 2346  df-nel 2441  df-ral 2458  df-rex 2459  df-reu 2460  df-rab 2462  df-v 2737  df-sbc 2961  df-dif 3129  df-un 3131  df-in 3133  df-ss 3140  df-pw 3574  df-sn 3595  df-pr 3596  df-op 3598  df-uni 3806  df-int 3841  df-br 3999  df-opab 4060  df-id 4287  df-xp 4626  df-rel 4627  df-cnv 4628  df-co 4629  df-dm 4630  df-iota 5170  df-fun 5210  df-fv 5216  df-riota 5821  df-ov 5868  df-oprab 5869  df-mpo 5870  df-pnf 7968  df-mnf 7969  df-xr 7970  df-ltxr 7971  df-le 7972  df-sub 8104  df-neg 8105  df-inn 8891  df-n0 9148  df-z 9225
This theorem is referenced by:  decltc  9383  numlti  9391
  Copyright terms: Public domain W3C validator