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 ( ( 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → ( ( 𝐽 ∈ ℝ ∧ 0 ≤ 𝐽 ∧ 𝐽 < ( ( 𝐿 − 𝑁 ) − 1 ) ) → ( 𝐿 − 1 ) ∈ ℕ ) )

Proof

Step Hyp Ref Expression
1 0red ⊢ ( ( 𝐽 ∈ ℝ ∧ ( 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) ) → 0 ∈ ℝ )
2 simpl ⊢ ( ( 𝐽 ∈ ℝ ∧ ( 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) ) → 𝐽 ∈ ℝ )
3 zre ⊢ ( 𝐿 ∈ ℤ → 𝐿 ∈ ℝ )
4 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
5 resubcl ⊢ ( ( 𝐿 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝐿 − 𝑁 ) ∈ ℝ )
6 3 4 5 syl2anr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → ( 𝐿 − 𝑁 ) ∈ ℝ )
7 6 adantl ⊢ ( ( 𝐽 ∈ ℝ ∧ ( 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) ) → ( 𝐿 − 𝑁 ) ∈ ℝ )
8 peano2rem ⊢ ( ( 𝐿 − 𝑁 ) ∈ ℝ → ( ( 𝐿 − 𝑁 ) − 1 ) ∈ ℝ )
9 7 8 syl ⊢ ( ( 𝐽 ∈ ℝ ∧ ( 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) ) → ( ( 𝐿 − 𝑁 ) − 1 ) ∈ ℝ )
10 lelttr ⊢ ( ( 0 ∈ ℝ ∧ 𝐽 ∈ ℝ ∧ ( ( 𝐿 − 𝑁 ) − 1 ) ∈ ℝ ) → ( ( 0 ≤ 𝐽 ∧ 𝐽 < ( ( 𝐿 − 𝑁 ) − 1 ) ) → 0 < ( ( 𝐿 − 𝑁 ) − 1 ) ) )
11 1 2 9 10 syl3anc ⊢ ( ( 𝐽 ∈ ℝ ∧ ( 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) ) → ( ( 0 ≤ 𝐽 ∧ 𝐽 < ( ( 𝐿 − 𝑁 ) − 1 ) ) → 0 < ( ( 𝐿 − 𝑁 ) − 1 ) ) )
12 1red ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → 1 ∈ ℝ )
13 12 6 posdifd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → ( 1 < ( 𝐿 − 𝑁 ) ↔ 0 < ( ( 𝐿 − 𝑁 ) − 1 ) ) )
14 4 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → 𝑁 ∈ ℝ )
15 3 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → 𝐿 ∈ ℝ )
16 12 14 15 ltaddsubd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → ( ( 1 + 𝑁 ) < 𝐿 ↔ 1 < ( 𝐿 − 𝑁 ) ) )
17 elnn0z ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℤ ∧ 0 ≤ 𝑁 ) )
18 0red ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → 0 ∈ ℝ )
19 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
20 19 adantr ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → 𝑁 ∈ ℝ )
21 1red ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → 1 ∈ ℝ )
22 18 20 21 leadd2d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 0 ≤ 𝑁 ↔ ( 1 + 0 ) ≤ ( 1 + 𝑁 ) ) )
23 1re ⊢ 1 ∈ ℝ
24 0re ⊢ 0 ∈ ℝ
25 23 24 readdcli ⊢ ( 1 + 0 ) ∈ ℝ
26 25 a1i ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 1 + 0 ) ∈ ℝ )
27 1red ⊢ ( 𝑁 ∈ ℤ → 1 ∈ ℝ )
28 27 19 readdcld ⊢ ( 𝑁 ∈ ℤ → ( 1 + 𝑁 ) ∈ ℝ )
29 28 adantr ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 1 + 𝑁 ) ∈ ℝ )
30 3 adantl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → 𝐿 ∈ ℝ )
31 lelttr ⊢ ( ( ( 1 + 0 ) ∈ ℝ ∧ ( 1 + 𝑁 ) ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( ( ( 1 + 0 ) ≤ ( 1 + 𝑁 ) ∧ ( 1 + 𝑁 ) < 𝐿 ) → ( 1 + 0 ) < 𝐿 ) )
32 26 29 30 31 syl3anc ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( ( 1 + 0 ) ≤ ( 1 + 𝑁 ) ∧ ( 1 + 𝑁 ) < 𝐿 ) → ( 1 + 0 ) < 𝐿 ) )
33 peano2zm ⊢ ( 𝐿 ∈ ℤ → ( 𝐿 − 1 ) ∈ ℤ )
34 33 adantl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝐿 − 1 ) ∈ ℤ )
35 34 adantr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 1 + 0 ) < 𝐿 ) → ( 𝐿 − 1 ) ∈ ℤ )
36 1red ⊢ ( 𝐿 ∈ ℤ → 1 ∈ ℝ )
37 0red ⊢ ( 𝐿 ∈ ℤ → 0 ∈ ℝ )
38 36 37 3 ltaddsub2d ⊢ ( 𝐿 ∈ ℤ → ( ( 1 + 0 ) < 𝐿 ↔ 0 < ( 𝐿 − 1 ) ) )
39 38 biimpd ⊢ ( 𝐿 ∈ ℤ → ( ( 1 + 0 ) < 𝐿 → 0 < ( 𝐿 − 1 ) ) )
40 39 adantl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( 1 + 0 ) < 𝐿 → 0 < ( 𝐿 − 1 ) ) )
41 40 imp ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 1 + 0 ) < 𝐿 ) → 0 < ( 𝐿 − 1 ) )
42 elnnz ⊢ ( ( 𝐿 − 1 ) ∈ ℕ ↔ ( ( 𝐿 − 1 ) ∈ ℤ ∧ 0 < ( 𝐿 − 1 ) ) )
43 35 41 42 sylanbrc ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 1 + 0 ) < 𝐿 ) → ( 𝐿 − 1 ) ∈ ℕ )
44 43 ex ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( 1 + 0 ) < 𝐿 → ( 𝐿 − 1 ) ∈ ℕ ) )
45 32 44 syld ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( ( 1 + 0 ) ≤ ( 1 + 𝑁 ) ∧ ( 1 + 𝑁 ) < 𝐿 ) → ( 𝐿 − 1 ) ∈ ℕ ) )
46 45 expd ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( 1 + 0 ) ≤ ( 1 + 𝑁 ) → ( ( 1 + 𝑁 ) < 𝐿 → ( 𝐿 − 1 ) ∈ ℕ ) ) )
47 22 46 sylbid ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 0 ≤ 𝑁 → ( ( 1 + 𝑁 ) < 𝐿 → ( 𝐿 − 1 ) ∈ ℕ ) ) )
48 47 impancom ⊢ ( ( 𝑁 ∈ ℤ ∧ 0 ≤ 𝑁 ) → ( 𝐿 ∈ ℤ → ( ( 1 + 𝑁 ) < 𝐿 → ( 𝐿 − 1 ) ∈ ℕ ) ) )
49 17 48 sylbi ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐿 ∈ ℤ → ( ( 1 + 𝑁 ) < 𝐿 → ( 𝐿 − 1 ) ∈ ℕ ) ) )
50 49 imp ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → ( ( 1 + 𝑁 ) < 𝐿 → ( 𝐿 − 1 ) ∈ ℕ ) )
51 16 50 sylbird ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → ( 1 < ( 𝐿 − 𝑁 ) → ( 𝐿 − 1 ) ∈ ℕ ) )
52 13 51 sylbird ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → ( 0 < ( ( 𝐿 − 𝑁 ) − 1 ) → ( 𝐿 − 1 ) ∈ ℕ ) )
53 52 adantl ⊢ ( ( 𝐽 ∈ ℝ ∧ ( 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) ) → ( 0 < ( ( 𝐿 − 𝑁 ) − 1 ) → ( 𝐿 − 1 ) ∈ ℕ ) )
54 11 53 syld ⊢ ( ( 𝐽 ∈ ℝ ∧ ( 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) ) → ( ( 0 ≤ 𝐽 ∧ 𝐽 < ( ( 𝐿 − 𝑁 ) − 1 ) ) → ( 𝐿 − 1 ) ∈ ℕ ) )
55 54 ex ⊢ ( 𝐽 ∈ ℝ → ( ( 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → ( ( 0 ≤ 𝐽 ∧ 𝐽 < ( ( 𝐿 − 𝑁 ) − 1 ) ) → ( 𝐿 − 1 ) ∈ ℕ ) ) )
56 55 com23 ⊢ ( 𝐽 ∈ ℝ → ( ( 0 ≤ 𝐽 ∧ 𝐽 < ( ( 𝐿 − 𝑁 ) − 1 ) ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → ( 𝐿 − 1 ) ∈ ℕ ) ) )
57 56 3impib ⊢ ( ( 𝐽 ∈ ℝ ∧ 0 ≤ 𝐽 ∧ 𝐽 < ( ( 𝐿 − 𝑁 ) − 1 ) ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → ( 𝐿 − 1 ) ∈ ℕ ) )
58 57 com12 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → ( ( 𝐽 ∈ ℝ ∧ 0 ≤ 𝐽 ∧ 𝐽 < ( ( 𝐿 − 𝑁 ) − 1 ) ) → ( 𝐿 − 1 ) ∈ ℕ ) )