jm2.17a

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

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ a = 0 \to {(2 A - 1)}^{a} = {(2 A - 1)}^{0}$
2		oveq1	$⊢ a = 0 \to a + 1 = 0 + 1$
3	2	oveq2d	$⊢ a = 0 \to A Y_{rm} (a + 1) = A Y_{rm} (0 + 1)$
4	1 3	breq12d	$⊢ a = 0 \to ({(2 A - 1)}^{a} \leq A Y_{rm} (a + 1) \leftrightarrow {(2 A - 1)}^{0} \leq A Y_{rm} (0 + 1))$
5	4	imbi2d	$⊢ a = 0 \to ((A \in ℤ_{\geq 2} \to {(2 A - 1)}^{a} \leq A Y_{rm} (a + 1)) \leftrightarrow (A \in ℤ_{\geq 2} \to {(2 A - 1)}^{0} \leq A Y_{rm} (0 + 1)))$
6		oveq2	$⊢ a = b \to {(2 A - 1)}^{a} = {(2 A - 1)}^{b}$
7		oveq1	$⊢ a = b \to a + 1 = b + 1$
8	7	oveq2d	$⊢ a = b \to A Y_{rm} (a + 1) = A Y_{rm} (b + 1)$
9	6 8	breq12d	$⊢ a = b \to ({(2 A - 1)}^{a} \leq A Y_{rm} (a + 1) \leftrightarrow {(2 A - 1)}^{b} \leq A Y_{rm} (b + 1))$
10	9	imbi2d	$⊢ a = b \to ((A \in ℤ_{\geq 2} \to {(2 A - 1)}^{a} \leq A Y_{rm} (a + 1)) \leftrightarrow (A \in ℤ_{\geq 2} \to {(2 A - 1)}^{b} \leq A Y_{rm} (b + 1)))$
11		oveq2	$⊢ a = b + 1 \to {(2 A - 1)}^{a} = {(2 A - 1)}^{b + 1}$
12		oveq1	$⊢ a = b + 1 \to a + 1 = b + 1 + 1$
13	12	oveq2d	$⊢ a = b + 1 \to A Y_{rm} (a + 1) = A Y_{rm} (b + 1 + 1)$
14	11 13	breq12d	$⊢ a = b + 1 \to ({(2 A - 1)}^{a} \leq A Y_{rm} (a + 1) \leftrightarrow {(2 A - 1)}^{b + 1} \leq A Y_{rm} (b + 1 + 1))$
15	14	imbi2d	$⊢ a = b + 1 \to ((A \in ℤ_{\geq 2} \to {(2 A - 1)}^{a} \leq A Y_{rm} (a + 1)) \leftrightarrow (A \in ℤ_{\geq 2} \to {(2 A - 1)}^{b + 1} \leq A Y_{rm} (b + 1 + 1)))$
16		oveq2	$⊢ a = N \to {(2 A - 1)}^{a} = {(2 A - 1)}^{N}$
17		oveq1	$⊢ a = N \to a + 1 = N + 1$
18	17	oveq2d	$⊢ a = N \to A Y_{rm} (a + 1) = A Y_{rm} (N + 1)$
19	16 18	breq12d	$⊢ a = N \to ({(2 A - 1)}^{a} \leq A Y_{rm} (a + 1) \leftrightarrow {(2 A - 1)}^{N} \leq A Y_{rm} (N + 1))$
20	19	imbi2d	$⊢ a = N \to ((A \in ℤ_{\geq 2} \to {(2 A - 1)}^{a} \leq A Y_{rm} (a + 1)) \leftrightarrow (A \in ℤ_{\geq 2} \to {(2 A - 1)}^{N} \leq A Y_{rm} (N + 1)))$
21		1le1	$⊢ 1 \leq 1$
22	21	a1i	$⊢ A \in ℤ_{\geq 2} \to 1 \leq 1$
23		2cn	$⊢ 2 \in ℂ$
24		eluzelcn	$⊢ A \in ℤ_{\geq 2} \to A \in ℂ$
25		mulcl	$⊢ (2 \in ℂ \land A \in ℂ) \to 2 A \in ℂ$
26	23 24 25	sylancr	$⊢ A \in ℤ_{\geq 2} \to 2 A \in ℂ$
27		ax-1cn	$⊢ 1 \in ℂ$
28		subcl	$⊢ (2 A \in ℂ \land 1 \in ℂ) \to 2 A - 1 \in ℂ$
29	26 27 28	sylancl	$⊢ A \in ℤ_{\geq 2} \to 2 A - 1 \in ℂ$
30	29	exp0d	$⊢ A \in ℤ_{\geq 2} \to {(2 A - 1)}^{0} = 1$
31		0p1e1	$⊢ 0 + 1 = 1$
32	31	oveq2i	$⊢ A Y_{rm} (0 + 1) = A Y_{rm} 1$
33		rmy1	$⊢ A \in ℤ_{\geq 2} \to A Y_{rm} 1 = 1$
34	32 33	eqtrid	$⊢ A \in ℤ_{\geq 2} \to A Y_{rm} (0 + 1) = 1$
35	22 30 34	3brtr4d	$⊢ A \in ℤ_{\geq 2} \to {(2 A - 1)}^{0} \leq A Y_{rm} (0 + 1)$
36		2re	$⊢ 2 \in ℝ$
37		eluzelre	$⊢ A \in ℤ_{\geq 2} \to A \in ℝ$
38	37	adantl	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to A \in ℝ$
39		remulcl	$⊢ (2 \in ℝ \land A \in ℝ) \to 2 A \in ℝ$
40	36 38 39	sylancr	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to 2 A \in ℝ$
41		1re	$⊢ 1 \in ℝ$
42		resubcl	$⊢ (2 A \in ℝ \land 1 \in ℝ) \to 2 A - 1 \in ℝ$
43	40 41 42	sylancl	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to 2 A - 1 \in ℝ$
44		peano2nn0	$⊢ b \in ℕ_{0} \to b + 1 \in ℕ_{0}$
45	44	adantr	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to b + 1 \in ℕ_{0}$
46	43 45	reexpcld	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to {(2 A - 1)}^{b + 1} \in ℝ$
47	46	3adant3	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land {(2 A - 1)}^{b} \leq A Y_{rm} (b + 1)) \to {(2 A - 1)}^{b + 1} \in ℝ$
48		simpr	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to A \in ℤ_{\geq 2}$
49		nn0z	$⊢ b \in ℕ_{0} \to b \in ℤ$
50	49	adantr	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to b \in ℤ$
51	50	peano2zd	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to b + 1 \in ℤ$
52		frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
53	52	fovcl	$⊢ (A \in ℤ_{\geq 2} \land b + 1 \in ℤ) \to A Y_{rm} (b + 1) \in ℤ$
54	53	zred	$⊢ (A \in ℤ_{\geq 2} \land b + 1 \in ℤ) \to A Y_{rm} (b + 1) \in ℝ$
55	48 51 54	syl2anc	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to A Y_{rm} (b + 1) \in ℝ$
56	55 43	remulcld	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to (A Y_{rm} (b + 1)) (2 A - 1) \in ℝ$
57	56	3adant3	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land {(2 A - 1)}^{b} \leq A Y_{rm} (b + 1)) \to (A Y_{rm} (b + 1)) (2 A - 1) \in ℝ$
58	51	peano2zd	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to b + 1 + 1 \in ℤ$
59	52	fovcl	$⊢ (A \in ℤ_{\geq 2} \land b + 1 + 1 \in ℤ) \to A Y_{rm} (b + 1 + 1) \in ℤ$
60	59	zred	$⊢ (A \in ℤ_{\geq 2} \land b + 1 + 1 \in ℤ) \to A Y_{rm} (b + 1 + 1) \in ℝ$
61	48 58 60	syl2anc	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to A Y_{rm} (b + 1 + 1) \in ℝ$
62	61	3adant3	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land {(2 A - 1)}^{b} \leq A Y_{rm} (b + 1)) \to A Y_{rm} (b + 1 + 1) \in ℝ$
63	29	3ad2ant2	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land {(2 A - 1)}^{b} \leq A Y_{rm} (b + 1)) \to 2 A - 1 \in ℂ$
64		simp1	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land {(2 A - 1)}^{b} \leq A Y_{rm} (b + 1)) \to b \in ℕ_{0}$
65	63 64	expp1d	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land {(2 A - 1)}^{b} \leq A Y_{rm} (b + 1)) \to {(2 A - 1)}^{b + 1} = {(2 A - 1)}^{b} (2 A - 1)$
66		simpl	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to b \in ℕ_{0}$
67	43 66	reexpcld	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to {(2 A - 1)}^{b} \in ℝ$
68		2nn	$⊢ 2 \in ℕ$
69		eluz2nn	$⊢ A \in ℤ_{\geq 2} \to A \in ℕ$
70	69	adantl	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to A \in ℕ$
71		nnmulcl	$⊢ (2 \in ℕ \land A \in ℕ) \to 2 A \in ℕ$
72	68 70 71	sylancr	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to 2 A \in ℕ$
73		nnm1nn0	$⊢ 2 A \in ℕ \to 2 A - 1 \in ℕ_{0}$
74		nn0ge0	$⊢ 2 A - 1 \in ℕ_{0} \to 0 \leq 2 A - 1$
75	72 73 74	3syl	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to 0 \leq 2 A - 1$
76	43 75	jca	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to (2 A - 1 \in ℝ \land 0 \leq 2 A - 1)$
77	67 55 76	3jca	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to ({(2 A - 1)}^{b} \in ℝ \land A Y_{rm} (b + 1) \in ℝ \land (2 A - 1 \in ℝ \land 0 \leq 2 A - 1))$
78		lemul1a	$⊢ (({(2 A - 1)}^{b} \in ℝ \land A Y_{rm} (b + 1) \in ℝ \land (2 A - 1 \in ℝ \land 0 \leq 2 A - 1)) \land {(2 A - 1)}^{b} \leq A Y_{rm} (b + 1)) \to {(2 A - 1)}^{b} (2 A - 1) \leq (A Y_{rm} (b + 1)) (2 A - 1)$
79	77 78	stoic3	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land {(2 A - 1)}^{b} \leq A Y_{rm} (b + 1)) \to {(2 A - 1)}^{b} (2 A - 1) \leq (A Y_{rm} (b + 1)) (2 A - 1)$
80	65 79	eqbrtrd	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land {(2 A - 1)}^{b} \leq A Y_{rm} (b + 1)) \to {(2 A - 1)}^{b + 1} \leq (A Y_{rm} (b + 1)) (2 A - 1)$
81		nn0cn	$⊢ b \in ℕ_{0} \to b \in ℂ$
82	81	adantr	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to b \in ℂ$
83		pncan	$⊢ (b \in ℂ \land 1 \in ℂ) \to b + 1 - 1 = b$
84	82 27 83	sylancl	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to b + 1 - 1 = b$
85	84	oveq2d	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to A Y_{rm} (b + 1 - 1) = A Y_{rm} b$
86	52	fovcl	$⊢ (A \in ℤ_{\geq 2} \land b \in ℤ) \to A Y_{rm} b \in ℤ$
87	86	zred	$⊢ (A \in ℤ_{\geq 2} \land b \in ℤ) \to A Y_{rm} b \in ℝ$
88	48 50 87	syl2anc	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to A Y_{rm} b \in ℝ$
89	85 88	eqeltrd	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to A Y_{rm} (b + 1 - 1) \in ℝ$
90		remulcl	$⊢ (A Y_{rm} (b + 1) \in ℝ \land 1 \in ℝ) \to (A Y_{rm} (b + 1)) \cdot 1 \in ℝ$
91	55 41 90	sylancl	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to (A Y_{rm} (b + 1)) \cdot 1 \in ℝ$
92	40 55	remulcld	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to 2 A (A Y_{rm} (b + 1)) \in ℝ$
93		nn0re	$⊢ b \in ℕ_{0} \to b \in ℝ$
94	93	adantr	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to b \in ℝ$
95	94	lep1d	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to b \leq b + 1$
96		lermy	$⊢ (A \in ℤ_{\geq 2} \land b \in ℤ \land b + 1 \in ℤ) \to (b \leq b + 1 \leftrightarrow A Y_{rm} b \leq A Y_{rm} (b + 1))$
97	48 50 51 96	syl3anc	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to (b \leq b + 1 \leftrightarrow A Y_{rm} b \leq A Y_{rm} (b + 1))$
98	95 97	mpbid	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to A Y_{rm} b \leq A Y_{rm} (b + 1)$
99	55	recnd	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to A Y_{rm} (b + 1) \in ℂ$
100	99	mulridd	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to (A Y_{rm} (b + 1)) \cdot 1 = A Y_{rm} (b + 1)$
101	98 85 100	3brtr4d	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to A Y_{rm} (b + 1 - 1) \leq (A Y_{rm} (b + 1)) \cdot 1$
102	89 91 92 101	lesub2dd	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to 2 A (A Y_{rm} (b + 1)) - (A Y_{rm} (b + 1)) \cdot 1 \leq 2 A (A Y_{rm} (b + 1)) - (A Y_{rm} (b + 1 - 1))$
103	40	recnd	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to 2 A \in ℂ$
104	27	a1i	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to 1 \in ℂ$
105	99 103 104	subdid	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to (A Y_{rm} (b + 1)) (2 A - 1) = (A Y_{rm} (b + 1)) 2 A - (A Y_{rm} (b + 1)) \cdot 1$
106	99 103	mulcomd	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to (A Y_{rm} (b + 1)) 2 A = 2 A (A Y_{rm} (b + 1))$
107	106	oveq1d	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to (A Y_{rm} (b + 1)) 2 A - (A Y_{rm} (b + 1)) \cdot 1 = 2 A (A Y_{rm} (b + 1)) - (A Y_{rm} (b + 1)) \cdot 1$
108	105 107	eqtrd	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to (A Y_{rm} (b + 1)) (2 A - 1) = 2 A (A Y_{rm} (b + 1)) - (A Y_{rm} (b + 1)) \cdot 1$
109		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))$
110	48 51 109	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))$
111	102 108 110	3brtr4d	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to (A Y_{rm} (b + 1)) (2 A - 1) \leq A Y_{rm} (b + 1 + 1)$
112	111	3adant3	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land {(2 A - 1)}^{b} \leq A Y_{rm} (b + 1)) \to (A Y_{rm} (b + 1)) (2 A - 1) \leq A Y_{rm} (b + 1 + 1)$
113	47 57 62 80 112	letrd	$⊢ (b \in ℕ_{0} \land A \in ℤ_{\geq 2} \land {(2 A - 1)}^{b} \leq A Y_{rm} (b + 1)) \to {(2 A - 1)}^{b + 1} \leq A Y_{rm} (b + 1 + 1)$
114	113	3exp	$⊢ b \in ℕ_{0} \to (A \in ℤ_{\geq 2} \to ({(2 A - 1)}^{b} \leq A Y_{rm} (b + 1) \to {(2 A - 1)}^{b + 1} \leq A Y_{rm} (b + 1 + 1)))$
115	114	a2d	$⊢ b \in ℕ_{0} \to ((A \in ℤ_{\geq 2} \to {(2 A - 1)}^{b} \leq A Y_{rm} (b + 1)) \to (A \in ℤ_{\geq 2} \to {(2 A - 1)}^{b + 1} \leq A Y_{rm} (b + 1 + 1)))$
116	5 10 15 20 35 115	nn0ind	$⊢ N \in ℕ_{0} \to (A \in ℤ_{\geq 2} \to {(2 A - 1)}^{N} \leq A Y_{rm} (N + 1))$
117	116	impcom	$⊢ (A \in ℤ_{\geq 2} \land N \in ℕ_{0}) \to {(2 A - 1)}^{N} \leq A Y_{rm} (N + 1)$

Metamath Proof Explorer

Theorem jm2.17a

Proof