Metamath Proof Explorer

Theorem subsubelfzo0

Description: Subtracting a difference from a number which is not less than the difference results in a bounded nonnegative integer. (Contributed by Alexander van der Vekens, 21-May-2018)

Ref Expression
Assertion subsubelfzo0 
|- ( ( A e. ( 0 ..^ N ) /\ I e. ( 0 ..^ N ) /\ -. I < ( N - A ) ) -> ( I - ( N - A ) ) e. ( 0 ..^ A ) )

Proof

Step Hyp Ref Expression
1 elfzo0 
 |-  ( A e. ( 0 ..^ N ) <-> ( A e. NN0 /\ N e. NN /\ A < N ) )
2 elfzo0 
 |-  ( I e. ( 0 ..^ N ) <-> ( I e. NN0 /\ N e. NN /\ I < N ) )
3 nnre 
 |-  ( N e. NN -> N e. RR )
4 3 3ad2ant2 
 |-  ( ( I e. NN0 /\ N e. NN /\ I < N ) -> N e. RR )
5 nn0re 
 |-  ( A e. NN0 -> A e. RR )
6 5 adantr 
 |-  ( ( A e. NN0 /\ A < N ) -> A e. RR )
7 resubcl 
 |-  ( ( N e. RR /\ A e. RR ) -> ( N - A ) e. RR )
8 4 6 7 syl2anr 
 |-  ( ( ( A e. NN0 /\ A < N ) /\ ( I e. NN0 /\ N e. NN /\ I < N ) ) -> ( N - A ) e. RR )
9 nn0re 
 |-  ( I e. NN0 -> I e. RR )
10 9 3ad2ant1 
 |-  ( ( I e. NN0 /\ N e. NN /\ I < N ) -> I e. RR )
11 10 adantl 
 |-  ( ( ( A e. NN0 /\ A < N ) /\ ( I e. NN0 /\ N e. NN /\ I < N ) ) -> I e. RR )
12 lenlt 
 |-  ( ( ( N - A ) e. RR /\ I e. RR ) -> ( ( N - A ) <_ I <-> -. I < ( N - A ) ) )
13 12 bicomd 
 |-  ( ( ( N - A ) e. RR /\ I e. RR ) -> ( -. I < ( N - A ) <-> ( N - A ) <_ I ) )
14 8 11 13 syl2anc 
 |-  ( ( ( A e. NN0 /\ A < N ) /\ ( I e. NN0 /\ N e. NN /\ I < N ) ) -> ( -. I < ( N - A ) <-> ( N - A ) <_ I ) )
15 14 biimpa 
 |-  ( ( ( ( A e. NN0 /\ A < N ) /\ ( I e. NN0 /\ N e. NN /\ I < N ) ) /\ -. I < ( N - A ) ) -> ( N - A ) <_ I )
16 nnz 
 |-  ( N e. NN -> N e. ZZ )
17 16 3ad2ant2 
 |-  ( ( I e. NN0 /\ N e. NN /\ I < N ) -> N e. ZZ )
18 nn0z 
 |-  ( A e. NN0 -> A e. ZZ )
19 18 adantr 
 |-  ( ( A e. NN0 /\ A < N ) -> A e. ZZ )
20 zsubcl 
 |-  ( ( N e. ZZ /\ A e. ZZ ) -> ( N - A ) e. ZZ )
21 17 19 20 syl2anr 
 |-  ( ( ( A e. NN0 /\ A < N ) /\ ( I e. NN0 /\ N e. NN /\ I < N ) ) -> ( N - A ) e. ZZ )
22 ltle 
 |-  ( ( A e. RR /\ N e. RR ) -> ( A < N -> A <_ N ) )
23 5 4 22 syl2an 
 |-  ( ( A e. NN0 /\ ( I e. NN0 /\ N e. NN /\ I < N ) ) -> ( A < N -> A <_ N ) )
24 23 impancom 
 |-  ( ( A e. NN0 /\ A < N ) -> ( ( I e. NN0 /\ N e. NN /\ I < N ) -> A <_ N ) )
25 24 imp 
 |-  ( ( ( A e. NN0 /\ A < N ) /\ ( I e. NN0 /\ N e. NN /\ I < N ) ) -> A <_ N )
26 subge0 
 |-  ( ( N e. RR /\ A e. RR ) -> ( 0 <_ ( N - A ) <-> A <_ N ) )
27 4 6 26 syl2anr 
 |-  ( ( ( A e. NN0 /\ A < N ) /\ ( I e. NN0 /\ N e. NN /\ I < N ) ) -> ( 0 <_ ( N - A ) <-> A <_ N ) )
28 25 27 mpbird 
 |-  ( ( ( A e. NN0 /\ A < N ) /\ ( I e. NN0 /\ N e. NN /\ I < N ) ) -> 0 <_ ( N - A ) )
29 elnn0z 
 |-  ( ( N - A ) e. NN0 <-> ( ( N - A ) e. ZZ /\ 0 <_ ( N - A ) ) )
30 21 28 29 sylanbrc 
 |-  ( ( ( A e. NN0 /\ A < N ) /\ ( I e. NN0 /\ N e. NN /\ I < N ) ) -> ( N - A ) e. NN0 )
31 30 adantr 
 |-  ( ( ( ( A e. NN0 /\ A < N ) /\ ( I e. NN0 /\ N e. NN /\ I < N ) ) /\ -. I < ( N - A ) ) -> ( N - A ) e. NN0 )
32 simplr1 
 |-  ( ( ( ( A e. NN0 /\ A < N ) /\ ( I e. NN0 /\ N e. NN /\ I < N ) ) /\ -. I < ( N - A ) ) -> I e. NN0 )
33 nn0sub 
 |-  ( ( ( N - A ) e. NN0 /\ I e. NN0 ) -> ( ( N - A ) <_ I <-> ( I - ( N - A ) ) e. NN0 ) )
34 31 32 33 syl2anc 
 |-  ( ( ( ( A e. NN0 /\ A < N ) /\ ( I e. NN0 /\ N e. NN /\ I < N ) ) /\ -. I < ( N - A ) ) -> ( ( N - A ) <_ I <-> ( I - ( N - A ) ) e. NN0 ) )
35 15 34 mpbid 
 |-  ( ( ( ( A e. NN0 /\ A < N ) /\ ( I e. NN0 /\ N e. NN /\ I < N ) ) /\ -. I < ( N - A ) ) -> ( I - ( N - A ) ) e. NN0 )
36 elnn0uz 
 |-  ( ( I - ( N - A ) ) e. NN0 <-> ( I - ( N - A ) ) e. ( ZZ>= ` 0 ) )
37 35 36 sylib 
 |-  ( ( ( ( A e. NN0 /\ A < N ) /\ ( I e. NN0 /\ N e. NN /\ I < N ) ) /\ -. I < ( N - A ) ) -> ( I - ( N - A ) ) e. ( ZZ>= ` 0 ) )
38 19 adantr 
 |-  ( ( ( A e. NN0 /\ A < N ) /\ ( I e. NN0 /\ N e. NN /\ I < N ) ) -> A e. ZZ )
39 38 adantr 
 |-  ( ( ( ( A e. NN0 /\ A < N ) /\ ( I e. NN0 /\ N e. NN /\ I < N ) ) /\ -. I < ( N - A ) ) -> A e. ZZ )
40 9 adantr 
 |-  ( ( I e. NN0 /\ N e. NN ) -> I e. RR )
41 40 adantl 
 |-  ( ( A e. NN0 /\ ( I e. NN0 /\ N e. NN ) ) -> I e. RR )
42 3 adantl 
 |-  ( ( I e. NN0 /\ N e. NN ) -> N e. RR )
43 42 adantl 
 |-  ( ( A e. NN0 /\ ( I e. NN0 /\ N e. NN ) ) -> N e. RR )
44 42 5 7 syl2anr 
 |-  ( ( A e. NN0 /\ ( I e. NN0 /\ N e. NN ) ) -> ( N - A ) e. RR )
45 41 43 44 ltsub1d 
 |-  ( ( A e. NN0 /\ ( I e. NN0 /\ N e. NN ) ) -> ( I < N <-> ( I - ( N - A ) ) < ( N - ( N - A ) ) ) )
46 nncn 
 |-  ( N e. NN -> N e. CC )
47 46 adantl 
 |-  ( ( I e. NN0 /\ N e. NN ) -> N e. CC )
48 nn0cn 
 |-  ( A e. NN0 -> A e. CC )
49 nncan 
 |-  ( ( N e. CC /\ A e. CC ) -> ( N - ( N - A ) ) = A )
50 47 48 49 syl2anr 
 |-  ( ( A e. NN0 /\ ( I e. NN0 /\ N e. NN ) ) -> ( N - ( N - A ) ) = A )
51 50 breq2d 
 |-  ( ( A e. NN0 /\ ( I e. NN0 /\ N e. NN ) ) -> ( ( I - ( N - A ) ) < ( N - ( N - A ) ) <-> ( I - ( N - A ) ) < A ) )
52 51 biimpd 
 |-  ( ( A e. NN0 /\ ( I e. NN0 /\ N e. NN ) ) -> ( ( I - ( N - A ) ) < ( N - ( N - A ) ) -> ( I - ( N - A ) ) < A ) )
53 45 52 sylbid 
 |-  ( ( A e. NN0 /\ ( I e. NN0 /\ N e. NN ) ) -> ( I < N -> ( I - ( N - A ) ) < A ) )
54 53 ex 
 |-  ( A e. NN0 -> ( ( I e. NN0 /\ N e. NN ) -> ( I < N -> ( I - ( N - A ) ) < A ) ) )
55 54 adantr 
 |-  ( ( A e. NN0 /\ A < N ) -> ( ( I e. NN0 /\ N e. NN ) -> ( I < N -> ( I - ( N - A ) ) < A ) ) )
56 55 com3l 
 |-  ( ( I e. NN0 /\ N e. NN ) -> ( I < N -> ( ( A e. NN0 /\ A < N ) -> ( I - ( N - A ) ) < A ) ) )
57 56 3impia 
 |-  ( ( I e. NN0 /\ N e. NN /\ I < N ) -> ( ( A e. NN0 /\ A < N ) -> ( I - ( N - A ) ) < A ) )
58 57 impcom 
 |-  ( ( ( A e. NN0 /\ A < N ) /\ ( I e. NN0 /\ N e. NN /\ I < N ) ) -> ( I - ( N - A ) ) < A )
59 58 adantr 
 |-  ( ( ( ( A e. NN0 /\ A < N ) /\ ( I e. NN0 /\ N e. NN /\ I < N ) ) /\ -. I < ( N - A ) ) -> ( I - ( N - A ) ) < A )
60 37 39 59 3jca 
 |-  ( ( ( ( A e. NN0 /\ A < N ) /\ ( I e. NN0 /\ N e. NN /\ I < N ) ) /\ -. I < ( N - A ) ) -> ( ( I - ( N - A ) ) e. ( ZZ>= ` 0 ) /\ A e. ZZ /\ ( I - ( N - A ) ) < A ) )
61 60 exp31 
 |-  ( ( A e. NN0 /\ A < N ) -> ( ( I e. NN0 /\ N e. NN /\ I < N ) -> ( -. I < ( N - A ) -> ( ( I - ( N - A ) ) e. ( ZZ>= ` 0 ) /\ A e. ZZ /\ ( I - ( N - A ) ) < A ) ) ) )
62 2 61 syl5bi 
 |-  ( ( A e. NN0 /\ A < N ) -> ( I e. ( 0 ..^ N ) -> ( -. I < ( N - A ) -> ( ( I - ( N - A ) ) e. ( ZZ>= ` 0 ) /\ A e. ZZ /\ ( I - ( N - A ) ) < A ) ) ) )
63 62 3adant2 
 |-  ( ( A e. NN0 /\ N e. NN /\ A < N ) -> ( I e. ( 0 ..^ N ) -> ( -. I < ( N - A ) -> ( ( I - ( N - A ) ) e. ( ZZ>= ` 0 ) /\ A e. ZZ /\ ( I - ( N - A ) ) < A ) ) ) )
64 1 63 sylbi 
 |-  ( A e. ( 0 ..^ N ) -> ( I e. ( 0 ..^ N ) -> ( -. I < ( N - A ) -> ( ( I - ( N - A ) ) e. ( ZZ>= ` 0 ) /\ A e. ZZ /\ ( I - ( N - A ) ) < A ) ) ) )
65 64 3imp 
 |-  ( ( A e. ( 0 ..^ N ) /\ I e. ( 0 ..^ N ) /\ -. I < ( N - A ) ) -> ( ( I - ( N - A ) ) e. ( ZZ>= ` 0 ) /\ A e. ZZ /\ ( I - ( N - A ) ) < A ) )
66 elfzo2 
 |-  ( ( I - ( N - A ) ) e. ( 0 ..^ A ) <-> ( ( I - ( N - A ) ) e. ( ZZ>= ` 0 ) /\ A e. ZZ /\ ( I - ( N - A ) ) < A ) )
67 65 66 sylibr 
 |-  ( ( A e. ( 0 ..^ N ) /\ I e. ( 0 ..^ N ) /\ -. I < ( N - A ) ) -> ( I - ( N - A ) ) e. ( 0 ..^ A ) )