Step |
Hyp |
Ref |
Expression |
1 |
|
reflcl |
|- ( A e. RR -> ( |_ ` A ) e. RR ) |
2 |
1
|
adantl |
|- ( ( N e. NN0 /\ A e. RR ) -> ( |_ ` A ) e. RR ) |
3 |
|
simpr |
|- ( ( N e. NN0 /\ A e. RR ) -> A e. RR ) |
4 |
|
simpl |
|- ( ( N e. NN0 /\ A e. RR ) -> N e. NN0 ) |
5 |
4
|
nn0red |
|- ( ( N e. NN0 /\ A e. RR ) -> N e. RR ) |
6 |
4
|
nn0ge0d |
|- ( ( N e. NN0 /\ A e. RR ) -> 0 <_ N ) |
7 |
|
flle |
|- ( A e. RR -> ( |_ ` A ) <_ A ) |
8 |
7
|
adantl |
|- ( ( N e. NN0 /\ A e. RR ) -> ( |_ ` A ) <_ A ) |
9 |
2 3 5 6 8
|
lemul2ad |
|- ( ( N e. NN0 /\ A e. RR ) -> ( N x. ( |_ ` A ) ) <_ ( N x. A ) ) |
10 |
5 3
|
remulcld |
|- ( ( N e. NN0 /\ A e. RR ) -> ( N x. A ) e. RR ) |
11 |
|
nn0z |
|- ( N e. NN0 -> N e. ZZ ) |
12 |
|
flcl |
|- ( A e. RR -> ( |_ ` A ) e. ZZ ) |
13 |
|
zmulcl |
|- ( ( N e. ZZ /\ ( |_ ` A ) e. ZZ ) -> ( N x. ( |_ ` A ) ) e. ZZ ) |
14 |
11 12 13
|
syl2an |
|- ( ( N e. NN0 /\ A e. RR ) -> ( N x. ( |_ ` A ) ) e. ZZ ) |
15 |
|
flge |
|- ( ( ( N x. A ) e. RR /\ ( N x. ( |_ ` A ) ) e. ZZ ) -> ( ( N x. ( |_ ` A ) ) <_ ( N x. A ) <-> ( N x. ( |_ ` A ) ) <_ ( |_ ` ( N x. A ) ) ) ) |
16 |
10 14 15
|
syl2anc |
|- ( ( N e. NN0 /\ A e. RR ) -> ( ( N x. ( |_ ` A ) ) <_ ( N x. A ) <-> ( N x. ( |_ ` A ) ) <_ ( |_ ` ( N x. A ) ) ) ) |
17 |
9 16
|
mpbid |
|- ( ( N e. NN0 /\ A e. RR ) -> ( N x. ( |_ ` A ) ) <_ ( |_ ` ( N x. A ) ) ) |