Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dpmul4 Structured version   Visualization version   GIF version

Theorem dpmul4 32655
Description: An upper bound to multiplication of decimal numbers with 4 digits. (Contributed by Thierry Arnoux, 25-Dec-2021.)
Hypotheses
Ref Expression
dpmul.a ๐ด โˆˆ โ„•0
dpmul.b ๐ต โˆˆ โ„•0
dpmul.c ๐ถ โˆˆ โ„•0
dpmul.d ๐ท โˆˆ โ„•0
dpmul.e ๐ธ โˆˆ โ„•0
dpmul.g ๐บ โˆˆ โ„•0
dpmul.j ๐ฝ โˆˆ โ„•0
dpmul.k ๐พ โˆˆ โ„•0
dpmul4.f ๐น โˆˆ โ„•0
dpmul4.h ๐ป โˆˆ โ„•0
dpmul4.i ๐ผ โˆˆ โ„•0
dpmul4.l ๐ฟ โˆˆ โ„•0
dpmul4.m ๐‘€ โˆˆ โ„•0
dpmul4.n ๐‘ โˆˆ โ„•0
dpmul4.o ๐‘‚ โˆˆ โ„•0
dpmul4.p ๐‘ƒ โˆˆ โ„•0
dpmul4.q ๐‘„ โˆˆ โ„•0
dpmul4.r ๐‘… โˆˆ โ„•0
dpmul4.s ๐‘† โˆˆ โ„•0
dpmul4.t ๐‘‡ โˆˆ โ„•0
dpmul4.u ๐‘ˆ โˆˆ โ„•0
dpmul4.w ๐‘Š โˆˆ โ„•0
dpmul4.x ๐‘‹ โˆˆ โ„•0
dpmul4.y ๐‘Œ โˆˆ โ„•0
dpmul4.z ๐‘ โˆˆ โ„•0
dpmul4.a ๐‘ˆ < 10
dpmul4.b ๐‘ƒ < 10
dpmul4.c ๐‘„ < 10
dpmul4.1 (๐ฟ๐‘€๐‘ + ๐‘‚) = ๐‘…๐‘†๐‘‡๐‘ˆ
dpmul4.2 ((๐ด.๐ต) ยท (๐ธ.๐น)) = (๐ผ.๐ฝ๐พ)
dpmul4.3 ((๐ถ.๐ท) ยท (๐บ.๐ป)) = (๐‘‚.๐‘ƒ๐‘„)
dpmul4.4 (๐ผ๐ฝ๐พ1 + ๐‘…๐‘†๐‘‡) = ๐‘Š๐‘‹๐‘Œ๐‘
dpmul4.5 (((๐ด.๐ต) + (๐ถ.๐ท)) ยท ((๐ธ.๐น) + (๐บ.๐ป))) = (((๐ผ.๐ฝ๐พ) + (๐ฟ.๐‘€๐‘)) + (๐‘‚.๐‘ƒ๐‘„))
Assertion
Ref Expression
dpmul4 ((๐ด.๐ต๐ถ๐ท) ยท (๐ธ.๐น๐บ๐ป)) < (๐‘Š.๐‘‹๐‘Œ๐‘)

Proof of Theorem dpmul4
StepHypRef Expression
1 dpmul.a . . . . . . . . 9 ๐ด โˆˆ โ„•0
2 dpmul.b . . . . . . . . 9 ๐ต โˆˆ โ„•0
31, 2deccl 12728 . . . . . . . 8 ๐ด๐ต โˆˆ โ„•0
4 dpmul.c . . . . . . . . 9 ๐ถ โˆˆ โ„•0
5 dpmul.d . . . . . . . . 9 ๐ท โˆˆ โ„•0
64, 5deccl 12728 . . . . . . . 8 ๐ถ๐ท โˆˆ โ„•0
7 dpmul.e . . . . . . . . 9 ๐ธ โˆˆ โ„•0
8 dpmul4.f . . . . . . . . 9 ๐น โˆˆ โ„•0
97, 8deccl 12728 . . . . . . . 8 ๐ธ๐น โˆˆ โ„•0
10 dpmul.g . . . . . . . . 9 ๐บ โˆˆ โ„•0
11 dpmul4.h . . . . . . . . 9 ๐ป โˆˆ โ„•0
1210, 11deccl 12728 . . . . . . . 8 ๐บ๐ป โˆˆ โ„•0
13 dpmul4.l . . . . . . . . . 10 ๐ฟ โˆˆ โ„•0
14 dpmul4.m . . . . . . . . . 10 ๐‘€ โˆˆ โ„•0
1513, 14deccl 12728 . . . . . . . . 9 ๐ฟ๐‘€ โˆˆ โ„•0
16 dpmul4.n . . . . . . . . 9 ๐‘ โˆˆ โ„•0
1715, 16deccl 12728 . . . . . . . 8 ๐ฟ๐‘€๐‘ โˆˆ โ„•0
18 2nn0 12525 . . . . . . . 8 2 โˆˆ โ„•0
192nn0rei 12519 . . . . . . . . . . . . 13 ๐ต โˆˆ โ„
20 dpcl 32632 . . . . . . . . . . . . 13 ((๐ด โˆˆ โ„•0 โˆง ๐ต โˆˆ โ„) โ†’ (๐ด.๐ต) โˆˆ โ„)
211, 19, 20mp2an 690 . . . . . . . . . . . 12 (๐ด.๐ต) โˆˆ โ„
2221recni 11264 . . . . . . . . . . 11 (๐ด.๐ต) โˆˆ โ„‚
23 10nn 12729 . . . . . . . . . . . 12 10 โˆˆ โ„•
2423nncni 12258 . . . . . . . . . . 11 10 โˆˆ โ„‚
258nn0rei 12519 . . . . . . . . . . . . 13 ๐น โˆˆ โ„
26 dpcl 32632 . . . . . . . . . . . . 13 ((๐ธ โˆˆ โ„•0 โˆง ๐น โˆˆ โ„) โ†’ (๐ธ.๐น) โˆˆ โ„)
277, 25, 26mp2an 690 . . . . . . . . . . . 12 (๐ธ.๐น) โˆˆ โ„
2827recni 11264 . . . . . . . . . . 11 (๐ธ.๐น) โˆˆ โ„‚
2922, 24, 28, 24mul4i 11447 . . . . . . . . . 10 (((๐ด.๐ต) ยท 10) ยท ((๐ธ.๐น) ยท 10)) = (((๐ด.๐ต) ยท (๐ธ.๐น)) ยท (10 ยท 10))
3022, 28mulcli 11257 . . . . . . . . . . 11 ((๐ด.๐ต) ยท (๐ธ.๐น)) โˆˆ โ„‚
3130, 24, 24mulassi 11261 . . . . . . . . . 10 ((((๐ด.๐ต) ยท (๐ธ.๐น)) ยท 10) ยท 10) = (((๐ด.๐ต) ยท (๐ธ.๐น)) ยท (10 ยท 10))
32 dpmul4.2 . . . . . . . . . . . . 13 ((๐ด.๐ต) ยท (๐ธ.๐น)) = (๐ผ.๐ฝ๐พ)
3332oveq1i 7434 . . . . . . . . . . . 12 (((๐ด.๐ต) ยท (๐ธ.๐น)) ยท 10) = ((๐ผ.๐ฝ๐พ) ยท 10)
34 dpmul4.i . . . . . . . . . . . . 13 ๐ผ โˆˆ โ„•0
35 dpmul.j . . . . . . . . . . . . 13 ๐ฝ โˆˆ โ„•0
36 dpmul.k . . . . . . . . . . . . . 14 ๐พ โˆˆ โ„•0
3736nn0rei 12519 . . . . . . . . . . . . 13 ๐พ โˆˆ โ„
3834, 35, 37dp3mul10 32639 . . . . . . . . . . . 12 ((๐ผ.๐ฝ๐พ) ยท 10) = (๐ผ๐ฝ.๐พ)
3933, 38eqtri 2755 . . . . . . . . . . 11 (((๐ด.๐ต) ยท (๐ธ.๐น)) ยท 10) = (๐ผ๐ฝ.๐พ)
4039oveq1i 7434 . . . . . . . . . 10 ((((๐ด.๐ต) ยท (๐ธ.๐น)) ยท 10) ยท 10) = ((๐ผ๐ฝ.๐พ) ยท 10)
4129, 31, 403eqtr2ri 2762 . . . . . . . . 9 ((๐ผ๐ฝ.๐พ) ยท 10) = (((๐ด.๐ต) ยท 10) ยท ((๐ธ.๐น) ยท 10))
4234, 35deccl 12728 . . . . . . . . . 10 ๐ผ๐ฝ โˆˆ โ„•0
4342, 37dpmul10 32636 . . . . . . . . 9 ((๐ผ๐ฝ.๐พ) ยท 10) = ๐ผ๐ฝ๐พ
441, 19dpmul10 32636 . . . . . . . . . 10 ((๐ด.๐ต) ยท 10) = ๐ด๐ต
457, 25dpmul10 32636 . . . . . . . . . 10 ((๐ธ.๐น) ยท 10) = ๐ธ๐น
4644, 45oveq12i 7436 . . . . . . . . 9 (((๐ด.๐ต) ยท 10) ยท ((๐ธ.๐น) ยท 10)) = (๐ด๐ต ยท ๐ธ๐น)
4741, 43, 463eqtr3ri 2764 . . . . . . . 8 (๐ด๐ต ยท ๐ธ๐น) = ๐ผ๐ฝ๐พ
485nn0rei 12519 . . . . . . . . . . . . 13 ๐ท โˆˆ โ„
49 dpcl 32632 . . . . . . . . . . . . 13 ((๐ถ โˆˆ โ„•0 โˆง ๐ท โˆˆ โ„) โ†’ (๐ถ.๐ท) โˆˆ โ„)
504, 48, 49mp2an 690 . . . . . . . . . . . 12 (๐ถ.๐ท) โˆˆ โ„
5150recni 11264 . . . . . . . . . . 11 (๐ถ.๐ท) โˆˆ โ„‚
5211nn0rei 12519 . . . . . . . . . . . . 13 ๐ป โˆˆ โ„
53 dpcl 32632 . . . . . . . . . . . . 13 ((๐บ โˆˆ โ„•0 โˆง ๐ป โˆˆ โ„) โ†’ (๐บ.๐ป) โˆˆ โ„)
5410, 52, 53mp2an 690 . . . . . . . . . . . 12 (๐บ.๐ป) โˆˆ โ„
5554recni 11264 . . . . . . . . . . 11 (๐บ.๐ป) โˆˆ โ„‚
5651, 24, 55, 24mul4i 11447 . . . . . . . . . 10 (((๐ถ.๐ท) ยท 10) ยท ((๐บ.๐ป) ยท 10)) = (((๐ถ.๐ท) ยท (๐บ.๐ป)) ยท (10 ยท 10))
5751, 55mulcli 11257 . . . . . . . . . . 11 ((๐ถ.๐ท) ยท (๐บ.๐ป)) โˆˆ โ„‚
5857, 24, 24mulassi 11261 . . . . . . . . . 10 ((((๐ถ.๐ท) ยท (๐บ.๐ป)) ยท 10) ยท 10) = (((๐ถ.๐ท) ยท (๐บ.๐ป)) ยท (10 ยท 10))
59 dpmul4.3 . . . . . . . . . . . . 13 ((๐ถ.๐ท) ยท (๐บ.๐ป)) = (๐‘‚.๐‘ƒ๐‘„)
6059oveq1i 7434 . . . . . . . . . . . 12 (((๐ถ.๐ท) ยท (๐บ.๐ป)) ยท 10) = ((๐‘‚.๐‘ƒ๐‘„) ยท 10)
61 dpmul4.o . . . . . . . . . . . . 13 ๐‘‚ โˆˆ โ„•0
62 dpmul4.p . . . . . . . . . . . . 13 ๐‘ƒ โˆˆ โ„•0
63 dpmul4.q . . . . . . . . . . . . . 14 ๐‘„ โˆˆ โ„•0
6463nn0rei 12519 . . . . . . . . . . . . 13 ๐‘„ โˆˆ โ„
6561, 62, 64dp3mul10 32639 . . . . . . . . . . . 12 ((๐‘‚.๐‘ƒ๐‘„) ยท 10) = (๐‘‚๐‘ƒ.๐‘„)
6660, 65eqtri 2755 . . . . . . . . . . 11 (((๐ถ.๐ท) ยท (๐บ.๐ป)) ยท 10) = (๐‘‚๐‘ƒ.๐‘„)
6766oveq1i 7434 . . . . . . . . . 10 ((((๐ถ.๐ท) ยท (๐บ.๐ป)) ยท 10) ยท 10) = ((๐‘‚๐‘ƒ.๐‘„) ยท 10)
6856, 58, 673eqtr2ri 2762 . . . . . . . . 9 ((๐‘‚๐‘ƒ.๐‘„) ยท 10) = (((๐ถ.๐ท) ยท 10) ยท ((๐บ.๐ป) ยท 10))
6961, 62deccl 12728 . . . . . . . . . 10 ๐‘‚๐‘ƒ โˆˆ โ„•0
7069, 64dpmul10 32636 . . . . . . . . 9 ((๐‘‚๐‘ƒ.๐‘„) ยท 10) = ๐‘‚๐‘ƒ๐‘„
714, 48dpmul10 32636 . . . . . . . . . 10 ((๐ถ.๐ท) ยท 10) = ๐ถ๐ท
7210, 52dpmul10 32636 . . . . . . . . . 10 ((๐บ.๐ป) ยท 10) = ๐บ๐ป
7371, 72oveq12i 7436 . . . . . . . . 9 (((๐ถ.๐ท) ยท 10) ยท ((๐บ.๐ป) ยท 10)) = (๐ถ๐ท ยท ๐บ๐ป)
7468, 70, 733eqtr3ri 2764 . . . . . . . 8 (๐ถ๐ท ยท ๐บ๐ป) = ๐‘‚๐‘ƒ๐‘„
7522, 51, 24adddiri 11263 . . . . . . . . . . . 12 (((๐ด.๐ต) + (๐ถ.๐ท)) ยท 10) = (((๐ด.๐ต) ยท 10) + ((๐ถ.๐ท) ยท 10))
7644, 71oveq12i 7436 . . . . . . . . . . . 12 (((๐ด.๐ต) ยท 10) + ((๐ถ.๐ท) ยท 10)) = (๐ด๐ต + ๐ถ๐ท)
7775, 76eqtr2i 2756 . . . . . . . . . . 11 (๐ด๐ต + ๐ถ๐ท) = (((๐ด.๐ต) + (๐ถ.๐ท)) ยท 10)
7828, 55, 24adddiri 11263 . . . . . . . . . . . 12 (((๐ธ.๐น) + (๐บ.๐ป)) ยท 10) = (((๐ธ.๐น) ยท 10) + ((๐บ.๐ป) ยท 10))
7945, 72oveq12i 7436 . . . . . . . . . . . 12 (((๐ธ.๐น) ยท 10) + ((๐บ.๐ป) ยท 10)) = (๐ธ๐น + ๐บ๐ป)
8078, 79eqtr2i 2756 . . . . . . . . . . 11 (๐ธ๐น + ๐บ๐ป) = (((๐ธ.๐น) + (๐บ.๐ป)) ยท 10)
8177, 80oveq12i 7436 . . . . . . . . . 10 ((๐ด๐ต + ๐ถ๐ท) ยท (๐ธ๐น + ๐บ๐ป)) = ((((๐ด.๐ต) + (๐ถ.๐ท)) ยท 10) ยท (((๐ธ.๐น) + (๐บ.๐ป)) ยท 10))
8222, 51addcli 11256 . . . . . . . . . . 11 ((๐ด.๐ต) + (๐ถ.๐ท)) โˆˆ โ„‚
8328, 55addcli 11256 . . . . . . . . . . 11 ((๐ธ.๐น) + (๐บ.๐ป)) โˆˆ โ„‚
8482, 24, 83, 24mul4i 11447 . . . . . . . . . 10 ((((๐ด.๐ต) + (๐ถ.๐ท)) ยท 10) ยท (((๐ธ.๐น) + (๐บ.๐ป)) ยท 10)) = ((((๐ด.๐ต) + (๐ถ.๐ท)) ยท ((๐ธ.๐น) + (๐บ.๐ป))) ยท (10 ยท 10))
85 dpmul4.5 . . . . . . . . . . 11 (((๐ด.๐ต) + (๐ถ.๐ท)) ยท ((๐ธ.๐น) + (๐บ.๐ป))) = (((๐ผ.๐ฝ๐พ) + (๐ฟ.๐‘€๐‘)) + (๐‘‚.๐‘ƒ๐‘„))
8685oveq1i 7434 . . . . . . . . . 10 ((((๐ด.๐ต) + (๐ถ.๐ท)) ยท ((๐ธ.๐น) + (๐บ.๐ป))) ยท (10 ยท 10)) = ((((๐ผ.๐ฝ๐พ) + (๐ฟ.๐‘€๐‘)) + (๐‘‚.๐‘ƒ๐‘„)) ยท (10 ยท 10))
8781, 84, 863eqtri 2759 . . . . . . . . 9 ((๐ด๐ต + ๐ถ๐ท) ยท (๐ธ๐น + ๐บ๐ป)) = ((((๐ผ.๐ฝ๐พ) + (๐ฟ.๐‘€๐‘)) + (๐‘‚.๐‘ƒ๐‘„)) ยท (10 ยท 10))
88 10nn0 12731 . . . . . . . . . . 11 10 โˆˆ โ„•0
8988dec0u 12734 . . . . . . . . . 10 (10 ยท 10) = 100
9089oveq2i 7435 . . . . . . . . 9 ((((๐ผ.๐ฝ๐พ) + (๐ฟ.๐‘€๐‘)) + (๐‘‚.๐‘ƒ๐‘„)) ยท (10 ยท 10)) = ((((๐ผ.๐ฝ๐พ) + (๐ฟ.๐‘€๐‘)) + (๐‘‚.๐‘ƒ๐‘„)) ยท 100)
9132, 30eqeltrri 2825 . . . . . . . . . . . 12 (๐ผ.๐ฝ๐พ) โˆˆ โ„‚
9214nn0rei 12519 . . . . . . . . . . . . . . 15 ๐‘€ โˆˆ โ„
9316nn0rei 12519 . . . . . . . . . . . . . . 15 ๐‘ โˆˆ โ„
94 dp2cl 32621 . . . . . . . . . . . . . . 15 ((๐‘€ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ ๐‘€๐‘ โˆˆ โ„)
9592, 93, 94mp2an 690 . . . . . . . . . . . . . 14 ๐‘€๐‘ โˆˆ โ„
96 dpcl 32632 . . . . . . . . . . . . . 14 ((๐ฟ โˆˆ โ„•0 โˆง ๐‘€๐‘ โˆˆ โ„) โ†’ (๐ฟ.๐‘€๐‘) โˆˆ โ„)
9713, 95, 96mp2an 690 . . . . . . . . . . . . 13 (๐ฟ.๐‘€๐‘) โˆˆ โ„
9897recni 11264 . . . . . . . . . . . 12 (๐ฟ.๐‘€๐‘) โˆˆ โ„‚
9991, 98addcli 11256 . . . . . . . . . . 11 ((๐ผ.๐ฝ๐พ) + (๐ฟ.๐‘€๐‘)) โˆˆ โ„‚
10059, 57eqeltrri 2825 . . . . . . . . . . 11 (๐‘‚.๐‘ƒ๐‘„) โˆˆ โ„‚
101 0nn0 12523 . . . . . . . . . . . . 13 0 โˆˆ โ„•0
10288, 101deccl 12728 . . . . . . . . . . . 12 100 โˆˆ โ„•0
103102nn0cni 12520 . . . . . . . . . . 11 100 โˆˆ โ„‚
10499, 100, 103adddiri 11263 . . . . . . . . . 10 ((((๐ผ.๐ฝ๐พ) + (๐ฟ.๐‘€๐‘)) + (๐‘‚.๐‘ƒ๐‘„)) ยท 100) = ((((๐ผ.๐ฝ๐พ) + (๐ฟ.๐‘€๐‘)) ยท 100) + ((๐‘‚.๐‘ƒ๐‘„) ยท 100))
10591, 98, 103adddiri 11263 . . . . . . . . . . 11 (((๐ผ.๐ฝ๐พ) + (๐ฟ.๐‘€๐‘)) ยท 100) = (((๐ผ.๐ฝ๐พ) ยท 100) + ((๐ฟ.๐‘€๐‘) ยท 100))
106105oveq1i 7434 . . . . . . . . . 10 ((((๐ผ.๐ฝ๐พ) + (๐ฟ.๐‘€๐‘)) ยท 100) + ((๐‘‚.๐‘ƒ๐‘„) ยท 100)) = ((((๐ผ.๐ฝ๐พ) ยท 100) + ((๐ฟ.๐‘€๐‘) ยท 100)) + ((๐‘‚.๐‘ƒ๐‘„) ยท 100))
10734, 35, 37dpmul100 32638 . . . . . . . . . . . 12 ((๐ผ.๐ฝ๐พ) ยท 100) = ๐ผ๐ฝ๐พ
10813, 14, 93dpmul100 32638 . . . . . . . . . . . 12 ((๐ฟ.๐‘€๐‘) ยท 100) = ๐ฟ๐‘€๐‘
109107, 108oveq12i 7436 . . . . . . . . . . 11 (((๐ผ.๐ฝ๐พ) ยท 100) + ((๐ฟ.๐‘€๐‘) ยท 100)) = (๐ผ๐ฝ๐พ + ๐ฟ๐‘€๐‘)
11061, 62, 64dpmul100 32638 . . . . . . . . . . 11 ((๐‘‚.๐‘ƒ๐‘„) ยท 100) = ๐‘‚๐‘ƒ๐‘„
111109, 110oveq12i 7436 . . . . . . . . . 10 ((((๐ผ.๐ฝ๐พ) ยท 100) + ((๐ฟ.๐‘€๐‘) ยท 100)) + ((๐‘‚.๐‘ƒ๐‘„) ยท 100)) = ((๐ผ๐ฝ๐พ + ๐ฟ๐‘€๐‘) + ๐‘‚๐‘ƒ๐‘„)
112104, 106, 1113eqtri 2759 . . . . . . . . 9 ((((๐ผ.๐ฝ๐พ) + (๐ฟ.๐‘€๐‘)) + (๐‘‚.๐‘ƒ๐‘„)) ยท 100) = ((๐ผ๐ฝ๐พ + ๐ฟ๐‘€๐‘) + ๐‘‚๐‘ƒ๐‘„)
11387, 90, 1123eqtri 2759 . . . . . . . 8 ((๐ด๐ต + ๐ถ๐ท) ยท (๐ธ๐น + ๐บ๐ป)) = ((๐ผ๐ฝ๐พ + ๐ฟ๐‘€๐‘) + ๐‘‚๐‘ƒ๐‘„)
114 sq10 14261 . . . . . . . . . . . 12 (10โ†‘2) = 100
115114oveq2i 7435 . . . . . . . . . . 11 (๐ด๐ต ยท (10โ†‘2)) = (๐ด๐ต ยท 100)
1163nn0cni 12520 . . . . . . . . . . . 12 ๐ด๐ต โˆˆ โ„‚
117103, 116mulcomi 11258 . . . . . . . . . . 11 (100 ยท ๐ด๐ต) = (๐ด๐ต ยท 100)
118115, 117eqtr4i 2758 . . . . . . . . . 10 (๐ด๐ต ยท (10โ†‘2)) = (100 ยท ๐ด๐ต)
119118oveq1i 7434 . . . . . . . . 9 ((๐ด๐ต ยท (10โ†‘2)) + ๐ถ๐ท) = ((100 ยท ๐ด๐ต) + ๐ถ๐ท)
1203, 4, 48dfdec100 32611 . . . . . . . . 9 ๐ด๐ต๐ถ๐ท = ((100 ยท ๐ด๐ต) + ๐ถ๐ท)
121119, 120eqtr4i 2758 . . . . . . . 8 ((๐ด๐ต ยท (10โ†‘2)) + ๐ถ๐ท) = ๐ด๐ต๐ถ๐ท
122114oveq2i 7435 . . . . . . . . . . 11 (๐ธ๐น ยท (10โ†‘2)) = (๐ธ๐น ยท 100)
1239nn0cni 12520 . . . . . . . . . . . 12 ๐ธ๐น โˆˆ โ„‚
124103, 123mulcomi 11258 . . . . . . . . . . 11 (100 ยท ๐ธ๐น) = (๐ธ๐น ยท 100)
125122, 124eqtr4i 2758 . . . . . . . . . 10 (๐ธ๐น ยท (10โ†‘2)) = (100 ยท ๐ธ๐น)
126125oveq1i 7434 . . . . . . . . 9 ((๐ธ๐น ยท (10โ†‘2)) + ๐บ๐ป) = ((100 ยท ๐ธ๐น) + ๐บ๐ป)
1279, 10, 52dfdec100 32611 . . . . . . . . 9 ๐ธ๐น๐บ๐ป = ((100 ยท ๐ธ๐น) + ๐บ๐ป)
128126, 127eqtr4i 2758 . . . . . . . 8 ((๐ธ๐น ยท (10โ†‘2)) + ๐บ๐ป) = ๐ธ๐น๐บ๐ป
12924sqvali 14181 . . . . . . . . . . . 12 (10โ†‘2) = (10 ยท 10)
130129oveq2i 7435 . . . . . . . . . . 11 (๐ผ๐ฝ๐พ ยท (10โ†‘2)) = (๐ผ๐ฝ๐พ ยท (10 ยท 10))
13142, 36deccl 12728 . . . . . . . . . . . . 13 ๐ผ๐ฝ๐พ โˆˆ โ„•0
132131nn0cni 12520 . . . . . . . . . . . 12 ๐ผ๐ฝ๐พ โˆˆ โ„‚
133132, 24, 24mulassi 11261 . . . . . . . . . . 11 ((๐ผ๐ฝ๐พ ยท 10) ยท 10) = (๐ผ๐ฝ๐พ ยท (10 ยท 10))
134130, 133eqtr4i 2758 . . . . . . . . . 10 (๐ผ๐ฝ๐พ ยท (10โ†‘2)) = ((๐ผ๐ฝ๐พ ยท 10) ยท 10)
135 dpmul4.r . . . . . . . . . . . . . . . 16 ๐‘… โˆˆ โ„•0
136 dpmul4.s . . . . . . . . . . . . . . . 16 ๐‘† โˆˆ โ„•0
137135, 136deccl 12728 . . . . . . . . . . . . . . 15 ๐‘…๐‘† โˆˆ โ„•0
138 dpmul4.t . . . . . . . . . . . . . . 15 ๐‘‡ โˆˆ โ„•0
139137, 138deccl 12728 . . . . . . . . . . . . . 14 ๐‘…๐‘†๐‘‡ โˆˆ โ„•0
140139nn0cni 12520 . . . . . . . . . . . . 13 ๐‘…๐‘†๐‘‡ โˆˆ โ„‚
141 ax-1cn 11202 . . . . . . . . . . . . 13 1 โˆˆ โ„‚
142140, 141addcli 11256 . . . . . . . . . . . 12 (๐‘…๐‘†๐‘‡ + 1) โˆˆ โ„‚
143132, 24mulcli 11257 . . . . . . . . . . . 12 (๐ผ๐ฝ๐พ ยท 10) โˆˆ โ„‚
144141, 143addcomi 11441 . . . . . . . . . . . . . . . 16 (1 + (๐ผ๐ฝ๐พ ยท 10)) = ((๐ผ๐ฝ๐พ ยท 10) + 1)
14524, 132mulcomi 11258 . . . . . . . . . . . . . . . . . 18 (10 ยท ๐ผ๐ฝ๐พ) = (๐ผ๐ฝ๐พ ยท 10)
146131dec0u 12734 . . . . . . . . . . . . . . . . . 18 (10 ยท ๐ผ๐ฝ๐พ) = ๐ผ๐ฝ๐พ0
147145, 146eqtr3i 2757 . . . . . . . . . . . . . . . . 17 (๐ผ๐ฝ๐พ ยท 10) = ๐ผ๐ฝ๐พ0
148147oveq1i 7434 . . . . . . . . . . . . . . . 16 ((๐ผ๐ฝ๐พ ยท 10) + 1) = (๐ผ๐ฝ๐พ0 + 1)
149141addlidi 11438 . . . . . . . . . . . . . . . . 17 (0 + 1) = 1
150 eqid 2727 . . . . . . . . . . . . . . . . 17 ๐ผ๐ฝ๐พ0 = ๐ผ๐ฝ๐พ0
151131, 101, 149, 150decsuc 12744 . . . . . . . . . . . . . . . 16 (๐ผ๐ฝ๐พ0 + 1) = ๐ผ๐ฝ๐พ1
152144, 148, 1513eqtri 2759 . . . . . . . . . . . . . . 15 (1 + (๐ผ๐ฝ๐พ ยท 10)) = ๐ผ๐ฝ๐พ1
153152oveq2i 7435 . . . . . . . . . . . . . 14 (๐‘…๐‘†๐‘‡ + (1 + (๐ผ๐ฝ๐พ ยท 10))) = (๐‘…๐‘†๐‘‡ + ๐ผ๐ฝ๐พ1)
154140, 141, 143addassi 11260 . . . . . . . . . . . . . 14 ((๐‘…๐‘†๐‘‡ + 1) + (๐ผ๐ฝ๐พ ยท 10)) = (๐‘…๐‘†๐‘‡ + (1 + (๐ผ๐ฝ๐พ ยท 10)))
155 1nn0 12524 . . . . . . . . . . . . . . . . 17 1 โˆˆ โ„•0
156131, 155deccl 12728 . . . . . . . . . . . . . . . 16 ๐ผ๐ฝ๐พ1 โˆˆ โ„•0
157156nn0cni 12520 . . . . . . . . . . . . . . 15 ๐ผ๐ฝ๐พ1 โˆˆ โ„‚
158157, 140addcomi 11441 . . . . . . . . . . . . . 14 (๐ผ๐ฝ๐พ1 + ๐‘…๐‘†๐‘‡) = (๐‘…๐‘†๐‘‡ + ๐ผ๐ฝ๐พ1)
159153, 154, 1583eqtr4i 2765 . . . . . . . . . . . . 13 ((๐‘…๐‘†๐‘‡ + 1) + (๐ผ๐ฝ๐พ ยท 10)) = (๐ผ๐ฝ๐พ1 + ๐‘…๐‘†๐‘‡)
160 dpmul4.4 . . . . . . . . . . . . 13 (๐ผ๐ฝ๐พ1 + ๐‘…๐‘†๐‘‡) = ๐‘Š๐‘‹๐‘Œ๐‘
161159, 160eqtri 2755 . . . . . . . . . . . 12 ((๐‘…๐‘†๐‘‡ + 1) + (๐ผ๐ฝ๐พ ยท 10)) = ๐‘Š๐‘‹๐‘Œ๐‘
162142, 143, 161mvlladdi 11514 . . . . . . . . . . 11 (๐ผ๐ฝ๐พ ยท 10) = (๐‘Š๐‘‹๐‘Œ๐‘ โˆ’ (๐‘…๐‘†๐‘‡ + 1))
163162oveq1i 7434 . . . . . . . . . 10 ((๐ผ๐ฝ๐พ ยท 10) ยท 10) = ((๐‘Š๐‘‹๐‘Œ๐‘ โˆ’ (๐‘…๐‘†๐‘‡ + 1)) ยท 10)
164134, 163eqtri 2755 . . . . . . . . 9 (๐ผ๐ฝ๐พ ยท (10โ†‘2)) = ((๐‘Š๐‘‹๐‘Œ๐‘ โˆ’ (๐‘…๐‘†๐‘‡ + 1)) ยท 10)
165164oveq1i 7434 . . . . . . . 8 ((๐ผ๐ฝ๐พ ยท (10โ†‘2)) + ๐ฟ๐‘€๐‘) = (((๐‘Š๐‘‹๐‘Œ๐‘ โˆ’ (๐‘…๐‘†๐‘‡ + 1)) ยท 10) + ๐ฟ๐‘€๐‘)
166 eqid 2727 . . . . . . . 8 (((((๐‘Š๐‘‹๐‘Œ๐‘ โˆ’ (๐‘…๐‘†๐‘‡ + 1)) ยท 10) + ๐ฟ๐‘€๐‘) ยท (10โ†‘2)) + ๐‘‚๐‘ƒ๐‘„) = (((((๐‘Š๐‘‹๐‘Œ๐‘ โˆ’ (๐‘…๐‘†๐‘‡ + 1)) ยท 10) + ๐ฟ๐‘€๐‘) ยท (10โ†‘2)) + ๐‘‚๐‘ƒ๐‘„)
1673, 6, 9, 12, 17, 18, 47, 74, 113, 121, 128, 165, 166karatsuba 17058 . . . . . . 7 (๐ด๐ต๐ถ๐ท ยท ๐ธ๐น๐บ๐ป) = (((((๐‘Š๐‘‹๐‘Œ๐‘ โˆ’ (๐‘…๐‘†๐‘‡ + 1)) ยท 10) + ๐ฟ๐‘€๐‘) ยท (10โ†‘2)) + ๐‘‚๐‘ƒ๐‘„)
168 dpmul4.w . . . . . . . . . . . . . . 15 ๐‘Š โˆˆ โ„•0
169 dpmul4.x . . . . . . . . . . . . . . 15 ๐‘‹ โˆˆ โ„•0
170168, 169deccl 12728 . . . . . . . . . . . . . 14 ๐‘Š๐‘‹ โˆˆ โ„•0
171 dpmul4.y . . . . . . . . . . . . . 14 ๐‘Œ โˆˆ โ„•0
172170, 171deccl 12728 . . . . . . . . . . . . 13 ๐‘Š๐‘‹๐‘Œ โˆˆ โ„•0
173 dpmul4.z . . . . . . . . . . . . 13 ๐‘ โˆˆ โ„•0
174172, 173deccl 12728 . . . . . . . . . . . 12 ๐‘Š๐‘‹๐‘Œ๐‘ โˆˆ โ„•0
175174nn0cni 12520 . . . . . . . . . . 11 ๐‘Š๐‘‹๐‘Œ๐‘ โˆˆ โ„‚
176102, 101deccl 12728 . . . . . . . . . . . 12 1000 โˆˆ โ„•0
177176nn0cni 12520 . . . . . . . . . . 11 1000 โˆˆ โ„‚
178175, 177mulcli 11257 . . . . . . . . . 10 (๐‘Š๐‘‹๐‘Œ๐‘ ยท 1000) โˆˆ โ„‚
179142, 177mulcli 11257 . . . . . . . . . 10 ((๐‘…๐‘†๐‘‡ + 1) ยท 1000) โˆˆ โ„‚
180178, 179subcli 11572 . . . . . . . . 9 ((๐‘Š๐‘‹๐‘Œ๐‘ ยท 1000) โˆ’ ((๐‘…๐‘†๐‘‡ + 1) ยท 1000)) โˆˆ โ„‚
18117nn0cni 12520 . . . . . . . . . 10 ๐ฟ๐‘€๐‘ โˆˆ โ„‚
182103, 181mulcli 11257 . . . . . . . . 9 (100 ยท ๐ฟ๐‘€๐‘) โˆˆ โ„‚
18361, 62, 64dfdec100 32611 . . . . . . . . . 10 ๐‘‚๐‘ƒ๐‘„ = ((100 ยท ๐‘‚) + ๐‘ƒ๐‘„)
18469, 63deccl 12728 . . . . . . . . . . 11 ๐‘‚๐‘ƒ๐‘„ โˆˆ โ„•0
185184nn0cni 12520 . . . . . . . . . 10 ๐‘‚๐‘ƒ๐‘„ โˆˆ โ„‚
186183, 185eqeltrri 2825 . . . . . . . . 9 ((100 ยท ๐‘‚) + ๐‘ƒ๐‘„) โˆˆ โ„‚
187180, 182, 186addassi 11260 . . . . . . . 8 ((((๐‘Š๐‘‹๐‘Œ๐‘ ยท 1000) โˆ’ ((๐‘…๐‘†๐‘‡ + 1) ยท 1000)) + (100 ยท ๐ฟ๐‘€๐‘)) + ((100 ยท ๐‘‚) + ๐‘ƒ๐‘„)) = (((๐‘Š๐‘‹๐‘Œ๐‘ ยท 1000) โˆ’ ((๐‘…๐‘†๐‘‡ + 1) ยท 1000)) + ((100 ยท ๐ฟ๐‘€๐‘) + ((100 ยท ๐‘‚) + ๐‘ƒ๐‘„)))
18824sqcli 14182 . . . . . . . . . . . . 13 (10โ†‘2) โˆˆ โ„‚
189132, 188mulcli 11257 . . . . . . . . . . . 12 (๐ผ๐ฝ๐พ ยท (10โ†‘2)) โˆˆ โ„‚
190164, 189eqeltrri 2825 . . . . . . . . . . 11 ((๐‘Š๐‘‹๐‘Œ๐‘ โˆ’ (๐‘…๐‘†๐‘‡ + 1)) ยท 10) โˆˆ โ„‚
191190, 181, 103adddiri 11263 . . . . . . . . . 10 ((((๐‘Š๐‘‹๐‘Œ๐‘ โˆ’ (๐‘…๐‘†๐‘‡ + 1)) ยท 10) + ๐ฟ๐‘€๐‘) ยท 100) = ((((๐‘Š๐‘‹๐‘Œ๐‘ โˆ’ (๐‘…๐‘†๐‘‡ + 1)) ยท 10) ยท 100) + (๐ฟ๐‘€๐‘ ยท 100))
192114oveq2i 7435 . . . . . . . . . 10 ((((๐‘Š๐‘‹๐‘Œ๐‘ โˆ’ (๐‘…๐‘†๐‘‡ + 1)) ยท 10) + ๐ฟ๐‘€๐‘) ยท (10โ†‘2)) = ((((๐‘Š๐‘‹๐‘Œ๐‘ โˆ’ (๐‘…๐‘†๐‘‡ + 1)) ยท 10) + ๐ฟ๐‘€๐‘) ยท 100)
193175, 142subcli 11572 . . . . . . . . . . . . 13 (๐‘Š๐‘‹๐‘Œ๐‘ โˆ’ (๐‘…๐‘†๐‘‡ + 1)) โˆˆ โ„‚
194193, 24, 103mulassi 11261 . . . . . . . . . . . 12 (((๐‘Š๐‘‹๐‘Œ๐‘ โˆ’ (๐‘…๐‘†๐‘‡ + 1)) ยท 10) ยท 100) = ((๐‘Š๐‘‹๐‘Œ๐‘ โˆ’ (๐‘…๐‘†๐‘‡ + 1)) ยท (10 ยท 100))
195102dec0u 12734 . . . . . . . . . . . . 13 (10 ยท 100) = 1000
196195oveq2i 7435 . . . . . . . . . . . 12 ((๐‘Š๐‘‹๐‘Œ๐‘ โˆ’ (๐‘…๐‘†๐‘‡ + 1)) ยท (10 ยท 100)) = ((๐‘Š๐‘‹๐‘Œ๐‘ โˆ’ (๐‘…๐‘†๐‘‡ + 1)) ยท 1000)
197175, 142, 177subdiri 11700 . . . . . . . . . . . 12 ((๐‘Š๐‘‹๐‘Œ๐‘ โˆ’ (๐‘…๐‘†๐‘‡ + 1)) ยท 1000) = ((๐‘Š๐‘‹๐‘Œ๐‘ ยท 1000) โˆ’ ((๐‘…๐‘†๐‘‡ + 1) ยท 1000))
198194, 196, 1973eqtrri 2760 . . . . . . . . . . 11 ((๐‘Š๐‘‹๐‘Œ๐‘ ยท 1000) โˆ’ ((๐‘…๐‘†๐‘‡ + 1) ยท 1000)) = (((๐‘Š๐‘‹๐‘Œ๐‘ โˆ’ (๐‘…๐‘†๐‘‡ + 1)) ยท 10) ยท 100)
199103, 181mulcomi 11258 . . . . . . . . . . 11 (100 ยท ๐ฟ๐‘€๐‘) = (๐ฟ๐‘€๐‘ ยท 100)
200198, 199oveq12i 7436 . . . . . . . . . 10 (((๐‘Š๐‘‹๐‘Œ๐‘ ยท 1000) โˆ’ ((๐‘…๐‘†๐‘‡ + 1) ยท 1000)) + (100 ยท ๐ฟ๐‘€๐‘)) = ((((๐‘Š๐‘‹๐‘Œ๐‘ โˆ’ (๐‘…๐‘†๐‘‡ + 1)) ยท 10) ยท 100) + (๐ฟ๐‘€๐‘ ยท 100))
201191, 192, 2003eqtr4i 2765 . . . . . . . . 9 ((((๐‘Š๐‘‹๐‘Œ๐‘ โˆ’ (๐‘…๐‘†๐‘‡ + 1)) ยท 10) + ๐ฟ๐‘€๐‘) ยท (10โ†‘2)) = (((๐‘Š๐‘‹๐‘Œ๐‘ ยท 1000) โˆ’ ((๐‘…๐‘†๐‘‡ + 1) ยท 1000)) + (100 ยท ๐ฟ๐‘€๐‘))
202201, 183oveq12i 7436 . . . . . . . 8 (((((๐‘Š๐‘‹๐‘Œ๐‘ โˆ’ (๐‘…๐‘†๐‘‡ + 1)) ยท 10) + ๐ฟ๐‘€๐‘) ยท (10โ†‘2)) + ๐‘‚๐‘ƒ๐‘„) = ((((๐‘Š๐‘‹๐‘Œ๐‘ ยท 1000) โˆ’ ((๐‘…๐‘†๐‘‡ + 1) ยท 1000)) + (100 ยท ๐ฟ๐‘€๐‘)) + ((100 ยท ๐‘‚) + ๐‘ƒ๐‘„))
203182, 186addcli 11256 . . . . . . . . 9 ((100 ยท ๐ฟ๐‘€๐‘) + ((100 ยท ๐‘‚) + ๐‘ƒ๐‘„)) โˆˆ โ„‚
204 subsub 11526 . . . . . . . . 9 (((๐‘Š๐‘‹๐‘Œ๐‘ ยท 1000) โˆˆ โ„‚ โˆง ((๐‘…๐‘†๐‘‡ + 1) ยท 1000) โˆˆ โ„‚ โˆง ((100 ยท ๐ฟ๐‘€๐‘) + ((100 ยท ๐‘‚) + ๐‘ƒ๐‘„)) โˆˆ โ„‚) โ†’ ((๐‘Š๐‘‹๐‘Œ๐‘ ยท 1000) โˆ’ (((๐‘…๐‘†๐‘‡ + 1) ยท 1000) โˆ’ ((100 ยท ๐ฟ๐‘€๐‘) + ((100 ยท ๐‘‚) + ๐‘ƒ๐‘„)))) = (((๐‘Š๐‘‹๐‘Œ๐‘ ยท 1000) โˆ’ ((๐‘…๐‘†๐‘‡ + 1) ยท 1000)) + ((100 ยท ๐ฟ๐‘€๐‘) + ((100 ยท ๐‘‚) + ๐‘ƒ๐‘„))))
205178, 179, 203, 204mp3an 1457 . . . . . . . 8 ((๐‘Š๐‘‹๐‘Œ๐‘ ยท 1000) โˆ’ (((๐‘…๐‘†๐‘‡ + 1) ยท 1000) โˆ’ ((100 ยท ๐ฟ๐‘€๐‘) + ((100 ยท ๐‘‚) + ๐‘ƒ๐‘„)))) = (((๐‘Š๐‘‹๐‘Œ๐‘ ยท 1000) โˆ’ ((๐‘…๐‘†๐‘‡ + 1) ยท 1000)) + ((100 ยท ๐ฟ๐‘€๐‘) + ((100 ยท ๐‘‚) + ๐‘ƒ๐‘„)))
206187, 202, 2053eqtr4ri 2766 . . . . . . 7 ((๐‘Š๐‘‹๐‘Œ๐‘ ยท 1000) โˆ’ (((๐‘…๐‘†๐‘‡ + 1) ยท 1000) โˆ’ ((100 ยท ๐ฟ๐‘€๐‘) + ((100 ยท ๐‘‚) + ๐‘ƒ๐‘„)))) = (((((๐‘Š๐‘‹๐‘Œ๐‘ โˆ’ (๐‘…๐‘†๐‘‡ + 1)) ยท 10) + ๐ฟ๐‘€๐‘) ยท (10โ†‘2)) + ๐‘‚๐‘ƒ๐‘„)
207167, 206eqtr4i 2758 . . . . . 6 (๐ด๐ต๐ถ๐ท ยท ๐ธ๐น๐บ๐ป) = ((๐‘Š๐‘‹๐‘Œ๐‘ ยท 1000) โˆ’ (((๐‘…๐‘†๐‘‡ + 1) ยท 1000) โˆ’ ((100 ยท ๐ฟ๐‘€๐‘) + ((100 ยท ๐‘‚) + ๐‘ƒ๐‘„))))
208174nn0rei 12519 . . . . . . . 8 ๐‘Š๐‘‹๐‘Œ๐‘ โˆˆ โ„
209176nn0rei 12519 . . . . . . . 8 1000 โˆˆ โ„
210208, 209remulcli 11266 . . . . . . 7 (๐‘Š๐‘‹๐‘Œ๐‘ ยท 1000) โˆˆ โ„
211139nn0rei 12519 . . . . . . . . . . 11 ๐‘…๐‘†๐‘‡ โˆˆ โ„
212 1re 11250 . . . . . . . . . . 11 1 โˆˆ โ„
213211, 212readdcli 11265 . . . . . . . . . 10 (๐‘…๐‘†๐‘‡ + 1) โˆˆ โ„
214213, 209remulcli 11266 . . . . . . . . 9 ((๐‘…๐‘†๐‘‡ + 1) ยท 1000) โˆˆ โ„
215102nn0rei 12519 . . . . . . . . . . 11 100 โˆˆ โ„
21617nn0rei 12519 . . . . . . . . . . 11 ๐ฟ๐‘€๐‘ โˆˆ โ„
217215, 216remulcli 11266 . . . . . . . . . 10 (100 ยท ๐ฟ๐‘€๐‘) โˆˆ โ„
21861nn0rei 12519 . . . . . . . . . . . 12 ๐‘‚ โˆˆ โ„
219215, 218remulcli 11266 . . . . . . . . . . 11 (100 ยท ๐‘‚) โˆˆ โ„
22062, 63deccl 12728 . . . . . . . . . . . 12 ๐‘ƒ๐‘„ โˆˆ โ„•0
221220nn0rei 12519 . . . . . . . . . . 11 ๐‘ƒ๐‘„ โˆˆ โ„
222219, 221readdcli 11265 . . . . . . . . . 10 ((100 ยท ๐‘‚) + ๐‘ƒ๐‘„) โˆˆ โ„
223217, 222readdcli 11265 . . . . . . . . 9 ((100 ยท ๐ฟ๐‘€๐‘) + ((100 ยท ๐‘‚) + ๐‘ƒ๐‘„)) โˆˆ โ„
224214, 223resubcli 11558 . . . . . . . 8 (((๐‘…๐‘†๐‘‡ + 1) ยท 1000) โˆ’ ((100 ยท ๐ฟ๐‘€๐‘) + ((100 ยท ๐‘‚) + ๐‘ƒ๐‘„))) โˆˆ โ„
225219recni 11264 . . . . . . . . . . . 12 (100 ยท ๐‘‚) โˆˆ โ„‚
226221recni 11264 . . . . . . . . . . . 12 ๐‘ƒ๐‘„ โˆˆ โ„‚
227182, 225, 226addassi 11260 . . . . . . . . . . 11 (((100 ยท ๐ฟ๐‘€๐‘) + (100 ยท ๐‘‚)) + ๐‘ƒ๐‘„) = ((100 ยท ๐ฟ๐‘€๐‘) + ((100 ยท ๐‘‚) + ๐‘ƒ๐‘„))
228218recni 11264 . . . . . . . . . . . . . 14 ๐‘‚ โˆˆ โ„‚
229103, 181, 228adddii 11262 . . . . . . . . . . . . 13 (100 ยท (๐ฟ๐‘€๐‘ + ๐‘‚)) = ((100 ยท ๐ฟ๐‘€๐‘) + (100 ยท ๐‘‚))
230 dpmul4.1 . . . . . . . . . . . . . 14 (๐ฟ๐‘€๐‘ + ๐‘‚) = ๐‘…๐‘†๐‘‡๐‘ˆ
231230oveq2i 7435 . . . . . . . . . . . . 13 (100 ยท (๐ฟ๐‘€๐‘ + ๐‘‚)) = (100 ยท ๐‘…๐‘†๐‘‡๐‘ˆ)
232229, 231eqtr3i 2757 . . . . . . . . . . . 12 ((100 ยท ๐ฟ๐‘€๐‘) + (100 ยท ๐‘‚)) = (100 ยท ๐‘…๐‘†๐‘‡๐‘ˆ)
233232oveq1i 7434 . . . . . . . . . . 11 (((100 ยท ๐ฟ๐‘€๐‘) + (100 ยท ๐‘‚)) + ๐‘ƒ๐‘„) = ((100 ยท ๐‘…๐‘†๐‘‡๐‘ˆ) + ๐‘ƒ๐‘„)
234227, 233eqtr3i 2757 . . . . . . . . . 10 ((100 ยท ๐ฟ๐‘€๐‘) + ((100 ยท ๐‘‚) + ๐‘ƒ๐‘„)) = ((100 ยท ๐‘…๐‘†๐‘‡๐‘ˆ) + ๐‘ƒ๐‘„)
235 dpmul4.u . . . . . . . . . . . . 13 ๐‘ˆ โˆˆ โ„•0
236 dpmul4.a . . . . . . . . . . . . 13 ๐‘ˆ < 10
237 dpmul4.b . . . . . . . . . . . . 13 ๐‘ƒ < 10
238 dpmul4.c . . . . . . . . . . . . 13 ๐‘„ < 10
239235, 88, 62, 101, 63, 101, 236, 237, 2383decltc 12746 . . . . . . . . . . . 12 ๐‘ˆ๐‘ƒ๐‘„ < 1000
240235, 62deccl 12728 . . . . . . . . . . . . . . 15 ๐‘ˆ๐‘ƒ โˆˆ โ„•0
241240, 63deccl 12728 . . . . . . . . . . . . . 14 ๐‘ˆ๐‘ƒ๐‘„ โˆˆ โ„•0
242241nn0rei 12519 . . . . . . . . . . . . 13 ๐‘ˆ๐‘ƒ๐‘„ โˆˆ โ„
243211, 209remulcli 11266 . . . . . . . . . . . . 13 (๐‘…๐‘†๐‘‡ ยท 1000) โˆˆ โ„
244242, 209, 243ltadd2i 11381 . . . . . . . . . . . 12 (๐‘ˆ๐‘ƒ๐‘„ < 1000 โ†” ((๐‘…๐‘†๐‘‡ ยท 1000) + ๐‘ˆ๐‘ƒ๐‘„) < ((๐‘…๐‘†๐‘‡ ยท 1000) + 1000))
245239, 244mpbi 229 . . . . . . . . . . 11 ((๐‘…๐‘†๐‘‡ ยท 1000) + ๐‘ˆ๐‘ƒ๐‘„) < ((๐‘…๐‘†๐‘‡ ยท 1000) + 1000)
246140, 177mulcli 11257 . . . . . . . . . . . . 13 (๐‘…๐‘†๐‘‡ ยท 1000) โˆˆ โ„‚
247235nn0cni 12520 . . . . . . . . . . . . . 14 ๐‘ˆ โˆˆ โ„‚
248103, 247mulcli 11257 . . . . . . . . . . . . 13 (100 ยท ๐‘ˆ) โˆˆ โ„‚
249246, 248, 226addassi 11260 . . . . . . . . . . . 12 (((๐‘…๐‘†๐‘‡ ยท 1000) + (100 ยท ๐‘ˆ)) + ๐‘ƒ๐‘„) = ((๐‘…๐‘†๐‘‡ ยท 1000) + ((100 ยท ๐‘ˆ) + ๐‘ƒ๐‘„))
250 dfdec10 12716 . . . . . . . . . . . . . . 15 ๐‘…๐‘†๐‘‡๐‘ˆ = ((10 ยท ๐‘…๐‘†๐‘‡) + ๐‘ˆ)
251250oveq2i 7435 . . . . . . . . . . . . . 14 (100 ยท ๐‘…๐‘†๐‘‡๐‘ˆ) = (100 ยท ((10 ยท ๐‘…๐‘†๐‘‡) + ๐‘ˆ))
25224, 140mulcli 11257 . . . . . . . . . . . . . . 15 (10 ยท ๐‘…๐‘†๐‘‡) โˆˆ โ„‚
253103, 252, 247adddii 11262 . . . . . . . . . . . . . 14 (100 ยท ((10 ยท ๐‘…๐‘†๐‘‡) + ๐‘ˆ)) = ((100 ยท (10 ยท ๐‘…๐‘†๐‘‡)) + (100 ยท ๐‘ˆ))
254140, 177mulcomi 11258 . . . . . . . . . . . . . . . 16 (๐‘…๐‘†๐‘‡ ยท 1000) = (1000 ยท ๐‘…๐‘†๐‘‡)
25524, 103mulcomi 11258 . . . . . . . . . . . . . . . . . 18 (10 ยท 100) = (100 ยท 10)
256255, 195eqtr3i 2757 . . . . . . . . . . . . . . . . 17 (100 ยท 10) = 1000
257256oveq1i 7434 . . . . . . . . . . . . . . . 16 ((100 ยท 10) ยท ๐‘…๐‘†๐‘‡) = (1000 ยท ๐‘…๐‘†๐‘‡)
258103, 24, 140mulassi 11261 . . . . . . . . . . . . . . . 16 ((100 ยท 10) ยท ๐‘…๐‘†๐‘‡) = (100 ยท (10 ยท ๐‘…๐‘†๐‘‡))
259254, 257, 2583eqtr2ri 2762 . . . . . . . . . . . . . . 15 (100 ยท (10 ยท ๐‘…๐‘†๐‘‡)) = (๐‘…๐‘†๐‘‡ ยท 1000)
260259oveq1i 7434 . . . . . . . . . . . . . 14 ((100 ยท (10 ยท ๐‘…๐‘†๐‘‡)) + (100 ยท ๐‘ˆ)) = ((๐‘…๐‘†๐‘‡ ยท 1000) + (100 ยท ๐‘ˆ))
261251, 253, 2603eqtri 2759 . . . . . . . . . . . . 13 (100 ยท ๐‘…๐‘†๐‘‡๐‘ˆ) = ((๐‘…๐‘†๐‘‡ ยท 1000) + (100 ยท ๐‘ˆ))
262261oveq1i 7434 . . . . . . . . . . . 12 ((100 ยท ๐‘…๐‘†๐‘‡๐‘ˆ) + ๐‘ƒ๐‘„) = (((๐‘…๐‘†๐‘‡ ยท 1000) + (100 ยท ๐‘ˆ)) + ๐‘ƒ๐‘„)
263235, 62, 64dfdec100 32611 . . . . . . . . . . . . 13 ๐‘ˆ๐‘ƒ๐‘„ = ((100 ยท ๐‘ˆ) + ๐‘ƒ๐‘„)
264263oveq2i 7435 . . . . . . . . . . . 12 ((๐‘…๐‘†๐‘‡ ยท 1000) + ๐‘ˆ๐‘ƒ๐‘„) = ((๐‘…๐‘†๐‘‡ ยท 1000) + ((100 ยท ๐‘ˆ) + ๐‘ƒ๐‘„))
265249, 262, 2643eqtr4i 2765 . . . . . . . . . . 11 ((100 ยท ๐‘…๐‘†๐‘‡๐‘ˆ) + ๐‘ƒ๐‘„) = ((๐‘…๐‘†๐‘‡ ยท 1000) + ๐‘ˆ๐‘ƒ๐‘„)
266140, 141, 177adddiri 11263 . . . . . . . . . . . 12 ((๐‘…๐‘†๐‘‡ + 1) ยท 1000) = ((๐‘…๐‘†๐‘‡ ยท 1000) + (1 ยท 1000))
267177mullidi 11255 . . . . . . . . . . . . 13 (1 ยท 1000) = 1000
268267oveq2i 7435 . . . . . . . . . . . 12 ((๐‘…๐‘†๐‘‡ ยท 1000) + (1 ยท 1000)) = ((๐‘…๐‘†๐‘‡ ยท 1000) + 1000)
269266, 268eqtri 2755 . . . . . . . . . . 11 ((๐‘…๐‘†๐‘‡ + 1) ยท 1000) = ((๐‘…๐‘†๐‘‡ ยท 1000) + 1000)
270245, 265, 2693brtr4i 5180 . . . . . . . . . 10 ((100 ยท ๐‘…๐‘†๐‘‡๐‘ˆ) + ๐‘ƒ๐‘„) < ((๐‘…๐‘†๐‘‡ + 1) ยท 1000)
271234, 270eqbrtri 5171 . . . . . . . . 9 ((100 ยท ๐ฟ๐‘€๐‘) + ((100 ยท ๐‘‚) + ๐‘ƒ๐‘„)) < ((๐‘…๐‘†๐‘‡ + 1) ยท 1000)
272223, 214posdifi 11800 . . . . . . . . 9 (((100 ยท ๐ฟ๐‘€๐‘) + ((100 ยท ๐‘‚) + ๐‘ƒ๐‘„)) < ((๐‘…๐‘†๐‘‡ + 1) ยท 1000) โ†” 0 < (((๐‘…๐‘†๐‘‡ + 1) ยท 1000) โˆ’ ((100 ยท ๐ฟ๐‘€๐‘) + ((100 ยท ๐‘‚) + ๐‘ƒ๐‘„))))
273271, 272mpbi 229 . . . . . . . 8 0 < (((๐‘…๐‘†๐‘‡ + 1) ยท 1000) โˆ’ ((100 ยท ๐ฟ๐‘€๐‘) + ((100 ยท ๐‘‚) + ๐‘ƒ๐‘„)))
274 elrp 13014 . . . . . . . 8 ((((๐‘…๐‘†๐‘‡ + 1) ยท 1000) โˆ’ ((100 ยท ๐ฟ๐‘€๐‘) + ((100 ยท ๐‘‚) + ๐‘ƒ๐‘„))) โˆˆ โ„+ โ†” ((((๐‘…๐‘†๐‘‡ + 1) ยท 1000) โˆ’ ((100 ยท ๐ฟ๐‘€๐‘) + ((100 ยท ๐‘‚) + ๐‘ƒ๐‘„))) โˆˆ โ„ โˆง 0 < (((๐‘…๐‘†๐‘‡ + 1) ยท 1000) โˆ’ ((100 ยท ๐ฟ๐‘€๐‘) + ((100 ยท ๐‘‚) + ๐‘ƒ๐‘„)))))
275224, 273, 274mpbir2an 709 . . . . . . 7 (((๐‘…๐‘†๐‘‡ + 1) ยท 1000) โˆ’ ((100 ยท ๐ฟ๐‘€๐‘) + ((100 ยท ๐‘‚) + ๐‘ƒ๐‘„))) โˆˆ โ„+
276 ltsubrp 13048 . . . . . . 7 (((๐‘Š๐‘‹๐‘Œ๐‘ ยท 1000) โˆˆ โ„ โˆง (((๐‘…๐‘†๐‘‡ + 1) ยท 1000) โˆ’ ((100 ยท ๐ฟ๐‘€๐‘) + ((100 ยท ๐‘‚) + ๐‘ƒ๐‘„))) โˆˆ โ„+) โ†’ ((๐‘Š๐‘‹๐‘Œ๐‘ ยท 1000) โˆ’ (((๐‘…๐‘†๐‘‡ + 1) ยท 1000) โˆ’ ((100 ยท ๐ฟ๐‘€๐‘) + ((100 ยท ๐‘‚) + ๐‘ƒ๐‘„)))) < (๐‘Š๐‘‹๐‘Œ๐‘ ยท 1000))
277210, 275, 276mp2an 690 . . . . . 6 ((๐‘Š๐‘‹๐‘Œ๐‘ ยท 1000) โˆ’ (((๐‘…๐‘†๐‘‡ + 1) ยท 1000) โˆ’ ((100 ยท ๐ฟ๐‘€๐‘) + ((100 ยท ๐‘‚) + ๐‘ƒ๐‘„)))) < (๐‘Š๐‘‹๐‘Œ๐‘ ยท 1000)
278207, 277eqbrtri 5171 . . . . 5 (๐ด๐ต๐ถ๐ท ยท ๐ธ๐น๐บ๐ป) < (๐‘Š๐‘‹๐‘Œ๐‘ ยท 1000)
2793, 4deccl 12728 . . . . . . . . 9 ๐ด๐ต๐ถ โˆˆ โ„•0
280279, 5deccl 12728 . . . . . . . 8 ๐ด๐ต๐ถ๐ท โˆˆ โ„•0
281280nn0rei 12519 . . . . . . 7 ๐ด๐ต๐ถ๐ท โˆˆ โ„
2829, 10deccl 12728 . . . . . . . . 9 ๐ธ๐น๐บ โˆˆ โ„•0
283282, 11deccl 12728 . . . . . . . 8 ๐ธ๐น๐บ๐ป โˆˆ โ„•0
284283nn0rei 12519 . . . . . . 7 ๐ธ๐น๐บ๐ป โˆˆ โ„
285281, 284remulcli 11266 . . . . . 6 (๐ด๐ต๐ถ๐ท ยท ๐ธ๐น๐บ๐ป) โˆˆ โ„
28623decnncl2 12737 . . . . . . . . 9 100 โˆˆ โ„•
287286decnncl2 12737 . . . . . . . 8 1000 โˆˆ โ„•
288287nngt0i 12287 . . . . . . 7 0 < 1000
289209, 288pm3.2i 469 . . . . . 6 (1000 โˆˆ โ„ โˆง 0 < 1000)
290 ltdiv1 12114 . . . . . 6 (((๐ด๐ต๐ถ๐ท ยท ๐ธ๐น๐บ๐ป) โˆˆ โ„ โˆง (๐‘Š๐‘‹๐‘Œ๐‘ ยท 1000) โˆˆ โ„ โˆง (1000 โˆˆ โ„ โˆง 0 < 1000)) โ†’ ((๐ด๐ต๐ถ๐ท ยท ๐ธ๐น๐บ๐ป) < (๐‘Š๐‘‹๐‘Œ๐‘ ยท 1000) โ†” ((๐ด๐ต๐ถ๐ท ยท ๐ธ๐น๐บ๐ป) / 1000) < ((๐‘Š๐‘‹๐‘Œ๐‘ ยท 1000) / 1000)))
291285, 210, 289, 290mp3an 1457 . . . . 5 ((๐ด๐ต๐ถ๐ท ยท ๐ธ๐น๐บ๐ป) < (๐‘Š๐‘‹๐‘Œ๐‘ ยท 1000) โ†” ((๐ด๐ต๐ถ๐ท ยท ๐ธ๐น๐บ๐ป) / 1000) < ((๐‘Š๐‘‹๐‘Œ๐‘ ยท 1000) / 1000))
292278, 291mpbi 229 . . . 4 ((๐ด๐ต๐ถ๐ท ยท ๐ธ๐น๐บ๐ป) / 1000) < ((๐‘Š๐‘‹๐‘Œ๐‘ ยท 1000) / 1000)
293280nn0cni 12520 . . . . . 6 ๐ด๐ต๐ถ๐ท โˆˆ โ„‚
294283nn0cni 12520 . . . . . 6 ๐ธ๐น๐บ๐ป โˆˆ โ„‚
295209, 288gt0ne0ii 11786 . . . . . 6 1000 โ‰  0
296293, 294, 177, 295div23i 12008 . . . . 5 ((๐ด๐ต๐ถ๐ท ยท ๐ธ๐น๐บ๐ป) / 1000) = ((๐ด๐ต๐ถ๐ท / 1000) ยท ๐ธ๐น๐บ๐ป)
2971, 2, 4, 48dpmul1000 32640 . . . . . . . 8 ((๐ด.๐ต๐ถ๐ท) ยท 1000) = ๐ด๐ต๐ถ๐ท
298297oveq1i 7434 . . . . . . 7 (((๐ด.๐ต๐ถ๐ท) ยท 1000) / 1000) = (๐ด๐ต๐ถ๐ท / 1000)
2994nn0rei 12519 . . . . . . . . . . . 12 ๐ถ โˆˆ โ„
300 dp2cl 32621 . . . . . . . . . . . 12 ((๐ถ โˆˆ โ„ โˆง ๐ท โˆˆ โ„) โ†’ ๐ถ๐ท โˆˆ โ„)
301299, 48, 300mp2an 690 . . . . . . . . . . 11 ๐ถ๐ท โˆˆ โ„
302 dp2cl 32621 . . . . . . . . . . 11 ((๐ต โˆˆ โ„ โˆง ๐ถ๐ท โˆˆ โ„) โ†’ ๐ต๐ถ๐ท โˆˆ โ„)
30319, 301, 302mp2an 690 . . . . . . . . . 10 ๐ต๐ถ๐ท โˆˆ โ„
304 dpcl 32632 . . . . . . . . . 10 ((๐ด โˆˆ โ„•0 โˆง ๐ต๐ถ๐ท โˆˆ โ„) โ†’ (๐ด.๐ต๐ถ๐ท) โˆˆ โ„)
3051, 303, 304mp2an 690 . . . . . . . . 9 (๐ด.๐ต๐ถ๐ท) โˆˆ โ„
306305recni 11264 . . . . . . . 8 (๐ด.๐ต๐ถ๐ท) โˆˆ โ„‚
307306, 177, 295divcan4i 11997 . . . . . . 7 (((๐ด.๐ต๐ถ๐ท) ยท 1000) / 1000) = (๐ด.๐ต๐ถ๐ท)
308298, 307eqtr3i 2757 . . . . . 6 (๐ด๐ต๐ถ๐ท / 1000) = (๐ด.๐ต๐ถ๐ท)
309308oveq1i 7434 . . . . 5 ((๐ด๐ต๐ถ๐ท / 1000) ยท ๐ธ๐น๐บ๐ป) = ((๐ด.๐ต๐ถ๐ท) ยท ๐ธ๐น๐บ๐ป)
310296, 309eqtri 2755 . . . 4 ((๐ด๐ต๐ถ๐ท ยท ๐ธ๐น๐บ๐ป) / 1000) = ((๐ด.๐ต๐ถ๐ท) ยท ๐ธ๐น๐บ๐ป)
311175, 177, 295divcan4i 11997 . . . 4 ((๐‘Š๐‘‹๐‘Œ๐‘ ยท 1000) / 1000) = ๐‘Š๐‘‹๐‘Œ๐‘
312292, 310, 3113brtr3i 5179 . . 3 ((๐ด.๐ต๐ถ๐ท) ยท ๐ธ๐น๐บ๐ป) < ๐‘Š๐‘‹๐‘Œ๐‘
313305, 284remulcli 11266 . . . 4 ((๐ด.๐ต๐ถ๐ท) ยท ๐ธ๐น๐บ๐ป) โˆˆ โ„
314 ltdiv1 12114 . . . 4 ((((๐ด.๐ต๐ถ๐ท) ยท ๐ธ๐น๐บ๐ป) โˆˆ โ„ โˆง ๐‘Š๐‘‹๐‘Œ๐‘ โˆˆ โ„ โˆง (1000 โˆˆ โ„ โˆง 0 < 1000)) โ†’ (((๐ด.๐ต๐ถ๐ท) ยท ๐ธ๐น๐บ๐ป) < ๐‘Š๐‘‹๐‘Œ๐‘ โ†” (((๐ด.๐ต๐ถ๐ท) ยท ๐ธ๐น๐บ๐ป) / 1000) < (๐‘Š๐‘‹๐‘Œ๐‘ / 1000)))
315313, 208, 289, 314mp3an 1457 . . 3 (((๐ด.๐ต๐ถ๐ท) ยท ๐ธ๐น๐บ๐ป) < ๐‘Š๐‘‹๐‘Œ๐‘ โ†” (((๐ด.๐ต๐ถ๐ท) ยท ๐ธ๐น๐บ๐ป) / 1000) < (๐‘Š๐‘‹๐‘Œ๐‘ / 1000))
316312, 315mpbi 229 . 2 (((๐ด.๐ต๐ถ๐ท) ยท ๐ธ๐น๐บ๐ป) / 1000) < (๐‘Š๐‘‹๐‘Œ๐‘ / 1000)
317306, 294, 177, 295divassi 12006 . . 3 (((๐ด.๐ต๐ถ๐ท) ยท ๐ธ๐น๐บ๐ป) / 1000) = ((๐ด.๐ต๐ถ๐ท) ยท (๐ธ๐น๐บ๐ป / 1000))
3187, 8, 10, 52dpmul1000 32640 . . . . . 6 ((๐ธ.๐น๐บ๐ป) ยท 1000) = ๐ธ๐น๐บ๐ป
319318oveq1i 7434 . . . . 5 (((๐ธ.๐น๐บ๐ป) ยท 1000) / 1000) = (๐ธ๐น๐บ๐ป / 1000)
32010nn0rei 12519 . . . . . . . . . 10 ๐บ โˆˆ โ„
321 dp2cl 32621 . . . . . . . . . 10 ((๐บ โˆˆ โ„ โˆง ๐ป โˆˆ โ„) โ†’ ๐บ๐ป โˆˆ โ„)
322320, 52, 321mp2an 690 . . . . . . . . 9 ๐บ๐ป โˆˆ โ„
323 dp2cl 32621 . . . . . . . . 9 ((๐น โˆˆ โ„ โˆง ๐บ๐ป โˆˆ โ„) โ†’ ๐น๐บ๐ป โˆˆ โ„)
32425, 322, 323mp2an 690 . . . . . . . 8 ๐น๐บ๐ป โˆˆ โ„
325 dpcl 32632 . . . . . . . 8 ((๐ธ โˆˆ โ„•0 โˆง ๐น๐บ๐ป โˆˆ โ„) โ†’ (๐ธ.๐น๐บ๐ป) โˆˆ โ„)
3267, 324, 325mp2an 690 . . . . . . 7 (๐ธ.๐น๐บ๐ป) โˆˆ โ„
327326recni 11264 . . . . . 6 (๐ธ.๐น๐บ๐ป) โˆˆ โ„‚
328327, 177, 295divcan4i 11997 . . . . 5 (((๐ธ.๐น๐บ๐ป) ยท 1000) / 1000) = (๐ธ.๐น๐บ๐ป)
329319, 328eqtr3i 2757 . . . 4 (๐ธ๐น๐บ๐ป / 1000) = (๐ธ.๐น๐บ๐ป)
330329oveq2i 7435 . . 3 ((๐ด.๐ต๐ถ๐ท) ยท (๐ธ๐น๐บ๐ป / 1000)) = ((๐ด.๐ต๐ถ๐ท) ยท (๐ธ.๐น๐บ๐ป))
331317, 330eqtri 2755 . 2 (((๐ด.๐ต๐ถ๐ท) ยท ๐ธ๐น๐บ๐ป) / 1000) = ((๐ด.๐ต๐ถ๐ท) ยท (๐ธ.๐น๐บ๐ป))
332173nn0rei 12519 . . . . 5 ๐‘ โˆˆ โ„
333168, 169, 171, 332dpmul1000 32640 . . . 4 ((๐‘Š.๐‘‹๐‘Œ๐‘) ยท 1000) = ๐‘Š๐‘‹๐‘Œ๐‘
334333oveq1i 7434 . . 3 (((๐‘Š.๐‘‹๐‘Œ๐‘) ยท 1000) / 1000) = (๐‘Š๐‘‹๐‘Œ๐‘ / 1000)
335169nn0rei 12519 . . . . . . 7 ๐‘‹ โˆˆ โ„
336171nn0rei 12519 . . . . . . . 8 ๐‘Œ โˆˆ โ„
337 dp2cl 32621 . . . . . . . 8 ((๐‘Œ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ ๐‘Œ๐‘ โˆˆ โ„)
338336, 332, 337mp2an 690 . . . . . . 7 ๐‘Œ๐‘ โˆˆ โ„
339 dp2cl 32621 . . . . . . 7 ((๐‘‹ โˆˆ โ„ โˆง ๐‘Œ๐‘ โˆˆ โ„) โ†’ ๐‘‹๐‘Œ๐‘ โˆˆ โ„)
340335, 338, 339mp2an 690 . . . . . 6 ๐‘‹๐‘Œ๐‘ โˆˆ โ„
341 dpcl 32632 . . . . . 6 ((๐‘Š โˆˆ โ„•0 โˆง ๐‘‹๐‘Œ๐‘ โˆˆ โ„) โ†’ (๐‘Š.๐‘‹๐‘Œ๐‘) โˆˆ โ„)
342168, 340, 341mp2an 690 . . . . 5 (๐‘Š.๐‘‹๐‘Œ๐‘) โˆˆ โ„
343342recni 11264 . . . 4 (๐‘Š.๐‘‹๐‘Œ๐‘) โˆˆ โ„‚
344343, 177, 295divcan4i 11997 . . 3 (((๐‘Š.๐‘‹๐‘Œ๐‘) ยท 1000) / 1000) = (๐‘Š.๐‘‹๐‘Œ๐‘)
345334, 344eqtr3i 2757 . 2 (๐‘Š๐‘‹๐‘Œ๐‘ / 1000) = (๐‘Š.๐‘‹๐‘Œ๐‘)
346316, 331, 3453brtr3i 5179 1 ((๐ด.๐ต๐ถ๐ท) ยท (๐ธ.๐น๐บ๐ป)) < (๐‘Š.๐‘‹๐‘Œ๐‘)
Colors of variables: wff setvar class
Syntax hints:   โ†” wb 205   โˆง wa 394   = wceq 1533   โˆˆ wcel 2098   class class class wbr 5150  (class class class)co 7424  โ„‚cc 11142  โ„cr 11143  0cc0 11144  1c1 11145   + caddc 11147   ยท cmul 11149   < clt 11284   โˆ’ cmin 11480   / cdiv 11907  2c2 12303  โ„•0cn0 12508  cdc 12713  โ„+crp 13012  โ†‘cexp 14064  cdp2 32612  .cdp 32629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2698  ax-sep 5301  ax-nul 5308  ax-pow 5367  ax-pr 5431  ax-un 7744  ax-cnex 11200  ax-resscn 11201  ax-1cn 11202  ax-icn 11203  ax-addcl 11204  ax-addrcl 11205  ax-mulcl 11206  ax-mulrcl 11207  ax-mulcom 11208  ax-addass 11209  ax-mulass 11210  ax-distr 11211  ax-i2m1 11212  ax-1ne0 11213  ax-1rid 11214  ax-rnegex 11215  ax-rrecex 11216  ax-cnre 11217  ax-pre-lttri 11218  ax-pre-lttrn 11219  ax-pre-ltadd 11220  ax-pre-mulgt0 11221
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2937  df-nel 3043  df-ral 3058  df-rex 3067  df-rmo 3372  df-reu 3373  df-rab 3429  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4325  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4911  df-iun 5000  df-br 5151  df-opab 5213  df-mpt 5234  df-tr 5268  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5635  df-we 5637  df-xp 5686  df-rel 5687  df-cnv 5688  df-co 5689  df-dm 5690  df-rn 5691  df-res 5692  df-ima 5693  df-pred 6308  df-ord 6375  df-on 6376  df-lim 6377  df-suc 6378  df-iota 6503  df-fun 6553  df-fn 6554  df-f 6555  df-f1 6556  df-fo 6557  df-f1o 6558  df-fv 6559  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-om 7875  df-2nd 7998  df-frecs 8291  df-wrecs 8322  df-recs 8396  df-rdg 8435  df-er 8729  df-en 8969  df-dom 8970  df-sdom 8971  df-pnf 11286  df-mnf 11287  df-xr 11288  df-ltxr 11289  df-le 11290  df-sub 11482  df-neg 11483  df-div 11908  df-nn 12249  df-2 12311  df-3 12312  df-4 12313  df-5 12314  df-6 12315  df-7 12316  df-8 12317  df-9 12318  df-n0 12509  df-z 12595  df-dec 12714  df-uz 12859  df-rp 13013  df-seq 14005  df-exp 14065  df-dp2 32613  df-dp 32630
This theorem is referenced by:  hgt750lem2  34289
  Copyright terms: Public domain W3C validator