| Step | Hyp | Ref
| Expression |
| 1 | | bpos.3 |
. . . . . 6
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1)) |
| 2 | | id 22 |
. . . . . . . 8
⊢ (𝑛 ∈ ℙ → 𝑛 ∈
ℙ) |
| 3 | | 5nn 12352 |
. . . . . . . . . . 11
⊢ 5 ∈
ℕ |
| 4 | | bpos.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘5)) |
| 5 | | eluznn 12960 |
. . . . . . . . . . 11
⊢ ((5
∈ ℕ ∧ 𝑁
∈ (ℤ≥‘5)) → 𝑁 ∈ ℕ) |
| 6 | 3, 4, 5 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 7 | 6 | nnnn0d 12587 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 8 | | fzctr 13680 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈ (0...(2
· 𝑁))) |
| 9 | | bccl2 14362 |
. . . . . . . . 9
⊢ (𝑁 ∈ (0...(2 · 𝑁)) → ((2 · 𝑁)C𝑁) ∈ ℕ) |
| 10 | 7, 8, 9 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → ((2 · 𝑁)C𝑁) ∈ ℕ) |
| 11 | | pccl 16887 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℙ ∧ ((2
· 𝑁)C𝑁) ∈ ℕ) → (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈
ℕ0) |
| 12 | 2, 10, 11 | syl2anr 597 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈
ℕ0) |
| 13 | 12 | ralrimiva 3146 |
. . . . . 6
⊢ (𝜑 → ∀𝑛 ∈ ℙ (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈
ℕ0) |
| 14 | 1, 13 | pcmptcl 16929 |
. . . . 5
⊢ (𝜑 → (𝐹:ℕ⟶ℕ ∧ seq1( ·
, 𝐹):ℕ⟶ℕ)) |
| 15 | 14 | simprd 495 |
. . . 4
⊢ (𝜑 → seq1( · , 𝐹):ℕ⟶ℕ) |
| 16 | | 3nn 12345 |
. . . . 5
⊢ 3 ∈
ℕ |
| 17 | | bpos.5 |
. . . . . 6
⊢ 𝑀 =
(⌊‘(√‘(2 · 𝑁))) |
| 18 | | 2z 12649 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
| 19 | 6 | nnzd 12640 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 20 | | zmulcl 12666 |
. . . . . . . . . . 11
⊢ ((2
∈ ℤ ∧ 𝑁
∈ ℤ) → (2 · 𝑁) ∈ ℤ) |
| 21 | 18, 19, 20 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝜑 → (2 · 𝑁) ∈
ℤ) |
| 22 | 21 | zred 12722 |
. . . . . . . . 9
⊢ (𝜑 → (2 · 𝑁) ∈
ℝ) |
| 23 | | 2nn 12339 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ |
| 24 | | nnmulcl 12290 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℕ ∧ 𝑁
∈ ℕ) → (2 · 𝑁) ∈ ℕ) |
| 25 | 23, 6, 24 | sylancr 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 · 𝑁) ∈
ℕ) |
| 26 | 25 | nnrpd 13075 |
. . . . . . . . . 10
⊢ (𝜑 → (2 · 𝑁) ∈
ℝ+) |
| 27 | 26 | rpge0d 13081 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (2 · 𝑁)) |
| 28 | 22, 27 | resqrtcld 15456 |
. . . . . . . 8
⊢ (𝜑 → (√‘(2 ·
𝑁)) ∈
ℝ) |
| 29 | 28 | flcld 13838 |
. . . . . . 7
⊢ (𝜑 →
(⌊‘(√‘(2 · 𝑁))) ∈ ℤ) |
| 30 | | sqrt9 15312 |
. . . . . . . . 9
⊢
(√‘9) = 3 |
| 31 | | 9re 12365 |
. . . . . . . . . . . 12
⊢ 9 ∈
ℝ |
| 32 | 31 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 9 ∈
ℝ) |
| 33 | | 10re 12752 |
. . . . . . . . . . . 12
⊢ ;10 ∈ ℝ |
| 34 | 33 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → ;10 ∈ ℝ) |
| 35 | | lep1 12108 |
. . . . . . . . . . . . . 14
⊢ (9 ∈
ℝ → 9 ≤ (9 + 1)) |
| 36 | 31, 35 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ 9 ≤ (9
+ 1) |
| 37 | | 9p1e10 12735 |
. . . . . . . . . . . . 13
⊢ (9 + 1) =
;10 |
| 38 | 36, 37 | breqtri 5168 |
. . . . . . . . . . . 12
⊢ 9 ≤
;10 |
| 39 | 38 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 9 ≤ ;10) |
| 40 | | 5cn 12354 |
. . . . . . . . . . . . 13
⊢ 5 ∈
ℂ |
| 41 | | 2cn 12341 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℂ |
| 42 | | 5t2e10 12833 |
. . . . . . . . . . . . 13
⊢ (5
· 2) = ;10 |
| 43 | 40, 41, 42 | mulcomli 11270 |
. . . . . . . . . . . 12
⊢ (2
· 5) = ;10 |
| 44 | | eluzle 12891 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘5) → 5 ≤ 𝑁) |
| 45 | 4, 44 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 5 ≤ 𝑁) |
| 46 | 6 | nnred 12281 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℝ) |
| 47 | | 5re 12353 |
. . . . . . . . . . . . . . 15
⊢ 5 ∈
ℝ |
| 48 | | 2re 12340 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ |
| 49 | | 2pos 12369 |
. . . . . . . . . . . . . . . 16
⊢ 0 <
2 |
| 50 | 48, 49 | pm3.2i 470 |
. . . . . . . . . . . . . . 15
⊢ (2 ∈
ℝ ∧ 0 < 2) |
| 51 | | lemul2 12120 |
. . . . . . . . . . . . . . 15
⊢ ((5
∈ ℝ ∧ 𝑁
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (5 ≤ 𝑁 ↔ (2 · 5) ≤ (2
· 𝑁))) |
| 52 | 47, 50, 51 | mp3an13 1454 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℝ → (5 ≤
𝑁 ↔ (2 · 5)
≤ (2 · 𝑁))) |
| 53 | 46, 52 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (5 ≤ 𝑁 ↔ (2 · 5) ≤ (2 ·
𝑁))) |
| 54 | 45, 53 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2 · 5) ≤ (2
· 𝑁)) |
| 55 | 43, 54 | eqbrtrrid 5179 |
. . . . . . . . . . 11
⊢ (𝜑 → ;10 ≤ (2 · 𝑁)) |
| 56 | 32, 34, 22, 39, 55 | letrd 11418 |
. . . . . . . . . 10
⊢ (𝜑 → 9 ≤ (2 · 𝑁)) |
| 57 | | 0re 11263 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ |
| 58 | | 9pos 12379 |
. . . . . . . . . . . . 13
⊢ 0 <
9 |
| 59 | 57, 31, 58 | ltleii 11384 |
. . . . . . . . . . . 12
⊢ 0 ≤
9 |
| 60 | 31, 59 | pm3.2i 470 |
. . . . . . . . . . 11
⊢ (9 ∈
ℝ ∧ 0 ≤ 9) |
| 61 | 22, 27 | jca 511 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 · 𝑁) ∈ ℝ ∧ 0 ≤ (2
· 𝑁))) |
| 62 | | sqrtle 15299 |
. . . . . . . . . . 11
⊢ (((9
∈ ℝ ∧ 0 ≤ 9) ∧ ((2 · 𝑁) ∈ ℝ ∧ 0 ≤ (2 ·
𝑁))) → (9 ≤ (2
· 𝑁) ↔
(√‘9) ≤ (√‘(2 · 𝑁)))) |
| 63 | 60, 61, 62 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝜑 → (9 ≤ (2 · 𝑁) ↔ (√‘9) ≤
(√‘(2 · 𝑁)))) |
| 64 | 56, 63 | mpbid 232 |
. . . . . . . . 9
⊢ (𝜑 → (√‘9) ≤
(√‘(2 · 𝑁))) |
| 65 | 30, 64 | eqbrtrrid 5179 |
. . . . . . . 8
⊢ (𝜑 → 3 ≤ (√‘(2
· 𝑁))) |
| 66 | | 3z 12650 |
. . . . . . . . 9
⊢ 3 ∈
ℤ |
| 67 | | flge 13845 |
. . . . . . . . 9
⊢
(((√‘(2 · 𝑁)) ∈ ℝ ∧ 3 ∈ ℤ)
→ (3 ≤ (√‘(2 · 𝑁)) ↔ 3 ≤
(⌊‘(√‘(2 · 𝑁))))) |
| 68 | 28, 66, 67 | sylancl 586 |
. . . . . . . 8
⊢ (𝜑 → (3 ≤ (√‘(2
· 𝑁)) ↔ 3 ≤
(⌊‘(√‘(2 · 𝑁))))) |
| 69 | 65, 68 | mpbid 232 |
. . . . . . 7
⊢ (𝜑 → 3 ≤
(⌊‘(√‘(2 · 𝑁)))) |
| 70 | 66 | eluz1i 12886 |
. . . . . . 7
⊢
((⌊‘(√‘(2 · 𝑁))) ∈ (ℤ≥‘3)
↔ ((⌊‘(√‘(2 · 𝑁))) ∈ ℤ ∧ 3 ≤
(⌊‘(√‘(2 · 𝑁))))) |
| 71 | 29, 69, 70 | sylanbrc 583 |
. . . . . 6
⊢ (𝜑 →
(⌊‘(√‘(2 · 𝑁))) ∈
(ℤ≥‘3)) |
| 72 | 17, 71 | eqeltrid 2845 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘3)) |
| 73 | | eluznn 12960 |
. . . . 5
⊢ ((3
∈ ℕ ∧ 𝑀
∈ (ℤ≥‘3)) → 𝑀 ∈ ℕ) |
| 74 | 16, 72, 73 | sylancr 587 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 75 | 15, 74 | ffvelcdmd 7105 |
. . 3
⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℕ) |
| 76 | 75 | nnred 12281 |
. 2
⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℝ) |
| 77 | 74 | nnred 12281 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℝ) |
| 78 | | ppicl 27174 |
. . . . 5
⊢ (𝑀 ∈ ℝ →
(π‘𝑀)
∈ ℕ0) |
| 79 | 77, 78 | syl 17 |
. . . 4
⊢ (𝜑 → (π‘𝑀) ∈
ℕ0) |
| 80 | 25, 79 | nnexpcld 14284 |
. . 3
⊢ (𝜑 → ((2 · 𝑁)↑(π‘𝑀)) ∈
ℕ) |
| 81 | 80 | nnred 12281 |
. 2
⊢ (𝜑 → ((2 · 𝑁)↑(π‘𝑀)) ∈
ℝ) |
| 82 | | nndivre 12307 |
. . . . 5
⊢
(((√‘(2 · 𝑁)) ∈ ℝ ∧ 3 ∈ ℕ)
→ ((√‘(2 · 𝑁)) / 3) ∈ ℝ) |
| 83 | 28, 16, 82 | sylancl 586 |
. . . 4
⊢ (𝜑 → ((√‘(2
· 𝑁)) / 3) ∈
ℝ) |
| 84 | | readdcl 11238 |
. . . 4
⊢
((((√‘(2 · 𝑁)) / 3) ∈ ℝ ∧ 2 ∈
ℝ) → (((√‘(2 · 𝑁)) / 3) + 2) ∈
ℝ) |
| 85 | 83, 48, 84 | sylancl 586 |
. . 3
⊢ (𝜑 → (((√‘(2
· 𝑁)) / 3) + 2)
∈ ℝ) |
| 86 | 22, 27, 85 | recxpcld 26765 |
. 2
⊢ (𝜑 → ((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
∈ ℝ) |
| 87 | | fveq2 6906 |
. . . . . 6
⊢ (𝑥 = 1 → (seq1( · ,
𝐹)‘𝑥) = (seq1( · , 𝐹)‘1)) |
| 88 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑥 = 1 →
(π‘𝑥) =
(π‘1)) |
| 89 | | ppi1 27207 |
. . . . . . . 8
⊢
(π‘1) = 0 |
| 90 | 88, 89 | eqtrdi 2793 |
. . . . . . 7
⊢ (𝑥 = 1 →
(π‘𝑥) =
0) |
| 91 | 90 | oveq2d 7447 |
. . . . . 6
⊢ (𝑥 = 1 → ((2 · 𝑁)↑(π‘𝑥)) = ((2 · 𝑁)↑0)) |
| 92 | 87, 91 | breq12d 5156 |
. . . . 5
⊢ (𝑥 = 1 → ((seq1( · ,
𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π‘𝑥)) ↔ (seq1( · , 𝐹)‘1) ≤ ((2 · 𝑁)↑0))) |
| 93 | 92 | imbi2d 340 |
. . . 4
⊢ (𝑥 = 1 → ((𝜑 → (seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π‘𝑥))) ↔ (𝜑 → (seq1( · , 𝐹)‘1) ≤ ((2 · 𝑁)↑0)))) |
| 94 | | fveq2 6906 |
. . . . . 6
⊢ (𝑥 = 𝑘 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑘)) |
| 95 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → (π‘𝑥) = (π‘𝑘)) |
| 96 | 95 | oveq2d 7447 |
. . . . . 6
⊢ (𝑥 = 𝑘 → ((2 · 𝑁)↑(π‘𝑥)) = ((2 · 𝑁)↑(π‘𝑘))) |
| 97 | 94, 96 | breq12d 5156 |
. . . . 5
⊢ (𝑥 = 𝑘 → ((seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π‘𝑥)) ↔ (seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π‘𝑘)))) |
| 98 | 97 | imbi2d 340 |
. . . 4
⊢ (𝑥 = 𝑘 → ((𝜑 → (seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π‘𝑥))) ↔ (𝜑 → (seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π‘𝑘))))) |
| 99 | | fveq2 6906 |
. . . . . 6
⊢ (𝑥 = (𝑘 + 1) → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘(𝑘 + 1))) |
| 100 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑥 = (𝑘 + 1) → (π‘𝑥) = (π‘(𝑘 + 1))) |
| 101 | 100 | oveq2d 7447 |
. . . . . 6
⊢ (𝑥 = (𝑘 + 1) → ((2 · 𝑁)↑(π‘𝑥)) = ((2 · 𝑁)↑(π‘(𝑘 + 1)))) |
| 102 | 99, 101 | breq12d 5156 |
. . . . 5
⊢ (𝑥 = (𝑘 + 1) → ((seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π‘𝑥)) ↔ (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1))))) |
| 103 | 102 | imbi2d 340 |
. . . 4
⊢ (𝑥 = (𝑘 + 1) → ((𝜑 → (seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π‘𝑥))) ↔ (𝜑 → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))))) |
| 104 | | fveq2 6906 |
. . . . . 6
⊢ (𝑥 = 𝑀 → (seq1( · , 𝐹)‘𝑥) = (seq1( · , 𝐹)‘𝑀)) |
| 105 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑥 = 𝑀 → (π‘𝑥) = (π‘𝑀)) |
| 106 | 105 | oveq2d 7447 |
. . . . . 6
⊢ (𝑥 = 𝑀 → ((2 · 𝑁)↑(π‘𝑥)) = ((2 · 𝑁)↑(π‘𝑀))) |
| 107 | 104, 106 | breq12d 5156 |
. . . . 5
⊢ (𝑥 = 𝑀 → ((seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π‘𝑥)) ↔ (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑(π‘𝑀)))) |
| 108 | 107 | imbi2d 340 |
. . . 4
⊢ (𝑥 = 𝑀 → ((𝜑 → (seq1( · , 𝐹)‘𝑥) ≤ ((2 · 𝑁)↑(π‘𝑥))) ↔ (𝜑 → (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑(π‘𝑀))))) |
| 109 | | 1z 12647 |
. . . . . . . 8
⊢ 1 ∈
ℤ |
| 110 | | seq1 14055 |
. . . . . . . 8
⊢ (1 ∈
ℤ → (seq1( · , 𝐹)‘1) = (𝐹‘1)) |
| 111 | 109, 110 | ax-mp 5 |
. . . . . . 7
⊢ (seq1(
· , 𝐹)‘1) =
(𝐹‘1) |
| 112 | | 1nn 12277 |
. . . . . . . 8
⊢ 1 ∈
ℕ |
| 113 | | 1nprm 16716 |
. . . . . . . . . . 11
⊢ ¬ 1
∈ ℙ |
| 114 | | eleq1 2829 |
. . . . . . . . . . 11
⊢ (𝑛 = 1 → (𝑛 ∈ ℙ ↔ 1 ∈
ℙ)) |
| 115 | 113, 114 | mtbiri 327 |
. . . . . . . . . 10
⊢ (𝑛 = 1 → ¬ 𝑛 ∈
ℙ) |
| 116 | 115 | iffalsed 4536 |
. . . . . . . . 9
⊢ (𝑛 = 1 → if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1) = 1) |
| 117 | | 1ex 11257 |
. . . . . . . . 9
⊢ 1 ∈
V |
| 118 | 116, 1, 117 | fvmpt 7016 |
. . . . . . . 8
⊢ (1 ∈
ℕ → (𝐹‘1)
= 1) |
| 119 | 112, 118 | ax-mp 5 |
. . . . . . 7
⊢ (𝐹‘1) = 1 |
| 120 | 111, 119 | eqtri 2765 |
. . . . . 6
⊢ (seq1(
· , 𝐹)‘1) =
1 |
| 121 | | 1le1 11891 |
. . . . . 6
⊢ 1 ≤
1 |
| 122 | 120, 121 | eqbrtri 5164 |
. . . . 5
⊢ (seq1(
· , 𝐹)‘1) ≤
1 |
| 123 | 21 | zcnd 12723 |
. . . . . 6
⊢ (𝜑 → (2 · 𝑁) ∈
ℂ) |
| 124 | 123 | exp0d 14180 |
. . . . 5
⊢ (𝜑 → ((2 · 𝑁)↑0) = 1) |
| 125 | 122, 124 | breqtrrid 5181 |
. . . 4
⊢ (𝜑 → (seq1( · , 𝐹)‘1) ≤ ((2 ·
𝑁)↑0)) |
| 126 | 15 | ffvelcdmda 7104 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( · ,
𝐹)‘𝑘) ∈ ℕ) |
| 127 | 126 | nnred 12281 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( · ,
𝐹)‘𝑘) ∈ ℝ) |
| 128 | 127 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (seq1( ·
, 𝐹)‘𝑘) ∈
ℝ) |
| 129 | 25 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (2 ·
𝑁) ∈
ℕ) |
| 130 | | nnre 12273 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ) |
| 131 | 130 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → 𝑘 ∈
ℝ) |
| 132 | | ppicl 27174 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℝ →
(π‘𝑘)
∈ ℕ0) |
| 133 | 131, 132 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) →
(π‘𝑘)
∈ ℕ0) |
| 134 | 129, 133 | nnexpcld 14284 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((2 ·
𝑁)↑(π‘𝑘)) ∈ ℕ) |
| 135 | 134 | nnred 12281 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((2 ·
𝑁)↑(π‘𝑘)) ∈ ℝ) |
| 136 | | nnre 12273 |
. . . . . . . . . . . . 13
⊢ ((2
· 𝑁) ∈ ℕ
→ (2 · 𝑁)
∈ ℝ) |
| 137 | | nngt0 12297 |
. . . . . . . . . . . . 13
⊢ ((2
· 𝑁) ∈ ℕ
→ 0 < (2 · 𝑁)) |
| 138 | 136, 137 | jca 511 |
. . . . . . . . . . . 12
⊢ ((2
· 𝑁) ∈ ℕ
→ ((2 · 𝑁)
∈ ℝ ∧ 0 < (2 · 𝑁))) |
| 139 | 25, 138 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 · 𝑁) ∈ ℝ ∧ 0 < (2
· 𝑁))) |
| 140 | 139 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((2 ·
𝑁) ∈ ℝ ∧ 0
< (2 · 𝑁))) |
| 141 | | lemul1 12119 |
. . . . . . . . . 10
⊢ (((seq1(
· , 𝐹)‘𝑘) ∈ ℝ ∧ ((2
· 𝑁)↑(π‘𝑘)) ∈ ℝ ∧ ((2 · 𝑁) ∈ ℝ ∧ 0 < (2
· 𝑁))) →
((seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π‘𝑘)) ↔ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ (((2 · 𝑁)↑(π‘𝑘)) · (2 · 𝑁)))) |
| 142 | 128, 135,
140, 141 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((seq1( ·
, 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π‘𝑘)) ↔ ((seq1( · ,
𝐹)‘𝑘) · (2 · 𝑁)) ≤ (((2 · 𝑁)↑(π‘𝑘)) · (2 · 𝑁)))) |
| 143 | | nnz 12634 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℤ) |
| 144 | 143 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ) |
| 145 | | ppiprm 27194 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℤ ∧ (𝑘 + 1) ∈ ℙ) →
(π‘(𝑘 + 1))
= ((π‘𝑘) +
1)) |
| 146 | 144, 145 | sylan 580 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) →
(π‘(𝑘 + 1))
= ((π‘𝑘) +
1)) |
| 147 | 146 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((2 ·
𝑁)↑(π‘(𝑘 + 1))) = ((2 · 𝑁)↑((π‘𝑘) + 1))) |
| 148 | 123 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (2 ·
𝑁) ∈
ℂ) |
| 149 | 148, 133 | expp1d 14187 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((2 ·
𝑁)↑((π‘𝑘) + 1)) = (((2 · 𝑁)↑(π‘𝑘)) · (2 · 𝑁))) |
| 150 | 147, 149 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((2 ·
𝑁)↑(π‘(𝑘 + 1))) = (((2 · 𝑁)↑(π‘𝑘)) · (2 · 𝑁))) |
| 151 | 150 | breq2d 5155 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (((seq1(
· , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1))) ↔ ((seq1( ·
, 𝐹)‘𝑘) · (2 · 𝑁)) ≤ (((2 · 𝑁)↑(π‘𝑘)) · (2 · 𝑁)))) |
| 152 | 142, 151 | bitr4d 282 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((seq1( ·
, 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π‘𝑘)) ↔ ((seq1( · ,
𝐹)‘𝑘) · (2 · 𝑁)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1))))) |
| 153 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) |
| 154 | | nnuz 12921 |
. . . . . . . . . . . . 13
⊢ ℕ =
(ℤ≥‘1) |
| 155 | 153, 154 | eleqtrdi 2851 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈
(ℤ≥‘1)) |
| 156 | | seqp1 14057 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈
(ℤ≥‘1) → (seq1( · , 𝐹)‘(𝑘 + 1)) = ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1)))) |
| 157 | 155, 156 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( · ,
𝐹)‘(𝑘 + 1)) = ((seq1( · ,
𝐹)‘𝑘) · (𝐹‘(𝑘 + 1)))) |
| 158 | 157 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (seq1( ·
, 𝐹)‘(𝑘 + 1)) = ((seq1( · ,
𝐹)‘𝑘) · (𝐹‘(𝑘 + 1)))) |
| 159 | | peano2nn 12278 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℕ) |
| 160 | 159 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ) |
| 161 | | eleq1 2829 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (𝑘 + 1) → (𝑛 ∈ ℙ ↔ (𝑘 + 1) ∈ ℙ)) |
| 162 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = (𝑘 + 1) → 𝑛 = (𝑘 + 1)) |
| 163 | | oveq1 7438 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = (𝑘 + 1) → (𝑛 pCnt ((2 · 𝑁)C𝑁)) = ((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))) |
| 164 | 162, 163 | oveq12d 7449 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (𝑘 + 1) → (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))) = ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁)))) |
| 165 | 161, 164 | ifbieq1d 4550 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (𝑘 + 1) → if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1) = if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))), 1)) |
| 166 | | ovex 7464 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))) ∈ V |
| 167 | 166, 117 | ifex 4576 |
. . . . . . . . . . . . . . 15
⊢ if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))), 1) ∈ V |
| 168 | 165, 1, 167 | fvmpt 7016 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 + 1) ∈ ℕ →
(𝐹‘(𝑘 + 1)) = if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))), 1)) |
| 169 | 160, 168 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) = if((𝑘 + 1) ∈ ℙ, ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))), 1)) |
| 170 | | iftrue 4531 |
. . . . . . . . . . . . 13
⊢ ((𝑘 + 1) ∈ ℙ →
if((𝑘 + 1) ∈ ℙ,
((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))), 1) = ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁)))) |
| 171 | 169, 170 | sylan9eq 2797 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (𝐹‘(𝑘 + 1)) = ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁)))) |
| 172 | 6 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑁 ∈ ℕ) |
| 173 | | bposlem1 27328 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ (𝑘 + 1) ∈ ℙ) →
((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁)) |
| 174 | 172, 173 | sylan 580 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((𝑘 + 1)↑((𝑘 + 1) pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁)) |
| 175 | 171, 174 | eqbrtrd 5165 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (𝐹‘(𝑘 + 1)) ≤ (2 · 𝑁)) |
| 176 | 14 | simpld 494 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹:ℕ⟶ℕ) |
| 177 | | ffvelcdm 7101 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:ℕ⟶ℕ ∧
(𝑘 + 1) ∈ ℕ)
→ (𝐹‘(𝑘 + 1)) ∈
ℕ) |
| 178 | 176, 159,
177 | syl2an 596 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ∈ ℕ) |
| 179 | 178 | nnred 12281 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(𝑘 + 1)) ∈ ℝ) |
| 180 | 179 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (𝐹‘(𝑘 + 1)) ∈ ℝ) |
| 181 | 22 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (2 ·
𝑁) ∈
ℝ) |
| 182 | | nnre 12273 |
. . . . . . . . . . . . . . 15
⊢ ((seq1(
· , 𝐹)‘𝑘) ∈ ℕ → (seq1(
· , 𝐹)‘𝑘) ∈
ℝ) |
| 183 | | nngt0 12297 |
. . . . . . . . . . . . . . 15
⊢ ((seq1(
· , 𝐹)‘𝑘) ∈ ℕ → 0 <
(seq1( · , 𝐹)‘𝑘)) |
| 184 | 182, 183 | jca 511 |
. . . . . . . . . . . . . 14
⊢ ((seq1(
· , 𝐹)‘𝑘) ∈ ℕ → ((seq1(
· , 𝐹)‘𝑘) ∈ ℝ ∧ 0 <
(seq1( · , 𝐹)‘𝑘))) |
| 185 | 126, 184 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((seq1( · ,
𝐹)‘𝑘) ∈ ℝ ∧ 0 < (seq1( ·
, 𝐹)‘𝑘))) |
| 186 | 185 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((seq1( ·
, 𝐹)‘𝑘) ∈ ℝ ∧ 0 <
(seq1( · , 𝐹)‘𝑘))) |
| 187 | | lemul2 12120 |
. . . . . . . . . . . 12
⊢ (((𝐹‘(𝑘 + 1)) ∈ ℝ ∧ (2 · 𝑁) ∈ ℝ ∧ ((seq1(
· , 𝐹)‘𝑘) ∈ ℝ ∧ 0 <
(seq1( · , 𝐹)‘𝑘))) → ((𝐹‘(𝑘 + 1)) ≤ (2 · 𝑁) ↔ ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1))) ≤ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)))) |
| 188 | 180, 181,
186, 187 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((𝐹‘(𝑘 + 1)) ≤ (2 · 𝑁) ↔ ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1))) ≤ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)))) |
| 189 | 175, 188 | mpbid 232 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((seq1( ·
, 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1))) ≤ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁))) |
| 190 | 158, 189 | eqbrtrd 5165 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (seq1( ·
, 𝐹)‘(𝑘 + 1)) ≤ ((seq1( · ,
𝐹)‘𝑘) · (2 · 𝑁))) |
| 191 | | ffvelcdm 7101 |
. . . . . . . . . . . . 13
⊢ ((seq1(
· , 𝐹):ℕ⟶ℕ ∧ (𝑘 + 1) ∈ ℕ) →
(seq1( · , 𝐹)‘(𝑘 + 1)) ∈ ℕ) |
| 192 | 15, 159, 191 | syl2an 596 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( · ,
𝐹)‘(𝑘 + 1)) ∈
ℕ) |
| 193 | 192 | nnred 12281 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( · ,
𝐹)‘(𝑘 + 1)) ∈
ℝ) |
| 194 | 25 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 · 𝑁) ∈
ℕ) |
| 195 | 126, 194 | nnmulcld 12319 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((seq1( · ,
𝐹)‘𝑘) · (2 · 𝑁)) ∈ ℕ) |
| 196 | 195 | nnred 12281 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((seq1( · ,
𝐹)‘𝑘) · (2 · 𝑁)) ∈ ℝ) |
| 197 | 160 | nnred 12281 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℝ) |
| 198 | | ppicl 27174 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 + 1) ∈ ℝ →
(π‘(𝑘 + 1))
∈ ℕ0) |
| 199 | 197, 198 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
(π‘(𝑘 + 1))
∈ ℕ0) |
| 200 | 194, 199 | nnexpcld 14284 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑁)↑(π‘(𝑘 + 1))) ∈
ℕ) |
| 201 | 200 | nnred 12281 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((2 · 𝑁)↑(π‘(𝑘 + 1))) ∈
ℝ) |
| 202 | | letr 11355 |
. . . . . . . . . . 11
⊢ (((seq1(
· , 𝐹)‘(𝑘 + 1)) ∈ ℝ ∧
((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ∈ ℝ ∧ ((2 · 𝑁)↑(π‘(𝑘 + 1))) ∈ ℝ) →
(((seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ∧ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))) → (seq1( ·
, 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1))))) |
| 203 | 193, 196,
201, 202 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((seq1( · ,
𝐹)‘(𝑘 + 1)) ≤ ((seq1( · ,
𝐹)‘𝑘) · (2 · 𝑁)) ∧ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))) → (seq1( ·
, 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1))))) |
| 204 | 203 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (((seq1(
· , 𝐹)‘(𝑘 + 1)) ≤ ((seq1( · ,
𝐹)‘𝑘) · (2 · 𝑁)) ∧ ((seq1( · , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))) → (seq1( ·
, 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1))))) |
| 205 | 190, 204 | mpand 695 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → (((seq1(
· , 𝐹)‘𝑘) · (2 · 𝑁)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1))) → (seq1( · ,
𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1))))) |
| 206 | 152, 205 | sylbid 240 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑘 + 1) ∈ ℙ) → ((seq1( ·
, 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π‘𝑘)) → (seq1( · ,
𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1))))) |
| 207 | 157 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) →
(seq1( · , 𝐹)‘(𝑘 + 1)) = ((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1)))) |
| 208 | | iffalse 4534 |
. . . . . . . . . . . 12
⊢ (¬
(𝑘 + 1) ∈ ℙ
→ if((𝑘 + 1) ∈
ℙ, ((𝑘 +
1)↑((𝑘 + 1) pCnt ((2
· 𝑁)C𝑁))), 1) = 1) |
| 209 | 169, 208 | sylan9eq 2797 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) →
(𝐹‘(𝑘 + 1)) = 1) |
| 210 | 209 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) →
((seq1( · , 𝐹)‘𝑘) · (𝐹‘(𝑘 + 1))) = ((seq1( · , 𝐹)‘𝑘) · 1)) |
| 211 | 126 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) →
(seq1( · , 𝐹)‘𝑘) ∈ ℕ) |
| 212 | 211 | nncnd 12282 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) →
(seq1( · , 𝐹)‘𝑘) ∈ ℂ) |
| 213 | 212 | mulridd 11278 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) →
((seq1( · , 𝐹)‘𝑘) · 1) = (seq1( · , 𝐹)‘𝑘)) |
| 214 | 207, 210,
213 | 3eqtrd 2781 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) →
(seq1( · , 𝐹)‘(𝑘 + 1)) = (seq1( · , 𝐹)‘𝑘)) |
| 215 | | ppinprm 27195 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℤ ∧ ¬
(𝑘 + 1) ∈ ℙ)
→ (π‘(𝑘 + 1)) = (π‘𝑘)) |
| 216 | 144, 215 | sylan 580 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) →
(π‘(𝑘 + 1))
= (π‘𝑘)) |
| 217 | 216 | oveq2d 7447 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) → ((2
· 𝑁)↑(π‘(𝑘 + 1))) = ((2 · 𝑁)↑(π‘𝑘))) |
| 218 | 214, 217 | breq12d 5156 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) →
((seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1))) ↔ (seq1( · ,
𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π‘𝑘)))) |
| 219 | 218 | biimprd 248 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ ¬ (𝑘 + 1) ∈ ℙ) →
((seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π‘𝑘)) → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1))))) |
| 220 | 206, 219 | pm2.61dan 813 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((seq1( · ,
𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π‘𝑘)) → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1))))) |
| 221 | 220 | expcom 413 |
. . . . 5
⊢ (𝑘 ∈ ℕ → (𝜑 → ((seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π‘𝑘)) → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))))) |
| 222 | 221 | a2d 29 |
. . . 4
⊢ (𝑘 ∈ ℕ → ((𝜑 → (seq1( · , 𝐹)‘𝑘) ≤ ((2 · 𝑁)↑(π‘𝑘))) → (𝜑 → (seq1( · , 𝐹)‘(𝑘 + 1)) ≤ ((2 · 𝑁)↑(π‘(𝑘 + 1)))))) |
| 223 | 93, 98, 103, 108, 125, 222 | nnind 12284 |
. . 3
⊢ (𝑀 ∈ ℕ → (𝜑 → (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑(π‘𝑀)))) |
| 224 | 74, 223 | mpcom 38 |
. 2
⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑(π‘𝑀))) |
| 225 | | cxpexp 26710 |
. . . 4
⊢ (((2
· 𝑁) ∈ ℂ
∧ (π‘𝑀)
∈ ℕ0) → ((2 · 𝑁)↑𝑐(π‘𝑀)) = ((2 · 𝑁)↑(π‘𝑀))) |
| 226 | 123, 79, 225 | syl2anc 584 |
. . 3
⊢ (𝜑 → ((2 · 𝑁)↑𝑐(π‘𝑀)) = ((2 · 𝑁)↑(π‘𝑀))) |
| 227 | 79 | nn0red 12588 |
. . . . 5
⊢ (𝜑 → (π‘𝑀) ∈
ℝ) |
| 228 | | nndivre 12307 |
. . . . . . 7
⊢ ((𝑀 ∈ ℝ ∧ 3 ∈
ℕ) → (𝑀 / 3)
∈ ℝ) |
| 229 | 77, 16, 228 | sylancl 586 |
. . . . . 6
⊢ (𝜑 → (𝑀 / 3) ∈ ℝ) |
| 230 | | readdcl 11238 |
. . . . . 6
⊢ (((𝑀 / 3) ∈ ℝ ∧ 2
∈ ℝ) → ((𝑀
/ 3) + 2) ∈ ℝ) |
| 231 | 229, 48, 230 | sylancl 586 |
. . . . 5
⊢ (𝜑 → ((𝑀 / 3) + 2) ∈ ℝ) |
| 232 | 74 | nnnn0d 12587 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
| 233 | 232 | nn0ge0d 12590 |
. . . . . 6
⊢ (𝜑 → 0 ≤ 𝑀) |
| 234 | | ppiub 27248 |
. . . . . 6
⊢ ((𝑀 ∈ ℝ ∧ 0 ≤
𝑀) →
(π‘𝑀) ≤
((𝑀 / 3) +
2)) |
| 235 | 77, 233, 234 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (π‘𝑀) ≤ ((𝑀 / 3) + 2)) |
| 236 | 48 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 2 ∈
ℝ) |
| 237 | | flle 13839 |
. . . . . . . . 9
⊢
((√‘(2 · 𝑁)) ∈ ℝ →
(⌊‘(√‘(2 · 𝑁))) ≤ (√‘(2 · 𝑁))) |
| 238 | 28, 237 | syl 17 |
. . . . . . . 8
⊢ (𝜑 →
(⌊‘(√‘(2 · 𝑁))) ≤ (√‘(2 · 𝑁))) |
| 239 | 17, 238 | eqbrtrid 5178 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ≤ (√‘(2 · 𝑁))) |
| 240 | | 3re 12346 |
. . . . . . . . . 10
⊢ 3 ∈
ℝ |
| 241 | | 3pos 12371 |
. . . . . . . . . 10
⊢ 0 <
3 |
| 242 | 240, 241 | pm3.2i 470 |
. . . . . . . . 9
⊢ (3 ∈
ℝ ∧ 0 < 3) |
| 243 | 242 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (3 ∈ ℝ ∧ 0
< 3)) |
| 244 | | lediv1 12133 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℝ ∧
(√‘(2 · 𝑁)) ∈ ℝ ∧ (3 ∈ ℝ
∧ 0 < 3)) → (𝑀
≤ (√‘(2 · 𝑁)) ↔ (𝑀 / 3) ≤ ((√‘(2 · 𝑁)) / 3))) |
| 245 | 77, 28, 243, 244 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → (𝑀 ≤ (√‘(2 · 𝑁)) ↔ (𝑀 / 3) ≤ ((√‘(2 · 𝑁)) / 3))) |
| 246 | 239, 245 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → (𝑀 / 3) ≤ ((√‘(2 · 𝑁)) / 3)) |
| 247 | 229, 83, 236, 246 | leadd1dd 11877 |
. . . . 5
⊢ (𝜑 → ((𝑀 / 3) + 2) ≤ (((√‘(2 ·
𝑁)) / 3) +
2)) |
| 248 | 227, 231,
85, 235, 247 | letrd 11418 |
. . . 4
⊢ (𝜑 → (π‘𝑀) ≤ (((√‘(2
· 𝑁)) / 3) +
2)) |
| 249 | | 2t1e2 12429 |
. . . . . . . 8
⊢ (2
· 1) = 2 |
| 250 | 6 | nnge1d 12314 |
. . . . . . . . 9
⊢ (𝜑 → 1 ≤ 𝑁) |
| 251 | | 1re 11261 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
| 252 | | lemul2 12120 |
. . . . . . . . . . 11
⊢ ((1
∈ ℝ ∧ 𝑁
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (1 ≤ 𝑁 ↔ (2 · 1) ≤ (2
· 𝑁))) |
| 253 | 251, 50, 252 | mp3an13 1454 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℝ → (1 ≤
𝑁 ↔ (2 · 1)
≤ (2 · 𝑁))) |
| 254 | 46, 253 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (1 ≤ 𝑁 ↔ (2 · 1) ≤ (2 ·
𝑁))) |
| 255 | 250, 254 | mpbid 232 |
. . . . . . . 8
⊢ (𝜑 → (2 · 1) ≤ (2
· 𝑁)) |
| 256 | 249, 255 | eqbrtrrid 5179 |
. . . . . . 7
⊢ (𝜑 → 2 ≤ (2 · 𝑁)) |
| 257 | 18 | eluz1i 12886 |
. . . . . . 7
⊢ ((2
· 𝑁) ∈
(ℤ≥‘2) ↔ ((2 · 𝑁) ∈ ℤ ∧ 2 ≤ (2 ·
𝑁))) |
| 258 | 21, 256, 257 | sylanbrc 583 |
. . . . . 6
⊢ (𝜑 → (2 · 𝑁) ∈
(ℤ≥‘2)) |
| 259 | | eluz2gt1 12962 |
. . . . . 6
⊢ ((2
· 𝑁) ∈
(ℤ≥‘2) → 1 < (2 · 𝑁)) |
| 260 | 258, 259 | syl 17 |
. . . . 5
⊢ (𝜑 → 1 < (2 · 𝑁)) |
| 261 | 22, 260, 227, 85 | cxpled 26762 |
. . . 4
⊢ (𝜑 → ((π‘𝑀) ≤ (((√‘(2
· 𝑁)) / 3) + 2)
↔ ((2 · 𝑁)↑𝑐(π‘𝑀)) ≤ ((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) +
2)))) |
| 262 | 248, 261 | mpbid 232 |
. . 3
⊢ (𝜑 → ((2 · 𝑁)↑𝑐(π‘𝑀)) ≤ ((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) +
2))) |
| 263 | 226, 262 | eqbrtrrd 5167 |
. 2
⊢ (𝜑 → ((2 · 𝑁)↑(π‘𝑀)) ≤ ((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) +
2))) |
| 264 | 76, 81, 86, 224, 263 | letrd 11418 |
1
⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) +
2))) |