This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rpnnen1lem5

Description: Lemma for rpnnen1 . (Contributed by Mario Carneiro, 12-May-2013) (Revised by NM, 13-Aug-2021) (Proof modification is discouraged.)

Ref Expression
Hypotheses rpnnen1lem.1 
|- T = { n e. ZZ | ( n / k ) < x }
rpnnen1lem.2 
|- F = ( x e. RR |-> ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) )
rpnnen1lem.n 
|- NN e. _V
rpnnen1lem.q 
|- QQ e. _V
Assertion rpnnen1lem5 
|- ( x e. RR -> sup ( ran ( F ` x ) , RR , < ) = x )

Proof

Step Hyp Ref Expression
1 rpnnen1lem.1 
 |-  T = { n e. ZZ | ( n / k ) < x }
2 rpnnen1lem.2 
 |-  F = ( x e. RR |-> ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) )
3 rpnnen1lem.n 
 |-  NN e. _V
4 rpnnen1lem.q 
 |-  QQ e. _V
5 1 2 3 4 rpnnen1lem3 
 |-  ( x e. RR -> A. n e. ran ( F ` x ) n <_ x )
6 1 2 3 4 rpnnen1lem1 
 |-  ( x e. RR -> ( F ` x ) e. ( QQ ^m NN ) )
7 4 3 elmap 
 |-  ( ( F ` x ) e. ( QQ ^m NN ) <-> ( F ` x ) : NN --> QQ )
8 6 7 sylib 
 |-  ( x e. RR -> ( F ` x ) : NN --> QQ )
9 frn 
 |-  ( ( F ` x ) : NN --> QQ -> ran ( F ` x ) C_ QQ )
10 qssre 
 |-  QQ C_ RR
11 9 10 sstrdi 
 |-  ( ( F ` x ) : NN --> QQ -> ran ( F ` x ) C_ RR )
12 8 11 syl 
 |-  ( x e. RR -> ran ( F ` x ) C_ RR )
13 1nn 
 |-  1 e. NN
14 13 ne0ii 
 |-  NN =/= (/)
15 fdm 
 |-  ( ( F ` x ) : NN --> QQ -> dom ( F ` x ) = NN )
16 15 neeq1d 
 |-  ( ( F ` x ) : NN --> QQ -> ( dom ( F ` x ) =/= (/) <-> NN =/= (/) ) )
17 14 16 mpbiri 
 |-  ( ( F ` x ) : NN --> QQ -> dom ( F ` x ) =/= (/) )
18 dm0rn0 
 |-  ( dom ( F ` x ) = (/) <-> ran ( F ` x ) = (/) )
19 18 necon3bii 
 |-  ( dom ( F ` x ) =/= (/) <-> ran ( F ` x ) =/= (/) )
20 17 19 sylib 
 |-  ( ( F ` x ) : NN --> QQ -> ran ( F ` x ) =/= (/) )
21 8 20 syl 
 |-  ( x e. RR -> ran ( F ` x ) =/= (/) )
22 breq2 
 |-  ( y = x -> ( n <_ y <-> n <_ x ) )
23 22 ralbidv 
 |-  ( y = x -> ( A. n e. ran ( F ` x ) n <_ y <-> A. n e. ran ( F ` x ) n <_ x ) )
24 23 rspcev 
 |-  ( ( x e. RR /\ A. n e. ran ( F ` x ) n <_ x ) -> E. y e. RR A. n e. ran ( F ` x ) n <_ y )
25 5 24 mpdan 
 |-  ( x e. RR -> E. y e. RR A. n e. ran ( F ` x ) n <_ y )
26 id 
 |-  ( x e. RR -> x e. RR )
27 suprleub 
 |-  ( ( ( ran ( F ` x ) C_ RR /\ ran ( F ` x ) =/= (/) /\ E. y e. RR A. n e. ran ( F ` x ) n <_ y ) /\ x e. RR ) -> ( sup ( ran ( F ` x ) , RR , < ) <_ x <-> A. n e. ran ( F ` x ) n <_ x ) )
28 12 21 25 26 27 syl31anc 
 |-  ( x e. RR -> ( sup ( ran ( F ` x ) , RR , < ) <_ x <-> A. n e. ran ( F ` x ) n <_ x ) )
29 5 28 mpbird 
 |-  ( x e. RR -> sup ( ran ( F ` x ) , RR , < ) <_ x )
30 1 2 3 4 rpnnen1lem4 
 |-  ( x e. RR -> sup ( ran ( F ` x ) , RR , < ) e. RR )
31 resubcl 
 |-  ( ( x e. RR /\ sup ( ran ( F ` x ) , RR , < ) e. RR ) -> ( x - sup ( ran ( F ` x ) , RR , < ) ) e. RR )
32 30 31 mpdan 
 |-  ( x e. RR -> ( x - sup ( ran ( F ` x ) , RR , < ) ) e. RR )
33 32 adantr 
 |-  ( ( x e. RR /\ sup ( ran ( F ` x ) , RR , < ) < x ) -> ( x - sup ( ran ( F ` x ) , RR , < ) ) e. RR )
34 posdif 
 |-  ( ( sup ( ran ( F ` x ) , RR , < ) e. RR /\ x e. RR ) -> ( sup ( ran ( F ` x ) , RR , < ) < x <-> 0 < ( x - sup ( ran ( F ` x ) , RR , < ) ) ) )
35 30 34 mpancom 
 |-  ( x e. RR -> ( sup ( ran ( F ` x ) , RR , < ) < x <-> 0 < ( x - sup ( ran ( F ` x ) , RR , < ) ) ) )
36 35 biimpa 
 |-  ( ( x e. RR /\ sup ( ran ( F ` x ) , RR , < ) < x ) -> 0 < ( x - sup ( ran ( F ` x ) , RR , < ) ) )
37 36 gt0ne0d 
 |-  ( ( x e. RR /\ sup ( ran ( F ` x ) , RR , < ) < x ) -> ( x - sup ( ran ( F ` x ) , RR , < ) ) =/= 0 )
38 33 37 rereccld 
 |-  ( ( x e. RR /\ sup ( ran ( F ` x ) , RR , < ) < x ) -> ( 1 / ( x - sup ( ran ( F ` x ) , RR , < ) ) ) e. RR )
39 arch 
 |-  ( ( 1 / ( x - sup ( ran ( F ` x ) , RR , < ) ) ) e. RR -> E. k e. NN ( 1 / ( x - sup ( ran ( F ` x ) , RR , < ) ) ) < k )
40 38 39 syl 
 |-  ( ( x e. RR /\ sup ( ran ( F ` x ) , RR , < ) < x ) -> E. k e. NN ( 1 / ( x - sup ( ran ( F ` x ) , RR , < ) ) ) < k )
41 40 ex 
 |-  ( x e. RR -> ( sup ( ran ( F ` x ) , RR , < ) < x -> E. k e. NN ( 1 / ( x - sup ( ran ( F ` x ) , RR , < ) ) ) < k ) )
42 1 2 rpnnen1lem2 
 |-  ( ( x e. RR /\ k e. NN ) -> sup ( T , RR , < ) e. ZZ )
43 42 zred 
 |-  ( ( x e. RR /\ k e. NN ) -> sup ( T , RR , < ) e. RR )
44 43 3adant3 
 |-  ( ( x e. RR /\ k e. NN /\ ( 1 / ( x - sup ( ran ( F ` x ) , RR , < ) ) ) < k ) -> sup ( T , RR , < ) e. RR )
45 44 ltp1d 
 |-  ( ( x e. RR /\ k e. NN /\ ( 1 / ( x - sup ( ran ( F ` x ) , RR , < ) ) ) < k ) -> sup ( T , RR , < ) < ( sup ( T , RR , < ) + 1 ) )
46 33 36 jca 
 |-  ( ( x e. RR /\ sup ( ran ( F ` x ) , RR , < ) < x ) -> ( ( x - sup ( ran ( F ` x ) , RR , < ) ) e. RR /\ 0 < ( x - sup ( ran ( F ` x ) , RR , < ) ) ) )
47 nnre 
 |-  ( k e. NN -> k e. RR )
48 nngt0 
 |-  ( k e. NN -> 0 < k )
49 47 48 jca 
 |-  ( k e. NN -> ( k e. RR /\ 0 < k ) )
50 ltrec1 
 |-  ( ( ( ( x - sup ( ran ( F ` x ) , RR , < ) ) e. RR /\ 0 < ( x - sup ( ran ( F ` x ) , RR , < ) ) ) /\ ( k e. RR /\ 0 < k ) ) -> ( ( 1 / ( x - sup ( ran ( F ` x ) , RR , < ) ) ) < k <-> ( 1 / k ) < ( x - sup ( ran ( F ` x ) , RR , < ) ) ) )
51 46 49 50 syl2an 
 |-  ( ( ( x e. RR /\ sup ( ran ( F ` x ) , RR , < ) < x ) /\ k e. NN ) -> ( ( 1 / ( x - sup ( ran ( F ` x ) , RR , < ) ) ) < k <-> ( 1 / k ) < ( x - sup ( ran ( F ` x ) , RR , < ) ) ) )
52 30 ad2antrr 
 |-  ( ( ( x e. RR /\ sup ( ran ( F ` x ) , RR , < ) < x ) /\ k e. NN ) -> sup ( ran ( F ` x ) , RR , < ) e. RR )
53 nnrecre 
 |-  ( k e. NN -> ( 1 / k ) e. RR )
54 53 adantl 
 |-  ( ( ( x e. RR /\ sup ( ran ( F ` x ) , RR , < ) < x ) /\ k e. NN ) -> ( 1 / k ) e. RR )
55 simpll 
 |-  ( ( ( x e. RR /\ sup ( ran ( F ` x ) , RR , < ) < x ) /\ k e. NN ) -> x e. RR )
56 52 54 55 ltaddsub2d 
 |-  ( ( ( x e. RR /\ sup ( ran ( F ` x ) , RR , < ) < x ) /\ k e. NN ) -> ( ( sup ( ran ( F ` x ) , RR , < ) + ( 1 / k ) ) < x <-> ( 1 / k ) < ( x - sup ( ran ( F ` x ) , RR , < ) ) ) )
57 12 adantr 
 |-  ( ( x e. RR /\ k e. NN ) -> ran ( F ` x ) C_ RR )
58 ffn 
 |-  ( ( F ` x ) : NN --> QQ -> ( F ` x ) Fn NN )
59 8 58 syl 
 |-  ( x e. RR -> ( F ` x ) Fn NN )
60 fnfvelrn 
 |-  ( ( ( F ` x ) Fn NN /\ k e. NN ) -> ( ( F ` x ) ` k ) e. ran ( F ` x ) )
61 59 60 sylan 
 |-  ( ( x e. RR /\ k e. NN ) -> ( ( F ` x ) ` k ) e. ran ( F ` x ) )
62 57 61 sseldd 
 |-  ( ( x e. RR /\ k e. NN ) -> ( ( F ` x ) ` k ) e. RR )
63 30 adantr 
 |-  ( ( x e. RR /\ k e. NN ) -> sup ( ran ( F ` x ) , RR , < ) e. RR )
64 53 adantl 
 |-  ( ( x e. RR /\ k e. NN ) -> ( 1 / k ) e. RR )
65 12 21 25 3jca 
 |-  ( x e. RR -> ( ran ( F ` x ) C_ RR /\ ran ( F ` x ) =/= (/) /\ E. y e. RR A. n e. ran ( F ` x ) n <_ y ) )
66 65 adantr 
 |-  ( ( x e. RR /\ k e. NN ) -> ( ran ( F ` x ) C_ RR /\ ran ( F ` x ) =/= (/) /\ E. y e. RR A. n e. ran ( F ` x ) n <_ y ) )
67 suprub 
 |-  ( ( ( ran ( F ` x ) C_ RR /\ ran ( F ` x ) =/= (/) /\ E. y e. RR A. n e. ran ( F ` x ) n <_ y ) /\ ( ( F ` x ) ` k ) e. ran ( F ` x ) ) -> ( ( F ` x ) ` k ) <_ sup ( ran ( F ` x ) , RR , < ) )
68 66 61 67 syl2anc 
 |-  ( ( x e. RR /\ k e. NN ) -> ( ( F ` x ) ` k ) <_ sup ( ran ( F ` x ) , RR , < ) )
69 62 63 64 68 leadd1dd 
 |-  ( ( x e. RR /\ k e. NN ) -> ( ( ( F ` x ) ` k ) + ( 1 / k ) ) <_ ( sup ( ran ( F ` x ) , RR , < ) + ( 1 / k ) ) )
70 62 64 readdcld 
 |-  ( ( x e. RR /\ k e. NN ) -> ( ( ( F ` x ) ` k ) + ( 1 / k ) ) e. RR )
71 readdcl 
 |-  ( ( sup ( ran ( F ` x ) , RR , < ) e. RR /\ ( 1 / k ) e. RR ) -> ( sup ( ran ( F ` x ) , RR , < ) + ( 1 / k ) ) e. RR )
72 30 53 71 syl2an 
 |-  ( ( x e. RR /\ k e. NN ) -> ( sup ( ran ( F ` x ) , RR , < ) + ( 1 / k ) ) e. RR )
73 simpl 
 |-  ( ( x e. RR /\ k e. NN ) -> x e. RR )
74 lelttr 
 |-  ( ( ( ( ( F ` x ) ` k ) + ( 1 / k ) ) e. RR /\ ( sup ( ran ( F ` x ) , RR , < ) + ( 1 / k ) ) e. RR /\ x e. RR ) -> ( ( ( ( ( F ` x ) ` k ) + ( 1 / k ) ) <_ ( sup ( ran ( F ` x ) , RR , < ) + ( 1 / k ) ) /\ ( sup ( ran ( F ` x ) , RR , < ) + ( 1 / k ) ) < x ) -> ( ( ( F ` x ) ` k ) + ( 1 / k ) ) < x ) )
75 74 expd 
 |-  ( ( ( ( ( F ` x ) ` k ) + ( 1 / k ) ) e. RR /\ ( sup ( ran ( F ` x ) , RR , < ) + ( 1 / k ) ) e. RR /\ x e. RR ) -> ( ( ( ( F ` x ) ` k ) + ( 1 / k ) ) <_ ( sup ( ran ( F ` x ) , RR , < ) + ( 1 / k ) ) -> ( ( sup ( ran ( F ` x ) , RR , < ) + ( 1 / k ) ) < x -> ( ( ( F ` x ) ` k ) + ( 1 / k ) ) < x ) ) )
76 70 72 73 75 syl3anc 
 |-  ( ( x e. RR /\ k e. NN ) -> ( ( ( ( F ` x ) ` k ) + ( 1 / k ) ) <_ ( sup ( ran ( F ` x ) , RR , < ) + ( 1 / k ) ) -> ( ( sup ( ran ( F ` x ) , RR , < ) + ( 1 / k ) ) < x -> ( ( ( F ` x ) ` k ) + ( 1 / k ) ) < x ) ) )
77 69 76 mpd 
 |-  ( ( x e. RR /\ k e. NN ) -> ( ( sup ( ran ( F ` x ) , RR , < ) + ( 1 / k ) ) < x -> ( ( ( F ` x ) ` k ) + ( 1 / k ) ) < x ) )
78 77 adantlr 
 |-  ( ( ( x e. RR /\ sup ( ran ( F ` x ) , RR , < ) < x ) /\ k e. NN ) -> ( ( sup ( ran ( F ` x ) , RR , < ) + ( 1 / k ) ) < x -> ( ( ( F ` x ) ` k ) + ( 1 / k ) ) < x ) )
79 56 78 sylbird 
 |-  ( ( ( x e. RR /\ sup ( ran ( F ` x ) , RR , < ) < x ) /\ k e. NN ) -> ( ( 1 / k ) < ( x - sup ( ran ( F ` x ) , RR , < ) ) -> ( ( ( F ` x ) ` k ) + ( 1 / k ) ) < x ) )
80 51 79 sylbid 
 |-  ( ( ( x e. RR /\ sup ( ran ( F ` x ) , RR , < ) < x ) /\ k e. NN ) -> ( ( 1 / ( x - sup ( ran ( F ` x ) , RR , < ) ) ) < k -> ( ( ( F ` x ) ` k ) + ( 1 / k ) ) < x ) )
81 42 peano2zd 
 |-  ( ( x e. RR /\ k e. NN ) -> ( sup ( T , RR , < ) + 1 ) e. ZZ )
82 oveq1 
 |-  ( n = ( sup ( T , RR , < ) + 1 ) -> ( n / k ) = ( ( sup ( T , RR , < ) + 1 ) / k ) )
83 82 breq1d 
 |-  ( n = ( sup ( T , RR , < ) + 1 ) -> ( ( n / k ) < x <-> ( ( sup ( T , RR , < ) + 1 ) / k ) < x ) )
84 83 1 elrab2 
 |-  ( ( sup ( T , RR , < ) + 1 ) e. T <-> ( ( sup ( T , RR , < ) + 1 ) e. ZZ /\ ( ( sup ( T , RR , < ) + 1 ) / k ) < x ) )
85 84 biimpri 
 |-  ( ( ( sup ( T , RR , < ) + 1 ) e. ZZ /\ ( ( sup ( T , RR , < ) + 1 ) / k ) < x ) -> ( sup ( T , RR , < ) + 1 ) e. T )
86 81 85 sylan 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ ( ( sup ( T , RR , < ) + 1 ) / k ) < x ) -> ( sup ( T , RR , < ) + 1 ) e. T )
87 ssrab2 
 |-  { n e. ZZ | ( n / k ) < x } C_ ZZ
88 1 87 eqsstri 
 |-  T C_ ZZ
89 zssre 
 |-  ZZ C_ RR
90 88 89 sstri 
 |-  T C_ RR
91 90 a1i 
 |-  ( ( x e. RR /\ k e. NN ) -> T C_ RR )
92 remulcl 
 |-  ( ( k e. RR /\ x e. RR ) -> ( k x. x ) e. RR )
93 92 ancoms 
 |-  ( ( x e. RR /\ k e. RR ) -> ( k x. x ) e. RR )
94 47 93 sylan2 
 |-  ( ( x e. RR /\ k e. NN ) -> ( k x. x ) e. RR )
95 btwnz 
 |-  ( ( k x. x ) e. RR -> ( E. n e. ZZ n < ( k x. x ) /\ E. n e. ZZ ( k x. x ) < n ) )
96 95 simpld 
 |-  ( ( k x. x ) e. RR -> E. n e. ZZ n < ( k x. x ) )
97 94 96 syl 
 |-  ( ( x e. RR /\ k e. NN ) -> E. n e. ZZ n < ( k x. x ) )
98 zre 
 |-  ( n e. ZZ -> n e. RR )
99 98 adantl 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> n e. RR )
100 simpll 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> x e. RR )
101 49 ad2antlr 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> ( k e. RR /\ 0 < k ) )
102 ltdivmul 
 |-  ( ( n e. RR /\ x e. RR /\ ( k e. RR /\ 0 < k ) ) -> ( ( n / k ) < x <-> n < ( k x. x ) ) )
103 99 100 101 102 syl3anc 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> ( ( n / k ) < x <-> n < ( k x. x ) ) )
104 103 rexbidva 
 |-  ( ( x e. RR /\ k e. NN ) -> ( E. n e. ZZ ( n / k ) < x <-> E. n e. ZZ n < ( k x. x ) ) )
105 97 104 mpbird 
 |-  ( ( x e. RR /\ k e. NN ) -> E. n e. ZZ ( n / k ) < x )
106 rabn0 
 |-  ( { n e. ZZ | ( n / k ) < x } =/= (/) <-> E. n e. ZZ ( n / k ) < x )
107 105 106 sylibr 
 |-  ( ( x e. RR /\ k e. NN ) -> { n e. ZZ | ( n / k ) < x } =/= (/) )
108 1 neeq1i 
 |-  ( T =/= (/) <-> { n e. ZZ | ( n / k ) < x } =/= (/) )
109 107 108 sylibr 
 |-  ( ( x e. RR /\ k e. NN ) -> T =/= (/) )
110 1 reqabi 
 |-  ( n e. T <-> ( n e. ZZ /\ ( n / k ) < x ) )
111 47 ad2antlr 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> k e. RR )
112 111 100 92 syl2anc 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> ( k x. x ) e. RR )
113 ltle 
 |-  ( ( n e. RR /\ ( k x. x ) e. RR ) -> ( n < ( k x. x ) -> n <_ ( k x. x ) ) )
114 99 112 113 syl2anc 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> ( n < ( k x. x ) -> n <_ ( k x. x ) ) )
115 103 114 sylbid 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. ZZ ) -> ( ( n / k ) < x -> n <_ ( k x. x ) ) )
116 115 impr 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ ( n e. ZZ /\ ( n / k ) < x ) ) -> n <_ ( k x. x ) )
117 110 116 sylan2b 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ n e. T ) -> n <_ ( k x. x ) )
118 117 ralrimiva 
 |-  ( ( x e. RR /\ k e. NN ) -> A. n e. T n <_ ( k x. x ) )
119 breq2 
 |-  ( y = ( k x. x ) -> ( n <_ y <-> n <_ ( k x. x ) ) )
120 119 ralbidv 
 |-  ( y = ( k x. x ) -> ( A. n e. T n <_ y <-> A. n e. T n <_ ( k x. x ) ) )
121 120 rspcev 
 |-  ( ( ( k x. x ) e. RR /\ A. n e. T n <_ ( k x. x ) ) -> E. y e. RR A. n e. T n <_ y )
122 94 118 121 syl2anc 
 |-  ( ( x e. RR /\ k e. NN ) -> E. y e. RR A. n e. T n <_ y )
123 91 109 122 3jca 
 |-  ( ( x e. RR /\ k e. NN ) -> ( T C_ RR /\ T =/= (/) /\ E. y e. RR A. n e. T n <_ y ) )
124 suprub 
 |-  ( ( ( T C_ RR /\ T =/= (/) /\ E. y e. RR A. n e. T n <_ y ) /\ ( sup ( T , RR , < ) + 1 ) e. T ) -> ( sup ( T , RR , < ) + 1 ) <_ sup ( T , RR , < ) )
125 123 124 sylan 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ ( sup ( T , RR , < ) + 1 ) e. T ) -> ( sup ( T , RR , < ) + 1 ) <_ sup ( T , RR , < ) )
126 86 125 syldan 
 |-  ( ( ( x e. RR /\ k e. NN ) /\ ( ( sup ( T , RR , < ) + 1 ) / k ) < x ) -> ( sup ( T , RR , < ) + 1 ) <_ sup ( T , RR , < ) )
127 126 ex 
 |-  ( ( x e. RR /\ k e. NN ) -> ( ( ( sup ( T , RR , < ) + 1 ) / k ) < x -> ( sup ( T , RR , < ) + 1 ) <_ sup ( T , RR , < ) ) )
128 42 zcnd 
 |-  ( ( x e. RR /\ k e. NN ) -> sup ( T , RR , < ) e. CC )
129 1cnd 
 |-  ( ( x e. RR /\ k e. NN ) -> 1 e. CC )
130 nncn 
 |-  ( k e. NN -> k e. CC )
131 nnne0 
 |-  ( k e. NN -> k =/= 0 )
132 130 131 jca 
 |-  ( k e. NN -> ( k e. CC /\ k =/= 0 ) )
133 132 adantl 
 |-  ( ( x e. RR /\ k e. NN ) -> ( k e. CC /\ k =/= 0 ) )
134 divdir 
 |-  ( ( sup ( T , RR , < ) e. CC /\ 1 e. CC /\ ( k e. CC /\ k =/= 0 ) ) -> ( ( sup ( T , RR , < ) + 1 ) / k ) = ( ( sup ( T , RR , < ) / k ) + ( 1 / k ) ) )
135 128 129 133 134 syl3anc 
 |-  ( ( x e. RR /\ k e. NN ) -> ( ( sup ( T , RR , < ) + 1 ) / k ) = ( ( sup ( T , RR , < ) / k ) + ( 1 / k ) ) )
136 3 mptex 
 |-  ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) e. _V
137 2 fvmpt2 
 |-  ( ( x e. RR /\ ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) e. _V ) -> ( F ` x ) = ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) )
138 136 137 mpan2 
 |-  ( x e. RR -> ( F ` x ) = ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) )
139 138 fveq1d 
 |-  ( x e. RR -> ( ( F ` x ) ` k ) = ( ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) ` k ) )
140 ovex 
 |-  ( sup ( T , RR , < ) / k ) e. _V
141 eqid 
 |-  ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) = ( k e. NN |-> ( sup ( T , RR , < ) / k ) )
142 141 fvmpt2 
 |-  ( ( k e. NN /\ ( sup ( T , RR , < ) / k ) e. _V ) -> ( ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) ` k ) = ( sup ( T , RR , < ) / k ) )
143 140 142 mpan2 
 |-  ( k e. NN -> ( ( k e. NN |-> ( sup ( T , RR , < ) / k ) ) ` k ) = ( sup ( T , RR , < ) / k ) )
144 139 143 sylan9eq 
 |-  ( ( x e. RR /\ k e. NN ) -> ( ( F ` x ) ` k ) = ( sup ( T , RR , < ) / k ) )
145 144 oveq1d 
 |-  ( ( x e. RR /\ k e. NN ) -> ( ( ( F ` x ) ` k ) + ( 1 / k ) ) = ( ( sup ( T , RR , < ) / k ) + ( 1 / k ) ) )
146 135 145 eqtr4d 
 |-  ( ( x e. RR /\ k e. NN ) -> ( ( sup ( T , RR , < ) + 1 ) / k ) = ( ( ( F ` x ) ` k ) + ( 1 / k ) ) )
147 146 breq1d 
 |-  ( ( x e. RR /\ k e. NN ) -> ( ( ( sup ( T , RR , < ) + 1 ) / k ) < x <-> ( ( ( F ` x ) ` k ) + ( 1 / k ) ) < x ) )
148 81 zred 
 |-  ( ( x e. RR /\ k e. NN ) -> ( sup ( T , RR , < ) + 1 ) e. RR )
149 148 43 lenltd 
 |-  ( ( x e. RR /\ k e. NN ) -> ( ( sup ( T , RR , < ) + 1 ) <_ sup ( T , RR , < ) <-> -. sup ( T , RR , < ) < ( sup ( T , RR , < ) + 1 ) ) )
150 127 147 149 3imtr3d 
 |-  ( ( x e. RR /\ k e. NN ) -> ( ( ( ( F ` x ) ` k ) + ( 1 / k ) ) < x -> -. sup ( T , RR , < ) < ( sup ( T , RR , < ) + 1 ) ) )
151 150 adantlr 
 |-  ( ( ( x e. RR /\ sup ( ran ( F ` x ) , RR , < ) < x ) /\ k e. NN ) -> ( ( ( ( F ` x ) ` k ) + ( 1 / k ) ) < x -> -. sup ( T , RR , < ) < ( sup ( T , RR , < ) + 1 ) ) )
152 80 151 syld 
 |-  ( ( ( x e. RR /\ sup ( ran ( F ` x ) , RR , < ) < x ) /\ k e. NN ) -> ( ( 1 / ( x - sup ( ran ( F ` x ) , RR , < ) ) ) < k -> -. sup ( T , RR , < ) < ( sup ( T , RR , < ) + 1 ) ) )
153 152 exp31 
 |-  ( x e. RR -> ( sup ( ran ( F ` x ) , RR , < ) < x -> ( k e. NN -> ( ( 1 / ( x - sup ( ran ( F ` x ) , RR , < ) ) ) < k -> -. sup ( T , RR , < ) < ( sup ( T , RR , < ) + 1 ) ) ) ) )
154 153 com4l 
 |-  ( sup ( ran ( F ` x ) , RR , < ) < x -> ( k e. NN -> ( ( 1 / ( x - sup ( ran ( F ` x ) , RR , < ) ) ) < k -> ( x e. RR -> -. sup ( T , RR , < ) < ( sup ( T , RR , < ) + 1 ) ) ) ) )
155 154 com14 
 |-  ( x e. RR -> ( k e. NN -> ( ( 1 / ( x - sup ( ran ( F ` x ) , RR , < ) ) ) < k -> ( sup ( ran ( F ` x ) , RR , < ) < x -> -. sup ( T , RR , < ) < ( sup ( T , RR , < ) + 1 ) ) ) ) )
156 155 3imp 
 |-  ( ( x e. RR /\ k e. NN /\ ( 1 / ( x - sup ( ran ( F ` x ) , RR , < ) ) ) < k ) -> ( sup ( ran ( F ` x ) , RR , < ) < x -> -. sup ( T , RR , < ) < ( sup ( T , RR , < ) + 1 ) ) )
157 45 156 mt2d 
 |-  ( ( x e. RR /\ k e. NN /\ ( 1 / ( x - sup ( ran ( F ` x ) , RR , < ) ) ) < k ) -> -. sup ( ran ( F ` x ) , RR , < ) < x )
158 157 rexlimdv3a 
 |-  ( x e. RR -> ( E. k e. NN ( 1 / ( x - sup ( ran ( F ` x ) , RR , < ) ) ) < k -> -. sup ( ran ( F ` x ) , RR , < ) < x ) )
159 41 158 syld 
 |-  ( x e. RR -> ( sup ( ran ( F ` x ) , RR , < ) < x -> -. sup ( ran ( F ` x ) , RR , < ) < x ) )
160 159 pm2.01d 
 |-  ( x e. RR -> -. sup ( ran ( F ` x ) , RR , < ) < x )
161 eqlelt 
 |-  ( ( sup ( ran ( F ` x ) , RR , < ) e. RR /\ x e. RR ) -> ( sup ( ran ( F ` x ) , RR , < ) = x <-> ( sup ( ran ( F ` x ) , RR , < ) <_ x /\ -. sup ( ran ( F ` x ) , RR , < ) < x ) ) )
162 30 161 mpancom 
 |-  ( x e. RR -> ( sup ( ran ( F ` x ) , RR , < ) = x <-> ( sup ( ran ( F ` x ) , RR , < ) <_ x /\ -. sup ( ran ( F ` x ) , RR , < ) < x ) ) )
163 29 160 162 mpbir2and 
 |-  ( x e. RR -> sup ( ran ( F ` x ) , RR , < ) = x )