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 27880 |
. . . 4
⊢ (𝜑 → 𝐹:ℕ⟶𝐴) |
8 | | chss 27470 |
. . . . 5
⊢ (𝐴 ∈
Cℋ → 𝐴 ⊆ ℋ) |
9 | 1, 8 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ ℋ) |
10 | 7, 9 | fssd 5970 |
. . 3
⊢ (𝜑 → 𝐹:ℕ⟶ ℋ) |
11 | | hlimcaui 27477 |
. . . . . . 7
⊢ (𝐻 ⇝𝑣
𝑢 → 𝐻 ∈ Cauchy) |
12 | 5, 11 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐻 ∈ Cauchy) |
13 | | hcaucvg 27427 |
. . . . . 6
⊢ ((𝐻 ∈ Cauchy ∧ 𝑥 ∈ ℝ+)
→ ∃𝑗 ∈
ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) < 𝑥) |
14 | 12, 13 | sylan 487 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) < 𝑥) |
15 | | eluznn 11634 |
. . . . . . . . 9
⊢ ((𝑗 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → 𝑘 ∈ ℕ) |
16 | 15 | adantll 746 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → 𝑘 ∈ ℕ) |
17 | | chsh 27465 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ∈
Cℋ → 𝐴 ∈ Sℋ
) |
18 | 1, 17 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐴 ∈ Sℋ
) |
19 | | chsh 27465 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐵 ∈
Cℋ → 𝐵 ∈ Sℋ
) |
20 | 2, 19 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐵 ∈ Sℋ
) |
21 | | shscl 27561 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
→ (𝐴
+ℋ 𝐵)
∈ Sℋ ) |
22 | 18, 20, 21 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐴 +ℋ 𝐵) ∈ Sℋ
) |
23 | | shss 27451 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 +ℋ 𝐵) ∈
Sℋ → (𝐴 +ℋ 𝐵) ⊆ ℋ) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐴 +ℋ 𝐵) ⊆ ℋ) |
25 | 24 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴 +ℋ 𝐵) ⊆ ℋ) |
26 | 4 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐻‘𝑗) ∈ (𝐴 +ℋ 𝐵)) |
27 | 25, 26 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐻‘𝑗) ∈ ℋ) |
28 | 27 | adantrr 749 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝐻‘𝑗) ∈ ℋ) |
29 | 4, 24 | fssd 5970 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐻:ℕ⟶ ℋ) |
30 | 29 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 𝐻:ℕ⟶ ℋ) |
31 | | simprr 792 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 𝑘 ∈ ℕ) |
32 | 30, 31 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝐻‘𝑘) ∈ ℋ) |
33 | | hvsubcl 27258 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐻‘𝑗) ∈ ℋ ∧ (𝐻‘𝑘) ∈ ℋ) → ((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) ∈ ℋ) |
34 | 28, 32, 33 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) ∈ ℋ) |
35 | 9 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐴 ⊆ ℋ) |
36 | 7 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ 𝐴) |
37 | 35, 36 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ ℋ) |
38 | 37 | adantrr 749 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝐹‘𝑗) ∈ ℋ) |
39 | 9 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 𝐴 ⊆ ℋ) |
40 | 7 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 𝐹:ℕ⟶𝐴) |
41 | 40, 31 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝐹‘𝑘) ∈ 𝐴) |
42 | 39, 41 | sseldd 3569 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝐹‘𝑘) ∈ ℋ) |
43 | | hvsubcl 27258 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹‘𝑗) ∈ ℋ ∧ (𝐹‘𝑘) ∈ ℋ) → ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ ℋ) |
44 | 38, 42, 43 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ ℋ) |
45 | | hvsubcl 27258 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) ∈ ℋ ∧ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ ℋ) → (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ ℋ) |
46 | 34, 44, 45 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ ℋ) |
47 | | normcl 27366 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ ℋ →
(normℎ‘(((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) ∈ ℝ) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
(normℎ‘(((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) ∈ ℝ) |
49 | 48 | sqge0d 12898 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 0 ≤
((normℎ‘(((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))))↑2)) |
50 | | normcl 27366 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ ℋ →
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ ℝ) |
51 | 44, 50 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ ℝ) |
52 | 51 | resqcld 12897 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))↑2) ∈ ℝ) |
53 | 48 | resqcld 12897 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
((normℎ‘(((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))))↑2) ∈ ℝ) |
54 | 52, 53 | addge01d 10494 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (0 ≤
((normℎ‘(((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))))↑2) ↔
((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))↑2) ≤
(((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))↑2) +
((normℎ‘(((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))))↑2)))) |
55 | 49, 54 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))↑2) ≤
(((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))↑2) +
((normℎ‘(((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))))↑2))) |
56 | 18 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 𝐴 ∈ Sℋ
) |
57 | 36 | adantrr 749 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝐹‘𝑗) ∈ 𝐴) |
58 | | shsubcl 27461 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈
Sℋ ∧ (𝐹‘𝑗) ∈ 𝐴 ∧ (𝐹‘𝑘) ∈ 𝐴) → ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ 𝐴) |
59 | 56, 57, 41, 58 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ 𝐴) |
60 | | hvsubsub4 27301 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐻‘𝑗) ∈ ℋ ∧ (𝐻‘𝑘) ∈ ℋ) ∧ ((𝐹‘𝑗) ∈ ℋ ∧ (𝐹‘𝑘) ∈ ℋ)) → (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) = (((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) −ℎ ((𝐻‘𝑘) −ℎ (𝐹‘𝑘)))) |
61 | 28, 32, 38, 42, 60 | syl22anc 1319 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) = (((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) −ℎ ((𝐻‘𝑘) −ℎ (𝐹‘𝑘)))) |
62 | | ocsh 27526 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ⊆ ℋ →
(⊥‘𝐴) ∈
Sℋ ) |
63 | 39, 62 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (⊥‘𝐴) ∈
Sℋ ) |
64 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 = 𝑗 → (𝐻‘𝑛) = (𝐻‘𝑗)) |
65 | 64 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 = 𝑗 → ((projℎ‘𝐴)‘(𝐻‘𝑛)) = ((projℎ‘𝐴)‘(𝐻‘𝑗))) |
66 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((projℎ‘𝐴)‘(𝐻‘𝑗)) ∈ V |
67 | 65, 6, 66 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑗 ∈ ℕ → (𝐹‘𝑗) = ((projℎ‘𝐴)‘(𝐻‘𝑗))) |
68 | 67 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ∈ ℕ →
((projℎ‘𝐴)‘(𝐻‘𝑗)) = (𝐹‘𝑗)) |
69 | 68 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
((projℎ‘𝐴)‘(𝐻‘𝑗)) = (𝐹‘𝑗)) |
70 | 1 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐴 ∈ Cℋ
) |
71 | 9, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (⊥‘𝐴) ∈
Sℋ ) |
72 | | shless 27602 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐵 ∈
Sℋ ∧ (⊥‘𝐴) ∈ Sℋ
∧ 𝐴 ∈
Sℋ ) ∧ 𝐵 ⊆ (⊥‘𝐴)) → (𝐵 +ℋ 𝐴) ⊆ ((⊥‘𝐴) +ℋ 𝐴)) |
73 | 20, 71, 18, 3, 72 | syl31anc 1321 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝐵 +ℋ 𝐴) ⊆ ((⊥‘𝐴) +ℋ 𝐴)) |
74 | | shscom 27562 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
→ (𝐴
+ℋ 𝐵) =
(𝐵 +ℋ
𝐴)) |
75 | 18, 20, 74 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝐴 +ℋ 𝐵) = (𝐵 +ℋ 𝐴)) |
76 | | shscom 27562 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈
Sℋ ∧ (⊥‘𝐴) ∈ Sℋ )
→ (𝐴
+ℋ (⊥‘𝐴)) = ((⊥‘𝐴) +ℋ 𝐴)) |
77 | 18, 71, 76 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝐴 +ℋ (⊥‘𝐴)) = ((⊥‘𝐴) +ℋ 𝐴)) |
78 | 73, 75, 77 | 3sstr4d 3611 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝐴 +ℋ 𝐵) ⊆ (𝐴 +ℋ (⊥‘𝐴))) |
79 | 78 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴 +ℋ 𝐵) ⊆ (𝐴 +ℋ (⊥‘𝐴))) |
80 | 79, 26 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐻‘𝑗) ∈ (𝐴 +ℋ (⊥‘𝐴))) |
81 | | pjpreeq 27641 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈
Cℋ ∧ (𝐻‘𝑗) ∈ (𝐴 +ℋ (⊥‘𝐴))) →
(((projℎ‘𝐴)‘(𝐻‘𝑗)) = (𝐹‘𝑗) ↔ ((𝐹‘𝑗) ∈ 𝐴 ∧ ∃𝑥 ∈ (⊥‘𝐴)(𝐻‘𝑗) = ((𝐹‘𝑗) +ℎ 𝑥)))) |
82 | 70, 80, 81 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
(((projℎ‘𝐴)‘(𝐻‘𝑗)) = (𝐹‘𝑗) ↔ ((𝐹‘𝑗) ∈ 𝐴 ∧ ∃𝑥 ∈ (⊥‘𝐴)(𝐻‘𝑗) = ((𝐹‘𝑗) +ℎ 𝑥)))) |
83 | 69, 82 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗) ∈ 𝐴 ∧ ∃𝑥 ∈ (⊥‘𝐴)(𝐻‘𝑗) = ((𝐹‘𝑗) +ℎ 𝑥))) |
84 | 83 | simprd 478 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∃𝑥 ∈ (⊥‘𝐴)(𝐻‘𝑗) = ((𝐹‘𝑗) +ℎ 𝑥)) |
85 | 27 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ (⊥‘𝐴)) → (𝐻‘𝑗) ∈ ℋ) |
86 | 37 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ (⊥‘𝐴)) → (𝐹‘𝑗) ∈ ℋ) |
87 | | shss 27451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((⊥‘𝐴)
∈ Sℋ → (⊥‘𝐴) ⊆
ℋ) |
88 | 71, 87 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (⊥‘𝐴) ⊆
ℋ) |
89 | 88 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (⊥‘𝐴) ⊆
ℋ) |
90 | 89 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ (⊥‘𝐴)) → 𝑥 ∈ ℋ) |
91 | | hvsubadd 27318 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐻‘𝑗) ∈ ℋ ∧ (𝐹‘𝑗) ∈ ℋ ∧ 𝑥 ∈ ℋ) → (((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) = 𝑥 ↔ ((𝐹‘𝑗) +ℎ 𝑥) = (𝐻‘𝑗))) |
92 | 85, 86, 90, 91 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ (⊥‘𝐴)) → (((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) = 𝑥 ↔ ((𝐹‘𝑗) +ℎ 𝑥) = (𝐻‘𝑗))) |
93 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = ((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) ↔ ((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) = 𝑥) |
94 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐻‘𝑗) = ((𝐹‘𝑗) +ℎ 𝑥) ↔ ((𝐹‘𝑗) +ℎ 𝑥) = (𝐻‘𝑗)) |
95 | 92, 93, 94 | 3bitr4g 302 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ (⊥‘𝐴)) → (𝑥 = ((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) ↔ (𝐻‘𝑗) = ((𝐹‘𝑗) +ℎ 𝑥))) |
96 | 95 | rexbidva 3031 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (∃𝑥 ∈ (⊥‘𝐴)𝑥 = ((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) ↔ ∃𝑥 ∈ (⊥‘𝐴)(𝐻‘𝑗) = ((𝐹‘𝑗) +ℎ 𝑥))) |
97 | 84, 96 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∃𝑥 ∈ (⊥‘𝐴)𝑥 = ((𝐻‘𝑗) −ℎ (𝐹‘𝑗))) |
98 | | risset 3044 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) ∈ (⊥‘𝐴) ↔ ∃𝑥 ∈ (⊥‘𝐴)𝑥 = ((𝐻‘𝑗) −ℎ (𝐹‘𝑗))) |
99 | 97, 98 | sylibr 223 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) ∈ (⊥‘𝐴)) |
100 | 99 | adantrr 749 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) ∈ (⊥‘𝐴)) |
101 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = 𝑘 → (𝑗 ∈ ℕ ↔ 𝑘 ∈ ℕ)) |
102 | 101 | anbi2d 736 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 𝑘 → ((𝜑 ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ 𝑘 ∈ ℕ))) |
103 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 = 𝑘 → (𝐻‘𝑗) = (𝐻‘𝑘)) |
104 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 = 𝑘 → (𝐹‘𝑗) = (𝐹‘𝑘)) |
105 | 103, 104 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = 𝑘 → ((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) = ((𝐻‘𝑘) −ℎ (𝐹‘𝑘))) |
106 | 105 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 𝑘 → (((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) ∈ (⊥‘𝐴) ↔ ((𝐻‘𝑘) −ℎ (𝐹‘𝑘)) ∈ (⊥‘𝐴))) |
107 | 102, 106 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = 𝑘 → (((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) ∈ (⊥‘𝐴)) ↔ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐻‘𝑘) −ℎ (𝐹‘𝑘)) ∈ (⊥‘𝐴)))) |
108 | 107, 99 | chvarv 2251 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐻‘𝑘) −ℎ (𝐹‘𝑘)) ∈ (⊥‘𝐴)) |
109 | 108 | adantrl 748 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((𝐻‘𝑘) −ℎ (𝐹‘𝑘)) ∈ (⊥‘𝐴)) |
110 | | shsubcl 27461 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊥‘𝐴)
∈ Sℋ ∧ ((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) ∈ (⊥‘𝐴) ∧ ((𝐻‘𝑘) −ℎ (𝐹‘𝑘)) ∈ (⊥‘𝐴)) → (((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) −ℎ ((𝐻‘𝑘) −ℎ (𝐹‘𝑘))) ∈ (⊥‘𝐴)) |
111 | 63, 100, 109, 110 | syl3anc 1318 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) −ℎ ((𝐻‘𝑘) −ℎ (𝐹‘𝑘))) ∈ (⊥‘𝐴)) |
112 | 61, 111 | eqeltrd 2688 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ (⊥‘𝐴)) |
113 | | shocorth 27535 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈
Sℋ → ((((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ 𝐴 ∧ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ (⊥‘𝐴)) → (((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ·ih
(((𝐻‘𝑗) −ℎ
(𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) = 0)) |
114 | 56, 113 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ 𝐴 ∧ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ (⊥‘𝐴)) → (((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ·ih
(((𝐻‘𝑗) −ℎ
(𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) = 0)) |
115 | 59, 112, 114 | mp2and 711 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ·ih
(((𝐻‘𝑗) −ℎ
(𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) = 0) |
116 | | normpyth 27386 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ ℋ ∧ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ ℋ) → ((((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ·ih
(((𝐻‘𝑗) −ℎ
(𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) = 0 →
((normℎ‘(((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) +ℎ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))))↑2) =
(((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))↑2) +
((normℎ‘(((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))))↑2)))) |
117 | 44, 46, 116 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ·ih
(((𝐻‘𝑗) −ℎ
(𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) = 0 →
((normℎ‘(((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) +ℎ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))))↑2) =
(((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))↑2) +
((normℎ‘(((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))))↑2)))) |
118 | 115, 117 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
((normℎ‘(((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) +ℎ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))))↑2) =
(((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))↑2) +
((normℎ‘(((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))))↑2))) |
119 | | hvpncan3 27283 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ ℋ ∧ ((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) ∈ ℋ) → (((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) +ℎ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) = ((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) |
120 | 44, 34, 119 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) +ℎ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) = ((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) |
121 | 120 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
(normℎ‘(((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) +ℎ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))))) =
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘)))) |
122 | 121 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
((normℎ‘(((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) +ℎ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))))↑2) =
((normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘)))↑2)) |
123 | 118, 122 | eqtr3d 2646 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
(((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))↑2) +
((normℎ‘(((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))))↑2)) =
((normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘)))↑2)) |
124 | 55, 123 | breqtrd 4609 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))↑2) ≤
((normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘)))↑2)) |
125 | | normcl 27366 |
. . . . . . . . . . . . . 14
⊢ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) ∈ ℋ →
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) ∈ ℝ) |
126 | 34, 125 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) ∈ ℝ) |
127 | | normge0 27367 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ ℋ → 0 ≤
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) |
128 | 44, 127 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 0 ≤
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) |
129 | | normge0 27367 |
. . . . . . . . . . . . . 14
⊢ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) ∈ ℋ → 0 ≤
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘)))) |
130 | 34, 129 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 0 ≤
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘)))) |
131 | 51, 126, 128, 130 | le2sqd 12906 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ≤
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) ↔
((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))↑2) ≤
((normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘)))↑2))) |
132 | 124, 131 | mpbird 246 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ≤
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘)))) |
133 | 132 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ≤
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘)))) |
134 | 51 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ ℝ) |
135 | 126 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) ∈ ℝ) |
136 | | rpre 11715 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
137 | 136 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 𝑥 ∈
ℝ) |
138 | | lelttr 10007 |
. . . . . . . . . . 11
⊢
(((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ ℝ ∧
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) ∈ ℝ ∧ 𝑥 ∈ ℝ) →
(((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ≤
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) ∧
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) < 𝑥) →
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) < 𝑥)) |
139 | 134, 135,
137, 138 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
(((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ≤
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) ∧
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) < 𝑥) →
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) < 𝑥)) |
140 | 133, 139 | mpand 707 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
((normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) < 𝑥 →
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) < 𝑥)) |
141 | 140 | anassrs 678 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ℕ) →
((normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) < 𝑥 →
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) < 𝑥)) |
142 | 16, 141 | syldan 486 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) →
((normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) < 𝑥 →
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) < 𝑥)) |
143 | 142 | ralimdva 2945 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) →
(∀𝑘 ∈
(ℤ≥‘𝑗)(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) < 𝑥 → ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) < 𝑥)) |
144 | 143 | reximdva 3000 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) < 𝑥 → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) < 𝑥)) |
145 | 14, 144 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) < 𝑥) |
146 | 145 | ralrimiva 2949 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) < 𝑥) |
147 | | hcau 27425 |
. . 3
⊢ (𝐹 ∈ Cauchy ↔ (𝐹:ℕ⟶ ℋ ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) < 𝑥)) |
148 | 10, 146, 147 | sylanbrc 695 |
. 2
⊢ (𝜑 → 𝐹 ∈ Cauchy) |
149 | | ax-hcompl 27443 |
. 2
⊢ (𝐹 ∈ Cauchy →
∃𝑥 ∈ ℋ
𝐹
⇝𝑣 𝑥) |
150 | | hlimf 27478 |
. . . . 5
⊢
⇝𝑣 :dom ⇝𝑣 ⟶
ℋ |
151 | | ffn 5958 |
. . . . 5
⊢ (
⇝𝑣 :dom ⇝𝑣 ⟶ ℋ
→ ⇝𝑣 Fn dom ⇝𝑣
) |
152 | 150, 151 | ax-mp 5 |
. . . 4
⊢
⇝𝑣 Fn dom ⇝𝑣 |
153 | | fnbr 5907 |
. . . 4
⊢ ((
⇝𝑣 Fn dom ⇝𝑣 ∧ 𝐹 ⇝𝑣
𝑥) → 𝐹 ∈ dom ⇝𝑣
) |
154 | 152, 153 | mpan 702 |
. . 3
⊢ (𝐹 ⇝𝑣
𝑥 → 𝐹 ∈ dom ⇝𝑣
) |
155 | 154 | rexlimivw 3011 |
. 2
⊢
(∃𝑥 ∈
ℋ 𝐹
⇝𝑣 𝑥 → 𝐹 ∈ dom ⇝𝑣
) |
156 | 148, 149,
155 | 3syl 18 |
1
⊢ (𝜑 → 𝐹 ∈ dom ⇝𝑣
) |