Step | Hyp | Ref
| Expression |
1 | | caucvgsr.cau |
. 2
โข (๐ โ โ๐ โ N โ๐ โ N (๐ <N
๐ โ ((๐นโ๐) <R ((๐นโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) โง (๐นโ๐) <R ((๐นโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R )))) |
2 | | caucvgsr.f |
. . . . . . . . . . . 12
โข (๐ โ ๐น:NโถR) |
3 | | caucvgsrlembnd.bnd |
. . . . . . . . . . . 12
โข (๐ โ โ๐ โ N ๐ด <R (๐นโ๐)) |
4 | | caucvgsrlembnd.offset |
. . . . . . . . . . . 12
โข ๐บ = (๐ โ N โฆ (((๐นโ๐) +R
1R) +R (๐ด ยทR
-1R))) |
5 | 2, 1, 3, 4 | caucvgsrlemoffval 7797 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ N) โ ((๐บโ๐) +R ๐ด) = ((๐นโ๐) +R
1R)) |
6 | 5 | adantr 276 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
((๐บโ๐) +R
๐ด) = ((๐นโ๐) +R
1R)) |
7 | 6 | eqcomd 2183 |
. . . . . . . . 9
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
((๐นโ๐) +R
1R) = ((๐บโ๐) +R ๐ด)) |
8 | 2 | ad2antrr 488 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
๐น:NโถR) |
9 | | simpr 110 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
๐ โ
N) |
10 | 8, 9 | ffvelcdmd 5654 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
(๐นโ๐) โ R) |
11 | | simplr 528 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
๐ โ
N) |
12 | | recnnpr 7549 |
. . . . . . . . . . . 12
โข (๐ โ N โ
โจ{๐ โฃ ๐ <Q
(*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ โ
P) |
13 | | prsrcl 7785 |
. . . . . . . . . . . 12
โข
(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ โ P โ
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R โ R) |
14 | 11, 12, 13 | 3syl 17 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R โ R) |
15 | | 1sr 7752 |
. . . . . . . . . . . 12
โข
1R โ R |
16 | 15 | a1i 9 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
1R โ R) |
17 | | addcomsrg 7756 |
. . . . . . . . . . . 12
โข ((๐ โ R โง
๐ โ R)
โ (๐
+R ๐) = (๐ +R ๐)) |
18 | 17 | adantl 277 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ โ N) โง ๐ โ N) โง
(๐ โ R
โง ๐ โ
R)) โ (๐
+R ๐) = (๐ +R ๐)) |
19 | | addasssrg 7757 |
. . . . . . . . . . . 12
โข ((๐ โ R โง
๐ โ R
โง โ โ
R) โ ((๐
+R ๐) +R โ) = (๐ +R (๐ +R
โ))) |
20 | 19 | adantl 277 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ โ N) โง ๐ โ N) โง
(๐ โ R
โง ๐ โ
R โง โ
โ R)) โ ((๐ +R ๐) +R
โ) = (๐ +R (๐ +R
โ))) |
21 | 10, 14, 16, 18, 20 | caov32d 6057 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
(((๐นโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) +R
1R) = (((๐นโ๐) +R
1R) +R [โจ(โจ{๐ โฃ ๐ <Q
(*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R )) |
22 | 2, 1, 3, 4 | caucvgsrlemoffval 7797 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ N) โ ((๐บโ๐) +R ๐ด) = ((๐นโ๐) +R
1R)) |
23 | 22 | adantlr 477 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
((๐บโ๐) +R
๐ด) = ((๐นโ๐) +R
1R)) |
24 | 23 | oveq1d 5892 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
(((๐บโ๐) +R
๐ด)
+R [โจ(โจ{๐ โฃ ๐ <Q
(*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) = (((๐นโ๐) +R
1R) +R [โจ(โจ{๐ โฃ ๐ <Q
(*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R )) |
25 | 2, 1, 3, 4 | caucvgsrlemofff 7798 |
. . . . . . . . . . . . 13
โข (๐ โ ๐บ:NโถR) |
26 | 25 | ad2antrr 488 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
๐บ:NโถR) |
27 | 26, 9 | ffvelcdmd 5654 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
(๐บโ๐) โ R) |
28 | 3 | caucvgsrlemasr 7791 |
. . . . . . . . . . . 12
โข (๐ โ ๐ด โ R) |
29 | 28 | ad2antrr 488 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
๐ด โ
R) |
30 | 27, 29, 14, 18, 20 | caov32d 6057 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
(((๐บโ๐) +R
๐ด)
+R [โจ(โจ{๐ โฃ ๐ <Q
(*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) = (((๐บโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) +R ๐ด)) |
31 | 21, 24, 30 | 3eqtr2d 2216 |
. . . . . . . . 9
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
(((๐นโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) +R
1R) = (((๐บโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) +R ๐ด)) |
32 | 7, 31 | breq12d 4018 |
. . . . . . . 8
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
(((๐นโ๐) +R
1R) <R (((๐นโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) +R
1R) โ ((๐บโ๐) +R ๐ด) <R
(((๐บโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) +R ๐ด))) |
33 | | ltasrg 7771 |
. . . . . . . . . 10
โข ((๐ โ R โง
๐ โ R
โง โ โ
R) โ (๐
<R ๐ โ (โ +R ๐) <R
(โ
+R ๐))) |
34 | 33 | adantl 277 |
. . . . . . . . 9
โข ((((๐ โง ๐ โ N) โง ๐ โ N) โง
(๐ โ R
โง ๐ โ
R โง โ
โ R)) โ (๐ <R ๐ โ (โ +R ๐) <R
(โ
+R ๐))) |
35 | 8, 11 | ffvelcdmd 5654 |
. . . . . . . . 9
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
(๐นโ๐) โ R) |
36 | | addclsr 7754 |
. . . . . . . . . 10
โข (((๐นโ๐) โ R โง
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R โ R) โ ((๐นโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) โ R) |
37 | 10, 14, 36 | syl2anc 411 |
. . . . . . . . 9
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
((๐นโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) โ R) |
38 | 34, 35, 37, 16, 18 | caovord2d 6046 |
. . . . . . . 8
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
((๐นโ๐) <R
((๐นโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) โ ((๐นโ๐) +R
1R) <R (((๐นโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) +R
1R))) |
39 | 26, 11 | ffvelcdmd 5654 |
. . . . . . . . 9
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
(๐บโ๐) โ R) |
40 | | addclsr 7754 |
. . . . . . . . . 10
โข (((๐บโ๐) โ R โง
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R โ R) โ ((๐บโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) โ R) |
41 | 27, 14, 40 | syl2anc 411 |
. . . . . . . . 9
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
((๐บโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) โ R) |
42 | 34, 39, 41, 29, 18 | caovord2d 6046 |
. . . . . . . 8
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
((๐บโ๐) <R
((๐บโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) โ ((๐บโ๐) +R ๐ด) <R
(((๐บโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) +R ๐ด))) |
43 | 32, 38, 42 | 3bitr4d 220 |
. . . . . . 7
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
((๐นโ๐) <R
((๐นโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) โ (๐บโ๐) <R ((๐บโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ))) |
44 | 23 | eqcomd 2183 |
. . . . . . . . 9
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
((๐นโ๐) +R
1R) = ((๐บโ๐) +R ๐ด)) |
45 | 35, 14, 16, 18, 20 | caov32d 6057 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
(((๐นโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) +R
1R) = (((๐นโ๐) +R
1R) +R [โจ(โจ{๐ โฃ ๐ <Q
(*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R )) |
46 | 6 | oveq1d 5892 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
(((๐บโ๐) +R
๐ด)
+R [โจ(โจ{๐ โฃ ๐ <Q
(*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) = (((๐นโ๐) +R
1R) +R [โจ(โจ{๐ โฃ ๐ <Q
(*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R )) |
47 | 39, 29, 14, 18, 20 | caov32d 6057 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
(((๐บโ๐) +R
๐ด)
+R [โจ(โจ{๐ โฃ ๐ <Q
(*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) = (((๐บโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) +R ๐ด)) |
48 | 45, 46, 47 | 3eqtr2d 2216 |
. . . . . . . . 9
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
(((๐นโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) +R
1R) = (((๐บโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) +R ๐ด)) |
49 | 44, 48 | breq12d 4018 |
. . . . . . . 8
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
(((๐นโ๐) +R
1R) <R (((๐นโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) +R
1R) โ ((๐บโ๐) +R ๐ด) <R
(((๐บโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) +R ๐ด))) |
50 | | addclsr 7754 |
. . . . . . . . . 10
โข (((๐นโ๐) โ R โง
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R โ R) โ ((๐นโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) โ R) |
51 | 35, 14, 50 | syl2anc 411 |
. . . . . . . . 9
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
((๐นโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) โ R) |
52 | 34, 10, 51, 16, 18 | caovord2d 6046 |
. . . . . . . 8
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
((๐นโ๐) <R
((๐นโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) โ ((๐นโ๐) +R
1R) <R (((๐นโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) +R
1R))) |
53 | | addclsr 7754 |
. . . . . . . . . 10
โข (((๐บโ๐) โ R โง
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R โ R) โ ((๐บโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) โ R) |
54 | 39, 14, 53 | syl2anc 411 |
. . . . . . . . 9
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
((๐บโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) โ R) |
55 | 34, 27, 54, 29, 18 | caovord2d 6046 |
. . . . . . . 8
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
((๐บโ๐) <R
((๐บโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) โ ((๐บโ๐) +R ๐ด) <R
(((๐บโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) +R ๐ด))) |
56 | 49, 52, 55 | 3bitr4d 220 |
. . . . . . 7
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
((๐นโ๐) <R
((๐นโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) โ (๐บโ๐) <R ((๐บโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ))) |
57 | 43, 56 | anbi12d 473 |
. . . . . 6
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
(((๐นโ๐) <R
((๐นโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) โง (๐นโ๐) <R ((๐นโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R )) โ ((๐บโ๐) <R ((๐บโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) โง (๐บโ๐) <R ((๐บโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R )))) |
58 | 57 | biimpd 144 |
. . . . 5
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
(((๐นโ๐) <R
((๐นโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) โง (๐นโ๐) <R ((๐นโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R )) โ ((๐บโ๐) <R ((๐บโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) โง (๐บโ๐) <R ((๐บโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R )))) |
59 | 58 | imim2d 54 |
. . . 4
โข (((๐ โง ๐ โ N) โง ๐ โ N) โ
((๐
<N ๐ โ ((๐นโ๐) <R ((๐นโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) โง (๐นโ๐) <R ((๐นโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ))) โ (๐ <N ๐ โ ((๐บโ๐) <R ((๐บโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) โง (๐บโ๐) <R ((๐บโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ))))) |
60 | 59 | ralimdva 2544 |
. . 3
โข ((๐ โง ๐ โ N) โ
(โ๐ โ
N (๐
<N ๐ โ ((๐นโ๐) <R ((๐นโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) โง (๐นโ๐) <R ((๐นโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ))) โ โ๐ โ N (๐ <N ๐ โ ((๐บโ๐) <R ((๐บโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) โง (๐บโ๐) <R ((๐บโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ))))) |
61 | 60 | ralimdva 2544 |
. 2
โข (๐ โ (โ๐ โ N
โ๐ โ
N (๐
<N ๐ โ ((๐นโ๐) <R ((๐นโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) โง (๐นโ๐) <R ((๐นโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ))) โ โ๐ โ N โ๐ โ N (๐ <N
๐ โ ((๐บโ๐) <R ((๐บโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) โง (๐บโ๐) <R ((๐บโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ))))) |
62 | 1, 61 | mpd 13 |
1
โข (๐ โ โ๐ โ N โ๐ โ N (๐ <N
๐ โ ((๐บโ๐) <R ((๐บโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R ) โง (๐บโ๐) <R ((๐บโ๐) +R
[โจ(โจ{๐ โฃ
๐
<Q (*Qโ[โจ๐, 1oโฉ]
~Q )}, {๐ข โฃ
(*Qโ[โจ๐, 1oโฉ]
~Q ) <Q ๐ข}โฉ +P
1P), 1Pโฉ]
~R )))) |