Proof of Theorem bposlem6
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 4nn 12350 | . . . . 5
⊢ 4 ∈
ℕ | 
| 2 |  | 5nn 12353 | . . . . . . 7
⊢ 5 ∈
ℕ | 
| 3 |  | bpos.1 | . . . . . . 7
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘5)) | 
| 4 |  | eluznn 12961 | . . . . . . 7
⊢ ((5
∈ ℕ ∧ 𝑁
∈ (ℤ≥‘5)) → 𝑁 ∈ ℕ) | 
| 5 | 2, 3, 4 | sylancr 587 | . . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 6 | 5 | nnnn0d 12589 | . . . . 5
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 7 |  | nnexpcl 14116 | . . . . 5
⊢ ((4
∈ ℕ ∧ 𝑁
∈ ℕ0) → (4↑𝑁) ∈ ℕ) | 
| 8 | 1, 6, 7 | sylancr 587 | . . . 4
⊢ (𝜑 → (4↑𝑁) ∈ ℕ) | 
| 9 | 8 | nnred 12282 | . . 3
⊢ (𝜑 → (4↑𝑁) ∈ ℝ) | 
| 10 | 9, 5 | nndivred 12321 | . 2
⊢ (𝜑 → ((4↑𝑁) / 𝑁) ∈ ℝ) | 
| 11 |  | fzctr 13681 | . . . . 5
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈ (0...(2
· 𝑁))) | 
| 12 | 6, 11 | syl 17 | . . . 4
⊢ (𝜑 → 𝑁 ∈ (0...(2 · 𝑁))) | 
| 13 |  | bccl2 14363 | . . . 4
⊢ (𝑁 ∈ (0...(2 · 𝑁)) → ((2 · 𝑁)C𝑁) ∈ ℕ) | 
| 14 | 12, 13 | syl 17 | . . 3
⊢ (𝜑 → ((2 · 𝑁)C𝑁) ∈ ℕ) | 
| 15 | 14 | nnred 12282 | . 2
⊢ (𝜑 → ((2 · 𝑁)C𝑁) ∈ ℝ) | 
| 16 |  | 2nn 12340 | . . . . . . 7
⊢ 2 ∈
ℕ | 
| 17 |  | nnmulcl 12291 | . . . . . . 7
⊢ ((2
∈ ℕ ∧ 𝑁
∈ ℕ) → (2 · 𝑁) ∈ ℕ) | 
| 18 | 16, 5, 17 | sylancr 587 | . . . . . 6
⊢ (𝜑 → (2 · 𝑁) ∈
ℕ) | 
| 19 | 18 | nnrpd 13076 | . . . . 5
⊢ (𝜑 → (2 · 𝑁) ∈
ℝ+) | 
| 20 | 18 | nnred 12282 | . . . . . . . 8
⊢ (𝜑 → (2 · 𝑁) ∈
ℝ) | 
| 21 | 19 | rpge0d 13082 | . . . . . . . 8
⊢ (𝜑 → 0 ≤ (2 · 𝑁)) | 
| 22 | 20, 21 | resqrtcld 15457 | . . . . . . 7
⊢ (𝜑 → (√‘(2 ·
𝑁)) ∈
ℝ) | 
| 23 |  | 3nn 12346 | . . . . . . 7
⊢ 3 ∈
ℕ | 
| 24 |  | nndivre 12308 | . . . . . . 7
⊢
(((√‘(2 · 𝑁)) ∈ ℝ ∧ 3 ∈ ℕ)
→ ((√‘(2 · 𝑁)) / 3) ∈ ℝ) | 
| 25 | 22, 23, 24 | sylancl 586 | . . . . . 6
⊢ (𝜑 → ((√‘(2
· 𝑁)) / 3) ∈
ℝ) | 
| 26 |  | 2re 12341 | . . . . . 6
⊢ 2 ∈
ℝ | 
| 27 |  | readdcl 11239 | . . . . . 6
⊢
((((√‘(2 · 𝑁)) / 3) ∈ ℝ ∧ 2 ∈
ℝ) → (((√‘(2 · 𝑁)) / 3) + 2) ∈
ℝ) | 
| 28 | 25, 26, 27 | sylancl 586 | . . . . 5
⊢ (𝜑 → (((√‘(2
· 𝑁)) / 3) + 2)
∈ ℝ) | 
| 29 | 19, 28 | rpcxpcld 26776 | . . . 4
⊢ (𝜑 → ((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
∈ ℝ+) | 
| 30 | 29 | rpred 13078 | . . 3
⊢ (𝜑 → ((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
∈ ℝ) | 
| 31 |  | 2rp 13040 | . . . . 5
⊢ 2 ∈
ℝ+ | 
| 32 |  | nnmulcl 12291 | . . . . . . . . 9
⊢ ((4
∈ ℕ ∧ 𝑁
∈ ℕ) → (4 · 𝑁) ∈ ℕ) | 
| 33 | 1, 5, 32 | sylancr 587 | . . . . . . . 8
⊢ (𝜑 → (4 · 𝑁) ∈
ℕ) | 
| 34 | 33 | nnred 12282 | . . . . . . 7
⊢ (𝜑 → (4 · 𝑁) ∈
ℝ) | 
| 35 |  | nndivre 12308 | . . . . . . 7
⊢ (((4
· 𝑁) ∈ ℝ
∧ 3 ∈ ℕ) → ((4 · 𝑁) / 3) ∈ ℝ) | 
| 36 | 34, 23, 35 | sylancl 586 | . . . . . 6
⊢ (𝜑 → ((4 · 𝑁) / 3) ∈
ℝ) | 
| 37 |  | 5re 12354 | . . . . . 6
⊢ 5 ∈
ℝ | 
| 38 |  | resubcl 11574 | . . . . . 6
⊢ ((((4
· 𝑁) / 3) ∈
ℝ ∧ 5 ∈ ℝ) → (((4 · 𝑁) / 3) − 5) ∈
ℝ) | 
| 39 | 36, 37, 38 | sylancl 586 | . . . . 5
⊢ (𝜑 → (((4 · 𝑁) / 3) − 5) ∈
ℝ) | 
| 40 |  | rpcxpcl 26719 | . . . . 5
⊢ ((2
∈ ℝ+ ∧ (((4 · 𝑁) / 3) − 5) ∈ ℝ) →
(2↑𝑐(((4 · 𝑁) / 3) − 5)) ∈
ℝ+) | 
| 41 | 31, 39, 40 | sylancr 587 | . . . 4
⊢ (𝜑 →
(2↑𝑐(((4 · 𝑁) / 3) − 5)) ∈
ℝ+) | 
| 42 | 41 | rpred 13078 | . . 3
⊢ (𝜑 →
(2↑𝑐(((4 · 𝑁) / 3) − 5)) ∈
ℝ) | 
| 43 | 30, 42 | remulcld 11292 | . 2
⊢ (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
· (2↑𝑐(((4 · 𝑁) / 3) − 5))) ∈
ℝ) | 
| 44 |  | df-5 12333 | . . . . 5
⊢ 5 = (4 +
1) | 
| 45 |  | 4z 12653 | . . . . . 6
⊢ 4 ∈
ℤ | 
| 46 |  | uzid 12894 | . . . . . 6
⊢ (4 ∈
ℤ → 4 ∈ (ℤ≥‘4)) | 
| 47 |  | peano2uz 12944 | . . . . . 6
⊢ (4 ∈
(ℤ≥‘4) → (4 + 1) ∈
(ℤ≥‘4)) | 
| 48 | 45, 46, 47 | mp2b 10 | . . . . 5
⊢ (4 + 1)
∈ (ℤ≥‘4) | 
| 49 | 44, 48 | eqeltri 2836 | . . . 4
⊢ 5 ∈
(ℤ≥‘4) | 
| 50 |  | eqid 2736 | . . . . 5
⊢
(ℤ≥‘4) =
(ℤ≥‘4) | 
| 51 | 50 | uztrn2 12898 | . . . 4
⊢ ((5
∈ (ℤ≥‘4) ∧ 𝑁 ∈ (ℤ≥‘5))
→ 𝑁 ∈
(ℤ≥‘4)) | 
| 52 | 49, 3, 51 | sylancr 587 | . . 3
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘4)) | 
| 53 |  | bclbnd 27325 | . . 3
⊢ (𝑁 ∈
(ℤ≥‘4) → ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁)) | 
| 54 | 52, 53 | syl 17 | . 2
⊢ (𝜑 → ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁)) | 
| 55 |  | bpos.3 | . . . . . . . 8
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1)) | 
| 56 |  | id 22 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℙ → 𝑛 ∈
ℙ) | 
| 57 |  | pccl 16888 | . . . . . . . . . 10
⊢ ((𝑛 ∈ ℙ ∧ ((2
· 𝑁)C𝑁) ∈ ℕ) → (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈
ℕ0) | 
| 58 | 56, 14, 57 | syl2anr 597 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈
ℕ0) | 
| 59 | 58 | ralrimiva 3145 | . . . . . . . 8
⊢ (𝜑 → ∀𝑛 ∈ ℙ (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈
ℕ0) | 
| 60 | 55, 59 | pcmptcl 16930 | . . . . . . 7
⊢ (𝜑 → (𝐹:ℕ⟶ℕ ∧ seq1( ·
, 𝐹):ℕ⟶ℕ)) | 
| 61 | 60 | simprd 495 | . . . . . 6
⊢ (𝜑 → seq1( · , 𝐹):ℕ⟶ℕ) | 
| 62 |  | bpos.2 | . . . . . . . . 9
⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁))) | 
| 63 |  | bpos.4 | . . . . . . . . 9
⊢ 𝐾 = (⌊‘((2 ·
𝑁) / 3)) | 
| 64 |  | bpos.5 | . . . . . . . . 9
⊢ 𝑀 =
(⌊‘(√‘(2 · 𝑁))) | 
| 65 | 3, 62, 55, 63, 64 | bposlem4 27332 | . . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ (3...𝐾)) | 
| 66 |  | elfzuz 13561 | . . . . . . . 8
⊢ (𝑀 ∈ (3...𝐾) → 𝑀 ∈
(ℤ≥‘3)) | 
| 67 | 65, 66 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘3)) | 
| 68 |  | eluznn 12961 | . . . . . . 7
⊢ ((3
∈ ℕ ∧ 𝑀
∈ (ℤ≥‘3)) → 𝑀 ∈ ℕ) | 
| 69 | 23, 67, 68 | sylancr 587 | . . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 70 | 61, 69 | ffvelcdmd 7104 | . . . . 5
⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℕ) | 
| 71 | 70 | nnred 12282 | . . . 4
⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℝ) | 
| 72 |  | 2z 12651 | . . . . . . . . 9
⊢ 2 ∈
ℤ | 
| 73 |  | nndivre 12308 | . . . . . . . . . . . 12
⊢ (((2
· 𝑁) ∈ ℝ
∧ 3 ∈ ℕ) → ((2 · 𝑁) / 3) ∈ ℝ) | 
| 74 | 20, 23, 73 | sylancl 586 | . . . . . . . . . . 11
⊢ (𝜑 → ((2 · 𝑁) / 3) ∈
ℝ) | 
| 75 | 74 | flcld 13839 | . . . . . . . . . 10
⊢ (𝜑 → (⌊‘((2
· 𝑁) / 3)) ∈
ℤ) | 
| 76 | 63, 75 | eqeltrid 2844 | . . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ ℤ) | 
| 77 |  | zmulcl 12668 | . . . . . . . . 9
⊢ ((2
∈ ℤ ∧ 𝐾
∈ ℤ) → (2 · 𝐾) ∈ ℤ) | 
| 78 | 72, 76, 77 | sylancr 587 | . . . . . . . 8
⊢ (𝜑 → (2 · 𝐾) ∈
ℤ) | 
| 79 | 2 | nnzi 12643 | . . . . . . . 8
⊢ 5 ∈
ℤ | 
| 80 |  | zsubcl 12661 | . . . . . . . 8
⊢ (((2
· 𝐾) ∈ ℤ
∧ 5 ∈ ℤ) → ((2 · 𝐾) − 5) ∈
ℤ) | 
| 81 | 78, 79, 80 | sylancl 586 | . . . . . . 7
⊢ (𝜑 → ((2 · 𝐾) − 5) ∈
ℤ) | 
| 82 | 81 | zred 12724 | . . . . . 6
⊢ (𝜑 → ((2 · 𝐾) − 5) ∈
ℝ) | 
| 83 |  | rpcxpcl 26719 | . . . . . 6
⊢ ((2
∈ ℝ+ ∧ ((2 · 𝐾) − 5) ∈ ℝ) →
(2↑𝑐((2 · 𝐾) − 5)) ∈
ℝ+) | 
| 84 | 31, 82, 83 | sylancr 587 | . . . . 5
⊢ (𝜑 →
(2↑𝑐((2 · 𝐾) − 5)) ∈
ℝ+) | 
| 85 | 84 | rpred 13078 | . . . 4
⊢ (𝜑 →
(2↑𝑐((2 · 𝐾) − 5)) ∈
ℝ) | 
| 86 | 71, 85 | remulcld 11292 | . . 3
⊢ (𝜑 → ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2
· 𝐾) − 5)))
∈ ℝ) | 
| 87 | 3, 62, 55, 63 | bposlem3 27331 | . . . 4
⊢ (𝜑 → (seq1( · , 𝐹)‘𝐾) = ((2 · 𝑁)C𝑁)) | 
| 88 |  | elfzuz3 13562 | . . . . . . . . . 10
⊢ (𝑀 ∈ (3...𝐾) → 𝐾 ∈ (ℤ≥‘𝑀)) | 
| 89 | 65, 88 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀)) | 
| 90 | 55, 59, 69, 89 | pcmptdvds 16933 | . . . . . . . 8
⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ∥ (seq1( · , 𝐹)‘𝐾)) | 
| 91 | 70 | nnzd 12642 | . . . . . . . . 9
⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℤ) | 
| 92 | 70 | nnne0d 12317 | . . . . . . . . 9
⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ≠ 0) | 
| 93 |  | uztrn 12897 | . . . . . . . . . . . . 13
⊢ ((𝐾 ∈
(ℤ≥‘𝑀) ∧ 𝑀 ∈ (ℤ≥‘3))
→ 𝐾 ∈
(ℤ≥‘3)) | 
| 94 | 89, 67, 93 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈
(ℤ≥‘3)) | 
| 95 |  | eluznn 12961 | . . . . . . . . . . . 12
⊢ ((3
∈ ℕ ∧ 𝐾
∈ (ℤ≥‘3)) → 𝐾 ∈ ℕ) | 
| 96 | 23, 94, 95 | sylancr 587 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ ℕ) | 
| 97 | 61, 96 | ffvelcdmd 7104 | . . . . . . . . . 10
⊢ (𝜑 → (seq1( · , 𝐹)‘𝐾) ∈ ℕ) | 
| 98 | 97 | nnzd 12642 | . . . . . . . . 9
⊢ (𝜑 → (seq1( · , 𝐹)‘𝐾) ∈ ℤ) | 
| 99 |  | dvdsval2 16294 | . . . . . . . . 9
⊢ (((seq1(
· , 𝐹)‘𝑀) ∈ ℤ ∧ (seq1(
· , 𝐹)‘𝑀) ≠ 0 ∧ (seq1( · ,
𝐹)‘𝐾) ∈ ℤ) → ((seq1( · ,
𝐹)‘𝑀) ∥ (seq1( · , 𝐹)‘𝐾) ↔ ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℤ)) | 
| 100 | 91, 92, 98, 99 | syl3anc 1372 | . . . . . . . 8
⊢ (𝜑 → ((seq1( · , 𝐹)‘𝑀) ∥ (seq1( · , 𝐹)‘𝐾) ↔ ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℤ)) | 
| 101 | 90, 100 | mpbid 232 | . . . . . . 7
⊢ (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℤ) | 
| 102 | 101 | zred 12724 | . . . . . 6
⊢ (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℝ) | 
| 103 | 69 | nnred 12282 | . . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℝ) | 
| 104 | 76 | zred 12724 | . . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ ℝ) | 
| 105 |  | eluzle 12892 | . . . . . . . . . 10
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝐾) | 
| 106 | 89, 105 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝑀 ≤ 𝐾) | 
| 107 |  | efchtdvds 27203 | . . . . . . . . 9
⊢ ((𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑀 ≤ 𝐾) → (exp‘(θ‘𝑀)) ∥
(exp‘(θ‘𝐾))) | 
| 108 | 103, 104,
106, 107 | syl3anc 1372 | . . . . . . . 8
⊢ (𝜑 →
(exp‘(θ‘𝑀)) ∥ (exp‘(θ‘𝐾))) | 
| 109 |  | efchtcl 27155 | . . . . . . . . . . 11
⊢ (𝑀 ∈ ℝ →
(exp‘(θ‘𝑀)) ∈ ℕ) | 
| 110 | 103, 109 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 →
(exp‘(θ‘𝑀)) ∈ ℕ) | 
| 111 | 110 | nnzd 12642 | . . . . . . . . 9
⊢ (𝜑 →
(exp‘(θ‘𝑀)) ∈ ℤ) | 
| 112 | 110 | nnne0d 12317 | . . . . . . . . 9
⊢ (𝜑 →
(exp‘(θ‘𝑀)) ≠ 0) | 
| 113 |  | efchtcl 27155 | . . . . . . . . . . 11
⊢ (𝐾 ∈ ℝ →
(exp‘(θ‘𝐾)) ∈ ℕ) | 
| 114 | 104, 113 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 →
(exp‘(θ‘𝐾)) ∈ ℕ) | 
| 115 | 114 | nnzd 12642 | . . . . . . . . 9
⊢ (𝜑 →
(exp‘(θ‘𝐾)) ∈ ℤ) | 
| 116 |  | dvdsval2 16294 | . . . . . . . . 9
⊢
(((exp‘(θ‘𝑀)) ∈ ℤ ∧
(exp‘(θ‘𝑀)) ≠ 0 ∧
(exp‘(θ‘𝐾)) ∈ ℤ) →
((exp‘(θ‘𝑀)) ∥ (exp‘(θ‘𝐾)) ↔
((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈
ℤ)) | 
| 117 | 111, 112,
115, 116 | syl3anc 1372 | . . . . . . . 8
⊢ (𝜑 →
((exp‘(θ‘𝑀)) ∥ (exp‘(θ‘𝐾)) ↔
((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈
ℤ)) | 
| 118 | 108, 117 | mpbid 232 | . . . . . . 7
⊢ (𝜑 →
((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈
ℤ) | 
| 119 | 118 | zred 12724 | . . . . . 6
⊢ (𝜑 →
((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈
ℝ) | 
| 120 |  | prmz 16713 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℤ) | 
| 121 |  | fllt 13847 | . . . . . . . . . . . . . . . . . 18
⊢
(((√‘(2 · 𝑁)) ∈ ℝ ∧ 𝑝 ∈ ℤ) → ((√‘(2
· 𝑁)) < 𝑝 ↔
(⌊‘(√‘(2 · 𝑁))) < 𝑝)) | 
| 122 | 22, 120, 121 | syl2an 596 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((√‘(2
· 𝑁)) < 𝑝 ↔
(⌊‘(√‘(2 · 𝑁))) < 𝑝)) | 
| 123 | 64 | breq1i 5149 | . . . . . . . . . . . . . . . . 17
⊢ (𝑀 < 𝑝 ↔ (⌊‘(√‘(2
· 𝑁))) < 𝑝) | 
| 124 | 122, 123 | bitr4di 289 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((√‘(2
· 𝑁)) < 𝑝 ↔ 𝑀 < 𝑝)) | 
| 125 | 120 | zred 12724 | . . . . . . . . . . . . . . . . 17
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℝ) | 
| 126 |  | ltnle 11341 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℝ ∧ 𝑝 ∈ ℝ) → (𝑀 < 𝑝 ↔ ¬ 𝑝 ≤ 𝑀)) | 
| 127 | 103, 125,
126 | syl2an 596 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑀 < 𝑝 ↔ ¬ 𝑝 ≤ 𝑀)) | 
| 128 | 124, 127 | bitrd 279 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((√‘(2
· 𝑁)) < 𝑝 ↔ ¬ 𝑝 ≤ 𝑀)) | 
| 129 |  | bposlem1 27329 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁)) | 
| 130 | 5, 129 | sylan 580 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁)) | 
| 131 | 125 | adantl 481 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℝ) | 
| 132 |  | id 22 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℙ) | 
| 133 |  | pccl 16888 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑝 ∈ ℙ ∧ ((2
· 𝑁)C𝑁) ∈ ℕ) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ∈
ℕ0) | 
| 134 | 132, 14, 133 | syl2anr 597 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ∈
ℕ0) | 
| 135 | 131, 134 | reexpcld 14204 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ∈ ℝ) | 
| 136 | 20 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (2 · 𝑁) ∈
ℝ) | 
| 137 | 131 | resqcld 14166 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝↑2) ∈ ℝ) | 
| 138 |  | lelttr 11352 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ∈ ℝ ∧ (2 · 𝑁) ∈ ℝ ∧ (𝑝↑2) ∈ ℝ) →
(((𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁) ∧ (2 · 𝑁) < (𝑝↑2)) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) < (𝑝↑2))) | 
| 139 | 135, 136,
137, 138 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (((𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁) ∧ (2 · 𝑁) < (𝑝↑2)) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) < (𝑝↑2))) | 
| 140 | 130, 139 | mpand 695 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((2 · 𝑁) < (𝑝↑2) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) < (𝑝↑2))) | 
| 141 |  | resqrtth 15295 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((2
· 𝑁) ∈ ℝ
∧ 0 ≤ (2 · 𝑁)) → ((√‘(2 · 𝑁))↑2) = (2 · 𝑁)) | 
| 142 | 20, 21, 141 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((√‘(2
· 𝑁))↑2) = (2
· 𝑁)) | 
| 143 | 142 | breq1d 5152 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (((√‘(2
· 𝑁))↑2) <
(𝑝↑2) ↔ (2
· 𝑁) < (𝑝↑2))) | 
| 144 | 143 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (((√‘(2
· 𝑁))↑2) <
(𝑝↑2) ↔ (2
· 𝑁) < (𝑝↑2))) | 
| 145 | 134 | nn0zd 12641 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ∈ ℤ) | 
| 146 | 72 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 2 ∈
ℤ) | 
| 147 |  | prmgt1 16735 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝 ∈ ℙ → 1 <
𝑝) | 
| 148 | 147 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 1 < 𝑝) | 
| 149 | 131, 145,
146, 148 | ltexp2d 14291 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt ((2 · 𝑁)C𝑁)) < 2 ↔ (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) < (𝑝↑2))) | 
| 150 | 140, 144,
149 | 3imtr4d 294 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (((√‘(2
· 𝑁))↑2) <
(𝑝↑2) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) < 2)) | 
| 151 |  | df-2 12330 | . . . . . . . . . . . . . . . . . 18
⊢ 2 = (1 +
1) | 
| 152 | 151 | breq2i 5150 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑝 pCnt ((2 · 𝑁)C𝑁)) < 2 ↔ (𝑝 pCnt ((2 · 𝑁)C𝑁)) < (1 + 1)) | 
| 153 | 150, 152 | imbitrdi 251 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (((√‘(2
· 𝑁))↑2) <
(𝑝↑2) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) < (1 + 1))) | 
| 154 | 22 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (√‘(2
· 𝑁)) ∈
ℝ) | 
| 155 | 20, 21 | sqrtge0d 15460 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 0 ≤ (√‘(2
· 𝑁))) | 
| 156 | 155 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 0 ≤
(√‘(2 · 𝑁))) | 
| 157 |  | prmnn 16712 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) | 
| 158 | 157 | nnrpd 13076 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℝ+) | 
| 159 | 158 | rpge0d 13082 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑝 ∈ ℙ → 0 ≤
𝑝) | 
| 160 | 159 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 0 ≤ 𝑝) | 
| 161 | 154, 131,
156, 160 | lt2sqd 14296 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((√‘(2
· 𝑁)) < 𝑝 ↔ ((√‘(2
· 𝑁))↑2) <
(𝑝↑2))) | 
| 162 |  | 1z 12649 | . . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℤ | 
| 163 |  | zleltp1 12670 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑝 pCnt ((2 · 𝑁)C𝑁)) ∈ ℤ ∧ 1 ∈ ℤ)
→ ((𝑝 pCnt ((2
· 𝑁)C𝑁)) ≤ 1 ↔ (𝑝 pCnt ((2 · 𝑁)C𝑁)) < (1 + 1))) | 
| 164 | 145, 162,
163 | sylancl 586 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1 ↔ (𝑝 pCnt ((2 · 𝑁)C𝑁)) < (1 + 1))) | 
| 165 | 153, 161,
164 | 3imtr4d 294 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((√‘(2
· 𝑁)) < 𝑝 → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1)) | 
| 166 | 128, 165 | sylbird 260 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (¬ 𝑝 ≤ 𝑀 → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1)) | 
| 167 | 166 | imp 406 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ ¬ 𝑝 ≤ 𝑀) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1) | 
| 168 | 167 | adantrl 716 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀)) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1) | 
| 169 |  | iftrue 4530 | . . . . . . . . . . . . 13
⊢ ((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) = (𝑝 pCnt ((2 · 𝑁)C𝑁))) | 
| 170 | 169 | adantl 481 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀)) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) = (𝑝 pCnt ((2 · 𝑁)C𝑁))) | 
| 171 |  | iftrue 4530 | . . . . . . . . . . . . 13
⊢ ((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0) = 1) | 
| 172 | 171 | adantl 481 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀)) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0) = 1) | 
| 173 | 168, 170,
172 | 3brtr4d 5174 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀)) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0)) | 
| 174 |  | 0le0 12368 | . . . . . . . . . . . . 13
⊢ 0 ≤
0 | 
| 175 |  | iffalse 4533 | . . . . . . . . . . . . . 14
⊢ (¬
(𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) = 0) | 
| 176 |  | iffalse 4533 | . . . . . . . . . . . . . 14
⊢ (¬
(𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0) = 0) | 
| 177 | 175, 176 | breq12d 5155 | . . . . . . . . . . . . 13
⊢ (¬
(𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀) → (if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0) ↔ 0 ≤ 0)) | 
| 178 | 174, 177 | mpbiri 258 | . . . . . . . . . . . 12
⊢ (¬
(𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0)) | 
| 179 | 178 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ ¬ (𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀)) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0)) | 
| 180 | 173, 179 | pm2.61dan 812 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0)) | 
| 181 | 59 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ∀𝑛 ∈ ℙ (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈
ℕ0) | 
| 182 | 69 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑀 ∈ ℕ) | 
| 183 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℙ) | 
| 184 |  | oveq1 7439 | . . . . . . . . . . 11
⊢ (𝑛 = 𝑝 → (𝑛 pCnt ((2 · 𝑁)C𝑁)) = (𝑝 pCnt ((2 · 𝑁)C𝑁))) | 
| 185 | 89 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝐾 ∈ (ℤ≥‘𝑀)) | 
| 186 | 55, 181, 182, 183, 184, 185 | pcmpt2 16932 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) = if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0)) | 
| 187 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) | 
| 188 | 187 | prmorcht 27222 | . . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ ℕ →
(exp‘(θ‘𝐾)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾)) | 
| 189 | 96, 188 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 →
(exp‘(θ‘𝐾)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾)) | 
| 190 | 187 | prmorcht 27222 | . . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ →
(exp‘(θ‘𝑀)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀)) | 
| 191 | 69, 190 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 →
(exp‘(θ‘𝑀)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀)) | 
| 192 | 189, 191 | oveq12d 7450 | . . . . . . . . . . . . 13
⊢ (𝜑 →
((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) = ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾) / (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀))) | 
| 193 | 192 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) →
((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) = ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾) / (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀))) | 
| 194 | 193 | oveq2d 7448 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀)))) = (𝑝 pCnt ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾) / (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀)))) | 
| 195 |  | nncn 12275 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) | 
| 196 | 195 | exp1d 14182 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (𝑛↑1) = 𝑛) | 
| 197 | 196 | ifeq1d 4544 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → if(𝑛 ∈ ℙ, (𝑛↑1), 1) = if(𝑛 ∈ ℙ, 𝑛, 1)) | 
| 198 | 197 | mpteq2ia 5244 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑1), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) | 
| 199 | 198 | eqcomi 2745 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑1), 1)) | 
| 200 |  | 1nn0 12544 | . . . . . . . . . . . . . . 15
⊢ 1 ∈
ℕ0 | 
| 201 | 200 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℙ) → 1 ∈
ℕ0) | 
| 202 | 201 | ralrimiva 3145 | . . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑛 ∈ ℙ 1 ∈
ℕ0) | 
| 203 | 202 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ∀𝑛 ∈ ℙ 1 ∈
ℕ0) | 
| 204 |  | eqidd 2737 | . . . . . . . . . . . 12
⊢ (𝑛 = 𝑝 → 1 = 1) | 
| 205 | 199, 203,
182, 183, 204, 185 | pcmpt2 16932 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾) / (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀))) = if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0)) | 
| 206 | 194, 205 | eqtrd 2776 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀)))) = if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0)) | 
| 207 | 180, 186,
206 | 3brtr4d 5174 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) ≤ (𝑝 pCnt ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀))))) | 
| 208 | 207 | ralrimiva 3145 | . . . . . . . 8
⊢ (𝜑 → ∀𝑝 ∈ ℙ (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) ≤ (𝑝 pCnt ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀))))) | 
| 209 |  | pc2dvds 16918 | . . . . . . . . 9
⊢ ((((seq1(
· , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℤ ∧
((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℤ) →
(((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∥ ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀))) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) ≤ (𝑝 pCnt ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀)))))) | 
| 210 | 101, 118,
209 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∥ ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀))) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) ≤ (𝑝 pCnt ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀)))))) | 
| 211 | 208, 210 | mpbird 257 | . . . . . . 7
⊢ (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∥ ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀)))) | 
| 212 | 114 | nnred 12282 | . . . . . . . . . 10
⊢ (𝜑 →
(exp‘(θ‘𝐾)) ∈ ℝ) | 
| 213 | 110 | nnred 12282 | . . . . . . . . . 10
⊢ (𝜑 →
(exp‘(θ‘𝑀)) ∈ ℝ) | 
| 214 | 114 | nngt0d 12316 | . . . . . . . . . 10
⊢ (𝜑 → 0 <
(exp‘(θ‘𝐾))) | 
| 215 | 110 | nngt0d 12316 | . . . . . . . . . 10
⊢ (𝜑 → 0 <
(exp‘(θ‘𝑀))) | 
| 216 | 212, 213,
214, 215 | divgt0d 12204 | . . . . . . . . 9
⊢ (𝜑 → 0 <
((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))) | 
| 217 |  | elnnz 12625 | . . . . . . . . 9
⊢
(((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℕ ↔
(((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℤ ∧ 0 <
((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))))) | 
| 218 | 118, 216,
217 | sylanbrc 583 | . . . . . . . 8
⊢ (𝜑 →
((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈
ℕ) | 
| 219 |  | dvdsle 16348 | . . . . . . . 8
⊢ ((((seq1(
· , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℤ ∧
((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℕ) →
(((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∥ ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀))) → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ≤ ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀))))) | 
| 220 | 101, 218,
219 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∥ ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀))) → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ≤ ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀))))) | 
| 221 | 211, 220 | mpd 15 | . . . . . 6
⊢ (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ≤ ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀)))) | 
| 222 |  | nndivre 12308 | . . . . . . . 8
⊢
(((exp‘(θ‘𝐾)) ∈ ℝ ∧ 4 ∈ ℕ)
→ ((exp‘(θ‘𝐾)) / 4) ∈ ℝ) | 
| 223 | 212, 1, 222 | sylancl 586 | . . . . . . 7
⊢ (𝜑 →
((exp‘(θ‘𝐾)) / 4) ∈ ℝ) | 
| 224 |  | 4re 12351 | . . . . . . . . . 10
⊢ 4 ∈
ℝ | 
| 225 | 224 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → 4 ∈
ℝ) | 
| 226 |  | 6re 12357 | . . . . . . . . . 10
⊢ 6 ∈
ℝ | 
| 227 | 226 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → 6 ∈
ℝ) | 
| 228 |  | 4lt6 12449 | . . . . . . . . . 10
⊢ 4 <
6 | 
| 229 | 228 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → 4 < 6) | 
| 230 |  | cht3 27217 | . . . . . . . . . . . 12
⊢
(θ‘3) = (log‘6) | 
| 231 | 230 | fveq2i 6908 | . . . . . . . . . . 11
⊢
(exp‘(θ‘3)) =
(exp‘(log‘6)) | 
| 232 |  | 6pos 12377 | . . . . . . . . . . . . 13
⊢ 0 <
6 | 
| 233 | 226, 232 | elrpii 13038 | . . . . . . . . . . . 12
⊢ 6 ∈
ℝ+ | 
| 234 |  | reeflog 26623 | . . . . . . . . . . . 12
⊢ (6 ∈
ℝ+ → (exp‘(log‘6)) = 6) | 
| 235 | 233, 234 | ax-mp 5 | . . . . . . . . . . 11
⊢
(exp‘(log‘6)) = 6 | 
| 236 | 231, 235 | eqtri 2764 | . . . . . . . . . 10
⊢
(exp‘(θ‘3)) = 6 | 
| 237 |  | 3re 12347 | . . . . . . . . . . . . 13
⊢ 3 ∈
ℝ | 
| 238 | 237 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → 3 ∈
ℝ) | 
| 239 |  | eluzle 12892 | . . . . . . . . . . . . 13
⊢ (𝑀 ∈
(ℤ≥‘3) → 3 ≤ 𝑀) | 
| 240 | 67, 239 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 3 ≤ 𝑀) | 
| 241 |  | chtwordi 27200 | . . . . . . . . . . . 12
⊢ ((3
∈ ℝ ∧ 𝑀
∈ ℝ ∧ 3 ≤ 𝑀) → (θ‘3) ≤
(θ‘𝑀)) | 
| 242 | 238, 103,
240, 241 | syl3anc 1372 | . . . . . . . . . . 11
⊢ (𝜑 → (θ‘3) ≤
(θ‘𝑀)) | 
| 243 |  | chtcl 27153 | . . . . . . . . . . . . 13
⊢ (3 ∈
ℝ → (θ‘3) ∈ ℝ) | 
| 244 | 237, 243 | ax-mp 5 | . . . . . . . . . . . 12
⊢
(θ‘3) ∈ ℝ | 
| 245 |  | chtcl 27153 | . . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℝ →
(θ‘𝑀) ∈
ℝ) | 
| 246 | 103, 245 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (θ‘𝑀) ∈
ℝ) | 
| 247 |  | efle 16155 | . . . . . . . . . . . 12
⊢
(((θ‘3) ∈ ℝ ∧ (θ‘𝑀) ∈ ℝ) →
((θ‘3) ≤ (θ‘𝑀) ↔ (exp‘(θ‘3)) ≤
(exp‘(θ‘𝑀)))) | 
| 248 | 244, 246,
247 | sylancr 587 | . . . . . . . . . . 11
⊢ (𝜑 → ((θ‘3) ≤
(θ‘𝑀) ↔
(exp‘(θ‘3)) ≤ (exp‘(θ‘𝑀)))) | 
| 249 | 242, 248 | mpbid 232 | . . . . . . . . . 10
⊢ (𝜑 →
(exp‘(θ‘3)) ≤ (exp‘(θ‘𝑀))) | 
| 250 | 236, 249 | eqbrtrrid 5178 | . . . . . . . . 9
⊢ (𝜑 → 6 ≤
(exp‘(θ‘𝑀))) | 
| 251 | 225, 227,
213, 229, 250 | ltletrd 11422 | . . . . . . . 8
⊢ (𝜑 → 4 <
(exp‘(θ‘𝑀))) | 
| 252 |  | 4pos 12374 | . . . . . . . . . 10
⊢ 0 <
4 | 
| 253 | 252 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → 0 < 4) | 
| 254 |  | ltdiv2 12155 | . . . . . . . . 9
⊢ (((4
∈ ℝ ∧ 0 < 4) ∧ ((exp‘(θ‘𝑀)) ∈ ℝ ∧ 0 <
(exp‘(θ‘𝑀))) ∧ ((exp‘(θ‘𝐾)) ∈ ℝ ∧ 0 <
(exp‘(θ‘𝐾)))) → (4 <
(exp‘(θ‘𝑀)) ↔ ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀))) < ((exp‘(θ‘𝐾)) / 4))) | 
| 255 | 225, 253,
213, 215, 212, 214, 254 | syl222anc 1387 | . . . . . . . 8
⊢ (𝜑 → (4 <
(exp‘(θ‘𝑀)) ↔ ((exp‘(θ‘𝐾)) /
(exp‘(θ‘𝑀))) < ((exp‘(θ‘𝐾)) / 4))) | 
| 256 | 251, 255 | mpbid 232 | . . . . . . 7
⊢ (𝜑 →
((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) <
((exp‘(θ‘𝐾)) / 4)) | 
| 257 | 26 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → 2 ∈
ℝ) | 
| 258 |  | 2lt3 12439 | . . . . . . . . . . . . . 14
⊢ 2 <
3 | 
| 259 | 258 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → 2 < 3) | 
| 260 | 238, 103,
104, 240, 106 | letrd 11419 | . . . . . . . . . . . . 13
⊢ (𝜑 → 3 ≤ 𝐾) | 
| 261 | 257, 238,
104, 259, 260 | ltletrd 11422 | . . . . . . . . . . . 12
⊢ (𝜑 → 2 < 𝐾) | 
| 262 |  | chtub 27257 | . . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℝ ∧ 2 <
𝐾) →
(θ‘𝐾) <
((log‘2) · ((2 · 𝐾) − 3))) | 
| 263 | 104, 261,
262 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → (θ‘𝐾) < ((log‘2) ·
((2 · 𝐾) −
3))) | 
| 264 |  | chtcl 27153 | . . . . . . . . . . . . 13
⊢ (𝐾 ∈ ℝ →
(θ‘𝐾) ∈
ℝ) | 
| 265 | 104, 264 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (θ‘𝐾) ∈
ℝ) | 
| 266 |  | relogcl 26618 | . . . . . . . . . . . . . 14
⊢ (2 ∈
ℝ+ → (log‘2) ∈ ℝ) | 
| 267 | 31, 266 | ax-mp 5 | . . . . . . . . . . . . 13
⊢
(log‘2) ∈ ℝ | 
| 268 |  | 3z 12652 | . . . . . . . . . . . . . . 15
⊢ 3 ∈
ℤ | 
| 269 |  | zsubcl 12661 | . . . . . . . . . . . . . . 15
⊢ (((2
· 𝐾) ∈ ℤ
∧ 3 ∈ ℤ) → ((2 · 𝐾) − 3) ∈
ℤ) | 
| 270 | 78, 268, 269 | sylancl 586 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((2 · 𝐾) − 3) ∈
ℤ) | 
| 271 | 270 | zred 12724 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((2 · 𝐾) − 3) ∈
ℝ) | 
| 272 |  | remulcl 11241 | . . . . . . . . . . . . 13
⊢
(((log‘2) ∈ ℝ ∧ ((2 · 𝐾) − 3) ∈ ℝ) →
((log‘2) · ((2 · 𝐾) − 3)) ∈
ℝ) | 
| 273 | 267, 271,
272 | sylancr 587 | . . . . . . . . . . . 12
⊢ (𝜑 → ((log‘2) ·
((2 · 𝐾) − 3))
∈ ℝ) | 
| 274 |  | eflt 16154 | . . . . . . . . . . . 12
⊢
(((θ‘𝐾)
∈ ℝ ∧ ((log‘2) · ((2 · 𝐾) − 3)) ∈ ℝ) →
((θ‘𝐾) <
((log‘2) · ((2 · 𝐾) − 3)) ↔
(exp‘(θ‘𝐾)) < (exp‘((log‘2) ·
((2 · 𝐾) −
3))))) | 
| 275 | 265, 273,
274 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → ((θ‘𝐾) < ((log‘2) ·
((2 · 𝐾) − 3))
↔ (exp‘(θ‘𝐾)) < (exp‘((log‘2) ·
((2 · 𝐾) −
3))))) | 
| 276 | 263, 275 | mpbid 232 | . . . . . . . . . 10
⊢ (𝜑 →
(exp‘(θ‘𝐾)) < (exp‘((log‘2) ·
((2 · 𝐾) −
3)))) | 
| 277 |  | reexplog 26638 | . . . . . . . . . . . 12
⊢ ((2
∈ ℝ+ ∧ ((2 · 𝐾) − 3) ∈ ℤ) →
(2↑((2 · 𝐾)
− 3)) = (exp‘(((2 · 𝐾) − 3) ·
(log‘2)))) | 
| 278 | 31, 270, 277 | sylancr 587 | . . . . . . . . . . 11
⊢ (𝜑 → (2↑((2 · 𝐾) − 3)) = (exp‘(((2
· 𝐾) − 3)
· (log‘2)))) | 
| 279 | 270 | zcnd 12725 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((2 · 𝐾) − 3) ∈
ℂ) | 
| 280 | 267 | recni 11276 | . . . . . . . . . . . . 13
⊢
(log‘2) ∈ ℂ | 
| 281 |  | mulcom 11242 | . . . . . . . . . . . . 13
⊢ ((((2
· 𝐾) − 3)
∈ ℂ ∧ (log‘2) ∈ ℂ) → (((2 · 𝐾) − 3) ·
(log‘2)) = ((log‘2) · ((2 · 𝐾) − 3))) | 
| 282 | 279, 280,
281 | sylancl 586 | . . . . . . . . . . . 12
⊢ (𝜑 → (((2 · 𝐾) − 3) ·
(log‘2)) = ((log‘2) · ((2 · 𝐾) − 3))) | 
| 283 | 282 | fveq2d 6909 | . . . . . . . . . . 11
⊢ (𝜑 → (exp‘(((2 ·
𝐾) − 3) ·
(log‘2))) = (exp‘((log‘2) · ((2 · 𝐾) − 3)))) | 
| 284 | 278, 283 | eqtrd 2776 | . . . . . . . . . 10
⊢ (𝜑 → (2↑((2 · 𝐾) − 3)) =
(exp‘((log‘2) · ((2 · 𝐾) − 3)))) | 
| 285 | 276, 284 | breqtrrd 5170 | . . . . . . . . 9
⊢ (𝜑 →
(exp‘(θ‘𝐾)) < (2↑((2 · 𝐾) − 3))) | 
| 286 |  | 3p2e5 12418 | . . . . . . . . . . . . . . . 16
⊢ (3 + 2) =
5 | 
| 287 | 286 | oveq1i 7442 | . . . . . . . . . . . . . . 15
⊢ ((3 + 2)
− 2) = (5 − 2) | 
| 288 |  | 3cn 12348 | . . . . . . . . . . . . . . . 16
⊢ 3 ∈
ℂ | 
| 289 |  | 2cn 12342 | . . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℂ | 
| 290 | 288, 289 | pncan3oi 11525 | . . . . . . . . . . . . . . 15
⊢ ((3 + 2)
− 2) = 3 | 
| 291 | 287, 290 | eqtr3i 2766 | . . . . . . . . . . . . . 14
⊢ (5
− 2) = 3 | 
| 292 | 291 | oveq2i 7443 | . . . . . . . . . . . . 13
⊢ ((2
· 𝐾) − (5
− 2)) = ((2 · 𝐾) − 3) | 
| 293 | 78 | zcnd 12725 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (2 · 𝐾) ∈
ℂ) | 
| 294 |  | 5cn 12355 | . . . . . . . . . . . . . . 15
⊢ 5 ∈
ℂ | 
| 295 |  | subsub 11540 | . . . . . . . . . . . . . . 15
⊢ (((2
· 𝐾) ∈ ℂ
∧ 5 ∈ ℂ ∧ 2 ∈ ℂ) → ((2 · 𝐾) − (5 − 2)) = (((2
· 𝐾) − 5) +
2)) | 
| 296 | 294, 289,
295 | mp3an23 1454 | . . . . . . . . . . . . . 14
⊢ ((2
· 𝐾) ∈ ℂ
→ ((2 · 𝐾)
− (5 − 2)) = (((2 · 𝐾) − 5) + 2)) | 
| 297 | 293, 296 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((2 · 𝐾) − (5 − 2)) = (((2
· 𝐾) − 5) +
2)) | 
| 298 | 292, 297 | eqtr3id 2790 | . . . . . . . . . . . 12
⊢ (𝜑 → ((2 · 𝐾) − 3) = (((2 ·
𝐾) − 5) +
2)) | 
| 299 | 298 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (𝜑 →
(2↑𝑐((2 · 𝐾) − 3)) =
(2↑𝑐(((2 · 𝐾) − 5) + 2))) | 
| 300 |  | 2ne0 12371 | . . . . . . . . . . . 12
⊢ 2 ≠
0 | 
| 301 |  | cxpexpz 26710 | . . . . . . . . . . . 12
⊢ ((2
∈ ℂ ∧ 2 ≠ 0 ∧ ((2 · 𝐾) − 3) ∈ ℤ) →
(2↑𝑐((2 · 𝐾) − 3)) = (2↑((2 · 𝐾) − 3))) | 
| 302 | 289, 300,
270, 301 | mp3an12i 1466 | . . . . . . . . . . 11
⊢ (𝜑 →
(2↑𝑐((2 · 𝐾) − 3)) = (2↑((2 · 𝐾) − 3))) | 
| 303 | 81 | zcnd 12725 | . . . . . . . . . . . 12
⊢ (𝜑 → ((2 · 𝐾) − 5) ∈
ℂ) | 
| 304 |  | 2cnne0 12477 | . . . . . . . . . . . . 13
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) | 
| 305 |  | cxpadd 26722 | . . . . . . . . . . . . 13
⊢ (((2
∈ ℂ ∧ 2 ≠ 0) ∧ ((2 · 𝐾) − 5) ∈ ℂ ∧ 2 ∈
ℂ) → (2↑𝑐(((2 · 𝐾) − 5) + 2)) =
((2↑𝑐((2 · 𝐾) − 5)) ·
(2↑𝑐2))) | 
| 306 | 304, 289,
305 | mp3an13 1453 | . . . . . . . . . . . 12
⊢ (((2
· 𝐾) − 5)
∈ ℂ → (2↑𝑐(((2 · 𝐾) − 5) + 2)) =
((2↑𝑐((2 · 𝐾) − 5)) ·
(2↑𝑐2))) | 
| 307 | 303, 306 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 →
(2↑𝑐(((2 · 𝐾) − 5) + 2)) =
((2↑𝑐((2 · 𝐾) − 5)) ·
(2↑𝑐2))) | 
| 308 | 299, 302,
307 | 3eqtr3d 2784 | . . . . . . . . . 10
⊢ (𝜑 → (2↑((2 · 𝐾) − 3)) =
((2↑𝑐((2 · 𝐾) − 5)) ·
(2↑𝑐2))) | 
| 309 |  | 2nn0 12545 | . . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 | 
| 310 |  | cxpexp 26711 | . . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ 2 ∈ ℕ0) →
(2↑𝑐2) = (2↑2)) | 
| 311 | 289, 309,
310 | mp2an 692 | . . . . . . . . . . . 12
⊢
(2↑𝑐2) = (2↑2) | 
| 312 |  | sq2 14237 | . . . . . . . . . . . 12
⊢
(2↑2) = 4 | 
| 313 | 311, 312 | eqtri 2764 | . . . . . . . . . . 11
⊢
(2↑𝑐2) = 4 | 
| 314 | 313 | oveq2i 7443 | . . . . . . . . . 10
⊢
((2↑𝑐((2 · 𝐾) − 5)) ·
(2↑𝑐2)) = ((2↑𝑐((2 ·
𝐾) − 5)) ·
4) | 
| 315 | 308, 314 | eqtrdi 2792 | . . . . . . . . 9
⊢ (𝜑 → (2↑((2 · 𝐾) − 3)) =
((2↑𝑐((2 · 𝐾) − 5)) · 4)) | 
| 316 | 285, 315 | breqtrd 5168 | . . . . . . . 8
⊢ (𝜑 →
(exp‘(θ‘𝐾)) < ((2↑𝑐((2
· 𝐾) − 5))
· 4)) | 
| 317 | 224, 252 | pm3.2i 470 | . . . . . . . . . 10
⊢ (4 ∈
ℝ ∧ 0 < 4) | 
| 318 | 317 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → (4 ∈ ℝ ∧ 0
< 4)) | 
| 319 |  | ltdivmul2 12146 | . . . . . . . . 9
⊢
(((exp‘(θ‘𝐾)) ∈ ℝ ∧
(2↑𝑐((2 · 𝐾) − 5)) ∈ ℝ ∧ (4 ∈
ℝ ∧ 0 < 4)) → (((exp‘(θ‘𝐾)) / 4) < (2↑𝑐((2
· 𝐾) − 5))
↔ (exp‘(θ‘𝐾)) < ((2↑𝑐((2
· 𝐾) − 5))
· 4))) | 
| 320 | 212, 85, 318, 319 | syl3anc 1372 | . . . . . . . 8
⊢ (𝜑 →
(((exp‘(θ‘𝐾)) / 4) < (2↑𝑐((2
· 𝐾) − 5))
↔ (exp‘(θ‘𝐾)) < ((2↑𝑐((2
· 𝐾) − 5))
· 4))) | 
| 321 | 316, 320 | mpbird 257 | . . . . . . 7
⊢ (𝜑 →
((exp‘(θ‘𝐾)) / 4) < (2↑𝑐((2
· 𝐾) −
5))) | 
| 322 | 119, 223,
85, 256, 321 | lttrd 11423 | . . . . . 6
⊢ (𝜑 →
((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) <
(2↑𝑐((2 · 𝐾) − 5))) | 
| 323 | 102, 119,
85, 221, 322 | lelttrd 11420 | . . . . 5
⊢ (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) < (2↑𝑐((2
· 𝐾) −
5))) | 
| 324 | 97 | nnred 12282 | . . . . . 6
⊢ (𝜑 → (seq1( · , 𝐹)‘𝐾) ∈ ℝ) | 
| 325 |  | nnre 12274 | . . . . . . . 8
⊢ ((seq1(
· , 𝐹)‘𝑀) ∈ ℕ → (seq1(
· , 𝐹)‘𝑀) ∈
ℝ) | 
| 326 |  | nngt0 12298 | . . . . . . . 8
⊢ ((seq1(
· , 𝐹)‘𝑀) ∈ ℕ → 0 <
(seq1( · , 𝐹)‘𝑀)) | 
| 327 | 325, 326 | jca 511 | . . . . . . 7
⊢ ((seq1(
· , 𝐹)‘𝑀) ∈ ℕ → ((seq1(
· , 𝐹)‘𝑀) ∈ ℝ ∧ 0 <
(seq1( · , 𝐹)‘𝑀))) | 
| 328 | 70, 327 | syl 17 | . . . . . 6
⊢ (𝜑 → ((seq1( · , 𝐹)‘𝑀) ∈ ℝ ∧ 0 < (seq1(
· , 𝐹)‘𝑀))) | 
| 329 |  | ltdivmul 12144 | . . . . . 6
⊢ (((seq1(
· , 𝐹)‘𝐾) ∈ ℝ ∧
(2↑𝑐((2 · 𝐾) − 5)) ∈ ℝ ∧ ((seq1(
· , 𝐹)‘𝑀) ∈ ℝ ∧ 0 <
(seq1( · , 𝐹)‘𝑀))) → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) < (2↑𝑐((2
· 𝐾) − 5))
↔ (seq1( · , 𝐹)‘𝐾) < ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2
· 𝐾) −
5))))) | 
| 330 | 324, 85, 328, 329 | syl3anc 1372 | . . . . 5
⊢ (𝜑 → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) < (2↑𝑐((2
· 𝐾) − 5))
↔ (seq1( · , 𝐹)‘𝐾) < ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2
· 𝐾) −
5))))) | 
| 331 | 323, 330 | mpbid 232 | . . . 4
⊢ (𝜑 → (seq1( · , 𝐹)‘𝐾) < ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2
· 𝐾) −
5)))) | 
| 332 | 87, 331 | eqbrtrrd 5166 | . . 3
⊢ (𝜑 → ((2 · 𝑁)C𝑁) < ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2
· 𝐾) −
5)))) | 
| 333 | 30, 85 | remulcld 11292 | . . . 4
⊢ (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
· (2↑𝑐((2 · 𝐾) − 5))) ∈
ℝ) | 
| 334 | 3, 62, 55, 63, 64 | bposlem5 27333 | . . . . 5
⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) +
2))) | 
| 335 | 71, 30, 84 | lemul1d 13121 | . . . . 5
⊢ (𝜑 → ((seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
↔ ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2
· 𝐾) − 5))) ≤
(((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
· (2↑𝑐((2 · 𝐾) − 5))))) | 
| 336 | 334, 335 | mpbid 232 | . . . 4
⊢ (𝜑 → ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2
· 𝐾) − 5)))
≤ (((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
· (2↑𝑐((2 · 𝐾) − 5)))) | 
| 337 | 78 | zred 12724 | . . . . . . 7
⊢ (𝜑 → (2 · 𝐾) ∈
ℝ) | 
| 338 | 37 | a1i 11 | . . . . . . 7
⊢ (𝜑 → 5 ∈
ℝ) | 
| 339 |  | flle 13840 | . . . . . . . . . . 11
⊢ (((2
· 𝑁) / 3) ∈
ℝ → (⌊‘((2 · 𝑁) / 3)) ≤ ((2 · 𝑁) / 3)) | 
| 340 | 74, 339 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (⌊‘((2
· 𝑁) / 3)) ≤ ((2
· 𝑁) /
3)) | 
| 341 | 63, 340 | eqbrtrid 5177 | . . . . . . . . 9
⊢ (𝜑 → 𝐾 ≤ ((2 · 𝑁) / 3)) | 
| 342 |  | 2pos 12370 | . . . . . . . . . . . 12
⊢ 0 <
2 | 
| 343 | 26, 342 | pm3.2i 470 | . . . . . . . . . . 11
⊢ (2 ∈
ℝ ∧ 0 < 2) | 
| 344 | 343 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → (2 ∈ ℝ ∧ 0
< 2)) | 
| 345 |  | lemul2 12121 | . . . . . . . . . 10
⊢ ((𝐾 ∈ ℝ ∧ ((2
· 𝑁) / 3) ∈
ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝐾 ≤ ((2 · 𝑁) / 3) ↔ (2 · 𝐾) ≤ (2 · ((2 · 𝑁) / 3)))) | 
| 346 | 104, 74, 344, 345 | syl3anc 1372 | . . . . . . . . 9
⊢ (𝜑 → (𝐾 ≤ ((2 · 𝑁) / 3) ↔ (2 · 𝐾) ≤ (2 · ((2 · 𝑁) / 3)))) | 
| 347 | 341, 346 | mpbid 232 | . . . . . . . 8
⊢ (𝜑 → (2 · 𝐾) ≤ (2 · ((2 ·
𝑁) / 3))) | 
| 348 | 18 | nncnd 12283 | . . . . . . . . . 10
⊢ (𝜑 → (2 · 𝑁) ∈
ℂ) | 
| 349 |  | 3ne0 12373 | . . . . . . . . . . . 12
⊢ 3 ≠
0 | 
| 350 | 288, 349 | pm3.2i 470 | . . . . . . . . . . 11
⊢ (3 ∈
ℂ ∧ 3 ≠ 0) | 
| 351 |  | divass 11941 | . . . . . . . . . . 11
⊢ ((2
∈ ℂ ∧ (2 · 𝑁) ∈ ℂ ∧ (3 ∈ ℂ
∧ 3 ≠ 0)) → ((2 · (2 · 𝑁)) / 3) = (2 · ((2 · 𝑁) / 3))) | 
| 352 | 289, 350,
351 | mp3an13 1453 | . . . . . . . . . 10
⊢ ((2
· 𝑁) ∈ ℂ
→ ((2 · (2 · 𝑁)) / 3) = (2 · ((2 · 𝑁) / 3))) | 
| 353 | 348, 352 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → ((2 · (2 ·
𝑁)) / 3) = (2 · ((2
· 𝑁) /
3))) | 
| 354 | 5 | nncnd 12283 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℂ) | 
| 355 |  | mulass 11244 | . . . . . . . . . . . 12
⊢ ((2
∈ ℂ ∧ 2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((2 · 2)
· 𝑁) = (2 ·
(2 · 𝑁))) | 
| 356 | 289, 289,
354, 355 | mp3an12i 1466 | . . . . . . . . . . 11
⊢ (𝜑 → ((2 · 2) ·
𝑁) = (2 · (2
· 𝑁))) | 
| 357 |  | 2t2e4 12431 | . . . . . . . . . . . 12
⊢ (2
· 2) = 4 | 
| 358 | 357 | oveq1i 7442 | . . . . . . . . . . 11
⊢ ((2
· 2) · 𝑁) =
(4 · 𝑁) | 
| 359 | 356, 358 | eqtr3di 2791 | . . . . . . . . . 10
⊢ (𝜑 → (2 · (2 ·
𝑁)) = (4 · 𝑁)) | 
| 360 | 359 | oveq1d 7447 | . . . . . . . . 9
⊢ (𝜑 → ((2 · (2 ·
𝑁)) / 3) = ((4 ·
𝑁) / 3)) | 
| 361 | 353, 360 | eqtr3d 2778 | . . . . . . . 8
⊢ (𝜑 → (2 · ((2 ·
𝑁) / 3)) = ((4 ·
𝑁) / 3)) | 
| 362 | 347, 361 | breqtrd 5168 | . . . . . . 7
⊢ (𝜑 → (2 · 𝐾) ≤ ((4 · 𝑁) / 3)) | 
| 363 | 337, 36, 338, 362 | lesub1dd 11880 | . . . . . 6
⊢ (𝜑 → ((2 · 𝐾) − 5) ≤ (((4 ·
𝑁) / 3) −
5)) | 
| 364 |  | 1lt2 12438 | . . . . . . . 8
⊢ 1 <
2 | 
| 365 | 364 | a1i 11 | . . . . . . 7
⊢ (𝜑 → 1 < 2) | 
| 366 | 257, 365,
82, 39 | cxpled 26763 | . . . . . 6
⊢ (𝜑 → (((2 · 𝐾) − 5) ≤ (((4 ·
𝑁) / 3) − 5) ↔
(2↑𝑐((2 · 𝐾) − 5)) ≤
(2↑𝑐(((4 · 𝑁) / 3) − 5)))) | 
| 367 | 363, 366 | mpbid 232 | . . . . 5
⊢ (𝜑 →
(2↑𝑐((2 · 𝐾) − 5)) ≤
(2↑𝑐(((4 · 𝑁) / 3) − 5))) | 
| 368 | 85, 42, 29 | lemul2d 13122 | . . . . 5
⊢ (𝜑 →
((2↑𝑐((2 · 𝐾) − 5)) ≤
(2↑𝑐(((4 · 𝑁) / 3) − 5)) ↔ (((2 ·
𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
· (2↑𝑐((2 · 𝐾) − 5))) ≤ (((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
· (2↑𝑐(((4 · 𝑁) / 3) − 5))))) | 
| 369 | 367, 368 | mpbid 232 | . . . 4
⊢ (𝜑 → (((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
· (2↑𝑐((2 · 𝐾) − 5))) ≤ (((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
· (2↑𝑐(((4 · 𝑁) / 3) − 5)))) | 
| 370 | 86, 333, 43, 336, 369 | letrd 11419 | . . 3
⊢ (𝜑 → ((seq1( · , 𝐹)‘𝑀) · (2↑𝑐((2
· 𝐾) − 5)))
≤ (((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
· (2↑𝑐(((4 · 𝑁) / 3) − 5)))) | 
| 371 | 15, 86, 43, 332, 370 | ltletrd 11422 | . 2
⊢ (𝜑 → ((2 · 𝑁)C𝑁) < (((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
· (2↑𝑐(((4 · 𝑁) / 3) − 5)))) | 
| 372 | 10, 15, 43, 54, 371 | lttrd 11423 | 1
⊢ (𝜑 → ((4↑𝑁) / 𝑁) < (((2 · 𝑁)↑𝑐(((√‘(2
· 𝑁)) / 3) + 2))
· (2↑𝑐(((4 · 𝑁) / 3) − 5)))) |