jm2.17b

Description: Weak form of the second half of lemma 2.17 of JonesMatijasevic p. 696, allowing induction to start lower. (Contributed by Stefan O'Rear, 15-Oct-2014)

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

Proof

Step	Hyp	Ref	Expression
1		oveq1	$⊢ a = 0 \to a + 1 = 0 + 1$
2	1	oveq2d	$⊢ a = 0 \to A Y_{rm} (a + 1) = A Y_{rm} (0 + 1)$
3		oveq2	$⊢ a = 0 \to {2 A}^{a} = {2 A}^{0}$
4	2 3	breq12d	$⊢ a = 0 \to (A Y_{rm} (a + 1) \leq {2 A}^{a} \leftrightarrow A Y_{rm} (0 + 1) \leq {2 A}^{0})$
5	4	imbi2d	$⊢ a = 0 \to ((A \in ℤ_{\geq 2} \to A Y_{rm} (a + 1) \leq {2 A}^{a}) \leftrightarrow (A \in ℤ_{\geq 2} \to A Y_{rm} (0 + 1) \leq {2 A}^{0}))$
6		oveq1	$⊢ a = b \to a + 1 = b + 1$
7	6	oveq2d	$⊢ a = b \to A Y_{rm} (a + 1) = A Y_{rm} (b + 1)$
8		oveq2	$⊢ a = b \to {2 A}^{a} = {2 A}^{b}$
9	7 8	breq12d	$⊢ a = b \to (A Y_{rm} (a + 1) \leq {2 A}^{a} \leftrightarrow A Y_{rm} (b + 1) \leq {2 A}^{b})$
10	9	imbi2d	$⊢ a = b \to ((A \in ℤ_{\geq 2} \to A Y_{rm} (a + 1) \leq {2 A}^{a}) \leftrightarrow (A \in ℤ_{\geq 2} \to A Y_{rm} (b + 1) \leq {2 A}^{b}))$
11		oveq1	$⊢ a = b + 1 \to a + 1 = b + 1 + 1$
12	11	oveq2d	$⊢ a = b + 1 \to A Y_{rm} (a + 1) = A Y_{rm} (b + 1 + 1)$
13		oveq2	$⊢ a = b + 1 \to {2 A}^{a} = {2 A}^{b + 1}$
14	12 13	breq12d	$⊢ a = b + 1 \to (A Y_{rm} (a + 1) \leq {2 A}^{a} \leftrightarrow A Y_{rm} (b + 1 + 1) \leq {2 A}^{b + 1})$
15	14	imbi2d	$⊢ a = b + 1 \to ((A \in ℤ_{\geq 2} \to A Y_{rm} (a + 1) \leq {2 A}^{a}) \leftrightarrow (A \in ℤ_{\geq 2} \to A Y_{rm} (b + 1 + 1) \leq {2 A}^{b + 1}))$
16		oveq1	$⊢ a = N \to a + 1 = N + 1$
17	16	oveq2d	$⊢ a = N \to A Y_{rm} (a + 1) = A Y_{rm} (N + 1)$
18		oveq2	$⊢ a = N \to {2 A}^{a} = {2 A}^{N}$
19	17 18	breq12d	$⊢ a = N \to (A Y_{rm} (a + 1) \leq {2 A}^{a} \leftrightarrow A Y_{rm} (N + 1) \leq {2 A}^{N})$
20	19	imbi2d	$⊢ a = N \to ((A \in ℤ_{\geq 2} \to A Y_{rm} (a + 1) \leq {2 A}^{a}) \leftrightarrow (A \in ℤ_{\geq 2} \to A Y_{rm} (N + 1) \leq {2 A}^{N}))$
21		1le1	$⊢ 1 \leq 1$
22		0p1e1	$⊢ 0 + 1 = 1$
23	22	oveq2i	$⊢ A Y_{rm} (0 + 1) = A Y_{rm} 1$
24		rmy1	$⊢ A \in ℤ_{\geq 2} \to A Y_{rm} 1 = 1$
25	23 24	eqtrid	$⊢ A \in ℤ_{\geq 2} \to A Y_{rm} (0 + 1) = 1$
26		2re	$⊢ 2 \in ℝ$
27		eluzelre	$⊢ A \in ℤ_{\geq 2} \to A \in ℝ$
28		remulcl	$⊢ (2 \in ℝ \land A \in ℝ) \to 2 A \in ℝ$
29	26 27 28	sylancr	$⊢ A \in ℤ_{\geq 2} \to 2 A \in ℝ$
30	29	recnd	$⊢ A \in ℤ_{\geq 2} \to 2 A \in ℂ$
31	30	exp0d	$⊢ A \in ℤ_{\geq 2} \to {2 A}^{0} = 1$
32	25 31	breq12d	$⊢ A \in ℤ_{\geq 2} \to (A Y_{rm} (0 + 1) \leq {2 A}^{0} \leftrightarrow 1 \leq 1)$
33	21 32	mpbiri	$⊢ A \in ℤ_{\geq 2} \to A Y_{rm} (0 + 1) \leq {2 A}^{0}$
34		simpr	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to A \in ℤ_{\geq 2}$
35		nn0z	$⊢ b \in ℕ_{0} \to b \in ℤ$
36	35	adantr	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to b \in ℤ$
37	36	peano2zd	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to b + 1 \in ℤ$
38		rmyluc2	$⊢ (A \in ℤ_{\geq 2} \land b + 1 \in ℤ) \to A Y_{rm} (b + 1 + 1) = 2 A (A Y_{rm} (b + 1)) - (A Y_{rm} (b + 1 - 1))$
39	34 37 38	syl2anc	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to A Y_{rm} (b + 1 + 1) = 2 A (A Y_{rm} (b + 1)) - (A Y_{rm} (b + 1 - 1))$
40		rmxypos	$⊢ (A \in ℤ_{\geq 2} \land b \in ℕ_{0}) \to (0 < A X_{rm} b \land 0 \leq A Y_{rm} b)$
41	40	simprd	$⊢ (A \in ℤ_{\geq 2} \land b \in ℕ_{0}) \to 0 \leq A Y_{rm} b$
42	41	ancoms	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to 0 \leq A Y_{rm} b$
43		nn0re	$⊢ b \in ℕ_{0} \to b \in ℝ$
44	43	adantr	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to b \in ℝ$
45	44	recnd	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to b \in ℂ$
46		ax-1cn	$⊢ 1 \in ℂ$
47		pncan	$⊢ (b \in ℂ \land 1 \in ℂ) \to b + 1 - 1 = b$
48	45 46 47	sylancl	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to b + 1 - 1 = b$
49	48	oveq2d	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to A Y_{rm} (b + 1 - 1) = A Y_{rm} b$
50	42 49	breqtrrd	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to 0 \leq A Y_{rm} (b + 1 - 1)$
51	27	adantl	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to A \in ℝ$
52	26 51 28	sylancr	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to 2 A \in ℝ$
53		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
54	53	fovcl	$⊢ (A \in ℤ_{\geq 2} \land b + 1 \in ℤ) \to A Y_{rm} (b + 1) \in ℤ$
55	54	zred	$⊢ (A \in ℤ_{\geq 2} \land b + 1 \in ℤ) \to A Y_{rm} (b + 1) \in ℝ$
56	34 37 55	syl2anc	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to A Y_{rm} (b + 1) \in ℝ$
57	52 56	remulcld	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to 2 A (A Y_{rm} (b + 1)) \in ℝ$
58	53	fovcl	$⊢ (A \in ℤ_{\geq 2} \land b \in ℤ) \to A Y_{rm} b \in ℤ$
59	58	zred	$⊢ (A \in ℤ_{\geq 2} \land b \in ℤ) \to A Y_{rm} b \in ℝ$
60	34 36 59	syl2anc	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to A Y_{rm} b \in ℝ$
61	49 60	eqeltrd	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to A Y_{rm} (b + 1 - 1) \in ℝ$
62	57 61	subge02d	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to (0 \leq A Y_{rm} (b + 1 - 1) \leftrightarrow 2 A (A Y_{rm} (b + 1)) - (A Y_{rm} (b + 1 - 1)) \leq 2 A (A Y_{rm} (b + 1)))$
63	50 62	mpbid	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to 2 A (A Y_{rm} (b + 1)) - (A Y_{rm} (b + 1 - 1)) \leq 2 A (A Y_{rm} (b + 1))$
64	39 63	eqbrtrd	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to A Y_{rm} (b + 1 + 1) \leq 2 A (A Y_{rm} (b + 1))$
65	64	3adant3	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land A Y_{rm} (b + 1) \leq {2 A}^{b}) \to A Y_{rm} (b + 1 + 1) \leq 2 A (A Y_{rm} (b + 1))$
66		simpl	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to b \in ℕ_{0}$
67	52 66	reexpcld	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to {2 A}^{b} \in ℝ$
68		2nn	$⊢ 2 \in ℕ$
69		eluz2nn	$⊢ A \in ℤ_{\geq 2} \to A \in ℕ$
70		nnmulcl	$⊢ (2 \in ℕ \land A \in ℕ) \to 2 A \in ℕ$
71	68 69 70	sylancr	$⊢ A \in ℤ_{\geq 2} \to 2 A \in ℕ$
72	71	nngt0d	$⊢ A \in ℤ_{\geq 2} \to 0 < 2 A$
73	72	adantl	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to 0 < 2 A$
74		lemul2	$⊢ (A Y_{rm} (b + 1) \in ℝ \land {2 A}^{b} \in ℝ \land (2 A \in ℝ \land 0 < 2 A)) \to (A Y_{rm} (b + 1) \leq {2 A}^{b} \leftrightarrow 2 A (A Y_{rm} (b + 1)) \leq 2 A {2 A}^{b})$
75	56 67 52 73 74	syl112anc	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to (A Y_{rm} (b + 1) \leq {2 A}^{b} \leftrightarrow 2 A (A Y_{rm} (b + 1)) \leq 2 A {2 A}^{b})$
76	75	biimp3a	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land A Y_{rm} (b + 1) \leq {2 A}^{b}) \to 2 A (A Y_{rm} (b + 1)) \leq 2 A {2 A}^{b}$
77	52	recnd	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to 2 A \in ℂ$
78	77 66	expp1d	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to {2 A}^{b + 1} = {2 A}^{b} 2 A$
79	67	recnd	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to {2 A}^{b} \in ℂ$
80	79 77	mulcomd	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to {2 A}^{b} 2 A = 2 A {2 A}^{b}$
81	78 80	eqtrd	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to {2 A}^{b + 1} = 2 A {2 A}^{b}$
82	81	3adant3	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land A Y_{rm} (b + 1) \leq {2 A}^{b}) \to {2 A}^{b + 1} = 2 A {2 A}^{b}$
83	76 82	breqtrrd	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land A Y_{rm} (b + 1) \leq {2 A}^{b}) \to 2 A (A Y_{rm} (b + 1)) \leq {2 A}^{b + 1}$
84	37	peano2zd	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to b + 1 + 1 \in ℤ$
85	53	fovcl	$⊢ (A \in ℤ_{\geq 2} \land b + 1 + 1 \in ℤ) \to A Y_{rm} (b + 1 + 1) \in ℤ$
86	85	zred	$⊢ (A \in ℤ_{\geq 2} \land b + 1 + 1 \in ℤ) \to A Y_{rm} (b + 1 + 1) \in ℝ$
87	34 84 86	syl2anc	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to A Y_{rm} (b + 1 + 1) \in ℝ$
88		peano2nn0	$⊢ b \in ℕ_{0} \to b + 1 \in ℕ_{0}$
89	88	adantr	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to b + 1 \in ℕ_{0}$
90	52 89	reexpcld	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to {2 A}^{b + 1} \in ℝ$
91		letr	$⊢ (A Y_{rm} (b + 1 + 1) \in ℝ \land 2 A (A Y_{rm} (b + 1)) \in ℝ \land {2 A}^{b + 1} \in ℝ) \to ((A Y_{rm} (b + 1 + 1) \leq 2 A (A Y_{rm} (b + 1)) \land 2 A (A Y_{rm} (b + 1)) \leq {2 A}^{b + 1}) \to A Y_{rm} (b + 1 + 1) \leq {2 A}^{b + 1})$
92	87 57 90 91	syl3anc	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to ((A Y_{rm} (b + 1 + 1) \leq 2 A (A Y_{rm} (b + 1)) \land 2 A (A Y_{rm} (b + 1)) \leq {2 A}^{b + 1}) \to A Y_{rm} (b + 1 + 1) \leq {2 A}^{b + 1})$
93	92	3adant3	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land A Y_{rm} (b + 1) \leq {2 A}^{b}) \to ((A Y_{rm} (b + 1 + 1) \leq 2 A (A Y_{rm} (b + 1)) \land 2 A (A Y_{rm} (b + 1)) \leq {2 A}^{b + 1}) \to A Y_{rm} (b + 1 + 1) \leq {2 A}^{b + 1})$
94	65 83 93	mp2and	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land A Y_{rm} (b + 1) \leq {2 A}^{b}) \to A Y_{rm} (b + 1 + 1) \leq {2 A}^{b + 1}$
95	94	3exp	$⊢ b \in ℕ_{0} \to (A \in ℤ_{\geq 2} \to (A Y_{rm} (b + 1) \leq {2 A}^{b} \to A Y_{rm} (b + 1 + 1) \leq {2 A}^{b + 1}))$
96	95	a2d	$⊢ b \in ℕ_{0} \to ((A \in ℤ_{\geq 2} \to A Y_{rm} (b + 1) \leq {2 A}^{b}) \to (A \in ℤ_{\geq 2} \to A Y_{rm} (b + 1 + 1) \leq {2 A}^{b + 1}))$
97	5 10 15 20 33 96	nn0ind	$⊢ N \in ℕ_{0} \to (A \in ℤ_{\geq 2} \to A Y_{rm} (N + 1) \leq {2 A}^{N})$
98	97	impcom	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0}) \to A Y_{rm} (N + 1) \leq {2 A}^{N}$

Metamath Proof Explorer

Theorem jm2.17b

Proof