Step |
Hyp |
Ref |
Expression |
1 |
|
rpreccl |
|- ( A e. RR+ -> ( 1 / A ) e. RR+ ) |
2 |
1
|
rpred |
|- ( A e. RR+ -> ( 1 / A ) e. RR ) |
3 |
1
|
rpge0d |
|- ( A e. RR+ -> 0 <_ ( 1 / A ) ) |
4 |
|
flge0nn0 |
|- ( ( ( 1 / A ) e. RR /\ 0 <_ ( 1 / A ) ) -> ( |_ ` ( 1 / A ) ) e. NN0 ) |
5 |
2 3 4
|
syl2anc |
|- ( A e. RR+ -> ( |_ ` ( 1 / A ) ) e. NN0 ) |
6 |
|
nn0p1nn |
|- ( ( |_ ` ( 1 / A ) ) e. NN0 -> ( ( |_ ` ( 1 / A ) ) + 1 ) e. NN ) |
7 |
5 6
|
syl |
|- ( A e. RR+ -> ( ( |_ ` ( 1 / A ) ) + 1 ) e. NN ) |
8 |
|
flltp1 |
|- ( ( 1 / A ) e. RR -> ( 1 / A ) < ( ( |_ ` ( 1 / A ) ) + 1 ) ) |
9 |
2 8
|
syl |
|- ( A e. RR+ -> ( 1 / A ) < ( ( |_ ` ( 1 / A ) ) + 1 ) ) |
10 |
7
|
nnrpd |
|- ( A e. RR+ -> ( ( |_ ` ( 1 / A ) ) + 1 ) e. RR+ ) |
11 |
1 10
|
ltrecd |
|- ( A e. RR+ -> ( ( 1 / A ) < ( ( |_ ` ( 1 / A ) ) + 1 ) <-> ( 1 / ( ( |_ ` ( 1 / A ) ) + 1 ) ) < ( 1 / ( 1 / A ) ) ) ) |
12 |
9 11
|
mpbid |
|- ( A e. RR+ -> ( 1 / ( ( |_ ` ( 1 / A ) ) + 1 ) ) < ( 1 / ( 1 / A ) ) ) |
13 |
|
rpcn |
|- ( A e. RR+ -> A e. CC ) |
14 |
|
rpne0 |
|- ( A e. RR+ -> A =/= 0 ) |
15 |
13 14
|
recrecd |
|- ( A e. RR+ -> ( 1 / ( 1 / A ) ) = A ) |
16 |
12 15
|
breqtrd |
|- ( A e. RR+ -> ( 1 / ( ( |_ ` ( 1 / A ) ) + 1 ) ) < A ) |
17 |
|
oveq2 |
|- ( n = ( ( |_ ` ( 1 / A ) ) + 1 ) -> ( 1 / n ) = ( 1 / ( ( |_ ` ( 1 / A ) ) + 1 ) ) ) |
18 |
17
|
breq1d |
|- ( n = ( ( |_ ` ( 1 / A ) ) + 1 ) -> ( ( 1 / n ) < A <-> ( 1 / ( ( |_ ` ( 1 / A ) ) + 1 ) ) < A ) ) |
19 |
18
|
rspcev |
|- ( ( ( ( |_ ` ( 1 / A ) ) + 1 ) e. NN /\ ( 1 / ( ( |_ ` ( 1 / A ) ) + 1 ) ) < A ) -> E. n e. NN ( 1 / n ) < A ) |
20 |
7 16 19
|
syl2anc |
|- ( A e. RR+ -> E. n e. NN ( 1 / n ) < A ) |