Step | Hyp | Ref
| Expression |
1 | | addpipqqslem 7368 |
. 2
โข (((๐ด โ N โง
๐ต โ N)
โง (๐ถ โ
N โง ๐ท
โ N)) โ โจ((๐ด ยทN ๐ท) +N
(๐ต
ยทN ๐ถ)), (๐ต ยทN ๐ท)โฉ โ (N
ร N)) |
2 | | addpipqqslem 7368 |
. 2
โข (((๐ โ N โง
๐ โ N)
โง (๐ โ
N โง โ
โ N)) โ โจ((๐ ยทN โ) +N
(๐
ยทN ๐)), (๐ ยทN โ)โฉ โ (N
ร N)) |
3 | | addpipqqslem 7368 |
. 2
โข (((๐ โ N โง
๐ โ N)
โง (๐ก โ
N โง ๐
โ N)) โ โจ((๐ ยทN ๐ ) +N
(๐
ยทN ๐ก)), (๐ ยทN ๐ )โฉ โ (N
ร N)) |
4 | | enqex 7359 |
. 2
โข
~Q โ V |
5 | | enqer 7357 |
. 2
โข
~Q Er (N ร
N) |
6 | | df-enq 7346 |
. 2
โข
~Q = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (N ร
N) โง ๐ฆ
โ (N ร N)) โง โ๐งโ๐คโ๐ฃโ๐ข((๐ฅ = โจ๐ง, ๐คโฉ โง ๐ฆ = โจ๐ฃ, ๐ขโฉ) โง (๐ง ยทN ๐ข) = (๐ค ยทN ๐ฃ)))} |
7 | | oveq12 5884 |
. . . 4
โข ((๐ง = ๐ โง ๐ข = ๐) โ (๐ง ยทN ๐ข) = (๐ ยทN ๐)) |
8 | | oveq12 5884 |
. . . 4
โข ((๐ค = ๐ โง ๐ฃ = ๐) โ (๐ค ยทN ๐ฃ) = (๐ ยทN ๐)) |
9 | 7, 8 | eqeqan12d 2193 |
. . 3
โข (((๐ง = ๐ โง ๐ข = ๐) โง (๐ค = ๐ โง ๐ฃ = ๐)) โ ((๐ง ยทN ๐ข) = (๐ค ยทN ๐ฃ) โ (๐ ยทN ๐) = (๐ ยทN ๐))) |
10 | 9 | an42s 589 |
. 2
โข (((๐ง = ๐ โง ๐ค = ๐) โง (๐ฃ = ๐ โง ๐ข = ๐)) โ ((๐ง ยทN ๐ข) = (๐ค ยทN ๐ฃ) โ (๐ ยทN ๐) = (๐ ยทN ๐))) |
11 | | oveq12 5884 |
. . . 4
โข ((๐ง = ๐ โง ๐ข = ๐ ) โ (๐ง ยทN ๐ข) = (๐ ยทN ๐ )) |
12 | | oveq12 5884 |
. . . 4
โข ((๐ค = โ โง ๐ฃ = ๐ก) โ (๐ค ยทN ๐ฃ) = (โ ยทN ๐ก)) |
13 | 11, 12 | eqeqan12d 2193 |
. . 3
โข (((๐ง = ๐ โง ๐ข = ๐ ) โง (๐ค = โ โง ๐ฃ = ๐ก)) โ ((๐ง ยทN ๐ข) = (๐ค ยทN ๐ฃ) โ (๐ ยทN ๐ ) = (โ ยทN ๐ก))) |
14 | 13 | an42s 589 |
. 2
โข (((๐ง = ๐ โง ๐ค = โ) โง (๐ฃ = ๐ก โง ๐ข = ๐ )) โ ((๐ง ยทN ๐ข) = (๐ค ยทN ๐ฃ) โ (๐ ยทN ๐ ) = (โ ยทN ๐ก))) |
15 | | dfplpq2 7353 |
. 2
โข
+pQ = {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ((๐ฅ โ (N ร
N) โง ๐ฆ
โ (N ร N)) โง โ๐คโ๐ฃโ๐ขโ๐((๐ฅ = โจ๐ค, ๐ฃโฉ โง ๐ฆ = โจ๐ข, ๐โฉ) โง ๐ง = โจ((๐ค ยทN ๐) +N
(๐ฃ
ยทN ๐ข)), (๐ฃ ยทN ๐)โฉ))} |
16 | | oveq12 5884 |
. . . . 5
โข ((๐ค = ๐ โง ๐ = โ) โ (๐ค ยทN ๐) = (๐ ยทN โ)) |
17 | | oveq12 5884 |
. . . . 5
โข ((๐ฃ = ๐ โง ๐ข = ๐) โ (๐ฃ ยทN ๐ข) = (๐ ยทN ๐)) |
18 | 16, 17 | oveqan12d 5894 |
. . . 4
โข (((๐ค = ๐ โง ๐ = โ) โง (๐ฃ = ๐ โง ๐ข = ๐)) โ ((๐ค ยทN ๐) +N
(๐ฃ
ยทN ๐ข)) = ((๐ ยทN โ) +N
(๐
ยทN ๐))) |
19 | 18 | an42s 589 |
. . 3
โข (((๐ค = ๐ โง ๐ฃ = ๐) โง (๐ข = ๐ โง ๐ = โ)) โ ((๐ค ยทN ๐) +N
(๐ฃ
ยทN ๐ข)) = ((๐ ยทN โ) +N
(๐
ยทN ๐))) |
20 | | oveq12 5884 |
. . . 4
โข ((๐ฃ = ๐ โง ๐ = โ) โ (๐ฃ ยทN ๐) = (๐ ยทN โ)) |
21 | 20 | ad2ant2l 508 |
. . 3
โข (((๐ค = ๐ โง ๐ฃ = ๐) โง (๐ข = ๐ โง ๐ = โ)) โ (๐ฃ ยทN ๐) = (๐ ยทN โ)) |
22 | 19, 21 | opeq12d 3787 |
. 2
โข (((๐ค = ๐ โง ๐ฃ = ๐) โง (๐ข = ๐ โง ๐ = โ)) โ โจ((๐ค ยทN ๐) +N
(๐ฃ
ยทN ๐ข)), (๐ฃ ยทN ๐)โฉ = โจ((๐
ยทN โ) +N (๐
ยทN ๐)), (๐ ยทN โ)โฉ) |
23 | | oveq12 5884 |
. . . . 5
โข ((๐ค = ๐ โง ๐ = ๐ ) โ (๐ค ยทN ๐) = (๐ ยทN ๐ )) |
24 | | oveq12 5884 |
. . . . 5
โข ((๐ฃ = ๐ โง ๐ข = ๐ก) โ (๐ฃ ยทN ๐ข) = (๐ ยทN ๐ก)) |
25 | 23, 24 | oveqan12d 5894 |
. . . 4
โข (((๐ค = ๐ โง ๐ = ๐ ) โง (๐ฃ = ๐ โง ๐ข = ๐ก)) โ ((๐ค ยทN ๐) +N
(๐ฃ
ยทN ๐ข)) = ((๐ ยทN ๐ ) +N
(๐
ยทN ๐ก))) |
26 | 25 | an42s 589 |
. . 3
โข (((๐ค = ๐ โง ๐ฃ = ๐) โง (๐ข = ๐ก โง ๐ = ๐ )) โ ((๐ค ยทN ๐) +N
(๐ฃ
ยทN ๐ข)) = ((๐ ยทN ๐ ) +N
(๐
ยทN ๐ก))) |
27 | | oveq12 5884 |
. . . 4
โข ((๐ฃ = ๐ โง ๐ = ๐ ) โ (๐ฃ ยทN ๐) = (๐ ยทN ๐ )) |
28 | 27 | ad2ant2l 508 |
. . 3
โข (((๐ค = ๐ โง ๐ฃ = ๐) โง (๐ข = ๐ก โง ๐ = ๐ )) โ (๐ฃ ยทN ๐) = (๐ ยทN ๐ )) |
29 | 26, 28 | opeq12d 3787 |
. 2
โข (((๐ค = ๐ โง ๐ฃ = ๐) โง (๐ข = ๐ก โง ๐ = ๐ )) โ โจ((๐ค ยทN ๐) +N
(๐ฃ
ยทN ๐ข)), (๐ฃ ยทN ๐)โฉ = โจ((๐
ยทN ๐ ) +N (๐
ยทN ๐ก)), (๐ ยทN ๐ )โฉ) |
30 | | oveq12 5884 |
. . . . 5
โข ((๐ค = ๐ด โง ๐ = ๐ท) โ (๐ค ยทN ๐) = (๐ด ยทN ๐ท)) |
31 | | oveq12 5884 |
. . . . 5
โข ((๐ฃ = ๐ต โง ๐ข = ๐ถ) โ (๐ฃ ยทN ๐ข) = (๐ต ยทN ๐ถ)) |
32 | 30, 31 | oveqan12d 5894 |
. . . 4
โข (((๐ค = ๐ด โง ๐ = ๐ท) โง (๐ฃ = ๐ต โง ๐ข = ๐ถ)) โ ((๐ค ยทN ๐) +N
(๐ฃ
ยทN ๐ข)) = ((๐ด ยทN ๐ท) +N
(๐ต
ยทN ๐ถ))) |
33 | 32 | an42s 589 |
. . 3
โข (((๐ค = ๐ด โง ๐ฃ = ๐ต) โง (๐ข = ๐ถ โง ๐ = ๐ท)) โ ((๐ค ยทN ๐) +N
(๐ฃ
ยทN ๐ข)) = ((๐ด ยทN ๐ท) +N
(๐ต
ยทN ๐ถ))) |
34 | | oveq12 5884 |
. . . 4
โข ((๐ฃ = ๐ต โง ๐ = ๐ท) โ (๐ฃ ยทN ๐) = (๐ต ยทN ๐ท)) |
35 | 34 | ad2ant2l 508 |
. . 3
โข (((๐ค = ๐ด โง ๐ฃ = ๐ต) โง (๐ข = ๐ถ โง ๐ = ๐ท)) โ (๐ฃ ยทN ๐) = (๐ต ยทN ๐ท)) |
36 | 33, 35 | opeq12d 3787 |
. 2
โข (((๐ค = ๐ด โง ๐ฃ = ๐ต) โง (๐ข = ๐ถ โง ๐ = ๐ท)) โ โจ((๐ค ยทN ๐) +N
(๐ฃ
ยทN ๐ข)), (๐ฃ ยทN ๐)โฉ = โจ((๐ด
ยทN ๐ท) +N (๐ต
ยทN ๐ถ)), (๐ต ยทN ๐ท)โฉ) |
37 | | df-plqqs 7348 |
. 2
โข
+Q = {โจโจ๐ฅ, ๐ฆโฉ, ๐งโฉ โฃ ((๐ฅ โ Q โง ๐ฆ โ Q) โง
โ๐โ๐โ๐โ๐((๐ฅ = [โจ๐, ๐โฉ] ~Q โง
๐ฆ = [โจ๐, ๐โฉ] ~Q ) โง
๐ง = [(โจ๐, ๐โฉ +pQ
โจ๐, ๐โฉ)] ~Q
))} |
38 | | df-nqqs 7347 |
. 2
โข
Q = ((N ร N) /
~Q ) |
39 | | addcmpblnq 7366 |
. 2
โข ((((๐ โ N โง
๐ โ N)
โง (๐ โ
N โง ๐
โ N)) โง ((๐ โ N โง โ โ N) โง
(๐ก โ N
โง ๐ โ
N))) โ (((๐ ยทN ๐) = (๐ ยทN ๐) โง (๐ ยทN ๐ ) = (โ ยทN ๐ก)) โ โจ((๐
ยทN โ) +N (๐
ยทN ๐)), (๐ ยทN โ)โฉ
~Q โจ((๐ ยทN ๐ ) +N
(๐
ยทN ๐ก)), (๐ ยทN ๐ )โฉ)) |
40 | 1, 2, 3, 4, 5, 6, 10, 14, 15, 22, 29, 36, 37, 38, 39 | oviec 6641 |
1
โข (((๐ด โ N โง
๐ต โ N)
โง (๐ถ โ
N โง ๐ท
โ N)) โ ([โจ๐ด, ๐ตโฉ] ~Q
+Q [โจ๐ถ, ๐ทโฉ] ~Q ) =
[โจ((๐ด
ยทN ๐ท) +N (๐ต
ยทN ๐ถ)), (๐ต ยทN ๐ท)โฉ]
~Q ) |