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 28496 |
. . . 4
⊢ (𝜑 → 𝐹:ℕ⟶𝐴) |
8 | | chss 28086 |
. . . . 5
⊢ (𝐴 ∈
Cℋ → 𝐴 ⊆ ℋ) |
9 | 1, 8 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ ℋ) |
10 | 7, 9 | fssd 6057 |
. . 3
⊢ (𝜑 → 𝐹:ℕ⟶ ℋ) |
11 | | hlimcaui 28093 |
. . . . . . 7
⊢ (𝐻 ⇝𝑣
𝑢 → 𝐻 ∈ Cauchy) |
12 | 5, 11 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐻 ∈ Cauchy) |
13 | | hcaucvg 28043 |
. . . . . 6
⊢ ((𝐻 ∈ Cauchy ∧ 𝑥 ∈ ℝ+)
→ ∃𝑗 ∈
ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) < 𝑥) |
14 | 12, 13 | sylan 488 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) < 𝑥) |
15 | | eluznn 11758 |
. . . . . . . . 9
⊢ ((𝑗 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → 𝑘 ∈ ℕ) |
16 | 15 | adantll 750 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → 𝑘 ∈ ℕ) |
17 | | chsh 28081 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ∈
Cℋ → 𝐴 ∈ Sℋ
) |
18 | 1, 17 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐴 ∈ Sℋ
) |
19 | | chsh 28081 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐵 ∈
Cℋ → 𝐵 ∈ Sℋ
) |
20 | 2, 19 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐵 ∈ Sℋ
) |
21 | | shscl 28177 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
→ (𝐴
+ℋ 𝐵)
∈ Sℋ ) |
22 | 18, 20, 21 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐴 +ℋ 𝐵) ∈ Sℋ
) |
23 | | shss 28067 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 +ℋ 𝐵) ∈
Sℋ → (𝐴 +ℋ 𝐵) ⊆ ℋ) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐴 +ℋ 𝐵) ⊆ ℋ) |
25 | 24 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴 +ℋ 𝐵) ⊆ ℋ) |
26 | 4 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐻‘𝑗) ∈ (𝐴 +ℋ 𝐵)) |
27 | 25, 26 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐻‘𝑗) ∈ ℋ) |
28 | 27 | adantrr 753 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝐻‘𝑗) ∈ ℋ) |
29 | 4, 24 | fssd 6057 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐻:ℕ⟶ ℋ) |
30 | 29 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 𝐻:ℕ⟶ ℋ) |
31 | | simprr 796 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 𝑘 ∈ ℕ) |
32 | 30, 31 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝐻‘𝑘) ∈ ℋ) |
33 | | hvsubcl 27874 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐻‘𝑗) ∈ ℋ ∧ (𝐻‘𝑘) ∈ ℋ) → ((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) ∈ ℋ) |
34 | 28, 32, 33 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) ∈ ℋ) |
35 | 9 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐴 ⊆ ℋ) |
36 | 7 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ 𝐴) |
37 | 35, 36 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ ℋ) |
38 | 37 | adantrr 753 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝐹‘𝑗) ∈ ℋ) |
39 | 9 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 𝐴 ⊆ ℋ) |
40 | 7 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 𝐹:ℕ⟶𝐴) |
41 | 40, 31 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝐹‘𝑘) ∈ 𝐴) |
42 | 39, 41 | sseldd 3604 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝐹‘𝑘) ∈ ℋ) |
43 | | hvsubcl 27874 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹‘𝑗) ∈ ℋ ∧ (𝐹‘𝑘) ∈ ℋ) → ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ ℋ) |
44 | 38, 42, 43 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ ℋ) |
45 | | hvsubcl 27874 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) ∈ ℋ ∧ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ ℋ) → (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ ℋ) |
46 | 34, 44, 45 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ ℋ) |
47 | | normcl 27982 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ ℋ →
(normℎ‘(((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) ∈ ℝ) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
(normℎ‘(((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) ∈ ℝ) |
49 | 48 | sqge0d 13036 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 0 ≤
((normℎ‘(((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))))↑2)) |
50 | | normcl 27982 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ ℋ →
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ ℝ) |
51 | 44, 50 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ ℝ) |
52 | 51 | resqcld 13035 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))↑2) ∈ ℝ) |
53 | 48 | resqcld 13035 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
((normℎ‘(((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))))↑2) ∈ ℝ) |
54 | 52, 53 | addge01d 10615 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (0 ≤
((normℎ‘(((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))))↑2) ↔
((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))↑2) ≤
(((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))↑2) +
((normℎ‘(((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))))↑2)))) |
55 | 49, 54 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))↑2) ≤
(((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))↑2) +
((normℎ‘(((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))))↑2))) |
56 | 18 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 𝐴 ∈ Sℋ
) |
57 | 36 | adantrr 753 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝐹‘𝑗) ∈ 𝐴) |
58 | | shsubcl 28077 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈
Sℋ ∧ (𝐹‘𝑗) ∈ 𝐴 ∧ (𝐹‘𝑘) ∈ 𝐴) → ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ 𝐴) |
59 | 56, 57, 41, 58 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ 𝐴) |
60 | | hvsubsub4 27917 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐻‘𝑗) ∈ ℋ ∧ (𝐻‘𝑘) ∈ ℋ) ∧ ((𝐹‘𝑗) ∈ ℋ ∧ (𝐹‘𝑘) ∈ ℋ)) → (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) = (((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) −ℎ ((𝐻‘𝑘) −ℎ (𝐹‘𝑘)))) |
61 | 28, 32, 38, 42, 60 | syl22anc 1327 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) = (((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) −ℎ ((𝐻‘𝑘) −ℎ (𝐹‘𝑘)))) |
62 | | ocsh 28142 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ⊆ ℋ →
(⊥‘𝐴) ∈
Sℋ ) |
63 | 39, 62 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (⊥‘𝐴) ∈
Sℋ ) |
64 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 = 𝑗 → (𝐻‘𝑛) = (𝐻‘𝑗)) |
65 | 64 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 = 𝑗 → ((projℎ‘𝐴)‘(𝐻‘𝑛)) = ((projℎ‘𝐴)‘(𝐻‘𝑗))) |
66 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((projℎ‘𝐴)‘(𝐻‘𝑗)) ∈ V |
67 | 65, 6, 66 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑗 ∈ ℕ → (𝐹‘𝑗) = ((projℎ‘𝐴)‘(𝐻‘𝑗))) |
68 | 67 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ∈ ℕ →
((projℎ‘𝐴)‘(𝐻‘𝑗)) = (𝐹‘𝑗)) |
69 | 68 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
((projℎ‘𝐴)‘(𝐻‘𝑗)) = (𝐹‘𝑗)) |
70 | 1 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐴 ∈ Cℋ
) |
71 | 9, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (⊥‘𝐴) ∈
Sℋ ) |
72 | | shless 28218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐵 ∈
Sℋ ∧ (⊥‘𝐴) ∈ Sℋ
∧ 𝐴 ∈
Sℋ ) ∧ 𝐵 ⊆ (⊥‘𝐴)) → (𝐵 +ℋ 𝐴) ⊆ ((⊥‘𝐴) +ℋ 𝐴)) |
73 | 20, 71, 18, 3, 72 | syl31anc 1329 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝐵 +ℋ 𝐴) ⊆ ((⊥‘𝐴) +ℋ 𝐴)) |
74 | | shscom 28178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
→ (𝐴
+ℋ 𝐵) =
(𝐵 +ℋ
𝐴)) |
75 | 18, 20, 74 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝐴 +ℋ 𝐵) = (𝐵 +ℋ 𝐴)) |
76 | | shscom 28178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈
Sℋ ∧ (⊥‘𝐴) ∈ Sℋ )
→ (𝐴
+ℋ (⊥‘𝐴)) = ((⊥‘𝐴) +ℋ 𝐴)) |
77 | 18, 71, 76 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝐴 +ℋ (⊥‘𝐴)) = ((⊥‘𝐴) +ℋ 𝐴)) |
78 | 73, 75, 77 | 3sstr4d 3648 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝐴 +ℋ 𝐵) ⊆ (𝐴 +ℋ (⊥‘𝐴))) |
79 | 78 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴 +ℋ 𝐵) ⊆ (𝐴 +ℋ (⊥‘𝐴))) |
80 | 79, 26 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐻‘𝑗) ∈ (𝐴 +ℋ (⊥‘𝐴))) |
81 | | pjpreeq 28257 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈
Cℋ ∧ (𝐻‘𝑗) ∈ (𝐴 +ℋ (⊥‘𝐴))) →
(((projℎ‘𝐴)‘(𝐻‘𝑗)) = (𝐹‘𝑗) ↔ ((𝐹‘𝑗) ∈ 𝐴 ∧ ∃𝑥 ∈ (⊥‘𝐴)(𝐻‘𝑗) = ((𝐹‘𝑗) +ℎ 𝑥)))) |
82 | 70, 80, 81 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
(((projℎ‘𝐴)‘(𝐻‘𝑗)) = (𝐹‘𝑗) ↔ ((𝐹‘𝑗) ∈ 𝐴 ∧ ∃𝑥 ∈ (⊥‘𝐴)(𝐻‘𝑗) = ((𝐹‘𝑗) +ℎ 𝑥)))) |
83 | 69, 82 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗) ∈ 𝐴 ∧ ∃𝑥 ∈ (⊥‘𝐴)(𝐻‘𝑗) = ((𝐹‘𝑗) +ℎ 𝑥))) |
84 | 83 | simprd 479 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∃𝑥 ∈ (⊥‘𝐴)(𝐻‘𝑗) = ((𝐹‘𝑗) +ℎ 𝑥)) |
85 | 27 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ (⊥‘𝐴)) → (𝐻‘𝑗) ∈ ℋ) |
86 | 37 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ (⊥‘𝐴)) → (𝐹‘𝑗) ∈ ℋ) |
87 | | shss 28067 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((⊥‘𝐴)
∈ Sℋ → (⊥‘𝐴) ⊆
ℋ) |
88 | 71, 87 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (⊥‘𝐴) ⊆
ℋ) |
89 | 88 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (⊥‘𝐴) ⊆
ℋ) |
90 | 89 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ (⊥‘𝐴)) → 𝑥 ∈ ℋ) |
91 | | hvsubadd 27934 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐻‘𝑗) ∈ ℋ ∧ (𝐹‘𝑗) ∈ ℋ ∧ 𝑥 ∈ ℋ) → (((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) = 𝑥 ↔ ((𝐹‘𝑗) +ℎ 𝑥) = (𝐻‘𝑗))) |
92 | 85, 86, 90, 91 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ (⊥‘𝐴)) → (((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) = 𝑥 ↔ ((𝐹‘𝑗) +ℎ 𝑥) = (𝐻‘𝑗))) |
93 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = ((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) ↔ ((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) = 𝑥) |
94 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐻‘𝑗) = ((𝐹‘𝑗) +ℎ 𝑥) ↔ ((𝐹‘𝑗) +ℎ 𝑥) = (𝐻‘𝑗)) |
95 | 92, 93, 94 | 3bitr4g 303 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ (⊥‘𝐴)) → (𝑥 = ((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) ↔ (𝐻‘𝑗) = ((𝐹‘𝑗) +ℎ 𝑥))) |
96 | 95 | rexbidva 3049 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (∃𝑥 ∈ (⊥‘𝐴)𝑥 = ((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) ↔ ∃𝑥 ∈ (⊥‘𝐴)(𝐻‘𝑗) = ((𝐹‘𝑗) +ℎ 𝑥))) |
97 | 84, 96 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∃𝑥 ∈ (⊥‘𝐴)𝑥 = ((𝐻‘𝑗) −ℎ (𝐹‘𝑗))) |
98 | | risset 3062 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) ∈ (⊥‘𝐴) ↔ ∃𝑥 ∈ (⊥‘𝐴)𝑥 = ((𝐻‘𝑗) −ℎ (𝐹‘𝑗))) |
99 | 97, 98 | sylibr 224 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) ∈ (⊥‘𝐴)) |
100 | 99 | adantrr 753 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) ∈ (⊥‘𝐴)) |
101 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = 𝑘 → (𝑗 ∈ ℕ ↔ 𝑘 ∈ ℕ)) |
102 | 101 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 𝑘 → ((𝜑 ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ 𝑘 ∈ ℕ))) |
103 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 = 𝑘 → (𝐻‘𝑗) = (𝐻‘𝑘)) |
104 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 = 𝑘 → (𝐹‘𝑗) = (𝐹‘𝑘)) |
105 | 103, 104 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = 𝑘 → ((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) = ((𝐻‘𝑘) −ℎ (𝐹‘𝑘))) |
106 | 105 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 𝑘 → (((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) ∈ (⊥‘𝐴) ↔ ((𝐻‘𝑘) −ℎ (𝐹‘𝑘)) ∈ (⊥‘𝐴))) |
107 | 102, 106 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = 𝑘 → (((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) ∈ (⊥‘𝐴)) ↔ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐻‘𝑘) −ℎ (𝐹‘𝑘)) ∈ (⊥‘𝐴)))) |
108 | 107, 99 | chvarv 2263 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐻‘𝑘) −ℎ (𝐹‘𝑘)) ∈ (⊥‘𝐴)) |
109 | 108 | adantrl 752 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((𝐻‘𝑘) −ℎ (𝐹‘𝑘)) ∈ (⊥‘𝐴)) |
110 | | shsubcl 28077 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊥‘𝐴)
∈ Sℋ ∧ ((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) ∈ (⊥‘𝐴) ∧ ((𝐻‘𝑘) −ℎ (𝐹‘𝑘)) ∈ (⊥‘𝐴)) → (((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) −ℎ ((𝐻‘𝑘) −ℎ (𝐹‘𝑘))) ∈ (⊥‘𝐴)) |
111 | 63, 100, 109, 110 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) −ℎ ((𝐻‘𝑘) −ℎ (𝐹‘𝑘))) ∈ (⊥‘𝐴)) |
112 | 61, 111 | eqeltrd 2701 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ (⊥‘𝐴)) |
113 | | shocorth 28151 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈
Sℋ → ((((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ 𝐴 ∧ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ (⊥‘𝐴)) → (((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ·ih
(((𝐻‘𝑗) −ℎ
(𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) = 0)) |
114 | 56, 113 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ 𝐴 ∧ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ (⊥‘𝐴)) → (((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ·ih
(((𝐻‘𝑗) −ℎ
(𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) = 0)) |
115 | 59, 112, 114 | mp2and 715 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ·ih
(((𝐻‘𝑗) −ℎ
(𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) = 0) |
116 | | normpyth 28002 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ ℋ ∧ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ ℋ) → ((((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ·ih
(((𝐻‘𝑗) −ℎ
(𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) = 0 →
((normℎ‘(((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) +ℎ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))))↑2) =
(((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))↑2) +
((normℎ‘(((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))))↑2)))) |
117 | 44, 46, 116 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ·ih
(((𝐻‘𝑗) −ℎ
(𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) = 0 →
((normℎ‘(((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) +ℎ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))))↑2) =
(((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))↑2) +
((normℎ‘(((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))))↑2)))) |
118 | 115, 117 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
((normℎ‘(((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) +ℎ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))))↑2) =
(((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))↑2) +
((normℎ‘(((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))))↑2))) |
119 | | hvpncan3 27899 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ ℋ ∧ ((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) ∈ ℋ) → (((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) +ℎ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) = ((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) |
120 | 44, 34, 119 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) +ℎ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) = ((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) |
121 | 120 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
(normℎ‘(((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) +ℎ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))))) =
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘)))) |
122 | 121 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
((normℎ‘(((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) +ℎ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))))↑2) =
((normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘)))↑2)) |
123 | 118, 122 | eqtr3d 2658 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
(((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))↑2) +
((normℎ‘(((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))))↑2)) =
((normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘)))↑2)) |
124 | 55, 123 | breqtrd 4679 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))↑2) ≤
((normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘)))↑2)) |
125 | | normcl 27982 |
. . . . . . . . . . . . . 14
⊢ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) ∈ ℋ →
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) ∈ ℝ) |
126 | 34, 125 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) ∈ ℝ) |
127 | | normge0 27983 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ ℋ → 0 ≤
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) |
128 | 44, 127 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 0 ≤
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) |
129 | | normge0 27983 |
. . . . . . . . . . . . . 14
⊢ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) ∈ ℋ → 0 ≤
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘)))) |
130 | 34, 129 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 0 ≤
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘)))) |
131 | 51, 126, 128, 130 | le2sqd 13044 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ≤
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) ↔
((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))↑2) ≤
((normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘)))↑2))) |
132 | 124, 131 | mpbird 247 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ≤
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘)))) |
133 | 132 | adantlr 751 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ≤
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘)))) |
134 | 51 | adantlr 751 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ ℝ) |
135 | 126 | adantlr 751 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) ∈ ℝ) |
136 | | rpre 11839 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
137 | 136 | ad2antlr 763 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 𝑥 ∈
ℝ) |
138 | | lelttr 10128 |
. . . . . . . . . . 11
⊢
(((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ ℝ ∧
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) ∈ ℝ ∧ 𝑥 ∈ ℝ) →
(((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ≤
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) ∧
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) < 𝑥) →
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) < 𝑥)) |
139 | 134, 135,
137, 138 | syl3anc 1326 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
(((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ≤
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) ∧
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) < 𝑥) →
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) < 𝑥)) |
140 | 133, 139 | mpand 711 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
((normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) < 𝑥 →
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) < 𝑥)) |
141 | 140 | anassrs 680 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ℕ) →
((normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) < 𝑥 →
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) < 𝑥)) |
142 | 16, 141 | syldan 487 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) →
((normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) < 𝑥 →
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) < 𝑥)) |
143 | 142 | ralimdva 2962 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) →
(∀𝑘 ∈
(ℤ≥‘𝑗)(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) < 𝑥 → ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) < 𝑥)) |
144 | 143 | reximdva 3017 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) < 𝑥 → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) < 𝑥)) |
145 | 14, 144 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) < 𝑥) |
146 | 145 | ralrimiva 2966 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) < 𝑥) |
147 | | hcau 28041 |
. . 3
⊢ (𝐹 ∈ Cauchy ↔ (𝐹:ℕ⟶ ℋ ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) < 𝑥)) |
148 | 10, 146, 147 | sylanbrc 698 |
. 2
⊢ (𝜑 → 𝐹 ∈ Cauchy) |
149 | | ax-hcompl 28059 |
. 2
⊢ (𝐹 ∈ Cauchy →
∃𝑥 ∈ ℋ
𝐹
⇝𝑣 𝑥) |
150 | | hlimf 28094 |
. . . . 5
⊢
⇝𝑣 :dom ⇝𝑣 ⟶
ℋ |
151 | | ffn 6045 |
. . . . 5
⊢ (
⇝𝑣 :dom ⇝𝑣 ⟶ ℋ
→ ⇝𝑣 Fn dom ⇝𝑣
) |
152 | 150, 151 | ax-mp 5 |
. . . 4
⊢
⇝𝑣 Fn dom ⇝𝑣 |
153 | | fnbr 5993 |
. . . 4
⊢ ((
⇝𝑣 Fn dom ⇝𝑣 ∧ 𝐹 ⇝𝑣
𝑥) → 𝐹 ∈ dom ⇝𝑣
) |
154 | 152, 153 | mpan 706 |
. . 3
⊢ (𝐹 ⇝𝑣
𝑥 → 𝐹 ∈ dom ⇝𝑣
) |
155 | 154 | rexlimivw 3029 |
. 2
⊢
(∃𝑥 ∈
ℋ 𝐹
⇝𝑣 𝑥 → 𝐹 ∈ dom ⇝𝑣
) |
156 | 148, 149,
155 | 3syl 18 |
1
⊢ (𝜑 → 𝐹 ∈ dom ⇝𝑣
) |