Step | Hyp | Ref
| Expression |
1 | | nnaass 6485 |
. . . . . . . . . . . . . 14
โข ((๐ โ ฯ โง ๐ โ ฯ โง โ โ ฯ) โ ((๐ +o ๐) +o โ) = (๐ +o (๐ +o โ))) |
2 | 1 | adantl 277 |
. . . . . . . . . . . . 13
โข ((((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โง (๐ โ ฯ โง ๐ โ ฯ โง โ โ ฯ)) โ ((๐ +o ๐) +o โ) = (๐ +o (๐ +o โ))) |
3 | | simpr 110 |
. . . . . . . . . . . . . 14
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ ๐ฆ โ
ฯ) |
4 | | 1onn 6520 |
. . . . . . . . . . . . . 14
โข
1o โ ฯ |
5 | | nnacl 6480 |
. . . . . . . . . . . . . 14
โข ((๐ฆ โ ฯ โง
1o โ ฯ) โ (๐ฆ +o 1o) โ
ฯ) |
6 | 3, 4, 5 | sylancl 413 |
. . . . . . . . . . . . 13
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ (๐ฆ +o 1o)
โ ฯ) |
7 | | 2onn 6521 |
. . . . . . . . . . . . . 14
โข
2o โ ฯ |
8 | 7 | a1i 9 |
. . . . . . . . . . . . 13
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ
2o โ ฯ) |
9 | | simpll 527 |
. . . . . . . . . . . . 13
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ ๐ โ
ฯ) |
10 | 2, 6, 8, 9 | caovassd 6033 |
. . . . . . . . . . . 12
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ (((๐ฆ +o 1o)
+o 2o) +o ๐) = ((๐ฆ +o 1o) +o
(2o +o ๐))) |
11 | 4 | a1i 9 |
. . . . . . . . . . . . 13
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ
1o โ ฯ) |
12 | | nnacom 6484 |
. . . . . . . . . . . . . 14
โข ((๐ โ ฯ โง ๐ โ ฯ) โ (๐ +o ๐) = (๐ +o ๐)) |
13 | 12 | adantl 277 |
. . . . . . . . . . . . 13
โข ((((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โง (๐ โ ฯ โง ๐ โ ฯ)) โ (๐ +o ๐) = (๐ +o ๐)) |
14 | | nnacl 6480 |
. . . . . . . . . . . . . 14
โข ((๐ โ ฯ โง ๐ โ ฯ) โ (๐ +o ๐) โ
ฯ) |
15 | 14 | adantl 277 |
. . . . . . . . . . . . 13
โข ((((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โง (๐ โ ฯ โง ๐ โ ฯ)) โ (๐ +o ๐) โ
ฯ) |
16 | 3, 8, 11, 13, 2, 9, 15 | caov4d 6058 |
. . . . . . . . . . . 12
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ ((๐ฆ +o 2o)
+o (1o +o ๐)) = ((๐ฆ +o 1o) +o
(2o +o ๐))) |
17 | 13, 11, 9 | caovcomd 6030 |
. . . . . . . . . . . . . 14
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ
(1o +o ๐) = (๐ +o
1o)) |
18 | | nnon 4609 |
. . . . . . . . . . . . . . 15
โข (๐ โ ฯ โ ๐ โ On) |
19 | | oa1suc 6467 |
. . . . . . . . . . . . . . 15
โข (๐ โ On โ (๐ +o 1o) =
suc ๐) |
20 | 9, 18, 19 | 3syl 17 |
. . . . . . . . . . . . . 14
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ (๐ +o 1o) =
suc ๐) |
21 | 17, 20 | eqtrd 2210 |
. . . . . . . . . . . . 13
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ
(1o +o ๐) = suc ๐) |
22 | 21 | oveq2d 5890 |
. . . . . . . . . . . 12
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ ((๐ฆ +o 2o)
+o (1o +o ๐)) = ((๐ฆ +o 2o) +o
suc ๐)) |
23 | 10, 16, 22 | 3eqtr2rd 2217 |
. . . . . . . . . . 11
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ ((๐ฆ +o 2o)
+o suc ๐) =
(((๐ฆ +o
1o) +o 2o) +o ๐)) |
24 | 23 | opeq1d 3784 |
. . . . . . . . . 10
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ
โจ((๐ฆ +o
2o) +o suc ๐), 1oโฉ = โจ(((๐ฆ +o 1o)
+o 2o) +o ๐), 1oโฉ) |
25 | 24 | eceq1d 6570 |
. . . . . . . . 9
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ
[โจ((๐ฆ +o
2o) +o suc ๐), 1oโฉ]
~Q = [โจ(((๐ฆ +o 1o) +o
2o) +o ๐), 1oโฉ]
~Q ) |
26 | 25 | oveq1d 5889 |
. . . . . . . 8
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ
([โจ((๐ฆ +o
2o) +o suc ๐), 1oโฉ]
~Q ยทQ ๐) = ([โจ(((๐ฆ +o 1o)
+o 2o) +o ๐), 1oโฉ]
~Q ยทQ ๐)) |
27 | 26 | oveq2d 5890 |
. . . . . . 7
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ (๐ด +Q
([โจ((๐ฆ +o
2o) +o suc ๐), 1oโฉ]
~Q ยทQ ๐)) = (๐ด +Q
([โจ(((๐ฆ +o
1o) +o 2o) +o ๐), 1oโฉ]
~Q ยทQ ๐))) |
28 | 27 | eleq1d 2246 |
. . . . . 6
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ ((๐ด +Q
([โจ((๐ฆ +o
2o) +o suc ๐), 1oโฉ]
~Q ยทQ ๐)) โ ๐ โ (๐ด +Q
([โจ(((๐ฆ +o
1o) +o 2o) +o ๐), 1oโฉ]
~Q ยทQ ๐)) โ ๐)) |
29 | 28 | biimpd 144 |
. . . . 5
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ ((๐ด +Q
([โจ((๐ฆ +o
2o) +o suc ๐), 1oโฉ]
~Q ยทQ ๐)) โ ๐ โ (๐ด +Q
([โจ(((๐ฆ +o
1o) +o 2o) +o ๐), 1oโฉ]
~Q ยทQ ๐)) โ ๐)) |
30 | | simplr1 1039 |
. . . . . . . . . . . 12
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ
โจ๐ฟ, ๐โฉ โ
P) |
31 | | simplr2 1040 |
. . . . . . . . . . . 12
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ ๐ด โ ๐ฟ) |
32 | | elprnql 7479 |
. . . . . . . . . . . 12
โข
((โจ๐ฟ, ๐โฉ โ P
โง ๐ด โ ๐ฟ) โ ๐ด โ Q) |
33 | 30, 31, 32 | syl2anc 411 |
. . . . . . . . . . 11
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ ๐ด โ
Q) |
34 | | 1pi 7313 |
. . . . . . . . . . . . . 14
โข
1o โ N |
35 | | nnppipi 7341 |
. . . . . . . . . . . . . 14
โข ((๐ฆ โ ฯ โง
1o โ N) โ (๐ฆ +o 1o) โ
N) |
36 | 3, 34, 35 | sylancl 413 |
. . . . . . . . . . . . 13
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ (๐ฆ +o 1o)
โ N) |
37 | | opelxpi 4658 |
. . . . . . . . . . . . . 14
โข (((๐ฆ +o 1o)
โ N โง 1o โ N) โ
โจ(๐ฆ +o
1o), 1oโฉ โ (N ร
N)) |
38 | 34, 37 | mpan2 425 |
. . . . . . . . . . . . 13
โข ((๐ฆ +o 1o)
โ N โ โจ(๐ฆ +o 1o),
1oโฉ โ (N ร
N)) |
39 | | enqex 7358 |
. . . . . . . . . . . . . . 15
โข
~Q โ V |
40 | 39 | ecelqsi 6588 |
. . . . . . . . . . . . . 14
โข
(โจ(๐ฆ
+o 1o), 1oโฉ โ (N
ร N) โ [โจ(๐ฆ +o 1o),
1oโฉ] ~Q โ ((N
ร N) / ~Q
)) |
41 | | df-nqqs 7346 |
. . . . . . . . . . . . . 14
โข
Q = ((N ร N) /
~Q ) |
42 | 40, 41 | eleqtrrdi 2271 |
. . . . . . . . . . . . 13
โข
(โจ(๐ฆ
+o 1o), 1oโฉ โ (N
ร N) โ [โจ(๐ฆ +o 1o),
1oโฉ] ~Q โ
Q) |
43 | 36, 38, 42 | 3syl 17 |
. . . . . . . . . . . 12
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ
[โจ(๐ฆ +o
1o), 1oโฉ] ~Q โ
Q) |
44 | | simplr3 1041 |
. . . . . . . . . . . 12
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ ๐ โ
Q) |
45 | | mulclnq 7374 |
. . . . . . . . . . . 12
โข
(([โจ(๐ฆ
+o 1o), 1oโฉ] ~Q
โ Q โง ๐ โ Q) โ
([โจ(๐ฆ +o
1o), 1oโฉ] ~Q
ยทQ ๐) โ Q) |
46 | 43, 44, 45 | syl2anc 411 |
. . . . . . . . . . 11
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ
([โจ(๐ฆ +o
1o), 1oโฉ] ~Q
ยทQ ๐) โ Q) |
47 | | nqnq0a 7452 |
. . . . . . . . . . 11
โข ((๐ด โ Q โง
([โจ(๐ฆ +o
1o), 1oโฉ] ~Q
ยทQ ๐) โ Q) โ (๐ด +Q
([โจ(๐ฆ +o
1o), 1oโฉ] ~Q
ยทQ ๐)) = (๐ด +Q0 ([โจ(๐ฆ +o 1o),
1oโฉ] ~Q
ยทQ ๐))) |
48 | 33, 46, 47 | syl2anc 411 |
. . . . . . . . . 10
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ (๐ด +Q
([โจ(๐ฆ +o
1o), 1oโฉ] ~Q
ยทQ ๐)) = (๐ด +Q0 ([โจ(๐ฆ +o 1o),
1oโฉ] ~Q
ยทQ ๐))) |
49 | | nqnq0m 7453 |
. . . . . . . . . . . . 13
โข
(([โจ(๐ฆ
+o 1o), 1oโฉ] ~Q
โ Q โง ๐ โ Q) โ
([โจ(๐ฆ +o
1o), 1oโฉ] ~Q
ยทQ ๐) = ([โจ(๐ฆ +o 1o),
1oโฉ] ~Q
ยทQ0 ๐)) |
50 | 43, 44, 49 | syl2anc 411 |
. . . . . . . . . . . 12
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ
([โจ(๐ฆ +o
1o), 1oโฉ] ~Q
ยทQ ๐) = ([โจ(๐ฆ +o 1o),
1oโฉ] ~Q
ยทQ0 ๐)) |
51 | | nqnq0pi 7436 |
. . . . . . . . . . . . . 14
โข (((๐ฆ +o 1o)
โ N โง 1o โ N) โ
[โจ(๐ฆ +o
1o), 1oโฉ] ~Q0 =
[โจ(๐ฆ +o
1o), 1oโฉ] ~Q
) |
52 | 36, 34, 51 | sylancl 413 |
. . . . . . . . . . . . 13
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ
[โจ(๐ฆ +o
1o), 1oโฉ] ~Q0 =
[โจ(๐ฆ +o
1o), 1oโฉ] ~Q
) |
53 | 52 | oveq1d 5889 |
. . . . . . . . . . . 12
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ
([โจ(๐ฆ +o
1o), 1oโฉ] ~Q0
ยทQ0 ๐) = ([โจ(๐ฆ +o 1o),
1oโฉ] ~Q
ยทQ0 ๐)) |
54 | 50, 53 | eqtr4d 2213 |
. . . . . . . . . . 11
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ
([โจ(๐ฆ +o
1o), 1oโฉ] ~Q
ยทQ ๐) = ([โจ(๐ฆ +o 1o),
1oโฉ] ~Q0
ยทQ0 ๐)) |
55 | 54 | oveq2d 5890 |
. . . . . . . . . 10
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ (๐ด +Q0
([โจ(๐ฆ +o
1o), 1oโฉ] ~Q
ยทQ ๐)) = (๐ด +Q0 ([โจ(๐ฆ +o 1o),
1oโฉ] ~Q0
ยทQ0 ๐))) |
56 | 48, 55 | eqtrd 2210 |
. . . . . . . . 9
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ (๐ด +Q
([โจ(๐ฆ +o
1o), 1oโฉ] ~Q
ยทQ ๐)) = (๐ด +Q0 ([โจ(๐ฆ +o 1o),
1oโฉ] ~Q0
ยทQ0 ๐))) |
57 | 56 | eleq1d 2246 |
. . . . . . . 8
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ ((๐ด +Q
([โจ(๐ฆ +o
1o), 1oโฉ] ~Q
ยทQ ๐)) โ ๐ฟ โ (๐ด +Q0 ([โจ(๐ฆ +o 1o),
1oโฉ] ~Q0
ยทQ0 ๐)) โ ๐ฟ)) |
58 | 57 | anbi1d 465 |
. . . . . . 7
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ (((๐ด +Q
([โจ(๐ฆ +o
1o), 1oโฉ] ~Q
ยทQ ๐)) โ ๐ฟ โง (๐ด +Q
([โจ(((๐ฆ +o
1o) +o 2o) +o ๐), 1oโฉ]
~Q ยทQ ๐)) โ ๐) โ ((๐ด +Q0 ([โจ(๐ฆ +o 1o),
1oโฉ] ~Q0
ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q
([โจ(((๐ฆ +o
1o) +o 2o) +o ๐), 1oโฉ]
~Q ยทQ ๐)) โ ๐))) |
59 | | opeq1 3778 |
. . . . . . . . . . . . . . 15
โข (๐ง = (๐ฆ +o 1o) โ
โจ๐ง,
1oโฉ = โจ(๐ฆ +o 1o),
1oโฉ) |
60 | 59 | eceq1d 6570 |
. . . . . . . . . . . . . 14
โข (๐ง = (๐ฆ +o 1o) โ
[โจ๐ง,
1oโฉ] ~Q0 = [โจ(๐ฆ +o 1o),
1oโฉ] ~Q0 ) |
61 | 60 | oveq1d 5889 |
. . . . . . . . . . . . 13
โข (๐ง = (๐ฆ +o 1o) โ
([โจ๐ง,
1oโฉ] ~Q0
ยทQ0 ๐) = ([โจ(๐ฆ +o 1o),
1oโฉ] ~Q0
ยทQ0 ๐)) |
62 | 61 | oveq2d 5890 |
. . . . . . . . . . . 12
โข (๐ง = (๐ฆ +o 1o) โ (๐ด +Q0
([โจ๐ง,
1oโฉ] ~Q0
ยทQ0 ๐)) = (๐ด +Q0 ([โจ(๐ฆ +o 1o),
1oโฉ] ~Q0
ยทQ0 ๐))) |
63 | 62 | eleq1d 2246 |
. . . . . . . . . . 11
โข (๐ง = (๐ฆ +o 1o) โ ((๐ด +Q0
([โจ๐ง,
1oโฉ] ~Q0
ยทQ0 ๐)) โ ๐ฟ โ (๐ด +Q0 ([โจ(๐ฆ +o 1o),
1oโฉ] ~Q0
ยทQ0 ๐)) โ ๐ฟ)) |
64 | | oveq1 5881 |
. . . . . . . . . . . . . . . . 17
โข (๐ง = (๐ฆ +o 1o) โ (๐ง +o 2o) =
((๐ฆ +o
1o) +o 2o)) |
65 | 64 | oveq1d 5889 |
. . . . . . . . . . . . . . . 16
โข (๐ง = (๐ฆ +o 1o) โ ((๐ง +o 2o)
+o ๐) = (((๐ฆ +o 1o)
+o 2o) +o ๐)) |
66 | 65 | opeq1d 3784 |
. . . . . . . . . . . . . . 15
โข (๐ง = (๐ฆ +o 1o) โ
โจ((๐ง +o
2o) +o ๐), 1oโฉ = โจ(((๐ฆ +o 1o)
+o 2o) +o ๐), 1oโฉ) |
67 | 66 | eceq1d 6570 |
. . . . . . . . . . . . . 14
โข (๐ง = (๐ฆ +o 1o) โ
[โจ((๐ง +o
2o) +o ๐), 1oโฉ]
~Q = [โจ(((๐ฆ +o 1o) +o
2o) +o ๐), 1oโฉ]
~Q ) |
68 | 67 | oveq1d 5889 |
. . . . . . . . . . . . 13
โข (๐ง = (๐ฆ +o 1o) โ
([โจ((๐ง +o
2o) +o ๐), 1oโฉ]
~Q ยทQ ๐) = ([โจ(((๐ฆ +o 1o)
+o 2o) +o ๐), 1oโฉ]
~Q ยทQ ๐)) |
69 | 68 | oveq2d 5890 |
. . . . . . . . . . . 12
โข (๐ง = (๐ฆ +o 1o) โ (๐ด +Q
([โจ((๐ง +o
2o) +o ๐), 1oโฉ]
~Q ยทQ ๐)) = (๐ด +Q
([โจ(((๐ฆ +o
1o) +o 2o) +o ๐), 1oโฉ]
~Q ยทQ ๐))) |
70 | 69 | eleq1d 2246 |
. . . . . . . . . . 11
โข (๐ง = (๐ฆ +o 1o) โ ((๐ด +Q
([โจ((๐ง +o
2o) +o ๐), 1oโฉ]
~Q ยทQ ๐)) โ ๐ โ (๐ด +Q
([โจ(((๐ฆ +o
1o) +o 2o) +o ๐), 1oโฉ]
~Q ยทQ ๐)) โ ๐)) |
71 | 63, 70 | anbi12d 473 |
. . . . . . . . . 10
โข (๐ง = (๐ฆ +o 1o) โ (((๐ด +Q0
([โจ๐ง,
1oโฉ] ~Q0
ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q ([โจ((๐ง +o 2o)
+o ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐) โ ((๐ด +Q0 ([โจ(๐ฆ +o 1o),
1oโฉ] ~Q0
ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q
([โจ(((๐ฆ +o
1o) +o 2o) +o ๐), 1oโฉ]
~Q ยทQ ๐)) โ ๐))) |
72 | 71 | rspcev 2841 |
. . . . . . . . 9
โข (((๐ฆ +o 1o)
โ ฯ โง ((๐ด
+Q0 ([โจ(๐ฆ +o 1o),
1oโฉ] ~Q0
ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q
([โจ(((๐ฆ +o
1o) +o 2o) +o ๐), 1oโฉ]
~Q ยทQ ๐)) โ ๐)) โ โ๐ง โ ฯ ((๐ด +Q0 ([โจ๐ง, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q ([โจ((๐ง +o 2o)
+o ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐)) |
73 | 72 | ex 115 |
. . . . . . . 8
โข ((๐ฆ +o 1o)
โ ฯ โ (((๐ด
+Q0 ([โจ(๐ฆ +o 1o),
1oโฉ] ~Q0
ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q
([โจ(((๐ฆ +o
1o) +o 2o) +o ๐), 1oโฉ]
~Q ยทQ ๐)) โ ๐) โ โ๐ง โ ฯ ((๐ด +Q0 ([โจ๐ง, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q ([โจ((๐ง +o 2o)
+o ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))) |
74 | 6, 73 | syl 14 |
. . . . . . 7
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ (((๐ด +Q0
([โจ(๐ฆ +o
1o), 1oโฉ] ~Q0
ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q
([โจ(((๐ฆ +o
1o) +o 2o) +o ๐), 1oโฉ]
~Q ยทQ ๐)) โ ๐) โ โ๐ง โ ฯ ((๐ด +Q0 ([โจ๐ง, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q ([โจ((๐ง +o 2o)
+o ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))) |
75 | 58, 74 | sylbid 150 |
. . . . . 6
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ (((๐ด +Q
([โจ(๐ฆ +o
1o), 1oโฉ] ~Q
ยทQ ๐)) โ ๐ฟ โง (๐ด +Q
([โจ(((๐ฆ +o
1o) +o 2o) +o ๐), 1oโฉ]
~Q ยทQ ๐)) โ ๐) โ โ๐ง โ ฯ ((๐ด +Q0 ([โจ๐ง, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q ([โจ((๐ง +o 2o)
+o ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))) |
76 | | opeq1 3778 |
. . . . . . . . . . . 12
โข (๐ง = ๐ฆ โ โจ๐ง, 1oโฉ = โจ๐ฆ,
1oโฉ) |
77 | 76 | eceq1d 6570 |
. . . . . . . . . . 11
โข (๐ง = ๐ฆ โ [โจ๐ง, 1oโฉ]
~Q0 = [โจ๐ฆ, 1oโฉ]
~Q0 ) |
78 | 77 | oveq1d 5889 |
. . . . . . . . . 10
โข (๐ง = ๐ฆ โ ([โจ๐ง, 1oโฉ]
~Q0 ยทQ0 ๐) = ([โจ๐ฆ, 1oโฉ]
~Q0 ยทQ0 ๐)) |
79 | 78 | oveq2d 5890 |
. . . . . . . . 9
โข (๐ง = ๐ฆ โ (๐ด +Q0 ([โจ๐ง, 1oโฉ]
~Q0 ยทQ0 ๐)) = (๐ด +Q0 ([โจ๐ฆ, 1oโฉ]
~Q0 ยทQ0 ๐))) |
80 | 79 | eleq1d 2246 |
. . . . . . . 8
โข (๐ง = ๐ฆ โ ((๐ด +Q0 ([โจ๐ง, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โ (๐ด +Q0 ([โจ๐ฆ, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ)) |
81 | | oveq1 5881 |
. . . . . . . . . . . . . 14
โข (๐ง = ๐ฆ โ (๐ง +o 2o) = (๐ฆ +o
2o)) |
82 | 81 | oveq1d 5889 |
. . . . . . . . . . . . 13
โข (๐ง = ๐ฆ โ ((๐ง +o 2o) +o
๐) = ((๐ฆ +o 2o) +o
๐)) |
83 | 82 | opeq1d 3784 |
. . . . . . . . . . . 12
โข (๐ง = ๐ฆ โ โจ((๐ง +o 2o) +o
๐), 1oโฉ =
โจ((๐ฆ +o
2o) +o ๐), 1oโฉ) |
84 | 83 | eceq1d 6570 |
. . . . . . . . . . 11
โข (๐ง = ๐ฆ โ [โจ((๐ง +o 2o) +o
๐), 1oโฉ]
~Q = [โจ((๐ฆ +o 2o) +o
๐), 1oโฉ]
~Q ) |
85 | 84 | oveq1d 5889 |
. . . . . . . . . 10
โข (๐ง = ๐ฆ โ ([โจ((๐ง +o 2o) +o
๐), 1oโฉ]
~Q ยทQ ๐) = ([โจ((๐ฆ +o 2o) +o
๐), 1oโฉ]
~Q ยทQ ๐)) |
86 | 85 | oveq2d 5890 |
. . . . . . . . 9
โข (๐ง = ๐ฆ โ (๐ด +Q ([โจ((๐ง +o 2o)
+o ๐),
1oโฉ] ~Q
ยทQ ๐)) = (๐ด +Q ([โจ((๐ฆ +o 2o)
+o ๐),
1oโฉ] ~Q
ยทQ ๐))) |
87 | 86 | eleq1d 2246 |
. . . . . . . 8
โข (๐ง = ๐ฆ โ ((๐ด +Q ([โจ((๐ง +o 2o)
+o ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐ โ (๐ด +Q ([โจ((๐ฆ +o 2o)
+o ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐)) |
88 | 80, 87 | anbi12d 473 |
. . . . . . 7
โข (๐ง = ๐ฆ โ (((๐ด +Q0 ([โจ๐ง, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q ([โจ((๐ง +o 2o)
+o ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐) โ ((๐ด +Q0 ([โจ๐ฆ, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q ([โจ((๐ฆ +o 2o)
+o ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))) |
89 | 88 | cbvrexv 2704 |
. . . . . 6
โข
(โ๐ง โ
ฯ ((๐ด
+Q0 ([โจ๐ง, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q ([โจ((๐ง +o 2o)
+o ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐) โ โ๐ฆ โ ฯ ((๐ด +Q0 ([โจ๐ฆ, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q ([โจ((๐ฆ +o 2o)
+o ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐)) |
90 | 75, 89 | imbitrdi 161 |
. . . . 5
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ (((๐ด +Q
([โจ(๐ฆ +o
1o), 1oโฉ] ~Q
ยทQ ๐)) โ ๐ฟ โง (๐ด +Q
([โจ(((๐ฆ +o
1o) +o 2o) +o ๐), 1oโฉ]
~Q ยทQ ๐)) โ ๐) โ โ๐ฆ โ ฯ ((๐ด +Q0 ([โจ๐ฆ, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q ([โจ((๐ฆ +o 2o)
+o ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))) |
91 | 29, 90 | sylan2d 294 |
. . . 4
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ (((๐ด +Q
([โจ(๐ฆ +o
1o), 1oโฉ] ~Q
ยทQ ๐)) โ ๐ฟ โง (๐ด +Q ([โจ((๐ฆ +o 2o)
+o suc ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐) โ โ๐ฆ โ ฯ ((๐ด +Q0 ([โจ๐ฆ, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q ([โจ((๐ฆ +o 2o)
+o ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))) |
92 | 91 | expdimp 259 |
. . 3
โข ((((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โง (๐ด +Q
([โจ(๐ฆ +o
1o), 1oโฉ] ~Q
ยทQ ๐)) โ ๐ฟ) โ ((๐ด +Q ([โจ((๐ฆ +o 2o)
+o suc ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐ โ โ๐ฆ โ ฯ ((๐ด +Q0 ([โจ๐ฆ, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q ([โจ((๐ฆ +o 2o)
+o ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))) |
93 | 92 | adantld 278 |
. 2
โข ((((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โง (๐ด +Q
([โจ(๐ฆ +o
1o), 1oโฉ] ~Q
ยทQ ๐)) โ ๐ฟ) โ (((๐ด +Q0 ([โจ๐ฆ, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q ([โจ((๐ฆ +o 2o)
+o suc ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐) โ โ๐ฆ โ ฯ ((๐ด +Q0 ([โจ๐ฆ, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q ([โจ((๐ฆ +o 2o)
+o ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))) |
94 | 93 | ex 115 |
1
โข (((๐ โ ฯ โง
(โจ๐ฟ, ๐โฉ โ P โง ๐ด โ ๐ฟ โง ๐ โ Q)) โง ๐ฆ โ ฯ) โ ((๐ด +Q
([โจ(๐ฆ +o
1o), 1oโฉ] ~Q
ยทQ ๐)) โ ๐ฟ โ (((๐ด +Q0 ([โจ๐ฆ, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q ([โจ((๐ฆ +o 2o)
+o suc ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐) โ โ๐ฆ โ ฯ ((๐ด +Q0 ([โจ๐ฆ, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ด +Q ([โจ((๐ฆ +o 2o)
+o ๐),
1oโฉ] ~Q
ยทQ ๐)) โ ๐)))) |