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

Theorem leibpi 25526
 Description: The Leibniz formula for π. This proof depends on three main facts: (1) the series 𝐹 is convergent, because it is an alternating series (iseralt 15032). (2) Using leibpilem2 25525 to rewrite the series as a power series, it is the 𝑥 = 1 special case of the Taylor series for arctan (atantayl2 25522). (3) Although we cannot directly plug 𝑥 = 1 into atantayl2 25522, Abel's theorem (abelth2 25035) says that the limit along any sequence converging to 1, such as 1 − 1 / 𝑛, of the power series converges to the power series extended to 1, and then since arctan is continuous at 1 (atancn 25520) we get the desired result. This is Metamath 100 proof #26. (Contributed by Mario Carneiro, 7-Apr-2015.)
Hypothesis
Ref Expression
leibpi.1 𝐹 = (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1)))
Assertion
Ref Expression
leibpi seq0( + , 𝐹) ⇝ (π / 4)

Proof of Theorem leibpi
Dummy variables 𝑗 𝑘 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nn0uz 12268 . . . . 5 0 = (ℤ‘0)
2 0zd 11981 . . . . 5 (⊤ → 0 ∈ ℤ)
3 eqidd 2823 . . . . 5 ((⊤ ∧ 𝑗 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) = ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗))
4 0cnd 10623 . . . . . . . . 9 ((𝑘 ∈ ℕ0 ∧ (𝑘 = 0 ∨ 2 ∥ 𝑘)) → 0 ∈ ℂ)
5 ioran 981 . . . . . . . . . 10 (¬ (𝑘 = 0 ∨ 2 ∥ 𝑘) ↔ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘))
6 neg1rr 11740 . . . . . . . . . . . . 13 -1 ∈ ℝ
7 leibpilem1 25524 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ0 ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → (𝑘 ∈ ℕ ∧ ((𝑘 − 1) / 2) ∈ ℕ0))
87simprd 499 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ0 ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → ((𝑘 − 1) / 2) ∈ ℕ0)
9 reexpcl 13442 . . . . . . . . . . . . 13 ((-1 ∈ ℝ ∧ ((𝑘 − 1) / 2) ∈ ℕ0) → (-1↑((𝑘 − 1) / 2)) ∈ ℝ)
106, 8, 9sylancr 590 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ0 ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → (-1↑((𝑘 − 1) / 2)) ∈ ℝ)
117simpld 498 . . . . . . . . . . . 12 ((𝑘 ∈ ℕ0 ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → 𝑘 ∈ ℕ)
1210, 11nndivred 11679 . . . . . . . . . . 11 ((𝑘 ∈ ℕ0 ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → ((-1↑((𝑘 − 1) / 2)) / 𝑘) ∈ ℝ)
1312recnd 10658 . . . . . . . . . 10 ((𝑘 ∈ ℕ0 ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → ((-1↑((𝑘 − 1) / 2)) / 𝑘) ∈ ℂ)
145, 13sylan2b 596 . . . . . . . . 9 ((𝑘 ∈ ℕ0 ∧ ¬ (𝑘 = 0 ∨ 2 ∥ 𝑘)) → ((-1↑((𝑘 − 1) / 2)) / 𝑘) ∈ ℂ)
154, 14ifclda 4473 . . . . . . . 8 (𝑘 ∈ ℕ0 → if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)) ∈ ℂ)
1615adantl 485 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ0) → if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)) ∈ ℂ)
1716fmpttd 6861 . . . . . 6 (⊤ → (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘))):ℕ0⟶ℂ)
1817ffvelrnda 6833 . . . . 5 ((⊤ ∧ 𝑗 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) ∈ ℂ)
19 2nn0 11902 . . . . . . . . . . . . . 14 2 ∈ ℕ0
2019a1i 11 . . . . . . . . . . . . 13 (⊤ → 2 ∈ ℕ0)
21 nn0mulcl 11921 . . . . . . . . . . . . 13 ((2 ∈ ℕ0𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
2220, 21sylan 583 . . . . . . . . . . . 12 ((⊤ ∧ 𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
23 nn0p1nn 11924 . . . . . . . . . . . 12 ((2 · 𝑛) ∈ ℕ0 → ((2 · 𝑛) + 1) ∈ ℕ)
2422, 23syl 17 . . . . . . . . . . 11 ((⊤ ∧ 𝑛 ∈ ℕ0) → ((2 · 𝑛) + 1) ∈ ℕ)
2524nnrecred 11676 . . . . . . . . . 10 ((⊤ ∧ 𝑛 ∈ ℕ0) → (1 / ((2 · 𝑛) + 1)) ∈ ℝ)
2625fmpttd 6861 . . . . . . . . 9 (⊤ → (𝑛 ∈ ℕ0 ↦ (1 / ((2 · 𝑛) + 1))):ℕ0⟶ℝ)
27 nn0mulcl 11921 . . . . . . . . . . . . . 14 ((2 ∈ ℕ0𝑘 ∈ ℕ0) → (2 · 𝑘) ∈ ℕ0)
2820, 27sylan 583 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2 · 𝑘) ∈ ℕ0)
2928nn0red 11944 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2 · 𝑘) ∈ ℝ)
30 peano2nn0 11925 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ0)
3130adantl 485 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ∈ ℕ0)
32 nn0mulcl 11921 . . . . . . . . . . . . . 14 ((2 ∈ ℕ0 ∧ (𝑘 + 1) ∈ ℕ0) → (2 · (𝑘 + 1)) ∈ ℕ0)
3319, 31, 32sylancr 590 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2 · (𝑘 + 1)) ∈ ℕ0)
3433nn0red 11944 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2 · (𝑘 + 1)) ∈ ℝ)
35 1red 10631 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ0) → 1 ∈ ℝ)
36 nn0re 11894 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ0𝑘 ∈ ℝ)
3736adantl 485 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℝ)
3837lep1d 11560 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ0) → 𝑘 ≤ (𝑘 + 1))
39 peano2re 10802 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℝ → (𝑘 + 1) ∈ ℝ)
4037, 39syl 17 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ∈ ℝ)
41 2re 11699 . . . . . . . . . . . . . . 15 2 ∈ ℝ
4241a1i 11 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑘 ∈ ℕ0) → 2 ∈ ℝ)
43 2pos 11728 . . . . . . . . . . . . . . 15 0 < 2
4443a1i 11 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑘 ∈ ℕ0) → 0 < 2)
45 lemul2 11482 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝑘 ≤ (𝑘 + 1) ↔ (2 · 𝑘) ≤ (2 · (𝑘 + 1))))
4637, 40, 42, 44, 45syl112anc 1371 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ0) → (𝑘 ≤ (𝑘 + 1) ↔ (2 · 𝑘) ≤ (2 · (𝑘 + 1))))
4738, 46mpbid 235 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2 · 𝑘) ≤ (2 · (𝑘 + 1)))
4829, 34, 35, 47leadd1dd 11243 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((2 · 𝑘) + 1) ≤ ((2 · (𝑘 + 1)) + 1))
49 nn0p1nn 11924 . . . . . . . . . . . . . 14 ((2 · 𝑘) ∈ ℕ0 → ((2 · 𝑘) + 1) ∈ ℕ)
5028, 49syl 17 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((2 · 𝑘) + 1) ∈ ℕ)
5150nnred 11640 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((2 · 𝑘) + 1) ∈ ℝ)
5250nngt0d 11674 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ0) → 0 < ((2 · 𝑘) + 1))
53 nn0p1nn 11924 . . . . . . . . . . . . . 14 ((2 · (𝑘 + 1)) ∈ ℕ0 → ((2 · (𝑘 + 1)) + 1) ∈ ℕ)
5433, 53syl 17 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((2 · (𝑘 + 1)) + 1) ∈ ℕ)
5554nnred 11640 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((2 · (𝑘 + 1)) + 1) ∈ ℝ)
5654nngt0d 11674 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ0) → 0 < ((2 · (𝑘 + 1)) + 1))
57 lerec 11512 . . . . . . . . . . . 12 (((((2 · 𝑘) + 1) ∈ ℝ ∧ 0 < ((2 · 𝑘) + 1)) ∧ (((2 · (𝑘 + 1)) + 1) ∈ ℝ ∧ 0 < ((2 · (𝑘 + 1)) + 1))) → (((2 · 𝑘) + 1) ≤ ((2 · (𝑘 + 1)) + 1) ↔ (1 / ((2 · (𝑘 + 1)) + 1)) ≤ (1 / ((2 · 𝑘) + 1))))
5851, 52, 55, 56, 57syl22anc 837 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → (((2 · 𝑘) + 1) ≤ ((2 · (𝑘 + 1)) + 1) ↔ (1 / ((2 · (𝑘 + 1)) + 1)) ≤ (1 / ((2 · 𝑘) + 1))))
5948, 58mpbid 235 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → (1 / ((2 · (𝑘 + 1)) + 1)) ≤ (1 / ((2 · 𝑘) + 1)))
60 oveq2 7148 . . . . . . . . . . . . . 14 (𝑛 = (𝑘 + 1) → (2 · 𝑛) = (2 · (𝑘 + 1)))
6160oveq1d 7155 . . . . . . . . . . . . 13 (𝑛 = (𝑘 + 1) → ((2 · 𝑛) + 1) = ((2 · (𝑘 + 1)) + 1))
6261oveq2d 7156 . . . . . . . . . . . 12 (𝑛 = (𝑘 + 1) → (1 / ((2 · 𝑛) + 1)) = (1 / ((2 · (𝑘 + 1)) + 1)))
63 eqid 2822 . . . . . . . . . . . 12 (𝑛 ∈ ℕ0 ↦ (1 / ((2 · 𝑛) + 1))) = (𝑛 ∈ ℕ0 ↦ (1 / ((2 · 𝑛) + 1)))
64 ovex 7173 . . . . . . . . . . . 12 (1 / ((2 · (𝑘 + 1)) + 1)) ∈ V
6562, 63, 64fvmpt 6750 . . . . . . . . . . 11 ((𝑘 + 1) ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ (1 / ((2 · 𝑛) + 1)))‘(𝑘 + 1)) = (1 / ((2 · (𝑘 + 1)) + 1)))
6631, 65syl 17 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (1 / ((2 · 𝑛) + 1)))‘(𝑘 + 1)) = (1 / ((2 · (𝑘 + 1)) + 1)))
67 oveq2 7148 . . . . . . . . . . . . . 14 (𝑛 = 𝑘 → (2 · 𝑛) = (2 · 𝑘))
6867oveq1d 7155 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → ((2 · 𝑛) + 1) = ((2 · 𝑘) + 1))
6968oveq2d 7156 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (1 / ((2 · 𝑛) + 1)) = (1 / ((2 · 𝑘) + 1)))
70 ovex 7173 . . . . . . . . . . . 12 (1 / ((2 · 𝑘) + 1)) ∈ V
7169, 63, 70fvmpt 6750 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ (1 / ((2 · 𝑛) + 1)))‘𝑘) = (1 / ((2 · 𝑘) + 1)))
7271adantl 485 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (1 / ((2 · 𝑛) + 1)))‘𝑘) = (1 / ((2 · 𝑘) + 1)))
7359, 66, 723brtr4d 5074 . . . . . . . . 9 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (1 / ((2 · 𝑛) + 1)))‘(𝑘 + 1)) ≤ ((𝑛 ∈ ℕ0 ↦ (1 / ((2 · 𝑛) + 1)))‘𝑘))
74 nnuz 12269 . . . . . . . . . 10 ℕ = (ℤ‘1)
75 1zzd 12001 . . . . . . . . . 10 (⊤ → 1 ∈ ℤ)
76 ax-1cn 10584 . . . . . . . . . . 11 1 ∈ ℂ
77 divcnv 15199 . . . . . . . . . . 11 (1 ∈ ℂ → (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0)
7876, 77mp1i 13 . . . . . . . . . 10 (⊤ → (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0)
79 nn0ex 11891 . . . . . . . . . . . 12 0 ∈ V
8079mptex 6968 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 ↦ (1 / ((2 · 𝑛) + 1))) ∈ V
8180a1i 11 . . . . . . . . . 10 (⊤ → (𝑛 ∈ ℕ0 ↦ (1 / ((2 · 𝑛) + 1))) ∈ V)
82 oveq2 7148 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → (1 / 𝑛) = (1 / 𝑘))
83 eqid 2822 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ ↦ (1 / 𝑛)) = (𝑛 ∈ ℕ ↦ (1 / 𝑛))
84 ovex 7173 . . . . . . . . . . . . 13 (1 / 𝑘) ∈ V
8582, 83, 84fvmpt 6750 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘) = (1 / 𝑘))
8685adantl 485 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘) = (1 / 𝑘))
87 nnrecre 11667 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
8887adantl 485 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ) → (1 / 𝑘) ∈ ℝ)
8986, 88eqeltrd 2914 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘) ∈ ℝ)
90 nnnn0 11892 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
9190adantl 485 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ0)
9291, 71syl 17 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ (1 / ((2 · 𝑛) + 1)))‘𝑘) = (1 / ((2 · 𝑘) + 1)))
9390, 50sylan2 595 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ ℕ)
9493nnrecred 11676 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ) → (1 / ((2 · 𝑘) + 1)) ∈ ℝ)
9592, 94eqeltrd 2914 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ (1 / ((2 · 𝑛) + 1)))‘𝑘) ∈ ℝ)
96 nnre 11632 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
9796adantl 485 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ)
9819, 91, 27sylancr 590 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ0)
9998nn0red 11944 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℝ)
100 peano2re 10802 . . . . . . . . . . . . . 14 ((2 · 𝑘) ∈ ℝ → ((2 · 𝑘) + 1) ∈ ℝ)
10199, 100syl 17 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ ℝ)
102 nn0addge1 11931 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℝ ∧ 𝑘 ∈ ℕ0) → 𝑘 ≤ (𝑘 + 𝑘))
10397, 91, 102syl2anc 587 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑘 ∈ ℕ) → 𝑘 ≤ (𝑘 + 𝑘))
10497recnd 10658 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℂ)
1051042timesd 11868 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) = (𝑘 + 𝑘))
106103, 105breqtrrd 5070 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ) → 𝑘 ≤ (2 · 𝑘))
10799lep1d 11560 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ≤ ((2 · 𝑘) + 1))
10897, 99, 101, 106, 107letrd 10786 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ) → 𝑘 ≤ ((2 · 𝑘) + 1))
109 nngt0 11656 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → 0 < 𝑘)
110109adantl 485 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ) → 0 < 𝑘)
11193nnred 11640 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ ℝ)
11293nngt0d 11674 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ) → 0 < ((2 · 𝑘) + 1))
113 lerec 11512 . . . . . . . . . . . . 13 (((𝑘 ∈ ℝ ∧ 0 < 𝑘) ∧ (((2 · 𝑘) + 1) ∈ ℝ ∧ 0 < ((2 · 𝑘) + 1))) → (𝑘 ≤ ((2 · 𝑘) + 1) ↔ (1 / ((2 · 𝑘) + 1)) ≤ (1 / 𝑘)))
11497, 110, 111, 112, 113syl22anc 837 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝑘 ≤ ((2 · 𝑘) + 1) ↔ (1 / ((2 · 𝑘) + 1)) ≤ (1 / 𝑘)))
115108, 114mpbid 235 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ) → (1 / ((2 · 𝑘) + 1)) ≤ (1 / 𝑘))
116115, 92, 863brtr4d 5074 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ (1 / ((2 · 𝑛) + 1)))‘𝑘) ≤ ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘))
11793nnrpd 12417 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ ℝ+)
118117rpreccld 12429 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ) → (1 / ((2 · 𝑘) + 1)) ∈ ℝ+)
119118rpge0d 12423 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ) → 0 ≤ (1 / ((2 · 𝑘) + 1)))
120119, 92breqtrrd 5070 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ) → 0 ≤ ((𝑛 ∈ ℕ0 ↦ (1 / ((2 · 𝑛) + 1)))‘𝑘))
12174, 75, 78, 81, 89, 95, 116, 120climsqz2 14989 . . . . . . . . 9 (⊤ → (𝑛 ∈ ℕ0 ↦ (1 / ((2 · 𝑛) + 1))) ⇝ 0)
122 neg1cn 11739 . . . . . . . . . . . . 13 -1 ∈ ℂ
123122a1i 11 . . . . . . . . . . . 12 (⊤ → -1 ∈ ℂ)
124 expcl 13443 . . . . . . . . . . . 12 ((-1 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (-1↑𝑘) ∈ ℂ)
125123, 124sylan 583 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → (-1↑𝑘) ∈ ℂ)
12650nncnd 11641 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((2 · 𝑘) + 1) ∈ ℂ)
12750nnne0d 11675 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((2 · 𝑘) + 1) ≠ 0)
128125, 126, 127divrecd 11408 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((-1↑𝑘) / ((2 · 𝑘) + 1)) = ((-1↑𝑘) · (1 / ((2 · 𝑘) + 1))))
129 oveq2 7148 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → (-1↑𝑛) = (-1↑𝑘))
130129, 68oveq12d 7158 . . . . . . . . . . . 12 (𝑛 = 𝑘 → ((-1↑𝑛) / ((2 · 𝑛) + 1)) = ((-1↑𝑘) / ((2 · 𝑘) + 1)))
131 eqid 2822 . . . . . . . . . . . 12 (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1))) = (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1)))
132 ovex 7173 . . . . . . . . . . . 12 ((-1↑𝑘) / ((2 · 𝑘) + 1)) ∈ V
133130, 131, 132fvmpt 6750 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1)))‘𝑘) = ((-1↑𝑘) / ((2 · 𝑘) + 1)))
134133adantl 485 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1)))‘𝑘) = ((-1↑𝑘) / ((2 · 𝑘) + 1)))
13572oveq2d 7156 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((-1↑𝑘) · ((𝑛 ∈ ℕ0 ↦ (1 / ((2 · 𝑛) + 1)))‘𝑘)) = ((-1↑𝑘) · (1 / ((2 · 𝑘) + 1))))
136128, 134, 1353eqtr4d 2867 . . . . . . . . 9 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1)))‘𝑘) = ((-1↑𝑘) · ((𝑛 ∈ ℕ0 ↦ (1 / ((2 · 𝑛) + 1)))‘𝑘)))
1371, 2, 26, 73, 121, 136iseralt 15032 . . . . . . . 8 (⊤ → seq0( + , (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1)))) ∈ dom ⇝ )
138 climdm 14902 . . . . . . . 8 (seq0( + , (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1)))) ∈ dom ⇝ ↔ seq0( + , (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1)))) ⇝ ( ⇝ ‘seq0( + , (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1))))))
139137, 138sylib 221 . . . . . . 7 (⊤ → seq0( + , (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1)))) ⇝ ( ⇝ ‘seq0( + , (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1))))))
140 eqid 2822 . . . . . . . 8 (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘))) = (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))
141 fvex 6665 . . . . . . . 8 ( ⇝ ‘seq0( + , (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1))))) ∈ V
142131, 140, 141leibpilem2 25525 . . . . . . 7 (seq0( + , (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1)))) ⇝ ( ⇝ ‘seq0( + , (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1))))) ↔ seq0( + , (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))) ⇝ ( ⇝ ‘seq0( + , (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1))))))
143139, 142sylib 221 . . . . . 6 (⊤ → seq0( + , (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))) ⇝ ( ⇝ ‘seq0( + , (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1))))))
144 seqex 13366 . . . . . . 7 seq0( + , (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))) ∈ V
145144, 141breldm 5754 . . . . . 6 (seq0( + , (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))) ⇝ ( ⇝ ‘seq0( + , (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1))))) → seq0( + , (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))) ∈ dom ⇝ )
146143, 145syl 17 . . . . 5 (⊤ → seq0( + , (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))) ∈ dom ⇝ )
1471, 2, 3, 18, 146isumclim2 15104 . . . 4 (⊤ → seq0( + , (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))) ⇝ Σ𝑗 ∈ ℕ0 ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗))
148 eqid 2822 . . . . . . . 8 (𝑥 ∈ (0[,]1) ↦ Σ𝑗 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥𝑗))) = (𝑥 ∈ (0[,]1) ↦ Σ𝑗 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥𝑗)))
14917, 146, 148abelth2 25035 . . . . . . 7 (⊤ → (𝑥 ∈ (0[,]1) ↦ Σ𝑗 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥𝑗))) ∈ ((0[,]1)–cn→ℂ))
150 nnrp 12388 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
151150adantl 485 . . . . . . . . . . . 12 ((⊤ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ+)
152151rpreccld 12429 . . . . . . . . . . 11 ((⊤ ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ∈ ℝ+)
153152rpred 12419 . . . . . . . . . 10 ((⊤ ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ∈ ℝ)
154152rpge0d 12423 . . . . . . . . . 10 ((⊤ ∧ 𝑛 ∈ ℕ) → 0 ≤ (1 / 𝑛))
155 nnge1 11653 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → 1 ≤ 𝑛)
156155adantl 485 . . . . . . . . . . . 12 ((⊤ ∧ 𝑛 ∈ ℕ) → 1 ≤ 𝑛)
157 nnre 11632 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
158157adantl 485 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ)
159158recnd 10658 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
160159mulid1d 10647 . . . . . . . . . . . 12 ((⊤ ∧ 𝑛 ∈ ℕ) → (𝑛 · 1) = 𝑛)
161156, 160breqtrrd 5070 . . . . . . . . . . 11 ((⊤ ∧ 𝑛 ∈ ℕ) → 1 ≤ (𝑛 · 1))
162 1red 10631 . . . . . . . . . . . 12 ((⊤ ∧ 𝑛 ∈ ℕ) → 1 ∈ ℝ)
163 nngt0 11656 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → 0 < 𝑛)
164163adantl 485 . . . . . . . . . . . 12 ((⊤ ∧ 𝑛 ∈ ℕ) → 0 < 𝑛)
165 ledivmul 11505 . . . . . . . . . . . 12 ((1 ∈ ℝ ∧ 1 ∈ ℝ ∧ (𝑛 ∈ ℝ ∧ 0 < 𝑛)) → ((1 / 𝑛) ≤ 1 ↔ 1 ≤ (𝑛 · 1)))
166162, 162, 158, 164, 165syl112anc 1371 . . . . . . . . . . 11 ((⊤ ∧ 𝑛 ∈ ℕ) → ((1 / 𝑛) ≤ 1 ↔ 1 ≤ (𝑛 · 1)))
167161, 166mpbird 260 . . . . . . . . . 10 ((⊤ ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ≤ 1)
168 elicc01 12844 . . . . . . . . . 10 ((1 / 𝑛) ∈ (0[,]1) ↔ ((1 / 𝑛) ∈ ℝ ∧ 0 ≤ (1 / 𝑛) ∧ (1 / 𝑛) ≤ 1))
169153, 154, 167, 168syl3anbrc 1340 . . . . . . . . 9 ((⊤ ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ∈ (0[,]1))
170 iirev 23532 . . . . . . . . 9 ((1 / 𝑛) ∈ (0[,]1) → (1 − (1 / 𝑛)) ∈ (0[,]1))
171169, 170syl 17 . . . . . . . 8 ((⊤ ∧ 𝑛 ∈ ℕ) → (1 − (1 / 𝑛)) ∈ (0[,]1))
172171fmpttd 6861 . . . . . . 7 (⊤ → (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛))):ℕ⟶(0[,]1))
173 1cnd 10625 . . . . . . . . 9 (⊤ → 1 ∈ ℂ)
174 nnex 11631 . . . . . . . . . . 11 ℕ ∈ V
175174mptex 6968 . . . . . . . . . 10 (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛))) ∈ V
176175a1i 11 . . . . . . . . 9 (⊤ → (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛))) ∈ V)
17789recnd 10658 . . . . . . . . 9 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘) ∈ ℂ)
17882oveq2d 7156 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (1 − (1 / 𝑛)) = (1 − (1 / 𝑘)))
179 eqid 2822 . . . . . . . . . . . 12 (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛))) = (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛)))
180 ovex 7173 . . . . . . . . . . . 12 (1 − (1 / 𝑘)) ∈ V
181178, 179, 180fvmpt 6750 . . . . . . . . . . 11 (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛)))‘𝑘) = (1 − (1 / 𝑘)))
18285oveq2d 7156 . . . . . . . . . . 11 (𝑘 ∈ ℕ → (1 − ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘)) = (1 − (1 / 𝑘)))
183181, 182eqtr4d 2860 . . . . . . . . . 10 (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛)))‘𝑘) = (1 − ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘)))
184183adantl 485 . . . . . . . . 9 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛)))‘𝑘) = (1 − ((𝑛 ∈ ℕ ↦ (1 / 𝑛))‘𝑘)))
18574, 75, 78, 173, 176, 177, 184climsubc2 14986 . . . . . . . 8 (⊤ → (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛))) ⇝ (1 − 0))
186 1m0e1 11746 . . . . . . . 8 (1 − 0) = 1
187185, 186breqtrdi 5083 . . . . . . 7 (⊤ → (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛))) ⇝ 1)
188 1elunit 12848 . . . . . . . 8 1 ∈ (0[,]1)
189188a1i 11 . . . . . . 7 (⊤ → 1 ∈ (0[,]1))
19074, 75, 149, 172, 187, 189climcncf 23503 . . . . . 6 (⊤ → ((𝑥 ∈ (0[,]1) ↦ Σ𝑗 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥𝑗))) ∘ (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛)))) ⇝ ((𝑥 ∈ (0[,]1) ↦ Σ𝑗 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥𝑗)))‘1))
191 eqidd 2823 . . . . . . . 8 (⊤ → (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛))) = (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛))))
192 eqidd 2823 . . . . . . . 8 (⊤ → (𝑥 ∈ (0[,]1) ↦ Σ𝑗 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥𝑗))) = (𝑥 ∈ (0[,]1) ↦ Σ𝑗 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥𝑗))))
193 oveq1 7147 . . . . . . . . . 10 (𝑥 = (1 − (1 / 𝑛)) → (𝑥𝑗) = ((1 − (1 / 𝑛))↑𝑗))
194193oveq2d 7156 . . . . . . . . 9 (𝑥 = (1 − (1 / 𝑛)) → (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥𝑗)) = (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · ((1 − (1 / 𝑛))↑𝑗)))
195194sumeq2sdv 15052 . . . . . . . 8 (𝑥 = (1 − (1 / 𝑛)) → Σ𝑗 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥𝑗)) = Σ𝑗 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · ((1 − (1 / 𝑛))↑𝑗)))
196171, 191, 192, 195fmptco 6873 . . . . . . 7 (⊤ → ((𝑥 ∈ (0[,]1) ↦ Σ𝑗 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥𝑗))) ∘ (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛)))) = (𝑛 ∈ ℕ ↦ Σ𝑗 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · ((1 − (1 / 𝑛))↑𝑗))))
197 0zd 11981 . . . . . . . . 9 ((⊤ ∧ 𝑛 ∈ ℕ) → 0 ∈ ℤ)
1988adantll 713 . . . . . . . . . . . . . . . . . . . . . 22 (((⊤ ∧ 𝑘 ∈ ℕ0) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → ((𝑘 − 1) / 2) ∈ ℕ0)
1996, 198, 9sylancr 590 . . . . . . . . . . . . . . . . . . . . 21 (((⊤ ∧ 𝑘 ∈ ℕ0) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → (-1↑((𝑘 − 1) / 2)) ∈ ℝ)
200199recnd 10658 . . . . . . . . . . . . . . . . . . . 20 (((⊤ ∧ 𝑘 ∈ ℕ0) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → (-1↑((𝑘 − 1) / 2)) ∈ ℂ)
201200adantllr 718 . . . . . . . . . . . . . . . . . . 19 ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → (-1↑((𝑘 − 1) / 2)) ∈ ℂ)
202 1re 10630 . . . . . . . . . . . . . . . . . . . . . . 23 1 ∈ ℝ
203 resubcl 10939 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 ∈ ℝ ∧ (1 / 𝑛) ∈ ℝ) → (1 − (1 / 𝑛)) ∈ ℝ)
204202, 153, 203sylancr 590 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑛 ∈ ℕ) → (1 − (1 / 𝑛)) ∈ ℝ)
205204ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → (1 − (1 / 𝑛)) ∈ ℝ)
206 simplr 768 . . . . . . . . . . . . . . . . . . . . 21 ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → 𝑘 ∈ ℕ0)
207205, 206reexpcld 13523 . . . . . . . . . . . . . . . . . . . 20 ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → ((1 − (1 / 𝑛))↑𝑘) ∈ ℝ)
208207recnd 10658 . . . . . . . . . . . . . . . . . . 19 ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → ((1 − (1 / 𝑛))↑𝑘) ∈ ℂ)
209 nn0cn 11895 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℕ0𝑘 ∈ ℂ)
210209ad2antlr 726 . . . . . . . . . . . . . . . . . . 19 ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → 𝑘 ∈ ℂ)
21111adantll 713 . . . . . . . . . . . . . . . . . . . 20 ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → 𝑘 ∈ ℕ)
212211nnne0d 11675 . . . . . . . . . . . . . . . . . . 19 ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → 𝑘 ≠ 0)
213201, 208, 210, 212div12d 11441 . . . . . . . . . . . . . . . . . 18 ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)) = (((1 − (1 / 𝑛))↑𝑘) · ((-1↑((𝑘 − 1) / 2)) / 𝑘)))
21413adantll 713 . . . . . . . . . . . . . . . . . . 19 ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → ((-1↑((𝑘 − 1) / 2)) / 𝑘) ∈ ℂ)
215208, 214mulcomd 10651 . . . . . . . . . . . . . . . . . 18 ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → (((1 − (1 / 𝑛))↑𝑘) · ((-1↑((𝑘 − 1) / 2)) / 𝑘)) = (((-1↑((𝑘 − 1) / 2)) / 𝑘) · ((1 − (1 / 𝑛))↑𝑘)))
216213, 215eqtrd 2857 . . . . . . . . . . . . . . . . 17 ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)) = (((-1↑((𝑘 − 1) / 2)) / 𝑘) · ((1 − (1 / 𝑛))↑𝑘)))
2175, 216sylan2b 596 . . . . . . . . . . . . . . . 16 ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) ∧ ¬ (𝑘 = 0 ∨ 2 ∥ 𝑘)) → ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)) = (((-1↑((𝑘 − 1) / 2)) / 𝑘) · ((1 − (1 / 𝑛))↑𝑘)))
218217ifeq2da 4470 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))) = if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, (((-1↑((𝑘 − 1) / 2)) / 𝑘) · ((1 − (1 / 𝑛))↑𝑘))))
219204recnd 10658 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑛 ∈ ℕ) → (1 − (1 / 𝑛)) ∈ ℂ)
220 expcl 13443 . . . . . . . . . . . . . . . . . 18 (((1 − (1 / 𝑛)) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((1 − (1 / 𝑛))↑𝑘) ∈ ℂ)
221219, 220sylan 583 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → ((1 − (1 / 𝑛))↑𝑘) ∈ ℂ)
222221mul02d 10827 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → (0 · ((1 − (1 / 𝑛))↑𝑘)) = 0)
223222ifeq1d 4457 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → if((𝑘 = 0 ∨ 2 ∥ 𝑘), (0 · ((1 − (1 / 𝑛))↑𝑘)), (((-1↑((𝑘 − 1) / 2)) / 𝑘) · ((1 − (1 / 𝑛))↑𝑘))) = if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, (((-1↑((𝑘 − 1) / 2)) / 𝑘) · ((1 − (1 / 𝑛))↑𝑘))))
224218, 223eqtr4d 2860 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))) = if((𝑘 = 0 ∨ 2 ∥ 𝑘), (0 · ((1 − (1 / 𝑛))↑𝑘)), (((-1↑((𝑘 − 1) / 2)) / 𝑘) · ((1 − (1 / 𝑛))↑𝑘))))
225 ovif 7235 . . . . . . . . . . . . . 14 (if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)) · ((1 − (1 / 𝑛))↑𝑘)) = if((𝑘 = 0 ∨ 2 ∥ 𝑘), (0 · ((1 − (1 / 𝑛))↑𝑘)), (((-1↑((𝑘 − 1) / 2)) / 𝑘) · ((1 − (1 / 𝑛))↑𝑘)))
226224, 225eqtr4di 2875 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))) = (if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)) · ((1 − (1 / 𝑛))↑𝑘)))
227 simpr 488 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
228 c0ex 10624 . . . . . . . . . . . . . . 15 0 ∈ V
229 ovex 7173 . . . . . . . . . . . . . . 15 ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)) ∈ V
230228, 229ifex 4487 . . . . . . . . . . . . . 14 if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))) ∈ V
231 eqid 2822 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)))) = (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))
232231fvmpt2 6761 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℕ0 ∧ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))) ∈ V) → ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))
233227, 230, 232sylancl 589 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))
234 ovex 7173 . . . . . . . . . . . . . . . 16 ((-1↑((𝑘 − 1) / 2)) / 𝑘) ∈ V
235228, 234ifex 4487 . . . . . . . . . . . . . . 15 if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)) ∈ V
236140fvmpt2 6761 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ0 ∧ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)) ∈ V) → ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑘) = if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))
237227, 235, 236sylancl 589 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑘) = if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))
238237oveq1d 7155 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑘) · ((1 − (1 / 𝑛))↑𝑘)) = (if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)) · ((1 − (1 / 𝑛))↑𝑘)))
239226, 233, 2383eqtr4d 2867 . . . . . . . . . . . 12 (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑘) · ((1 − (1 / 𝑛))↑𝑘)))
240239ralrimiva 3174 . . . . . . . . . . 11 ((⊤ ∧ 𝑛 ∈ ℕ) → ∀𝑘 ∈ ℕ0 ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑘) · ((1 − (1 / 𝑛))↑𝑘)))
241 nfv 1915 . . . . . . . . . . . 12 𝑗((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑘) · ((1 − (1 / 𝑛))↑𝑘))
242 nffvmpt1 6663 . . . . . . . . . . . . 13 𝑘((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗)
243 nffvmpt1 6663 . . . . . . . . . . . . . 14 𝑘((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗)
244 nfcv 2979 . . . . . . . . . . . . . 14 𝑘 ·
245 nfcv 2979 . . . . . . . . . . . . . 14 𝑘((1 − (1 / 𝑛))↑𝑗)
246243, 244, 245nfov 7170 . . . . . . . . . . . . 13 𝑘(((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · ((1 − (1 / 𝑛))↑𝑗))
247242, 246nfeq 2992 . . . . . . . . . . . 12 𝑘((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗) = (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · ((1 − (1 / 𝑛))↑𝑗))
248 fveq2 6652 . . . . . . . . . . . . 13 (𝑘 = 𝑗 → ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗))
249 fveq2 6652 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑘) = ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗))
250 oveq2 7148 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → ((1 − (1 / 𝑛))↑𝑘) = ((1 − (1 / 𝑛))↑𝑗))
251249, 250oveq12d 7158 . . . . . . . . . . . . 13 (𝑘 = 𝑗 → (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑘) · ((1 − (1 / 𝑛))↑𝑘)) = (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · ((1 − (1 / 𝑛))↑𝑗)))
252248, 251eqeq12d 2838 . . . . . . . . . . . 12 (𝑘 = 𝑗 → (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑘) · ((1 − (1 / 𝑛))↑𝑘)) ↔ ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗) = (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · ((1 − (1 / 𝑛))↑𝑗))))
253241, 247, 252cbvralw 3415 . . . . . . . . . . 11 (∀𝑘 ∈ ℕ0 ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑘) · ((1 − (1 / 𝑛))↑𝑘)) ↔ ∀𝑗 ∈ ℕ0 ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗) = (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · ((1 − (1 / 𝑛))↑𝑗)))
254240, 253sylib 221 . . . . . . . . . 10 ((⊤ ∧ 𝑛 ∈ ℕ) → ∀𝑗 ∈ ℕ0 ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗) = (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · ((1 − (1 / 𝑛))↑𝑗)))
255254r19.21bi 3198 . . . . . . . . 9 (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗) = (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · ((1 − (1 / 𝑛))↑𝑗)))
256 0cnd 10623 . . . . . . . . . . . . 13 ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) ∧ (𝑘 = 0 ∨ 2 ∥ 𝑘)) → 0 ∈ ℂ)
257207, 211nndivred 11679 . . . . . . . . . . . . . . . 16 ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → (((1 − (1 / 𝑛))↑𝑘) / 𝑘) ∈ ℝ)
258257recnd 10658 . . . . . . . . . . . . . . 15 ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → (((1 − (1 / 𝑛))↑𝑘) / 𝑘) ∈ ℂ)
259201, 258mulcld 10650 . . . . . . . . . . . . . 14 ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) ∧ (¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘)) → ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)) ∈ ℂ)
2605, 259sylan2b 596 . . . . . . . . . . . . 13 ((((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) ∧ ¬ (𝑘 = 0 ∨ 2 ∥ 𝑘)) → ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)) ∈ ℂ)
261256, 260ifclda 4473 . . . . . . . . . . . 12 (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))) ∈ ℂ)
262261fmpttd 6861 . . . . . . . . . . 11 ((⊤ ∧ 𝑛 ∈ ℕ) → (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)))):ℕ0⟶ℂ)
263262ffvelrnda 6833 . . . . . . . . . 10 (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗) ∈ ℂ)
264255, 263eqeltrrd 2915 . . . . . . . . 9 (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ0) → (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · ((1 − (1 / 𝑛))↑𝑗)) ∈ ℂ)
265 0nn0 11900 . . . . . . . . . . . 12 0 ∈ ℕ0
266265a1i 11 . . . . . . . . . . 11 ((⊤ ∧ 𝑛 ∈ ℕ) → 0 ∈ ℕ0)
267 0p1e1 11747 . . . . . . . . . . . . 13 (0 + 1) = 1
268 seqeq1 13367 . . . . . . . . . . . . 13 ((0 + 1) = 1 → seq(0 + 1)( + , (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))) = seq1( + , (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))))
269267, 268ax-mp 5 . . . . . . . . . . . 12 seq(0 + 1)( + , (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))) = seq1( + , (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)))))
270 1zzd 12001 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑛 ∈ ℕ) → 1 ∈ ℤ)
271 elnnuz 12270 . . . . . . . . . . . . . . 15 (𝑗 ∈ ℕ ↔ 𝑗 ∈ (ℤ‘1))
272 nnne0 11659 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ ℕ → 𝑘 ≠ 0)
273272neneqd 3016 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ ℕ → ¬ 𝑘 = 0)
274 biorf 934 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘 = 0 → (2 ∥ 𝑘 ↔ (𝑘 = 0 ∨ 2 ∥ 𝑘)))
275273, 274syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ ℕ → (2 ∥ 𝑘 ↔ (𝑘 = 0 ∨ 2 ∥ 𝑘)))
276275bicomd 226 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ℕ → ((𝑘 = 0 ∨ 2 ∥ 𝑘) ↔ 2 ∥ 𝑘))
277276ifbid 4461 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℕ → if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))) = if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))
27890, 230, 232sylancl 589 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))
279228, 229ifex 4487 . . . . . . . . . . . . . . . . . . . . 21 if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))) ∈ V
280 eqid 2822 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)))) = (𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))
281280fvmpt2 6761 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ ∧ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))) ∈ V) → ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))
282279, 281mpan2 690 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))
283277, 278, 2823eqtr4d 2867 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℕ → ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘))
284283rgen 3140 . . . . . . . . . . . . . . . . . 18 𝑘 ∈ ℕ ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘)
285284a1i 11 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑛 ∈ ℕ) → ∀𝑘 ∈ ℕ ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘))
286 nfv 1915 . . . . . . . . . . . . . . . . . 18 𝑗((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘)
287 nffvmpt1 6663 . . . . . . . . . . . . . . . . . . 19 𝑘((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗)
288242, 287nfeq 2992 . . . . . . . . . . . . . . . . . 18 𝑘((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗) = ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗)
289 fveq2 6652 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑗 → ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗))
290248, 289eqeq12d 2838 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑗 → (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) ↔ ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗) = ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗)))
291286, 288, 290cbvralw 3415 . . . . . . . . . . . . . . . . 17 (∀𝑘 ∈ ℕ ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) = ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑘) ↔ ∀𝑗 ∈ ℕ ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗) = ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗))
292285, 291sylib 221 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑛 ∈ ℕ) → ∀𝑗 ∈ ℕ ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗) = ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗))
293292r19.21bi 3198 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗) = ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗))
294271, 293sylan2br 597 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (ℤ‘1)) → ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗) = ((𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘𝑗))
295270, 294seqfeq 13391 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑛 ∈ ℕ) → seq1( + , (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))) = seq1( + , (𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))))
296153, 162, 167abssubge0d 14782 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑛 ∈ ℕ) → (abs‘(1 − (1 / 𝑛))) = (1 − (1 / 𝑛)))
297 ltsubrp 12413 . . . . . . . . . . . . . . . 16 ((1 ∈ ℝ ∧ (1 / 𝑛) ∈ ℝ+) → (1 − (1 / 𝑛)) < 1)
298202, 152, 297sylancr 590 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑛 ∈ ℕ) → (1 − (1 / 𝑛)) < 1)
299296, 298eqbrtrd 5064 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑛 ∈ ℕ) → (abs‘(1 − (1 / 𝑛))) < 1)
300280atantayl2 25522 . . . . . . . . . . . . . 14 (((1 − (1 / 𝑛)) ∈ ℂ ∧ (abs‘(1 − (1 / 𝑛))) < 1) → seq1( + , (𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))) ⇝ (arctan‘(1 − (1 / 𝑛))))
301219, 299, 300syl2anc 587 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑛 ∈ ℕ) → seq1( + , (𝑘 ∈ ℕ ↦ if(2 ∥ 𝑘, 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))) ⇝ (arctan‘(1 − (1 / 𝑛))))
302295, 301eqbrtrd 5064 . . . . . . . . . . . 12 ((⊤ ∧ 𝑛 ∈ ℕ) → seq1( + , (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))) ⇝ (arctan‘(1 − (1 / 𝑛))))
303269, 302eqbrtrid 5077 . . . . . . . . . . 11 ((⊤ ∧ 𝑛 ∈ ℕ) → seq(0 + 1)( + , (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))) ⇝ (arctan‘(1 − (1 / 𝑛))))
3041, 266, 263, 303clim2ser2 15003 . . . . . . . . . 10 ((⊤ ∧ 𝑛 ∈ ℕ) → seq0( + , (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))) ⇝ ((arctan‘(1 − (1 / 𝑛))) + (seq0( + , (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)))))‘0)))
305 0z 11980 . . . . . . . . . . . . . 14 0 ∈ ℤ
306 seq1 13377 . . . . . . . . . . . . . 14 (0 ∈ ℤ → (seq0( + , (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)))))‘0) = ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘0))
307305, 306ax-mp 5 . . . . . . . . . . . . 13 (seq0( + , (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)))))‘0) = ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘0)
308 iftrue 4445 . . . . . . . . . . . . . . . 16 ((𝑘 = 0 ∨ 2 ∥ 𝑘) → if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))) = 0)
309308orcs 872 . . . . . . . . . . . . . . 15 (𝑘 = 0 → if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))) = 0)
310309, 231, 228fvmpt 6750 . . . . . . . . . . . . . 14 (0 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘0) = 0)
311265, 310ax-mp 5 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))‘0) = 0
312307, 311eqtri 2845 . . . . . . . . . . . 12 (seq0( + , (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)))))‘0) = 0
313312oveq2i 7151 . . . . . . . . . . 11 ((arctan‘(1 − (1 / 𝑛))) + (seq0( + , (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)))))‘0)) = ((arctan‘(1 − (1 / 𝑛))) + 0)
314 atanrecl 25495 . . . . . . . . . . . . . 14 ((1 − (1 / 𝑛)) ∈ ℝ → (arctan‘(1 − (1 / 𝑛))) ∈ ℝ)
315204, 314syl 17 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑛 ∈ ℕ) → (arctan‘(1 − (1 / 𝑛))) ∈ ℝ)
316315recnd 10658 . . . . . . . . . . . 12 ((⊤ ∧ 𝑛 ∈ ℕ) → (arctan‘(1 − (1 / 𝑛))) ∈ ℂ)
317316addid1d 10829 . . . . . . . . . . 11 ((⊤ ∧ 𝑛 ∈ ℕ) → ((arctan‘(1 − (1 / 𝑛))) + 0) = (arctan‘(1 − (1 / 𝑛))))
318313, 317syl5eq 2869 . . . . . . . . . 10 ((⊤ ∧ 𝑛 ∈ ℕ) → ((arctan‘(1 − (1 / 𝑛))) + (seq0( + , (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘)))))‘0)) = (arctan‘(1 − (1 / 𝑛))))
319304, 318breqtrd 5068 . . . . . . . . 9 ((⊤ ∧ 𝑛 ∈ ℕ) → seq0( + , (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) · (((1 − (1 / 𝑛))↑𝑘) / 𝑘))))) ⇝ (arctan‘(1 − (1 / 𝑛))))
3201, 197, 255, 264, 319isumclim 15103 . . . . . . . 8 ((⊤ ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · ((1 − (1 / 𝑛))↑𝑗)) = (arctan‘(1 − (1 / 𝑛))))
321320mpteq2dva 5137 . . . . . . 7 (⊤ → (𝑛 ∈ ℕ ↦ Σ𝑗 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · ((1 − (1 / 𝑛))↑𝑗))) = (𝑛 ∈ ℕ ↦ (arctan‘(1 − (1 / 𝑛)))))
322196, 321eqtrd 2857 . . . . . 6 (⊤ → ((𝑥 ∈ (0[,]1) ↦ Σ𝑗 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥𝑗))) ∘ (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛)))) = (𝑛 ∈ ℕ ↦ (arctan‘(1 − (1 / 𝑛)))))
323 oveq1 7147 . . . . . . . . . . . 12 (𝑥 = 1 → (𝑥𝑗) = (1↑𝑗))
324 nn0z 11993 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ0𝑗 ∈ ℤ)
325 1exp 13454 . . . . . . . . . . . . 13 (𝑗 ∈ ℤ → (1↑𝑗) = 1)
326324, 325syl 17 . . . . . . . . . . . 12 (𝑗 ∈ ℕ0 → (1↑𝑗) = 1)
327323, 326sylan9eq 2877 . . . . . . . . . . 11 ((𝑥 = 1 ∧ 𝑗 ∈ ℕ0) → (𝑥𝑗) = 1)
328327oveq2d 7156 . . . . . . . . . 10 ((𝑥 = 1 ∧ 𝑗 ∈ ℕ0) → (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥𝑗)) = (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · 1))
32917mptru 1545 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘))):ℕ0⟶ℂ
330329ffvelrni 6832 . . . . . . . . . . . 12 (𝑗 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) ∈ ℂ)
331330mulid1d 10647 . . . . . . . . . . 11 (𝑗 ∈ ℕ0 → (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · 1) = ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗))
332331adantl 485 . . . . . . . . . 10 ((𝑥 = 1 ∧ 𝑗 ∈ ℕ0) → (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · 1) = ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗))
333328, 332eqtrd 2857 . . . . . . . . 9 ((𝑥 = 1 ∧ 𝑗 ∈ ℕ0) → (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥𝑗)) = ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗))
334333sumeq2dv 15051 . . . . . . . 8 (𝑥 = 1 → Σ𝑗 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥𝑗)) = Σ𝑗 ∈ ℕ0 ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗))
335 sumex 15035 . . . . . . . 8 Σ𝑗 ∈ ℕ0 ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) ∈ V
336334, 148, 335fvmpt 6750 . . . . . . 7 (1 ∈ (0[,]1) → ((𝑥 ∈ (0[,]1) ↦ Σ𝑗 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥𝑗)))‘1) = Σ𝑗 ∈ ℕ0 ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗))
337188, 336mp1i 13 . . . . . 6 (⊤ → ((𝑥 ∈ (0[,]1) ↦ Σ𝑗 ∈ ℕ0 (((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) · (𝑥𝑗)))‘1) = Σ𝑗 ∈ ℕ0 ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗))
338190, 322, 3373brtr3d 5073 . . . . 5 (⊤ → (𝑛 ∈ ℕ ↦ (arctan‘(1 − (1 / 𝑛)))) ⇝ Σ𝑗 ∈ ℕ0 ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗))
339 eqid 2822 . . . . . . . . 9 (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
340 eqid 2822 . . . . . . . . 9 {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))} = {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}
341339, 340atancn 25520 . . . . . . . 8 (arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}) ∈ ({𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}–cn→ℂ)
342341a1i 11 . . . . . . 7 (⊤ → (arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}) ∈ ({𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}–cn→ℂ))
343 unitssre 12877 . . . . . . . . 9 (0[,]1) ⊆ ℝ
344339, 340ressatans 25518 . . . . . . . . 9 ℝ ⊆ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}
345343, 344sstri 3951 . . . . . . . 8 (0[,]1) ⊆ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}
346 fss 6508 . . . . . . . 8 (((𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛))):ℕ⟶(0[,]1) ∧ (0[,]1) ⊆ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}) → (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛))):ℕ⟶{𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))})
347172, 345, 346sylancl 589 . . . . . . 7 (⊤ → (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛))):ℕ⟶{𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))})
348344, 202sselii 3939 . . . . . . . 8 1 ∈ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}
349348a1i 11 . . . . . . 7 (⊤ → 1 ∈ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))})
35074, 75, 342, 347, 187, 349climcncf 23503 . . . . . 6 (⊤ → ((arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}) ∘ (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛)))) ⇝ ((arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))})‘1))
351345, 171sseldi 3940 . . . . . . 7 ((⊤ ∧ 𝑛 ∈ ℕ) → (1 − (1 / 𝑛)) ∈ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))})
352 cncff 23496 . . . . . . . . . 10 ((arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}) ∈ ({𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}–cn→ℂ) → (arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}):{𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}⟶ℂ)
353341, 352mp1i 13 . . . . . . . . 9 (⊤ → (arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}):{𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}⟶ℂ)
354353feqmptd 6715 . . . . . . . 8 (⊤ → (arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}) = (𝑘 ∈ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))} ↦ ((arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))})‘𝑘)))
355 fvres 6671 . . . . . . . . 9 (𝑘 ∈ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))} → ((arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))})‘𝑘) = (arctan‘𝑘))
356355mpteq2ia 5133 . . . . . . . 8 (𝑘 ∈ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))} ↦ ((arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))})‘𝑘)) = (𝑘 ∈ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))} ↦ (arctan‘𝑘))
357354, 356syl6eq 2873 . . . . . . 7 (⊤ → (arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}) = (𝑘 ∈ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))} ↦ (arctan‘𝑘)))
358 fveq2 6652 . . . . . . 7 (𝑘 = (1 − (1 / 𝑛)) → (arctan‘𝑘) = (arctan‘(1 − (1 / 𝑛))))
359351, 191, 357, 358fmptco 6873 . . . . . 6 (⊤ → ((arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))}) ∘ (𝑛 ∈ ℕ ↦ (1 − (1 / 𝑛)))) = (𝑛 ∈ ℕ ↦ (arctan‘(1 − (1 / 𝑛)))))
360 fvres 6671 . . . . . . . 8 (1 ∈ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))} → ((arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))})‘1) = (arctan‘1))
361348, 360mp1i 13 . . . . . . 7 (⊤ → ((arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))})‘1) = (arctan‘1))
362 atan1 25512 . . . . . . 7 (arctan‘1) = (π / 4)
363361, 362syl6eq 2873 . . . . . 6 (⊤ → ((arctan ↾ {𝑥 ∈ ℂ ∣ (1 + (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0))})‘1) = (π / 4))
364350, 359, 3633brtr3d 5073 . . . . 5 (⊤ → (𝑛 ∈ ℕ ↦ (arctan‘(1 − (1 / 𝑛)))) ⇝ (π / 4))
365 climuni 14900 . . . . 5 (((𝑛 ∈ ℕ ↦ (arctan‘(1 − (1 / 𝑛)))) ⇝ Σ𝑗 ∈ ℕ0 ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) ∧ (𝑛 ∈ ℕ ↦ (arctan‘(1 − (1 / 𝑛)))) ⇝ (π / 4)) → Σ𝑗 ∈ ℕ0 ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) = (π / 4))
366338, 364, 365syl2anc 587 . . . 4 (⊤ → Σ𝑗 ∈ ℕ0 ((𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))‘𝑗) = (π / 4))
367147, 366breqtrd 5068 . . 3 (⊤ → seq0( + , (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))) ⇝ (π / 4))
368367mptru 1545 . 2 seq0( + , (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))) ⇝ (π / 4)
369 leibpi.1 . . 3 𝐹 = (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1)))
370 ovex 7173 . . 3 (π / 4) ∈ V
371369, 140, 370leibpilem2 25525 . 2 (seq0( + , 𝐹) ⇝ (π / 4) ↔ seq0( + , (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))) ⇝ (π / 4))
372368, 371mpbir 234 1 seq0( + , 𝐹) ⇝ (π / 4)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 399   ∨ wo 844   = wceq 1538  ⊤wtru 1539   ∈ wcel 2114  ∀wral 3130  {crab 3134  Vcvv 3469   ∖ cdif 3905   ⊆ wss 3908  ifcif 4439   class class class wbr 5042   ↦ cmpt 5122  dom cdm 5532   ↾ cres 5534   ∘ ccom 5536  ⟶wf 6330  ‘cfv 6334  (class class class)co 7140  ℂcc 10524  ℝcr 10525  0cc0 10526  1c1 10527   + caddc 10529   · cmul 10531  -∞cmnf 10662   < clt 10664   ≤ cle 10665   − cmin 10859  -cneg 10860   / cdiv 11286  ℕcn 11625  2c2 11680  4c4 11682  ℕ0cn0 11885  ℤcz 11969  ℤ≥cuz 12231  ℝ+crp 12377  (,]cioc 12727  [,]cicc 12729  seqcseq 13364  ↑cexp 13425  abscabs 14584   ⇝ cli 14832  Σcsu 15033  πcpi 15411   ∥ cdvds 15598  –cn→ccncf 23479  arctancatan 25448 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-inf2 9092  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604  ax-addf 10605  ax-mulf 10606 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-nel 3116  df-ral 3135  df-rex 3136  df-reu 3137  df-rmo 3138  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-uni 4814  df-int 4852  df-iun 4896  df-iin 4897  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5437  df-eprel 5442  df-po 5451  df-so 5452  df-fr 5491  df-se 5492  df-we 5493  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-isom 6343  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-of 7394  df-om 7566  df-1st 7675  df-2nd 7676  df-supp 7818  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-2o 8090  df-oadd 8093  df-er 8276  df-map 8395  df-pm 8396  df-ixp 8449  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fsupp 8822  df-fi 8863  df-sup 8894  df-inf 8895  df-oi 8962  df-card 9356  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-n0 11886  df-xnn0 11956  df-z 11970  df-dec 12087  df-uz 12232  df-q 12337  df-rp 12378  df-xneg 12495  df-xadd 12496  df-xmul 12497  df-ioo 12730  df-ioc 12731  df-ico 12732  df-icc 12733  df-fz 12886  df-fzo 13029  df-fl 13157  df-mod 13233  df-seq 13365  df-exp 13426  df-fac 13630  df-bc 13659  df-hash 13687  df-shft 14417  df-cj 14449  df-re 14450  df-im 14451  df-sqrt 14585  df-abs 14586  df-limsup 14819  df-clim 14836  df-rlim 14837  df-sum 15034  df-ef 15412  df-sin 15414  df-cos 15415  df-tan 15416  df-pi 15417  df-dvds 15599  df-struct 16476  df-ndx 16477  df-slot 16478  df-base 16480  df-sets 16481  df-ress 16482  df-plusg 16569  df-mulr 16570  df-starv 16571  df-sca 16572  df-vsca 16573  df-ip 16574  df-tset 16575  df-ple 16576  df-ds 16578  df-unif 16579  df-hom 16580  df-cco 16581  df-rest 16687  df-topn 16688  df-0g 16706  df-gsum 16707  df-topgen 16708  df-pt 16709  df-prds 16712  df-xrs 16766  df-qtop 16771  df-imas 16772  df-xps 16774  df-mre 16848  df-mrc 16849  df-acs 16851  df-mgm 17843  df-sgrp 17892  df-mnd 17903  df-submnd 17948  df-mulg 18216  df-cntz 18438  df-cmn 18899  df-psmet 20081  df-xmet 20082  df-met 20083  df-bl 20084  df-mopn 20085  df-fbas 20086  df-fg 20087  df-cnfld 20090  df-top 21497  df-topon 21514  df-topsp 21536  df-bases 21549  df-cld 21622  df-ntr 21623  df-cls 21624  df-nei 21701  df-lp 21739  df-perf 21740  df-cn 21830  df-cnp 21831  df-t1 21917  df-haus 21918  df-cmp 21990  df-tx 22165  df-hmeo 22358  df-fil 22449  df-fm 22541  df-flim 22542  df-flf 22543  df-xms 22925  df-ms 22926  df-tms 22927  df-cncf 23481  df-limc 24467  df-dv 24468  df-ulm 24970  df-log 25146  df-atan 25451 This theorem is referenced by:  leibpisum  25527
 Copyright terms: Public domain W3C validator