Metamath Proof Explorer


Theorem fladdz

Description: An integer can be moved in and out of the floor of a sum. (Contributed by NM, 27-Apr-2005) (Proof shortened by Fan Zheng, 16-Jun-2016)

Ref Expression
Assertion fladdz
|- ( ( A e. RR /\ N e. ZZ ) -> ( |_ ` ( A + N ) ) = ( ( |_ ` A ) + N ) )

Proof

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 ) )