Step | Hyp | Ref
| Expression |
1 | | dpmul1000.a |
. . . . . 6
โข ๐ด โ
โ0 |
2 | | dpmul1000.b |
. . . . . . . 8
โข ๐ต โ
โ0 |
3 | 2 | nn0rei 12431 |
. . . . . . 7
โข ๐ต โ โ |
4 | | dpmul1000.c |
. . . . . . . . 9
โข ๐ถ โ
โ0 |
5 | 4 | nn0rei 12431 |
. . . . . . . 8
โข ๐ถ โ โ |
6 | | dpmul1000.d |
. . . . . . . 8
โข ๐ท โ โ |
7 | | dp2cl 31778 |
. . . . . . . 8
โข ((๐ถ โ โ โง ๐ท โ โ) โ _๐ถ๐ท โ โ) |
8 | 5, 6, 7 | mp2an 691 |
. . . . . . 7
โข _๐ถ๐ท โ โ |
9 | | dp2cl 31778 |
. . . . . . 7
โข ((๐ต โ โ โง _๐ถ๐ท โ โ) โ _๐ต_๐ถ๐ท โ โ) |
10 | 3, 8, 9 | mp2an 691 |
. . . . . 6
โข _๐ต_๐ถ๐ท โ โ |
11 | | dpcl 31789 |
. . . . . 6
โข ((๐ด โ โ0
โง _๐ต_๐ถ๐ท โ โ) โ (๐ด._๐ต_๐ถ๐ท) โ โ) |
12 | 1, 10, 11 | mp2an 691 |
. . . . 5
โข (๐ด._๐ต_๐ถ๐ท) โ โ |
13 | 12 | recni 11176 |
. . . 4
โข (๐ด._๐ต_๐ถ๐ท) โ โ |
14 | | 10nn0 12643 |
. . . . . 6
โข ;10 โ
โ0 |
15 | | 0nn0 12435 |
. . . . . 6
โข 0 โ
โ0 |
16 | 14, 15 | deccl 12640 |
. . . . 5
โข ;;100 โ โ0 |
17 | 16 | nn0cni 12432 |
. . . 4
โข ;;100 โ โ |
18 | 14 | nn0cni 12432 |
. . . 4
โข ;10 โ โ |
19 | 13, 17, 18 | mulassi 11173 |
. . 3
โข (((๐ด._๐ต_๐ถ๐ท) ยท ;;100)
ยท ;10) = ((๐ด._๐ต_๐ถ๐ท) ยท (;;100
ยท ;10)) |
20 | 1, 2, 8 | dpmul100 31795 |
. . . 4
โข ((๐ด._๐ต_๐ถ๐ท) ยท ;;100) =
;;๐ด๐ต_๐ถ๐ท |
21 | 20 | oveq1i 7372 |
. . 3
โข (((๐ด._๐ต_๐ถ๐ท) ยท ;;100)
ยท ;10) = (;;๐ด๐ต_๐ถ๐ท ยท ;10) |
22 | 16 | dec0u 12646 |
. . . . 5
โข (;10 ยท ;;100) =
;;;1000 |
23 | 18, 17, 22 | mulcomli 11171 |
. . . 4
โข (;;100 ยท ;10) = ;;;1000 |
24 | 23 | oveq2i 7373 |
. . 3
โข ((๐ด._๐ต_๐ถ๐ท) ยท (;;100
ยท ;10)) = ((๐ด._๐ต_๐ถ๐ท) ยท ;;;1000) |
25 | 19, 21, 24 | 3eqtr3i 2773 |
. 2
โข (;;๐ด๐ต_๐ถ๐ท ยท ;10) = ((๐ด._๐ต_๐ถ๐ท) ยท ;;;1000) |
26 | | dfdec10 12628 |
. . . 4
โข ;;๐ด๐ต_๐ถ๐ท = ((;10 ยท ;๐ด๐ต) + _๐ถ๐ท) |
27 | 26 | oveq1i 7372 |
. . 3
โข (;;๐ด๐ต_๐ถ๐ท ยท ;10) = (((;10 ยท ;๐ด๐ต) + _๐ถ๐ท) ยท ;10) |
28 | 1, 2 | deccl 12640 |
. . . . . 6
โข ;๐ด๐ต โ โ0 |
29 | 28 | nn0cni 12432 |
. . . . 5
โข ;๐ด๐ต โ โ |
30 | 18, 29 | mulcli 11169 |
. . . 4
โข (;10 ยท ;๐ด๐ต) โ โ |
31 | 8 | recni 11176 |
. . . 4
โข _๐ถ๐ท โ โ |
32 | 30, 31, 18 | adddiri 11175 |
. . 3
โข (((;10 ยท ;๐ด๐ต) + _๐ถ๐ท) ยท ;10) = (((;10 ยท ;๐ด๐ต) ยท ;10) + (_๐ถ๐ท ยท ;10)) |
33 | 28, 4, 6 | dfdec100 31768 |
. . . 4
โข ;;;๐ด๐ต๐ถ๐ท = ((;;100
ยท ;๐ด๐ต) + ;๐ถ๐ท) |
34 | 14 | dec0u 12646 |
. . . . . . 7
โข (;10 ยท ;10) = ;;100 |
35 | 34 | oveq1i 7372 |
. . . . . 6
โข ((;10 ยท ;10) ยท ;๐ด๐ต) = (;;100
ยท ;๐ด๐ต) |
36 | 18, 18, 29 | mul32i 11358 |
. . . . . 6
โข ((;10 ยท ;10) ยท ;๐ด๐ต) = ((;10 ยท ;๐ด๐ต) ยท ;10) |
37 | 35, 36 | eqtr3i 2767 |
. . . . 5
โข (;;100 ยท ;๐ด๐ต) = ((;10 ยท ;๐ด๐ต) ยท ;10) |
38 | 4, 6 | dpmul10 31793 |
. . . . . 6
โข ((๐ถ.๐ท) ยท ;10) = ;๐ถ๐ท |
39 | | dpval 31788 |
. . . . . . . 8
โข ((๐ถ โ โ0
โง ๐ท โ โ)
โ (๐ถ.๐ท) = _๐ถ๐ท) |
40 | 4, 6, 39 | mp2an 691 |
. . . . . . 7
โข (๐ถ.๐ท) = _๐ถ๐ท |
41 | 40 | oveq1i 7372 |
. . . . . 6
โข ((๐ถ.๐ท) ยท ;10) = (_๐ถ๐ท ยท ;10) |
42 | 38, 41 | eqtr3i 2767 |
. . . . 5
โข ;๐ถ๐ท = (_๐ถ๐ท ยท ;10) |
43 | 37, 42 | oveq12i 7374 |
. . . 4
โข ((;;100 ยท ;๐ด๐ต) + ;๐ถ๐ท) = (((;10 ยท ;๐ด๐ต) ยท ;10) + (_๐ถ๐ท ยท ;10)) |
44 | 33, 43 | eqtr2i 2766 |
. . 3
โข (((;10 ยท ;๐ด๐ต) ยท ;10) + (_๐ถ๐ท ยท ;10)) = ;;;๐ด๐ต๐ถ๐ท |
45 | 27, 32, 44 | 3eqtri 2769 |
. 2
โข (;;๐ด๐ต_๐ถ๐ท ยท ;10) = ;;;๐ด๐ต๐ถ๐ท |
46 | 25, 45 | eqtr3i 2767 |
1
โข ((๐ด._๐ต_๐ถ๐ท) ยท ;;;1000) = ;;;๐ด๐ต๐ถ๐ท |