Step | Hyp | Ref
| Expression |
1 | | simprll 537 |
. . . . 5
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ ๐ โ
Q) |
2 | | nqnq0a 7466 |
. . . . 5
โข ((๐ โ Q โง
๐ โ Q)
โ (๐
+Q ๐) = (๐ +Q0 ๐)) |
3 | 1, 1, 2 | syl2anc 411 |
. . . 4
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ (๐ +Q
๐) = (๐ +Q0 ๐)) |
4 | 3 | oveq2d 5904 |
. . 3
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ (๐ด +Q0
(๐
+Q ๐)) = (๐ด +Q0 (๐ +Q0
๐))) |
5 | | simpll 527 |
. . . . 5
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ ๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐))) |
6 | | simprrl 539 |
. . . . . 6
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ ๐ โ
Q) |
7 | | simprrr 540 |
. . . . . . . 8
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ ๐ โ
ฯ) |
8 | | 1pi 7327 |
. . . . . . . . . . 11
โข
1o โ N |
9 | | opelxpi 4670 |
. . . . . . . . . . 11
โข ((๐ โ ฯ โง
1o โ N) โ โจ๐, 1oโฉ โ (ฯ
ร N)) |
10 | 8, 9 | mpan2 425 |
. . . . . . . . . 10
โข (๐ โ ฯ โ
โจ๐,
1oโฉ โ (ฯ ร N)) |
11 | | enq0ex 7451 |
. . . . . . . . . . 11
โข
~Q0 โ V |
12 | 11 | ecelqsi 6602 |
. . . . . . . . . 10
โข
(โจ๐,
1oโฉ โ (ฯ ร N) โ
[โจ๐,
1oโฉ] ~Q0 โ ((ฯ ร
N) / ~Q0 )) |
13 | 10, 12 | syl 14 |
. . . . . . . . 9
โข (๐ โ ฯ โ
[โจ๐,
1oโฉ] ~Q0 โ ((ฯ ร
N) / ~Q0 )) |
14 | | df-nq0 7437 |
. . . . . . . . 9
โข
Q0 = ((ฯ ร N)
/ ~Q0 ) |
15 | 13, 14 | eleqtrrdi 2281 |
. . . . . . . 8
โข (๐ โ ฯ โ
[โจ๐,
1oโฉ] ~Q0 โ
Q0) |
16 | 7, 15 | syl 14 |
. . . . . . 7
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ
[โจ๐,
1oโฉ] ~Q0 โ
Q0) |
17 | | nqnq0 7453 |
. . . . . . . 8
โข
Q โ Q0 |
18 | 17, 1 | sselid 3165 |
. . . . . . 7
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ ๐ โ
Q0) |
19 | | mulclnq0 7464 |
. . . . . . 7
โข
(([โจ๐,
1oโฉ] ~Q0 โ
Q0 โง ๐ โ Q0) โ
([โจ๐,
1oโฉ] ~Q0
ยทQ0 ๐) โ
Q0) |
20 | 16, 18, 19 | syl2anc 411 |
. . . . . 6
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ
([โจ๐,
1oโฉ] ~Q0
ยทQ0 ๐) โ
Q0) |
21 | | nqpnq0nq 7465 |
. . . . . 6
โข ((๐ โ Q โง
([โจ๐,
1oโฉ] ~Q0
ยทQ0 ๐) โ Q0) โ
(๐
+Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ
Q) |
22 | 6, 20, 21 | syl2anc 411 |
. . . . 5
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ (๐ +Q0
([โจ๐,
1oโฉ] ~Q0
ยทQ0 ๐)) โ Q) |
23 | 5, 22 | eqeltrd 2264 |
. . . 4
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ ๐ด โ
Q) |
24 | | addclnq 7387 |
. . . . 5
โข ((๐ โ Q โง
๐ โ Q)
โ (๐
+Q ๐) โ Q) |
25 | 1, 1, 24 | syl2anc 411 |
. . . 4
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ (๐ +Q
๐) โ
Q) |
26 | | nqnq0a 7466 |
. . . 4
โข ((๐ด โ Q โง
(๐
+Q ๐) โ Q) โ (๐ด +Q
(๐
+Q ๐)) = (๐ด +Q0 (๐ +Q
๐))) |
27 | 23, 25, 26 | syl2anc 411 |
. . 3
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ (๐ด +Q
(๐
+Q ๐)) = (๐ด +Q0 (๐ +Q
๐))) |
28 | | simplr 528 |
. . . . . 6
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) |
29 | | 2onn 6535 |
. . . . . . . . . . . . . 14
โข
2o โ ฯ |
30 | | 2on0 6440 |
. . . . . . . . . . . . . 14
โข
2o โ โ
|
31 | | elni 7320 |
. . . . . . . . . . . . . 14
โข
(2o โ N โ (2o โ
ฯ โง 2o โ โ
)) |
32 | 29, 30, 31 | mpbir2an 943 |
. . . . . . . . . . . . 13
โข
2o โ N |
33 | | nnppipi 7355 |
. . . . . . . . . . . . 13
โข ((๐ โ ฯ โง
2o โ N) โ (๐ +o 2o) โ
N) |
34 | 32, 33 | mpan2 425 |
. . . . . . . . . . . 12
โข (๐ โ ฯ โ (๐ +o 2o)
โ N) |
35 | | opelxpi 4670 |
. . . . . . . . . . . 12
โข (((๐ +o 2o)
โ N โง 1o โ N) โ
โจ(๐ +o
2o), 1oโฉ โ (N ร
N)) |
36 | 34, 8, 35 | sylancl 413 |
. . . . . . . . . . 11
โข (๐ โ ฯ โ
โจ(๐ +o
2o), 1oโฉ โ (N ร
N)) |
37 | | enqex 7372 |
. . . . . . . . . . . 12
โข
~Q โ V |
38 | 37 | ecelqsi 6602 |
. . . . . . . . . . 11
โข
(โจ(๐
+o 2o), 1oโฉ โ (N
ร N) โ [โจ(๐ +o 2o),
1oโฉ] ~Q โ ((N
ร N) / ~Q
)) |
39 | 36, 38 | syl 14 |
. . . . . . . . . 10
โข (๐ โ ฯ โ
[โจ(๐ +o
2o), 1oโฉ] ~Q โ
((N ร N) / ~Q
)) |
40 | | df-nqqs 7360 |
. . . . . . . . . 10
โข
Q = ((N ร N) /
~Q ) |
41 | 39, 40 | eleqtrrdi 2281 |
. . . . . . . . 9
โข (๐ โ ฯ โ
[โจ(๐ +o
2o), 1oโฉ] ~Q โ
Q) |
42 | 7, 41 | syl 14 |
. . . . . . . 8
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ
[โจ(๐ +o
2o), 1oโฉ] ~Q โ
Q) |
43 | | mulclnq 7388 |
. . . . . . . 8
โข
(([โจ(๐
+o 2o), 1oโฉ] ~Q
โ Q โง ๐ โ Q) โ
([โจ(๐ +o
2o), 1oโฉ] ~Q
ยทQ ๐) โ Q) |
44 | 42, 1, 43 | syl2anc 411 |
. . . . . . 7
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ
([โจ(๐ +o
2o), 1oโฉ] ~Q
ยทQ ๐) โ Q) |
45 | | nqnq0a 7466 |
. . . . . . 7
โข ((๐ โ Q โง
([โจ(๐ +o
2o), 1oโฉ] ~Q
ยทQ ๐) โ Q) โ (๐ +Q
([โจ(๐ +o
2o), 1oโฉ] ~Q
ยทQ ๐)) = (๐ +Q0 ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) |
46 | 6, 44, 45 | syl2anc 411 |
. . . . . 6
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ (๐ +Q
([โจ(๐ +o
2o), 1oโฉ] ~Q
ยทQ ๐)) = (๐ +Q0 ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) |
47 | | nqnq0m 7467 |
. . . . . . . . 9
โข
(([โจ(๐
+o 2o), 1oโฉ] ~Q
โ Q โง ๐ โ Q) โ
([โจ(๐ +o
2o), 1oโฉ] ~Q
ยทQ ๐) = ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ0 ๐)) |
48 | 42, 1, 47 | syl2anc 411 |
. . . . . . . 8
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ
([โจ(๐ +o
2o), 1oโฉ] ~Q
ยทQ ๐) = ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ0 ๐)) |
49 | | nqnq0pi 7450 |
. . . . . . . . . . 11
โข (((๐ +o 2o)
โ N โง 1o โ N) โ
[โจ(๐ +o
2o), 1oโฉ] ~Q0 =
[โจ(๐ +o
2o), 1oโฉ] ~Q
) |
50 | 34, 8, 49 | sylancl 413 |
. . . . . . . . . 10
โข (๐ โ ฯ โ
[โจ(๐ +o
2o), 1oโฉ] ~Q0 =
[โจ(๐ +o
2o), 1oโฉ] ~Q
) |
51 | 7, 50 | syl 14 |
. . . . . . . . 9
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ
[โจ(๐ +o
2o), 1oโฉ] ~Q0 =
[โจ(๐ +o
2o), 1oโฉ] ~Q
) |
52 | 51 | oveq1d 5903 |
. . . . . . . 8
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ
([โจ(๐ +o
2o), 1oโฉ] ~Q0
ยทQ0 ๐) = ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ0 ๐)) |
53 | 48, 52 | eqtr4d 2223 |
. . . . . . 7
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ
([โจ(๐ +o
2o), 1oโฉ] ~Q
ยทQ ๐) = ([โจ(๐ +o 2o),
1oโฉ] ~Q0
ยทQ0 ๐)) |
54 | 53 | oveq2d 5904 |
. . . . . 6
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ (๐ +Q0
([โจ(๐ +o
2o), 1oโฉ] ~Q
ยทQ ๐)) = (๐ +Q0 ([โจ(๐ +o 2o),
1oโฉ] ~Q0
ยทQ0 ๐))) |
55 | 28, 46, 54 | 3eqtrd 2224 |
. . . . 5
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ ๐ต = (๐ +Q0 ([โจ(๐ +o 2o),
1oโฉ] ~Q0
ยทQ0 ๐))) |
56 | | nnanq0 7470 |
. . . . . . . . . 10
โข ((๐ โ ฯ โง
2o โ ฯ โง 1o โ N) โ
[โจ(๐ +o
2o), 1oโฉ] ~Q0 =
([โจ๐,
1oโฉ] ~Q0 +Q0
[โจ2o, 1oโฉ] ~Q0
)) |
57 | 8, 56 | mp3an3 1336 |
. . . . . . . . 9
โข ((๐ โ ฯ โง
2o โ ฯ) โ [โจ(๐ +o 2o),
1oโฉ] ~Q0 = ([โจ๐, 1oโฉ]
~Q0 +Q0 [โจ2o,
1oโฉ] ~Q0 )) |
58 | 7, 29, 57 | sylancl 413 |
. . . . . . . 8
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ
[โจ(๐ +o
2o), 1oโฉ] ~Q0 =
([โจ๐,
1oโฉ] ~Q0 +Q0
[โจ2o, 1oโฉ] ~Q0
)) |
59 | 58 | oveq1d 5903 |
. . . . . . 7
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ
([โจ(๐ +o
2o), 1oโฉ] ~Q0
ยทQ0 ๐) = (([โจ๐, 1oโฉ]
~Q0 +Q0 [โจ2o,
1oโฉ] ~Q0 )
ยทQ0 ๐)) |
60 | | opelxpi 4670 |
. . . . . . . . . . . 12
โข
((2o โ ฯ โง 1o โ
N) โ โจ2o, 1oโฉ โ
(ฯ ร N)) |
61 | 29, 8, 60 | mp2an 426 |
. . . . . . . . . . 11
โข
โจ2o, 1oโฉ โ (ฯ ร
N) |
62 | 11 | ecelqsi 6602 |
. . . . . . . . . . 11
โข
(โจ2o, 1oโฉ โ (ฯ ร
N) โ [โจ2o, 1oโฉ]
~Q0 โ ((ฯ ร N) /
~Q0 )) |
63 | 61, 62 | ax-mp 5 |
. . . . . . . . . 10
โข
[โจ2o, 1oโฉ] ~Q0
โ ((ฯ ร N) / ~Q0
) |
64 | 63, 14 | eleqtrri 2263 |
. . . . . . . . 9
โข
[โจ2o, 1oโฉ] ~Q0
โ Q0 |
65 | | distnq0r 7475 |
. . . . . . . . 9
โข ((๐ โ
Q0 โง [โจ๐, 1oโฉ]
~Q0 โ Q0 โง
[โจ2o, 1oโฉ] ~Q0 โ
Q0) โ (([โจ๐, 1oโฉ]
~Q0 +Q0 [โจ2o,
1oโฉ] ~Q0 )
ยทQ0 ๐) = (([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐) +Q0
([โจ2o, 1oโฉ] ~Q0
ยทQ0 ๐))) |
66 | 64, 65 | mp3an3 1336 |
. . . . . . . 8
โข ((๐ โ
Q0 โง [โจ๐, 1oโฉ]
~Q0 โ Q0) โ
(([โจ๐,
1oโฉ] ~Q0 +Q0
[โจ2o, 1oโฉ] ~Q0 )
ยทQ0 ๐) = (([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐) +Q0
([โจ2o, 1oโฉ] ~Q0
ยทQ0 ๐))) |
67 | 18, 16, 66 | syl2anc 411 |
. . . . . . 7
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ
(([โจ๐,
1oโฉ] ~Q0 +Q0
[โจ2o, 1oโฉ] ~Q0 )
ยทQ0 ๐) = (([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐) +Q0
([โจ2o, 1oโฉ] ~Q0
ยทQ0 ๐))) |
68 | 59, 67 | eqtrd 2220 |
. . . . . 6
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ
([โจ(๐ +o
2o), 1oโฉ] ~Q0
ยทQ0 ๐) = (([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐) +Q0
([โจ2o, 1oโฉ] ~Q0
ยทQ0 ๐))) |
69 | 68 | oveq2d 5904 |
. . . . 5
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ (๐ +Q0
([โจ(๐ +o
2o), 1oโฉ] ~Q0
ยทQ0 ๐)) = (๐ +Q0 (([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐) +Q0
([โจ2o, 1oโฉ] ~Q0
ยทQ0 ๐)))) |
70 | | nq02m 7477 |
. . . . . . . . 9
โข (๐ โ
Q0 โ ([โจ2o, 1oโฉ]
~Q0 ยทQ0 ๐) = (๐ +Q0 ๐)) |
71 | 70 | oveq2d 5904 |
. . . . . . . 8
โข (๐ โ
Q0 โ (([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐) +Q0
([โจ2o, 1oโฉ] ~Q0
ยทQ0 ๐)) = (([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐) +Q0
(๐
+Q0 ๐))) |
72 | 71 | oveq2d 5904 |
. . . . . . 7
โข (๐ โ
Q0 โ (๐ +Q0 (([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐) +Q0
([โจ2o, 1oโฉ] ~Q0
ยทQ0 ๐))) = (๐ +Q0 (([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐) +Q0
(๐
+Q0 ๐)))) |
73 | 18, 72 | syl 14 |
. . . . . 6
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ (๐ +Q0
(([โจ๐,
1oโฉ] ~Q0
ยทQ0 ๐) +Q0
([โจ2o, 1oโฉ] ~Q0
ยทQ0 ๐))) = (๐ +Q0 (([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐) +Q0
(๐
+Q0 ๐)))) |
74 | 17, 6 | sselid 3165 |
. . . . . . 7
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ ๐ โ
Q0) |
75 | | addclnq0 7463 |
. . . . . . . 8
โข ((๐ โ
Q0 โง ๐ โ Q0) โ
(๐
+Q0 ๐) โ
Q0) |
76 | 18, 18, 75 | syl2anc 411 |
. . . . . . 7
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ (๐ +Q0
๐) โ
Q0) |
77 | | addassnq0 7474 |
. . . . . . 7
โข ((๐ โ
Q0 โง ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐) โ
Q0 โง (๐ +Q0 ๐) โ
Q0) โ ((๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) +Q0
(๐
+Q0 ๐)) = (๐ +Q0 (([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐) +Q0
(๐
+Q0 ๐)))) |
78 | 74, 20, 76, 77 | syl3anc 1248 |
. . . . . 6
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ
((๐
+Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) +Q0
(๐
+Q0 ๐)) = (๐ +Q0 (([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐) +Q0
(๐
+Q0 ๐)))) |
79 | 73, 78 | eqtr4d 2223 |
. . . . 5
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ (๐ +Q0
(([โจ๐,
1oโฉ] ~Q0
ยทQ0 ๐) +Q0
([โจ2o, 1oโฉ] ~Q0
ยทQ0 ๐))) = ((๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) +Q0
(๐
+Q0 ๐))) |
80 | 55, 69, 79 | 3eqtrd 2224 |
. . . 4
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ ๐ต = ((๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) +Q0
(๐
+Q0 ๐))) |
81 | | oveq1 5895 |
. . . . . 6
โข (๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ (๐ด +Q0 (๐ +Q0
๐)) = ((๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) +Q0
(๐
+Q0 ๐))) |
82 | 81 | eqeq2d 2199 |
. . . . 5
โข (๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ (๐ต = (๐ด +Q0 (๐ +Q0
๐)) โ ๐ต = ((๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) +Q0
(๐
+Q0 ๐)))) |
83 | 5, 82 | syl 14 |
. . . 4
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ (๐ต = (๐ด +Q0 (๐ +Q0
๐)) โ ๐ต = ((๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) +Q0
(๐
+Q0 ๐)))) |
84 | 80, 83 | mpbird 167 |
. . 3
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ ๐ต = (๐ด +Q0 (๐ +Q0
๐))) |
85 | 4, 27, 84 | 3eqtr4rd 2231 |
. 2
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ ๐ต = (๐ด +Q (๐ +Q
๐))) |
86 | | simprlr 538 |
. . 3
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ (๐ +Q
๐)
<Q ๐) |
87 | | ltrelnq 7377 |
. . . . . 6
โข
<Q โ (Q ร
Q) |
88 | 87 | brel 4690 |
. . . . 5
โข ((๐ +Q
๐)
<Q ๐ โ ((๐ +Q ๐) โ Q โง
๐ โ
Q)) |
89 | 86, 88 | syl 14 |
. . . 4
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ
((๐
+Q ๐) โ Q โง ๐ โ
Q)) |
90 | | ltanqg 7412 |
. . . . 5
โข (((๐ +Q
๐) โ Q
โง ๐ โ
Q โง ๐ด
โ Q) โ ((๐ +Q ๐) <Q
๐ โ (๐ด +Q (๐ +Q
๐))
<Q (๐ด +Q ๐))) |
91 | 90 | 3expa 1204 |
. . . 4
โข ((((๐ +Q
๐) โ Q
โง ๐ โ
Q) โง ๐ด
โ Q) โ ((๐ +Q ๐) <Q
๐ โ (๐ด +Q (๐ +Q
๐))
<Q (๐ด +Q ๐))) |
92 | 89, 23, 91 | syl2anc 411 |
. . 3
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ
((๐
+Q ๐) <Q ๐ โ (๐ด +Q (๐ +Q
๐))
<Q (๐ด +Q ๐))) |
93 | 86, 92 | mpbid 147 |
. 2
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ (๐ด +Q
(๐
+Q ๐)) <Q (๐ด +Q
๐)) |
94 | 85, 93 | eqbrtrd 4037 |
1
โข (((๐ด = (๐ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ต = (๐ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ โ Q โง ๐ โ ฯ))) โ ๐ต <Q
(๐ด
+Q ๐)) |