Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  nn0sumshdiglem1 Structured version   Visualization version   GIF version

Theorem nn0sumshdiglem1 47772
Description: Lemma 1 for nn0sumshdig 47774 (induction step). (Contributed by AV, 7-Jun-2020.)
Assertion
Ref Expression
nn0sumshdiglem1 (𝑦 ∈ ℕ → (∀𝑎 ∈ ℕ0 ((#b𝑎) = 𝑦𝑎 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))) → ∀𝑎 ∈ ℕ0 ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))
Distinct variable group:   𝑘,𝑎,𝑦

Proof of Theorem nn0sumshdiglem1
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 fveqeq2 6911 . . . 4 (𝑎 = 𝑥 → ((#b𝑎) = 𝑦 ↔ (#b𝑥) = 𝑦))
2 id 22 . . . . 5 (𝑎 = 𝑥𝑎 = 𝑥)
3 oveq2 7434 . . . . . . 7 (𝑎 = 𝑥 → (𝑘(digit‘2)𝑎) = (𝑘(digit‘2)𝑥))
43oveq1d 7441 . . . . . 6 (𝑎 = 𝑥 → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = ((𝑘(digit‘2)𝑥) · (2↑𝑘)))
54sumeq2sdv 15690 . . . . 5 (𝑎 = 𝑥 → Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)))
62, 5eqeq12d 2744 . . . 4 (𝑎 = 𝑥 → (𝑎 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘)) ↔ 𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))))
71, 6imbi12d 343 . . 3 (𝑎 = 𝑥 → (((#b𝑎) = 𝑦𝑎 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))) ↔ ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)))))
87cbvralvw 3232 . 2 (∀𝑎 ∈ ℕ0 ((#b𝑎) = 𝑦𝑎 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))) ↔ ∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))))
9 elnn0 12512 . . . . . 6 (𝑎 ∈ ℕ0 ↔ (𝑎 ∈ ℕ ∨ 𝑎 = 0))
10 nn0sumshdiglemA 47770 . . . . . . . . 9 (((𝑎 ∈ ℕ ∧ (𝑎 / 2) ∈ ℕ) ∧ 𝑦 ∈ ℕ) → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))
1110expimpd 452 . . . . . . . 8 ((𝑎 ∈ ℕ ∧ (𝑎 / 2) ∈ ℕ) → ((𝑦 ∈ ℕ ∧ ∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))
12 nn0sumshdiglemB 47771 . . . . . . . . 9 (((𝑎 ∈ ℕ ∧ ((𝑎 − 1) / 2) ∈ ℕ0) ∧ 𝑦 ∈ ℕ) → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))
1312expimpd 452 . . . . . . . 8 ((𝑎 ∈ ℕ ∧ ((𝑎 − 1) / 2) ∈ ℕ0) → ((𝑦 ∈ ℕ ∧ ∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))
14 nneom 47678 . . . . . . . 8 (𝑎 ∈ ℕ → ((𝑎 / 2) ∈ ℕ ∨ ((𝑎 − 1) / 2) ∈ ℕ0))
1511, 13, 14mpjaodan 956 . . . . . . 7 (𝑎 ∈ ℕ → ((𝑦 ∈ ℕ ∧ ∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))
16 eqcom 2735 . . . . . . . . . . . . . 14 (1 = (𝑦 + 1) ↔ (𝑦 + 1) = 1)
1716a1i 11 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (1 = (𝑦 + 1) ↔ (𝑦 + 1) = 1))
18 nncn 12258 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
19 1cnd 11247 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 1 ∈ ℂ)
2018, 19, 19addlsub 11668 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → ((𝑦 + 1) = 1 ↔ 𝑦 = (1 − 1)))
21 1m1e0 12322 . . . . . . . . . . . . . . 15 (1 − 1) = 0
2221a1i 11 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (1 − 1) = 0)
2322eqeq2d 2739 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (𝑦 = (1 − 1) ↔ 𝑦 = 0))
2417, 20, 233bitrd 304 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (1 = (𝑦 + 1) ↔ 𝑦 = 0))
25 oveq1 7433 . . . . . . . . . . . . . . . 16 (𝑦 = 0 → (𝑦 + 1) = (0 + 1))
2625oveq2d 7442 . . . . . . . . . . . . . . 15 (𝑦 = 0 → (0..^(𝑦 + 1)) = (0..^(0 + 1)))
27 0p1e1 12372 . . . . . . . . . . . . . . . . 17 (0 + 1) = 1
2827oveq2i 7437 . . . . . . . . . . . . . . . 16 (0..^(0 + 1)) = (0..^1)
29 fzo01 13754 . . . . . . . . . . . . . . . 16 (0..^1) = {0}
3028, 29eqtri 2756 . . . . . . . . . . . . . . 15 (0..^(0 + 1)) = {0}
3126, 30eqtrdi 2784 . . . . . . . . . . . . . 14 (𝑦 = 0 → (0..^(𝑦 + 1)) = {0})
3231sumeq1d 15687 . . . . . . . . . . . . 13 (𝑦 = 0 → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)0) · (2↑𝑘)) = Σ𝑘 ∈ {0} ((𝑘(digit‘2)0) · (2↑𝑘)))
33 0cn 11244 . . . . . . . . . . . . . 14 0 ∈ ℂ
34 oveq1 7433 . . . . . . . . . . . . . . . . . 18 (𝑘 = 0 → (𝑘(digit‘2)0) = (0(digit‘2)0))
35 2nn 12323 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℕ
36 0z 12607 . . . . . . . . . . . . . . . . . . 19 0 ∈ ℤ
37 dig0 47757 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℕ ∧ 0 ∈ ℤ) → (0(digit‘2)0) = 0)
3835, 36, 37mp2an 690 . . . . . . . . . . . . . . . . . 18 (0(digit‘2)0) = 0
3934, 38eqtrdi 2784 . . . . . . . . . . . . . . . . 17 (𝑘 = 0 → (𝑘(digit‘2)0) = 0)
40 oveq2 7434 . . . . . . . . . . . . . . . . . 18 (𝑘 = 0 → (2↑𝑘) = (2↑0))
41 2cn 12325 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℂ
42 exp0 14070 . . . . . . . . . . . . . . . . . . 19 (2 ∈ ℂ → (2↑0) = 1)
4341, 42ax-mp 5 . . . . . . . . . . . . . . . . . 18 (2↑0) = 1
4440, 43eqtrdi 2784 . . . . . . . . . . . . . . . . 17 (𝑘 = 0 → (2↑𝑘) = 1)
4539, 44oveq12d 7444 . . . . . . . . . . . . . . . 16 (𝑘 = 0 → ((𝑘(digit‘2)0) · (2↑𝑘)) = (0 · 1))
46 1re 11252 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ
47 mul02lem2 11429 . . . . . . . . . . . . . . . . 17 (1 ∈ ℝ → (0 · 1) = 0)
4846, 47ax-mp 5 . . . . . . . . . . . . . . . 16 (0 · 1) = 0
4945, 48eqtrdi 2784 . . . . . . . . . . . . . . 15 (𝑘 = 0 → ((𝑘(digit‘2)0) · (2↑𝑘)) = 0)
5049sumsn 15732 . . . . . . . . . . . . . 14 ((0 ∈ ℂ ∧ 0 ∈ ℂ) → Σ𝑘 ∈ {0} ((𝑘(digit‘2)0) · (2↑𝑘)) = 0)
5133, 33, 50mp2an 690 . . . . . . . . . . . . 13 Σ𝑘 ∈ {0} ((𝑘(digit‘2)0) · (2↑𝑘)) = 0
5232, 51eqtr2di 2785 . . . . . . . . . . . 12 (𝑦 = 0 → 0 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)0) · (2↑𝑘)))
5324, 52biimtrdi 252 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (1 = (𝑦 + 1) → 0 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)0) · (2↑𝑘))))
5453adantl 480 . . . . . . . . . 10 ((𝑎 = 0 ∧ 𝑦 ∈ ℕ) → (1 = (𝑦 + 1) → 0 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)0) · (2↑𝑘))))
55 fveq2 6902 . . . . . . . . . . . . . 14 (𝑎 = 0 → (#b𝑎) = (#b‘0))
56 blen0 47723 . . . . . . . . . . . . . 14 (#b‘0) = 1
5755, 56eqtrdi 2784 . . . . . . . . . . . . 13 (𝑎 = 0 → (#b𝑎) = 1)
5857eqeq1d 2730 . . . . . . . . . . . 12 (𝑎 = 0 → ((#b𝑎) = (𝑦 + 1) ↔ 1 = (𝑦 + 1)))
59 id 22 . . . . . . . . . . . . 13 (𝑎 = 0 → 𝑎 = 0)
60 oveq2 7434 . . . . . . . . . . . . . . 15 (𝑎 = 0 → (𝑘(digit‘2)𝑎) = (𝑘(digit‘2)0))
6160oveq1d 7441 . . . . . . . . . . . . . 14 (𝑎 = 0 → ((𝑘(digit‘2)𝑎) · (2↑𝑘)) = ((𝑘(digit‘2)0) · (2↑𝑘)))
6261sumeq2sdv 15690 . . . . . . . . . . . . 13 (𝑎 = 0 → Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)0) · (2↑𝑘)))
6359, 62eqeq12d 2744 . . . . . . . . . . . 12 (𝑎 = 0 → (𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)) ↔ 0 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)0) · (2↑𝑘))))
6458, 63imbi12d 343 . . . . . . . . . . 11 (𝑎 = 0 → (((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))) ↔ (1 = (𝑦 + 1) → 0 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)0) · (2↑𝑘)))))
6564adantr 479 . . . . . . . . . 10 ((𝑎 = 0 ∧ 𝑦 ∈ ℕ) → (((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))) ↔ (1 = (𝑦 + 1) → 0 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)0) · (2↑𝑘)))))
6654, 65mpbird 256 . . . . . . . . 9 ((𝑎 = 0 ∧ 𝑦 ∈ ℕ) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))
6766a1d 25 . . . . . . . 8 ((𝑎 = 0 ∧ 𝑦 ∈ ℕ) → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))
6867expimpd 452 . . . . . . 7 (𝑎 = 0 → ((𝑦 ∈ ℕ ∧ ∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))
6915, 68jaoi 855 . . . . . 6 ((𝑎 ∈ ℕ ∨ 𝑎 = 0) → ((𝑦 ∈ ℕ ∧ ∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))
709, 69sylbi 216 . . . . 5 (𝑎 ∈ ℕ0 → ((𝑦 ∈ ℕ ∧ ∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)))) → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))
7170com12 32 . . . 4 ((𝑦 ∈ ℕ ∧ ∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)))) → (𝑎 ∈ ℕ0 → ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))
7271ralrimiv 3142 . . 3 ((𝑦 ∈ ℕ ∧ ∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘)))) → ∀𝑎 ∈ ℕ0 ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘))))
7372ex 411 . 2 (𝑦 ∈ ℕ → (∀𝑥 ∈ ℕ0 ((#b𝑥) = 𝑦𝑥 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑥) · (2↑𝑘))) → ∀𝑎 ∈ ℕ0 ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))
748, 73biimtrid 241 1 (𝑦 ∈ ℕ → (∀𝑎 ∈ ℕ0 ((#b𝑎) = 𝑦𝑎 = Σ𝑘 ∈ (0..^𝑦)((𝑘(digit‘2)𝑎) · (2↑𝑘))) → ∀𝑎 ∈ ℕ0 ((#b𝑎) = (𝑦 + 1) → 𝑎 = Σ𝑘 ∈ (0..^(𝑦 + 1))((𝑘(digit‘2)𝑎) · (2↑𝑘)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  wo 845   = wceq 1533  wcel 2098  wral 3058  {csn 4632  cfv 6553  (class class class)co 7426  cc 11144  cr 11145  0cc0 11146  1c1 11147   + caddc 11149   · cmul 11151  cmin 11482   / cdiv 11909  cn 12250  2c2 12305  0cn0 12510  cz 12596  ..^cfzo 13667  cexp 14066  Σcsu 15672  #bcblen 47720  digitcdig 47746
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-inf2 9672  ax-cnex 11202  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222  ax-pre-mulgt0 11223  ax-pre-sup 11224  ax-addf 11225
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-tp 4637  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-iin 5003  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-se 5638  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-isom 6562  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-of 7691  df-om 7877  df-1st 7999  df-2nd 8000  df-supp 8172  df-frecs 8293  df-wrecs 8324  df-recs 8398  df-rdg 8437  df-1o 8493  df-2o 8494  df-er 8731  df-map 8853  df-pm 8854  df-ixp 8923  df-en 8971  df-dom 8972  df-sdom 8973  df-fin 8974  df-fsupp 9394  df-fi 9442  df-sup 9473  df-inf 9474  df-oi 9541  df-card 9970  df-pnf 11288  df-mnf 11289  df-xr 11290  df-ltxr 11291  df-le 11292  df-sub 11484  df-neg 11485  df-div 11910  df-nn 12251  df-2 12313  df-3 12314  df-4 12315  df-5 12316  df-6 12317  df-7 12318  df-8 12319  df-9 12320  df-n0 12511  df-z 12597  df-dec 12716  df-uz 12861  df-q 12971  df-rp 13015  df-xneg 13132  df-xadd 13133  df-xmul 13134  df-ioo 13368  df-ioc 13369  df-ico 13370  df-icc 13371  df-fz 13525  df-fzo 13668  df-fl 13797  df-mod 13875  df-seq 14007  df-exp 14067  df-fac 14273  df-bc 14302  df-hash 14330  df-shft 15054  df-cj 15086  df-re 15087  df-im 15088  df-sqrt 15222  df-abs 15223  df-limsup 15455  df-clim 15472  df-rlim 15473  df-sum 15673  df-ef 16051  df-sin 16053  df-cos 16054  df-pi 16056  df-dvds 16239  df-struct 17123  df-sets 17140  df-slot 17158  df-ndx 17170  df-base 17188  df-ress 17217  df-plusg 17253  df-mulr 17254  df-starv 17255  df-sca 17256  df-vsca 17257  df-ip 17258  df-tset 17259  df-ple 17260  df-ds 17262  df-unif 17263  df-hom 17264  df-cco 17265  df-rest 17411  df-topn 17412  df-0g 17430  df-gsum 17431  df-topgen 17432  df-pt 17433  df-prds 17436  df-xrs 17491  df-qtop 17496  df-imas 17497  df-xps 17499  df-mre 17573  df-mrc 17574  df-acs 17576  df-mgm 18607  df-sgrp 18686  df-mnd 18702  df-submnd 18748  df-mulg 19031  df-cntz 19275  df-cmn 19744  df-psmet 21278  df-xmet 21279  df-met 21280  df-bl 21281  df-mopn 21282  df-fbas 21283  df-fg 21284  df-cnfld 21287  df-top 22816  df-topon 22833  df-topsp 22855  df-bases 22869  df-cld 22943  df-ntr 22944  df-cls 22945  df-nei 23022  df-lp 23060  df-perf 23061  df-cn 23151  df-cnp 23152  df-haus 23239  df-tx 23486  df-hmeo 23679  df-fil 23770  df-fm 23862  df-flim 23863  df-flf 23864  df-xms 24246  df-ms 24247  df-tms 24248  df-cncf 24818  df-limc 25815  df-dv 25816  df-log 26510  df-cxp 26511  df-logb 26717  df-blen 47721  df-dig 47747
This theorem is referenced by:  nn0sumshdiglem2  47773
  Copyright terms: Public domain W3C validator