Metamath Proof Explorer

Theorem lnconi

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

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

Proof

Step Hyp Ref Expression
1 lncon.1 
 |-  ( T e. C -> S e. RR )
2 lncon.2 
 |-  ( ( T e. C /\ y e. ~H ) -> ( N ` ( T ` y ) ) <_ ( S x. ( normh ` y ) ) )
3 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 ) )
4 lncon.4 
 |-  ( y e. ~H -> ( N ` ( T ` y ) ) e. RR )
5 lncon.5 
 |-  ( ( w e. ~H /\ x e. ~H ) -> ( T ` ( w -h x ) ) = ( ( T ` w ) M ( T ` x ) ) )
6 2 ralrimiva 
 |-  ( T e. C -> A. y e. ~H ( N ` ( T ` y ) ) <_ ( S x. ( normh ` y ) ) )
7 oveq1 
 |-  ( x = S -> ( x x. ( normh ` y ) ) = ( S x. ( normh ` y ) ) )
8 7 breq2d 
 |-  ( x = S -> ( ( N ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) <-> ( N ` ( T ` y ) ) <_ ( S x. ( normh ` y ) ) ) )
9 8 ralbidv 
 |-  ( x = S -> ( A. y e. ~H ( N ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) <-> A. y e. ~H ( N ` ( T ` y ) ) <_ ( S x. ( normh ` y ) ) ) )
10 9 rspcev 
 |-  ( ( 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 ) ) )
11 1 6 10 syl2anc 
 |-  ( T e. C -> E. x e. RR A. y e. ~H ( N ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) )
12 arch 
 |-  ( x e. RR -> E. n e. NN x < n )
13 12 adantr 
 |-  ( ( x e. RR /\ A. y e. ~H ( N ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) ) -> E. n e. NN x < n )
14 nnre 
 |-  ( n e. NN -> n e. RR )
15 simplll 
 |-  ( ( ( ( x e. RR /\ n e. RR ) /\ x < n ) /\ y e. ~H ) -> x e. RR )
16 simpllr 
 |-  ( ( ( ( x e. RR /\ n e. RR ) /\ x < n ) /\ y e. ~H ) -> n e. RR )
17 normcl 
 |-  ( y e. ~H -> ( normh ` y ) e. RR )
18 17 adantl 
 |-  ( ( ( ( x e. RR /\ n e. RR ) /\ x < n ) /\ y e. ~H ) -> ( normh ` y ) e. RR )
19 normge0 
 |-  ( y e. ~H -> 0 <_ ( normh ` y ) )
20 19 adantl 
 |-  ( ( ( ( x e. RR /\ n e. RR ) /\ x < n ) /\ y e. ~H ) -> 0 <_ ( normh ` y ) )
21 ltle 
 |-  ( ( x e. RR /\ n e. RR ) -> ( x < n -> x <_ n ) )
22 21 imp 
 |-  ( ( ( x e. RR /\ n e. RR ) /\ x < n ) -> x <_ n )
23 22 adantr 
 |-  ( ( ( ( x e. RR /\ n e. RR ) /\ x < n ) /\ y e. ~H ) -> x <_ n )
24 15 16 18 20 23 lemul1ad 
 |-  ( ( ( ( x e. RR /\ n e. RR ) /\ x < n ) /\ y e. ~H ) -> ( x x. ( normh ` y ) ) <_ ( n x. ( normh ` y ) ) )
25 4 adantl 
 |-  ( ( ( ( x e. RR /\ n e. RR ) /\ x < n ) /\ y e. ~H ) -> ( N ` ( T ` y ) ) e. RR )
26 simpll 
 |-  ( ( ( x e. RR /\ n e. RR ) /\ x < n ) -> x e. RR )
27 remulcl 
 |-  ( ( x e. RR /\ ( normh ` y ) e. RR ) -> ( x x. ( normh ` y ) ) e. RR )
28 26 17 27 syl2an 
 |-  ( ( ( ( x e. RR /\ n e. RR ) /\ x < n ) /\ y e. ~H ) -> ( x x. ( normh ` y ) ) e. RR )
29 simplr 
 |-  ( ( ( x e. RR /\ n e. RR ) /\ x < n ) -> n e. RR )
30 remulcl 
 |-  ( ( n e. RR /\ ( normh ` y ) e. RR ) -> ( n x. ( normh ` y ) ) e. RR )
31 29 17 30 syl2an 
 |-  ( ( ( ( x e. RR /\ n e. RR ) /\ x < n ) /\ y e. ~H ) -> ( n x. ( normh ` y ) ) e. RR )
32 letr 
 |-  ( ( ( 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 ) ) ) )
33 25 28 31 32 syl3anc 
 |-  ( ( ( ( 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 ) ) ) )
34 24 33 mpan2d 
 |-  ( ( ( ( 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 ) ) ) )
35 34 ralimdva 
 |-  ( ( ( 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 ) ) ) )
36 35 impancom 
 |-  ( ( ( 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 ) ) ) )
37 36 an32s 
 |-  ( ( ( 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 ) ) ) )
38 14 37 sylan2 
 |-  ( ( ( 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 ) ) ) )
39 38 reximdva 
 |-  ( ( 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 ) ) ) )
40 13 39 mpd 
 |-  ( ( 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 ) ) )
41 40 rexlimiva 
 |-  ( 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 ) ) )
42 simprr 
 |-  ( ( ( n e. NN /\ A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) ) /\ ( x e. ~H /\ z e. RR+ ) ) -> z e. RR+ )
43 simpll 
 |-  ( ( ( n e. NN /\ A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) ) /\ ( x e. ~H /\ z e. RR+ ) ) -> n e. NN )
44 43 nnrpd 
 |-  ( ( ( n e. NN /\ A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) ) /\ ( x e. ~H /\ z e. RR+ ) ) -> n e. RR+ )
45 42 44 rpdivcld 
 |-  ( ( ( n e. NN /\ A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) ) /\ ( x e. ~H /\ z e. RR+ ) ) -> ( z / n ) e. RR+ )
46 simprr 
 |-  ( ( n e. NN /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> w e. ~H )
47 simprll 
 |-  ( ( n e. NN /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> x e. ~H )
48 hvsubcl 
 |-  ( ( w e. ~H /\ x e. ~H ) -> ( w -h x ) e. ~H )
49 46 47 48 syl2anc 
 |-  ( ( n e. NN /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> ( w -h x ) e. ~H )
50 2fveq3 
 |-  ( y = ( w -h x ) -> ( N ` ( T ` y ) ) = ( N ` ( T ` ( w -h x ) ) ) )
51 fveq2 
 |-  ( y = ( w -h x ) -> ( normh ` y ) = ( normh ` ( w -h x ) ) )
52 51 oveq2d 
 |-  ( y = ( w -h x ) -> ( n x. ( normh ` y ) ) = ( n x. ( normh ` ( w -h x ) ) ) )
53 50 52 breq12d 
 |-  ( y = ( w -h x ) -> ( ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) <-> ( N ` ( T ` ( w -h x ) ) ) <_ ( n x. ( normh ` ( w -h x ) ) ) ) )
54 53 rspcva 
 |-  ( ( ( 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 ) ) ) )
55 49 54 sylan 
 |-  ( ( ( 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 ) ) ) )
56 55 an32s 
 |-  ( ( ( 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 ) ) ) )
57 50 eleq1d 
 |-  ( y = ( w -h x ) -> ( ( N ` ( T ` y ) ) e. RR <-> ( N ` ( T ` ( w -h x ) ) ) e. RR ) )
58 57 4 vtoclga 
 |-  ( ( w -h x ) e. ~H -> ( N ` ( T ` ( w -h x ) ) ) e. RR )
59 49 58 syl 
 |-  ( ( n e. NN /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> ( N ` ( T ` ( w -h x ) ) ) e. RR )
60 14 adantr 
 |-  ( ( n e. NN /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> n e. RR )
61 normcl 
 |-  ( ( w -h x ) e. ~H -> ( normh ` ( w -h x ) ) e. RR )
62 49 61 syl 
 |-  ( ( n e. NN /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> ( normh ` ( w -h x ) ) e. RR )
63 remulcl 
 |-  ( ( n e. RR /\ ( normh ` ( w -h x ) ) e. RR ) -> ( n x. ( normh ` ( w -h x ) ) ) e. RR )
64 60 62 63 syl2anc 
 |-  ( ( n e. NN /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> ( n x. ( normh ` ( w -h x ) ) ) e. RR )
65 simprlr 
 |-  ( ( n e. NN /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> z e. RR+ )
66 65 rpred 
 |-  ( ( n e. NN /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> z e. RR )
67 lelttr 
 |-  ( ( ( 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 ) )
68 59 64 66 67 syl3anc 
 |-  ( ( 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 ) )
69 68 adantlr 
 |-  ( ( ( 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 ) )
70 56 69 mpand 
 |-  ( ( ( 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 ) )
71 nnrp 
 |-  ( n e. NN -> n e. RR+ )
72 71 rpregt0d 
 |-  ( n e. NN -> ( n e. RR /\ 0 < n ) )
73 72 adantr 
 |-  ( ( n e. NN /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> ( n e. RR /\ 0 < n ) )
74 ltmuldiv2 
 |-  ( ( ( 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 ) ) )
75 62 66 73 74 syl3anc 
 |-  ( ( 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 ) ) )
76 75 adantlr 
 |-  ( ( ( 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 ) ) )
77 46 47 5 syl2anc 
 |-  ( ( n e. NN /\ ( ( x e. ~H /\ z e. RR+ ) /\ w e. ~H ) ) -> ( T ` ( w -h x ) ) = ( ( T ` w ) M ( T ` x ) ) )
78 77 adantlr 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( 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 70 76 80 3imtr3d 
 |-  ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( y = ( z / n ) -> ( ( normh ` ( w -h x ) ) < y <-> ( normh ` ( w -h x ) ) < ( z / n ) ) )
85 84 rspceaimv 
 |-  ( ( ( 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 ) )
86 45 83 85 syl2anc 
 |-  ( ( ( 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 ) )
87 86 ralrimivva 
 |-  ( ( 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 ) )
88 87 rexlimiva 
 |-  ( 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 ) )
89 88 3 sylibr 
 |-  ( E. n e. NN A. y e. ~H ( N ` ( T ` y ) ) <_ ( n x. ( normh ` y ) ) -> T e. C )
90 41 89 syl 
 |-  ( E. x e. RR A. y e. ~H ( N ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) -> T e. C )
91 11 90 impbii 
 |-  ( T e. C <-> E. x e. RR A. y e. ~H ( N ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) )