Metamath Proof Explorer

Theorem fzonmapblen

Description: The result of subtracting a nonnegative integer from a positive integer and adding another nonnegative integer which is less than the first one is less than the positive integer. (Contributed by Alexander van der Vekens, 19-May-2018)

Ref Expression
Assertion fzonmapblen 
|- ( ( A e. ( 0 ..^ N ) /\ B e. ( 0 ..^ N ) /\ B < A ) -> ( B + ( N - A ) ) < N )

Proof

Step Hyp Ref Expression
1 elfzo0 
 |-  ( A e. ( 0 ..^ N ) <-> ( A e. NN0 /\ N e. NN /\ A < N ) )
2 nn0re 
 |-  ( A e. NN0 -> A e. RR )
3 nnre 
 |-  ( N e. NN -> N e. RR )
4 2 3 anim12i 
 |-  ( ( A e. NN0 /\ N e. NN ) -> ( A e. RR /\ N e. RR ) )
5 4 3adant3 
 |-  ( ( A e. NN0 /\ N e. NN /\ A < N ) -> ( A e. RR /\ N e. RR ) )
6 1 5 sylbi 
 |-  ( A e. ( 0 ..^ N ) -> ( A e. RR /\ N e. RR ) )
7 elfzoelz 
 |-  ( B e. ( 0 ..^ N ) -> B e. ZZ )
8 7 zred 
 |-  ( B e. ( 0 ..^ N ) -> B e. RR )
9 simpr 
 |-  ( ( ( A e. RR /\ N e. RR ) /\ B e. RR ) -> B e. RR )
10 simpll 
 |-  ( ( ( A e. RR /\ N e. RR ) /\ B e. RR ) -> A e. RR )
11 resubcl 
 |-  ( ( N e. RR /\ A e. RR ) -> ( N - A ) e. RR )
12 11 ancoms 
 |-  ( ( A e. RR /\ N e. RR ) -> ( N - A ) e. RR )
13 12 adantr 
 |-  ( ( ( A e. RR /\ N e. RR ) /\ B e. RR ) -> ( N - A ) e. RR )
14 9 10 13 ltadd1d 
 |-  ( ( ( A e. RR /\ N e. RR ) /\ B e. RR ) -> ( B < A <-> ( B + ( N - A ) ) < ( A + ( N - A ) ) ) )
15 14 biimpa 
 |-  ( ( ( ( A e. RR /\ N e. RR ) /\ B e. RR ) /\ B < A ) -> ( B + ( N - A ) ) < ( A + ( N - A ) ) )
16 recn 
 |-  ( A e. RR -> A e. CC )
17 recn 
 |-  ( N e. RR -> N e. CC )
18 16 17 anim12i 
 |-  ( ( A e. RR /\ N e. RR ) -> ( A e. CC /\ N e. CC ) )
19 18 adantr 
 |-  ( ( ( A e. RR /\ N e. RR ) /\ B e. RR ) -> ( A e. CC /\ N e. CC ) )
20 19 adantr 
 |-  ( ( ( ( A e. RR /\ N e. RR ) /\ B e. RR ) /\ B < A ) -> ( A e. CC /\ N e. CC ) )
21 pncan3 
 |-  ( ( A e. CC /\ N e. CC ) -> ( A + ( N - A ) ) = N )
22 20 21 syl 
 |-  ( ( ( ( A e. RR /\ N e. RR ) /\ B e. RR ) /\ B < A ) -> ( A + ( N - A ) ) = N )
23 15 22 breqtrd 
 |-  ( ( ( ( A e. RR /\ N e. RR ) /\ B e. RR ) /\ B < A ) -> ( B + ( N - A ) ) < N )
24 23 ex 
 |-  ( ( ( A e. RR /\ N e. RR ) /\ B e. RR ) -> ( B < A -> ( B + ( N - A ) ) < N ) )
25 6 8 24 syl2an 
 |-  ( ( A e. ( 0 ..^ N ) /\ B e. ( 0 ..^ N ) ) -> ( B < A -> ( B + ( N - A ) ) < N ) )
26 25 3impia 
 |-  ( ( A e. ( 0 ..^ N ) /\ B e. ( 0 ..^ N ) /\ B < A ) -> ( B + ( N - A ) ) < N )