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 0 ..^ N I 0 ..^ N ¬ I < N A I N A 0 ..^ A

Proof

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