Theorem lnconi 27734

Description: Lemma for lnopconi 27735 and lnfnconi 27756. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.)

Hypotheses

Ref	Expression
lncon.1	|- ( T e. C -> S e. RR )
lncon.2	|- ( ( T e. C /\ y e. ~H ) -> ( N ` ( T ` y ) ) <_ ( S x. ( normh ` y ) ) )
lncon.3	|- ( T e. C <-> A. x e. ~H A. z e. RR+ E. y e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < y -> ( N ` ( ( T ` w ) M ( T ` x ) ) ) < z ) )
lncon.4	|- ( y e. ~H -> ( N ` ( T ` y ) ) e. RR )
lncon.5	|- ( ( w e. ~H /\ x e. ~H ) -> ( T ` ( w -h x ) ) = ( ( T ` w ) M ( T ` x ) ) )

Assertion

Ref	Expression
lnconi	|- ( T e. C <-> E. x e. RR A. y e. ~H ( N ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) )

Distinct variable groups:   x, w, y, z, N   y, M   w, T, x, y, z   x, S, y   y, C

Allowed substitution hints:   C( x, z, w)   S( z, w)   M( x, z, w)

Proof of Theorem lnconi

Dummy variable n is distinct from all other variables.

Step	Hyp	Ref	Expression
1		lncon.1	. . 3 |- ( T e. C -> S e. RR )
2		lncon.2	. . . 4 |- ( ( T e. C /\ y e. ~H ) -> ( N ` ( T ` y ) ) <_ ( S x. ( normh ` y ) ) )
3	2	ralrimiva 2813	. . 3 |- ( T e. C -> A. y e. ~H ( N ` ( T ` y ) ) <_ ( S x. ( normh ` y ) ) )
4		oveq1 6321	. . . . . 6 |- ( x = S -> ( x x. ( normh ` y ) ) = ( S x. ( normh ` y ) ) )
5	4	breq2d 4427	. . . . 5 |- ( x = S -> ( ( N ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) <-> ( N ` ( T ` y ) ) <_ ( S x. ( normh ` y ) ) ) )
6	5	ralbidv 2838	. . . 4 |- ( x = S -> ( A. y e. ~H ( N ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) <-> A. y e. ~H ( N ` ( T ` y ) ) <_ ( S x. ( normh ` y ) ) ) )
7	6	rspcev 3161	. . 3 |- ( ( S e. RR /\ A. y e. ~H ( N ` ( T ` y ) ) <_ ( S x. ( normh ` y ) ) ) -> E. x e. RR A. y e. ~H ( N ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) )
8	1, 3, 7	syl2anc 671	. 2 |- ( T e. C -> E. x e. RR A. y e. ~H ( N ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) )
9		arch 10894	. . . . . 6 |- ( x e. RR -> E. n e. NN x < n )
10	9	adantr 471	. . . . 5 |- ( ( x e. RR /\ A. y e. ~H ( N ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) ) -> E. n e. NN x < n )
11		nnre 10643	. . . . . . 7 |- ( n e. NN -> n e. RR )
12		simplll 773	. . . . . . . . . . . 12 |- ( ( ( ( x e. RR /\ n e. RR ) /\ x < n ) /\ y e. ~H ) -> x e. RR )
13		simpllr 774	. . . . . . . . . . . 12 |- ( ( ( ( x e. RR /\ n e. RR ) /\ x < n ) /\ y e. ~H ) -> n e. RR )
14		normcl 26826	. . . . . . . . . . . . 13 |- ( y e. ~H -> ( normh ` y ) e. RR )
15	14	adantl 472	. . . . . . . . . . . 12 |- ( ( ( ( x e. RR /\ n e. RR ) /\ x < n ) /\ y e. ~H ) -> ( normh ` y ) e. RR )
16		normge0 26827	. . . . . . . . . . . . 13 |- ( y e. ~H -> 0 <_ ( normh ` y ) )
17	16	adantl 472	. . . . . . . . . . . 12 |- ( ( ( ( x e. RR /\ n e. RR ) /\ x < n ) /\ y e. ~H ) -> 0 <_ ( normh ` y ) )
18		ltle 9747	. . . . . . . . . . . . . 14 |- ( ( x e. RR /\ n e. RR ) -> ( x < n -> x <_ n ) )
19	18	imp 435	. . . . . . . . . . . . 13 |- ( ( ( x e. RR /\ n e. RR ) /\ x < n ) -> x <_ n )
20	19	adantr 471	. . . . . . . . . . . 12 |- ( ( ( ( x e. RR /\ n e. RR ) /\ x < n ) /\ y e. ~H ) -> x <_ n )
21	12, 13, 15, 17, 20	lemul1ad 10573	. . . . . . . . . . 11 |- ( ( ( ( x e. RR /\ n e. RR ) /\ x < n ) /\ y e. ~H ) -> ( x x. ( normh ` y ) ) <_ ( n x. ( normh ` y ) ) )
22		lncon.4	. . . . . . . . . . . . 13 |- ( y e. ~H -> ( N ` ( T ` y ) ) e. RR )
23	22	adantl 472	. . . . . . . . . . . 12 |- ( ( ( ( x e. RR /\ n e. RR ) /\ x < n ) /\ y e. ~H ) -> ( N ` ( T ` y ) ) e. RR )
24		simpll 765	. . . . . . . . . . . . 13 |- ( ( ( x e. RR /\ n e. RR ) /\ x < n ) -> x e. RR )
25		remulcl 9649	. . . . . . . . . . . . 13 |- ( ( x e. RR /\ ( normh ` y ) e. RR ) -> ( x x. ( normh ` y ) ) e. RR )
26	24, 14, 25	syl2an 484	. . . . . . . . . . . 12 |- ( ( ( ( x e. RR /\ n e. RR ) /\ x < n ) /\ y e. ~H ) -> ( x x. ( normh ` y ) ) e. RR )
27		simplr 767	. . . . . . . . . . . . 13 |- ( ( ( x e. RR /\ n e. RR ) /\ x < n ) -> n e. RR )
28		remulcl 9649	. . . . . . . . . . . . 13 |- ( ( n e. RR /\ ( normh ` y ) e. RR ) -> ( n x. ( normh ` y ) ) e. RR )
29	27, 14, 28	syl2an 484	. . . . . . . . . . . 12 |- ( ( ( ( x e. RR /\ n e. RR ) /\ x < n ) /\ y e. ~H ) -> ( n x. ( normh ` y ) ) e. RR )
30		letr 9752	. . . . . . . . . . . 12 |- ( ( ( N ` ( T ` y ) ) e. RR /\ ( x x. ( normh ` y ) ) e. RR /\ ( n x. ( normh ` y ) ) e. RR ) -> ( ( ( N ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) /\ ( x x. ( normh ` y ) ) <_ ( n x. ( normh ` y ) ) ) -> ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) ) )
31	23, 26, 29, 30	syl3anc 1276	. . . . . . . . . . 11 |- ( ( ( ( x e. RR /\ n e. RR ) /\ x < n ) /\ y e. ~H ) -> ( ( ( N ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) /\ ( x x. ( normh ` y ) ) <_ ( n x. ( normh ` y ) ) ) -> ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) ) )
32	21, 31	mpan2d 685	. . . . . . . . . 10 |- ( ( ( ( x e. RR /\ n e. RR ) /\ x < n ) /\ y e. ~H ) -> ( ( N ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) -> ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) ) )
33	32	ralimdva 2807	. . . . . . . . 9 |- ( ( ( x e. RR /\ n e. RR ) /\ x < n ) -> ( A. y e. ~H ( N ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) -> A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) ) )
34	33	impancom 446	. . . . . . . 8 |- ( ( ( x e. RR /\ n e. RR ) /\ A. y e. ~H ( N ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) ) -> ( x < n -> A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) ) )
35	34	an32s 818	. . . . . . 7 |- ( ( ( x e. RR /\ A. y e. ~H ( N ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) ) /\ n e. RR ) -> ( x < n -> A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) ) )
36	11, 35	sylan2 481	. . . . . 6 |- ( ( ( x e. RR /\ A. y e. ~H ( N ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) ) /\ n e. NN ) -> ( x < n -> A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) ) )
37	36	reximdva 2873	. . . . 5 |- ( ( x e. RR /\ A. y e. ~H ( N ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) ) -> ( E. n e. NN x < n -> E. n e. NN A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) ) )
38	10, 37	mpd 15	. . . 4 |- ( ( x e. RR /\ A. y e. ~H ( N ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) ) -> E. n e. NN A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) )
39	38	rexlimiva 2886	. . 3 |- ( E. x e. RR A. y e. ~H ( N ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) -> E. n e. NN A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) )
40		simprr 771	. . . . . . . 8 |- ( ( ( n e. NN /\ A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) ) /\ ( x e. ~H /\ z e. RR+ ) ) -> z e. RR+ )
41		simpll 765	. . . . . . . . 9 |- ( ( ( n e. NN /\ A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) ) /\ ( x e. ~H /\ z e. RR+ ) ) -> n e. NN )
42	41	nnrpd 11367	. . . . . . . 8 |- ( ( ( n e. NN /\ A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) ) /\ ( x e. ~H /\ z e. RR+ ) ) -> n e. RR+ )
43	40, 42	rpdivcld 11386	. . . . . . 7 |- ( ( ( n e. NN /\ A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) ) /\ ( x e. ~H /\ z e. RR+ ) ) -> ( z / n ) e. RR+ )
44		simprr 771	. . . . . . . . . . . . . 14 |- ( ( n e. NN /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> w e. ~H )
45		simprll 777	. . . . . . . . . . . . . 14 |- ( ( n e. NN /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> x e. ~H )
46		hvsubcl 26718	. . . . . . . . . . . . . 14 |- ( ( w e. ~H /\ x e. ~H ) -> ( w -h x ) e. ~H )
47	44, 45, 46	syl2anc 671	. . . . . . . . . . . . 13 |- ( ( n e. NN /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> ( w -h x ) e. ~H )
48		fveq2 5887	. . . . . . . . . . . . . . . 16 |- ( y = ( w -h x ) -> ( T ` y ) = ( T ` ( w -h x ) ) )
49	48	fveq2d 5891	. . . . . . . . . . . . . . 15 |- ( y = ( w -h x ) -> ( N ` ( T ` y ) ) = ( N ` ( T ` ( w -h x ) ) ) )
50		fveq2 5887	. . . . . . . . . . . . . . . 16 |- ( y = ( w -h x ) -> ( normh ` y ) = ( normh ` ( w -h x ) ) )
51	50	oveq2d 6330	. . . . . . . . . . . . . . 15 |- ( y = ( w -h x ) -> ( n x. ( normh ` y ) ) = ( n x. ( normh ` ( w -h x ) ) ) )
52	49, 51	breq12d 4428	. . . . . . . . . . . . . 14 |- ( y = ( w -h x ) -> ( ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) <-> ( N ` ( T ` ( w -h x ) ) ) <_ ( n x. ( normh ` ( w -h x ) ) ) ) )
53	52	rspcva 3159	. . . . . . . . . . . . 13 |- ( ( ( w -h x ) e. ~H /\ A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) ) -> ( N ` ( T ` ( w -h x ) ) ) <_ ( n x. ( normh ` ( w -h x ) ) ) )
54	47, 53	sylan 478	. . . . . . . . . . . 12 |- ( ( ( n e. NN /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) /\ A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) ) -> ( N ` ( T ` ( w -h x ) ) ) <_ ( n x. ( normh ` ( w -h x ) ) ) )
55	54	an32s 818	. . . . . . . . . . 11 |- ( ( ( n e. NN /\ A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) ) /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> ( N ` ( T ` ( w -h x ) ) ) <_ ( n x. ( normh ` ( w -h x ) ) ) )
56	49	eleq1d 2523	. . . . . . . . . . . . . . 15 |- ( y = ( w -h x ) -> ( ( N ` ( T ` y ) ) e. RR <-> ( N ` ( T ` ( w -h x ) ) ) e. RR ) )
57	56, 22	vtoclga 3124	. . . . . . . . . . . . . 14 |- ( ( w -h x ) e. ~H -> ( N ` ( T ` ( w -h x ) ) ) e. RR )
58	47, 57	syl 17	. . . . . . . . . . . . 13 |- ( ( n e. NN /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> ( N ` ( T ` ( w -h x ) ) ) e. RR )
59	11	adantr 471	. . . . . . . . . . . . . 14 |- ( ( n e. NN /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> n e. RR )
60		normcl 26826	. . . . . . . . . . . . . . 15 |- ( ( w -h x ) e. ~H -> ( normh ` ( w -h x ) ) e. RR )
61	47, 60	syl 17	. . . . . . . . . . . . . 14 |- ( ( n e. NN /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> ( normh ` ( w -h x ) ) e. RR )
62		remulcl 9649	. . . . . . . . . . . . . 14 |- ( ( n e. RR /\ ( normh ` ( w -h x ) ) e. RR ) -> ( n x. ( normh ` ( w -h x ) ) ) e. RR )
63	59, 61, 62	syl2anc 671	. . . . . . . . . . . . 13 |- ( ( n e. NN /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> ( n x. ( normh ` ( w -h x ) ) ) e. RR )
64		simprlr 778	. . . . . . . . . . . . . 14 |- ( ( n e. NN /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> z e. RR+ )
65	64	rpred 11369	. . . . . . . . . . . . 13 |- ( ( n e. NN /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> z e. RR )
66		lelttr 9749	. . . . . . . . . . . . 13 |- ( ( ( N ` ( T ` ( w -h x ) ) ) e. RR /\ ( n x. ( normh ` ( w -h x ) ) ) e. RR /\ z e. RR ) -> ( ( ( N ` ( T ` ( w -h x ) ) ) <_ ( n x. ( normh ` ( w -h x ) ) ) /\ ( n x. ( normh ` ( w -h x ) ) ) < z ) -> ( N ` ( T ` ( w -h x ) ) ) < z ) )
67	58, 63, 65, 66	syl3anc 1276	. . . . . . . . . . . 12 |- ( ( n e. NN /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> ( ( ( N ` ( T ` ( w -h x ) ) ) <_ ( n x. ( normh ` ( w -h x ) ) ) /\ ( n x. ( normh ` ( w -h x ) ) ) < z ) -> ( N ` ( T ` ( w -h x ) ) ) < z ) )
68	67	adantlr 726	. . . . . . . . . . 11 |- ( ( ( n e. NN /\ A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) ) /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> ( ( ( N ` ( T ` ( w -h x ) ) ) <_ ( n x. ( normh ` ( w -h x ) ) ) /\ ( n x. ( normh ` ( w -h x ) ) ) < z ) -> ( N ` ( T ` ( w -h x ) ) ) < z ) )
69	55, 68	mpand 686	. . . . . . . . . 10 |- ( ( ( n e. NN /\ A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) ) /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> ( ( n x. ( normh ` ( w -h x ) ) ) < z -> ( N ` ( T ` ( w -h x ) ) ) < z ) )
70		nnrp 11339	. . . . . . . . . . . . . 14 |- ( n e. NN -> n e. RR+ )
71	70	rpregt0d 11375	. . . . . . . . . . . . 13 |- ( n e. NN -> ( n e. RR /\ 0 < n ) )
72	71	adantr 471	. . . . . . . . . . . 12 |- ( ( n e. NN /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> ( n e. RR /\ 0 < n ) )
73		ltmuldiv2 10506	. . . . . . . . . . . 12 |- ( ( ( normh ` ( w -h x ) ) e. RR /\ z e. RR /\ ( n e. RR /\ 0 < n ) ) -> ( ( n x. ( normh ` ( w -h x ) ) ) < z <-> ( normh ` ( w -h x ) ) < ( z / n ) ) )
74	61, 65, 72, 73	syl3anc 1276	. . . . . . . . . . 11 |- ( ( n e. NN /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> ( ( n x. ( normh ` ( w -h x ) ) ) < z <-> ( normh ` ( w -h x ) ) < ( z / n ) ) )
75	74	adantlr 726	. . . . . . . . . 10 |- ( ( ( n e. NN /\ A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) ) /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> ( ( n x. ( normh ` ( w -h x ) ) ) < z <-> ( normh ` ( w -h x ) ) < ( z / n ) ) )
76		lncon.5	. . . . . . . . . . . . . 14 |- ( ( w e. ~H /\ x e. ~H ) -> ( T ` ( w -h x ) ) = ( ( T ` w ) M ( T ` x ) ) )
77	44, 45, 76	syl2anc 671	. . . . . . . . . . . . 13 |- ( ( n e. NN /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> ( T ` ( w -h x ) ) = ( ( T ` w ) M ( T ` x ) ) )
78	77	adantlr 726	. . . . . . . . . . . 12 |- ( ( ( n e. NN /\ A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) ) /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> ( T ` ( w -h x ) ) = ( ( T ` w ) M ( T ` x ) ) )
79	78	fveq2d 5891	. . . . . . . . . . 11 |- ( ( ( n e. NN /\ A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) ) /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> ( N ` ( T ` ( w -h x ) ) ) = ( N ` ( ( T ` w ) M ( T ` x ) ) ) )
80	79	breq1d 4425	. . . . . . . . . 10 |- ( ( ( n e. NN /\ A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) ) /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> ( ( N ` ( T ` ( w -h x ) ) ) < z <-> ( N ` ( ( T ` w ) M ( T ` x ) ) ) < z ) )
81	69, 75, 80	3imtr3d 275	. . . . . . . . 9 |- ( ( ( n e. NN /\ A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) ) /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> ( ( normh ` ( w -h x ) ) < ( z / n ) -> ( N ` ( ( T ` w ) M ( T ` x ) ) ) < z ) )
82	81	anassrs 658	. . . . . . . 8 |- ( ( ( ( n e. NN /\ A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) ) /\ ( x e. ~H /\ z e. RR+ ) ) /\ w e. ~H ) -> ( ( normh ` ( w -h x ) ) < ( z / n ) -> ( N ` ( ( T ` w ) M ( T ` x ) ) ) < z ) )
83	82	ralrimiva 2813	. . . . . . 7 |- ( ( ( n e. NN /\ A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) ) /\ ( x e. ~H /\ z e. RR+ ) ) -> A. w e. ~H ( ( normh ` ( w -h x ) ) < ( z / n ) -> ( N ` ( ( T ` w ) M ( T ` x ) ) ) < z ) )
84		breq2 4419	. . . . . . . . . 10 |- ( y = ( z / n ) -> ( ( normh ` ( w -h x ) ) < y <-> ( normh ` ( w -h x ) ) < ( z / n ) ) )
85	84	imbi1d 323	. . . . . . . . 9 |- ( y = ( z / n ) -> ( ( ( normh ` ( w -h x ) ) < y -> ( N ` ( ( T ` w ) M ( T ` x ) ) ) < z ) <-> ( ( normh ` ( w -h x ) ) < ( z / n ) -> ( N ` ( ( T ` w ) M ( T ` x ) ) ) < z ) ) )
86	85	ralbidv 2838	. . . . . . . 8 |- ( y = ( z / n ) -> ( A. w e. ~H ( ( normh ` ( w -h x ) ) < y -> ( N ` ( ( T ` w ) M ( T ` x ) ) ) < z ) <-> A. w e. ~H ( ( normh ` ( w -h x ) ) < ( z / n ) -> ( N ` ( ( T ` w ) M ( T ` x ) ) ) < z ) ) )
87	86	rspcev 3161	. . . . . . 7 |- ( ( ( z / n ) e. RR+ /\ A. w e. ~H ( ( normh ` ( w -h x ) ) < ( z / n ) -> ( N ` ( ( T ` w ) M ( T ` x ) ) ) < z ) ) -> E. y e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < y -> ( N ` ( ( T ` w ) M ( T ` x ) ) ) < z ) )
88	43, 83, 87	syl2anc 671	. . . . . 6 |- ( ( ( n e. NN /\ A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) ) /\ ( x e. ~H /\ z e. RR+ ) ) -> E. y e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < y -> ( N ` ( ( T ` w ) M ( T ` x ) ) ) < z ) )
89	88	ralrimivva 2820	. . . . 5 |- ( ( n e. NN /\ A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) ) -> A. x e. ~H A. z e. RR+ E. y e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < y -> ( N ` ( ( T ` w ) M ( T ` x ) ) ) < z ) )
90	89	rexlimiva 2886	. . . 4 |- ( E. n e. NN A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) -> A. x e. ~H A. z e. RR+ E. y e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < y -> ( N ` ( ( T ` w ) M ( T ` x ) ) ) < z ) )
91		lncon.3	. . . 4 |- ( T e. C <-> A. x e. ~H A. z e. RR+ E. y e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < y -> ( N ` ( ( T ` w ) M ( T ` x ) ) ) < z ) )
92	90, 91	sylibr 217	. . 3 |- ( E. n e. NN A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) -> T e. C )
93	39, 92	syl 17	. 2 |- ( E. x e. RR A. y e. ~H ( N ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) -> T e. C )
94	8, 93	impbii 192	1 |- ( T e. C <-> E. x e. RR A. y e. ~H ( N ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   = wceq 1454   e. wcel 1897   A.wral 2748   E.wrex 2749   class class class wbr 4415   ` cfv 5600  (class class class)co 6314   RRcr 9563   0cc0 9564   x. cmul 9569   < clt 9700   <_ cle 9701   / cdiv 10296   NNcn 10636   RR+crp 11330   ~Hchil 26620   normhcno 26624   -h cmv 26626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609  ax-cnex 9620  ax-resscn 9621  ax-1cn 9622  ax-icn 9623  ax-addcl 9624  ax-addrcl 9625  ax-mulcl 9626  ax-mulrcl 9627  ax-mulcom 9628  ax-addass 9629  ax-mulass 9630  ax-distr 9631  ax-i2m1 9632  ax-1ne0 9633  ax-1rid 9634  ax-rnegex 9635  ax-rrecex 9636  ax-cnre 9637  ax-pre-lttri 9638  ax-pre-lttrn 9639  ax-pre-ltadd 9640  ax-pre-mulgt0 9641  ax-pre-sup 9642  ax-hfvadd 26701  ax-hv0cl 26704  ax-hfvmul 26706  ax-hvmul0 26711  ax-hfi 26780  ax-his1 26783  ax-his3 26785  ax-his4 26786

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-nel 2635  df-ral 2753  df-rex 2754  df-reu 2755  df-rmo 2756  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-pss 3431  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-tp 3984  df-op 3986  df-uni 4212  df-iun 4293  df-br 4416  df-opab 4475  df-mpt 4476  df-tr 4511  df-eprel 4763  df-id 4767  df-po 4773  df-so 4774  df-fr 4811  df-we 4813  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-pred 5398  df-ord 5444  df-on 5445  df-lim 5446  df-suc 5447  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-riota 6276  df-ov 6317  df-oprab 6318  df-mpt2 6319  df-om 6719  df-2nd 6820  df-wrecs 7053  df-recs 7115  df-rdg 7153  df-er 7388  df-en 7595  df-dom 7596  df-sdom 7597  df-sup 7981  df-pnf 9702  df-mnf 9703  df-xr 9704  df-ltxr 9705  df-le 9706  df-sub 9887  df-neg 9888  df-div 10297  df-nn 10637  df-2 10695  df-3 10696  df-n0 10898  df-z 10966  df-uz 11188  df-rp 11331  df-seq 12245  df-exp 12304  df-cj 13210  df-re 13211  df-im 13212  df-sqrt 13346  df-hnorm 26669  df-hvsub 26672

This theorem is referenced by:  lnopconi  27735  lnfnconi  27756