| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nn0uz 12921 | . . . 4
⊢
ℕ0 = (ℤ≥‘0) | 
| 2 |  | 0zd 12627 | . . . 4
⊢ (𝐻 ∈ dom ⇝ → 0
∈ ℤ) | 
| 3 |  | 1ex 11258 | . . . . . 6
⊢ 1 ∈
V | 
| 4 | 3 | fvconst2 7225 | . . . . 5
⊢ (𝑘 ∈ ℕ0
→ ((ℕ0 × {1})‘𝑘) = 1) | 
| 5 | 4 | adantl 481 | . . . 4
⊢ ((𝐻 ∈ dom ⇝ ∧ 𝑘 ∈ ℕ0)
→ ((ℕ0 × {1})‘𝑘) = 1) | 
| 6 |  | 1red 11263 | . . . 4
⊢ ((𝐻 ∈ dom ⇝ ∧ 𝑘 ∈ ℕ0)
→ 1 ∈ ℝ) | 
| 7 |  | harmonic.2 | . . . . . . 7
⊢ 𝐻 = seq1( + , 𝐹) | 
| 8 | 7 | eleq1i 2831 | . . . . . 6
⊢ (𝐻 ∈ dom ⇝ ↔ seq1(
+ , 𝐹) ∈ dom ⇝
) | 
| 9 | 8 | biimpi 216 | . . . . 5
⊢ (𝐻 ∈ dom ⇝ → seq1(
+ , 𝐹) ∈ dom ⇝
) | 
| 10 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑛 = 𝑘 → (1 / 𝑛) = (1 / 𝑘)) | 
| 11 |  | harmonic.1 | . . . . . . . . 9
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (1 / 𝑛)) | 
| 12 |  | ovex 7465 | . . . . . . . . 9
⊢ (1 /
𝑘) ∈
V | 
| 13 | 10, 11, 12 | fvmpt 7015 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) = (1 / 𝑘)) | 
| 14 |  | nnrecre 12309 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ) | 
| 15 | 13, 14 | eqeltrd 2840 | . . . . . . 7
⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) ∈ ℝ) | 
| 16 | 15 | adantl 481 | . . . . . 6
⊢ ((𝐻 ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℝ) | 
| 17 |  | nnrp 13047 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ+) | 
| 18 | 17 | rpreccld 13088 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ+) | 
| 19 | 18 | rpge0d 13082 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ → 0 ≤ (1
/ 𝑘)) | 
| 20 | 19, 13 | breqtrrd 5170 | . . . . . . 7
⊢ (𝑘 ∈ ℕ → 0 ≤
(𝐹‘𝑘)) | 
| 21 | 20 | adantl 481 | . . . . . 6
⊢ ((𝐻 ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 0 ≤
(𝐹‘𝑘)) | 
| 22 |  | nnre 12274 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ) | 
| 23 | 22 | lep1d 12200 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ → 𝑘 ≤ (𝑘 + 1)) | 
| 24 |  | nngt0 12298 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 0 <
𝑘) | 
| 25 |  | peano2re 11435 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈
ℝ) | 
| 26 | 22, 25 | syl 17 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℝ) | 
| 27 |  | peano2nn 12279 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℕ) | 
| 28 | 27 | nngt0d 12316 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 0 <
(𝑘 + 1)) | 
| 29 |  | lerec 12152 | . . . . . . . . . 10
⊢ (((𝑘 ∈ ℝ ∧ 0 <
𝑘) ∧ ((𝑘 + 1) ∈ ℝ ∧ 0
< (𝑘 + 1))) →
(𝑘 ≤ (𝑘 + 1) ↔ (1 / (𝑘 + 1)) ≤ (1 / 𝑘))) | 
| 30 | 22, 24, 26, 28, 29 | syl22anc 838 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (𝑘 ≤ (𝑘 + 1) ↔ (1 / (𝑘 + 1)) ≤ (1 / 𝑘))) | 
| 31 | 23, 30 | mpbid 232 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ → (1 /
(𝑘 + 1)) ≤ (1 / 𝑘)) | 
| 32 |  | oveq2 7440 | . . . . . . . . . 10
⊢ (𝑛 = (𝑘 + 1) → (1 / 𝑛) = (1 / (𝑘 + 1))) | 
| 33 |  | ovex 7465 | . . . . . . . . . 10
⊢ (1 /
(𝑘 + 1)) ∈
V | 
| 34 | 32, 11, 33 | fvmpt 7015 | . . . . . . . . 9
⊢ ((𝑘 + 1) ∈ ℕ →
(𝐹‘(𝑘 + 1)) = (1 / (𝑘 + 1))) | 
| 35 | 27, 34 | syl 17 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ → (𝐹‘(𝑘 + 1)) = (1 / (𝑘 + 1))) | 
| 36 | 31, 35, 13 | 3brtr4d 5174 | . . . . . . 7
⊢ (𝑘 ∈ ℕ → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) | 
| 37 | 36 | adantl 481 | . . . . . 6
⊢ ((𝐻 ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ≤ (𝐹‘𝑘)) | 
| 38 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑘 = 𝑗 → (2↑𝑘) = (2↑𝑗)) | 
| 39 | 38 | fveq2d 6909 | . . . . . . . . 9
⊢ (𝑘 = 𝑗 → (𝐹‘(2↑𝑘)) = (𝐹‘(2↑𝑗))) | 
| 40 | 38, 39 | oveq12d 7450 | . . . . . . . 8
⊢ (𝑘 = 𝑗 → ((2↑𝑘) · (𝐹‘(2↑𝑘))) = ((2↑𝑗) · (𝐹‘(2↑𝑗)))) | 
| 41 |  | fconstmpt 5746 | . . . . . . . . 9
⊢
(ℕ0 × {1}) = (𝑘 ∈ ℕ0 ↦
1) | 
| 42 |  | 2nn 12340 | . . . . . . . . . . . . . 14
⊢ 2 ∈
ℕ | 
| 43 |  | nnexpcl 14116 | . . . . . . . . . . . . . 14
⊢ ((2
∈ ℕ ∧ 𝑘
∈ ℕ0) → (2↑𝑘) ∈ ℕ) | 
| 44 | 42, 43 | mpan 690 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
→ (2↑𝑘) ∈
ℕ) | 
| 45 |  | oveq2 7440 | . . . . . . . . . . . . . 14
⊢ (𝑛 = (2↑𝑘) → (1 / 𝑛) = (1 / (2↑𝑘))) | 
| 46 |  | ovex 7465 | . . . . . . . . . . . . . 14
⊢ (1 /
(2↑𝑘)) ∈
V | 
| 47 | 45, 11, 46 | fvmpt 7015 | . . . . . . . . . . . . 13
⊢
((2↑𝑘) ∈
ℕ → (𝐹‘(2↑𝑘)) = (1 / (2↑𝑘))) | 
| 48 | 44, 47 | syl 17 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ (𝐹‘(2↑𝑘)) = (1 / (2↑𝑘))) | 
| 49 | 48 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ ((2↑𝑘) ·
(𝐹‘(2↑𝑘))) = ((2↑𝑘) · (1 / (2↑𝑘)))) | 
| 50 |  | nncn 12275 | . . . . . . . . . . . . 13
⊢
((2↑𝑘) ∈
ℕ → (2↑𝑘)
∈ ℂ) | 
| 51 |  | nnne0 12301 | . . . . . . . . . . . . 13
⊢
((2↑𝑘) ∈
ℕ → (2↑𝑘)
≠ 0) | 
| 52 | 50, 51 | recidd 12039 | . . . . . . . . . . . 12
⊢
((2↑𝑘) ∈
ℕ → ((2↑𝑘)
· (1 / (2↑𝑘)))
= 1) | 
| 53 | 44, 52 | syl 17 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ ((2↑𝑘) ·
(1 / (2↑𝑘))) =
1) | 
| 54 | 49, 53 | eqtrd 2776 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ ((2↑𝑘) ·
(𝐹‘(2↑𝑘))) = 1) | 
| 55 | 54 | mpteq2ia 5244 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
↦ ((2↑𝑘)
· (𝐹‘(2↑𝑘)))) = (𝑘 ∈ ℕ0 ↦
1) | 
| 56 | 41, 55 | eqtr4i 2767 | . . . . . . . 8
⊢
(ℕ0 × {1}) = (𝑘 ∈ ℕ0 ↦
((2↑𝑘) · (𝐹‘(2↑𝑘)))) | 
| 57 |  | ovex 7465 | . . . . . . . 8
⊢
((2↑𝑗) ·
(𝐹‘(2↑𝑗))) ∈ V | 
| 58 | 40, 56, 57 | fvmpt 7015 | . . . . . . 7
⊢ (𝑗 ∈ ℕ0
→ ((ℕ0 × {1})‘𝑗) = ((2↑𝑗) · (𝐹‘(2↑𝑗)))) | 
| 59 | 58 | adantl 481 | . . . . . 6
⊢ ((𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ0)
→ ((ℕ0 × {1})‘𝑗) = ((2↑𝑗) · (𝐹‘(2↑𝑗)))) | 
| 60 | 16, 21, 37, 59 | climcnds 15888 | . . . . 5
⊢ (𝐻 ∈ dom ⇝ →
(seq1( + , 𝐹) ∈ dom
⇝ ↔ seq0( + , (ℕ0 × {1})) ∈ dom ⇝
)) | 
| 61 | 9, 60 | mpbid 232 | . . . 4
⊢ (𝐻 ∈ dom ⇝ → seq0(
+ , (ℕ0 × {1})) ∈ dom ⇝ ) | 
| 62 | 1, 2, 5, 6, 61 | isumrecl 15802 | . . 3
⊢ (𝐻 ∈ dom ⇝ →
Σ𝑘 ∈
ℕ0 1 ∈ ℝ) | 
| 63 |  | arch 12525 | . . 3
⊢
(Σ𝑘 ∈
ℕ0 1 ∈ ℝ → ∃𝑗 ∈ ℕ Σ𝑘 ∈ ℕ0 1 < 𝑗) | 
| 64 | 62, 63 | syl 17 | . 2
⊢ (𝐻 ∈ dom ⇝ →
∃𝑗 ∈ ℕ
Σ𝑘 ∈
ℕ0 1 < 𝑗) | 
| 65 |  | fzfid 14015 | . . . . . . 7
⊢ ((𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) →
(1...𝑗) ∈
Fin) | 
| 66 |  | ax-1cn 11214 | . . . . . . 7
⊢ 1 ∈
ℂ | 
| 67 |  | fsumconst 15827 | . . . . . . 7
⊢
(((1...𝑗) ∈ Fin
∧ 1 ∈ ℂ) → Σ𝑘 ∈ (1...𝑗)1 = ((♯‘(1...𝑗)) · 1)) | 
| 68 | 65, 66, 67 | sylancl 586 | . . . . . 6
⊢ ((𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) →
Σ𝑘 ∈ (1...𝑗)1 = ((♯‘(1...𝑗)) · 1)) | 
| 69 |  | nnnn0 12535 | . . . . . . . . 9
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℕ0) | 
| 70 | 69 | adantl 481 | . . . . . . . 8
⊢ ((𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℕ0) | 
| 71 |  | hashfz1 14386 | . . . . . . . 8
⊢ (𝑗 ∈ ℕ0
→ (♯‘(1...𝑗)) = 𝑗) | 
| 72 | 70, 71 | syl 17 | . . . . . . 7
⊢ ((𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) →
(♯‘(1...𝑗)) =
𝑗) | 
| 73 | 72 | oveq1d 7447 | . . . . . 6
⊢ ((𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) →
((♯‘(1...𝑗))
· 1) = (𝑗 ·
1)) | 
| 74 |  | nncn 12275 | . . . . . . . 8
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℂ) | 
| 75 | 74 | adantl 481 | . . . . . . 7
⊢ ((𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℂ) | 
| 76 | 75 | mulridd 11279 | . . . . . 6
⊢ ((𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → (𝑗 · 1) = 𝑗) | 
| 77 | 68, 73, 76 | 3eqtrd 2780 | . . . . 5
⊢ ((𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) →
Σ𝑘 ∈ (1...𝑗)1 = 𝑗) | 
| 78 |  | 0zd 12627 | . . . . . 6
⊢ ((𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → 0 ∈
ℤ) | 
| 79 |  | elfznn 13594 | . . . . . . . . 9
⊢ (𝑘 ∈ (1...𝑗) → 𝑘 ∈ ℕ) | 
| 80 |  | nnnn0 12535 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) | 
| 81 | 79, 80 | syl 17 | . . . . . . . 8
⊢ (𝑘 ∈ (1...𝑗) → 𝑘 ∈ ℕ0) | 
| 82 | 81 | ssriv 3986 | . . . . . . 7
⊢
(1...𝑗) ⊆
ℕ0 | 
| 83 | 82 | a1i 11 | . . . . . 6
⊢ ((𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) →
(1...𝑗) ⊆
ℕ0) | 
| 84 | 4 | adantl 481 | . . . . . 6
⊢ (((𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ℕ0)
→ ((ℕ0 × {1})‘𝑘) = 1) | 
| 85 |  | 1red 11263 | . . . . . 6
⊢ (((𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ℕ0)
→ 1 ∈ ℝ) | 
| 86 |  | 0le1 11787 | . . . . . . 7
⊢ 0 ≤
1 | 
| 87 | 86 | a1i 11 | . . . . . 6
⊢ (((𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ ℕ0)
→ 0 ≤ 1) | 
| 88 | 61 | adantr 480 | . . . . . 6
⊢ ((𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → seq0( +
, (ℕ0 × {1})) ∈ dom ⇝ ) | 
| 89 | 1, 78, 65, 83, 84, 85, 87, 88 | isumless 15882 | . . . . 5
⊢ ((𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) →
Σ𝑘 ∈ (1...𝑗)1 ≤ Σ𝑘 ∈ ℕ0
1) | 
| 90 | 77, 89 | eqbrtrrd 5166 | . . . 4
⊢ ((𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → 𝑗 ≤ Σ𝑘 ∈ ℕ0
1) | 
| 91 |  | nnre 12274 | . . . . 5
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℝ) | 
| 92 |  | lenlt 11340 | . . . . 5
⊢ ((𝑗 ∈ ℝ ∧
Σ𝑘 ∈
ℕ0 1 ∈ ℝ) → (𝑗 ≤ Σ𝑘 ∈ ℕ0 1 ↔ ¬
Σ𝑘 ∈
ℕ0 1 < 𝑗)) | 
| 93 | 91, 62, 92 | syl2anr 597 | . . . 4
⊢ ((𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → (𝑗 ≤ Σ𝑘 ∈ ℕ0 1 ↔ ¬
Σ𝑘 ∈
ℕ0 1 < 𝑗)) | 
| 94 | 90, 93 | mpbid 232 | . . 3
⊢ ((𝐻 ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → ¬
Σ𝑘 ∈
ℕ0 1 < 𝑗) | 
| 95 | 94 | nrexdv 3148 | . 2
⊢ (𝐻 ∈ dom ⇝ → ¬
∃𝑗 ∈ ℕ
Σ𝑘 ∈
ℕ0 1 < 𝑗) | 
| 96 | 64, 95 | pm2.65i 194 | 1
⊢  ¬
𝐻 ∈ dom
⇝ |