Metamath Proof Explorer

Theorem nmcexi

Description: Lemma for nmcopexi and nmcfnexi . The norm of a continuous linear Hilbert space operator or functional exists. Theorem 3.5(i) of Beran p. 99. (Contributed by Mario Carneiro, 17-Nov-2013) (Proof shortened by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses nmcex.1 ⊢ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) < 𝑦 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) < 1 )
nmcex.2 ⊢ ( 𝑆 ‘ 𝑇 ) = sup ( { 𝑚 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ* , < )
nmcex.3 ⊢ ( 𝑥 ∈ ℋ → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
nmcex.4 ⊢ ( 𝑁 ‘ ( 𝑇 ‘ 0ℎ ) ) = 0
nmcex.5 ⊢ ( ( ( 𝑦 / 2 ) ∈ ℝ+ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑦 / 2 ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) = ( 𝑁 ‘ ( 𝑇 ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) ) )
Assertion nmcexi ( 𝑆 ‘ 𝑇 ) ∈ ℝ

Proof

Step Hyp Ref Expression
1 nmcex.1 ⊢ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) < 𝑦 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) < 1 )
2 nmcex.2 ⊢ ( 𝑆 ‘ 𝑇 ) = sup ( { 𝑚 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ* , < )
3 nmcex.3 ⊢ ( 𝑥 ∈ ℋ → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
4 nmcex.4 ⊢ ( 𝑁 ‘ ( 𝑇 ‘ 0ℎ ) ) = 0
5 nmcex.5 ⊢ ( ( ( 𝑦 / 2 ) ∈ ℝ+ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑦 / 2 ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) = ( 𝑁 ‘ ( 𝑇 ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) ) )
6 eleq1 ⊢ ( 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) → ( 𝑚 ∈ ℝ ↔ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) )
7 3 6 syl5ibrcom ⊢ ( 𝑥 ∈ ℋ → ( 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) → 𝑚 ∈ ℝ ) )
8 7 imp ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑚 ∈ ℝ )
9 8 adantrl ⊢ ( ( 𝑥 ∈ ℋ ∧ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ) → 𝑚 ∈ ℝ )
10 9 rexlimiva ⊢ ( ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑚 ∈ ℝ )
11 10 abssi ⊢ { 𝑚 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } ⊆ ℝ
12 ax-hv0cl ⊢ 0ℎ ∈ ℋ
13 norm0 ⊢ ( normℎ ‘ 0ℎ ) = 0
14 0le1 ⊢ 0 ≤ 1
15 13 14 eqbrtri ⊢ ( normℎ ‘ 0ℎ ) ≤ 1
16 4 eqcomi ⊢ 0 = ( 𝑁 ‘ ( 𝑇 ‘ 0ℎ ) )
17 15 16 pm3.2i ⊢ ( ( normℎ ‘ 0ℎ ) ≤ 1 ∧ 0 = ( 𝑁 ‘ ( 𝑇 ‘ 0ℎ ) ) )
18 fveq2 ⊢ ( 𝑥 = 0ℎ → ( normℎ ‘ 𝑥 ) = ( normℎ ‘ 0ℎ ) )
19 18 breq1d ⊢ ( 𝑥 = 0ℎ → ( ( normℎ ‘ 𝑥 ) ≤ 1 ↔ ( normℎ ‘ 0ℎ ) ≤ 1 ) )
20 2fveq3 ⊢ ( 𝑥 = 0ℎ → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) = ( 𝑁 ‘ ( 𝑇 ‘ 0ℎ ) ) )
21 20 eqeq2d ⊢ ( 𝑥 = 0ℎ → ( 0 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ↔ 0 = ( 𝑁 ‘ ( 𝑇 ‘ 0ℎ ) ) ) )
22 19 21 anbi12d ⊢ ( 𝑥 = 0ℎ → ( ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 0 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ↔ ( ( normℎ ‘ 0ℎ ) ≤ 1 ∧ 0 = ( 𝑁 ‘ ( 𝑇 ‘ 0ℎ ) ) ) ) )
23 22 rspcev ⊢ ( ( 0ℎ ∈ ℋ ∧ ( ( normℎ ‘ 0ℎ ) ≤ 1 ∧ 0 = ( 𝑁 ‘ ( 𝑇 ‘ 0ℎ ) ) ) ) → ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 0 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
24 12 17 23 mp2an ⊢ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 0 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) )
25 c0ex ⊢ 0 ∈ V
26 eqeq1 ⊢ ( 𝑚 = 0 → ( 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ↔ 0 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
27 26 anbi2d ⊢ ( 𝑚 = 0 → ( ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ↔ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 0 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ) )
28 27 rexbidv ⊢ ( 𝑚 = 0 → ( ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ↔ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 0 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ) )
29 25 28 elab ⊢ ( 0 ∈ { 𝑚 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } ↔ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 0 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
30 24 29 mpbir ⊢ 0 ∈ { 𝑚 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) }
31 30 ne0ii ⊢ { 𝑚 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } ≠ ∅
32 2rp ⊢ 2 ∈ ℝ+
33 rpdivcl ⊢ ( ( 2 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) → ( 2 / 𝑦 ) ∈ ℝ+ )
34 32 33 mpan ⊢ ( 𝑦 ∈ ℝ+ → ( 2 / 𝑦 ) ∈ ℝ+ )
35 34 rpred ⊢ ( 𝑦 ∈ ℝ+ → ( 2 / 𝑦 ) ∈ ℝ )
36 35 adantr ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) < 𝑦 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) < 1 ) ) → ( 2 / 𝑦 ) ∈ ℝ )
37 rpre ⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ )
38 37 adantr ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → 𝑦 ∈ ℝ )
39 38 rehalfcld ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( 𝑦 / 2 ) ∈ ℝ )
40 39 recnd ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( 𝑦 / 2 ) ∈ ℂ )
41 simprl ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → 𝑥 ∈ ℋ )
42 hvmulcl ⊢ ( ( ( 𝑦 / 2 ) ∈ ℂ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ∈ ℋ )
43 40 41 42 syl2anc ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ∈ ℋ )
44 normcl ⊢ ( ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ∈ ℋ → ( normℎ ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) ∈ ℝ )
45 43 44 syl ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( normℎ ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) ∈ ℝ )
46 simprr ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( normℎ ‘ 𝑥 ) ≤ 1 )
47 normcl ⊢ ( 𝑥 ∈ ℋ → ( normℎ ‘ 𝑥 ) ∈ ℝ )
48 47 ad2antrl ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( normℎ ‘ 𝑥 ) ∈ ℝ )
49 1red ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → 1 ∈ ℝ )
50 rphalfcl ⊢ ( 𝑦 ∈ ℝ+ → ( 𝑦 / 2 ) ∈ ℝ+ )
51 50 adantr ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( 𝑦 / 2 ) ∈ ℝ+ )
52 48 49 51 lemul2d ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( ( normℎ ‘ 𝑥 ) ≤ 1 ↔ ( ( 𝑦 / 2 ) · ( normℎ ‘ 𝑥 ) ) ≤ ( ( 𝑦 / 2 ) · 1 ) ) )
53 46 52 mpbid ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( ( 𝑦 / 2 ) · ( normℎ ‘ 𝑥 ) ) ≤ ( ( 𝑦 / 2 ) · 1 ) )
54 rpcn ⊢ ( ( 𝑦 / 2 ) ∈ ℝ+ → ( 𝑦 / 2 ) ∈ ℂ )
55 norm-iii ⊢ ( ( ( 𝑦 / 2 ) ∈ ℂ ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) = ( ( abs ‘ ( 𝑦 / 2 ) ) · ( normℎ ‘ 𝑥 ) ) )
56 54 55 sylan ⊢ ( ( ( 𝑦 / 2 ) ∈ ℝ+ ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) = ( ( abs ‘ ( 𝑦 / 2 ) ) · ( normℎ ‘ 𝑥 ) ) )
57 rpre ⊢ ( ( 𝑦 / 2 ) ∈ ℝ+ → ( 𝑦 / 2 ) ∈ ℝ )
58 rpge0 ⊢ ( ( 𝑦 / 2 ) ∈ ℝ+ → 0 ≤ ( 𝑦 / 2 ) )
59 57 58 absidd ⊢ ( ( 𝑦 / 2 ) ∈ ℝ+ → ( abs ‘ ( 𝑦 / 2 ) ) = ( 𝑦 / 2 ) )
60 59 oveq1d ⊢ ( ( 𝑦 / 2 ) ∈ ℝ+ → ( ( abs ‘ ( 𝑦 / 2 ) ) · ( normℎ ‘ 𝑥 ) ) = ( ( 𝑦 / 2 ) · ( normℎ ‘ 𝑥 ) ) )
61 60 adantr ⊢ ( ( ( 𝑦 / 2 ) ∈ ℝ+ ∧ 𝑥 ∈ ℋ ) → ( ( abs ‘ ( 𝑦 / 2 ) ) · ( normℎ ‘ 𝑥 ) ) = ( ( 𝑦 / 2 ) · ( normℎ ‘ 𝑥 ) ) )
62 56 61 eqtr2d ⊢ ( ( ( 𝑦 / 2 ) ∈ ℝ+ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑦 / 2 ) · ( normℎ ‘ 𝑥 ) ) = ( normℎ ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) )
63 51 41 62 syl2anc ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( ( 𝑦 / 2 ) · ( normℎ ‘ 𝑥 ) ) = ( normℎ ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) )
64 40 mulridd ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( ( 𝑦 / 2 ) · 1 ) = ( 𝑦 / 2 ) )
65 53 63 64 3brtr3d ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( normℎ ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) ≤ ( 𝑦 / 2 ) )
66 rphalflt ⊢ ( 𝑦 ∈ ℝ+ → ( 𝑦 / 2 ) < 𝑦 )
67 66 adantr ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( 𝑦 / 2 ) < 𝑦 )
68 45 39 38 65 67 lelttrd ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( normℎ ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) < 𝑦 )
69 fveq2 ⊢ ( 𝑧 = ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) → ( normℎ ‘ 𝑧 ) = ( normℎ ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) )
70 69 breq1d ⊢ ( 𝑧 = ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) → ( ( normℎ ‘ 𝑧 ) < 𝑦 ↔ ( normℎ ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) < 𝑦 ) )
71 2fveq3 ⊢ ( 𝑧 = ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) = ( 𝑁 ‘ ( 𝑇 ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) ) )
72 71 breq1d ⊢ ( 𝑧 = ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) < 1 ↔ ( 𝑁 ‘ ( 𝑇 ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) ) < 1 ) )
73 70 72 imbi12d ⊢ ( 𝑧 = ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) → ( ( ( normℎ ‘ 𝑧 ) < 𝑦 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) < 1 ) ↔ ( ( normℎ ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) < 𝑦 → ( 𝑁 ‘ ( 𝑇 ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) ) < 1 ) ) )
74 73 rspcv ⊢ ( ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ∈ ℋ → ( ∀ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) < 𝑦 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) < 1 ) → ( ( normℎ ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) < 𝑦 → ( 𝑁 ‘ ( 𝑇 ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) ) < 1 ) ) )
75 43 74 syl ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( ∀ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) < 𝑦 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) < 1 ) → ( ( normℎ ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) < 𝑦 → ( 𝑁 ‘ ( 𝑇 ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) ) < 1 ) ) )
76 68 75 mpid ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( ∀ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) < 𝑦 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) < 1 ) → ( 𝑁 ‘ ( 𝑇 ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) ) < 1 ) )
77 3 ad2antrl ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
78 77 49 51 ltmuldiv2d ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( ( ( 𝑦 / 2 ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) < 1 ↔ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) < ( 1 / ( 𝑦 / 2 ) ) ) )
79 51 rprecred ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( 1 / ( 𝑦 / 2 ) ) ∈ ℝ )
80 ltle ⊢ ( ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 1 / ( 𝑦 / 2 ) ) ∈ ℝ ) → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) < ( 1 / ( 𝑦 / 2 ) ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 1 / ( 𝑦 / 2 ) ) ) )
81 77 79 80 syl2anc ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) < ( 1 / ( 𝑦 / 2 ) ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 1 / ( 𝑦 / 2 ) ) ) )
82 78 81 sylbid ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( ( ( 𝑦 / 2 ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) < 1 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 1 / ( 𝑦 / 2 ) ) ) )
83 51 41 5 syl2anc ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( ( 𝑦 / 2 ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) = ( 𝑁 ‘ ( 𝑇 ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) ) )
84 83 breq1d ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( ( ( 𝑦 / 2 ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) < 1 ↔ ( 𝑁 ‘ ( 𝑇 ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) ) < 1 ) )
85 rpcn ⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℂ )
86 rpne0 ⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ≠ 0 )
87 2cn ⊢ 2 ∈ ℂ
88 2ne0 ⊢ 2 ≠ 0
89 recdiv ⊢ ( ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( 1 / ( 𝑦 / 2 ) ) = ( 2 / 𝑦 ) )
90 87 88 89 mpanr12 ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) → ( 1 / ( 𝑦 / 2 ) ) = ( 2 / 𝑦 ) )
91 85 86 90 syl2anc ⊢ ( 𝑦 ∈ ℝ+ → ( 1 / ( 𝑦 / 2 ) ) = ( 2 / 𝑦 ) )
92 91 adantr ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( 1 / ( 𝑦 / 2 ) ) = ( 2 / 𝑦 ) )
93 92 breq2d ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 1 / ( 𝑦 / 2 ) ) ↔ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 2 / 𝑦 ) ) )
94 82 84 93 3imtr3d ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( ( 𝑁 ‘ ( 𝑇 ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) ) < 1 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 2 / 𝑦 ) ) )
95 76 94 syld ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( ∀ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) < 𝑦 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) < 1 ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 2 / 𝑦 ) ) )
96 95 imp ⊢ ( ( ( 𝑦 ∈ ℝ+ ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) ∧ ∀ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) < 𝑦 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) < 1 ) ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 2 / 𝑦 ) )
97 96 an32s ⊢ ( ( ( 𝑦 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) < 𝑦 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) < 1 ) ) ∧ ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 2 / 𝑦 ) )
98 97 anassrs ⊢ ( ( ( ( 𝑦 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) < 𝑦 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) < 1 ) ) ∧ 𝑥 ∈ ℋ ) ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 2 / 𝑦 ) )
99 breq1 ⊢ ( 𝑛 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) → ( 𝑛 ≤ ( 2 / 𝑦 ) ↔ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 2 / 𝑦 ) ) )
100 98 99 syl5ibrcom ⊢ ( ( ( ( 𝑦 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) < 𝑦 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) < 1 ) ) ∧ 𝑥 ∈ ℋ ) ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → ( 𝑛 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) → 𝑛 ≤ ( 2 / 𝑦 ) ) )
101 100 expimpd ⊢ ( ( ( 𝑦 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) < 𝑦 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) < 1 ) ) ∧ 𝑥 ∈ ℋ ) → ( ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑛 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑛 ≤ ( 2 / 𝑦 ) ) )
102 101 rexlimdva ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) < 𝑦 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) < 1 ) ) → ( ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑛 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑛 ≤ ( 2 / 𝑦 ) ) )
103 102 alrimiv ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) < 𝑦 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) < 1 ) ) → ∀ 𝑛 ( ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑛 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑛 ≤ ( 2 / 𝑦 ) ) )
104 eqeq1 ⊢ ( 𝑚 = 𝑛 → ( 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ↔ 𝑛 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
105 104 anbi2d ⊢ ( 𝑚 = 𝑛 → ( ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ↔ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑛 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ) )
106 105 rexbidv ⊢ ( 𝑚 = 𝑛 → ( ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ↔ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑛 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ) )
107 106 ralab ⊢ ( ∀ 𝑛 ∈ { 𝑚 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } 𝑛 ≤ 𝑧 ↔ ∀ 𝑛 ( ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑛 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑛 ≤ 𝑧 ) )
108 breq2 ⊢ ( 𝑧 = ( 2 / 𝑦 ) → ( 𝑛 ≤ 𝑧 ↔ 𝑛 ≤ ( 2 / 𝑦 ) ) )
109 108 imbi2d ⊢ ( 𝑧 = ( 2 / 𝑦 ) → ( ( ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑛 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑛 ≤ 𝑧 ) ↔ ( ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑛 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑛 ≤ ( 2 / 𝑦 ) ) ) )
110 109 albidv ⊢ ( 𝑧 = ( 2 / 𝑦 ) → ( ∀ 𝑛 ( ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑛 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑛 ≤ 𝑧 ) ↔ ∀ 𝑛 ( ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑛 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑛 ≤ ( 2 / 𝑦 ) ) ) )
111 107 110 bitrid ⊢ ( 𝑧 = ( 2 / 𝑦 ) → ( ∀ 𝑛 ∈ { 𝑚 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } 𝑛 ≤ 𝑧 ↔ ∀ 𝑛 ( ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑛 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑛 ≤ ( 2 / 𝑦 ) ) ) )
112 111 rspcev ⊢ ( ( ( 2 / 𝑦 ) ∈ ℝ ∧ ∀ 𝑛 ( ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑛 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → 𝑛 ≤ ( 2 / 𝑦 ) ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑛 ∈ { 𝑚 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } 𝑛 ≤ 𝑧 )
113 36 103 112 syl2anc ⊢ ( ( 𝑦 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) < 𝑦 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) < 1 ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑛 ∈ { 𝑚 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } 𝑛 ≤ 𝑧 )
114 113 rexlimiva ⊢ ( ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) < 𝑦 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) < 1 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑛 ∈ { 𝑚 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } 𝑛 ≤ 𝑧 )
115 1 114 ax-mp ⊢ ∃ 𝑧 ∈ ℝ ∀ 𝑛 ∈ { 𝑚 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } 𝑛 ≤ 𝑧
116 supxrre ⊢ ( ( { 𝑚 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } ⊆ ℝ ∧ { 𝑚 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } ≠ ∅ ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑛 ∈ { 𝑚 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } 𝑛 ≤ 𝑧 ) → sup ( { 𝑚 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ* , < ) = sup ( { 𝑚 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ , < ) )
117 11 31 115 116 mp3an ⊢ sup ( { 𝑚 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ* , < ) = sup ( { 𝑚 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ , < )
118 2 117 eqtri ⊢ ( 𝑆 ‘ 𝑇 ) = sup ( { 𝑚 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ , < )
119 suprcl ⊢ ( ( { 𝑚 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } ⊆ ℝ ∧ { 𝑚 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } ≠ ∅ ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑛 ∈ { 𝑚 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } 𝑛 ≤ 𝑧 ) → sup ( { 𝑚 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ , < ) ∈ ℝ )
120 11 31 115 119 mp3an ⊢ sup ( { 𝑚 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ , < ) ∈ ℝ
121 118 120 eqeltri ⊢ ( 𝑆 ‘ 𝑇 ) ∈ ℝ