basellem8 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > basellem8		Structured version Visualization version GIF version

Theorem basellem8 27054

Description: Lemma for basel 27056. The function 𝐹 of partial sums of the inverse squares is bounded below by 𝐽 and above by 𝐾, obtained by summing the inequality cot↑2𝑥 ≤ 1 / 𝑥↑2 ≤ csc↑2𝑥 = cot↑2𝑥 + 1 over the 𝑀 roots of the polynomial 𝑃, and applying the identity basellem5 27051. (Contributed by Mario Carneiro, 29-Jul-2014.)

**Hypotheses**
Ref	Expression
basel.g	⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1)))
basel.f	⊢ 𝐹 = seq1( + , (𝑛 ∈ ℕ ↦ (𝑛↑-2)))
basel.h	⊢ 𝐻 = ((ℕ × {((π↑2) / 6)}) ∘_f · ((ℕ × {1}) ∘_f − 𝐺))
basel.j	⊢ 𝐽 = (𝐻 ∘_f · ((ℕ × {1}) ∘_f + ((ℕ × {-2}) ∘_f · 𝐺)))
basel.k	⊢ 𝐾 = (𝐻 ∘_f · ((ℕ × {1}) ∘_f + 𝐺))
basellem8.n	⊢ 𝑁 = ((2 · 𝑀) + 1)

**Assertion**
Ref	Expression
basellem8	⊢ (𝑀 ∈ ℕ → ((𝐽‘𝑀) ≤ (𝐹‘𝑀) ∧ (𝐹‘𝑀) ≤ (𝐾‘𝑀)))

Distinct variable groups: 𝑛,𝐹 𝑛,𝑀 𝑛,𝐽 𝑛,𝑁 Allowed substitution hints: 𝐺(𝑛) 𝐻(𝑛) 𝐾(𝑛)

Proof of Theorem basellem8 Dummy variables 𝑘 𝑥 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fzfid 13896	. . . 4 ⊢ (𝑀 ∈ ℕ → (1...𝑀) ∈ Fin)
2		pire 26422	. . . . . . . 8 ⊢ π ∈ ℝ
3		basellem8.n	. . . . . . . . 9 ⊢ 𝑁 = ((2 · 𝑀) + 1)
4		2nn 12218	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ
5		nnmulcl 12169	. . . . . . . . . . 11 ⊢ ((2 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (2 · 𝑀) ∈ ℕ)
6	4, 5	mpan 690	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (2 · 𝑀) ∈ ℕ)
7	6	peano2nnd 12162	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) + 1) ∈ ℕ)
8	3, 7	eqeltrid 2840	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → 𝑁 ∈ ℕ)
9		nndivre 12186	. . . . . . . 8 ⊢ ((π ∈ ℝ ∧ 𝑁 ∈ ℕ) → (π / 𝑁) ∈ ℝ)
10	2, 8, 9	sylancr 587	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (π / 𝑁) ∈ ℝ)
11	10	resqcld 14048	. . . . . 6 ⊢ (𝑀 ∈ ℕ → ((π / 𝑁)↑2) ∈ ℝ)
12	11	adantr 480	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((π / 𝑁)↑2) ∈ ℝ)
13	3	basellem1 27047	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)))
14		tanrpcl 26469	. . . . . . . 8 ⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) → (tan‘((𝑘 · π) / 𝑁)) ∈ ℝ⁺)
15	13, 14	syl 17	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) ∈ ℝ⁺)
16	15	rpred 12949	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) ∈ ℝ)
17	15	rpne0d 12954	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) ≠ 0)
18		2z 12523	. . . . . . . 8 ⊢ 2 ∈ ℤ
19		znegcl 12526	. . . . . . . 8 ⊢ (2 ∈ ℤ → -2 ∈ ℤ)
20	18, 19	ax-mp 5	. . . . . . 7 ⊢ -2 ∈ ℤ
21	20	a1i 11	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → -2 ∈ ℤ)
22	16, 17, 21	reexpclzd 14172	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑-2) ∈ ℝ)
23	12, 22	remulcld 11162	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)) ∈ ℝ)
24		elfznn 13469	. . . . . . 7 ⊢ (𝑘 ∈ (1...𝑀) → 𝑘 ∈ ℕ)
25	24	adantl 481	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℕ)
26	25	nnred 12160	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℝ)
27	25	nnne0d 12195	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ≠ 0)
28	26, 27, 21	reexpclzd 14172	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ∈ ℝ)
29	16	recnd 11160	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) ∈ ℂ)
30		2nn0 12418	. . . . . . . 8 ⊢ 2 ∈ ℕ₀
31		expneg 13992	. . . . . . . 8 ⊢ (((tan‘((𝑘 · π) / 𝑁)) ∈ ℂ ∧ 2 ∈ ℕ₀) → ((tan‘((𝑘 · π) / 𝑁))↑-2) = (1 / ((tan‘((𝑘 · π) / 𝑁))↑2)))
32	29, 30, 31	sylancl 586	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑-2) = (1 / ((tan‘((𝑘 · π) / 𝑁))↑2)))
33	32	oveq2d 7374	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)) = (((π / 𝑁)↑2) · (1 / ((tan‘((𝑘 · π) / 𝑁))↑2))))
34	10	recnd 11160	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (π / 𝑁) ∈ ℂ)
35	34	sqcld 14067	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((π / 𝑁)↑2) ∈ ℂ)
36	35	adantr 480	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((π / 𝑁)↑2) ∈ ℂ)
37		rpexpcl 14003	. . . . . . . . . 10 ⊢ (((tan‘((𝑘 · π) / 𝑁)) ∈ ℝ⁺ ∧ 2 ∈ ℤ) → ((tan‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ⁺)
38	15, 18, 37	sylancl 586	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ⁺)
39	38	rpred 12949	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ)
40	39	recnd 11160	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) ∈ ℂ)
41	38	rpne0d 12954	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) ≠ 0)
42	36, 40, 41	divrecd 11920	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / ((tan‘((𝑘 · π) / 𝑁))↑2)) = (((π / 𝑁)↑2) · (1 / ((tan‘((𝑘 · π) / 𝑁))↑2))))
43	33, 42	eqtr4d 2774	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)) = (((π / 𝑁)↑2) / ((tan‘((𝑘 · π) / 𝑁))↑2)))
44	25	nnrpd 12947	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℝ⁺)
45		rpexpcl 14003	. . . . . . 7 ⊢ ((𝑘 ∈ ℝ⁺ ∧ -2 ∈ ℤ) → (𝑘↑-2) ∈ ℝ⁺)
46	44, 20, 45	sylancl 586	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ∈ ℝ⁺)
47	25	nncnd 12161	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℂ)
48	47, 27, 21	expnegd 14076	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑--2) = (1 / (𝑘↑-2)))
49		2cn 12220	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
50	49	negnegi 11451	. . . . . . . . . . 11 ⊢ --2 = 2
51	50	oveq2i 7369	. . . . . . . . . 10 ⊢ (𝑘↑--2) = (𝑘↑2)
52	48, 51	eqtr3di 2786	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 / (𝑘↑-2)) = (𝑘↑2))
53	52	oveq1d 7373	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((1 / (𝑘↑-2)) · ((π / 𝑁)↑2)) = ((𝑘↑2) · ((π / 𝑁)↑2)))
54		nncn 12153	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
55		nnne0 12179	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 ≠ 0)
56	20	a1i 11	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → -2 ∈ ℤ)
57	54, 55, 56	expclzd 14074	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (𝑘↑-2) ∈ ℂ)
58	25, 57	syl 17	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ∈ ℂ)
59	47, 27, 21	expne0d 14075	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ≠ 0)
60	36, 58, 59	divrec2d 11921	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / (𝑘↑-2)) = ((1 / (𝑘↑-2)) · ((π / 𝑁)↑2)))
61	2	recni 11146	. . . . . . . . . . . 12 ⊢ π ∈ ℂ
62	61	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → π ∈ ℂ)
63	8	nncnd 12161	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → 𝑁 ∈ ℂ)
64	8	nnne0d 12195	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → 𝑁 ≠ 0)
65	63, 64	jca 511	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0))
66	65	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0))
67		divass 11814	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℂ ∧ π ∈ ℂ ∧ (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) → ((𝑘 · π) / 𝑁) = (𝑘 · (π / 𝑁)))
68	47, 62, 66, 67	syl3anc 1373	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) = (𝑘 · (π / 𝑁)))
69	68	oveq1d 7373	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) = ((𝑘 · (π / 𝑁))↑2))
70	34	adantr 480	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (π / 𝑁) ∈ ℂ)
71	47, 70	sqmuld 14081	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · (π / 𝑁))↑2) = ((𝑘↑2) · ((π / 𝑁)↑2)))
72	69, 71	eqtrd 2771	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) = ((𝑘↑2) · ((π / 𝑁)↑2)))
73	53, 60, 72	3eqtr4d 2781	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / (𝑘↑-2)) = (((𝑘 · π) / 𝑁)↑2))
74		elioore 13291	. . . . . . . . . 10 ⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) → ((𝑘 · π) / 𝑁) ∈ ℝ)
75	13, 74	syl 17	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) ∈ ℝ)
76	75	resqcld 14048	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) ∈ ℝ)
77		tangtx 26470	. . . . . . . . . 10 ⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) → ((𝑘 · π) / 𝑁) < (tan‘((𝑘 · π) / 𝑁)))
78	13, 77	syl 17	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) < (tan‘((𝑘 · π) / 𝑁)))
79		eliooord 13321	. . . . . . . . . . . . . 14 ⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) → (0 < ((𝑘 · π) / 𝑁) ∧ ((𝑘 · π) / 𝑁) < (π / 2)))
80	13, 79	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (0 < ((𝑘 · π) / 𝑁) ∧ ((𝑘 · π) / 𝑁) < (π / 2)))
81	80	simpld 494	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 < ((𝑘 · π) / 𝑁))
82	75, 81	elrpd 12946	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) ∈ ℝ⁺)
83	82	rpge0d 12953	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 ≤ ((𝑘 · π) / 𝑁))
84	15	rpge0d 12953	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 ≤ (tan‘((𝑘 · π) / 𝑁)))
85	75, 16, 83, 84	lt2sqd 14179	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁) < (tan‘((𝑘 · π) / 𝑁)) ↔ (((𝑘 · π) / 𝑁)↑2) < ((tan‘((𝑘 · π) / 𝑁))↑2)))
86	78, 85	mpbid 232	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) < ((tan‘((𝑘 · π) / 𝑁))↑2))
87	76, 39, 86	ltled 11281	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) ≤ ((tan‘((𝑘 · π) / 𝑁))↑2))
88	73, 87	eqbrtrd 5120	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / (𝑘↑-2)) ≤ ((tan‘((𝑘 · π) / 𝑁))↑2))
89	12, 46, 38, 88	lediv23d 13017	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / ((tan‘((𝑘 · π) / 𝑁))↑2)) ≤ (𝑘↑-2))
90	43, 89	eqbrtrd 5120	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)) ≤ (𝑘↑-2))
91	1, 23, 28, 90	fsumle 15722	. . 3 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)) ≤ Σ𝑘 ∈ (1...𝑀)(𝑘↑-2))
92		oveq2 7366	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑀 → (2 · 𝑛) = (2 · 𝑀))
93	92	oveq1d 7373	. . . . . . . . . 10 ⊢ (𝑛 = 𝑀 → ((2 · 𝑛) + 1) = ((2 · 𝑀) + 1))
94	93, 3	eqtr4di 2789	. . . . . . . . 9 ⊢ (𝑛 = 𝑀 → ((2 · 𝑛) + 1) = 𝑁)
95	94	oveq2d 7374	. . . . . . . 8 ⊢ (𝑛 = 𝑀 → (1 / ((2 · 𝑛) + 1)) = (1 / 𝑁))
96	95	oveq2d 7374	. . . . . . 7 ⊢ (𝑛 = 𝑀 → (1 − (1 / ((2 · 𝑛) + 1))) = (1 − (1 / 𝑁)))
97	96	oveq2d 7374	. . . . . 6 ⊢ (𝑛 = 𝑀 → (((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) = (((π↑2) / 6) · (1 − (1 / 𝑁))))
98	95	oveq2d 7374	. . . . . . 7 ⊢ (𝑛 = 𝑀 → (-2 · (1 / ((2 · 𝑛) + 1))) = (-2 · (1 / 𝑁)))
99	98	oveq2d 7374	. . . . . 6 ⊢ (𝑛 = 𝑀 → (1 + (-2 · (1 / ((2 · 𝑛) + 1)))) = (1 + (-2 · (1 / 𝑁))))
100	97, 99	oveq12d 7376	. . . . 5 ⊢ (𝑛 = 𝑀 → ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (-2 · (1 / ((2 · 𝑛) + 1))))) = ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))))
101		basel.j	. . . . . 6 ⊢ 𝐽 = (𝐻 ∘_f · ((ℕ × {1}) ∘_f + ((ℕ × {-2}) ∘_f · 𝐺)))
102		nnex 12151	. . . . . . . . 9 ⊢ ℕ ∈ V
103	102	a1i 11	. . . . . . . 8 ⊢ (⊤ → ℕ ∈ V)
104		ovexd 7393	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) ∈ V)
105		ovexd 7393	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 + (-2 · (1 / ((2 · 𝑛) + 1)))) ∈ V)
106		basel.h	. . . . . . . . 9 ⊢ 𝐻 = ((ℕ × {((π↑2) / 6)}) ∘_f · ((ℕ × {1}) ∘_f − 𝐺))
107	2	resqcli 14109	. . . . . . . . . . . 12 ⊢ (π↑2) ∈ ℝ
108		6re 12235	. . . . . . . . . . . 12 ⊢ 6 ∈ ℝ
109		6nn 12234	. . . . . . . . . . . . 13 ⊢ 6 ∈ ℕ
110	109	nnne0i 12185	. . . . . . . . . . . 12 ⊢ 6 ≠ 0
111	107, 108, 110	redivcli 11908	. . . . . . . . . . 11 ⊢ ((π↑2) / 6) ∈ ℝ
112	111	a1i 11	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → ((π↑2) / 6) ∈ ℝ)
113		ovexd 7393	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 − (1 / ((2 · 𝑛) + 1))) ∈ V)
114		fconstmpt 5686	. . . . . . . . . . 11 ⊢ (ℕ × {((π↑2) / 6)}) = (𝑛 ∈ ℕ ↦ ((π↑2) / 6))
115	114	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → (ℕ × {((π↑2) / 6)}) = (𝑛 ∈ ℕ ↦ ((π↑2) / 6)))
116		1zzd 12522	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → 1 ∈ ℤ)
117		ovexd 7393	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 / ((2 · 𝑛) + 1)) ∈ V)
118		fconstmpt 5686	. . . . . . . . . . . 12 ⊢ (ℕ × {1}) = (𝑛 ∈ ℕ ↦ 1)
119	118	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → (ℕ × {1}) = (𝑛 ∈ ℕ ↦ 1))
120		basel.g	. . . . . . . . . . . 12 ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1)))
121	120	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1))))
122	103, 116, 117, 119, 121	offval2 7642	. . . . . . . . . 10 ⊢ (⊤ → ((ℕ × {1}) ∘_f − 𝐺) = (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1)))))
123	103, 112, 113, 115, 122	offval2 7642	. . . . . . . . 9 ⊢ (⊤ → ((ℕ × {((π↑2) / 6)}) ∘_f · ((ℕ × {1}) ∘_f − 𝐺)) = (𝑛 ∈ ℕ ↦ (((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1))))))
124	106, 123	eqtrid 2783	. . . . . . . 8 ⊢ (⊤ → 𝐻 = (𝑛 ∈ ℕ ↦ (((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1))))))
125		ovexd 7393	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (-2 · (1 / ((2 · 𝑛) + 1))) ∈ V)
126	49	negcli 11449	. . . . . . . . . . 11 ⊢ -2 ∈ ℂ
127	126	a1i 11	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → -2 ∈ ℂ)
128		fconstmpt 5686	. . . . . . . . . . 11 ⊢ (ℕ × {-2}) = (𝑛 ∈ ℕ ↦ -2)
129	128	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → (ℕ × {-2}) = (𝑛 ∈ ℕ ↦ -2))
130	103, 127, 117, 129, 121	offval2 7642	. . . . . . . . 9 ⊢ (⊤ → ((ℕ × {-2}) ∘_f · 𝐺) = (𝑛 ∈ ℕ ↦ (-2 · (1 / ((2 · 𝑛) + 1)))))
131	103, 116, 125, 119, 130	offval2 7642	. . . . . . . 8 ⊢ (⊤ → ((ℕ × {1}) ∘_f + ((ℕ × {-2}) ∘_f · 𝐺)) = (𝑛 ∈ ℕ ↦ (1 + (-2 · (1 / ((2 · 𝑛) + 1))))))
132	103, 104, 105, 124, 131	offval2 7642	. . . . . . 7 ⊢ (⊤ → (𝐻 ∘_f · ((ℕ × {1}) ∘_f + ((ℕ × {-2}) ∘_f · 𝐺))) = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (-2 · (1 / ((2 · 𝑛) + 1)))))))
133	132	mptru 1548	. . . . . 6 ⊢ (𝐻 ∘_f · ((ℕ × {1}) ∘_f + ((ℕ × {-2}) ∘_f · 𝐺))) = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (-2 · (1 / ((2 · 𝑛) + 1))))))
134	101, 133	eqtri 2759	. . . . 5 ⊢ 𝐽 = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (-2 · (1 / ((2 · 𝑛) + 1))))))
135		ovex 7391	. . . . 5 ⊢ ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))) ∈ V
136	100, 134, 135	fvmpt 6941	. . . 4 ⊢ (𝑀 ∈ ℕ → (𝐽‘𝑀) = ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))))
137	111	recni 11146	. . . . . . . 8 ⊢ ((π↑2) / 6) ∈ ℂ
138	137	a1i 11	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → ((π↑2) / 6) ∈ ℂ)
139	6	nncnd 12161	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (2 · 𝑀) ∈ ℂ)
140	139, 63, 64	divcld 11917	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) / 𝑁) ∈ ℂ)
141		ax-1cn 11084	. . . . . . . . 9 ⊢ 1 ∈ ℂ
142		subcl 11379	. . . . . . . . 9 ⊢ (((2 · 𝑀) ∈ ℂ ∧ 1 ∈ ℂ) → ((2 · 𝑀) − 1) ∈ ℂ)
143	139, 141, 142	sylancl 586	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) − 1) ∈ ℂ)
144	143, 63, 64	divcld 11917	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) − 1) / 𝑁) ∈ ℂ)
145	138, 140, 144	mulassd 11155	. . . . . 6 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · ((2 · 𝑀) / 𝑁)) · (((2 · 𝑀) − 1) / 𝑁)) = (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁))))
146		1cnd 11127	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → 1 ∈ ℂ)
147	63, 146, 63, 64	divsubdird 11956	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((𝑁 − 1) / 𝑁) = ((𝑁 / 𝑁) − (1 / 𝑁)))
148	3	oveq1i 7368	. . . . . . . . . . 11 ⊢ (𝑁 − 1) = (((2 · 𝑀) + 1) − 1)
149		pncan 11386	. . . . . . . . . . . 12 ⊢ (((2 · 𝑀) ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑀) + 1) − 1) = (2 · 𝑀))
150	139, 141, 149	sylancl 586	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) + 1) − 1) = (2 · 𝑀))
151	148, 150	eqtrid 2783	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁 − 1) = (2 · 𝑀))
152	151	oveq1d 7373	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((𝑁 − 1) / 𝑁) = ((2 · 𝑀) / 𝑁))
153	63, 64	dividd 11915	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁 / 𝑁) = 1)
154	153	oveq1d 7373	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((𝑁 / 𝑁) − (1 / 𝑁)) = (1 − (1 / 𝑁)))
155	147, 152, 154	3eqtr3rd 2780	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (1 − (1 / 𝑁)) = ((2 · 𝑀) / 𝑁))
156	155	oveq2d 7374	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π↑2) / 6) · (1 − (1 / 𝑁))) = (((π↑2) / 6) · ((2 · 𝑀) / 𝑁)))
157	126	a1i 11	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → -2 ∈ ℂ)
158	63, 157, 63, 64	divdird 11955	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((𝑁 + -2) / 𝑁) = ((𝑁 / 𝑁) + (-2 / 𝑁)))
159		negsub 11429	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℂ ∧ 2 ∈ ℂ) → (𝑁 + -2) = (𝑁 − 2))
160	63, 49, 159	sylancl 586	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁 + -2) = (𝑁 − 2))
161		df-2 12208	. . . . . . . . . . . 12 ⊢ 2 = (1 + 1)
162	3, 161	oveq12i 7370	. . . . . . . . . . 11 ⊢ (𝑁 − 2) = (((2 · 𝑀) + 1) − (1 + 1))
163	139, 146, 146	pnpcan2d 11530	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) + 1) − (1 + 1)) = ((2 · 𝑀) − 1))
164	162, 163	eqtrid 2783	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁 − 2) = ((2 · 𝑀) − 1))
165	160, 164	eqtrd 2771	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (𝑁 + -2) = ((2 · 𝑀) − 1))
166	165	oveq1d 7373	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((𝑁 + -2) / 𝑁) = (((2 · 𝑀) − 1) / 𝑁))
167	157, 63, 64	divrecd 11920	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (-2 / 𝑁) = (-2 · (1 / 𝑁)))
168	153, 167	oveq12d 7376	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((𝑁 / 𝑁) + (-2 / 𝑁)) = (1 + (-2 · (1 / 𝑁))))
169	158, 166, 168	3eqtr3rd 2780	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (1 + (-2 · (1 / 𝑁))) = (((2 · 𝑀) − 1) / 𝑁))
170	156, 169	oveq12d 7376	. . . . . 6 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))) = ((((π↑2) / 6) · ((2 · 𝑀) / 𝑁)) · (((2 · 𝑀) − 1) / 𝑁)))
171	8	nnsqcld 14167	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → (𝑁↑2) ∈ ℕ)
172	171	nncnd 12161	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁↑2) ∈ ℂ)
173		6cn 12236	. . . . . . . . . 10 ⊢ 6 ∈ ℂ
174		mulcom 11112	. . . . . . . . . 10 ⊢ (((𝑁↑2) ∈ ℂ ∧ 6 ∈ ℂ) → ((𝑁↑2) · 6) = (6 · (𝑁↑2)))
175	172, 173, 174	sylancl 586	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((𝑁↑2) · 6) = (6 · (𝑁↑2)))
176	175	oveq2d 7374	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / ((𝑁↑2) · 6)) = (((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / (6 · (𝑁↑2))))
177	107	recni 11146	. . . . . . . . . 10 ⊢ (π↑2) ∈ ℂ
178	177	a1i 11	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (π↑2) ∈ ℂ)
179	139, 143	mulcld 11152	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · ((2 · 𝑀) − 1)) ∈ ℂ)
180	171	nnne0d 12195	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁↑2) ≠ 0)
181	172, 180	jca 511	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((𝑁↑2) ∈ ℂ ∧ (𝑁↑2) ≠ 0))
182	173, 110	pm3.2i 470	. . . . . . . . . 10 ⊢ (6 ∈ ℂ ∧ 6 ≠ 0)
183	182	a1i 11	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (6 ∈ ℂ ∧ 6 ≠ 0))
184		divmuldiv 11841	. . . . . . . . 9 ⊢ ((((π↑2) ∈ ℂ ∧ ((2 · 𝑀) · ((2 · 𝑀) − 1)) ∈ ℂ) ∧ (((𝑁↑2) ∈ ℂ ∧ (𝑁↑2) ≠ 0) ∧ (6 ∈ ℂ ∧ 6 ≠ 0))) → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) = (((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / ((𝑁↑2) · 6)))
185	178, 179, 181, 183, 184	syl22anc 838	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) = (((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / ((𝑁↑2) · 6)))
186		divmuldiv 11841	. . . . . . . . 9 ⊢ ((((π↑2) ∈ ℂ ∧ ((2 · 𝑀) · ((2 · 𝑀) − 1)) ∈ ℂ) ∧ ((6 ∈ ℂ ∧ 6 ≠ 0) ∧ ((𝑁↑2) ∈ ℂ ∧ (𝑁↑2) ≠ 0))) → (((π↑2) / 6) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2))) = (((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / (6 · (𝑁↑2))))
187	178, 179, 183, 181, 186	syl22anc 838	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((π↑2) / 6) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2))) = (((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / (6 · (𝑁↑2))))
188	176, 185, 187	3eqtr4d 2781	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) = (((π↑2) / 6) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2))))
189	61	a1i 11	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → π ∈ ℂ)
190	189, 63, 64	sqdivd 14082	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((π / 𝑁)↑2) = ((π↑2) / (𝑁↑2)))
191	190	oveq1d 7373	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) = (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)))
192	139, 63, 143, 63, 64, 64	divmuldivd 11958	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁 · 𝑁)))
193	63	sqvald 14066	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁↑2) = (𝑁 · 𝑁))
194	193	oveq2d 7374	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁 · 𝑁)))
195	192, 194	eqtr4d 2774	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2)))
196	195	oveq2d 7374	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁))) = (((π↑2) / 6) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2))))
197	188, 191, 196	3eqtr4d 2781	. . . . . 6 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) = (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁))))
198	145, 170, 197	3eqtr4d 2781	. . . . 5 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))) = (((π / 𝑁)↑2) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)))
199		eqid 2736	. . . . . . 7 ⊢ (𝑥 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑥↑𝑗))) = (𝑥 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑥↑𝑗)))
200		eqid 2736	. . . . . . 7 ⊢ (𝑛 ∈ (1...𝑀) ↦ ((tan‘((𝑛 · π) / 𝑁))↑-2)) = (𝑛 ∈ (1...𝑀) ↦ ((tan‘((𝑛 · π) / 𝑁))↑-2))
201	3, 199, 200	basellem5 27051	. . . . . 6 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6))
202	201	oveq2d 7374	. . . . 5 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2)) = (((π / 𝑁)↑2) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)))
203	198, 202	eqtr4d 2774	. . . 4 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))) = (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2)))
204	22	recnd 11160	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑-2) ∈ ℂ)
205	1, 35, 204	fsummulc2 15707	. . . 4 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2)) = Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)))
206	136, 203, 205	3eqtrd 2775	. . 3 ⊢ (𝑀 ∈ ℕ → (𝐽‘𝑀) = Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)))
207		basel.f	. . . . 5 ⊢ 𝐹 = seq1( + , (𝑛 ∈ ℕ ↦ (𝑛↑-2)))
208	207	fveq1i 6835	. . . 4 ⊢ (𝐹‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑛↑-2)))‘𝑀)
209		oveq1 7365	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (𝑛↑-2) = (𝑘↑-2))
210		eqid 2736	. . . . . . 7 ⊢ (𝑛 ∈ ℕ ↦ (𝑛↑-2)) = (𝑛 ∈ ℕ ↦ (𝑛↑-2))
211		ovex 7391	. . . . . . 7 ⊢ (𝑘↑-2) ∈ V
212	209, 210, 211	fvmpt 6941	. . . . . 6 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑛↑-2))‘𝑘) = (𝑘↑-2))
213	25, 212	syl 17	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ (𝑛↑-2))‘𝑘) = (𝑘↑-2))
214		id 22	. . . . . 6 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℕ)
215		nnuz 12790	. . . . . 6 ⊢ ℕ = (ℤ_≥‘1)
216	214, 215	eleqtrdi 2846	. . . . 5 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ (ℤ_≥‘1))
217	213, 216, 58	fsumser 15653	. . . 4 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)(𝑘↑-2) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑛↑-2)))‘𝑀))
218	208, 217	eqtr4id 2790	. . 3 ⊢ (𝑀 ∈ ℕ → (𝐹‘𝑀) = Σ𝑘 ∈ (1...𝑀)(𝑘↑-2))
219	91, 206, 218	3brtr4d 5130	. 2 ⊢ (𝑀 ∈ ℕ → (𝐽‘𝑀) ≤ (𝐹‘𝑀))
220	75	resincld 16068	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ∈ ℝ)
221		sincosq1sgn 26463	. . . . . . . . 9 ⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) → (0 < (sin‘((𝑘 · π) / 𝑁)) ∧ 0 < (cos‘((𝑘 · π) / 𝑁))))
222	13, 221	syl 17	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (0 < (sin‘((𝑘 · π) / 𝑁)) ∧ 0 < (cos‘((𝑘 · π) / 𝑁))))
223	222	simpld 494	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 < (sin‘((𝑘 · π) / 𝑁)))
224	223	gt0ne0d 11701	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ≠ 0)
225	220, 224, 21	reexpclzd 14172	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑-2) ∈ ℝ)
226	12, 225	remulcld 11162	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)) ∈ ℝ)
227		sinltx 16114	. . . . . . . . . 10 ⊢ (((𝑘 · π) / 𝑁) ∈ ℝ⁺ → (sin‘((𝑘 · π) / 𝑁)) < ((𝑘 · π) / 𝑁))
228	82, 227	syl 17	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) < ((𝑘 · π) / 𝑁))
229	220, 75, 228	ltled 11281	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ≤ ((𝑘 · π) / 𝑁))
230		0re 11134	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
231		ltle 11221	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ (sin‘((𝑘 · π) / 𝑁)) ∈ ℝ) → (0 < (sin‘((𝑘 · π) / 𝑁)) → 0 ≤ (sin‘((𝑘 · π) / 𝑁))))
232	230, 220, 231	sylancr 587	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (0 < (sin‘((𝑘 · π) / 𝑁)) → 0 ≤ (sin‘((𝑘 · π) / 𝑁))))
233	223, 232	mpd 15	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 ≤ (sin‘((𝑘 · π) / 𝑁)))
234	220, 75, 233, 83	le2sqd 14180	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁)) ≤ ((𝑘 · π) / 𝑁) ↔ ((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((𝑘 · π) / 𝑁)↑2)))
235	229, 234	mpbid 232	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((𝑘 · π) / 𝑁)↑2))
236	235, 73	breqtrrd 5126	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((π / 𝑁)↑2) / (𝑘↑-2)))
237	220	resqcld 14048	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ)
238	237, 12, 46	lemuldiv2d 12999	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘↑-2) · ((sin‘((𝑘 · π) / 𝑁))↑2)) ≤ ((π / 𝑁)↑2) ↔ ((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((π / 𝑁)↑2) / (𝑘↑-2))))
239	220, 223	elrpd 12946	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ∈ ℝ⁺)
240		rpexpcl 14003	. . . . . . . . 9 ⊢ (((sin‘((𝑘 · π) / 𝑁)) ∈ ℝ⁺ ∧ 2 ∈ ℤ) → ((sin‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ⁺)
241	239, 18, 240	sylancl 586	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ⁺)
242	28, 12, 241	lemuldivd 12998	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘↑-2) · ((sin‘((𝑘 · π) / 𝑁))↑2)) ≤ ((π / 𝑁)↑2) ↔ (𝑘↑-2) ≤ (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2))))
243	238, 242	bitr3d 281	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((π / 𝑁)↑2) / (𝑘↑-2)) ↔ (𝑘↑-2) ≤ (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2))))
244	236, 243	mpbid 232	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ≤ (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)))
245	220	recnd 11160	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ∈ ℂ)
246		expneg 13992	. . . . . . . 8 ⊢ (((sin‘((𝑘 · π) / 𝑁)) ∈ ℂ ∧ 2 ∈ ℕ₀) → ((sin‘((𝑘 · π) / 𝑁))↑-2) = (1 / ((sin‘((𝑘 · π) / 𝑁))↑2)))
247	245, 30, 246	sylancl 586	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑-2) = (1 / ((sin‘((𝑘 · π) / 𝑁))↑2)))
248	247	oveq2d 7374	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)) = (((π / 𝑁)↑2) · (1 / ((sin‘((𝑘 · π) / 𝑁))↑2))))
249	237	recnd 11160	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ∈ ℂ)
250	241	rpne0d 12954	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ≠ 0)
251	36, 249, 250	divrecd 11920	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) = (((π / 𝑁)↑2) · (1 / ((sin‘((𝑘 · π) / 𝑁))↑2))))
252	248, 251	eqtr4d 2774	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)) = (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)))
253	244, 252	breqtrrd 5126	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ≤ (((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)))
254	1, 28, 226, 253	fsumle 15722	. . 3 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)(𝑘↑-2) ≤ Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)))
255	95	oveq2d 7374	. . . . . 6 ⊢ (𝑛 = 𝑀 → (1 + (1 / ((2 · 𝑛) + 1))) = (1 + (1 / 𝑁)))
256	97, 255	oveq12d 7376	. . . . 5 ⊢ (𝑛 = 𝑀 → ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (1 / ((2 · 𝑛) + 1)))) = ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁))))
257		basel.k	. . . . . 6 ⊢ 𝐾 = (𝐻 ∘_f · ((ℕ × {1}) ∘_f + 𝐺))
258		ovexd 7393	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 + (1 / ((2 · 𝑛) + 1))) ∈ V)
259	103, 116, 117, 119, 121	offval2 7642	. . . . . . . 8 ⊢ (⊤ → ((ℕ × {1}) ∘_f + 𝐺) = (𝑛 ∈ ℕ ↦ (1 + (1 / ((2 · 𝑛) + 1)))))
260	103, 104, 258, 124, 259	offval2 7642	. . . . . . 7 ⊢ (⊤ → (𝐻 ∘_f · ((ℕ × {1}) ∘_f + 𝐺)) = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (1 / ((2 · 𝑛) + 1))))))
261	260	mptru 1548	. . . . . 6 ⊢ (𝐻 ∘_f · ((ℕ × {1}) ∘_f + 𝐺)) = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (1 / ((2 · 𝑛) + 1)))))
262	257, 261	eqtri 2759	. . . . 5 ⊢ 𝐾 = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (1 / ((2 · 𝑛) + 1)))))
263		ovex 7391	. . . . 5 ⊢ ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁))) ∈ V
264	256, 262, 263	fvmpt 6941	. . . 4 ⊢ (𝑀 ∈ ℕ → (𝐾‘𝑀) = ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁))))
265		peano2cn 11305	. . . . . . . 8 ⊢ (𝑁 ∈ ℂ → (𝑁 + 1) ∈ ℂ)
266	63, 265	syl 17	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (𝑁 + 1) ∈ ℂ)
267	266, 63, 64	divcld 11917	. . . . . 6 ⊢ (𝑀 ∈ ℕ → ((𝑁 + 1) / 𝑁) ∈ ℂ)
268	138, 140, 267	mulassd 11155	. . . . 5 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · ((2 · 𝑀) / 𝑁)) · ((𝑁 + 1) / 𝑁)) = (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁))))
269	63, 146, 63, 64	divdird 11955	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → ((𝑁 + 1) / 𝑁) = ((𝑁 / 𝑁) + (1 / 𝑁)))
270	153	oveq1d 7373	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → ((𝑁 / 𝑁) + (1 / 𝑁)) = (1 + (1 / 𝑁)))
271	269, 270	eqtr2d 2772	. . . . . 6 ⊢ (𝑀 ∈ ℕ → (1 + (1 / 𝑁)) = ((𝑁 + 1) / 𝑁))
272	156, 271	oveq12d 7376	. . . . 5 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁))) = ((((π↑2) / 6) · ((2 · 𝑀) / 𝑁)) · ((𝑁 + 1) / 𝑁)))
273	175	oveq2d 7374	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π↑2) · ((2 · 𝑀) · (𝑁 + 1))) / ((𝑁↑2) · 6)) = (((π↑2) · ((2 · 𝑀) · (𝑁 + 1))) / (6 · (𝑁↑2))))
274	139, 266	mulcld 11152	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · (𝑁 + 1)) ∈ ℂ)
275		divmuldiv 11841	. . . . . . . 8 ⊢ ((((π↑2) ∈ ℂ ∧ ((2 · 𝑀) · (𝑁 + 1)) ∈ ℂ) ∧ (((𝑁↑2) ∈ ℂ ∧ (𝑁↑2) ≠ 0) ∧ (6 ∈ ℂ ∧ 6 ≠ 0))) → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · (𝑁 + 1)) / 6)) = (((π↑2) · ((2 · 𝑀) · (𝑁 + 1))) / ((𝑁↑2) · 6)))
276	178, 274, 181, 183, 275	syl22anc 838	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · (𝑁 + 1)) / 6)) = (((π↑2) · ((2 · 𝑀) · (𝑁 + 1))) / ((𝑁↑2) · 6)))
277		divmuldiv 11841	. . . . . . . 8 ⊢ ((((π↑2) ∈ ℂ ∧ ((2 · 𝑀) · (𝑁 + 1)) ∈ ℂ) ∧ ((6 ∈ ℂ ∧ 6 ≠ 0) ∧ ((𝑁↑2) ∈ ℂ ∧ (𝑁↑2) ≠ 0))) → (((π↑2) / 6) · (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2))) = (((π↑2) · ((2 · 𝑀) · (𝑁 + 1))) / (6 · (𝑁↑2))))
278	178, 274, 183, 181, 277	syl22anc 838	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π↑2) / 6) · (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2))) = (((π↑2) · ((2 · 𝑀) · (𝑁 + 1))) / (6 · (𝑁↑2))))
279	273, 276, 278	3eqtr4d 2781	. . . . . 6 ⊢ (𝑀 ∈ ℕ → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · (𝑁 + 1)) / 6)) = (((π↑2) / 6) · (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2))))
280	75	recoscld 16069	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (cos‘((𝑘 · π) / 𝑁)) ∈ ℝ)
281	280	recnd 11160	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (cos‘((𝑘 · π) / 𝑁)) ∈ ℂ)
282	281	sqcld 14067	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((cos‘((𝑘 · π) / 𝑁))↑2) ∈ ℂ)
283	249, 282, 249, 250	divdird 11955	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((((sin‘((𝑘 · π) / 𝑁))↑2) + ((cos‘((𝑘 · π) / 𝑁))↑2)) / ((sin‘((𝑘 · π) / 𝑁))↑2)) = ((((sin‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) + (((cos‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2))))
284	75	recnd 11160	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) ∈ ℂ)
285		sincossq 16101	. . . . . . . . . . . . . 14 ⊢ (((𝑘 · π) / 𝑁) ∈ ℂ → (((sin‘((𝑘 · π) / 𝑁))↑2) + ((cos‘((𝑘 · π) / 𝑁))↑2)) = 1)
286	284, 285	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((sin‘((𝑘 · π) / 𝑁))↑2) + ((cos‘((𝑘 · π) / 𝑁))↑2)) = 1)
287	286	oveq1d 7373	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((((sin‘((𝑘 · π) / 𝑁))↑2) + ((cos‘((𝑘 · π) / 𝑁))↑2)) / ((sin‘((𝑘 · π) / 𝑁))↑2)) = (1 / ((sin‘((𝑘 · π) / 𝑁))↑2)))
288	249, 250	dividd 11915	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((sin‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) = 1)
289	222	simprd 495	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 < (cos‘((𝑘 · π) / 𝑁)))
290	289	gt0ne0d 11701	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (cos‘((𝑘 · π) / 𝑁)) ≠ 0)
291		tanval 16053	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑘 · π) / 𝑁) ∈ ℂ ∧ (cos‘((𝑘 · π) / 𝑁)) ≠ 0) → (tan‘((𝑘 · π) / 𝑁)) = ((sin‘((𝑘 · π) / 𝑁)) / (cos‘((𝑘 · π) / 𝑁))))
292	284, 290, 291	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) = ((sin‘((𝑘 · π) / 𝑁)) / (cos‘((𝑘 · π) / 𝑁))))
293	292	oveq1d 7373	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) = (((sin‘((𝑘 · π) / 𝑁)) / (cos‘((𝑘 · π) / 𝑁)))↑2))
294	245, 281, 290	sqdivd 14082	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((sin‘((𝑘 · π) / 𝑁)) / (cos‘((𝑘 · π) / 𝑁)))↑2) = (((sin‘((𝑘 · π) / 𝑁))↑2) / ((cos‘((𝑘 · π) / 𝑁))↑2)))
295	293, 294	eqtrd 2771	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) = (((sin‘((𝑘 · π) / 𝑁))↑2) / ((cos‘((𝑘 · π) / 𝑁))↑2)))
296	295	oveq2d 7374	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 / ((tan‘((𝑘 · π) / 𝑁))↑2)) = (1 / (((sin‘((𝑘 · π) / 𝑁))↑2) / ((cos‘((𝑘 · π) / 𝑁))↑2))))
297		sqne0 14046	. . . . . . . . . . . . . . . . 17 ⊢ ((cos‘((𝑘 · π) / 𝑁)) ∈ ℂ → (((cos‘((𝑘 · π) / 𝑁))↑2) ≠ 0 ↔ (cos‘((𝑘 · π) / 𝑁)) ≠ 0))
298	281, 297	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((cos‘((𝑘 · π) / 𝑁))↑2) ≠ 0 ↔ (cos‘((𝑘 · π) / 𝑁)) ≠ 0))
299	290, 298	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((cos‘((𝑘 · π) / 𝑁))↑2) ≠ 0)
300	249, 282, 250, 299	recdivd 11934	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 / (((sin‘((𝑘 · π) / 𝑁))↑2) / ((cos‘((𝑘 · π) / 𝑁))↑2))) = (((cos‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)))
301	32, 296, 300	3eqtrrd 2776	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((cos‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) = ((tan‘((𝑘 · π) / 𝑁))↑-2))
302	288, 301	oveq12d 7376	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((((sin‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) + (((cos‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2))) = (1 + ((tan‘((𝑘 · π) / 𝑁))↑-2)))
303	283, 287, 302	3eqtr3d 2779	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 / ((sin‘((𝑘 · π) / 𝑁))↑2)) = (1 + ((tan‘((𝑘 · π) / 𝑁))↑-2)))
304		addcom 11319	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℂ ∧ ((tan‘((𝑘 · π) / 𝑁))↑-2) ∈ ℂ) → (1 + ((tan‘((𝑘 · π) / 𝑁))↑-2)) = (((tan‘((𝑘 · π) / 𝑁))↑-2) + 1))
305	141, 204, 304	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 + ((tan‘((𝑘 · π) / 𝑁))↑-2)) = (((tan‘((𝑘 · π) / 𝑁))↑-2) + 1))
306	247, 303, 305	3eqtrd 2775	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑-2) = (((tan‘((𝑘 · π) / 𝑁))↑-2) + 1))
307	306	sumeq2dv 15625	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2) = Σ𝑘 ∈ (1...𝑀)(((tan‘((𝑘 · π) / 𝑁))↑-2) + 1))
308		1cnd 11127	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 1 ∈ ℂ)
309	1, 204, 308	fsumadd 15663	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)(((tan‘((𝑘 · π) / 𝑁))↑-2) + 1) = (Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2) + Σ𝑘 ∈ (1...𝑀)1))
310		fsumconst 15713	. . . . . . . . . . . 12 ⊢ (((1...𝑀) ∈ Fin ∧ 1 ∈ ℂ) → Σ𝑘 ∈ (1...𝑀)1 = ((♯‘(1...𝑀)) · 1))
311	1, 141, 310	sylancl 586	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)1 = ((♯‘(1...𝑀)) · 1))
312		nnnn0 12408	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℕ₀)
313		hashfz1 14269	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ₀ → (♯‘(1...𝑀)) = 𝑀)
314	312, 313	syl 17	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → (♯‘(1...𝑀)) = 𝑀)
315	314	oveq1d 7373	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → ((♯‘(1...𝑀)) · 1) = (𝑀 · 1))
316		nncn 12153	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℂ)
317	316	mulridd 11149	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → (𝑀 · 1) = 𝑀)
318	311, 315, 317	3eqtrd 2775	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)1 = 𝑀)
319	201, 318	oveq12d 7376	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2) + Σ𝑘 ∈ (1...𝑀)1) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + 𝑀))
320	307, 309, 319	3eqtrd 2775	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + 𝑀))
321		3cn 12226	. . . . . . . . . . . . 13 ⊢ 3 ∈ ℂ
322	321	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → 3 ∈ ℂ)
323	139, 143, 322	adddid 11156	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · (((2 · 𝑀) − 1) + 3)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) + ((2 · 𝑀) · 3)))
324		df-3 12209	. . . . . . . . . . . . . . . . 17 ⊢ 3 = (2 + 1)
325	324	oveq1i 7368	. . . . . . . . . . . . . . . 16 ⊢ (3 − 1) = ((2 + 1) − 1)
326	49, 141	pncan3oi 11396	. . . . . . . . . . . . . . . 16 ⊢ ((2 + 1) − 1) = 2
327	325, 326, 161	3eqtri 2763	. . . . . . . . . . . . . . 15 ⊢ (3 − 1) = (1 + 1)
328	327	oveq2i 7369	. . . . . . . . . . . . . 14 ⊢ ((2 · 𝑀) + (3 − 1)) = ((2 · 𝑀) + (1 + 1))
329	139, 146, 322	subadd23d 11514	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) − 1) + 3) = ((2 · 𝑀) + (3 − 1)))
330	139, 146, 146	addassd 11154	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) + 1) + 1) = ((2 · 𝑀) + (1 + 1)))
331	328, 329, 330	3eqtr4a 2797	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) − 1) + 3) = (((2 · 𝑀) + 1) + 1))
332	3	oveq1i 7368	. . . . . . . . . . . . 13 ⊢ (𝑁 + 1) = (((2 · 𝑀) + 1) + 1)
333	331, 332	eqtr4di 2789	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) − 1) + 3) = (𝑁 + 1))
334	333	oveq2d 7374	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · (((2 · 𝑀) − 1) + 3)) = ((2 · 𝑀) · (𝑁 + 1)))
335		2cnd 12223	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ → 2 ∈ ℂ)
336	335, 316, 322	mul32d 11343	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · 3) = ((2 · 3) · 𝑀))
337		3t2e6 12306	. . . . . . . . . . . . . . 15 ⊢ (3 · 2) = 6
338	321, 49	mulcomi 11140	. . . . . . . . . . . . . . 15 ⊢ (3 · 2) = (2 · 3)
339	337, 338	eqtr3i 2761	. . . . . . . . . . . . . 14 ⊢ 6 = (2 · 3)
340	339	oveq1i 7368	. . . . . . . . . . . . 13 ⊢ (6 · 𝑀) = ((2 · 3) · 𝑀)
341	336, 340	eqtr4di 2789	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · 3) = (6 · 𝑀))
342	341	oveq2d 7374	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) · ((2 · 𝑀) − 1)) + ((2 · 𝑀) · 3)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) + (6 · 𝑀)))
343	323, 334, 342	3eqtr3d 2779	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · (𝑁 + 1)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) + (6 · 𝑀)))
344	343	oveq1d 7373	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) · (𝑁 + 1)) / 6) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) + (6 · 𝑀)) / 6))
345		mulcl 11110	. . . . . . . . . . 11 ⊢ ((6 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (6 · 𝑀) ∈ ℂ)
346	173, 316, 345	sylancr 587	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (6 · 𝑀) ∈ ℂ)
347	173	a1i 11	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → 6 ∈ ℂ)
348	110	a1i 11	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → 6 ≠ 0)
349	179, 346, 347, 348	divdird 11955	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((((2 · 𝑀) · ((2 · 𝑀) − 1)) + (6 · 𝑀)) / 6) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + ((6 · 𝑀) / 6)))
350	316, 347, 348	divcan3d 11922	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → ((6 · 𝑀) / 6) = 𝑀)
351	350	oveq2d 7374	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + ((6 · 𝑀) / 6)) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + 𝑀))
352	344, 349, 351	3eqtrd 2775	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) · (𝑁 + 1)) / 6) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + 𝑀))
353	320, 352	eqtr4d 2774	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2) = (((2 · 𝑀) · (𝑁 + 1)) / 6))
354	190, 353	oveq12d 7376	. . . . . 6 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2)) = (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · (𝑁 + 1)) / 6)))
355	139, 63, 266, 63, 64, 64	divmuldivd 11958	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁)) = (((2 · 𝑀) · (𝑁 + 1)) / (𝑁 · 𝑁)))
356	193	oveq2d 7374	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2)) = (((2 · 𝑀) · (𝑁 + 1)) / (𝑁 · 𝑁)))
357	355, 356	eqtr4d 2774	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁)) = (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2)))
358	357	oveq2d 7374	. . . . . 6 ⊢ (𝑀 ∈ ℕ → (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁))) = (((π↑2) / 6) · (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2))))
359	279, 354, 358	3eqtr4d 2781	. . . . 5 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2)) = (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁))))
360	268, 272, 359	3eqtr4d 2781	. . . 4 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁))) = (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2)))
361	225	recnd 11160	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑-2) ∈ ℂ)
362	1, 35, 361	fsummulc2 15707	. . . 4 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2)) = Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)))
363	264, 360, 362	3eqtrd 2775	. . 3 ⊢ (𝑀 ∈ ℕ → (𝐾‘𝑀) = Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)))
364	254, 218, 363	3brtr4d 5130	. 2 ⊢ (𝑀 ∈ ℕ → (𝐹‘𝑀) ≤ (𝐾‘𝑀))
365	219, 364	jca 511	1 ⊢ (𝑀 ∈ ℕ → ((𝐽‘𝑀) ≤ (𝐹‘𝑀) ∧ (𝐹‘𝑀) ≤ (𝐾‘𝑀)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1541 ⊤wtru 1542 ∈ wcel 2113 ≠ wne 2932 Vcvv 3440 {csn 4580 class class class wbr 5098 ↦ cmpt 5179 × cxp 5622 ‘cfv 6492 (class class class)co 7358 ∘_f cof 7620 Fincfn 8883 ℂcc 11024 ℝcr 11025 0cc0 11026 1c1 11027 + caddc 11029 · cmul 11031 < clt 11166 ≤ cle 11167 − cmin 11364 -cneg 11365 / cdiv 11794 ℕcn 12145 2c2 12200 3c3 12201 6c6 12204 ℕ₀cn0 12401 ℤcz 12488 ℤ_≥cuz 12751 ℝ⁺crp 12905 (,)cioo 13261 ...cfz 13423 seqcseq 13924 ↑cexp 13984 Ccbc 14225 ♯chash 14253 Σcsu 15609 sincsin 15986 cosccos 15987 tanctan 15988 πcpi 15989

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-inf2 9550 ax-cnex 11082 ax-resscn 11083 ax-1cn 11084 ax-icn 11085 ax-addcl 11086 ax-addrcl 11087 ax-mulcl 11088 ax-mulrcl 11089 ax-mulcom 11090 ax-addass 11091 ax-mulass 11092 ax-distr 11093 ax-i2m1 11094 ax-1ne0 11095 ax-1rid 11096 ax-rnegex 11097 ax-rrecex 11098 ax-cnre 11099 ax-pre-lttri 11100 ax-pre-lttrn 11101 ax-pre-ltadd 11102 ax-pre-mulgt0 11103 ax-pre-sup 11104 ax-addf 11105

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-tp 4585 df-op 4587 df-uni 4864 df-int 4903 df-iun 4948 df-iin 4949 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-se 5578 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-isom 6501 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-of 7622 df-om 7809 df-1st 7933 df-2nd 7934 df-supp 8103 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-1o 8397 df-2o 8398 df-oadd 8401 df-er 8635 df-map 8765 df-pm 8766 df-ixp 8836 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-fsupp 9265 df-fi 9314 df-sup 9345 df-inf 9346 df-oi 9415 df-dju 9813 df-card 9851 df-pnf 11168 df-mnf 11169 df-xr 11170 df-ltxr 11171 df-le 11172 df-sub 11366 df-neg 11367 df-div 11795 df-nn 12146 df-2 12208 df-3 12209 df-4 12210 df-5 12211 df-6 12212 df-7 12213 df-8 12214 df-9 12215 df-n0 12402 df-xnn0 12475 df-z 12489 df-dec 12608 df-uz 12752 df-q 12862 df-rp 12906 df-xneg 13026 df-xadd 13027 df-xmul 13028 df-ioo 13265 df-ioc 13266 df-ico 13267 df-icc 13268 df-fz 13424 df-fzo 13571 df-fl 13712 df-mod 13790 df-seq 13925 df-exp 13985 df-fac 14197 df-bc 14226 df-hash 14254 df-shft 14990 df-cj 15022 df-re 15023 df-im 15024 df-sqrt 15158 df-abs 15159 df-limsup 15394 df-clim 15411 df-rlim 15412 df-sum 15610 df-ef 15990 df-sin 15992 df-cos 15993 df-tan 15994 df-pi 15995 df-struct 17074 df-sets 17091 df-slot 17109 df-ndx 17121 df-base 17137 df-ress 17158 df-plusg 17190 df-mulr 17191 df-starv 17192 df-sca 17193 df-vsca 17194 df-ip 17195 df-tset 17196 df-ple 17197 df-ds 17199 df-unif 17200 df-hom 17201 df-cco 17202 df-rest 17342 df-topn 17343 df-0g 17361 df-gsum 17362 df-topgen 17363 df-pt 17364 df-prds 17367 df-xrs 17423 df-qtop 17428 df-imas 17429 df-xps 17431 df-mre 17505 df-mrc 17506 df-acs 17508 df-mgm 18565 df-sgrp 18644 df-mnd 18660 df-submnd 18709 df-mulg 18998 df-cntz 19246 df-cmn 19711 df-psmet 21301 df-xmet 21302 df-met 21303 df-bl 21304 df-mopn 21305 df-fbas 21306 df-fg 21307 df-cnfld 21310 df-top 22838 df-topon 22855 df-topsp 22877 df-bases 22890 df-cld 22963 df-ntr 22964 df-cls 22965 df-nei 23042 df-lp 23080 df-perf 23081 df-cn 23171 df-cnp 23172 df-haus 23259 df-tx 23506 df-hmeo 23699 df-fil 23790 df-fm 23882 df-flim 23883 df-flf 23884 df-xms 24264 df-ms 24265 df-tms 24266 df-cncf 24827 df-0p 25627 df-limc 25823 df-dv 25824 df-ply 26149 df-idp 26150 df-coe 26151 df-dgr 26152 df-quot 26255

This theorem is referenced by: basellem9 27055

W3C validator