Step | Hyp | Ref
| Expression |
1 | | eqid 2732 |
. . 3
β’
(BaseSetβπ) =
(BaseSetβπ) |
2 | | vacn.g |
. . 3
β’ πΊ = ( +π£
βπ) |
3 | 1, 2 | nvgf 29858 |
. 2
β’ (π β NrmCVec β πΊ:((BaseSetβπ) Γ (BaseSetβπ))βΆ(BaseSetβπ)) |
4 | | rphalfcl 12997 |
. . . . . 6
β’ (π β β+
β (π / 2) β
β+) |
5 | 4 | adantl 482 |
. . . . 5
β’ (((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β (π / 2) β
β+) |
6 | | simplll 773 |
. . . . . . . . . 10
β’ ((((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β§ (π§ β (BaseSetβπ) β§ π€ β (BaseSetβπ))) β π β NrmCVec) |
7 | | vacn.c |
. . . . . . . . . . 11
β’ πΆ = (IndMetβπ) |
8 | 1, 7 | imsmet 29931 |
. . . . . . . . . 10
β’ (π β NrmCVec β πΆ β
(Metβ(BaseSetβπ))) |
9 | 6, 8 | syl 17 |
. . . . . . . . 9
β’ ((((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β§ (π§ β (BaseSetβπ) β§ π€ β (BaseSetβπ))) β πΆ β (Metβ(BaseSetβπ))) |
10 | | simplrl 775 |
. . . . . . . . . 10
β’ (((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β π₯ β (BaseSetβπ)) |
11 | 10 | adantr 481 |
. . . . . . . . 9
β’ ((((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β§ (π§ β (BaseSetβπ) β§ π€ β (BaseSetβπ))) β π₯ β (BaseSetβπ)) |
12 | | simprl 769 |
. . . . . . . . 9
β’ ((((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β§ (π§ β (BaseSetβπ) β§ π€ β (BaseSetβπ))) β π§ β (BaseSetβπ)) |
13 | | metcl 23829 |
. . . . . . . . 9
β’ ((πΆ β
(Metβ(BaseSetβπ)) β§ π₯ β (BaseSetβπ) β§ π§ β (BaseSetβπ)) β (π₯πΆπ§) β β) |
14 | 9, 11, 12, 13 | syl3anc 1371 |
. . . . . . . 8
β’ ((((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β§ (π§ β (BaseSetβπ) β§ π€ β (BaseSetβπ))) β (π₯πΆπ§) β β) |
15 | | simplrr 776 |
. . . . . . . . . 10
β’ (((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β π¦ β (BaseSetβπ)) |
16 | 15 | adantr 481 |
. . . . . . . . 9
β’ ((((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β§ (π§ β (BaseSetβπ) β§ π€ β (BaseSetβπ))) β π¦ β (BaseSetβπ)) |
17 | | simprr 771 |
. . . . . . . . 9
β’ ((((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β§ (π§ β (BaseSetβπ) β§ π€ β (BaseSetβπ))) β π€ β (BaseSetβπ)) |
18 | | metcl 23829 |
. . . . . . . . 9
β’ ((πΆ β
(Metβ(BaseSetβπ)) β§ π¦ β (BaseSetβπ) β§ π€ β (BaseSetβπ)) β (π¦πΆπ€) β β) |
19 | 9, 16, 17, 18 | syl3anc 1371 |
. . . . . . . 8
β’ ((((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β§ (π§ β (BaseSetβπ) β§ π€ β (BaseSetβπ))) β (π¦πΆπ€) β β) |
20 | | rpre 12978 |
. . . . . . . . 9
β’ (π β β+
β π β
β) |
21 | 20 | ad2antlr 725 |
. . . . . . . 8
β’ ((((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β§ (π§ β (BaseSetβπ) β§ π€ β (BaseSetβπ))) β π β β) |
22 | | lt2halves 12443 |
. . . . . . . 8
β’ (((π₯πΆπ§) β β β§ (π¦πΆπ€) β β β§ π β β) β (((π₯πΆπ§) < (π / 2) β§ (π¦πΆπ€) < (π / 2)) β ((π₯πΆπ§) + (π¦πΆπ€)) < π)) |
23 | 14, 19, 21, 22 | syl3anc 1371 |
. . . . . . 7
β’ ((((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β§ (π§ β (BaseSetβπ) β§ π€ β (BaseSetβπ))) β (((π₯πΆπ§) < (π / 2) β§ (π¦πΆπ€) < (π / 2)) β ((π₯πΆπ§) + (π¦πΆπ€)) < π)) |
24 | | eqid 2732 |
. . . . . . . . . . . 12
β’ (
βπ£ βπ) = ( βπ£
βπ) |
25 | 1, 24 | nvmcl 29886 |
. . . . . . . . . . 11
β’ ((π β NrmCVec β§ π₯ β (BaseSetβπ) β§ π§ β (BaseSetβπ)) β (π₯( βπ£ βπ)π§) β (BaseSetβπ)) |
26 | 6, 11, 12, 25 | syl3anc 1371 |
. . . . . . . . . 10
β’ ((((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β§ (π§ β (BaseSetβπ) β§ π€ β (BaseSetβπ))) β (π₯( βπ£ βπ)π§) β (BaseSetβπ)) |
27 | 1, 24 | nvmcl 29886 |
. . . . . . . . . . 11
β’ ((π β NrmCVec β§ π¦ β (BaseSetβπ) β§ π€ β (BaseSetβπ)) β (π¦( βπ£ βπ)π€) β (BaseSetβπ)) |
28 | 6, 16, 17, 27 | syl3anc 1371 |
. . . . . . . . . 10
β’ ((((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β§ (π§ β (BaseSetβπ) β§ π€ β (BaseSetβπ))) β (π¦( βπ£ βπ)π€) β (BaseSetβπ)) |
29 | | eqid 2732 |
. . . . . . . . . . 11
β’
(normCVβπ) = (normCVβπ) |
30 | 1, 2, 29 | nvtri 29910 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ (π₯( βπ£
βπ)π§) β (BaseSetβπ) β§ (π¦( βπ£ βπ)π€) β (BaseSetβπ)) β ((normCVβπ)β((π₯( βπ£ βπ)π§)πΊ(π¦( βπ£ βπ)π€))) β€ (((normCVβπ)β(π₯( βπ£ βπ)π§)) + ((normCVβπ)β(π¦( βπ£ βπ)π€)))) |
31 | 6, 26, 28, 30 | syl3anc 1371 |
. . . . . . . . 9
β’ ((((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β§ (π§ β (BaseSetβπ) β§ π€ β (BaseSetβπ))) β ((normCVβπ)β((π₯( βπ£ βπ)π§)πΊ(π¦( βπ£ βπ)π€))) β€ (((normCVβπ)β(π₯( βπ£ βπ)π§)) + ((normCVβπ)β(π¦( βπ£ βπ)π€)))) |
32 | 1, 2 | nvgcl 29860 |
. . . . . . . . . . . 12
β’ ((π β NrmCVec β§ π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ)) β (π₯πΊπ¦) β (BaseSetβπ)) |
33 | 6, 11, 16, 32 | syl3anc 1371 |
. . . . . . . . . . 11
β’ ((((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β§ (π§ β (BaseSetβπ) β§ π€ β (BaseSetβπ))) β (π₯πΊπ¦) β (BaseSetβπ)) |
34 | 1, 2 | nvgcl 29860 |
. . . . . . . . . . . 12
β’ ((π β NrmCVec β§ π§ β (BaseSetβπ) β§ π€ β (BaseSetβπ)) β (π§πΊπ€) β (BaseSetβπ)) |
35 | 6, 12, 17, 34 | syl3anc 1371 |
. . . . . . . . . . 11
β’ ((((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β§ (π§ β (BaseSetβπ) β§ π€ β (BaseSetβπ))) β (π§πΊπ€) β (BaseSetβπ)) |
36 | 1, 24, 29, 7 | imsdval 29926 |
. . . . . . . . . . 11
β’ ((π β NrmCVec β§ (π₯πΊπ¦) β (BaseSetβπ) β§ (π§πΊπ€) β (BaseSetβπ)) β ((π₯πΊπ¦)πΆ(π§πΊπ€)) = ((normCVβπ)β((π₯πΊπ¦)( βπ£ βπ)(π§πΊπ€)))) |
37 | 6, 33, 35, 36 | syl3anc 1371 |
. . . . . . . . . 10
β’ ((((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β§ (π§ β (BaseSetβπ) β§ π€ β (BaseSetβπ))) β ((π₯πΊπ¦)πΆ(π§πΊπ€)) = ((normCVβπ)β((π₯πΊπ¦)( βπ£ βπ)(π§πΊπ€)))) |
38 | 1, 2, 24 | nvaddsub4 29897 |
. . . . . . . . . . . 12
β’ ((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ)) β§ (π§ β (BaseSetβπ) β§ π€ β (BaseSetβπ))) β ((π₯πΊπ¦)( βπ£ βπ)(π§πΊπ€)) = ((π₯( βπ£ βπ)π§)πΊ(π¦( βπ£ βπ)π€))) |
39 | 6, 11, 16, 12, 17, 38 | syl122anc 1379 |
. . . . . . . . . . 11
β’ ((((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β§ (π§ β (BaseSetβπ) β§ π€ β (BaseSetβπ))) β ((π₯πΊπ¦)( βπ£ βπ)(π§πΊπ€)) = ((π₯( βπ£ βπ)π§)πΊ(π¦( βπ£ βπ)π€))) |
40 | 39 | fveq2d 6892 |
. . . . . . . . . 10
β’ ((((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β§ (π§ β (BaseSetβπ) β§ π€ β (BaseSetβπ))) β ((normCVβπ)β((π₯πΊπ¦)( βπ£ βπ)(π§πΊπ€))) = ((normCVβπ)β((π₯( βπ£ βπ)π§)πΊ(π¦( βπ£ βπ)π€)))) |
41 | 37, 40 | eqtrd 2772 |
. . . . . . . . 9
β’ ((((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β§ (π§ β (BaseSetβπ) β§ π€ β (BaseSetβπ))) β ((π₯πΊπ¦)πΆ(π§πΊπ€)) = ((normCVβπ)β((π₯( βπ£ βπ)π§)πΊ(π¦( βπ£ βπ)π€)))) |
42 | 1, 24, 29, 7 | imsdval 29926 |
. . . . . . . . . . 11
β’ ((π β NrmCVec β§ π₯ β (BaseSetβπ) β§ π§ β (BaseSetβπ)) β (π₯πΆπ§) = ((normCVβπ)β(π₯( βπ£ βπ)π§))) |
43 | 6, 11, 12, 42 | syl3anc 1371 |
. . . . . . . . . 10
β’ ((((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β§ (π§ β (BaseSetβπ) β§ π€ β (BaseSetβπ))) β (π₯πΆπ§) = ((normCVβπ)β(π₯( βπ£ βπ)π§))) |
44 | 1, 24, 29, 7 | imsdval 29926 |
. . . . . . . . . . 11
β’ ((π β NrmCVec β§ π¦ β (BaseSetβπ) β§ π€ β (BaseSetβπ)) β (π¦πΆπ€) = ((normCVβπ)β(π¦( βπ£ βπ)π€))) |
45 | 6, 16, 17, 44 | syl3anc 1371 |
. . . . . . . . . 10
β’ ((((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β§ (π§ β (BaseSetβπ) β§ π€ β (BaseSetβπ))) β (π¦πΆπ€) = ((normCVβπ)β(π¦( βπ£ βπ)π€))) |
46 | 43, 45 | oveq12d 7423 |
. . . . . . . . 9
β’ ((((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β§ (π§ β (BaseSetβπ) β§ π€ β (BaseSetβπ))) β ((π₯πΆπ§) + (π¦πΆπ€)) = (((normCVβπ)β(π₯( βπ£ βπ)π§)) + ((normCVβπ)β(π¦( βπ£ βπ)π€)))) |
47 | 31, 41, 46 | 3brtr4d 5179 |
. . . . . . . 8
β’ ((((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β§ (π§ β (BaseSetβπ) β§ π€ β (BaseSetβπ))) β ((π₯πΊπ¦)πΆ(π§πΊπ€)) β€ ((π₯πΆπ§) + (π¦πΆπ€))) |
48 | | metcl 23829 |
. . . . . . . . . 10
β’ ((πΆ β
(Metβ(BaseSetβπ)) β§ (π₯πΊπ¦) β (BaseSetβπ) β§ (π§πΊπ€) β (BaseSetβπ)) β ((π₯πΊπ¦)πΆ(π§πΊπ€)) β β) |
49 | 9, 33, 35, 48 | syl3anc 1371 |
. . . . . . . . 9
β’ ((((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β§ (π§ β (BaseSetβπ) β§ π€ β (BaseSetβπ))) β ((π₯πΊπ¦)πΆ(π§πΊπ€)) β β) |
50 | 14, 19 | readdcld 11239 |
. . . . . . . . 9
β’ ((((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β§ (π§ β (BaseSetβπ) β§ π€ β (BaseSetβπ))) β ((π₯πΆπ§) + (π¦πΆπ€)) β β) |
51 | | lelttr 11300 |
. . . . . . . . 9
β’ ((((π₯πΊπ¦)πΆ(π§πΊπ€)) β β β§ ((π₯πΆπ§) + (π¦πΆπ€)) β β β§ π β β) β ((((π₯πΊπ¦)πΆ(π§πΊπ€)) β€ ((π₯πΆπ§) + (π¦πΆπ€)) β§ ((π₯πΆπ§) + (π¦πΆπ€)) < π) β ((π₯πΊπ¦)πΆ(π§πΊπ€)) < π)) |
52 | 49, 50, 21, 51 | syl3anc 1371 |
. . . . . . . 8
β’ ((((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β§ (π§ β (BaseSetβπ) β§ π€ β (BaseSetβπ))) β ((((π₯πΊπ¦)πΆ(π§πΊπ€)) β€ ((π₯πΆπ§) + (π¦πΆπ€)) β§ ((π₯πΆπ§) + (π¦πΆπ€)) < π) β ((π₯πΊπ¦)πΆ(π§πΊπ€)) < π)) |
53 | 47, 52 | mpand 693 |
. . . . . . 7
β’ ((((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β§ (π§ β (BaseSetβπ) β§ π€ β (BaseSetβπ))) β (((π₯πΆπ§) + (π¦πΆπ€)) < π β ((π₯πΊπ¦)πΆ(π§πΊπ€)) < π)) |
54 | 23, 53 | syld 47 |
. . . . . 6
β’ ((((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β§ (π§ β (BaseSetβπ) β§ π€ β (BaseSetβπ))) β (((π₯πΆπ§) < (π / 2) β§ (π¦πΆπ€) < (π / 2)) β ((π₯πΊπ¦)πΆ(π§πΊπ€)) < π)) |
55 | 54 | ralrimivva 3200 |
. . . . 5
β’ (((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β
βπ§ β
(BaseSetβπ)βπ€ β (BaseSetβπ)(((π₯πΆπ§) < (π / 2) β§ (π¦πΆπ€) < (π / 2)) β ((π₯πΊπ¦)πΆ(π§πΊπ€)) < π)) |
56 | | breq2 5151 |
. . . . . . . . 9
β’ (π = (π / 2) β ((π₯πΆπ§) < π β (π₯πΆπ§) < (π / 2))) |
57 | | breq2 5151 |
. . . . . . . . 9
β’ (π = (π / 2) β ((π¦πΆπ€) < π β (π¦πΆπ€) < (π / 2))) |
58 | 56, 57 | anbi12d 631 |
. . . . . . . 8
β’ (π = (π / 2) β (((π₯πΆπ§) < π β§ (π¦πΆπ€) < π ) β ((π₯πΆπ§) < (π / 2) β§ (π¦πΆπ€) < (π / 2)))) |
59 | 58 | imbi1d 341 |
. . . . . . 7
β’ (π = (π / 2) β ((((π₯πΆπ§) < π β§ (π¦πΆπ€) < π ) β ((π₯πΊπ¦)πΆ(π§πΊπ€)) < π) β (((π₯πΆπ§) < (π / 2) β§ (π¦πΆπ€) < (π / 2)) β ((π₯πΊπ¦)πΆ(π§πΊπ€)) < π))) |
60 | 59 | 2ralbidv 3218 |
. . . . . 6
β’ (π = (π / 2) β (βπ§ β (BaseSetβπ)βπ€ β (BaseSetβπ)(((π₯πΆπ§) < π β§ (π¦πΆπ€) < π ) β ((π₯πΊπ¦)πΆ(π§πΊπ€)) < π) β βπ§ β (BaseSetβπ)βπ€ β (BaseSetβπ)(((π₯πΆπ§) < (π / 2) β§ (π¦πΆπ€) < (π / 2)) β ((π₯πΊπ¦)πΆ(π§πΊπ€)) < π))) |
61 | 60 | rspcev 3612 |
. . . . 5
β’ (((π / 2) β β+
β§ βπ§ β
(BaseSetβπ)βπ€ β (BaseSetβπ)(((π₯πΆπ§) < (π / 2) β§ (π¦πΆπ€) < (π / 2)) β ((π₯πΊπ¦)πΆ(π§πΊπ€)) < π)) β βπ β β+ βπ§ β (BaseSetβπ)βπ€ β (BaseSetβπ)(((π₯πΆπ§) < π β§ (π¦πΆπ€) < π ) β ((π₯πΊπ¦)πΆ(π§πΊπ€)) < π)) |
62 | 5, 55, 61 | syl2anc 584 |
. . . 4
β’ (((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β§ π β β+) β
βπ β
β+ βπ§ β (BaseSetβπ)βπ€ β (BaseSetβπ)(((π₯πΆπ§) < π β§ (π¦πΆπ€) < π ) β ((π₯πΊπ¦)πΆ(π§πΊπ€)) < π)) |
63 | 62 | ralrimiva 3146 |
. . 3
β’ ((π β NrmCVec β§ (π₯ β (BaseSetβπ) β§ π¦ β (BaseSetβπ))) β βπ β β+ βπ β β+
βπ§ β
(BaseSetβπ)βπ€ β (BaseSetβπ)(((π₯πΆπ§) < π β§ (π¦πΆπ€) < π ) β ((π₯πΊπ¦)πΆ(π§πΊπ€)) < π)) |
64 | 63 | ralrimivva 3200 |
. 2
β’ (π β NrmCVec β
βπ₯ β
(BaseSetβπ)βπ¦ β (BaseSetβπ)βπ β β+ βπ β β+
βπ§ β
(BaseSetβπ)βπ€ β (BaseSetβπ)(((π₯πΆπ§) < π β§ (π¦πΆπ€) < π ) β ((π₯πΊπ¦)πΆ(π§πΊπ€)) < π)) |
65 | 1, 7 | imsxmet 29932 |
. . 3
β’ (π β NrmCVec β πΆ β
(βMetβ(BaseSetβπ))) |
66 | | vacn.j |
. . . 4
β’ π½ = (MetOpenβπΆ) |
67 | 66, 66, 66 | txmetcn 24048 |
. . 3
β’ ((πΆ β
(βMetβ(BaseSetβπ)) β§ πΆ β
(βMetβ(BaseSetβπ)) β§ πΆ β
(βMetβ(BaseSetβπ))) β (πΊ β ((π½ Γt π½) Cn π½) β (πΊ:((BaseSetβπ) Γ (BaseSetβπ))βΆ(BaseSetβπ) β§ βπ₯ β (BaseSetβπ)βπ¦ β (BaseSetβπ)βπ β β+ βπ β β+
βπ§ β
(BaseSetβπ)βπ€ β (BaseSetβπ)(((π₯πΆπ§) < π β§ (π¦πΆπ€) < π ) β ((π₯πΊπ¦)πΆ(π§πΊπ€)) < π)))) |
68 | 65, 65, 65, 67 | syl3anc 1371 |
. 2
β’ (π β NrmCVec β (πΊ β ((π½ Γt π½) Cn π½) β (πΊ:((BaseSetβπ) Γ (BaseSetβπ))βΆ(BaseSetβπ) β§ βπ₯ β (BaseSetβπ)βπ¦ β (BaseSetβπ)βπ β β+ βπ β β+
βπ§ β
(BaseSetβπ)βπ€ β (BaseSetβπ)(((π₯πΆπ§) < π β§ (π¦πΆπ€) < π ) β ((π₯πΊπ¦)πΆ(π§πΊπ€)) < π)))) |
69 | 3, 64, 68 | mpbir2and 711 |
1
β’ (π β NrmCVec β πΊ β ((π½ Γt π½) Cn π½)) |