Step | Hyp | Ref
| Expression |
1 | | prml 7475 |
. . . . . . 7
โข
(โจ๐ฟ, ๐โฉ โ P
โ โ๐ฅ โ
Q ๐ฅ โ
๐ฟ) |
2 | | df-rex 2461 |
. . . . . . 7
โข
(โ๐ฅ โ
Q ๐ฅ โ
๐ฟ โ โ๐ฅ(๐ฅ โ Q โง ๐ฅ โ ๐ฟ)) |
3 | 1, 2 | sylib 122 |
. . . . . 6
โข
(โจ๐ฟ, ๐โฉ โ P
โ โ๐ฅ(๐ฅ โ Q โง
๐ฅ โ ๐ฟ)) |
4 | 3 | adantr 276 |
. . . . 5
โข
((โจ๐ฟ, ๐โฉ โ P
โง ๐ โ
Q) โ โ๐ฅ(๐ฅ โ Q โง ๐ฅ โ ๐ฟ)) |
5 | | prmu 7476 |
. . . . . . 7
โข
(โจ๐ฟ, ๐โฉ โ P
โ โ๐ฆ โ
Q ๐ฆ โ
๐) |
6 | | df-rex 2461 |
. . . . . . 7
โข
(โ๐ฆ โ
Q ๐ฆ โ
๐ โ โ๐ฆ(๐ฆ โ Q โง ๐ฆ โ ๐)) |
7 | 5, 6 | sylib 122 |
. . . . . 6
โข
(โจ๐ฟ, ๐โฉ โ P
โ โ๐ฆ(๐ฆ โ Q โง
๐ฆ โ ๐)) |
8 | 7 | adantr 276 |
. . . . 5
โข
((โจ๐ฟ, ๐โฉ โ P
โง ๐ โ
Q) โ โ๐ฆ(๐ฆ โ Q โง ๐ฆ โ ๐)) |
9 | | subhalfnqq 7412 |
. . . . . . . . 9
โข (๐ โ Q โ
โ๐ โ
Q (๐
+Q ๐) <Q ๐) |
10 | 9 | adantl 277 |
. . . . . . . 8
โข
((โจ๐ฟ, ๐โฉ โ P
โง ๐ โ
Q) โ โ๐ โ Q (๐ +Q ๐) <Q
๐) |
11 | | df-rex 2461 |
. . . . . . . 8
โข
(โ๐ โ
Q (๐
+Q ๐) <Q ๐ โ โ๐(๐ โ Q โง (๐ +Q
๐)
<Q ๐)) |
12 | 10, 11 | sylib 122 |
. . . . . . 7
โข
((โจ๐ฟ, ๐โฉ โ P
โง ๐ โ
Q) โ โ๐(๐ โ Q โง (๐ +Q
๐)
<Q ๐)) |
13 | 12 | ancli 323 |
. . . . . 6
โข
((โจ๐ฟ, ๐โฉ โ P
โง ๐ โ
Q) โ ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
โ๐(๐ โ Q โง (๐ +Q
๐)
<Q ๐))) |
14 | | 19.42v 1906 |
. . . . . 6
โข
(โ๐((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐)) โ ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
โ๐(๐ โ Q โง (๐ +Q
๐)
<Q ๐))) |
15 | 13, 14 | sylibr 134 |
. . . . 5
โข
((โจ๐ฟ, ๐โฉ โ P
โง ๐ โ
Q) โ โ๐((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) |
16 | | eeeanv 1933 |
. . . . 5
โข
(โ๐ฅโ๐ฆโ๐((๐ฅ โ Q โง ๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โ (โ๐ฅ(๐ฅ โ Q โง ๐ฅ โ ๐ฟ) โง โ๐ฆ(๐ฆ โ Q โง ๐ฆ โ ๐) โง โ๐((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐)))) |
17 | 4, 8, 15, 16 | syl3anbrc 1181 |
. . . 4
โข
((โจ๐ฟ, ๐โฉ โ P
โง ๐ โ
Q) โ โ๐ฅโ๐ฆโ๐((๐ฅ โ Q โง ๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐)))) |
18 | | prarloclemarch2 7417 |
. . . . . . . . . . . . . 14
โข ((๐ฆ โ Q โง
๐ฅ โ Q
โง ๐ โ
Q) โ โ๐ โ N (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐)))) |
19 | | df-rex 2461 |
. . . . . . . . . . . . . 14
โข
(โ๐ โ
N (1o <N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐))) โ โ๐(๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐))))) |
20 | 18, 19 | sylib 122 |
. . . . . . . . . . . . 13
โข ((๐ฆ โ Q โง
๐ฅ โ Q
โง ๐ โ
Q) โ โ๐(๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐))))) |
21 | 20 | 3com12 1207 |
. . . . . . . . . . . 12
โข ((๐ฅ โ Q โง
๐ฆ โ Q
โง ๐ โ
Q) โ โ๐(๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐))))) |
22 | 21 | 3adant1r 1231 |
. . . . . . . . . . 11
โข (((๐ฅ โ Q โง
๐ฅ โ ๐ฟ) โง ๐ฆ โ Q โง ๐ โ Q) โ
โ๐(๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐))))) |
23 | 22 | 3adant2r 1233 |
. . . . . . . . . 10
โข (((๐ฅ โ Q โง
๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ๐ โ Q) โ โ๐(๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐))))) |
24 | 23 | 3adant3r 1235 |
. . . . . . . . 9
โข (((๐ฅ โ Q โง
๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง (๐ โ Q โง (๐ +Q
๐)
<Q ๐)) โ โ๐(๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐))))) |
25 | 24 | 3adant3l 1234 |
. . . . . . . 8
โข (((๐ฅ โ Q โง
๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โ โ๐(๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐))))) |
26 | 25 | ancli 323 |
. . . . . . 7
โข (((๐ฅ โ Q โง
๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โ (((๐ฅ โ Q โง ๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โง โ๐(๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐)))))) |
27 | | 19.42v 1906 |
. . . . . . 7
โข
(โ๐(((๐ฅ โ Q โง
๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โง (๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐))))) โ (((๐ฅ โ Q โง ๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โง โ๐(๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐)))))) |
28 | 26, 27 | sylibr 134 |
. . . . . 6
โข (((๐ฅ โ Q โง
๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โ โ๐(((๐ฅ โ Q โง ๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โง (๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐)))))) |
29 | 28 | 2eximi 1601 |
. . . . 5
โข
(โ๐ฆโ๐((๐ฅ โ Q โง ๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โ โ๐ฆโ๐โ๐(((๐ฅ โ Q โง ๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โง (๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐)))))) |
30 | 29 | eximi 1600 |
. . . 4
โข
(โ๐ฅโ๐ฆโ๐((๐ฅ โ Q โง ๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โ โ๐ฅโ๐ฆโ๐โ๐(((๐ฅ โ Q โง ๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โง (๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐)))))) |
31 | | simpl1l 1048 |
. . . . . . . . . 10
โข ((((๐ฅ โ Q โง
๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โง (๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐))))) โ ๐ฅ โ Q) |
32 | | simp3rl 1070 |
. . . . . . . . . . 11
โข (((๐ฅ โ Q โง
๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โ ๐ โ Q) |
33 | 32 | adantr 276 |
. . . . . . . . . 10
โข ((((๐ฅ โ Q โง
๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โง (๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐))))) โ ๐ โ Q) |
34 | | simp3rr 1071 |
. . . . . . . . . . 11
โข (((๐ฅ โ Q โง
๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โ (๐ +Q ๐) <Q
๐) |
35 | 34 | adantr 276 |
. . . . . . . . . 10
โข ((((๐ฅ โ Q โง
๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โง (๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐))))) โ (๐ +Q ๐) <Q
๐) |
36 | 31, 33, 35 | 3jca 1177 |
. . . . . . . . 9
โข ((((๐ฅ โ Q โง
๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โง (๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐))))) โ (๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐)) |
37 | | simp3ll 1068 |
. . . . . . . . . . . 12
โข (((๐ฅ โ Q โง
๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โ โจ๐ฟ, ๐โฉ โ
P) |
38 | 37 | adantr 276 |
. . . . . . . . . . 11
โข ((((๐ฅ โ Q โง
๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โง (๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐))))) โ โจ๐ฟ, ๐โฉ โ
P) |
39 | | simpl1r 1049 |
. . . . . . . . . . 11
โข ((((๐ฅ โ Q โง
๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โง (๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐))))) โ ๐ฅ โ ๐ฟ) |
40 | | simprl 529 |
. . . . . . . . . . 11
โข ((((๐ฅ โ Q โง
๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โง (๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐))))) โ ๐ โ N) |
41 | | simprrl 539 |
. . . . . . . . . . 11
โข ((((๐ฅ โ Q โง
๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โง (๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐))))) โ 1o
<N ๐) |
42 | | simprrr 540 |
. . . . . . . . . . . 12
โข ((((๐ฅ โ Q โง
๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โง (๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐))))) โ ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐))) |
43 | | simpl2r 1051 |
. . . . . . . . . . . . 13
โข ((((๐ฅ โ Q โง
๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โง (๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐))))) โ ๐ฆ โ ๐) |
44 | | prcunqu 7483 |
. . . . . . . . . . . . 13
โข
((โจ๐ฟ, ๐โฉ โ P
โง ๐ฆ โ ๐) โ (๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐)) โ (๐ฅ +Q ([โจ๐, 1oโฉ]
~Q ยทQ ๐)) โ ๐)) |
45 | 38, 43, 44 | syl2anc 411 |
. . . . . . . . . . . 12
โข ((((๐ฅ โ Q โง
๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โง (๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐))))) โ (๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐)) โ (๐ฅ +Q ([โจ๐, 1oโฉ]
~Q ยทQ ๐)) โ ๐)) |
46 | 42, 45 | mpd 13 |
. . . . . . . . . . 11
โข ((((๐ฅ โ Q โง
๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โง (๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐))))) โ (๐ฅ +Q ([โจ๐, 1oโฉ]
~Q ยทQ ๐)) โ ๐) |
47 | | prarloclem 7499 |
. . . . . . . . . . 11
โข
(((โจ๐ฟ, ๐โฉ โ P
โง ๐ฅ โ ๐ฟ) โง (๐ โ N โง ๐ โ Q โง
1o <N ๐) โง (๐ฅ +Q ([โจ๐, 1oโฉ]
~Q ยทQ ๐)) โ ๐) โ โ๐ โ ฯ ((๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐)) |
48 | 38, 39, 40, 33, 41, 46, 47 | syl231anc 1258 |
. . . . . . . . . 10
โข ((((๐ฅ โ Q โง
๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โง (๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐))))) โ โ๐ โ ฯ ((๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐)) |
49 | | df-rex 2461 |
. . . . . . . . . 10
โข
(โ๐ โ
ฯ ((๐ฅ
+Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐) โ โ๐(๐ โ ฯ โง ((๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))) |
50 | 48, 49 | sylib 122 |
. . . . . . . . 9
โข ((((๐ฅ โ Q โง
๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โง (๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐))))) โ โ๐(๐ โ ฯ โง ((๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))) |
51 | 36, 50 | jca 306 |
. . . . . . . 8
โข ((((๐ฅ โ Q โง
๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โง (๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐))))) โ ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง โ๐(๐ โ ฯ โง ((๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐)))) |
52 | | 19.42v 1906 |
. . . . . . . 8
โข
(โ๐((๐ฅ โ Q โง
๐ โ Q
โง (๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง ((๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))) โ ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง โ๐(๐ โ ฯ โง ((๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐)))) |
53 | 51, 52 | sylibr 134 |
. . . . . . 7
โข ((((๐ฅ โ Q โง
๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โง (๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐))))) โ โ๐((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง ((๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐)))) |
54 | | simprrl 539 |
. . . . . . . . . . . 12
โข (((๐ฅ โ Q โง
๐ โ Q
โง (๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง ((๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))) โ (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ) |
55 | | eleq1 2240 |
. . . . . . . . . . . . . . . . 17
โข (๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ (๐ โ ๐ฟ โ (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ)) |
56 | 55 | anbi1d 465 |
. . . . . . . . . . . . . . . 16
โข (๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ((๐ โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐) โ ((๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))) |
57 | 56 | anbi2d 464 |
. . . . . . . . . . . . . . 15
โข (๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ((๐ โ ฯ โง (๐ โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐)) โ (๐ โ ฯ โง ((๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐)))) |
58 | 57 | anbi2d 464 |
. . . . . . . . . . . . . 14
โข (๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ (((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))) โ ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง ((๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))))) |
59 | 58 | ceqsexgv 2866 |
. . . . . . . . . . . . 13
โข ((๐ฅ +Q0
([โจ๐,
1oโฉ] ~Q0
ยทQ0 ๐)) โ ๐ฟ โ (โ๐(๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐)))) โ ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง ((๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))))) |
60 | 59 | biimprcd 160 |
. . . . . . . . . . . 12
โข (((๐ฅ โ Q โง
๐ โ Q
โง (๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง ((๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))) โ ((๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โ โ๐(๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐)))))) |
61 | 54, 60 | mpd 13 |
. . . . . . . . . . 11
โข (((๐ฅ โ Q โง
๐ โ Q
โง (๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง ((๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))) โ โ๐(๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))))) |
62 | | simprrr 540 |
. . . . . . . . . . 11
โข (((๐ฅ โ Q โง
๐ โ Q
โง (๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง ((๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))) โ (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐) |
63 | | eleq1 2240 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ (๐ โ ๐ โ (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐)) |
64 | 63 | anbi2d 464 |
. . . . . . . . . . . . . . . . 17
โข (๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ((๐ โ ๐ฟ โง ๐ โ ๐) โ (๐ โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))) |
65 | 64 | anbi2d 464 |
. . . . . . . . . . . . . . . 16
โข (๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ((๐ โ ฯ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ (๐ โ ฯ โง (๐ โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐)))) |
66 | 65 | anbi2d 464 |
. . . . . . . . . . . . . . 15
โข (๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ (((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง ๐ โ ๐))) โ ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))))) |
67 | 66 | anbi2d 464 |
. . . . . . . . . . . . . 14
โข (๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ((๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง ๐ โ ๐)))) โ (๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐)))))) |
68 | 67 | exbidv 1825 |
. . . . . . . . . . . . 13
โข (๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ (โ๐(๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง ๐ โ ๐)))) โ โ๐(๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐)))))) |
69 | 68 | ceqsexgv 2866 |
. . . . . . . . . . . 12
โข ((๐ฅ +Q
([โจ(๐ +o
2o), 1oโฉ] ~Q
ยทQ ๐)) โ ๐ โ (โ๐(๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โง โ๐(๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง ๐ โ ๐))))) โ โ๐(๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐)))))) |
70 | 69 | biimprcd 160 |
. . . . . . . . . . 11
โข
(โ๐(๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐)))) โ ((๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐ โ โ๐(๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โง โ๐(๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง ๐ โ ๐))))))) |
71 | 61, 62, 70 | sylc 62 |
. . . . . . . . . 10
โข (((๐ฅ โ Q โง
๐ โ Q
โง (๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง ((๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))) โ โ๐(๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โง โ๐(๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง ๐ โ ๐)))))) |
72 | | 19.42v 1906 |
. . . . . . . . . . 11
โข
(โ๐(๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โง (๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง ๐ โ ๐))))) โ (๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โง โ๐(๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง ๐ โ ๐)))))) |
73 | 72 | exbii 1605 |
. . . . . . . . . 10
โข
(โ๐โ๐(๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โง (๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง ๐ โ ๐))))) โ โ๐(๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โง โ๐(๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง ๐ โ ๐)))))) |
74 | 71, 73 | sylibr 134 |
. . . . . . . . 9
โข (((๐ฅ โ Q โง
๐ โ Q
โง (๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง ((๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))) โ โ๐โ๐(๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โง (๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง ๐ โ ๐)))))) |
75 | | simprrl 539 |
. . . . . . . . . . . . . 14
โข (((๐ฅ โ Q โง
๐ โ Q
โง (๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง ๐ โ ๐))) โ ๐ โ ๐ฟ) |
76 | 75 | adantl 277 |
. . . . . . . . . . . . 13
โข (((๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง ๐ โ ๐)))) โ ๐ โ ๐ฟ) |
77 | | simprrr 540 |
. . . . . . . . . . . . . . 15
โข (((๐ฅ โ Q โง
๐ โ Q
โง (๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง ๐ โ ๐))) โ ๐ โ ๐) |
78 | 77 | adantl 277 |
. . . . . . . . . . . . . 14
โข (((๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง ๐ โ ๐)))) โ ๐ โ ๐) |
79 | | simpl 109 |
. . . . . . . . . . . . . . 15
โข (((๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง ๐ โ ๐)))) โ (๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)))) |
80 | | simprl2 1043 |
. . . . . . . . . . . . . . . 16
โข (((๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง ๐ โ ๐)))) โ ๐ โ Q) |
81 | | simprl3 1044 |
. . . . . . . . . . . . . . . 16
โข (((๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง ๐ โ ๐)))) โ (๐ +Q ๐) <Q
๐) |
82 | 80, 81 | jca 306 |
. . . . . . . . . . . . . . 15
โข (((๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง ๐ โ ๐)))) โ (๐ โ Q โง (๐ +Q
๐)
<Q ๐)) |
83 | | simprl1 1042 |
. . . . . . . . . . . . . . . 16
โข (((๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง ๐ โ ๐)))) โ ๐ฅ โ Q) |
84 | | simprrl 539 |
. . . . . . . . . . . . . . . 16
โข (((๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง ๐ โ ๐)))) โ ๐ โ ฯ) |
85 | 83, 84 | jca 306 |
. . . . . . . . . . . . . . 15
โข (((๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง ๐ โ ๐)))) โ (๐ฅ โ Q โง ๐ โ
ฯ)) |
86 | | prarloclemcalc 7500 |
. . . . . . . . . . . . . . 15
โข (((๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ โ Q โง (๐ +Q
๐)
<Q ๐) โง (๐ฅ โ Q โง ๐ โ ฯ))) โ ๐ <Q
(๐
+Q ๐)) |
87 | 79, 82, 85, 86 | syl12anc 1236 |
. . . . . . . . . . . . . 14
โข (((๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง ๐ โ ๐)))) โ ๐ <Q (๐ +Q
๐)) |
88 | 78, 87 | jca 306 |
. . . . . . . . . . . . 13
โข (((๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง ๐ โ ๐)))) โ (๐ โ ๐ โง ๐ <Q (๐ +Q
๐))) |
89 | 76, 88 | jca 306 |
. . . . . . . . . . . 12
โข (((๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐))) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง ๐ โ ๐)))) โ (๐ โ ๐ฟ โง (๐ โ ๐ โง ๐ <Q (๐ +Q
๐)))) |
90 | 89 | ancom1s 569 |
. . . . . . . . . . 11
โข (((๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โง ๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐))) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง ๐ โ ๐)))) โ (๐ โ ๐ฟ โง (๐ โ ๐ โง ๐ <Q (๐ +Q
๐)))) |
91 | 90 | anasss 399 |
. . . . . . . . . 10
โข ((๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โง (๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง ๐ โ ๐))))) โ (๐ โ ๐ฟ โง (๐ โ ๐ โง ๐ <Q (๐ +Q
๐)))) |
92 | 91 | 2eximi 1601 |
. . . . . . . . 9
โข
(โ๐โ๐(๐ = (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โง (๐ = (๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โง ((๐ฅ โ Q โง ๐ โ Q โง
(๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง (๐ โ ๐ฟ โง ๐ โ ๐))))) โ โ๐โ๐(๐ โ ๐ฟ โง (๐ โ ๐ โง ๐ <Q (๐ +Q
๐)))) |
93 | 74, 92 | syl 14 |
. . . . . . . 8
โข (((๐ฅ โ Q โง
๐ โ Q
โง (๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง ((๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))) โ โ๐โ๐(๐ โ ๐ฟ โง (๐ โ ๐ โง ๐ <Q (๐ +Q
๐)))) |
94 | 93 | exlimiv 1598 |
. . . . . . 7
โข
(โ๐((๐ฅ โ Q โง
๐ โ Q
โง (๐
+Q ๐) <Q ๐) โง (๐ โ ฯ โง ((๐ฅ +Q0 ([โจ๐, 1oโฉ]
~Q0 ยทQ0 ๐)) โ ๐ฟ โง (๐ฅ +Q ([โจ(๐ +o 2o),
1oโฉ] ~Q
ยทQ ๐)) โ ๐))) โ โ๐โ๐(๐ โ ๐ฟ โง (๐ โ ๐ โง ๐ <Q (๐ +Q
๐)))) |
95 | 53, 94 | syl 14 |
. . . . . 6
โข ((((๐ฅ โ Q โง
๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โง (๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐))))) โ โ๐โ๐(๐ โ ๐ฟ โง (๐ โ ๐ โง ๐ <Q (๐ +Q
๐)))) |
96 | 95 | exlimivv 1896 |
. . . . 5
โข
(โ๐โ๐(((๐ฅ โ Q โง ๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โง (๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐))))) โ โ๐โ๐(๐ โ ๐ฟ โง (๐ โ ๐ โง ๐ <Q (๐ +Q
๐)))) |
97 | 96 | exlimivv 1896 |
. . . 4
โข
(โ๐ฅโ๐ฆโ๐โ๐(((๐ฅ โ Q โง ๐ฅ โ ๐ฟ) โง (๐ฆ โ Q โง ๐ฆ โ ๐) โง ((โจ๐ฟ, ๐โฉ โ P โง ๐ โ Q) โง
(๐ โ Q
โง (๐
+Q ๐) <Q ๐))) โง (๐ โ N โง (1o
<N ๐ โง ๐ฆ <Q (๐ฅ +Q
([โจ๐,
1oโฉ] ~Q
ยทQ ๐))))) โ โ๐โ๐(๐ โ ๐ฟ โง (๐ โ ๐ โง ๐ <Q (๐ +Q
๐)))) |
98 | 17, 30, 97 | 3syl 17 |
. . 3
โข
((โจ๐ฟ, ๐โฉ โ P
โง ๐ โ
Q) โ โ๐โ๐(๐ โ ๐ฟ โง (๐ โ ๐ โง ๐ <Q (๐ +Q
๐)))) |
99 | | excom 1664 |
. . 3
โข
(โ๐โ๐(๐ โ ๐ฟ โง (๐ โ ๐ โง ๐ <Q (๐ +Q
๐))) โ โ๐โ๐(๐ โ ๐ฟ โง (๐ โ ๐ โง ๐ <Q (๐ +Q
๐)))) |
100 | 98, 99 | sylib 122 |
. 2
โข
((โจ๐ฟ, ๐โฉ โ P
โง ๐ โ
Q) โ โ๐โ๐(๐ โ ๐ฟ โง (๐ โ ๐ โง ๐ <Q (๐ +Q
๐)))) |
101 | | 19.42v 1906 |
. . . . 5
โข
(โ๐(๐ โ ๐ฟ โง (๐ โ ๐ โง ๐ <Q (๐ +Q
๐))) โ (๐ โ ๐ฟ โง โ๐(๐ โ ๐ โง ๐ <Q (๐ +Q
๐)))) |
102 | | df-rex 2461 |
. . . . . 6
โข
(โ๐ โ
๐ ๐ <Q (๐ +Q
๐) โ โ๐(๐ โ ๐ โง ๐ <Q (๐ +Q
๐))) |
103 | 102 | anbi2i 457 |
. . . . 5
โข ((๐ โ ๐ฟ โง โ๐ โ ๐ ๐ <Q (๐ +Q
๐)) โ (๐ โ ๐ฟ โง โ๐(๐ โ ๐ โง ๐ <Q (๐ +Q
๐)))) |
104 | 101, 103 | bitr4i 187 |
. . . 4
โข
(โ๐(๐ โ ๐ฟ โง (๐ โ ๐ โง ๐ <Q (๐ +Q
๐))) โ (๐ โ ๐ฟ โง โ๐ โ ๐ ๐ <Q (๐ +Q
๐))) |
105 | 104 | exbii 1605 |
. . 3
โข
(โ๐โ๐(๐ โ ๐ฟ โง (๐ โ ๐ โง ๐ <Q (๐ +Q
๐))) โ โ๐(๐ โ ๐ฟ โง โ๐ โ ๐ ๐ <Q (๐ +Q
๐))) |
106 | | df-rex 2461 |
. . 3
โข
(โ๐ โ
๐ฟ โ๐ โ ๐ ๐ <Q (๐ +Q
๐) โ โ๐(๐ โ ๐ฟ โง โ๐ โ ๐ ๐ <Q (๐ +Q
๐))) |
107 | 105, 106 | bitr4i 187 |
. 2
โข
(โ๐โ๐(๐ โ ๐ฟ โง (๐ โ ๐ โง ๐ <Q (๐ +Q
๐))) โ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ <Q (๐ +Q
๐)) |
108 | 100, 107 | sylib 122 |
1
โข
((โจ๐ฟ, ๐โฉ โ P
โง ๐ โ
Q) โ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ <Q (๐ +Q
๐)) |