basellem1

Description: Lemma for basel . Closure of the sequence of roots. (Contributed by Mario Carneiro, 30-Jul-2014) Replace OLD theorem. (Revised by Wolf Lammen, 18-Sep-2020)

		Ref	Expression
	Hypothesis	basel.n	$⊢ N = 2 \cdot M + 1$
	Assertion	basellem1	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to \frac{K π}{N} \in (0, \frac{π}{2})$

Proof

Step	Hyp	Ref	Expression
1		basel.n	$⊢ N = 2 \cdot M + 1$
2		elfznn	$⊢ K \in (1 \dots M) \to K \in ℕ$
3	2	nnrpd	$⊢ K \in (1 \dots M) \to K \in ℝ^{+}$
4		pirp	$⊢ π \in ℝ^{+}$
5		rpmulcl	$⊢ (K \in ℝ^{+} \land π \in ℝ^{+}) \to K π \in ℝ^{+}$
6	3 4 5	sylancl	$⊢ K \in (1 \dots M) \to K π \in ℝ^{+}$
7		2nn	$⊢ 2 \in ℕ$
8		nnmulcl	$⊢ (2 \in ℕ \land M \in ℕ) \to 2 \cdot M \in ℕ$
9	7 8	mpan	$⊢ M \in ℕ \to 2 \cdot M \in ℕ$
10	9	peano2nnd	$⊢ M \in ℕ \to 2 \cdot M + 1 \in ℕ$
11	1 10	eqeltrid	$⊢ M \in ℕ \to N \in ℕ$
12	11	nnrpd	$⊢ M \in ℕ \to N \in ℝ^{+}$
13		rpdivcl	$⊢ (K π \in ℝ^{+} \land N \in ℝ^{+}) \to \frac{K π}{N} \in ℝ^{+}$
14	6 12 13	syl2anr	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to \frac{K π}{N} \in ℝ^{+}$
15	14	rpred	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to \frac{K π}{N} \in ℝ$
16	14	rpgt0d	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to 0 < \frac{K π}{N}$
17	2	adantl	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to K \in ℕ$
18		nnmulcl	$⊢ (K \in ℕ \land 2 \in ℕ) \to K \cdot 2 \in ℕ$
19	17 7 18	sylancl	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to K \cdot 2 \in ℕ$
20	19	nnred	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to K \cdot 2 \in ℝ$
21	9	adantr	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to 2 \cdot M \in ℕ$
22	21	nnred	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to 2 \cdot M \in ℝ$
23	11	adantr	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to N \in ℕ$
24	23	nnred	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to N \in ℝ$
25	1 24	eqeltrrid	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to 2 \cdot M + 1 \in ℝ$
26	17	nncnd	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to K \in ℂ$
27		2cn	$⊢ 2 \in ℂ$
28		mulcom	$⊢ (K \in ℂ \land 2 \in ℂ) \to K \cdot 2 = 2 K$
29	26 27 28	sylancl	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to K \cdot 2 = 2 K$
30		elfzle2	$⊢ K \in (1 \dots M) \to K \leq M$
31	30	adantl	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to K \leq M$
32	17	nnred	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to K \in ℝ$
33		nnre	$⊢ M \in ℕ \to M \in ℝ$
34	33	adantr	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to M \in ℝ$
35		2re	$⊢ 2 \in ℝ$
36		2pos	$⊢ 0 < 2$
37	35 36	pm3.2i	$⊢ (2 \in ℝ \land 0 < 2)$
38	37	a1i	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to (2 \in ℝ \land 0 < 2)$
39		lemul2	$⊢ (K \in ℝ \land M \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (K \leq M \leftrightarrow 2 K \leq 2 \cdot M)$
40	32 34 38 39	syl3anc	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to (K \leq M \leftrightarrow 2 K \leq 2 \cdot M)$
41	31 40	mpbid	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to 2 K \leq 2 \cdot M$
42	29 41	eqbrtrd	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to K \cdot 2 \leq 2 \cdot M$
43	22	ltp1d	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to 2 \cdot M < 2 \cdot M + 1$
44	20 22 25 42 43	lelttrd	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to K \cdot 2 < 2 \cdot M + 1$
45	44 1	breqtrrdi	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to K \cdot 2 < N$
46	19	nngt0d	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to 0 < K \cdot 2$
47	23	nngt0d	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to 0 < N$
48		pire	$⊢ π \in ℝ$
49		remulcl	$⊢ (K \in ℝ \land π \in ℝ) \to K π \in ℝ$
50	32 48 49	sylancl	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to K π \in ℝ$
51	6	adantl	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to K π \in ℝ^{+}$
52	51	rpgt0d	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to 0 < K π$
53		ltdiv2	$⊢ ((K \cdot 2 \in ℝ \land 0 < K \cdot 2) \land (N \in ℝ \land 0 < N) \land (K π \in ℝ \land 0 < K π)) \to (K \cdot 2 < N \leftrightarrow \frac{K π}{N} < \frac{K π}{K \cdot 2})$
54	20 46 24 47 50 52 53	syl222anc	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to (K \cdot 2 < N \leftrightarrow \frac{K π}{N} < \frac{K π}{K \cdot 2})$
55	45 54	mpbid	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to \frac{K π}{N} < \frac{K π}{K \cdot 2}$
56		picn	$⊢ π \in ℂ$
57	56	a1i	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to π \in ℂ$
58		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
59	58	a1i	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to (2 \in ℂ \land 2 \neq 0)$
60	17	nnne0d	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to K \neq 0$
61		divcan5	$⊢ (π \in ℂ \land (2 \in ℂ \land 2 \neq 0) \land (K \in ℂ \land K \neq 0)) \to \frac{K π}{K \cdot 2} = \frac{π}{2}$
62	57 59 26 60 61	syl112anc	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to \frac{K π}{K \cdot 2} = \frac{π}{2}$
63	55 62	breqtrd	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to \frac{K π}{N} < \frac{π}{2}$
64		0xr	$⊢ 0 \in ℝ^{*}$
65		rehalfcl	$⊢ π \in ℝ \to \frac{π}{2} \in ℝ$
66		rexr	$⊢ \frac{π}{2} \in ℝ \to \frac{π}{2} \in ℝ^{*}$
67	48 65 66	mp2b	$⊢ \frac{π}{2} \in ℝ^{*}$
68		elioo2	$⊢ (0 \in ℝ^{} \land \frac{π}{2} \in ℝ^{}) \to (\frac{K π}{N} \in (0, \frac{π}{2}) \leftrightarrow (\frac{K π}{N} \in ℝ \land 0 < \frac{K π}{N} \land \frac{K π}{N} < \frac{π}{2}))$
69	64 67 68	mp2an	$⊢ \frac{K π}{N} \in (0, \frac{π}{2}) \leftrightarrow (\frac{K π}{N} \in ℝ \land 0 < \frac{K π}{N} \land \frac{K π}{N} < \frac{π}{2})$
70	15 16 63 69	syl3anbrc	$⊢ (M \in ℕ \land K \in (1 \dots M)) \to \frac{K π}{N} \in (0, \frac{π}{2})$

Metamath Proof Explorer

Theorem basellem1

Proof