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 27397

Description: Lemma for basel 27399. 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 27394. (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 14096	. . . 4 ⊢ (𝑀 ∈ ℕ → (1...𝑀) ∈ Fin)
2		pire 26765	. . . . . . . 8 ⊢ π ∈ ℝ
3		basellem8.n	. . . . . . . . 9 ⊢ 𝑁 = ((2 · 𝑀) + 1)
4		2nn 12397	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ
5		nnmulcl 12340	. . . . . . . . . . 11 ⊢ ((2 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (2 · 𝑀) ∈ ℕ)
6	4, 5	mpan 703	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (2 · 𝑀) ∈ ℕ)
7	6	peano2nnd 12333	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) + 1) ∈ ℕ)
8	3, 7	eqeltrid 2865	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → 𝑁 ∈ ℕ)
9		nndivre 12360	. . . . . . . 8 ⊢ ((π ∈ ℝ ∧ 𝑁 ∈ ℕ) → (π / 𝑁) ∈ ℝ)
10	2, 8, 9	sylancr 599	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (π / 𝑁) ∈ ℝ)
11	10	resqcld 14248	. . . . . 6 ⊢ (𝑀 ∈ ℕ → ((π / 𝑁)↑2) ∈ ℝ)
12	11	adantr 486	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((π / 𝑁)↑2) ∈ ℝ)
13	3	basellem1 27390	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)))
14		tanrpcl 26815	. . . . . . . 8 ⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) → (tan‘((𝑘 · π) / 𝑁)) ∈ ℝ⁺)
15	13, 14	syl 18	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) ∈ ℝ⁺)
16	15	rpred 13145	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) ∈ ℝ)
17	15	rpne0d 13150	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) ≠ 0)
18		2z 12709	. . . . . . . 8 ⊢ 2 ∈ ℤ
19		znegcl 12712	. . . . . . . 8 ⊢ (2 ∈ ℤ → -2 ∈ ℤ)
20	18, 19	ax-mp 5	. . . . . . 7 ⊢ -2 ∈ ℤ
21	20	a1i 11	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → -2 ∈ ℤ)
22	16, 17, 21	reexpclzd 14373	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑-2) ∈ ℝ)
23	12, 22	remulcld 11320	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)) ∈ ℝ)
24		elfznn 13667	. . . . . . 7 ⊢ (𝑘 ∈ (1...𝑀) → 𝑘 ∈ ℕ)
25	24	adantl 487	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℕ)
26	25	nnred 12331	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℝ)
27	25	nnne0d 12369	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ≠ 0)
28	26, 27, 21	reexpclzd 14373	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ∈ ℝ)
29	15	rpcnd 13147	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) ∈ ℂ)
30		2nn0 12604	. . . . . . . 8 ⊢ 2 ∈ ℕ₀
31		expneg 14192	. . . . . . . 8 ⊢ (((tan‘((𝑘 · π) / 𝑁)) ∈ ℂ ∧ 2 ∈ ℕ₀) → ((tan‘((𝑘 · π) / 𝑁))↑-2) = (1 / ((tan‘((𝑘 · π) / 𝑁))↑2)))
32	29, 30, 31	sylancl 598	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑-2) = (1 / ((tan‘((𝑘 · π) / 𝑁))↑2)))
33	32	oveq2d 7428	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)) = (((π / 𝑁)↑2) · (1 / ((tan‘((𝑘 · π) / 𝑁))↑2))))
34	10	recnd 11318	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (π / 𝑁) ∈ ℂ)
35	34	sqcld 14267	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((π / 𝑁)↑2) ∈ ℂ)
36	35	adantr 486	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((π / 𝑁)↑2) ∈ ℂ)
37		rpexpcl 14203	. . . . . . . . 9 ⊢ (((tan‘((𝑘 · π) / 𝑁)) ∈ ℝ⁺ ∧ 2 ∈ ℤ) → ((tan‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ⁺)
38	15, 18, 37	sylancl 598	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ⁺)
39	38	rpcnd 13147	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) ∈ ℂ)
40	38	rpne0d 13150	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) ≠ 0)
41	36, 39, 40	divrecd 12077	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / ((tan‘((𝑘 · π) / 𝑁))↑2)) = (((π / 𝑁)↑2) · (1 / ((tan‘((𝑘 · π) / 𝑁))↑2))))
42	33, 41	eqtr4d 2799	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)) = (((π / 𝑁)↑2) / ((tan‘((𝑘 · π) / 𝑁))↑2)))
43	25	nnrpd 13143	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℝ⁺)
44		rpexpcl 14203	. . . . . . 7 ⊢ ((𝑘 ∈ ℝ⁺ ∧ -2 ∈ ℤ) → (𝑘↑-2) ∈ ℝ⁺)
45	43, 20, 44	sylancl 598	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ∈ ℝ⁺)
46	25	nncnd 12332	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℂ)
47	46, 27, 21	expnegd 14276	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑--2) = (1 / (𝑘↑-2)))
48		2cn 12399	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
49	48	negnegi 11609	. . . . . . . . . . 11 ⊢ --2 = 2
50	49	oveq2i 7423	. . . . . . . . . 10 ⊢ (𝑘↑--2) = (𝑘↑2)
51	47, 50	eqtr3di 2811	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 / (𝑘↑-2)) = (𝑘↑2))
52	51	oveq1d 7427	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((1 / (𝑘↑-2)) · ((π / 𝑁)↑2)) = ((𝑘↑2) · ((π / 𝑁)↑2)))
53		nncn 12324	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
54		nnne0 12353	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 ≠ 0)
55	20	a1i 11	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → -2 ∈ ℤ)
56	53, 54, 55	expclzd 14274	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (𝑘↑-2) ∈ ℂ)
57	25, 56	syl 18	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ∈ ℂ)
58	46, 27, 21	expne0d 14275	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ≠ 0)
59	36, 57, 58	divrec2d 12078	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / (𝑘↑-2)) = ((1 / (𝑘↑-2)) · ((π / 𝑁)↑2)))
60		picn 26767	. . . . . . . . . . . 12 ⊢ π ∈ ℂ
61	60	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → π ∈ ℂ)
62	8	nncnd 12332	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → 𝑁 ∈ ℂ)
63	62	adantr 486	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑁 ∈ ℂ)
64	8	nnne0d 12369	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → 𝑁 ≠ 0)
65	64	adantr 486	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑁 ≠ 0)
66	46, 61, 63, 65	divassd 12109	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) = (𝑘 · (π / 𝑁)))
67	66	oveq1d 7427	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) = ((𝑘 · (π / 𝑁))↑2))
68	34	adantr 486	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (π / 𝑁) ∈ ℂ)
69	46, 68	sqmuld 14281	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · (π / 𝑁))↑2) = ((𝑘↑2) · ((π / 𝑁)↑2)))
70	67, 69	eqtrd 2796	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) = ((𝑘↑2) · ((π / 𝑁)↑2)))
71	52, 59, 70	3eqtr4d 2806	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / (𝑘↑-2)) = (((𝑘 · π) / 𝑁)↑2))
72		elioore 13487	. . . . . . . . . 10 ⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) → ((𝑘 · π) / 𝑁) ∈ ℝ)
73	13, 72	syl 18	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) ∈ ℝ)
74	73	resqcld 14248	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) ∈ ℝ)
75	38	rpred 13145	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ)
76		tangtx 26816	. . . . . . . . . 10 ⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) → ((𝑘 · π) / 𝑁) < (tan‘((𝑘 · π) / 𝑁)))
77	13, 76	syl 18	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) < (tan‘((𝑘 · π) / 𝑁)))
78		eliooord 13517	. . . . . . . . . . . . . 14 ⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) → (0 < ((𝑘 · π) / 𝑁) ∧ ((𝑘 · π) / 𝑁) < (π / 2)))
79	13, 78	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (0 < ((𝑘 · π) / 𝑁) ∧ ((𝑘 · π) / 𝑁) < (π / 2)))
80	79	simpld 500	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 < ((𝑘 · π) / 𝑁))
81	73, 80	elrpd 13142	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) ∈ ℝ⁺)
82	81	rpge0d 13149	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 ≤ ((𝑘 · π) / 𝑁))
83	15	rpge0d 13149	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 ≤ (tan‘((𝑘 · π) / 𝑁)))
84	73, 16, 82, 83	lt2sqd 14380	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁) < (tan‘((𝑘 · π) / 𝑁)) ↔ (((𝑘 · π) / 𝑁)↑2) < ((tan‘((𝑘 · π) / 𝑁))↑2)))
85	77, 84	mpbid 235	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) < ((tan‘((𝑘 · π) / 𝑁))↑2))
86	74, 75, 85	ltled 11439	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) ≤ ((tan‘((𝑘 · π) / 𝑁))↑2))
87	71, 86	eqbrtrd 5127	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / (𝑘↑-2)) ≤ ((tan‘((𝑘 · π) / 𝑁))↑2))
88	12, 45, 38, 87	lediv23d 13213	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / ((tan‘((𝑘 · π) / 𝑁))↑2)) ≤ (𝑘↑-2))
89	42, 88	eqbrtrd 5127	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)) ≤ (𝑘↑-2))
90	1, 23, 28, 89	fsumle 15946	. . 3 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)) ≤ Σ𝑘 ∈ (1...𝑀)(𝑘↑-2))
91		oveq2 7420	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑀 → (2 · 𝑛) = (2 · 𝑀))
92	91	oveq1d 7427	. . . . . . . . . 10 ⊢ (𝑛 = 𝑀 → ((2 · 𝑛) + 1) = ((2 · 𝑀) + 1))
93	92, 3	eqtr4di 2814	. . . . . . . . 9 ⊢ (𝑛 = 𝑀 → ((2 · 𝑛) + 1) = 𝑁)
94	93	oveq2d 7428	. . . . . . . 8 ⊢ (𝑛 = 𝑀 → (1 / ((2 · 𝑛) + 1)) = (1 / 𝑁))
95	94	oveq2d 7428	. . . . . . 7 ⊢ (𝑛 = 𝑀 → (1 − (1 / ((2 · 𝑛) + 1))) = (1 − (1 / 𝑁)))
96	95	oveq2d 7428	. . . . . 6 ⊢ (𝑛 = 𝑀 → (((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) = (((π↑2) / 6) · (1 − (1 / 𝑁))))
97	94	oveq2d 7428	. . . . . . 7 ⊢ (𝑛 = 𝑀 → (-2 · (1 / ((2 · 𝑛) + 1))) = (-2 · (1 / 𝑁)))
98	97	oveq2d 7428	. . . . . 6 ⊢ (𝑛 = 𝑀 → (1 + (-2 · (1 / ((2 · 𝑛) + 1)))) = (1 + (-2 · (1 / 𝑁))))
99	96, 98	oveq12d 7430	. . . . 5 ⊢ (𝑛 = 𝑀 → ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (-2 · (1 / ((2 · 𝑛) + 1))))) = ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))))
100		basel.j	. . . . . 6 ⊢ 𝐽 = (𝐻 ∘_f · ((ℕ × {1}) ∘_f + ((ℕ × {-2}) ∘_f · 𝐺)))
101		nnex 12322	. . . . . . . . 9 ⊢ ℕ ∈ V
102	101	a1i 11	. . . . . . . 8 ⊢ (⊤ → ℕ ∈ V)
103		ovexd 7447	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) ∈ V)
104		ovexd 7447	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 + (-2 · (1 / ((2 · 𝑛) + 1)))) ∈ V)
105		basel.h	. . . . . . . . 9 ⊢ 𝐻 = ((ℕ × {((π↑2) / 6)}) ∘_f · ((ℕ × {1}) ∘_f − 𝐺))
106	2	resqcli 14309	. . . . . . . . . . . 12 ⊢ (π↑2) ∈ ℝ
107		6re 12414	. . . . . . . . . . . 12 ⊢ 6 ∈ ℝ
108		6nn 12413	. . . . . . . . . . . . 13 ⊢ 6 ∈ ℕ
109	108	nnne0i 12359	. . . . . . . . . . . 12 ⊢ 6 ≠ 0
110	106, 107, 109	redivcli 12065	. . . . . . . . . . 11 ⊢ ((π↑2) / 6) ∈ ℝ
111	110	a1i 11	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → ((π↑2) / 6) ∈ ℝ)
112		ovexd 7447	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 − (1 / ((2 · 𝑛) + 1))) ∈ V)
113		fconstmpt 5713	. . . . . . . . . . 11 ⊢ (ℕ × {((π↑2) / 6)}) = (𝑛 ∈ ℕ ↦ ((π↑2) / 6))
114	113	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → (ℕ × {((π↑2) / 6)}) = (𝑛 ∈ ℕ ↦ ((π↑2) / 6)))
115		1zzd 12708	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → 1 ∈ ℤ)
116		ovexd 7447	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 / ((2 · 𝑛) + 1)) ∈ V)
117		fconstmpt 5713	. . . . . . . . . . . 12 ⊢ (ℕ × {1}) = (𝑛 ∈ ℕ ↦ 1)
118	117	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → (ℕ × {1}) = (𝑛 ∈ ℕ ↦ 1))
119		basel.g	. . . . . . . . . . . 12 ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1)))
120	119	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1))))
121	102, 115, 116, 118, 120	offval2 7702	. . . . . . . . . 10 ⊢ (⊤ → ((ℕ × {1}) ∘_f − 𝐺) = (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1)))))
122	102, 111, 112, 114, 121	offval2 7702	. . . . . . . . 9 ⊢ (⊤ → ((ℕ × {((π↑2) / 6)}) ∘_f · ((ℕ × {1}) ∘_f − 𝐺)) = (𝑛 ∈ ℕ ↦ (((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1))))))
123	105, 122	eqtrid 2808	. . . . . . . 8 ⊢ (⊤ → 𝐻 = (𝑛 ∈ ℕ ↦ (((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1))))))
124		ovexd 7447	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (-2 · (1 / ((2 · 𝑛) + 1))) ∈ V)
125	48	negcli 11607	. . . . . . . . . . 11 ⊢ -2 ∈ ℂ
126	125	a1i 11	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → -2 ∈ ℂ)
127		fconstmpt 5713	. . . . . . . . . . 11 ⊢ (ℕ × {-2}) = (𝑛 ∈ ℕ ↦ -2)
128	127	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → (ℕ × {-2}) = (𝑛 ∈ ℕ ↦ -2))
129	102, 126, 116, 128, 120	offval2 7702	. . . . . . . . 9 ⊢ (⊤ → ((ℕ × {-2}) ∘_f · 𝐺) = (𝑛 ∈ ℕ ↦ (-2 · (1 / ((2 · 𝑛) + 1)))))
130	102, 115, 124, 118, 129	offval2 7702	. . . . . . . 8 ⊢ (⊤ → ((ℕ × {1}) ∘_f + ((ℕ × {-2}) ∘_f · 𝐺)) = (𝑛 ∈ ℕ ↦ (1 + (-2 · (1 / ((2 · 𝑛) + 1))))))
131	102, 103, 104, 123, 130	offval2 7702	. . . . . . 7 ⊢ (⊤ → (𝐻 ∘_f · ((ℕ × {1}) ∘_f + ((ℕ × {-2}) ∘_f · 𝐺))) = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (-2 · (1 / ((2 · 𝑛) + 1)))))))
132	131	mptru 1577	. . . . . 6 ⊢ (𝐻 ∘_f · ((ℕ × {1}) ∘_f + ((ℕ × {-2}) ∘_f · 𝐺))) = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (-2 · (1 / ((2 · 𝑛) + 1))))))
133	100, 132	eqtri 2784	. . . . 5 ⊢ 𝐽 = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (-2 · (1 / ((2 · 𝑛) + 1))))))
134		ovex 7445	. . . . 5 ⊢ ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))) ∈ V
135	99, 133, 134	fvmpt 6985	. . . 4 ⊢ (𝑀 ∈ ℕ → (𝐽‘𝑀) = ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))))
136	110	recni 11304	. . . . . . . 8 ⊢ ((π↑2) / 6) ∈ ℂ
137	136	a1i 11	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → ((π↑2) / 6) ∈ ℂ)
138	6	nncnd 12332	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (2 · 𝑀) ∈ ℂ)
139	138, 62, 64	divcld 12074	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) / 𝑁) ∈ ℂ)
140		ax-1cn 11239	. . . . . . . . 9 ⊢ 1 ∈ ℂ
141		subcl 11537	. . . . . . . . 9 ⊢ (((2 · 𝑀) ∈ ℂ ∧ 1 ∈ ℂ) → ((2 · 𝑀) − 1) ∈ ℂ)
142	138, 140, 141	sylancl 598	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) − 1) ∈ ℂ)
143	142, 62, 64	divcld 12074	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) − 1) / 𝑁) ∈ ℂ)
144	137, 139, 143	mulassd 11313	. . . . . 6 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · ((2 · 𝑀) / 𝑁)) · (((2 · 𝑀) − 1) / 𝑁)) = (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁))))
145		1cnd 11283	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → 1 ∈ ℂ)
146	62, 145, 62, 64	divsubdird 12113	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((𝑁 − 1) / 𝑁) = ((𝑁 / 𝑁) − (1 / 𝑁)))
147	3	oveq1i 7422	. . . . . . . . . . 11 ⊢ (𝑁 − 1) = (((2 · 𝑀) + 1) − 1)
148		pncan 11544	. . . . . . . . . . . 12 ⊢ (((2 · 𝑀) ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑀) + 1) − 1) = (2 · 𝑀))
149	138, 140, 148	sylancl 598	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) + 1) − 1) = (2 · 𝑀))
150	147, 149	eqtrid 2808	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁 − 1) = (2 · 𝑀))
151	150	oveq1d 7427	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((𝑁 − 1) / 𝑁) = ((2 · 𝑀) / 𝑁))
152	62, 64	dividd 12072	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁 / 𝑁) = 1)
153	152	oveq1d 7427	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((𝑁 / 𝑁) − (1 / 𝑁)) = (1 − (1 / 𝑁)))
154	146, 151, 153	3eqtr3rd 2805	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (1 − (1 / 𝑁)) = ((2 · 𝑀) / 𝑁))
155	154	oveq2d 7428	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π↑2) / 6) · (1 − (1 / 𝑁))) = (((π↑2) / 6) · ((2 · 𝑀) / 𝑁)))
156	125	a1i 11	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → -2 ∈ ℂ)
157	62, 156, 62, 64	divdird 12112	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((𝑁 + -2) / 𝑁) = ((𝑁 / 𝑁) + (-2 / 𝑁)))
158		negsub 11587	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℂ ∧ 2 ∈ ℂ) → (𝑁 + -2) = (𝑁 − 2))
159	62, 48, 158	sylancl 598	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁 + -2) = (𝑁 − 2))
160		df-2 12386	. . . . . . . . . . . 12 ⊢ 2 = (1 + 1)
161	3, 160	oveq12i 7424	. . . . . . . . . . 11 ⊢ (𝑁 − 2) = (((2 · 𝑀) + 1) − (1 + 1))
162	138, 145, 145	pnpcan2d 11688	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) + 1) − (1 + 1)) = ((2 · 𝑀) − 1))
163	161, 162	eqtrid 2808	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁 − 2) = ((2 · 𝑀) − 1))
164	159, 163	eqtrd 2796	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (𝑁 + -2) = ((2 · 𝑀) − 1))
165	164	oveq1d 7427	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((𝑁 + -2) / 𝑁) = (((2 · 𝑀) − 1) / 𝑁))
166	156, 62, 64	divrecd 12077	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (-2 / 𝑁) = (-2 · (1 / 𝑁)))
167	152, 166	oveq12d 7430	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((𝑁 / 𝑁) + (-2 / 𝑁)) = (1 + (-2 · (1 / 𝑁))))
168	157, 165, 167	3eqtr3rd 2805	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (1 + (-2 · (1 / 𝑁))) = (((2 · 𝑀) − 1) / 𝑁))
169	155, 168	oveq12d 7430	. . . . . 6 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))) = ((((π↑2) / 6) · ((2 · 𝑀) / 𝑁)) · (((2 · 𝑀) − 1) / 𝑁)))
170	8	nnsqcld 14368	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → (𝑁↑2) ∈ ℕ)
171	170	nncnd 12332	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁↑2) ∈ ℂ)
172		6cn 12415	. . . . . . . . . . 11 ⊢ 6 ∈ ℂ
173	172	a1i 11	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → 6 ∈ ℂ)
174	171, 173	mulcomd 11311	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((𝑁↑2) · 6) = (6 · (𝑁↑2)))
175	174	oveq2d 7428	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / ((𝑁↑2) · 6)) = (((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / (6 · (𝑁↑2))))
176	106	recni 11304	. . . . . . . . . 10 ⊢ (π↑2) ∈ ℂ
177	176	a1i 11	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (π↑2) ∈ ℂ)
178	138, 142	mulcld 11310	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · ((2 · 𝑀) − 1)) ∈ ℂ)
179	170	nnne0d 12369	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁↑2) ≠ 0)
180	171, 179	jca 521	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((𝑁↑2) ∈ ℂ ∧ (𝑁↑2) ≠ 0))
181	172, 109	pm3.2i 476	. . . . . . . . . 10 ⊢ (6 ∈ ℂ ∧ 6 ≠ 0)
182	181	a1i 11	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (6 ∈ ℂ ∧ 6 ≠ 0))
183		divmuldiv 11998	. . . . . . . . 9 ⊢ ((((π↑2) ∈ ℂ ∧ ((2 · 𝑀) · ((2 · 𝑀) − 1)) ∈ ℂ) ∧ (((𝑁↑2) ∈ ℂ ∧ (𝑁↑2) ≠ 0) ∧ (6 ∈ ℂ ∧ 6 ≠ 0))) → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) = (((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / ((𝑁↑2) · 6)))
184	177, 178, 180, 182, 183	syl22anc 852	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) = (((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / ((𝑁↑2) · 6)))
185		divmuldiv 11998	. . . . . . . . 9 ⊢ ((((π↑2) ∈ ℂ ∧ ((2 · 𝑀) · ((2 · 𝑀) − 1)) ∈ ℂ) ∧ ((6 ∈ ℂ ∧ 6 ≠ 0) ∧ ((𝑁↑2) ∈ ℂ ∧ (𝑁↑2) ≠ 0))) → (((π↑2) / 6) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2))) = (((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / (6 · (𝑁↑2))))
186	177, 178, 182, 180, 185	syl22anc 852	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((π↑2) / 6) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2))) = (((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / (6 · (𝑁↑2))))
187	175, 184, 186	3eqtr4d 2806	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) = (((π↑2) / 6) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2))))
188	60	a1i 11	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → π ∈ ℂ)
189	188, 62, 64	sqdivd 14282	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((π / 𝑁)↑2) = ((π↑2) / (𝑁↑2)))
190	189	oveq1d 7427	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) = (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)))
191	138, 62, 142, 62, 64, 64	divmuldivd 12115	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁 · 𝑁)))
192	62	sqvald 14266	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁↑2) = (𝑁 · 𝑁))
193	192	oveq2d 7428	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁 · 𝑁)))
194	191, 193	eqtr4d 2799	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2)))
195	194	oveq2d 7428	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁))) = (((π↑2) / 6) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2))))
196	187, 190, 195	3eqtr4d 2806	. . . . . 6 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) = (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁))))
197	144, 169, 196	3eqtr4d 2806	. . . . 5 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))) = (((π / 𝑁)↑2) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)))
198		eqid 2761	. . . . . . 7 ⊢ (𝑥 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑥↑𝑗))) = (𝑥 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑥↑𝑗)))
199		eqid 2761	. . . . . . 7 ⊢ (𝑛 ∈ (1...𝑀) ↦ ((tan‘((𝑛 · π) / 𝑁))↑-2)) = (𝑛 ∈ (1...𝑀) ↦ ((tan‘((𝑛 · π) / 𝑁))↑-2))
200	3, 198, 199	basellem5 27394	. . . . . 6 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6))
201	200	oveq2d 7428	. . . . 5 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2)) = (((π / 𝑁)↑2) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)))
202	197, 201	eqtr4d 2799	. . . 4 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))) = (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2)))
203	22	recnd 11318	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑-2) ∈ ℂ)
204	1, 35, 203	fsummulc2 15930	. . . 4 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2)) = Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)))
205	135, 202, 204	3eqtrd 2800	. . 3 ⊢ (𝑀 ∈ ℕ → (𝐽‘𝑀) = Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)))
206		basel.f	. . . . 5 ⊢ 𝐹 = seq1( + , (𝑛 ∈ ℕ ↦ (𝑛↑-2)))
207	206	fveq1i 6878	. . . 4 ⊢ (𝐹‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑛↑-2)))‘𝑀)
208		oveq1 7419	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (𝑛↑-2) = (𝑘↑-2))
209		eqid 2761	. . . . . . 7 ⊢ (𝑛 ∈ ℕ ↦ (𝑛↑-2)) = (𝑛 ∈ ℕ ↦ (𝑛↑-2))
210		ovex 7445	. . . . . . 7 ⊢ (𝑘↑-2) ∈ V
211	208, 209, 210	fvmpt 6985	. . . . . 6 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑛↑-2))‘𝑘) = (𝑘↑-2))
212	25, 211	syl 18	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ (𝑛↑-2))‘𝑘) = (𝑘↑-2))
213		id 23	. . . . . 6 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℕ)
214		nnuz 12985	. . . . . 6 ⊢ ℕ = (ℤ_≥‘1)
215	213, 214	eleqtrdi 2871	. . . . 5 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ (ℤ_≥‘1))
216	212, 215, 57	fsumser 15876	. . . 4 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)(𝑘↑-2) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑛↑-2)))‘𝑀))
217	207, 216	eqtr4id 2815	. . 3 ⊢ (𝑀 ∈ ℕ → (𝐹‘𝑀) = Σ𝑘 ∈ (1...𝑀)(𝑘↑-2))
218	90, 205, 217	3brtr4d 5137	. 2 ⊢ (𝑀 ∈ ℕ → (𝐽‘𝑀) ≤ (𝐹‘𝑀))
219	73	resincld 16291	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ∈ ℝ)
220		sincosq1sgn 26809	. . . . . . . . 9 ⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) → (0 < (sin‘((𝑘 · π) / 𝑁)) ∧ 0 < (cos‘((𝑘 · π) / 𝑁))))
221	13, 220	syl 18	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (0 < (sin‘((𝑘 · π) / 𝑁)) ∧ 0 < (cos‘((𝑘 · π) / 𝑁))))
222	221	simpld 500	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 < (sin‘((𝑘 · π) / 𝑁)))
223	222	gt0ne0d 11861	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ≠ 0)
224	219, 223, 21	reexpclzd 14373	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑-2) ∈ ℝ)
225	12, 224	remulcld 11320	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)) ∈ ℝ)
226		sinltx 16337	. . . . . . . . . 10 ⊢ (((𝑘 · π) / 𝑁) ∈ ℝ⁺ → (sin‘((𝑘 · π) / 𝑁)) < ((𝑘 · π) / 𝑁))
227	81, 226	syl 18	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) < ((𝑘 · π) / 𝑁))
228	219, 73, 227	ltled 11439	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ≤ ((𝑘 · π) / 𝑁))
229		0re 11291	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
230		ltle 11379	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ (sin‘((𝑘 · π) / 𝑁)) ∈ ℝ) → (0 < (sin‘((𝑘 · π) / 𝑁)) → 0 ≤ (sin‘((𝑘 · π) / 𝑁))))
231	229, 219, 230	sylancr 599	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (0 < (sin‘((𝑘 · π) / 𝑁)) → 0 ≤ (sin‘((𝑘 · π) / 𝑁))))
232	222, 231	mpd 16	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 ≤ (sin‘((𝑘 · π) / 𝑁)))
233	219, 73, 232, 82	le2sqd 14381	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁)) ≤ ((𝑘 · π) / 𝑁) ↔ ((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((𝑘 · π) / 𝑁)↑2)))
234	228, 233	mpbid 235	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((𝑘 · π) / 𝑁)↑2))
235	234, 71	breqtrrd 5133	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((π / 𝑁)↑2) / (𝑘↑-2)))
236	219	resqcld 14248	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ)
237	236, 12, 45	lemuldiv2d 13195	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘↑-2) · ((sin‘((𝑘 · π) / 𝑁))↑2)) ≤ ((π / 𝑁)↑2) ↔ ((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((π / 𝑁)↑2) / (𝑘↑-2))))
238	219, 222	elrpd 13142	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ∈ ℝ⁺)
239		rpexpcl 14203	. . . . . . . . 9 ⊢ (((sin‘((𝑘 · π) / 𝑁)) ∈ ℝ⁺ ∧ 2 ∈ ℤ) → ((sin‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ⁺)
240	238, 18, 239	sylancl 598	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ⁺)
241	28, 12, 240	lemuldivd 13194	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘↑-2) · ((sin‘((𝑘 · π) / 𝑁))↑2)) ≤ ((π / 𝑁)↑2) ↔ (𝑘↑-2) ≤ (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2))))
242	237, 241	bitr3d 284	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((π / 𝑁)↑2) / (𝑘↑-2)) ↔ (𝑘↑-2) ≤ (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2))))
243	235, 242	mpbid 235	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ≤ (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)))
244	219	recnd 11318	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ∈ ℂ)
245		expneg 14192	. . . . . . . 8 ⊢ (((sin‘((𝑘 · π) / 𝑁)) ∈ ℂ ∧ 2 ∈ ℕ₀) → ((sin‘((𝑘 · π) / 𝑁))↑-2) = (1 / ((sin‘((𝑘 · π) / 𝑁))↑2)))
246	244, 30, 245	sylancl 598	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑-2) = (1 / ((sin‘((𝑘 · π) / 𝑁))↑2)))
247	246	oveq2d 7428	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)) = (((π / 𝑁)↑2) · (1 / ((sin‘((𝑘 · π) / 𝑁))↑2))))
248	236	recnd 11318	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ∈ ℂ)
249	240	rpne0d 13150	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ≠ 0)
250	36, 248, 249	divrecd 12077	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) = (((π / 𝑁)↑2) · (1 / ((sin‘((𝑘 · π) / 𝑁))↑2))))
251	247, 250	eqtr4d 2799	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)) = (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)))
252	243, 251	breqtrrd 5133	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ≤ (((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)))
253	1, 28, 225, 252	fsumle 15946	. . 3 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)(𝑘↑-2) ≤ Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)))
254	94	oveq2d 7428	. . . . . 6 ⊢ (𝑛 = 𝑀 → (1 + (1 / ((2 · 𝑛) + 1))) = (1 + (1 / 𝑁)))
255	96, 254	oveq12d 7430	. . . . 5 ⊢ (𝑛 = 𝑀 → ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (1 / ((2 · 𝑛) + 1)))) = ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁))))
256		basel.k	. . . . . 6 ⊢ 𝐾 = (𝐻 ∘_f · ((ℕ × {1}) ∘_f + 𝐺))
257		ovexd 7447	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 + (1 / ((2 · 𝑛) + 1))) ∈ V)
258	102, 115, 116, 118, 120	offval2 7702	. . . . . . . 8 ⊢ (⊤ → ((ℕ × {1}) ∘_f + 𝐺) = (𝑛 ∈ ℕ ↦ (1 + (1 / ((2 · 𝑛) + 1)))))
259	102, 103, 257, 123, 258	offval2 7702	. . . . . . 7 ⊢ (⊤ → (𝐻 ∘_f · ((ℕ × {1}) ∘_f + 𝐺)) = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (1 / ((2 · 𝑛) + 1))))))
260	259	mptru 1577	. . . . . 6 ⊢ (𝐻 ∘_f · ((ℕ × {1}) ∘_f + 𝐺)) = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (1 / ((2 · 𝑛) + 1)))))
261	256, 260	eqtri 2784	. . . . 5 ⊢ 𝐾 = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (1 / ((2 · 𝑛) + 1)))))
262		ovex 7445	. . . . 5 ⊢ ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁))) ∈ V
263	255, 261, 262	fvmpt 6985	. . . 4 ⊢ (𝑀 ∈ ℕ → (𝐾‘𝑀) = ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁))))
264		peano2cn 11463	. . . . . . . 8 ⊢ (𝑁 ∈ ℂ → (𝑁 + 1) ∈ ℂ)
265	62, 264	syl 18	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (𝑁 + 1) ∈ ℂ)
266	265, 62, 64	divcld 12074	. . . . . 6 ⊢ (𝑀 ∈ ℕ → ((𝑁 + 1) / 𝑁) ∈ ℂ)
267	137, 139, 266	mulassd 11313	. . . . 5 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · ((2 · 𝑀) / 𝑁)) · ((𝑁 + 1) / 𝑁)) = (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁))))
268	62, 145, 62, 64	divdird 12112	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → ((𝑁 + 1) / 𝑁) = ((𝑁 / 𝑁) + (1 / 𝑁)))
269	152	oveq1d 7427	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → ((𝑁 / 𝑁) + (1 / 𝑁)) = (1 + (1 / 𝑁)))
270	268, 269	eqtr2d 2797	. . . . . 6 ⊢ (𝑀 ∈ ℕ → (1 + (1 / 𝑁)) = ((𝑁 + 1) / 𝑁))
271	155, 270	oveq12d 7430	. . . . 5 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁))) = ((((π↑2) / 6) · ((2 · 𝑀) / 𝑁)) · ((𝑁 + 1) / 𝑁)))
272	174	oveq2d 7428	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π↑2) · ((2 · 𝑀) · (𝑁 + 1))) / ((𝑁↑2) · 6)) = (((π↑2) · ((2 · 𝑀) · (𝑁 + 1))) / (6 · (𝑁↑2))))
273	138, 265	mulcld 11310	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · (𝑁 + 1)) ∈ ℂ)
274		divmuldiv 11998	. . . . . . . 8 ⊢ ((((π↑2) ∈ ℂ ∧ ((2 · 𝑀) · (𝑁 + 1)) ∈ ℂ) ∧ (((𝑁↑2) ∈ ℂ ∧ (𝑁↑2) ≠ 0) ∧ (6 ∈ ℂ ∧ 6 ≠ 0))) → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · (𝑁 + 1)) / 6)) = (((π↑2) · ((2 · 𝑀) · (𝑁 + 1))) / ((𝑁↑2) · 6)))
275	177, 273, 180, 182, 274	syl22anc 852	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · (𝑁 + 1)) / 6)) = (((π↑2) · ((2 · 𝑀) · (𝑁 + 1))) / ((𝑁↑2) · 6)))
276		divmuldiv 11998	. . . . . . . 8 ⊢ ((((π↑2) ∈ ℂ ∧ ((2 · 𝑀) · (𝑁 + 1)) ∈ ℂ) ∧ ((6 ∈ ℂ ∧ 6 ≠ 0) ∧ ((𝑁↑2) ∈ ℂ ∧ (𝑁↑2) ≠ 0))) → (((π↑2) / 6) · (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2))) = (((π↑2) · ((2 · 𝑀) · (𝑁 + 1))) / (6 · (𝑁↑2))))
277	177, 273, 182, 180, 276	syl22anc 852	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π↑2) / 6) · (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2))) = (((π↑2) · ((2 · 𝑀) · (𝑁 + 1))) / (6 · (𝑁↑2))))
278	272, 275, 277	3eqtr4d 2806	. . . . . 6 ⊢ (𝑀 ∈ ℕ → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · (𝑁 + 1)) / 6)) = (((π↑2) / 6) · (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2))))
279	73	recoscld 16292	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (cos‘((𝑘 · π) / 𝑁)) ∈ ℝ)
280	279	recnd 11318	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (cos‘((𝑘 · π) / 𝑁)) ∈ ℂ)
281	280	sqcld 14267	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((cos‘((𝑘 · π) / 𝑁))↑2) ∈ ℂ)
282	248, 281, 248, 249	divdird 12112	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((((sin‘((𝑘 · π) / 𝑁))↑2) + ((cos‘((𝑘 · π) / 𝑁))↑2)) / ((sin‘((𝑘 · π) / 𝑁))↑2)) = ((((sin‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) + (((cos‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2))))
283	73	recnd 11318	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) ∈ ℂ)
284		sincossq 16324	. . . . . . . . . . . . . 14 ⊢ (((𝑘 · π) / 𝑁) ∈ ℂ → (((sin‘((𝑘 · π) / 𝑁))↑2) + ((cos‘((𝑘 · π) / 𝑁))↑2)) = 1)
285	283, 284	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((sin‘((𝑘 · π) / 𝑁))↑2) + ((cos‘((𝑘 · π) / 𝑁))↑2)) = 1)
286	285	oveq1d 7427	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((((sin‘((𝑘 · π) / 𝑁))↑2) + ((cos‘((𝑘 · π) / 𝑁))↑2)) / ((sin‘((𝑘 · π) / 𝑁))↑2)) = (1 / ((sin‘((𝑘 · π) / 𝑁))↑2)))
287	248, 249	dividd 12072	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((sin‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) = 1)
288	221	simprd 501	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 < (cos‘((𝑘 · π) / 𝑁)))
289	288	gt0ne0d 11861	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (cos‘((𝑘 · π) / 𝑁)) ≠ 0)
290		tanval 16276	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑘 · π) / 𝑁) ∈ ℂ ∧ (cos‘((𝑘 · π) / 𝑁)) ≠ 0) → (tan‘((𝑘 · π) / 𝑁)) = ((sin‘((𝑘 · π) / 𝑁)) / (cos‘((𝑘 · π) / 𝑁))))
291	283, 289, 290	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) = ((sin‘((𝑘 · π) / 𝑁)) / (cos‘((𝑘 · π) / 𝑁))))
292	291	oveq1d 7427	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) = (((sin‘((𝑘 · π) / 𝑁)) / (cos‘((𝑘 · π) / 𝑁)))↑2))
293	244, 280, 289	sqdivd 14282	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((sin‘((𝑘 · π) / 𝑁)) / (cos‘((𝑘 · π) / 𝑁)))↑2) = (((sin‘((𝑘 · π) / 𝑁))↑2) / ((cos‘((𝑘 · π) / 𝑁))↑2)))
294	292, 293	eqtrd 2796	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) = (((sin‘((𝑘 · π) / 𝑁))↑2) / ((cos‘((𝑘 · π) / 𝑁))↑2)))
295	294	oveq2d 7428	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 / ((tan‘((𝑘 · π) / 𝑁))↑2)) = (1 / (((sin‘((𝑘 · π) / 𝑁))↑2) / ((cos‘((𝑘 · π) / 𝑁))↑2))))
296		sqne0 14246	. . . . . . . . . . . . . . . . 17 ⊢ ((cos‘((𝑘 · π) / 𝑁)) ∈ ℂ → (((cos‘((𝑘 · π) / 𝑁))↑2) ≠ 0 ↔ (cos‘((𝑘 · π) / 𝑁)) ≠ 0))
297	280, 296	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((cos‘((𝑘 · π) / 𝑁))↑2) ≠ 0 ↔ (cos‘((𝑘 · π) / 𝑁)) ≠ 0))
298	289, 297	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((cos‘((𝑘 · π) / 𝑁))↑2) ≠ 0)
299	248, 281, 249, 298	recdivd 12091	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 / (((sin‘((𝑘 · π) / 𝑁))↑2) / ((cos‘((𝑘 · π) / 𝑁))↑2))) = (((cos‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)))
300	32, 295, 299	3eqtrrd 2801	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((cos‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) = ((tan‘((𝑘 · π) / 𝑁))↑-2))
301	287, 300	oveq12d 7430	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((((sin‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) + (((cos‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2))) = (1 + ((tan‘((𝑘 · π) / 𝑁))↑-2)))
302	282, 286, 301	3eqtr3d 2804	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 / ((sin‘((𝑘 · π) / 𝑁))↑2)) = (1 + ((tan‘((𝑘 · π) / 𝑁))↑-2)))
303		addcom 11477	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℂ ∧ ((tan‘((𝑘 · π) / 𝑁))↑-2) ∈ ℂ) → (1 + ((tan‘((𝑘 · π) / 𝑁))↑-2)) = (((tan‘((𝑘 · π) / 𝑁))↑-2) + 1))
304	140, 203, 303	sylancr 599	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 + ((tan‘((𝑘 · π) / 𝑁))↑-2)) = (((tan‘((𝑘 · π) / 𝑁))↑-2) + 1))
305	246, 302, 304	3eqtrd 2800	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑-2) = (((tan‘((𝑘 · π) / 𝑁))↑-2) + 1))
306	305	sumeq2dv 15849	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2) = Σ𝑘 ∈ (1...𝑀)(((tan‘((𝑘 · π) / 𝑁))↑-2) + 1))
307		1cnd 11283	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 1 ∈ ℂ)
308	1, 203, 307	fsumadd 15886	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)(((tan‘((𝑘 · π) / 𝑁))↑-2) + 1) = (Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2) + Σ𝑘 ∈ (1...𝑀)1))
309		fsumconst 15936	. . . . . . . . . . . 12 ⊢ (((1...𝑀) ∈ Fin ∧ 1 ∈ ℂ) → Σ𝑘 ∈ (1...𝑀)1 = ((♯‘(1...𝑀)) · 1))
310	1, 140, 309	sylancl 598	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)1 = ((♯‘(1...𝑀)) · 1))
311		nnnn0 12594	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℕ₀)
312		hashfz1 14470	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ₀ → (♯‘(1...𝑀)) = 𝑀)
313	311, 312	syl 18	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → (♯‘(1...𝑀)) = 𝑀)
314	313	oveq1d 7427	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → ((♯‘(1...𝑀)) · 1) = (𝑀 · 1))
315		nncn 12324	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℂ)
316	315	mulridd 11307	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → (𝑀 · 1) = 𝑀)
317	310, 314, 316	3eqtrd 2800	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)1 = 𝑀)
318	200, 317	oveq12d 7430	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2) + Σ𝑘 ∈ (1...𝑀)1) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + 𝑀))
319	306, 308, 318	3eqtrd 2800	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + 𝑀))
320		3cn 12405	. . . . . . . . . . . . 13 ⊢ 3 ∈ ℂ
321	320	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → 3 ∈ ℂ)
322	138, 142, 321	adddid 11314	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · (((2 · 𝑀) − 1) + 3)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) + ((2 · 𝑀) · 3)))
323		3m1e2 12451	. . . . . . . . . . . . . . . 16 ⊢ (3 − 1) = 2
324	323, 160	eqtri 2784	. . . . . . . . . . . . . . 15 ⊢ (3 − 1) = (1 + 1)
325	324	oveq2i 7423	. . . . . . . . . . . . . 14 ⊢ ((2 · 𝑀) + (3 − 1)) = ((2 · 𝑀) + (1 + 1))
326	138, 145, 321	subadd23d 11672	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) − 1) + 3) = ((2 · 𝑀) + (3 − 1)))
327	138, 145, 145	addassd 11312	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) + 1) + 1) = ((2 · 𝑀) + (1 + 1)))
328	325, 326, 327	3eqtr4a 2822	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) − 1) + 3) = (((2 · 𝑀) + 1) + 1))
329	3	oveq1i 7422	. . . . . . . . . . . . 13 ⊢ (𝑁 + 1) = (((2 · 𝑀) + 1) + 1)
330	328, 329	eqtr4di 2814	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) − 1) + 3) = (𝑁 + 1))
331	330	oveq2d 7428	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · (((2 · 𝑀) − 1) + 3)) = ((2 · 𝑀) · (𝑁 + 1)))
332		2cnd 12402	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ → 2 ∈ ℂ)
333	332, 315, 321	mul32d 11501	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · 3) = ((2 · 3) · 𝑀))
334		2t3e6 12490	. . . . . . . . . . . . . 14 ⊢ (2 · 3) = 6
335	334	oveq1i 7422	. . . . . . . . . . . . 13 ⊢ ((2 · 3) · 𝑀) = (6 · 𝑀)
336	333, 335	eqtrdi 2812	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · 3) = (6 · 𝑀))
337	336	oveq2d 7428	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) · ((2 · 𝑀) − 1)) + ((2 · 𝑀) · 3)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) + (6 · 𝑀)))
338	322, 331, 337	3eqtr3d 2804	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · (𝑁 + 1)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) + (6 · 𝑀)))
339	338	oveq1d 7427	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) · (𝑁 + 1)) / 6) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) + (6 · 𝑀)) / 6))
340		mulcl 11265	. . . . . . . . . . 11 ⊢ ((6 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (6 · 𝑀) ∈ ℂ)
341	172, 315, 340	sylancr 599	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (6 · 𝑀) ∈ ℂ)
342	109	a1i 11	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → 6 ≠ 0)
343	178, 341, 173, 342	divdird 12112	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((((2 · 𝑀) · ((2 · 𝑀) − 1)) + (6 · 𝑀)) / 6) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + ((6 · 𝑀) / 6)))
344	315, 173, 342	divcan3d 12079	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → ((6 · 𝑀) / 6) = 𝑀)
345	344	oveq2d 7428	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + ((6 · 𝑀) / 6)) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + 𝑀))
346	339, 343, 345	3eqtrd 2800	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) · (𝑁 + 1)) / 6) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + 𝑀))
347	319, 346	eqtr4d 2799	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2) = (((2 · 𝑀) · (𝑁 + 1)) / 6))
348	189, 347	oveq12d 7430	. . . . . 6 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2)) = (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · (𝑁 + 1)) / 6)))
349	138, 62, 265, 62, 64, 64	divmuldivd 12115	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁)) = (((2 · 𝑀) · (𝑁 + 1)) / (𝑁 · 𝑁)))
350	192	oveq2d 7428	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2)) = (((2 · 𝑀) · (𝑁 + 1)) / (𝑁 · 𝑁)))
351	349, 350	eqtr4d 2799	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁)) = (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2)))
352	351	oveq2d 7428	. . . . . 6 ⊢ (𝑀 ∈ ℕ → (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁))) = (((π↑2) / 6) · (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2))))
353	278, 348, 352	3eqtr4d 2806	. . . . 5 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2)) = (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁))))
354	267, 271, 353	3eqtr4d 2806	. . . 4 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁))) = (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2)))
355	224	recnd 11318	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑-2) ∈ ℂ)
356	1, 35, 355	fsummulc2 15930	. . . 4 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2)) = Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)))
357	263, 354, 356	3eqtrd 2800	. . 3 ⊢ (𝑀 ∈ ℕ → (𝐾‘𝑀) = Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)))
358	253, 217, 357	3brtr4d 5137	. 2 ⊢ (𝑀 ∈ ℕ → (𝐹‘𝑀) ≤ (𝐾‘𝑀))
359	218, 358	jca 521	1 ⊢ (𝑀 ∈ ℕ → ((𝐽‘𝑀) ≤ (𝐹‘𝑀) ∧ (𝐹‘𝑀) ≤ (𝐾‘𝑀)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ⊤wtru 1571 ∈ wcel 2145 ≠ wne 2956 Vcvv 3451 {csn 4584 class class class wbr 5103 ↦ cmpt 5186 × cxp 5649 ‘cfv 6531 (class class class)co 7412 ∘_f cof 7680 Fincfn 8957 ℂcc 11179 ℝcr 11180 0cc0 11181 1c1 11182 + caddc 11184 · cmul 11186 < clt 11324 ≤ cle 11325 − cmin 11522 -cneg 11523 / cdiv 11954 ℕcn 12316 2c2 12378 3c3 12379 6c6 12382 ℕ₀cn0 12587 ℤcz 12674 ℤ_≥cuz 12946 ℝ⁺crp 13101 (,)cioo 13457 ...cfz 13620 seqcseq 14124 ↑cexp 14184 Ccbc 14426 ♯chash 14454 Σcsu 15833 sincsin 16209 cosccos 16210 tanctan 16211 πcpi 16212

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7740 ax-inf2 9626 ax-cnex 11237 ax-resscn 11238 ax-1cn 11239 ax-icn 11240 ax-addcl 11241 ax-addrcl 11242 ax-mulcl 11243 ax-mulrcl 11244 ax-mulcom 11245 ax-addass 11246 ax-mulass 11247 ax-distr 11248 ax-i2m1 11249 ax-1ne0 11250 ax-1rid 11251 ax-rnegex 11252 ax-rrecex 11253 ax-cnre 11254 ax-pre-lttri 11255 ax-pre-lttrn 11256 ax-pre-ltadd 11257 ax-pre-mulgt0 11258 ax-pre-sup 11259 ax-addf 11260

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6297 df-ord 6358 df-on 6359 df-lim 6360 df-suc 6361 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-isom 6540 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-of 7682 df-om 7867 df-1st 7990 df-2nd 7991 df-supp 8162 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8460 df-2o 8461 df-oadd 8464 df-er 8701 df-map 8833 df-pm 8834 df-ixp 8910 df-en 8958 df-dom 8959 df-sdom 8960 df-fin 8961 df-fsupp 9338 df-fi 9387 df-sup 9418 df-inf 9419 df-oi 9488 df-dju 9963 df-card 10001 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11524 df-neg 11525 df-div 11955 df-nn 12317 df-2 12386 df-3 12387 df-4 12388 df-5 12389 df-6 12390 df-7 12391 df-8 12392 df-9 12393 df-n0 12588 df-xnn0 12661 df-z 12675 df-dec 12796 df-uz 12947 df-q 13057 df-rp 13102 df-xneg 13222 df-xadd 13223 df-xmul 13224 df-ioo 13461 df-ioc 13462 df-ico 13463 df-icc 13464 df-fz 13621 df-fzo 13769 df-fl 13912 df-mod 13990 df-seq 14125 df-exp 14185 df-fac 14398 df-bc 14427 df-hash 14455 df-shft 15200 df-cj 15246 df-re 15247 df-im 15248 df-sqrt 15382 df-abs 15383 df-limsup 15618 df-clim 15635 df-rlim 15636 df-sum 15834 df-ef 16213 df-sin 16215 df-cos 16216 df-tan 16217 df-pi 16218 df-struct 17305 df-sets 17322 df-slot 17340 df-ndx 17352 df-base 17368 df-ress 17389 df-plusg 17421 df-mulr 17422 df-starv 17423 df-sca 17424 df-vsca 17425 df-ip 17426 df-tset 17427 df-ple 17428 df-ds 17430 df-unif 17431 df-hom 17432 df-cco 17433 df-rest 17573 df-topn 17574 df-0g 17592 df-gsum 17593 df-topgen 17594 df-pt 17595 df-prds 17598 df-xrs 17654 df-qtop 17659 df-imas 17660 df-xps 17662 df-mre 17736 df-mrc 17737 df-acs 17739 df-mgm 18796 df-sgrp 18888 df-mnd 18904 df-submnd 18959 df-mulg 19258 df-cntz 19511 df-cmn 19976 df-psmet 21650 df-xmet 21651 df-met 21652 df-bl 21653 df-mopn 21654 df-fbas 21655 df-fg 21656 df-cnfld 21659 df-top 23192 df-topon 23209 df-topsp 23231 df-bases 23244 df-cld 23317 df-ntr 23318 df-cls 23319 df-nei 23396 df-lp 23434 df-perf 23435 df-cn 23525 df-cnp 23526 df-haus 23613 df-tx 23861 df-hmeo 24054 df-fil 24145 df-fm 24237 df-flim 24238 df-flf 24239 df-xms 24619 df-ms 24620 df-tms 24621 df-cncf 25179 df-0p 25971 df-limc 26166 df-dv 26167 df-ply 26486 df-idp 26487 df-coe 26488 df-dgr 26489 df-quot 26594

This theorem is used by: basellem9 27398

W3C validator