Step | Hyp | Ref
| Expression |
1 | | df-nq0 7423 |
. . 3
โข
Q0 = ((ฯ ร N)
/ ~Q0 ) |
2 | | oveq1 5881 |
. . . 4
โข
([โจ๐ฅ, ๐ฆโฉ]
~Q0 = ๐ด โ ([โจ๐ฅ, ๐ฆโฉ] ~Q0
+Q0 [โจ๐ง, ๐คโฉ] ~Q0 ) =
(๐ด
+Q0 [โจ๐ง, ๐คโฉ] ~Q0
)) |
3 | 2 | eleq1d 2246 |
. . 3
โข
([โจ๐ฅ, ๐ฆโฉ]
~Q0 = ๐ด โ (([โจ๐ฅ, ๐ฆโฉ] ~Q0
+Q0 [โจ๐ง, ๐คโฉ] ~Q0 ) โ
((ฯ ร N) / ~Q0 )
โ (๐ด
+Q0 [โจ๐ง, ๐คโฉ] ~Q0 ) โ
((ฯ ร N) / ~Q0
))) |
4 | | oveq2 5882 |
. . . 4
โข
([โจ๐ง, ๐คโฉ]
~Q0 = ๐ต โ (๐ด +Q0 [โจ๐ง, ๐คโฉ] ~Q0 ) =
(๐ด
+Q0 ๐ต)) |
5 | 4 | eleq1d 2246 |
. . 3
โข
([โจ๐ง, ๐คโฉ]
~Q0 = ๐ต โ ((๐ด +Q0 [โจ๐ง, ๐คโฉ] ~Q0 ) โ
((ฯ ร N) / ~Q0 )
โ (๐ด
+Q0 ๐ต) โ ((ฯ ร N)
/ ~Q0 ))) |
6 | | addnnnq0 7447 |
. . . 4
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ค โ N))
โ ([โจ๐ฅ, ๐ฆโฉ]
~Q0 +Q0 [โจ๐ง, ๐คโฉ] ~Q0 ) =
[โจ((๐ฅ
ยทo ๐ค)
+o (๐ฆ
ยทo ๐ง)),
(๐ฆ ยทo
๐ค)โฉ]
~Q0 ) |
7 | | pinn 7307 |
. . . . . . . . 9
โข (๐ค โ N โ
๐ค โ
ฯ) |
8 | | nnmcl 6481 |
. . . . . . . . 9
โข ((๐ฅ โ ฯ โง ๐ค โ ฯ) โ (๐ฅ ยทo ๐ค) โ
ฯ) |
9 | 7, 8 | sylan2 286 |
. . . . . . . 8
โข ((๐ฅ โ ฯ โง ๐ค โ N) โ
(๐ฅ ยทo
๐ค) โ
ฯ) |
10 | | pinn 7307 |
. . . . . . . . 9
โข (๐ฆ โ N โ
๐ฆ โ
ฯ) |
11 | | nnmcl 6481 |
. . . . . . . . 9
โข ((๐ฆ โ ฯ โง ๐ง โ ฯ) โ (๐ฆ ยทo ๐ง) โ
ฯ) |
12 | 10, 11 | sylan 283 |
. . . . . . . 8
โข ((๐ฆ โ N โง
๐ง โ ฯ) โ
(๐ฆ ยทo
๐ง) โ
ฯ) |
13 | | nnacl 6480 |
. . . . . . . 8
โข (((๐ฅ ยทo ๐ค) โ ฯ โง (๐ฆ ยทo ๐ง) โ ฯ) โ ((๐ฅ ยทo ๐ค) +o (๐ฆ ยทo ๐ง)) โ
ฯ) |
14 | 9, 12, 13 | syl2an 289 |
. . . . . . 7
โข (((๐ฅ โ ฯ โง ๐ค โ N) โง
(๐ฆ โ N
โง ๐ง โ ฯ))
โ ((๐ฅ
ยทo ๐ค)
+o (๐ฆ
ยทo ๐ง))
โ ฯ) |
15 | 14 | an42s 589 |
. . . . . 6
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ค โ N))
โ ((๐ฅ
ยทo ๐ค)
+o (๐ฆ
ยทo ๐ง))
โ ฯ) |
16 | | mulpiord 7315 |
. . . . . . . 8
โข ((๐ฆ โ N โง
๐ค โ N)
โ (๐ฆ
ยทN ๐ค) = (๐ฆ ยทo ๐ค)) |
17 | | mulclpi 7326 |
. . . . . . . 8
โข ((๐ฆ โ N โง
๐ค โ N)
โ (๐ฆ
ยทN ๐ค) โ N) |
18 | 16, 17 | eqeltrrd 2255 |
. . . . . . 7
โข ((๐ฆ โ N โง
๐ค โ N)
โ (๐ฆ
ยทo ๐ค)
โ N) |
19 | 18 | ad2ant2l 508 |
. . . . . 6
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ค โ N))
โ (๐ฆ
ยทo ๐ค)
โ N) |
20 | 15, 19 | jca 306 |
. . . . 5
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ค โ N))
โ (((๐ฅ
ยทo ๐ค)
+o (๐ฆ
ยทo ๐ง))
โ ฯ โง (๐ฆ
ยทo ๐ค)
โ N)) |
21 | | opelxpi 4658 |
. . . . 5
โข ((((๐ฅ ยทo ๐ค) +o (๐ฆ ยทo ๐ง)) โ ฯ โง (๐ฆ ยทo ๐ค) โ N) โ
โจ((๐ฅ
ยทo ๐ค)
+o (๐ฆ
ยทo ๐ง)),
(๐ฆ ยทo
๐ค)โฉ โ (ฯ
ร N)) |
22 | | enq0ex 7437 |
. . . . . 6
โข
~Q0 โ V |
23 | 22 | ecelqsi 6588 |
. . . . 5
โข
(โจ((๐ฅ
ยทo ๐ค)
+o (๐ฆ
ยทo ๐ง)),
(๐ฆ ยทo
๐ค)โฉ โ (ฯ
ร N) โ [โจ((๐ฅ ยทo ๐ค) +o (๐ฆ ยทo ๐ง)), (๐ฆ ยทo ๐ค)โฉ] ~Q0 โ
((ฯ ร N) / ~Q0
)) |
24 | 20, 21, 23 | 3syl 17 |
. . . 4
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ค โ N))
โ [โจ((๐ฅ
ยทo ๐ค)
+o (๐ฆ
ยทo ๐ง)),
(๐ฆ ยทo
๐ค)โฉ]
~Q0 โ ((ฯ ร N) /
~Q0 )) |
25 | 6, 24 | eqeltrd 2254 |
. . 3
โข (((๐ฅ โ ฯ โง ๐ฆ โ N) โง
(๐ง โ ฯ โง
๐ค โ N))
โ ([โจ๐ฅ, ๐ฆโฉ]
~Q0 +Q0 [โจ๐ง, ๐คโฉ] ~Q0 ) โ
((ฯ ร N) / ~Q0
)) |
26 | 1, 3, 5, 25 | 2ecoptocl 6622 |
. 2
โข ((๐ด โ
Q0 โง ๐ต โ Q0) โ
(๐ด
+Q0 ๐ต) โ ((ฯ ร N)
/ ~Q0 )) |
27 | 26, 1 | eleqtrrdi 2271 |
1
โข ((๐ด โ
Q0 โง ๐ต โ Q0) โ
(๐ด
+Q0 ๐ต) โ
Q0) |