Step | Hyp | Ref
| Expression |
1 | | numma.1 |
. . . . 5
โข ๐ โ
โ0 |
2 | 1 | nn0cni 12426 |
. . . 4
โข ๐ โ โ |
3 | | numma.2 |
. . . . . . . . 9
โข ๐ด โ
โ0 |
4 | 3 | nn0cni 12426 |
. . . . . . . 8
โข ๐ด โ โ |
5 | | nummac.8 |
. . . . . . . . 9
โข ๐ โ
โ0 |
6 | 5 | nn0cni 12426 |
. . . . . . . 8
โข ๐ โ โ |
7 | 4, 6 | mulcli 11163 |
. . . . . . 7
โข (๐ด ยท ๐) โ โ |
8 | | numma.4 |
. . . . . . . 8
โข ๐ถ โ
โ0 |
9 | 8 | nn0cni 12426 |
. . . . . . 7
โข ๐ถ โ โ |
10 | | nummac.10 |
. . . . . . . 8
โข ๐บ โ
โ0 |
11 | 10 | nn0cni 12426 |
. . . . . . 7
โข ๐บ โ โ |
12 | 7, 9, 11 | addassi 11166 |
. . . . . 6
โข (((๐ด ยท ๐) + ๐ถ) + ๐บ) = ((๐ด ยท ๐) + (๐ถ + ๐บ)) |
13 | | nummac.11 |
. . . . . 6
โข ((๐ด ยท ๐) + (๐ถ + ๐บ)) = ๐ธ |
14 | 12, 13 | eqtri 2765 |
. . . . 5
โข (((๐ด ยท ๐) + ๐ถ) + ๐บ) = ๐ธ |
15 | 7, 9 | addcli 11162 |
. . . . . 6
โข ((๐ด ยท ๐) + ๐ถ) โ โ |
16 | 15, 11 | addcli 11162 |
. . . . 5
โข (((๐ด ยท ๐) + ๐ถ) + ๐บ) โ โ |
17 | 14, 16 | eqeltrri 2835 |
. . . 4
โข ๐ธ โ โ |
18 | 2, 17, 11 | subdii 11605 |
. . 3
โข (๐ ยท (๐ธ โ ๐บ)) = ((๐ ยท ๐ธ) โ (๐ ยท ๐บ)) |
19 | 18 | oveq1i 7368 |
. 2
โข ((๐ ยท (๐ธ โ ๐บ)) + ((๐ ยท ๐บ) + ๐น)) = (((๐ ยท ๐ธ) โ (๐ ยท ๐บ)) + ((๐ ยท ๐บ) + ๐น)) |
20 | | numma.3 |
. . 3
โข ๐ต โ
โ0 |
21 | | numma.5 |
. . 3
โข ๐ท โ
โ0 |
22 | | numma.6 |
. . 3
โข ๐ = ((๐ ยท ๐ด) + ๐ต) |
23 | | numma.7 |
. . 3
โข ๐ = ((๐ ยท ๐ถ) + ๐ท) |
24 | 17, 11, 15 | subadd2i 11490 |
. . . . 5
โข ((๐ธ โ ๐บ) = ((๐ด ยท ๐) + ๐ถ) โ (((๐ด ยท ๐) + ๐ถ) + ๐บ) = ๐ธ) |
25 | 14, 24 | mpbir 230 |
. . . 4
โข (๐ธ โ ๐บ) = ((๐ด ยท ๐) + ๐ถ) |
26 | 25 | eqcomi 2746 |
. . 3
โข ((๐ด ยท ๐) + ๐ถ) = (๐ธ โ ๐บ) |
27 | | nummac.12 |
. . 3
โข ((๐ต ยท ๐) + ๐ท) = ((๐ ยท ๐บ) + ๐น) |
28 | 1, 3, 20, 8, 21, 22, 23, 5, 26, 27 | numma 12663 |
. 2
โข ((๐ ยท ๐) + ๐) = ((๐ ยท (๐ธ โ ๐บ)) + ((๐ ยท ๐บ) + ๐น)) |
29 | 2, 17 | mulcli 11163 |
. . . . 5
โข (๐ ยท ๐ธ) โ โ |
30 | 2, 11 | mulcli 11163 |
. . . . 5
โข (๐ ยท ๐บ) โ โ |
31 | | npcan 11411 |
. . . . 5
โข (((๐ ยท ๐ธ) โ โ โง (๐ ยท ๐บ) โ โ) โ (((๐ ยท ๐ธ) โ (๐ ยท ๐บ)) + (๐ ยท ๐บ)) = (๐ ยท ๐ธ)) |
32 | 29, 30, 31 | mp2an 691 |
. . . 4
โข (((๐ ยท ๐ธ) โ (๐ ยท ๐บ)) + (๐ ยท ๐บ)) = (๐ ยท ๐ธ) |
33 | 32 | oveq1i 7368 |
. . 3
โข ((((๐ ยท ๐ธ) โ (๐ ยท ๐บ)) + (๐ ยท ๐บ)) + ๐น) = ((๐ ยท ๐ธ) + ๐น) |
34 | 29, 30 | subcli 11478 |
. . . 4
โข ((๐ ยท ๐ธ) โ (๐ ยท ๐บ)) โ โ |
35 | | nummac.9 |
. . . . 5
โข ๐น โ
โ0 |
36 | 35 | nn0cni 12426 |
. . . 4
โข ๐น โ โ |
37 | 34, 30, 36 | addassi 11166 |
. . 3
โข ((((๐ ยท ๐ธ) โ (๐ ยท ๐บ)) + (๐ ยท ๐บ)) + ๐น) = (((๐ ยท ๐ธ) โ (๐ ยท ๐บ)) + ((๐ ยท ๐บ) + ๐น)) |
38 | 33, 37 | eqtr3i 2767 |
. 2
โข ((๐ ยท ๐ธ) + ๐น) = (((๐ ยท ๐ธ) โ (๐ ยท ๐บ)) + ((๐ ยท ๐บ) + ๐น)) |
39 | 19, 28, 38 | 3eqtr4i 2775 |
1
โข ((๐ ยท ๐) + ๐) = ((๐ ยท ๐ธ) + ๐น) |