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 \in ℕ_{0} \land L \in ℤ) \to ((J \in ℝ \land 0 \leq J \land J < L - N - 1) \to L - 1 \in ℕ)$

Proof

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

Metamath Proof Explorer

Theorem zm1nn

Proof