| Step | Hyp | Ref
| Expression |
| 1 | | nnuz 12921 |
. 2
⊢ ℕ =
(ℤ≥‘1) |
| 2 | | 1zzd 12648 |
. 2
⊢ (𝜑 → 1 ∈
ℤ) |
| 3 | | oveq1 7438 |
. . . . 5
⊢ (𝑛 = 𝑘 → (𝑛↑𝑐-(ℜ‘𝑆)) = (𝑘↑𝑐-(ℜ‘𝑆))) |
| 4 | | eqid 2737 |
. . . . 5
⊢ (𝑛 ∈ ℕ ↦ (𝑛↑𝑐-(ℜ‘𝑆))) = (𝑛 ∈ ℕ ↦ (𝑛↑𝑐-(ℜ‘𝑆))) |
| 5 | | ovex 7464 |
. . . . 5
⊢ (𝑘↑𝑐-(ℜ‘𝑆)) ∈ V |
| 6 | 3, 4, 5 | fvmpt 7016 |
. . . 4
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑛↑𝑐-(ℜ‘𝑆)))‘𝑘) = (𝑘↑𝑐-(ℜ‘𝑆))) |
| 7 | 6 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑛↑𝑐-(ℜ‘𝑆)))‘𝑘) = (𝑘↑𝑐-(ℜ‘𝑆))) |
| 8 | | zetacvg.3 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = (𝑘↑𝑐-𝑆)) |
| 9 | | nncn 12274 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) |
| 10 | 9 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℂ) |
| 11 | | nnne0 12300 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → 𝑘 ≠ 0) |
| 12 | 11 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ≠ 0) |
| 13 | | zetacvg.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ ℂ) |
| 14 | 13 | negcld 11607 |
. . . . . . . 8
⊢ (𝜑 → -𝑆 ∈ ℂ) |
| 15 | 14 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → -𝑆 ∈ ℂ) |
| 16 | 10, 12, 15 | cxpefd 26754 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘↑𝑐-𝑆) = (exp‘(-𝑆 · (log‘𝑘)))) |
| 17 | 8, 16 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = (exp‘(-𝑆 · (log‘𝑘)))) |
| 18 | 17 | fveq2d 6910 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(𝐹‘𝑘)) = (abs‘(exp‘(-𝑆 · (log‘𝑘))))) |
| 19 | | nnrp 13046 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ+) |
| 20 | 19 | relogcld 26665 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ →
(log‘𝑘) ∈
ℝ) |
| 21 | 20 | recnd 11289 |
. . . . . 6
⊢ (𝑘 ∈ ℕ →
(log‘𝑘) ∈
ℂ) |
| 22 | | mulcl 11239 |
. . . . . 6
⊢ ((-𝑆 ∈ ℂ ∧
(log‘𝑘) ∈
ℂ) → (-𝑆
· (log‘𝑘))
∈ ℂ) |
| 23 | 14, 21, 22 | syl2an 596 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (-𝑆 · (log‘𝑘)) ∈ ℂ) |
| 24 | | absef 16233 |
. . . . 5
⊢ ((-𝑆 · (log‘𝑘)) ∈ ℂ →
(abs‘(exp‘(-𝑆
· (log‘𝑘)))) =
(exp‘(ℜ‘(-𝑆 · (log‘𝑘))))) |
| 25 | 23, 24 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
(abs‘(exp‘(-𝑆
· (log‘𝑘)))) =
(exp‘(ℜ‘(-𝑆 · (log‘𝑘))))) |
| 26 | | remul 15168 |
. . . . . . . 8
⊢ ((-𝑆 ∈ ℂ ∧
(log‘𝑘) ∈
ℂ) → (ℜ‘(-𝑆 · (log‘𝑘))) = (((ℜ‘-𝑆) · (ℜ‘(log‘𝑘))) −
((ℑ‘-𝑆)
· (ℑ‘(log‘𝑘))))) |
| 27 | 14, 21, 26 | syl2an 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (ℜ‘(-𝑆 · (log‘𝑘))) = (((ℜ‘-𝑆) ·
(ℜ‘(log‘𝑘))) − ((ℑ‘-𝑆) ·
(ℑ‘(log‘𝑘))))) |
| 28 | 13 | renegd 15248 |
. . . . . . . . 9
⊢ (𝜑 → (ℜ‘-𝑆) = -(ℜ‘𝑆)) |
| 29 | 20 | rered 15263 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ →
(ℜ‘(log‘𝑘)) = (log‘𝑘)) |
| 30 | 28, 29 | oveqan12d 7450 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ℜ‘-𝑆) ·
(ℜ‘(log‘𝑘))) = (-(ℜ‘𝑆) · (log‘𝑘))) |
| 31 | 20 | reim0d 15264 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ →
(ℑ‘(log‘𝑘)) = 0) |
| 32 | 31 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ →
((ℑ‘-𝑆)
· (ℑ‘(log‘𝑘))) = ((ℑ‘-𝑆) · 0)) |
| 33 | | imcl 15150 |
. . . . . . . . . . . 12
⊢ (-𝑆 ∈ ℂ →
(ℑ‘-𝑆) ∈
ℝ) |
| 34 | 33 | recnd 11289 |
. . . . . . . . . . 11
⊢ (-𝑆 ∈ ℂ →
(ℑ‘-𝑆) ∈
ℂ) |
| 35 | 14, 34 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (ℑ‘-𝑆) ∈
ℂ) |
| 36 | 35 | mul01d 11460 |
. . . . . . . . 9
⊢ (𝜑 → ((ℑ‘-𝑆) · 0) =
0) |
| 37 | 32, 36 | sylan9eqr 2799 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
((ℑ‘-𝑆)
· (ℑ‘(log‘𝑘))) = 0) |
| 38 | 30, 37 | oveq12d 7449 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
(((ℜ‘-𝑆)
· (ℜ‘(log‘𝑘))) − ((ℑ‘-𝑆) ·
(ℑ‘(log‘𝑘)))) = ((-(ℜ‘𝑆) · (log‘𝑘)) − 0)) |
| 39 | 13 | recld 15233 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℜ‘𝑆) ∈
ℝ) |
| 40 | 39 | renegcld 11690 |
. . . . . . . . . 10
⊢ (𝜑 → -(ℜ‘𝑆) ∈
ℝ) |
| 41 | 40 | recnd 11289 |
. . . . . . . . 9
⊢ (𝜑 → -(ℜ‘𝑆) ∈
ℂ) |
| 42 | | mulcl 11239 |
. . . . . . . . 9
⊢
((-(ℜ‘𝑆)
∈ ℂ ∧ (log‘𝑘) ∈ ℂ) →
(-(ℜ‘𝑆) ·
(log‘𝑘)) ∈
ℂ) |
| 43 | 41, 21, 42 | syl2an 596 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (-(ℜ‘𝑆) · (log‘𝑘)) ∈
ℂ) |
| 44 | 43 | subid1d 11609 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
((-(ℜ‘𝑆)
· (log‘𝑘))
− 0) = (-(ℜ‘𝑆) · (log‘𝑘))) |
| 45 | 27, 38, 44 | 3eqtrd 2781 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (ℜ‘(-𝑆 · (log‘𝑘))) = (-(ℜ‘𝑆) · (log‘𝑘))) |
| 46 | 45 | fveq2d 6910 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
(exp‘(ℜ‘(-𝑆 · (log‘𝑘)))) = (exp‘(-(ℜ‘𝑆) · (log‘𝑘)))) |
| 47 | 41 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → -(ℜ‘𝑆) ∈
ℂ) |
| 48 | 10, 12, 47 | cxpefd 26754 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘↑𝑐-(ℜ‘𝑆)) =
(exp‘(-(ℜ‘𝑆) · (log‘𝑘)))) |
| 49 | 46, 48 | eqtr4d 2780 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
(exp‘(ℜ‘(-𝑆 · (log‘𝑘)))) = (𝑘↑𝑐-(ℜ‘𝑆))) |
| 50 | 18, 25, 49 | 3eqtrd 2781 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(𝐹‘𝑘)) = (𝑘↑𝑐-(ℜ‘𝑆))) |
| 51 | 7, 50 | eqtr4d 2780 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑛↑𝑐-(ℜ‘𝑆)))‘𝑘) = (abs‘(𝐹‘𝑘))) |
| 52 | 10, 15 | cxpcld 26750 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘↑𝑐-𝑆) ∈ ℂ) |
| 53 | 8, 52 | eqeltrd 2841 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) |
| 54 | | 2rp 13039 |
. . . . . . 7
⊢ 2 ∈
ℝ+ |
| 55 | | 1re 11261 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
| 56 | | resubcl 11573 |
. . . . . . . 8
⊢ ((1
∈ ℝ ∧ (ℜ‘𝑆) ∈ ℝ) → (1 −
(ℜ‘𝑆)) ∈
ℝ) |
| 57 | 55, 39, 56 | sylancr 587 |
. . . . . . 7
⊢ (𝜑 → (1 −
(ℜ‘𝑆)) ∈
ℝ) |
| 58 | | rpcxpcl 26718 |
. . . . . . 7
⊢ ((2
∈ ℝ+ ∧ (1 − (ℜ‘𝑆)) ∈ ℝ) →
(2↑𝑐(1 − (ℜ‘𝑆))) ∈
ℝ+) |
| 59 | 54, 57, 58 | sylancr 587 |
. . . . . 6
⊢ (𝜑 →
(2↑𝑐(1 − (ℜ‘𝑆))) ∈
ℝ+) |
| 60 | 59 | rpcnd 13079 |
. . . . 5
⊢ (𝜑 →
(2↑𝑐(1 − (ℜ‘𝑆))) ∈ ℂ) |
| 61 | | zetacvg.2 |
. . . . . . . . 9
⊢ (𝜑 → 1 < (ℜ‘𝑆)) |
| 62 | | recl 15149 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ ℂ →
(ℜ‘𝑆) ∈
ℝ) |
| 63 | 62 | recnd 11289 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ ℂ →
(ℜ‘𝑆) ∈
ℂ) |
| 64 | 13, 63 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (ℜ‘𝑆) ∈
ℂ) |
| 65 | 64 | addlidd 11462 |
. . . . . . . . 9
⊢ (𝜑 → (0 + (ℜ‘𝑆)) = (ℜ‘𝑆)) |
| 66 | 61, 65 | breqtrrd 5171 |
. . . . . . . 8
⊢ (𝜑 → 1 < (0 +
(ℜ‘𝑆))) |
| 67 | | 0re 11263 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ |
| 68 | | ltsubadd 11733 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ (ℜ‘𝑆) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((1 − (ℜ‘𝑆)) < 0 ↔ 1 < (0 +
(ℜ‘𝑆)))) |
| 69 | 55, 67, 68 | mp3an13 1454 |
. . . . . . . . 9
⊢
((ℜ‘𝑆)
∈ ℝ → ((1 − (ℜ‘𝑆)) < 0 ↔ 1 < (0 +
(ℜ‘𝑆)))) |
| 70 | 39, 69 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((1 −
(ℜ‘𝑆)) < 0
↔ 1 < (0 + (ℜ‘𝑆)))) |
| 71 | 66, 70 | mpbird 257 |
. . . . . . 7
⊢ (𝜑 → (1 −
(ℜ‘𝑆)) <
0) |
| 72 | | 2re 12340 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
| 73 | | 1lt2 12437 |
. . . . . . . . 9
⊢ 1 <
2 |
| 74 | | cxplt 26736 |
. . . . . . . . 9
⊢ (((2
∈ ℝ ∧ 1 < 2) ∧ ((1 − (ℜ‘𝑆)) ∈ ℝ ∧ 0 ∈
ℝ)) → ((1 − (ℜ‘𝑆)) < 0 ↔
(2↑𝑐(1 − (ℜ‘𝑆))) <
(2↑𝑐0))) |
| 75 | 72, 73, 74 | mpanl12 702 |
. . . . . . . 8
⊢ (((1
− (ℜ‘𝑆))
∈ ℝ ∧ 0 ∈ ℝ) → ((1 − (ℜ‘𝑆)) < 0 ↔
(2↑𝑐(1 − (ℜ‘𝑆))) <
(2↑𝑐0))) |
| 76 | 57, 67, 75 | sylancl 586 |
. . . . . . 7
⊢ (𝜑 → ((1 −
(ℜ‘𝑆)) < 0
↔ (2↑𝑐(1 − (ℜ‘𝑆))) <
(2↑𝑐0))) |
| 77 | 71, 76 | mpbid 232 |
. . . . . 6
⊢ (𝜑 →
(2↑𝑐(1 − (ℜ‘𝑆))) <
(2↑𝑐0)) |
| 78 | 59 | rprege0d 13084 |
. . . . . . 7
⊢ (𝜑 →
((2↑𝑐(1 − (ℜ‘𝑆))) ∈ ℝ ∧ 0 ≤
(2↑𝑐(1 − (ℜ‘𝑆))))) |
| 79 | | absid 15335 |
. . . . . . 7
⊢
(((2↑𝑐(1 − (ℜ‘𝑆))) ∈ ℝ ∧ 0 ≤
(2↑𝑐(1 − (ℜ‘𝑆)))) →
(abs‘(2↑𝑐(1 − (ℜ‘𝑆)))) =
(2↑𝑐(1 − (ℜ‘𝑆)))) |
| 80 | 78, 79 | syl 17 |
. . . . . 6
⊢ (𝜑 →
(abs‘(2↑𝑐(1 − (ℜ‘𝑆)))) =
(2↑𝑐(1 − (ℜ‘𝑆)))) |
| 81 | | 2cn 12341 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
| 82 | | cxp0 26712 |
. . . . . . . . 9
⊢ (2 ∈
ℂ → (2↑𝑐0) = 1) |
| 83 | 81, 82 | ax-mp 5 |
. . . . . . . 8
⊢
(2↑𝑐0) = 1 |
| 84 | 83 | eqcomi 2746 |
. . . . . . 7
⊢ 1 =
(2↑𝑐0) |
| 85 | 84 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 1 =
(2↑𝑐0)) |
| 86 | 77, 80, 85 | 3brtr4d 5175 |
. . . . 5
⊢ (𝜑 →
(abs‘(2↑𝑐(1 − (ℜ‘𝑆)))) < 1) |
| 87 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → ((2↑𝑐(1
− (ℜ‘𝑆)))↑𝑛) = ((2↑𝑐(1 −
(ℜ‘𝑆)))↑𝑚)) |
| 88 | | eqid 2737 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
↦ ((2↑𝑐(1 − (ℜ‘𝑆)))↑𝑛)) = (𝑛 ∈ ℕ0 ↦
((2↑𝑐(1 − (ℜ‘𝑆)))↑𝑛)) |
| 89 | | ovex 7464 |
. . . . . . 7
⊢
((2↑𝑐(1 − (ℜ‘𝑆)))↑𝑚) ∈ V |
| 90 | 87, 88, 89 | fvmpt 7016 |
. . . . . 6
⊢ (𝑚 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ ((2↑𝑐(1 −
(ℜ‘𝑆)))↑𝑛))‘𝑚) = ((2↑𝑐(1 −
(ℜ‘𝑆)))↑𝑚)) |
| 91 | 90 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ ((2↑𝑐(1 − (ℜ‘𝑆)))↑𝑛))‘𝑚) = ((2↑𝑐(1 −
(ℜ‘𝑆)))↑𝑚)) |
| 92 | 60, 86, 91 | geolim 15906 |
. . . 4
⊢ (𝜑 → seq0( + , (𝑛 ∈ ℕ0
↦ ((2↑𝑐(1 − (ℜ‘𝑆)))↑𝑛))) ⇝ (1 / (1 −
(2↑𝑐(1 − (ℜ‘𝑆)))))) |
| 93 | | seqex 14044 |
. . . . 5
⊢ seq0( + ,
(𝑛 ∈
ℕ0 ↦ ((2↑𝑐(1 −
(ℜ‘𝑆)))↑𝑛))) ∈ V |
| 94 | | ovex 7464 |
. . . . 5
⊢ (1 / (1
− (2↑𝑐(1 − (ℜ‘𝑆))))) ∈ V |
| 95 | 93, 94 | breldm 5919 |
. . . 4
⊢ (seq0( +
, (𝑛 ∈
ℕ0 ↦ ((2↑𝑐(1 −
(ℜ‘𝑆)))↑𝑛))) ⇝ (1 / (1 −
(2↑𝑐(1 − (ℜ‘𝑆))))) → seq0( + , (𝑛 ∈ ℕ0 ↦
((2↑𝑐(1 − (ℜ‘𝑆)))↑𝑛))) ∈ dom ⇝ ) |
| 96 | 92, 95 | syl 17 |
. . 3
⊢ (𝜑 → seq0( + , (𝑛 ∈ ℕ0
↦ ((2↑𝑐(1 − (ℜ‘𝑆)))↑𝑛))) ∈ dom ⇝ ) |
| 97 | | rpcxpcl 26718 |
. . . . . . 7
⊢ ((𝑘 ∈ ℝ+
∧ -(ℜ‘𝑆)
∈ ℝ) → (𝑘↑𝑐-(ℜ‘𝑆)) ∈
ℝ+) |
| 98 | 19, 40, 97 | syl2anr 597 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘↑𝑐-(ℜ‘𝑆)) ∈
ℝ+) |
| 99 | 98 | rpred 13077 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘↑𝑐-(ℜ‘𝑆)) ∈
ℝ) |
| 100 | 7, 99 | eqeltrd 2841 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑛↑𝑐-(ℜ‘𝑆)))‘𝑘) ∈ ℝ) |
| 101 | 98 | rpge0d 13081 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝑘↑𝑐-(ℜ‘𝑆))) |
| 102 | 101, 7 | breqtrrd 5171 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 ≤ ((𝑛 ∈ ℕ ↦ (𝑛↑𝑐-(ℜ‘𝑆)))‘𝑘)) |
| 103 | | nnre 12273 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ) |
| 104 | 103 | lep1d 12199 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → 𝑘 ≤ (𝑘 + 1)) |
| 105 | 19 | reeflogd 26666 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ →
(exp‘(log‘𝑘)) =
𝑘) |
| 106 | | peano2nn 12278 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℕ) |
| 107 | 106 | nnrpd 13075 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℝ+) |
| 108 | 107 | reeflogd 26666 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ →
(exp‘(log‘(𝑘 +
1))) = (𝑘 +
1)) |
| 109 | 104, 105,
108 | 3brtr4d 5175 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ →
(exp‘(log‘𝑘))
≤ (exp‘(log‘(𝑘 + 1)))) |
| 110 | 107 | relogcld 26665 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ →
(log‘(𝑘 + 1)) ∈
ℝ) |
| 111 | | efle 16154 |
. . . . . . . . . . . 12
⊢
(((log‘𝑘)
∈ ℝ ∧ (log‘(𝑘 + 1)) ∈ ℝ) →
((log‘𝑘) ≤
(log‘(𝑘 + 1)) ↔
(exp‘(log‘𝑘))
≤ (exp‘(log‘(𝑘 + 1))))) |
| 112 | 20, 110, 111 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ →
((log‘𝑘) ≤
(log‘(𝑘 + 1)) ↔
(exp‘(log‘𝑘))
≤ (exp‘(log‘(𝑘 + 1))))) |
| 113 | 109, 112 | mpbird 257 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ →
(log‘𝑘) ≤
(log‘(𝑘 +
1))) |
| 114 | 113 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (log‘𝑘) ≤ (log‘(𝑘 + 1))) |
| 115 | 20 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (log‘𝑘) ∈
ℝ) |
| 116 | 106 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ) |
| 117 | 116 | nnrpd 13075 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈
ℝ+) |
| 118 | 117 | relogcld 26665 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (log‘(𝑘 + 1)) ∈
ℝ) |
| 119 | 39 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (ℜ‘𝑆) ∈
ℝ) |
| 120 | 67 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈
ℝ) |
| 121 | 55 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℝ) |
| 122 | | 0lt1 11785 |
. . . . . . . . . . . . 13
⊢ 0 <
1 |
| 123 | 122 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < 1) |
| 124 | 120, 121,
39, 123, 61 | lttrd 11422 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < (ℜ‘𝑆)) |
| 125 | 124 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 <
(ℜ‘𝑆)) |
| 126 | | lemul2 12120 |
. . . . . . . . . 10
⊢
(((log‘𝑘)
∈ ℝ ∧ (log‘(𝑘 + 1)) ∈ ℝ ∧
((ℜ‘𝑆) ∈
ℝ ∧ 0 < (ℜ‘𝑆))) → ((log‘𝑘) ≤ (log‘(𝑘 + 1)) ↔ ((ℜ‘𝑆) · (log‘𝑘)) ≤ ((ℜ‘𝑆) · (log‘(𝑘 + 1))))) |
| 127 | 115, 118,
119, 125, 126 | syl112anc 1376 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((log‘𝑘) ≤ (log‘(𝑘 + 1)) ↔
((ℜ‘𝑆) ·
(log‘𝑘)) ≤
((ℜ‘𝑆) ·
(log‘(𝑘 +
1))))) |
| 128 | 114, 127 | mpbid 232 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ℜ‘𝑆) · (log‘𝑘)) ≤ ((ℜ‘𝑆) · (log‘(𝑘 + 1)))) |
| 129 | | remulcl 11240 |
. . . . . . . . . 10
⊢
(((ℜ‘𝑆)
∈ ℝ ∧ (log‘𝑘) ∈ ℝ) → ((ℜ‘𝑆) · (log‘𝑘)) ∈
ℝ) |
| 130 | 39, 20, 129 | syl2an 596 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ℜ‘𝑆) · (log‘𝑘)) ∈
ℝ) |
| 131 | | remulcl 11240 |
. . . . . . . . . 10
⊢
(((ℜ‘𝑆)
∈ ℝ ∧ (log‘(𝑘 + 1)) ∈ ℝ) →
((ℜ‘𝑆) ·
(log‘(𝑘 + 1))) ∈
ℝ) |
| 132 | 39, 110, 131 | syl2an 596 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((ℜ‘𝑆) · (log‘(𝑘 + 1))) ∈
ℝ) |
| 133 | 130, 132 | lenegd 11842 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((ℜ‘𝑆) · (log‘𝑘)) ≤ ((ℜ‘𝑆) · (log‘(𝑘 + 1))) ↔
-((ℜ‘𝑆) ·
(log‘(𝑘 + 1))) ≤
-((ℜ‘𝑆) ·
(log‘𝑘)))) |
| 134 | 128, 133 | mpbid 232 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → -((ℜ‘𝑆) · (log‘(𝑘 + 1))) ≤
-((ℜ‘𝑆) ·
(log‘𝑘))) |
| 135 | 110 | recnd 11289 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ →
(log‘(𝑘 + 1)) ∈
ℂ) |
| 136 | | mulneg1 11699 |
. . . . . . . 8
⊢
(((ℜ‘𝑆)
∈ ℂ ∧ (log‘(𝑘 + 1)) ∈ ℂ) →
(-(ℜ‘𝑆) ·
(log‘(𝑘 + 1))) =
-((ℜ‘𝑆) ·
(log‘(𝑘 +
1)))) |
| 137 | 64, 135, 136 | syl2an 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (-(ℜ‘𝑆) · (log‘(𝑘 + 1))) = -((ℜ‘𝑆) · (log‘(𝑘 + 1)))) |
| 138 | | mulneg1 11699 |
. . . . . . . 8
⊢
(((ℜ‘𝑆)
∈ ℂ ∧ (log‘𝑘) ∈ ℂ) →
(-(ℜ‘𝑆) ·
(log‘𝑘)) =
-((ℜ‘𝑆) ·
(log‘𝑘))) |
| 139 | 64, 21, 138 | syl2an 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (-(ℜ‘𝑆) · (log‘𝑘)) = -((ℜ‘𝑆) · (log‘𝑘))) |
| 140 | 134, 137,
139 | 3brtr4d 5175 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (-(ℜ‘𝑆) · (log‘(𝑘 + 1))) ≤
(-(ℜ‘𝑆) ·
(log‘𝑘))) |
| 141 | | remulcl 11240 |
. . . . . . . 8
⊢
((-(ℜ‘𝑆)
∈ ℝ ∧ (log‘(𝑘 + 1)) ∈ ℝ) →
(-(ℜ‘𝑆) ·
(log‘(𝑘 + 1))) ∈
ℝ) |
| 142 | 40, 110, 141 | syl2an 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (-(ℜ‘𝑆) · (log‘(𝑘 + 1))) ∈
ℝ) |
| 143 | | remulcl 11240 |
. . . . . . . 8
⊢
((-(ℜ‘𝑆)
∈ ℝ ∧ (log‘𝑘) ∈ ℝ) →
(-(ℜ‘𝑆) ·
(log‘𝑘)) ∈
ℝ) |
| 144 | 40, 20, 143 | syl2an 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (-(ℜ‘𝑆) · (log‘𝑘)) ∈
ℝ) |
| 145 | | efle 16154 |
. . . . . . 7
⊢
(((-(ℜ‘𝑆)
· (log‘(𝑘 +
1))) ∈ ℝ ∧ (-(ℜ‘𝑆) · (log‘𝑘)) ∈ ℝ) →
((-(ℜ‘𝑆)
· (log‘(𝑘 +
1))) ≤ (-(ℜ‘𝑆) · (log‘𝑘)) ↔ (exp‘(-(ℜ‘𝑆) · (log‘(𝑘 + 1)))) ≤
(exp‘(-(ℜ‘𝑆) · (log‘𝑘))))) |
| 146 | 142, 144,
145 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
((-(ℜ‘𝑆)
· (log‘(𝑘 +
1))) ≤ (-(ℜ‘𝑆) · (log‘𝑘)) ↔ (exp‘(-(ℜ‘𝑆) · (log‘(𝑘 + 1)))) ≤
(exp‘(-(ℜ‘𝑆) · (log‘𝑘))))) |
| 147 | 140, 146 | mpbid 232 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
(exp‘(-(ℜ‘𝑆) · (log‘(𝑘 + 1)))) ≤
(exp‘(-(ℜ‘𝑆) · (log‘𝑘)))) |
| 148 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑛 = (𝑘 + 1) → (𝑛↑𝑐-(ℜ‘𝑆)) = ((𝑘 +
1)↑𝑐-(ℜ‘𝑆))) |
| 149 | | ovex 7464 |
. . . . . . . 8
⊢ ((𝑘 +
1)↑𝑐-(ℜ‘𝑆)) ∈ V |
| 150 | 148, 4, 149 | fvmpt 7016 |
. . . . . . 7
⊢ ((𝑘 + 1) ∈ ℕ →
((𝑛 ∈ ℕ ↦
(𝑛↑𝑐-(ℜ‘𝑆)))‘(𝑘 + 1)) = ((𝑘 +
1)↑𝑐-(ℜ‘𝑆))) |
| 151 | 116, 150 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑛↑𝑐-(ℜ‘𝑆)))‘(𝑘 + 1)) = ((𝑘 +
1)↑𝑐-(ℜ‘𝑆))) |
| 152 | 116 | nncnd 12282 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℂ) |
| 153 | 116 | nnne0d 12316 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ≠ 0) |
| 154 | 152, 153,
47 | cxpefd 26754 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑘 +
1)↑𝑐-(ℜ‘𝑆)) = (exp‘(-(ℜ‘𝑆) · (log‘(𝑘 + 1))))) |
| 155 | 151, 154 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑛↑𝑐-(ℜ‘𝑆)))‘(𝑘 + 1)) = (exp‘(-(ℜ‘𝑆) · (log‘(𝑘 + 1))))) |
| 156 | 7, 48 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑛↑𝑐-(ℜ‘𝑆)))‘𝑘) = (exp‘(-(ℜ‘𝑆) · (log‘𝑘)))) |
| 157 | 147, 155,
156 | 3brtr4d 5175 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑛↑𝑐-(ℜ‘𝑆)))‘(𝑘 + 1)) ≤ ((𝑛 ∈ ℕ ↦ (𝑛↑𝑐-(ℜ‘𝑆)))‘𝑘)) |
| 158 | 57 | recnd 11289 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 −
(ℜ‘𝑆)) ∈
ℂ) |
| 159 | 158 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (1
− (ℜ‘𝑆))
∈ ℂ) |
| 160 | | nn0re 12535 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℝ) |
| 161 | 160 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
ℝ) |
| 162 | 161 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
ℂ) |
| 163 | 159, 162 | mulcomd 11282 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((1
− (ℜ‘𝑆))
· 𝑚) = (𝑚 · (1 −
(ℜ‘𝑆)))) |
| 164 | 163 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
(2↑𝑐((1 − (ℜ‘𝑆)) · 𝑚)) = (2↑𝑐(𝑚 · (1 −
(ℜ‘𝑆))))) |
| 165 | 54 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 2 ∈
ℝ+) |
| 166 | 165, 161,
159 | cxpmuld 26779 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
(2↑𝑐(𝑚 · (1 − (ℜ‘𝑆)))) =
((2↑𝑐𝑚)↑𝑐(1 −
(ℜ‘𝑆)))) |
| 167 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
ℕ0) |
| 168 | | cxpexp 26710 |
. . . . . . . . . 10
⊢ ((2
∈ ℂ ∧ 𝑚
∈ ℕ0) → (2↑𝑐𝑚) = (2↑𝑚)) |
| 169 | 81, 167, 168 | sylancr 587 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
(2↑𝑐𝑚) = (2↑𝑚)) |
| 170 | | ax-1cn 11213 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
| 171 | 64 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
(ℜ‘𝑆) ∈
ℂ) |
| 172 | | negsub 11557 |
. . . . . . . . . . 11
⊢ ((1
∈ ℂ ∧ (ℜ‘𝑆) ∈ ℂ) → (1 +
-(ℜ‘𝑆)) = (1
− (ℜ‘𝑆))) |
| 173 | 170, 171,
172 | sylancr 587 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (1 +
-(ℜ‘𝑆)) = (1
− (ℜ‘𝑆))) |
| 174 | 173 | eqcomd 2743 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (1
− (ℜ‘𝑆)) =
(1 + -(ℜ‘𝑆))) |
| 175 | 169, 174 | oveq12d 7449 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
((2↑𝑐𝑚)↑𝑐(1 −
(ℜ‘𝑆))) =
((2↑𝑚)↑𝑐(1 +
-(ℜ‘𝑆)))) |
| 176 | 164, 166,
175 | 3eqtrd 2781 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
(2↑𝑐((1 − (ℜ‘𝑆)) · 𝑚)) = ((2↑𝑚)↑𝑐(1 +
-(ℜ‘𝑆)))) |
| 177 | 57 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (1
− (ℜ‘𝑆))
∈ ℝ) |
| 178 | 165, 177,
162 | cxpmuld 26779 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
(2↑𝑐((1 − (ℜ‘𝑆)) · 𝑚)) = ((2↑𝑐(1 −
(ℜ‘𝑆)))↑𝑐𝑚)) |
| 179 | | 2nn 12339 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ |
| 180 | | nnexpcl 14115 |
. . . . . . . . . . 11
⊢ ((2
∈ ℕ ∧ 𝑚
∈ ℕ0) → (2↑𝑚) ∈ ℕ) |
| 181 | 179, 180 | mpan 690 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ0
→ (2↑𝑚) ∈
ℕ) |
| 182 | 181 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
(2↑𝑚) ∈
ℕ) |
| 183 | 182 | nncnd 12282 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
(2↑𝑚) ∈
ℂ) |
| 184 | 182 | nnne0d 12316 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
(2↑𝑚) ≠
0) |
| 185 | | 1cnd 11256 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 1 ∈
ℂ) |
| 186 | 41 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
-(ℜ‘𝑆) ∈
ℂ) |
| 187 | 183, 184,
185, 186 | cxpaddd 26759 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
((2↑𝑚)↑𝑐(1 +
-(ℜ‘𝑆))) =
(((2↑𝑚)↑𝑐1) ·
((2↑𝑚)↑𝑐-(ℜ‘𝑆)))) |
| 188 | 176, 178,
187 | 3eqtr3d 2785 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
((2↑𝑐(1 − (ℜ‘𝑆)))↑𝑐𝑚) = (((2↑𝑚)↑𝑐1) ·
((2↑𝑚)↑𝑐-(ℜ‘𝑆)))) |
| 189 | | cxpexp 26710 |
. . . . . . 7
⊢
(((2↑𝑐(1 − (ℜ‘𝑆))) ∈ ℂ ∧ 𝑚 ∈ ℕ0) →
((2↑𝑐(1 − (ℜ‘𝑆)))↑𝑐𝑚) =
((2↑𝑐(1 − (ℜ‘𝑆)))↑𝑚)) |
| 190 | 60, 189 | sylan 580 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
((2↑𝑐(1 − (ℜ‘𝑆)))↑𝑐𝑚) =
((2↑𝑐(1 − (ℜ‘𝑆)))↑𝑚)) |
| 191 | 183 | cxp1d 26748 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
((2↑𝑚)↑𝑐1) = (2↑𝑚)) |
| 192 | 191 | oveq1d 7446 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
(((2↑𝑚)↑𝑐1) ·
((2↑𝑚)↑𝑐-(ℜ‘𝑆))) = ((2↑𝑚) · ((2↑𝑚)↑𝑐-(ℜ‘𝑆)))) |
| 193 | 188, 190,
192 | 3eqtr3d 2785 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
((2↑𝑐(1 − (ℜ‘𝑆)))↑𝑚) = ((2↑𝑚) · ((2↑𝑚)↑𝑐-(ℜ‘𝑆)))) |
| 194 | 179, 167,
180 | sylancr 587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
(2↑𝑚) ∈
ℕ) |
| 195 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑛 = (2↑𝑚) → (𝑛↑𝑐-(ℜ‘𝑆)) = ((2↑𝑚)↑𝑐-(ℜ‘𝑆))) |
| 196 | | ovex 7464 |
. . . . . . . 8
⊢
((2↑𝑚)↑𝑐-(ℜ‘𝑆)) ∈ V |
| 197 | 195, 4, 196 | fvmpt 7016 |
. . . . . . 7
⊢
((2↑𝑚) ∈
ℕ → ((𝑛 ∈
ℕ ↦ (𝑛↑𝑐-(ℜ‘𝑆)))‘(2↑𝑚)) = ((2↑𝑚)↑𝑐-(ℜ‘𝑆))) |
| 198 | 194, 197 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((𝑛 ∈ ℕ ↦ (𝑛↑𝑐-(ℜ‘𝑆)))‘(2↑𝑚)) = ((2↑𝑚)↑𝑐-(ℜ‘𝑆))) |
| 199 | 198 | oveq2d 7447 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
((2↑𝑚) ·
((𝑛 ∈ ℕ ↦
(𝑛↑𝑐-(ℜ‘𝑆)))‘(2↑𝑚))) = ((2↑𝑚) · ((2↑𝑚)↑𝑐-(ℜ‘𝑆)))) |
| 200 | 193, 91, 199 | 3eqtr4d 2787 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ ((2↑𝑐(1 − (ℜ‘𝑆)))↑𝑛))‘𝑚) = ((2↑𝑚) · ((𝑛 ∈ ℕ ↦ (𝑛↑𝑐-(ℜ‘𝑆)))‘(2↑𝑚)))) |
| 201 | 100, 102,
157, 200 | climcnds 15887 |
. . 3
⊢ (𝜑 → (seq1( + , (𝑛 ∈ ℕ ↦ (𝑛↑𝑐-(ℜ‘𝑆)))) ∈ dom ⇝ ↔
seq0( + , (𝑛 ∈
ℕ0 ↦ ((2↑𝑐(1 −
(ℜ‘𝑆)))↑𝑛))) ∈ dom ⇝ )) |
| 202 | 96, 201 | mpbird 257 |
. 2
⊢ (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦ (𝑛↑𝑐-(ℜ‘𝑆)))) ∈ dom ⇝
) |
| 203 | 1, 2, 51, 53, 202 | abscvgcvg 15855 |
1
⊢ (𝜑 → seq1( + , 𝐹) ∈ dom ⇝
) |