Step | Hyp | Ref
| Expression |
1 | | nnuz 12621 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 12351 |
. . . . . . . . 9
⊢ (⊤
→ 1 ∈ ℤ) |
3 | | nnrecre 12015 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (1 /
𝑛) ∈
ℝ) |
4 | 3 | adantl 482 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑛
∈ ℕ) → (1 / 𝑛) ∈ ℝ) |
5 | | 0re 10977 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ |
6 | | ifcl 4504 |
. . . . . . . . . . . 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 6988 |
. . . . . . . . . 10
⊢ (⊤
→ 𝐹:ℕ⟶ℝ) |
10 | 9 | ffvelrnda 6961 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑗
∈ ℕ) → (𝐹‘𝑗) ∈ ℝ) |
11 | 1, 2, 10 | serfre 13752 |
. . . . . . . 8
⊢ (⊤
→ seq1( + , 𝐹):ℕ⟶ℝ) |
12 | 11 | mptru 1546 |
. . . . . . 7
⊢ seq1( + ,
𝐹):ℕ⟶ℝ |
13 | | frn 6607 |
. . . . . . 7
⊢ (seq1( +
, 𝐹):ℕ⟶ℝ
→ ran seq1( + , 𝐹)
⊆ ℝ) |
14 | 12, 13 | mp1i 13 |
. . . . . 6
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ran seq1( + , 𝐹)
⊆ ℝ) |
15 | | 1nn 11984 |
. . . . . . . 8
⊢ 1 ∈
ℕ |
16 | 12 | fdmi 6612 |
. . . . . . . 8
⊢ dom seq1(
+ , 𝐹) =
ℕ |
17 | 15, 16 | eleqtrri 2838 |
. . . . . . 7
⊢ 1 ∈
dom seq1( + , 𝐹) |
18 | | ne0i 4268 |
. . . . . . . 8
⊢ (1 ∈
dom seq1( + , 𝐹) → dom
seq1( + , 𝐹) ≠
∅) |
19 | | dm0rn0 5834 |
. . . . . . . . 9
⊢ (dom
seq1( + , 𝐹) = ∅
↔ ran seq1( + , 𝐹) =
∅) |
20 | 19 | necon3bii 2996 |
. . . . . . . 8
⊢ (dom
seq1( + , 𝐹) ≠ ∅
↔ ran seq1( + , 𝐹)
≠ ∅) |
21 | 18, 20 | sylib 217 |
. . . . . . 7
⊢ (1 ∈
dom seq1( + , 𝐹) → ran
seq1( + , 𝐹) ≠
∅) |
22 | 17, 21 | mp1i 13 |
. . . . . 6
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ran seq1( + , 𝐹)
≠ ∅) |
23 | | 1zzd 12351 |
. . . . . . . . 9
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ 1 ∈ ℤ) |
24 | | climdm 15263 |
. . . . . . . . . 10
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
↔ seq1( + , 𝐹) ⇝
( ⇝ ‘seq1( + , 𝐹))) |
25 | 24 | biimpi 215 |
. . . . . . . . 9
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ seq1( + , 𝐹) ⇝
( ⇝ ‘seq1( + , 𝐹))) |
26 | 12 | a1i 11 |
. . . . . . . . . 10
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ seq1( + , 𝐹):ℕ⟶ℝ) |
27 | 26 | ffvelrnda 6961 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (seq1( + , 𝐹)‘𝑘) ∈ ℝ) |
28 | 1, 23, 25, 27 | climrecl 15292 |
. . . . . . . 8
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ( ⇝ ‘seq1( + , 𝐹)) ∈ ℝ) |
29 | | simpr 485 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ 𝑘 ∈
ℕ) |
30 | 25 | adantr 481 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ seq1( + , 𝐹) ⇝
( ⇝ ‘seq1( + , 𝐹))) |
31 | | eleq1w 2821 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑗 → (𝑛 ∈ ℙ ↔ 𝑗 ∈ ℙ)) |
32 | | oveq2 7283 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑗 → (1 / 𝑛) = (1 / 𝑗)) |
33 | 31, 32 | ifbieq1d 4483 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑗 → if(𝑛 ∈ ℙ, (1 / 𝑛), 0) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) |
34 | | prmnn 16379 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℙ → 𝑗 ∈
ℕ) |
35 | 34 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑗
∈ ℙ) → 𝑗
∈ ℕ) |
36 | 35 | nnrecred 12024 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑗
∈ ℙ) → (1 / 𝑗) ∈ ℝ) |
37 | 5 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ ¬ 𝑗 ∈ ℙ) → 0 ∈
ℝ) |
38 | 36, 37 | ifclda 4494 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ if(𝑗 ∈ ℙ,
(1 / 𝑗), 0) ∈
ℝ) |
39 | 38 | mptru 1546 |
. . . . . . . . . . . . . . 15
⊢ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈
ℝ |
40 | 39 | elexi 3451 |
. . . . . . . . . . . . . 14
⊢ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ V |
41 | 33, 8, 40 | fvmpt 6875 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ℕ → (𝐹‘𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) |
42 | 41 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑗 ∈ ℕ)
→ (𝐹‘𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) |
43 | 39 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑗 ∈ ℕ)
→ if(𝑗 ∈ ℙ,
(1 / 𝑗), 0) ∈
ℝ) |
44 | 42, 43 | eqeltrd 2839 |
. . . . . . . . . . 11
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑗 ∈ ℕ)
→ (𝐹‘𝑗) ∈
ℝ) |
45 | 44 | adantlr 712 |
. . . . . . . . . 10
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
→ (𝐹‘𝑗) ∈
ℝ) |
46 | | nnrp 12741 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℝ+) |
47 | 46 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑗 ∈ ℕ)
→ 𝑗 ∈
ℝ+) |
48 | 47 | rpreccld 12782 |
. . . . . . . . . . . . . 14
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑗 ∈ ℕ)
→ (1 / 𝑗) ∈
ℝ+) |
49 | 48 | rpge0d 12776 |
. . . . . . . . . . . . 13
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑗 ∈ ℕ)
→ 0 ≤ (1 / 𝑗)) |
50 | | 0le0 12074 |
. . . . . . . . . . . . 13
⊢ 0 ≤
0 |
51 | | breq2 5078 |
. . . . . . . . . . . . . 14
⊢ ((1 /
𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0) → (0 ≤ (1 / 𝑗) ↔ 0 ≤ if(𝑗 ∈ ℙ, (1 / 𝑗), 0))) |
52 | | breq2 5078 |
. . . . . . . . . . . . . 14
⊢ (0 =
if(𝑗 ∈ ℙ, (1 /
𝑗), 0) → (0 ≤ 0
↔ 0 ≤ if(𝑗 ∈
ℙ, (1 / 𝑗),
0))) |
53 | 51, 52 | ifboth 4498 |
. . . . . . . . . . . . 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 5102 |
. . . . . . . . . . 11
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑗 ∈ ℕ)
→ 0 ≤ (𝐹‘𝑗)) |
56 | 55 | adantlr 712 |
. . . . . . . . . 10
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
→ 0 ≤ (𝐹‘𝑗)) |
57 | 1, 29, 30, 45, 56 | climserle 15374 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹))) |
58 | 57 | ralrimiva 3103 |
. . . . . . . 8
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ∀𝑘 ∈
ℕ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹))) |
59 | | brralrspcev 5134 |
. . . . . . . 8
⊢ (((
⇝ ‘seq1( + , 𝐹)) ∈ ℝ ∧ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹))) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥) |
60 | 28, 58, 59 | syl2anc 584 |
. . . . . . 7
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ∃𝑥 ∈
ℝ ∀𝑘 ∈
ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥) |
61 | | ffn 6600 |
. . . . . . . . 9
⊢ (seq1( +
, 𝐹):ℕ⟶ℝ
→ seq1( + , 𝐹) Fn
ℕ) |
62 | | breq1 5077 |
. . . . . . . . . 10
⊢ (𝑧 = (seq1( + , 𝐹)‘𝑘) → (𝑧 ≤ 𝑥 ↔ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)) |
63 | 62 | ralrn 6964 |
. . . . . . . . 9
⊢ (seq1( +
, 𝐹) Fn ℕ →
(∀𝑧 ∈ ran seq1(
+ , 𝐹)𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)) |
64 | 12, 61, 63 | mp2b 10 |
. . . . . . . 8
⊢
(∀𝑧 ∈
ran seq1( + , 𝐹)𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥) |
65 | 64 | rexbii 3181 |
. . . . . . 7
⊢
(∃𝑥 ∈
ℝ ∀𝑧 ∈
ran seq1( + , 𝐹)𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥) |
66 | 60, 65 | sylibr 233 |
. . . . . 6
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ∃𝑥 ∈
ℝ ∀𝑧 ∈
ran seq1( + , 𝐹)𝑧 ≤ 𝑥) |
67 | 14, 22, 66 | suprcld 11938 |
. . . . 5
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ sup(ran seq1( + , 𝐹), ℝ, < ) ∈
ℝ) |
68 | | 2rp 12735 |
. . . . . 6
⊢ 2 ∈
ℝ+ |
69 | | rpreccl 12756 |
. . . . . 6
⊢ (2 ∈
ℝ+ → (1 / 2) ∈ ℝ+) |
70 | 68, 69 | ax-mp 5 |
. . . . 5
⊢ (1 / 2)
∈ ℝ+ |
71 | | ltsubrp 12766 |
. . . . 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 12187 |
. . . . . 6
⊢ (1 / 2)
∈ ℝ |
74 | | resubcl 11285 |
. . . . . 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 11939 |
. . . . 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 1372 |
. . . 4
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ((sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) <
sup(ran seq1( + , 𝐹),
ℝ, < ) ↔ ∃𝑦 ∈ ran seq1( + , 𝐹)(sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) <
𝑦)) |
78 | 72, 77 | mpbid 231 |
. . 3
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ∃𝑦 ∈ ran
seq1( + , 𝐹)(sup(ran seq1(
+ , 𝐹), ℝ, < )
− (1 / 2)) < 𝑦) |
79 | | breq2 5078 |
. . . . 5
⊢ (𝑦 = (seq1( + , 𝐹)‘𝑘) → ((sup(ran seq1( + , 𝐹), ℝ, < ) − (1 /
2)) < 𝑦 ↔ (sup(ran
seq1( + , 𝐹), ℝ, <
) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘))) |
80 | 79 | rexrn 6963 |
. . . 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 217 |
. 2
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ∃𝑘 ∈
ℕ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) <
(seq1( + , 𝐹)‘𝑘)) |
83 | | 2re 12047 |
. . . . . 6
⊢ 2 ∈
ℝ |
84 | | 2nn 12046 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
85 | | nnmulcl 11997 |
. . . . . . . . 9
⊢ ((2
∈ ℕ ∧ 𝑘
∈ ℕ) → (2 · 𝑘) ∈ ℕ) |
86 | 84, 29, 85 | sylancr 587 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2 · 𝑘)
∈ ℕ) |
87 | 86 | peano2nnd 11990 |
. . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2 · 𝑘) + 1)
∈ ℕ) |
88 | 87 | nnnn0d 12293 |
. . . . . 6
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2 · 𝑘) + 1)
∈ ℕ0) |
89 | | reexpcl 13799 |
. . . . . 6
⊢ ((2
∈ ℝ ∧ ((2 · 𝑘) + 1) ∈ ℕ0) →
(2↑((2 · 𝑘) +
1)) ∈ ℝ) |
90 | 83, 88, 89 | sylancr 587 |
. . . . 5
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑((2 · 𝑘) + 1)) ∈ ℝ) |
91 | 90 | ltnrd 11109 |
. . . 4
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ¬ (2↑((2 · 𝑘) + 1)) < (2↑((2 · 𝑘) + 1))) |
92 | 29 | adantr 481 |
. . . . . . 7
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → 𝑘 ∈ ℕ) |
93 | | peano2nn 11985 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℕ) |
94 | 93 | adantl 482 |
. . . . . . . . . . 11
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (𝑘 + 1) ∈
ℕ) |
95 | 94 | nnnn0d 12293 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (𝑘 + 1) ∈
ℕ0) |
96 | | nnexpcl 13795 |
. . . . . . . . . 10
⊢ ((2
∈ ℕ ∧ (𝑘 +
1) ∈ ℕ0) → (2↑(𝑘 + 1)) ∈ ℕ) |
97 | 84, 95, 96 | sylancr 587 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑(𝑘 + 1))
∈ ℕ) |
98 | 97 | nnsqcld 13959 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2↑(𝑘 +
1))↑2) ∈ ℕ) |
99 | 98 | adantr 481 |
. . . . . . 7
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → ((2↑(𝑘 + 1))↑2) ∈
ℕ) |
100 | | breq1 5077 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑤 → (𝑝 ∥ 𝑟 ↔ 𝑤 ∥ 𝑟)) |
101 | 100 | notbid 318 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑤 → (¬ 𝑝 ∥ 𝑟 ↔ ¬ 𝑤 ∥ 𝑟)) |
102 | 101 | cbvralvw 3383 |
. . . . . . . . 9
⊢
(∀𝑝 ∈
(ℙ ∖ (1...𝑘))
¬ 𝑝 ∥ 𝑟 ↔ ∀𝑤 ∈ (ℙ ∖
(1...𝑘)) ¬ 𝑤 ∥ 𝑟) |
103 | | breq2 5078 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑛 → (𝑤 ∥ 𝑟 ↔ 𝑤 ∥ 𝑛)) |
104 | 103 | notbid 318 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑛 → (¬ 𝑤 ∥ 𝑟 ↔ ¬ 𝑤 ∥ 𝑛)) |
105 | 104 | ralbidv 3112 |
. . . . . . . . 9
⊢ (𝑟 = 𝑛 → (∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑟 ↔ ∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑛)) |
106 | 102, 105 | bitrid 282 |
. . . . . . . 8
⊢ (𝑟 = 𝑛 → (∀𝑝 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑝 ∥ 𝑟 ↔ ∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑛)) |
107 | 106 | cbvrabv 3426 |
. . . . . . 7
⊢ {𝑟 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣
∀𝑝 ∈ (ℙ
∖ (1...𝑘)) ¬
𝑝 ∥ 𝑟} = {𝑛 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣ ∀𝑤 ∈ (ℙ ∖
(1...𝑘)) ¬ 𝑤 ∥ 𝑛} |
108 | | simpll 764 |
. . . . . . 7
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → seq1( + , 𝐹) ∈ dom ⇝
) |
109 | | eleq1w 2821 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑗 → (𝑚 ∈ ℙ ↔ 𝑗 ∈ ℙ)) |
110 | | oveq2 7283 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑗 → (1 / 𝑚) = (1 / 𝑗)) |
111 | 109, 110 | ifbieq1d 4483 |
. . . . . . . . 9
⊢ (𝑚 = 𝑗 → if(𝑚 ∈ ℙ, (1 / 𝑚), 0) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) |
112 | 111 | cbvsumv 15408 |
. . . . . . . 8
⊢
Σ𝑚 ∈
(ℤ≥‘(𝑘 + 1))if(𝑚 ∈ ℙ, (1 / 𝑚), 0) = Σ𝑗 ∈ (ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) |
113 | | simpr 485 |
. . . . . . . 8
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) |
114 | 112, 113 | eqbrtrid 5109 |
. . . . . . 7
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → Σ𝑚 ∈
(ℤ≥‘(𝑘 + 1))if(𝑚 ∈ ℙ, (1 / 𝑚), 0) < (1 / 2)) |
115 | | eqid 2738 |
. . . . . . 7
⊢ (𝑤 ∈ ℕ ↦ {𝑛 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣ (𝑤 ∈ ℙ ∧ 𝑤 ∥ 𝑛)}) = (𝑤 ∈ ℕ ↦ {𝑛 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣ (𝑤 ∈ ℙ ∧ 𝑤 ∥ 𝑛)}) |
116 | 8, 92, 99, 107, 108, 114, 115 | prmreclem5 16621 |
. . . . . 6
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → (((2↑(𝑘 + 1))↑2) / 2) <
((2↑𝑘) ·
(√‘((2↑(𝑘
+ 1))↑2)))) |
117 | 116 | ex 413 |
. . . . 5
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2) → (((2↑(𝑘 + 1))↑2) / 2) <
((2↑𝑘) ·
(√‘((2↑(𝑘
+ 1))↑2))))) |
118 | | eqid 2738 |
. . . . . . . . 9
⊢
(ℤ≥‘(𝑘 + 1)) = (ℤ≥‘(𝑘 + 1)) |
119 | 94 | nnzd 12425 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (𝑘 + 1) ∈
ℤ) |
120 | | eluznn 12658 |
. . . . . . . . . . 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 483 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ seq1( + , 𝐹) ∈
dom ⇝ ) |
125 | 41 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
→ (𝐹‘𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) |
126 | 39 | recni 10989 |
. . . . . . . . . . . . 13
⊢ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈
ℂ |
127 | 126 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
→ if(𝑗 ∈ ℙ,
(1 / 𝑗), 0) ∈
ℂ) |
128 | 125, 127 | eqeltrd 2839 |
. . . . . . . . . . 11
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
→ (𝐹‘𝑗) ∈
ℂ) |
129 | 1, 94, 128 | iserex 15368 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (seq1( + , 𝐹) ∈
dom ⇝ ↔ seq(𝑘 +
1)( + , 𝐹) ∈ dom
⇝ )) |
130 | 124, 129 | mpbid 231 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ seq(𝑘 + 1)( + ,
𝐹) ∈ dom ⇝
) |
131 | 118, 119,
122, 123, 130 | isumrecl 15477 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ) |
132 | 73 | a1i 11 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (1 / 2) ∈ ℝ) |
133 | | elfznn 13285 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (1...𝑘) → 𝑗 ∈ ℕ) |
134 | 133 | adantl 482 |
. . . . . . . . . . 11
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈ (1...𝑘)) → 𝑗 ∈ ℕ) |
135 | 134, 41 | syl 17 |
. . . . . . . . . 10
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈ (1...𝑘)) → (𝐹‘𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) |
136 | 29, 1 | eleqtrdi 2849 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ 𝑘 ∈
(ℤ≥‘1)) |
137 | 126 | a1i 11 |
. . . . . . . . . 10
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈ (1...𝑘)) → if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℂ) |
138 | 135, 136,
137 | fsumser 15442 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ Σ𝑗 ∈
(1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = (seq1( + , 𝐹)‘𝑘)) |
139 | 138, 27 | eqeltrd 2839 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ Σ𝑗 ∈
(1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈
ℝ) |
140 | 131, 132,
139 | ltadd2d 11131 |
. . . . . . 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 15552 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0) =
(Σ𝑗 ∈
(1...((𝑘 + 1) −
1))if(𝑗 ∈ ℙ, (1
/ 𝑗), 0) + Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0))) |
142 | | nncn 11981 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) |
143 | 142 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ 𝑘 ∈
ℂ) |
144 | | ax-1cn 10929 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
145 | | pncan 11227 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑘 + 1)
− 1) = 𝑘) |
146 | 143, 144,
145 | sylancl 586 |
. . . . . . . . . . . 12
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((𝑘 + 1) − 1)
= 𝑘) |
147 | 146 | oveq2d 7291 |
. . . . . . . . . . 11
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (1...((𝑘 + 1)
− 1)) = (1...𝑘)) |
148 | 147 | sumeq1d 15413 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ Σ𝑗 ∈
(1...((𝑘 + 1) −
1))if(𝑗 ∈ ℙ, (1
/ 𝑗), 0) = Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) |
149 | 148 | oveq1d 7290 |
. . . . . . . . 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 2778 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0) =
(Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + Σ𝑗 ∈ (ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0))) |
151 | 150 | breq1d 5084 |
. . . . . . 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 281 |
. . . . . 6
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2) ↔ Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + (1 / 2)))) |
153 | | eqid 2738 |
. . . . . . . . . 10
⊢ seq1( + ,
𝐹) = seq1( + , 𝐹) |
154 | 1, 153, 23, 42, 43, 54, 60 | isumsup 15559 |
. . . . . . . . 9
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0) =
sup(ran seq1( + , 𝐹),
ℝ, < )) |
155 | 154, 67 | eqeltrd 2839 |
. . . . . . . 8
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0) ∈
ℝ) |
156 | 155 | adantr 481 |
. . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0) ∈
ℝ) |
157 | 156, 132,
139 | ltsubaddd 11571 |
. . . . . 6
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0)
− (1 / 2)) < Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ↔ Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + (1 / 2)))) |
158 | 154 | adantr 481 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0) =
sup(ran seq1( + , 𝐹),
ℝ, < )) |
159 | 158 | oveq1d 7290 |
. . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0)
− (1 / 2)) = (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 /
2))) |
160 | 159, 138 | breq12d 5087 |
. . . . . 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 12048 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℂ |
163 | 162 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ 2 ∈ ℂ) |
164 | 144 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ 1 ∈ ℂ) |
165 | 163, 143,
164 | adddid 10999 |
. . . . . . . . . . 11
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2 · (𝑘 + 1))
= ((2 · 𝑘) + (2
· 1))) |
166 | 94 | nncnd 11989 |
. . . . . . . . . . . 12
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (𝑘 + 1) ∈
ℂ) |
167 | | mulcom 10957 |
. . . . . . . . . . . 12
⊢ (((𝑘 + 1) ∈ ℂ ∧ 2
∈ ℂ) → ((𝑘
+ 1) · 2) = (2 · (𝑘 + 1))) |
168 | 166, 162,
167 | sylancl 586 |
. . . . . . . . . . 11
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((𝑘 + 1) · 2)
= (2 · (𝑘 +
1))) |
169 | 86 | nncnd 11989 |
. . . . . . . . . . . . 13
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2 · 𝑘)
∈ ℂ) |
170 | 169, 164,
164 | addassd 10997 |
. . . . . . . . . . . 12
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (((2 · 𝑘) +
1) + 1) = ((2 · 𝑘) +
(1 + 1))) |
171 | 144 | 2timesi 12111 |
. . . . . . . . . . . . 13
⊢ (2
· 1) = (1 + 1) |
172 | 171 | oveq2i 7286 |
. . . . . . . . . . . 12
⊢ ((2
· 𝑘) + (2 ·
1)) = ((2 · 𝑘) + (1
+ 1)) |
173 | 170, 172 | eqtr4di 2796 |
. . . . . . . . . . 11
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (((2 · 𝑘) +
1) + 1) = ((2 · 𝑘) +
(2 · 1))) |
174 | 165, 168,
173 | 3eqtr4d 2788 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((𝑘 + 1) · 2)
= (((2 · 𝑘) + 1) +
1)) |
175 | 174 | oveq2d 7291 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑((𝑘 + 1)
· 2)) = (2↑(((2 · 𝑘) + 1) + 1))) |
176 | | 2nn0 12250 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ0 |
177 | 176 | a1i 11 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ 2 ∈ ℕ0) |
178 | 163, 177,
95 | expmuld 13867 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑((𝑘 + 1)
· 2)) = ((2↑(𝑘
+ 1))↑2)) |
179 | | expp1 13789 |
. . . . . . . . . 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 2786 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2↑(𝑘 +
1))↑2) = ((2↑((2 · 𝑘) + 1)) · 2)) |
182 | 181 | oveq1d 7290 |
. . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (((2↑(𝑘 +
1))↑2) / 2) = (((2↑((2 · 𝑘) + 1)) · 2) / 2)) |
183 | | expcl 13800 |
. . . . . . . . 9
⊢ ((2
∈ ℂ ∧ ((2 · 𝑘) + 1) ∈ ℕ0) →
(2↑((2 · 𝑘) +
1)) ∈ ℂ) |
184 | 162, 88, 183 | sylancr 587 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑((2 · 𝑘) + 1)) ∈ ℂ) |
185 | | 2ne0 12077 |
. . . . . . . . 9
⊢ 2 ≠
0 |
186 | | divcan4 11660 |
. . . . . . . . 9
⊢
(((2↑((2 · 𝑘) + 1)) ∈ ℂ ∧ 2 ∈ ℂ
∧ 2 ≠ 0) → (((2↑((2 · 𝑘) + 1)) · 2) / 2) = (2↑((2
· 𝑘) +
1))) |
187 | 162, 185,
186 | mp3an23 1452 |
. . . . . . . 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 2778 |
. . . . . 6
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (((2↑(𝑘 +
1))↑2) / 2) = (2↑((2 · 𝑘) + 1))) |
190 | | nnnn0 12240 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
191 | 190 | adantl 482 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ 𝑘 ∈
ℕ0) |
192 | 163, 95, 191 | expaddd 13866 |
. . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑(𝑘 + (𝑘 + 1))) = ((2↑𝑘) · (2↑(𝑘 + 1)))) |
193 | 143 | 2timesd 12216 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2 · 𝑘) =
(𝑘 + 𝑘)) |
194 | 193 | oveq1d 7290 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2 · 𝑘) + 1)
= ((𝑘 + 𝑘) + 1)) |
195 | 143, 143,
164 | addassd 10997 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((𝑘 + 𝑘) + 1) = (𝑘 + (𝑘 + 1))) |
196 | 194, 195 | eqtrd 2778 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2 · 𝑘) + 1)
= (𝑘 + (𝑘 + 1))) |
197 | 196 | oveq2d 7291 |
. . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑((2 · 𝑘) + 1)) = (2↑(𝑘 + (𝑘 + 1)))) |
198 | 97 | nnrpd 12770 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑(𝑘 + 1))
∈ ℝ+) |
199 | 198 | rprege0d 12779 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2↑(𝑘 + 1))
∈ ℝ ∧ 0 ≤ (2↑(𝑘 + 1)))) |
200 | | sqrtsq 14981 |
. . . . . . . . 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 7291 |
. . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2↑𝑘) ·
(√‘((2↑(𝑘
+ 1))↑2))) = ((2↑𝑘) · (2↑(𝑘 + 1)))) |
203 | 192, 197,
202 | 3eqtr4rd 2789 |
. . . . . 6
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2↑𝑘) ·
(√‘((2↑(𝑘
+ 1))↑2))) = (2↑((2 · 𝑘) + 1))) |
204 | 189, 203 | breq12d 5087 |
. . . . 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 197 |
. . 3
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ¬ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) <
(seq1( + , 𝐹)‘𝑘)) |
207 | 206 | nrexdv 3198 |
. 2
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ¬ ∃𝑘
∈ ℕ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) <
(seq1( + , 𝐹)‘𝑘)) |
208 | 82, 207 | pm2.65i 193 |
1
⊢ ¬
seq1( + , 𝐹) ∈ dom
⇝ |