Step | Hyp | Ref
| Expression |
1 | | df-nqqs 7349 |
. 2
โข
Q = ((N ร N) /
~Q ) |
2 | | addpipqqs 7371 |
. 2
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N)) โ ([โจ๐ฅ, ๐ฆโฉ] ~Q
+Q [โจ๐ง, ๐คโฉ] ~Q ) =
[โจ((๐ฅ
ยทN ๐ค) +N (๐ฆ
ยทN ๐ง)), (๐ฆ ยทN ๐ค)โฉ]
~Q ) |
3 | | addpipqqs 7371 |
. 2
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ ([โจ๐ง, ๐คโฉ] ~Q
+Q [โจ๐ฃ, ๐ขโฉ] ~Q ) =
[โจ((๐ง
ยทN ๐ข) +N (๐ค
ยทN ๐ฃ)), (๐ค ยทN ๐ข)โฉ]
~Q ) |
4 | | addpipqqs 7371 |
. 2
โข
(((((๐ฅ
ยทN ๐ค) +N (๐ฆ
ยทN ๐ง)) โ N โง (๐ฆ
ยทN ๐ค) โ N) โง (๐ฃ โ N โง
๐ข โ N))
โ ([โจ((๐ฅ
ยทN ๐ค) +N (๐ฆ
ยทN ๐ง)), (๐ฆ ยทN ๐ค)โฉ]
~Q +Q [โจ๐ฃ, ๐ขโฉ] ~Q ) =
[โจ((((๐ฅ
ยทN ๐ค) +N (๐ฆ
ยทN ๐ง)) ยทN ๐ข) +N
((๐ฆ
ยทN ๐ค) ยทN ๐ฃ)), ((๐ฆ ยทN ๐ค)
ยทN ๐ข)โฉ] ~Q
) |
5 | | addpipqqs 7371 |
. 2
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (((๐ง
ยทN ๐ข) +N (๐ค
ยทN ๐ฃ)) โ N โง (๐ค
ยทN ๐ข) โ N)) โ
([โจ๐ฅ, ๐ฆโฉ]
~Q +Q [โจ((๐ง
ยทN ๐ข) +N (๐ค
ยทN ๐ฃ)), (๐ค ยทN ๐ข)โฉ]
~Q ) = [โจ((๐ฅ ยทN (๐ค
ยทN ๐ข)) +N (๐ฆ
ยทN ((๐ง ยทN ๐ข) +N
(๐ค
ยทN ๐ฃ)))), (๐ฆ ยทN (๐ค
ยทN ๐ข))โฉ] ~Q
) |
6 | | mulclpi 7329 |
. . . . 5
โข ((๐ฅ โ N โง
๐ค โ N)
โ (๐ฅ
ยทN ๐ค) โ N) |
7 | 6 | ad2ant2rl 511 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N)) โ (๐ฅ ยทN ๐ค) โ
N) |
8 | | mulclpi 7329 |
. . . . 5
โข ((๐ฆ โ N โง
๐ง โ N)
โ (๐ฆ
ยทN ๐ง) โ N) |
9 | 8 | ad2ant2lr 510 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N)) โ (๐ฆ ยทN ๐ง) โ
N) |
10 | | addclpi 7328 |
. . . 4
โข (((๐ฅ
ยทN ๐ค) โ N โง (๐ฆ
ยทN ๐ง) โ N) โ ((๐ฅ
ยทN ๐ค) +N (๐ฆ
ยทN ๐ง)) โ N) |
11 | 7, 9, 10 | syl2anc 411 |
. . 3
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N)) โ ((๐ฅ ยทN ๐ค) +N
(๐ฆ
ยทN ๐ง)) โ N) |
12 | | mulclpi 7329 |
. . . 4
โข ((๐ฆ โ N โง
๐ค โ N)
โ (๐ฆ
ยทN ๐ค) โ N) |
13 | 12 | ad2ant2l 508 |
. . 3
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N)) โ (๐ฆ ยทN ๐ค) โ
N) |
14 | 11, 13 | jca 306 |
. 2
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N)) โ (((๐ฅ ยทN ๐ค) +N
(๐ฆ
ยทN ๐ง)) โ N โง (๐ฆ
ยทN ๐ค) โ N)) |
15 | | mulclpi 7329 |
. . . . 5
โข ((๐ง โ N โง
๐ข โ N)
โ (๐ง
ยทN ๐ข) โ N) |
16 | 15 | ad2ant2rl 511 |
. . . 4
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ (๐ง ยทN ๐ข) โ
N) |
17 | | mulclpi 7329 |
. . . . 5
โข ((๐ค โ N โง
๐ฃ โ N)
โ (๐ค
ยทN ๐ฃ) โ N) |
18 | 17 | ad2ant2lr 510 |
. . . 4
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ (๐ค ยทN ๐ฃ) โ
N) |
19 | | addclpi 7328 |
. . . 4
โข (((๐ง
ยทN ๐ข) โ N โง (๐ค
ยทN ๐ฃ) โ N) โ ((๐ง
ยทN ๐ข) +N (๐ค
ยทN ๐ฃ)) โ N) |
20 | 16, 18, 19 | syl2anc 411 |
. . 3
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ ((๐ง ยทN ๐ข) +N
(๐ค
ยทN ๐ฃ)) โ N) |
21 | | mulclpi 7329 |
. . . 4
โข ((๐ค โ N โง
๐ข โ N)
โ (๐ค
ยทN ๐ข) โ N) |
22 | 21 | ad2ant2l 508 |
. . 3
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ (๐ค ยทN ๐ข) โ
N) |
23 | 20, 22 | jca 306 |
. 2
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ (((๐ง ยทN ๐ข) +N
(๐ค
ยทN ๐ฃ)) โ N โง (๐ค
ยทN ๐ข) โ N)) |
24 | | simp1l 1021 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
๐ฅ โ
N) |
25 | | simp2r 1024 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
๐ค โ
N) |
26 | | simp3r 1026 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
๐ข โ
N) |
27 | 25, 26, 21 | syl2anc 411 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(๐ค
ยทN ๐ข) โ N) |
28 | | mulclpi 7329 |
. . . . 5
โข ((๐ฅ โ N โง
(๐ค
ยทN ๐ข) โ N) โ (๐ฅ
ยทN (๐ค ยทN ๐ข)) โ
N) |
29 | 24, 27, 28 | syl2anc 411 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(๐ฅ
ยทN (๐ค ยทN ๐ข)) โ
N) |
30 | | simp1r 1022 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
๐ฆ โ
N) |
31 | | simp2l 1023 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
๐ง โ
N) |
32 | 31, 26, 15 | syl2anc 411 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(๐ง
ยทN ๐ข) โ N) |
33 | | mulclpi 7329 |
. . . . 5
โข ((๐ฆ โ N โง
(๐ง
ยทN ๐ข) โ N) โ (๐ฆ
ยทN (๐ง ยทN ๐ข)) โ
N) |
34 | 30, 32, 33 | syl2anc 411 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(๐ฆ
ยทN (๐ง ยทN ๐ข)) โ
N) |
35 | | simp3l 1025 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
๐ฃ โ
N) |
36 | 25, 35, 17 | syl2anc 411 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(๐ค
ยทN ๐ฃ) โ N) |
37 | | mulclpi 7329 |
. . . . 5
โข ((๐ฆ โ N โง
(๐ค
ยทN ๐ฃ) โ N) โ (๐ฆ
ยทN (๐ค ยทN ๐ฃ)) โ
N) |
38 | 30, 36, 37 | syl2anc 411 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(๐ฆ
ยทN (๐ค ยทN ๐ฃ)) โ
N) |
39 | | addasspig 7331 |
. . . 4
โข (((๐ฅ
ยทN (๐ค ยทN ๐ข)) โ N โง
(๐ฆ
ยทN (๐ง ยทN ๐ข)) โ N โง
(๐ฆ
ยทN (๐ค ยทN ๐ฃ)) โ N)
โ (((๐ฅ
ยทN (๐ค ยทN ๐ข)) +N
(๐ฆ
ยทN (๐ง ยทN ๐ข))) +N
(๐ฆ
ยทN (๐ค ยทN ๐ฃ))) = ((๐ฅ ยทN (๐ค
ยทN ๐ข)) +N ((๐ฆ
ยทN (๐ง ยทN ๐ข)) +N
(๐ฆ
ยทN (๐ค ยทN ๐ฃ))))) |
40 | 29, 34, 38, 39 | syl3anc 1238 |
. . 3
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(((๐ฅ
ยทN (๐ค ยทN ๐ข)) +N
(๐ฆ
ยทN (๐ง ยทN ๐ข))) +N
(๐ฆ
ยทN (๐ค ยทN ๐ฃ))) = ((๐ฅ ยทN (๐ค
ยทN ๐ข)) +N ((๐ฆ
ยทN (๐ง ยทN ๐ข)) +N
(๐ฆ
ยทN (๐ค ยทN ๐ฃ))))) |
41 | | mulcompig 7332 |
. . . . . 6
โข ((๐ โ N โง
๐ โ N)
โ (๐
ยทN ๐) = (๐ ยทN ๐)) |
42 | 41 | adantl 277 |
. . . . 5
โข ((((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โง
(๐ โ N
โง ๐ โ
N)) โ (๐
ยทN ๐) = (๐ ยทN ๐)) |
43 | | distrpig 7334 |
. . . . . . . 8
โข ((โ โ N โง
๐ โ N
โง ๐ โ
N) โ (โ
ยทN (๐ +N ๐)) = ((โ ยทN ๐) +N
(โ
ยทN ๐))) |
44 | 43 | 3coml 1210 |
. . . . . . 7
โข ((๐ โ N โง
๐ โ N
โง โ โ
N) โ (โ
ยทN (๐ +N ๐)) = ((โ ยทN ๐) +N
(โ
ยทN ๐))) |
45 | | addclpi 7328 |
. . . . . . . . . 10
โข ((๐ โ N โง
๐ โ N)
โ (๐
+N ๐) โ N) |
46 | | mulcompig 7332 |
. . . . . . . . . 10
โข ((โ โ N โง
(๐
+N ๐) โ N) โ (โ
ยทN (๐ +N ๐)) = ((๐ +N ๐)
ยทN โ)) |
47 | 45, 46 | sylan2 286 |
. . . . . . . . 9
โข ((โ โ N โง
(๐ โ N
โง ๐ โ
N)) โ (โ
ยทN (๐ +N ๐)) = ((๐ +N ๐)
ยทN โ)) |
48 | 47 | ancoms 268 |
. . . . . . . 8
โข (((๐ โ N โง
๐ โ N)
โง โ โ
N) โ (โ
ยทN (๐ +N ๐)) = ((๐ +N ๐)
ยทN โ)) |
49 | 48 | 3impa 1194 |
. . . . . . 7
โข ((๐ โ N โง
๐ โ N
โง โ โ
N) โ (โ
ยทN (๐ +N ๐)) = ((๐ +N ๐)
ยทN โ)) |
50 | | mulcompig 7332 |
. . . . . . . . . 10
โข ((โ โ N โง
๐ โ N)
โ (โ
ยทN ๐) = (๐ ยทN โ)) |
51 | 50 | ancoms 268 |
. . . . . . . . 9
โข ((๐ โ N โง
โ โ N)
โ (โ
ยทN ๐) = (๐ ยทN โ)) |
52 | 51 | 3adant2 1016 |
. . . . . . . 8
โข ((๐ โ N โง
๐ โ N
โง โ โ
N) โ (โ
ยทN ๐) = (๐ ยทN โ)) |
53 | | mulcompig 7332 |
. . . . . . . . . 10
โข ((โ โ N โง
๐ โ N)
โ (โ
ยทN ๐) = (๐ ยทN โ)) |
54 | 53 | ancoms 268 |
. . . . . . . . 9
โข ((๐ โ N โง
โ โ N)
โ (โ
ยทN ๐) = (๐ ยทN โ)) |
55 | 54 | 3adant1 1015 |
. . . . . . . 8
โข ((๐ โ N โง
๐ โ N
โง โ โ
N) โ (โ
ยทN ๐) = (๐ ยทN โ)) |
56 | 52, 55 | oveq12d 5895 |
. . . . . . 7
โข ((๐ โ N โง
๐ โ N
โง โ โ
N) โ ((โ
ยทN ๐) +N (โ
ยทN ๐)) = ((๐ ยทN โ) +N
(๐
ยทN โ))) |
57 | 44, 49, 56 | 3eqtr3d 2218 |
. . . . . 6
โข ((๐ โ N โง
๐ โ N
โง โ โ
N) โ ((๐
+N ๐) ยทN โ) = ((๐ ยทN โ) +N
(๐
ยทN โ))) |
58 | 57 | adantl 277 |
. . . . 5
โข ((((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โง
(๐ โ N
โง ๐ โ
N โง โ
โ N)) โ ((๐ +N ๐)
ยทN โ) = ((๐ ยทN โ) +N
(๐
ยทN โ))) |
59 | | mulasspig 7333 |
. . . . . 6
โข ((๐ โ N โง
๐ โ N
โง โ โ
N) โ ((๐
ยทN ๐) ยทN โ) = (๐ ยทN (๐
ยทN โ))) |
60 | 59 | adantl 277 |
. . . . 5
โข ((((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โง
(๐ โ N
โง ๐ โ
N โง โ
โ N)) โ ((๐ ยทN ๐)
ยทN โ) = (๐ ยทN (๐
ยทN โ))) |
61 | | mulclpi 7329 |
. . . . . 6
โข ((๐ โ N โง
๐ โ N)
โ (๐
ยทN ๐) โ N) |
62 | 61 | adantl 277 |
. . . . 5
โข ((((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โง
(๐ โ N
โง ๐ โ
N)) โ (๐
ยทN ๐) โ N) |
63 | 42, 58, 60, 62, 24, 30, 25, 31, 26 | caovdilemd 6068 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(((๐ฅ
ยทN ๐ค) +N (๐ฆ
ยทN ๐ง)) ยทN ๐ข) = ((๐ฅ ยทN (๐ค
ยทN ๐ข)) +N (๐ฆ
ยทN (๐ง ยทN ๐ข)))) |
64 | | mulasspig 7333 |
. . . . . . 7
โข ((๐ฆ โ N โง
๐ค โ N
โง ๐ฃ โ
N) โ ((๐ฆ
ยทN ๐ค) ยทN ๐ฃ) = (๐ฆ ยทN (๐ค
ยทN ๐ฃ))) |
65 | 64 | 3adant1l 1230 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง ๐ค โ
N โง ๐ฃ
โ N) โ ((๐ฆ ยทN ๐ค)
ยทN ๐ฃ) = (๐ฆ ยทN (๐ค
ยทN ๐ฃ))) |
66 | 65 | 3adant2l 1232 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง ๐ฃ โ N) โ ((๐ฆ
ยทN ๐ค) ยทN ๐ฃ) = (๐ฆ ยทN (๐ค
ยทN ๐ฃ))) |
67 | 66 | 3adant3r 1235 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
((๐ฆ
ยทN ๐ค) ยทN ๐ฃ) = (๐ฆ ยทN (๐ค
ยทN ๐ฃ))) |
68 | 63, 67 | oveq12d 5895 |
. . 3
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
((((๐ฅ
ยทN ๐ค) +N (๐ฆ
ยทN ๐ง)) ยทN ๐ข) +N
((๐ฆ
ยทN ๐ค) ยทN ๐ฃ)) = (((๐ฅ ยทN (๐ค
ยทN ๐ข)) +N (๐ฆ
ยทN (๐ง ยทN ๐ข))) +N
(๐ฆ
ยทN (๐ค ยทN ๐ฃ)))) |
69 | | distrpig 7334 |
. . . . 5
โข ((๐ฆ โ N โง
(๐ง
ยทN ๐ข) โ N โง (๐ค
ยทN ๐ฃ) โ N) โ (๐ฆ
ยทN ((๐ง ยทN ๐ข) +N
(๐ค
ยทN ๐ฃ))) = ((๐ฆ ยทN (๐ง
ยทN ๐ข)) +N (๐ฆ
ยทN (๐ค ยทN ๐ฃ)))) |
70 | 30, 32, 36, 69 | syl3anc 1238 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(๐ฆ
ยทN ((๐ง ยทN ๐ข) +N
(๐ค
ยทN ๐ฃ))) = ((๐ฆ ยทN (๐ง
ยทN ๐ข)) +N (๐ฆ
ยทN (๐ค ยทN ๐ฃ)))) |
71 | 70 | oveq2d 5893 |
. . 3
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
((๐ฅ
ยทN (๐ค ยทN ๐ข)) +N
(๐ฆ
ยทN ((๐ง ยทN ๐ข) +N
(๐ค
ยทN ๐ฃ)))) = ((๐ฅ ยทN (๐ค
ยทN ๐ข)) +N ((๐ฆ
ยทN (๐ง ยทN ๐ข)) +N
(๐ฆ
ยทN (๐ค ยทN ๐ฃ))))) |
72 | 40, 68, 71 | 3eqtr4d 2220 |
. 2
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
((((๐ฅ
ยทN ๐ค) +N (๐ฆ
ยทN ๐ง)) ยทN ๐ข) +N
((๐ฆ
ยทN ๐ค) ยทN ๐ฃ)) = ((๐ฅ ยทN (๐ค
ยทN ๐ข)) +N (๐ฆ
ยทN ((๐ง ยทN ๐ข) +N
(๐ค
ยทN ๐ฃ))))) |
73 | | mulasspig 7333 |
. . . . 5
โข ((๐ฆ โ N โง
๐ค โ N
โง ๐ข โ
N) โ ((๐ฆ
ยทN ๐ค) ยทN ๐ข) = (๐ฆ ยทN (๐ค
ยทN ๐ข))) |
74 | 73 | 3adant1l 1230 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง ๐ค โ
N โง ๐ข
โ N) โ ((๐ฆ ยทN ๐ค)
ยทN ๐ข) = (๐ฆ ยทN (๐ค
ยทN ๐ข))) |
75 | 74 | 3adant2l 1232 |
. . 3
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง ๐ข โ N) โ ((๐ฆ
ยทN ๐ค) ยทN ๐ข) = (๐ฆ ยทN (๐ค
ยทN ๐ข))) |
76 | 75 | 3adant3l 1234 |
. 2
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
((๐ฆ
ยทN ๐ค) ยทN ๐ข) = (๐ฆ ยทN (๐ค
ยทN ๐ข))) |
77 | 1, 2, 3, 4, 5, 14,
23, 72, 76 | ecoviass 6647 |
1
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ((๐ด
+Q ๐ต) +Q ๐ถ) = (๐ด +Q (๐ต +Q
๐ถ))) |