| Step | Hyp | Ref
| Expression |
| 1 | | nmcex.2 |
. . 3
⊢ (𝑆‘𝑇) = sup({𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}, ℝ*, <
) |
| 2 | | nmcex.3 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℋ → (𝑁‘(𝑇‘𝑥)) ∈ ℝ) |
| 3 | | eleq1 2829 |
. . . . . . . . 9
⊢ (𝑚 = (𝑁‘(𝑇‘𝑥)) → (𝑚 ∈ ℝ ↔ (𝑁‘(𝑇‘𝑥)) ∈ ℝ)) |
| 4 | 2, 3 | syl5ibrcom 247 |
. . . . . . . 8
⊢ (𝑥 ∈ ℋ → (𝑚 = (𝑁‘(𝑇‘𝑥)) → 𝑚 ∈ ℝ)) |
| 5 | 4 | imp 406 |
. . . . . . 7
⊢ ((𝑥 ∈ ℋ ∧ 𝑚 = (𝑁‘(𝑇‘𝑥))) → 𝑚 ∈ ℝ) |
| 6 | 5 | adantrl 716 |
. . . . . 6
⊢ ((𝑥 ∈ ℋ ∧
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))) → 𝑚 ∈ ℝ) |
| 7 | 6 | rexlimiva 3147 |
. . . . 5
⊢
(∃𝑥 ∈
ℋ ((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥))) → 𝑚 ∈ ℝ) |
| 8 | 7 | abssi 4070 |
. . . 4
⊢ {𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))} ⊆ ℝ |
| 9 | | ax-hv0cl 31022 |
. . . . . . 7
⊢
0ℎ ∈ ℋ |
| 10 | | norm0 31147 |
. . . . . . . . 9
⊢
(normℎ‘0ℎ) =
0 |
| 11 | | 0le1 11786 |
. . . . . . . . 9
⊢ 0 ≤
1 |
| 12 | 10, 11 | eqbrtri 5164 |
. . . . . . . 8
⊢
(normℎ‘0ℎ) ≤
1 |
| 13 | | nmcex.4 |
. . . . . . . . 9
⊢ (𝑁‘(𝑇‘0ℎ)) =
0 |
| 14 | 13 | eqcomi 2746 |
. . . . . . . 8
⊢ 0 =
(𝑁‘(𝑇‘0ℎ)) |
| 15 | 12, 14 | pm3.2i 470 |
. . . . . . 7
⊢
((normℎ‘0ℎ) ≤ 1 ∧ 0 =
(𝑁‘(𝑇‘0ℎ))) |
| 16 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑥 = 0ℎ →
(normℎ‘𝑥) =
(normℎ‘0ℎ)) |
| 17 | 16 | breq1d 5153 |
. . . . . . . . 9
⊢ (𝑥 = 0ℎ →
((normℎ‘𝑥) ≤ 1 ↔
(normℎ‘0ℎ) ≤ 1)) |
| 18 | | 2fveq3 6911 |
. . . . . . . . . 10
⊢ (𝑥 = 0ℎ →
(𝑁‘(𝑇‘𝑥)) = (𝑁‘(𝑇‘0ℎ))) |
| 19 | 18 | eqeq2d 2748 |
. . . . . . . . 9
⊢ (𝑥 = 0ℎ →
(0 = (𝑁‘(𝑇‘𝑥)) ↔ 0 = (𝑁‘(𝑇‘0ℎ)))) |
| 20 | 17, 19 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑥 = 0ℎ →
(((normℎ‘𝑥) ≤ 1 ∧ 0 = (𝑁‘(𝑇‘𝑥))) ↔
((normℎ‘0ℎ) ≤ 1 ∧ 0 = (𝑁‘(𝑇‘0ℎ))))) |
| 21 | 20 | rspcev 3622 |
. . . . . . 7
⊢
((0ℎ ∈ ℋ ∧
((normℎ‘0ℎ) ≤ 1 ∧ 0 = (𝑁‘(𝑇‘0ℎ)))) →
∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 0 = (𝑁‘(𝑇‘𝑥)))) |
| 22 | 9, 15, 21 | mp2an 692 |
. . . . . 6
⊢
∃𝑥 ∈
ℋ ((normℎ‘𝑥) ≤ 1 ∧ 0 = (𝑁‘(𝑇‘𝑥))) |
| 23 | | c0ex 11255 |
. . . . . . 7
⊢ 0 ∈
V |
| 24 | | eqeq1 2741 |
. . . . . . . . 9
⊢ (𝑚 = 0 → (𝑚 = (𝑁‘(𝑇‘𝑥)) ↔ 0 = (𝑁‘(𝑇‘𝑥)))) |
| 25 | 24 | anbi2d 630 |
. . . . . . . 8
⊢ (𝑚 = 0 →
(((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥))) ↔
((normℎ‘𝑥) ≤ 1 ∧ 0 = (𝑁‘(𝑇‘𝑥))))) |
| 26 | 25 | rexbidv 3179 |
. . . . . . 7
⊢ (𝑚 = 0 → (∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥))) ↔ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 0 = (𝑁‘(𝑇‘𝑥))))) |
| 27 | 23, 26 | elab 3679 |
. . . . . 6
⊢ (0 ∈
{𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))} ↔ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 0 = (𝑁‘(𝑇‘𝑥)))) |
| 28 | 22, 27 | mpbir 231 |
. . . . 5
⊢ 0 ∈
{𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))} |
| 29 | 28 | ne0ii 4344 |
. . . 4
⊢ {𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))} ≠ ∅ |
| 30 | | nmcex.1 |
. . . . 5
⊢
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ ℋ
((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1) |
| 31 | | 2rp 13039 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ+ |
| 32 | | rpdivcl 13060 |
. . . . . . . . . 10
⊢ ((2
∈ ℝ+ ∧ 𝑦 ∈ ℝ+) → (2 /
𝑦) ∈
ℝ+) |
| 33 | 31, 32 | mpan 690 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ+
→ (2 / 𝑦) ∈
ℝ+) |
| 34 | 33 | rpred 13077 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ+
→ (2 / 𝑦) ∈
ℝ) |
| 35 | 34 | adantr 480 |
. . . . . . 7
⊢ ((𝑦 ∈ ℝ+
∧ ∀𝑧 ∈
ℋ ((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1)) → (2 / 𝑦) ∈ ℝ) |
| 36 | | rpre 13043 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℝ) |
| 37 | 36 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → 𝑦 ∈ ℝ) |
| 38 | 37 | rehalfcld 12513 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (𝑦 / 2) ∈ ℝ) |
| 39 | 38 | recnd 11289 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (𝑦 / 2) ∈ ℂ) |
| 40 | | simprl 771 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → 𝑥 ∈ ℋ) |
| 41 | | hvmulcl 31032 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦 / 2) ∈ ℂ ∧ 𝑥 ∈ ℋ) → ((𝑦 / 2)
·ℎ 𝑥) ∈ ℋ) |
| 42 | 39, 40, 41 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → ((𝑦 / 2) ·ℎ
𝑥) ∈
ℋ) |
| 43 | | normcl 31144 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 / 2)
·ℎ 𝑥) ∈ ℋ →
(normℎ‘((𝑦 / 2) ·ℎ
𝑥)) ∈
ℝ) |
| 44 | 42, 43 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) →
(normℎ‘((𝑦 / 2) ·ℎ
𝑥)) ∈
ℝ) |
| 45 | | simprr 773 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) →
(normℎ‘𝑥) ≤ 1) |
| 46 | | normcl 31144 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℋ →
(normℎ‘𝑥) ∈ ℝ) |
| 47 | 46 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) →
(normℎ‘𝑥) ∈ ℝ) |
| 48 | | 1red 11262 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → 1 ∈
ℝ) |
| 49 | | rphalfcl 13062 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℝ+
→ (𝑦 / 2) ∈
ℝ+) |
| 50 | 49 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (𝑦 / 2) ∈
ℝ+) |
| 51 | 47, 48, 50 | lemul2d 13121 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) →
((normℎ‘𝑥) ≤ 1 ↔ ((𝑦 / 2) ·
(normℎ‘𝑥)) ≤ ((𝑦 / 2) · 1))) |
| 52 | 45, 51 | mpbid 232 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → ((𝑦 / 2) ·
(normℎ‘𝑥)) ≤ ((𝑦 / 2) · 1)) |
| 53 | | rpcn 13045 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 / 2) ∈ ℝ+
→ (𝑦 / 2) ∈
ℂ) |
| 54 | | norm-iii 31159 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑦 / 2) ∈ ℂ ∧ 𝑥 ∈ ℋ) →
(normℎ‘((𝑦 / 2) ·ℎ
𝑥)) = ((abs‘(𝑦 / 2)) ·
(normℎ‘𝑥))) |
| 55 | 53, 54 | sylan 580 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 / 2) ∈ ℝ+
∧ 𝑥 ∈ ℋ)
→ (normℎ‘((𝑦 / 2) ·ℎ
𝑥)) = ((abs‘(𝑦 / 2)) ·
(normℎ‘𝑥))) |
| 56 | | rpre 13043 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 / 2) ∈ ℝ+
→ (𝑦 / 2) ∈
ℝ) |
| 57 | | rpge0 13048 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 / 2) ∈ ℝ+
→ 0 ≤ (𝑦 /
2)) |
| 58 | 56, 57 | absidd 15461 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 / 2) ∈ ℝ+
→ (abs‘(𝑦 / 2))
= (𝑦 / 2)) |
| 59 | 58 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 / 2) ∈ ℝ+
→ ((abs‘(𝑦 / 2))
· (normℎ‘𝑥)) = ((𝑦 / 2) ·
(normℎ‘𝑥))) |
| 60 | 59 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 / 2) ∈ ℝ+
∧ 𝑥 ∈ ℋ)
→ ((abs‘(𝑦 / 2))
· (normℎ‘𝑥)) = ((𝑦 / 2) ·
(normℎ‘𝑥))) |
| 61 | 55, 60 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦 / 2) ∈ ℝ+
∧ 𝑥 ∈ ℋ)
→ ((𝑦 / 2) ·
(normℎ‘𝑥)) = (normℎ‘((𝑦 / 2)
·ℎ 𝑥))) |
| 62 | 50, 40, 61 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → ((𝑦 / 2) ·
(normℎ‘𝑥)) = (normℎ‘((𝑦 / 2)
·ℎ 𝑥))) |
| 63 | 39 | mulridd 11278 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → ((𝑦 / 2) · 1) = (𝑦 / 2)) |
| 64 | 52, 62, 63 | 3brtr3d 5174 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) →
(normℎ‘((𝑦 / 2) ·ℎ
𝑥)) ≤ (𝑦 / 2)) |
| 65 | | rphalflt 13064 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℝ+
→ (𝑦 / 2) < 𝑦) |
| 66 | 65 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (𝑦 / 2) < 𝑦) |
| 67 | 44, 38, 37, 64, 66 | lelttrd 11419 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) →
(normℎ‘((𝑦 / 2) ·ℎ
𝑥)) < 𝑦) |
| 68 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = ((𝑦 / 2) ·ℎ
𝑥) →
(normℎ‘𝑧) = (normℎ‘((𝑦 / 2)
·ℎ 𝑥))) |
| 69 | 68 | breq1d 5153 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = ((𝑦 / 2) ·ℎ
𝑥) →
((normℎ‘𝑧) < 𝑦 ↔
(normℎ‘((𝑦 / 2) ·ℎ
𝑥)) < 𝑦)) |
| 70 | | 2fveq3 6911 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = ((𝑦 / 2) ·ℎ
𝑥) → (𝑁‘(𝑇‘𝑧)) = (𝑁‘(𝑇‘((𝑦 / 2) ·ℎ
𝑥)))) |
| 71 | 70 | breq1d 5153 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = ((𝑦 / 2) ·ℎ
𝑥) → ((𝑁‘(𝑇‘𝑧)) < 1 ↔ (𝑁‘(𝑇‘((𝑦 / 2) ·ℎ
𝑥))) <
1)) |
| 72 | 69, 71 | imbi12d 344 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = ((𝑦 / 2) ·ℎ
𝑥) →
(((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1) ↔
((normℎ‘((𝑦 / 2) ·ℎ
𝑥)) < 𝑦 → (𝑁‘(𝑇‘((𝑦 / 2) ·ℎ
𝑥))) <
1))) |
| 73 | 72 | rspcv 3618 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 / 2)
·ℎ 𝑥) ∈ ℋ → (∀𝑧 ∈ ℋ
((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1) →
((normℎ‘((𝑦 / 2) ·ℎ
𝑥)) < 𝑦 → (𝑁‘(𝑇‘((𝑦 / 2) ·ℎ
𝑥))) <
1))) |
| 74 | 42, 73 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (∀𝑧 ∈ ℋ
((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1) →
((normℎ‘((𝑦 / 2) ·ℎ
𝑥)) < 𝑦 → (𝑁‘(𝑇‘((𝑦 / 2) ·ℎ
𝑥))) <
1))) |
| 75 | 67, 74 | mpid 44 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (∀𝑧 ∈ ℋ
((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1) → (𝑁‘(𝑇‘((𝑦 / 2) ·ℎ
𝑥))) <
1)) |
| 76 | 2 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (𝑁‘(𝑇‘𝑥)) ∈ ℝ) |
| 77 | 76, 48, 50 | ltmuldiv2d 13125 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (((𝑦 / 2) · (𝑁‘(𝑇‘𝑥))) < 1 ↔ (𝑁‘(𝑇‘𝑥)) < (1 / (𝑦 / 2)))) |
| 78 | 50 | rprecred 13088 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (1 / (𝑦 / 2)) ∈ ℝ) |
| 79 | | ltle 11349 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁‘(𝑇‘𝑥)) ∈ ℝ ∧ (1 / (𝑦 / 2)) ∈ ℝ) →
((𝑁‘(𝑇‘𝑥)) < (1 / (𝑦 / 2)) → (𝑁‘(𝑇‘𝑥)) ≤ (1 / (𝑦 / 2)))) |
| 80 | 76, 78, 79 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → ((𝑁‘(𝑇‘𝑥)) < (1 / (𝑦 / 2)) → (𝑁‘(𝑇‘𝑥)) ≤ (1 / (𝑦 / 2)))) |
| 81 | 77, 80 | sylbid 240 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (((𝑦 / 2) · (𝑁‘(𝑇‘𝑥))) < 1 → (𝑁‘(𝑇‘𝑥)) ≤ (1 / (𝑦 / 2)))) |
| 82 | | nmcex.5 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 / 2) ∈ ℝ+
∧ 𝑥 ∈ ℋ)
→ ((𝑦 / 2) ·
(𝑁‘(𝑇‘𝑥))) = (𝑁‘(𝑇‘((𝑦 / 2) ·ℎ
𝑥)))) |
| 83 | 50, 40, 82 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → ((𝑦 / 2) · (𝑁‘(𝑇‘𝑥))) = (𝑁‘(𝑇‘((𝑦 / 2) ·ℎ
𝑥)))) |
| 84 | 83 | breq1d 5153 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (((𝑦 / 2) · (𝑁‘(𝑇‘𝑥))) < 1 ↔ (𝑁‘(𝑇‘((𝑦 / 2) ·ℎ
𝑥))) <
1)) |
| 85 | | rpcn 13045 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℂ) |
| 86 | | rpne0 13051 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ≠
0) |
| 87 | | 2cn 12341 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℂ |
| 88 | | 2ne0 12370 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ≠
0 |
| 89 | | recdiv 11973 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) ∧ (2 ∈ ℂ
∧ 2 ≠ 0)) → (1 / (𝑦 / 2)) = (2 / 𝑦)) |
| 90 | 87, 88, 89 | mpanr12 705 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) → (1 / (𝑦 / 2)) = (2 / 𝑦)) |
| 91 | 85, 86, 90 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℝ+
→ (1 / (𝑦 / 2)) = (2 /
𝑦)) |
| 92 | 91 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (1 / (𝑦 / 2)) = (2 / 𝑦)) |
| 93 | 92 | breq2d 5155 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → ((𝑁‘(𝑇‘𝑥)) ≤ (1 / (𝑦 / 2)) ↔ (𝑁‘(𝑇‘𝑥)) ≤ (2 / 𝑦))) |
| 94 | 81, 84, 93 | 3imtr3d 293 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → ((𝑁‘(𝑇‘((𝑦 / 2) ·ℎ
𝑥))) < 1 → (𝑁‘(𝑇‘𝑥)) ≤ (2 / 𝑦))) |
| 95 | 75, 94 | syld 47 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) → (∀𝑧 ∈ ℋ
((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1) → (𝑁‘(𝑇‘𝑥)) ≤ (2 / 𝑦))) |
| 96 | 95 | imp 406 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ ℝ+
∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) ∧ ∀𝑧 ∈ ℋ
((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1)) → (𝑁‘(𝑇‘𝑥)) ≤ (2 / 𝑦)) |
| 97 | 96 | an32s 652 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ ℝ+
∧ ∀𝑧 ∈
ℋ ((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1)) ∧ (𝑥 ∈ ℋ ∧
(normℎ‘𝑥) ≤ 1)) → (𝑁‘(𝑇‘𝑥)) ≤ (2 / 𝑦)) |
| 98 | 97 | anassrs 467 |
. . . . . . . . . . 11
⊢ ((((𝑦 ∈ ℝ+
∧ ∀𝑧 ∈
ℋ ((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1)) ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) → (𝑁‘(𝑇‘𝑥)) ≤ (2 / 𝑦)) |
| 99 | | breq1 5146 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑁‘(𝑇‘𝑥)) → (𝑛 ≤ (2 / 𝑦) ↔ (𝑁‘(𝑇‘𝑥)) ≤ (2 / 𝑦))) |
| 100 | 98, 99 | syl5ibrcom 247 |
. . . . . . . . . 10
⊢ ((((𝑦 ∈ ℝ+
∧ ∀𝑧 ∈
ℋ ((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1)) ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) → (𝑛 = (𝑁‘(𝑇‘𝑥)) → 𝑛 ≤ (2 / 𝑦))) |
| 101 | 100 | expimpd 453 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ℝ+
∧ ∀𝑧 ∈
ℋ ((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1)) ∧ 𝑥 ∈ ℋ) →
(((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))) → 𝑛 ≤ (2 / 𝑦))) |
| 102 | 101 | rexlimdva 3155 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℝ+
∧ ∀𝑧 ∈
ℋ ((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1)) → (∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))) → 𝑛 ≤ (2 / 𝑦))) |
| 103 | 102 | alrimiv 1927 |
. . . . . . 7
⊢ ((𝑦 ∈ ℝ+
∧ ∀𝑧 ∈
ℋ ((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1)) → ∀𝑛(∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))) → 𝑛 ≤ (2 / 𝑦))) |
| 104 | | eqeq1 2741 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (𝑚 = (𝑁‘(𝑇‘𝑥)) ↔ 𝑛 = (𝑁‘(𝑇‘𝑥)))) |
| 105 | 104 | anbi2d 630 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 →
(((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥))) ↔
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))))) |
| 106 | 105 | rexbidv 3179 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥))) ↔ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))))) |
| 107 | 106 | ralab 3697 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
{𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}𝑛 ≤ 𝑧 ↔ ∀𝑛(∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))) → 𝑛 ≤ 𝑧)) |
| 108 | | breq2 5147 |
. . . . . . . . . . 11
⊢ (𝑧 = (2 / 𝑦) → (𝑛 ≤ 𝑧 ↔ 𝑛 ≤ (2 / 𝑦))) |
| 109 | 108 | imbi2d 340 |
. . . . . . . . . 10
⊢ (𝑧 = (2 / 𝑦) → ((∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))) → 𝑛 ≤ 𝑧) ↔ (∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))) → 𝑛 ≤ (2 / 𝑦)))) |
| 110 | 109 | albidv 1920 |
. . . . . . . . 9
⊢ (𝑧 = (2 / 𝑦) → (∀𝑛(∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))) → 𝑛 ≤ 𝑧) ↔ ∀𝑛(∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))) → 𝑛 ≤ (2 / 𝑦)))) |
| 111 | 107, 110 | bitrid 283 |
. . . . . . . 8
⊢ (𝑧 = (2 / 𝑦) → (∀𝑛 ∈ {𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}𝑛 ≤ 𝑧 ↔ ∀𝑛(∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))) → 𝑛 ≤ (2 / 𝑦)))) |
| 112 | 111 | rspcev 3622 |
. . . . . . 7
⊢ (((2 /
𝑦) ∈ ℝ ∧
∀𝑛(∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑛 = (𝑁‘(𝑇‘𝑥))) → 𝑛 ≤ (2 / 𝑦))) → ∃𝑧 ∈ ℝ ∀𝑛 ∈ {𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}𝑛 ≤ 𝑧) |
| 113 | 35, 103, 112 | syl2anc 584 |
. . . . . 6
⊢ ((𝑦 ∈ ℝ+
∧ ∀𝑧 ∈
ℋ ((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1)) → ∃𝑧 ∈ ℝ ∀𝑛 ∈ {𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}𝑛 ≤ 𝑧) |
| 114 | 113 | rexlimiva 3147 |
. . . . 5
⊢
(∃𝑦 ∈
ℝ+ ∀𝑧 ∈ ℋ
((normℎ‘𝑧) < 𝑦 → (𝑁‘(𝑇‘𝑧)) < 1) → ∃𝑧 ∈ ℝ ∀𝑛 ∈ {𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}𝑛 ≤ 𝑧) |
| 115 | 30, 114 | ax-mp 5 |
. . . 4
⊢
∃𝑧 ∈
ℝ ∀𝑛 ∈
{𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}𝑛 ≤ 𝑧 |
| 116 | | supxrre 13369 |
. . . 4
⊢ (({𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))} ⊆ ℝ ∧ {𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))} ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑛 ∈ {𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}𝑛 ≤ 𝑧) → sup({𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}, ℝ*, < ) =
sup({𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}, ℝ, < )) |
| 117 | 8, 29, 115, 116 | mp3an 1463 |
. . 3
⊢
sup({𝑚 ∣
∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}, ℝ*, < ) =
sup({𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}, ℝ, < ) |
| 118 | 1, 117 | eqtri 2765 |
. 2
⊢ (𝑆‘𝑇) = sup({𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}, ℝ, < ) |
| 119 | | suprcl 12228 |
. . 3
⊢ (({𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))} ⊆ ℝ ∧ {𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))} ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑛 ∈ {𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}𝑛 ≤ 𝑧) → sup({𝑚 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}, ℝ, < ) ∈
ℝ) |
| 120 | 8, 29, 115, 119 | mp3an 1463 |
. 2
⊢
sup({𝑚 ∣
∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑚 = (𝑁‘(𝑇‘𝑥)))}, ℝ, < ) ∈
ℝ |
| 121 | 118, 120 | eqeltri 2837 |
1
⊢ (𝑆‘𝑇) ∈ ℝ |