Step |
Hyp |
Ref |
Expression |
1 |
|
iinhoiicclem.k |
|- F/ k ph |
2 |
|
iinhoiicclem.a |
|- ( ( ph /\ k e. X ) -> A e. RR ) |
3 |
|
iinhoiicclem.b |
|- ( ( ph /\ k e. X ) -> B e. RR ) |
4 |
|
iinhoiicclem.f |
|- ( ph -> F e. |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) ) |
5 |
4
|
elexd |
|- ( ph -> F e. _V ) |
6 |
|
1nn |
|- 1 e. NN |
7 |
6
|
a1i |
|- ( ph -> 1 e. NN ) |
8 |
|
peano2re |
|- ( B e. RR -> ( B + 1 ) e. RR ) |
9 |
3 8
|
syl |
|- ( ( ph /\ k e. X ) -> ( B + 1 ) e. RR ) |
10 |
9
|
rexrd |
|- ( ( ph /\ k e. X ) -> ( B + 1 ) e. RR* ) |
11 |
|
icossre |
|- ( ( A e. RR /\ ( B + 1 ) e. RR* ) -> ( A [,) ( B + 1 ) ) C_ RR ) |
12 |
2 10 11
|
syl2anc |
|- ( ( ph /\ k e. X ) -> ( A [,) ( B + 1 ) ) C_ RR ) |
13 |
1 12
|
ixpssixp |
|- ( ph -> X_ k e. X ( A [,) ( B + 1 ) ) C_ X_ k e. X RR ) |
14 |
|
oveq2 |
|- ( n = 1 -> ( 1 / n ) = ( 1 / 1 ) ) |
15 |
|
1div1e1 |
|- ( 1 / 1 ) = 1 |
16 |
15
|
a1i |
|- ( n = 1 -> ( 1 / 1 ) = 1 ) |
17 |
14 16
|
eqtrd |
|- ( n = 1 -> ( 1 / n ) = 1 ) |
18 |
17
|
oveq2d |
|- ( n = 1 -> ( B + ( 1 / n ) ) = ( B + 1 ) ) |
19 |
18
|
oveq2d |
|- ( n = 1 -> ( A [,) ( B + ( 1 / n ) ) ) = ( A [,) ( B + 1 ) ) ) |
20 |
19
|
ixpeq2dv |
|- ( n = 1 -> X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) = X_ k e. X ( A [,) ( B + 1 ) ) ) |
21 |
20
|
sseq1d |
|- ( n = 1 -> ( X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) C_ X_ k e. X RR <-> X_ k e. X ( A [,) ( B + 1 ) ) C_ X_ k e. X RR ) ) |
22 |
21
|
rspcev |
|- ( ( 1 e. NN /\ X_ k e. X ( A [,) ( B + 1 ) ) C_ X_ k e. X RR ) -> E. n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) C_ X_ k e. X RR ) |
23 |
7 13 22
|
syl2anc |
|- ( ph -> E. n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) C_ X_ k e. X RR ) |
24 |
|
iinss |
|- ( E. n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) C_ X_ k e. X RR -> |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) C_ X_ k e. X RR ) |
25 |
23 24
|
syl |
|- ( ph -> |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) C_ X_ k e. X RR ) |
26 |
25 4
|
sseldd |
|- ( ph -> F e. X_ k e. X RR ) |
27 |
|
elixpconstg |
|- ( F e. |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) -> ( F e. X_ k e. X RR <-> F : X --> RR ) ) |
28 |
4 27
|
syl |
|- ( ph -> ( F e. X_ k e. X RR <-> F : X --> RR ) ) |
29 |
26 28
|
mpbid |
|- ( ph -> F : X --> RR ) |
30 |
29
|
ffnd |
|- ( ph -> F Fn X ) |
31 |
29
|
ffvelrnda |
|- ( ( ph /\ k e. X ) -> ( F ` k ) e. RR ) |
32 |
2
|
rexrd |
|- ( ( ph /\ k e. X ) -> A e. RR* ) |
33 |
|
ssid |
|- X_ k e. X ( A [,) ( B + 1 ) ) C_ X_ k e. X ( A [,) ( B + 1 ) ) |
34 |
33
|
a1i |
|- ( ph -> X_ k e. X ( A [,) ( B + 1 ) ) C_ X_ k e. X ( A [,) ( B + 1 ) ) ) |
35 |
20
|
sseq1d |
|- ( n = 1 -> ( X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) C_ X_ k e. X ( A [,) ( B + 1 ) ) <-> X_ k e. X ( A [,) ( B + 1 ) ) C_ X_ k e. X ( A [,) ( B + 1 ) ) ) ) |
36 |
35
|
rspcev |
|- ( ( 1 e. NN /\ X_ k e. X ( A [,) ( B + 1 ) ) C_ X_ k e. X ( A [,) ( B + 1 ) ) ) -> E. n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) C_ X_ k e. X ( A [,) ( B + 1 ) ) ) |
37 |
7 34 36
|
syl2anc |
|- ( ph -> E. n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) C_ X_ k e. X ( A [,) ( B + 1 ) ) ) |
38 |
|
iinss |
|- ( E. n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) C_ X_ k e. X ( A [,) ( B + 1 ) ) -> |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) C_ X_ k e. X ( A [,) ( B + 1 ) ) ) |
39 |
37 38
|
syl |
|- ( ph -> |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) C_ X_ k e. X ( A [,) ( B + 1 ) ) ) |
40 |
39 4
|
sseldd |
|- ( ph -> F e. X_ k e. X ( A [,) ( B + 1 ) ) ) |
41 |
40
|
adantr |
|- ( ( ph /\ k e. X ) -> F e. X_ k e. X ( A [,) ( B + 1 ) ) ) |
42 |
|
simpr |
|- ( ( ph /\ k e. X ) -> k e. X ) |
43 |
|
fvixp2 |
|- ( ( F e. X_ k e. X ( A [,) ( B + 1 ) ) /\ k e. X ) -> ( F ` k ) e. ( A [,) ( B + 1 ) ) ) |
44 |
41 42 43
|
syl2anc |
|- ( ( ph /\ k e. X ) -> ( F ` k ) e. ( A [,) ( B + 1 ) ) ) |
45 |
|
icogelb |
|- ( ( A e. RR* /\ ( B + 1 ) e. RR* /\ ( F ` k ) e. ( A [,) ( B + 1 ) ) ) -> A <_ ( F ` k ) ) |
46 |
32 10 44 45
|
syl3anc |
|- ( ( ph /\ k e. X ) -> A <_ ( F ` k ) ) |
47 |
31
|
adantr |
|- ( ( ( ph /\ k e. X ) /\ n e. NN ) -> ( F ` k ) e. RR ) |
48 |
3
|
adantr |
|- ( ( ( ph /\ k e. X ) /\ n e. NN ) -> B e. RR ) |
49 |
|
nnrecre |
|- ( n e. NN -> ( 1 / n ) e. RR ) |
50 |
49
|
adantl |
|- ( ( ( ph /\ k e. X ) /\ n e. NN ) -> ( 1 / n ) e. RR ) |
51 |
48 50
|
readdcld |
|- ( ( ( ph /\ k e. X ) /\ n e. NN ) -> ( B + ( 1 / n ) ) e. RR ) |
52 |
32
|
adantr |
|- ( ( ( ph /\ k e. X ) /\ n e. NN ) -> A e. RR* ) |
53 |
|
ressxr |
|- RR C_ RR* |
54 |
53 51
|
sselid |
|- ( ( ( ph /\ k e. X ) /\ n e. NN ) -> ( B + ( 1 / n ) ) e. RR* ) |
55 |
|
eliin |
|- ( F e. _V -> ( F e. |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) <-> A. n e. NN F e. X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) ) ) |
56 |
5 55
|
syl |
|- ( ph -> ( F e. |^|_ n e. NN X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) <-> A. n e. NN F e. X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) ) ) |
57 |
4 56
|
mpbid |
|- ( ph -> A. n e. NN F e. X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) ) |
58 |
57
|
r19.21bi |
|- ( ( ph /\ n e. NN ) -> F e. X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) ) |
59 |
|
elixp2 |
|- ( F e. X_ k e. X ( A [,) ( B + ( 1 / n ) ) ) <-> ( F e. _V /\ F Fn X /\ A. k e. X ( F ` k ) e. ( A [,) ( B + ( 1 / n ) ) ) ) ) |
60 |
58 59
|
sylib |
|- ( ( ph /\ n e. NN ) -> ( F e. _V /\ F Fn X /\ A. k e. X ( F ` k ) e. ( A [,) ( B + ( 1 / n ) ) ) ) ) |
61 |
60
|
simp3d |
|- ( ( ph /\ n e. NN ) -> A. k e. X ( F ` k ) e. ( A [,) ( B + ( 1 / n ) ) ) ) |
62 |
61
|
r19.21bi |
|- ( ( ( ph /\ n e. NN ) /\ k e. X ) -> ( F ` k ) e. ( A [,) ( B + ( 1 / n ) ) ) ) |
63 |
62
|
an32s |
|- ( ( ( ph /\ k e. X ) /\ n e. NN ) -> ( F ` k ) e. ( A [,) ( B + ( 1 / n ) ) ) ) |
64 |
|
icoltub |
|- ( ( A e. RR* /\ ( B + ( 1 / n ) ) e. RR* /\ ( F ` k ) e. ( A [,) ( B + ( 1 / n ) ) ) ) -> ( F ` k ) < ( B + ( 1 / n ) ) ) |
65 |
52 54 63 64
|
syl3anc |
|- ( ( ( ph /\ k e. X ) /\ n e. NN ) -> ( F ` k ) < ( B + ( 1 / n ) ) ) |
66 |
47 51 65
|
ltled |
|- ( ( ( ph /\ k e. X ) /\ n e. NN ) -> ( F ` k ) <_ ( B + ( 1 / n ) ) ) |
67 |
66
|
ralrimiva |
|- ( ( ph /\ k e. X ) -> A. n e. NN ( F ` k ) <_ ( B + ( 1 / n ) ) ) |
68 |
|
nfv |
|- F/ n ( ph /\ k e. X ) |
69 |
53 31
|
sselid |
|- ( ( ph /\ k e. X ) -> ( F ` k ) e. RR* ) |
70 |
68 69 3
|
xrralrecnnle |
|- ( ( ph /\ k e. X ) -> ( ( F ` k ) <_ B <-> A. n e. NN ( F ` k ) <_ ( B + ( 1 / n ) ) ) ) |
71 |
67 70
|
mpbird |
|- ( ( ph /\ k e. X ) -> ( F ` k ) <_ B ) |
72 |
2 3 31 46 71
|
eliccd |
|- ( ( ph /\ k e. X ) -> ( F ` k ) e. ( A [,] B ) ) |
73 |
72
|
ex |
|- ( ph -> ( k e. X -> ( F ` k ) e. ( A [,] B ) ) ) |
74 |
1 73
|
ralrimi |
|- ( ph -> A. k e. X ( F ` k ) e. ( A [,] B ) ) |
75 |
5 30 74
|
3jca |
|- ( ph -> ( F e. _V /\ F Fn X /\ A. k e. X ( F ` k ) e. ( A [,] B ) ) ) |
76 |
|
elixp2 |
|- ( F e. X_ k e. X ( A [,] B ) <-> ( F e. _V /\ F Fn X /\ A. k e. X ( F ` k ) e. ( A [,] B ) ) ) |
77 |
75 76
|
sylibr |
|- ( ph -> F e. X_ k e. X ( A [,] B ) ) |