Step | Hyp | Ref
| Expression |
1 | | nmcex.2 |
. . 3
⊢ (𝑆‘𝑇) = sup({𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}, ℝ*, <
) |
2 | | nmcex.3 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℋ → (𝑁‘(𝑇‘𝑥)) ∈ ℝ) |
3 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝑚 = (𝑁‘(𝑇‘𝑥)) → (𝑚 ∈ ℝ ↔ (𝑁‘(𝑇‘𝑥)) ∈ ℝ)) |
4 | 2, 3 | syl5ibrcom 236 |
. . . . . . . 8
⊢ (𝑥 ∈ ℋ → (𝑚 = (𝑁‘(𝑇‘𝑥)) → 𝑚 ∈ ℝ)) |
5 | 4 | imp 444 |
. . . . . . 7
⊢ ((𝑥 ∈ ℋ ∧ 𝑚 = (𝑁‘(𝑇‘𝑥))) → 𝑚 ∈ ℝ) |
6 | 5 | adantrl 748 |
. . . . . 6
⊢ ((𝑥 ∈ ℋ ∧
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))) → 𝑚 ∈ ℝ) |
7 | 6 | rexlimiva 3010 |
. . . . 5
⊢
(∃𝑥 ∈
ℋ ((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥))) → 𝑚 ∈ ℝ) |
8 | 7 | abssi 3640 |
. . . 4
⊢ {𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))} ⊆ ℝ |
9 | | ax-hv0cl 27244 |
. . . . . . 7
⊢
0ℎ ∈ ℋ |
10 | | norm0 27369 |
. . . . . . . . 9
⊢
(normℎ‘0ℎ) =
0 |
11 | | 0le1 10430 |
. . . . . . . . 9
⊢ 0 ≤
1 |
12 | 10, 11 | eqbrtri 4604 |
. . . . . . . 8
⊢
(normℎ‘0ℎ) ≤
1 |
13 | | nmcex.4 |
. . . . . . . . 9
⊢ (𝑁‘(𝑇‘0ℎ)) =
0 |
14 | 13 | eqcomi 2619 |
. . . . . . . 8
⊢ 0 =
(𝑁‘(𝑇‘0ℎ)) |
15 | 12, 14 | pm3.2i 470 |
. . . . . . 7
⊢
((normℎ‘0ℎ) ≤ 1 ∧ 0 =
(𝑁‘(𝑇‘0ℎ))) |
16 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = 0ℎ →
(normℎ‘𝑥) =
(normℎ‘0ℎ)) |
17 | 16 | breq1d 4593 |
. . . . . . . . 9
⊢ (𝑥 = 0ℎ →
((normℎ‘𝑥) ≤ 1 ↔
(normℎ‘0ℎ) ≤ 1)) |
18 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑥 = 0ℎ →
(𝑇‘𝑥) = (𝑇‘0ℎ)) |
19 | 18 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑥 = 0ℎ →
(𝑁‘(𝑇‘𝑥)) = (𝑁‘(𝑇‘0ℎ))) |
20 | 19 | eqeq2d 2620 |
. . . . . . . . 9
⊢ (𝑥 = 0ℎ →
(0 = (𝑁‘(𝑇‘𝑥)) ↔ 0 = (𝑁‘(𝑇‘0ℎ)))) |
21 | 17, 20 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑥 = 0ℎ →
(((normℎ‘𝑥) ≤ 1 ∧ 0 = (𝑁‘(𝑇‘𝑥))) ↔
((normℎ‘0ℎ) ≤ 1 ∧ 0 = (𝑁‘(𝑇‘0ℎ))))) |
22 | 21 | rspcev 3282 |
. . . . . . 7
⊢
((0ℎ ∈ ℋ ∧
((normℎ‘0ℎ) ≤ 1 ∧ 0 = (𝑁‘(𝑇‘0ℎ)))) →
∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 0 = (𝑁‘(𝑇‘𝑥)))) |
23 | 9, 15, 22 | mp2an 704 |
. . . . . 6
⊢
∃𝑥 ∈
ℋ ((normℎ‘𝑥) ≤ 1 ∧ 0 = (𝑁‘(𝑇‘𝑥))) |
24 | | c0ex 9913 |
. . . . . . 7
⊢ 0 ∈
V |
25 | | eqeq1 2614 |
. . . . . . . . 9
⊢ (𝑚 = 0 → (𝑚 = (𝑁‘(𝑇‘𝑥)) ↔ 0 = (𝑁‘(𝑇‘𝑥)))) |
26 | 25 | anbi2d 736 |
. . . . . . . 8
⊢ (𝑚 = 0 →
(((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥))) ↔
((normℎ‘𝑥) ≤ 1 ∧ 0 = (𝑁‘(𝑇‘𝑥))))) |
27 | 26 | rexbidv 3034 |
. . . . . . 7
⊢ (𝑚 = 0 → (∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥))) ↔ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 0 = (𝑁‘(𝑇‘𝑥))))) |
28 | 24, 27 | elab 3319 |
. . . . . 6
⊢ (0 ∈
{𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))} ↔ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 0 = (𝑁‘(𝑇‘𝑥)))) |
29 | 23, 28 | mpbir 220 |
. . . . 5
⊢ 0 ∈
{𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))} |
30 | 29 | ne0ii 3882 |
. . . 4
⊢ {𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))} ≠ ∅ |
31 | | nmcex.1 |
. . . . 5
⊢
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ ℋ
((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1) |
32 | | 2rp 11713 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ+ |
33 | | rpdivcl 11732 |
. . . . . . . . . 10
⊢ ((2
∈ ℝ+ ∧ 𝑦 ∈ ℝ+) → (2 /
𝑦) ∈
ℝ+) |
34 | 32, 33 | mpan 702 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ+
→ (2 / 𝑦) ∈
ℝ+) |
35 | 34 | rpred 11748 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ+
→ (2 / 𝑦) ∈
ℝ) |
36 | 35 | adantr 480 |
. . . . . . 7
⊢ ((𝑦 ∈ ℝ+
∧ ∀𝑧 ∈
ℋ ((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1)) → (2 / 𝑦) ∈ ℝ) |
37 | | rpre 11715 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℝ) |
38 | 37 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → 𝑦 ∈ ℝ) |
39 | 38 | rehalfcld 11156 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (𝑦 / 2) ∈ ℝ) |
40 | 39 | recnd 9947 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (𝑦 / 2) ∈ ℂ) |
41 | | simprl 790 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → 𝑥 ∈ ℋ) |
42 | | hvmulcl 27254 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦 / 2) ∈ ℂ ∧ 𝑥 ∈ ℋ) → ((𝑦 / 2)
·ℎ 𝑥) ∈ ℋ) |
43 | 40, 41, 42 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → ((𝑦 / 2) ·ℎ
𝑥) ∈
ℋ) |
44 | | normcl 27366 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 / 2)
·ℎ 𝑥) ∈ ℋ →
(normℎ‘((𝑦 / 2) ·ℎ
𝑥)) ∈
ℝ) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) →
(normℎ‘((𝑦 / 2) ·ℎ
𝑥)) ∈
ℝ) |
46 | | simprr 792 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) →
(normℎ‘𝑥) ≤ 1) |
47 | | normcl 27366 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℋ →
(normℎ‘𝑥) ∈ ℝ) |
48 | 47 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) →
(normℎ‘𝑥) ∈ ℝ) |
49 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → 1 ∈
ℝ) |
50 | | rphalfcl 11734 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℝ+
→ (𝑦 / 2) ∈
ℝ+) |
51 | 50 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (𝑦 / 2) ∈
ℝ+) |
52 | 48, 49, 51 | lemul2d 11792 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) →
((normℎ‘𝑥) ≤ 1 ↔ ((𝑦 / 2) ·
(normℎ‘𝑥)) ≤ ((𝑦 / 2) · 1))) |
53 | 46, 52 | mpbid 221 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → ((𝑦 / 2) ·
(normℎ‘𝑥)) ≤ ((𝑦 / 2) · 1)) |
54 | | rpcn 11717 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 / 2) ∈ ℝ+
→ (𝑦 / 2) ∈
ℂ) |
55 | | norm-iii 27381 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑦 / 2) ∈ ℂ ∧ 𝑥 ∈ ℋ) →
(normℎ‘((𝑦 / 2) ·ℎ
𝑥)) = ((abs‘(𝑦 / 2)) ·
(normℎ‘𝑥))) |
56 | 54, 55 | sylan 487 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 / 2) ∈ ℝ+
∧ 𝑥 ∈ ℋ)
→ (normℎ‘((𝑦 / 2) ·ℎ
𝑥)) = ((abs‘(𝑦 / 2)) ·
(normℎ‘𝑥))) |
57 | | rpre 11715 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 / 2) ∈ ℝ+
→ (𝑦 / 2) ∈
ℝ) |
58 | | rpge0 11721 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 / 2) ∈ ℝ+
→ 0 ≤ (𝑦 /
2)) |
59 | 57, 58 | absidd 14009 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 / 2) ∈ ℝ+
→ (abs‘(𝑦 / 2))
= (𝑦 / 2)) |
60 | 59 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 / 2) ∈ ℝ+
→ ((abs‘(𝑦 / 2))
· (normℎ‘𝑥)) = ((𝑦 / 2) ·
(normℎ‘𝑥))) |
61 | 60 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 / 2) ∈ ℝ+
∧ 𝑥 ∈ ℋ)
→ ((abs‘(𝑦 / 2))
· (normℎ‘𝑥)) = ((𝑦 / 2) ·
(normℎ‘𝑥))) |
62 | 56, 61 | eqtr2d 2645 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦 / 2) ∈ ℝ+
∧ 𝑥 ∈ ℋ)
→ ((𝑦 / 2) ·
(normℎ‘𝑥)) = (normℎ‘((𝑦 / 2)
·ℎ 𝑥))) |
63 | 51, 41, 62 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → ((𝑦 / 2) ·
(normℎ‘𝑥)) = (normℎ‘((𝑦 / 2)
·ℎ 𝑥))) |
64 | 40 | mulid1d 9936 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → ((𝑦 / 2) · 1) = (𝑦 / 2)) |
65 | 53, 63, 64 | 3brtr3d 4614 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) →
(normℎ‘((𝑦 / 2) ·ℎ
𝑥)) ≤ (𝑦 / 2)) |
66 | | rphalflt 11736 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℝ+
→ (𝑦 / 2) < 𝑦) |
67 | 66 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (𝑦 / 2) < 𝑦) |
68 | 45, 39, 38, 65, 67 | lelttrd 10074 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) →
(normℎ‘((𝑦 / 2) ·ℎ
𝑥)) < 𝑦) |
69 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = ((𝑦 / 2) ·ℎ
𝑥) →
(normℎ‘𝑧) = (normℎ‘((𝑦 / 2)
·ℎ 𝑥))) |
70 | 69 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = ((𝑦 / 2) ·ℎ
𝑥) →
((normℎ‘𝑧) < 𝑦 ↔
(normℎ‘((𝑦 / 2) ·ℎ
𝑥)) < 𝑦)) |
71 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = ((𝑦 / 2) ·ℎ
𝑥) → (𝑇‘𝑧) = (𝑇‘((𝑦 / 2) ·ℎ
𝑥))) |
72 | 71 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = ((𝑦 / 2) ·ℎ
𝑥) → (𝑁‘(𝑇‘𝑧)) = (𝑁‘(𝑇‘((𝑦 / 2) ·ℎ
𝑥)))) |
73 | 72 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = ((𝑦 / 2) ·ℎ
𝑥) → ((𝑁‘(𝑇‘𝑧)) < 1 ↔ (𝑁‘(𝑇‘((𝑦 / 2) ·ℎ
𝑥))) <
1)) |
74 | 70, 73 | imbi12d 333 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = ((𝑦 / 2) ·ℎ
𝑥) →
(((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1) ↔
((normℎ‘((𝑦 / 2) ·ℎ
𝑥)) < 𝑦 → (𝑁‘(𝑇‘((𝑦 / 2) ·ℎ
𝑥))) <
1))) |
75 | 74 | rspcv 3278 |
. . . . . . . . . . . . . . . . 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 43 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (∀𝑧 ∈ ℋ
((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1) → (𝑁‘(𝑇‘((𝑦 / 2) ·ℎ
𝑥))) <
1)) |
78 | 2 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (𝑁‘(𝑇‘𝑥)) ∈ ℝ) |
79 | 78, 49, 51 | ltmuldiv2d 11796 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (((𝑦 / 2) · (𝑁‘(𝑇‘𝑥))) < 1 ↔ (𝑁‘(𝑇‘𝑥)) < (1 / (𝑦 / 2)))) |
80 | 51 | rprecred 11759 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (1 / (𝑦 / 2)) ∈ ℝ) |
81 | | ltle 10005 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁‘(𝑇‘𝑥)) ∈ ℝ ∧ (1 / (𝑦 / 2)) ∈ ℝ) →
((𝑁‘(𝑇‘𝑥)) < (1 / (𝑦 / 2)) → (𝑁‘(𝑇‘𝑥)) ≤ (1 / (𝑦 / 2)))) |
82 | 78, 80, 81 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → ((𝑁‘(𝑇‘𝑥)) < (1 / (𝑦 / 2)) → (𝑁‘(𝑇‘𝑥)) ≤ (1 / (𝑦 / 2)))) |
83 | 79, 82 | sylbid 229 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (((𝑦 / 2) · (𝑁‘(𝑇‘𝑥))) < 1 → (𝑁‘(𝑇‘𝑥)) ≤ (1 / (𝑦 / 2)))) |
84 | | nmcex.5 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 / 2) ∈ ℝ+
∧ 𝑥 ∈ ℋ)
→ ((𝑦 / 2) ·
(𝑁‘(𝑇‘𝑥))) = (𝑁‘(𝑇‘((𝑦 / 2) ·ℎ
𝑥)))) |
85 | 51, 41, 84 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → ((𝑦 / 2) · (𝑁‘(𝑇‘𝑥))) = (𝑁‘(𝑇‘((𝑦 / 2) ·ℎ
𝑥)))) |
86 | 85 | breq1d 4593 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (((𝑦 / 2) · (𝑁‘(𝑇‘𝑥))) < 1 ↔ (𝑁‘(𝑇‘((𝑦 / 2) ·ℎ
𝑥))) <
1)) |
87 | | rpcn 11717 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℂ) |
88 | | rpne0 11724 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ≠
0) |
89 | | 2cn 10968 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℂ |
90 | | 2ne0 10990 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ≠
0 |
91 | | recdiv 10610 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) ∧ (2 ∈ ℂ
∧ 2 ≠ 0)) → (1 / (𝑦 / 2)) = (2 / 𝑦)) |
92 | 89, 90, 91 | mpanr12 717 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) → (1 / (𝑦 / 2)) = (2 / 𝑦)) |
93 | 87, 88, 92 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℝ+
→ (1 / (𝑦 / 2)) = (2 /
𝑦)) |
94 | 93 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (1 / (𝑦 / 2)) = (2 / 𝑦)) |
95 | 94 | breq2d 4595 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → ((𝑁‘(𝑇‘𝑥)) ≤ (1 / (𝑦 / 2)) ↔ (𝑁‘(𝑇‘𝑥)) ≤ (2 / 𝑦))) |
96 | 83, 86, 95 | 3imtr3d 281 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → ((𝑁‘(𝑇‘((𝑦 / 2) ·ℎ
𝑥))) < 1 → (𝑁‘(𝑇‘𝑥)) ≤ (2 / 𝑦))) |
97 | 77, 96 | syld 46 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (∀𝑧 ∈ ℋ
((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1) → (𝑁‘(𝑇‘𝑥)) ≤ (2 / 𝑦))) |
98 | 97 | imp 444 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) ∧ ∀𝑧 ∈ ℋ
((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1)) → (𝑁‘(𝑇‘𝑥)) ≤ (2 / 𝑦)) |
99 | 98 | an32s 842 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ ℝ+
∧ ∀𝑧 ∈
ℋ ((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1)) ∧ (𝑥 ∈ ℋ ∧
(normℎ‘𝑥) ≤ 1)) → (𝑁‘(𝑇‘𝑥)) ≤ (2 / 𝑦)) |
100 | 99 | anassrs 678 |
. . . . . . . . . . 11
⊢ ((((𝑦 ∈ ℝ+
∧ ∀𝑧 ∈
ℋ ((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1)) ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) → (𝑁‘(𝑇‘𝑥)) ≤ (2 / 𝑦)) |
101 | | breq1 4586 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑁‘(𝑇‘𝑥)) → (𝑛 ≤ (2 / 𝑦) ↔ (𝑁‘(𝑇‘𝑥)) ≤ (2 / 𝑦))) |
102 | 100, 101 | syl5ibrcom 236 |
. . . . . . . . . 10
⊢ ((((𝑦 ∈ ℝ+
∧ ∀𝑧 ∈
ℋ ((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1)) ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) → (𝑛 = (𝑁‘(𝑇‘𝑥)) → 𝑛 ≤ (2 / 𝑦))) |
103 | 102 | expimpd 627 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ℝ+
∧ ∀𝑧 ∈
ℋ ((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1)) ∧ 𝑥 ∈ ℋ) →
(((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))) → 𝑛 ≤ (2 / 𝑦))) |
104 | 103 | rexlimdva 3013 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℝ+
∧ ∀𝑧 ∈
ℋ ((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1)) → (∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))) → 𝑛 ≤ (2 / 𝑦))) |
105 | 104 | alrimiv 1842 |
. . . . . . 7
⊢ ((𝑦 ∈ ℝ+
∧ ∀𝑧 ∈
ℋ ((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1)) → ∀𝑛(∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))) → 𝑛 ≤ (2 / 𝑦))) |
106 | | eqeq1 2614 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (𝑚 = (𝑁‘(𝑇‘𝑥)) ↔ 𝑛 = (𝑁‘(𝑇‘𝑥)))) |
107 | 106 | anbi2d 736 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 →
(((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥))) ↔
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))))) |
108 | 107 | rexbidv 3034 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥))) ↔ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))))) |
109 | 108 | ralab 3334 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
{𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}𝑛 ≤ 𝑧 ↔ ∀𝑛(∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))) → 𝑛 ≤ 𝑧)) |
110 | | breq2 4587 |
. . . . . . . . . . 11
⊢ (𝑧 = (2 / 𝑦) → (𝑛 ≤ 𝑧 ↔ 𝑛 ≤ (2 / 𝑦))) |
111 | 110 | imbi2d 329 |
. . . . . . . . . 10
⊢ (𝑧 = (2 / 𝑦) → ((∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))) → 𝑛 ≤ 𝑧) ↔ (∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))) → 𝑛 ≤ (2 / 𝑦)))) |
112 | 111 | albidv 1836 |
. . . . . . . . 9
⊢ (𝑧 = (2 / 𝑦) → (∀𝑛(∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))) → 𝑛 ≤ 𝑧) ↔ ∀𝑛(∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))) → 𝑛 ≤ (2 / 𝑦)))) |
113 | 109, 112 | syl5bb 271 |
. . . . . . . 8
⊢ (𝑧 = (2 / 𝑦) → (∀𝑛 ∈ {𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}𝑛 ≤ 𝑧 ↔ ∀𝑛(∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))) → 𝑛 ≤ (2 / 𝑦)))) |
114 | 113 | rspcev 3282 |
. . . . . . 7
⊢ (((2 /
𝑦) ∈ ℝ ∧
∀𝑛(∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))) → 𝑛 ≤ (2 / 𝑦))) → ∃𝑧 ∈ ℝ ∀𝑛 ∈ {𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}𝑛 ≤ 𝑧) |
115 | 36, 105, 114 | syl2anc 691 |
. . . . . 6
⊢ ((𝑦 ∈ ℝ+
∧ ∀𝑧 ∈
ℋ ((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1)) → ∃𝑧 ∈ ℝ ∀𝑛 ∈ {𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}𝑛 ≤ 𝑧) |
116 | 115 | rexlimiva 3010 |
. . . . 5
⊢
(∃𝑦 ∈
ℝ+ ∀𝑧 ∈ ℋ
((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1) → ∃𝑧 ∈ ℝ ∀𝑛 ∈ {𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}𝑛 ≤ 𝑧) |
117 | 31, 116 | ax-mp 5 |
. . . 4
⊢
∃𝑧 ∈
ℝ ∀𝑛 ∈
{𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}𝑛 ≤ 𝑧 |
118 | | supxrre 12029 |
. . . 4
⊢ (({𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))} ⊆ ℝ ∧ {𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))} ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑛 ∈ {𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}𝑛 ≤ 𝑧) → sup({𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}, ℝ*, < ) =
sup({𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}, ℝ, < )) |
119 | 8, 30, 117, 118 | mp3an 1416 |
. . 3
⊢
sup({𝑚 ∣
∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}, ℝ*, < ) =
sup({𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}, ℝ, < ) |
120 | 1, 119 | eqtri 2632 |
. 2
⊢ (𝑆‘𝑇) = sup({𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}, ℝ, < ) |
121 | | suprcl 10862 |
. . 3
⊢ (({𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))} ⊆ ℝ ∧ {𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))} ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑛 ∈ {𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}𝑛 ≤ 𝑧) → sup({𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}, ℝ, < ) ∈
ℝ) |
122 | 8, 30, 117, 121 | mp3an 1416 |
. 2
⊢
sup({𝑚 ∣
∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}, ℝ, < ) ∈
ℝ |
123 | 120, 122 | eqeltri 2684 |
1
⊢ (𝑆‘𝑇) ∈ ℝ |