Step | Hyp | Ref
| Expression |
1 | | cevath.sigar |
. . . 4
โข ๐บ = (๐ฅ โ โ, ๐ฆ โ โ โฆ
(โโ((โโ๐ฅ) ยท ๐ฆ))) |
2 | | cevath.a |
. . . . . . 7
โข (๐ โ (๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ)) |
3 | 2 | simp2d 1144 |
. . . . . 6
โข (๐ โ ๐ต โ โ) |
4 | | cevath.c |
. . . . . 6
โข (๐ โ ๐ โ โ) |
5 | 3, 4 | subcld 11571 |
. . . . 5
โข (๐ โ (๐ต โ ๐) โ โ) |
6 | 2 | simp3d 1145 |
. . . . . 6
โข (๐ โ ๐ถ โ โ) |
7 | 6, 4 | subcld 11571 |
. . . . 5
โข (๐ โ (๐ถ โ ๐) โ โ) |
8 | 5, 7 | jca 513 |
. . . 4
โข (๐ โ ((๐ต โ ๐) โ โ โง (๐ถ โ ๐) โ โ)) |
9 | 1, 8 | sigarimcd 45578 |
. . 3
โข (๐ โ ((๐ต โ ๐)๐บ(๐ถ โ ๐)) โ โ) |
10 | 2 | simp1d 1143 |
. . . 4
โข (๐ โ ๐ด โ โ) |
11 | | cevath.b |
. . . . 5
โข (๐ โ (๐น โ โ โง ๐ท โ โ โง ๐ธ โ โ)) |
12 | 11 | simp1d 1143 |
. . . 4
โข (๐ โ ๐น โ โ) |
13 | 10, 12 | subcld 11571 |
. . 3
โข (๐ โ (๐ด โ ๐น) โ โ) |
14 | 10, 4 | subcld 11571 |
. . . . 5
โข (๐ โ (๐ด โ ๐) โ โ) |
15 | 7, 14 | jca 513 |
. . . 4
โข (๐ โ ((๐ถ โ ๐) โ โ โง (๐ด โ ๐) โ โ)) |
16 | 1, 15 | sigarimcd 45578 |
. . 3
โข (๐ โ ((๐ถ โ ๐)๐บ(๐ด โ ๐)) โ โ) |
17 | 9, 13, 16 | 3jca 1129 |
. 2
โข (๐ โ (((๐ต โ ๐)๐บ(๐ถ โ ๐)) โ โ โง (๐ด โ ๐น) โ โ โง ((๐ถ โ ๐)๐บ(๐ด โ ๐)) โ โ)) |
18 | 12, 3 | subcld 11571 |
. . 3
โข (๐ โ (๐น โ ๐ต) โ โ) |
19 | 14, 5 | jca 513 |
. . . 4
โข (๐ โ ((๐ด โ ๐) โ โ โง (๐ต โ ๐) โ โ)) |
20 | 1, 19 | sigarimcd 45578 |
. . 3
โข (๐ โ ((๐ด โ ๐)๐บ(๐ต โ ๐)) โ โ) |
21 | 11 | simp3d 1145 |
. . . 4
โข (๐ โ ๐ธ โ โ) |
22 | 6, 21 | subcld 11571 |
. . 3
โข (๐ โ (๐ถ โ ๐ธ) โ โ) |
23 | 18, 20, 22 | 3jca 1129 |
. 2
โข (๐ โ ((๐น โ ๐ต) โ โ โง ((๐ด โ ๐)๐บ(๐ต โ ๐)) โ โ โง (๐ถ โ ๐ธ) โ โ)) |
24 | 21, 10 | subcld 11571 |
. . 3
โข (๐ โ (๐ธ โ ๐ด) โ โ) |
25 | 11 | simp2d 1144 |
. . . 4
โข (๐ โ ๐ท โ โ) |
26 | 3, 25 | subcld 11571 |
. . 3
โข (๐ โ (๐ต โ ๐ท) โ โ) |
27 | 25, 6 | subcld 11571 |
. . 3
โข (๐ โ (๐ท โ ๐ถ) โ โ) |
28 | 24, 26, 27 | 3jca 1129 |
. 2
โข (๐ โ ((๐ธ โ ๐ด) โ โ โง (๐ต โ ๐ท) โ โ โง (๐ท โ ๐ถ) โ โ)) |
29 | | cevath.f |
. . . 4
โข (๐ โ (((๐ด โ ๐)๐บ(๐ต โ ๐)) โ 0 โง ((๐ต โ ๐)๐บ(๐ถ โ ๐)) โ 0 โง ((๐ถ โ ๐)๐บ(๐ด โ ๐)) โ 0)) |
30 | 29 | simp2d 1144 |
. . 3
โข (๐ โ ((๐ต โ ๐)๐บ(๐ถ โ ๐)) โ 0) |
31 | 29 | simp1d 1143 |
. . 3
โข (๐ โ ((๐ด โ ๐)๐บ(๐ต โ ๐)) โ 0) |
32 | 29 | simp3d 1145 |
. . 3
โข (๐ โ ((๐ถ โ ๐)๐บ(๐ด โ ๐)) โ 0) |
33 | 30, 31, 32 | 3jca 1129 |
. 2
โข (๐ โ (((๐ต โ ๐)๐บ(๐ถ โ ๐)) โ 0 โง ((๐ด โ ๐)๐บ(๐ต โ ๐)) โ 0 โง ((๐ถ โ ๐)๐บ(๐ด โ ๐)) โ 0)) |
34 | 6, 10, 3 | 3jca 1129 |
. . . 4
โข (๐ โ (๐ถ โ โ โง ๐ด โ โ โง ๐ต โ โ)) |
35 | 21, 12, 25 | 3jca 1129 |
. . . 4
โข (๐ โ (๐ธ โ โ โง ๐น โ โ โง ๐ท โ โ)) |
36 | | cevath.d |
. . . . . 6
โข (๐ โ (((๐ด โ ๐)๐บ(๐ท โ ๐)) = 0 โง ((๐ต โ ๐)๐บ(๐ธ โ ๐)) = 0 โง ((๐ถ โ ๐)๐บ(๐น โ ๐)) = 0)) |
37 | 36 | simp3d 1145 |
. . . . 5
โข (๐ โ ((๐ถ โ ๐)๐บ(๐น โ ๐)) = 0) |
38 | 36 | simp1d 1143 |
. . . . 5
โข (๐ โ ((๐ด โ ๐)๐บ(๐ท โ ๐)) = 0) |
39 | 36 | simp2d 1144 |
. . . . 5
โข (๐ โ ((๐ต โ ๐)๐บ(๐ธ โ ๐)) = 0) |
40 | 37, 38, 39 | 3jca 1129 |
. . . 4
โข (๐ โ (((๐ถ โ ๐)๐บ(๐น โ ๐)) = 0 โง ((๐ด โ ๐)๐บ(๐ท โ ๐)) = 0 โง ((๐ต โ ๐)๐บ(๐ธ โ ๐)) = 0)) |
41 | | cevath.e |
. . . . . 6
โข (๐ โ (((๐ด โ ๐น)๐บ(๐ต โ ๐น)) = 0 โง ((๐ต โ ๐ท)๐บ(๐ถ โ ๐ท)) = 0 โง ((๐ถ โ ๐ธ)๐บ(๐ด โ ๐ธ)) = 0)) |
42 | 41 | simp3d 1145 |
. . . . 5
โข (๐ โ ((๐ถ โ ๐ธ)๐บ(๐ด โ ๐ธ)) = 0) |
43 | 41 | simp1d 1143 |
. . . . 5
โข (๐ โ ((๐ด โ ๐น)๐บ(๐ต โ ๐น)) = 0) |
44 | 41 | simp2d 1144 |
. . . . 5
โข (๐ โ ((๐ต โ ๐ท)๐บ(๐ถ โ ๐ท)) = 0) |
45 | 42, 43, 44 | 3jca 1129 |
. . . 4
โข (๐ โ (((๐ถ โ ๐ธ)๐บ(๐ด โ ๐ธ)) = 0 โง ((๐ด โ ๐น)๐บ(๐ต โ ๐น)) = 0 โง ((๐ต โ ๐ท)๐บ(๐ถ โ ๐ท)) = 0)) |
46 | 32, 31, 30 | 3jca 1129 |
. . . 4
โข (๐ โ (((๐ถ โ ๐)๐บ(๐ด โ ๐)) โ 0 โง ((๐ด โ ๐)๐บ(๐ต โ ๐)) โ 0 โง ((๐ต โ ๐)๐บ(๐ถ โ ๐)) โ 0)) |
47 | 1, 34, 35, 4, 40, 45, 46 | cevathlem2 45584 |
. . 3
โข (๐ โ (((๐ต โ ๐)๐บ(๐ถ โ ๐)) ยท (๐ด โ ๐น)) = (((๐ถ โ ๐)๐บ(๐ด โ ๐)) ยท (๐น โ ๐ต))) |
48 | 3, 6, 10 | 3jca 1129 |
. . . 4
โข (๐ โ (๐ต โ โ โง ๐ถ โ โ โง ๐ด โ โ)) |
49 | 25, 21, 12 | 3jca 1129 |
. . . 4
โข (๐ โ (๐ท โ โ โง ๐ธ โ โ โง ๐น โ โ)) |
50 | 39, 37, 38 | 3jca 1129 |
. . . 4
โข (๐ โ (((๐ต โ ๐)๐บ(๐ธ โ ๐)) = 0 โง ((๐ถ โ ๐)๐บ(๐น โ ๐)) = 0 โง ((๐ด โ ๐)๐บ(๐ท โ ๐)) = 0)) |
51 | 44, 42, 43 | 3jca 1129 |
. . . 4
โข (๐ โ (((๐ต โ ๐ท)๐บ(๐ถ โ ๐ท)) = 0 โง ((๐ถ โ ๐ธ)๐บ(๐ด โ ๐ธ)) = 0 โง ((๐ด โ ๐น)๐บ(๐ต โ ๐น)) = 0)) |
52 | 30, 32, 31 | 3jca 1129 |
. . . 4
โข (๐ โ (((๐ต โ ๐)๐บ(๐ถ โ ๐)) โ 0 โง ((๐ถ โ ๐)๐บ(๐ด โ ๐)) โ 0 โง ((๐ด โ ๐)๐บ(๐ต โ ๐)) โ 0)) |
53 | 1, 48, 49, 4, 50, 51, 52 | cevathlem2 45584 |
. . 3
โข (๐ โ (((๐ด โ ๐)๐บ(๐ต โ ๐)) ยท (๐ถ โ ๐ธ)) = (((๐ต โ ๐)๐บ(๐ถ โ ๐)) ยท (๐ธ โ ๐ด))) |
54 | 1, 2, 11, 4, 36, 41, 29 | cevathlem2 45584 |
. . 3
โข (๐ โ (((๐ถ โ ๐)๐บ(๐ด โ ๐)) ยท (๐ต โ ๐ท)) = (((๐ด โ ๐)๐บ(๐ต โ ๐)) ยท (๐ท โ ๐ถ))) |
55 | 47, 53, 54 | 3jca 1129 |
. 2
โข (๐ โ ((((๐ต โ ๐)๐บ(๐ถ โ ๐)) ยท (๐ด โ ๐น)) = (((๐ถ โ ๐)๐บ(๐ด โ ๐)) ยท (๐น โ ๐ต)) โง (((๐ด โ ๐)๐บ(๐ต โ ๐)) ยท (๐ถ โ ๐ธ)) = (((๐ต โ ๐)๐บ(๐ถ โ ๐)) ยท (๐ธ โ ๐ด)) โง (((๐ถ โ ๐)๐บ(๐ด โ ๐)) ยท (๐ต โ ๐ท)) = (((๐ด โ ๐)๐บ(๐ต โ ๐)) ยท (๐ท โ ๐ถ)))) |
56 | 17, 23, 28, 33, 55 | cevathlem1 45583 |
1
โข (๐ โ (((๐ด โ ๐น) ยท (๐ถ โ ๐ธ)) ยท (๐ต โ ๐ท)) = (((๐น โ ๐ต) ยท (๐ธ โ ๐ด)) ยท (๐ท โ ๐ถ))) |