2ap1caineq

Description: Inequality for Theorem 6.6 for AKS. (Contributed by metakunt, 8-Jun-2024)

	Ref	Expression
Hypotheses	2ap1caineq.1	$⊢ φ \to N \in ℤ$
	2ap1caineq.2	$⊢ φ \to 2 \leq N$
Assertion	2ap1caineq	$⊢ φ \to 2^{N + 1} < (\binom{2 \cdot N + 1}{N})$

Proof

Step	Hyp	Ref	Expression
1		2ap1caineq.1	$⊢ φ \to N \in ℤ$
2		2ap1caineq.2	$⊢ φ \to 2 \leq N$
3		oveq1	$⊢ j = 2 \to j + 1 = 2 + 1$
4	3	oveq2d	$⊢ j = 2 \to 2^{j + 1} = 2^{2 + 1}$
5		oveq2	$⊢ j = 2 \to 2 j = 2 \cdot 2$
6	5	oveq1d	$⊢ j = 2 \to 2 j + 1 = 2 \cdot 2 + 1$
7		id	$⊢ j = 2 \to j = 2$
8	6 7	oveq12d	$⊢ j = 2 \to (\binom{2 j + 1}{j}) = (\binom{2 \cdot 2 + 1}{2})$
9	4 8	breq12d	$⊢ j = 2 \to (2^{j + 1} < (\binom{2 j + 1}{j}) \leftrightarrow 2^{2 + 1} < (\binom{2 \cdot 2 + 1}{2}))$
10		oveq1	$⊢ j = k \to j + 1 = k + 1$
11	10	oveq2d	$⊢ j = k \to 2^{j + 1} = 2^{k + 1}$
12		oveq2	$⊢ j = k \to 2 j = 2 k$
13	12	oveq1d	$⊢ j = k \to 2 j + 1 = 2 k + 1$
14		id	$⊢ j = k \to j = k$
15	13 14	oveq12d	$⊢ j = k \to (\binom{2 j + 1}{j}) = (\binom{2 k + 1}{k})$
16	11 15	breq12d	$⊢ j = k \to (2^{j + 1} < (\binom{2 j + 1}{j}) \leftrightarrow 2^{k + 1} < (\binom{2 k + 1}{k}))$
17		oveq1	$⊢ j = k + 1 \to j + 1 = k + 1 + 1$
18	17	oveq2d	$⊢ j = k + 1 \to 2^{j + 1} = 2^{k + 1 + 1}$
19		oveq2	$⊢ j = k + 1 \to 2 j = 2 (k + 1)$
20	19	oveq1d	$⊢ j = k + 1 \to 2 j + 1 = 2 (k + 1) + 1$
21		id	$⊢ j = k + 1 \to j = k + 1$
22	20 21	oveq12d	$⊢ j = k + 1 \to (\binom{2 j + 1}{j}) = (\binom{2 (k + 1) + 1}{k + 1})$
23	18 22	breq12d	$⊢ j = k + 1 \to (2^{j + 1} < (\binom{2 j + 1}{j}) \leftrightarrow 2^{k + 1 + 1} < (\binom{2 (k + 1) + 1}{k + 1}))$
24		oveq1	$⊢ j = N \to j + 1 = N + 1$
25	24	oveq2d	$⊢ j = N \to 2^{j + 1} = 2^{N + 1}$
26		oveq2	$⊢ j = N \to 2 j = 2 \cdot N$
27	26	oveq1d	$⊢ j = N \to 2 j + 1 = 2 \cdot N + 1$
28		id	$⊢ j = N \to j = N$
29	27 28	oveq12d	$⊢ j = N \to (\binom{2 j + 1}{j}) = (\binom{2 \cdot N + 1}{N})$
30	25 29	breq12d	$⊢ j = N \to (2^{j + 1} < (\binom{2 j + 1}{j}) \leftrightarrow 2^{N + 1} < (\binom{2 \cdot N + 1}{N}))$
31		8lt10	$⊢ 8 < 10$
32		eqid	$⊢ 8 = 8$
33		cu2	$⊢ 2^{3} = 8$
34	32 33	eqtr4i	$⊢ 8 = 2^{3}$
35		5bc2eq10	$⊢ (\binom{5}{2}) = 10$
36	35	eqcomi	$⊢ 10 = (\binom{5}{2})$
37	34 36	breq12i	$⊢ 8 < 10 \leftrightarrow 2^{3} < (\binom{5}{2})$
38	31 37	mpbi	$⊢ 2^{3} < (\binom{5}{2})$
39		df-3	$⊢ 3 = 2 + 1$
40	39	oveq2i	$⊢ 2^{3} = 2^{2 + 1}$
41		eqid	$⊢ 5 = 5$
42		2t2e4	$⊢ 2 \cdot 2 = 4$
43	42	oveq1i	$⊢ 2 \cdot 2 + 1 = 4 + 1$
44		4p1e5	$⊢ 4 + 1 = 5$
45	43 44	eqtri	$⊢ 2 \cdot 2 + 1 = 5$
46	41 45	eqtr4i	$⊢ 5 = 2 \cdot 2 + 1$
47	46	oveq1i	$⊢ (\binom{5}{2}) = (\binom{2 \cdot 2 + 1}{2})$
48	40 47	breq12i	$⊢ 2^{3} < (\binom{5}{2}) \leftrightarrow 2^{2 + 1} < (\binom{2 \cdot 2 + 1}{2})$
49	38 48	mpbi	$⊢ 2^{2 + 1} < (\binom{2 \cdot 2 + 1}{2})$
50	49	a1i	$⊢ φ \to 2^{2 + 1} < (\binom{2 \cdot 2 + 1}{2})$
51		2re	$⊢ 2 \in ℝ$
52	51	a1i	$⊢ (φ \land 2^{k + 1} < (\binom{2 k + 1}{k}) \land (k \in ℤ \land 2 \leq k)) \to 2 \in ℝ$
53		simpl	$⊢ (k \in ℤ \land 2 \leq k) \to k \in ℤ$
54		0red	$⊢ (k \in ℤ \land 2 \leq k) \to 0 \in ℝ$
55	51	a1i	$⊢ (k \in ℤ \land 2 \leq k) \to 2 \in ℝ$
56	53	zred	$⊢ (k \in ℤ \land 2 \leq k) \to k \in ℝ$
57		2pos	$⊢ 0 < 2$
58	57	a1i	$⊢ (k \in ℤ \land 2 \leq k) \to 0 < 2$
59		simpr	$⊢ (k \in ℤ \land 2 \leq k) \to 2 \leq k$
60	54 55 56 58 59	ltletrd	$⊢ (k \in ℤ \land 2 \leq k) \to 0 < k$
61	53 60	jca	$⊢ (k \in ℤ \land 2 \leq k) \to (k \in ℤ \land 0 < k)$
62		elnnz	$⊢ k \in ℕ \leftrightarrow (k \in ℤ \land 0 < k)$
63	61 62	sylibr	$⊢ (k \in ℤ \land 2 \leq k) \to k \in ℕ$
64		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
65	63 64	syl	$⊢ (k \in ℤ \land 2 \leq k) \to k \in ℕ_{0}$
66	65	nn0red	$⊢ (k \in ℤ \land 2 \leq k) \to k \in ℝ$
67	54 55 66 58 59	ltletrd	$⊢ (k \in ℤ \land 2 \leq k) \to 0 < k$
68	53 67	jca	$⊢ (k \in ℤ \land 2 \leq k) \to (k \in ℤ \land 0 < k)$
69	68 62	sylibr	$⊢ (k \in ℤ \land 2 \leq k) \to k \in ℕ$
70	69	nnred	$⊢ (k \in ℤ \land 2 \leq k) \to k \in ℝ$
71	70	3ad2ant3	$⊢ (φ \land 2^{k + 1} < (\binom{2 k + 1}{k}) \land (k \in ℤ \land 2 \leq k)) \to k \in ℝ$
72	52 71	remulcld	$⊢ (φ \land 2^{k + 1} < (\binom{2 k + 1}{k}) \land (k \in ℤ \land 2 \leq k)) \to 2 k \in ℝ$
73		3re	$⊢ 3 \in ℝ$
74	73	a1i	$⊢ (φ \land 2^{k + 1} < (\binom{2 k + 1}{k}) \land (k \in ℤ \land 2 \leq k)) \to 3 \in ℝ$
75	72 74	readdcld	$⊢ (φ \land 2^{k + 1} < (\binom{2 k + 1}{k}) \land (k \in ℤ \land 2 \leq k)) \to 2 k + 3 \in ℝ$
76	71 52	readdcld	$⊢ (φ \land 2^{k + 1} < (\binom{2 k + 1}{k}) \land (k \in ℤ \land 2 \leq k)) \to k + 2 \in ℝ$
77	70 55	readdcld	$⊢ (k \in ℤ \land 2 \leq k) \to k + 2 \in ℝ$
78	69	nngt0d	$⊢ (k \in ℤ \land 2 \leq k) \to 0 < k$
79		2rp	$⊢ 2 \in ℝ^{+}$
80	79	a1i	$⊢ (k \in ℤ \land 2 \leq k) \to 2 \in ℝ^{+}$
81	70 80	ltaddrpd	$⊢ (k \in ℤ \land 2 \leq k) \to k < k + 2$
82	54 70 77 78 81	lttrd	$⊢ (k \in ℤ \land 2 \leq k) \to 0 < k + 2$
83	54 82	ltned	$⊢ (k \in ℤ \land 2 \leq k) \to 0 \neq k + 2$
84	83	necomd	$⊢ (k \in ℤ \land 2 \leq k) \to k + 2 \neq 0$
85	84	3ad2ant3	$⊢ (φ \land 2^{k + 1} < (\binom{2 k + 1}{k}) \land (k \in ℤ \land 2 \leq k)) \to k + 2 \neq 0$
86	75 76 85	redivcld	$⊢ (φ \land 2^{k + 1} < (\binom{2 k + 1}{k}) \land (k \in ℤ \land 2 \leq k)) \to \frac{2 k + 3}{k + 2} \in ℝ$
87	52 86	remulcld	$⊢ (φ \land 2^{k + 1} < (\binom{2 k + 1}{k}) \land (k \in ℤ \land 2 \leq k)) \to 2 (\frac{2 k + 3}{k + 2}) \in ℝ$
88		1nn0	$⊢ 1 \in ℕ_{0}$
89	88	a1i	$⊢ (k \in ℤ \land 2 \leq k) \to 1 \in ℕ_{0}$
90	65 89	nn0addcld	$⊢ (k \in ℤ \land 2 \leq k) \to k + 1 \in ℕ_{0}$
91	55 90	reexpcld	$⊢ (k \in ℤ \land 2 \leq k) \to 2^{k + 1} \in ℝ$
92	91	3ad2ant3	$⊢ (φ \land 2^{k + 1} < (\binom{2 k + 1}{k}) \land (k \in ℤ \land 2 \leq k)) \to 2^{k + 1} \in ℝ$
93		2nn0	$⊢ 2 \in ℕ_{0}$
94	93	a1i	$⊢ (k \in ℤ \land 2 \leq k) \to 2 \in ℕ_{0}$
95	94 65	nn0mulcld	$⊢ (k \in ℤ \land 2 \leq k) \to 2 k \in ℕ_{0}$
96	95 89	nn0addcld	$⊢ (k \in ℤ \land 2 \leq k) \to 2 k + 1 \in ℕ_{0}$
97		bccl	$⊢ (2 k + 1 \in ℕ_{0} \land k \in ℤ) \to (\binom{2 k + 1}{k}) \in ℕ_{0}$
98	96 53 97	syl2anc	$⊢ (k \in ℤ \land 2 \leq k) \to (\binom{2 k + 1}{k}) \in ℕ_{0}$
99	98	nn0red	$⊢ (k \in ℤ \land 2 \leq k) \to (\binom{2 k + 1}{k}) \in ℝ$
100	99	3ad2ant3	$⊢ (φ \land 2^{k + 1} < (\binom{2 k + 1}{k}) \land (k \in ℤ \land 2 \leq k)) \to (\binom{2 k + 1}{k}) \in ℝ$
101		0le2	$⊢ 0 \leq 2$
102	101	a1i	$⊢ (φ \land 2^{k + 1} < (\binom{2 k + 1}{k}) \land (k \in ℤ \land 2 \leq k)) \to 0 \leq 2$
103		eqid	$⊢ 2 = 2$
104		2t1e2	$⊢ 2 \cdot 1 = 2$
105	103 104	eqtr4i	$⊢ 2 = 2 \cdot 1$
106	105	a1i	$⊢ (k \in ℤ \land 2 \leq k) \to 2 = 2 \cdot 1$
107		1red	$⊢ (k \in ℤ \land 2 \leq k) \to 1 \in ℝ$
108	55 70	remulcld	$⊢ (k \in ℤ \land 2 \leq k) \to 2 k \in ℝ$
109	73	a1i	$⊢ (k \in ℤ \land 2 \leq k) \to 3 \in ℝ$
110	108 109	readdcld	$⊢ (k \in ℤ \land 2 \leq k) \to 2 k + 3 \in ℝ$
111	110 77 84	redivcld	$⊢ (k \in ℤ \land 2 \leq k) \to \frac{2 k + 3}{k + 2} \in ℝ$
112		nnrp	$⊢ k \in ℕ \to k \in ℝ^{+}$
113	79	a1i	$⊢ k \in ℕ \to 2 \in ℝ^{+}$
114	112 113	rpaddcld	$⊢ k \in ℕ \to k + 2 \in ℝ^{+}$
115	114	rpcnd	$⊢ k \in ℕ \to k + 2 \in ℂ$
116	115	mulid1d	$⊢ k \in ℕ \to (k + 2) \cdot 1 = k + 2$
117		nnre	$⊢ k \in ℕ \to k \in ℝ$
118	51	a1i	$⊢ k \in ℕ \to 2 \in ℝ$
119	118 117	remulcld	$⊢ k \in ℕ \to 2 k \in ℝ$
120	73	a1i	$⊢ k \in ℕ \to 3 \in ℝ$
121	112	rpge0d	$⊢ k \in ℕ \to 0 \leq k$
122		1le2	$⊢ 1 \leq 2$
123	122	a1i	$⊢ k \in ℕ \to 1 \leq 2$
124	117 118 121 123	lemulge12d	$⊢ k \in ℕ \to k \leq 2 k$
125		2lt3	$⊢ 2 < 3$
126	125	a1i	$⊢ k \in ℕ \to 2 < 3$
127	117 118 119 120 124 126	leltaddd	$⊢ k \in ℕ \to k + 2 < 2 k + 3$
128	116 127	eqbrtrd	$⊢ k \in ℕ \to (k + 2) \cdot 1 < 2 k + 3$
129		1red	$⊢ k \in ℕ \to 1 \in ℝ$
130	119 120	readdcld	$⊢ k \in ℕ \to 2 k + 3 \in ℝ$
131	129 130 114	ltmuldiv2d	$⊢ k \in ℕ \to ((k + 2) \cdot 1 < 2 k + 3 \leftrightarrow 1 < \frac{2 k + 3}{k + 2})$
132	128 131	mpbid	$⊢ k \in ℕ \to 1 < \frac{2 k + 3}{k + 2}$
133	69 132	syl	$⊢ (k \in ℤ \land 2 \leq k) \to 1 < \frac{2 k + 3}{k + 2}$
134	107 111 80 133	ltmul2dd	$⊢ (k \in ℤ \land 2 \leq k) \to 2 \cdot 1 < 2 (\frac{2 k + 3}{k + 2})$
135	106 134	eqbrtrd	$⊢ (k \in ℤ \land 2 \leq k) \to 2 < 2 (\frac{2 k + 3}{k + 2})$
136	135	3ad2ant3	$⊢ (φ \land 2^{k + 1} < (\binom{2 k + 1}{k}) \land (k \in ℤ \land 2 \leq k)) \to 2 < 2 (\frac{2 k + 3}{k + 2})$
137	101	a1i	$⊢ (k \in ℤ \land 2 \leq k) \to 0 \leq 2$
138	55 90 137	expge0d	$⊢ (k \in ℤ \land 2 \leq k) \to 0 \leq 2^{k + 1}$
139	138	3ad2ant3	$⊢ (φ \land 2^{k + 1} < (\binom{2 k + 1}{k}) \land (k \in ℤ \land 2 \leq k)) \to 0 \leq 2^{k + 1}$
140		simp2	$⊢ (φ \land 2^{k + 1} < (\binom{2 k + 1}{k}) \land (k \in ℤ \land 2 \leq k)) \to 2^{k + 1} < (\binom{2 k + 1}{k})$
141	52 87 92 100 102 136 139 140	ltmul12ad	$⊢ (φ \land 2^{k + 1} < (\binom{2 k + 1}{k}) \land (k \in ℤ \land 2 \leq k)) \to 2 2^{k + 1} < 2 (\frac{2 k + 3}{k + 2}) (\binom{2 k + 1}{k})$
142		2cnd	$⊢ (k \in ℤ \land 2 \leq k) \to 2 \in ℂ$
143	142 89 90	expaddd	$⊢ (k \in ℤ \land 2 \leq k) \to 2^{k + 1 + 1} = 2^{k + 1} 2^{1}$
144	142 90	expcld	$⊢ (k \in ℤ \land 2 \leq k) \to 2^{k + 1} \in ℂ$
145	142 89	expcld	$⊢ (k \in ℤ \land 2 \leq k) \to 2^{1} \in ℂ$
146	144 145	mulcomd	$⊢ (k \in ℤ \land 2 \leq k) \to 2^{k + 1} 2^{1} = 2^{1} 2^{k + 1}$
147	142	exp1d	$⊢ (k \in ℤ \land 2 \leq k) \to 2^{1} = 2$
148	147	oveq1d	$⊢ (k \in ℤ \land 2 \leq k) \to 2^{1} 2^{k + 1} = 2 2^{k + 1}$
149		eqidd	$⊢ (k \in ℤ \land 2 \leq k) \to 2 2^{k + 1} = 2 2^{k + 1}$
150	146 148 149	3eqtrd	$⊢ (k \in ℤ \land 2 \leq k) \to 2^{k + 1} 2^{1} = 2 2^{k + 1}$
151	143 150	eqtrd	$⊢ (k \in ℤ \land 2 \leq k) \to 2^{k + 1 + 1} = 2 2^{k + 1}$
152	151	eqcomd	$⊢ (k \in ℤ \land 2 \leq k) \to 2 2^{k + 1} = 2^{k + 1 + 1}$
153	152	3ad2ant3	$⊢ (φ \land 2^{k + 1} < (\binom{2 k + 1}{k}) \land (k \in ℤ \land 2 \leq k)) \to 2 2^{k + 1} = 2^{k + 1 + 1}$
154	65	2np3bcnp1	$⊢ (k \in ℤ \land 2 \leq k) \to (\binom{2 (k + 1) + 1}{k + 1}) = (\binom{2 k + 1}{k}) 2 (\frac{2 k + 3}{k + 2})$
155	98	nn0cnd	$⊢ (k \in ℤ \land 2 \leq k) \to (\binom{2 k + 1}{k}) \in ℂ$
156	69	nncnd	$⊢ (k \in ℤ \land 2 \leq k) \to k \in ℂ$
157	142 156	mulcld	$⊢ (k \in ℤ \land 2 \leq k) \to 2 k \in ℂ$
158		3cn	$⊢ 3 \in ℂ$
159	158	a1i	$⊢ (k \in ℤ \land 2 \leq k) \to 3 \in ℂ$
160	157 159	addcld	$⊢ (k \in ℤ \land 2 \leq k) \to 2 k + 3 \in ℂ$
161	156 142	addcld	$⊢ (k \in ℤ \land 2 \leq k) \to k + 2 \in ℂ$
162	160 161 84	divcld	$⊢ (k \in ℤ \land 2 \leq k) \to \frac{2 k + 3}{k + 2} \in ℂ$
163	142 162	mulcld	$⊢ (k \in ℤ \land 2 \leq k) \to 2 (\frac{2 k + 3}{k + 2}) \in ℂ$
164	155 163	mulcomd	$⊢ (k \in ℤ \land 2 \leq k) \to (\binom{2 k + 1}{k}) 2 (\frac{2 k + 3}{k + 2}) = 2 (\frac{2 k + 3}{k + 2}) (\binom{2 k + 1}{k})$
165	154 164	eqtrd	$⊢ (k \in ℤ \land 2 \leq k) \to (\binom{2 (k + 1) + 1}{k + 1}) = 2 (\frac{2 k + 3}{k + 2}) (\binom{2 k + 1}{k})$
166	165	eqcomd	$⊢ (k \in ℤ \land 2 \leq k) \to 2 (\frac{2 k + 3}{k + 2}) (\binom{2 k + 1}{k}) = (\binom{2 (k + 1) + 1}{k + 1})$
167	166	3ad2ant3	$⊢ (φ \land 2^{k + 1} < (\binom{2 k + 1}{k}) \land (k \in ℤ \land 2 \leq k)) \to 2 (\frac{2 k + 3}{k + 2}) (\binom{2 k + 1}{k}) = (\binom{2 (k + 1) + 1}{k + 1})$
168	153 167	breq12d	$⊢ (φ \land 2^{k + 1} < (\binom{2 k + 1}{k}) \land (k \in ℤ \land 2 \leq k)) \to (2 2^{k + 1} < 2 (\frac{2 k + 3}{k + 2}) (\binom{2 k + 1}{k}) \leftrightarrow 2^{k + 1 + 1} < (\binom{2 (k + 1) + 1}{k + 1}))$
169	141 168	mpbid	$⊢ (φ \land 2^{k + 1} < (\binom{2 k + 1}{k}) \land (k \in ℤ \land 2 \leq k)) \to 2^{k + 1 + 1} < (\binom{2 (k + 1) + 1}{k + 1})$
170		2z	$⊢ 2 \in ℤ$
171	170	a1i	$⊢ φ \to 2 \in ℤ$
172	9 16 23 30 50 169 171 1 2	uzindd	$⊢ φ \to 2^{N + 1} < (\binom{2 \cdot N + 1}{N})$

Metamath Proof Explorer

Theorem 2ap1caineq

Proof