Metamath Proof Explorer

Theorem zm1nn

Description: An integer minus 1 is positive under certain circumstances. (Contributed by Alexander van der Vekens, 9-Jun-2018)

Ref Expression
Assertion zm1nn 
|- ( ( N e. NN0 /\ L e. ZZ ) -> ( ( J e. RR /\ 0 <_ J /\ J < ( ( L - N ) - 1 ) ) -> ( L - 1 ) e. NN ) )

Proof

Step Hyp Ref Expression
1 0red 
 |-  ( ( J e. RR /\ ( N e. NN0 /\ L e. ZZ ) ) -> 0 e. RR )
2 simpl 
 |-  ( ( J e. RR /\ ( N e. NN0 /\ L e. ZZ ) ) -> J e. RR )
3 zre 
 |-  ( L e. ZZ -> L e. RR )
4 nn0re 
 |-  ( N e. NN0 -> N e. RR )
5 resubcl 
 |-  ( ( L e. RR /\ N e. RR ) -> ( L - N ) e. RR )
6 3 4 5 syl2anr 
 |-  ( ( N e. NN0 /\ L e. ZZ ) -> ( L - N ) e. RR )
7 6 adantl 
 |-  ( ( J e. RR /\ ( N e. NN0 /\ L e. ZZ ) ) -> ( L - N ) e. RR )
8 peano2rem 
 |-  ( ( L - N ) e. RR -> ( ( L - N ) - 1 ) e. RR )
9 7 8 syl 
 |-  ( ( J e. RR /\ ( N e. NN0 /\ L e. ZZ ) ) -> ( ( L - N ) - 1 ) e. RR )
10 lelttr 
 |-  ( ( 0 e. RR /\ J e. RR /\ ( ( L - N ) - 1 ) e. RR ) -> ( ( 0 <_ J /\ J < ( ( L - N ) - 1 ) ) -> 0 < ( ( L - N ) - 1 ) ) )
11 1 2 9 10 syl3anc 
 |-  ( ( J e. RR /\ ( N e. NN0 /\ L e. ZZ ) ) -> ( ( 0 <_ J /\ J < ( ( L - N ) - 1 ) ) -> 0 < ( ( L - N ) - 1 ) ) )
12 1red 
 |-  ( ( N e. NN0 /\ L e. ZZ ) -> 1 e. RR )
13 12 6 posdifd 
 |-  ( ( N e. NN0 /\ L e. ZZ ) -> ( 1 < ( L - N ) <-> 0 < ( ( L - N ) - 1 ) ) )
14 4 adantr 
 |-  ( ( N e. NN0 /\ L e. ZZ ) -> N e. RR )
15 3 adantl 
 |-  ( ( N e. NN0 /\ L e. ZZ ) -> L e. RR )
16 12 14 15 ltaddsubd 
 |-  ( ( N e. NN0 /\ L e. ZZ ) -> ( ( 1 + N ) < L <-> 1 < ( L - N ) ) )
17 elnn0z 
 |-  ( N e. NN0 <-> ( N e. ZZ /\ 0 <_ N ) )
18 0red 
 |-  ( ( N e. ZZ /\ L e. ZZ ) -> 0 e. RR )
19 zre 
 |-  ( N e. ZZ -> N e. RR )
20 19 adantr 
 |-  ( ( N e. ZZ /\ L e. ZZ ) -> N e. RR )
21 1red 
 |-  ( ( N e. ZZ /\ L e. ZZ ) -> 1 e. RR )
22 18 20 21 leadd2d 
 |-  ( ( N e. ZZ /\ L e. ZZ ) -> ( 0 <_ N <-> ( 1 + 0 ) <_ ( 1 + N ) ) )
23 1re 
 |-  1 e. RR
24 0re 
 |-  0 e. RR
25 23 24 readdcli 
 |-  ( 1 + 0 ) e. RR
26 25 a1i 
 |-  ( ( N e. ZZ /\ L e. ZZ ) -> ( 1 + 0 ) e. RR )
27 1red 
 |-  ( N e. ZZ -> 1 e. RR )
28 27 19 readdcld 
 |-  ( N e. ZZ -> ( 1 + N ) e. RR )
29 28 adantr 
 |-  ( ( N e. ZZ /\ L e. ZZ ) -> ( 1 + N ) e. RR )
30 3 adantl 
 |-  ( ( N e. ZZ /\ L e. ZZ ) -> L e. RR )
31 lelttr 
 |-  ( ( ( 1 + 0 ) e. RR /\ ( 1 + N ) e. RR /\ L e. RR ) -> ( ( ( 1 + 0 ) <_ ( 1 + N ) /\ ( 1 + N ) < L ) -> ( 1 + 0 ) < L ) )
32 26 29 30 31 syl3anc 
 |-  ( ( N e. ZZ /\ L e. ZZ ) -> ( ( ( 1 + 0 ) <_ ( 1 + N ) /\ ( 1 + N ) < L ) -> ( 1 + 0 ) < L ) )
33 peano2zm 
 |-  ( L e. ZZ -> ( L - 1 ) e. ZZ )
34 33 adantl 
 |-  ( ( N e. ZZ /\ L e. ZZ ) -> ( L - 1 ) e. ZZ )
35 34 adantr 
 |-  ( ( ( N e. ZZ /\ L e. ZZ ) /\ ( 1 + 0 ) < L ) -> ( L - 1 ) e. ZZ )
36 1red 
 |-  ( L e. ZZ -> 1 e. RR )
37 0red 
 |-  ( L e. ZZ -> 0 e. RR )
38 36 37 3 ltaddsub2d 
 |-  ( L e. ZZ -> ( ( 1 + 0 ) < L <-> 0 < ( L - 1 ) ) )
39 38 biimpd 
 |-  ( L e. ZZ -> ( ( 1 + 0 ) < L -> 0 < ( L - 1 ) ) )
40 39 adantl 
 |-  ( ( N e. ZZ /\ L e. ZZ ) -> ( ( 1 + 0 ) < L -> 0 < ( L - 1 ) ) )
41 40 imp 
 |-  ( ( ( N e. ZZ /\ L e. ZZ ) /\ ( 1 + 0 ) < L ) -> 0 < ( L - 1 ) )
42 elnnz 
 |-  ( ( L - 1 ) e. NN <-> ( ( L - 1 ) e. ZZ /\ 0 < ( L - 1 ) ) )
43 35 41 42 sylanbrc 
 |-  ( ( ( N e. ZZ /\ L e. ZZ ) /\ ( 1 + 0 ) < L ) -> ( L - 1 ) e. NN )
44 43 ex 
 |-  ( ( N e. ZZ /\ L e. ZZ ) -> ( ( 1 + 0 ) < L -> ( L - 1 ) e. NN ) )
45 32 44 syld 
 |-  ( ( N e. ZZ /\ L e. ZZ ) -> ( ( ( 1 + 0 ) <_ ( 1 + N ) /\ ( 1 + N ) < L ) -> ( L - 1 ) e. NN ) )
46 45 expd 
 |-  ( ( N e. ZZ /\ L e. ZZ ) -> ( ( 1 + 0 ) <_ ( 1 + N ) -> ( ( 1 + N ) < L -> ( L - 1 ) e. NN ) ) )
47 22 46 sylbid 
 |-  ( ( N e. ZZ /\ L e. ZZ ) -> ( 0 <_ N -> ( ( 1 + N ) < L -> ( L - 1 ) e. NN ) ) )
48 47 impancom 
 |-  ( ( N e. ZZ /\ 0 <_ N ) -> ( L e. ZZ -> ( ( 1 + N ) < L -> ( L - 1 ) e. NN ) ) )
49 17 48 sylbi 
 |-  ( N e. NN0 -> ( L e. ZZ -> ( ( 1 + N ) < L -> ( L - 1 ) e. NN ) ) )
50 49 imp 
 |-  ( ( N e. NN0 /\ L e. ZZ ) -> ( ( 1 + N ) < L -> ( L - 1 ) e. NN ) )
51 16 50 sylbird 
 |-  ( ( N e. NN0 /\ L e. ZZ ) -> ( 1 < ( L - N ) -> ( L - 1 ) e. NN ) )
52 13 51 sylbird 
 |-  ( ( N e. NN0 /\ L e. ZZ ) -> ( 0 < ( ( L - N ) - 1 ) -> ( L - 1 ) e. NN ) )
53 52 adantl 
 |-  ( ( J e. RR /\ ( N e. NN0 /\ L e. ZZ ) ) -> ( 0 < ( ( L - N ) - 1 ) -> ( L - 1 ) e. NN ) )
54 11 53 syld 
 |-  ( ( J e. RR /\ ( N e. NN0 /\ L e. ZZ ) ) -> ( ( 0 <_ J /\ J < ( ( L - N ) - 1 ) ) -> ( L - 1 ) e. NN ) )
55 54 ex 
 |-  ( J e. RR -> ( ( N e. NN0 /\ L e. ZZ ) -> ( ( 0 <_ J /\ J < ( ( L - N ) - 1 ) ) -> ( L - 1 ) e. NN ) ) )
56 55 com23 
 |-  ( J e. RR -> ( ( 0 <_ J /\ J < ( ( L - N ) - 1 ) ) -> ( ( N e. NN0 /\ L e. ZZ ) -> ( L - 1 ) e. NN ) ) )
57 56 3impib 
 |-  ( ( J e. RR /\ 0 <_ J /\ J < ( ( L - N ) - 1 ) ) -> ( ( N e. NN0 /\ L e. ZZ ) -> ( L - 1 ) e. NN ) )
58 57 com12 
 |-  ( ( N e. NN0 /\ L e. ZZ ) -> ( ( J e. RR /\ 0 <_ J /\ J < ( ( L - N ) - 1 ) ) -> ( L - 1 ) e. NN ) )