Step | Hyp | Ref
| Expression |
1 | | lltropt 27605 |
. . . 4
โข ( L
โ๐ด) <<s ( R
โ๐ด) |
2 | | precsexlem.4 |
. . . . . . 7
โข (๐ โ ๐ด โ No
) |
3 | | precsexlem.5 |
. . . . . . 7
โข (๐ โ 0s <s ๐ด) |
4 | 2, 3 | 0elleft 27642 |
. . . . . 6
โข (๐ โ 0s โ ( L
โ๐ด)) |
5 | 4 | snssd 4812 |
. . . . 5
โข (๐ โ { 0s } โ
( L โ๐ด)) |
6 | | ssrab2 4077 |
. . . . . 6
โข {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ} โ ( L โ๐ด) |
7 | 6 | a1i 11 |
. . . . 5
โข (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โ ( L โ๐ด)) |
8 | 5, 7 | unssd 4186 |
. . . 4
โข (๐ โ ({ 0s } โช
{๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โ ( L
โ๐ด)) |
9 | | sssslt1 27534 |
. . . 4
โข ((( L
โ๐ด) <<s ( R
โ๐ด) โง ({
0s } โช {๐ฅ
โ ( L โ๐ด)
โฃ 0s <s ๐ฅ}) โ ( L โ๐ด)) โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) <<s ( R
โ๐ด)) |
10 | 1, 8, 9 | sylancr 586 |
. . 3
โข (๐ โ ({ 0s } โช
{๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) <<s ( R
โ๐ด)) |
11 | | precsexlem.1 |
. . . 4
โข ๐น = rec((๐ โ V โฆ
โฆ(1st โ๐) / ๐โฆโฆ(2nd
โ๐) / ๐โฆโจ(๐ โช ({๐ โฃ โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐ฟ โ ๐ ๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐
)}
โช {๐ โฃ
โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐
โ ๐ ๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐ฟ)})),
(๐ โช ({๐ โฃ โ๐ฅ๐ฟ โ
{๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐ฟ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐ฟ)}
โช {๐ โฃ
โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐
โ ๐ ๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐
)}))โฉ), โจ{
0s }, โ
โฉ) |
12 | | precsexlem.2 |
. . . 4
โข ๐ฟ = (1st โ ๐น) |
13 | | precsexlem.3 |
. . . 4
โข ๐
= (2nd โ ๐น) |
14 | | precsexlem.6 |
. . . 4
โข (๐ โ โ๐ฅ๐ โ (( L โ๐ด) โช ( R โ๐ด))( 0s <s ๐ฅ๐ โ
โ๐ฆ โ No (๐ฅ๐ ยทs
๐ฆ) = 1s
)) |
15 | 11, 12, 13, 2, 3, 14 | precsexlem10 27902 |
. . 3
โข (๐ โ โช (๐ฟ
โ ฯ) <<s โช (๐
โ ฯ)) |
16 | 2, 3 | cutpos 27659 |
. . 3
โข (๐ โ ๐ด = (({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) |s ( R โ๐ด))) |
17 | | precsexlem.7 |
. . . 4
โข ๐ = (โช
(๐ฟ โ ฯ) |s
โช (๐
โ ฯ)) |
18 | 17 | a1i 11 |
. . 3
โข (๐ โ ๐ = (โช (๐ฟ โ ฯ) |s โช (๐
โ ฯ))) |
19 | 10, 15, 16, 18 | mulsunif 27845 |
. 2
โข (๐ โ (๐ด ยทs ๐) = (({๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐
โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))}) |s ({๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))}))) |
20 | | 0sno 27565 |
. . . . . . . . 9
โข
0s โ No |
21 | 20 | elexi 3493 |
. . . . . . . 8
โข
0s โ V |
22 | 21 | snid 4664 |
. . . . . . 7
โข
0s โ { 0s } |
23 | | elun1 4176 |
. . . . . . 7
โข (
0s โ { 0s } โ 0s โ ({
0s } โช {๐ฅ
โ ( L โ๐ด)
โฃ 0s <s ๐ฅ})) |
24 | 22, 23 | ax-mp 5 |
. . . . . 6
โข
0s โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) |
25 | | peano1 7883 |
. . . . . . . . 9
โข โ
โ ฯ |
26 | 11, 12, 13 | precsexlem1 27893 |
. . . . . . . . . 10
โข (๐ฟโโ
) = {
0s } |
27 | 22, 26 | eleqtrri 2831 |
. . . . . . . . 9
โข
0s โ (๐ฟโโ
) |
28 | | fveq2 6891 |
. . . . . . . . . . 11
โข (๐ = โ
โ (๐ฟโ๐) = (๐ฟโโ
)) |
29 | 28 | eleq2d 2818 |
. . . . . . . . . 10
โข (๐ = โ
โ (
0s โ (๐ฟโ๐) โ 0s โ (๐ฟโโ
))) |
30 | 29 | rspcev 3612 |
. . . . . . . . 9
โข ((โ
โ ฯ โง 0s โ (๐ฟโโ
)) โ โ๐ โ ฯ 0s
โ (๐ฟโ๐)) |
31 | 25, 27, 30 | mp2an 689 |
. . . . . . . 8
โข
โ๐ โ
ฯ 0s โ (๐ฟโ๐) |
32 | | eliun 5001 |
. . . . . . . 8
โข (
0s โ โช ๐ โ ฯ (๐ฟโ๐) โ โ๐ โ ฯ 0s โ (๐ฟโ๐)) |
33 | 31, 32 | mpbir 230 |
. . . . . . 7
โข
0s โ โช ๐ โ ฯ (๐ฟโ๐) |
34 | | fo1st 7999 |
. . . . . . . . . . 11
โข
1st :VโontoโV |
35 | | fofun 6806 |
. . . . . . . . . . 11
โข
(1st :VโontoโV โ Fun 1st ) |
36 | 34, 35 | ax-mp 5 |
. . . . . . . . . 10
โข Fun
1st |
37 | | rdgfun 8420 |
. . . . . . . . . . 11
โข Fun
rec((๐ โ V โฆ
โฆ(1st โ๐) / ๐โฆโฆ(2nd
โ๐) / ๐โฆโจ(๐ โช ({๐ โฃ โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐ฟ โ ๐ ๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐
)}
โช {๐ โฃ
โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐
โ ๐ ๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐ฟ)})),
(๐ โช ({๐ โฃ โ๐ฅ๐ฟ โ
{๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐ฟ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐ฟ)}
โช {๐ โฃ
โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐
โ ๐ ๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐
)}))โฉ), โจ{
0s }, โ
โฉ) |
38 | 11 | funeqi 6569 |
. . . . . . . . . . 11
โข (Fun
๐น โ Fun rec((๐ โ V โฆ
โฆ(1st โ๐) / ๐โฆโฆ(2nd
โ๐) / ๐โฆโจ(๐ โช ({๐ โฃ โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐ฟ โ ๐ ๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐
)}
โช {๐ โฃ
โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐
โ ๐ ๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐ฟ)})),
(๐ โช ({๐ โฃ โ๐ฅ๐ฟ โ
{๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐ฟ โ ๐ ๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐ฟ)}
โช {๐ โฃ
โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐
โ ๐ ๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐
)}))โฉ), โจ{
0s }, โ
โฉ)) |
39 | 37, 38 | mpbir 230 |
. . . . . . . . . 10
โข Fun ๐น |
40 | | funco 6588 |
. . . . . . . . . 10
โข ((Fun
1st โง Fun ๐น)
โ Fun (1st โ ๐น)) |
41 | 36, 39, 40 | mp2an 689 |
. . . . . . . . 9
โข Fun
(1st โ ๐น) |
42 | 12 | funeqi 6569 |
. . . . . . . . 9
โข (Fun
๐ฟ โ Fun
(1st โ ๐น)) |
43 | 41, 42 | mpbir 230 |
. . . . . . . 8
โข Fun ๐ฟ |
44 | | funiunfv 7250 |
. . . . . . . 8
โข (Fun
๐ฟ โ โช ๐ โ ฯ (๐ฟโ๐) = โช (๐ฟ โ
ฯ)) |
45 | 43, 44 | ax-mp 5 |
. . . . . . 7
โข โช ๐ โ ฯ (๐ฟโ๐) = โช (๐ฟ โ
ฯ) |
46 | 33, 45 | eleqtri 2830 |
. . . . . 6
โข
0s โ โช (๐ฟ โ ฯ) |
47 | | addsrid 27687 |
. . . . . . . . . 10
โข (
0s โ No โ ( 0s
+s 0s ) = 0s ) |
48 | 20, 47 | ax-mp 5 |
. . . . . . . . 9
โข (
0s +s 0s ) = 0s |
49 | | muls01 27808 |
. . . . . . . . . 10
โข (
0s โ No โ ( 0s
ยทs 0s ) = 0s ) |
50 | 20, 49 | ax-mp 5 |
. . . . . . . . 9
โข (
0s ยทs 0s ) =
0s |
51 | 48, 50 | oveq12i 7424 |
. . . . . . . 8
โข ((
0s +s 0s ) -s ( 0s
ยทs 0s )) = ( 0s -s
0s ) |
52 | | subsid 27777 |
. . . . . . . . 9
โข (
0s โ No โ ( 0s
-s 0s ) = 0s ) |
53 | 20, 52 | ax-mp 5 |
. . . . . . . 8
โข (
0s -s 0s ) = 0s |
54 | 51, 53 | eqtr2i 2760 |
. . . . . . 7
โข
0s = (( 0s +s 0s ) -s (
0s ยทs 0s )) |
55 | 15 | scutcld 27542 |
. . . . . . . . . . 11
โข (๐ โ (โช (๐ฟ
โ ฯ) |s โช (๐
โ ฯ)) โ No ) |
56 | 17, 55 | eqeltrid 2836 |
. . . . . . . . . 10
โข (๐ โ ๐ โ No
) |
57 | | muls02 27837 |
. . . . . . . . . 10
โข (๐ โ
No โ ( 0s ยทs ๐) = 0s ) |
58 | 56, 57 | syl 17 |
. . . . . . . . 9
โข (๐ โ ( 0s
ยทs ๐) =
0s ) |
59 | | muls01 27808 |
. . . . . . . . . 10
โข (๐ด โ
No โ (๐ด
ยทs 0s ) = 0s ) |
60 | 2, 59 | syl 17 |
. . . . . . . . 9
โข (๐ โ (๐ด ยทs 0s ) =
0s ) |
61 | 58, 60 | oveq12d 7430 |
. . . . . . . 8
โข (๐ โ (( 0s
ยทs ๐)
+s (๐ด
ยทs 0s )) = ( 0s +s
0s )) |
62 | 61 | oveq1d 7427 |
. . . . . . 7
โข (๐ โ ((( 0s
ยทs ๐)
+s (๐ด
ยทs 0s )) -s ( 0s
ยทs 0s )) = (( 0s +s
0s ) -s ( 0s ยทs
0s ))) |
63 | 54, 62 | eqtr4id 2790 |
. . . . . 6
โข (๐ โ 0s = (((
0s ยทs ๐) +s (๐ด ยทs 0s ))
-s ( 0s ยทs 0s
))) |
64 | | oveq1 7419 |
. . . . . . . . . 10
โข (๐ = 0s โ (๐ ยทs ๐) = ( 0s
ยทs ๐)) |
65 | 64 | oveq1d 7427 |
. . . . . . . . 9
โข (๐ = 0s โ ((๐ ยทs ๐) +s (๐ด ยทs ๐)) = (( 0s
ยทs ๐)
+s (๐ด
ยทs ๐))) |
66 | | oveq1 7419 |
. . . . . . . . 9
โข (๐ = 0s โ (๐ ยทs ๐) = ( 0s
ยทs ๐)) |
67 | 65, 66 | oveq12d 7430 |
. . . . . . . 8
โข (๐ = 0s โ (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) = ((( 0s
ยทs ๐)
+s (๐ด
ยทs ๐))
-s ( 0s ยทs ๐))) |
68 | 67 | eqeq2d 2742 |
. . . . . . 7
โข (๐ = 0s โ (
0s = (((๐
ยทs ๐)
+s (๐ด
ยทs ๐))
-s (๐
ยทs ๐))
โ 0s = ((( 0s ยทs ๐) +s (๐ด ยทs ๐)) -s ( 0s
ยทs ๐)))) |
69 | | oveq2 7420 |
. . . . . . . . . 10
โข (๐ = 0s โ (๐ด ยทs ๐) = (๐ด ยทs 0s
)) |
70 | 69 | oveq2d 7428 |
. . . . . . . . 9
โข (๐ = 0s โ ((
0s ยทs ๐) +s (๐ด ยทs ๐)) = (( 0s ยทs
๐) +s (๐ด ยทs
0s ))) |
71 | | oveq2 7420 |
. . . . . . . . 9
โข (๐ = 0s โ (
0s ยทs ๐) = ( 0s ยทs
0s )) |
72 | 70, 71 | oveq12d 7430 |
. . . . . . . 8
โข (๐ = 0s โ (((
0s ยทs ๐) +s (๐ด ยทs ๐)) -s ( 0s
ยทs ๐)) =
((( 0s ยทs ๐) +s (๐ด ยทs 0s ))
-s ( 0s ยทs 0s
))) |
73 | 72 | eqeq2d 2742 |
. . . . . . 7
โข (๐ = 0s โ (
0s = ((( 0s ยทs ๐) +s (๐ด ยทs ๐)) -s ( 0s
ยทs ๐))
โ 0s = ((( 0s ยทs ๐) +s (๐ด ยทs 0s ))
-s ( 0s ยทs 0s
)))) |
74 | 68, 73 | rspc2ev 3624 |
. . . . . 6
โข ((
0s โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โง 0s โ
โช (๐ฟ โ ฯ) โง 0s = (((
0s ยทs ๐) +s (๐ด ยทs 0s ))
-s ( 0s ยทs 0s ))) โ
โ๐ โ ({
0s } โช {๐ฅ
โ ( L โ๐ด)
โฃ 0s <s ๐ฅ})โ๐ โ โช (๐ฟ โ ฯ) 0s
= (((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) |
75 | 24, 46, 63, 74 | mp3an12i 1464 |
. . . . 5
โข (๐ โ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ) 0s = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) |
76 | | eqeq1 2735 |
. . . . . . 7
โข (๐ = 0s โ (๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ 0s = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)))) |
77 | 76 | 2rexbidv 3218 |
. . . . . 6
โข (๐ = 0s โ
(โ๐ โ ({
0s } โช {๐ฅ
โ ( L โ๐ด)
โฃ 0s <s ๐ฅ})โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ) 0s = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)))) |
78 | 21, 77 | elab 3668 |
. . . . 5
โข (
0s โ {๐
โฃ โ๐ โ ({
0s } โช {๐ฅ
โ ( L โ๐ด)
โฃ 0s <s ๐ฅ})โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ) 0s = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) |
79 | 75, 78 | sylibr 233 |
. . . 4
โข (๐ โ 0s โ
{๐ โฃ โ๐ โ ({ 0s } โช
{๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))}) |
80 | | elun1 4176 |
. . . 4
โข (
0s โ {๐
โฃ โ๐ โ ({
0s } โช {๐ฅ
โ ( L โ๐ด)
โฃ 0s <s ๐ฅ})โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โ 0s โ ({๐ โฃ โ๐ โ ({ 0s } โช
{๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐
โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))})) |
81 | 79, 80 | syl 17 |
. . 3
โข (๐ โ 0s โ
({๐ โฃ โ๐ โ ({ 0s } โช
{๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐
โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))})) |
82 | | eqid 2731 |
. . . . . . 7
โข (๐ โ ({ 0s } โช
{๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}), ๐ โ โช (๐ฟ โ ฯ) โฆ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) = (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}), ๐ โ โช (๐ฟ โ ฯ) โฆ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) |
83 | 82 | rnmpo 7545 |
. . . . . 6
โข ran
(๐ โ ({ 0s
} โช {๐ฅ โ ( L
โ๐ด) โฃ
0s <s ๐ฅ}),
๐ โ โช (๐ฟ
โ ฯ) โฆ (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) = {๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} |
84 | | ssltex1 27525 |
. . . . . . . . 9
โข (({
0s } โช {๐ฅ
โ ( L โ๐ด)
โฃ 0s <s ๐ฅ}) <<s ( R โ๐ด) โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โ
V) |
85 | 10, 84 | syl 17 |
. . . . . . . 8
โข (๐ โ ({ 0s } โช
{๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โ
V) |
86 | | ssltex1 27525 |
. . . . . . . . 9
โข (โช (๐ฟ
โ ฯ) <<s โช (๐
โ ฯ) โ โช (๐ฟ
โ ฯ) โ V) |
87 | 15, 86 | syl 17 |
. . . . . . . 8
โข (๐ โ โช (๐ฟ
โ ฯ) โ V) |
88 | | mpoexga 8068 |
. . . . . . . 8
โข ((({
0s } โช {๐ฅ
โ ( L โ๐ด)
โฃ 0s <s ๐ฅ}) โ V โง โช (๐ฟ
โ ฯ) โ V) โ (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}), ๐ โ โช (๐ฟ โ ฯ) โฆ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) โ V) |
89 | 85, 87, 88 | syl2anc 583 |
. . . . . . 7
โข (๐ โ (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}), ๐ โ โช (๐ฟ โ ฯ) โฆ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) โ V) |
90 | | rnexg 7899 |
. . . . . . 7
โข ((๐ โ ({ 0s } โช
{๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}), ๐ โ โช (๐ฟ โ ฯ) โฆ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) โ V โ ran (๐ โ ({ 0s } โช
{๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}), ๐ โ โช (๐ฟ โ ฯ) โฆ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) โ V) |
91 | 89, 90 | syl 17 |
. . . . . 6
โข (๐ โ ran (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}), ๐ โ โช (๐ฟ โ ฯ) โฆ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) โ V) |
92 | 83, 91 | eqeltrrid 2837 |
. . . . 5
โข (๐ โ {๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โ V) |
93 | | eqid 2731 |
. . . . . . 7
โข (๐ โ ( R โ๐ด), ๐ โ โช (๐
โ ฯ) โฆ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) = (๐ โ ( R โ๐ด), ๐ โ โช (๐
โ ฯ) โฆ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) |
94 | 93 | rnmpo 7545 |
. . . . . 6
โข ran
(๐ โ ( R โ๐ด), ๐ โ โช (๐
โ ฯ) โฆ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) = {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐
โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} |
95 | | fvex 6904 |
. . . . . . . 8
โข ( R
โ๐ด) โ
V |
96 | | ssltex2 27526 |
. . . . . . . . 9
โข (โช (๐ฟ
โ ฯ) <<s โช (๐
โ ฯ) โ โช (๐
โ ฯ) โ V) |
97 | 15, 96 | syl 17 |
. . . . . . . 8
โข (๐ โ โช (๐
โ ฯ) โ V) |
98 | | mpoexga 8068 |
. . . . . . . 8
โข ((( R
โ๐ด) โ V โง
โช (๐
โ ฯ) โ V) โ (๐ โ ( R โ๐ด), ๐ โ โช (๐
โ ฯ) โฆ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) โ V) |
99 | 95, 97, 98 | sylancr 586 |
. . . . . . 7
โข (๐ โ (๐ โ ( R โ๐ด), ๐ โ โช (๐
โ ฯ) โฆ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) โ V) |
100 | | rnexg 7899 |
. . . . . . 7
โข ((๐ โ ( R โ๐ด), ๐ โ โช (๐
โ ฯ) โฆ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) โ V โ ran (๐ โ ( R โ๐ด), ๐ โ โช (๐
โ ฯ) โฆ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) โ V) |
101 | 99, 100 | syl 17 |
. . . . . 6
โข (๐ โ ran (๐ โ ( R โ๐ด), ๐ โ โช (๐
โ ฯ) โฆ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) โ V) |
102 | 94, 101 | eqeltrrid 2837 |
. . . . 5
โข (๐ โ {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐
โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โ V) |
103 | 92, 102 | unexd 7745 |
. . . 4
โข (๐ โ ({๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐
โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))}) โ V) |
104 | | snex 5431 |
. . . . 5
โข {
1s } โ V |
105 | 104 | a1i 11 |
. . . 4
โข (๐ โ { 1s } โ
V) |
106 | | ssltss1 27527 |
. . . . . . . . . . . . . 14
โข (({
0s } โช {๐ฅ
โ ( L โ๐ด)
โฃ 0s <s ๐ฅ}) <<s ( R โ๐ด) โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โ No ) |
107 | 10, 106 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ ({ 0s } โช
{๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โ No ) |
108 | 107 | sselda 3982 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})) โ ๐ โ
No ) |
109 | 108 | adantrr 714 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โง ๐ โ โช (๐ฟ
โ ฯ))) โ ๐
โ No ) |
110 | 56 | adantr 480 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โง ๐ โ โช (๐ฟ
โ ฯ))) โ ๐
โ No ) |
111 | 109, 110 | mulscld 27831 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โง ๐ โ โช (๐ฟ
โ ฯ))) โ (๐ ยทs ๐) โ No
) |
112 | 2 | adantr 480 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โง ๐ โ โช (๐ฟ
โ ฯ))) โ ๐ด
โ No ) |
113 | | ssltss1 27527 |
. . . . . . . . . . . . . 14
โข (โช (๐ฟ
โ ฯ) <<s โช (๐
โ ฯ) โ โช (๐ฟ
โ ฯ) โ No ) |
114 | 15, 113 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ โช (๐ฟ
โ ฯ) โ No ) |
115 | 114 | sselda 3982 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ โช (๐ฟ โ ฯ)) โ ๐ โ
No ) |
116 | 115 | adantrl 713 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โง ๐ โ โช (๐ฟ
โ ฯ))) โ ๐
โ No ) |
117 | 112, 116 | mulscld 27831 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โง ๐ โ โช (๐ฟ
โ ฯ))) โ (๐ด ยทs ๐) โ No
) |
118 | 111, 117 | addscld 27703 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โง ๐ โ โช (๐ฟ
โ ฯ))) โ ((๐ ยทs ๐) +s (๐ด ยทs ๐)) โ No
) |
119 | 109, 116 | mulscld 27831 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โง ๐ โ โช (๐ฟ
โ ฯ))) โ (๐ ยทs ๐) โ No
) |
120 | 118, 119 | subscld 27775 |
. . . . . . . 8
โข ((๐ โง (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โง ๐ โ โช (๐ฟ
โ ฯ))) โ (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ No
) |
121 | | eleq1 2820 |
. . . . . . . 8
โข (๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ (๐ โ No
โ (((๐
ยทs ๐)
+s (๐ด
ยทs ๐))
-s (๐
ยทs ๐))
โ No )) |
122 | 120, 121 | syl5ibrcom 246 |
. . . . . . 7
โข ((๐ โง (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โง ๐ โ โช (๐ฟ
โ ฯ))) โ (๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ ๐ โ No
)) |
123 | 122 | rexlimdvva 3210 |
. . . . . 6
โข (๐ โ (โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ ๐ โ No
)) |
124 | 123 | abssdv 4065 |
. . . . 5
โข (๐ โ {๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โ No ) |
125 | | rightssno 27614 |
. . . . . . . . . . . . . 14
โข ( R
โ๐ด) โ No |
126 | 125 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ ( R โ๐ด) โ
No ) |
127 | 126 | sselda 3982 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ( R โ๐ด)) โ ๐ โ No
) |
128 | 127 | adantrr 714 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ ๐ โ
No ) |
129 | 56 | adantr 480 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ ๐ โ
No ) |
130 | 128, 129 | mulscld 27831 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ
(๐ ยทs
๐) โ No ) |
131 | 2 | adantr 480 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ ๐ด โ
No ) |
132 | | ssltss2 27528 |
. . . . . . . . . . . . . 14
โข (โช (๐ฟ
โ ฯ) <<s โช (๐
โ ฯ) โ โช (๐
โ ฯ) โ No ) |
133 | 15, 132 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ โช (๐
โ ฯ) โ No ) |
134 | 133 | sselda 3982 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ โช (๐
โ ฯ)) โ ๐ โ
No ) |
135 | 134 | adantrl 713 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ ๐ โ
No ) |
136 | 131, 135 | mulscld 27831 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ
(๐ด ยทs
๐) โ No ) |
137 | 130, 136 | addscld 27703 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ
((๐ ยทs
๐) +s (๐ด ยทs ๐)) โ
No ) |
138 | 128, 135 | mulscld 27831 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ
(๐ ยทs
๐) โ No ) |
139 | 137, 138 | subscld 27775 |
. . . . . . . 8
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ
No ) |
140 | 139, 121 | syl5ibrcom 246 |
. . . . . . 7
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ
(๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ ๐ โ No
)) |
141 | 140 | rexlimdvva 3210 |
. . . . . 6
โข (๐ โ (โ๐ โ ( R โ๐ด)โ๐ โ โช (๐
โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ ๐ โ No
)) |
142 | 141 | abssdv 4065 |
. . . . 5
โข (๐ โ {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐
โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โ No
) |
143 | 124, 142 | unssd 4186 |
. . . 4
โข (๐ โ ({๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐
โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))}) โ No
) |
144 | | 1sno 27566 |
. . . . 5
โข
1s โ No |
145 | | snssi 4811 |
. . . . 5
โข (
1s โ No โ { 1s }
โ No ) |
146 | 144, 145 | mp1i 13 |
. . . 4
โข (๐ โ { 1s } โ
No ) |
147 | | elun 4148 |
. . . . . . . . 9
โข (๐ โ ({๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐
โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))}) โ (๐ โ {๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โจ ๐ โ {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐
โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))})) |
148 | | vex 3477 |
. . . . . . . . . . 11
โข ๐ โ V |
149 | | eqeq1 2735 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ ๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)))) |
150 | 149 | 2rexbidv 3218 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ โ๐ โ ({ 0s } โช
{๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)))) |
151 | 148, 150 | elab 3668 |
. . . . . . . . . 10
โข (๐ โ {๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โ โ๐ โ ({ 0s } โช
{๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) |
152 | 149 | 2rexbidv 3218 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (โ๐ โ ( R โ๐ด)โ๐ โ โช (๐
โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐
โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)))) |
153 | 148, 152 | elab 3668 |
. . . . . . . . . 10
โข (๐ โ {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐
โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐
โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) |
154 | 151, 153 | orbi12i 912 |
. . . . . . . . 9
โข ((๐ โ {๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โจ ๐ โ {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐
โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))}) โ (โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โจ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐
โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)))) |
155 | 147, 154 | bitri 275 |
. . . . . . . 8
โข (๐ โ ({๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐
โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))}) โ (โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โจ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐
โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)))) |
156 | | elun 4148 |
. . . . . . . . . . . . . 14
โข (๐ โ ({ 0s } โช
{๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โ (๐ โ { 0s } โจ
๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})) |
157 | | velsn 4644 |
. . . . . . . . . . . . . . 15
โข (๐ โ { 0s } โ
๐ = 0s
) |
158 | 157 | orbi1i 911 |
. . . . . . . . . . . . . 14
โข ((๐ โ { 0s } โจ
๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โ (๐ = 0s โจ ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ})) |
159 | 156, 158 | bitri 275 |
. . . . . . . . . . . . 13
โข (๐ โ ({ 0s } โช
{๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โ (๐ = 0s โจ ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ})) |
160 | 58 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โ โช (๐ฟ โ ฯ)) โ (
0s ยทs ๐) = 0s ) |
161 | 160 | oveq1d 7427 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ โ โช (๐ฟ โ ฯ)) โ ((
0s ยทs ๐) +s (๐ด ยทs ๐)) = ( 0s +s (๐ด ยทs ๐))) |
162 | | muls02 27837 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ
No โ ( 0s ยทs ๐) = 0s ) |
163 | 115, 162 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ โ โช (๐ฟ โ ฯ)) โ (
0s ยทs ๐) = 0s ) |
164 | 161, 163 | oveq12d 7430 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โ โช (๐ฟ โ ฯ)) โ (((
0s ยทs ๐) +s (๐ด ยทs ๐)) -s ( 0s
ยทs ๐)) =
(( 0s +s (๐ด ยทs ๐)) -s 0s
)) |
165 | 2 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ โ โช (๐ฟ โ ฯ)) โ ๐ด โ
No ) |
166 | 165, 115 | mulscld 27831 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โ โช (๐ฟ โ ฯ)) โ (๐ด ยทs ๐) โ
No ) |
167 | | addslid 27691 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ด ยทs ๐) โ
No โ ( 0s +s (๐ด ยทs ๐)) = (๐ด ยทs ๐)) |
168 | 166, 167 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ โ โช (๐ฟ โ ฯ)) โ (
0s +s (๐ด ยทs ๐)) = (๐ด ยทs ๐)) |
169 | 168 | oveq1d 7427 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โ โช (๐ฟ โ ฯ)) โ ((
0s +s (๐ด ยทs ๐)) -s 0s ) = ((๐ด ยทs ๐) -s 0s
)) |
170 | | subsid1 27776 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด ยทs ๐) โ
No โ ((๐ด
ยทs ๐)
-s 0s ) = (๐ด ยทs ๐)) |
171 | 166, 170 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โ โช (๐ฟ โ ฯ)) โ
((๐ด ยทs
๐) -s
0s ) = (๐ด
ยทs ๐)) |
172 | 164, 169,
171 | 3eqtrd 2775 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ โช (๐ฟ โ ฯ)) โ (((
0s ยทs ๐) +s (๐ด ยทs ๐)) -s ( 0s
ยทs ๐)) =
(๐ด ยทs
๐)) |
173 | | eliun 5001 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โช ๐ โ ฯ (๐ฟโ๐) โ โ๐ โ ฯ ๐ โ (๐ฟโ๐)) |
174 | | funiunfv 7250 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (Fun
๐ฟ โ โช ๐ โ ฯ (๐ฟโ๐) = โช (๐ฟ โ
ฯ)) |
175 | 43, 174 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
โข โช ๐ โ ฯ (๐ฟโ๐) = โช (๐ฟ โ
ฯ) |
176 | 175 | eleq2i 2824 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โช ๐ โ ฯ (๐ฟโ๐) โ ๐ โ โช (๐ฟ โ
ฯ)) |
177 | 173, 176 | bitr3i 277 |
. . . . . . . . . . . . . . . . . . 19
โข
(โ๐ โ
ฯ ๐ โ (๐ฟโ๐) โ ๐ โ โช (๐ฟ โ
ฯ)) |
178 | 11, 12, 13, 2, 3, 14 | precsexlem9 27901 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ๐ โ ฯ) โ (โ๐ โ (๐ฟโ๐)(๐ด ยทs ๐) <s 1s โง โ๐ โ (๐
โ๐) 1s <s (๐ด ยทs ๐))) |
179 | 178 | simpld 494 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ โ ฯ) โ โ๐ โ (๐ฟโ๐)(๐ด ยทs ๐) <s 1s ) |
180 | | rsp 3243 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(โ๐ โ
(๐ฟโ๐)(๐ด ยทs ๐) <s 1s โ (๐ โ (๐ฟโ๐) โ (๐ด ยทs ๐) <s 1s )) |
181 | 179, 180 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โ ฯ) โ (๐ โ (๐ฟโ๐) โ (๐ด ยทs ๐) <s 1s )) |
182 | 181 | rexlimdva 3154 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (โ๐ โ ฯ ๐ โ (๐ฟโ๐) โ (๐ด ยทs ๐) <s 1s )) |
183 | 177, 182 | biimtrrid 242 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (๐ โ โช (๐ฟ โ ฯ) โ (๐ด ยทs ๐) <s 1s
)) |
184 | 183 | imp 406 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ โช (๐ฟ โ ฯ)) โ (๐ด ยทs ๐) <s 1s
) |
185 | 172, 184 | eqbrtrd 5170 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ โช (๐ฟ โ ฯ)) โ (((
0s ยทs ๐) +s (๐ด ยทs ๐)) -s ( 0s
ยทs ๐))
<s 1s ) |
186 | 185 | ex 412 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ โ โช (๐ฟ โ ฯ) โ (((
0s ยทs ๐) +s (๐ด ยทs ๐)) -s ( 0s
ยทs ๐))
<s 1s )) |
187 | 67 | breq1d 5158 |
. . . . . . . . . . . . . . . 16
โข (๐ = 0s โ
((((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s 1s โ
((( 0s ยทs ๐) +s (๐ด ยทs ๐)) -s ( 0s
ยทs ๐))
<s 1s )) |
188 | 187 | imbi2d 340 |
. . . . . . . . . . . . . . 15
โข (๐ = 0s โ ((๐ โ โช (๐ฟ
โ ฯ) โ (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s 1s ) โ (๐ โ โช (๐ฟ
โ ฯ) โ ((( 0s ยทs ๐) +s (๐ด ยทs ๐)) -s ( 0s
ยทs ๐))
<s 1s ))) |
189 | 186, 188 | syl5ibrcom 246 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ = 0s โ (๐ โ โช (๐ฟ โ ฯ) โ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s 1s
))) |
190 | | scutcut 27540 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (โช (๐ฟ
โ ฯ) <<s โช (๐
โ ฯ) โ ((โช (๐ฟ
โ ฯ) |s โช (๐
โ ฯ)) โ No โง โช (๐ฟ โ ฯ) <<s
{(โช (๐ฟ โ ฯ) |s โช (๐
โ ฯ))} โง {(โช (๐ฟ โ ฯ) |s โช (๐
โ ฯ))} <<s โช (๐
โ ฯ))) |
191 | 15, 190 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ((โช (๐ฟ
โ ฯ) |s โช (๐
โ ฯ)) โ No โง โช (๐ฟ โ ฯ) <<s
{(โช (๐ฟ โ ฯ) |s โช (๐
โ ฯ))} โง {(โช (๐ฟ โ ฯ) |s โช (๐
โ ฯ))} <<s โช (๐
โ ฯ))) |
192 | 191 | simp3d 1143 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ {(โช (๐ฟ
โ ฯ) |s โช (๐
โ ฯ))} <<s โช (๐
โ ฯ)) |
193 | 192 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐ฟ โ ฯ))) โ
{(โช (๐ฟ โ ฯ) |s โช (๐
โ ฯ))} <<s โช (๐
โ ฯ)) |
194 | | ovex 7445 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (โช (๐ฟ
โ ฯ) |s โช (๐
โ ฯ)) โ V |
195 | 194 | snid 4664 |
. . . . . . . . . . . . . . . . . . . . 21
โข (โช (๐ฟ
โ ฯ) |s โช (๐
โ ฯ)) โ {(โช (๐ฟ
โ ฯ) |s โช (๐
โ ฯ))} |
196 | 17, 195 | eqeltri 2828 |
. . . . . . . . . . . . . . . . . . . 20
โข ๐ โ {(โช (๐ฟ
โ ฯ) |s โช (๐
โ ฯ))} |
197 | 196 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐ฟ โ ฯ))) โ ๐ โ {(โช (๐ฟ
โ ฯ) |s โช (๐
โ ฯ))}) |
198 | | peano2 7885 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ ฯ โ suc ๐ โ
ฯ) |
199 | 198 | ad2antrl 725 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โง ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โง (๐ โ ฯ โง ๐ โ (๐ฟโ๐))) โ suc ๐ โ ฯ) |
200 | | eqid 2731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) = (( 1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) |
201 | | oveq1 7419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
โข (๐ฅ๐ฟ = ๐ โ (๐ฅ๐ฟ -s ๐ด) = (๐ -s ๐ด)) |
202 | 201 | oveq1d 7427 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข (๐ฅ๐ฟ = ๐ โ ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ฟ) = ((๐ -s ๐ด) ยทs ๐ฆ๐ฟ)) |
203 | 202 | oveq2d 7428 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (๐ฅ๐ฟ = ๐ โ ( 1s
+s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ฟ)) = (
1s +s ((๐ -s ๐ด) ยทs ๐ฆ๐ฟ))) |
204 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (๐ฅ๐ฟ = ๐ โ ๐ฅ๐ฟ = ๐) |
205 | 203, 204 | oveq12d 7430 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (๐ฅ๐ฟ = ๐ โ (( 1s
+s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ฟ))
/su ๐ฅ๐ฟ) = (( 1s
+s ((๐
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐)) |
206 | 205 | eqeq2d 2742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ฅ๐ฟ = ๐ โ ((( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐) = ((
1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ฟ))
/su ๐ฅ๐ฟ) โ (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐) = ((
1s +s ((๐ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su
๐))) |
207 | | oveq2 7420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข (๐ฆ๐ฟ = ๐ โ ((๐ -s ๐ด) ยทs ๐ฆ๐ฟ) = ((๐ -s ๐ด) ยทs ๐)) |
208 | 207 | oveq2d 7428 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (๐ฆ๐ฟ = ๐ โ ( 1s
+s ((๐
-s ๐ด)
ยทs ๐ฆ๐ฟ)) = ( 1s
+s ((๐
-s ๐ด)
ยทs ๐))) |
209 | 208 | oveq1d 7427 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (๐ฆ๐ฟ = ๐ โ (( 1s
+s ((๐
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐) = (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐)) |
210 | 209 | eqeq2d 2742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ฆ๐ฟ = ๐ โ ((( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐) = ((
1s +s ((๐ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su
๐) โ (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐) = ((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐))) |
211 | 206, 210 | rspc2ev 3624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ (๐ฟโ๐) โง (( 1s +s
((๐ -s ๐ด) ยทs ๐)) /su ๐) = (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐))
โ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐ฟ โ (๐ฟโ๐)(( 1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐ฟ)) |
212 | 200, 211 | mp3an3 1449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ (๐ฟโ๐)) โ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐ฟ โ (๐ฟโ๐)(( 1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐ฟ)) |
213 | 212 | ad2ant2l 743 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (((๐ โง ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โง (๐ โ ฯ โง ๐ โ (๐ฟโ๐))) โ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐ฟ โ (๐ฟโ๐)(( 1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐ฟ)) |
214 | | ovex 7445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ V |
215 | | eqeq1 2735 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ = (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐)
โ (๐ = ((
1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ฟ))
/su ๐ฅ๐ฟ) โ (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐) = ((
1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐ฟ))
/su ๐ฅ๐ฟ))) |
216 | 215 | 2rexbidv 3218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ = (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐)
โ (โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐ฟ โ (๐ฟโ๐)๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐ฟ)
โ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐ฟ โ (๐ฟโ๐)(( 1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐ฟ))) |
217 | 214, 216 | elab 3668 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ {๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐ฟ โ (๐ฟโ๐)๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐ฟ)}
โ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐ฟ โ (๐ฟโ๐)(( 1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐ฟ)) |
218 | 213, 217 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ โง ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โง (๐ โ ฯ โง ๐ โ (๐ฟโ๐))) โ (( 1s +s
((๐ -s ๐ด) ยทs ๐)) /su ๐) โ {๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐ฟ โ (๐ฟโ๐)๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐ฟ)}) |
219 | | elun1 4176 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ {๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐ฟ โ (๐ฟโ๐)๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐ฟ)}
โ (( 1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ ({๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐ฟ โ (๐ฟโ๐)๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐ฟ)}
โช {๐ โฃ
โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐
โ (๐
โ๐)๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐
)})) |
220 | | elun2 4177 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ ({๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐ฟ โ (๐ฟโ๐)๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐ฟ)}
โช {๐ โฃ
โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐
โ (๐
โ๐)๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐
)})
โ (( 1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ ((๐
โ๐) โช ({๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐ฟ โ (๐ฟโ๐)๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐ฟ)}
โช {๐ โฃ
โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐
โ (๐
โ๐)๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐
)}))) |
221 | 218, 219,
220 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โง ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โง (๐ โ ฯ โง ๐ โ (๐ฟโ๐))) โ (( 1s +s
((๐ -s ๐ด) ยทs ๐)) /su ๐) โ ((๐
โ๐) โช ({๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐ฟ โ (๐ฟโ๐)๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐ฟ)}
โช {๐ โฃ
โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐
โ (๐
โ๐)๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐
)}))) |
222 | 11, 12, 13 | precsexlem5 27897 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ ฯ โ (๐
โsuc ๐) = ((๐
โ๐) โช ({๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐ฟ โ (๐ฟโ๐)๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐ฟ)}
โช {๐ โฃ
โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐
โ (๐
โ๐)๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐
)}))) |
223 | 222 | ad2antrl 725 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โง ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โง (๐ โ ฯ โง ๐ โ (๐ฟโ๐))) โ (๐
โsuc ๐) = ((๐
โ๐) โช ({๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐ฟ โ (๐ฟโ๐)๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐ฟ)}
โช {๐ โฃ
โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐
โ (๐
โ๐)๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐
)}))) |
224 | 221, 223 | eleqtrrd 2835 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โง ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โง (๐ โ ฯ โง ๐ โ (๐ฟโ๐))) โ (( 1s +s
((๐ -s ๐ด) ยทs ๐)) /su ๐) โ (๐
โsuc ๐)) |
225 | | fveq2 6891 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ = suc ๐ โ (๐
โ๐) = (๐
โsuc ๐)) |
226 | 225 | eleq2d 2818 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ = suc ๐ โ ((( 1s +s
((๐ -s ๐ด) ยทs ๐)) /su ๐) โ (๐
โ๐) โ (( 1s +s
((๐ -s ๐ด) ยทs ๐)) /su ๐) โ (๐
โsuc ๐))) |
227 | 226 | rspcev 3612 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((suc
๐ โ ฯ โง ((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ (๐
โsuc ๐)) โ โ๐ โ ฯ (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐)
โ (๐
โ๐)) |
228 | 199, 224,
227 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โง (๐ โ ฯ โง ๐ โ (๐ฟโ๐))) โ โ๐ โ ฯ (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐)
โ (๐
โ๐)) |
229 | 228 | rexlimdvaa 3155 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โ (โ๐ โ ฯ ๐ โ (๐ฟโ๐) โ โ๐ โ ฯ (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐)
โ (๐
โ๐))) |
230 | | eliun 5001 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ โช
๐ โ ฯ (๐
โ๐) โ โ๐ โ ฯ (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐)
โ (๐
โ๐)) |
231 | | fo2nd 8000 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข
2nd :VโontoโV |
232 | | fofun 6806 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข
(2nd :VโontoโV โ Fun 2nd ) |
233 | 231, 232 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข Fun
2nd |
234 | | funco 6588 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((Fun
2nd โง Fun ๐น)
โ Fun (2nd โ ๐น)) |
235 | 233, 39, 234 | mp2an 689 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข Fun
(2nd โ ๐น) |
236 | 13 | funeqi 6569 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (Fun
๐
โ Fun
(2nd โ ๐น)) |
237 | 235, 236 | mpbir 230 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข Fun ๐
|
238 | | funiunfv 7250 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (Fun
๐
โ โช ๐ โ ฯ (๐
โ๐) = โช (๐
โ
ฯ)) |
239 | 237, 238 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข โช ๐ โ ฯ (๐
โ๐) = โช (๐
โ
ฯ) |
240 | 239 | eleq2i 2824 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ โช
๐ โ ฯ (๐
โ๐) โ (( 1s +s
((๐ -s ๐ด) ยทs ๐)) /su ๐) โ โช (๐
โ ฯ)) |
241 | 230, 240 | bitr3i 277 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(โ๐ โ
ฯ (( 1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ (๐
โ๐) โ (( 1s +s
((๐ -s ๐ด) ยทs ๐)) /su ๐) โ โช (๐
โ ฯ)) |
242 | 229, 177,
241 | 3imtr3g 295 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โ (๐ โ โช (๐ฟ โ ฯ) โ ((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ โช (๐
โ
ฯ))) |
243 | 242 | impr 454 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐ฟ โ ฯ))) โ ((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ โช (๐
โ
ฯ)) |
244 | 193, 197,
243 | ssltsepcd 27533 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐ฟ โ ฯ))) โ ๐ <s (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐)) |
245 | 56 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐ฟ โ ฯ))) โ ๐ โ
No ) |
246 | 144 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐ฟ โ ฯ))) โ
1s โ No ) |
247 | | leftssno 27613 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ( L
โ๐ด) โ No |
248 | 6, 247 | sstri 3991 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ} โ No |
249 | 248 | sseli 3978 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โ ๐ โ No
) |
250 | 249 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โ ๐ โ No
) |
251 | 2 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โ ๐ด โ No
) |
252 | 250, 251 | subscld 27775 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โ (๐ -s ๐ด) โ No
) |
253 | 252 | adantrr 714 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐ฟ โ ฯ))) โ
(๐ -s ๐ด) โ
No ) |
254 | 115 | adantrl 713 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐ฟ โ ฯ))) โ ๐ โ
No ) |
255 | 253, 254 | mulscld 27831 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐ฟ โ ฯ))) โ
((๐ -s ๐ด) ยทs ๐) โ
No ) |
256 | 246, 255 | addscld 27703 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐ฟ โ ฯ))) โ (
1s +s ((๐ -s ๐ด) ยทs ๐)) โ No
) |
257 | 249 | ad2antrl 725 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐ฟ โ ฯ))) โ ๐ โ
No ) |
258 | | breq2 5152 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฅ = ๐ โ ( 0s <s ๐ฅ โ 0s <s
๐)) |
259 | 258 | elrab 3683 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โ (๐ โ ( L โ๐ด) โง 0s <s ๐)) |
260 | 259 | simprbi 496 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โ 0s <s
๐) |
261 | 260 | ad2antrl 725 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐ฟ โ ฯ))) โ
0s <s ๐) |
262 | 260 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โ 0s <s
๐) |
263 | | breq2 5152 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฅ๐ = ๐ โ ( 0s <s
๐ฅ๐
โ 0s <s ๐)) |
264 | | oveq1 7419 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ฅ๐ = ๐ โ (๐ฅ๐ ยทs
๐ฆ) = (๐ ยทs ๐ฆ)) |
265 | 264 | eqeq1d 2733 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ฅ๐ = ๐ โ ((๐ฅ๐ ยทs
๐ฆ) = 1s โ
(๐ ยทs
๐ฆ) = 1s
)) |
266 | 265 | rexbidv 3177 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฅ๐ = ๐ โ (โ๐ฆ โ
No (๐ฅ๐ ยทs
๐ฆ) = 1s โ
โ๐ฆ โ No (๐ ยทs ๐ฆ) = 1s )) |
267 | 263, 266 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฅ๐ = ๐ โ (( 0s <s
๐ฅ๐
โ โ๐ฆ โ
No (๐ฅ๐ ยทs
๐ฆ) = 1s ) โ
( 0s <s ๐
โ โ๐ฆ โ
No (๐ ยทs ๐ฆ) = 1s ))) |
268 | 14 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โ โ๐ฅ๐ โ (( L
โ๐ด) โช ( R
โ๐ด))( 0s
<s ๐ฅ๐
โ โ๐ฆ โ
No (๐ฅ๐ ยทs
๐ฆ) = 1s
)) |
269 | | ssun1 4172 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ( L
โ๐ด) โ (( L
โ๐ด) โช ( R
โ๐ด)) |
270 | 6, 269 | sstri 3991 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ} โ (( L
โ๐ด) โช ( R
โ๐ด)) |
271 | 270 | sseli 3978 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โ ๐ โ (( L โ๐ด) โช ( R โ๐ด))) |
272 | 271 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โ ๐ โ (( L โ๐ด) โช ( R โ๐ด))) |
273 | 267, 268,
272 | rspcdva 3613 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โ ( 0s <s
๐ โ โ๐ฆ โ
No (๐
ยทs ๐ฆ) =
1s )) |
274 | 262, 273 | mpd 15 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โ โ๐ฆ โ
No (๐
ยทs ๐ฆ) =
1s ) |
275 | 274 | adantrr 714 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐ฟ โ ฯ))) โ
โ๐ฆ โ No (๐ ยทs ๐ฆ) = 1s ) |
276 | 245, 256,
257, 261, 275 | sltmuldiv2wd 27889 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐ฟ โ ฯ))) โ
((๐ ยทs
๐) <s ( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
โ ๐ <s ((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐))) |
277 | 244, 276 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐ฟ โ ฯ))) โ
(๐ ยทs
๐) <s ( 1s
+s ((๐
-s ๐ด)
ยทs ๐))) |
278 | 257, 254 | mulscld 27831 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐ฟ โ ฯ))) โ
(๐ ยทs
๐) โ No ) |
279 | 166 | adantrl 713 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐ฟ โ ฯ))) โ
(๐ด ยทs
๐) โ No ) |
280 | 246, 278,
279 | addsubsassd 27788 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐ฟ โ ฯ))) โ ((
1s +s (๐ ยทs ๐)) -s (๐ด ยทs ๐)) = ( 1s +s ((๐ ยทs ๐) -s (๐ด ยทs ๐)))) |
281 | 2 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐ฟ โ ฯ))) โ ๐ด โ
No ) |
282 | 257, 281,
254 | subsdird 27854 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐ฟ โ ฯ))) โ
((๐ -s ๐ด) ยทs ๐) = ((๐ ยทs ๐) -s (๐ด ยทs ๐))) |
283 | 282 | oveq2d 7428 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐ฟ โ ฯ))) โ (
1s +s ((๐ -s ๐ด) ยทs ๐)) = ( 1s +s ((๐ ยทs ๐) -s (๐ด ยทs ๐)))) |
284 | 280, 283 | eqtr4d 2774 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐ฟ โ ฯ))) โ ((
1s +s (๐ ยทs ๐)) -s (๐ด ยทs ๐)) = ( 1s +s ((๐ -s ๐ด) ยทs ๐))) |
285 | 277, 284 | breqtrrd 5176 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐ฟ โ ฯ))) โ
(๐ ยทs
๐) <s (( 1s
+s (๐
ยทs ๐))
-s (๐ด
ยทs ๐))) |
286 | 56 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โ ๐ โ No
) |
287 | 250, 286 | mulscld 27831 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โ (๐ ยทs ๐) โ No
) |
288 | 287 | adantrr 714 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐ฟ โ ฯ))) โ
(๐ ยทs
๐) โ No ) |
289 | 288, 279 | addscld 27703 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐ฟ โ ฯ))) โ
((๐ ยทs
๐) +s (๐ด ยทs ๐)) โ
No ) |
290 | 289, 278,
246 | sltsubaddd 27796 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐ฟ โ ฯ))) โ
((((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s 1s โ
((๐ ยทs
๐) +s (๐ด ยทs ๐)) <s ( 1s
+s (๐
ยทs ๐)))) |
291 | 246, 278 | addscld 27703 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐ฟ โ ฯ))) โ (
1s +s (๐ ยทs ๐)) โ No
) |
292 | 288, 279,
291 | sltaddsubd 27798 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐ฟ โ ฯ))) โ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) <s ( 1s
+s (๐
ยทs ๐))
โ (๐
ยทs ๐)
<s (( 1s +s (๐ ยทs ๐)) -s (๐ด ยทs ๐)))) |
293 | 290, 292 | bitrd 279 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐ฟ โ ฯ))) โ
((((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s 1s โ
(๐ ยทs
๐) <s (( 1s
+s (๐
ยทs ๐))
-s (๐ด
ยทs ๐)))) |
294 | 285, 293 | mpbird 257 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐ฟ โ ฯ))) โ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s 1s
) |
295 | 294 | exp32 420 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โ (๐ โ โช (๐ฟ โ ฯ) โ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s 1s
))) |
296 | 189, 295 | jaod 856 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ = 0s โจ ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โ (๐ โ โช (๐ฟ โ ฯ) โ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s 1s
))) |
297 | 159, 296 | biimtrid 241 |
. . . . . . . . . . . 12
โข (๐ โ (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โ (๐ โ โช (๐ฟ
โ ฯ) โ (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s 1s ))) |
298 | 297 | imp32 418 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โง ๐ โ โช (๐ฟ
โ ฯ))) โ (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s 1s ) |
299 | | breq1 5151 |
. . . . . . . . . . 11
โข (๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ (๐ <s 1s โ (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s 1s
)) |
300 | 298, 299 | syl5ibrcom 246 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โง ๐ โ โช (๐ฟ
โ ฯ))) โ (๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ ๐ <s 1s )) |
301 | 300 | rexlimdvva 3210 |
. . . . . . . . 9
โข (๐ โ (โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ ๐ <s 1s )) |
302 | 192 | adantr 480 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ
{(โช (๐ฟ โ ฯ) |s โช (๐
โ ฯ))} <<s โช (๐
โ ฯ)) |
303 | 196 | a1i 11 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ ๐ โ {(โช (๐ฟ
โ ฯ) |s โช (๐
โ ฯ))}) |
304 | 198 | ad2antrl 725 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ โ ( R โ๐ด)) โง (๐ โ ฯ โง ๐ โ (๐
โ๐))) โ suc ๐ โ ฯ) |
305 | | oveq1 7419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ฅ๐
= ๐ โ (๐ฅ๐
-s ๐ด) = (๐ -s ๐ด)) |
306 | 305 | oveq1d 7427 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ฅ๐
= ๐ โ ((๐ฅ๐
-s ๐ด) ยทs ๐ฆ๐
) = ((๐ -s ๐ด) ยทs ๐ฆ๐
)) |
307 | 306 | oveq2d 7428 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ฅ๐
= ๐ โ ( 1s
+s ((๐ฅ๐
-s ๐ด) ยทs ๐ฆ๐
)) = (
1s +s ((๐ -s ๐ด) ยทs ๐ฆ๐
))) |
308 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ฅ๐
= ๐ โ ๐ฅ๐
= ๐) |
309 | 307, 308 | oveq12d 7430 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ฅ๐
= ๐ โ (( 1s
+s ((๐ฅ๐
-s ๐ด) ยทs ๐ฆ๐
))
/su ๐ฅ๐
) = (( 1s
+s ((๐
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐)) |
310 | 309 | eqeq2d 2742 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ฅ๐
= ๐ โ ((( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐) = ((
1s +s ((๐ฅ๐
-s ๐ด) ยทs ๐ฆ๐
))
/su ๐ฅ๐
) โ (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐) = ((
1s +s ((๐ -s ๐ด) ยทs ๐ฆ๐
)) /su
๐))) |
311 | | oveq2 7420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ฆ๐
= ๐ โ ((๐ -s ๐ด) ยทs ๐ฆ๐
) = ((๐ -s ๐ด) ยทs ๐)) |
312 | 311 | oveq2d 7428 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ฆ๐
= ๐ โ ( 1s
+s ((๐
-s ๐ด)
ยทs ๐ฆ๐
)) = ( 1s
+s ((๐
-s ๐ด)
ยทs ๐))) |
313 | 312 | oveq1d 7427 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ฆ๐
= ๐ โ (( 1s
+s ((๐
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐) = (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐)) |
314 | 313 | eqeq2d 2742 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ฆ๐
= ๐ โ ((( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐) = ((
1s +s ((๐ -s ๐ด) ยทs ๐ฆ๐
)) /su
๐) โ (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐) = ((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐))) |
315 | 310, 314 | rspc2ev 3624 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ โ ( R โ๐ด) โง ๐ โ (๐
โ๐) โง (( 1s +s
((๐ -s ๐ด) ยทs ๐)) /su ๐) = (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐))
โ โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐
โ (๐
โ๐)(( 1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐
)) |
316 | 200, 315 | mp3an3 1449 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โ ( R โ๐ด) โง ๐ โ (๐
โ๐)) โ โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐
โ (๐
โ๐)(( 1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐
)) |
317 | 316 | ad2ant2l 743 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง ๐ โ ( R โ๐ด)) โง (๐ โ ฯ โง ๐ โ (๐
โ๐))) โ โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐
โ (๐
โ๐)(( 1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐
)) |
318 | | eqeq1 2735 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ = (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐)
โ (๐ = ((
1s +s ((๐ฅ๐
-s ๐ด) ยทs ๐ฆ๐
))
/su ๐ฅ๐
) โ (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐) = ((
1s +s ((๐ฅ๐
-s ๐ด) ยทs ๐ฆ๐
))
/su ๐ฅ๐
))) |
319 | 318 | 2rexbidv 3218 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ = (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐)
โ (โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐
โ (๐
โ๐)๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐
)
โ โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐
โ (๐
โ๐)(( 1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐
))) |
320 | 214, 319 | elab 3668 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ {๐ โฃ โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐
โ (๐
โ๐)๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐
)}
โ โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐
โ (๐
โ๐)(( 1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐
)) |
321 | 317, 320 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง ๐ โ ( R โ๐ด)) โง (๐ โ ฯ โง ๐ โ (๐
โ๐))) โ (( 1s +s
((๐ -s ๐ด) ยทs ๐)) /su ๐) โ {๐ โฃ โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐
โ (๐
โ๐)๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐
)}) |
322 | | elun2 4177 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ {๐ โฃ โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐
โ (๐
โ๐)๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐
)}
โ (( 1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ ({๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐ฟ โ (๐ฟโ๐)๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐ฟ)}
โช {๐ โฃ
โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐
โ (๐
โ๐)๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐
)})) |
323 | 321, 322,
220 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ โ ( R โ๐ด)) โง (๐ โ ฯ โง ๐ โ (๐
โ๐))) โ (( 1s +s
((๐ -s ๐ด) ยทs ๐)) /su ๐) โ ((๐
โ๐) โช ({๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐ฟ โ (๐ฟโ๐)๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐ฟ)}
โช {๐ โฃ
โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐
โ (๐
โ๐)๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐
)}))) |
324 | 222 | ad2antrl 725 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ โ ( R โ๐ด)) โง (๐ โ ฯ โง ๐ โ (๐
โ๐))) โ (๐
โsuc ๐) = ((๐
โ๐) โช ({๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐ฟ โ (๐ฟโ๐)๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐ฟ)}
โช {๐ โฃ
โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐
โ (๐
โ๐)๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐
)}))) |
325 | 323, 324 | eleqtrrd 2835 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ โ ( R โ๐ด)) โง (๐ โ ฯ โง ๐ โ (๐
โ๐))) โ (( 1s +s
((๐ -s ๐ด) ยทs ๐)) /su ๐) โ (๐
โsuc ๐)) |
326 | 304, 325,
227 | syl2anc 583 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ โ ( R โ๐ด)) โง (๐ โ ฯ โง ๐ โ (๐
โ๐))) โ โ๐ โ ฯ (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐)
โ (๐
โ๐)) |
327 | 326 | rexlimdvaa 3155 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ ( R โ๐ด)) โ (โ๐ โ ฯ ๐ โ (๐
โ๐) โ โ๐ โ ฯ (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐)
โ (๐
โ๐))) |
328 | | eliun 5001 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โช ๐ โ ฯ (๐
โ๐) โ โ๐ โ ฯ ๐ โ (๐
โ๐)) |
329 | | funiunfv 7250 |
. . . . . . . . . . . . . . . . . . . 20
โข (Fun
๐
โ โช ๐ โ ฯ (๐
โ๐) = โช (๐
โ
ฯ)) |
330 | 237, 329 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
โข โช ๐ โ ฯ (๐
โ๐) = โช (๐
โ
ฯ) |
331 | 330 | eleq2i 2824 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โช ๐ โ ฯ (๐
โ๐) โ ๐ โ โช (๐
โ
ฯ)) |
332 | 328, 331 | bitr3i 277 |
. . . . . . . . . . . . . . . . 17
โข
(โ๐ โ
ฯ ๐ โ (๐
โ๐) โ ๐ โ โช (๐
โ
ฯ)) |
333 | 327, 332,
241 | 3imtr3g 295 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ ( R โ๐ด)) โ (๐ โ โช (๐
โ ฯ) โ ((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ โช (๐
โ
ฯ))) |
334 | 333 | impr 454 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ ((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ โช (๐
โ
ฯ)) |
335 | 302, 303,
334 | ssltsepcd 27533 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ ๐ <s (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐)) |
336 | 144 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ
1s โ No ) |
337 | 2 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ โ ( R โ๐ด)) โ ๐ด โ No
) |
338 | 127, 337 | subscld 27775 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โ ( R โ๐ด)) โ (๐ -s ๐ด) โ No
) |
339 | 338 | adantrr 714 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ
(๐ -s ๐ด) โ
No ) |
340 | 339, 135 | mulscld 27831 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ
((๐ -s ๐ด) ยทs ๐) โ
No ) |
341 | 336, 340 | addscld 27703 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ (
1s +s ((๐ -s ๐ด) ยทs ๐)) โ No
) |
342 | 20 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ ( R โ๐ด)) โ 0s โ No ) |
343 | 3 | adantr 480 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ ( R โ๐ด)) โ 0s <s ๐ด) |
344 | | breq2 5152 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฅ๐ = ๐ โ (๐ด <s ๐ฅ๐ โ ๐ด <s ๐)) |
345 | | rightval 27597 |
. . . . . . . . . . . . . . . . . . . 20
โข ( R
โ๐ด) = {๐ฅ๐ โ ( O
โ( bday โ๐ด)) โฃ ๐ด <s ๐ฅ๐} |
346 | 344, 345 | elrab2 3686 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ( R โ๐ด) โ (๐ โ ( O โ(
bday โ๐ด))
โง ๐ด <s ๐)) |
347 | 346 | simprbi 496 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ( R โ๐ด) โ ๐ด <s ๐) |
348 | 347 | adantl 481 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ ( R โ๐ด)) โ ๐ด <s ๐) |
349 | 342, 337,
127, 343, 348 | slttrd 27499 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ ( R โ๐ด)) โ 0s <s ๐) |
350 | 349 | adantrr 714 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ
0s <s ๐) |
351 | 14 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โ ( R โ๐ด)) โ โ๐ฅ๐ โ (( L โ๐ด) โช ( R โ๐ด))( 0s <s ๐ฅ๐ โ
โ๐ฆ โ No (๐ฅ๐ ยทs
๐ฆ) = 1s
)) |
352 | | elun2 4177 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ( R โ๐ด) โ ๐ โ (( L โ๐ด) โช ( R โ๐ด))) |
353 | 352 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โ ( R โ๐ด)) โ ๐ โ (( L โ๐ด) โช ( R โ๐ด))) |
354 | 267, 351,
353 | rspcdva 3613 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ ( R โ๐ด)) โ ( 0s <s ๐ โ โ๐ฆ โ
No (๐
ยทs ๐ฆ) =
1s )) |
355 | 349, 354 | mpd 15 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ ( R โ๐ด)) โ โ๐ฆ โ No
(๐ ยทs
๐ฆ) = 1s
) |
356 | 355 | adantrr 714 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ
โ๐ฆ โ No (๐ ยทs ๐ฆ) = 1s ) |
357 | 129, 341,
128, 350, 356 | sltmuldiv2wd 27889 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ
((๐ ยทs
๐) <s ( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
โ ๐ <s ((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐))) |
358 | 335, 357 | mpbird 257 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ
(๐ ยทs
๐) <s ( 1s
+s ((๐
-s ๐ด)
ยทs ๐))) |
359 | 336, 138,
136 | addsubsassd 27788 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ ((
1s +s (๐ ยทs ๐)) -s (๐ด ยทs ๐)) = ( 1s +s ((๐ ยทs ๐) -s (๐ด ยทs ๐)))) |
360 | 128, 131,
135 | subsdird 27854 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ
((๐ -s ๐ด) ยทs ๐) = ((๐ ยทs ๐) -s (๐ด ยทs ๐))) |
361 | 360 | oveq2d 7428 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ (
1s +s ((๐ -s ๐ด) ยทs ๐)) = ( 1s +s ((๐ ยทs ๐) -s (๐ด ยทs ๐)))) |
362 | 359, 361 | eqtr4d 2774 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ ((
1s +s (๐ ยทs ๐)) -s (๐ด ยทs ๐)) = ( 1s +s ((๐ -s ๐ด) ยทs ๐))) |
363 | 358, 362 | breqtrrd 5176 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ
(๐ ยทs
๐) <s (( 1s
+s (๐
ยทs ๐))
-s (๐ด
ยทs ๐))) |
364 | 137, 138,
336 | sltsubaddd 27796 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ
((((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s 1s โ
((๐ ยทs
๐) +s (๐ด ยทs ๐)) <s ( 1s
+s (๐
ยทs ๐)))) |
365 | 336, 138 | addscld 27703 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ (
1s +s (๐ ยทs ๐)) โ No
) |
366 | 130, 136,
365 | sltaddsubd 27798 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) <s ( 1s
+s (๐
ยทs ๐))
โ (๐
ยทs ๐)
<s (( 1s +s (๐ ยทs ๐)) -s (๐ด ยทs ๐)))) |
367 | 364, 366 | bitrd 279 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ
((((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s 1s โ
(๐ ยทs
๐) <s (( 1s
+s (๐
ยทs ๐))
-s (๐ด
ยทs ๐)))) |
368 | 363, 367 | mpbird 257 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s 1s
) |
369 | 368, 299 | syl5ibrcom 246 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐
โ ฯ))) โ
(๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ ๐ <s 1s )) |
370 | 369 | rexlimdvva 3210 |
. . . . . . . . 9
โข (๐ โ (โ๐ โ ( R โ๐ด)โ๐ โ โช (๐
โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ ๐ <s 1s )) |
371 | 301, 370 | jaod 856 |
. . . . . . . 8
โข (๐ โ ((โ๐ โ ({ 0s } โช
{๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โจ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐
โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) โ ๐ <s 1s )) |
372 | 155, 371 | biimtrid 241 |
. . . . . . 7
โข (๐ โ (๐ โ ({๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐
โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))}) โ ๐ <s 1s )) |
373 | 372 | imp 406 |
. . . . . 6
โข ((๐ โง ๐ โ ({๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐
โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))})) โ ๐ <s 1s ) |
374 | | velsn 4644 |
. . . . . . 7
โข (๐ โ { 1s } โ
๐ = 1s
) |
375 | | breq2 5152 |
. . . . . . 7
โข (๐ = 1s โ (๐ <s ๐ โ ๐ <s 1s )) |
376 | 374, 375 | sylbi 216 |
. . . . . 6
โข (๐ โ { 1s } โ
(๐ <s ๐ โ ๐ <s 1s )) |
377 | 373, 376 | syl5ibrcom 246 |
. . . . 5
โข ((๐ โง ๐ โ ({๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐
โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))})) โ (๐ โ { 1s } โ ๐ <s ๐)) |
378 | 377 | 3impia 1116 |
. . . 4
โข ((๐ โง ๐ โ ({๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐
โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))}) โง ๐ โ { 1s }) โ ๐ <s ๐) |
379 | 103, 105,
143, 146, 378 | ssltd 27530 |
. . 3
โข (๐ โ ({๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐
โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))}) <<s { 1s
}) |
380 | | eqid 2731 |
. . . . . . 7
โข (๐ โ ({ 0s } โช
{๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}), ๐ โ โช (๐
โ ฯ) โฆ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) = (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}), ๐ โ โช (๐
โ ฯ) โฆ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) |
381 | 380 | rnmpo 7545 |
. . . . . 6
โข ran
(๐ โ ({ 0s
} โช {๐ฅ โ ( L
โ๐ด) โฃ
0s <s ๐ฅ}),
๐ โ โช (๐
โ ฯ) โฆ (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) = {๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} |
382 | | mpoexga 8068 |
. . . . . . . 8
โข ((({
0s } โช {๐ฅ
โ ( L โ๐ด)
โฃ 0s <s ๐ฅ}) โ V โง โช (๐
โ ฯ) โ V) โ (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}), ๐ โ โช (๐
โ ฯ) โฆ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) โ V) |
383 | 85, 97, 382 | syl2anc 583 |
. . . . . . 7
โข (๐ โ (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}), ๐ โ โช (๐
โ ฯ) โฆ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) โ V) |
384 | | rnexg 7899 |
. . . . . . 7
โข ((๐ โ ({ 0s } โช
{๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}), ๐ โ โช (๐
โ ฯ) โฆ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) โ V โ ran (๐ โ ({ 0s } โช
{๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}), ๐ โ โช (๐
โ ฯ) โฆ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) โ V) |
385 | 383, 384 | syl 17 |
. . . . . 6
โข (๐ โ ran (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}), ๐ โ โช (๐
โ ฯ) โฆ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) โ V) |
386 | 381, 385 | eqeltrrid 2837 |
. . . . 5
โข (๐ โ {๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โ V) |
387 | | eqid 2731 |
. . . . . . 7
โข (๐ โ ( R โ๐ด), ๐ โ โช (๐ฟ โ ฯ) โฆ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) = (๐ โ ( R โ๐ด), ๐ โ โช (๐ฟ โ ฯ) โฆ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) |
388 | 387 | rnmpo 7545 |
. . . . . 6
โข ran
(๐ โ ( R โ๐ด), ๐ โ โช (๐ฟ โ ฯ) โฆ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) = {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} |
389 | | mpoexga 8068 |
. . . . . . . 8
โข ((( R
โ๐ด) โ V โง
โช (๐ฟ โ ฯ) โ V) โ (๐ โ ( R โ๐ด), ๐ โ โช (๐ฟ โ ฯ) โฆ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) โ V) |
390 | 95, 87, 389 | sylancr 586 |
. . . . . . 7
โข (๐ โ (๐ โ ( R โ๐ด), ๐ โ โช (๐ฟ โ ฯ) โฆ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) โ V) |
391 | | rnexg 7899 |
. . . . . . 7
โข ((๐ โ ( R โ๐ด), ๐ โ โช (๐ฟ โ ฯ) โฆ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) โ V โ ran (๐ โ ( R โ๐ด), ๐ โ โช (๐ฟ โ ฯ) โฆ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) โ V) |
392 | 390, 391 | syl 17 |
. . . . . 6
โข (๐ โ ran (๐ โ ( R โ๐ด), ๐ โ โช (๐ฟ โ ฯ) โฆ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) โ V) |
393 | 388, 392 | eqeltrrid 2837 |
. . . . 5
โข (๐ โ {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โ V) |
394 | 386, 393 | unexd 7745 |
. . . 4
โข (๐ โ ({๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))}) โ V) |
395 | 108 | adantrr 714 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โง ๐ โ โช (๐
โ ฯ))) โ ๐
โ No ) |
396 | 56 | adantr 480 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โง ๐ โ โช (๐
โ ฯ))) โ ๐
โ No ) |
397 | 395, 396 | mulscld 27831 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โง ๐ โ โช (๐
โ ฯ))) โ (๐ ยทs ๐) โ No
) |
398 | 2 | adantr 480 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โง ๐ โ โช (๐
โ ฯ))) โ ๐ด
โ No ) |
399 | 134 | adantrl 713 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โง ๐ โ โช (๐
โ ฯ))) โ ๐
โ No ) |
400 | 398, 399 | mulscld 27831 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โง ๐ โ โช (๐
โ ฯ))) โ (๐ด ยทs ๐) โ No
) |
401 | 397, 400 | addscld 27703 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โง ๐ โ โช (๐
โ ฯ))) โ ((๐ ยทs ๐) +s (๐ด ยทs ๐)) โ No
) |
402 | 395, 399 | mulscld 27831 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โง ๐ โ โช (๐
โ ฯ))) โ (๐ ยทs ๐) โ No
) |
403 | 401, 402 | subscld 27775 |
. . . . . . . 8
โข ((๐ โง (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โง ๐ โ โช (๐
โ ฯ))) โ (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ No
) |
404 | 403, 121 | syl5ibrcom 246 |
. . . . . . 7
โข ((๐ โง (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โง ๐ โ โช (๐
โ ฯ))) โ (๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ ๐ โ No
)) |
405 | 404 | rexlimdvva 3210 |
. . . . . 6
โข (๐ โ (โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ ๐ โ No
)) |
406 | 405 | abssdv 4065 |
. . . . 5
โข (๐ โ {๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โ No ) |
407 | 127 | adantrr 714 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ ๐ โ
No ) |
408 | 56 | adantr 480 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ ๐ โ
No ) |
409 | 407, 408 | mulscld 27831 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ
(๐ ยทs
๐) โ No ) |
410 | 2 | adantr 480 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ ๐ด โ
No ) |
411 | 115 | adantrl 713 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ ๐ โ
No ) |
412 | 410, 411 | mulscld 27831 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ
(๐ด ยทs
๐) โ No ) |
413 | 409, 412 | addscld 27703 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ
((๐ ยทs
๐) +s (๐ด ยทs ๐)) โ
No ) |
414 | 407, 411 | mulscld 27831 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ
(๐ ยทs
๐) โ No ) |
415 | 413, 414 | subscld 27775 |
. . . . . . . 8
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ
No ) |
416 | 415, 121 | syl5ibrcom 246 |
. . . . . . 7
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ
(๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ ๐ โ No
)) |
417 | 416 | rexlimdvva 3210 |
. . . . . 6
โข (๐ โ (โ๐ โ ( R โ๐ด)โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ ๐ โ No
)) |
418 | 417 | abssdv 4065 |
. . . . 5
โข (๐ โ {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โ No
) |
419 | 406, 418 | unssd 4186 |
. . . 4
โข (๐ โ ({๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))}) โ No
) |
420 | | elun 4148 |
. . . . . . . 8
โข (๐ โ ({๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))}) โ (๐ โ {๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โจ ๐ โ {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))})) |
421 | | vex 3477 |
. . . . . . . . . 10
โข ๐ โ V |
422 | | eqeq1 2735 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ ๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)))) |
423 | 422 | 2rexbidv 3218 |
. . . . . . . . . 10
โข (๐ = ๐ โ (โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ โ๐ โ ({ 0s } โช
{๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)))) |
424 | 421, 423 | elab 3668 |
. . . . . . . . 9
โข (๐ โ {๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โ โ๐ โ ({ 0s } โช
{๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) |
425 | 422 | 2rexbidv 3218 |
. . . . . . . . . 10
โข (๐ = ๐ โ (โ๐ โ ( R โ๐ด)โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)))) |
426 | 421, 425 | elab 3668 |
. . . . . . . . 9
โข (๐ โ {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) |
427 | 424, 426 | orbi12i 912 |
. . . . . . . 8
โข ((๐ โ {๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โจ ๐ โ {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))}) โ (โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โจ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)))) |
428 | 420, 427 | bitri 275 |
. . . . . . 7
โข (๐ โ ({๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))}) โ (โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โจ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)))) |
429 | | eliun 5001 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โช ๐ โ ฯ (๐
โ๐) โ โ๐ โ ฯ ๐ โ (๐
โ๐)) |
430 | 239 | eleq2i 2824 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โช ๐ โ ฯ (๐
โ๐) โ ๐ โ โช (๐
โ
ฯ)) |
431 | 429, 430 | bitr3i 277 |
. . . . . . . . . . . . . . . . . 18
โข
(โ๐ โ
ฯ ๐ โ (๐
โ๐) โ ๐ โ โช (๐
โ
ฯ)) |
432 | 11, 12, 13, 2, 3, 14 | precsexlem9 27901 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โ ฯ) โ (โ๐ โ (๐ฟโ๐)(๐ด ยทs ๐) <s 1s โง โ๐ โ (๐
โ๐) 1s <s (๐ด ยทs ๐))) |
433 | | rsp 3243 |
. . . . . . . . . . . . . . . . . . . 20
โข
(โ๐ โ
(๐
โ๐) 1s <s (๐ด ยทs ๐) โ (๐ โ (๐
โ๐) โ 1s <s (๐ด ยทs ๐))) |
434 | 432, 433 | simpl2im 503 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ โ ฯ) โ (๐ โ (๐
โ๐) โ 1s <s (๐ด ยทs ๐))) |
435 | 434 | rexlimdva 3154 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (โ๐ โ ฯ ๐ โ (๐
โ๐) โ 1s <s (๐ด ยทs ๐))) |
436 | 431, 435 | biimtrrid 242 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐ โ โช (๐
โ ฯ) โ
1s <s (๐ด
ยทs ๐))) |
437 | 436 | imp 406 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ โช (๐
โ ฯ)) โ
1s <s (๐ด
ยทs ๐)) |
438 | 56 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โ โช (๐
โ ฯ)) โ ๐ โ
No ) |
439 | 57 | oveq1d 7427 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ
No โ (( 0s ยทs ๐) +s (๐ด ยทs ๐)) = ( 0s +s (๐ด ยทs ๐))) |
440 | 438, 439 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ โ โช (๐
โ ฯ)) โ ((
0s ยทs ๐) +s (๐ด ยทs ๐)) = ( 0s +s (๐ด ยทs ๐))) |
441 | 2 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ โ โช (๐
โ ฯ)) โ ๐ด โ
No ) |
442 | 441, 134 | mulscld 27831 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โ โช (๐
โ ฯ)) โ (๐ด ยทs ๐) โ
No ) |
443 | 442, 167 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ โ โช (๐
โ ฯ)) โ (
0s +s (๐ด ยทs ๐)) = (๐ด ยทs ๐)) |
444 | 440, 443 | eqtrd 2771 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โ โช (๐
โ ฯ)) โ ((
0s ยทs ๐) +s (๐ด ยทs ๐)) = (๐ด ยทs ๐)) |
445 | 134, 162 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โ โช (๐
โ ฯ)) โ (
0s ยทs ๐) = 0s ) |
446 | 444, 445 | oveq12d 7430 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ โช (๐
โ ฯ)) โ (((
0s ยทs ๐) +s (๐ด ยทs ๐)) -s ( 0s
ยทs ๐)) =
((๐ด ยทs
๐) -s
0s )) |
447 | 442, 170 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ โช (๐
โ ฯ)) โ
((๐ด ยทs
๐) -s
0s ) = (๐ด
ยทs ๐)) |
448 | 446, 447 | eqtrd 2771 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ โช (๐
โ ฯ)) โ (((
0s ยทs ๐) +s (๐ด ยทs ๐)) -s ( 0s
ยทs ๐)) =
(๐ด ยทs
๐)) |
449 | 437, 448 | breqtrrd 5176 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ โช (๐
โ ฯ)) โ
1s <s ((( 0s ยทs ๐) +s (๐ด ยทs ๐)) -s ( 0s
ยทs ๐))) |
450 | 449 | ex 412 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ โ โช (๐
โ ฯ) โ
1s <s ((( 0s ยทs ๐) +s (๐ด ยทs ๐)) -s ( 0s
ยทs ๐)))) |
451 | 67 | breq2d 5160 |
. . . . . . . . . . . . . . 15
โข (๐ = 0s โ (
1s <s (((๐
ยทs ๐)
+s (๐ด
ยทs ๐))
-s (๐
ยทs ๐))
โ 1s <s ((( 0s ยทs ๐) +s (๐ด ยทs ๐)) -s ( 0s
ยทs ๐)))) |
452 | 451 | imbi2d 340 |
. . . . . . . . . . . . . 14
โข (๐ = 0s โ ((๐ โ โช (๐
โ ฯ) โ 1s <s (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) โ (๐ โ โช (๐
โ ฯ) โ
1s <s ((( 0s ยทs ๐) +s (๐ด ยทs ๐)) -s ( 0s
ยทs ๐))))) |
453 | 450, 452 | syl5ibrcom 246 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ = 0s โ (๐ โ โช (๐
โ ฯ) โ
1s <s (((๐
ยทs ๐)
+s (๐ด
ยทs ๐))
-s (๐
ยทs ๐))))) |
454 | 144 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐
โ ฯ))) โ
1s โ No ) |
455 | 249 | ad2antrl 725 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐
โ ฯ))) โ ๐ โ
No ) |
456 | 134 | adantrl 713 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐
โ ฯ))) โ ๐ โ
No ) |
457 | 455, 456 | mulscld 27831 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐
โ ฯ))) โ
(๐ ยทs
๐) โ No ) |
458 | 442 | adantrl 713 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐
โ ฯ))) โ
(๐ด ยทs
๐) โ No ) |
459 | 454, 457,
458 | addsubsassd 27788 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐
โ ฯ))) โ ((
1s +s (๐ ยทs ๐)) -s (๐ด ยทs ๐)) = ( 1s +s ((๐ ยทs ๐) -s (๐ด ยทs ๐)))) |
460 | 2 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐
โ ฯ))) โ ๐ด โ
No ) |
461 | 455, 460,
456 | subsdird 27854 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐
โ ฯ))) โ
((๐ -s ๐ด) ยทs ๐) = ((๐ ยทs ๐) -s (๐ด ยทs ๐))) |
462 | 461 | oveq2d 7428 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐
โ ฯ))) โ (
1s +s ((๐ -s ๐ด) ยทs ๐)) = ( 1s +s ((๐ ยทs ๐) -s (๐ด ยทs ๐)))) |
463 | 459, 462 | eqtr4d 2774 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐
โ ฯ))) โ ((
1s +s (๐ ยทs ๐)) -s (๐ด ยทs ๐)) = ( 1s +s ((๐ -s ๐ด) ยทs ๐))) |
464 | 191 | simp2d 1142 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โช (๐ฟ
โ ฯ) <<s {(โช (๐ฟ โ ฯ) |s โช (๐
โ ฯ))}) |
465 | 464 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐
โ ฯ))) โ โช (๐ฟ
โ ฯ) <<s {(โช (๐ฟ โ ฯ) |s โช (๐
โ ฯ))}) |
466 | 198 | ad2antrl 725 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โง (๐ โ ฯ โง ๐ โ (๐
โ๐))) โ suc ๐ โ ฯ) |
467 | 201 | oveq1d 7427 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (๐ฅ๐ฟ = ๐ โ ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐
) = ((๐ -s ๐ด) ยทs ๐ฆ๐
)) |
468 | 467 | oveq2d 7428 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (๐ฅ๐ฟ = ๐ โ ( 1s
+s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐
)) = (
1s +s ((๐ -s ๐ด) ยทs ๐ฆ๐
))) |
469 | 468, 204 | oveq12d 7430 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (๐ฅ๐ฟ = ๐ โ (( 1s
+s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐
))
/su ๐ฅ๐ฟ) = (( 1s
+s ((๐
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐)) |
470 | 469 | eqeq2d 2742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ฅ๐ฟ = ๐ โ ((( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐) = ((
1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐
))
/su ๐ฅ๐ฟ) โ (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐) = ((
1s +s ((๐ -s ๐ด) ยทs ๐ฆ๐
)) /su
๐))) |
471 | 470, 314 | rspc2ev 3624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ (๐
โ๐) โง (( 1s +s
((๐ -s ๐ด) ยทs ๐)) /su ๐) = (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐))
โ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐
โ (๐
โ๐)(( 1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐ฟ)) |
472 | 200, 471 | mp3an3 1449 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ (๐
โ๐)) โ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐
โ (๐
โ๐)(( 1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐ฟ)) |
473 | 472 | ad2ant2l 743 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ โง ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โง (๐ โ ฯ โง ๐ โ (๐
โ๐))) โ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐
โ (๐
โ๐)(( 1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐ฟ)) |
474 | | eqeq1 2735 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ = (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐)
โ (๐ = ((
1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐
))
/su ๐ฅ๐ฟ) โ (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐) = ((
1s +s ((๐ฅ๐ฟ -s ๐ด) ยทs ๐ฆ๐
))
/su ๐ฅ๐ฟ))) |
475 | 474 | 2rexbidv 3218 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ = (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐)
โ (โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐
โ (๐
โ๐)๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐ฟ)
โ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐
โ (๐
โ๐)(( 1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐ฟ))) |
476 | 214, 475 | elab 3668 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ {๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐
โ (๐
โ๐)๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐ฟ)}
โ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐
โ (๐
โ๐)(( 1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐ฟ)) |
477 | 473, 476 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โง ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โง (๐ โ ฯ โง ๐ โ (๐
โ๐))) โ (( 1s +s
((๐ -s ๐ด) ยทs ๐)) /su ๐) โ {๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐
โ (๐
โ๐)๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐ฟ)}) |
478 | | elun2 4177 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ {๐ โฃ โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐
โ (๐
โ๐)๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐ฟ)}
โ (( 1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ ({๐ โฃ โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐ฟ โ (๐ฟโ๐)๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐
)}
โช {๐ โฃ
โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐
โ (๐
โ๐)๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐ฟ)})) |
479 | | elun2 4177 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ ({๐ โฃ โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐ฟ โ (๐ฟโ๐)๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐
)}
โช {๐ โฃ
โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐
โ (๐
โ๐)๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐ฟ)})
โ (( 1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ ((๐ฟโ๐) โช ({๐ โฃ โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐ฟ โ (๐ฟโ๐)๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐
)}
โช {๐ โฃ
โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐
โ (๐
โ๐)๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐ฟ)}))) |
480 | 477, 478,
479 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โง ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โง (๐ โ ฯ โง ๐ โ (๐
โ๐))) โ (( 1s +s
((๐ -s ๐ด) ยทs ๐)) /su ๐) โ ((๐ฟโ๐) โช ({๐ โฃ โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐ฟ โ (๐ฟโ๐)๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐
)}
โช {๐ โฃ
โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐
โ (๐
โ๐)๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐ฟ)}))) |
481 | 11, 12, 13 | precsexlem4 27896 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ ฯ โ (๐ฟโsuc ๐) = ((๐ฟโ๐) โช ({๐ โฃ โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐ฟ โ (๐ฟโ๐)๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐
)}
โช {๐ โฃ
โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐
โ (๐
โ๐)๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐ฟ)}))) |
482 | 481 | ad2antrl 725 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โง ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โง (๐ โ ฯ โง ๐ โ (๐
โ๐))) โ (๐ฟโsuc ๐) = ((๐ฟโ๐) โช ({๐ โฃ โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐ฟ โ (๐ฟโ๐)๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐
)}
โช {๐ โฃ
โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐
โ (๐
โ๐)๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐ฟ)}))) |
483 | 480, 482 | eleqtrrd 2835 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โง (๐ โ ฯ โง ๐ โ (๐
โ๐))) โ (( 1s +s
((๐ -s ๐ด) ยทs ๐)) /su ๐) โ (๐ฟโsuc ๐)) |
484 | | fveq2 6891 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ = suc ๐ โ (๐ฟโ๐) = (๐ฟโsuc ๐)) |
485 | 484 | eleq2d 2818 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ = suc ๐ โ ((( 1s +s
((๐ -s ๐ด) ยทs ๐)) /su ๐) โ (๐ฟโ๐) โ (( 1s +s
((๐ -s ๐ด) ยทs ๐)) /su ๐) โ (๐ฟโsuc ๐))) |
486 | 485 | rspcev 3612 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((suc
๐ โ ฯ โง ((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ (๐ฟโsuc ๐)) โ โ๐ โ ฯ (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐)
โ (๐ฟโ๐)) |
487 | 466, 483,
486 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โง (๐ โ ฯ โง ๐ โ (๐
โ๐))) โ โ๐ โ ฯ (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐)
โ (๐ฟโ๐)) |
488 | 487 | rexlimdvaa 3155 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โ (โ๐ โ ฯ ๐ โ (๐
โ๐) โ โ๐ โ ฯ (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐)
โ (๐ฟโ๐))) |
489 | | eliun 5001 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ โช
๐ โ ฯ (๐ฟโ๐) โ โ๐ โ ฯ (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐)
โ (๐ฟโ๐)) |
490 | | funiunfv 7250 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (Fun
๐ฟ โ โช ๐ โ ฯ (๐ฟโ๐) = โช (๐ฟ โ
ฯ)) |
491 | 43, 490 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
โข โช ๐ โ ฯ (๐ฟโ๐) = โช (๐ฟ โ
ฯ) |
492 | 491 | eleq2i 2824 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ โช
๐ โ ฯ (๐ฟโ๐) โ (( 1s +s
((๐ -s ๐ด) ยทs ๐)) /su ๐) โ โช (๐ฟ
โ ฯ)) |
493 | 489, 492 | bitr3i 277 |
. . . . . . . . . . . . . . . . . . . 20
โข
(โ๐ โ
ฯ (( 1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ (๐ฟโ๐) โ (( 1s +s
((๐ -s ๐ด) ยทs ๐)) /su ๐) โ โช (๐ฟ
โ ฯ)) |
494 | 488, 332,
493 | 3imtr3g 295 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โ (๐ โ โช (๐
โ ฯ) โ ((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ โช (๐ฟ โ
ฯ))) |
495 | 494 | impr 454 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐
โ ฯ))) โ ((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ โช (๐ฟ โ
ฯ)) |
496 | 196 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐
โ ฯ))) โ ๐ โ {(โช (๐ฟ
โ ฯ) |s โช (๐
โ ฯ))}) |
497 | 465, 495,
496 | ssltsepcd 27533 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐
โ ฯ))) โ ((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) <s ๐) |
498 | 252 | adantrr 714 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐
โ ฯ))) โ
(๐ -s ๐ด) โ
No ) |
499 | 498, 456 | mulscld 27831 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐
โ ฯ))) โ
((๐ -s ๐ด) ยทs ๐) โ
No ) |
500 | 454, 499 | addscld 27703 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐
โ ฯ))) โ (
1s +s ((๐ -s ๐ด) ยทs ๐)) โ No
) |
501 | 56 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐
โ ฯ))) โ ๐ โ
No ) |
502 | 260 | ad2antrl 725 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐
โ ฯ))) โ
0s <s ๐) |
503 | 274 | adantrr 714 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐
โ ฯ))) โ
โ๐ฆ โ No (๐ ยทs ๐ฆ) = 1s ) |
504 | 500, 501,
455, 502, 503 | sltdivmulwd 27886 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐
โ ฯ))) โ (((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) <s ๐ โ ( 1s +s
((๐ -s ๐ด) ยทs ๐)) <s (๐ ยทs ๐))) |
505 | 497, 504 | mpbid 231 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐
โ ฯ))) โ (
1s +s ((๐ -s ๐ด) ยทs ๐)) <s (๐ ยทs ๐)) |
506 | 463, 505 | eqbrtrd 5170 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐
โ ฯ))) โ ((
1s +s (๐ ยทs ๐)) -s (๐ด ยทs ๐)) <s (๐ ยทs ๐)) |
507 | 454, 457 | addscld 27703 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐
โ ฯ))) โ (
1s +s (๐ ยทs ๐)) โ No
) |
508 | 287 | adantrr 714 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐
โ ฯ))) โ
(๐ ยทs
๐) โ No ) |
509 | 507, 458,
508 | sltsubaddd 27796 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐
โ ฯ))) โ (((
1s +s (๐ ยทs ๐)) -s (๐ด ยทs ๐)) <s (๐ ยทs ๐) โ ( 1s +s
(๐ ยทs
๐)) <s ((๐ ยทs ๐) +s (๐ด ยทs ๐)))) |
510 | 508, 458 | addscld 27703 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐
โ ฯ))) โ
((๐ ยทs
๐) +s (๐ด ยทs ๐)) โ
No ) |
511 | 454, 457,
510 | sltaddsubd 27798 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐
โ ฯ))) โ ((
1s +s (๐ ยทs ๐)) <s ((๐ ยทs ๐) +s (๐ด ยทs ๐)) โ 1s <s (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)))) |
512 | 509, 511 | bitrd 279 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐
โ ฯ))) โ (((
1s +s (๐ ยทs ๐)) -s (๐ด ยทs ๐)) <s (๐ ยทs ๐) โ 1s <s (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)))) |
513 | 506, 512 | mpbid 231 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โง ๐ โ โช (๐
โ ฯ))) โ
1s <s (((๐
ยทs ๐)
+s (๐ด
ยทs ๐))
-s (๐
ยทs ๐))) |
514 | 513 | exp32 420 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ} โ (๐ โ โช (๐
โ ฯ) โ
1s <s (((๐
ยทs ๐)
+s (๐ด
ยทs ๐))
-s (๐
ยทs ๐))))) |
515 | 453, 514 | jaod 856 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ = 0s โจ ๐ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s ๐ฅ}) โ (๐ โ โช (๐
โ ฯ) โ
1s <s (((๐
ยทs ๐)
+s (๐ด
ยทs ๐))
-s (๐
ยทs ๐))))) |
516 | 159, 515 | biimtrid 241 |
. . . . . . . . . . 11
โข (๐ โ (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โ (๐ โ โช (๐
โ ฯ) โ 1s <s (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))))) |
517 | 516 | imp32 418 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โง ๐ โ โช (๐
โ ฯ))) โ 1s <s (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) |
518 | | breq2 5152 |
. . . . . . . . . 10
โข (๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ ( 1s <s ๐ โ 1s <s
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)))) |
519 | 517, 518 | syl5ibrcom 246 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}) โง ๐ โ โช (๐
โ ฯ))) โ (๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ 1s <s ๐)) |
520 | 519 | rexlimdvva 3210 |
. . . . . . . 8
โข (๐ โ (โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ 1s <s
๐)) |
521 | 144 | a1i 11 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ
1s โ No ) |
522 | 521, 414,
412 | addsubsassd 27788 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ ((
1s +s (๐ ยทs ๐)) -s (๐ด ยทs ๐)) = ( 1s +s ((๐ ยทs ๐) -s (๐ด ยทs ๐)))) |
523 | 407, 410,
411 | subsdird 27854 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ
((๐ -s ๐ด) ยทs ๐) = ((๐ ยทs ๐) -s (๐ด ยทs ๐))) |
524 | 523 | oveq2d 7428 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ (
1s +s ((๐ -s ๐ด) ยทs ๐)) = ( 1s +s ((๐ ยทs ๐) -s (๐ด ยทs ๐)))) |
525 | 522, 524 | eqtr4d 2774 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ ((
1s +s (๐ ยทs ๐)) -s (๐ด ยทs ๐)) = ( 1s +s ((๐ -s ๐ด) ยทs ๐))) |
526 | 464 | adantr 480 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ โช (๐ฟ
โ ฯ) <<s {(โช (๐ฟ โ ฯ) |s โช (๐
โ ฯ))}) |
527 | 198 | ad2antrl 725 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ โ ( R โ๐ด)) โง (๐ โ ฯ โง ๐ โ (๐ฟโ๐))) โ suc ๐ โ ฯ) |
528 | 305 | oveq1d 7427 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ฅ๐
= ๐ โ ((๐ฅ๐
-s ๐ด) ยทs ๐ฆ๐ฟ) = ((๐ -s ๐ด) ยทs ๐ฆ๐ฟ)) |
529 | 528 | oveq2d 7428 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ฅ๐
= ๐ โ ( 1s
+s ((๐ฅ๐
-s ๐ด) ยทs ๐ฆ๐ฟ)) = (
1s +s ((๐ -s ๐ด) ยทs ๐ฆ๐ฟ))) |
530 | 529, 308 | oveq12d 7430 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ฅ๐
= ๐ โ (( 1s
+s ((๐ฅ๐
-s ๐ด) ยทs ๐ฆ๐ฟ))
/su ๐ฅ๐
) = (( 1s
+s ((๐
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐)) |
531 | 530 | eqeq2d 2742 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ฅ๐
= ๐ โ ((( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐) = ((
1s +s ((๐ฅ๐
-s ๐ด) ยทs ๐ฆ๐ฟ))
/su ๐ฅ๐
) โ (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐) = ((
1s +s ((๐ -s ๐ด) ยทs ๐ฆ๐ฟ)) /su
๐))) |
532 | 531, 210 | rspc2ev 3624 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โ ( R โ๐ด) โง ๐ โ (๐ฟโ๐) โง (( 1s +s
((๐ -s ๐ด) ยทs ๐)) /su ๐) = (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐))
โ โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐ฟ โ (๐ฟโ๐)(( 1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐
)) |
533 | 200, 532 | mp3an3 1449 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โ ( R โ๐ด) โง ๐ โ (๐ฟโ๐)) โ โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐ฟ โ (๐ฟโ๐)(( 1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐
)) |
534 | 533 | ad2ant2l 743 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง ๐ โ ( R โ๐ด)) โง (๐ โ ฯ โง ๐ โ (๐ฟโ๐))) โ โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐ฟ โ (๐ฟโ๐)(( 1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐
)) |
535 | | eqeq1 2735 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ = (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐)
โ (๐ = ((
1s +s ((๐ฅ๐
-s ๐ด) ยทs ๐ฆ๐ฟ))
/su ๐ฅ๐
) โ (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐) = ((
1s +s ((๐ฅ๐
-s ๐ด) ยทs ๐ฆ๐ฟ))
/su ๐ฅ๐
))) |
536 | 535 | 2rexbidv 3218 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ = (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐)
โ (โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐ฟ โ (๐ฟโ๐)๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐
)
โ โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐ฟ โ (๐ฟโ๐)(( 1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐
))) |
537 | 214, 536 | elab 3668 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ {๐ โฃ โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐ฟ โ (๐ฟโ๐)๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐
)}
โ โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐ฟ โ (๐ฟโ๐)(( 1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐
)) |
538 | 534, 537 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ โ ( R โ๐ด)) โง (๐ โ ฯ โง ๐ โ (๐ฟโ๐))) โ (( 1s +s
((๐ -s ๐ด) ยทs ๐)) /su ๐) โ {๐ โฃ โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐ฟ โ (๐ฟโ๐)๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐
)}) |
539 | | elun1 4176 |
. . . . . . . . . . . . . . . . . . . 20
โข (((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ {๐ โฃ โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐ฟ โ (๐ฟโ๐)๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐
)}
โ (( 1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ ({๐ โฃ โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐ฟ โ (๐ฟโ๐)๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐
)}
โช {๐ โฃ
โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐
โ (๐
โ๐)๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐ฟ)})) |
540 | 538, 539,
479 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ โ ( R โ๐ด)) โง (๐ โ ฯ โง ๐ โ (๐ฟโ๐))) โ (( 1s +s
((๐ -s ๐ด) ยทs ๐)) /su ๐) โ ((๐ฟโ๐) โช ({๐ โฃ โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐ฟ โ (๐ฟโ๐)๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐
)}
โช {๐ โฃ
โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐
โ (๐
โ๐)๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐ฟ)}))) |
541 | 481 | ad2antrl 725 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ โ ( R โ๐ด)) โง (๐ โ ฯ โง ๐ โ (๐ฟโ๐))) โ (๐ฟโsuc ๐) = ((๐ฟโ๐) โช ({๐ โฃ โ๐ฅ๐
โ ( R โ๐ด)โ๐ฆ๐ฟ โ (๐ฟโ๐)๐ = (( 1s +s ((๐ฅ๐
-s ๐ด)
ยทs ๐ฆ๐ฟ)) /su
๐ฅ๐
)}
โช {๐ โฃ
โ๐ฅ๐ฟ โ {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ}โ๐ฆ๐
โ (๐
โ๐)๐ = (( 1s +s ((๐ฅ๐ฟ
-s ๐ด)
ยทs ๐ฆ๐
)) /su
๐ฅ๐ฟ)}))) |
542 | 540, 541 | eleqtrrd 2835 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ โ ( R โ๐ด)) โง (๐ โ ฯ โง ๐ โ (๐ฟโ๐))) โ (( 1s +s
((๐ -s ๐ด) ยทs ๐)) /su ๐) โ (๐ฟโsuc ๐)) |
543 | 527, 542,
486 | syl2anc 583 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ โ ( R โ๐ด)) โง (๐ โ ฯ โง ๐ โ (๐ฟโ๐))) โ โ๐ โ ฯ (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐)
โ (๐ฟโ๐)) |
544 | 543 | rexlimdvaa 3155 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ ( R โ๐ด)) โ (โ๐ โ ฯ ๐ โ (๐ฟโ๐) โ โ๐ โ ฯ (( 1s
+s ((๐
-s ๐ด)
ยทs ๐))
/su ๐)
โ (๐ฟโ๐))) |
545 | 544, 177,
493 | 3imtr3g 295 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ ( R โ๐ด)) โ (๐ โ โช (๐ฟ โ ฯ) โ ((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ โช (๐ฟ โ
ฯ))) |
546 | 545 | impr 454 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ ((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) โ โช (๐ฟ โ
ฯ)) |
547 | 196 | a1i 11 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ ๐ โ {(โช (๐ฟ
โ ฯ) |s โช (๐
โ ฯ))}) |
548 | 526, 546,
547 | ssltsepcd 27533 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ ((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) <s ๐) |
549 | 338 | adantrr 714 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ
(๐ -s ๐ด) โ
No ) |
550 | 549, 411 | mulscld 27831 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ
((๐ -s ๐ด) ยทs ๐) โ
No ) |
551 | 521, 550 | addscld 27703 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ (
1s +s ((๐ -s ๐ด) ยทs ๐)) โ No
) |
552 | 349 | adantrr 714 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ
0s <s ๐) |
553 | 355 | adantrr 714 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ
โ๐ฆ โ No (๐ ยทs ๐ฆ) = 1s ) |
554 | 551, 408,
407, 552, 553 | sltdivmulwd 27886 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ (((
1s +s ((๐ -s ๐ด) ยทs ๐)) /su ๐) <s ๐ โ ( 1s +s
((๐ -s ๐ด) ยทs ๐)) <s (๐ ยทs ๐))) |
555 | 548, 554 | mpbid 231 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ (
1s +s ((๐ -s ๐ด) ยทs ๐)) <s (๐ ยทs ๐)) |
556 | 525, 555 | eqbrtrd 5170 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ ((
1s +s (๐ ยทs ๐)) -s (๐ด ยทs ๐)) <s (๐ ยทs ๐)) |
557 | 521, 414 | addscld 27703 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ (
1s +s (๐ ยทs ๐)) โ No
) |
558 | 557, 412,
409 | sltsubaddd 27796 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ (((
1s +s (๐ ยทs ๐)) -s (๐ด ยทs ๐)) <s (๐ ยทs ๐) โ ( 1s +s
(๐ ยทs
๐)) <s ((๐ ยทs ๐) +s (๐ด ยทs ๐)))) |
559 | 521, 414,
413 | sltaddsubd 27798 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ ((
1s +s (๐ ยทs ๐)) <s ((๐ ยทs ๐) +s (๐ด ยทs ๐)) โ 1s <s (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)))) |
560 | 558, 559 | bitrd 279 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ (((
1s +s (๐ ยทs ๐)) -s (๐ด ยทs ๐)) <s (๐ ยทs ๐) โ 1s <s (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)))) |
561 | 556, 560 | mpbid 231 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ
1s <s (((๐
ยทs ๐)
+s (๐ด
ยทs ๐))
-s (๐
ยทs ๐))) |
562 | 561, 518 | syl5ibrcom 246 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ โช (๐ฟ โ ฯ))) โ
(๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ 1s <s ๐)) |
563 | 562 | rexlimdvva 3210 |
. . . . . . . 8
โข (๐ โ (โ๐ โ ( R โ๐ด)โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ 1s <s ๐)) |
564 | 520, 563 | jaod 856 |
. . . . . . 7
โข (๐ โ ((โ๐ โ ({ 0s } โช
{๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โจ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) โ 1s <s ๐)) |
565 | 428, 564 | biimtrid 241 |
. . . . . 6
โข (๐ โ (๐ โ ({๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))}) โ 1s <s ๐)) |
566 | | velsn 4644 |
. . . . . . 7
โข (๐ โ { 1s } โ
๐ = 1s
) |
567 | | breq1 5151 |
. . . . . . . 8
โข (๐ = 1s โ (๐ <s ๐ โ 1s <s ๐)) |
568 | 567 | imbi2d 340 |
. . . . . . 7
โข (๐ = 1s โ ((๐ โ ({๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))}) โ ๐ <s ๐) โ (๐ โ ({๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))}) โ 1s <s ๐))) |
569 | 566, 568 | sylbi 216 |
. . . . . 6
โข (๐ โ { 1s } โ
((๐ โ ({๐ โฃ โ๐ โ ({ 0s } โช
{๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))}) โ ๐ <s ๐) โ (๐ โ ({๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))}) โ 1s <s ๐))) |
570 | 565, 569 | syl5ibrcom 246 |
. . . . 5
โข (๐ โ (๐ โ { 1s } โ (๐ โ ({๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))}) โ ๐ <s ๐))) |
571 | 570 | 3imp 1110 |
. . . 4
โข ((๐ โง ๐ โ { 1s } โง ๐ โ ({๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))})) โ ๐ <s ๐) |
572 | 105, 394,
146, 419, 571 | ssltd 27530 |
. . 3
โข (๐ โ { 1s }
<<s ({๐ โฃ
โ๐ โ ({
0s } โช {๐ฅ
โ ( L โ๐ด)
โฃ 0s <s ๐ฅ})โ๐ โ โช (๐
โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))})) |
573 | 81, 379, 572 | cuteq1 27572 |
. 2
โข (๐ โ (({๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐ฟ
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐
โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))}) |s ({๐ โฃ โ๐ โ ({ 0s } โช {๐ฅ โ ( L โ๐ด) โฃ 0s <s
๐ฅ})โ๐ โ โช (๐
โ ฯ)๐ =
(((๐ ยทs
๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ( R โ๐ด)โ๐ โ โช (๐ฟ โ ฯ)๐ = (((๐ ยทs ๐) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))})) = 1s ) |
574 | 19, 573 | eqtrd 2771 |
1
โข (๐ โ (๐ด ยทs ๐) = 1s ) |