Step | Hyp | Ref
| Expression |
1 | | 2nn 11185 |
. . . . . 6
⊢ 2 ∈
ℕ |
2 | | nnmulcl 11043 |
. . . . . 6
⊢ ((2
∈ ℕ ∧ 𝑁
∈ ℕ) → (2 · 𝑁) ∈ ℕ) |
3 | 1, 2 | mpan 706 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (2
· 𝑁) ∈
ℕ) |
4 | 3 | nnred 11035 |
. . . 4
⊢ (𝑁 ∈ ℕ → (2
· 𝑁) ∈
ℝ) |
5 | | peano2rem 10348 |
. . . 4
⊢ ((2
· 𝑁) ∈ ℝ
→ ((2 · 𝑁)
− 1) ∈ ℝ) |
6 | 4, 5 | syl 17 |
. . 3
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) − 1)
∈ ℝ) |
7 | | chtcl 24835 |
. . 3
⊢ (((2
· 𝑁) − 1)
∈ ℝ → (θ‘((2 · 𝑁) − 1)) ∈
ℝ) |
8 | 6, 7 | syl 17 |
. 2
⊢ (𝑁 ∈ ℕ →
(θ‘((2 · 𝑁) − 1)) ∈
ℝ) |
9 | | nnre 11027 |
. . . 4
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
10 | | chtcl 24835 |
. . . 4
⊢ (𝑁 ∈ ℝ →
(θ‘𝑁) ∈
ℝ) |
11 | 9, 10 | syl 17 |
. . 3
⊢ (𝑁 ∈ ℕ →
(θ‘𝑁) ∈
ℝ) |
12 | | nnnn0 11299 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
13 | | 2m1e1 11135 |
. . . . . . . . . . 11
⊢ (2
− 1) = 1 |
14 | 13 | oveq2i 6661 |
. . . . . . . . . 10
⊢ ((2
· 𝑁) − (2
− 1)) = ((2 · 𝑁) − 1) |
15 | 3 | nncnd 11036 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (2
· 𝑁) ∈
ℂ) |
16 | | 2cn 11091 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℂ |
17 | | ax-1cn 9994 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
18 | | subsub 10311 |
. . . . . . . . . . . . 13
⊢ (((2
· 𝑁) ∈ ℂ
∧ 2 ∈ ℂ ∧ 1 ∈ ℂ) → ((2 · 𝑁) − (2 − 1)) = (((2
· 𝑁) − 2) +
1)) |
19 | 16, 17, 18 | mp3an23 1416 |
. . . . . . . . . . . 12
⊢ ((2
· 𝑁) ∈ ℂ
→ ((2 · 𝑁)
− (2 − 1)) = (((2 · 𝑁) − 2) + 1)) |
20 | 15, 19 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) − (2
− 1)) = (((2 · 𝑁) − 2) + 1)) |
21 | | nncn 11028 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
22 | | subdi 10463 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℂ ∧ 𝑁
∈ ℂ ∧ 1 ∈ ℂ) → (2 · (𝑁 − 1)) = ((2 · 𝑁) − (2 ·
1))) |
23 | 16, 17, 22 | mp3an13 1415 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℂ → (2
· (𝑁 − 1)) =
((2 · 𝑁) − (2
· 1))) |
24 | 21, 23 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → (2
· (𝑁 − 1)) =
((2 · 𝑁) − (2
· 1))) |
25 | | 2t1e2 11176 |
. . . . . . . . . . . . . 14
⊢ (2
· 1) = 2 |
26 | 25 | oveq2i 6661 |
. . . . . . . . . . . . 13
⊢ ((2
· 𝑁) − (2
· 1)) = ((2 · 𝑁) − 2) |
27 | 24, 26 | syl6eq 2672 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (2
· (𝑁 − 1)) =
((2 · 𝑁) −
2)) |
28 | 27 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((2
· (𝑁 − 1)) +
1) = (((2 · 𝑁)
− 2) + 1)) |
29 | 20, 28 | eqtr4d 2659 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) − (2
− 1)) = ((2 · (𝑁 − 1)) + 1)) |
30 | 14, 29 | syl5eqr 2670 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) − 1) =
((2 · (𝑁 − 1))
+ 1)) |
31 | | 2nn0 11309 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ0 |
32 | | nnm1nn0 11334 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
33 | | nn0mulcl 11329 |
. . . . . . . . . . 11
⊢ ((2
∈ ℕ0 ∧ (𝑁 − 1) ∈ ℕ0)
→ (2 · (𝑁
− 1)) ∈ ℕ0) |
34 | 31, 32, 33 | sylancr 695 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (2
· (𝑁 − 1))
∈ ℕ0) |
35 | | nn0p1nn 11332 |
. . . . . . . . . 10
⊢ ((2
· (𝑁 − 1))
∈ ℕ0 → ((2 · (𝑁 − 1)) + 1) ∈
ℕ) |
36 | 34, 35 | syl 17 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ((2
· (𝑁 − 1)) +
1) ∈ ℕ) |
37 | 30, 36 | eqeltrd 2701 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) − 1)
∈ ℕ) |
38 | | nnnn0 11299 |
. . . . . . . 8
⊢ (((2
· 𝑁) − 1)
∈ ℕ → ((2 · 𝑁) − 1) ∈
ℕ0) |
39 | 37, 38 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) − 1)
∈ ℕ0) |
40 | | 1re 10039 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
41 | 40 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 1 ∈
ℝ) |
42 | | nnge1 11046 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 1 ≤
𝑁) |
43 | 41, 9, 9, 42 | leadd2dd 10642 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ≤ (𝑁 + 𝑁)) |
44 | 21 | 2timesd 11275 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (2
· 𝑁) = (𝑁 + 𝑁)) |
45 | 43, 44 | breqtrrd 4681 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ≤ (2 · 𝑁)) |
46 | | leaddsub 10504 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 1 ∈
ℝ ∧ (2 · 𝑁) ∈ ℝ) → ((𝑁 + 1) ≤ (2 · 𝑁) ↔ 𝑁 ≤ ((2 · 𝑁) − 1))) |
47 | 9, 41, 4, 46 | syl3anc 1326 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) ≤ (2 · 𝑁) ↔ 𝑁 ≤ ((2 · 𝑁) − 1))) |
48 | 45, 47 | mpbid 222 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ≤ ((2 · 𝑁) − 1)) |
49 | | elfz2nn0 12431 |
. . . . . . 7
⊢ (𝑁 ∈ (0...((2 · 𝑁) − 1)) ↔ (𝑁 ∈ ℕ0
∧ ((2 · 𝑁)
− 1) ∈ ℕ0 ∧ 𝑁 ≤ ((2 · 𝑁) − 1))) |
50 | 12, 39, 48, 49 | syl3anbrc 1246 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (0...((2 · 𝑁) − 1))) |
51 | | bccl2 13110 |
. . . . . 6
⊢ (𝑁 ∈ (0...((2 · 𝑁) − 1)) → (((2
· 𝑁) −
1)C𝑁) ∈
ℕ) |
52 | 50, 51 | syl 17 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) −
1)C𝑁) ∈
ℕ) |
53 | 52 | nnrpd 11870 |
. . . 4
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) −
1)C𝑁) ∈
ℝ+) |
54 | 53 | relogcld 24369 |
. . 3
⊢ (𝑁 ∈ ℕ →
(log‘(((2 · 𝑁)
− 1)C𝑁)) ∈
ℝ) |
55 | 11, 54 | readdcld 10069 |
. 2
⊢ (𝑁 ∈ ℕ →
((θ‘𝑁) +
(log‘(((2 · 𝑁)
− 1)C𝑁))) ∈
ℝ) |
56 | | 4re 11097 |
. . . . . 6
⊢ 4 ∈
ℝ |
57 | | 4pos 11116 |
. . . . . 6
⊢ 0 <
4 |
58 | 56, 57 | elrpii 11835 |
. . . . 5
⊢ 4 ∈
ℝ+ |
59 | | relogcl 24322 |
. . . . 5
⊢ (4 ∈
ℝ+ → (log‘4) ∈ ℝ) |
60 | 58, 59 | ax-mp 5 |
. . . 4
⊢
(log‘4) ∈ ℝ |
61 | 32 | nn0red 11352 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℝ) |
62 | | remulcl 10021 |
. . . 4
⊢
(((log‘4) ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ) →
((log‘4) · (𝑁
− 1)) ∈ ℝ) |
63 | 60, 61, 62 | sylancr 695 |
. . 3
⊢ (𝑁 ∈ ℕ →
((log‘4) · (𝑁
− 1)) ∈ ℝ) |
64 | 11, 63 | readdcld 10069 |
. 2
⊢ (𝑁 ∈ ℕ →
((θ‘𝑁) +
((log‘4) · (𝑁
− 1))) ∈ ℝ) |
65 | | iftrue 4092 |
. . . . . . . . . . . 12
⊢ (𝑝 ≤ ((2 · 𝑁) − 1) → if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) =
1) |
66 | 65 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ ((2 · 𝑁) − 1)) → if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) =
1) |
67 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℙ) |
68 | 52 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (((2
· 𝑁) −
1)C𝑁) ∈
ℕ) |
69 | 67, 68 | pccld 15555 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)) ∈
ℕ0) |
70 | | nn0addge1 11339 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℝ ∧ (𝑝
pCnt (((2 · 𝑁)
− 1)C𝑁)) ∈
ℕ0) → 1 ≤ (1 + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))) |
71 | 40, 69, 70 | sylancr 695 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 1 ≤
(1 + (𝑝 pCnt (((2 ·
𝑁) − 1)C𝑁)))) |
72 | | iftrue 4092 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 ≤ 𝑁 → if(𝑝 ≤ 𝑁, 1, 0) = 1) |
73 | 72 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 ≤ 𝑁 → (if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) = (1 + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))) |
74 | 73 | breq2d 4665 |
. . . . . . . . . . . . . 14
⊢ (𝑝 ≤ 𝑁 → (1 ≤ (if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) ↔ 1 ≤ (1 + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))) |
75 | 71, 74 | syl5ibrcom 237 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 ≤ 𝑁 → 1 ≤ (if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))) |
76 | 75 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ ((2 · 𝑁) − 1)) → (𝑝 ≤ 𝑁 → 1 ≤ (if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))) |
77 | | prmnn 15388 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
78 | 77 | ad2antlr 763 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → 𝑝 ∈ ℕ) |
79 | | simprl 794 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → 𝑝 ≤ ((2 · 𝑁) − 1)) |
80 | | prmz 15389 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℤ) |
81 | 37 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) − 1)
∈ ℤ) |
82 | | eluz 11701 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑝 ∈ ℤ ∧ ((2
· 𝑁) − 1)
∈ ℤ) → (((2 · 𝑁) − 1) ∈
(ℤ≥‘𝑝) ↔ 𝑝 ≤ ((2 · 𝑁) − 1))) |
83 | 80, 81, 82 | syl2anr 495 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (((2
· 𝑁) − 1)
∈ (ℤ≥‘𝑝) ↔ 𝑝 ≤ ((2 · 𝑁) − 1))) |
84 | 83 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → (((2 · 𝑁) − 1) ∈
(ℤ≥‘𝑝) ↔ 𝑝 ≤ ((2 · 𝑁) − 1))) |
85 | 79, 84 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → ((2 · 𝑁) − 1) ∈
(ℤ≥‘𝑝)) |
86 | | dvdsfac 15048 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑝 ∈ ℕ ∧ ((2
· 𝑁) − 1)
∈ (ℤ≥‘𝑝)) → 𝑝 ∥ (!‘((2 · 𝑁) − 1))) |
87 | 78, 85, 86 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → 𝑝 ∥ (!‘((2 · 𝑁) − 1))) |
88 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℙ) |
89 | | faccl 13070 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((2
· 𝑁) − 1)
∈ ℕ0 → (!‘((2 · 𝑁) − 1)) ∈
ℕ) |
90 | 39, 89 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ →
(!‘((2 · 𝑁)
− 1)) ∈ ℕ) |
91 | | pcelnn 15574 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑝 ∈ ℙ ∧
(!‘((2 · 𝑁)
− 1)) ∈ ℕ) → ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) ∈ ℕ ↔ 𝑝 ∥ (!‘((2 ·
𝑁) −
1)))) |
92 | 88, 90, 91 | syl2anr 495 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt (!‘((2 ·
𝑁) − 1))) ∈
ℕ ↔ 𝑝 ∥
(!‘((2 · 𝑁)
− 1)))) |
93 | 92 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) ∈ ℕ ↔ 𝑝 ∥ (!‘((2 ·
𝑁) −
1)))) |
94 | 87, 93 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → (𝑝 pCnt (!‘((2 · 𝑁) − 1))) ∈
ℕ) |
95 | 94 | nnge1d 11063 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → 1 ≤ (𝑝 pCnt (!‘((2 · 𝑁) − 1)))) |
96 | | iffalse 4095 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑝 ≤ 𝑁 → if(𝑝 ≤ 𝑁, 1, 0) = 0) |
97 | 96 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑝 ≤ 𝑁 → (if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) = (0 + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))) |
98 | 97 | ad2antll 765 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → (if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) = (0 + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))) |
99 | 69 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)) ∈ ℂ) |
100 | 99 | addid2d 10237 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (0 +
(𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) = (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) |
101 | 100 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → (0 + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) = (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) |
102 | | bcval2 13092 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ (0...((2 · 𝑁) − 1)) → (((2
· 𝑁) −
1)C𝑁) = ((!‘((2
· 𝑁) − 1)) /
((!‘(((2 · 𝑁)
− 1) − 𝑁))
· (!‘𝑁)))) |
103 | 50, 102 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) −
1)C𝑁) = ((!‘((2
· 𝑁) − 1)) /
((!‘(((2 · 𝑁)
− 1) − 𝑁))
· (!‘𝑁)))) |
104 | 44 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) − 1) =
((𝑁 + 𝑁) − 1)) |
105 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℕ → 1 ∈
ℂ) |
106 | 21, 21, 105 | addsubassd 10412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ → ((𝑁 + 𝑁) − 1) = (𝑁 + (𝑁 − 1))) |
107 | 104, 106 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) − 1) =
(𝑁 + (𝑁 − 1))) |
108 | 107 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) − 1)
− 𝑁) = ((𝑁 + (𝑁 − 1)) − 𝑁)) |
109 | 32 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℂ) |
110 | 21, 109 | pncan2d 10394 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → ((𝑁 + (𝑁 − 1)) − 𝑁) = (𝑁 − 1)) |
111 | 108, 110 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) − 1)
− 𝑁) = (𝑁 − 1)) |
112 | 111 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ →
(!‘(((2 · 𝑁)
− 1) − 𝑁)) =
(!‘(𝑁 −
1))) |
113 | 112 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ →
((!‘(((2 · 𝑁)
− 1) − 𝑁))
· (!‘𝑁)) =
((!‘(𝑁 − 1))
· (!‘𝑁))) |
114 | 113 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ →
((!‘((2 · 𝑁)
− 1)) / ((!‘(((2 · 𝑁) − 1) − 𝑁)) · (!‘𝑁))) = ((!‘((2 · 𝑁) − 1)) / ((!‘(𝑁 − 1)) ·
(!‘𝑁)))) |
115 | 103, 114 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) −
1)C𝑁) = ((!‘((2
· 𝑁) − 1)) /
((!‘(𝑁 − 1))
· (!‘𝑁)))) |
116 | 115 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (((2
· 𝑁) −
1)C𝑁) = ((!‘((2
· 𝑁) − 1)) /
((!‘(𝑁 − 1))
· (!‘𝑁)))) |
117 | 116 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)) = (𝑝 pCnt ((!‘((2 · 𝑁) − 1)) / ((!‘(𝑁 − 1)) ·
(!‘𝑁))))) |
118 | | nnz 11399 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((!‘((2 · 𝑁) − 1)) ∈ ℕ →
(!‘((2 · 𝑁)
− 1)) ∈ ℤ) |
119 | | nnne0 11053 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((!‘((2 · 𝑁) − 1)) ∈ ℕ →
(!‘((2 · 𝑁)
− 1)) ≠ 0) |
120 | 118, 119 | jca 554 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((!‘((2 · 𝑁) − 1)) ∈ ℕ →
((!‘((2 · 𝑁)
− 1)) ∈ ℤ ∧ (!‘((2 · 𝑁) − 1)) ≠ 0)) |
121 | 90, 120 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ →
((!‘((2 · 𝑁)
− 1)) ∈ ℤ ∧ (!‘((2 · 𝑁) − 1)) ≠ 0)) |
122 | 121 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
((!‘((2 · 𝑁)
− 1)) ∈ ℤ ∧ (!‘((2 · 𝑁) − 1)) ≠ 0)) |
123 | | faccl 13070 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 − 1) ∈
ℕ0 → (!‘(𝑁 − 1)) ∈
ℕ) |
124 | 32, 123 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ →
(!‘(𝑁 − 1))
∈ ℕ) |
125 | | faccl 13070 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℕ) |
126 | 12, 125 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ →
(!‘𝑁) ∈
ℕ) |
127 | 124, 126 | nnmulcld 11068 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ →
((!‘(𝑁 − 1))
· (!‘𝑁))
∈ ℕ) |
128 | 127 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
((!‘(𝑁 − 1))
· (!‘𝑁))
∈ ℕ) |
129 | | pcdiv 15557 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑝 ∈ ℙ ∧
((!‘((2 · 𝑁)
− 1)) ∈ ℤ ∧ (!‘((2 · 𝑁) − 1)) ≠ 0) ∧ ((!‘(𝑁 − 1)) ·
(!‘𝑁)) ∈
ℕ) → (𝑝 pCnt
((!‘((2 · 𝑁)
− 1)) / ((!‘(𝑁
− 1)) · (!‘𝑁)))) = ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − (𝑝 pCnt ((!‘(𝑁 − 1)) · (!‘𝑁))))) |
130 | 67, 122, 128, 129 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((!‘((2 ·
𝑁) − 1)) /
((!‘(𝑁 − 1))
· (!‘𝑁)))) =
((𝑝 pCnt (!‘((2
· 𝑁) − 1)))
− (𝑝 pCnt
((!‘(𝑁 − 1))
· (!‘𝑁))))) |
131 | | nnz 11399 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((!‘(𝑁 −
1)) ∈ ℕ → (!‘(𝑁 − 1)) ∈
ℤ) |
132 | | nnne0 11053 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((!‘(𝑁 −
1)) ∈ ℕ → (!‘(𝑁 − 1)) ≠ 0) |
133 | 131, 132 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((!‘(𝑁 −
1)) ∈ ℕ → ((!‘(𝑁 − 1)) ∈ ℤ ∧
(!‘(𝑁 − 1))
≠ 0)) |
134 | 124, 133 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ →
((!‘(𝑁 − 1))
∈ ℤ ∧ (!‘(𝑁 − 1)) ≠ 0)) |
135 | 134 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
((!‘(𝑁 − 1))
∈ ℤ ∧ (!‘(𝑁 − 1)) ≠ 0)) |
136 | | nnz 11399 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((!‘𝑁) ∈
ℕ → (!‘𝑁)
∈ ℤ) |
137 | | nnne0 11053 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((!‘𝑁) ∈
ℕ → (!‘𝑁)
≠ 0) |
138 | 136, 137 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((!‘𝑁) ∈
ℕ → ((!‘𝑁)
∈ ℤ ∧ (!‘𝑁) ≠ 0)) |
139 | 126, 138 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ →
((!‘𝑁) ∈ ℤ
∧ (!‘𝑁) ≠
0)) |
140 | 139 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
((!‘𝑁) ∈ ℤ
∧ (!‘𝑁) ≠
0)) |
141 | | pcmul 15556 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑝 ∈ ℙ ∧
((!‘(𝑁 − 1))
∈ ℤ ∧ (!‘(𝑁 − 1)) ≠ 0) ∧ ((!‘𝑁) ∈ ℤ ∧
(!‘𝑁) ≠ 0)) →
(𝑝 pCnt ((!‘(𝑁 − 1)) ·
(!‘𝑁))) = ((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁)))) |
142 | 67, 135, 140, 141 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((!‘(𝑁 − 1)) ·
(!‘𝑁))) = ((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁)))) |
143 | 142 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt (!‘((2 ·
𝑁) − 1))) −
(𝑝 pCnt ((!‘(𝑁 − 1)) ·
(!‘𝑁)))) = ((𝑝 pCnt (!‘((2 ·
𝑁) − 1))) −
((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁))))) |
144 | 117, 130,
143 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)) = ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − ((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁))))) |
145 | 144 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)) = ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − ((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁))))) |
146 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → ¬ 𝑝 ≤ 𝑁) |
147 | | prmfac1 15431 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ ℕ0
∧ 𝑝 ∈ ℙ
∧ 𝑝 ∥
(!‘𝑁)) → 𝑝 ≤ 𝑁) |
148 | 147 | 3expia 1267 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℕ0
∧ 𝑝 ∈ ℙ)
→ (𝑝 ∥
(!‘𝑁) → 𝑝 ≤ 𝑁)) |
149 | 12, 148 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (!‘𝑁) → 𝑝 ≤ 𝑁)) |
150 | 149 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → (𝑝 ∥ (!‘𝑁) → 𝑝 ≤ 𝑁)) |
151 | 146, 150 | mtod 189 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → ¬ 𝑝 ∥ (!‘𝑁)) |
152 | 80 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℤ) |
153 | 135 | simpld 475 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
(!‘(𝑁 − 1))
∈ ℤ) |
154 | | nnz 11399 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
155 | 154 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑁 ∈
ℤ) |
156 | | dvdsmultr1 15019 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑝 ∈ ℤ ∧
(!‘(𝑁 − 1))
∈ ℤ ∧ 𝑁
∈ ℤ) → (𝑝
∥ (!‘(𝑁 −
1)) → 𝑝 ∥
((!‘(𝑁 − 1))
· 𝑁))) |
157 | 152, 153,
155, 156 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (!‘(𝑁 − 1)) → 𝑝 ∥ ((!‘(𝑁 − 1)) · 𝑁))) |
158 | | facnn2 13069 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ →
(!‘𝑁) =
((!‘(𝑁 − 1))
· 𝑁)) |
159 | 158 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
(!‘𝑁) =
((!‘(𝑁 − 1))
· 𝑁)) |
160 | 159 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (!‘𝑁) ↔ 𝑝 ∥ ((!‘(𝑁 − 1)) · 𝑁))) |
161 | 157, 160 | sylibrd 249 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (!‘(𝑁 − 1)) → 𝑝 ∥ (!‘𝑁))) |
162 | 161 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → (𝑝 ∥ (!‘(𝑁 − 1)) → 𝑝 ∥ (!‘𝑁))) |
163 | 151, 162 | mtod 189 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → ¬ 𝑝 ∥ (!‘(𝑁 − 1))) |
164 | | pceq0 15575 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑝 ∈ ℙ ∧
(!‘(𝑁 − 1))
∈ ℕ) → ((𝑝
pCnt (!‘(𝑁 −
1))) = 0 ↔ ¬ 𝑝
∥ (!‘(𝑁 −
1)))) |
165 | 88, 124, 164 | syl2anr 495 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt (!‘(𝑁 − 1))) = 0 ↔ ¬
𝑝 ∥ (!‘(𝑁 − 1)))) |
166 | 165 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → ((𝑝 pCnt (!‘(𝑁 − 1))) = 0 ↔ ¬ 𝑝 ∥ (!‘(𝑁 − 1)))) |
167 | 163, 166 | mpbird 247 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → (𝑝 pCnt (!‘(𝑁 − 1))) = 0) |
168 | | pceq0 15575 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑝 ∈ ℙ ∧
(!‘𝑁) ∈ ℕ)
→ ((𝑝 pCnt
(!‘𝑁)) = 0 ↔
¬ 𝑝 ∥
(!‘𝑁))) |
169 | 88, 126, 168 | syl2anr 495 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt (!‘𝑁)) = 0 ↔ ¬ 𝑝 ∥ (!‘𝑁))) |
170 | 169 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → ((𝑝 pCnt (!‘𝑁)) = 0 ↔ ¬ 𝑝 ∥ (!‘𝑁))) |
171 | 151, 170 | mpbird 247 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → (𝑝 pCnt (!‘𝑁)) = 0) |
172 | 167, 171 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → ((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁))) = (0 + 0)) |
173 | | 00id 10211 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 + 0) =
0 |
174 | 172, 173 | syl6eq 2672 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → ((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁))) = 0) |
175 | 174 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − ((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁)))) = ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − 0)) |
176 | | pccl 15554 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑝 ∈ ℙ ∧
(!‘((2 · 𝑁)
− 1)) ∈ ℕ) → (𝑝 pCnt (!‘((2 · 𝑁) − 1))) ∈
ℕ0) |
177 | 88, 90, 176 | syl2anr 495 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (!‘((2 ·
𝑁) − 1))) ∈
ℕ0) |
178 | 177 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (!‘((2 ·
𝑁) − 1))) ∈
ℂ) |
179 | 178 | subid1d 10381 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt (!‘((2 ·
𝑁) − 1))) − 0)
= (𝑝 pCnt (!‘((2
· 𝑁) −
1)))) |
180 | 179 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − 0) = (𝑝 pCnt (!‘((2 ·
𝑁) −
1)))) |
181 | 145, 175,
180 | 3eqtrd 2660 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)) = (𝑝 pCnt (!‘((2 · 𝑁) − 1)))) |
182 | 98, 101, 181 | 3eqtrd 2660 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → (if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) = (𝑝 pCnt (!‘((2 · 𝑁) − 1)))) |
183 | 95, 182 | breqtrrd 4681 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝 ≤ 𝑁)) → 1 ≤ (if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))) |
184 | 183 | expr 643 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ ((2 · 𝑁) − 1)) → (¬
𝑝 ≤ 𝑁 → 1 ≤ (if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))) |
185 | 76, 184 | pm2.61d 170 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ ((2 · 𝑁) − 1)) → 1 ≤
(if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))) |
186 | 66, 185 | eqbrtrd 4675 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ ((2 · 𝑁) − 1)) → if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) ≤
(if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))) |
187 | 186 | ex 450 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 ≤ ((2 · 𝑁) − 1) → if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) ≤
(if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))) |
188 | | 1nn0 11308 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℕ0 |
189 | | 0nn0 11307 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℕ0 |
190 | 188, 189 | keepel 4155 |
. . . . . . . . . . . 12
⊢ if(𝑝 ≤ 𝑁, 1, 0) ∈
ℕ0 |
191 | | nn0addcl 11328 |
. . . . . . . . . . . 12
⊢
((if(𝑝 ≤ 𝑁, 1, 0) ∈
ℕ0 ∧ (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)) ∈ ℕ0) →
(if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) ∈
ℕ0) |
192 | 190, 69, 191 | sylancr 695 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
(if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) ∈
ℕ0) |
193 | 192 | nn0ge0d 11354 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 0 ≤
(if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))) |
194 | | iffalse 4095 |
. . . . . . . . . . 11
⊢ (¬
𝑝 ≤ ((2 · 𝑁) − 1) → if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) =
0) |
195 | 194 | breq1d 4663 |
. . . . . . . . . 10
⊢ (¬
𝑝 ≤ ((2 · 𝑁) − 1) → (if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) ≤
(if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) ↔ 0 ≤ (if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))) |
196 | 193, 195 | syl5ibrcom 237 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (¬
𝑝 ≤ ((2 · 𝑁) − 1) → if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) ≤
(if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))) |
197 | 187, 196 | pm2.61d 170 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) ≤
(if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))) |
198 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) |
199 | 198 | prmorcht 24904 |
. . . . . . . . . . . 12
⊢ (((2
· 𝑁) − 1)
∈ ℕ → (exp‘(θ‘((2 · 𝑁) − 1))) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘((2 · 𝑁) − 1))) |
200 | 37, 199 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
(exp‘(θ‘((2 · 𝑁) − 1))) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘((2 · 𝑁) − 1))) |
201 | 200 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (𝑝 pCnt
(exp‘(θ‘((2 · 𝑁) − 1)))) = (𝑝 pCnt (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘((2 · 𝑁) − 1)))) |
202 | 201 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt
(exp‘(θ‘((2 · 𝑁) − 1)))) = (𝑝 pCnt (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘((2 · 𝑁) − 1)))) |
203 | | nncn 11028 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
204 | 203 | exp1d 13003 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (𝑛↑1) = 𝑛) |
205 | 204 | ifeq1d 4104 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → if(𝑛 ∈ ℙ, (𝑛↑1), 1) = if(𝑛 ∈ ℙ, 𝑛, 1)) |
206 | 205 | mpteq2ia 4740 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑1), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) |
207 | 206 | eqcomi 2631 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑1), 1)) |
208 | 188 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑛 ∈ ℙ) → 1 ∈
ℕ0) |
209 | 208 | ralrimiva 2966 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
∀𝑛 ∈ ℙ 1
∈ ℕ0) |
210 | 37 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((2
· 𝑁) − 1)
∈ ℕ) |
211 | | eqidd 2623 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑝 → 1 = 1) |
212 | 207, 209,
210, 67, 211 | pcmpt 15596 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘((2 · 𝑁) − 1))) = if(𝑝 ≤ ((2 · 𝑁) − 1), 1,
0)) |
213 | 202, 212 | eqtrd 2656 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt
(exp‘(θ‘((2 · 𝑁) − 1)))) = if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0)) |
214 | | efchtcl 24837 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℝ →
(exp‘(θ‘𝑁)) ∈ ℕ) |
215 | 9, 214 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ →
(exp‘(θ‘𝑁)) ∈ ℕ) |
216 | 215 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
(exp‘(θ‘𝑁)) ∈ ℕ) |
217 | | nnz 11399 |
. . . . . . . . . . . 12
⊢
((exp‘(θ‘𝑁)) ∈ ℕ →
(exp‘(θ‘𝑁)) ∈ ℤ) |
218 | | nnne0 11053 |
. . . . . . . . . . . 12
⊢
((exp‘(θ‘𝑁)) ∈ ℕ →
(exp‘(θ‘𝑁)) ≠ 0) |
219 | 217, 218 | jca 554 |
. . . . . . . . . . 11
⊢
((exp‘(θ‘𝑁)) ∈ ℕ →
((exp‘(θ‘𝑁)) ∈ ℤ ∧
(exp‘(θ‘𝑁)) ≠ 0)) |
220 | 216, 219 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) →
((exp‘(θ‘𝑁)) ∈ ℤ ∧
(exp‘(θ‘𝑁)) ≠ 0)) |
221 | | nnz 11399 |
. . . . . . . . . . . 12
⊢ ((((2
· 𝑁) −
1)C𝑁) ∈ ℕ →
(((2 · 𝑁) −
1)C𝑁) ∈
ℤ) |
222 | | nnne0 11053 |
. . . . . . . . . . . 12
⊢ ((((2
· 𝑁) −
1)C𝑁) ∈ ℕ →
(((2 · 𝑁) −
1)C𝑁) ≠
0) |
223 | 221, 222 | jca 554 |
. . . . . . . . . . 11
⊢ ((((2
· 𝑁) −
1)C𝑁) ∈ ℕ →
((((2 · 𝑁) −
1)C𝑁) ∈ ℤ ∧
(((2 · 𝑁) −
1)C𝑁) ≠
0)) |
224 | 68, 223 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((((2
· 𝑁) −
1)C𝑁) ∈ ℤ ∧
(((2 · 𝑁) −
1)C𝑁) ≠
0)) |
225 | | pcmul 15556 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ ℙ ∧
((exp‘(θ‘𝑁)) ∈ ℤ ∧
(exp‘(θ‘𝑁)) ≠ 0) ∧ ((((2 · 𝑁) − 1)C𝑁) ∈ ℤ ∧ (((2 · 𝑁) − 1)C𝑁) ≠ 0)) → (𝑝 pCnt ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))) = ((𝑝 pCnt (exp‘(θ‘𝑁))) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))) |
226 | 67, 220, 224, 225 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt
((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))) = ((𝑝 pCnt (exp‘(θ‘𝑁))) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))) |
227 | 198 | prmorcht 24904 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ →
(exp‘(θ‘𝑁)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑁)) |
228 | 227 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (𝑝 pCnt
(exp‘(θ‘𝑁))) = (𝑝 pCnt (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑁))) |
229 | 228 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt
(exp‘(θ‘𝑁))) = (𝑝 pCnt (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑁))) |
230 | | simpl 473 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑁 ∈
ℕ) |
231 | 207, 209,
230, 67, 211 | pcmpt 15596 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑁)) = if(𝑝 ≤ 𝑁, 1, 0)) |
232 | 229, 231 | eqtrd 2656 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt
(exp‘(θ‘𝑁))) = if(𝑝 ≤ 𝑁, 1, 0)) |
233 | 232 | oveq1d 6665 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt
(exp‘(θ‘𝑁))) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) = (if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))) |
234 | 226, 233 | eqtrd 2656 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt
((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))) = (if(𝑝 ≤ 𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))) |
235 | 197, 213,
234 | 3brtr4d 4685 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt
(exp‘(θ‘((2 · 𝑁) − 1)))) ≤ (𝑝 pCnt ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)))) |
236 | 235 | ralrimiva 2966 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
∀𝑝 ∈ ℙ
(𝑝 pCnt
(exp‘(θ‘((2 · 𝑁) − 1)))) ≤ (𝑝 pCnt ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)))) |
237 | | efchtcl 24837 |
. . . . . . . . 9
⊢ (((2
· 𝑁) − 1)
∈ ℝ → (exp‘(θ‘((2 · 𝑁) − 1))) ∈
ℕ) |
238 | 6, 237 | syl 17 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(exp‘(θ‘((2 · 𝑁) − 1))) ∈
ℕ) |
239 | 238 | nnzd 11481 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(exp‘(θ‘((2 · 𝑁) − 1))) ∈
ℤ) |
240 | 215, 52 | nnmulcld 11068 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) ∈ ℕ) |
241 | 240 | nnzd 11481 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) ∈ ℤ) |
242 | | pc2dvds 15583 |
. . . . . . 7
⊢
(((exp‘(θ‘((2 · 𝑁) − 1))) ∈ ℤ ∧
((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) ∈ ℤ) →
((exp‘(θ‘((2 · 𝑁) − 1))) ∥
((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt (exp‘(θ‘((2 ·
𝑁) − 1)))) ≤
(𝑝 pCnt
((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))))) |
243 | 239, 241,
242 | syl2anc 693 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
((exp‘(θ‘((2 · 𝑁) − 1))) ∥
((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt (exp‘(θ‘((2 ·
𝑁) − 1)))) ≤
(𝑝 pCnt
((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))))) |
244 | 236, 243 | mpbird 247 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(exp‘(θ‘((2 · 𝑁) − 1))) ∥
((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))) |
245 | | dvdsle 15032 |
. . . . . 6
⊢
(((exp‘(θ‘((2 · 𝑁) − 1))) ∈ ℤ ∧
((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) ∈ ℕ) →
((exp‘(θ‘((2 · 𝑁) − 1))) ∥
((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) → (exp‘(θ‘((2
· 𝑁) − 1)))
≤ ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)))) |
246 | 239, 240,
245 | syl2anc 693 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
((exp‘(θ‘((2 · 𝑁) − 1))) ∥
((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) → (exp‘(θ‘((2
· 𝑁) − 1)))
≤ ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)))) |
247 | 244, 246 | mpd 15 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(exp‘(θ‘((2 · 𝑁) − 1))) ≤
((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))) |
248 | 11 | recnd 10068 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(θ‘𝑁) ∈
ℂ) |
249 | 54 | recnd 10068 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(log‘(((2 · 𝑁)
− 1)C𝑁)) ∈
ℂ) |
250 | | efadd 14824 |
. . . . . 6
⊢
(((θ‘𝑁)
∈ ℂ ∧ (log‘(((2 · 𝑁) − 1)C𝑁)) ∈ ℂ) →
(exp‘((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁)))) = ((exp‘(θ‘𝑁)) ·
(exp‘(log‘(((2 · 𝑁) − 1)C𝑁))))) |
251 | 248, 249,
250 | syl2anc 693 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(exp‘((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁)))) = ((exp‘(θ‘𝑁)) ·
(exp‘(log‘(((2 · 𝑁) − 1)C𝑁))))) |
252 | 53 | reeflogd 24370 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(exp‘(log‘(((2 · 𝑁) − 1)C𝑁))) = (((2 · 𝑁) − 1)C𝑁)) |
253 | 252 | oveq2d 6666 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
((exp‘(θ‘𝑁)) · (exp‘(log‘(((2
· 𝑁) −
1)C𝑁)))) =
((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))) |
254 | 251, 253 | eqtrd 2656 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(exp‘((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁)))) = ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))) |
255 | 247, 254 | breqtrrd 4681 |
. . 3
⊢ (𝑁 ∈ ℕ →
(exp‘(θ‘((2 · 𝑁) − 1))) ≤
(exp‘((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁))))) |
256 | | efle 14848 |
. . . 4
⊢
(((θ‘((2 · 𝑁) − 1)) ∈ ℝ ∧
((θ‘𝑁) +
(log‘(((2 · 𝑁)
− 1)C𝑁))) ∈
ℝ) → ((θ‘((2 · 𝑁) − 1)) ≤ ((θ‘𝑁) + (log‘(((2 ·
𝑁) − 1)C𝑁))) ↔
(exp‘(θ‘((2 · 𝑁) − 1))) ≤
(exp‘((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁)))))) |
257 | 8, 55, 256 | syl2anc 693 |
. . 3
⊢ (𝑁 ∈ ℕ →
((θ‘((2 · 𝑁) − 1)) ≤ ((θ‘𝑁) + (log‘(((2 ·
𝑁) − 1)C𝑁))) ↔
(exp‘(θ‘((2 · 𝑁) − 1))) ≤
(exp‘((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁)))))) |
258 | 255, 257 | mpbird 247 |
. 2
⊢ (𝑁 ∈ ℕ →
(θ‘((2 · 𝑁) − 1)) ≤ ((θ‘𝑁) + (log‘(((2 ·
𝑁) − 1)C𝑁)))) |
259 | | fzfid 12772 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (0...((2
· 𝑁) − 1))
∈ Fin) |
260 | | elfzelz 12342 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (0...((2 · 𝑁) − 1)) → 𝑘 ∈
ℤ) |
261 | | bccl 13109 |
. . . . . . . . . . 11
⊢ ((((2
· 𝑁) − 1)
∈ ℕ0 ∧ 𝑘 ∈ ℤ) → (((2 · 𝑁) − 1)C𝑘) ∈
ℕ0) |
262 | 39, 260, 261 | syl2an 494 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...((2 · 𝑁) − 1))) → (((2
· 𝑁) −
1)C𝑘) ∈
ℕ0) |
263 | 262 | nn0red 11352 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...((2 · 𝑁) − 1))) → (((2
· 𝑁) −
1)C𝑘) ∈
ℝ) |
264 | 262 | nn0ge0d 11354 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...((2 · 𝑁) − 1))) → 0 ≤
(((2 · 𝑁) −
1)C𝑘)) |
265 | | nn0uz 11722 |
. . . . . . . . . . . 12
⊢
ℕ0 = (ℤ≥‘0) |
266 | 32, 265 | syl6eleq 2711 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
(ℤ≥‘0)) |
267 | | fzss1 12380 |
. . . . . . . . . . 11
⊢ ((𝑁 − 1) ∈
(ℤ≥‘0) → ((𝑁 − 1)...𝑁) ⊆ (0...𝑁)) |
268 | 266, 267 | syl 17 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1)...𝑁) ⊆ (0...𝑁)) |
269 | | eluz 11701 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ ((2
· 𝑁) − 1)
∈ ℤ) → (((2 · 𝑁) − 1) ∈
(ℤ≥‘𝑁) ↔ 𝑁 ≤ ((2 · 𝑁) − 1))) |
270 | 154, 81, 269 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) − 1)
∈ (ℤ≥‘𝑁) ↔ 𝑁 ≤ ((2 · 𝑁) − 1))) |
271 | 48, 270 | mpbird 247 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁) − 1)
∈ (ℤ≥‘𝑁)) |
272 | | fzss2 12381 |
. . . . . . . . . . 11
⊢ (((2
· 𝑁) − 1)
∈ (ℤ≥‘𝑁) → (0...𝑁) ⊆ (0...((2 · 𝑁) − 1))) |
273 | 271, 272 | syl 17 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(0...𝑁) ⊆ (0...((2
· 𝑁) −
1))) |
274 | 268, 273 | sstrd 3613 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1)...𝑁) ⊆ (0...((2 · 𝑁) − 1))) |
275 | 259, 263,
264, 274 | fsumless 14528 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ ((𝑁 − 1)...𝑁)(((2 · 𝑁) − 1)C𝑘) ≤ Σ𝑘 ∈ (0...((2 · 𝑁) − 1))(((2 · 𝑁) − 1)C𝑘)) |
276 | 32 | nn0zd 11480 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℤ) |
277 | | bccmpl 13096 |
. . . . . . . . . . . . . . 15
⊢ ((((2
· 𝑁) − 1)
∈ ℕ0 ∧ 𝑁 ∈ ℤ) → (((2 · 𝑁) − 1)C𝑁) = (((2 · 𝑁) − 1)C(((2 · 𝑁) − 1) − 𝑁))) |
278 | 39, 154, 277 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) −
1)C𝑁) = (((2 · 𝑁) − 1)C(((2 · 𝑁) − 1) − 𝑁))) |
279 | 111 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) − 1)C(((2
· 𝑁) − 1)
− 𝑁)) = (((2 ·
𝑁) − 1)C(𝑁 − 1))) |
280 | 278, 279 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) −
1)C𝑁) = (((2 · 𝑁) − 1)C(𝑁 − 1))) |
281 | 52 | nncnd 11036 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) −
1)C𝑁) ∈
ℂ) |
282 | 280, 281 | eqeltrrd 2702 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) −
1)C(𝑁 − 1)) ∈
ℂ) |
283 | | oveq2 6658 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑁 − 1) → (((2 · 𝑁) − 1)C𝑘) = (((2 · 𝑁) − 1)C(𝑁 − 1))) |
284 | 283 | fsum1 14476 |
. . . . . . . . . . . 12
⊢ (((𝑁 − 1) ∈ ℤ ∧
(((2 · 𝑁) −
1)C(𝑁 − 1)) ∈
ℂ) → Σ𝑘
∈ ((𝑁 −
1)...(𝑁 − 1))(((2
· 𝑁) −
1)C𝑘) = (((2 · 𝑁) − 1)C(𝑁 − 1))) |
285 | 276, 282,
284 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ ((𝑁 − 1)...(𝑁 − 1))(((2 · 𝑁) − 1)C𝑘) = (((2 · 𝑁) − 1)C(𝑁 − 1))) |
286 | 285, 280 | eqtr4d 2659 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ ((𝑁 − 1)...(𝑁 − 1))(((2 · 𝑁) − 1)C𝑘) = (((2 · 𝑁) − 1)C𝑁)) |
287 | 286 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(Σ𝑘 ∈ ((𝑁 − 1)...(𝑁 − 1))(((2 · 𝑁) − 1)C𝑘) + (((2 · 𝑁) − 1)C𝑁)) = ((((2 · 𝑁) − 1)C𝑁) + (((2 · 𝑁) − 1)C𝑁))) |
288 | 21, 105 | npcand 10396 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) + 1) = 𝑁) |
289 | | uzid 11702 |
. . . . . . . . . . . . 13
⊢ ((𝑁 − 1) ∈ ℤ
→ (𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1))) |
290 | 276, 289 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1))) |
291 | | peano2uz 11741 |
. . . . . . . . . . . 12
⊢ ((𝑁 − 1) ∈
(ℤ≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
292 | 290, 291 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) + 1) ∈
(ℤ≥‘(𝑁 − 1))) |
293 | 288, 292 | eqeltrrd 2702 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
(ℤ≥‘(𝑁 − 1))) |
294 | 274 | sselda 3603 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ((𝑁 − 1)...𝑁)) → 𝑘 ∈ (0...((2 · 𝑁) − 1))) |
295 | 262 | nn0cnd 11353 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...((2 · 𝑁) − 1))) → (((2
· 𝑁) −
1)C𝑘) ∈
ℂ) |
296 | 294, 295 | syldan 487 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ((𝑁 − 1)...𝑁)) → (((2 · 𝑁) − 1)C𝑘) ∈ ℂ) |
297 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑁 → (((2 · 𝑁) − 1)C𝑘) = (((2 · 𝑁) − 1)C𝑁)) |
298 | 293, 296,
297 | fsumm1 14480 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ ((𝑁 − 1)...𝑁)(((2 · 𝑁) − 1)C𝑘) = (Σ𝑘 ∈ ((𝑁 − 1)...(𝑁 − 1))(((2 · 𝑁) − 1)C𝑘) + (((2 · 𝑁) − 1)C𝑁))) |
299 | 281 | 2timesd 11275 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (2
· (((2 · 𝑁)
− 1)C𝑁)) = ((((2
· 𝑁) −
1)C𝑁) + (((2 · 𝑁) − 1)C𝑁))) |
300 | 287, 298,
299 | 3eqtr4rd 2667 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (2
· (((2 · 𝑁)
− 1)C𝑁)) =
Σ𝑘 ∈ ((𝑁 − 1)...𝑁)(((2 · 𝑁) − 1)C𝑘)) |
301 | | binom11 14564 |
. . . . . . . . 9
⊢ (((2
· 𝑁) − 1)
∈ ℕ0 → (2↑((2 · 𝑁) − 1)) = Σ𝑘 ∈ (0...((2 · 𝑁) − 1))(((2 · 𝑁) − 1)C𝑘)) |
302 | 39, 301 | syl 17 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(2↑((2 · 𝑁)
− 1)) = Σ𝑘
∈ (0...((2 · 𝑁)
− 1))(((2 · 𝑁)
− 1)C𝑘)) |
303 | 275, 300,
302 | 3brtr4d 4685 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (2
· (((2 · 𝑁)
− 1)C𝑁)) ≤
(2↑((2 · 𝑁)
− 1))) |
304 | | mulcom 10022 |
. . . . . . . 8
⊢ ((2
∈ ℂ ∧ (((2 · 𝑁) − 1)C𝑁) ∈ ℂ) → (2 · (((2
· 𝑁) −
1)C𝑁)) = ((((2 ·
𝑁) − 1)C𝑁) · 2)) |
305 | 16, 281, 304 | sylancr 695 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (2
· (((2 · 𝑁)
− 1)C𝑁)) = ((((2
· 𝑁) −
1)C𝑁) ·
2)) |
306 | 30 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(2↑((2 · 𝑁)
− 1)) = (2↑((2 · (𝑁 − 1)) + 1))) |
307 | | expp1 12867 |
. . . . . . . . 9
⊢ ((2
∈ ℂ ∧ (2 · (𝑁 − 1)) ∈ ℕ0)
→ (2↑((2 · (𝑁 − 1)) + 1)) = ((2↑(2 ·
(𝑁 − 1))) ·
2)) |
308 | 16, 34, 307 | sylancr 695 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(2↑((2 · (𝑁
− 1)) + 1)) = ((2↑(2 · (𝑁 − 1))) · 2)) |
309 | 16 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 2 ∈
ℂ) |
310 | 31 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 2 ∈
ℕ0) |
311 | 309, 32, 310 | expmuld 13011 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(2↑(2 · (𝑁
− 1))) = ((2↑2)↑(𝑁 − 1))) |
312 | | sq2 12960 |
. . . . . . . . . . 11
⊢
(2↑2) = 4 |
313 | 312 | oveq1i 6660 |
. . . . . . . . . 10
⊢
((2↑2)↑(𝑁
− 1)) = (4↑(𝑁
− 1)) |
314 | 311, 313 | syl6eq 2672 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(2↑(2 · (𝑁
− 1))) = (4↑(𝑁
− 1))) |
315 | 314 | oveq1d 6665 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
((2↑(2 · (𝑁
− 1))) · 2) = ((4↑(𝑁 − 1)) · 2)) |
316 | 306, 308,
315 | 3eqtrd 2660 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(2↑((2 · 𝑁)
− 1)) = ((4↑(𝑁
− 1)) · 2)) |
317 | 303, 305,
316 | 3brtr3d 4684 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → ((((2
· 𝑁) −
1)C𝑁) · 2) ≤
((4↑(𝑁 − 1))
· 2)) |
318 | 52 | nnred 11035 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) −
1)C𝑁) ∈
ℝ) |
319 | | reexpcl 12877 |
. . . . . . . 8
⊢ ((4
∈ ℝ ∧ (𝑁
− 1) ∈ ℕ0) → (4↑(𝑁 − 1)) ∈
ℝ) |
320 | 56, 32, 319 | sylancr 695 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(4↑(𝑁 − 1))
∈ ℝ) |
321 | | 2re 11090 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
322 | | 2pos 11112 |
. . . . . . . . 9
⊢ 0 <
2 |
323 | 321, 322 | pm3.2i 471 |
. . . . . . . 8
⊢ (2 ∈
ℝ ∧ 0 < 2) |
324 | 323 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (2 ∈
ℝ ∧ 0 < 2)) |
325 | | lemul1 10875 |
. . . . . . 7
⊢ (((((2
· 𝑁) −
1)C𝑁) ∈ ℝ ∧
(4↑(𝑁 − 1))
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((((2 ·
𝑁) − 1)C𝑁) ≤ (4↑(𝑁 − 1)) ↔ ((((2
· 𝑁) −
1)C𝑁) · 2) ≤
((4↑(𝑁 − 1))
· 2))) |
326 | 318, 320,
324, 325 | syl3anc 1326 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → ((((2
· 𝑁) −
1)C𝑁) ≤ (4↑(𝑁 − 1)) ↔ ((((2
· 𝑁) −
1)C𝑁) · 2) ≤
((4↑(𝑁 − 1))
· 2))) |
327 | 317, 326 | mpbird 247 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (((2
· 𝑁) −
1)C𝑁) ≤ (4↑(𝑁 − 1))) |
328 | 60 | recni 10052 |
. . . . . . . 8
⊢
(log‘4) ∈ ℂ |
329 | | mulcom 10022 |
. . . . . . . 8
⊢
(((log‘4) ∈ ℂ ∧ (𝑁 − 1) ∈ ℂ) →
((log‘4) · (𝑁
− 1)) = ((𝑁 −
1) · (log‘4))) |
330 | 328, 109,
329 | sylancr 695 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
((log‘4) · (𝑁
− 1)) = ((𝑁 −
1) · (log‘4))) |
331 | 330 | fveq2d 6195 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(exp‘((log‘4) · (𝑁 − 1))) = (exp‘((𝑁 − 1) ·
(log‘4)))) |
332 | | reexplog 24341 |
. . . . . . 7
⊢ ((4
∈ ℝ+ ∧ (𝑁 − 1) ∈ ℤ) →
(4↑(𝑁 − 1)) =
(exp‘((𝑁 − 1)
· (log‘4)))) |
333 | 58, 276, 332 | sylancr 695 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(4↑(𝑁 − 1)) =
(exp‘((𝑁 − 1)
· (log‘4)))) |
334 | 331, 333 | eqtr4d 2659 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(exp‘((log‘4) · (𝑁 − 1))) = (4↑(𝑁 − 1))) |
335 | 327, 252,
334 | 3brtr4d 4685 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(exp‘(log‘(((2 · 𝑁) − 1)C𝑁))) ≤ (exp‘((log‘4) ·
(𝑁 −
1)))) |
336 | | efle 14848 |
. . . . 5
⊢
(((log‘(((2 · 𝑁) − 1)C𝑁)) ∈ ℝ ∧ ((log‘4)
· (𝑁 − 1))
∈ ℝ) → ((log‘(((2 · 𝑁) − 1)C𝑁)) ≤ ((log‘4) · (𝑁 − 1)) ↔
(exp‘(log‘(((2 · 𝑁) − 1)C𝑁))) ≤ (exp‘((log‘4) ·
(𝑁 −
1))))) |
337 | 54, 63, 336 | syl2anc 693 |
. . . 4
⊢ (𝑁 ∈ ℕ →
((log‘(((2 · 𝑁) − 1)C𝑁)) ≤ ((log‘4) · (𝑁 − 1)) ↔
(exp‘(log‘(((2 · 𝑁) − 1)C𝑁))) ≤ (exp‘((log‘4) ·
(𝑁 −
1))))) |
338 | 335, 337 | mpbird 247 |
. . 3
⊢ (𝑁 ∈ ℕ →
(log‘(((2 · 𝑁)
− 1)C𝑁)) ≤
((log‘4) · (𝑁
− 1))) |
339 | 54, 63, 11, 338 | leadd2dd 10642 |
. 2
⊢ (𝑁 ∈ ℕ →
((θ‘𝑁) +
(log‘(((2 · 𝑁)
− 1)C𝑁))) ≤
((θ‘𝑁) +
((log‘4) · (𝑁
− 1)))) |
340 | 8, 55, 64, 258, 339 | letrd 10194 |
1
⊢ (𝑁 ∈ ℕ →
(θ‘((2 · 𝑁) − 1)) ≤ ((θ‘𝑁) + ((log‘4) ·
(𝑁 −
1)))) |