jm2.17c

		Ref	Expression
	Assertion	jm2.17c	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A Y_{rm} (N + 1 + 1) < {2 A}^{N + 1}$

Proof

Step	Hyp	Ref	Expression
1		2re	$⊢ 2 \in ℝ$
2		eluzelre	$⊢ A \in ℤ_{\geq 2} \to A \in ℝ$
3	2	adantr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A \in ℝ$
4		remulcl	$⊢ (2 \in ℝ \land A \in ℝ) \to 2 A \in ℝ$
5	1 3 4	sylancr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 2 A \in ℝ$
6		nnz	$⊢ N \in ℕ \to N \in ℤ$
7	6	adantl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to N \in ℤ$
8	7	peano2zd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to N + 1 \in ℤ$
9		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
10	9	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N + 1 \in ℤ) \to A Y_{rm} (N + 1) \in ℤ$
11	10	zred	$⊢ (A \in ℤ_{\geq 2} \land N + 1 \in ℤ) \to A Y_{rm} (N + 1) \in ℝ$
12	8 11	syldan	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A Y_{rm} (N + 1) \in ℝ$
13	5 12	remulcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 2 A (A Y_{rm} (N + 1)) \in ℝ$
14		nncn	$⊢ N \in ℕ \to N \in ℂ$
15	14	adantl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to N \in ℂ$
16		ax-1cn	$⊢ 1 \in ℂ$
17		pncan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N + 1 - 1 = N$
18	15 16 17	sylancl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to N + 1 - 1 = N$
19	18	oveq2d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A Y_{rm} (N + 1 - 1) = A Y_{rm} N$
20	9	fovcl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N \in ℤ$
21	20	zred	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A Y_{rm} N \in ℝ$
22	6 21	sylan2	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A Y_{rm} N \in ℝ$
23	19 22	eqeltrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A Y_{rm} (N + 1 - 1) \in ℝ$
24	13 23	resubcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 2 A (A Y_{rm} (N + 1)) - (A Y_{rm} (N + 1 - 1)) \in ℝ$
25		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
26	25	adantl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to N \in ℕ_{0}$
27	5 26	reexpcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to {2 A}^{N} \in ℝ$
28	5 27	remulcld	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 2 A {2 A}^{N} \in ℝ$
29		rmy0	$⊢ A \in ℤ_{\geq 2} \to A Y_{rm} 0 = 0$
30	29	adantr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A Y_{rm} 0 = 0$
31		nngt0	$⊢ N \in ℕ \to 0 < N$
32	31	adantl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 0 < N$
33		simpl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A \in ℤ_{\geq 2}$
34		0zd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 0 \in ℤ$
35		ltrmy	$⊢ (A \in ℤ_{\geq 2} \land 0 \in ℤ \land N \in ℤ) \to (0 < N \leftrightarrow A Y_{rm} 0 < A Y_{rm} N)$
36	33 34 7 35	syl3anc	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to (0 < N \leftrightarrow A Y_{rm} 0 < A Y_{rm} N)$
37	32 36	mpbid	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A Y_{rm} 0 < A Y_{rm} N$
38	30 37	eqbrtrrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 0 < A Y_{rm} N$
39	38 19	breqtrrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 0 < A Y_{rm} (N + 1 - 1)$
40	23 13	ltsubposd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to (0 < A Y_{rm} (N + 1 - 1) \leftrightarrow 2 A (A Y_{rm} (N + 1)) - (A Y_{rm} (N + 1 - 1)) < 2 A (A Y_{rm} (N + 1)))$
41	39 40	mpbid	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 2 A (A Y_{rm} (N + 1)) - (A Y_{rm} (N + 1 - 1)) < 2 A (A Y_{rm} (N + 1))$
42		jm2.17b	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0}) \to A Y_{rm} (N + 1) \leq {2 A}^{N}$
43	25 42	sylan2	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A Y_{rm} (N + 1) \leq {2 A}^{N}$
44		2nn	$⊢ 2 \in ℕ$
45		eluz2nn	$⊢ A \in ℤ_{\geq 2} \to A \in ℕ$
46		nnmulcl	$⊢ (2 \in ℕ \land A \in ℕ) \to 2 A \in ℕ$
47	44 45 46	sylancr	$⊢ A \in ℤ_{\geq 2} \to 2 A \in ℕ$
48	47	nngt0d	$⊢ A \in ℤ_{\geq 2} \to 0 < 2 A$
49	48	adantr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 0 < 2 A$
50		lemul2	$⊢ (A Y_{rm} (N + 1) \in ℝ \land {2 A}^{N} \in ℝ \land (2 A \in ℝ \land 0 < 2 A)) \to (A Y_{rm} (N + 1) \leq {2 A}^{N} \leftrightarrow 2 A (A Y_{rm} (N + 1)) \leq 2 A {2 A}^{N})$
51	12 27 5 49 50	syl112anc	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to (A Y_{rm} (N + 1) \leq {2 A}^{N} \leftrightarrow 2 A (A Y_{rm} (N + 1)) \leq 2 A {2 A}^{N})$
52	43 51	mpbid	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 2 A (A Y_{rm} (N + 1)) \leq 2 A {2 A}^{N}$
53	24 13 28 41 52	ltletrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 2 A (A Y_{rm} (N + 1)) - (A Y_{rm} (N + 1 - 1)) < 2 A {2 A}^{N}$
54		rmyluc2	$⊢ (A \in ℤ_{\geq 2} \land N + 1 \in ℤ) \to A Y_{rm} (N + 1 + 1) = 2 A (A Y_{rm} (N + 1)) - (A Y_{rm} (N + 1 - 1))$
55	8 54	syldan	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A Y_{rm} (N + 1 + 1) = 2 A (A Y_{rm} (N + 1)) - (A Y_{rm} (N + 1 - 1))$
56	5	recnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to 2 A \in ℂ$
57	56 26	expp1d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to {2 A}^{N + 1} = {2 A}^{N} 2 A$
58	27	recnd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to {2 A}^{N} \in ℂ$
59	58 56	mulcomd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to {2 A}^{N} 2 A = 2 A {2 A}^{N}$
60	57 59	eqtrd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to {2 A}^{N + 1} = 2 A {2 A}^{N}$
61	53 55 60	3brtr4d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ) \to A Y_{rm} (N + 1 + 1) < {2 A}^{N + 1}$

Metamath Proof Explorer

Theorem jm2.17c

Proof