jm2.24

Description: Lemma 2.24 of JonesMatijasevic p. 697 extended to ZZ . Could be eliminated with a more careful proof of jm2.26lem3 . (Contributed by Stefan O'Rear, 3-Oct-2014)

		Ref	Expression
	Assertion	jm2.24	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A Y_{rm} (N - 1)) + (A Y_{rm} N) < A X_{rm} N$

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to A \in ℤ_{\geq 2}$
2		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
3	2	ad2antlr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to N - 1 \in ℤ$
4		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
5	4	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N - 1 \in ℤ) \to A Y_{rm} (N - 1) \in ℤ$
6	1 3 5	syl2anc	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to A Y_{rm} (N - 1) \in ℤ$
7	6	zred	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to A Y_{rm} (N - 1) \in ℝ$
8	4	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N \in ℤ$
9	8	zred	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N \in ℝ$
10	9	adantr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to A Y_{rm} N \in ℝ$
11	7 10	readdcld	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to (A Y_{rm} (N - 1)) + (A Y_{rm} N) \in ℝ$
12		0red	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to 0 \in ℝ$
13		frmx	$⊢ X_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℕ_{0}$
14	13	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℕ_{0}$
15	14	adantr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to A X_{rm} N \in ℕ_{0}$
16	15	nn0red	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to A X_{rm} N \in ℝ$
17		znegcl	$⊢ N \in ℤ \to - N \in ℤ$
18	17	ad2antlr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to - N \in ℤ$
19	18	peano2zd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to - N + 1 \in ℤ$
20	4	fovcl	$⊢ (A \in ℤ_{\geq 2} \land - N + 1 \in ℤ) \to A Y_{rm} (- N + 1) \in ℤ$
21	1 19 20	syl2anc	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to A Y_{rm} (- N + 1) \in ℤ$
22	21	zred	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to A Y_{rm} (- N + 1) \in ℝ$
23	4	fovcl	$⊢ (A \in ℤ_{\geq 2} \land - N \in ℤ) \to A Y_{rm} -N \in ℤ$
24	1 18 23	syl2anc	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to A Y_{rm} -N \in ℤ$
25	24	zred	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to A Y_{rm} -N \in ℝ$
26		rmy0	$⊢ A \in ℤ_{\geq 2} \to A Y_{rm} 0 = 0$
27	26	ad2antrr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to A Y_{rm} 0 = 0$
28		simpr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to N \leq 0$
29		zre	$⊢ N \in ℤ \to N \in ℝ$
30	29	ad2antlr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to N \in ℝ$
31	30	le0neg1d	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to (N \leq 0 \leftrightarrow 0 \leq - N)$
32	28 31	mpbid	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to 0 \leq - N$
33		0zd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to 0 \in ℤ$
34		zleltp1	$⊢ (0 \in ℤ \land - N \in ℤ) \to (0 \leq - N \leftrightarrow 0 < - N + 1)$
35	33 18 34	syl2anc	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to (0 \leq - N \leftrightarrow 0 < - N + 1)$
36	32 35	mpbid	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to 0 < - N + 1$
37		ltrmy	$⊢ (A \in ℤ_{\geq 2} \land 0 \in ℤ \land - N + 1 \in ℤ) \to (0 < - N + 1 \leftrightarrow A Y_{rm} 0 < A Y_{rm} (- N + 1))$
38	1 33 19 37	syl3anc	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to (0 < - N + 1 \leftrightarrow A Y_{rm} 0 < A Y_{rm} (- N + 1))$
39	36 38	mpbid	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to A Y_{rm} 0 < A Y_{rm} (- N + 1)$
40	27 39	eqbrtrrd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to 0 < A Y_{rm} (- N + 1)$
41		lermy	$⊢ (A \in ℤ_{\geq 2} \land 0 \in ℤ \land - N \in ℤ) \to (0 \leq - N \leftrightarrow A Y_{rm} 0 \leq A Y_{rm} -N)$
42	1 33 18 41	syl3anc	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to (0 \leq - N \leftrightarrow A Y_{rm} 0 \leq A Y_{rm} -N)$
43	32 42	mpbid	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to A Y_{rm} 0 \leq A Y_{rm} -N$
44	27 43	eqbrtrrd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to 0 \leq A Y_{rm} -N$
45	22 25 40 44	addgtge0d	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to 0 < (A Y_{rm} (- N + 1)) + (A Y_{rm} -N)$
46	7	recnd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to A Y_{rm} (N - 1) \in ℂ$
47	10	recnd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to A Y_{rm} N \in ℂ$
48	46 47	negdid	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to - ((A Y_{rm} (N - 1)) + (A Y_{rm} N)) = - (A Y_{rm} (N - 1)) + (- (A Y_{rm} N))$
49		rmyneg	$⊢ (A \in ℤ_{\geq 2} \land N - 1 \in ℤ) \to A Y_{rm} (- (N - 1)) = - (A Y_{rm} (N - 1))$
50	1 3 49	syl2anc	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to A Y_{rm} (- (N - 1)) = - (A Y_{rm} (N - 1))$
51		rmyneg	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} -N = - (A Y_{rm} N)$
52	51	adantr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to A Y_{rm} -N = - (A Y_{rm} N)$
53	50 52	oveq12d	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to (A Y_{rm} (- (N - 1))) + (A Y_{rm} -N) = - (A Y_{rm} (N - 1)) + (- (A Y_{rm} N))$
54		zcn	$⊢ N \in ℤ \to N \in ℂ$
55	54	ad2antlr	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to N \in ℂ$
56		ax-1cn	$⊢ 1 \in ℂ$
57		negsubdi	$⊢ (N \in ℂ \land 1 \in ℂ) \to - (N - 1) = - N + 1$
58	55 56 57	sylancl	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to - (N - 1) = - N + 1$
59	58	oveq2d	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to A Y_{rm} (- (N - 1)) = A Y_{rm} (- N + 1)$
60	59	oveq1d	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to (A Y_{rm} (- (N - 1))) + (A Y_{rm} -N) = (A Y_{rm} (- N + 1)) + (A Y_{rm} -N)$
61	48 53 60	3eqtr2d	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to - ((A Y_{rm} (N - 1)) + (A Y_{rm} N)) = (A Y_{rm} (- N + 1)) + (A Y_{rm} -N)$
62	45 61	breqtrrd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to 0 < - ((A Y_{rm} (N - 1)) + (A Y_{rm} N))$
63	11	lt0neg1d	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to ((A Y_{rm} (N - 1)) + (A Y_{rm} N) < 0 \leftrightarrow 0 < - ((A Y_{rm} (N - 1)) + (A Y_{rm} N)))$
64	62 63	mpbird	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to (A Y_{rm} (N - 1)) + (A Y_{rm} N) < 0$
65	15	nn0ge0d	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to 0 \leq A X_{rm} N$
66	11 12 16 64 65	ltletrd	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land N \leq 0) \to (A Y_{rm} (N - 1)) + (A Y_{rm} N) < A X_{rm} N$
67		simpll	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land 0 < N) \to A \in ℤ_{\geq 2}$
68		elnnz	$⊢ N \in ℕ \leftrightarrow (N \in ℤ \land 0 < N)$
69	68	biimpri	$⊢ (N \in ℤ \land 0 < N) \to N \in ℕ$
70	69	adantll	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land 0 < N) \to N \in ℕ$
71		jm2.24nn	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to (A Y_{rm} (N - 1)) + (A Y_{rm} N) < A X_{rm} N$
72	67 70 71	syl2anc	$⊢ ((A \in ℤ_{\geq 2} \land N \in ℤ) \land 0 < N) \to (A Y_{rm} (N - 1)) + (A Y_{rm} N) < A X_{rm} N$
73	29	adantl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to N \in ℝ$
74		0re	$⊢ 0 \in ℝ$
75		lelttric	$⊢ (N \in ℝ \land 0 \in ℝ) \to (N \leq 0 \lor 0 < N)$
76	73 74 75	sylancl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (N \leq 0 \lor 0 < N)$
77	66 72 76	mpjaodan	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (A Y_{rm} (N - 1)) + (A Y_{rm} N) < A X_{rm} N$

Metamath Proof Explorer

Theorem jm2.24

Proof