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

Theorem dchrisum0 26666
Description: The sum Σ𝑛 ∈ ℕ, 𝑋(𝑛) / 𝑛 is nonzero for all non-principal Dirichlet characters (i.e. the assumption 𝑋𝑊 is contradictory). This is the key result that allows us to eliminate the conditionals from dchrmusum2 26640 and dchrvmasumif 26649. Lemma 9.4.4 of [Shapiro], p. 382. (Contributed by Mario Carneiro, 12-May-2016.)
Hypotheses
Ref Expression
rpvmasum.z 𝑍 = (ℤ/nℤ‘𝑁)
rpvmasum.l 𝐿 = (ℤRHom‘𝑍)
rpvmasum.a (𝜑𝑁 ∈ ℕ)
rpvmasum2.g 𝐺 = (DChr‘𝑁)
rpvmasum2.d 𝐷 = (Base‘𝐺)
rpvmasum2.1 1 = (0g𝐺)
rpvmasum2.w 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿𝑚)) / 𝑚) = 0}
dchrisum0.b (𝜑𝑋𝑊)
Assertion
Ref Expression
dchrisum0 ¬ 𝜑
Distinct variable groups:   𝑦,𝑚, 1   𝑚,𝑁,𝑦   𝜑,𝑚   𝑚,𝑍,𝑦   𝐷,𝑚,𝑦   𝑚,𝐿,𝑦   𝑚,𝑋,𝑦
Allowed substitution hints:   𝜑(𝑦)   𝐺(𝑦,𝑚)   𝑊(𝑦,𝑚)

Proof of Theorem dchrisum0
Dummy variables 𝑘 𝑥 𝑧 𝑐 𝑖 𝑡 𝑑 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rpvmasum.z . 2 𝑍 = (ℤ/nℤ‘𝑁)
2 rpvmasum.l . 2 𝐿 = (ℤRHom‘𝑍)
3 rpvmasum.a . 2 (𝜑𝑁 ∈ ℕ)
4 rpvmasum2.g . 2 𝐺 = (DChr‘𝑁)
5 rpvmasum2.d . 2 𝐷 = (Base‘𝐺)
6 rpvmasum2.1 . 2 1 = (0g𝐺)
7 eqid 2740 . 2 (𝑏 ∈ ℕ ↦ Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖𝑏} (𝑋‘(𝐿𝑦))) = (𝑏 ∈ ℕ ↦ Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖𝑏} (𝑋‘(𝐿𝑦)))
8 rpvmasum2.w . . . . 5 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿𝑚)) / 𝑚) = 0}
98ssrab3 4020 . . . 4 𝑊 ⊆ (𝐷 ∖ { 1 })
10 difss 4071 . . . 4 (𝐷 ∖ { 1 }) ⊆ 𝐷
119, 10sstri 3935 . . 3 𝑊𝐷
12 dchrisum0.b . . 3 (𝜑𝑋𝑊)
1311, 12sselid 3924 . 2 (𝜑𝑋𝐷)
141, 2, 3, 4, 5, 6, 8, 12dchrisum0re 26659 . 2 (𝜑𝑋:(Base‘𝑍)⟶ℝ)
15 fveq2 6771 . . . . . . . 8 (𝑘 = (𝑚 · 𝑑) → (√‘𝑘) = (√‘(𝑚 · 𝑑)))
1615oveq2d 7287 . . . . . . 7 (𝑘 = (𝑚 · 𝑑) → ((𝑋‘(𝐿𝑚)) / (√‘𝑘)) = ((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑))))
17 rpre 12737 . . . . . . . 8 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
1817adantl 482 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ)
1913ad3antrrr 727 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖𝑘}) → 𝑋𝐷)
20 elrabi 3620 . . . . . . . . . . . 12 (𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖𝑘} → 𝑚 ∈ ℕ)
2120nnzd 12424 . . . . . . . . . . 11 (𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖𝑘} → 𝑚 ∈ ℤ)
2221adantl 482 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖𝑘}) → 𝑚 ∈ ℤ)
234, 1, 5, 2, 19, 22dchrzrhcl 26391 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖𝑘}) → (𝑋‘(𝐿𝑚)) ∈ ℂ)
24 elfznn 13284 . . . . . . . . . . . . . 14 (𝑘 ∈ (1...(⌊‘𝑥)) → 𝑘 ∈ ℕ)
2524adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → 𝑘 ∈ ℕ)
2625nnrpd 12769 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → 𝑘 ∈ ℝ+)
2726rpsqrtcld 15121 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → (√‘𝑘) ∈ ℝ+)
2827rpcnd 12773 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → (√‘𝑘) ∈ ℂ)
2928adantr 481 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖𝑘}) → (√‘𝑘) ∈ ℂ)
3027rpne0d 12776 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → (√‘𝑘) ≠ 0)
3130adantr 481 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖𝑘}) → (√‘𝑘) ≠ 0)
3223, 29, 31divcld 11751 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖𝑘}) → ((𝑋‘(𝐿𝑚)) / (√‘𝑘)) ∈ ℂ)
3332anasss 467 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖𝑘})) → ((𝑋‘(𝐿𝑚)) / (√‘𝑘)) ∈ ℂ)
3416, 18, 33dvdsflsumcom 26335 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖𝑘} ((𝑋‘(𝐿𝑚)) / (√‘𝑘)) = Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘(𝑥 / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑))))
351, 2, 3, 4, 5, 6, 7dchrisum0fval 26651 . . . . . . . . . 10 (𝑘 ∈ ℕ → ((𝑏 ∈ ℕ ↦ Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖𝑏} (𝑋‘(𝐿𝑦)))‘𝑘) = Σ𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖𝑘} (𝑋‘(𝐿𝑚)))
3625, 35syl 17 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → ((𝑏 ∈ ℕ ↦ Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖𝑏} (𝑋‘(𝐿𝑦)))‘𝑘) = Σ𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖𝑘} (𝑋‘(𝐿𝑚)))
3736oveq1d 7286 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → (((𝑏 ∈ ℕ ↦ Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖𝑏} (𝑋‘(𝐿𝑦)))‘𝑘) / (√‘𝑘)) = (Σ𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖𝑘} (𝑋‘(𝐿𝑚)) / (√‘𝑘)))
38 fzfid 13691 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → (1...𝑘) ∈ Fin)
39 dvdsssfz1 16025 . . . . . . . . . . 11 (𝑘 ∈ ℕ → {𝑖 ∈ ℕ ∣ 𝑖𝑘} ⊆ (1...𝑘))
4025, 39syl 17 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → {𝑖 ∈ ℕ ∣ 𝑖𝑘} ⊆ (1...𝑘))
4138, 40ssfid 9020 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → {𝑖 ∈ ℕ ∣ 𝑖𝑘} ∈ Fin)
4241, 28, 23, 30fsumdivc 15496 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖𝑘} (𝑋‘(𝐿𝑚)) / (√‘𝑘)) = Σ𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖𝑘} ((𝑋‘(𝐿𝑚)) / (√‘𝑘)))
4337, 42eqtrd 2780 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → (((𝑏 ∈ ℕ ↦ Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖𝑏} (𝑋‘(𝐿𝑦)))‘𝑘) / (√‘𝑘)) = Σ𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖𝑘} ((𝑋‘(𝐿𝑚)) / (√‘𝑘)))
4443sumeq2dv 15413 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → Σ𝑘 ∈ (1...(⌊‘𝑥))(((𝑏 ∈ ℕ ↦ Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖𝑏} (𝑋‘(𝐿𝑦)))‘𝑘) / (√‘𝑘)) = Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ {𝑖 ∈ ℕ ∣ 𝑖𝑘} ((𝑋‘(𝐿𝑚)) / (√‘𝑘)))
45 rprege0 12744 . . . . . . . . . . 11 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
4645adantl 482 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
47 resqrtth 14965 . . . . . . . . . 10 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → ((√‘𝑥)↑2) = 𝑥)
4846, 47syl 17 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ+) → ((√‘𝑥)↑2) = 𝑥)
4948fveq2d 6775 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ+) → (⌊‘((√‘𝑥)↑2)) = (⌊‘𝑥))
5049oveq2d 7287 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → (1...(⌊‘((√‘𝑥)↑2))) = (1...(⌊‘𝑥)))
5148fvoveq1d 7293 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ+) → (⌊‘(((√‘𝑥)↑2) / 𝑚)) = (⌊‘(𝑥 / 𝑚)))
5251oveq2d 7287 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ+) → (1...(⌊‘(((√‘𝑥)↑2) / 𝑚))) = (1...(⌊‘(𝑥 / 𝑚))))
5352sumeq1d 15411 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ+) → Σ𝑑 ∈ (1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑑 ∈ (1...(⌊‘(𝑥 / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑))))
5453adantr 481 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘((√‘𝑥)↑2)))) → Σ𝑑 ∈ (1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑑 ∈ (1...(⌊‘(𝑥 / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑))))
5550, 54sumeq12dv 15416 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → Σ𝑚 ∈ (1...(⌊‘((√‘𝑥)↑2)))Σ𝑑 ∈ (1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘(𝑥 / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑))))
5634, 44, 553eqtr4d 2790 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → Σ𝑘 ∈ (1...(⌊‘𝑥))(((𝑏 ∈ ℕ ↦ Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖𝑏} (𝑋‘(𝐿𝑦)))‘𝑘) / (√‘𝑘)) = Σ𝑚 ∈ (1...(⌊‘((√‘𝑥)↑2)))Σ𝑑 ∈ (1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑))))
5756mpteq2dva 5179 . . . 4 (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑘 ∈ (1...(⌊‘𝑥))(((𝑏 ∈ ℕ ↦ Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖𝑏} (𝑋‘(𝐿𝑦)))‘𝑘) / (√‘𝑘))) = (𝑥 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘((√‘𝑥)↑2)))Σ𝑑 ∈ (1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑)))))
58 rpsqrtcl 14974 . . . . . 6 (𝑥 ∈ ℝ+ → (√‘𝑥) ∈ ℝ+)
5958adantl 482 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → (√‘𝑥) ∈ ℝ+)
60 eqidd 2741 . . . . 5 (𝜑 → (𝑥 ∈ ℝ+ ↦ (√‘𝑥)) = (𝑥 ∈ ℝ+ ↦ (√‘𝑥)))
61 eqidd 2741 . . . . 5 (𝜑 → (𝑧 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑)))) = (𝑧 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑)))))
62 oveq1 7278 . . . . . . . 8 (𝑧 = (√‘𝑥) → (𝑧↑2) = ((√‘𝑥)↑2))
6362fveq2d 6775 . . . . . . 7 (𝑧 = (√‘𝑥) → (⌊‘(𝑧↑2)) = (⌊‘((√‘𝑥)↑2)))
6463oveq2d 7287 . . . . . 6 (𝑧 = (√‘𝑥) → (1...(⌊‘(𝑧↑2))) = (1...(⌊‘((√‘𝑥)↑2))))
6562fvoveq1d 7293 . . . . . . . . 9 (𝑧 = (√‘𝑥) → (⌊‘((𝑧↑2) / 𝑚)) = (⌊‘(((√‘𝑥)↑2) / 𝑚)))
6665oveq2d 7287 . . . . . . . 8 (𝑧 = (√‘𝑥) → (1...(⌊‘((𝑧↑2) / 𝑚))) = (1...(⌊‘(((√‘𝑥)↑2) / 𝑚))))
6766sumeq1d 15411 . . . . . . 7 (𝑧 = (√‘𝑥) → Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑑 ∈ (1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑))))
6867adantr 481 . . . . . 6 ((𝑧 = (√‘𝑥) ∧ 𝑚 ∈ (1...(⌊‘(𝑧↑2)))) → Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑑 ∈ (1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑))))
6964, 68sumeq12dv 15416 . . . . 5 (𝑧 = (√‘𝑥) → Σ𝑚 ∈ (1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑚 ∈ (1...(⌊‘((√‘𝑥)↑2)))Σ𝑑 ∈ (1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑))))
7059, 60, 61, 69fmptco 6998 . . . 4 (𝜑 → ((𝑧 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑)))) ∘ (𝑥 ∈ ℝ+ ↦ (√‘𝑥))) = (𝑥 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘((√‘𝑥)↑2)))Σ𝑑 ∈ (1...(⌊‘(((√‘𝑥)↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑)))))
7157, 70eqtr4d 2783 . . 3 (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑘 ∈ (1...(⌊‘𝑥))(((𝑏 ∈ ℕ ↦ Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖𝑏} (𝑋‘(𝐿𝑦)))‘𝑘) / (√‘𝑘))) = ((𝑧 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑)))) ∘ (𝑥 ∈ ℝ+ ↦ (√‘𝑥))))
72 eqid 2740 . . . . . . . 8 (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / (√‘𝑎))) = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / (√‘𝑎)))
731, 2, 3, 4, 5, 6, 8, 12, 72dchrisum0lema 26660 . . . . . . 7 (𝜑 → ∃𝑡𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))))
743adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))))) → 𝑁 ∈ ℕ)
7512adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))))) → 𝑋𝑊)
76 simprl 768 . . . . . . . . . 10 ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))))) → 𝑐 ∈ (0[,)+∞))
77 simprrl 778 . . . . . . . . . 10 ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))))) → seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / (√‘𝑎)))) ⇝ 𝑡)
78 simprrr 779 . . . . . . . . . 10 ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))))) → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦)))
791, 2, 74, 4, 5, 6, 8, 75, 72, 76, 77, 78dchrisum0lem3 26665 . . . . . . . . 9 ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))))) → (𝑧 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ 𝑂(1))
8079rexlimdvaa 3216 . . . . . . . 8 (𝜑 → (∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))) → (𝑧 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ 𝑂(1)))
8180exlimdv 1940 . . . . . . 7 (𝜑 → (∃𝑡𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / (√‘𝑎)))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿𝑎)) / (√‘𝑎))))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))) → (𝑧 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ 𝑂(1)))
8273, 81mpd 15 . . . . . 6 (𝜑 → (𝑧 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ 𝑂(1))
83 o1f 15236 . . . . . 6 ((𝑧 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ 𝑂(1) → (𝑧 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑)))):dom (𝑧 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑))))⟶ℂ)
8482, 83syl 17 . . . . 5 (𝜑 → (𝑧 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑)))):dom (𝑧 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑))))⟶ℂ)
85 sumex 15397 . . . . . . 7 Σ𝑚 ∈ (1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑))) ∈ V
86 eqid 2740 . . . . . . 7 (𝑧 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑)))) = (𝑧 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑))))
8785, 86dmmpti 6575 . . . . . 6 dom (𝑧 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑)))) = ℝ+
8887feq2i 6590 . . . . 5 ((𝑧 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑)))):dom (𝑧 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑))))⟶ℂ ↔ (𝑧 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑)))):ℝ+⟶ℂ)
8984, 88sylib 217 . . . 4 (𝜑 → (𝑧 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑)))):ℝ+⟶ℂ)
90 rpssre 12736 . . . . 5 + ⊆ ℝ
9190a1i 11 . . . 4 (𝜑 → ℝ+ ⊆ ℝ)
92 resqcl 13842 . . . . 5 (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℝ)
93 0red 10979 . . . . . . . 8 (((𝜑𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) → 0 ∈ ℝ)
94 simplr 766 . . . . . . . 8 (((𝜑𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) → 𝑡 ∈ ℝ)
95 simplrr 775 . . . . . . . . . 10 ((((𝜑𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → (𝑡↑2) ≤ 𝑥)
9645ad2antrl 725 . . . . . . . . . . . 12 (((𝜑𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
9796adantr 481 . . . . . . . . . . 11 ((((𝜑𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
9897, 47syl 17 . . . . . . . . . 10 ((((𝜑𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → ((√‘𝑥)↑2) = 𝑥)
9995, 98breqtrrd 5107 . . . . . . . . 9 ((((𝜑𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → (𝑡↑2) ≤ ((√‘𝑥)↑2))
10094adantr 481 . . . . . . . . . 10 ((((𝜑𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → 𝑡 ∈ ℝ)
10159rpred 12771 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ+) → (√‘𝑥) ∈ ℝ)
102101ad2ant2r 744 . . . . . . . . . . 11 (((𝜑𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) → (√‘𝑥) ∈ ℝ)
103102adantr 481 . . . . . . . . . 10 ((((𝜑𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → (√‘𝑥) ∈ ℝ)
104 simpr 485 . . . . . . . . . 10 ((((𝜑𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → 0 ≤ 𝑡)
105 sqrtge0 14967 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → 0 ≤ (√‘𝑥))
10696, 105syl 17 . . . . . . . . . . 11 (((𝜑𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) → 0 ≤ (√‘𝑥))
107106adantr 481 . . . . . . . . . 10 ((((𝜑𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → 0 ≤ (√‘𝑥))
108100, 103, 104, 107le2sqd 13972 . . . . . . . . 9 ((((𝜑𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → (𝑡 ≤ (√‘𝑥) ↔ (𝑡↑2) ≤ ((√‘𝑥)↑2)))
10999, 108mpbird 256 . . . . . . . 8 ((((𝜑𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 0 ≤ 𝑡) → 𝑡 ≤ (√‘𝑥))
11094adantr 481 . . . . . . . . 9 ((((𝜑𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 𝑡 ≤ 0) → 𝑡 ∈ ℝ)
111 0red 10979 . . . . . . . . 9 ((((𝜑𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 𝑡 ≤ 0) → 0 ∈ ℝ)
112102adantr 481 . . . . . . . . 9 ((((𝜑𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 𝑡 ≤ 0) → (√‘𝑥) ∈ ℝ)
113 simpr 485 . . . . . . . . 9 ((((𝜑𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 𝑡 ≤ 0) → 𝑡 ≤ 0)
114106adantr 481 . . . . . . . . 9 ((((𝜑𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 𝑡 ≤ 0) → 0 ≤ (√‘𝑥))
115110, 111, 112, 113, 114letrd 11132 . . . . . . . 8 ((((𝜑𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) ∧ 𝑡 ≤ 0) → 𝑡 ≤ (√‘𝑥))
11693, 94, 109, 115lecasei 11081 . . . . . . 7 (((𝜑𝑡 ∈ ℝ) ∧ (𝑥 ∈ ℝ+ ∧ (𝑡↑2) ≤ 𝑥)) → 𝑡 ≤ (√‘𝑥))
117116expr 457 . . . . . 6 (((𝜑𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → ((𝑡↑2) ≤ 𝑥𝑡 ≤ (√‘𝑥)))
118117ralrimiva 3110 . . . . 5 ((𝜑𝑡 ∈ ℝ) → ∀𝑥 ∈ ℝ+ ((𝑡↑2) ≤ 𝑥𝑡 ≤ (√‘𝑥)))
119 breq1 5082 . . . . . 6 (𝑐 = (𝑡↑2) → (𝑐𝑥 ↔ (𝑡↑2) ≤ 𝑥))
120119rspceaimv 3566 . . . . 5 (((𝑡↑2) ∈ ℝ ∧ ∀𝑥 ∈ ℝ+ ((𝑡↑2) ≤ 𝑥𝑡 ≤ (√‘𝑥))) → ∃𝑐 ∈ ℝ ∀𝑥 ∈ ℝ+ (𝑐𝑥𝑡 ≤ (√‘𝑥)))
12192, 118, 120syl2an2 683 . . . 4 ((𝜑𝑡 ∈ ℝ) → ∃𝑐 ∈ ℝ ∀𝑥 ∈ ℝ+ (𝑐𝑥𝑡 ≤ (√‘𝑥)))
12289, 82, 59, 91, 121o1compt 15294 . . 3 (𝜑 → ((𝑧 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘(𝑧↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑧↑2) / 𝑚)))((𝑋‘(𝐿𝑚)) / (√‘(𝑚 · 𝑑)))) ∘ (𝑥 ∈ ℝ+ ↦ (√‘𝑥))) ∈ 𝑂(1))
12371, 122eqeltrd 2841 . 2 (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑘 ∈ (1...(⌊‘𝑥))(((𝑏 ∈ ℕ ↦ Σ𝑦 ∈ {𝑖 ∈ ℕ ∣ 𝑖𝑏} (𝑋‘(𝐿𝑦)))‘𝑘) / (√‘𝑘))) ∈ 𝑂(1))
1241, 2, 3, 4, 5, 6, 7, 13, 14, 123dchrisum0fno1 26657 1 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396   = wceq 1542  wex 1786  wcel 2110  wne 2945  wral 3066  wrex 3067  {crab 3070  cdif 3889  wss 3892  {csn 4567   class class class wbr 5079  cmpt 5162  dom cdm 5590  ccom 5594  wf 6428  cfv 6432  (class class class)co 7271  cc 10870  cr 10871  0cc0 10872  1c1 10873   + caddc 10875   · cmul 10877  +∞cpnf 11007  cle 11011  cmin 11205   / cdiv 11632  cn 11973  2c2 12028  cz 12319  +crp 12729  [,)cico 13080  ...cfz 13238  cfl 13508  seqcseq 13719  cexp 13780  csqrt 14942  abscabs 14943  cli 15191  𝑂(1)co1 15193  Σcsu 15395  cdvds 15961  Basecbs 16910  0gc0g 17148  ℤRHomczrh 20699  ℤ/nczn 20702  DChrcdchr 26378
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-rep 5214  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7582  ax-inf2 9377  ax-cnex 10928  ax-resscn 10929  ax-1cn 10930  ax-icn 10931  ax-addcl 10932  ax-addrcl 10933  ax-mulcl 10934  ax-mulrcl 10935  ax-mulcom 10936  ax-addass 10937  ax-mulass 10938  ax-distr 10939  ax-i2m1 10940  ax-1ne0 10941  ax-1rid 10942  ax-rnegex 10943  ax-rrecex 10944  ax-cnre 10945  ax-pre-lttri 10946  ax-pre-lttrn 10947  ax-pre-ltadd 10948  ax-pre-mulgt0 10949  ax-pre-sup 10950  ax-addf 10951  ax-mulf 10952
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-nel 3052  df-ral 3071  df-rex 3072  df-reu 3073  df-rmo 3074  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4846  df-int 4886  df-iun 4932  df-iin 4933  df-disj 5045  df-br 5080  df-opab 5142  df-mpt 5163  df-tr 5197  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-se 5546  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6201  df-ord 6268  df-on 6269  df-lim 6270  df-suc 6271  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-f1 6437  df-fo 6438  df-f1o 6439  df-fv 6440  df-isom 6441  df-riota 7228  df-ov 7274  df-oprab 7275  df-mpo 7276  df-of 7527  df-rpss 7570  df-om 7707  df-1st 7824  df-2nd 7825  df-supp 7969  df-tpos 8033  df-frecs 8088  df-wrecs 8119  df-recs 8193  df-rdg 8232  df-1o 8288  df-2o 8289  df-oadd 8292  df-omul 8293  df-er 8481  df-ec 8483  df-qs 8487  df-map 8600  df-pm 8601  df-ixp 8669  df-en 8717  df-dom 8718  df-sdom 8719  df-fin 8720  df-fsupp 9107  df-fi 9148  df-sup 9179  df-inf 9180  df-oi 9247  df-dju 9660  df-card 9698  df-acn 9701  df-pnf 11012  df-mnf 11013  df-xr 11014  df-ltxr 11015  df-le 11016  df-sub 11207  df-neg 11208  df-div 11633  df-nn 11974  df-2 12036  df-3 12037  df-4 12038  df-5 12039  df-6 12040  df-7 12041  df-8 12042  df-9 12043  df-n0 12234  df-xnn0 12306  df-z 12320  df-dec 12437  df-uz 12582  df-q 12688  df-rp 12730  df-xneg 12847  df-xadd 12848  df-xmul 12849  df-ioo 13082  df-ioc 13083  df-ico 13084  df-icc 13085  df-fz 13239  df-fzo 13382  df-fl 13510  df-mod 13588  df-seq 13720  df-exp 13781  df-fac 13986  df-bc 14015  df-hash 14043  df-word 14216  df-concat 14272  df-s1 14299  df-shft 14776  df-cj 14808  df-re 14809  df-im 14810  df-sqrt 14944  df-abs 14945  df-limsup 15178  df-clim 15195  df-rlim 15196  df-o1 15197  df-lo1 15198  df-sum 15396  df-ef 15775  df-e 15776  df-sin 15777  df-cos 15778  df-tan 15779  df-pi 15780  df-dvds 15962  df-gcd 16200  df-prm 16375  df-numer 16437  df-denom 16438  df-phi 16465  df-pc 16536  df-struct 16846  df-sets 16863  df-slot 16881  df-ndx 16893  df-base 16911  df-ress 16940  df-plusg 16973  df-mulr 16974  df-starv 16975  df-sca 16976  df-vsca 16977  df-ip 16978  df-tset 16979  df-ple 16980  df-ds 16982  df-unif 16983  df-hom 16984  df-cco 16985  df-rest 17131  df-topn 17132  df-0g 17150  df-gsum 17151  df-topgen 17152  df-pt 17153  df-prds 17156  df-xrs 17211  df-qtop 17216  df-imas 17217  df-qus 17218  df-xps 17219  df-mre 17293  df-mrc 17294  df-acs 17296  df-mgm 18324  df-sgrp 18373  df-mnd 18384  df-mhm 18428  df-submnd 18429  df-grp 18578  df-minusg 18579  df-sbg 18580  df-mulg 18699  df-subg 18750  df-nsg 18751  df-eqg 18752  df-ghm 18830  df-gim 18873  df-ga 18894  df-cntz 18921  df-oppg 18948  df-od 19134  df-gex 19135  df-pgp 19136  df-lsm 19239  df-pj1 19240  df-cmn 19386  df-abl 19387  df-cyg 19476  df-dprd 19596  df-dpj 19597  df-mgp 19719  df-ur 19736  df-ring 19783  df-cring 19784  df-oppr 19860  df-dvdsr 19881  df-unit 19882  df-invr 19912  df-dvr 19923  df-rnghom 19957  df-drng 19991  df-subrg 20020  df-lmod 20123  df-lss 20192  df-lsp 20232  df-sra 20432  df-rgmod 20433  df-lidl 20434  df-rsp 20435  df-2idl 20501  df-psmet 20587  df-xmet 20588  df-met 20589  df-bl 20590  df-mopn 20591  df-fbas 20592  df-fg 20593  df-cnfld 20596  df-zring 20669  df-zrh 20703  df-zn 20706  df-top 22041  df-topon 22058  df-topsp 22080  df-bases 22094  df-cld 22168  df-ntr 22169  df-cls 22170  df-nei 22247  df-lp 22285  df-perf 22286  df-cn 22376  df-cnp 22377  df-haus 22464  df-cmp 22536  df-tx 22711  df-hmeo 22904  df-fil 22995  df-fm 23087  df-flim 23088  df-flf 23089  df-xms 23471  df-ms 23472  df-tms 23473  df-cncf 24039  df-0p 24832  df-limc 25028  df-dv 25029  df-ply 25347  df-idp 25348  df-coe 25349  df-dgr 25350  df-quot 25449  df-ulm 25534  df-log 25710  df-cxp 25711  df-atan 26015  df-em 26140  df-cht 26244  df-vma 26245  df-chp 26246  df-ppi 26247  df-mu 26248  df-dchr 26379
This theorem is referenced by:  dchrisumn0  26667  rpvmasum  26672
  Copyright terms: Public domain W3C validator