Step | Hyp | Ref
| Expression |
1 | | dpmul.a |
. . . . 5
โข ๐ด โ
โ0 |
2 | | dpmul.b |
. . . . 5
โข ๐ต โ
โ0 |
3 | 1, 2 | deccl 12640 |
. . . 4
โข ;๐ด๐ต โ โ0 |
4 | | dpmul.c |
. . . 4
โข ๐ถ โ
โ0 |
5 | | dpmul.d |
. . . 4
โข ๐ท โ
โ0 |
6 | | eqid 2737 |
. . . 4
โข ;๐ถ๐ท = ;๐ถ๐ท |
7 | | dpmul.k |
. . . 4
โข ๐พ โ
โ0 |
8 | | dpmul.2 |
. . . . . 6
โข (๐ด ยท ๐ท) = ๐ |
9 | 1, 5 | nn0mulcli 12458 |
. . . . . 6
โข (๐ด ยท ๐ท) โ
โ0 |
10 | 8, 9 | eqeltrri 2835 |
. . . . 5
โข ๐ โ
โ0 |
11 | | dpmul.e |
. . . . 5
โข ๐ธ โ
โ0 |
12 | 10, 11 | nn0addcli 12457 |
. . . 4
โข (๐ + ๐ธ) โ
โ0 |
13 | | eqid 2737 |
. . . . . . 7
โข ;๐ด๐ต = ;๐ด๐ต |
14 | | dpmul.1 |
. . . . . . 7
โข (๐ด ยท ๐ถ) = ๐น |
15 | | dpmul.3 |
. . . . . . 7
โข (๐ต ยท ๐ถ) = ๐ฟ |
16 | 4, 1, 2, 13, 14, 15 | decmul1 12689 |
. . . . . 6
โข (;๐ด๐ต ยท ๐ถ) = ;๐น๐ฟ |
17 | 16 | oveq1i 7372 |
. . . . 5
โข ((;๐ด๐ต ยท ๐ถ) + (๐ + ๐ธ)) = (;๐น๐ฟ + (๐ + ๐ธ)) |
18 | | dfdec10 12628 |
. . . . . 6
โข ;๐น๐ฟ = ((;10 ยท ๐น) + ๐ฟ) |
19 | 18 | oveq1i 7372 |
. . . . 5
โข (;๐น๐ฟ + (๐ + ๐ธ)) = (((;10 ยท ๐น) + ๐ฟ) + (๐ + ๐ธ)) |
20 | | 10nn0 12643 |
. . . . . . . . 9
โข ;10 โ
โ0 |
21 | 20 | nn0cni 12432 |
. . . . . . . 8
โข ;10 โ โ |
22 | 1, 4 | nn0mulcli 12458 |
. . . . . . . . . 10
โข (๐ด ยท ๐ถ) โ
โ0 |
23 | 14, 22 | eqeltrri 2835 |
. . . . . . . . 9
โข ๐น โ
โ0 |
24 | 23 | nn0cni 12432 |
. . . . . . . 8
โข ๐น โ โ |
25 | 21, 24 | mulcli 11169 |
. . . . . . 7
โข (;10 ยท ๐น) โ โ |
26 | 2, 4 | nn0mulcli 12458 |
. . . . . . . . 9
โข (๐ต ยท ๐ถ) โ
โ0 |
27 | 15, 26 | eqeltrri 2835 |
. . . . . . . 8
โข ๐ฟ โ
โ0 |
28 | 27 | nn0cni 12432 |
. . . . . . 7
โข ๐ฟ โ โ |
29 | 12 | nn0cni 12432 |
. . . . . . 7
โข (๐ + ๐ธ) โ โ |
30 | 25, 28, 29 | addassi 11172 |
. . . . . 6
โข (((;10 ยท ๐น) + ๐ฟ) + (๐ + ๐ธ)) = ((;10 ยท ๐น) + (๐ฟ + (๐ + ๐ธ))) |
31 | | dpmul.5 |
. . . . . . . 8
โข ((๐ฟ + ๐) + ๐ธ) = ;๐บ๐ฝ |
32 | 10 | nn0cni 12432 |
. . . . . . . . 9
โข ๐ โ โ |
33 | 11 | nn0cni 12432 |
. . . . . . . . 9
โข ๐ธ โ โ |
34 | 28, 32, 33 | addassi 11172 |
. . . . . . . 8
โข ((๐ฟ + ๐) + ๐ธ) = (๐ฟ + (๐ + ๐ธ)) |
35 | | dfdec10 12628 |
. . . . . . . 8
โข ;๐บ๐ฝ = ((;10 ยท ๐บ) + ๐ฝ) |
36 | 31, 34, 35 | 3eqtr3ri 2774 |
. . . . . . 7
โข ((;10 ยท ๐บ) + ๐ฝ) = (๐ฟ + (๐ + ๐ธ)) |
37 | 36 | oveq2i 7373 |
. . . . . 6
โข ((;10 ยท ๐น) + ((;10 ยท ๐บ) + ๐ฝ)) = ((;10 ยท ๐น) + (๐ฟ + (๐ + ๐ธ))) |
38 | | dfdec10 12628 |
. . . . . . 7
โข ;๐ผ๐ฝ = ((;10 ยท ๐ผ) + ๐ฝ) |
39 | | dpmul.g |
. . . . . . . . . . 11
โข ๐บ โ
โ0 |
40 | 39 | nn0cni 12432 |
. . . . . . . . . 10
โข ๐บ โ โ |
41 | 21, 24, 40 | adddii 11174 |
. . . . . . . . 9
โข (;10 ยท (๐น + ๐บ)) = ((;10 ยท ๐น) + (;10 ยท ๐บ)) |
42 | | dpmul.6 |
. . . . . . . . . 10
โข (๐น + ๐บ) = ๐ผ |
43 | 42 | oveq2i 7373 |
. . . . . . . . 9
โข (;10 ยท (๐น + ๐บ)) = (;10 ยท ๐ผ) |
44 | 41, 43 | eqtr3i 2767 |
. . . . . . . 8
โข ((;10 ยท ๐น) + (;10 ยท ๐บ)) = (;10 ยท ๐ผ) |
45 | 44 | oveq1i 7372 |
. . . . . . 7
โข (((;10 ยท ๐น) + (;10 ยท ๐บ)) + ๐ฝ) = ((;10 ยท ๐ผ) + ๐ฝ) |
46 | 21, 40 | mulcli 11169 |
. . . . . . . 8
โข (;10 ยท ๐บ) โ โ |
47 | | dpmul.j |
. . . . . . . . 9
โข ๐ฝ โ
โ0 |
48 | 47 | nn0cni 12432 |
. . . . . . . 8
โข ๐ฝ โ โ |
49 | 25, 46, 48 | addassi 11172 |
. . . . . . 7
โข (((;10 ยท ๐น) + (;10 ยท ๐บ)) + ๐ฝ) = ((;10 ยท ๐น) + ((;10 ยท ๐บ) + ๐ฝ)) |
50 | 38, 45, 49 | 3eqtr2ri 2772 |
. . . . . 6
โข ((;10 ยท ๐น) + ((;10 ยท ๐บ) + ๐ฝ)) = ;๐ผ๐ฝ |
51 | 30, 37, 50 | 3eqtr2i 2771 |
. . . . 5
โข (((;10 ยท ๐น) + ๐ฟ) + (๐ + ๐ธ)) = ;๐ผ๐ฝ |
52 | 17, 19, 51 | 3eqtri 2769 |
. . . 4
โข ((;๐ด๐ต ยท ๐ถ) + (๐ + ๐ธ)) = ;๐ผ๐ฝ |
53 | 8 | oveq1i 7372 |
. . . . 5
โข ((๐ด ยท ๐ท) + ๐ธ) = (๐ + ๐ธ) |
54 | | dpmul.4 |
. . . . 5
โข (๐ต ยท ๐ท) = ;๐ธ๐พ |
55 | 5, 1, 2, 13, 7, 11, 53, 54 | decmul1c 12690 |
. . . 4
โข (;๐ด๐ต ยท ๐ท) = ;(๐ + ๐ธ)๐พ |
56 | 3, 4, 5, 6, 7, 12,
52, 55 | decmul2c 12691 |
. . 3
โข (;๐ด๐ต ยท ;๐ถ๐ท) = ;;๐ผ๐ฝ๐พ |
57 | 2 | nn0rei 12431 |
. . . . . . 7
โข ๐ต โ โ |
58 | | dpcl 31789 |
. . . . . . 7
โข ((๐ด โ โ0
โง ๐ต โ โ)
โ (๐ด.๐ต) โ โ) |
59 | 1, 57, 58 | mp2an 691 |
. . . . . 6
โข (๐ด.๐ต) โ โ |
60 | 59 | recni 11176 |
. . . . 5
โข (๐ด.๐ต) โ โ |
61 | 5 | nn0rei 12431 |
. . . . . . 7
โข ๐ท โ โ |
62 | | dpcl 31789 |
. . . . . . 7
โข ((๐ถ โ โ0
โง ๐ท โ โ)
โ (๐ถ.๐ท) โ โ) |
63 | 4, 61, 62 | mp2an 691 |
. . . . . 6
โข (๐ถ.๐ท) โ โ |
64 | 63 | recni 11176 |
. . . . 5
โข (๐ถ.๐ท) โ โ |
65 | 60, 64, 21, 21 | mul4i 11359 |
. . . 4
โข (((๐ด.๐ต) ยท (๐ถ.๐ท)) ยท (;10 ยท ;10)) = (((๐ด.๐ต) ยท ;10) ยท ((๐ถ.๐ท) ยท ;10)) |
66 | 20 | dec0u 12646 |
. . . . 5
โข (;10 ยท ;10) = ;;100 |
67 | 66 | oveq2i 7373 |
. . . 4
โข (((๐ด.๐ต) ยท (๐ถ.๐ท)) ยท (;10 ยท ;10)) = (((๐ด.๐ต) ยท (๐ถ.๐ท)) ยท ;;100) |
68 | 1, 57 | dpmul10 31793 |
. . . . 5
โข ((๐ด.๐ต) ยท ;10) = ;๐ด๐ต |
69 | 4, 61 | dpmul10 31793 |
. . . . 5
โข ((๐ถ.๐ท) ยท ;10) = ;๐ถ๐ท |
70 | 68, 69 | oveq12i 7374 |
. . . 4
โข (((๐ด.๐ต) ยท ;10) ยท ((๐ถ.๐ท) ยท ;10)) = (;๐ด๐ต ยท ;๐ถ๐ท) |
71 | 65, 67, 70 | 3eqtr3i 2773 |
. . 3
โข (((๐ด.๐ต) ยท (๐ถ.๐ท)) ยท ;;100) =
(;๐ด๐ต ยท ;๐ถ๐ท) |
72 | 23, 39 | nn0addcli 12457 |
. . . . 5
โข (๐น + ๐บ) โ
โ0 |
73 | 42, 72 | eqeltrri 2835 |
. . . 4
โข ๐ผ โ
โ0 |
74 | 7 | nn0rei 12431 |
. . . 4
โข ๐พ โ โ |
75 | 73, 47, 74 | dpmul100 31795 |
. . 3
โข ((๐ผ._๐ฝ๐พ) ยท ;;100) =
;;๐ผ๐ฝ๐พ |
76 | 56, 71, 75 | 3eqtr4i 2775 |
. 2
โข (((๐ด.๐ต) ยท (๐ถ.๐ท)) ยท ;;100) =
((๐ผ._๐ฝ๐พ) ยท ;;100) |
77 | 60, 64 | mulcli 11169 |
. . 3
โข ((๐ด.๐ต) ยท (๐ถ.๐ท)) โ โ |
78 | 47 | nn0rei 12431 |
. . . . . 6
โข ๐ฝ โ โ |
79 | | dp2cl 31778 |
. . . . . 6
โข ((๐ฝ โ โ โง ๐พ โ โ) โ _๐ฝ๐พ โ โ) |
80 | 78, 74, 79 | mp2an 691 |
. . . . 5
โข _๐ฝ๐พ โ โ |
81 | | dpcl 31789 |
. . . . 5
โข ((๐ผ โ โ0
โง _๐ฝ๐พ โ โ) โ (๐ผ._๐ฝ๐พ) โ โ) |
82 | 73, 80, 81 | mp2an 691 |
. . . 4
โข (๐ผ._๐ฝ๐พ) โ โ |
83 | 82 | recni 11176 |
. . 3
โข (๐ผ._๐ฝ๐พ) โ โ |
84 | | 10nn 12641 |
. . . . . 6
โข ;10 โ โ |
85 | 84 | decnncl2 12649 |
. . . . 5
โข ;;100 โ โ |
86 | 85 | nncni 12170 |
. . . 4
โข ;;100 โ โ |
87 | 85 | nnne0i 12200 |
. . . 4
โข ;;100 โ 0 |
88 | 86, 87 | pm3.2i 472 |
. . 3
โข (;;100 โ โ โง ;;100
โ 0) |
89 | | mulcan2 11800 |
. . 3
โข ((((๐ด.๐ต) ยท (๐ถ.๐ท)) โ โ โง (๐ผ._๐ฝ๐พ) โ โ โง (;;100
โ โ โง ;;100 โ 0)) โ ((((๐ด.๐ต) ยท (๐ถ.๐ท)) ยท ;;100) =
((๐ผ._๐ฝ๐พ) ยท ;;100)
โ ((๐ด.๐ต) ยท (๐ถ.๐ท)) = (๐ผ._๐ฝ๐พ))) |
90 | 77, 83, 88, 89 | mp3an 1462 |
. 2
โข ((((๐ด.๐ต) ยท (๐ถ.๐ท)) ยท ;;100) =
((๐ผ._๐ฝ๐พ) ยท ;;100)
โ ((๐ด.๐ต) ยท (๐ถ.๐ท)) = (๐ผ._๐ฝ๐พ)) |
91 | 76, 90 | mpbi 229 |
1
โข ((๐ด.๐ต) ยท (๐ถ.๐ท)) = (๐ผ._๐ฝ๐พ) |