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