Step | Hyp | Ref
| Expression |
1 | | nmcex.2 |
. . 3
⊢ (𝑆‘𝑇) = sup({𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}, ℝ*, <
) |
2 | | nmcex.3 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℋ → (𝑁‘(𝑇‘𝑥)) ∈ ℝ) |
3 | | eleq1 2689 |
. . . . . . . . 9
⊢ (𝑚 = (𝑁‘(𝑇‘𝑥)) → (𝑚 ∈ ℝ ↔ (𝑁‘(𝑇‘𝑥)) ∈ ℝ)) |
4 | 2, 3 | syl5ibrcom 237 |
. . . . . . . 8
⊢ (𝑥 ∈ ℋ → (𝑚 = (𝑁‘(𝑇‘𝑥)) → 𝑚 ∈ ℝ)) |
5 | 4 | imp 445 |
. . . . . . 7
⊢ ((𝑥 ∈ ℋ ∧ 𝑚 = (𝑁‘(𝑇‘𝑥))) → 𝑚 ∈ ℝ) |
6 | 5 | adantrl 752 |
. . . . . 6
⊢ ((𝑥 ∈ ℋ ∧
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))) → 𝑚 ∈ ℝ) |
7 | 6 | rexlimiva 3028 |
. . . . 5
⊢
(∃𝑥 ∈
ℋ ((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥))) → 𝑚 ∈ ℝ) |
8 | 7 | abssi 3677 |
. . . 4
⊢ {𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))} ⊆ ℝ |
9 | | ax-hv0cl 27860 |
. . . . . . 7
⊢
0ℎ ∈ ℋ |
10 | | norm0 27985 |
. . . . . . . . 9
⊢
(normℎ‘0ℎ) =
0 |
11 | | 0le1 10551 |
. . . . . . . . 9
⊢ 0 ≤
1 |
12 | 10, 11 | eqbrtri 4674 |
. . . . . . . 8
⊢
(normℎ‘0ℎ) ≤
1 |
13 | | nmcex.4 |
. . . . . . . . 9
⊢ (𝑁‘(𝑇‘0ℎ)) =
0 |
14 | 13 | eqcomi 2631 |
. . . . . . . 8
⊢ 0 =
(𝑁‘(𝑇‘0ℎ)) |
15 | 12, 14 | pm3.2i 471 |
. . . . . . 7
⊢
((normℎ‘0ℎ) ≤ 1 ∧ 0 =
(𝑁‘(𝑇‘0ℎ))) |
16 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑥 = 0ℎ →
(normℎ‘𝑥) =
(normℎ‘0ℎ)) |
17 | 16 | breq1d 4663 |
. . . . . . . . 9
⊢ (𝑥 = 0ℎ →
((normℎ‘𝑥) ≤ 1 ↔
(normℎ‘0ℎ) ≤ 1)) |
18 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑥 = 0ℎ →
(𝑇‘𝑥) = (𝑇‘0ℎ)) |
19 | 18 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑥 = 0ℎ →
(𝑁‘(𝑇‘𝑥)) = (𝑁‘(𝑇‘0ℎ))) |
20 | 19 | eqeq2d 2632 |
. . . . . . . . 9
⊢ (𝑥 = 0ℎ →
(0 = (𝑁‘(𝑇‘𝑥)) ↔ 0 = (𝑁‘(𝑇‘0ℎ)))) |
21 | 17, 20 | anbi12d 747 |
. . . . . . . 8
⊢ (𝑥 = 0ℎ →
(((normℎ‘𝑥) ≤ 1 ∧ 0 = (𝑁‘(𝑇‘𝑥))) ↔
((normℎ‘0ℎ) ≤ 1 ∧ 0 = (𝑁‘(𝑇‘0ℎ))))) |
22 | 21 | rspcev 3309 |
. . . . . . 7
⊢
((0ℎ ∈ ℋ ∧
((normℎ‘0ℎ) ≤ 1 ∧ 0 = (𝑁‘(𝑇‘0ℎ)))) →
∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 0 = (𝑁‘(𝑇‘𝑥)))) |
23 | 9, 15, 22 | mp2an 708 |
. . . . . 6
⊢
∃𝑥 ∈
ℋ ((normℎ‘𝑥) ≤ 1 ∧ 0 = (𝑁‘(𝑇‘𝑥))) |
24 | | c0ex 10034 |
. . . . . . 7
⊢ 0 ∈
V |
25 | | eqeq1 2626 |
. . . . . . . . 9
⊢ (𝑚 = 0 → (𝑚 = (𝑁‘(𝑇‘𝑥)) ↔ 0 = (𝑁‘(𝑇‘𝑥)))) |
26 | 25 | anbi2d 740 |
. . . . . . . 8
⊢ (𝑚 = 0 →
(((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥))) ↔
((normℎ‘𝑥) ≤ 1 ∧ 0 = (𝑁‘(𝑇‘𝑥))))) |
27 | 26 | rexbidv 3052 |
. . . . . . 7
⊢ (𝑚 = 0 → (∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥))) ↔ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 0 = (𝑁‘(𝑇‘𝑥))))) |
28 | 24, 27 | elab 3350 |
. . . . . 6
⊢ (0 ∈
{𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))} ↔ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 0 = (𝑁‘(𝑇‘𝑥)))) |
29 | 23, 28 | mpbir 221 |
. . . . 5
⊢ 0 ∈
{𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))} |
30 | 29 | ne0ii 3923 |
. . . 4
⊢ {𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))} ≠ ∅ |
31 | | nmcex.1 |
. . . . 5
⊢
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ ℋ
((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1) |
32 | | 2rp 11837 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ+ |
33 | | rpdivcl 11856 |
. . . . . . . . . 10
⊢ ((2
∈ ℝ+ ∧ 𝑦 ∈ ℝ+) → (2 /
𝑦) ∈
ℝ+) |
34 | 32, 33 | mpan 706 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ+
→ (2 / 𝑦) ∈
ℝ+) |
35 | 34 | rpred 11872 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ+
→ (2 / 𝑦) ∈
ℝ) |
36 | 35 | adantr 481 |
. . . . . . 7
⊢ ((𝑦 ∈ ℝ+
∧ ∀𝑧 ∈
ℋ ((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1)) → (2 / 𝑦) ∈ ℝ) |
37 | | rpre 11839 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℝ) |
38 | 37 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → 𝑦 ∈ ℝ) |
39 | 38 | rehalfcld 11279 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (𝑦 / 2) ∈ ℝ) |
40 | 39 | recnd 10068 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (𝑦 / 2) ∈ ℂ) |
41 | | simprl 794 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → 𝑥 ∈ ℋ) |
42 | | hvmulcl 27870 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦 / 2) ∈ ℂ ∧ 𝑥 ∈ ℋ) → ((𝑦 / 2)
·ℎ 𝑥) ∈ ℋ) |
43 | 40, 41, 42 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → ((𝑦 / 2) ·ℎ
𝑥) ∈
ℋ) |
44 | | normcl 27982 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 / 2)
·ℎ 𝑥) ∈ ℋ →
(normℎ‘((𝑦 / 2) ·ℎ
𝑥)) ∈
ℝ) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) →
(normℎ‘((𝑦 / 2) ·ℎ
𝑥)) ∈
ℝ) |
46 | | simprr 796 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) →
(normℎ‘𝑥) ≤ 1) |
47 | | normcl 27982 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℋ →
(normℎ‘𝑥) ∈ ℝ) |
48 | 47 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) →
(normℎ‘𝑥) ∈ ℝ) |
49 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → 1 ∈
ℝ) |
50 | | rphalfcl 11858 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℝ+
→ (𝑦 / 2) ∈
ℝ+) |
51 | 50 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (𝑦 / 2) ∈
ℝ+) |
52 | 48, 49, 51 | lemul2d 11916 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) →
((normℎ‘𝑥) ≤ 1 ↔ ((𝑦 / 2) ·
(normℎ‘𝑥)) ≤ ((𝑦 / 2) · 1))) |
53 | 46, 52 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → ((𝑦 / 2) ·
(normℎ‘𝑥)) ≤ ((𝑦 / 2) · 1)) |
54 | | rpcn 11841 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 / 2) ∈ ℝ+
→ (𝑦 / 2) ∈
ℂ) |
55 | | norm-iii 27997 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑦 / 2) ∈ ℂ ∧ 𝑥 ∈ ℋ) →
(normℎ‘((𝑦 / 2) ·ℎ
𝑥)) = ((abs‘(𝑦 / 2)) ·
(normℎ‘𝑥))) |
56 | 54, 55 | sylan 488 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 / 2) ∈ ℝ+
∧ 𝑥 ∈ ℋ)
→ (normℎ‘((𝑦 / 2) ·ℎ
𝑥)) = ((abs‘(𝑦 / 2)) ·
(normℎ‘𝑥))) |
57 | | rpre 11839 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 / 2) ∈ ℝ+
→ (𝑦 / 2) ∈
ℝ) |
58 | | rpge0 11845 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 / 2) ∈ ℝ+
→ 0 ≤ (𝑦 /
2)) |
59 | 57, 58 | absidd 14161 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 / 2) ∈ ℝ+
→ (abs‘(𝑦 / 2))
= (𝑦 / 2)) |
60 | 59 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 / 2) ∈ ℝ+
→ ((abs‘(𝑦 / 2))
· (normℎ‘𝑥)) = ((𝑦 / 2) ·
(normℎ‘𝑥))) |
61 | 60 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 / 2) ∈ ℝ+
∧ 𝑥 ∈ ℋ)
→ ((abs‘(𝑦 / 2))
· (normℎ‘𝑥)) = ((𝑦 / 2) ·
(normℎ‘𝑥))) |
62 | 56, 61 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦 / 2) ∈ ℝ+
∧ 𝑥 ∈ ℋ)
→ ((𝑦 / 2) ·
(normℎ‘𝑥)) = (normℎ‘((𝑦 / 2)
·ℎ 𝑥))) |
63 | 51, 41, 62 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → ((𝑦 / 2) ·
(normℎ‘𝑥)) = (normℎ‘((𝑦 / 2)
·ℎ 𝑥))) |
64 | 40 | mulid1d 10057 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → ((𝑦 / 2) · 1) = (𝑦 / 2)) |
65 | 53, 63, 64 | 3brtr3d 4684 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) →
(normℎ‘((𝑦 / 2) ·ℎ
𝑥)) ≤ (𝑦 / 2)) |
66 | | rphalflt 11860 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℝ+
→ (𝑦 / 2) < 𝑦) |
67 | 66 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (𝑦 / 2) < 𝑦) |
68 | 45, 39, 38, 65, 67 | lelttrd 10195 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) →
(normℎ‘((𝑦 / 2) ·ℎ
𝑥)) < 𝑦) |
69 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = ((𝑦 / 2) ·ℎ
𝑥) →
(normℎ‘𝑧) = (normℎ‘((𝑦 / 2)
·ℎ 𝑥))) |
70 | 69 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = ((𝑦 / 2) ·ℎ
𝑥) →
((normℎ‘𝑧) < 𝑦 ↔
(normℎ‘((𝑦 / 2) ·ℎ
𝑥)) < 𝑦)) |
71 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = ((𝑦 / 2) ·ℎ
𝑥) → (𝑇‘𝑧) = (𝑇‘((𝑦 / 2) ·ℎ
𝑥))) |
72 | 71 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = ((𝑦 / 2) ·ℎ
𝑥) → (𝑁‘(𝑇‘𝑧)) = (𝑁‘(𝑇‘((𝑦 / 2) ·ℎ
𝑥)))) |
73 | 72 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = ((𝑦 / 2) ·ℎ
𝑥) → ((𝑁‘(𝑇‘𝑧)) < 1 ↔ (𝑁‘(𝑇‘((𝑦 / 2) ·ℎ
𝑥))) <
1)) |
74 | 70, 73 | imbi12d 334 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = ((𝑦 / 2) ·ℎ
𝑥) →
(((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1) ↔
((normℎ‘((𝑦 / 2) ·ℎ
𝑥)) < 𝑦 → (𝑁‘(𝑇‘((𝑦 / 2) ·ℎ
𝑥))) <
1))) |
75 | 74 | rspcv 3305 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 / 2)
·ℎ 𝑥) ∈ ℋ → (∀𝑧 ∈ ℋ
((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1) →
((normℎ‘((𝑦 / 2) ·ℎ
𝑥)) < 𝑦 → (𝑁‘(𝑇‘((𝑦 / 2) ·ℎ
𝑥))) <
1))) |
76 | 43, 75 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (∀𝑧 ∈ ℋ
((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1) →
((normℎ‘((𝑦 / 2) ·ℎ
𝑥)) < 𝑦 → (𝑁‘(𝑇‘((𝑦 / 2) ·ℎ
𝑥))) <
1))) |
77 | 68, 76 | mpid 44 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (∀𝑧 ∈ ℋ
((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1) → (𝑁‘(𝑇‘((𝑦 / 2) ·ℎ
𝑥))) <
1)) |
78 | 2 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (𝑁‘(𝑇‘𝑥)) ∈ ℝ) |
79 | 78, 49, 51 | ltmuldiv2d 11920 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (((𝑦 / 2) · (𝑁‘(𝑇‘𝑥))) < 1 ↔ (𝑁‘(𝑇‘𝑥)) < (1 / (𝑦 / 2)))) |
80 | 51 | rprecred 11883 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (1 / (𝑦 / 2)) ∈ ℝ) |
81 | | ltle 10126 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁‘(𝑇‘𝑥)) ∈ ℝ ∧ (1 / (𝑦 / 2)) ∈ ℝ) →
((𝑁‘(𝑇‘𝑥)) < (1 / (𝑦 / 2)) → (𝑁‘(𝑇‘𝑥)) ≤ (1 / (𝑦 / 2)))) |
82 | 78, 80, 81 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → ((𝑁‘(𝑇‘𝑥)) < (1 / (𝑦 / 2)) → (𝑁‘(𝑇‘𝑥)) ≤ (1 / (𝑦 / 2)))) |
83 | 79, 82 | sylbid 230 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (((𝑦 / 2) · (𝑁‘(𝑇‘𝑥))) < 1 → (𝑁‘(𝑇‘𝑥)) ≤ (1 / (𝑦 / 2)))) |
84 | | nmcex.5 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 / 2) ∈ ℝ+
∧ 𝑥 ∈ ℋ)
→ ((𝑦 / 2) ·
(𝑁‘(𝑇‘𝑥))) = (𝑁‘(𝑇‘((𝑦 / 2) ·ℎ
𝑥)))) |
85 | 51, 41, 84 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → ((𝑦 / 2) · (𝑁‘(𝑇‘𝑥))) = (𝑁‘(𝑇‘((𝑦 / 2) ·ℎ
𝑥)))) |
86 | 85 | breq1d 4663 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (((𝑦 / 2) · (𝑁‘(𝑇‘𝑥))) < 1 ↔ (𝑁‘(𝑇‘((𝑦 / 2) ·ℎ
𝑥))) <
1)) |
87 | | rpcn 11841 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℂ) |
88 | | rpne0 11848 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ≠
0) |
89 | | 2cn 11091 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℂ |
90 | | 2ne0 11113 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ≠
0 |
91 | | recdiv 10731 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) ∧ (2 ∈ ℂ
∧ 2 ≠ 0)) → (1 / (𝑦 / 2)) = (2 / 𝑦)) |
92 | 89, 90, 91 | mpanr12 721 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) → (1 / (𝑦 / 2)) = (2 / 𝑦)) |
93 | 87, 88, 92 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℝ+
→ (1 / (𝑦 / 2)) = (2 /
𝑦)) |
94 | 93 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (1 / (𝑦 / 2)) = (2 / 𝑦)) |
95 | 94 | breq2d 4665 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → ((𝑁‘(𝑇‘𝑥)) ≤ (1 / (𝑦 / 2)) ↔ (𝑁‘(𝑇‘𝑥)) ≤ (2 / 𝑦))) |
96 | 83, 86, 95 | 3imtr3d 282 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → ((𝑁‘(𝑇‘((𝑦 / 2) ·ℎ
𝑥))) < 1 → (𝑁‘(𝑇‘𝑥)) ≤ (2 / 𝑦))) |
97 | 77, 96 | syld 47 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (∀𝑧 ∈ ℋ
((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1) → (𝑁‘(𝑇‘𝑥)) ≤ (2 / 𝑦))) |
98 | 97 | imp 445 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) ∧ ∀𝑧 ∈ ℋ
((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1)) → (𝑁‘(𝑇‘𝑥)) ≤ (2 / 𝑦)) |
99 | 98 | an32s 846 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ ℝ+
∧ ∀𝑧 ∈
ℋ ((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1)) ∧ (𝑥 ∈ ℋ ∧
(normℎ‘𝑥) ≤ 1)) → (𝑁‘(𝑇‘𝑥)) ≤ (2 / 𝑦)) |
100 | 99 | anassrs 680 |
. . . . . . . . . . 11
⊢ ((((𝑦 ∈ ℝ+
∧ ∀𝑧 ∈
ℋ ((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1)) ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) → (𝑁‘(𝑇‘𝑥)) ≤ (2 / 𝑦)) |
101 | | breq1 4656 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑁‘(𝑇‘𝑥)) → (𝑛 ≤ (2 / 𝑦) ↔ (𝑁‘(𝑇‘𝑥)) ≤ (2 / 𝑦))) |
102 | 100, 101 | syl5ibrcom 237 |
. . . . . . . . . 10
⊢ ((((𝑦 ∈ ℝ+
∧ ∀𝑧 ∈
ℋ ((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1)) ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) → (𝑛 = (𝑁‘(𝑇‘𝑥)) → 𝑛 ≤ (2 / 𝑦))) |
103 | 102 | expimpd 629 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ℝ+
∧ ∀𝑧 ∈
ℋ ((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1)) ∧ 𝑥 ∈ ℋ) →
(((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))) → 𝑛 ≤ (2 / 𝑦))) |
104 | 103 | rexlimdva 3031 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℝ+
∧ ∀𝑧 ∈
ℋ ((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1)) → (∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))) → 𝑛 ≤ (2 / 𝑦))) |
105 | 104 | alrimiv 1855 |
. . . . . . 7
⊢ ((𝑦 ∈ ℝ+
∧ ∀𝑧 ∈
ℋ ((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1)) → ∀𝑛(∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))) → 𝑛 ≤ (2 / 𝑦))) |
106 | | eqeq1 2626 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (𝑚 = (𝑁‘(𝑇‘𝑥)) ↔ 𝑛 = (𝑁‘(𝑇‘𝑥)))) |
107 | 106 | anbi2d 740 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 →
(((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥))) ↔
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))))) |
108 | 107 | rexbidv 3052 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥))) ↔ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))))) |
109 | 108 | ralab 3367 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
{𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}𝑛 ≤ 𝑧 ↔ ∀𝑛(∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))) → 𝑛 ≤ 𝑧)) |
110 | | breq2 4657 |
. . . . . . . . . . 11
⊢ (𝑧 = (2 / 𝑦) → (𝑛 ≤ 𝑧 ↔ 𝑛 ≤ (2 / 𝑦))) |
111 | 110 | imbi2d 330 |
. . . . . . . . . 10
⊢ (𝑧 = (2 / 𝑦) → ((∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))) → 𝑛 ≤ 𝑧) ↔ (∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))) → 𝑛 ≤ (2 / 𝑦)))) |
112 | 111 | albidv 1849 |
. . . . . . . . 9
⊢ (𝑧 = (2 / 𝑦) → (∀𝑛(∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))) → 𝑛 ≤ 𝑧) ↔ ∀𝑛(∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))) → 𝑛 ≤ (2 / 𝑦)))) |
113 | 109, 112 | syl5bb 272 |
. . . . . . . 8
⊢ (𝑧 = (2 / 𝑦) → (∀𝑛 ∈ {𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}𝑛 ≤ 𝑧 ↔ ∀𝑛(∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))) → 𝑛 ≤ (2 / 𝑦)))) |
114 | 113 | rspcev 3309 |
. . . . . . 7
⊢ (((2 /
𝑦) ∈ ℝ ∧
∀𝑛(∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))) → 𝑛 ≤ (2 / 𝑦))) → ∃𝑧 ∈ ℝ ∀𝑛 ∈ {𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}𝑛 ≤ 𝑧) |
115 | 36, 105, 114 | syl2anc 693 |
. . . . . 6
⊢ ((𝑦 ∈ ℝ+
∧ ∀𝑧 ∈
ℋ ((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1)) → ∃𝑧 ∈ ℝ ∀𝑛 ∈ {𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}𝑛 ≤ 𝑧) |
116 | 115 | rexlimiva 3028 |
. . . . 5
⊢
(∃𝑦 ∈
ℝ+ ∀𝑧 ∈ ℋ
((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1) → ∃𝑧 ∈ ℝ ∀𝑛 ∈ {𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}𝑛 ≤ 𝑧) |
117 | 31, 116 | ax-mp 5 |
. . . 4
⊢
∃𝑧 ∈
ℝ ∀𝑛 ∈
{𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}𝑛 ≤ 𝑧 |
118 | | supxrre 12157 |
. . . 4
⊢ (({𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))} ⊆ ℝ ∧ {𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))} ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑛 ∈ {𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}𝑛 ≤ 𝑧) → sup({𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}, ℝ*, < ) =
sup({𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}, ℝ, < )) |
119 | 8, 30, 117, 118 | mp3an 1424 |
. . 3
⊢
sup({𝑚 ∣
∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}, ℝ*, < ) =
sup({𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}, ℝ, < ) |
120 | 1, 119 | eqtri 2644 |
. 2
⊢ (𝑆‘𝑇) = sup({𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}, ℝ, < ) |
121 | | suprcl 10983 |
. . 3
⊢ (({𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))} ⊆ ℝ ∧ {𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))} ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑛 ∈ {𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}𝑛 ≤ 𝑧) → sup({𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}, ℝ, < ) ∈
ℝ) |
122 | 8, 30, 117, 121 | mp3an 1424 |
. 2
⊢
sup({𝑚 ∣
∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}, ℝ, < ) ∈
ℝ |
123 | 120, 122 | eqeltri 2697 |
1
⊢ (𝑆‘𝑇) ∈ ℝ |