Step | Hyp | Ref
| Expression |
1 | | nnuz 12806 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 12534 |
. . . . . . . . 9
⊢ (⊤
→ 1 ∈ ℤ) |
3 | | nnrecre 12195 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (1 /
𝑛) ∈
ℝ) |
4 | 3 | adantl 482 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑛
∈ ℕ) → (1 / 𝑛) ∈ ℝ) |
5 | | 0re 11157 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ |
6 | | ifcl 4531 |
. . . . . . . . . . . 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 7062 |
. . . . . . . . . 10
⊢ (⊤
→ 𝐹:ℕ⟶ℝ) |
10 | 9 | ffvelcdmda 7035 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑗
∈ ℕ) → (𝐹‘𝑗) ∈ ℝ) |
11 | 1, 2, 10 | serfre 13937 |
. . . . . . . 8
⊢ (⊤
→ seq1( + , 𝐹):ℕ⟶ℝ) |
12 | 11 | mptru 1548 |
. . . . . . 7
⊢ seq1( + ,
𝐹):ℕ⟶ℝ |
13 | | frn 6675 |
. . . . . . 7
⊢ (seq1( +
, 𝐹):ℕ⟶ℝ
→ ran seq1( + , 𝐹)
⊆ ℝ) |
14 | 12, 13 | mp1i 13 |
. . . . . 6
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ran seq1( + , 𝐹)
⊆ ℝ) |
15 | | 1nn 12164 |
. . . . . . . 8
⊢ 1 ∈
ℕ |
16 | 12 | fdmi 6680 |
. . . . . . . 8
⊢ dom seq1(
+ , 𝐹) =
ℕ |
17 | 15, 16 | eleqtrri 2837 |
. . . . . . 7
⊢ 1 ∈
dom seq1( + , 𝐹) |
18 | | ne0i 4294 |
. . . . . . . 8
⊢ (1 ∈
dom seq1( + , 𝐹) → dom
seq1( + , 𝐹) ≠
∅) |
19 | | dm0rn0 5880 |
. . . . . . . . 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 12534 |
. . . . . . . . 9
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ 1 ∈ ℤ) |
24 | | climdm 15436 |
. . . . . . . . . 10
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
↔ seq1( + , 𝐹) ⇝
( ⇝ ‘seq1( + , 𝐹))) |
25 | 24 | biimpi 215 |
. . . . . . . . 9
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ seq1( + , 𝐹) ⇝
( ⇝ ‘seq1( + , 𝐹))) |
26 | 12 | a1i 11 |
. . . . . . . . . 10
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ seq1( + , 𝐹):ℕ⟶ℝ) |
27 | 26 | ffvelcdmda 7035 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (seq1( + , 𝐹)‘𝑘) ∈ ℝ) |
28 | 1, 23, 25, 27 | climrecl 15465 |
. . . . . . . 8
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ( ⇝ ‘seq1( + , 𝐹)) ∈ ℝ) |
29 | | simpr 485 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ 𝑘 ∈
ℕ) |
30 | 25 | adantr 481 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ seq1( + , 𝐹) ⇝
( ⇝ ‘seq1( + , 𝐹))) |
31 | | eleq1w 2820 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑗 → (𝑛 ∈ ℙ ↔ 𝑗 ∈ ℙ)) |
32 | | oveq2 7365 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑗 → (1 / 𝑛) = (1 / 𝑗)) |
33 | 31, 32 | ifbieq1d 4510 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑗 → if(𝑛 ∈ ℙ, (1 / 𝑛), 0) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) |
34 | | prmnn 16550 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℙ → 𝑗 ∈
ℕ) |
35 | 34 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑗
∈ ℙ) → 𝑗
∈ ℕ) |
36 | 35 | nnrecred 12204 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑗
∈ ℙ) → (1 / 𝑗) ∈ ℝ) |
37 | 5 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ ¬ 𝑗 ∈ ℙ) → 0 ∈
ℝ) |
38 | 36, 37 | ifclda 4521 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ if(𝑗 ∈ ℙ,
(1 / 𝑗), 0) ∈
ℝ) |
39 | 38 | mptru 1548 |
. . . . . . . . . . . . . . 15
⊢ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈
ℝ |
40 | 39 | elexi 3464 |
. . . . . . . . . . . . . 14
⊢ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ V |
41 | 33, 8, 40 | fvmpt 6948 |
. . . . . . . . . . . . 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 2838 |
. . . . . . . . . . 11
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑗 ∈ ℕ)
→ (𝐹‘𝑗) ∈
ℝ) |
45 | 44 | adantlr 713 |
. . . . . . . . . 10
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
→ (𝐹‘𝑗) ∈
ℝ) |
46 | | nnrp 12926 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℝ+) |
47 | 46 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑗 ∈ ℕ)
→ 𝑗 ∈
ℝ+) |
48 | 47 | rpreccld 12967 |
. . . . . . . . . . . . . 14
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑗 ∈ ℕ)
→ (1 / 𝑗) ∈
ℝ+) |
49 | 48 | rpge0d 12961 |
. . . . . . . . . . . . 13
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑗 ∈ ℕ)
→ 0 ≤ (1 / 𝑗)) |
50 | | 0le0 12254 |
. . . . . . . . . . . . 13
⊢ 0 ≤
0 |
51 | | breq2 5109 |
. . . . . . . . . . . . . 14
⊢ ((1 /
𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0) → (0 ≤ (1 / 𝑗) ↔ 0 ≤ if(𝑗 ∈ ℙ, (1 / 𝑗), 0))) |
52 | | breq2 5109 |
. . . . . . . . . . . . . 14
⊢ (0 =
if(𝑗 ∈ ℙ, (1 /
𝑗), 0) → (0 ≤ 0
↔ 0 ≤ if(𝑗 ∈
ℙ, (1 / 𝑗),
0))) |
53 | 51, 52 | ifboth 4525 |
. . . . . . . . . . . . 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 5133 |
. . . . . . . . . . 11
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑗 ∈ ℕ)
→ 0 ≤ (𝐹‘𝑗)) |
56 | 55 | adantlr 713 |
. . . . . . . . . 10
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
→ 0 ≤ (𝐹‘𝑗)) |
57 | 1, 29, 30, 45, 56 | climserle 15547 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹))) |
58 | 57 | ralrimiva 3143 |
. . . . . . . 8
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ∀𝑘 ∈
ℕ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹))) |
59 | | brralrspcev 5165 |
. . . . . . . 8
⊢ (((
⇝ ‘seq1( + , 𝐹)) ∈ ℝ ∧ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹))) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥) |
60 | 28, 58, 59 | syl2anc 584 |
. . . . . . 7
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ∃𝑥 ∈
ℝ ∀𝑘 ∈
ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥) |
61 | | ffn 6668 |
. . . . . . . . 9
⊢ (seq1( +
, 𝐹):ℕ⟶ℝ
→ seq1( + , 𝐹) Fn
ℕ) |
62 | | breq1 5108 |
. . . . . . . . . 10
⊢ (𝑧 = (seq1( + , 𝐹)‘𝑘) → (𝑧 ≤ 𝑥 ↔ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)) |
63 | 62 | ralrn 7038 |
. . . . . . . . 9
⊢ (seq1( +
, 𝐹) Fn ℕ →
(∀𝑧 ∈ ran seq1(
+ , 𝐹)𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)) |
64 | 12, 61, 63 | mp2b 10 |
. . . . . . . 8
⊢
(∀𝑧 ∈
ran seq1( + , 𝐹)𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥) |
65 | 64 | rexbii 3097 |
. . . . . . 7
⊢
(∃𝑥 ∈
ℝ ∀𝑧 ∈
ran seq1( + , 𝐹)𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥) |
66 | 60, 65 | sylibr 233 |
. . . . . 6
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ∃𝑥 ∈
ℝ ∀𝑧 ∈
ran seq1( + , 𝐹)𝑧 ≤ 𝑥) |
67 | 14, 22, 66 | suprcld 12118 |
. . . . 5
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ sup(ran seq1( + , 𝐹), ℝ, < ) ∈
ℝ) |
68 | | 2rp 12920 |
. . . . . 6
⊢ 2 ∈
ℝ+ |
69 | | rpreccl 12941 |
. . . . . 6
⊢ (2 ∈
ℝ+ → (1 / 2) ∈ ℝ+) |
70 | 68, 69 | ax-mp 5 |
. . . . 5
⊢ (1 / 2)
∈ ℝ+ |
71 | | ltsubrp 12951 |
. . . . 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 12367 |
. . . . . 6
⊢ (1 / 2)
∈ ℝ |
74 | | resubcl 11465 |
. . . . . 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 12119 |
. . . . 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 1373 |
. . . 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 5109 |
. . . . 5
⊢ (𝑦 = (seq1( + , 𝐹)‘𝑘) → ((sup(ran seq1( + , 𝐹), ℝ, < ) − (1 /
2)) < 𝑦 ↔ (sup(ran
seq1( + , 𝐹), ℝ, <
) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘))) |
80 | 79 | rexrn 7037 |
. . . 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 12227 |
. . . . . 6
⊢ 2 ∈
ℝ |
84 | | 2nn 12226 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
85 | | nnmulcl 12177 |
. . . . . . . . 9
⊢ ((2
∈ ℕ ∧ 𝑘
∈ ℕ) → (2 · 𝑘) ∈ ℕ) |
86 | 84, 29, 85 | sylancr 587 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2 · 𝑘)
∈ ℕ) |
87 | 86 | peano2nnd 12170 |
. . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2 · 𝑘) + 1)
∈ ℕ) |
88 | 87 | nnnn0d 12473 |
. . . . . 6
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2 · 𝑘) + 1)
∈ ℕ0) |
89 | | reexpcl 13984 |
. . . . . 6
⊢ ((2
∈ ℝ ∧ ((2 · 𝑘) + 1) ∈ ℕ0) →
(2↑((2 · 𝑘) +
1)) ∈ ℝ) |
90 | 83, 88, 89 | sylancr 587 |
. . . . 5
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑((2 · 𝑘) + 1)) ∈ ℝ) |
91 | 90 | ltnrd 11289 |
. . . 4
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ¬ (2↑((2 · 𝑘) + 1)) < (2↑((2 · 𝑘) + 1))) |
92 | 29 | adantr 481 |
. . . . . . 7
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → 𝑘 ∈ ℕ) |
93 | | peano2nn 12165 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℕ) |
94 | 93 | adantl 482 |
. . . . . . . . . . 11
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (𝑘 + 1) ∈
ℕ) |
95 | 94 | nnnn0d 12473 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (𝑘 + 1) ∈
ℕ0) |
96 | | nnexpcl 13980 |
. . . . . . . . . 10
⊢ ((2
∈ ℕ ∧ (𝑘 +
1) ∈ ℕ0) → (2↑(𝑘 + 1)) ∈ ℕ) |
97 | 84, 95, 96 | sylancr 587 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑(𝑘 + 1))
∈ ℕ) |
98 | 97 | nnsqcld 14147 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2↑(𝑘 +
1))↑2) ∈ ℕ) |
99 | 98 | adantr 481 |
. . . . . . 7
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → ((2↑(𝑘 + 1))↑2) ∈
ℕ) |
100 | | breq1 5108 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑤 → (𝑝 ∥ 𝑟 ↔ 𝑤 ∥ 𝑟)) |
101 | 100 | notbid 317 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑤 → (¬ 𝑝 ∥ 𝑟 ↔ ¬ 𝑤 ∥ 𝑟)) |
102 | 101 | cbvralvw 3225 |
. . . . . . . . 9
⊢
(∀𝑝 ∈
(ℙ ∖ (1...𝑘))
¬ 𝑝 ∥ 𝑟 ↔ ∀𝑤 ∈ (ℙ ∖
(1...𝑘)) ¬ 𝑤 ∥ 𝑟) |
103 | | breq2 5109 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑛 → (𝑤 ∥ 𝑟 ↔ 𝑤 ∥ 𝑛)) |
104 | 103 | notbid 317 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑛 → (¬ 𝑤 ∥ 𝑟 ↔ ¬ 𝑤 ∥ 𝑛)) |
105 | 104 | ralbidv 3174 |
. . . . . . . . 9
⊢ (𝑟 = 𝑛 → (∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑟 ↔ ∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑛)) |
106 | 102, 105 | bitrid 282 |
. . . . . . . 8
⊢ (𝑟 = 𝑛 → (∀𝑝 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑝 ∥ 𝑟 ↔ ∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑛)) |
107 | 106 | cbvrabv 3417 |
. . . . . . 7
⊢ {𝑟 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣
∀𝑝 ∈ (ℙ
∖ (1...𝑘)) ¬
𝑝 ∥ 𝑟} = {𝑛 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣ ∀𝑤 ∈ (ℙ ∖
(1...𝑘)) ¬ 𝑤 ∥ 𝑛} |
108 | | simpll 765 |
. . . . . . 7
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → seq1( + , 𝐹) ∈ dom ⇝
) |
109 | | eleq1w 2820 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑗 → (𝑚 ∈ ℙ ↔ 𝑗 ∈ ℙ)) |
110 | | oveq2 7365 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑗 → (1 / 𝑚) = (1 / 𝑗)) |
111 | 109, 110 | ifbieq1d 4510 |
. . . . . . . . 9
⊢ (𝑚 = 𝑗 → if(𝑚 ∈ ℙ, (1 / 𝑚), 0) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) |
112 | 111 | cbvsumv 15581 |
. . . . . . . 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 5140 |
. . . . . . 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 16792 |
. . . . . 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 2736 |
. . . . . . . . 9
⊢
(ℤ≥‘(𝑘 + 1)) = (ℤ≥‘(𝑘 + 1)) |
119 | 94 | nnzd 12526 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (𝑘 + 1) ∈
ℤ) |
120 | | eluznn 12843 |
. . . . . . . . . . 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 11169 |
. . . . . . . . . . . . 13
⊢ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈
ℂ |
127 | 126 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
→ if(𝑗 ∈ ℙ,
(1 / 𝑗), 0) ∈
ℂ) |
128 | 125, 127 | eqeltrd 2838 |
. . . . . . . . . . 11
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈ ℕ)
→ (𝐹‘𝑗) ∈
ℂ) |
129 | 1, 94, 128 | iserex 15541 |
. . . . . . . . . 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 15650 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ) |
132 | 73 | a1i 11 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (1 / 2) ∈ ℝ) |
133 | | elfznn 13470 |
. . . . . . . . . . . 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 2848 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ 𝑘 ∈
(ℤ≥‘1)) |
137 | 126 | a1i 11 |
. . . . . . . . . 10
⊢ (((seq1(
+ , 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
∧ 𝑗 ∈ (1...𝑘)) → if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℂ) |
138 | 135, 136,
137 | fsumser 15615 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ Σ𝑗 ∈
(1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = (seq1( + , 𝐹)‘𝑘)) |
139 | 138, 27 | eqeltrd 2838 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ Σ𝑗 ∈
(1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈
ℝ) |
140 | 131, 132,
139 | ltadd2d 11311 |
. . . . . . 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 15725 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0) =
(Σ𝑗 ∈
(1...((𝑘 + 1) −
1))if(𝑗 ∈ ℙ, (1
/ 𝑗), 0) + Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0))) |
142 | | nncn 12161 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) |
143 | 142 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ 𝑘 ∈
ℂ) |
144 | | ax-1cn 11109 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
145 | | pncan 11407 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑘 + 1)
− 1) = 𝑘) |
146 | 143, 144,
145 | sylancl 586 |
. . . . . . . . . . . 12
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((𝑘 + 1) − 1)
= 𝑘) |
147 | 146 | oveq2d 7373 |
. . . . . . . . . . 11
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (1...((𝑘 + 1)
− 1)) = (1...𝑘)) |
148 | 147 | sumeq1d 15586 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ Σ𝑗 ∈
(1...((𝑘 + 1) −
1))if(𝑗 ∈ ℙ, (1
/ 𝑗), 0) = Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) |
149 | 148 | oveq1d 7372 |
. . . . . . . . 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 5115 |
. . . . . . 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 2736 |
. . . . . . . . . 10
⊢ seq1( + ,
𝐹) = seq1( + , 𝐹) |
154 | 1, 153, 23, 42, 43, 54, 60 | isumsup 15732 |
. . . . . . . . 9
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0) =
sup(ran seq1( + , 𝐹),
ℝ, < )) |
155 | 154, 67 | eqeltrd 2838 |
. . . . . . . 8
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0) ∈
ℝ) |
156 | 155 | adantr 481 |
. . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0) ∈
ℝ) |
157 | 156, 132,
139 | ltsubaddd 11751 |
. . . . . 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 7372 |
. . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0)
− (1 / 2)) = (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 /
2))) |
160 | 159, 138 | breq12d 5118 |
. . . . . 6
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((Σ𝑗 ∈
ℕ if(𝑗 ∈
ℙ, (1 / 𝑗), 0)
− (1 / 2)) < Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ↔ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 /
2)) < (seq1( + , 𝐹)‘𝑘))) |
161 | 152, 157,
160 | 3bitr2d 306 |
. . . . 5
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (Σ𝑗 ∈
(ℤ≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2) ↔ (sup(ran seq1( + ,
𝐹), ℝ, < ) −
(1 / 2)) < (seq1( + , 𝐹)‘𝑘))) |
162 | | 2cn 12228 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℂ |
163 | 162 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ 2 ∈ ℂ) |
164 | 144 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ 1 ∈ ℂ) |
165 | 163, 143,
164 | adddid 11179 |
. . . . . . . . . . 11
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2 · (𝑘 + 1))
= ((2 · 𝑘) + (2
· 1))) |
166 | 94 | nncnd 12169 |
. . . . . . . . . . . 12
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (𝑘 + 1) ∈
ℂ) |
167 | | mulcom 11137 |
. . . . . . . . . . . 12
⊢ (((𝑘 + 1) ∈ ℂ ∧ 2
∈ ℂ) → ((𝑘
+ 1) · 2) = (2 · (𝑘 + 1))) |
168 | 166, 162,
167 | sylancl 586 |
. . . . . . . . . . 11
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((𝑘 + 1) · 2)
= (2 · (𝑘 +
1))) |
169 | 86 | nncnd 12169 |
. . . . . . . . . . . . 13
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2 · 𝑘)
∈ ℂ) |
170 | 169, 164,
164 | addassd 11177 |
. . . . . . . . . . . 12
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (((2 · 𝑘) +
1) + 1) = ((2 · 𝑘) +
(1 + 1))) |
171 | 144 | 2timesi 12291 |
. . . . . . . . . . . . 13
⊢ (2
· 1) = (1 + 1) |
172 | 171 | oveq2i 7368 |
. . . . . . . . . . . 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 7373 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑((𝑘 + 1)
· 2)) = (2↑(((2 · 𝑘) + 1) + 1))) |
176 | | 2nn0 12430 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ0 |
177 | 176 | a1i 11 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ 2 ∈ ℕ0) |
178 | 163, 177,
95 | expmuld 14054 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑((𝑘 + 1)
· 2)) = ((2↑(𝑘
+ 1))↑2)) |
179 | | expp1 13974 |
. . . . . . . . . 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 7372 |
. . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (((2↑(𝑘 +
1))↑2) / 2) = (((2↑((2 · 𝑘) + 1)) · 2) / 2)) |
183 | | expcl 13985 |
. . . . . . . . 9
⊢ ((2
∈ ℂ ∧ ((2 · 𝑘) + 1) ∈ ℕ0) →
(2↑((2 · 𝑘) +
1)) ∈ ℂ) |
184 | 162, 88, 183 | sylancr 587 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑((2 · 𝑘) + 1)) ∈ ℂ) |
185 | | 2ne0 12257 |
. . . . . . . . 9
⊢ 2 ≠
0 |
186 | | divcan4 11840 |
. . . . . . . . 9
⊢
(((2↑((2 · 𝑘) + 1)) ∈ ℂ ∧ 2 ∈ ℂ
∧ 2 ≠ 0) → (((2↑((2 · 𝑘) + 1)) · 2) / 2) = (2↑((2
· 𝑘) +
1))) |
187 | 162, 185,
186 | mp3an23 1453 |
. . . . . . . 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 12420 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
191 | 190 | adantl 482 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ 𝑘 ∈
ℕ0) |
192 | 163, 95, 191 | expaddd 14053 |
. . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑(𝑘 + (𝑘 + 1))) = ((2↑𝑘) · (2↑(𝑘 + 1)))) |
193 | 143 | 2timesd 12396 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2 · 𝑘) =
(𝑘 + 𝑘)) |
194 | 193 | oveq1d 7372 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2 · 𝑘) + 1)
= ((𝑘 + 𝑘) + 1)) |
195 | 143, 143,
164 | addassd 11177 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((𝑘 + 𝑘) + 1) = (𝑘 + (𝑘 + 1))) |
196 | 194, 195 | eqtrd 2776 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2 · 𝑘) + 1)
= (𝑘 + (𝑘 + 1))) |
197 | 196 | oveq2d 7373 |
. . . . . . 7
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑((2 · 𝑘) + 1)) = (2↑(𝑘 + (𝑘 + 1)))) |
198 | 97 | nnrpd 12955 |
. . . . . . . . . 10
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ (2↑(𝑘 + 1))
∈ ℝ+) |
199 | 198 | rprege0d 12964 |
. . . . . . . . 9
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((2↑(𝑘 + 1))
∈ ℝ ∧ 0 ≤ (2↑(𝑘 + 1)))) |
200 | | sqrtsq 15154 |
. . . . . . . . 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 7373 |
. . . . . . 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 5118 |
. . . . 5
⊢ ((seq1( +
, 𝐹) ∈ dom ⇝
∧ 𝑘 ∈ ℕ)
→ ((((2↑(𝑘 +
1))↑2) / 2) < ((2↑𝑘) · (√‘((2↑(𝑘 + 1))↑2))) ↔
(2↑((2 · 𝑘) +
1)) < (2↑((2 · 𝑘) + 1)))) |
205 | 117, 161,
204 | 3imtr3d 292 |
. . . 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 3146 |
. 2
⊢ (seq1( +
, 𝐹) ∈ dom ⇝
→ ¬ ∃𝑘
∈ ℕ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) <
(seq1( + , 𝐹)‘𝑘)) |
208 | 82, 207 | pm2.65i 193 |
1
⊢ ¬
seq1( + , 𝐹) ∈ dom
⇝ |