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 30008 |
. . . 4
⊢ (𝜑 → 𝐹:ℕ⟶𝐴) |
8 | | chss 29600 |
. . . . 5
⊢ (𝐴 ∈
Cℋ → 𝐴 ⊆ ℋ) |
9 | 1, 8 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ ℋ) |
10 | 7, 9 | fssd 6627 |
. . 3
⊢ (𝜑 → 𝐹:ℕ⟶ ℋ) |
11 | | hlimcaui 29607 |
. . . . . . 7
⊢ (𝐻 ⇝𝑣
𝑢 → 𝐻 ∈ Cauchy) |
12 | 5, 11 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐻 ∈ Cauchy) |
13 | | hcaucvg 29557 |
. . . . . 6
⊢ ((𝐻 ∈ Cauchy ∧ 𝑥 ∈ ℝ+)
→ ∃𝑗 ∈
ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) < 𝑥) |
14 | 12, 13 | sylan 580 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) < 𝑥) |
15 | | eluznn 12667 |
. . . . . . . . 9
⊢ ((𝑗 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → 𝑘 ∈ ℕ) |
16 | 15 | adantll 711 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → 𝑘 ∈ ℕ) |
17 | | chsh 29595 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ∈
Cℋ → 𝐴 ∈ Sℋ
) |
18 | 1, 17 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐴 ∈ Sℋ
) |
19 | | chsh 29595 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐵 ∈
Cℋ → 𝐵 ∈ Sℋ
) |
20 | 2, 19 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐵 ∈ Sℋ
) |
21 | | shscl 29689 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
→ (𝐴
+ℋ 𝐵)
∈ Sℋ ) |
22 | 18, 20, 21 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐴 +ℋ 𝐵) ∈ Sℋ
) |
23 | | shss 29581 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 +ℋ 𝐵) ∈
Sℋ → (𝐴 +ℋ 𝐵) ⊆ ℋ) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐴 +ℋ 𝐵) ⊆ ℋ) |
25 | 24 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴 +ℋ 𝐵) ⊆ ℋ) |
26 | 4 | ffvelrnda 6970 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐻‘𝑗) ∈ (𝐴 +ℋ 𝐵)) |
27 | 25, 26 | sseldd 3923 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐻‘𝑗) ∈ ℋ) |
28 | 27 | adantrr 714 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝐻‘𝑗) ∈ ℋ) |
29 | 4, 24 | fssd 6627 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐻:ℕ⟶ ℋ) |
30 | 29 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 𝐻:ℕ⟶ ℋ) |
31 | | simprr 770 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 𝑘 ∈ ℕ) |
32 | 30, 31 | ffvelrnd 6971 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝐻‘𝑘) ∈ ℋ) |
33 | | hvsubcl 29388 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐻‘𝑗) ∈ ℋ ∧ (𝐻‘𝑘) ∈ ℋ) → ((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) ∈ ℋ) |
34 | 28, 32, 33 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) ∈ ℋ) |
35 | 9 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐴 ⊆ ℋ) |
36 | 7 | ffvelrnda 6970 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ 𝐴) |
37 | 35, 36 | sseldd 3923 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ ℋ) |
38 | 37 | adantrr 714 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝐹‘𝑗) ∈ ℋ) |
39 | 9 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 𝐴 ⊆ ℋ) |
40 | 7 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 𝐹:ℕ⟶𝐴) |
41 | 40, 31 | ffvelrnd 6971 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝐹‘𝑘) ∈ 𝐴) |
42 | 39, 41 | sseldd 3923 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝐹‘𝑘) ∈ ℋ) |
43 | | hvsubcl 29388 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹‘𝑗) ∈ ℋ ∧ (𝐹‘𝑘) ∈ ℋ) → ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ ℋ) |
44 | 38, 42, 43 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ ℋ) |
45 | | hvsubcl 29388 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) ∈ ℋ ∧ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ ℋ) → (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ ℋ) |
46 | 34, 44, 45 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ ℋ) |
47 | | normcl 29496 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ ℋ →
(normℎ‘(((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) ∈ ℝ) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
(normℎ‘(((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) ∈ ℝ) |
49 | 48 | sqge0d 13975 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 0 ≤
((normℎ‘(((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))))↑2)) |
50 | | normcl 29496 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ ℋ →
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ ℝ) |
51 | 44, 50 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ ℝ) |
52 | 51 | resqcld 13974 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))↑2) ∈ ℝ) |
53 | 48 | resqcld 13974 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
((normℎ‘(((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))))↑2) ∈ ℝ) |
54 | 52, 53 | addge01d 11572 |
. . . . . . . . . . . . . 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 714 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝐹‘𝑗) ∈ 𝐴) |
58 | | shsubcl 29591 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈
Sℋ ∧ (𝐹‘𝑗) ∈ 𝐴 ∧ (𝐹‘𝑘) ∈ 𝐴) → ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ 𝐴) |
59 | 56, 57, 41, 58 | syl3anc 1370 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ 𝐴) |
60 | | hvsubsub4 29431 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐻‘𝑗) ∈ ℋ ∧ (𝐻‘𝑘) ∈ ℋ) ∧ ((𝐹‘𝑗) ∈ ℋ ∧ (𝐹‘𝑘) ∈ ℋ)) → (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) = (((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) −ℎ ((𝐻‘𝑘) −ℎ (𝐹‘𝑘)))) |
61 | 28, 32, 38, 42, 60 | syl22anc 836 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) = (((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) −ℎ ((𝐻‘𝑘) −ℎ (𝐹‘𝑘)))) |
62 | | ocsh 29654 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ⊆ ℋ →
(⊥‘𝐴) ∈
Sℋ ) |
63 | 39, 62 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (⊥‘𝐴) ∈
Sℋ ) |
64 | | 2fveq3 6788 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 = 𝑗 → ((projℎ‘𝐴)‘(𝐻‘𝑛)) = ((projℎ‘𝐴)‘(𝐻‘𝑗))) |
65 | | fvex 6796 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((projℎ‘𝐴)‘(𝐻‘𝑗)) ∈ V |
66 | 64, 6, 65 | fvmpt 6884 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑗 ∈ ℕ → (𝐹‘𝑗) = ((projℎ‘𝐴)‘(𝐻‘𝑗))) |
67 | 66 | eqcomd 2745 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ∈ ℕ →
((projℎ‘𝐴)‘(𝐻‘𝑗)) = (𝐹‘𝑗)) |
68 | 67 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) →
((projℎ‘𝐴)‘(𝐻‘𝑗)) = (𝐹‘𝑗)) |
69 | 1 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐴 ∈ Cℋ
) |
70 | 9, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (⊥‘𝐴) ∈
Sℋ ) |
71 | | shless 29730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐵 ∈
Sℋ ∧ (⊥‘𝐴) ∈ Sℋ
∧ 𝐴 ∈
Sℋ ) ∧ 𝐵 ⊆ (⊥‘𝐴)) → (𝐵 +ℋ 𝐴) ⊆ ((⊥‘𝐴) +ℋ 𝐴)) |
72 | 20, 70, 18, 3, 71 | syl31anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝐵 +ℋ 𝐴) ⊆ ((⊥‘𝐴) +ℋ 𝐴)) |
73 | | shscom 29690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
→ (𝐴
+ℋ 𝐵) =
(𝐵 +ℋ
𝐴)) |
74 | 18, 20, 73 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝐴 +ℋ 𝐵) = (𝐵 +ℋ 𝐴)) |
75 | | shscom 29690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈
Sℋ ∧ (⊥‘𝐴) ∈ Sℋ )
→ (𝐴
+ℋ (⊥‘𝐴)) = ((⊥‘𝐴) +ℋ 𝐴)) |
76 | 18, 70, 75 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝐴 +ℋ (⊥‘𝐴)) = ((⊥‘𝐴) +ℋ 𝐴)) |
77 | 72, 74, 76 | 3sstr4d 3969 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝐴 +ℋ 𝐵) ⊆ (𝐴 +ℋ (⊥‘𝐴))) |
78 | 77 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐴 +ℋ 𝐵) ⊆ (𝐴 +ℋ (⊥‘𝐴))) |
79 | 78, 26 | sseldd 3923 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐻‘𝑗) ∈ (𝐴 +ℋ (⊥‘𝐴))) |
80 | | pjpreeq 29769 |
. . . . . . . . . . . . . . . . . . . . . . . 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 29581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((⊥‘𝐴)
∈ Sℋ → (⊥‘𝐴) ⊆
ℋ) |
87 | 70, 86 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (⊥‘𝐴) ⊆
ℋ) |
88 | 87 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (⊥‘𝐴) ⊆
ℋ) |
89 | 88 | sselda 3922 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ (⊥‘𝐴)) → 𝑥 ∈ ℋ) |
90 | | hvsubadd 29448 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐻‘𝑗) ∈ ℋ ∧ (𝐹‘𝑗) ∈ ℋ ∧ 𝑥 ∈ ℋ) → (((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) = 𝑥 ↔ ((𝐹‘𝑗) +ℎ 𝑥) = (𝐻‘𝑗))) |
91 | 84, 85, 89, 90 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ (⊥‘𝐴)) → (((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) = 𝑥 ↔ ((𝐹‘𝑗) +ℎ 𝑥) = (𝐻‘𝑗))) |
92 | | eqcom 2746 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = ((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) ↔ ((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) = 𝑥) |
93 | | eqcom 2746 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐻‘𝑗) = ((𝐹‘𝑗) +ℎ 𝑥) ↔ ((𝐹‘𝑗) +ℎ 𝑥) = (𝐻‘𝑗)) |
94 | 91, 92, 93 | 3bitr4g 314 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑥 ∈ (⊥‘𝐴)) → (𝑥 = ((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) ↔ (𝐻‘𝑗) = ((𝐹‘𝑗) +ℎ 𝑥))) |
95 | 94 | rexbidva 3226 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (∃𝑥 ∈ (⊥‘𝐴)𝑥 = ((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) ↔ ∃𝑥 ∈ (⊥‘𝐴)(𝐻‘𝑗) = ((𝐹‘𝑗) +ℎ 𝑥))) |
96 | 83, 95 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∃𝑥 ∈ (⊥‘𝐴)𝑥 = ((𝐻‘𝑗) −ℎ (𝐹‘𝑗))) |
97 | | risset 3195 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) ∈ (⊥‘𝐴) ↔ ∃𝑥 ∈ (⊥‘𝐴)𝑥 = ((𝐻‘𝑗) −ℎ (𝐹‘𝑗))) |
98 | 96, 97 | sylibr 233 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) ∈ (⊥‘𝐴)) |
99 | 98 | adantrr 714 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) ∈ (⊥‘𝐴)) |
100 | | eleq1w 2822 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = 𝑘 → (𝑗 ∈ ℕ ↔ 𝑘 ∈ ℕ)) |
101 | 100 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 𝑘 → ((𝜑 ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ 𝑘 ∈ ℕ))) |
102 | | fveq2 6783 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 = 𝑘 → (𝐻‘𝑗) = (𝐻‘𝑘)) |
103 | | fveq2 6783 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 = 𝑘 → (𝐹‘𝑗) = (𝐹‘𝑘)) |
104 | 102, 103 | oveq12d 7302 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = 𝑘 → ((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) = ((𝐻‘𝑘) −ℎ (𝐹‘𝑘))) |
105 | 104 | eleq1d 2824 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 𝑘 → (((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) ∈ (⊥‘𝐴) ↔ ((𝐻‘𝑘) −ℎ (𝐹‘𝑘)) ∈ (⊥‘𝐴))) |
106 | 101, 105 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = 𝑘 → (((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) ∈ (⊥‘𝐴)) ↔ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐻‘𝑘) −ℎ (𝐹‘𝑘)) ∈ (⊥‘𝐴)))) |
107 | 106, 98 | chvarvv 2003 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐻‘𝑘) −ℎ (𝐹‘𝑘)) ∈ (⊥‘𝐴)) |
108 | 107 | adantrl 713 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((𝐻‘𝑘) −ℎ (𝐹‘𝑘)) ∈ (⊥‘𝐴)) |
109 | | shsubcl 29591 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊥‘𝐴)
∈ Sℋ ∧ ((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) ∈ (⊥‘𝐴) ∧ ((𝐻‘𝑘) −ℎ (𝐹‘𝑘)) ∈ (⊥‘𝐴)) → (((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) −ℎ ((𝐻‘𝑘) −ℎ (𝐹‘𝑘))) ∈ (⊥‘𝐴)) |
110 | 63, 99, 108, 109 | syl3anc 1370 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((𝐻‘𝑗) −ℎ (𝐹‘𝑗)) −ℎ ((𝐻‘𝑘) −ℎ (𝐹‘𝑘))) ∈ (⊥‘𝐴)) |
111 | 61, 110 | eqeltrd 2840 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ (⊥‘𝐴)) |
112 | | shocorth 29663 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈
Sℋ → ((((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ 𝐴 ∧ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ (⊥‘𝐴)) → (((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ·ih
(((𝐻‘𝑗) −ℎ
(𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) = 0)) |
113 | 56, 112 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ 𝐴 ∧ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ (⊥‘𝐴)) → (((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ·ih
(((𝐻‘𝑗) −ℎ
(𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) = 0)) |
114 | 59, 111, 113 | mp2and 696 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ·ih
(((𝐻‘𝑗) −ℎ
(𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) = 0) |
115 | | normpyth 29516 |
. . . . . . . . . . . . . . . 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 29413 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ ℋ ∧ ((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) ∈ ℋ) → (((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) +ℎ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) = ((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) |
119 | 44, 34, 118 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) +ℎ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) = ((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) |
120 | 119 | fveq2d 6787 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
(normℎ‘(((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) +ℎ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))))) =
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘)))) |
121 | 120 | oveq1d 7299 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
((normℎ‘(((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) +ℎ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))))↑2) =
((normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘)))↑2)) |
122 | 117, 121 | eqtr3d 2781 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
(((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))↑2) +
((normℎ‘(((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) −ℎ ((𝐹‘𝑗) −ℎ (𝐹‘𝑘))))↑2)) =
((normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘)))↑2)) |
123 | 55, 122 | breqtrd 5101 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))↑2) ≤
((normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘)))↑2)) |
124 | | normcl 29496 |
. . . . . . . . . . . . . 14
⊢ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) ∈ ℋ →
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) ∈ ℝ) |
125 | 34, 124 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) ∈ ℝ) |
126 | | normge0 29497 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑗) −ℎ (𝐹‘𝑘)) ∈ ℋ → 0 ≤
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) |
127 | 44, 126 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 0 ≤
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))) |
128 | | normge0 29497 |
. . . . . . . . . . . . . 14
⊢ (((𝐻‘𝑗) −ℎ (𝐻‘𝑘)) ∈ ℋ → 0 ≤
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘)))) |
129 | 34, 128 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 0 ≤
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘)))) |
130 | 51, 125, 127, 129 | le2sqd 13983 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ≤
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) ↔
((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘)))↑2) ≤
((normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘)))↑2))) |
131 | 123, 130 | mpbird 256 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ≤
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘)))) |
132 | 131 | adantlr 712 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ≤
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘)))) |
133 | 51 | adantlr 712 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ ℝ) |
134 | 125 | adantlr 712 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) ∈ ℝ) |
135 | | rpre 12747 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
136 | 135 | ad2antlr 724 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → 𝑥 ∈
ℝ) |
137 | | lelttr 11074 |
. . . . . . . . . . 11
⊢
(((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ∈ ℝ ∧
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) ∈ ℝ ∧ 𝑥 ∈ ℝ) →
(((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ≤
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) ∧
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) < 𝑥) →
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) < 𝑥)) |
138 | 133, 134,
136, 137 | syl3anc 1370 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
(((normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) ≤
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) ∧
(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) < 𝑥) →
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) < 𝑥)) |
139 | 132, 138 | mpand 692 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) →
((normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) < 𝑥 →
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) < 𝑥)) |
140 | 139 | anassrs 468 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ℕ) →
((normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) < 𝑥 →
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) < 𝑥)) |
141 | 16, 140 | syldan 591 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) →
((normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) < 𝑥 →
(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) < 𝑥)) |
142 | 141 | ralimdva 3109 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) →
(∀𝑘 ∈
(ℤ≥‘𝑗)(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) < 𝑥 → ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) < 𝑥)) |
143 | 142 | reximdva 3204 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)(normℎ‘((𝐻‘𝑗) −ℎ (𝐻‘𝑘))) < 𝑥 → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) < 𝑥)) |
144 | 14, 143 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) < 𝑥) |
145 | 144 | ralrimiva 3104 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) < 𝑥) |
146 | | hcau 29555 |
. . 3
⊢ (𝐹 ∈ Cauchy ↔ (𝐹:ℕ⟶ ℋ ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(normℎ‘((𝐹‘𝑗) −ℎ (𝐹‘𝑘))) < 𝑥)) |
147 | 10, 145, 146 | sylanbrc 583 |
. 2
⊢ (𝜑 → 𝐹 ∈ Cauchy) |
148 | | ax-hcompl 29573 |
. 2
⊢ (𝐹 ∈ Cauchy →
∃𝑥 ∈ ℋ
𝐹
⇝𝑣 𝑥) |
149 | | hlimf 29608 |
. . . . 5
⊢
⇝𝑣 :dom ⇝𝑣 ⟶
ℋ |
150 | | ffn 6609 |
. . . . 5
⊢ (
⇝𝑣 :dom ⇝𝑣 ⟶ ℋ
→ ⇝𝑣 Fn dom ⇝𝑣
) |
151 | 149, 150 | ax-mp 5 |
. . . 4
⊢
⇝𝑣 Fn dom ⇝𝑣 |
152 | | fnbr 6550 |
. . . 4
⊢ ((
⇝𝑣 Fn dom ⇝𝑣 ∧ 𝐹 ⇝𝑣
𝑥) → 𝐹 ∈ dom ⇝𝑣
) |
153 | 151, 152 | mpan 687 |
. . 3
⊢ (𝐹 ⇝𝑣
𝑥 → 𝐹 ∈ dom ⇝𝑣
) |
154 | 153 | rexlimivw 3212 |
. 2
⊢
(∃𝑥 ∈
ℋ 𝐹
⇝𝑣 𝑥 → 𝐹 ∈ dom ⇝𝑣
) |
155 | 147, 148,
154 | 3syl 18 |
1
⊢ (𝜑 → 𝐹 ∈ dom ⇝𝑣
) |