Theorem nmcopexlem5 9870

Description: Lemma for nmcopex 9872.

Hypotheses

Ref	Expression
nmcopex.1	|- T e. LinOp
nmcopex.2	|- T e. ConOp
nmcopexlem4.3	|- A = {k e. NN | (1 / k) < y}
nmcopexlem4.4	|- M = sup(A, RR, `' < )

Assertion

Ref	Expression
nmcopexlem5	|- (((y e. RR /\ 0 < y) /\ (n e. NN /\ M <_ n) /\ (x e. H~ /\ (normh` x) <_ 1)) -> (normh` ((1 / n) .h x)) < y)

Distinct variable groups:   x,k,M   y,k,T,x   x,n,y,T

Proof of Theorem nmcopexlem5

Step	Hyp	Ref	Expression
1		hvmulclt 8804	. . . . . 6 |- (((1 / n) e. CC /\ x e. H~) -> ((1 / n) .h x) e. H~)
2		rerecclt 5759	. . . . . . . 8 |- ((n e. RR /\ n =/= 0) -> (1 / n) e. RR)
3		nnret 5877	. . . . . . . 8 |- (n e. NN -> n e. RR)
4		nnne0t 5897	. . . . . . . 8 |- (n e. NN -> n =/= 0)
5	2, 3, 4	sylanc 471	. . . . . . 7 |- (n e. NN -> (1 / n) e. RR)
6	5	recnd 5287	. . . . . 6 |- (n e. NN -> (1 / n) e. CC)
7	1, 6	sylan 448	. . . . 5 |- ((n e. NN /\ x e. H~) -> ((1 / n) .h x) e. H~)
8		normclt 8912	. . . . 5 |- (((1 / n) .h x) e. H~ -> (normh` ((1 / n) .h x)) e. RR)
9	7, 8	syl 10	. . . 4 |- ((n e. NN /\ x e. H~) -> (normh` ((1 / n) .h x)) e. RR)
10	9	ad2ant2r 409	. . 3 |- (((n e. NN /\ M <_ n) /\ (x e. H~ /\ (normh` x) <_ 1)) -> (normh` ((1 / n) .h x)) e. RR)
11	10	3adant1 795	. 2 |- (((y e. RR /\ 0 < y) /\ (n e. NN /\ M <_ n) /\ (x e. H~ /\ (normh` x) <_ 1)) -> (normh` ((1 / n) .h x)) e. RR)
12		nmcopex.1	. . . . . 6 |- T e. LinOp
13		nmcopex.2	. . . . . 6 |- T e. ConOp
14		nmcopexlem4.3	. . . . . 6 |- A = {k e. NN | (1 / k) < y}
15		nmcopexlem4.4	. . . . . 6 |- M = sup(A, RR, `' < )
16	12, 13, 14, 15	nmcopexlem4 9869	. . . . 5 |- ((y e. RR /\ 0 < y) -> (M e. NN /\ (1 / M) < y))
17	16	pm3.26d 321	. . . 4 |- ((y e. RR /\ 0 < y) -> M e. NN)
18		rerecclt 5759	. . . . 5 |- ((M e. RR /\ M =/= 0) -> (1 / M) e. RR)
19		nnret 5877	. . . . 5 |- (M e. NN -> M e. RR)
20		nnne0t 5897	. . . . 5 |- (M e. NN -> M =/= 0)
21	18, 19, 20	sylanc 471	. . . 4 |- (M e. NN -> (1 / M) e. RR)
22	17, 21	syl 10	. . 3 |- ((y e. RR /\ 0 < y) -> (1 / M) e. RR)
23	22	3ad2ant1 798	. 2 |- (((y e. RR /\ 0 < y) /\ (n e. NN /\ M <_ n) /\ (x e. H~ /\ (normh` x) <_ 1)) -> (1 / M) e. RR)
24		pm3.26 319	. . 3 |- ((y e. RR /\ 0 < y) -> y e. RR)
25	24	3ad2ant1 798	. 2 |- (((y e. RR /\ 0 < y) /\ (n e. NN /\ M <_ n) /\ (x e. H~ /\ (normh` x) <_ 1)) -> y e. RR)
26	10	3adant1 795	. . . 4 |- ((M e. NN /\ (n e. NN /\ M <_ n) /\ (x e. H~ /\ (normh` x) <_ 1)) -> (normh` ((1 / n) .h x)) e. RR)
27	5	ad2antrr 404	. . . . 5 |- (((n e. NN /\ M <_ n) /\ (x e. H~ /\ (normh` x) <_ 1)) -> (1 / n) e. RR)
28	27	3adant1 795	. . . 4 |- ((M e. NN /\ (n e. NN /\ M <_ n) /\ (x e. H~ /\ (normh` x) <_ 1)) -> (1 / n) e. RR)
29	21	3ad2ant1 798	. . . 4 |- ((M e. NN /\ (n e. NN /\ M <_ n) /\ (x e. H~ /\ (normh` x) <_ 1)) -> (1 / M) e. RR)
30		lemul2itOLD 5796	. . . . . 6 |- ((((normh` x) e. RR /\ 1 e. RR /\ (1 / n) e. RR) /\ (0 <_ (1 / n) /\ (normh` x) <_ 1)) -> ((1 / n) x. (normh` x)) <_ ((1 / n) x. 1))
31		normclt 8912	. . . . . . . . 9 |- (x e. H~ -> (normh` x) e. RR)
32	31	ad2antrl 406	. . . . . . . 8 |- ((M e. NN /\ (x e. H~ /\ (normh` x) <_ 1)) -> (normh` x) e. RR)
33	32	3adant2 796	. . . . . . 7 |- ((M e. NN /\ (n e. NN /\ M <_ n) /\ (x e. H~ /\ (normh` x) <_ 1)) -> (normh` x) e. RR)
34		1re 5407	. . . . . . . 8 |- 1 e. RR
35	34	a1i 8	. . . . . . 7 |- ((M e. NN /\ (n e. NN /\ M <_ n) /\ (x e. H~ /\ (normh` x) <_ 1)) -> 1 e. RR)
36	33, 35, 28	3jca 817	. . . . . 6 |- ((M e. NN /\ (n e. NN /\ M <_ n) /\ (x e. H~ /\ (normh` x) <_ 1)) -> ((normh` x) e. RR /\ 1 e. RR /\ (1 / n) e. RR))
37		0re 5412	. . . . . . . . . . . 12 |- 0 e. RR
38		lt01 5653	. . . . . . . . . . . 12 |- 0 < 1
39	37, 34, 38	ltlei 5554	. . . . . . . . . . 11 |- 0 <_ 1
40		divge0t 5810	. . . . . . . . . . 11 |- (((1 e. RR /\ 0 <_ 1) /\ (n e. RR /\ 0 < n)) -> 0 <_ (1 / n))
41	34, 39, 40	mpanl12 706	. . . . . . . . . 10 |- ((n e. RR /\ 0 < n) -> 0 <_ (1 / n))
42		nngt0t 5894	. . . . . . . . . 10 |- (n e. NN -> 0 < n)
43	41, 3, 42	sylanc 471	. . . . . . . . 9 |- (n e. NN -> 0 <_ (1 / n))
44	43	ad2antrl 406	. . . . . . . 8 |- ((M e. NN /\ (n e. NN /\ M <_ n)) -> 0 <_ (1 / n))
45	44	3adant3 797	. . . . . . 7 |- ((M e. NN /\ (n e. NN /\ M <_ n) /\ (x e. H~ /\ (normh` x) <_ 1)) -> 0 <_ (1 / n))
46		pm3.27 323	. . . . . . . 8 |- ((x e. H~ /\ (normh` x) <_ 1) -> (normh` x) <_ 1)
47	46	3ad2ant3 800	. . . . . . 7 |- ((M e. NN /\ (n e. NN /\ M <_ n) /\ (x e. H~ /\ (normh` x) <_ 1)) -> (normh` x) <_ 1)
48	45, 47	jca 288	. . . . . 6 |- ((M e. NN /\ (n e. NN /\ M <_ n) /\ (x e. H~ /\ (normh` x) <_ 1)) -> (0 <_ (1 / n) /\ (normh` x) <_ 1))
49	30, 36, 48	sylanc 471	. . . . 5 |- ((M e. NN /\ (n e. NN /\ M <_ n) /\ (x e. H~ /\ (normh` x) <_ 1)) -> ((1 / n) x. (normh` x)) <_ ((1 / n) x. 1))
50		norm-iiit 8928	. . . . . . . . 9 |- (((1 / n) e. CC /\ x e. H~) -> (normh` ((1 / n) .h x)) = ((abs` (1 / n)) x. (normh` x)))
51	50, 6	sylan 448	. . . . . . . 8 |- ((n e. NN /\ x e. H~) -> (normh` ((1 / n) .h x)) = ((abs` (1 / n)) x. (normh` x)))
52		absidt 6797	. . . . . . . . . . 11 |- (((1 / n) e. RR /\ 0 <_ (1 / n)) -> (abs` (1 / n)) = (1 / n))
53	52, 5, 43	sylanc 471	. . . . . . . . . 10 |- (n e. NN -> (abs` (1 / n)) = (1 / n))
54	53	adantr 389	. . . . . . . . 9 |- ((n e. NN /\ x e. H~) -> (abs` (1 / n)) = (1 / n))
55	54	opreq1d 3960	. . . . . . . 8 |- ((n e. NN /\ x e. H~) -> ((abs` (1 / n)) x. (normh` x)) = ((1 / n) x. (normh` x)))
56	51, 55	eqtr2d 1500	. . . . . . 7 |- ((n e. NN /\ x e. H~) -> ((1 / n) x. (normh` x)) = (normh` ((1 / n) .h x)))
57	56	ad2ant2r 409	. . . . . 6 |- (((n e. NN /\ M <_ n) /\ (x e. H~ /\ (normh` x) <_ 1)) -> ((1 / n) x. (normh` x)) = (normh` ((1 / n) .h x)))
58	57	3adant1 795	. . . . 5 |- ((M e. NN /\ (n e. NN /\ M <_ n) /\ (x e. H~ /\ (normh` x) <_ 1)) -> ((1 / n) x. (normh` x)) = (normh` ((1 / n) .h x)))
59		ax1id 5254	. . . . . . . 8 |- ((1 / n) e. CC -> ((1 / n) x. 1) = (1 / n))
60	6, 59	syl 10	. . . . . . 7 |- (n e. NN -> ((1 / n) x. 1) = (1 / n))
61	60	ad2antrl 406	. . . . . 6 |- ((M e. NN /\ (n e. NN /\ M <_ n)) -> ((1 / n) x. 1) = (1 / n))
62	61	3adant3 797	. . . . 5 |- ((M e. NN /\ (n e. NN /\ M <_ n) /\ (x e. H~ /\ (normh` x) <_ 1)) -> ((1 / n) x. 1) = (1 / n))
63	49, 58, 62	3brtr3d 2634	. . . 4 |- ((M e. NN /\ (n e. NN /\ M <_ n) /\ (x e. H~ /\ (normh` x) <_ 1)) -> (normh` ((1 / n) .h x)) <_ (1 / n))
64		lerect 5833	. . . . . . . 8 |- (((M e. RR /\ 0 < M) /\ (n e. RR /\ 0 < n)) -> (M <_ n <-> (1 / n) <_ (1 / M)))
65		nngt0t 5894	. . . . . . . . 9 |- (M e. NN -> 0 < M)
66	19, 65	jca 288	. . . . . . . 8 |- (M e. NN -> (M e. RR /\ 0