Step | Hyp | Ref
| Expression |
1 | | chscl.1 |
. . . . 5
โข (๐ โ ๐ด โ Cโ
) |
2 | | chscl.2 |
. . . . 5
โข (๐ โ ๐ต โ Cโ
) |
3 | | chscl.3 |
. . . . 5
โข (๐ โ ๐ต โ (โฅโ๐ด)) |
4 | | chscl.4 |
. . . . 5
โข (๐ โ ๐ป:โโถ(๐ด +โ ๐ต)) |
5 | | chscl.5 |
. . . . 5
โข (๐ โ ๐ป โ๐ฃ ๐ข) |
6 | | chscl.6 |
. . . . 5
โข ๐น = (๐ โ โ โฆ
((projโโ๐ด)โ(๐ปโ๐))) |
7 | 1, 2, 3, 4, 5, 6 | chscllem1 30928 |
. . . 4
โข (๐ โ ๐น:โโถ๐ด) |
8 | | chss 30520 |
. . . . 5
โข (๐ด โ
Cโ โ ๐ด โ โ) |
9 | 1, 8 | syl 17 |
. . . 4
โข (๐ โ ๐ด โ โ) |
10 | 7, 9 | fssd 6735 |
. . 3
โข (๐ โ ๐น:โโถ โ) |
11 | | hlimcaui 30527 |
. . . . . . 7
โข (๐ป โ๐ฃ
๐ข โ ๐ป โ Cauchy) |
12 | 5, 11 | syl 17 |
. . . . . 6
โข (๐ โ ๐ป โ Cauchy) |
13 | | hcaucvg 30477 |
. . . . . 6
โข ((๐ป โ Cauchy โง ๐ฅ โ โ+)
โ โ๐ โ
โ โ๐ โ
(โคโฅโ๐)(normโโ((๐ปโ๐) โโ (๐ปโ๐))) < ๐ฅ) |
14 | 12, 13 | sylan 580 |
. . . . 5
โข ((๐ โง ๐ฅ โ โ+) โ
โ๐ โ โ
โ๐ โ
(โคโฅโ๐)(normโโ((๐ปโ๐) โโ (๐ปโ๐))) < ๐ฅ) |
15 | | eluznn 12904 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ
(โคโฅโ๐)) โ ๐ โ โ) |
16 | 15 | adantll 712 |
. . . . . . . 8
โข ((((๐ โง ๐ฅ โ โ+) โง ๐ โ โ) โง ๐ โ
(โคโฅโ๐)) โ ๐ โ โ) |
17 | | chsh 30515 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ด โ
Cโ โ ๐ด โ Sโ
) |
18 | 1, 17 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ ๐ด โ Sโ
) |
19 | | chsh 30515 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ต โ
Cโ โ ๐ต โ Sโ
) |
20 | 2, 19 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ ๐ต โ Sโ
) |
21 | | shscl 30609 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ด โ
Sโ โง ๐ต โ Sโ )
โ (๐ด
+โ ๐ต)
โ Sโ ) |
22 | 18, 20, 21 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (๐ด +โ ๐ต) โ Sโ
) |
23 | | shss 30501 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ด +โ ๐ต) โ
Sโ โ (๐ด +โ ๐ต) โ โ) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (๐ด +โ ๐ต) โ โ) |
25 | 24 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โ โ) โ (๐ด +โ ๐ต) โ โ) |
26 | 4 | ffvelcdmda 7086 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โ โ) โ (๐ปโ๐) โ (๐ด +โ ๐ต)) |
27 | 25, 26 | sseldd 3983 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ โ โ) โ (๐ปโ๐) โ โ) |
28 | 27 | adantrr 715 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ (๐ปโ๐) โ โ) |
29 | 4, 24 | fssd 6735 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ๐ป:โโถ โ) |
30 | 29 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ๐ป:โโถ โ) |
31 | | simprr 771 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ๐ โ โ) |
32 | 30, 31 | ffvelcdmd 7087 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ (๐ปโ๐) โ โ) |
33 | | hvsubcl 30308 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ปโ๐) โ โ โง (๐ปโ๐) โ โ) โ ((๐ปโ๐) โโ (๐ปโ๐)) โ โ) |
34 | 28, 32, 33 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ((๐ปโ๐) โโ (๐ปโ๐)) โ โ) |
35 | 9 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โ โ) โ ๐ด โ โ) |
36 | 7 | ffvelcdmda 7086 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โ โ) โ (๐นโ๐) โ ๐ด) |
37 | 35, 36 | sseldd 3983 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ โ โ) โ (๐นโ๐) โ โ) |
38 | 37 | adantrr 715 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ (๐นโ๐) โ โ) |
39 | 9 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ๐ด โ โ) |
40 | 7 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ๐น:โโถ๐ด) |
41 | 40, 31 | ffvelcdmd 7087 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ (๐นโ๐) โ ๐ด) |
42 | 39, 41 | sseldd 3983 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ (๐นโ๐) โ โ) |
43 | | hvsubcl 30308 |
. . . . . . . . . . . . . . . . . 18
โข (((๐นโ๐) โ โ โง (๐นโ๐) โ โ) โ ((๐นโ๐) โโ (๐นโ๐)) โ โ) |
44 | 38, 42, 43 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ((๐นโ๐) โโ (๐นโ๐)) โ โ) |
45 | | hvsubcl 30308 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ปโ๐) โโ (๐ปโ๐)) โ โ โง ((๐นโ๐) โโ (๐นโ๐)) โ โ) โ (((๐ปโ๐) โโ (๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐))) โ โ) |
46 | 34, 44, 45 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ (((๐ปโ๐) โโ (๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐))) โ โ) |
47 | | normcl 30416 |
. . . . . . . . . . . . . . . 16
โข ((((๐ปโ๐) โโ (๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐))) โ โ โ
(normโโ(((๐ปโ๐) โโ (๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐)))) โ โ) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ
(normโโ(((๐ปโ๐) โโ (๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐)))) โ โ) |
49 | 48 | sqge0d 14104 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ 0 โค
((normโโ(((๐ปโ๐) โโ (๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐))))โ2)) |
50 | | normcl 30416 |
. . . . . . . . . . . . . . . . 17
โข (((๐นโ๐) โโ (๐นโ๐)) โ โ โ
(normโโ((๐นโ๐) โโ (๐นโ๐))) โ โ) |
51 | 44, 50 | syl 17 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ
(normโโ((๐นโ๐) โโ (๐นโ๐))) โ โ) |
52 | 51 | resqcld 14092 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ
((normโโ((๐นโ๐) โโ (๐นโ๐)))โ2) โ โ) |
53 | 48 | resqcld 14092 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ
((normโโ(((๐ปโ๐) โโ (๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐))))โ2) โ โ) |
54 | 52, 53 | addge01d 11804 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ (0 โค
((normโโ(((๐ปโ๐) โโ (๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐))))โ2) โ
((normโโ((๐นโ๐) โโ (๐นโ๐)))โ2) โค
(((normโโ((๐นโ๐) โโ (๐นโ๐)))โ2) +
((normโโ(((๐ปโ๐) โโ (๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐))))โ2)))) |
55 | 49, 54 | mpbid 231 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ
((normโโ((๐นโ๐) โโ (๐นโ๐)))โ2) โค
(((normโโ((๐นโ๐) โโ (๐นโ๐)))โ2) +
((normโโ(((๐ปโ๐) โโ (๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐))))โ2))) |
56 | 18 | adantr 481 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ๐ด โ Sโ
) |
57 | 36 | adantrr 715 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ (๐นโ๐) โ ๐ด) |
58 | | shsubcl 30511 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ
Sโ โง (๐นโ๐) โ ๐ด โง (๐นโ๐) โ ๐ด) โ ((๐นโ๐) โโ (๐นโ๐)) โ ๐ด) |
59 | 56, 57, 41, 58 | syl3anc 1371 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ((๐นโ๐) โโ (๐นโ๐)) โ ๐ด) |
60 | | hvsubsub4 30351 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ปโ๐) โ โ โง (๐ปโ๐) โ โ) โง ((๐นโ๐) โ โ โง (๐นโ๐) โ โ)) โ (((๐ปโ๐) โโ (๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐))) = (((๐ปโ๐) โโ (๐นโ๐)) โโ ((๐ปโ๐) โโ (๐นโ๐)))) |
61 | 28, 32, 38, 42, 60 | syl22anc 837 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ (((๐ปโ๐) โโ (๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐))) = (((๐ปโ๐) โโ (๐นโ๐)) โโ ((๐ปโ๐) โโ (๐นโ๐)))) |
62 | | ocsh 30574 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ด โ โ โ
(โฅโ๐ด) โ
Sโ ) |
63 | 39, 62 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ (โฅโ๐ด) โ
Sโ ) |
64 | | 2fveq3 6896 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ = ๐ โ ((projโโ๐ด)โ(๐ปโ๐)) = ((projโโ๐ด)โ(๐ปโ๐))) |
65 | | fvex 6904 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข
((projโโ๐ด)โ(๐ปโ๐)) โ V |
66 | 64, 6, 65 | fvmpt 6998 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ โ โ (๐นโ๐) = ((projโโ๐ด)โ(๐ปโ๐))) |
67 | 66 | eqcomd 2738 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ โ โ
((projโโ๐ด)โ(๐ปโ๐)) = (๐นโ๐)) |
68 | 67 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง ๐ โ โ) โ
((projโโ๐ด)โ(๐ปโ๐)) = (๐นโ๐)) |
69 | 1 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ โง ๐ โ โ) โ ๐ด โ Cโ
) |
70 | 9, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ โ (โฅโ๐ด) โ
Sโ ) |
71 | | shless 30650 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (((๐ต โ
Sโ โง (โฅโ๐ด) โ Sโ
โง ๐ด โ
Sโ ) โง ๐ต โ (โฅโ๐ด)) โ (๐ต +โ ๐ด) โ ((โฅโ๐ด) +โ ๐ด)) |
72 | 20, 70, 18, 3, 71 | syl31anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ โ (๐ต +โ ๐ด) โ ((โฅโ๐ด) +โ ๐ด)) |
73 | | shscom 30610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐ด โ
Sโ โง ๐ต โ Sโ )
โ (๐ด
+โ ๐ต) =
(๐ต +โ
๐ด)) |
74 | 18, 20, 73 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ โ (๐ด +โ ๐ต) = (๐ต +โ ๐ด)) |
75 | | shscom 30610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((๐ด โ
Sโ โง (โฅโ๐ด) โ Sโ )
โ (๐ด
+โ (โฅโ๐ด)) = ((โฅโ๐ด) +โ ๐ด)) |
76 | 18, 70, 75 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ โ (๐ด +โ (โฅโ๐ด)) = ((โฅโ๐ด) +โ ๐ด)) |
77 | 72, 74, 76 | 3sstr4d 4029 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ (๐ด +โ ๐ต) โ (๐ด +โ (โฅโ๐ด))) |
78 | 77 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ โง ๐ โ โ) โ (๐ด +โ ๐ต) โ (๐ด +โ (โฅโ๐ด))) |
79 | 78, 26 | sseldd 3983 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ โง ๐ โ โ) โ (๐ปโ๐) โ (๐ด +โ (โฅโ๐ด))) |
80 | | pjpreeq 30689 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ด โ
Cโ โง (๐ปโ๐) โ (๐ด +โ (โฅโ๐ด))) โ
(((projโโ๐ด)โ(๐ปโ๐)) = (๐นโ๐) โ ((๐นโ๐) โ ๐ด โง โ๐ฅ โ (โฅโ๐ด)(๐ปโ๐) = ((๐นโ๐) +โ ๐ฅ)))) |
81 | 69, 79, 80 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง ๐ โ โ) โ
(((projโโ๐ด)โ(๐ปโ๐)) = (๐นโ๐) โ ((๐นโ๐) โ ๐ด โง โ๐ฅ โ (โฅโ๐ด)(๐ปโ๐) = ((๐นโ๐) +โ ๐ฅ)))) |
82 | 68, 81 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ๐ โ โ) โ ((๐นโ๐) โ ๐ด โง โ๐ฅ โ (โฅโ๐ด)(๐ปโ๐) = ((๐นโ๐) +โ ๐ฅ))) |
83 | 82 | simprd 496 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ โ โ) โ โ๐ฅ โ (โฅโ๐ด)(๐ปโ๐) = ((๐นโ๐) +โ ๐ฅ)) |
84 | 27 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โง ๐ โ โ) โง ๐ฅ โ (โฅโ๐ด)) โ (๐ปโ๐) โ โ) |
85 | 37 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โง ๐ โ โ) โง ๐ฅ โ (โฅโ๐ด)) โ (๐นโ๐) โ โ) |
86 | | shss 30501 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข
((โฅโ๐ด)
โ Sโ โ (โฅโ๐ด) โ
โ) |
87 | 70, 86 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ (โฅโ๐ด) โ
โ) |
88 | 87 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ โง ๐ โ โ) โ (โฅโ๐ด) โ
โ) |
89 | 88 | sselda 3982 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ โง ๐ โ โ) โง ๐ฅ โ (โฅโ๐ด)) โ ๐ฅ โ โ) |
90 | | hvsubadd 30368 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ปโ๐) โ โ โง (๐นโ๐) โ โ โง ๐ฅ โ โ) โ (((๐ปโ๐) โโ (๐นโ๐)) = ๐ฅ โ ((๐นโ๐) +โ ๐ฅ) = (๐ปโ๐))) |
91 | 84, 85, 89, 90 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โง ๐ โ โ) โง ๐ฅ โ (โฅโ๐ด)) โ (((๐ปโ๐) โโ (๐นโ๐)) = ๐ฅ โ ((๐นโ๐) +โ ๐ฅ) = (๐ปโ๐))) |
92 | | eqcom 2739 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฅ = ((๐ปโ๐) โโ (๐นโ๐)) โ ((๐ปโ๐) โโ (๐นโ๐)) = ๐ฅ) |
93 | | eqcom 2739 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ปโ๐) = ((๐นโ๐) +โ ๐ฅ) โ ((๐นโ๐) +โ ๐ฅ) = (๐ปโ๐)) |
94 | 91, 92, 93 | 3bitr4g 313 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง ๐ โ โ) โง ๐ฅ โ (โฅโ๐ด)) โ (๐ฅ = ((๐ปโ๐) โโ (๐นโ๐)) โ (๐ปโ๐) = ((๐นโ๐) +โ ๐ฅ))) |
95 | 94 | rexbidva 3176 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ โ โ) โ (โ๐ฅ โ (โฅโ๐ด)๐ฅ = ((๐ปโ๐) โโ (๐นโ๐)) โ โ๐ฅ โ (โฅโ๐ด)(๐ปโ๐) = ((๐นโ๐) +โ ๐ฅ))) |
96 | 83, 95 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โ โ) โ โ๐ฅ โ (โฅโ๐ด)๐ฅ = ((๐ปโ๐) โโ (๐นโ๐))) |
97 | | risset 3230 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ปโ๐) โโ (๐นโ๐)) โ (โฅโ๐ด) โ โ๐ฅ โ (โฅโ๐ด)๐ฅ = ((๐ปโ๐) โโ (๐นโ๐))) |
98 | 96, 97 | sylibr 233 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ โ โ) โ ((๐ปโ๐) โโ (๐นโ๐)) โ (โฅโ๐ด)) |
99 | 98 | adantrr 715 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ((๐ปโ๐) โโ (๐นโ๐)) โ (โฅโ๐ด)) |
100 | | eleq1w 2816 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ = ๐ โ (๐ โ โ โ ๐ โ โ)) |
101 | 100 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = ๐ โ ((๐ โง ๐ โ โ) โ (๐ โง ๐ โ โ))) |
102 | | fveq2 6891 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ = ๐ โ (๐ปโ๐) = (๐ปโ๐)) |
103 | | fveq2 6891 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ = ๐ โ (๐นโ๐) = (๐นโ๐)) |
104 | 102, 103 | oveq12d 7429 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ = ๐ โ ((๐ปโ๐) โโ (๐นโ๐)) = ((๐ปโ๐) โโ (๐นโ๐))) |
105 | 104 | eleq1d 2818 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = ๐ โ (((๐ปโ๐) โโ (๐นโ๐)) โ (โฅโ๐ด) โ ((๐ปโ๐) โโ (๐นโ๐)) โ (โฅโ๐ด))) |
106 | 101, 105 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = ๐ โ (((๐ โง ๐ โ โ) โ ((๐ปโ๐) โโ (๐นโ๐)) โ (โฅโ๐ด)) โ ((๐ โง ๐ โ โ) โ ((๐ปโ๐) โโ (๐นโ๐)) โ (โฅโ๐ด)))) |
107 | 106, 98 | chvarvv 2002 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ โ โ) โ ((๐ปโ๐) โโ (๐นโ๐)) โ (โฅโ๐ด)) |
108 | 107 | adantrl 714 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ((๐ปโ๐) โโ (๐นโ๐)) โ (โฅโ๐ด)) |
109 | | shsubcl 30511 |
. . . . . . . . . . . . . . . . . 18
โข
(((โฅโ๐ด)
โ Sโ โง ((๐ปโ๐) โโ (๐นโ๐)) โ (โฅโ๐ด) โง ((๐ปโ๐) โโ (๐นโ๐)) โ (โฅโ๐ด)) โ (((๐ปโ๐) โโ (๐นโ๐)) โโ ((๐ปโ๐) โโ (๐นโ๐))) โ (โฅโ๐ด)) |
110 | 63, 99, 108, 109 | syl3anc 1371 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ (((๐ปโ๐) โโ (๐นโ๐)) โโ ((๐ปโ๐) โโ (๐นโ๐))) โ (โฅโ๐ด)) |
111 | 61, 110 | eqeltrd 2833 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ (((๐ปโ๐) โโ (๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐))) โ (โฅโ๐ด)) |
112 | | shocorth 30583 |
. . . . . . . . . . . . . . . . 17
โข (๐ด โ
Sโ โ ((((๐นโ๐) โโ (๐นโ๐)) โ ๐ด โง (((๐ปโ๐) โโ (๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐))) โ (โฅโ๐ด)) โ (((๐นโ๐) โโ (๐นโ๐)) ยทih
(((๐ปโ๐) โโ
(๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐)))) = 0)) |
113 | 56, 112 | syl 17 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ((((๐นโ๐) โโ (๐นโ๐)) โ ๐ด โง (((๐ปโ๐) โโ (๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐))) โ (โฅโ๐ด)) โ (((๐นโ๐) โโ (๐นโ๐)) ยทih
(((๐ปโ๐) โโ
(๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐)))) = 0)) |
114 | 59, 111, 113 | mp2and 697 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ (((๐นโ๐) โโ (๐นโ๐)) ยทih
(((๐ปโ๐) โโ
(๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐)))) = 0) |
115 | | normpyth 30436 |
. . . . . . . . . . . . . . . 16
โข ((((๐นโ๐) โโ (๐นโ๐)) โ โ โง (((๐ปโ๐) โโ (๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐))) โ โ) โ ((((๐นโ๐) โโ (๐นโ๐)) ยทih
(((๐ปโ๐) โโ
(๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐)))) = 0 โ
((normโโ(((๐นโ๐) โโ (๐นโ๐)) +โ (((๐ปโ๐) โโ (๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐)))))โ2) =
(((normโโ((๐นโ๐) โโ (๐นโ๐)))โ2) +
((normโโ(((๐ปโ๐) โโ (๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐))))โ2)))) |
116 | 44, 46, 115 | syl2anc 584 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ((((๐นโ๐) โโ (๐นโ๐)) ยทih
(((๐ปโ๐) โโ
(๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐)))) = 0 โ
((normโโ(((๐นโ๐) โโ (๐นโ๐)) +โ (((๐ปโ๐) โโ (๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐)))))โ2) =
(((normโโ((๐นโ๐) โโ (๐นโ๐)))โ2) +
((normโโ(((๐ปโ๐) โโ (๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐))))โ2)))) |
117 | 114, 116 | mpd 15 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ
((normโโ(((๐นโ๐) โโ (๐นโ๐)) +โ (((๐ปโ๐) โโ (๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐)))))โ2) =
(((normโโ((๐นโ๐) โโ (๐นโ๐)))โ2) +
((normโโ(((๐ปโ๐) โโ (๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐))))โ2))) |
118 | | hvpncan3 30333 |
. . . . . . . . . . . . . . . . 17
โข ((((๐นโ๐) โโ (๐นโ๐)) โ โ โง ((๐ปโ๐) โโ (๐ปโ๐)) โ โ) โ (((๐นโ๐) โโ (๐นโ๐)) +โ (((๐ปโ๐) โโ (๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐)))) = ((๐ปโ๐) โโ (๐ปโ๐))) |
119 | 44, 34, 118 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ (((๐นโ๐) โโ (๐นโ๐)) +โ (((๐ปโ๐) โโ (๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐)))) = ((๐ปโ๐) โโ (๐ปโ๐))) |
120 | 119 | fveq2d 6895 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ
(normโโ(((๐นโ๐) โโ (๐นโ๐)) +โ (((๐ปโ๐) โโ (๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐))))) =
(normโโ((๐ปโ๐) โโ (๐ปโ๐)))) |
121 | 120 | oveq1d 7426 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ
((normโโ(((๐นโ๐) โโ (๐นโ๐)) +โ (((๐ปโ๐) โโ (๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐)))))โ2) =
((normโโ((๐ปโ๐) โโ (๐ปโ๐)))โ2)) |
122 | 117, 121 | eqtr3d 2774 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ
(((normโโ((๐นโ๐) โโ (๐นโ๐)))โ2) +
((normโโ(((๐ปโ๐) โโ (๐ปโ๐)) โโ ((๐นโ๐) โโ (๐นโ๐))))โ2)) =
((normโโ((๐ปโ๐) โโ (๐ปโ๐)))โ2)) |
123 | 55, 122 | breqtrd 5174 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ
((normโโ((๐นโ๐) โโ (๐นโ๐)))โ2) โค
((normโโ((๐ปโ๐) โโ (๐ปโ๐)))โ2)) |
124 | | normcl 30416 |
. . . . . . . . . . . . . 14
โข (((๐ปโ๐) โโ (๐ปโ๐)) โ โ โ
(normโโ((๐ปโ๐) โโ (๐ปโ๐))) โ โ) |
125 | 34, 124 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ
(normโโ((๐ปโ๐) โโ (๐ปโ๐))) โ โ) |
126 | | normge0 30417 |
. . . . . . . . . . . . . 14
โข (((๐นโ๐) โโ (๐นโ๐)) โ โ โ 0 โค
(normโโ((๐นโ๐) โโ (๐นโ๐)))) |
127 | 44, 126 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ 0 โค
(normโโ((๐นโ๐) โโ (๐นโ๐)))) |
128 | | normge0 30417 |
. . . . . . . . . . . . . 14
โข (((๐ปโ๐) โโ (๐ปโ๐)) โ โ โ 0 โค
(normโโ((๐ปโ๐) โโ (๐ปโ๐)))) |
129 | 34, 128 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ 0 โค
(normโโ((๐ปโ๐) โโ (๐ปโ๐)))) |
130 | 51, 125, 127, 129 | le2sqd 14222 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ
((normโโ((๐นโ๐) โโ (๐นโ๐))) โค
(normโโ((๐ปโ๐) โโ (๐ปโ๐))) โ
((normโโ((๐นโ๐) โโ (๐นโ๐)))โ2) โค
((normโโ((๐ปโ๐) โโ (๐ปโ๐)))โ2))) |
131 | 123, 130 | mpbird 256 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ
(normโโ((๐นโ๐) โโ (๐นโ๐))) โค
(normโโ((๐ปโ๐) โโ (๐ปโ๐)))) |
132 | 131 | adantlr 713 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ โ+) โง (๐ โ โ โง ๐ โ โ)) โ
(normโโ((๐นโ๐) โโ (๐นโ๐))) โค
(normโโ((๐ปโ๐) โโ (๐ปโ๐)))) |
133 | 51 | adantlr 713 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ โ+) โง (๐ โ โ โง ๐ โ โ)) โ
(normโโ((๐นโ๐) โโ (๐นโ๐))) โ โ) |
134 | 125 | adantlr 713 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ โ+) โง (๐ โ โ โง ๐ โ โ)) โ
(normโโ((๐ปโ๐) โโ (๐ปโ๐))) โ โ) |
135 | | rpre 12984 |
. . . . . . . . . . . 12
โข (๐ฅ โ โ+
โ ๐ฅ โ
โ) |
136 | 135 | ad2antlr 725 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ โ+) โง (๐ โ โ โง ๐ โ โ)) โ ๐ฅ โ
โ) |
137 | | lelttr 11306 |
. . . . . . . . . . 11
โข
(((normโโ((๐นโ๐) โโ (๐นโ๐))) โ โ โง
(normโโ((๐ปโ๐) โโ (๐ปโ๐))) โ โ โง ๐ฅ โ โ) โ
(((normโโ((๐นโ๐) โโ (๐นโ๐))) โค
(normโโ((๐ปโ๐) โโ (๐ปโ๐))) โง
(normโโ((๐ปโ๐) โโ (๐ปโ๐))) < ๐ฅ) โ
(normโโ((๐นโ๐) โโ (๐นโ๐))) < ๐ฅ)) |
138 | 133, 134,
136, 137 | syl3anc 1371 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ โ+) โง (๐ โ โ โง ๐ โ โ)) โ
(((normโโ((๐นโ๐) โโ (๐นโ๐))) โค
(normโโ((๐ปโ๐) โโ (๐ปโ๐))) โง
(normโโ((๐ปโ๐) โโ (๐ปโ๐))) < ๐ฅ) โ
(normโโ((๐นโ๐) โโ (๐นโ๐))) < ๐ฅ)) |
139 | 132, 138 | mpand 693 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ โ+) โง (๐ โ โ โง ๐ โ โ)) โ
((normโโ((๐ปโ๐) โโ (๐ปโ๐))) < ๐ฅ โ
(normโโ((๐นโ๐) โโ (๐นโ๐))) < ๐ฅ)) |
140 | 139 | anassrs 468 |
. . . . . . . 8
โข ((((๐ โง ๐ฅ โ โ+) โง ๐ โ โ) โง ๐ โ โ) โ
((normโโ((๐ปโ๐) โโ (๐ปโ๐))) < ๐ฅ โ
(normโโ((๐นโ๐) โโ (๐นโ๐))) < ๐ฅ)) |
141 | 16, 140 | syldan 591 |
. . . . . . 7
โข ((((๐ โง ๐ฅ โ โ+) โง ๐ โ โ) โง ๐ โ
(โคโฅโ๐)) โ
((normโโ((๐ปโ๐) โโ (๐ปโ๐))) < ๐ฅ โ
(normโโ((๐นโ๐) โโ (๐นโ๐))) < ๐ฅ)) |
142 | 141 | ralimdva 3167 |
. . . . . 6
โข (((๐ โง ๐ฅ โ โ+) โง ๐ โ โ) โ
(โ๐ โ
(โคโฅโ๐)(normโโ((๐ปโ๐) โโ (๐ปโ๐))) < ๐ฅ โ โ๐ โ (โคโฅโ๐)(normโโ((๐นโ๐) โโ (๐นโ๐))) < ๐ฅ)) |
143 | 142 | reximdva 3168 |
. . . . 5
โข ((๐ โง ๐ฅ โ โ+) โ
(โ๐ โ โ
โ๐ โ
(โคโฅโ๐)(normโโ((๐ปโ๐) โโ (๐ปโ๐))) < ๐ฅ โ โ๐ โ โ โ๐ โ (โคโฅโ๐)(normโโ((๐นโ๐) โโ (๐นโ๐))) < ๐ฅ)) |
144 | 14, 143 | mpd 15 |
. . . 4
โข ((๐ โง ๐ฅ โ โ+) โ
โ๐ โ โ
โ๐ โ
(โคโฅโ๐)(normโโ((๐นโ๐) โโ (๐นโ๐))) < ๐ฅ) |
145 | 144 | ralrimiva 3146 |
. . 3
โข (๐ โ โ๐ฅ โ โ+ โ๐ โ โ โ๐ โ
(โคโฅโ๐)(normโโ((๐นโ๐) โโ (๐นโ๐))) < ๐ฅ) |
146 | | hcau 30475 |
. . 3
โข (๐น โ Cauchy โ (๐น:โโถ โ โง
โ๐ฅ โ
โ+ โ๐ โ โ โ๐ โ (โคโฅโ๐)(normโโ((๐นโ๐) โโ (๐นโ๐))) < ๐ฅ)) |
147 | 10, 145, 146 | sylanbrc 583 |
. 2
โข (๐ โ ๐น โ Cauchy) |
148 | | ax-hcompl 30493 |
. 2
โข (๐น โ Cauchy โ
โ๐ฅ โ โ
๐น
โ๐ฃ ๐ฅ) |
149 | | hlimf 30528 |
. . . . 5
โข
โ๐ฃ :dom โ๐ฃ โถ
โ |
150 | | ffn 6717 |
. . . . 5
โข (
โ๐ฃ :dom โ๐ฃ โถ โ
โ โ๐ฃ Fn dom โ๐ฃ
) |
151 | 149, 150 | ax-mp 5 |
. . . 4
โข
โ๐ฃ Fn dom โ๐ฃ |
152 | | fnbr 6657 |
. . . 4
โข ((
โ๐ฃ Fn dom โ๐ฃ โง ๐น โ๐ฃ
๐ฅ) โ ๐น โ dom โ๐ฃ
) |
153 | 151, 152 | mpan 688 |
. . 3
โข (๐น โ๐ฃ
๐ฅ โ ๐น โ dom โ๐ฃ
) |
154 | 153 | rexlimivw 3151 |
. 2
โข
(โ๐ฅ โ
โ ๐น
โ๐ฃ ๐ฅ โ ๐น โ dom โ๐ฃ
) |
155 | 147, 148,
154 | 3syl 18 |
1
โข (๐ โ ๐น โ dom โ๐ฃ
) |