jm2.24nn

Description: X(n) is strictly greater than Y(n) + Y(n-1). Lemma 2.24 of JonesMatijasevic p. 697 restricted to NN . (Contributed by Stefan O'Rear, 3-Oct-2014)

		Ref	Expression
	Assertion	jm2.24nn	$⊢ (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		nnz	$⊢ N \in ℕ \to N \in ℤ$
2		1z	$⊢ 1 \in ℤ$
3		zsubcl	$⊢ (N \in ℤ \land 1 \in ℤ) \to N - 1 \in ℤ$
4	1 2 3	sylancl	$⊢ N \in ℕ \to N - 1 \in ℤ$
5		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
6	5	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N - 1 \in ℤ) \to A Y_{rm} (N - 1) \in ℤ$
7	4 6	sylan2	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A Y_{rm} (N - 1) \in ℤ$
8	7	zred	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A Y_{rm} (N - 1) \in ℝ$
9	5	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N \in ℤ$
10	1 9	sylan2	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A Y_{rm} N \in ℤ$
11	10	zred	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A Y_{rm} N \in ℝ$
12	8 11	readdcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to (A Y_{rm} (N - 1)) + (A Y_{rm} N) \in ℝ$
13		2re	$⊢ 2 \in ℝ$
14		remulcl	$⊢ (2 \in ℝ \land A Y_{rm} N \in ℝ) \to 2 (A Y_{rm} N) \in ℝ$
15	13 11 14	sylancr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 2 (A Y_{rm} N) \in ℝ$
16	15 8	resubcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 2 (A Y_{rm} N) - (A Y_{rm} (N - 1)) \in ℝ$
17		frmx	$⊢ X_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℕ_{0}$
18	17	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A X_{rm} N \in ℕ_{0}$
19	1 18	sylan2	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A X_{rm} N \in ℕ_{0}$
20	19	nn0red	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A X_{rm} N \in ℝ$
21	11 8	resubcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to (A Y_{rm} N) - (A Y_{rm} (N - 1)) \in ℝ$
22		remulcl	$⊢ (2 \in ℝ \land A Y_{rm} (N - 1) \in ℝ) \to 2 (A Y_{rm} (N - 1)) \in ℝ$
23	13 8 22	sylancr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 2 (A Y_{rm} (N - 1)) \in ℝ$
24		eluzelre	$⊢ A \in ℤ_{\geq 2} \to A \in ℝ$
25	24	adantr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A \in ℝ$
26	25 8	remulcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A (A Y_{rm} (N - 1)) \in ℝ$
27	8 25	remulcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to (A Y_{rm} (N - 1)) A \in ℝ$
28	17	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N - 1 \in ℤ) \to A X_{rm} (N - 1) \in ℕ_{0}$
29	4 28	sylan2	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A X_{rm} (N - 1) \in ℕ_{0}$
30	29	nn0red	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A X_{rm} (N - 1) \in ℝ$
31	27 30	readdcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to (A Y_{rm} (N - 1)) A + (A X_{rm} (N - 1)) \in ℝ$
32	13	a1i	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 2 \in ℝ$
33		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
34		rmxypos	$⊢ (A \in ℤ_{\geq 2} \land N - 1 \in ℕ_{0}) \to (0 < A X_{rm} (N - 1) \land 0 \leq A Y_{rm} (N - 1))$
35	34	simprd	$⊢ (A \in ℤ_{\geq 2} \land N - 1 \in ℕ_{0}) \to 0 \leq A Y_{rm} (N - 1)$
36	33 35	sylan2	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 0 \leq A Y_{rm} (N - 1)$
37		eluzle	$⊢ A \in ℤ_{\geq 2} \to 2 \leq A$
38	37	adantr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 2 \leq A$
39	32 25 8 36 38	lemul1ad	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 2 (A Y_{rm} (N - 1)) \leq A (A Y_{rm} (N - 1))$
40	25	recnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A \in ℂ$
41	8	recnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A Y_{rm} (N - 1) \in ℂ$
42	40 41	mulcomd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A (A Y_{rm} (N - 1)) = (A Y_{rm} (N - 1)) A$
43	34	simpld	$⊢ (A \in ℤ_{\geq 2} \land N - 1 \in ℕ_{0}) \to 0 < A X_{rm} (N - 1)$
44	33 43	sylan2	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 0 < A X_{rm} (N - 1)$
45	30 27	ltaddposd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to (0 < A X_{rm} (N - 1) \leftrightarrow (A Y_{rm} (N - 1)) A < (A Y_{rm} (N - 1)) A + (A X_{rm} (N - 1)))$
46	44 45	mpbid	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to (A Y_{rm} (N - 1)) A < (A Y_{rm} (N - 1)) A + (A X_{rm} (N - 1))$
47	42 46	eqbrtrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A (A Y_{rm} (N - 1)) < (A Y_{rm} (N - 1)) A + (A X_{rm} (N - 1))$
48	23 26 31 39 47	lelttrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 2 (A Y_{rm} (N - 1)) < (A Y_{rm} (N - 1)) A + (A X_{rm} (N - 1))$
49	41	2timesd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 2 (A Y_{rm} (N - 1)) = (A Y_{rm} (N - 1)) + (A Y_{rm} (N - 1))$
50		rmyp1	$⊢ (A \in ℤ_{\geq 2} \land N - 1 \in ℤ) \to A Y_{rm} (N - 1 + 1) = (A Y_{rm} (N - 1)) A + (A X_{rm} (N - 1))$
51	4 50	sylan2	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A Y_{rm} (N - 1 + 1) = (A Y_{rm} (N - 1)) A + (A X_{rm} (N - 1))$
52		nnre	$⊢ N \in ℕ \to N \in ℝ$
53	52	adantl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to N \in ℝ$
54	53	recnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to N \in ℂ$
55		ax-1cn	$⊢ 1 \in ℂ$
56		npcan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N - 1 + 1 = N$
57	54 55 56	sylancl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to N - 1 + 1 = N$
58	57	oveq2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A Y_{rm} (N - 1 + 1) = A Y_{rm} N$
59	51 58	eqtr3d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to (A Y_{rm} (N - 1)) A + (A X_{rm} (N - 1)) = A Y_{rm} N$
60	48 49 59	3brtr3d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to (A Y_{rm} (N - 1)) + (A Y_{rm} (N - 1)) < A Y_{rm} N$
61	8 8 11	ltaddsubd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to ((A Y_{rm} (N - 1)) + (A Y_{rm} (N - 1)) < A Y_{rm} N \leftrightarrow A Y_{rm} (N - 1) < (A Y_{rm} N) - (A Y_{rm} (N - 1)))$
62	60 61	mpbid	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A Y_{rm} (N - 1) < (A Y_{rm} N) - (A Y_{rm} (N - 1))$
63	8 21 11 62	ltadd1dd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to (A Y_{rm} (N - 1)) + (A Y_{rm} N) < (A Y_{rm} N) - (A Y_{rm} (N - 1)) + (A Y_{rm} N)$
64	11	recnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A Y_{rm} N \in ℂ$
65	64	2timesd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 2 (A Y_{rm} N) = (A Y_{rm} N) + (A Y_{rm} N)$
66	65	oveq1d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 2 (A Y_{rm} N) - (A Y_{rm} (N - 1)) = (A Y_{rm} N) + (A Y_{rm} N) - (A Y_{rm} (N - 1))$
67	64 64 41	addsubd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to (A Y_{rm} N) + (A Y_{rm} N) - (A Y_{rm} (N - 1)) = (A Y_{rm} N) - (A Y_{rm} (N - 1)) + (A Y_{rm} N)$
68	66 67	eqtrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 2 (A Y_{rm} N) - (A Y_{rm} (N - 1)) = (A Y_{rm} N) - (A Y_{rm} (N - 1)) + (A Y_{rm} N)$
69	63 68	breqtrrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to (A Y_{rm} (N - 1)) + (A Y_{rm} N) < 2 (A Y_{rm} N) - (A Y_{rm} (N - 1))$
70	25 11	remulcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A (A Y_{rm} N) \in ℝ$
71		rmy0	$⊢ A \in ℤ_{\geq 2} \to A Y_{rm} 0 = 0$
72	71	adantr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A Y_{rm} 0 = 0$
73		nngt0	$⊢ N \in ℕ \to 0 < N$
74	73	adantl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 0 < N$
75		simpl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A \in ℤ_{\geq 2}$
76		0zd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 0 \in ℤ$
77	1	adantl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to N \in ℤ$
78		ltrmy	$⊢ (A \in ℤ_{\geq 2} \land 0 \in ℤ \land N \in ℤ) \to (0 < N \leftrightarrow A Y_{rm} 0 < A Y_{rm} N)$
79	75 76 77 78	syl3anc	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to (0 < N \leftrightarrow A Y_{rm} 0 < A Y_{rm} N)$
80	74 79	mpbid	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A Y_{rm} 0 < A Y_{rm} N$
81	72 80	eqbrtrrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 0 < A Y_{rm} N$
82		lemul1	$⊢ (2 \in ℝ \land A \in ℝ \land (A Y_{rm} N \in ℝ \land 0 < A Y_{rm} N)) \to (2 \leq A \leftrightarrow 2 (A Y_{rm} N) \leq A (A Y_{rm} N))$
83	32 25 11 81 82	syl112anc	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to (2 \leq A \leftrightarrow 2 (A Y_{rm} N) \leq A (A Y_{rm} N))$
84	38 83	mpbid	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 2 (A Y_{rm} N) \leq A (A Y_{rm} N)$
85	15 70 8 84	lesub1dd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 2 (A Y_{rm} N) - (A Y_{rm} (N - 1)) \leq A (A Y_{rm} N) - (A Y_{rm} (N - 1))$
86		rmym1	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} (N - 1) = (A Y_{rm} N) A - (A X_{rm} N)$
87	1 86	sylan2	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A Y_{rm} (N - 1) = (A Y_{rm} N) A - (A X_{rm} N)$
88	64 40	mulcomd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to (A Y_{rm} N) A = A (A Y_{rm} N)$
89	88	oveq1d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to (A Y_{rm} N) A - (A X_{rm} N) = A (A Y_{rm} N) - (A X_{rm} N)$
90	87 89	eqtr2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A (A Y_{rm} N) - (A X_{rm} N) = A Y_{rm} (N - 1)$
91	70	recnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A (A Y_{rm} N) \in ℂ$
92	20	recnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A X_{rm} N \in ℂ$
93		subsub23	$⊢ (A (A Y_{rm} N) \in ℂ \land A X_{rm} N \in ℂ \land A Y_{rm} (N - 1) \in ℂ) \to (A (A Y_{rm} N) - (A X_{rm} N) = A Y_{rm} (N - 1) \leftrightarrow A (A Y_{rm} N) - (A Y_{rm} (N - 1)) = A X_{rm} N)$
94	91 92 41 93	syl3anc	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to (A (A Y_{rm} N) - (A X_{rm} N) = A Y_{rm} (N - 1) \leftrightarrow A (A Y_{rm} N) - (A Y_{rm} (N - 1)) = A X_{rm} N)$
95	90 94	mpbid	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A (A Y_{rm} N) - (A Y_{rm} (N - 1)) = A X_{rm} N$
96	85 95	breqtrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 2 (A Y_{rm} N) - (A Y_{rm} (N - 1)) \leq A X_{rm} N$
97	12 16 20 69 96	ltletrd	$⊢ (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.24nn

Proof