Step | Hyp | Ref
| Expression |
1 | | nnuz 11599 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 11285 |
. . . . . . . . 9
⊢ (⊤
→ 1 ∈ ℤ) |
3 | | nnrecre 10934 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (1 /
𝑛) ∈
ℝ) |
4 | 3 | adantl 481 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑛
∈ ℕ) → (1 / 𝑛) ∈ ℝ) |
5 | | 0re 9919 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ |
6 | | ifcl 4080 |
. . . . . . . . . . . 12
⊢ (((1 /
𝑛) ∈ ℝ ∧ 0
∈ ℝ) → if(𝑛
∈ ℙ, (1 / 𝑛), 0)
∈ ℝ) |
7 | 4, 5, 6 | sylancl 693 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑛
∈ ℕ) → if(𝑛
∈ ℙ, (1 / 𝑛), 0)
∈ ℝ) |
8 | | prmrec.1 |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0)) |
9 | 7, 8 | fmptd 6292 |
. . . . . . . . . 10
⊢ (⊤
→ 𝐹:ℕ⟶ℝ) |
10 | 9 | ffvelrnda 6267 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑗
∈ ℕ) → (𝐹‘𝑗) ∈ ℝ) |
11 | 1, 2, 10 | serfre 12692 |
. . . . . . . 8
⊢ (⊤
→ seq1( + , 𝐹):ℕ⟶ℝ) |
12 | 11 | trud 1484 |
. . . . . . 7
⊢ seq1( + ,
𝐹):ℕ⟶ℝ |
13 | | frn 5966 |
. . . . . . 7
⊢ (seq1( +
, 𝐹):ℕ⟶ℝ
→ ran seq1( + , 𝐹)
⊆ ℝ) |
14 | 12, 13 | mp1i 13 |
. . . . . 6
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ran seq1( + , 𝐹)
⊆ ℝ) |
15 | | 1nn 10908 |
. . . . . . . 8
⊢ 1 ∈
ℕ |
16 | 12 | fdmi 5965 |
. . . . . . . 8
⊢ dom seq1(
+ , 𝐹) =
ℕ |
17 | 15, 16 | eleqtrri 2687 |
. . . . . . 7
⊢ 1 ∈
dom seq1( + , 𝐹) |
18 | | ne0i 3880 |
. . . . . . . 8
⊢ (1 ∈
dom seq1( + , 𝐹) → dom
seq1( + , 𝐹) ≠
∅) |
19 | | dm0rn0 5263 |
. . . . . . . . 9
⊢ (dom
seq1( + , 𝐹) = ∅
↔ ran seq1( + , 𝐹) =
∅) |
20 | 19 | necon3bii 2834 |
. . . . . . . 8
⊢ (dom
seq1( + , 𝐹) ≠ ∅
↔ ran seq1( + , 𝐹)
≠ ∅) |
21 | 18, 20 | sylib 207 |
. . . . . . 7
⊢ (1 ∈
dom seq1( + , 𝐹) → ran
seq1( + , 𝐹) ≠
∅) |
22 | 17, 21 | mp1i 13 |
. . . . . 6
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ran seq1( + , 𝐹)
≠ ∅) |
23 | | 1zzd 11285 |
. . . . . . . . 9
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ 1 ∈ ℤ) |
24 | | climdm 14133 |
. . . . . . . . . 10
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
↔ seq1( + , 𝐹) ⇝
( ⇝ ‘seq1( + , 𝐹))) |
25 | 24 | biimpi 205 |
. . . . . . . . 9
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ seq1( + , 𝐹) ⇝
( ⇝ ‘seq1( + , 𝐹))) |
26 | 12 | a1i 11 |
. . . . . . . . . 10
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ seq1( + , 𝐹):ℕ⟶ℝ) |
27 | 26 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (seq1( + , 𝐹)‘𝑘) ∈ ℝ) |
28 | 1, 23, 25, 27 | climrecl 14162 |
. . . . . . . 8
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ( ⇝ ‘seq1( + , 𝐹)) ∈ ℝ) |
29 | | simpr 476 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ 𝑘 ∈
ℕ) |
30 | 25 | adantr 480 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ seq1( + , 𝐹) ⇝
( ⇝ ‘seq1( + , 𝐹))) |
31 | | eleq1 2676 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑗 → (𝑛 ∈ ℙ ↔ 𝑗 ∈ ℙ)) |
32 | | oveq2 6557 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑗 → (1 / 𝑛) = (1 / 𝑗)) |
33 | 31, 32 | ifbieq1d 4059 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑗 → if(𝑛 ∈ ℙ, (1 / 𝑛), 0) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) |
34 | | prmnn 15226 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℙ → 𝑗 ∈
ℕ) |
35 | 34 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑗
∈ ℙ) → 𝑗
∈ ℕ) |
36 | 35 | nnrecred 10943 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑗
∈ ℙ) → (1 / 𝑗) ∈ ℝ) |
37 | 5 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ ¬ 𝑗 ∈ ℙ) → 0 ∈
ℝ) |
38 | 36, 37 | ifclda 4070 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ if(𝑗 ∈ ℙ,
(1 / 𝑗), 0) ∈
ℝ) |
39 | 38 | trud 1484 |
. . . . . . . . . . . . . . 15
⊢ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈
ℝ |
40 | 39 | elexi 3186 |
. . . . . . . . . . . . . 14
⊢ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ V |
41 | 33, 8, 40 | fvmpt 6191 |
. . . . . . . . . . . . 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 2688 |
. . . . . . . . . . 11
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑗 ∈ ℕ)
→ (𝐹‘𝑗) ∈
ℝ) |
45 | 44 | adantlr 747 |
. . . . . . . . . 10
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
→ (𝐹‘𝑗) ∈
ℝ) |
46 | | nnrp 11718 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℝ+) |
47 | 46 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑗 ∈ ℕ)
→ 𝑗 ∈
ℝ+) |
48 | 47 | rpreccld 11758 |
. . . . . . . . . . . . . 14
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑗 ∈ ℕ)
→ (1 / 𝑗) ∈
ℝ+) |
49 | 48 | rpge0d 11752 |
. . . . . . . . . . . . 13
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑗 ∈ ℕ)
→ 0 ≤ (1 / 𝑗)) |
50 | | 0le0 10987 |
. . . . . . . . . . . . 13
⊢ 0 ≤
0 |
51 | | breq2 4587 |
. . . . . . . . . . . . . 14
⊢ ((1 /
𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0) → (0 ≤ (1 / 𝑗) ↔ 0 ≤ if(𝑗 ∈ ℙ, (1 / 𝑗), 0))) |
52 | | breq2 4587 |
. . . . . . . . . . . . . 14
⊢ (0 =
if(𝑗 ∈ ℙ, (1 /
𝑗), 0) → (0 ≤ 0
↔ 0 ≤ if(𝑗 ∈
ℙ, (1 / 𝑗),
0))) |
53 | 51, 52 | ifboth 4074 |
. . . . . . . . . . . . 13
⊢ ((0 ≤
(1 / 𝑗) ∧ 0 ≤ 0)
→ 0 ≤ if(𝑗 ∈
ℙ, (1 / 𝑗),
0)) |
54 | 49, 50, 53 | sylancl 693 |
. . . . . . . . . . . 12
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑗 ∈ ℕ)
→ 0 ≤ if(𝑗 ∈
ℙ, (1 / 𝑗),
0)) |
55 | 54, 42 | breqtrrd 4611 |
. . . . . . . . . . 11
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑗 ∈ ℕ)
→ 0 ≤ (𝐹‘𝑗)) |
56 | 55 | adantlr 747 |
. . . . . . . . . 10
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
→ 0 ≤ (𝐹‘𝑗)) |
57 | 1, 29, 30, 45, 56 | climserle 14241 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹))) |
58 | 57 | ralrimiva 2949 |
. . . . . . . 8
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ∀𝑘 ∈
ℕ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹))) |
59 | | breq2 4587 |
. . . . . . . . . 10
⊢ (𝑥 = ( ⇝ ‘seq1( + ,
𝐹)) → ((seq1( + ,
𝐹)‘𝑘) ≤ 𝑥 ↔ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹)))) |
60 | 59 | ralbidv 2969 |
. . . . . . . . 9
⊢ (𝑥 = ( ⇝ ‘seq1( + ,
𝐹)) → (∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹)))) |
61 | 60 | rspcev 3282 |
. . . . . . . 8
⊢ (((
⇝ ‘seq1( + , 𝐹)) ∈ ℝ ∧ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹))) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥) |
62 | 28, 58, 61 | syl2anc 691 |
. . . . . . 7
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ∃𝑥 ∈
ℝ ∀𝑘 ∈
ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥) |
63 | | ffn 5958 |
. . . . . . . . 9
⊢ (seq1( +
, 𝐹):ℕ⟶ℝ
→ seq1( + , 𝐹) Fn
ℕ) |
64 | | breq1 4586 |
. . . . . . . . . 10
⊢ (𝑧 = (seq1( + , 𝐹)‘𝑘) → (𝑧 ≤ 𝑥 ↔ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)) |
65 | 64 | ralrn 6270 |
. . . . . . . . 9
⊢ (seq1( +
, 𝐹) Fn ℕ →
(∀𝑧 ∈ ran seq1(
+ , 𝐹)𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)) |
66 | 12, 63, 65 | mp2b 10 |
. . . . . . . 8
⊢
(∀𝑧 ∈
ran seq1( + , 𝐹)𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥) |
67 | 66 | rexbii 3023 |
. . . . . . 7
⊢
(∃𝑥 ∈
ℝ ∀𝑧 ∈
ran seq1( + , 𝐹)𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥) |
68 | 62, 67 | sylibr 223 |
. . . . . 6
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ∃𝑥 ∈
ℝ ∀𝑧 ∈
ran seq1( + , 𝐹)𝑧 ≤ 𝑥) |
69 | | suprcl 10862 |
. . . . . 6
⊢ ((ran
seq1( + , 𝐹) ⊆
ℝ ∧ ran seq1( + , 𝐹) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran seq1( + , 𝐹)𝑧 ≤ 𝑥) → sup(ran seq1( + , 𝐹), ℝ, < ) ∈
ℝ) |
70 | 14, 22, 68, 69 | syl3anc 1318 |
. . . . 5
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ sup(ran seq1( + , 𝐹), ℝ, < ) ∈
ℝ) |
71 | | 2rp 11713 |
. . . . . 6
⊢ 2 ∈
ℝ+ |
72 | | rpreccl 11733 |
. . . . . 6
⊢ (2 ∈
ℝ+ → (1 / 2) ∈ ℝ+) |
73 | 71, 72 | ax-mp 5 |
. . . . 5
⊢ (1 / 2)
∈ ℝ+ |
74 | | ltsubrp 11742 |
. . . . 5
⊢ ((sup(ran
seq1( + , 𝐹), ℝ, <
) ∈ ℝ ∧ (1 / 2) ∈ ℝ+) → (sup(ran
seq1( + , 𝐹), ℝ, <
) − (1 / 2)) < sup(ran seq1( + , 𝐹), ℝ, < )) |
75 | 70, 73, 74 | sylancl 693 |
. . . 4
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) <
sup(ran seq1( + , 𝐹),
ℝ, < )) |
76 | | halfre 11123 |
. . . . . 6
⊢ (1 / 2)
∈ ℝ |
77 | | resubcl 10224 |
. . . . . 6
⊢ ((sup(ran
seq1( + , 𝐹), ℝ, <
) ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 /
2)) ∈ ℝ) |
78 | 70, 76, 77 | sylancl 693 |
. . . . 5
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) ∈
ℝ) |
79 | | suprlub 10864 |
. . . . 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)) <
𝑦)) |
80 | 14, 22, 68, 78, 79 | syl31anc 1321 |
. . . 4
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ((sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) <
sup(ran seq1( + , 𝐹),
ℝ, < ) ↔ ∃𝑦 ∈ ran seq1( + , 𝐹)(sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) <
𝑦)) |
81 | 75, 80 | mpbid 221 |
. . 3
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ∃𝑦 ∈ ran
seq1( + , 𝐹)(sup(ran seq1(
+ , 𝐹), ℝ, < )
− (1 / 2)) < 𝑦) |
82 | | breq2 4587 |
. . . . 5
⊢ (𝑦 = (seq1( + , 𝐹)‘𝑘) → ((sup(ran seq1( + , 𝐹), ℝ, < ) − (1 /
2)) < 𝑦 ↔ (sup(ran
seq1( + , 𝐹), ℝ, <
) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘))) |
83 | 82 | rexrn 6269 |
. . . 4
⊢ (seq1( +
, 𝐹) Fn ℕ →
(∃𝑦 ∈ ran seq1(
+ , 𝐹)(sup(ran seq1( + ,
𝐹), ℝ, < ) −
(1 / 2)) < 𝑦 ↔
∃𝑘 ∈ ℕ
(sup(ran seq1( + , 𝐹),
ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘))) |
84 | 12, 63, 83 | mp2b 10 |
. . 3
⊢
(∃𝑦 ∈ ran
seq1( + , 𝐹)(sup(ran seq1(
+ , 𝐹), ℝ, < )
− (1 / 2)) < 𝑦
↔ ∃𝑘 ∈
ℕ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) <
(seq1( + , 𝐹)‘𝑘)) |
85 | 81, 84 | sylib 207 |
. 2
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ∃𝑘 ∈
ℕ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) <
(seq1( + , 𝐹)‘𝑘)) |
86 | | 2re 10967 |
. . . . . 6
⊢ 2 ∈
ℝ |
87 | | 2nn 11062 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
88 | | nnmulcl 10920 |
. . . . . . . . 9
⊢ ((2
∈ ℕ ∧ 𝑘
∈ ℕ) → (2 · 𝑘) ∈ ℕ) |
89 | 87, 29, 88 | sylancr 694 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2 · 𝑘)
∈ ℕ) |
90 | 89 | peano2nnd 10914 |
. . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2 · 𝑘) + 1)
∈ ℕ) |
91 | 90 | nnnn0d 11228 |
. . . . . 6
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2 · 𝑘) + 1)
∈ ℕ0) |
92 | | reexpcl 12739 |
. . . . . 6
⊢ ((2
∈ ℝ ∧ ((2 · 𝑘) + 1) ∈ ℕ0) →
(2↑((2 · 𝑘) +
1)) ∈ ℝ) |
93 | 86, 91, 92 | sylancr 694 |
. . . . 5
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑((2 · 𝑘) + 1)) ∈ ℝ) |
94 | 93 | ltnrd 10050 |
. . . 4
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ¬ (2↑((2 · 𝑘) + 1)) < (2↑((2 · 𝑘) + 1))) |
95 | 29 | adantr 480 |
. . . . . . 7
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → 𝑘 ∈ ℕ) |
96 | | peano2nn 10909 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℕ) |
97 | 96 | adantl 481 |
. . . . . . . . . . 11
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (𝑘 + 1) ∈
ℕ) |
98 | 97 | nnnn0d 11228 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (𝑘 + 1) ∈
ℕ0) |
99 | | nnexpcl 12735 |
. . . . . . . . . 10
⊢ ((2
∈ ℕ ∧ (𝑘 +
1) ∈ ℕ0) → (2↑(𝑘 + 1)) ∈ ℕ) |
100 | 87, 98, 99 | sylancr 694 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑(𝑘 + 1))
∈ ℕ) |
101 | 100 | nnsqcld 12891 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2↑(𝑘 +
1))↑2) ∈ ℕ) |
102 | 101 | adantr 480 |
. . . . . . 7
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → ((2↑(𝑘 + 1))↑2) ∈
ℕ) |
103 | | breq1 4586 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑤 → (𝑝 ∥ 𝑟 ↔ 𝑤 ∥ 𝑟)) |
104 | 103 | notbid 307 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑤 → (¬ 𝑝 ∥ 𝑟 ↔ ¬ 𝑤 ∥ 𝑟)) |
105 | 104 | cbvralv 3147 |
. . . . . . . . 9
⊢
(∀𝑝 ∈
(ℙ ∖ (1...𝑘))
¬ 𝑝 ∥ 𝑟 ↔ ∀𝑤 ∈ (ℙ ∖
(1...𝑘)) ¬ 𝑤 ∥ 𝑟) |
106 | | breq2 4587 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑛 → (𝑤 ∥ 𝑟 ↔ 𝑤 ∥ 𝑛)) |
107 | 106 | notbid 307 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑛 → (¬ 𝑤 ∥ 𝑟 ↔ ¬ 𝑤 ∥ 𝑛)) |
108 | 107 | ralbidv 2969 |
. . . . . . . . 9
⊢ (𝑟 = 𝑛 → (∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑟 ↔ ∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑛)) |
109 | 105, 108 | syl5bb 271 |
. . . . . . . 8
⊢ (𝑟 = 𝑛 → (∀𝑝 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑝 ∥ 𝑟 ↔ ∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑛)) |
110 | 109 | cbvrabv 3172 |
. . . . . . 7
⊢ {𝑟 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣
∀𝑝 ∈ (ℙ
∖ (1...𝑘)) ¬
𝑝 ∥ 𝑟} = {𝑛 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣ ∀𝑤 ∈ (ℙ ∖
(1...𝑘)) ¬ 𝑤 ∥ 𝑛} |
111 | | simpll 786 |
. . . . . . 7
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → seq1( + , 𝐹) ∈ dom ⇝
) |
112 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑗 → (𝑚 ∈ ℙ ↔ 𝑗 ∈ ℙ)) |
113 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑗 → (1 / 𝑚) = (1 / 𝑗)) |
114 | 112, 113 | ifbieq1d 4059 |
. . . . . . . . 9
⊢ (𝑚 = 𝑗 → if(𝑚 ∈ ℙ, (1 / 𝑚), 0) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) |
115 | 114 | cbvsumv 14274 |
. . . . . . . 8
⊢
Σ𝑚 ∈
(ℤ≥‘(𝑘 + 1))if(𝑚 ∈ ℙ, (1 / 𝑚), 0) = Σ𝑗 ∈ (ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) |
116 | | simpr 476 |
. . . . . . . 8
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) |
117 | 115, 116 | syl5eqbr 4618 |
. . . . . . 7
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → Σ𝑚 ∈
(ℤ≥‘(𝑘 + 1))if(𝑚 ∈ ℙ, (1 / 𝑚), 0) < (1 / 2)) |
118 | | eqid 2610 |
. . . . . . 7
⊢ (𝑤 ∈ ℕ ↦ {𝑛 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣ (𝑤 ∈ ℙ ∧ 𝑤 ∥ 𝑛)}) = (𝑤 ∈ ℕ ↦ {𝑛 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣ (𝑤 ∈ ℙ ∧ 𝑤 ∥ 𝑛)}) |
119 | 8, 95, 102, 110, 111, 117, 118 | prmreclem5 15462 |
. . . . . 6
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → (((2↑(𝑘 + 1))↑2) / 2) <
((2↑𝑘) ·
(√‘((2↑(𝑘
+ 1))↑2)))) |
120 | 119 | ex 449 |
. . . . 5
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2) → (((2↑(𝑘 + 1))↑2) / 2) <
((2↑𝑘) ·
(√‘((2↑(𝑘
+ 1))↑2))))) |
121 | | eqid 2610 |
. . . . . . . . 9
⊢
(ℤ≥‘(𝑘 + 1)) = (ℤ≥‘(𝑘 + 1)) |
122 | 97 | nnzd 11357 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (𝑘 + 1) ∈
ℤ) |
123 | | eluznn 11634 |
. . . . . . . . . . 11
⊢ (((𝑘 + 1) ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘(𝑘 + 1))) → 𝑗 ∈ ℕ) |
124 | 97, 123 | sylan 487 |
. . . . . . . . . 10
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈
(ℤ≥‘(𝑘 + 1))) → 𝑗 ∈ ℕ) |
125 | 124, 41 | syl 17 |
. . . . . . . . 9
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈
(ℤ≥‘(𝑘 + 1))) → (𝐹‘𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) |
126 | 39 | a1i 11 |
. . . . . . . . 9
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈
(ℤ≥‘(𝑘 + 1))) → if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ) |
127 | | simpl 472 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ seq1( + , 𝐹) ∈
dom ⇝ ) |
128 | 41 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
→ (𝐹‘𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) |
129 | 39 | recni 9931 |
. . . . . . . . . . . . 13
⊢ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈
ℂ |
130 | 129 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
→ if(𝑗 ∈ ℙ,
(1 / 𝑗), 0) ∈
ℂ) |
131 | 128, 130 | eqeltrd 2688 |
. . . . . . . . . . 11
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
→ (𝐹‘𝑗) ∈
ℂ) |
132 | 1, 97, 131 | iserex 14235 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (seq1( + , 𝐹) ∈
dom ⇝ ↔ seq(𝑘 +
1)( + , 𝐹) ∈ dom
⇝ )) |
133 | 127, 132 | mpbid 221 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ seq(𝑘 + 1)( + ,
𝐹) ∈ dom ⇝
) |
134 | 121, 122,
125, 126, 133 | isumrecl 14338 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ) |
135 | 76 | a1i 11 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (1 / 2) ∈ ℝ) |
136 | | elfznn 12241 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (1...𝑘) → 𝑗 ∈ ℕ) |
137 | 136 | adantl 481 |
. . . . . . . . . . 11
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈ (1...𝑘)) → 𝑗 ∈ ℕ) |
138 | 137, 41 | syl 17 |
. . . . . . . . . 10
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈ (1...𝑘)) → (𝐹‘𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) |
139 | 29, 1 | syl6eleq 2698 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ 𝑘 ∈
(ℤ≥‘1)) |
140 | 129 | a1i 11 |
. . . . . . . . . 10
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈ (1...𝑘)) → if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℂ) |
141 | 138, 139,
140 | fsumser 14308 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ Σ𝑗 ∈
(1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = (seq1( + , 𝐹)‘𝑘)) |
142 | 141, 27 | eqeltrd 2688 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ Σ𝑗 ∈
(1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈
ℝ) |
143 | 134, 135,
142 | ltadd2d 10072 |
. . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2) ↔ (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + Σ𝑗 ∈ (ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) < (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + (1 / 2)))) |
144 | 1, 121, 97, 128, 130, 127 | isumsplit 14411 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0) =
(Σ𝑗 ∈
(1...((𝑘 + 1) −
1))if(𝑗 ∈ ℙ, (1
/ 𝑗), 0) + Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0))) |
145 | | nncn 10905 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) |
146 | 145 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ 𝑘 ∈
ℂ) |
147 | | ax-1cn 9873 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
148 | | pncan 10166 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑘 + 1)
− 1) = 𝑘) |
149 | 146, 147,
148 | sylancl 693 |
. . . . . . . . . . . 12
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((𝑘 + 1) − 1)
= 𝑘) |
150 | 149 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (1...((𝑘 + 1)
− 1)) = (1...𝑘)) |
151 | 150 | sumeq1d 14279 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ Σ𝑗 ∈
(1...((𝑘 + 1) −
1))if(𝑗 ∈ ℙ, (1
/ 𝑗), 0) = Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) |
152 | 151 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (Σ𝑗 ∈
(1...((𝑘 + 1) −
1))if(𝑗 ∈ ℙ, (1
/ 𝑗), 0) + Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) = (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + Σ𝑗 ∈ (ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0))) |
153 | 144, 152 | eqtrd 2644 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0) =
(Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + Σ𝑗 ∈ (ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0))) |
154 | 153 | breq1d 4593 |
. . . . . . 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)))) |
155 | 143, 154 | bitr4d 270 |
. . . . . 6
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2) ↔ Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + (1 / 2)))) |
156 | | eqid 2610 |
. . . . . . . . . 10
⊢ seq1( + ,
𝐹) = seq1( + , 𝐹) |
157 | 1, 156, 23, 42, 43, 54, 62 | isumsup 14418 |
. . . . . . . . 9
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0) =
sup(ran seq1( + , 𝐹),
ℝ, < )) |
158 | 157, 70 | eqeltrd 2688 |
. . . . . . . 8
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0) ∈
ℝ) |
159 | 158 | adantr 480 |
. . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0) ∈
ℝ) |
160 | 159, 135,
142 | ltsubaddd 10502 |
. . . . . 6
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0)
− (1 / 2)) < Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ↔ Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + (1 / 2)))) |
161 | 157 | adantr 480 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0) =
sup(ran seq1( + , 𝐹),
ℝ, < )) |
162 | 161 | oveq1d 6564 |
. . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0)
− (1 / 2)) = (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 /
2))) |
163 | 162, 141 | breq12d 4596 |
. . . . . 6
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0)
− (1 / 2)) < Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ↔ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 /
2)) < (seq1( + , 𝐹)‘𝑘))) |
164 | 155, 160,
163 | 3bitr2d 295 |
. . . . 5
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2) ↔ (sup(ran seq1( + ,
𝐹), ℝ, < ) −
(1 / 2)) < (seq1( + , 𝐹)‘𝑘))) |
165 | | 2cn 10968 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℂ |
166 | 165 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ 2 ∈ ℂ) |
167 | 147 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ 1 ∈ ℂ) |
168 | 166, 146,
167 | adddid 9943 |
. . . . . . . . . . 11
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2 · (𝑘 + 1))
= ((2 · 𝑘) + (2
· 1))) |
169 | 97 | nncnd 10913 |
. . . . . . . . . . . 12
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (𝑘 + 1) ∈
ℂ) |
170 | | mulcom 9901 |
. . . . . . . . . . . 12
⊢ (((𝑘 + 1) ∈ ℂ ∧ 2
∈ ℂ) → ((𝑘
+ 1) · 2) = (2 · (𝑘 + 1))) |
171 | 169, 165,
170 | sylancl 693 |
. . . . . . . . . . 11
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((𝑘 + 1) · 2)
= (2 · (𝑘 +
1))) |
172 | 89 | nncnd 10913 |
. . . . . . . . . . . . 13
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2 · 𝑘)
∈ ℂ) |
173 | 172, 167,
167 | addassd 9941 |
. . . . . . . . . . . 12
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (((2 · 𝑘) +
1) + 1) = ((2 · 𝑘) +
(1 + 1))) |
174 | 147 | 2timesi 11024 |
. . . . . . . . . . . . 13
⊢ (2
· 1) = (1 + 1) |
175 | 174 | oveq2i 6560 |
. . . . . . . . . . . 12
⊢ ((2
· 𝑘) + (2 ·
1)) = ((2 · 𝑘) + (1
+ 1)) |
176 | 173, 175 | syl6eqr 2662 |
. . . . . . . . . . 11
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (((2 · 𝑘) +
1) + 1) = ((2 · 𝑘) +
(2 · 1))) |
177 | 168, 171,
176 | 3eqtr4d 2654 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((𝑘 + 1) · 2)
= (((2 · 𝑘) + 1) +
1)) |
178 | 177 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑((𝑘 + 1)
· 2)) = (2↑(((2 · 𝑘) + 1) + 1))) |
179 | | 2nn0 11186 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ0 |
180 | 179 | a1i 11 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ 2 ∈ ℕ0) |
181 | 166, 180,
98 | expmuld 12873 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑((𝑘 + 1)
· 2)) = ((2↑(𝑘
+ 1))↑2)) |
182 | | expp1 12729 |
. . . . . . . . . 10
⊢ ((2
∈ ℂ ∧ ((2 · 𝑘) + 1) ∈ ℕ0) →
(2↑(((2 · 𝑘) +
1) + 1)) = ((2↑((2 · 𝑘) + 1)) · 2)) |
183 | 165, 91, 182 | sylancr 694 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑(((2 · 𝑘) + 1) + 1)) = ((2↑((2 · 𝑘) + 1)) ·
2)) |
184 | 178, 181,
183 | 3eqtr3d 2652 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2↑(𝑘 +
1))↑2) = ((2↑((2 · 𝑘) + 1)) · 2)) |
185 | 184 | oveq1d 6564 |
. . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (((2↑(𝑘 +
1))↑2) / 2) = (((2↑((2 · 𝑘) + 1)) · 2) / 2)) |
186 | | expcl 12740 |
. . . . . . . . 9
⊢ ((2
∈ ℂ ∧ ((2 · 𝑘) + 1) ∈ ℕ0) →
(2↑((2 · 𝑘) +
1)) ∈ ℂ) |
187 | 165, 91, 186 | sylancr 694 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑((2 · 𝑘) + 1)) ∈ ℂ) |
188 | | 2ne0 10990 |
. . . . . . . . 9
⊢ 2 ≠
0 |
189 | | divcan4 10591 |
. . . . . . . . 9
⊢
(((2↑((2 · 𝑘) + 1)) ∈ ℂ ∧ 2 ∈ ℂ
∧ 2 ≠ 0) → (((2↑((2 · 𝑘) + 1)) · 2) / 2) = (2↑((2
· 𝑘) +
1))) |
190 | 165, 188,
189 | mp3an23 1408 |
. . . . . . . 8
⊢
((2↑((2 · 𝑘) + 1)) ∈ ℂ → (((2↑((2
· 𝑘) + 1)) ·
2) / 2) = (2↑((2 · 𝑘) + 1))) |
191 | 187, 190 | syl 17 |
. . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (((2↑((2 · 𝑘) + 1)) · 2) / 2) = (2↑((2
· 𝑘) +
1))) |
192 | 185, 191 | eqtrd 2644 |
. . . . . 6
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (((2↑(𝑘 +
1))↑2) / 2) = (2↑((2 · 𝑘) + 1))) |
193 | | nnnn0 11176 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
194 | 193 | adantl 481 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ 𝑘 ∈
ℕ0) |
195 | 166, 98, 194 | expaddd 12872 |
. . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑(𝑘 + (𝑘 + 1))) = ((2↑𝑘) · (2↑(𝑘 + 1)))) |
196 | 146 | 2timesd 11152 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2 · 𝑘) =
(𝑘 + 𝑘)) |
197 | 196 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2 · 𝑘) + 1)
= ((𝑘 + 𝑘) + 1)) |
198 | 146, 146,
167 | addassd 9941 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((𝑘 + 𝑘) + 1) = (𝑘 + (𝑘 + 1))) |
199 | 197, 198 | eqtrd 2644 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2 · 𝑘) + 1)
= (𝑘 + (𝑘 + 1))) |
200 | 199 | oveq2d 6565 |
. . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑((2 · 𝑘) + 1)) = (2↑(𝑘 + (𝑘 + 1)))) |
201 | 100 | nnrpd 11746 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑(𝑘 + 1))
∈ ℝ+) |
202 | 201 | rprege0d 11755 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2↑(𝑘 + 1))
∈ ℝ ∧ 0 ≤ (2↑(𝑘 + 1)))) |
203 | | sqrtsq 13858 |
. . . . . . . . 9
⊢
(((2↑(𝑘 + 1))
∈ ℝ ∧ 0 ≤ (2↑(𝑘 + 1))) → (√‘((2↑(𝑘 + 1))↑2)) = (2↑(𝑘 + 1))) |
204 | 202, 203 | syl 17 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (√‘((2↑(𝑘 + 1))↑2)) = (2↑(𝑘 + 1))) |
205 | 204 | oveq2d 6565 |
. . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2↑𝑘) ·
(√‘((2↑(𝑘
+ 1))↑2))) = ((2↑𝑘) · (2↑(𝑘 + 1)))) |
206 | 195, 200,
205 | 3eqtr4rd 2655 |
. . . . . 6
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2↑𝑘) ·
(√‘((2↑(𝑘
+ 1))↑2))) = (2↑((2 · 𝑘) + 1))) |
207 | 192, 206 | breq12d 4596 |
. . . . 5
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((((2↑(𝑘 +
1))↑2) / 2) < ((2↑𝑘) · (√‘((2↑(𝑘 + 1))↑2))) ↔
(2↑((2 · 𝑘) +
1)) < (2↑((2 · 𝑘) + 1)))) |
208 | 120, 164,
207 | 3imtr3d 281 |
. . . 4
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) <
(seq1( + , 𝐹)‘𝑘) → (2↑((2 ·
𝑘) + 1)) < (2↑((2
· 𝑘) +
1)))) |
209 | 94, 208 | mtod 188 |
. . 3
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ¬ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) <
(seq1( + , 𝐹)‘𝑘)) |
210 | 209 | nrexdv 2984 |
. 2
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ¬ ∃𝑘
∈ ℕ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) <
(seq1( + , 𝐹)‘𝑘)) |
211 | 85, 210 | pm2.65i 184 |
1
⊢ ¬
seq1( + , 𝐹) ∈ dom
⇝ |