| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2nn 12339 | . . . . . 6
⊢ 2 ∈
ℕ | 
| 2 |  | nnmulcl 12290 | . . . . . 6
⊢ ((2
∈ ℕ ∧ 𝑁
∈ ℕ) → (2 · 𝑁) ∈ ℕ) | 
| 3 | 1, 2 | mpan 690 | . . . . 5
⊢ (𝑁 ∈ ℕ → (2
· 𝑁) ∈
ℕ) | 
| 4 | 3 | nnred 12281 | . . . 4
⊢ (𝑁 ∈ ℕ → (2
· 𝑁) ∈
ℝ) | 
| 5 |  | peano2rem 11576 | . . . 4
⊢ ((2
· 𝑁) ∈ ℝ
→ ((2 · 𝑁)
− 1) ∈ ℝ) | 
| 6 | 4, 5 | syl 17 | . . 3
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) − 1)
∈ ℝ) | 
| 7 |  | chtcl 27152 | . . 3
⊢ (((2
· 𝑁) − 1)
∈ ℝ → (θ‘((2 · 𝑁) − 1)) ∈
ℝ) | 
| 8 | 6, 7 | syl 17 | . 2
⊢ (𝑁 ∈ ℕ →
(θ‘((2 · 𝑁) − 1)) ∈
ℝ) | 
| 9 |  | nnre 12273 | . . . 4
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) | 
| 10 |  | chtcl 27152 | . . . 4
⊢ (𝑁 ∈ ℝ →
(θ‘𝑁) ∈
ℝ) | 
| 11 | 9, 10 | syl 17 | . . 3
⊢ (𝑁 ∈ ℕ →
(θ‘𝑁) ∈
ℝ) | 
| 12 |  | nnnn0 12533 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) | 
| 13 |  | 2m1e1 12392 | . . . . . . . . . . 11
⊢ (2
− 1) = 1 | 
| 14 | 13 | oveq2i 7442 | . . . . . . . . . 10
⊢ ((2
· 𝑁) − (2
− 1)) = ((2 · 𝑁) − 1) | 
| 15 | 3 | nncnd 12282 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (2
· 𝑁) ∈
ℂ) | 
| 16 |  | 2cn 12341 | . . . . . . . . . . . . 13
⊢ 2 ∈
ℂ | 
| 17 |  | ax-1cn 11213 | . . . . . . . . . . . . 13
⊢ 1 ∈
ℂ | 
| 18 |  | subsub 11539 | . . . . . . . . . . . . 13
⊢ (((2
· 𝑁) ∈ ℂ
∧ 2 ∈ ℂ ∧ 1 ∈ ℂ) → ((2 · 𝑁) − (2 − 1)) = (((2
· 𝑁) − 2) +
1)) | 
| 19 | 16, 17, 18 | mp3an23 1455 | . . . . . . . . . . . 12
⊢ ((2
· 𝑁) ∈ ℂ
→ ((2 · 𝑁)
− (2 − 1)) = (((2 · 𝑁) − 2) + 1)) | 
| 20 | 15, 19 | syl 17 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) − (2
− 1)) = (((2 · 𝑁) − 2) + 1)) | 
| 21 |  | nncn 12274 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) | 
| 22 |  | subdi 11696 | . . . . . . . . . . . . . . 15
⊢ ((2
∈ ℂ ∧ 𝑁
∈ ℂ ∧ 1 ∈ ℂ) → (2 · (𝑁 − 1)) = ((2 · 𝑁) − (2 ·
1))) | 
| 23 | 16, 17, 22 | mp3an13 1454 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℂ → (2
· (𝑁 − 1)) =
((2 · 𝑁) − (2
· 1))) | 
| 24 | 21, 23 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → (2
· (𝑁 − 1)) =
((2 · 𝑁) − (2
· 1))) | 
| 25 |  | 2t1e2 12429 | . . . . . . . . . . . . . 14
⊢ (2
· 1) = 2 | 
| 26 | 25 | oveq2i 7442 | . . . . . . . . . . . . 13
⊢ ((2
· 𝑁) − (2
· 1)) = ((2 · 𝑁) − 2) | 
| 27 | 24, 26 | eqtrdi 2793 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (2
· (𝑁 − 1)) =
((2 · 𝑁) −
2)) | 
| 28 | 27 | oveq1d 7446 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((2
· (𝑁 − 1)) +
1) = (((2 · 𝑁)
− 2) + 1)) | 
| 29 | 20, 28 | eqtr4d 2780 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) − (2
− 1)) = ((2 · (𝑁 − 1)) + 1)) | 
| 30 | 14, 29 | eqtr3id 2791 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) − 1) =
((2 · (𝑁 − 1))
+ 1)) | 
| 31 |  | 2nn0 12543 | . . . . . . . . . . 11
⊢ 2 ∈
ℕ0 | 
| 32 |  | nnm1nn0 12567 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) | 
| 33 |  | nn0mulcl 12562 | . . . . . . . . . . 11
⊢ ((2
∈ ℕ0 ∧ (𝑁 − 1) ∈ ℕ0)
→ (2 · (𝑁
− 1)) ∈ ℕ0) | 
| 34 | 31, 32, 33 | sylancr 587 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (2
· (𝑁 − 1))
∈ ℕ0) | 
| 35 |  | nn0p1nn 12565 | . . . . . . . . . 10
⊢ ((2
· (𝑁 − 1))
∈ ℕ0 → ((2 · (𝑁 − 1)) + 1) ∈
ℕ) | 
| 36 | 34, 35 | syl 17 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ((2
· (𝑁 − 1)) +
1) ∈ ℕ) | 
| 37 | 30, 36 | eqeltrd 2841 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) − 1)
∈ ℕ) | 
| 38 |  | nnnn0 12533 | . . . . . . . 8
⊢ (((2
· 𝑁) − 1)
∈ ℕ → ((2 · 𝑁) − 1) ∈
ℕ0) | 
| 39 | 37, 38 | syl 17 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) − 1)
∈ ℕ0) | 
| 40 |  | 1re 11261 | . . . . . . . . . . 11
⊢ 1 ∈
ℝ | 
| 41 | 40 | a1i 11 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 1 ∈
ℝ) | 
| 42 |  | nnge1 12294 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 1 ≤
𝑁) | 
| 43 | 41, 9, 9, 42 | leadd2dd 11878 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ≤ (𝑁 + 𝑁)) | 
| 44 | 21 | 2timesd 12509 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (2
· 𝑁) = (𝑁 + 𝑁)) | 
| 45 | 43, 44 | breqtrrd 5171 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ≤ (2 · 𝑁)) | 
| 46 |  | leaddsub 11739 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 1 ∈
ℝ ∧ (2 · 𝑁) ∈ ℝ) → ((𝑁 + 1) ≤ (2 · 𝑁) ↔ 𝑁 ≤ ((2 · 𝑁) − 1))) | 
| 47 | 9, 41, 4, 46 | syl3anc 1373 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) ≤ (2 · 𝑁) ↔ 𝑁 ≤ ((2 · 𝑁) − 1))) | 
| 48 | 45, 47 | mpbid 232 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ≤ ((2 · 𝑁) − 1)) | 
| 49 |  | elfz2nn0 13658 | . . . . . . 7
⊢ (𝑁 ∈ (0...((2 · 𝑁) − 1)) ↔ (𝑁 ∈ ℕ0
∧ ((2 · 𝑁)
− 1) ∈ ℕ0 ∧ 𝑁 ≤ ((2 · 𝑁) − 1))) | 
| 50 | 12, 39, 48, 49 | syl3anbrc 1344 | . . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (0...((2 · 𝑁) − 1))) | 
| 51 |  | bccl2 14362 | . . . . . 6
⊢ (𝑁 ∈ (0...((2 · 𝑁) − 1)) → (((2
· 𝑁) −
1)C𝑁) ∈
ℕ) | 
| 52 | 50, 51 | syl 17 | . . . . 5
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) −
1)C𝑁) ∈
ℕ) | 
| 53 | 52 | nnrpd 13075 | . . . 4
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) −
1)C𝑁) ∈
ℝ+) | 
| 54 | 53 | relogcld 26665 | . . 3
⊢ (𝑁 ∈ ℕ →
(log‘(((2 · 𝑁)
− 1)C𝑁)) ∈
ℝ) | 
| 55 | 11, 54 | readdcld 11290 | . 2
⊢ (𝑁 ∈ ℕ →
((θ‘𝑁) +
(log‘(((2 · 𝑁)
− 1)C𝑁))) ∈
ℝ) | 
| 56 |  | 4re 12350 | . . . . . 6
⊢ 4 ∈
ℝ | 
| 57 |  | 4pos 12373 | . . . . . 6
⊢ 0 <
4 | 
| 58 | 56, 57 | elrpii 13037 | . . . . 5
⊢ 4 ∈
ℝ+ | 
| 59 |  | relogcl 26617 | . . . . 5
⊢ (4 ∈
ℝ+ → (log‘4) ∈ ℝ) | 
| 60 | 58, 59 | ax-mp 5 | . . . 4
⊢
(log‘4) ∈ ℝ | 
| 61 | 32 | nn0red 12588 | . . . 4
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℝ) | 
| 62 |  | remulcl 11240 | . . . 4
⊢
(((log‘4) ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ) →
((log‘4) · (𝑁
− 1)) ∈ ℝ) | 
| 63 | 60, 61, 62 | sylancr 587 | . . 3
⊢ (𝑁 ∈ ℕ →
((log‘4) · (𝑁
− 1)) ∈ ℝ) | 
| 64 | 11, 63 | readdcld 11290 | . 2
⊢ (𝑁 ∈ ℕ →
((θ‘𝑁) +
((log‘4) · (𝑁
− 1))) ∈ ℝ) | 
| 65 |  | iftrue 4531 | . . . . . . . . . . . 12
⊢ (𝑝 ≤ ((2 · 𝑁) − 1) → if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) =
1) | 
| 66 | 65 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ ((2 · 𝑁) − 1)) → if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) =
1) | 
| 67 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℙ) | 
| 68 | 52 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (((2
· 𝑁) −
1)C𝑁) ∈
ℕ) | 
| 69 | 67, 68 | pccld 16888 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)) ∈
ℕ0) | 
| 70 |  | nn0addge1 12572 | . . . . . . . . . . . . . . 15
⊢ ((1
∈ ℝ ∧ (𝑝
pCnt (((2 · 𝑁)
− 1)C𝑁)) ∈
ℕ0) → 1 ≤ (1 + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))) | 
| 71 | 40, 69, 70 | sylancr 587 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 1 ≤
(1 + (𝑝 pCnt (((2 ·
𝑁) − 1)C𝑁)))) | 
| 72 |  | iftrue 4531 | . . . . . . . . . . . . . . . 16
⊢ (𝑝 ≤ 𝑁 → if(𝑝 ≤ 𝑁, 1, 0) = 1) | 
| 73 | 72 | oveq1d 7446 | . . . . . . . . . . . . . . 15
⊢ (𝑝 ≤ 𝑁 → (if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) = (1 + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))) | 
| 74 | 73 | breq2d 5155 | . . . . . . . . . . . . . 14
⊢ (𝑝 ≤ 𝑁 → (1 ≤ (if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) ↔ 1 ≤ (1 + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))) | 
| 75 | 71, 74 | syl5ibrcom 247 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 ≤ 𝑁 → 1 ≤ (if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))) | 
| 76 | 75 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ ((2 · 𝑁) − 1)) → (𝑝 ≤ 𝑁 → 1 ≤ (if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))) | 
| 77 |  | prmnn 16711 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) | 
| 78 | 77 | ad2antlr 727 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → 𝑝 ∈ ℕ) | 
| 79 |  | simprl 771 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → 𝑝 ≤ ((2 · 𝑁) − 1)) | 
| 80 |  | prmz 16712 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℤ) | 
| 81 | 37 | nnzd 12640 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) − 1)
∈ ℤ) | 
| 82 |  | eluz 12892 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑝 ∈ ℤ ∧ ((2
· 𝑁) − 1)
∈ ℤ) → (((2 · 𝑁) − 1) ∈
(ℤ≥‘𝑝) ↔ 𝑝 ≤ ((2 · 𝑁) − 1))) | 
| 83 | 80, 81, 82 | syl2anr 597 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (((2
· 𝑁) − 1)
∈ (ℤ≥‘𝑝) ↔ 𝑝 ≤ ((2 · 𝑁) − 1))) | 
| 84 | 83 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → (((2 · 𝑁) − 1) ∈
(ℤ≥‘𝑝) ↔ 𝑝 ≤ ((2 · 𝑁) − 1))) | 
| 85 | 79, 84 | mpbird 257 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → ((2 · 𝑁) − 1) ∈
(ℤ≥‘𝑝)) | 
| 86 |  | dvdsfac 16363 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑝 ∈ ℕ ∧ ((2
· 𝑁) − 1)
∈ (ℤ≥‘𝑝)) → 𝑝 ∥ (!‘((2 · 𝑁) − 1))) | 
| 87 | 78, 85, 86 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → 𝑝 ∥ (!‘((2 · 𝑁) − 1))) | 
| 88 |  | id 22 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℙ) | 
| 89 | 39 | faccld 14323 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ →
(!‘((2 · 𝑁)
− 1)) ∈ ℕ) | 
| 90 |  | pcelnn 16908 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑝 ∈ ℙ ∧
(!‘((2 · 𝑁)
− 1)) ∈ ℕ) → ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) ∈ ℕ ↔ 𝑝 ∥ (!‘((2 ·
𝑁) −
1)))) | 
| 91 | 88, 89, 90 | syl2anr 597 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt (!‘((2 ·
𝑁) − 1))) ∈
ℕ ↔ 𝑝 ∥
(!‘((2 · 𝑁)
− 1)))) | 
| 92 | 91 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) ∈ ℕ ↔ 𝑝 ∥ (!‘((2 ·
𝑁) −
1)))) | 
| 93 | 87, 92 | mpbird 257 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → (𝑝 pCnt (!‘((2 · 𝑁) − 1))) ∈
ℕ) | 
| 94 | 93 | nnge1d 12314 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → 1 ≤ (𝑝 pCnt (!‘((2 · 𝑁) − 1)))) | 
| 95 |  | iffalse 4534 | . . . . . . . . . . . . . . . . 17
⊢ (¬
𝑝 ≤ 𝑁 → if(𝑝 ≤ 𝑁, 1, 0) = 0) | 
| 96 | 95 | oveq1d 7446 | . . . . . . . . . . . . . . . 16
⊢ (¬
𝑝 ≤ 𝑁 → (if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) = (0 + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))) | 
| 97 | 96 | ad2antll 729 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → (if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) = (0 + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))) | 
| 98 | 69 | nn0cnd 12589 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)) ∈ ℂ) | 
| 99 | 98 | addlidd 11462 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (0 +
(𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) = (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) | 
| 100 | 99 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → (0 + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) = (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) | 
| 101 |  | bcval2 14344 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ (0...((2 · 𝑁) − 1)) → (((2
· 𝑁) −
1)C𝑁) = ((!‘((2
· 𝑁) − 1)) /
((!‘(((2 · 𝑁)
− 1) − 𝑁))
· (!‘𝑁)))) | 
| 102 | 50, 101 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) −
1)C𝑁) = ((!‘((2
· 𝑁) − 1)) /
((!‘(((2 · 𝑁)
− 1) − 𝑁))
· (!‘𝑁)))) | 
| 103 | 32 | nn0cnd 12589 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℂ) | 
| 104 | 17 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → 1 ∈
ℂ) | 
| 105 | 44 | oveq1d 7446 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) − 1) =
((𝑁 + 𝑁) − 1)) | 
| 106 | 21, 21, 104, 105 | assraddsubd 11677 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) − 1) =
(𝑁 + (𝑁 − 1))) | 
| 107 | 21, 103, 106 | mvrladdd 11676 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) − 1)
− 𝑁) = (𝑁 − 1)) | 
| 108 | 107 | fveq2d 6910 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ →
(!‘(((2 · 𝑁)
− 1) − 𝑁)) =
(!‘(𝑁 −
1))) | 
| 109 | 108 | oveq1d 7446 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ →
((!‘(((2 · 𝑁)
− 1) − 𝑁))
· (!‘𝑁)) =
((!‘(𝑁 − 1))
· (!‘𝑁))) | 
| 110 | 109 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ →
((!‘((2 · 𝑁)
− 1)) / ((!‘(((2 · 𝑁) − 1) − 𝑁)) · (!‘𝑁))) = ((!‘((2 · 𝑁) − 1)) / ((!‘(𝑁 − 1)) ·
(!‘𝑁)))) | 
| 111 | 102, 110 | eqtrd 2777 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) −
1)C𝑁) = ((!‘((2
· 𝑁) − 1)) /
((!‘(𝑁 − 1))
· (!‘𝑁)))) | 
| 112 | 111 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (((2
· 𝑁) −
1)C𝑁) = ((!‘((2
· 𝑁) − 1)) /
((!‘(𝑁 − 1))
· (!‘𝑁)))) | 
| 113 | 112 | oveq2d 7447 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)) = (𝑝 pCnt ((!‘((2 · 𝑁) − 1)) / ((!‘(𝑁 − 1)) ·
(!‘𝑁))))) | 
| 114 |  | nnz 12634 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((!‘((2 · 𝑁) − 1)) ∈ ℕ →
(!‘((2 · 𝑁)
− 1)) ∈ ℤ) | 
| 115 |  | nnne0 12300 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((!‘((2 · 𝑁) − 1)) ∈ ℕ →
(!‘((2 · 𝑁)
− 1)) ≠ 0) | 
| 116 | 114, 115 | jca 511 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((!‘((2 · 𝑁) − 1)) ∈ ℕ →
((!‘((2 · 𝑁)
− 1)) ∈ ℤ ∧ (!‘((2 · 𝑁) − 1)) ≠ 0)) | 
| 117 | 89, 116 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ →
((!‘((2 · 𝑁)
− 1)) ∈ ℤ ∧ (!‘((2 · 𝑁) − 1)) ≠ 0)) | 
| 118 | 117 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
((!‘((2 · 𝑁)
− 1)) ∈ ℤ ∧ (!‘((2 · 𝑁) − 1)) ≠ 0)) | 
| 119 | 32 | faccld 14323 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ →
(!‘(𝑁 − 1))
∈ ℕ) | 
| 120 | 12 | faccld 14323 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ →
(!‘𝑁) ∈
ℕ) | 
| 121 | 119, 120 | nnmulcld 12319 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ →
((!‘(𝑁 − 1))
· (!‘𝑁))
∈ ℕ) | 
| 122 | 121 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
((!‘(𝑁 − 1))
· (!‘𝑁))
∈ ℕ) | 
| 123 |  | pcdiv 16890 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑝 ∈ ℙ ∧
((!‘((2 · 𝑁)
− 1)) ∈ ℤ ∧ (!‘((2 · 𝑁) − 1)) ≠ 0) ∧ ((!‘(𝑁 − 1)) ·
(!‘𝑁)) ∈
ℕ) → (𝑝 pCnt
((!‘((2 · 𝑁)
− 1)) / ((!‘(𝑁
− 1)) · (!‘𝑁)))) = ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − (𝑝 pCnt ((!‘(𝑁 − 1)) · (!‘𝑁))))) | 
| 124 | 67, 118, 122, 123 | syl3anc 1373 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((!‘((2 ·
𝑁) − 1)) /
((!‘(𝑁 − 1))
· (!‘𝑁)))) =
((𝑝 pCnt (!‘((2
· 𝑁) − 1)))
− (𝑝 pCnt
((!‘(𝑁 − 1))
· (!‘𝑁))))) | 
| 125 |  | nnz 12634 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((!‘(𝑁 −
1)) ∈ ℕ → (!‘(𝑁 − 1)) ∈
ℤ) | 
| 126 |  | nnne0 12300 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((!‘(𝑁 −
1)) ∈ ℕ → (!‘(𝑁 − 1)) ≠ 0) | 
| 127 | 125, 126 | jca 511 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((!‘(𝑁 −
1)) ∈ ℕ → ((!‘(𝑁 − 1)) ∈ ℤ ∧
(!‘(𝑁 − 1))
≠ 0)) | 
| 128 | 119, 127 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ →
((!‘(𝑁 − 1))
∈ ℤ ∧ (!‘(𝑁 − 1)) ≠ 0)) | 
| 129 | 128 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
((!‘(𝑁 − 1))
∈ ℤ ∧ (!‘(𝑁 − 1)) ≠ 0)) | 
| 130 |  | nnz 12634 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((!‘𝑁) ∈
ℕ → (!‘𝑁)
∈ ℤ) | 
| 131 |  | nnne0 12300 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((!‘𝑁) ∈
ℕ → (!‘𝑁)
≠ 0) | 
| 132 | 130, 131 | jca 511 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((!‘𝑁) ∈
ℕ → ((!‘𝑁)
∈ ℤ ∧ (!‘𝑁) ≠ 0)) | 
| 133 | 120, 132 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ →
((!‘𝑁) ∈ ℤ
∧ (!‘𝑁) ≠
0)) | 
| 134 | 133 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
((!‘𝑁) ∈ ℤ
∧ (!‘𝑁) ≠
0)) | 
| 135 |  | pcmul 16889 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑝 ∈ ℙ ∧
((!‘(𝑁 − 1))
∈ ℤ ∧ (!‘(𝑁 − 1)) ≠ 0) ∧ ((!‘𝑁) ∈ ℤ ∧
(!‘𝑁) ≠ 0)) →
(𝑝 pCnt ((!‘(𝑁 − 1)) ·
(!‘𝑁))) = ((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁)))) | 
| 136 | 67, 129, 134, 135 | syl3anc 1373 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((!‘(𝑁 − 1)) ·
(!‘𝑁))) = ((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁)))) | 
| 137 | 136 | oveq2d 7447 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt (!‘((2 ·
𝑁) − 1))) −
(𝑝 pCnt ((!‘(𝑁 − 1)) ·
(!‘𝑁)))) = ((𝑝 pCnt (!‘((2 ·
𝑁) − 1))) −
((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁))))) | 
| 138 | 113, 124,
137 | 3eqtrd 2781 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)) = ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − ((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁))))) | 
| 139 | 138 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)) = ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − ((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁))))) | 
| 140 |  | simprr 773 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → ¬ 𝑝 ≤ 𝑁) | 
| 141 |  | prmfac1 16757 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ ℕ0
∧ 𝑝 ∈ ℙ
∧ 𝑝 ∥
(!‘𝑁)) → 𝑝 ≤ 𝑁) | 
| 142 | 141 | 3expia 1122 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℕ0
∧ 𝑝 ∈ ℙ)
→ (𝑝 ∥
(!‘𝑁) → 𝑝 ≤ 𝑁)) | 
| 143 | 12, 142 | sylan 580 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (!‘𝑁) → 𝑝 ≤ 𝑁)) | 
| 144 | 143 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → (𝑝 ∥ (!‘𝑁) → 𝑝 ≤ 𝑁)) | 
| 145 | 140, 144 | mtod 198 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → ¬ 𝑝 ∥ (!‘𝑁)) | 
| 146 | 80 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℤ) | 
| 147 | 129 | simpld 494 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
(!‘(𝑁 − 1))
∈ ℤ) | 
| 148 |  | nnz 12634 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) | 
| 149 | 148 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑁 ∈
ℤ) | 
| 150 |  | dvdsmultr1 16333 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑝 ∈ ℤ ∧
(!‘(𝑁 − 1))
∈ ℤ ∧ 𝑁
∈ ℤ) → (𝑝
∥ (!‘(𝑁 −
1)) → 𝑝 ∥
((!‘(𝑁 − 1))
· 𝑁))) | 
| 151 | 146, 147,
149, 150 | syl3anc 1373 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (!‘(𝑁 − 1)) → 𝑝 ∥ ((!‘(𝑁 − 1)) · 𝑁))) | 
| 152 |  | facnn2 14321 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ →
(!‘𝑁) =
((!‘(𝑁 − 1))
· 𝑁)) | 
| 153 | 152 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
(!‘𝑁) =
((!‘(𝑁 − 1))
· 𝑁)) | 
| 154 | 153 | breq2d 5155 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (!‘𝑁) ↔ 𝑝 ∥ ((!‘(𝑁 − 1)) · 𝑁))) | 
| 155 | 151, 154 | sylibrd 259 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (!‘(𝑁 − 1)) → 𝑝 ∥ (!‘𝑁))) | 
| 156 | 155 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → (𝑝 ∥ (!‘(𝑁 − 1)) → 𝑝 ∥ (!‘𝑁))) | 
| 157 | 145, 156 | mtod 198 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → ¬ 𝑝 ∥ (!‘(𝑁 − 1))) | 
| 158 |  | pceq0 16909 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑝 ∈ ℙ ∧
(!‘(𝑁 − 1))
∈ ℕ) → ((𝑝
pCnt (!‘(𝑁 −
1))) = 0 ↔ ¬ 𝑝
∥ (!‘(𝑁 −
1)))) | 
| 159 | 88, 119, 158 | syl2anr 597 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt (!‘(𝑁 − 1))) = 0 ↔ ¬
𝑝 ∥ (!‘(𝑁 − 1)))) | 
| 160 | 159 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → ((𝑝 pCnt (!‘(𝑁 − 1))) = 0 ↔ ¬ 𝑝 ∥ (!‘(𝑁 − 1)))) | 
| 161 | 157, 160 | mpbird 257 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → (𝑝 pCnt (!‘(𝑁 − 1))) = 0) | 
| 162 |  | pceq0 16909 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑝 ∈ ℙ ∧
(!‘𝑁) ∈ ℕ)
→ ((𝑝 pCnt
(!‘𝑁)) = 0 ↔
¬ 𝑝 ∥
(!‘𝑁))) | 
| 163 | 88, 120, 162 | syl2anr 597 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt (!‘𝑁)) = 0 ↔ ¬ 𝑝 ∥ (!‘𝑁))) | 
| 164 | 163 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → ((𝑝 pCnt (!‘𝑁)) = 0 ↔ ¬ 𝑝 ∥ (!‘𝑁))) | 
| 165 | 145, 164 | mpbird 257 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → (𝑝 pCnt (!‘𝑁)) = 0) | 
| 166 | 161, 165 | oveq12d 7449 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → ((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁))) = (0 + 0)) | 
| 167 |  | 00id 11436 | . . . . . . . . . . . . . . . . . 18
⊢ (0 + 0) =
0 | 
| 168 | 166, 167 | eqtrdi 2793 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → ((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁))) = 0) | 
| 169 | 168 | oveq2d 7447 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − ((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁)))) = ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − 0)) | 
| 170 |  | pccl 16887 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑝 ∈ ℙ ∧
(!‘((2 · 𝑁)
− 1)) ∈ ℕ) → (𝑝 pCnt (!‘((2 · 𝑁) − 1))) ∈
ℕ0) | 
| 171 | 88, 89, 170 | syl2anr 597 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (!‘((2 ·
𝑁) − 1))) ∈
ℕ0) | 
| 172 | 171 | nn0cnd 12589 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (!‘((2 ·
𝑁) − 1))) ∈
ℂ) | 
| 173 | 172 | subid1d 11609 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt (!‘((2 ·
𝑁) − 1))) − 0)
= (𝑝 pCnt (!‘((2
· 𝑁) −
1)))) | 
| 174 | 173 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − 0) = (𝑝 pCnt (!‘((2 ·
𝑁) −
1)))) | 
| 175 | 139, 169,
174 | 3eqtrd 2781 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)) = (𝑝 pCnt (!‘((2 · 𝑁) − 1)))) | 
| 176 | 97, 100, 175 | 3eqtrd 2781 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → (if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) = (𝑝 pCnt (!‘((2 · 𝑁) − 1)))) | 
| 177 | 94, 176 | breqtrrd 5171 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → 1 ≤ (if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))) | 
| 178 | 177 | expr 456 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ ((2 · 𝑁) − 1)) → (¬
𝑝 ≤ 𝑁 → 1 ≤ (if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))) | 
| 179 | 76, 178 | pm2.61d 179 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ ((2 · 𝑁) − 1)) → 1 ≤
(if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))) | 
| 180 | 66, 179 | eqbrtrd 5165 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ ((2 · 𝑁) − 1)) → if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) ≤
(if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))) | 
| 181 | 180 | ex 412 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 ≤ ((2 · 𝑁) − 1) → if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) ≤
(if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))) | 
| 182 |  | 1nn0 12542 | . . . . . . . . . . . . 13
⊢ 1 ∈
ℕ0 | 
| 183 |  | 0nn0 12541 | . . . . . . . . . . . . 13
⊢ 0 ∈
ℕ0 | 
| 184 | 182, 183 | ifcli 4573 | . . . . . . . . . . . 12
⊢ if(𝑝 ≤ 𝑁, 1, 0) ∈
ℕ0 | 
| 185 |  | nn0addcl 12561 | . . . . . . . . . . . 12
⊢
((if(𝑝 ≤ 𝑁, 1, 0) ∈
ℕ0 ∧ (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)) ∈ ℕ0) →
(if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) ∈
ℕ0) | 
| 186 | 184, 69, 185 | sylancr 587 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
(if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) ∈
ℕ0) | 
| 187 | 186 | nn0ge0d 12590 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 0 ≤
(if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))) | 
| 188 |  | iffalse 4534 | . . . . . . . . . . 11
⊢ (¬
𝑝 ≤ ((2 · 𝑁) − 1) → if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) =
0) | 
| 189 | 188 | breq1d 5153 | . . . . . . . . . 10
⊢ (¬
𝑝 ≤ ((2 · 𝑁) − 1) → (if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) ≤
(if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) ↔ 0 ≤ (if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))) | 
| 190 | 187, 189 | syl5ibrcom 247 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (¬
𝑝 ≤ ((2 · 𝑁) − 1) → if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) ≤
(if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))) | 
| 191 | 181, 190 | pm2.61d 179 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) ≤
(if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))) | 
| 192 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) | 
| 193 | 192 | prmorcht 27221 | . . . . . . . . . . . 12
⊢ (((2
· 𝑁) − 1)
∈ ℕ → (exp‘(θ‘((2 · 𝑁) − 1))) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘((2 · 𝑁) − 1))) | 
| 194 | 37, 193 | syl 17 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
(exp‘(θ‘((2 · 𝑁) − 1))) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘((2 · 𝑁) − 1))) | 
| 195 | 194 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (𝑝 pCnt
(exp‘(θ‘((2 · 𝑁) − 1)))) = (𝑝 pCnt (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘((2 · 𝑁) − 1)))) | 
| 196 | 195 | adantr 480 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt
(exp‘(θ‘((2 · 𝑁) − 1)))) = (𝑝 pCnt (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘((2 · 𝑁) − 1)))) | 
| 197 |  | nncn 12274 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) | 
| 198 | 197 | exp1d 14181 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (𝑛↑1) = 𝑛) | 
| 199 | 198 | ifeq1d 4545 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → if(𝑛 ∈ ℙ, (𝑛↑1), 1) = if(𝑛 ∈ ℙ, 𝑛, 1)) | 
| 200 | 199 | mpteq2ia 5245 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑1), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) | 
| 201 | 200 | eqcomi 2746 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑1), 1)) | 
| 202 | 182 | a1i 11 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑛 ∈ ℙ) → 1 ∈
ℕ0) | 
| 203 | 202 | ralrimiva 3146 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
∀𝑛 ∈ ℙ 1
∈ ℕ0) | 
| 204 | 37 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((2
· 𝑁) − 1)
∈ ℕ) | 
| 205 |  | eqidd 2738 | . . . . . . . . . 10
⊢ (𝑛 = 𝑝 → 1 = 1) | 
| 206 | 201, 203,
204, 67, 205 | pcmpt 16930 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘((2 · 𝑁) − 1))) = if(𝑝 ≤ ((2 · 𝑁) − 1), 1,
0)) | 
| 207 | 196, 206 | eqtrd 2777 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt
(exp‘(θ‘((2 · 𝑁) − 1)))) = if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0)) | 
| 208 |  | efchtcl 27154 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℝ →
(exp‘(θ‘𝑁)) ∈ ℕ) | 
| 209 | 9, 208 | syl 17 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ →
(exp‘(θ‘𝑁)) ∈ ℕ) | 
| 210 | 209 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
(exp‘(θ‘𝑁)) ∈ ℕ) | 
| 211 |  | nnz 12634 | . . . . . . . . . . . 12
⊢
((exp‘(θ‘𝑁)) ∈ ℕ →
(exp‘(θ‘𝑁)) ∈ ℤ) | 
| 212 |  | nnne0 12300 | . . . . . . . . . . . 12
⊢
((exp‘(θ‘𝑁)) ∈ ℕ →
(exp‘(θ‘𝑁)) ≠ 0) | 
| 213 | 211, 212 | jca 511 | . . . . . . . . . . 11
⊢
((exp‘(θ‘𝑁)) ∈ ℕ →
((exp‘(θ‘𝑁)) ∈ ℤ ∧
(exp‘(θ‘𝑁)) ≠ 0)) | 
| 214 | 210, 213 | syl 17 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
((exp‘(θ‘𝑁)) ∈ ℤ ∧
(exp‘(θ‘𝑁)) ≠ 0)) | 
| 215 |  | nnz 12634 | . . . . . . . . . . . 12
⊢ ((((2
· 𝑁) −
1)C𝑁) ∈ ℕ →
(((2 · 𝑁) −
1)C𝑁) ∈
ℤ) | 
| 216 |  | nnne0 12300 | . . . . . . . . . . . 12
⊢ ((((2
· 𝑁) −
1)C𝑁) ∈ ℕ →
(((2 · 𝑁) −
1)C𝑁) ≠
0) | 
| 217 | 215, 216 | jca 511 | . . . . . . . . . . 11
⊢ ((((2
· 𝑁) −
1)C𝑁) ∈ ℕ →
((((2 · 𝑁) −
1)C𝑁) ∈ ℤ ∧
(((2 · 𝑁) −
1)C𝑁) ≠
0)) | 
| 218 | 68, 217 | syl 17 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((((2
· 𝑁) −
1)C𝑁) ∈ ℤ ∧
(((2 · 𝑁) −
1)C𝑁) ≠
0)) | 
| 219 |  | pcmul 16889 | . . . . . . . . . 10
⊢ ((𝑝 ∈ ℙ ∧
((exp‘(θ‘𝑁)) ∈ ℤ ∧
(exp‘(θ‘𝑁)) ≠ 0) ∧ ((((2 · 𝑁) − 1)C𝑁) ∈ ℤ ∧ (((2 · 𝑁) − 1)C𝑁) ≠ 0)) → (𝑝 pCnt ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))) = ((𝑝 pCnt (exp‘(θ‘𝑁))) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))) | 
| 220 | 67, 214, 218, 219 | syl3anc 1373 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt
((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))) = ((𝑝 pCnt (exp‘(θ‘𝑁))) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))) | 
| 221 | 192 | prmorcht 27221 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ →
(exp‘(θ‘𝑁)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑁)) | 
| 222 | 221 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (𝑝 pCnt
(exp‘(θ‘𝑁))) = (𝑝 pCnt (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑁))) | 
| 223 | 222 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt
(exp‘(θ‘𝑁))) = (𝑝 pCnt (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑁))) | 
| 224 |  | simpl 482 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑁 ∈
ℕ) | 
| 225 | 201, 203,
224, 67, 205 | pcmpt 16930 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑁)) = if(𝑝 ≤ 𝑁, 1, 0)) | 
| 226 | 223, 225 | eqtrd 2777 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt
(exp‘(θ‘𝑁))) = if(𝑝 ≤ 𝑁, 1, 0)) | 
| 227 | 226 | oveq1d 7446 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt
(exp‘(θ‘𝑁))) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) = (if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))) | 
| 228 | 220, 227 | eqtrd 2777 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt
((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))) = (if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))) | 
| 229 | 191, 207,
228 | 3brtr4d 5175 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt
(exp‘(θ‘((2 · 𝑁) − 1)))) ≤ (𝑝 pCnt ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)))) | 
| 230 | 229 | ralrimiva 3146 | . . . . . 6
⊢ (𝑁 ∈ ℕ →
∀𝑝 ∈ ℙ
(𝑝 pCnt
(exp‘(θ‘((2 · 𝑁) − 1)))) ≤ (𝑝 pCnt ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)))) | 
| 231 |  | efchtcl 27154 | . . . . . . . . 9
⊢ (((2
· 𝑁) − 1)
∈ ℝ → (exp‘(θ‘((2 · 𝑁) − 1))) ∈
ℕ) | 
| 232 | 6, 231 | syl 17 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(exp‘(θ‘((2 · 𝑁) − 1))) ∈
ℕ) | 
| 233 | 232 | nnzd 12640 | . . . . . . 7
⊢ (𝑁 ∈ ℕ →
(exp‘(θ‘((2 · 𝑁) − 1))) ∈
ℤ) | 
| 234 | 209, 52 | nnmulcld 12319 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ →
((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) ∈ ℕ) | 
| 235 | 234 | nnzd 12640 | . . . . . . 7
⊢ (𝑁 ∈ ℕ →
((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) ∈ ℤ) | 
| 236 |  | pc2dvds 16917 | . . . . . . 7
⊢
(((exp‘(θ‘((2 · 𝑁) − 1))) ∈ ℤ ∧
((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) ∈ ℤ) →
((exp‘(θ‘((2 · 𝑁) − 1))) ∥
((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt (exp‘(θ‘((2 ·
𝑁) − 1)))) ≤
(𝑝 pCnt
((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))))) | 
| 237 | 233, 235,
236 | syl2anc 584 | . . . . . 6
⊢ (𝑁 ∈ ℕ →
((exp‘(θ‘((2 · 𝑁) − 1))) ∥
((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt (exp‘(θ‘((2 ·
𝑁) − 1)))) ≤
(𝑝 pCnt
((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))))) | 
| 238 | 230, 237 | mpbird 257 | . . . . 5
⊢ (𝑁 ∈ ℕ →
(exp‘(θ‘((2 · 𝑁) − 1))) ∥
((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))) | 
| 239 |  | dvdsle 16347 | . . . . . 6
⊢
(((exp‘(θ‘((2 · 𝑁) − 1))) ∈ ℤ ∧
((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) ∈ ℕ) →
((exp‘(θ‘((2 · 𝑁) − 1))) ∥
((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) → (exp‘(θ‘((2
· 𝑁) − 1)))
≤ ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)))) | 
| 240 | 233, 234,
239 | syl2anc 584 | . . . . 5
⊢ (𝑁 ∈ ℕ →
((exp‘(θ‘((2 · 𝑁) − 1))) ∥
((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) → (exp‘(θ‘((2
· 𝑁) − 1)))
≤ ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)))) | 
| 241 | 238, 240 | mpd 15 | . . . 4
⊢ (𝑁 ∈ ℕ →
(exp‘(θ‘((2 · 𝑁) − 1))) ≤
((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))) | 
| 242 | 11 | recnd 11289 | . . . . . 6
⊢ (𝑁 ∈ ℕ →
(θ‘𝑁) ∈
ℂ) | 
| 243 | 54 | recnd 11289 | . . . . . 6
⊢ (𝑁 ∈ ℕ →
(log‘(((2 · 𝑁)
− 1)C𝑁)) ∈
ℂ) | 
| 244 |  | efadd 16130 | . . . . . 6
⊢
(((θ‘𝑁)
∈ ℂ ∧ (log‘(((2 · 𝑁) − 1)C𝑁)) ∈ ℂ) →
(exp‘((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁)))) = ((exp‘(θ‘𝑁)) ·
(exp‘(log‘(((2 · 𝑁) − 1)C𝑁))))) | 
| 245 | 242, 243,
244 | syl2anc 584 | . . . . 5
⊢ (𝑁 ∈ ℕ →
(exp‘((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁)))) = ((exp‘(θ‘𝑁)) ·
(exp‘(log‘(((2 · 𝑁) − 1)C𝑁))))) | 
| 246 | 53 | reeflogd 26666 | . . . . . 6
⊢ (𝑁 ∈ ℕ →
(exp‘(log‘(((2 · 𝑁) − 1)C𝑁))) = (((2 · 𝑁) − 1)C𝑁)) | 
| 247 | 246 | oveq2d 7447 | . . . . 5
⊢ (𝑁 ∈ ℕ →
((exp‘(θ‘𝑁)) · (exp‘(log‘(((2
· 𝑁) −
1)C𝑁)))) =
((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))) | 
| 248 | 245, 247 | eqtrd 2777 | . . . 4
⊢ (𝑁 ∈ ℕ →
(exp‘((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁)))) = ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))) | 
| 249 | 241, 248 | breqtrrd 5171 | . . 3
⊢ (𝑁 ∈ ℕ →
(exp‘(θ‘((2 · 𝑁) − 1))) ≤
(exp‘((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁))))) | 
| 250 |  | efle 16154 | . . . 4
⊢
(((θ‘((2 · 𝑁) − 1)) ∈ ℝ ∧
((θ‘𝑁) +
(log‘(((2 · 𝑁)
− 1)C𝑁))) ∈
ℝ) → ((θ‘((2 · 𝑁) − 1)) ≤ ((θ‘𝑁) + (log‘(((2 ·
𝑁) − 1)C𝑁))) ↔
(exp‘(θ‘((2 · 𝑁) − 1))) ≤
(exp‘((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁)))))) | 
| 251 | 8, 55, 250 | syl2anc 584 | . . 3
⊢ (𝑁 ∈ ℕ →
((θ‘((2 · 𝑁) − 1)) ≤ ((θ‘𝑁) + (log‘(((2 ·
𝑁) − 1)C𝑁))) ↔
(exp‘(θ‘((2 · 𝑁) − 1))) ≤
(exp‘((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁)))))) | 
| 252 | 249, 251 | mpbird 257 | . 2
⊢ (𝑁 ∈ ℕ →
(θ‘((2 · 𝑁) − 1)) ≤ ((θ‘𝑁) + (log‘(((2 ·
𝑁) − 1)C𝑁)))) | 
| 253 |  | fzfid 14014 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (0...((2
· 𝑁) − 1))
∈ Fin) | 
| 254 |  | elfzelz 13564 | . . . . . . . . . . 11
⊢ (𝑘 ∈ (0...((2 · 𝑁) − 1)) → 𝑘 ∈
ℤ) | 
| 255 |  | bccl 14361 | . . . . . . . . . . 11
⊢ ((((2
· 𝑁) − 1)
∈ ℕ0 ∧ 𝑘 ∈ ℤ) → (((2 · 𝑁) − 1)C𝑘) ∈
ℕ0) | 
| 256 | 39, 254, 255 | syl2an 596 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...((2 · 𝑁) − 1))) → (((2
· 𝑁) −
1)C𝑘) ∈
ℕ0) | 
| 257 | 256 | nn0red 12588 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...((2 · 𝑁) − 1))) → (((2
· 𝑁) −
1)C𝑘) ∈
ℝ) | 
| 258 | 256 | nn0ge0d 12590 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...((2 · 𝑁) − 1))) → 0 ≤
(((2 · 𝑁) −
1)C𝑘)) | 
| 259 |  | nn0uz 12920 | . . . . . . . . . . . 12
⊢
ℕ0 = (ℤ≥‘0) | 
| 260 | 32, 259 | eleqtrdi 2851 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
(ℤ≥‘0)) | 
| 261 |  | fzss1 13603 | . . . . . . . . . . 11
⊢ ((𝑁 − 1) ∈
(ℤ≥‘0) → ((𝑁 − 1)...𝑁) ⊆ (0...𝑁)) | 
| 262 | 260, 261 | syl 17 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1)...𝑁) ⊆ (0...𝑁)) | 
| 263 |  | eluz 12892 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ ((2
· 𝑁) − 1)
∈ ℤ) → (((2 · 𝑁) − 1) ∈
(ℤ≥‘𝑁) ↔ 𝑁 ≤ ((2 · 𝑁) − 1))) | 
| 264 | 148, 81, 263 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) − 1)
∈ (ℤ≥‘𝑁) ↔ 𝑁 ≤ ((2 · 𝑁) − 1))) | 
| 265 | 48, 264 | mpbird 257 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) − 1)
∈ (ℤ≥‘𝑁)) | 
| 266 |  | fzss2 13604 | . . . . . . . . . . 11
⊢ (((2
· 𝑁) − 1)
∈ (ℤ≥‘𝑁) → (0...𝑁) ⊆ (0...((2 · 𝑁) − 1))) | 
| 267 | 265, 266 | syl 17 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(0...𝑁) ⊆ (0...((2
· 𝑁) −
1))) | 
| 268 | 262, 267 | sstrd 3994 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1)...𝑁) ⊆ (0...((2 · 𝑁) − 1))) | 
| 269 | 253, 257,
258, 268 | fsumless 15832 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ ((𝑁 − 1)...𝑁)(((2 · 𝑁) − 1)C𝑘) ≤ Σ𝑘 ∈ (0...((2 · 𝑁) − 1))(((2 · 𝑁) − 1)C𝑘)) | 
| 270 | 32 | nn0zd 12639 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℤ) | 
| 271 |  | bccmpl 14348 | . . . . . . . . . . . . . . 15
⊢ ((((2
· 𝑁) − 1)
∈ ℕ0 ∧ 𝑁 ∈ ℤ) → (((2 · 𝑁) − 1)C𝑁) = (((2 · 𝑁) − 1)C(((2 · 𝑁) − 1) − 𝑁))) | 
| 272 | 39, 148, 271 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) −
1)C𝑁) = (((2 · 𝑁) − 1)C(((2 · 𝑁) − 1) − 𝑁))) | 
| 273 | 107 | oveq2d 7447 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) − 1)C(((2
· 𝑁) − 1)
− 𝑁)) = (((2 ·
𝑁) − 1)C(𝑁 − 1))) | 
| 274 | 272, 273 | eqtrd 2777 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) −
1)C𝑁) = (((2 · 𝑁) − 1)C(𝑁 − 1))) | 
| 275 | 52 | nncnd 12282 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) −
1)C𝑁) ∈
ℂ) | 
| 276 | 274, 275 | eqeltrrd 2842 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) −
1)C(𝑁 − 1)) ∈
ℂ) | 
| 277 |  | oveq2 7439 | . . . . . . . . . . . . 13
⊢ (𝑘 = (𝑁 − 1) → (((2 · 𝑁) − 1)C𝑘) = (((2 · 𝑁) − 1)C(𝑁 − 1))) | 
| 278 | 277 | fsum1 15783 | . . . . . . . . . . . 12
⊢ (((𝑁 − 1) ∈ ℤ ∧
(((2 · 𝑁) −
1)C(𝑁 − 1)) ∈
ℂ) → Σ𝑘
∈ ((𝑁 −
1)...(𝑁 − 1))(((2
· 𝑁) −
1)C𝑘) = (((2 · 𝑁) − 1)C(𝑁 − 1))) | 
| 279 | 270, 276,
278 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ ((𝑁 − 1)...(𝑁 − 1))(((2 · 𝑁) − 1)C𝑘) = (((2 · 𝑁) − 1)C(𝑁 − 1))) | 
| 280 | 279, 274 | eqtr4d 2780 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ ((𝑁 − 1)...(𝑁 − 1))(((2 · 𝑁) − 1)C𝑘) = (((2 · 𝑁) − 1)C𝑁)) | 
| 281 | 280 | oveq1d 7446 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(Σ𝑘 ∈ ((𝑁 − 1)...(𝑁 − 1))(((2 · 𝑁) − 1)C𝑘) + (((2 · 𝑁) − 1)C𝑁)) = ((((2 · 𝑁) − 1)C𝑁) + (((2 · 𝑁) − 1)C𝑁))) | 
| 282 | 21, 104 | npcand 11624 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) + 1) = 𝑁) | 
| 283 |  | uzid 12893 | . . . . . . . . . . . . 13
⊢ ((𝑁 − 1) ∈ ℤ
→ (𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1))) | 
| 284 | 270, 283 | syl 17 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1))) | 
| 285 |  | peano2uz 12943 | . . . . . . . . . . . 12
⊢ ((𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) | 
| 286 | 284, 285 | syl 17 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) | 
| 287 | 282, 286 | eqeltrrd 2842 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
(ℤ≥‘(𝑁 − 1))) | 
| 288 | 268 | sselda 3983 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ((𝑁 − 1)...𝑁)) → 𝑘 ∈ (0...((2 · 𝑁) − 1))) | 
| 289 | 256 | nn0cnd 12589 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...((2 · 𝑁) − 1))) → (((2
· 𝑁) −
1)C𝑘) ∈
ℂ) | 
| 290 | 288, 289 | syldan 591 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ((𝑁 − 1)...𝑁)) → (((2 · 𝑁) − 1)C𝑘) ∈ ℂ) | 
| 291 |  | oveq2 7439 | . . . . . . . . . 10
⊢ (𝑘 = 𝑁 → (((2 · 𝑁) − 1)C𝑘) = (((2 · 𝑁) − 1)C𝑁)) | 
| 292 | 287, 290,
291 | fsumm1 15787 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ ((𝑁 − 1)...𝑁)(((2 · 𝑁) − 1)C𝑘) = (Σ𝑘 ∈ ((𝑁 − 1)...(𝑁 − 1))(((2 · 𝑁) − 1)C𝑘) + (((2 · 𝑁) − 1)C𝑁))) | 
| 293 | 275 | 2timesd 12509 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (2
· (((2 · 𝑁)
− 1)C𝑁)) = ((((2
· 𝑁) −
1)C𝑁) + (((2 · 𝑁) − 1)C𝑁))) | 
| 294 | 281, 292,
293 | 3eqtr4rd 2788 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ → (2
· (((2 · 𝑁)
− 1)C𝑁)) =
Σ𝑘 ∈ ((𝑁 − 1)...𝑁)(((2 · 𝑁) − 1)C𝑘)) | 
| 295 |  | binom11 15868 | . . . . . . . . 9
⊢ (((2
· 𝑁) − 1)
∈ ℕ0 → (2↑((2 · 𝑁) − 1)) = Σ𝑘 ∈ (0...((2 · 𝑁) − 1))(((2 · 𝑁) − 1)C𝑘)) | 
| 296 | 39, 295 | syl 17 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(2↑((2 · 𝑁)
− 1)) = Σ𝑘
∈ (0...((2 · 𝑁)
− 1))(((2 · 𝑁)
− 1)C𝑘)) | 
| 297 | 269, 294,
296 | 3brtr4d 5175 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → (2
· (((2 · 𝑁)
− 1)C𝑁)) ≤
(2↑((2 · 𝑁)
− 1))) | 
| 298 |  | mulcom 11241 | . . . . . . . 8
⊢ ((2
∈ ℂ ∧ (((2 · 𝑁) − 1)C𝑁) ∈ ℂ) → (2 · (((2
· 𝑁) −
1)C𝑁)) = ((((2 ·
𝑁) − 1)C𝑁) · 2)) | 
| 299 | 16, 275, 298 | sylancr 587 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → (2
· (((2 · 𝑁)
− 1)C𝑁)) = ((((2
· 𝑁) −
1)C𝑁) ·
2)) | 
| 300 | 30 | oveq2d 7447 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(2↑((2 · 𝑁)
− 1)) = (2↑((2 · (𝑁 − 1)) + 1))) | 
| 301 |  | expp1 14109 | . . . . . . . . 9
⊢ ((2
∈ ℂ ∧ (2 · (𝑁 − 1)) ∈ ℕ0)
→ (2↑((2 · (𝑁 − 1)) + 1)) = ((2↑(2 ·
(𝑁 − 1))) ·
2)) | 
| 302 | 16, 34, 301 | sylancr 587 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(2↑((2 · (𝑁
− 1)) + 1)) = ((2↑(2 · (𝑁 − 1))) · 2)) | 
| 303 | 16 | a1i 11 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 2 ∈
ℂ) | 
| 304 | 31 | a1i 11 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 2 ∈
ℕ0) | 
| 305 | 303, 32, 304 | expmuld 14189 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(2↑(2 · (𝑁
− 1))) = ((2↑2)↑(𝑁 − 1))) | 
| 306 |  | sq2 14236 | . . . . . . . . . . 11
⊢
(2↑2) = 4 | 
| 307 | 306 | oveq1i 7441 | . . . . . . . . . 10
⊢
((2↑2)↑(𝑁
− 1)) = (4↑(𝑁
− 1)) | 
| 308 | 305, 307 | eqtrdi 2793 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(2↑(2 · (𝑁
− 1))) = (4↑(𝑁
− 1))) | 
| 309 | 308 | oveq1d 7446 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ →
((2↑(2 · (𝑁
− 1))) · 2) = ((4↑(𝑁 − 1)) · 2)) | 
| 310 | 300, 302,
309 | 3eqtrd 2781 | . . . . . . 7
⊢ (𝑁 ∈ ℕ →
(2↑((2 · 𝑁)
− 1)) = ((4↑(𝑁
− 1)) · 2)) | 
| 311 | 297, 299,
310 | 3brtr3d 5174 | . . . . . 6
⊢ (𝑁 ∈ ℕ → ((((2
· 𝑁) −
1)C𝑁) · 2) ≤
((4↑(𝑁 − 1))
· 2)) | 
| 312 | 52 | nnred 12281 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) −
1)C𝑁) ∈
ℝ) | 
| 313 |  | reexpcl 14119 | . . . . . . . 8
⊢ ((4
∈ ℝ ∧ (𝑁
− 1) ∈ ℕ0) → (4↑(𝑁 − 1)) ∈
ℝ) | 
| 314 | 56, 32, 313 | sylancr 587 | . . . . . . 7
⊢ (𝑁 ∈ ℕ →
(4↑(𝑁 − 1))
∈ ℝ) | 
| 315 |  | 2re 12340 | . . . . . . . . 9
⊢ 2 ∈
ℝ | 
| 316 |  | 2pos 12369 | . . . . . . . . 9
⊢ 0 <
2 | 
| 317 | 315, 316 | pm3.2i 470 | . . . . . . . 8
⊢ (2 ∈
ℝ ∧ 0 < 2) | 
| 318 | 317 | a1i 11 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → (2 ∈
ℝ ∧ 0 < 2)) | 
| 319 |  | lemul1 12119 | . . . . . . 7
⊢ (((((2
· 𝑁) −
1)C𝑁) ∈ ℝ ∧
(4↑(𝑁 − 1))
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((((2 ·
𝑁) − 1)C𝑁) ≤ (4↑(𝑁 − 1)) ↔ ((((2
· 𝑁) −
1)C𝑁) · 2) ≤
((4↑(𝑁 − 1))
· 2))) | 
| 320 | 312, 314,
318, 319 | syl3anc 1373 | . . . . . 6
⊢ (𝑁 ∈ ℕ → ((((2
· 𝑁) −
1)C𝑁) ≤ (4↑(𝑁 − 1)) ↔ ((((2
· 𝑁) −
1)C𝑁) · 2) ≤
((4↑(𝑁 − 1))
· 2))) | 
| 321 | 311, 320 | mpbird 257 | . . . . 5
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) −
1)C𝑁) ≤ (4↑(𝑁 − 1))) | 
| 322 | 60 | recni 11275 | . . . . . . . 8
⊢
(log‘4) ∈ ℂ | 
| 323 |  | mulcom 11241 | . . . . . . . 8
⊢
(((log‘4) ∈ ℂ ∧ (𝑁 − 1) ∈ ℂ) →
((log‘4) · (𝑁
− 1)) = ((𝑁 −
1) · (log‘4))) | 
| 324 | 322, 103,
323 | sylancr 587 | . . . . . . 7
⊢ (𝑁 ∈ ℕ →
((log‘4) · (𝑁
− 1)) = ((𝑁 −
1) · (log‘4))) | 
| 325 | 324 | fveq2d 6910 | . . . . . 6
⊢ (𝑁 ∈ ℕ →
(exp‘((log‘4) · (𝑁 − 1))) = (exp‘((𝑁 − 1) ·
(log‘4)))) | 
| 326 |  | reexplog 26637 | . . . . . . 7
⊢ ((4
∈ ℝ+ ∧ (𝑁 − 1) ∈ ℤ) →
(4↑(𝑁 − 1)) =
(exp‘((𝑁 − 1)
· (log‘4)))) | 
| 327 | 58, 270, 326 | sylancr 587 | . . . . . 6
⊢ (𝑁 ∈ ℕ →
(4↑(𝑁 − 1)) =
(exp‘((𝑁 − 1)
· (log‘4)))) | 
| 328 | 325, 327 | eqtr4d 2780 | . . . . 5
⊢ (𝑁 ∈ ℕ →
(exp‘((log‘4) · (𝑁 − 1))) = (4↑(𝑁 − 1))) | 
| 329 | 321, 246,
328 | 3brtr4d 5175 | . . . 4
⊢ (𝑁 ∈ ℕ →
(exp‘(log‘(((2 · 𝑁) − 1)C𝑁))) ≤ (exp‘((log‘4) ·
(𝑁 −
1)))) | 
| 330 |  | efle 16154 | . . . . 5
⊢
(((log‘(((2 · 𝑁) − 1)C𝑁)) ∈ ℝ ∧ ((log‘4)
· (𝑁 − 1))
∈ ℝ) → ((log‘(((2 · 𝑁) − 1)C𝑁)) ≤ ((log‘4) · (𝑁 − 1)) ↔
(exp‘(log‘(((2 · 𝑁) − 1)C𝑁))) ≤ (exp‘((log‘4) ·
(𝑁 −
1))))) | 
| 331 | 54, 63, 330 | syl2anc 584 | . . . 4
⊢ (𝑁 ∈ ℕ →
((log‘(((2 · 𝑁) − 1)C𝑁)) ≤ ((log‘4) · (𝑁 − 1)) ↔
(exp‘(log‘(((2 · 𝑁) − 1)C𝑁))) ≤ (exp‘((log‘4) ·
(𝑁 −
1))))) | 
| 332 | 329, 331 | mpbird 257 | . . 3
⊢ (𝑁 ∈ ℕ →
(log‘(((2 · 𝑁)
− 1)C𝑁)) ≤
((log‘4) · (𝑁
− 1))) | 
| 333 | 54, 63, 11, 332 | leadd2dd 11878 | . 2
⊢ (𝑁 ∈ ℕ →
((θ‘𝑁) +
(log‘(((2 · 𝑁)
− 1)C𝑁))) ≤
((θ‘𝑁) +
((log‘4) · (𝑁
− 1)))) | 
| 334 | 8, 55, 64, 252, 333 | letrd 11418 | 1
⊢ (𝑁 ∈ ℕ →
(θ‘((2 · 𝑁) − 1)) ≤ ((θ‘𝑁) + ((log‘4) ·
(𝑁 −
1)))) |