Step | Hyp | Ref
| Expression |
1 | | numma.6 |
. . . 4
โข ๐ = ((๐ ยท ๐ด) + ๐ต) |
2 | 1 | oveq1i 7368 |
. . 3
โข (๐ ยท ๐) = (((๐ ยท ๐ด) + ๐ต) ยท ๐) |
3 | | numma.7 |
. . 3
โข ๐ = ((๐ ยท ๐ถ) + ๐ท) |
4 | 2, 3 | oveq12i 7370 |
. 2
โข ((๐ ยท ๐) + ๐) = ((((๐ ยท ๐ด) + ๐ต) ยท ๐) + ((๐ ยท ๐ถ) + ๐ท)) |
5 | | numma.1 |
. . . . . . 7
โข ๐ โ
โ0 |
6 | 5 | nn0cni 12426 |
. . . . . 6
โข ๐ โ โ |
7 | | numma.2 |
. . . . . . . 8
โข ๐ด โ
โ0 |
8 | 7 | nn0cni 12426 |
. . . . . . 7
โข ๐ด โ โ |
9 | | numma.8 |
. . . . . . . 8
โข ๐ โ
โ0 |
10 | 9 | nn0cni 12426 |
. . . . . . 7
โข ๐ โ โ |
11 | 8, 10 | mulcli 11163 |
. . . . . 6
โข (๐ด ยท ๐) โ โ |
12 | | numma.4 |
. . . . . . 7
โข ๐ถ โ
โ0 |
13 | 12 | nn0cni 12426 |
. . . . . 6
โข ๐ถ โ โ |
14 | 6, 11, 13 | adddii 11168 |
. . . . 5
โข (๐ ยท ((๐ด ยท ๐) + ๐ถ)) = ((๐ ยท (๐ด ยท ๐)) + (๐ ยท ๐ถ)) |
15 | 6, 8, 10 | mulassi 11167 |
. . . . . 6
โข ((๐ ยท ๐ด) ยท ๐) = (๐ ยท (๐ด ยท ๐)) |
16 | 15 | oveq1i 7368 |
. . . . 5
โข (((๐ ยท ๐ด) ยท ๐) + (๐ ยท ๐ถ)) = ((๐ ยท (๐ด ยท ๐)) + (๐ ยท ๐ถ)) |
17 | 14, 16 | eqtr4i 2768 |
. . . 4
โข (๐ ยท ((๐ด ยท ๐) + ๐ถ)) = (((๐ ยท ๐ด) ยท ๐) + (๐ ยท ๐ถ)) |
18 | 17 | oveq1i 7368 |
. . 3
โข ((๐ ยท ((๐ด ยท ๐) + ๐ถ)) + ((๐ต ยท ๐) + ๐ท)) = ((((๐ ยท ๐ด) ยท ๐) + (๐ ยท ๐ถ)) + ((๐ต ยท ๐) + ๐ท)) |
19 | 6, 8 | mulcli 11163 |
. . . . . 6
โข (๐ ยท ๐ด) โ โ |
20 | | numma.3 |
. . . . . . 7
โข ๐ต โ
โ0 |
21 | 20 | nn0cni 12426 |
. . . . . 6
โข ๐ต โ โ |
22 | 19, 21, 10 | adddiri 11169 |
. . . . 5
โข (((๐ ยท ๐ด) + ๐ต) ยท ๐) = (((๐ ยท ๐ด) ยท ๐) + (๐ต ยท ๐)) |
23 | 22 | oveq1i 7368 |
. . . 4
โข ((((๐ ยท ๐ด) + ๐ต) ยท ๐) + ((๐ ยท ๐ถ) + ๐ท)) = ((((๐ ยท ๐ด) ยท ๐) + (๐ต ยท ๐)) + ((๐ ยท ๐ถ) + ๐ท)) |
24 | 19, 10 | mulcli 11163 |
. . . . 5
โข ((๐ ยท ๐ด) ยท ๐) โ โ |
25 | 6, 13 | mulcli 11163 |
. . . . 5
โข (๐ ยท ๐ถ) โ โ |
26 | 21, 10 | mulcli 11163 |
. . . . 5
โข (๐ต ยท ๐) โ โ |
27 | | numma.5 |
. . . . . 6
โข ๐ท โ
โ0 |
28 | 27 | nn0cni 12426 |
. . . . 5
โข ๐ท โ โ |
29 | 24, 25, 26, 28 | add4i 11380 |
. . . 4
โข ((((๐ ยท ๐ด) ยท ๐) + (๐ ยท ๐ถ)) + ((๐ต ยท ๐) + ๐ท)) = ((((๐ ยท ๐ด) ยท ๐) + (๐ต ยท ๐)) + ((๐ ยท ๐ถ) + ๐ท)) |
30 | 23, 29 | eqtr4i 2768 |
. . 3
โข ((((๐ ยท ๐ด) + ๐ต) ยท ๐) + ((๐ ยท ๐ถ) + ๐ท)) = ((((๐ ยท ๐ด) ยท ๐) + (๐ ยท ๐ถ)) + ((๐ต ยท ๐) + ๐ท)) |
31 | 18, 30 | eqtr4i 2768 |
. 2
โข ((๐ ยท ((๐ด ยท ๐) + ๐ถ)) + ((๐ต ยท ๐) + ๐ท)) = ((((๐ ยท ๐ด) + ๐ต) ยท ๐) + ((๐ ยท ๐ถ) + ๐ท)) |
32 | | numma.9 |
. . . 4
โข ((๐ด ยท ๐) + ๐ถ) = ๐ธ |
33 | 32 | oveq2i 7369 |
. . 3
โข (๐ ยท ((๐ด ยท ๐) + ๐ถ)) = (๐ ยท ๐ธ) |
34 | | numma.10 |
. . 3
โข ((๐ต ยท ๐) + ๐ท) = ๐น |
35 | 33, 34 | oveq12i 7370 |
. 2
โข ((๐ ยท ((๐ด ยท ๐) + ๐ถ)) + ((๐ต ยท ๐) + ๐ท)) = ((๐ ยท ๐ธ) + ๐น) |
36 | 4, 31, 35 | 3eqtr2i 2771 |
1
โข ((๐ ยท ๐) + ๐) = ((๐ ยท ๐ธ) + ๐น) |