lcmineqlem20

Description: Inequality for lcm lemma. (Contributed by metakunt, 12-May-2024)

		Ref	Expression
	Hypothesis	lcmineqlem20.1	$⊢ φ \to N \in ℕ$
	Assertion	lcmineqlem20	$⊢ φ \to N 2^{2 \cdot N} \leq \underline{lcm} ((1 \dots 2 \cdot N + 1))$

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem20.1	$⊢ φ \to N \in ℕ$
2	1	nnred	$⊢ φ \to N \in ℝ$
3		2nn0	$⊢ 2 \in ℕ_{0}$
4	3	a1i	$⊢ φ \to 2 \in ℕ_{0}$
5	1	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
6	4 5	nn0mulcld	$⊢ φ \to 2 \cdot N \in ℕ_{0}$
7		2re	$⊢ 2 \in ℝ$
8		reexpcl	$⊢ (2 \in ℝ \land 2 \cdot N \in ℕ_{0}) \to 2^{2 \cdot N} \in ℝ$
9	7 8	mpan	$⊢ 2 \cdot N \in ℕ_{0} \to 2^{2 \cdot N} \in ℝ$
10	6 9	syl	$⊢ φ \to 2^{2 \cdot N} \in ℝ$
11	2 10	remulcld	$⊢ φ \to N 2^{2 \cdot N} \in ℝ$
12	7	a1i	$⊢ φ \to 2 \in ℝ$
13	12 2	remulcld	$⊢ φ \to 2 \cdot N \in ℝ$
14		1red	$⊢ φ \to 1 \in ℝ$
15	13 14	readdcld	$⊢ φ \to 2 \cdot N + 1 \in ℝ$
16		2nn	$⊢ 2 \in ℕ$
17	16	a1i	$⊢ φ \to 2 \in ℕ$
18	17 1	nnmulcld	$⊢ φ \to 2 \cdot N \in ℕ$
19	5	nn0ge0d	$⊢ φ \to 0 \leq N$
20	17	nnge1d	$⊢ φ \to 1 \leq 2$
21	2 12 19 20	lemulge12d	$⊢ φ \to N \leq 2 \cdot N$
22	18 5 21	bccl2d	$⊢ φ \to (\binom{2 \cdot N}{N}) \in ℕ$
23	22	nnred	$⊢ φ \to (\binom{2 \cdot N}{N}) \in ℝ$
24	15 23	remulcld	$⊢ φ \to (2 \cdot N + 1) (\binom{2 \cdot N}{N}) \in ℝ$
25	2 24	remulcld	$⊢ φ \to N (2 \cdot N + 1) (\binom{2 \cdot N}{N}) \in ℝ$
26		fz1ssnn	$⊢ (1 \dots 2 \cdot N + 1) \subseteq ℕ$
27		fzfi	$⊢ (1 \dots 2 \cdot N + 1) \in Fin$
28		lcmfnncl	$⊢ ((1 \dots 2 \cdot N + 1) \subseteq ℕ \land (1 \dots 2 \cdot N + 1) \in Fin) \to \underline{lcm} ((1 \dots 2 \cdot N + 1)) \in ℕ$
29	26 27 28	mp2an	$⊢ \underline{lcm} ((1 \dots 2 \cdot N + 1)) \in ℕ$
30	29	a1i	$⊢ φ \to \underline{lcm} ((1 \dots 2 \cdot N + 1)) \in ℕ$
31	30	nnred	$⊢ φ \to \underline{lcm} ((1 \dots 2 \cdot N + 1)) \in ℝ$
32	5	lcmineqlem17	$⊢ φ \to 2^{2 \cdot N} \leq (2 \cdot N + 1) (\binom{2 \cdot N}{N})$
33	1	nnrpd	$⊢ φ \to N \in ℝ^{+}$
34	10 24 33	lemul2d	$⊢ φ \to (2^{2 \cdot N} \leq (2 \cdot N + 1) (\binom{2 \cdot N}{N}) \leftrightarrow N 2^{2 \cdot N} \leq N (2 \cdot N + 1) (\binom{2 \cdot N}{N}))$
35	32 34	mpbid	$⊢ φ \to N 2^{2 \cdot N} \leq N (2 \cdot N + 1) (\binom{2 \cdot N}{N})$
36	2	recnd	$⊢ φ \to N \in ℂ$
37	15	recnd	$⊢ φ \to 2 \cdot N + 1 \in ℂ$
38	23	recnd	$⊢ φ \to (\binom{2 \cdot N}{N}) \in ℂ$
39	36 37 38	mulassd	$⊢ φ \to N (2 \cdot N + 1) (\binom{2 \cdot N}{N}) = N (2 \cdot N + 1) (\binom{2 \cdot N}{N})$
40	1	lcmineqlem19	$⊢ φ \to N (2 \cdot N + 1) (\binom{2 \cdot N}{N}) ∥ \underline{lcm} ((1 \dots 2 \cdot N + 1))$
41	18	peano2nnd	$⊢ φ \to 2 \cdot N + 1 \in ℕ$
42	1 41	nnmulcld	$⊢ φ \to N (2 \cdot N + 1) \in ℕ$
43	42 22	nnmulcld	$⊢ φ \to N (2 \cdot N + 1) (\binom{2 \cdot N}{N}) \in ℕ$
44	43	nnzd	$⊢ φ \to N (2 \cdot N + 1) (\binom{2 \cdot N}{N}) \in ℤ$
45		dvdsle	$⊢ (N (2 \cdot N + 1) (\binom{2 \cdot N}{N}) \in ℤ \land \underline{lcm} ((1 \dots 2 \cdot N + 1)) \in ℕ) \to (N (2 \cdot N + 1) (\binom{2 \cdot N}{N}) ∥ \underline{lcm} ((1 \dots 2 \cdot N + 1)) \to N (2 \cdot N + 1) (\binom{2 \cdot N}{N}) \leq \underline{lcm} ((1 \dots 2 \cdot N + 1)))$
46	44 30 45	syl2anc	$⊢ φ \to (N (2 \cdot N + 1) (\binom{2 \cdot N}{N}) ∥ \underline{lcm} ((1 \dots 2 \cdot N + 1)) \to N (2 \cdot N + 1) (\binom{2 \cdot N}{N}) \leq \underline{lcm} ((1 \dots 2 \cdot N + 1)))$
47	40 46	mpd	$⊢ φ \to N (2 \cdot N + 1) (\binom{2 \cdot N}{N}) \leq \underline{lcm} ((1 \dots 2 \cdot N + 1))$
48	39 47	eqbrtrrd	$⊢ φ \to N (2 \cdot N + 1) (\binom{2 \cdot N}{N}) \leq \underline{lcm} ((1 \dots 2 \cdot N + 1))$
49	11 25 31 35 48	letrd	$⊢ φ \to N 2^{2 \cdot N} \leq \underline{lcm} ((1 \dots 2 \cdot N + 1))$

Metamath Proof Explorer

Theorem lcmineqlem20

Proof