Step | Hyp | Ref
| Expression |
1 | | totbndbnd 36294 |
. 2
β’ (π· β (TotBndβπ) β π· β (Bndβπ)) |
2 | | rpcn 12930 |
. . . . . . . . . 10
β’ (π β β+
β π β
β) |
3 | 2 | adantl 483 |
. . . . . . . . 9
β’ ((π· β (Bndβπ) β§ π β β+) β π β
β) |
4 | | gzcn 16809 |
. . . . . . . . 9
β’ (π§ β β€[i] β π§ β
β) |
5 | | mulcl 11140 |
. . . . . . . . 9
β’ ((π β β β§ π§ β β) β (π Β· π§) β β) |
6 | 3, 4, 5 | syl2an 597 |
. . . . . . . 8
β’ (((π· β (Bndβπ) β§ π β β+) β§ π§ β β€[i]) β
(π Β· π§) β
β) |
7 | 6 | fmpttd 7064 |
. . . . . . 7
β’ ((π· β (Bndβπ) β§ π β β+) β (π§ β β€[i] β¦
(π Β· π§)):β€[i]βΆβ) |
8 | 7 | frnd 6677 |
. . . . . 6
β’ ((π· β (Bndβπ) β§ π β β+) β ran
(π§ β β€[i]
β¦ (π Β· π§)) β
β) |
9 | | cnex 11137 |
. . . . . . 7
β’ β
β V |
10 | 9 | elpw2 5303 |
. . . . . 6
β’ (ran
(π§ β β€[i]
β¦ (π Β· π§)) β π« β
β ran (π§ β
β€[i] β¦ (π
Β· π§)) β
β) |
11 | 8, 10 | sylibr 233 |
. . . . 5
β’ ((π· β (Bndβπ) β§ π β β+) β ran
(π§ β β€[i]
β¦ (π Β· π§)) β π«
β) |
12 | | cnmet 24151 |
. . . . . . . . . . . . . . . . 17
β’ (abs
β β ) β (Metββ) |
13 | | cntotbnd.d |
. . . . . . . . . . . . . . . . . 18
β’ π· = ((abs β β )
βΎ (π Γ π)) |
14 | 13 | bnd2lem 36296 |
. . . . . . . . . . . . . . . . 17
β’ (((abs
β β ) β (Metββ) β§ π· β (Bndβπ)) β π β β) |
15 | 12, 14 | mpan 689 |
. . . . . . . . . . . . . . . 16
β’ (π· β (Bndβπ) β π β β) |
16 | 15 | sselda 3945 |
. . . . . . . . . . . . . . 15
β’ ((π· β (Bndβπ) β§ π¦ β π) β π¦ β β) |
17 | 16 | adantrl 715 |
. . . . . . . . . . . . . 14
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β π¦ β β) |
18 | 17 | recld 15085 |
. . . . . . . . . . . . 13
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β (ββπ¦) β β) |
19 | | simprl 770 |
. . . . . . . . . . . . 13
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β π β β+) |
20 | 18, 19 | rerpdivcld 12993 |
. . . . . . . . . . . 12
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β ((ββπ¦) / π) β β) |
21 | | halfre 12372 |
. . . . . . . . . . . 12
β’ (1 / 2)
β β |
22 | | readdcl 11139 |
. . . . . . . . . . . 12
β’
((((ββπ¦)
/ π) β β β§
(1 / 2) β β) β (((ββπ¦) / π) + (1 / 2)) β β) |
23 | 20, 21, 22 | sylancl 587 |
. . . . . . . . . . 11
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β (((ββπ¦) / π) + (1 / 2)) β β) |
24 | 23 | flcld 13709 |
. . . . . . . . . 10
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
(ββ(((ββπ¦) / π) + (1 / 2))) β
β€) |
25 | 17 | imcld 15086 |
. . . . . . . . . . . . 13
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β (ββπ¦) β β) |
26 | 25, 19 | rerpdivcld 12993 |
. . . . . . . . . . . 12
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β ((ββπ¦) / π) β β) |
27 | | readdcl 11139 |
. . . . . . . . . . . 12
β’
((((ββπ¦)
/ π) β β β§
(1 / 2) β β) β (((ββπ¦) / π) + (1 / 2)) β β) |
28 | 26, 21, 27 | sylancl 587 |
. . . . . . . . . . 11
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β (((ββπ¦) / π) + (1 / 2)) β β) |
29 | 28 | flcld 13709 |
. . . . . . . . . 10
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
(ββ(((ββπ¦) / π) + (1 / 2))) β
β€) |
30 | | gzreim 16816 |
. . . . . . . . . 10
β’
(((ββ(((ββπ¦) / π) + (1 / 2))) β β€ β§
(ββ(((ββπ¦) / π) + (1 / 2))) β β€) β
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β
β€[i]) |
31 | 24, 29, 30 | syl2anc 585 |
. . . . . . . . 9
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β
β€[i]) |
32 | | gzcn 16809 |
. . . . . . . . . . . . . . 15
β’
(((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β β€[i] β
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β
β) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β
β) |
34 | 19 | rpcnd 12964 |
. . . . . . . . . . . . . . 15
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β π β β) |
35 | 19 | rpne0d 12967 |
. . . . . . . . . . . . . . 15
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β π β 0) |
36 | 17, 34, 35 | divcld 11936 |
. . . . . . . . . . . . . 14
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β (π¦ / π) β β) |
37 | 33, 36 | subcld 11517 |
. . . . . . . . . . . . 13
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
(((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β (π¦ / π)) β β) |
38 | 37 | abscld 15327 |
. . . . . . . . . . . 12
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
(absβ(((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β (π¦ / π))) β β) |
39 | | 1re 11160 |
. . . . . . . . . . . . 13
β’ 1 β
β |
40 | 39 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β 1 β β) |
41 | 24 | zcnd 12613 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
(ββ(((ββπ¦) / π) + (1 / 2))) β
β) |
42 | | ax-icn 11115 |
. . . . . . . . . . . . . . . . . . . . 21
β’ i β
β |
43 | 29 | zcnd 12613 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
(ββ(((ββπ¦) / π) + (1 / 2))) β
β) |
44 | | mulcl 11140 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((i
β β β§ (ββ(((ββπ¦) / π) + (1 / 2))) β β) β (i
Β· (ββ(((ββπ¦) / π) + (1 / 2)))) β
β) |
45 | 42, 43, 44 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β (i Β·
(ββ(((ββπ¦) / π) + (1 / 2)))) β
β) |
46 | 20 | recnd 11188 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β ((ββπ¦) / π) β β) |
47 | 26 | recnd 11188 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β ((ββπ¦) / π) β β) |
48 | | mulcl 11140 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((i
β β β§ ((ββπ¦) / π) β β) β (i Β·
((ββπ¦) / π)) β
β) |
49 | 42, 47, 48 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β (i Β· ((ββπ¦) / π)) β β) |
50 | 41, 45, 46, 49 | addsub4d 11564 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
(((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β (((ββπ¦) / π) + (i Β· ((ββπ¦) / π)))) = (((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)) + ((i Β·
(ββ(((ββπ¦) / π) + (1 / 2)))) β (i Β·
((ββπ¦) / π))))) |
51 | 36 | replimd 15088 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β (π¦ / π) = ((ββ(π¦ / π)) + (i Β· (ββ(π¦ / π))))) |
52 | 19 | rpred 12962 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β π β β) |
53 | 52, 17, 35 | redivd 15120 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β (ββ(π¦ / π)) = ((ββπ¦) / π)) |
54 | 52, 17, 35 | imdivd 15121 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β (ββ(π¦ / π)) = ((ββπ¦) / π)) |
55 | 54 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β (i Β· (ββ(π¦ / π))) = (i Β· ((ββπ¦) / π))) |
56 | 53, 55 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β ((ββ(π¦ / π)) + (i Β· (ββ(π¦ / π)))) = (((ββπ¦) / π) + (i Β· ((ββπ¦) / π)))) |
57 | 51, 56 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β (π¦ / π) = (((ββπ¦) / π) + (i Β· ((ββπ¦) / π)))) |
58 | 57 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
(((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β (π¦ / π)) = (((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β (((ββπ¦) / π) + (i Β· ((ββπ¦) / π))))) |
59 | 42 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β i β β) |
60 | 59, 43, 47 | subdid 11616 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β (i Β·
((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π))) = ((i Β·
(ββ(((ββπ¦) / π) + (1 / 2)))) β (i Β·
((ββπ¦) / π)))) |
61 | 60 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
(((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)) + (i Β·
((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)))) = (((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)) + ((i Β·
(ββ(((ββπ¦) / π) + (1 / 2)))) β (i Β·
((ββπ¦) / π))))) |
62 | 50, 58, 61 | 3eqtr4d 2783 |
. . . . . . . . . . . . . . . . . 18
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
(((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β (π¦ / π)) = (((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)) + (i Β·
((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π))))) |
63 | 62 | fveq2d 6847 |
. . . . . . . . . . . . . . . . 17
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
(absβ(((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β (π¦ / π))) =
(absβ(((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)) + (i Β·
((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)))))) |
64 | 63 | oveq1d 7373 |
. . . . . . . . . . . . . . . 16
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
((absβ(((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β (π¦ / π)))β2) =
((absβ(((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)) + (i Β·
((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)))))β2)) |
65 | 24 | zred 12612 |
. . . . . . . . . . . . . . . . . 18
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
(ββ(((ββπ¦) / π) + (1 / 2))) β
β) |
66 | 65, 20 | resubcld 11588 |
. . . . . . . . . . . . . . . . 17
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)) β β) |
67 | 29 | zred 12612 |
. . . . . . . . . . . . . . . . . 18
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
(ββ(((ββπ¦) / π) + (1 / 2))) β
β) |
68 | 67, 26 | resubcld 11588 |
. . . . . . . . . . . . . . . . 17
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)) β β) |
69 | | absreimsq 15183 |
. . . . . . . . . . . . . . . . 17
β’
((((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)) β β β§
((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)) β β) β
((absβ(((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)) + (i Β·
((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)))))β2) =
((((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π))β2) +
(((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π))β2))) |
70 | 66, 68, 69 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
((absβ(((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)) + (i Β·
((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)))))β2) =
((((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π))β2) +
(((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π))β2))) |
71 | 64, 70 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
((absβ(((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β (π¦ / π)))β2) =
((((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π))β2) +
(((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π))β2))) |
72 | 66 | resqcld 14036 |
. . . . . . . . . . . . . . . 16
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
(((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π))β2) β β) |
73 | 68 | resqcld 14036 |
. . . . . . . . . . . . . . . 16
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
(((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π))β2) β β) |
74 | 21 | resqcli 14096 |
. . . . . . . . . . . . . . . . . 18
β’ ((1 /
2)β2) β β |
75 | 74 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β ((1 / 2)β2) β
β) |
76 | 21 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β (1 / 2) β
β) |
77 | | absresq 15193 |
. . . . . . . . . . . . . . . . . . 19
β’
(((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)) β β β
((absβ((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)))β2) =
(((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π))β2)) |
78 | 66, 77 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
((absβ((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)))β2) =
(((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π))β2)) |
79 | | rddif 15231 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((ββπ¦) /
π) β β β
(absβ((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π))) β€ (1 / 2)) |
80 | 20, 79 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
(absβ((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π))) β€ (1 / 2)) |
81 | 66 | recnd 11188 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)) β β) |
82 | 81 | abscld 15327 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
(absβ((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π))) β β) |
83 | 81 | absge0d 15335 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β 0 β€
(absβ((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)))) |
84 | | halfgt0 12374 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 0 < (1
/ 2) |
85 | 21, 84 | elrpii 12923 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (1 / 2)
β β+ |
86 | | rpge0 12933 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((1 / 2)
β β+ β 0 β€ (1 / 2)) |
87 | 85, 86 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β 0 β€ (1 / 2)) |
88 | 82, 76, 83, 87 | le2sqd 14166 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
((absβ((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π))) β€ (1 / 2) β
((absβ((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)))β2) β€ ((1 /
2)β2))) |
89 | 80, 88 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
((absβ((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)))β2) β€ ((1 /
2)β2)) |
90 | 78, 89 | eqbrtrrd 5130 |
. . . . . . . . . . . . . . . . 17
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
(((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π))β2) β€ ((1 /
2)β2)) |
91 | | halfcn 12373 |
. . . . . . . . . . . . . . . . . . . 20
β’ (1 / 2)
β β |
92 | 91 | sqvali 14090 |
. . . . . . . . . . . . . . . . . . 19
β’ ((1 /
2)β2) = ((1 / 2) Β· (1 / 2)) |
93 | | halflt1 12376 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (1 / 2)
< 1 |
94 | 21, 39, 21, 84 | ltmul1ii 12088 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((1 / 2)
< 1 β ((1 / 2) Β· (1 / 2)) < (1 Β· (1 /
2))) |
95 | 93, 94 | mpbi 229 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((1 / 2)
Β· (1 / 2)) < (1 Β· (1 / 2)) |
96 | 91 | mulid2i 11165 |
. . . . . . . . . . . . . . . . . . . 20
β’ (1
Β· (1 / 2)) = (1 / 2) |
97 | 95, 96 | breqtri 5131 |
. . . . . . . . . . . . . . . . . . 19
β’ ((1 / 2)
Β· (1 / 2)) < (1 / 2) |
98 | 92, 97 | eqbrtri 5127 |
. . . . . . . . . . . . . . . . . 18
β’ ((1 /
2)β2) < (1 / 2) |
99 | 98 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β ((1 / 2)β2) < (1 /
2)) |
100 | 72, 75, 76, 90, 99 | lelttrd 11318 |
. . . . . . . . . . . . . . . 16
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
(((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π))β2) < (1 / 2)) |
101 | | absresq 15193 |
. . . . . . . . . . . . . . . . . . 19
β’
(((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)) β β β
((absβ((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)))β2) =
(((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π))β2)) |
102 | 68, 101 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
((absβ((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)))β2) =
(((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π))β2)) |
103 | | rddif 15231 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((ββπ¦)
/ π) β β β
(absβ((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π))) β€ (1 / 2)) |
104 | 26, 103 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
(absβ((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π))) β€ (1 / 2)) |
105 | 68 | recnd 11188 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)) β β) |
106 | 105 | abscld 15327 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
(absβ((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π))) β β) |
107 | 105 | absge0d 15335 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β 0 β€
(absβ((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)))) |
108 | 106, 76, 107, 87 | le2sqd 14166 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
((absβ((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π))) β€ (1 / 2) β
((absβ((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)))β2) β€ ((1 /
2)β2))) |
109 | 104, 108 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
((absβ((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π)))β2) β€ ((1 /
2)β2)) |
110 | 102, 109 | eqbrtrrd 5130 |
. . . . . . . . . . . . . . . . 17
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
(((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π))β2) β€ ((1 /
2)β2)) |
111 | 73, 75, 76, 110, 99 | lelttrd 11318 |
. . . . . . . . . . . . . . . 16
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
(((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π))β2) < (1 / 2)) |
112 | 72, 73, 40, 100, 111 | lt2halvesd 12406 |
. . . . . . . . . . . . . . 15
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
((((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π))β2) +
(((ββ(((ββπ¦) / π) + (1 / 2))) β ((ββπ¦) / π))β2)) < 1) |
113 | 71, 112 | eqbrtrd 5128 |
. . . . . . . . . . . . . 14
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
((absβ(((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β (π¦ / π)))β2) < 1) |
114 | | sq1 14105 |
. . . . . . . . . . . . . 14
β’
(1β2) = 1 |
115 | 113, 114 | breqtrrdi 5148 |
. . . . . . . . . . . . 13
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
((absβ(((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β (π¦ / π)))β2) < (1β2)) |
116 | 37 | absge0d 15335 |
. . . . . . . . . . . . . 14
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β 0 β€
(absβ(((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β (π¦ / π)))) |
117 | | 0le1 11683 |
. . . . . . . . . . . . . . 15
β’ 0 β€
1 |
118 | 117 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β 0 β€ 1) |
119 | 38, 40, 116, 118 | lt2sqd 14165 |
. . . . . . . . . . . . 13
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
((absβ(((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β (π¦ / π))) < 1 β
((absβ(((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β (π¦ / π)))β2) <
(1β2))) |
120 | 115, 119 | mpbird 257 |
. . . . . . . . . . . 12
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β
(absβ(((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β (π¦ / π))) < 1) |
121 | 38, 40, 19, 120 | ltmul2dd 13018 |
. . . . . . . . . . 11
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β (π Β·
(absβ(((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β (π¦ / π)))) < (π Β· 1)) |
122 | 34, 33 | mulcld 11180 |
. . . . . . . . . . . . 13
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β (π Β·
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2)))))) β
β) |
123 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ (abs
β β ) = (abs β β ) |
124 | 123 | cnmetdval 24150 |
. . . . . . . . . . . . 13
β’ (((π Β·
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2)))))) β β β§ π¦ β β) β ((π Β·
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))))(abs β β )π¦) = (absβ((π Β·
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2)))))) β π¦))) |
125 | 122, 17, 124 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β ((π Β·
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))))(abs β β )π¦) = (absβ((π Β·
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2)))))) β π¦))) |
126 | 34, 33, 36 | subdid 11616 |
. . . . . . . . . . . . . . 15
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β (π Β·
(((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β (π¦ / π))) = ((π Β·
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2)))))) β (π Β· (π¦ / π)))) |
127 | 17, 34, 35 | divcan2d 11938 |
. . . . . . . . . . . . . . . 16
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β (π Β· (π¦ / π)) = π¦) |
128 | 127 | oveq2d 7374 |
. . . . . . . . . . . . . . 15
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β ((π Β·
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2)))))) β (π Β· (π¦ / π))) = ((π Β·
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2)))))) β π¦)) |
129 | 126, 128 | eqtrd 2773 |
. . . . . . . . . . . . . 14
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β (π Β·
(((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β (π¦ / π))) = ((π Β·
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2)))))) β π¦)) |
130 | 129 | fveq2d 6847 |
. . . . . . . . . . . . 13
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β (absβ(π Β·
(((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β (π¦ / π)))) = (absβ((π Β·
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2)))))) β π¦))) |
131 | 34, 37 | absmuld 15345 |
. . . . . . . . . . . . 13
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β (absβ(π Β·
(((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β (π¦ / π)))) = ((absβπ) Β·
(absβ(((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β (π¦ / π))))) |
132 | 130, 131 | eqtr3d 2775 |
. . . . . . . . . . . 12
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β (absβ((π Β·
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2)))))) β π¦)) = ((absβπ) Β·
(absβ(((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β (π¦ / π))))) |
133 | 19 | rpge0d 12966 |
. . . . . . . . . . . . . 14
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β 0 β€ π) |
134 | 52, 133 | absidd 15313 |
. . . . . . . . . . . . 13
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β (absβπ) = π) |
135 | 134 | oveq1d 7373 |
. . . . . . . . . . . 12
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β ((absβπ) Β·
(absβ(((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β (π¦ / π)))) = (π Β·
(absβ(((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β (π¦ / π))))) |
136 | 125, 132,
135 | 3eqtrrd 2778 |
. . . . . . . . . . 11
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β (π Β·
(absβ(((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β (π¦ / π)))) = ((π Β·
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))))(abs β β )π¦)) |
137 | 34 | mulid1d 11177 |
. . . . . . . . . . 11
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β (π Β· 1) = π) |
138 | 121, 136,
137 | 3brtr3d 5137 |
. . . . . . . . . 10
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β ((π Β·
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))))(abs β β )π¦) < π) |
139 | | cnxmet 24152 |
. . . . . . . . . . . 12
β’ (abs
β β ) β (βMetββ) |
140 | 139 | a1i 11 |
. . . . . . . . . . 11
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β (abs β β ) β
(βMetββ)) |
141 | | rpxr 12929 |
. . . . . . . . . . . 12
β’ (π β β+
β π β
β*) |
142 | 141 | ad2antrl 727 |
. . . . . . . . . . 11
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β π β β*) |
143 | | elbl2 23759 |
. . . . . . . . . . 11
β’ ((((abs
β β ) β (βMetββ) β§ π β β*) β§ ((π Β·
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2)))))) β β β§ π¦ β β)) β (π¦ β ((π Β·
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))))(ballβ(abs β
β ))π) β ((π Β·
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))))(abs β β )π¦) < π)) |
144 | 140, 142,
122, 17, 143 | syl22anc 838 |
. . . . . . . . . 10
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β (π¦ β ((π Β·
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))))(ballβ(abs β
β ))π) β ((π Β·
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))))(abs β β )π¦) < π)) |
145 | 138, 144 | mpbird 257 |
. . . . . . . . 9
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β π¦ β ((π Β·
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))))(ballβ(abs β
β ))π)) |
146 | | oveq2 7366 |
. . . . . . . . . . . 12
β’ (π§ =
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β (π Β· π§) = (π Β·
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))))) |
147 | 146 | oveq1d 7373 |
. . . . . . . . . . 11
β’ (π§ =
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β ((π Β· π§)(ballβ(abs β β ))π) = ((π Β·
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))))(ballβ(abs β
β ))π)) |
148 | 147 | eleq2d 2820 |
. . . . . . . . . 10
β’ (π§ =
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β (π¦ β ((π Β· π§)(ballβ(abs β β ))π) β π¦ β ((π Β·
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))))(ballβ(abs β
β ))π))) |
149 | 148 | rspcev 3580 |
. . . . . . . . 9
β’
((((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))) β β€[i] β§ π¦ β ((π Β·
((ββ(((ββπ¦) / π) + (1 / 2))) + (i Β·
(ββ(((ββπ¦) / π) + (1 / 2))))))(ballβ(abs β
β ))π)) β
βπ§ β β€[i]
π¦ β ((π Β· π§)(ballβ(abs β β ))π)) |
150 | 31, 145, 149 | syl2anc 585 |
. . . . . . . 8
β’ ((π· β (Bndβπ) β§ (π β β+ β§ π¦ β π)) β βπ§ β β€[i] π¦ β ((π Β· π§)(ballβ(abs β β ))π)) |
151 | 150 | expr 458 |
. . . . . . 7
β’ ((π· β (Bndβπ) β§ π β β+) β (π¦ β π β βπ§ β β€[i] π¦ β ((π Β· π§)(ballβ(abs β β ))π))) |
152 | | eliun 4959 |
. . . . . . . 8
β’ (π¦ β βͺ π₯ β ran (π§ β β€[i] β¦ (π Β· π§))(π₯(ballβ(abs β β ))π) β βπ₯ β ran (π§ β β€[i] β¦ (π Β· π§))π¦ β (π₯(ballβ(abs β β ))π)) |
153 | | ovex 7391 |
. . . . . . . . . 10
β’ (π Β· π§) β V |
154 | 153 | rgenw 3065 |
. . . . . . . . 9
β’
βπ§ β
β€[i] (π Β·
π§) β
V |
155 | | eqid 2733 |
. . . . . . . . . 10
β’ (π§ β β€[i] β¦
(π Β· π§)) = (π§ β β€[i] β¦ (π Β· π§)) |
156 | | oveq1 7365 |
. . . . . . . . . . 11
β’ (π₯ = (π Β· π§) β (π₯(ballβ(abs β β ))π) = ((π Β· π§)(ballβ(abs β β ))π)) |
157 | 156 | eleq2d 2820 |
. . . . . . . . . 10
β’ (π₯ = (π Β· π§) β (π¦ β (π₯(ballβ(abs β β ))π) β π¦ β ((π Β· π§)(ballβ(abs β β ))π))) |
158 | 155, 157 | rexrnmptw 7046 |
. . . . . . . . 9
β’
(βπ§ β
β€[i] (π Β·
π§) β V β
(βπ₯ β ran (π§ β β€[i] β¦
(π Β· π§))π¦ β (π₯(ballβ(abs β β ))π) β βπ§ β β€[i] π¦ β ((π Β· π§)(ballβ(abs β β ))π))) |
159 | 154, 158 | ax-mp 5 |
. . . . . . . 8
β’
(βπ₯ β ran
(π§ β β€[i]
β¦ (π Β· π§))π¦ β (π₯(ballβ(abs β β ))π) β βπ§ β β€[i] π¦ β ((π Β· π§)(ballβ(abs β β ))π)) |
160 | 152, 159 | bitri 275 |
. . . . . . 7
β’ (π¦ β βͺ π₯ β ran (π§ β β€[i] β¦ (π Β· π§))(π₯(ballβ(abs β β ))π) β βπ§ β β€[i] π¦ β ((π Β· π§)(ballβ(abs β β ))π)) |
161 | 151, 160 | syl6ibr 252 |
. . . . . 6
β’ ((π· β (Bndβπ) β§ π β β+) β (π¦ β π β π¦ β βͺ
π₯ β ran (π§ β β€[i] β¦
(π Β· π§))(π₯(ballβ(abs β β ))π))) |
162 | 161 | ssrdv 3951 |
. . . . 5
β’ ((π· β (Bndβπ) β§ π β β+) β π β βͺ π₯ β ran (π§ β β€[i] β¦ (π Β· π§))(π₯(ballβ(abs β β ))π)) |
163 | | simpl 484 |
. . . . . . 7
β’ ((π· β (Bndβπ) β§ π β β+) β π· β (Bndβπ)) |
164 | | 0cn 11152 |
. . . . . . . 8
β’ 0 β
β |
165 | 13 | ssbnd 36293 |
. . . . . . . 8
β’ (((abs
β β ) β (Metββ) β§ 0 β β) β
(π· β (Bndβπ) β βπ β β π β (0(ballβ(abs
β β ))π))) |
166 | 12, 164, 165 | mp2an 691 |
. . . . . . 7
β’ (π· β (Bndβπ) β βπ β β π β (0(ballβ(abs
β β ))π)) |
167 | 163, 166 | sylib 217 |
. . . . . 6
β’ ((π· β (Bndβπ) β§ π β β+) β
βπ β β
π β
(0(ballβ(abs β β ))π)) |
168 | | fzfi 13883 |
. . . . . . . . 9
β’
(-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β Fin |
169 | | xpfi 9264 |
. . . . . . . . 9
β’
(((-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β Fin β§
(-((ββ((π +
π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β Fin) β
((-((ββ((π +
π) / π)) + 1)...((ββ((π + π) / π)) + 1)) Γ (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1))) β Fin) |
170 | 168, 168,
169 | mp2an 691 |
. . . . . . . 8
β’
((-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) Γ (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1))) β Fin |
171 | | eqid 2733 |
. . . . . . . . . 10
β’ (π β
(-((ββ((π +
π) / π)) + 1)...((ββ((π + π) / π)) + 1)), π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β¦ (π Β· (π + (i Β· π)))) = (π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)), π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β¦ (π Β· (π + (i Β· π)))) |
172 | | ovex 7391 |
. . . . . . . . . 10
β’ (π Β· (π + (i Β· π))) β V |
173 | 171, 172 | fnmpoi 8003 |
. . . . . . . . 9
β’ (π β
(-((ββ((π +
π) / π)) + 1)...((ββ((π + π) / π)) + 1)), π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β¦ (π Β· (π + (i Β· π)))) Fn ((-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) Γ (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1))) |
174 | | dffn4 6763 |
. . . . . . . . 9
β’ ((π β
(-((ββ((π +
π) / π)) + 1)...((ββ((π + π) / π)) + 1)), π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β¦ (π Β· (π + (i Β· π)))) Fn ((-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) Γ (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1))) β (π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)), π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β¦ (π Β· (π + (i Β· π)))):((-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) Γ (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)))βontoβran (π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)), π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β¦ (π Β· (π + (i Β· π))))) |
175 | 173, 174 | mpbi 229 |
. . . . . . . 8
β’ (π β
(-((ββ((π +
π) / π)) + 1)...((ββ((π + π) / π)) + 1)), π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β¦ (π Β· (π + (i Β· π)))):((-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) Γ (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)))βontoβran (π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)), π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β¦ (π Β· (π + (i Β· π)))) |
176 | | fofi 9285 |
. . . . . . . 8
β’
((((-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) Γ (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1))) β Fin β§ (π β
(-((ββ((π +
π) / π)) + 1)...((ββ((π + π) / π)) + 1)), π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β¦ (π Β· (π + (i Β· π)))):((-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) Γ (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)))βontoβran (π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)), π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β¦ (π Β· (π + (i Β· π))))) β ran (π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)), π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β¦ (π Β· (π + (i Β· π)))) β Fin) |
177 | 170, 175,
176 | mp2an 691 |
. . . . . . 7
β’ ran
(π β
(-((ββ((π +
π) / π)) + 1)...((ββ((π + π) / π)) + 1)), π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β¦ (π Β· (π + (i Β· π)))) β Fin |
178 | 155, 153 | elrnmpti 5916 |
. . . . . . . . . 10
β’ (π₯ β ran (π§ β β€[i] β¦ (π Β· π§)) β βπ§ β β€[i] π₯ = (π Β· π§)) |
179 | | elgz 16808 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π§ β β€[i] β (π§ β β β§
(ββπ§) β
β€ β§ (ββπ§) β β€)) |
180 | 179 | simp2bi 1147 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π§ β β€[i] β
(ββπ§) β
β€) |
181 | 180 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β (ββπ§) β
β€) |
182 | 181 | zcnd 12613 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β (ββπ§) β
β) |
183 | 182 | abscld 15327 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β
(absβ(ββπ§)) β β) |
184 | 4 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β π§ β β) |
185 | 184 | abscld 15327 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β (absβπ§) β
β) |
186 | | simpllr 775 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π· β (Bndβπ) β§ π β β+) β§ (π β β β§ π β (0(ballβ(abs
β β ))π)))
β§ π§ β β€[i])
β π β
β+) |
187 | 186 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β π β β+) |
188 | 187 | rpred 12962 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β π β β) |
189 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π· β (Bndβπ) β§ π β β+) β§ (π β β β§ π β (0(ballβ(abs
β β ))π)))
β§ π§ β β€[i])
β π β
β) |
190 | 189 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β π β β) |
191 | 188, 190 | readdcld 11189 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β (π + π) β β) |
192 | 191, 187 | rerpdivcld 12993 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β ((π + π) / π) β β) |
193 | 192 | flcld 13709 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β
(ββ((π + π) / π)) β β€) |
194 | 193 | peano2zd 12615 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β
((ββ((π + π) / π)) + 1) β β€) |
195 | 194 | zred 12612 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β
((ββ((π + π) / π)) + 1) β β) |
196 | | absrele 15199 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ β β β
(absβ(ββπ§)) β€ (absβπ§)) |
197 | 184, 196 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β
(absβ(ββπ§)) β€ (absβπ§)) |
198 | 187 | rpcnd 12964 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β π β β) |
199 | 198, 184 | absmuld 15345 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β (absβ(π Β· π§)) = ((absβπ) Β· (absβπ§))) |
200 | 187 | rpge0d 12966 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β 0 β€ π) |
201 | 188, 200 | absidd 15313 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β (absβπ) = π) |
202 | 201 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β ((absβπ) Β· (absβπ§)) = (π Β· (absβπ§))) |
203 | 199, 202 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β (absβ(π Β· π§)) = (π Β· (absβπ§))) |
204 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π· β (Bndβπ) β§ π β β+) β§ (π β β β§ π β (0(ballβ(abs
β β ))π)))
β§ π§ β β€[i])
β π β
(0(ballβ(abs β β ))π)) |
205 | | sslin 4195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (0(ballβ(abs
β β ))π) β
(((π Β· π§)(ballβ(abs β
β ))π) β© π) β (((π Β· π§)(ballβ(abs β β ))π) β© (0(ballβ(abs
β β ))π))) |
206 | 204, 205 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π· β (Bndβπ) β§ π β β+) β§ (π β β β§ π β (0(ballβ(abs
β β ))π)))
β§ π§ β β€[i])
β (((π Β· π§)(ballβ(abs β
β ))π) β© π) β (((π Β· π§)(ballβ(abs β β ))π) β© (0(ballβ(abs
β β ))π))) |
207 | 139 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π· β (Bndβπ) β§ π β β+) β§ (π β β β§ π β (0(ballβ(abs
β β ))π)))
β§ π§ β β€[i])
β (abs β β ) β
(βMetββ)) |
208 | 6 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π· β (Bndβπ) β§ π β β+) β§ (π β β β§ π β (0(ballβ(abs
β β ))π)))
β§ π§ β β€[i])
β (π Β· π§) β
β) |
209 | 164 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π· β (Bndβπ) β§ π β β+) β§ (π β β β§ π β (0(ballβ(abs
β β ))π)))
β§ π§ β β€[i])
β 0 β β) |
210 | 186 | rpxrd 12963 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π· β (Bndβπ) β§ π β β+) β§ (π β β β§ π β (0(ballβ(abs
β β ))π)))
β§ π§ β β€[i])
β π β
β*) |
211 | 189 | rexrd 11210 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π· β (Bndβπ) β§ π β β+) β§ (π β β β§ π β (0(ballβ(abs
β β ))π)))
β§ π§ β β€[i])
β π β
β*) |
212 | | bldisj 23767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((abs
β β ) β (βMetββ) β§ (π Β· π§) β β β§ 0 β β)
β§ (π β
β* β§ π
β β* β§ (π +π π) β€ ((π Β· π§)(abs β β )0))) β (((π Β· π§)(ballβ(abs β β ))π) β© (0(ballβ(abs
β β ))π)) =
β
) |
213 | 212 | 3exp2 1355 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((abs
β β ) β (βMetββ) β§ (π Β· π§) β β β§ 0 β β)
β (π β
β* β (π β β* β ((π +π π) β€ ((π Β· π§)(abs β β )0) β (((π Β· π§)(ballβ(abs β β ))π) β© (0(ballβ(abs
β β ))π)) =
β
)))) |
214 | 213 | imp32 420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((abs
β β ) β (βMetββ) β§ (π Β· π§) β β β§ 0 β β)
β§ (π β
β* β§ π
β β*)) β ((π +π π) β€ ((π Β· π§)(abs β β )0) β (((π Β· π§)(ballβ(abs β β ))π) β© (0(ballβ(abs
β β ))π)) =
β
)) |
215 | 207, 208,
209, 210, 211, 214 | syl32anc 1379 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π· β (Bndβπ) β§ π β β+) β§ (π β β β§ π β (0(ballβ(abs
β β ))π)))
β§ π§ β β€[i])
β ((π
+π π)
β€ ((π Β· π§)(abs β β )0) β
(((π Β· π§)(ballβ(abs β
β ))π) β©
(0(ballβ(abs β β ))π)) = β
)) |
216 | | sseq0 4360 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π Β·
π§)(ballβ(abs β
β ))π) β© π) β (((π Β· π§)(ballβ(abs β β ))π) β© (0(ballβ(abs
β β ))π)) β§
(((π Β· π§)(ballβ(abs β
β ))π) β©
(0(ballβ(abs β β ))π)) = β
) β (((π Β· π§)(ballβ(abs β β ))π) β© π) = β
) |
217 | 206, 215,
216 | syl6an 683 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π· β (Bndβπ) β§ π β β+) β§ (π β β β§ π β (0(ballβ(abs
β β ))π)))
β§ π§ β β€[i])
β ((π
+π π)
β€ ((π Β· π§)(abs β β )0) β
(((π Β· π§)(ballβ(abs β
β ))π) β© π) = β
)) |
218 | 217 | necon3ad 2953 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π· β (Bndβπ) β§ π β β+) β§ (π β β β§ π β (0(ballβ(abs
β β ))π)))
β§ π§ β β€[i])
β ((((π Β· π§)(ballβ(abs β
β ))π) β© π) β β
β Β¬
(π +π
π) β€ ((π Β· π§)(abs β β )0))) |
219 | 218 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β Β¬ (π +π π) β€ ((π Β· π§)(abs β β )0)) |
220 | | rexadd 13157 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β β β§ π β β) β (π +π π) = (π + π)) |
221 | 188, 190,
220 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β (π +π π) = (π + π)) |
222 | 208 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β (π Β· π§) β β) |
223 | 123 | cnmetdval 24150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π Β· π§) β β β§ 0 β β)
β ((π Β· π§)(abs β β )0) =
(absβ((π Β·
π§) β
0))) |
224 | 222, 164,
223 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β ((π Β· π§)(abs β β )0) =
(absβ((π Β·
π§) β
0))) |
225 | 222 | subid1d 11506 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β ((π Β· π§) β 0) = (π Β· π§)) |
226 | 225 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β (absβ((π Β· π§) β 0)) = (absβ(π Β· π§))) |
227 | 224, 226 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β ((π Β· π§)(abs β β )0) = (absβ(π Β· π§))) |
228 | 221, 227 | breq12d 5119 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β ((π +π π) β€ ((π Β· π§)(abs β β )0) β (π + π) β€ (absβ(π Β· π§)))) |
229 | 219, 228 | mtbid 324 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β Β¬ (π + π) β€ (absβ(π Β· π§))) |
230 | 222 | abscld 15327 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β (absβ(π Β· π§)) β β) |
231 | 230, 191 | ltnled 11307 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β ((absβ(π Β· π§)) < (π + π) β Β¬ (π + π) β€ (absβ(π Β· π§)))) |
232 | 229, 231 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β (absβ(π Β· π§)) < (π + π)) |
233 | 203, 232 | eqbrtrrd 5130 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β (π Β· (absβπ§)) < (π + π)) |
234 | 185, 191,
187 | ltmuldiv2d 13010 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β ((π Β· (absβπ§)) < (π + π) β (absβπ§) < ((π + π) / π))) |
235 | 233, 234 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β (absβπ§) < ((π + π) / π)) |
236 | | flltp1 13711 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π + π) / π) β β β ((π + π) / π) < ((ββ((π + π) / π)) + 1)) |
237 | 192, 236 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β ((π + π) / π) < ((ββ((π + π) / π)) + 1)) |
238 | 185, 192,
195, 235, 237 | lttrd 11321 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β (absβπ§) < ((ββ((π + π) / π)) + 1)) |
239 | 185, 195,
238 | ltled 11308 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β (absβπ§) β€ ((ββ((π + π) / π)) + 1)) |
240 | 183, 185,
195, 197, 239 | letrd 11317 |
. . . . . . . . . . . . . . . . 17
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β
(absβ(ββπ§)) β€ ((ββ((π + π) / π)) + 1)) |
241 | 181 | zred 12612 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β (ββπ§) β
β) |
242 | 241, 195 | absled 15321 |
. . . . . . . . . . . . . . . . 17
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β
((absβ(ββπ§)) β€ ((ββ((π + π) / π)) + 1) β (-((ββ((π + π) / π)) + 1) β€ (ββπ§) β§ (ββπ§) β€ ((ββ((π + π) / π)) + 1)))) |
243 | 240, 242 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β
(-((ββ((π +
π) / π)) + 1) β€ (ββπ§) β§ (ββπ§) β€ ((ββ((π + π) / π)) + 1))) |
244 | 194 | znegcld 12614 |
. . . . . . . . . . . . . . . . 17
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β
-((ββ((π +
π) / π)) + 1) β β€) |
245 | | elfz 13436 |
. . . . . . . . . . . . . . . . 17
β’
(((ββπ§)
β β€ β§ -((ββ((π + π) / π)) + 1) β β€ β§
((ββ((π + π) / π)) + 1) β β€) β
((ββπ§) β
(-((ββ((π +
π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β (-((ββ((π + π) / π)) + 1) β€ (ββπ§) β§ (ββπ§) β€ ((ββ((π + π) / π)) + 1)))) |
246 | 181, 244,
194, 245 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β ((ββπ§) β
(-((ββ((π +
π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β (-((ββ((π + π) / π)) + 1) β€ (ββπ§) β§ (ββπ§) β€ ((ββ((π + π) / π)) + 1)))) |
247 | 243, 246 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β (ββπ§) β
(-((ββ((π +
π) / π)) + 1)...((ββ((π + π) / π)) + 1))) |
248 | 179 | simp3bi 1148 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π§ β β€[i] β
(ββπ§) β
β€) |
249 | 248 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β (ββπ§) β
β€) |
250 | 249 | zcnd 12613 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β (ββπ§) β
β) |
251 | 250 | abscld 15327 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β
(absβ(ββπ§)) β β) |
252 | | absimle 15200 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ β β β
(absβ(ββπ§)) β€ (absβπ§)) |
253 | 184, 252 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β
(absβ(ββπ§)) β€ (absβπ§)) |
254 | 251, 185,
195, 253, 239 | letrd 11317 |
. . . . . . . . . . . . . . . . 17
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β
(absβ(ββπ§)) β€ ((ββ((π + π) / π)) + 1)) |
255 | 249 | zred 12612 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β (ββπ§) β
β) |
256 | 255, 195 | absled 15321 |
. . . . . . . . . . . . . . . . 17
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β
((absβ(ββπ§)) β€ ((ββ((π + π) / π)) + 1) β (-((ββ((π + π) / π)) + 1) β€ (ββπ§) β§ (ββπ§) β€ ((ββ((π + π) / π)) + 1)))) |
257 | 254, 256 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β
(-((ββ((π +
π) / π)) + 1) β€ (ββπ§) β§ (ββπ§) β€ ((ββ((π + π) / π)) + 1))) |
258 | | elfz 13436 |
. . . . . . . . . . . . . . . . 17
β’
(((ββπ§)
β β€ β§ -((ββ((π + π) / π)) + 1) β β€ β§
((ββ((π + π) / π)) + 1) β β€) β
((ββπ§) β
(-((ββ((π +
π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β (-((ββ((π + π) / π)) + 1) β€ (ββπ§) β§ (ββπ§) β€ ((ββ((π + π) / π)) + 1)))) |
259 | 249, 244,
194, 258 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β ((ββπ§) β
(-((ββ((π +
π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β (-((ββ((π + π) / π)) + 1) β€ (ββπ§) β§ (ββπ§) β€ ((ββ((π + π) / π)) + 1)))) |
260 | 257, 259 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β (ββπ§) β
(-((ββ((π +
π) / π)) + 1)...((ββ((π + π) / π)) + 1))) |
261 | 184 | replimd 15088 |
. . . . . . . . . . . . . . . 16
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β π§ = ((ββπ§) + (i Β· (ββπ§)))) |
262 | 261 | oveq2d 7374 |
. . . . . . . . . . . . . . 15
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β (π Β· π§) = (π Β· ((ββπ§) + (i Β· (ββπ§))))) |
263 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (ββπ§) β (π + (i Β· π)) = ((ββπ§) + (i Β· π))) |
264 | 263 | oveq2d 7374 |
. . . . . . . . . . . . . . . . 17
β’ (π = (ββπ§) β (π Β· (π + (i Β· π))) = (π Β· ((ββπ§) + (i Β· π)))) |
265 | 264 | eqeq2d 2744 |
. . . . . . . . . . . . . . . 16
β’ (π = (ββπ§) β ((π Β· π§) = (π Β· (π + (i Β· π))) β (π Β· π§) = (π Β· ((ββπ§) + (i Β· π))))) |
266 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (ββπ§) β (i Β· π) = (i Β·
(ββπ§))) |
267 | 266 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (ββπ§) β ((ββπ§) + (i Β· π)) = ((ββπ§) + (i Β·
(ββπ§)))) |
268 | 267 | oveq2d 7374 |
. . . . . . . . . . . . . . . . 17
β’ (π = (ββπ§) β (π Β· ((ββπ§) + (i Β· π))) = (π Β· ((ββπ§) + (i Β· (ββπ§))))) |
269 | 268 | eqeq2d 2744 |
. . . . . . . . . . . . . . . 16
β’ (π = (ββπ§) β ((π Β· π§) = (π Β· ((ββπ§) + (i Β· π))) β (π Β· π§) = (π Β· ((ββπ§) + (i Β· (ββπ§)))))) |
270 | 265, 269 | rspc2ev 3591 |
. . . . . . . . . . . . . . 15
β’
(((ββπ§)
β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β§ (ββπ§) β
(-((ββ((π +
π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β§ (π Β· π§) = (π Β· ((ββπ§) + (i Β· (ββπ§))))) β βπ β
(-((ββ((π +
π) / π)) + 1)...((ββ((π + π) / π)) + 1))βπ β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1))(π Β· π§) = (π Β· (π + (i Β· π)))) |
271 | 247, 260,
262, 270 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’
(((((π· β
(Bndβπ) β§ π β β+)
β§ (π β β
β§ π β
(0(ballβ(abs β β ))π))) β§ π§ β β€[i]) β§ (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
) β βπ β
(-((ββ((π +
π) / π)) + 1)...((ββ((π + π) / π)) + 1))βπ β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1))(π Β· π§) = (π Β· (π + (i Β· π)))) |
272 | 271 | ex 414 |
. . . . . . . . . . . . 13
β’ ((((π· β (Bndβπ) β§ π β β+) β§ (π β β β§ π β (0(ballβ(abs
β β ))π)))
β§ π§ β β€[i])
β ((((π Β· π§)(ballβ(abs β
β ))π) β© π) β β
β
βπ β
(-((ββ((π +
π) / π)) + 1)...((ββ((π + π) / π)) + 1))βπ β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1))(π Β· π§) = (π Β· (π + (i Β· π))))) |
273 | 171, 172 | elrnmpo 7493 |
. . . . . . . . . . . . 13
β’ ((π Β· π§) β ran (π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)), π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β¦ (π Β· (π + (i Β· π)))) β βπ β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1))βπ β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1))(π Β· π§) = (π Β· (π + (i Β· π)))) |
274 | 272, 273 | syl6ibr 252 |
. . . . . . . . . . . 12
β’ ((((π· β (Bndβπ) β§ π β β+) β§ (π β β β§ π β (0(ballβ(abs
β β ))π)))
β§ π§ β β€[i])
β ((((π Β· π§)(ballβ(abs β
β ))π) β© π) β β
β (π Β· π§) β ran (π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)), π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β¦ (π Β· (π + (i Β· π)))))) |
275 | 156 | ineq1d 4172 |
. . . . . . . . . . . . . 14
β’ (π₯ = (π Β· π§) β ((π₯(ballβ(abs β β ))π) β© π) = (((π Β· π§)(ballβ(abs β β ))π) β© π)) |
276 | 275 | neeq1d 3000 |
. . . . . . . . . . . . 13
β’ (π₯ = (π Β· π§) β (((π₯(ballβ(abs β β ))π) β© π) β β
β (((π Β· π§)(ballβ(abs β β ))π) β© π) β β
)) |
277 | | eleq1 2822 |
. . . . . . . . . . . . 13
β’ (π₯ = (π Β· π§) β (π₯ β ran (π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)), π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β¦ (π Β· (π + (i Β· π)))) β (π Β· π§) β ran (π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)), π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β¦ (π Β· (π + (i Β· π)))))) |
278 | 276, 277 | imbi12d 345 |
. . . . . . . . . . . 12
β’ (π₯ = (π Β· π§) β ((((π₯(ballβ(abs β β ))π) β© π) β β
β π₯ β ran (π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)), π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β¦ (π Β· (π + (i Β· π))))) β ((((π Β· π§)(ballβ(abs β β ))π) β© π) β β
β (π Β· π§) β ran (π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)), π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β¦ (π Β· (π + (i Β· π))))))) |
279 | 274, 278 | syl5ibrcom 247 |
. . . . . . . . . . 11
β’ ((((π· β (Bndβπ) β§ π β β+) β§ (π β β β§ π β (0(ballβ(abs
β β ))π)))
β§ π§ β β€[i])
β (π₯ = (π Β· π§) β (((π₯(ballβ(abs β β ))π) β© π) β β
β π₯ β ran (π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)), π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β¦ (π Β· (π + (i Β· π))))))) |
280 | 279 | rexlimdva 3149 |
. . . . . . . . . 10
β’ (((π· β (Bndβπ) β§ π β β+) β§ (π β β β§ π β (0(ballβ(abs
β β ))π)))
β (βπ§ β
β€[i] π₯ = (π Β· π§) β (((π₯(ballβ(abs β β ))π) β© π) β β
β π₯ β ran (π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)), π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β¦ (π Β· (π + (i Β· π))))))) |
281 | 178, 280 | biimtrid 241 |
. . . . . . . . 9
β’ (((π· β (Bndβπ) β§ π β β+) β§ (π β β β§ π β (0(ballβ(abs
β β ))π)))
β (π₯ β ran (π§ β β€[i] β¦
(π Β· π§)) β (((π₯(ballβ(abs β β ))π) β© π) β β
β π₯ β ran (π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)), π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β¦ (π Β· (π + (i Β· π))))))) |
282 | 281 | 3imp 1112 |
. . . . . . . 8
β’ ((((π· β (Bndβπ) β§ π β β+) β§ (π β β β§ π β (0(ballβ(abs
β β ))π)))
β§ π₯ β ran (π§ β β€[i] β¦
(π Β· π§)) β§ ((π₯(ballβ(abs β β ))π) β© π) β β
) β π₯ β ran (π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)), π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β¦ (π Β· (π + (i Β· π))))) |
283 | 282 | rabssdv 4033 |
. . . . . . 7
β’ (((π· β (Bndβπ) β§ π β β+) β§ (π β β β§ π β (0(ballβ(abs
β β ))π)))
β {π₯ β ran (π§ β β€[i] β¦
(π Β· π§)) β£ ((π₯(ballβ(abs β β ))π) β© π) β β
} β ran (π β
(-((ββ((π +
π) / π)) + 1)...((ββ((π + π) / π)) + 1)), π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β¦ (π Β· (π + (i Β· π))))) |
284 | | ssfi 9120 |
. . . . . . 7
β’ ((ran
(π β
(-((ββ((π +
π) / π)) + 1)...((ββ((π + π) / π)) + 1)), π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β¦ (π Β· (π + (i Β· π)))) β Fin β§ {π₯ β ran (π§ β β€[i] β¦ (π Β· π§)) β£ ((π₯(ballβ(abs β β ))π) β© π) β β
} β ran (π β
(-((ββ((π +
π) / π)) + 1)...((ββ((π + π) / π)) + 1)), π β (-((ββ((π + π) / π)) + 1)...((ββ((π + π) / π)) + 1)) β¦ (π Β· (π + (i Β· π))))) β {π₯ β ran (π§ β β€[i] β¦ (π Β· π§)) β£ ((π₯(ballβ(abs β β ))π) β© π) β β
} β Fin) |
285 | 177, 283,
284 | sylancr 588 |
. . . . . 6
β’ (((π· β (Bndβπ) β§ π β β+) β§ (π β β β§ π β (0(ballβ(abs
β β ))π)))
β {π₯ β ran (π§ β β€[i] β¦
(π Β· π§)) β£ ((π₯(ballβ(abs β β ))π) β© π) β β
} β Fin) |
286 | 167, 285 | rexlimddv 3155 |
. . . . 5
β’ ((π· β (Bndβπ) β§ π β β+) β {π₯ β ran (π§ β β€[i] β¦ (π Β· π§)) β£ ((π₯(ballβ(abs β β ))π) β© π) β β
} β Fin) |
287 | | iuneq1 4971 |
. . . . . . . 8
β’ (π¦ = ran (π§ β β€[i] β¦ (π Β· π§)) β βͺ
π₯ β π¦ (π₯(ballβ(abs β β ))π) = βͺ π₯ β ran (π§ β β€[i] β¦ (π Β· π§))(π₯(ballβ(abs β β ))π)) |
288 | 287 | sseq2d 3977 |
. . . . . . 7
β’ (π¦ = ran (π§ β β€[i] β¦ (π Β· π§)) β (π β βͺ
π₯ β π¦ (π₯(ballβ(abs β β ))π) β π β βͺ
π₯ β ran (π§ β β€[i] β¦
(π Β· π§))(π₯(ballβ(abs β β ))π))) |
289 | | rabeq 3420 |
. . . . . . . 8
β’ (π¦ = ran (π§ β β€[i] β¦ (π Β· π§)) β {π₯ β π¦ β£ ((π₯(ballβ(abs β β ))π) β© π) β β
} = {π₯ β ran (π§ β β€[i] β¦ (π Β· π§)) β£ ((π₯(ballβ(abs β β ))π) β© π) β β
}) |
290 | 289 | eleq1d 2819 |
. . . . . . 7
β’ (π¦ = ran (π§ β β€[i] β¦ (π Β· π§)) β ({π₯ β π¦ β£ ((π₯(ballβ(abs β β ))π) β© π) β β
} β Fin β {π₯ β ran (π§ β β€[i] β¦ (π Β· π§)) β£ ((π₯(ballβ(abs β β ))π) β© π) β β
} β
Fin)) |
291 | 288, 290 | anbi12d 632 |
. . . . . 6
β’ (π¦ = ran (π§ β β€[i] β¦ (π Β· π§)) β ((π β βͺ
π₯ β π¦ (π₯(ballβ(abs β β ))π) β§ {π₯ β π¦ β£ ((π₯(ballβ(abs β β ))π) β© π) β β
} β Fin) β (π β βͺ π₯ β ran (π§ β β€[i] β¦ (π Β· π§))(π₯(ballβ(abs β β ))π) β§ {π₯ β ran (π§ β β€[i] β¦ (π Β· π§)) β£ ((π₯(ballβ(abs β β ))π) β© π) β β
} β
Fin))) |
292 | 291 | rspcev 3580 |
. . . . 5
β’ ((ran
(π§ β β€[i]
β¦ (π Β· π§)) β π« β
β§ (π β βͺ π₯ β ran (π§ β β€[i] β¦ (π Β· π§))(π₯(ballβ(abs β β ))π) β§ {π₯ β ran (π§ β β€[i] β¦ (π Β· π§)) β£ ((π₯(ballβ(abs β β ))π) β© π) β β
} β Fin)) β
βπ¦ β π«
β(π β βͺ π₯ β π¦ (π₯(ballβ(abs β β ))π) β§ {π₯ β π¦ β£ ((π₯(ballβ(abs β β ))π) β© π) β β
} β
Fin)) |
293 | 11, 162, 286, 292 | syl12anc 836 |
. . . 4
β’ ((π· β (Bndβπ) β§ π β β+) β
βπ¦ β π«
β(π β βͺ π₯ β π¦ (π₯(ballβ(abs β β ))π) β§ {π₯ β π¦ β£ ((π₯(ballβ(abs β β ))π) β© π) β β
} β
Fin)) |
294 | 293 | ralrimiva 3140 |
. . 3
β’ (π· β (Bndβπ) β βπ β β+
βπ¦ β π«
β(π β βͺ π₯ β π¦ (π₯(ballβ(abs β β ))π) β§ {π₯ β π¦ β£ ((π₯(ballβ(abs β β ))π) β© π) β β
} β
Fin)) |
295 | 13 | sstotbnd3 36281 |
. . . 4
β’ (((abs
β β ) β (Metββ) β§ π β β) β (π· β (TotBndβπ) β βπ β β+ βπ¦ β π« β(π β βͺ π₯ β π¦ (π₯(ballβ(abs β β ))π) β§ {π₯ β π¦ β£ ((π₯(ballβ(abs β β ))π) β© π) β β
} β
Fin))) |
296 | 12, 15, 295 | sylancr 588 |
. . 3
β’ (π· β (Bndβπ) β (π· β (TotBndβπ) β βπ β β+ βπ¦ β π« β(π β βͺ π₯ β π¦ (π₯(ballβ(abs β β ))π) β§ {π₯ β π¦ β£ ((π₯(ballβ(abs β β ))π) β© π) β β
} β
Fin))) |
297 | 294, 296 | mpbird 257 |
. 2
β’ (π· β (Bndβπ) β π· β (TotBndβπ)) |
298 | 1, 297 | impbii 208 |
1
β’ (π· β (TotBndβπ) β π· β (Bndβπ)) |