Step |
Hyp |
Ref |
Expression |
1 |
|
reflcl |
|- ( A e. RR -> ( |_ ` A ) e. RR ) |
2 |
1
|
adantr |
|- ( ( A e. RR /\ N e. ZZ ) -> ( |_ ` A ) e. RR ) |
3 |
|
simpl |
|- ( ( A e. RR /\ N e. ZZ ) -> A e. RR ) |
4 |
|
simpr |
|- ( ( A e. RR /\ N e. ZZ ) -> N e. ZZ ) |
5 |
4
|
zred |
|- ( ( A e. RR /\ N e. ZZ ) -> N e. RR ) |
6 |
|
flle |
|- ( A e. RR -> ( |_ ` A ) <_ A ) |
7 |
6
|
adantr |
|- ( ( A e. RR /\ N e. ZZ ) -> ( |_ ` A ) <_ A ) |
8 |
2 3 5 7
|
leadd1dd |
|- ( ( A e. RR /\ N e. ZZ ) -> ( ( |_ ` A ) + N ) <_ ( A + N ) ) |
9 |
|
1red |
|- ( ( A e. RR /\ N e. ZZ ) -> 1 e. RR ) |
10 |
2 9
|
readdcld |
|- ( ( A e. RR /\ N e. ZZ ) -> ( ( |_ ` A ) + 1 ) e. RR ) |
11 |
|
flltp1 |
|- ( A e. RR -> A < ( ( |_ ` A ) + 1 ) ) |
12 |
11
|
adantr |
|- ( ( A e. RR /\ N e. ZZ ) -> A < ( ( |_ ` A ) + 1 ) ) |
13 |
3 10 5 12
|
ltadd1dd |
|- ( ( A e. RR /\ N e. ZZ ) -> ( A + N ) < ( ( ( |_ ` A ) + 1 ) + N ) ) |
14 |
2
|
recnd |
|- ( ( A e. RR /\ N e. ZZ ) -> ( |_ ` A ) e. CC ) |
15 |
|
1cnd |
|- ( ( A e. RR /\ N e. ZZ ) -> 1 e. CC ) |
16 |
5
|
recnd |
|- ( ( A e. RR /\ N e. ZZ ) -> N e. CC ) |
17 |
14 15 16
|
add32d |
|- ( ( A e. RR /\ N e. ZZ ) -> ( ( ( |_ ` A ) + 1 ) + N ) = ( ( ( |_ ` A ) + N ) + 1 ) ) |
18 |
13 17
|
breqtrd |
|- ( ( A e. RR /\ N e. ZZ ) -> ( A + N ) < ( ( ( |_ ` A ) + N ) + 1 ) ) |
19 |
3 5
|
readdcld |
|- ( ( A e. RR /\ N e. ZZ ) -> ( A + N ) e. RR ) |
20 |
3
|
flcld |
|- ( ( A e. RR /\ N e. ZZ ) -> ( |_ ` A ) e. ZZ ) |
21 |
20 4
|
zaddcld |
|- ( ( A e. RR /\ N e. ZZ ) -> ( ( |_ ` A ) + N ) e. ZZ ) |
22 |
|
flbi |
|- ( ( ( A + N ) e. RR /\ ( ( |_ ` A ) + N ) e. ZZ ) -> ( ( |_ ` ( A + N ) ) = ( ( |_ ` A ) + N ) <-> ( ( ( |_ ` A ) + N ) <_ ( A + N ) /\ ( A + N ) < ( ( ( |_ ` A ) + N ) + 1 ) ) ) ) |
23 |
19 21 22
|
syl2anc |
|- ( ( A e. RR /\ N e. ZZ ) -> ( ( |_ ` ( A + N ) ) = ( ( |_ ` A ) + N ) <-> ( ( ( |_ ` A ) + N ) <_ ( A + N ) /\ ( A + N ) < ( ( ( |_ ` A ) + N ) + 1 ) ) ) ) |
24 |
8 18 23
|
mpbir2and |
|- ( ( A e. RR /\ N e. ZZ ) -> ( |_ ` ( A + N ) ) = ( ( |_ ` A ) + N ) ) |