| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nnuz 12922 | . . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) | 
| 2 |  | 1zzd 12650 | . . . . . . . . 9
⊢ (⊤
→ 1 ∈ ℤ) | 
| 3 |  | nnrecre 12309 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (1 /
𝑛) ∈
ℝ) | 
| 4 | 3 | adantl 481 | . . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑛
∈ ℕ) → (1 / 𝑛) ∈ ℝ) | 
| 5 |  | 0re 11264 | . . . . . . . . . . . 12
⊢ 0 ∈
ℝ | 
| 6 |  | ifcl 4570 | . . . . . . . . . . . 12
⊢ (((1 /
𝑛) ∈ ℝ ∧ 0
∈ ℝ) → if(𝑛
∈ ℙ, (1 / 𝑛), 0)
∈ ℝ) | 
| 7 | 4, 5, 6 | sylancl 586 | . . . . . . . . . . 11
⊢
((⊤ ∧ 𝑛
∈ ℕ) → if(𝑛
∈ ℙ, (1 / 𝑛), 0)
∈ ℝ) | 
| 8 |  | prmrec.1 | . . . . . . . . . . 11
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0)) | 
| 9 | 7, 8 | fmptd 7133 | . . . . . . . . . 10
⊢ (⊤
→ 𝐹:ℕ⟶ℝ) | 
| 10 | 9 | ffvelcdmda 7103 | . . . . . . . . 9
⊢
((⊤ ∧ 𝑗
∈ ℕ) → (𝐹‘𝑗) ∈ ℝ) | 
| 11 | 1, 2, 10 | serfre 14073 | . . . . . . . 8
⊢ (⊤
→ seq1( + , 𝐹):ℕ⟶ℝ) | 
| 12 | 11 | mptru 1546 | . . . . . . 7
⊢ seq1( + ,
𝐹):ℕ⟶ℝ | 
| 13 |  | frn 6742 | . . . . . . 7
⊢ (seq1( +
, 𝐹):ℕ⟶ℝ
→ ran seq1( + , 𝐹)
⊆ ℝ) | 
| 14 | 12, 13 | mp1i 13 | . . . . . 6
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ran seq1( + , 𝐹)
⊆ ℝ) | 
| 15 |  | 1nn 12278 | . . . . . . . 8
⊢ 1 ∈
ℕ | 
| 16 | 12 | fdmi 6746 | . . . . . . . 8
⊢ dom seq1(
+ , 𝐹) =
ℕ | 
| 17 | 15, 16 | eleqtrri 2839 | . . . . . . 7
⊢ 1 ∈
dom seq1( + , 𝐹) | 
| 18 |  | ne0i 4340 | . . . . . . . 8
⊢ (1 ∈
dom seq1( + , 𝐹) → dom
seq1( + , 𝐹) ≠
∅) | 
| 19 |  | dm0rn0 5934 | . . . . . . . . 9
⊢ (dom
seq1( + , 𝐹) = ∅
↔ ran seq1( + , 𝐹) =
∅) | 
| 20 | 19 | necon3bii 2992 | . . . . . . . 8
⊢ (dom
seq1( + , 𝐹) ≠ ∅
↔ ran seq1( + , 𝐹)
≠ ∅) | 
| 21 | 18, 20 | sylib 218 | . . . . . . 7
⊢ (1 ∈
dom seq1( + , 𝐹) → ran
seq1( + , 𝐹) ≠
∅) | 
| 22 | 17, 21 | mp1i 13 | . . . . . 6
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ran seq1( + , 𝐹)
≠ ∅) | 
| 23 |  | 1zzd 12650 | . . . . . . . . 9
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ 1 ∈ ℤ) | 
| 24 |  | climdm 15591 | . . . . . . . . . 10
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
↔ seq1( + , 𝐹) ⇝
( ⇝ ‘seq1( + , 𝐹))) | 
| 25 | 24 | biimpi 216 | . . . . . . . . 9
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ seq1( + , 𝐹) ⇝
( ⇝ ‘seq1( + , 𝐹))) | 
| 26 | 12 | a1i 11 | . . . . . . . . . 10
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ seq1( + , 𝐹):ℕ⟶ℝ) | 
| 27 | 26 | ffvelcdmda 7103 | . . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (seq1( + , 𝐹)‘𝑘) ∈ ℝ) | 
| 28 | 1, 23, 25, 27 | climrecl 15620 | . . . . . . . 8
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ( ⇝ ‘seq1( + , 𝐹)) ∈ ℝ) | 
| 29 |  | simpr 484 | . . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ 𝑘 ∈
ℕ) | 
| 30 | 25 | adantr 480 | . . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ seq1( + , 𝐹) ⇝
( ⇝ ‘seq1( + , 𝐹))) | 
| 31 |  | eleq1w 2823 | . . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑗 → (𝑛 ∈ ℙ ↔ 𝑗 ∈ ℙ)) | 
| 32 |  | oveq2 7440 | . . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑗 → (1 / 𝑛) = (1 / 𝑗)) | 
| 33 | 31, 32 | ifbieq1d 4549 | . . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑗 → if(𝑛 ∈ ℙ, (1 / 𝑛), 0) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) | 
| 34 |  | prmnn 16712 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℙ → 𝑗 ∈
ℕ) | 
| 35 | 34 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑗
∈ ℙ) → 𝑗
∈ ℕ) | 
| 36 | 35 | nnrecred 12318 | . . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑗
∈ ℙ) → (1 / 𝑗) ∈ ℝ) | 
| 37 | 5 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ ¬ 𝑗 ∈ ℙ) → 0 ∈
ℝ) | 
| 38 | 36, 37 | ifclda 4560 | . . . . . . . . . . . . . . . 16
⊢ (⊤
→ if(𝑗 ∈ ℙ,
(1 / 𝑗), 0) ∈
ℝ) | 
| 39 | 38 | mptru 1546 | . . . . . . . . . . . . . . 15
⊢ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈
ℝ | 
| 40 | 39 | elexi 3502 | . . . . . . . . . . . . . 14
⊢ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ V | 
| 41 | 33, 8, 40 | fvmpt 7015 | . . . . . . . . . . . . 13
⊢ (𝑗 ∈ ℕ → (𝐹‘𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) | 
| 42 | 41 | adantl 481 | . . . . . . . . . . . 12
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑗 ∈ ℕ)
→ (𝐹‘𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) | 
| 43 | 39 | a1i 11 | . . . . . . . . . . . 12
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑗 ∈ ℕ)
→ if(𝑗 ∈ ℙ,
(1 / 𝑗), 0) ∈
ℝ) | 
| 44 | 42, 43 | eqeltrd 2840 | . . . . . . . . . . 11
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑗 ∈ ℕ)
→ (𝐹‘𝑗) ∈
ℝ) | 
| 45 | 44 | adantlr 715 | . . . . . . . . . 10
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
→ (𝐹‘𝑗) ∈
ℝ) | 
| 46 |  | nnrp 13047 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℝ+) | 
| 47 | 46 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑗 ∈ ℕ)
→ 𝑗 ∈
ℝ+) | 
| 48 | 47 | rpreccld 13088 | . . . . . . . . . . . . . 14
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑗 ∈ ℕ)
→ (1 / 𝑗) ∈
ℝ+) | 
| 49 | 48 | rpge0d 13082 | . . . . . . . . . . . . 13
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑗 ∈ ℕ)
→ 0 ≤ (1 / 𝑗)) | 
| 50 |  | 0le0 12368 | . . . . . . . . . . . . 13
⊢ 0 ≤
0 | 
| 51 |  | breq2 5146 | . . . . . . . . . . . . . 14
⊢ ((1 /
𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0) → (0 ≤ (1 / 𝑗) ↔ 0 ≤ if(𝑗 ∈ ℙ, (1 / 𝑗), 0))) | 
| 52 |  | breq2 5146 | . . . . . . . . . . . . . 14
⊢ (0 =
if(𝑗 ∈ ℙ, (1 /
𝑗), 0) → (0 ≤ 0
↔ 0 ≤ if(𝑗 ∈
ℙ, (1 / 𝑗),
0))) | 
| 53 | 51, 52 | ifboth 4564 | . . . . . . . . . . . . 13
⊢ ((0 ≤
(1 / 𝑗) ∧ 0 ≤ 0)
→ 0 ≤ if(𝑗 ∈
ℙ, (1 / 𝑗),
0)) | 
| 54 | 49, 50, 53 | sylancl 586 | . . . . . . . . . . . 12
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑗 ∈ ℕ)
→ 0 ≤ if(𝑗 ∈
ℙ, (1 / 𝑗),
0)) | 
| 55 | 54, 42 | breqtrrd 5170 | . . . . . . . . . . 11
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑗 ∈ ℕ)
→ 0 ≤ (𝐹‘𝑗)) | 
| 56 | 55 | adantlr 715 | . . . . . . . . . 10
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
→ 0 ≤ (𝐹‘𝑗)) | 
| 57 | 1, 29, 30, 45, 56 | climserle 15700 | . . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹))) | 
| 58 | 57 | ralrimiva 3145 | . . . . . . . 8
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ∀𝑘 ∈
ℕ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹))) | 
| 59 |  | brralrspcev 5202 | . . . . . . . 8
⊢ (((
⇝ ‘seq1( + , 𝐹)) ∈ ℝ ∧ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹))) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥) | 
| 60 | 28, 58, 59 | syl2anc 584 | . . . . . . 7
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ∃𝑥 ∈
ℝ ∀𝑘 ∈
ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥) | 
| 61 |  | ffn 6735 | . . . . . . . . 9
⊢ (seq1( +
, 𝐹):ℕ⟶ℝ
→ seq1( + , 𝐹) Fn
ℕ) | 
| 62 |  | breq1 5145 | . . . . . . . . . 10
⊢ (𝑧 = (seq1( + , 𝐹)‘𝑘) → (𝑧 ≤ 𝑥 ↔ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)) | 
| 63 | 62 | ralrn 7107 | . . . . . . . . 9
⊢ (seq1( +
, 𝐹) Fn ℕ →
(∀𝑧 ∈ ran seq1(
+ , 𝐹)𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)) | 
| 64 | 12, 61, 63 | mp2b 10 | . . . . . . . 8
⊢
(∀𝑧 ∈
ran seq1( + , 𝐹)𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥) | 
| 65 | 64 | rexbii 3093 | . . . . . . 7
⊢
(∃𝑥 ∈
ℝ ∀𝑧 ∈
ran seq1( + , 𝐹)𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥) | 
| 66 | 60, 65 | sylibr 234 | . . . . . 6
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ∃𝑥 ∈
ℝ ∀𝑧 ∈
ran seq1( + , 𝐹)𝑧 ≤ 𝑥) | 
| 67 | 14, 22, 66 | suprcld 12232 | . . . . 5
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ sup(ran seq1( + , 𝐹), ℝ, < ) ∈
ℝ) | 
| 68 |  | 2rp 13040 | . . . . . 6
⊢ 2 ∈
ℝ+ | 
| 69 |  | rpreccl 13062 | . . . . . 6
⊢ (2 ∈
ℝ+ → (1 / 2) ∈ ℝ+) | 
| 70 | 68, 69 | ax-mp 5 | . . . . 5
⊢ (1 / 2)
∈ ℝ+ | 
| 71 |  | ltsubrp 13072 | . . . . 5
⊢ ((sup(ran
seq1( + , 𝐹), ℝ, <
) ∈ ℝ ∧ (1 / 2) ∈ ℝ+) → (sup(ran
seq1( + , 𝐹), ℝ, <
) − (1 / 2)) < sup(ran seq1( + , 𝐹), ℝ, < )) | 
| 72 | 67, 70, 71 | sylancl 586 | . . . 4
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) <
sup(ran seq1( + , 𝐹),
ℝ, < )) | 
| 73 |  | halfre 12481 | . . . . . 6
⊢ (1 / 2)
∈ ℝ | 
| 74 |  | resubcl 11574 | . . . . . 6
⊢ ((sup(ran
seq1( + , 𝐹), ℝ, <
) ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 /
2)) ∈ ℝ) | 
| 75 | 67, 73, 74 | sylancl 586 | . . . . 5
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) ∈
ℝ) | 
| 76 |  | suprlub 12233 | . . . . 5
⊢ (((ran
seq1( + , 𝐹) ⊆
ℝ ∧ ran seq1( + , 𝐹) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran seq1( + , 𝐹)𝑧 ≤ 𝑥) ∧ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) ∈
ℝ) → ((sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) <
sup(ran seq1( + , 𝐹),
ℝ, < ) ↔ ∃𝑦 ∈ ran seq1( + , 𝐹)(sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) <
𝑦)) | 
| 77 | 14, 22, 66, 75, 76 | syl31anc 1374 | . . . 4
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ((sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) <
sup(ran seq1( + , 𝐹),
ℝ, < ) ↔ ∃𝑦 ∈ ran seq1( + , 𝐹)(sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) <
𝑦)) | 
| 78 | 72, 77 | mpbid 232 | . . 3
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ∃𝑦 ∈ ran
seq1( + , 𝐹)(sup(ran seq1(
+ , 𝐹), ℝ, < )
− (1 / 2)) < 𝑦) | 
| 79 |  | breq2 5146 | . . . . 5
⊢ (𝑦 = (seq1( + , 𝐹)‘𝑘) → ((sup(ran seq1( + , 𝐹), ℝ, < ) − (1 /
2)) < 𝑦 ↔ (sup(ran
seq1( + , 𝐹), ℝ, <
) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘))) | 
| 80 | 79 | rexrn 7106 | . . . 4
⊢ (seq1( +
, 𝐹) Fn ℕ →
(∃𝑦 ∈ ran seq1(
+ , 𝐹)(sup(ran seq1( + ,
𝐹), ℝ, < ) −
(1 / 2)) < 𝑦 ↔
∃𝑘 ∈ ℕ
(sup(ran seq1( + , 𝐹),
ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘))) | 
| 81 | 12, 61, 80 | mp2b 10 | . . 3
⊢
(∃𝑦 ∈ ran
seq1( + , 𝐹)(sup(ran seq1(
+ , 𝐹), ℝ, < )
− (1 / 2)) < 𝑦
↔ ∃𝑘 ∈
ℕ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) <
(seq1( + , 𝐹)‘𝑘)) | 
| 82 | 78, 81 | sylib 218 | . 2
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ∃𝑘 ∈
ℕ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) <
(seq1( + , 𝐹)‘𝑘)) | 
| 83 |  | 2re 12341 | . . . . . 6
⊢ 2 ∈
ℝ | 
| 84 |  | 2nn 12340 | . . . . . . . . 9
⊢ 2 ∈
ℕ | 
| 85 |  | nnmulcl 12291 | . . . . . . . . 9
⊢ ((2
∈ ℕ ∧ 𝑘
∈ ℕ) → (2 · 𝑘) ∈ ℕ) | 
| 86 | 84, 29, 85 | sylancr 587 | . . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2 · 𝑘)
∈ ℕ) | 
| 87 | 86 | peano2nnd 12284 | . . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2 · 𝑘) + 1)
∈ ℕ) | 
| 88 | 87 | nnnn0d 12589 | . . . . . 6
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2 · 𝑘) + 1)
∈ ℕ0) | 
| 89 |  | reexpcl 14120 | . . . . . 6
⊢ ((2
∈ ℝ ∧ ((2 · 𝑘) + 1) ∈ ℕ0) →
(2↑((2 · 𝑘) +
1)) ∈ ℝ) | 
| 90 | 83, 88, 89 | sylancr 587 | . . . . 5
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑((2 · 𝑘) + 1)) ∈ ℝ) | 
| 91 | 90 | ltnrd 11396 | . . . 4
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ¬ (2↑((2 · 𝑘) + 1)) < (2↑((2 · 𝑘) + 1))) | 
| 92 | 29 | adantr 480 | . . . . . . 7
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → 𝑘 ∈ ℕ) | 
| 93 |  | peano2nn 12279 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℕ) | 
| 94 | 93 | adantl 481 | . . . . . . . . . . 11
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (𝑘 + 1) ∈
ℕ) | 
| 95 | 94 | nnnn0d 12589 | . . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (𝑘 + 1) ∈
ℕ0) | 
| 96 |  | nnexpcl 14116 | . . . . . . . . . 10
⊢ ((2
∈ ℕ ∧ (𝑘 +
1) ∈ ℕ0) → (2↑(𝑘 + 1)) ∈ ℕ) | 
| 97 | 84, 95, 96 | sylancr 587 | . . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑(𝑘 + 1))
∈ ℕ) | 
| 98 | 97 | nnsqcld 14284 | . . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2↑(𝑘 +
1))↑2) ∈ ℕ) | 
| 99 | 98 | adantr 480 | . . . . . . 7
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → ((2↑(𝑘 + 1))↑2) ∈
ℕ) | 
| 100 |  | breq1 5145 | . . . . . . . . . . 11
⊢ (𝑝 = 𝑤 → (𝑝 ∥ 𝑟 ↔ 𝑤 ∥ 𝑟)) | 
| 101 | 100 | notbid 318 | . . . . . . . . . 10
⊢ (𝑝 = 𝑤 → (¬ 𝑝 ∥ 𝑟 ↔ ¬ 𝑤 ∥ 𝑟)) | 
| 102 | 101 | cbvralvw 3236 | . . . . . . . . 9
⊢
(∀𝑝 ∈
(ℙ ∖ (1...𝑘))
¬ 𝑝 ∥ 𝑟 ↔ ∀𝑤 ∈ (ℙ ∖
(1...𝑘)) ¬ 𝑤 ∥ 𝑟) | 
| 103 |  | breq2 5146 | . . . . . . . . . . 11
⊢ (𝑟 = 𝑛 → (𝑤 ∥ 𝑟 ↔ 𝑤 ∥ 𝑛)) | 
| 104 | 103 | notbid 318 | . . . . . . . . . 10
⊢ (𝑟 = 𝑛 → (¬ 𝑤 ∥ 𝑟 ↔ ¬ 𝑤 ∥ 𝑛)) | 
| 105 | 104 | ralbidv 3177 | . . . . . . . . 9
⊢ (𝑟 = 𝑛 → (∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑟 ↔ ∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑛)) | 
| 106 | 102, 105 | bitrid 283 | . . . . . . . 8
⊢ (𝑟 = 𝑛 → (∀𝑝 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑝 ∥ 𝑟 ↔ ∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑛)) | 
| 107 | 106 | cbvrabv 3446 | . . . . . . 7
⊢ {𝑟 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣
∀𝑝 ∈ (ℙ
∖ (1...𝑘)) ¬
𝑝 ∥ 𝑟} = {𝑛 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣ ∀𝑤 ∈ (ℙ ∖
(1...𝑘)) ¬ 𝑤 ∥ 𝑛} | 
| 108 |  | simpll 766 | . . . . . . 7
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → seq1( + , 𝐹) ∈ dom ⇝
) | 
| 109 |  | eleq1w 2823 | . . . . . . . . . 10
⊢ (𝑚 = 𝑗 → (𝑚 ∈ ℙ ↔ 𝑗 ∈ ℙ)) | 
| 110 |  | oveq2 7440 | . . . . . . . . . 10
⊢ (𝑚 = 𝑗 → (1 / 𝑚) = (1 / 𝑗)) | 
| 111 | 109, 110 | ifbieq1d 4549 | . . . . . . . . 9
⊢ (𝑚 = 𝑗 → if(𝑚 ∈ ℙ, (1 / 𝑚), 0) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) | 
| 112 | 111 | cbvsumv 15733 | . . . . . . . 8
⊢
Σ𝑚 ∈
(ℤ≥‘(𝑘 + 1))if(𝑚 ∈ ℙ, (1 / 𝑚), 0) = Σ𝑗 ∈ (ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) | 
| 113 |  | simpr 484 | . . . . . . . 8
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) | 
| 114 | 112, 113 | eqbrtrid 5177 | . . . . . . 7
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → Σ𝑚 ∈
(ℤ≥‘(𝑘 + 1))if(𝑚 ∈ ℙ, (1 / 𝑚), 0) < (1 / 2)) | 
| 115 |  | eqid 2736 | . . . . . . 7
⊢ (𝑤 ∈ ℕ ↦ {𝑛 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣ (𝑤 ∈ ℙ ∧ 𝑤 ∥ 𝑛)}) = (𝑤 ∈ ℕ ↦ {𝑛 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣ (𝑤 ∈ ℙ ∧ 𝑤 ∥ 𝑛)}) | 
| 116 | 8, 92, 99, 107, 108, 114, 115 | prmreclem5 16959 | . . . . . 6
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → (((2↑(𝑘 + 1))↑2) / 2) <
((2↑𝑘) ·
(√‘((2↑(𝑘
+ 1))↑2)))) | 
| 117 | 116 | ex 412 | . . . . 5
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2) → (((2↑(𝑘 + 1))↑2) / 2) <
((2↑𝑘) ·
(√‘((2↑(𝑘
+ 1))↑2))))) | 
| 118 |  | eqid 2736 | . . . . . . . . 9
⊢
(ℤ≥‘(𝑘 + 1)) = (ℤ≥‘(𝑘 + 1)) | 
| 119 | 94 | nnzd 12642 | . . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (𝑘 + 1) ∈
ℤ) | 
| 120 |  | eluznn 12961 | . . . . . . . . . . 11
⊢ (((𝑘 + 1) ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(𝑘 + 1))) → 𝑗 ∈ ℕ) | 
| 121 | 94, 120 | sylan 580 | . . . . . . . . . 10
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈
(ℤ≥‘(𝑘 + 1))) → 𝑗 ∈ ℕ) | 
| 122 | 121, 41 | syl 17 | . . . . . . . . 9
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈
(ℤ≥‘(𝑘 + 1))) → (𝐹‘𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) | 
| 123 | 39 | a1i 11 | . . . . . . . . 9
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈
(ℤ≥‘(𝑘 + 1))) → if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ) | 
| 124 |  | simpl 482 | . . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ seq1( + , 𝐹) ∈
dom ⇝ ) | 
| 125 | 41 | adantl 481 | . . . . . . . . . . . 12
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
→ (𝐹‘𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) | 
| 126 | 39 | recni 11276 | . . . . . . . . . . . . 13
⊢ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈
ℂ | 
| 127 | 126 | a1i 11 | . . . . . . . . . . . 12
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
→ if(𝑗 ∈ ℙ,
(1 / 𝑗), 0) ∈
ℂ) | 
| 128 | 125, 127 | eqeltrd 2840 | . . . . . . . . . . 11
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
→ (𝐹‘𝑗) ∈
ℂ) | 
| 129 | 1, 94, 128 | iserex 15694 | . . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (seq1( + , 𝐹) ∈
dom ⇝ ↔ seq(𝑘 +
1)( + , 𝐹) ∈ dom
⇝ )) | 
| 130 | 124, 129 | mpbid 232 | . . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ seq(𝑘 + 1)( + ,
𝐹) ∈ dom ⇝
) | 
| 131 | 118, 119,
122, 123, 130 | isumrecl 15802 | . . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ) | 
| 132 | 73 | a1i 11 | . . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (1 / 2) ∈ ℝ) | 
| 133 |  | elfznn 13594 | . . . . . . . . . . . 12
⊢ (𝑗 ∈ (1...𝑘) → 𝑗 ∈ ℕ) | 
| 134 | 133 | adantl 481 | . . . . . . . . . . 11
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈ (1...𝑘)) → 𝑗 ∈ ℕ) | 
| 135 | 134, 41 | syl 17 | . . . . . . . . . 10
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈ (1...𝑘)) → (𝐹‘𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) | 
| 136 | 29, 1 | eleqtrdi 2850 | . . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ 𝑘 ∈
(ℤ≥‘1)) | 
| 137 | 126 | a1i 11 | . . . . . . . . . 10
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈ (1...𝑘)) → if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℂ) | 
| 138 | 135, 136,
137 | fsumser 15767 | . . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ Σ𝑗 ∈
(1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = (seq1( + , 𝐹)‘𝑘)) | 
| 139 | 138, 27 | eqeltrd 2840 | . . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ Σ𝑗 ∈
(1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈
ℝ) | 
| 140 | 131, 132,
139 | ltadd2d 11418 | . . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2) ↔ (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + Σ𝑗 ∈ (ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) < (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + (1 / 2)))) | 
| 141 | 1, 118, 94, 125, 127, 124 | isumsplit 15877 | . . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0) =
(Σ𝑗 ∈
(1...((𝑘 + 1) −
1))if(𝑗 ∈ ℙ, (1
/ 𝑗), 0) + Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0))) | 
| 142 |  | nncn 12275 | . . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) | 
| 143 | 142 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ 𝑘 ∈
ℂ) | 
| 144 |  | ax-1cn 11214 | . . . . . . . . . . . . 13
⊢ 1 ∈
ℂ | 
| 145 |  | pncan 11515 | . . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑘 + 1)
− 1) = 𝑘) | 
| 146 | 143, 144,
145 | sylancl 586 | . . . . . . . . . . . 12
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((𝑘 + 1) − 1)
= 𝑘) | 
| 147 | 146 | oveq2d 7448 | . . . . . . . . . . 11
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (1...((𝑘 + 1)
− 1)) = (1...𝑘)) | 
| 148 | 147 | sumeq1d 15737 | . . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ Σ𝑗 ∈
(1...((𝑘 + 1) −
1))if(𝑗 ∈ ℙ, (1
/ 𝑗), 0) = Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) | 
| 149 | 148 | oveq1d 7447 | . . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (Σ𝑗 ∈
(1...((𝑘 + 1) −
1))if(𝑗 ∈ ℙ, (1
/ 𝑗), 0) + Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) = (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + Σ𝑗 ∈ (ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0))) | 
| 150 | 141, 149 | eqtrd 2776 | . . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0) =
(Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + Σ𝑗 ∈ (ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0))) | 
| 151 | 150 | breq1d 5152 | . . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0) <
(Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + (1 / 2)) ↔ (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + Σ𝑗 ∈ (ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) < (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + (1 / 2)))) | 
| 152 | 140, 151 | bitr4d 282 | . . . . . 6
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2) ↔ Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + (1 / 2)))) | 
| 153 |  | eqid 2736 | . . . . . . . . . 10
⊢ seq1( + ,
𝐹) = seq1( + , 𝐹) | 
| 154 | 1, 153, 23, 42, 43, 54, 60 | isumsup 15884 | . . . . . . . . 9
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0) =
sup(ran seq1( + , 𝐹),
ℝ, < )) | 
| 155 | 154, 67 | eqeltrd 2840 | . . . . . . . 8
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0) ∈
ℝ) | 
| 156 | 155 | adantr 480 | . . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0) ∈
ℝ) | 
| 157 | 156, 132,
139 | ltsubaddd 11860 | . . . . . 6
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0)
− (1 / 2)) < Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ↔ Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + (1 / 2)))) | 
| 158 | 154 | adantr 480 | . . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0) =
sup(ran seq1( + , 𝐹),
ℝ, < )) | 
| 159 | 158 | oveq1d 7447 | . . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0)
− (1 / 2)) = (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 /
2))) | 
| 160 | 159, 138 | breq12d 5155 | . . . . . 6
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0)
− (1 / 2)) < Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ↔ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 /
2)) < (seq1( + , 𝐹)‘𝑘))) | 
| 161 | 152, 157,
160 | 3bitr2d 307 | . . . . 5
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2) ↔ (sup(ran seq1( + ,
𝐹), ℝ, < ) −
(1 / 2)) < (seq1( + , 𝐹)‘𝑘))) | 
| 162 |  | 2cn 12342 | . . . . . . . . . . . . 13
⊢ 2 ∈
ℂ | 
| 163 | 162 | a1i 11 | . . . . . . . . . . . 12
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ 2 ∈ ℂ) | 
| 164 | 144 | a1i 11 | . . . . . . . . . . . 12
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ 1 ∈ ℂ) | 
| 165 | 163, 143,
164 | adddid 11286 | . . . . . . . . . . 11
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2 · (𝑘 + 1))
= ((2 · 𝑘) + (2
· 1))) | 
| 166 | 94 | nncnd 12283 | . . . . . . . . . . . 12
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (𝑘 + 1) ∈
ℂ) | 
| 167 |  | mulcom 11242 | . . . . . . . . . . . 12
⊢ (((𝑘 + 1) ∈ ℂ ∧ 2
∈ ℂ) → ((𝑘
+ 1) · 2) = (2 · (𝑘 + 1))) | 
| 168 | 166, 162,
167 | sylancl 586 | . . . . . . . . . . 11
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((𝑘 + 1) · 2)
= (2 · (𝑘 +
1))) | 
| 169 | 86 | nncnd 12283 | . . . . . . . . . . . . 13
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2 · 𝑘)
∈ ℂ) | 
| 170 | 169, 164,
164 | addassd 11284 | . . . . . . . . . . . 12
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (((2 · 𝑘) +
1) + 1) = ((2 · 𝑘) +
(1 + 1))) | 
| 171 | 144 | 2timesi 12405 | . . . . . . . . . . . . 13
⊢ (2
· 1) = (1 + 1) | 
| 172 | 171 | oveq2i 7443 | . . . . . . . . . . . 12
⊢ ((2
· 𝑘) + (2 ·
1)) = ((2 · 𝑘) + (1
+ 1)) | 
| 173 | 170, 172 | eqtr4di 2794 | . . . . . . . . . . 11
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (((2 · 𝑘) +
1) + 1) = ((2 · 𝑘) +
(2 · 1))) | 
| 174 | 165, 168,
173 | 3eqtr4d 2786 | . . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((𝑘 + 1) · 2)
= (((2 · 𝑘) + 1) +
1)) | 
| 175 | 174 | oveq2d 7448 | . . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑((𝑘 + 1)
· 2)) = (2↑(((2 · 𝑘) + 1) + 1))) | 
| 176 |  | 2nn0 12545 | . . . . . . . . . . 11
⊢ 2 ∈
ℕ0 | 
| 177 | 176 | a1i 11 | . . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ 2 ∈ ℕ0) | 
| 178 | 163, 177,
95 | expmuld 14190 | . . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑((𝑘 + 1)
· 2)) = ((2↑(𝑘
+ 1))↑2)) | 
| 179 |  | expp1 14110 | . . . . . . . . . 10
⊢ ((2
∈ ℂ ∧ ((2 · 𝑘) + 1) ∈ ℕ0) →
(2↑(((2 · 𝑘) +
1) + 1)) = ((2↑((2 · 𝑘) + 1)) · 2)) | 
| 180 | 162, 88, 179 | sylancr 587 | . . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑(((2 · 𝑘) + 1) + 1)) = ((2↑((2 · 𝑘) + 1)) ·
2)) | 
| 181 | 175, 178,
180 | 3eqtr3d 2784 | . . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2↑(𝑘 +
1))↑2) = ((2↑((2 · 𝑘) + 1)) · 2)) | 
| 182 | 181 | oveq1d 7447 | . . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (((2↑(𝑘 +
1))↑2) / 2) = (((2↑((2 · 𝑘) + 1)) · 2) / 2)) | 
| 183 |  | expcl 14121 | . . . . . . . . 9
⊢ ((2
∈ ℂ ∧ ((2 · 𝑘) + 1) ∈ ℕ0) →
(2↑((2 · 𝑘) +
1)) ∈ ℂ) | 
| 184 | 162, 88, 183 | sylancr 587 | . . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑((2 · 𝑘) + 1)) ∈ ℂ) | 
| 185 |  | 2ne0 12371 | . . . . . . . . 9
⊢ 2 ≠
0 | 
| 186 |  | divcan4 11950 | . . . . . . . . 9
⊢
(((2↑((2 · 𝑘) + 1)) ∈ ℂ ∧ 2 ∈ ℂ
∧ 2 ≠ 0) → (((2↑((2 · 𝑘) + 1)) · 2) / 2) = (2↑((2
· 𝑘) +
1))) | 
| 187 | 162, 185,
186 | mp3an23 1454 | . . . . . . . 8
⊢
((2↑((2 · 𝑘) + 1)) ∈ ℂ → (((2↑((2
· 𝑘) + 1)) ·
2) / 2) = (2↑((2 · 𝑘) + 1))) | 
| 188 | 184, 187 | syl 17 | . . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (((2↑((2 · 𝑘) + 1)) · 2) / 2) = (2↑((2
· 𝑘) +
1))) | 
| 189 | 182, 188 | eqtrd 2776 | . . . . . 6
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (((2↑(𝑘 +
1))↑2) / 2) = (2↑((2 · 𝑘) + 1))) | 
| 190 |  | nnnn0 12535 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) | 
| 191 | 190 | adantl 481 | . . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ 𝑘 ∈
ℕ0) | 
| 192 | 163, 95, 191 | expaddd 14189 | . . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑(𝑘 + (𝑘 + 1))) = ((2↑𝑘) · (2↑(𝑘 + 1)))) | 
| 193 | 143 | 2timesd 12511 | . . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2 · 𝑘) =
(𝑘 + 𝑘)) | 
| 194 | 193 | oveq1d 7447 | . . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2 · 𝑘) + 1)
= ((𝑘 + 𝑘) + 1)) | 
| 195 | 143, 143,
164 | addassd 11284 | . . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((𝑘 + 𝑘) + 1) = (𝑘 + (𝑘 + 1))) | 
| 196 | 194, 195 | eqtrd 2776 | . . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2 · 𝑘) + 1)
= (𝑘 + (𝑘 + 1))) | 
| 197 | 196 | oveq2d 7448 | . . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑((2 · 𝑘) + 1)) = (2↑(𝑘 + (𝑘 + 1)))) | 
| 198 | 97 | nnrpd 13076 | . . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑(𝑘 + 1))
∈ ℝ+) | 
| 199 | 198 | rprege0d 13085 | . . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2↑(𝑘 + 1))
∈ ℝ ∧ 0 ≤ (2↑(𝑘 + 1)))) | 
| 200 |  | sqrtsq 15309 | . . . . . . . . 9
⊢
(((2↑(𝑘 + 1))
∈ ℝ ∧ 0 ≤ (2↑(𝑘 + 1))) → (√‘((2↑(𝑘 + 1))↑2)) = (2↑(𝑘 + 1))) | 
| 201 | 199, 200 | syl 17 | . . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (√‘((2↑(𝑘 + 1))↑2)) = (2↑(𝑘 + 1))) | 
| 202 | 201 | oveq2d 7448 | . . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2↑𝑘) ·
(√‘((2↑(𝑘
+ 1))↑2))) = ((2↑𝑘) · (2↑(𝑘 + 1)))) | 
| 203 | 192, 197,
202 | 3eqtr4rd 2787 | . . . . . 6
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2↑𝑘) ·
(√‘((2↑(𝑘
+ 1))↑2))) = (2↑((2 · 𝑘) + 1))) | 
| 204 | 189, 203 | breq12d 5155 | . . . . 5
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((((2↑(𝑘 +
1))↑2) / 2) < ((2↑𝑘) · (√‘((2↑(𝑘 + 1))↑2))) ↔
(2↑((2 · 𝑘) +
1)) < (2↑((2 · 𝑘) + 1)))) | 
| 205 | 117, 161,
204 | 3imtr3d 293 | . . . 4
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) <
(seq1( + , 𝐹)‘𝑘) → (2↑((2 ·
𝑘) + 1)) < (2↑((2
· 𝑘) +
1)))) | 
| 206 | 91, 205 | mtod 198 | . . 3
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ¬ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) <
(seq1( + , 𝐹)‘𝑘)) | 
| 207 | 206 | nrexdv 3148 | . 2
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ¬ ∃𝑘
∈ ℕ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) <
(seq1( + , 𝐹)‘𝑘)) | 
| 208 | 82, 207 | pm2.65i 194 | 1
⊢  ¬
seq1( + , 𝐹) ∈ dom
⇝ |