Step | Hyp | Ref
| Expression |
1 | | df-nqqs 7346 |
. . 3
โข
Q = ((N ร N) /
~Q ) |
2 | | oveq1 5881 |
. . . 4
โข
([โจ๐ฅ, ๐ฆโฉ]
~Q = ๐ด โ ([โจ๐ฅ, ๐ฆโฉ] ~Q
+Q [โจ๐ง, ๐คโฉ] ~Q ) =
(๐ด
+Q [โจ๐ง, ๐คโฉ] ~Q
)) |
3 | 2 | eleq1d 2246 |
. . 3
โข
([โจ๐ฅ, ๐ฆโฉ]
~Q = ๐ด โ (([โจ๐ฅ, ๐ฆโฉ] ~Q
+Q [โจ๐ง, ๐คโฉ] ~Q ) โ
((N ร N) / ~Q
) โ (๐ด
+Q [โจ๐ง, ๐คโฉ] ~Q ) โ
((N ร N) / ~Q
))) |
4 | | oveq2 5882 |
. . . 4
โข
([โจ๐ง, ๐คโฉ]
~Q = ๐ต โ (๐ด +Q [โจ๐ง, ๐คโฉ] ~Q ) =
(๐ด
+Q ๐ต)) |
5 | 4 | eleq1d 2246 |
. . 3
โข
([โจ๐ง, ๐คโฉ]
~Q = ๐ต โ ((๐ด +Q [โจ๐ง, ๐คโฉ] ~Q ) โ
((N ร N) / ~Q
) โ (๐ด
+Q ๐ต) โ ((N ร
N) / ~Q ))) |
6 | | addpipqqs 7368 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N)) โ ([โจ๐ฅ, ๐ฆโฉ] ~Q
+Q [โจ๐ง, ๐คโฉ] ~Q ) =
[โจ((๐ฅ
ยทN ๐ค) +N (๐ฆ
ยทN ๐ง)), (๐ฆ ยทN ๐ค)โฉ]
~Q ) |
7 | | mulclpi 7326 |
. . . . . . . 8
โข ((๐ฅ โ N โง
๐ค โ N)
โ (๐ฅ
ยทN ๐ค) โ N) |
8 | | mulclpi 7326 |
. . . . . . . 8
โข ((๐ฆ โ N โง
๐ง โ N)
โ (๐ฆ
ยทN ๐ง) โ N) |
9 | | addclpi 7325 |
. . . . . . . 8
โข (((๐ฅ
ยทN ๐ค) โ N โง (๐ฆ
ยทN ๐ง) โ N) โ ((๐ฅ
ยทN ๐ค) +N (๐ฆ
ยทN ๐ง)) โ N) |
10 | 7, 8, 9 | syl2an 289 |
. . . . . . 7
โข (((๐ฅ โ N โง
๐ค โ N)
โง (๐ฆ โ
N โง ๐ง
โ N)) โ ((๐ฅ ยทN ๐ค) +N
(๐ฆ
ยทN ๐ง)) โ N) |
11 | 10 | an42s 589 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N)) โ ((๐ฅ ยทN ๐ค) +N
(๐ฆ
ยทN ๐ง)) โ N) |
12 | | mulclpi 7326 |
. . . . . . 7
โข ((๐ฆ โ N โง
๐ค โ N)
โ (๐ฆ
ยทN ๐ค) โ N) |
13 | 12 | ad2ant2l 508 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N)) โ (๐ฆ ยทN ๐ค) โ
N) |
14 | 11, 13 | jca 306 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N)) โ (((๐ฅ ยทN ๐ค) +N
(๐ฆ
ยทN ๐ง)) โ N โง (๐ฆ
ยทN ๐ค) โ N)) |
15 | | opelxpi 4658 |
. . . . 5
โข ((((๐ฅ
ยทN ๐ค) +N (๐ฆ
ยทN ๐ง)) โ N โง (๐ฆ
ยทN ๐ค) โ N) โ
โจ((๐ฅ
ยทN ๐ค) +N (๐ฆ
ยทN ๐ง)), (๐ฆ ยทN ๐ค)โฉ โ (N
ร N)) |
16 | | enqex 7358 |
. . . . . 6
โข
~Q โ V |
17 | 16 | ecelqsi 6588 |
. . . . 5
โข
(โจ((๐ฅ
ยทN ๐ค) +N (๐ฆ
ยทN ๐ง)), (๐ฆ ยทN ๐ค)โฉ โ (N
ร N) โ [โจ((๐ฅ ยทN ๐ค) +N
(๐ฆ
ยทN ๐ง)), (๐ฆ ยทN ๐ค)โฉ]
~Q โ ((N ร N)
/ ~Q )) |
18 | 14, 15, 17 | 3syl 17 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N)) โ [โจ((๐ฅ ยทN ๐ค) +N
(๐ฆ
ยทN ๐ง)), (๐ฆ ยทN ๐ค)โฉ]
~Q โ ((N ร N)
/ ~Q )) |
19 | 6, 18 | eqeltrd 2254 |
. . 3
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N)) โ ([โจ๐ฅ, ๐ฆโฉ] ~Q
+Q [โจ๐ง, ๐คโฉ] ~Q ) โ
((N ร N) / ~Q
)) |
20 | 1, 3, 5, 19 | 2ecoptocl 6622 |
. 2
โข ((๐ด โ Q โง
๐ต โ Q)
โ (๐ด
+Q ๐ต) โ ((N ร
N) / ~Q )) |
21 | 20, 1 | eleqtrrdi 2271 |
1
โข ((๐ด โ Q โง
๐ต โ Q)
โ (๐ด
+Q ๐ต) โ Q) |