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	⊢ ( 𝑆 ‘ 𝑇 ) ∈ ℝ