MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  chtublem Structured version   Visualization version   GIF version

Theorem chtublem 24681
Description: Lemma for chtub 24682. (Contributed by Mario Carneiro, 13-Mar-2014.)
Assertion
Ref Expression
chtublem (𝑁 ∈ ℕ → (θ‘((2 · 𝑁) − 1)) ≤ ((θ‘𝑁) + ((log‘4) · (𝑁 − 1))))

Proof of Theorem chtublem
Dummy variables 𝑘 𝑛 𝑝 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 2nn 11035 . . . . . 6 2 ∈ ℕ
2 nnmulcl 10893 . . . . . 6 ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 · 𝑁) ∈ ℕ)
31, 2mpan 701 . . . . 5 (𝑁 ∈ ℕ → (2 · 𝑁) ∈ ℕ)
43nnred 10885 . . . 4 (𝑁 ∈ ℕ → (2 · 𝑁) ∈ ℝ)
5 peano2rem 10200 . . . 4 ((2 · 𝑁) ∈ ℝ → ((2 · 𝑁) − 1) ∈ ℝ)
64, 5syl 17 . . 3 (𝑁 ∈ ℕ → ((2 · 𝑁) − 1) ∈ ℝ)
7 chtcl 24580 . . 3 (((2 · 𝑁) − 1) ∈ ℝ → (θ‘((2 · 𝑁) − 1)) ∈ ℝ)
86, 7syl 17 . 2 (𝑁 ∈ ℕ → (θ‘((2 · 𝑁) − 1)) ∈ ℝ)
9 nnre 10877 . . . 4 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
10 chtcl 24580 . . . 4 (𝑁 ∈ ℝ → (θ‘𝑁) ∈ ℝ)
119, 10syl 17 . . 3 (𝑁 ∈ ℕ → (θ‘𝑁) ∈ ℝ)
12 nnnn0 11149 . . . . . . 7 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
13 2m1e1 10985 . . . . . . . . . . 11 (2 − 1) = 1
1413oveq2i 6538 . . . . . . . . . 10 ((2 · 𝑁) − (2 − 1)) = ((2 · 𝑁) − 1)
153nncnd 10886 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (2 · 𝑁) ∈ ℂ)
16 2cn 10941 . . . . . . . . . . . . 13 2 ∈ ℂ
17 ax-1cn 9851 . . . . . . . . . . . . 13 1 ∈ ℂ
18 subsub 10163 . . . . . . . . . . . . 13 (((2 · 𝑁) ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ) → ((2 · 𝑁) − (2 − 1)) = (((2 · 𝑁) − 2) + 1))
1916, 17, 18mp3an23 1407 . . . . . . . . . . . 12 ((2 · 𝑁) ∈ ℂ → ((2 · 𝑁) − (2 − 1)) = (((2 · 𝑁) − 2) + 1))
2015, 19syl 17 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((2 · 𝑁) − (2 − 1)) = (((2 · 𝑁) − 2) + 1))
21 nncn 10878 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
22 subdi 10315 . . . . . . . . . . . . . . 15 ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → (2 · (𝑁 − 1)) = ((2 · 𝑁) − (2 · 1)))
2316, 17, 22mp3an13 1406 . . . . . . . . . . . . . 14 (𝑁 ∈ ℂ → (2 · (𝑁 − 1)) = ((2 · 𝑁) − (2 · 1)))
2421, 23syl 17 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (2 · (𝑁 − 1)) = ((2 · 𝑁) − (2 · 1)))
25 2t1e2 11026 . . . . . . . . . . . . . 14 (2 · 1) = 2
2625oveq2i 6538 . . . . . . . . . . . . 13 ((2 · 𝑁) − (2 · 1)) = ((2 · 𝑁) − 2)
2724, 26syl6eq 2659 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (2 · (𝑁 − 1)) = ((2 · 𝑁) − 2))
2827oveq1d 6542 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((2 · (𝑁 − 1)) + 1) = (((2 · 𝑁) − 2) + 1))
2920, 28eqtr4d 2646 . . . . . . . . . 10 (𝑁 ∈ ℕ → ((2 · 𝑁) − (2 − 1)) = ((2 · (𝑁 − 1)) + 1))
3014, 29syl5eqr 2657 . . . . . . . . 9 (𝑁 ∈ ℕ → ((2 · 𝑁) − 1) = ((2 · (𝑁 − 1)) + 1))
31 2nn0 11159 . . . . . . . . . . 11 2 ∈ ℕ0
32 nnm1nn0 11184 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
33 nn0mulcl 11179 . . . . . . . . . . 11 ((2 ∈ ℕ0 ∧ (𝑁 − 1) ∈ ℕ0) → (2 · (𝑁 − 1)) ∈ ℕ0)
3431, 32, 33sylancr 693 . . . . . . . . . 10 (𝑁 ∈ ℕ → (2 · (𝑁 − 1)) ∈ ℕ0)
35 nn0p1nn 11182 . . . . . . . . . 10 ((2 · (𝑁 − 1)) ∈ ℕ0 → ((2 · (𝑁 − 1)) + 1) ∈ ℕ)
3634, 35syl 17 . . . . . . . . 9 (𝑁 ∈ ℕ → ((2 · (𝑁 − 1)) + 1) ∈ ℕ)
3730, 36eqeltrd 2687 . . . . . . . 8 (𝑁 ∈ ℕ → ((2 · 𝑁) − 1) ∈ ℕ)
38 nnnn0 11149 . . . . . . . 8 (((2 · 𝑁) − 1) ∈ ℕ → ((2 · 𝑁) − 1) ∈ ℕ0)
3937, 38syl 17 . . . . . . 7 (𝑁 ∈ ℕ → ((2 · 𝑁) − 1) ∈ ℕ0)
40 1re 9896 . . . . . . . . . . 11 1 ∈ ℝ
4140a1i 11 . . . . . . . . . 10 (𝑁 ∈ ℕ → 1 ∈ ℝ)
42 nnge1 10896 . . . . . . . . . 10 (𝑁 ∈ ℕ → 1 ≤ 𝑁)
4341, 9, 9, 42leadd2dd 10494 . . . . . . . . 9 (𝑁 ∈ ℕ → (𝑁 + 1) ≤ (𝑁 + 𝑁))
44212timesd 11125 . . . . . . . . 9 (𝑁 ∈ ℕ → (2 · 𝑁) = (𝑁 + 𝑁))
4543, 44breqtrrd 4605 . . . . . . . 8 (𝑁 ∈ ℕ → (𝑁 + 1) ≤ (2 · 𝑁))
46 leaddsub 10356 . . . . . . . . 9 ((𝑁 ∈ ℝ ∧ 1 ∈ ℝ ∧ (2 · 𝑁) ∈ ℝ) → ((𝑁 + 1) ≤ (2 · 𝑁) ↔ 𝑁 ≤ ((2 · 𝑁) − 1)))
479, 41, 4, 46syl3anc 1317 . . . . . . . 8 (𝑁 ∈ ℕ → ((𝑁 + 1) ≤ (2 · 𝑁) ↔ 𝑁 ≤ ((2 · 𝑁) − 1)))
4845, 47mpbid 220 . . . . . . 7 (𝑁 ∈ ℕ → 𝑁 ≤ ((2 · 𝑁) − 1))
49 elfz2nn0 12258 . . . . . . 7 (𝑁 ∈ (0...((2 · 𝑁) − 1)) ↔ (𝑁 ∈ ℕ0 ∧ ((2 · 𝑁) − 1) ∈ ℕ0𝑁 ≤ ((2 · 𝑁) − 1)))
5012, 39, 48, 49syl3anbrc 1238 . . . . . 6 (𝑁 ∈ ℕ → 𝑁 ∈ (0...((2 · 𝑁) − 1)))
51 bccl2 12930 . . . . . 6 (𝑁 ∈ (0...((2 · 𝑁) − 1)) → (((2 · 𝑁) − 1)C𝑁) ∈ ℕ)
5250, 51syl 17 . . . . 5 (𝑁 ∈ ℕ → (((2 · 𝑁) − 1)C𝑁) ∈ ℕ)
5352nnrpd 11705 . . . 4 (𝑁 ∈ ℕ → (((2 · 𝑁) − 1)C𝑁) ∈ ℝ+)
5453relogcld 24118 . . 3 (𝑁 ∈ ℕ → (log‘(((2 · 𝑁) − 1)C𝑁)) ∈ ℝ)
5511, 54readdcld 9926 . 2 (𝑁 ∈ ℕ → ((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁))) ∈ ℝ)
56 4re 10947 . . . . . 6 4 ∈ ℝ
57 4pos 10966 . . . . . 6 0 < 4
5856, 57elrpii 11670 . . . . 5 4 ∈ ℝ+
59 relogcl 24071 . . . . 5 (4 ∈ ℝ+ → (log‘4) ∈ ℝ)
6058, 59ax-mp 5 . . . 4 (log‘4) ∈ ℝ
6132nn0red 11202 . . . 4 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℝ)
62 remulcl 9878 . . . 4 (((log‘4) ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ) → ((log‘4) · (𝑁 − 1)) ∈ ℝ)
6360, 61, 62sylancr 693 . . 3 (𝑁 ∈ ℕ → ((log‘4) · (𝑁 − 1)) ∈ ℝ)
6411, 63readdcld 9926 . 2 (𝑁 ∈ ℕ → ((θ‘𝑁) + ((log‘4) · (𝑁 − 1))) ∈ ℝ)
65 iftrue 4041 . . . . . . . . . . . 12 (𝑝 ≤ ((2 · 𝑁) − 1) → if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) = 1)
6665adantl 480 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ ((2 · 𝑁) − 1)) → if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) = 1)
67 simpr 475 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℙ)
6852adantr 479 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (((2 · 𝑁) − 1)C𝑁) ∈ ℕ)
6967, 68pccld 15342 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)) ∈ ℕ0)
70 nn0addge1 11189 . . . . . . . . . . . . . . 15 ((1 ∈ ℝ ∧ (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)) ∈ ℕ0) → 1 ≤ (1 + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))
7140, 69, 70sylancr 693 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 1 ≤ (1 + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))
72 iftrue 4041 . . . . . . . . . . . . . . . 16 (𝑝𝑁 → if(𝑝𝑁, 1, 0) = 1)
7372oveq1d 6542 . . . . . . . . . . . . . . 15 (𝑝𝑁 → (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) = (1 + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))
7473breq2d 4589 . . . . . . . . . . . . . 14 (𝑝𝑁 → (1 ≤ (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) ↔ 1 ≤ (1 + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))))
7571, 74syl5ibrcom 235 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝𝑁 → 1 ≤ (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))))
7675adantr 479 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ ((2 · 𝑁) − 1)) → (𝑝𝑁 → 1 ≤ (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))))
77 prmnn 15175 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
7877ad2antlr 758 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → 𝑝 ∈ ℕ)
79 simprl 789 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → 𝑝 ≤ ((2 · 𝑁) − 1))
80 prmz 15176 . . . . . . . . . . . . . . . . . . . 20 (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
8137nnzd 11316 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ → ((2 · 𝑁) − 1) ∈ ℤ)
82 eluz 11536 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 ∈ ℤ ∧ ((2 · 𝑁) − 1) ∈ ℤ) → (((2 · 𝑁) − 1) ∈ (ℤ𝑝) ↔ 𝑝 ≤ ((2 · 𝑁) − 1)))
8380, 81, 82syl2anr 493 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (((2 · 𝑁) − 1) ∈ (ℤ𝑝) ↔ 𝑝 ≤ ((2 · 𝑁) − 1)))
8483adantr 479 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → (((2 · 𝑁) − 1) ∈ (ℤ𝑝) ↔ 𝑝 ≤ ((2 · 𝑁) − 1)))
8579, 84mpbird 245 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → ((2 · 𝑁) − 1) ∈ (ℤ𝑝))
86 dvdsfac 14835 . . . . . . . . . . . . . . . . 17 ((𝑝 ∈ ℕ ∧ ((2 · 𝑁) − 1) ∈ (ℤ𝑝)) → 𝑝 ∥ (!‘((2 · 𝑁) − 1)))
8778, 85, 86syl2anc 690 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → 𝑝 ∥ (!‘((2 · 𝑁) − 1)))
88 id 22 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ ℙ → 𝑝 ∈ ℙ)
89 faccl 12890 . . . . . . . . . . . . . . . . . . 19 (((2 · 𝑁) − 1) ∈ ℕ0 → (!‘((2 · 𝑁) − 1)) ∈ ℕ)
9039, 89syl 17 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → (!‘((2 · 𝑁) − 1)) ∈ ℕ)
91 pcelnn 15361 . . . . . . . . . . . . . . . . . 18 ((𝑝 ∈ ℙ ∧ (!‘((2 · 𝑁) − 1)) ∈ ℕ) → ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) ∈ ℕ ↔ 𝑝 ∥ (!‘((2 · 𝑁) − 1))))
9288, 90, 91syl2anr 493 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) ∈ ℕ ↔ 𝑝 ∥ (!‘((2 · 𝑁) − 1))))
9392adantr 479 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) ∈ ℕ ↔ 𝑝 ∥ (!‘((2 · 𝑁) − 1))))
9487, 93mpbird 245 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → (𝑝 pCnt (!‘((2 · 𝑁) − 1))) ∈ ℕ)
9594nnge1d 10913 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → 1 ≤ (𝑝 pCnt (!‘((2 · 𝑁) − 1))))
96 iffalse 4044 . . . . . . . . . . . . . . . . 17 𝑝𝑁 → if(𝑝𝑁, 1, 0) = 0)
9796oveq1d 6542 . . . . . . . . . . . . . . . 16 𝑝𝑁 → (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) = (0 + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))
9897ad2antll 760 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) = (0 + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))
9969nn0cnd 11203 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)) ∈ ℂ)
10099addid2d 10089 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (0 + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) = (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))
101100adantr 479 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → (0 + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) = (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))
102 bcval2 12912 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ (0...((2 · 𝑁) − 1)) → (((2 · 𝑁) − 1)C𝑁) = ((!‘((2 · 𝑁) − 1)) / ((!‘(((2 · 𝑁) − 1) − 𝑁)) · (!‘𝑁))))
10350, 102syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ → (((2 · 𝑁) − 1)C𝑁) = ((!‘((2 · 𝑁) − 1)) / ((!‘(((2 · 𝑁) − 1) − 𝑁)) · (!‘𝑁))))
10444oveq1d 6542 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ ℕ → ((2 · 𝑁) − 1) = ((𝑁 + 𝑁) − 1))
10517a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ ℕ → 1 ∈ ℂ)
10621, 21, 105addsubassd 10264 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ ℕ → ((𝑁 + 𝑁) − 1) = (𝑁 + (𝑁 − 1)))
107104, 106eqtrd 2643 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℕ → ((2 · 𝑁) − 1) = (𝑁 + (𝑁 − 1)))
108107oveq1d 6542 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ → (((2 · 𝑁) − 1) − 𝑁) = ((𝑁 + (𝑁 − 1)) − 𝑁))
10932nn0cnd 11203 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℂ)
11021, 109pncan2d 10246 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ → ((𝑁 + (𝑁 − 1)) − 𝑁) = (𝑁 − 1))
111108, 110eqtrd 2643 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ → (((2 · 𝑁) − 1) − 𝑁) = (𝑁 − 1))
112111fveq2d 6092 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ ℕ → (!‘(((2 · 𝑁) − 1) − 𝑁)) = (!‘(𝑁 − 1)))
113112oveq1d 6542 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ ℕ → ((!‘(((2 · 𝑁) − 1) − 𝑁)) · (!‘𝑁)) = ((!‘(𝑁 − 1)) · (!‘𝑁)))
114113oveq2d 6543 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ → ((!‘((2 · 𝑁) − 1)) / ((!‘(((2 · 𝑁) − 1) − 𝑁)) · (!‘𝑁))) = ((!‘((2 · 𝑁) − 1)) / ((!‘(𝑁 − 1)) · (!‘𝑁))))
115103, 114eqtrd 2643 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ → (((2 · 𝑁) − 1)C𝑁) = ((!‘((2 · 𝑁) − 1)) / ((!‘(𝑁 − 1)) · (!‘𝑁))))
116115adantr 479 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (((2 · 𝑁) − 1)C𝑁) = ((!‘((2 · 𝑁) − 1)) / ((!‘(𝑁 − 1)) · (!‘𝑁))))
117116oveq2d 6543 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)) = (𝑝 pCnt ((!‘((2 · 𝑁) − 1)) / ((!‘(𝑁 − 1)) · (!‘𝑁)))))
118 nnz 11235 . . . . . . . . . . . . . . . . . . . . . 22 ((!‘((2 · 𝑁) − 1)) ∈ ℕ → (!‘((2 · 𝑁) − 1)) ∈ ℤ)
119 nnne0 10903 . . . . . . . . . . . . . . . . . . . . . 22 ((!‘((2 · 𝑁) − 1)) ∈ ℕ → (!‘((2 · 𝑁) − 1)) ≠ 0)
120118, 119jca 552 . . . . . . . . . . . . . . . . . . . . 21 ((!‘((2 · 𝑁) − 1)) ∈ ℕ → ((!‘((2 · 𝑁) − 1)) ∈ ℤ ∧ (!‘((2 · 𝑁) − 1)) ≠ 0))
12190, 120syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ → ((!‘((2 · 𝑁) − 1)) ∈ ℤ ∧ (!‘((2 · 𝑁) − 1)) ≠ 0))
122121adantr 479 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((!‘((2 · 𝑁) − 1)) ∈ ℤ ∧ (!‘((2 · 𝑁) − 1)) ≠ 0))
123 faccl 12890 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑁 − 1) ∈ ℕ0 → (!‘(𝑁 − 1)) ∈ ℕ)
12432, 123syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ → (!‘(𝑁 − 1)) ∈ ℕ)
125 faccl 12890 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ)
12612, 125syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ → (!‘𝑁) ∈ ℕ)
127124, 126nnmulcld 10918 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ → ((!‘(𝑁 − 1)) · (!‘𝑁)) ∈ ℕ)
128127adantr 479 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((!‘(𝑁 − 1)) · (!‘𝑁)) ∈ ℕ)
129 pcdiv 15344 . . . . . . . . . . . . . . . . . . 19 ((𝑝 ∈ ℙ ∧ ((!‘((2 · 𝑁) − 1)) ∈ ℤ ∧ (!‘((2 · 𝑁) − 1)) ≠ 0) ∧ ((!‘(𝑁 − 1)) · (!‘𝑁)) ∈ ℕ) → (𝑝 pCnt ((!‘((2 · 𝑁) − 1)) / ((!‘(𝑁 − 1)) · (!‘𝑁)))) = ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − (𝑝 pCnt ((!‘(𝑁 − 1)) · (!‘𝑁)))))
13067, 122, 128, 129syl3anc 1317 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((!‘((2 · 𝑁) − 1)) / ((!‘(𝑁 − 1)) · (!‘𝑁)))) = ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − (𝑝 pCnt ((!‘(𝑁 − 1)) · (!‘𝑁)))))
131 nnz 11235 . . . . . . . . . . . . . . . . . . . . . . 23 ((!‘(𝑁 − 1)) ∈ ℕ → (!‘(𝑁 − 1)) ∈ ℤ)
132 nnne0 10903 . . . . . . . . . . . . . . . . . . . . . . 23 ((!‘(𝑁 − 1)) ∈ ℕ → (!‘(𝑁 − 1)) ≠ 0)
133131, 132jca 552 . . . . . . . . . . . . . . . . . . . . . 22 ((!‘(𝑁 − 1)) ∈ ℕ → ((!‘(𝑁 − 1)) ∈ ℤ ∧ (!‘(𝑁 − 1)) ≠ 0))
134124, 133syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ → ((!‘(𝑁 − 1)) ∈ ℤ ∧ (!‘(𝑁 − 1)) ≠ 0))
135134adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((!‘(𝑁 − 1)) ∈ ℤ ∧ (!‘(𝑁 − 1)) ≠ 0))
136 nnz 11235 . . . . . . . . . . . . . . . . . . . . . . 23 ((!‘𝑁) ∈ ℕ → (!‘𝑁) ∈ ℤ)
137 nnne0 10903 . . . . . . . . . . . . . . . . . . . . . . 23 ((!‘𝑁) ∈ ℕ → (!‘𝑁) ≠ 0)
138136, 137jca 552 . . . . . . . . . . . . . . . . . . . . . 22 ((!‘𝑁) ∈ ℕ → ((!‘𝑁) ∈ ℤ ∧ (!‘𝑁) ≠ 0))
139126, 138syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ → ((!‘𝑁) ∈ ℤ ∧ (!‘𝑁) ≠ 0))
140139adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((!‘𝑁) ∈ ℤ ∧ (!‘𝑁) ≠ 0))
141 pcmul 15343 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 ∈ ℙ ∧ ((!‘(𝑁 − 1)) ∈ ℤ ∧ (!‘(𝑁 − 1)) ≠ 0) ∧ ((!‘𝑁) ∈ ℤ ∧ (!‘𝑁) ≠ 0)) → (𝑝 pCnt ((!‘(𝑁 − 1)) · (!‘𝑁))) = ((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁))))
14267, 135, 140, 141syl3anc 1317 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((!‘(𝑁 − 1)) · (!‘𝑁))) = ((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁))))
143142oveq2d 6543 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − (𝑝 pCnt ((!‘(𝑁 − 1)) · (!‘𝑁)))) = ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − ((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁)))))
144117, 130, 1433eqtrd 2647 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)) = ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − ((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁)))))
145144adantr 479 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)) = ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − ((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁)))))
146 simprr 791 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → ¬ 𝑝𝑁)
147 prmfac1 15218 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑁 ∈ ℕ0𝑝 ∈ ℙ ∧ 𝑝 ∥ (!‘𝑁)) → 𝑝𝑁)
1481473expia 1258 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑁 ∈ ℕ0𝑝 ∈ ℙ) → (𝑝 ∥ (!‘𝑁) → 𝑝𝑁))
14912, 148sylan 486 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (!‘𝑁) → 𝑝𝑁))
150149adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → (𝑝 ∥ (!‘𝑁) → 𝑝𝑁))
151146, 150mtod 187 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → ¬ 𝑝 ∥ (!‘𝑁))
15280adantl 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℤ)
153135simpld 473 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (!‘(𝑁 − 1)) ∈ ℤ)
154 nnz 11235 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
155154adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑁 ∈ ℤ)
156 dvdsmultr1 14806 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑝 ∈ ℤ ∧ (!‘(𝑁 − 1)) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑝 ∥ (!‘(𝑁 − 1)) → 𝑝 ∥ ((!‘(𝑁 − 1)) · 𝑁)))
157152, 153, 155, 156syl3anc 1317 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (!‘(𝑁 − 1)) → 𝑝 ∥ ((!‘(𝑁 − 1)) · 𝑁)))
158 facnn2 12889 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ → (!‘𝑁) = ((!‘(𝑁 − 1)) · 𝑁))
159158adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (!‘𝑁) = ((!‘(𝑁 − 1)) · 𝑁))
160159breq2d 4589 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (!‘𝑁) ↔ 𝑝 ∥ ((!‘(𝑁 − 1)) · 𝑁)))
161157, 160sylibrd 247 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (!‘(𝑁 − 1)) → 𝑝 ∥ (!‘𝑁)))
162161adantr 479 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → (𝑝 ∥ (!‘(𝑁 − 1)) → 𝑝 ∥ (!‘𝑁)))
163151, 162mtod 187 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → ¬ 𝑝 ∥ (!‘(𝑁 − 1)))
164 pceq0 15362 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑝 ∈ ℙ ∧ (!‘(𝑁 − 1)) ∈ ℕ) → ((𝑝 pCnt (!‘(𝑁 − 1))) = 0 ↔ ¬ 𝑝 ∥ (!‘(𝑁 − 1))))
16588, 124, 164syl2anr 493 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt (!‘(𝑁 − 1))) = 0 ↔ ¬ 𝑝 ∥ (!‘(𝑁 − 1))))
166165adantr 479 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → ((𝑝 pCnt (!‘(𝑁 − 1))) = 0 ↔ ¬ 𝑝 ∥ (!‘(𝑁 − 1))))
167163, 166mpbird 245 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → (𝑝 pCnt (!‘(𝑁 − 1))) = 0)
168 pceq0 15362 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑝 ∈ ℙ ∧ (!‘𝑁) ∈ ℕ) → ((𝑝 pCnt (!‘𝑁)) = 0 ↔ ¬ 𝑝 ∥ (!‘𝑁)))
16988, 126, 168syl2anr 493 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt (!‘𝑁)) = 0 ↔ ¬ 𝑝 ∥ (!‘𝑁)))
170169adantr 479 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → ((𝑝 pCnt (!‘𝑁)) = 0 ↔ ¬ 𝑝 ∥ (!‘𝑁)))
171151, 170mpbird 245 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → (𝑝 pCnt (!‘𝑁)) = 0)
172167, 171oveq12d 6545 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → ((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁))) = (0 + 0))
173 00id 10063 . . . . . . . . . . . . . . . . . 18 (0 + 0) = 0
174172, 173syl6eq 2659 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → ((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁))) = 0)
175174oveq2d 6543 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − ((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁)))) = ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − 0))
176 pccl 15341 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 ∈ ℙ ∧ (!‘((2 · 𝑁) − 1)) ∈ ℕ) → (𝑝 pCnt (!‘((2 · 𝑁) − 1))) ∈ ℕ0)
17788, 90, 176syl2anr 493 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (!‘((2 · 𝑁) − 1))) ∈ ℕ0)
178177nn0cnd 11203 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (!‘((2 · 𝑁) − 1))) ∈ ℂ)
179178subid1d 10233 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − 0) = (𝑝 pCnt (!‘((2 · 𝑁) − 1))))
180179adantr 479 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − 0) = (𝑝 pCnt (!‘((2 · 𝑁) − 1))))
181145, 175, 1803eqtrd 2647 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)) = (𝑝 pCnt (!‘((2 · 𝑁) − 1))))
18298, 101, 1813eqtrd 2647 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) = (𝑝 pCnt (!‘((2 · 𝑁) − 1))))
18395, 182breqtrrd 4605 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → 1 ≤ (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))
184183expr 640 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ ((2 · 𝑁) − 1)) → (¬ 𝑝𝑁 → 1 ≤ (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))))
18576, 184pm2.61d 168 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ ((2 · 𝑁) − 1)) → 1 ≤ (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))
18666, 185eqbrtrd 4599 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ ((2 · 𝑁) − 1)) → if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) ≤ (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))
187186ex 448 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 ≤ ((2 · 𝑁) − 1) → if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) ≤ (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))))
188 1nn0 11158 . . . . . . . . . . . . 13 1 ∈ ℕ0
189 0nn0 11157 . . . . . . . . . . . . 13 0 ∈ ℕ0
190188, 189keepel 4104 . . . . . . . . . . . 12 if(𝑝𝑁, 1, 0) ∈ ℕ0
191 nn0addcl 11178 . . . . . . . . . . . 12 ((if(𝑝𝑁, 1, 0) ∈ ℕ0 ∧ (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)) ∈ ℕ0) → (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) ∈ ℕ0)
192190, 69, 191sylancr 693 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) ∈ ℕ0)
193192nn0ge0d 11204 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 0 ≤ (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))
194 iffalse 4044 . . . . . . . . . . 11 𝑝 ≤ ((2 · 𝑁) − 1) → if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) = 0)
195194breq1d 4587 . . . . . . . . . 10 𝑝 ≤ ((2 · 𝑁) − 1) → (if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) ≤ (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) ↔ 0 ≤ (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))))
196193, 195syl5ibrcom 235 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (¬ 𝑝 ≤ ((2 · 𝑁) − 1) → if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) ≤ (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))))
197187, 196pm2.61d 168 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) ≤ (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))
198 eqid 2609 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1))
199198prmorcht 24649 . . . . . . . . . . . 12 (((2 · 𝑁) − 1) ∈ ℕ → (exp‘(θ‘((2 · 𝑁) − 1))) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘((2 · 𝑁) − 1)))
20037, 199syl 17 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (exp‘(θ‘((2 · 𝑁) − 1))) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘((2 · 𝑁) − 1)))
201200oveq2d 6543 . . . . . . . . . 10 (𝑁 ∈ ℕ → (𝑝 pCnt (exp‘(θ‘((2 · 𝑁) − 1)))) = (𝑝 pCnt (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘((2 · 𝑁) − 1))))
202201adantr 479 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (exp‘(θ‘((2 · 𝑁) − 1)))) = (𝑝 pCnt (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘((2 · 𝑁) − 1))))
203 nncn 10878 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
204203exp1d 12823 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (𝑛↑1) = 𝑛)
205204ifeq1d 4053 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → if(𝑛 ∈ ℙ, (𝑛↑1), 1) = if(𝑛 ∈ ℙ, 𝑛, 1))
206205mpteq2ia 4662 . . . . . . . . . . 11 (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑1), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1))
207206eqcomi 2618 . . . . . . . . . 10 (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑1), 1))
208188a1i 11 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑛 ∈ ℙ) → 1 ∈ ℕ0)
209208ralrimiva 2948 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ∀𝑛 ∈ ℙ 1 ∈ ℕ0)
21037adantr 479 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((2 · 𝑁) − 1) ∈ ℕ)
211 eqidd 2610 . . . . . . . . . 10 (𝑛 = 𝑝 → 1 = 1)
212207, 209, 210, 67, 211pcmpt 15383 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘((2 · 𝑁) − 1))) = if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0))
213202, 212eqtrd 2643 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (exp‘(θ‘((2 · 𝑁) − 1)))) = if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0))
214 efchtcl 24582 . . . . . . . . . . . . 13 (𝑁 ∈ ℝ → (exp‘(θ‘𝑁)) ∈ ℕ)
2159, 214syl 17 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (exp‘(θ‘𝑁)) ∈ ℕ)
216215adantr 479 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (exp‘(θ‘𝑁)) ∈ ℕ)
217 nnz 11235 . . . . . . . . . . . 12 ((exp‘(θ‘𝑁)) ∈ ℕ → (exp‘(θ‘𝑁)) ∈ ℤ)
218 nnne0 10903 . . . . . . . . . . . 12 ((exp‘(θ‘𝑁)) ∈ ℕ → (exp‘(θ‘𝑁)) ≠ 0)
219217, 218jca 552 . . . . . . . . . . 11 ((exp‘(θ‘𝑁)) ∈ ℕ → ((exp‘(θ‘𝑁)) ∈ ℤ ∧ (exp‘(θ‘𝑁)) ≠ 0))
220216, 219syl 17 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((exp‘(θ‘𝑁)) ∈ ℤ ∧ (exp‘(θ‘𝑁)) ≠ 0))
221 nnz 11235 . . . . . . . . . . . 12 ((((2 · 𝑁) − 1)C𝑁) ∈ ℕ → (((2 · 𝑁) − 1)C𝑁) ∈ ℤ)
222 nnne0 10903 . . . . . . . . . . . 12 ((((2 · 𝑁) − 1)C𝑁) ∈ ℕ → (((2 · 𝑁) − 1)C𝑁) ≠ 0)
223221, 222jca 552 . . . . . . . . . . 11 ((((2 · 𝑁) − 1)C𝑁) ∈ ℕ → ((((2 · 𝑁) − 1)C𝑁) ∈ ℤ ∧ (((2 · 𝑁) − 1)C𝑁) ≠ 0))
22468, 223syl 17 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((((2 · 𝑁) − 1)C𝑁) ∈ ℤ ∧ (((2 · 𝑁) − 1)C𝑁) ≠ 0))
225 pcmul 15343 . . . . . . . . . 10 ((𝑝 ∈ ℙ ∧ ((exp‘(θ‘𝑁)) ∈ ℤ ∧ (exp‘(θ‘𝑁)) ≠ 0) ∧ ((((2 · 𝑁) − 1)C𝑁) ∈ ℤ ∧ (((2 · 𝑁) − 1)C𝑁) ≠ 0)) → (𝑝 pCnt ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))) = ((𝑝 pCnt (exp‘(θ‘𝑁))) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))
22667, 220, 224, 225syl3anc 1317 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))) = ((𝑝 pCnt (exp‘(θ‘𝑁))) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))
227198prmorcht 24649 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (exp‘(θ‘𝑁)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑁))
228227oveq2d 6543 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (𝑝 pCnt (exp‘(θ‘𝑁))) = (𝑝 pCnt (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑁)))
229228adantr 479 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (exp‘(θ‘𝑁))) = (𝑝 pCnt (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑁)))
230 simpl 471 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑁 ∈ ℕ)
231207, 209, 230, 67, 211pcmpt 15383 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑁)) = if(𝑝𝑁, 1, 0))
232229, 231eqtrd 2643 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (exp‘(θ‘𝑁))) = if(𝑝𝑁, 1, 0))
233232oveq1d 6542 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt (exp‘(θ‘𝑁))) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) = (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))
234226, 233eqtrd 2643 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))) = (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))
235197, 213, 2343brtr4d 4609 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (exp‘(θ‘((2 · 𝑁) − 1)))) ≤ (𝑝 pCnt ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))))
236235ralrimiva 2948 . . . . . 6 (𝑁 ∈ ℕ → ∀𝑝 ∈ ℙ (𝑝 pCnt (exp‘(θ‘((2 · 𝑁) − 1)))) ≤ (𝑝 pCnt ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))))
237 efchtcl 24582 . . . . . . . . 9 (((2 · 𝑁) − 1) ∈ ℝ → (exp‘(θ‘((2 · 𝑁) − 1))) ∈ ℕ)
2386, 237syl 17 . . . . . . . 8 (𝑁 ∈ ℕ → (exp‘(θ‘((2 · 𝑁) − 1))) ∈ ℕ)
239238nnzd 11316 . . . . . . 7 (𝑁 ∈ ℕ → (exp‘(θ‘((2 · 𝑁) − 1))) ∈ ℤ)
240215, 52nnmulcld 10918 . . . . . . . 8 (𝑁 ∈ ℕ → ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) ∈ ℕ)
241240nnzd 11316 . . . . . . 7 (𝑁 ∈ ℕ → ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) ∈ ℤ)
242 pc2dvds 15370 . . . . . . 7 (((exp‘(θ‘((2 · 𝑁) − 1))) ∈ ℤ ∧ ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) ∈ ℤ) → ((exp‘(θ‘((2 · 𝑁) − 1))) ∥ ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt (exp‘(θ‘((2 · 𝑁) − 1)))) ≤ (𝑝 pCnt ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)))))
243239, 241, 242syl2anc 690 . . . . . 6 (𝑁 ∈ ℕ → ((exp‘(θ‘((2 · 𝑁) − 1))) ∥ ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt (exp‘(θ‘((2 · 𝑁) − 1)))) ≤ (𝑝 pCnt ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)))))
244236, 243mpbird 245 . . . . 5 (𝑁 ∈ ℕ → (exp‘(θ‘((2 · 𝑁) − 1))) ∥ ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)))
245 dvdsle 14819 . . . . . 6 (((exp‘(θ‘((2 · 𝑁) − 1))) ∈ ℤ ∧ ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) ∈ ℕ) → ((exp‘(θ‘((2 · 𝑁) − 1))) ∥ ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) → (exp‘(θ‘((2 · 𝑁) − 1))) ≤ ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))))
246239, 240, 245syl2anc 690 . . . . 5 (𝑁 ∈ ℕ → ((exp‘(θ‘((2 · 𝑁) − 1))) ∥ ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) → (exp‘(θ‘((2 · 𝑁) − 1))) ≤ ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))))
247244, 246mpd 15 . . . 4 (𝑁 ∈ ℕ → (exp‘(θ‘((2 · 𝑁) − 1))) ≤ ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)))
24811recnd 9925 . . . . . 6 (𝑁 ∈ ℕ → (θ‘𝑁) ∈ ℂ)
24954recnd 9925 . . . . . 6 (𝑁 ∈ ℕ → (log‘(((2 · 𝑁) − 1)C𝑁)) ∈ ℂ)
250 efadd 14612 . . . . . 6 (((θ‘𝑁) ∈ ℂ ∧ (log‘(((2 · 𝑁) − 1)C𝑁)) ∈ ℂ) → (exp‘((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁)))) = ((exp‘(θ‘𝑁)) · (exp‘(log‘(((2 · 𝑁) − 1)C𝑁)))))
251248, 249, 250syl2anc 690 . . . . 5 (𝑁 ∈ ℕ → (exp‘((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁)))) = ((exp‘(θ‘𝑁)) · (exp‘(log‘(((2 · 𝑁) − 1)C𝑁)))))
25253reeflogd 24119 . . . . . 6 (𝑁 ∈ ℕ → (exp‘(log‘(((2 · 𝑁) − 1)C𝑁))) = (((2 · 𝑁) − 1)C𝑁))
253252oveq2d 6543 . . . . 5 (𝑁 ∈ ℕ → ((exp‘(θ‘𝑁)) · (exp‘(log‘(((2 · 𝑁) − 1)C𝑁)))) = ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)))
254251, 253eqtrd 2643 . . . 4 (𝑁 ∈ ℕ → (exp‘((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁)))) = ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)))
255247, 254breqtrrd 4605 . . 3 (𝑁 ∈ ℕ → (exp‘(θ‘((2 · 𝑁) − 1))) ≤ (exp‘((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁)))))
256 efle 14636 . . . 4 (((θ‘((2 · 𝑁) − 1)) ∈ ℝ ∧ ((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁))) ∈ ℝ) → ((θ‘((2 · 𝑁) − 1)) ≤ ((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁))) ↔ (exp‘(θ‘((2 · 𝑁) − 1))) ≤ (exp‘((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁))))))
2578, 55, 256syl2anc 690 . . 3 (𝑁 ∈ ℕ → ((θ‘((2 · 𝑁) − 1)) ≤ ((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁))) ↔ (exp‘(θ‘((2 · 𝑁) − 1))) ≤ (exp‘((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁))))))
258255, 257mpbird 245 . 2 (𝑁 ∈ ℕ → (θ‘((2 · 𝑁) − 1)) ≤ ((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁))))
259 fzfid 12592 . . . . . . . . 9 (𝑁 ∈ ℕ → (0...((2 · 𝑁) − 1)) ∈ Fin)
260 elfzelz 12171 . . . . . . . . . . 11 (𝑘 ∈ (0...((2 · 𝑁) − 1)) → 𝑘 ∈ ℤ)
261 bccl 12929 . . . . . . . . . . 11 ((((2 · 𝑁) − 1) ∈ ℕ0𝑘 ∈ ℤ) → (((2 · 𝑁) − 1)C𝑘) ∈ ℕ0)
26239, 260, 261syl2an 492 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...((2 · 𝑁) − 1))) → (((2 · 𝑁) − 1)C𝑘) ∈ ℕ0)
263262nn0red 11202 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...((2 · 𝑁) − 1))) → (((2 · 𝑁) − 1)C𝑘) ∈ ℝ)
264262nn0ge0d 11204 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...((2 · 𝑁) − 1))) → 0 ≤ (((2 · 𝑁) − 1)C𝑘))
265 nn0uz 11557 . . . . . . . . . . . 12 0 = (ℤ‘0)
26632, 265syl6eleq 2697 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (ℤ‘0))
267 fzss1 12209 . . . . . . . . . . 11 ((𝑁 − 1) ∈ (ℤ‘0) → ((𝑁 − 1)...𝑁) ⊆ (0...𝑁))
268266, 267syl 17 . . . . . . . . . 10 (𝑁 ∈ ℕ → ((𝑁 − 1)...𝑁) ⊆ (0...𝑁))
269 eluz 11536 . . . . . . . . . . . . 13 ((𝑁 ∈ ℤ ∧ ((2 · 𝑁) − 1) ∈ ℤ) → (((2 · 𝑁) − 1) ∈ (ℤ𝑁) ↔ 𝑁 ≤ ((2 · 𝑁) − 1)))
270154, 81, 269syl2anc 690 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (((2 · 𝑁) − 1) ∈ (ℤ𝑁) ↔ 𝑁 ≤ ((2 · 𝑁) − 1)))
27148, 270mpbird 245 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((2 · 𝑁) − 1) ∈ (ℤ𝑁))
272 fzss2 12210 . . . . . . . . . . 11 (((2 · 𝑁) − 1) ∈ (ℤ𝑁) → (0...𝑁) ⊆ (0...((2 · 𝑁) − 1)))
273271, 272syl 17 . . . . . . . . . 10 (𝑁 ∈ ℕ → (0...𝑁) ⊆ (0...((2 · 𝑁) − 1)))
274268, 273sstrd 3577 . . . . . . . . 9 (𝑁 ∈ ℕ → ((𝑁 − 1)...𝑁) ⊆ (0...((2 · 𝑁) − 1)))
275259, 263, 264, 274fsumless 14318 . . . . . . . 8 (𝑁 ∈ ℕ → Σ𝑘 ∈ ((𝑁 − 1)...𝑁)(((2 · 𝑁) − 1)C𝑘) ≤ Σ𝑘 ∈ (0...((2 · 𝑁) − 1))(((2 · 𝑁) − 1)C𝑘))
27632nn0zd 11315 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℤ)
277 bccmpl 12916 . . . . . . . . . . . . . . 15 ((((2 · 𝑁) − 1) ∈ ℕ0𝑁 ∈ ℤ) → (((2 · 𝑁) − 1)C𝑁) = (((2 · 𝑁) − 1)C(((2 · 𝑁) − 1) − 𝑁)))
27839, 154, 277syl2anc 690 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → (((2 · 𝑁) − 1)C𝑁) = (((2 · 𝑁) − 1)C(((2 · 𝑁) − 1) − 𝑁)))
279111oveq2d 6543 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → (((2 · 𝑁) − 1)C(((2 · 𝑁) − 1) − 𝑁)) = (((2 · 𝑁) − 1)C(𝑁 − 1)))
280278, 279eqtrd 2643 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (((2 · 𝑁) − 1)C𝑁) = (((2 · 𝑁) − 1)C(𝑁 − 1)))
28152nncnd 10886 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (((2 · 𝑁) − 1)C𝑁) ∈ ℂ)
282280, 281eqeltrrd 2688 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (((2 · 𝑁) − 1)C(𝑁 − 1)) ∈ ℂ)
283 oveq2 6535 . . . . . . . . . . . . 13 (𝑘 = (𝑁 − 1) → (((2 · 𝑁) − 1)C𝑘) = (((2 · 𝑁) − 1)C(𝑁 − 1)))
284283fsum1 14269 . . . . . . . . . . . 12 (((𝑁 − 1) ∈ ℤ ∧ (((2 · 𝑁) − 1)C(𝑁 − 1)) ∈ ℂ) → Σ𝑘 ∈ ((𝑁 − 1)...(𝑁 − 1))(((2 · 𝑁) − 1)C𝑘) = (((2 · 𝑁) − 1)C(𝑁 − 1)))
285276, 282, 284syl2anc 690 . . . . . . . . . . 11 (𝑁 ∈ ℕ → Σ𝑘 ∈ ((𝑁 − 1)...(𝑁 − 1))(((2 · 𝑁) − 1)C𝑘) = (((2 · 𝑁) − 1)C(𝑁 − 1)))
286285, 280eqtr4d 2646 . . . . . . . . . 10 (𝑁 ∈ ℕ → Σ𝑘 ∈ ((𝑁 − 1)...(𝑁 − 1))(((2 · 𝑁) − 1)C𝑘) = (((2 · 𝑁) − 1)C𝑁))
287286oveq1d 6542 . . . . . . . . 9 (𝑁 ∈ ℕ → (Σ𝑘 ∈ ((𝑁 − 1)...(𝑁 − 1))(((2 · 𝑁) − 1)C𝑘) + (((2 · 𝑁) − 1)C𝑁)) = ((((2 · 𝑁) − 1)C𝑁) + (((2 · 𝑁) − 1)C𝑁)))
28821, 105npcand 10248 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((𝑁 − 1) + 1) = 𝑁)
289 uzid 11537 . . . . . . . . . . . . 13 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
290276, 289syl 17 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
291 peano2uz 11576 . . . . . . . . . . . 12 ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
292290, 291syl 17 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
293288, 292eqeltrrd 2688 . . . . . . . . . 10 (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ‘(𝑁 − 1)))
294274sselda 3567 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ((𝑁 − 1)...𝑁)) → 𝑘 ∈ (0...((2 · 𝑁) − 1)))
295262nn0cnd 11203 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...((2 · 𝑁) − 1))) → (((2 · 𝑁) − 1)C𝑘) ∈ ℂ)
296294, 295syldan 485 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ((𝑁 − 1)...𝑁)) → (((2 · 𝑁) − 1)C𝑘) ∈ ℂ)
297 oveq2 6535 . . . . . . . . . 10 (𝑘 = 𝑁 → (((2 · 𝑁) − 1)C𝑘) = (((2 · 𝑁) − 1)C𝑁))
298293, 296, 297fsumm1 14273 . . . . . . . . 9 (𝑁 ∈ ℕ → Σ𝑘 ∈ ((𝑁 − 1)...𝑁)(((2 · 𝑁) − 1)C𝑘) = (Σ𝑘 ∈ ((𝑁 − 1)...(𝑁 − 1))(((2 · 𝑁) − 1)C𝑘) + (((2 · 𝑁) − 1)C𝑁)))
2992812timesd 11125 . . . . . . . . 9 (𝑁 ∈ ℕ → (2 · (((2 · 𝑁) − 1)C𝑁)) = ((((2 · 𝑁) − 1)C𝑁) + (((2 · 𝑁) − 1)C𝑁)))
300287, 298, 2993eqtr4rd 2654 . . . . . . . 8 (𝑁 ∈ ℕ → (2 · (((2 · 𝑁) − 1)C𝑁)) = Σ𝑘 ∈ ((𝑁 − 1)...𝑁)(((2 · 𝑁) − 1)C𝑘))
301 binom11 14352 . . . . . . . . 9 (((2 · 𝑁) − 1) ∈ ℕ0 → (2↑((2 · 𝑁) − 1)) = Σ𝑘 ∈ (0...((2 · 𝑁) − 1))(((2 · 𝑁) − 1)C𝑘))
30239, 301syl 17 . . . . . . . 8 (𝑁 ∈ ℕ → (2↑((2 · 𝑁) − 1)) = Σ𝑘 ∈ (0...((2 · 𝑁) − 1))(((2 · 𝑁) − 1)C𝑘))
303275, 300, 3023brtr4d 4609 . . . . . . 7 (𝑁 ∈ ℕ → (2 · (((2 · 𝑁) − 1)C𝑁)) ≤ (2↑((2 · 𝑁) − 1)))
304 mulcom 9879 . . . . . . . 8 ((2 ∈ ℂ ∧ (((2 · 𝑁) − 1)C𝑁) ∈ ℂ) → (2 · (((2 · 𝑁) − 1)C𝑁)) = ((((2 · 𝑁) − 1)C𝑁) · 2))
30516, 281, 304sylancr 693 . . . . . . 7 (𝑁 ∈ ℕ → (2 · (((2 · 𝑁) − 1)C𝑁)) = ((((2 · 𝑁) − 1)C𝑁) · 2))
30630oveq2d 6543 . . . . . . . 8 (𝑁 ∈ ℕ → (2↑((2 · 𝑁) − 1)) = (2↑((2 · (𝑁 − 1)) + 1)))
307 expp1 12687 . . . . . . . . 9 ((2 ∈ ℂ ∧ (2 · (𝑁 − 1)) ∈ ℕ0) → (2↑((2 · (𝑁 − 1)) + 1)) = ((2↑(2 · (𝑁 − 1))) · 2))
30816, 34, 307sylancr 693 . . . . . . . 8 (𝑁 ∈ ℕ → (2↑((2 · (𝑁 − 1)) + 1)) = ((2↑(2 · (𝑁 − 1))) · 2))
30916a1i 11 . . . . . . . . . . 11 (𝑁 ∈ ℕ → 2 ∈ ℂ)
31031a1i 11 . . . . . . . . . . 11 (𝑁 ∈ ℕ → 2 ∈ ℕ0)
311309, 32, 310expmuld 12831 . . . . . . . . . 10 (𝑁 ∈ ℕ → (2↑(2 · (𝑁 − 1))) = ((2↑2)↑(𝑁 − 1)))
312 sq2 12780 . . . . . . . . . . 11 (2↑2) = 4
313312oveq1i 6537 . . . . . . . . . 10 ((2↑2)↑(𝑁 − 1)) = (4↑(𝑁 − 1))
314311, 313syl6eq 2659 . . . . . . . . 9 (𝑁 ∈ ℕ → (2↑(2 · (𝑁 − 1))) = (4↑(𝑁 − 1)))
315314oveq1d 6542 . . . . . . . 8 (𝑁 ∈ ℕ → ((2↑(2 · (𝑁 − 1))) · 2) = ((4↑(𝑁 − 1)) · 2))
316306, 308, 3153eqtrd 2647 . . . . . . 7 (𝑁 ∈ ℕ → (2↑((2 · 𝑁) − 1)) = ((4↑(𝑁 − 1)) · 2))
317303, 305, 3163brtr3d 4608 . . . . . 6 (𝑁 ∈ ℕ → ((((2 · 𝑁) − 1)C𝑁) · 2) ≤ ((4↑(𝑁 − 1)) · 2))
31852nnred 10885 . . . . . . 7 (𝑁 ∈ ℕ → (((2 · 𝑁) − 1)C𝑁) ∈ ℝ)
319 reexpcl 12697 . . . . . . . 8 ((4 ∈ ℝ ∧ (𝑁 − 1) ∈ ℕ0) → (4↑(𝑁 − 1)) ∈ ℝ)
32056, 32, 319sylancr 693 . . . . . . 7 (𝑁 ∈ ℕ → (4↑(𝑁 − 1)) ∈ ℝ)
321 2re 10940 . . . . . . . . 9 2 ∈ ℝ
322 2pos 10962 . . . . . . . . 9 0 < 2
323321, 322pm3.2i 469 . . . . . . . 8 (2 ∈ ℝ ∧ 0 < 2)
324323a1i 11 . . . . . . 7 (𝑁 ∈ ℕ → (2 ∈ ℝ ∧ 0 < 2))
325 lemul1 10727 . . . . . . 7 (((((2 · 𝑁) − 1)C𝑁) ∈ ℝ ∧ (4↑(𝑁 − 1)) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((((2 · 𝑁) − 1)C𝑁) ≤ (4↑(𝑁 − 1)) ↔ ((((2 · 𝑁) − 1)C𝑁) · 2) ≤ ((4↑(𝑁 − 1)) · 2)))
326318, 320, 324, 325syl3anc 1317 . . . . . 6 (𝑁 ∈ ℕ → ((((2 · 𝑁) − 1)C𝑁) ≤ (4↑(𝑁 − 1)) ↔ ((((2 · 𝑁) − 1)C𝑁) · 2) ≤ ((4↑(𝑁 − 1)) · 2)))
327317, 326mpbird 245 . . . . 5 (𝑁 ∈ ℕ → (((2 · 𝑁) − 1)C𝑁) ≤ (4↑(𝑁 − 1)))
32860recni 9909 . . . . . . . 8 (log‘4) ∈ ℂ
329 mulcom 9879 . . . . . . . 8 (((log‘4) ∈ ℂ ∧ (𝑁 − 1) ∈ ℂ) → ((log‘4) · (𝑁 − 1)) = ((𝑁 − 1) · (log‘4)))
330328, 109, 329sylancr 693 . . . . . . 7 (𝑁 ∈ ℕ → ((log‘4) · (𝑁 − 1)) = ((𝑁 − 1) · (log‘4)))
331330fveq2d 6092 . . . . . 6 (𝑁 ∈ ℕ → (exp‘((log‘4) · (𝑁 − 1))) = (exp‘((𝑁 − 1) · (log‘4))))
332 reexplog 24090 . . . . . . 7 ((4 ∈ ℝ+ ∧ (𝑁 − 1) ∈ ℤ) → (4↑(𝑁 − 1)) = (exp‘((𝑁 − 1) · (log‘4))))
33358, 276, 332sylancr 693 . . . . . 6 (𝑁 ∈ ℕ → (4↑(𝑁 − 1)) = (exp‘((𝑁 − 1) · (log‘4))))
334331, 333eqtr4d 2646 . . . . 5 (𝑁 ∈ ℕ → (exp‘((log‘4) · (𝑁 − 1))) = (4↑(𝑁 − 1)))
335327, 252, 3343brtr4d 4609 . . . 4 (𝑁 ∈ ℕ → (exp‘(log‘(((2 · 𝑁) − 1)C𝑁))) ≤ (exp‘((log‘4) · (𝑁 − 1))))
336 efle 14636 . . . . 5 (((log‘(((2 · 𝑁) − 1)C𝑁)) ∈ ℝ ∧ ((log‘4) · (𝑁 − 1)) ∈ ℝ) → ((log‘(((2 · 𝑁) − 1)C𝑁)) ≤ ((log‘4) · (𝑁 − 1)) ↔ (exp‘(log‘(((2 · 𝑁) − 1)C𝑁))) ≤ (exp‘((log‘4) · (𝑁 − 1)))))
33754, 63, 336syl2anc 690 . . . 4 (𝑁 ∈ ℕ → ((log‘(((2 · 𝑁) − 1)C𝑁)) ≤ ((log‘4) · (𝑁 − 1)) ↔ (exp‘(log‘(((2 · 𝑁) − 1)C𝑁))) ≤ (exp‘((log‘4) · (𝑁 − 1)))))
338335, 337mpbird 245 . . 3 (𝑁 ∈ ℕ → (log‘(((2 · 𝑁) − 1)C𝑁)) ≤ ((log‘4) · (𝑁 − 1)))
33954, 63, 11, 338leadd2dd 10494 . 2 (𝑁 ∈ ℕ → ((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁))) ≤ ((θ‘𝑁) + ((log‘4) · (𝑁 − 1))))
3408, 55, 64, 258, 339letrd 10046 1 (𝑁 ∈ ℕ → (θ‘((2 · 𝑁) − 1)) ≤ ((θ‘𝑁) + ((log‘4) · (𝑁 − 1))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382   = wceq 1474  wcel 1976  wne 2779  wral 2895  wss 3539  ifcif 4035   class class class wbr 4577  cmpt 4637  cfv 5790  (class class class)co 6527  cc 9791  cr 9792  0cc0 9793  1c1 9794   + caddc 9796   · cmul 9798   < clt 9931  cle 9932  cmin 10118   / cdiv 10536  cn 10870  2c2 10920  4c4 10922  0cn0 11142  cz 11213  cuz 11522  +crp 11667  ...cfz 12155  seqcseq 12621  cexp 12680  !cfa 12880  Ccbc 12909  Σcsu 14213  expce 14580  cdvds 14770  cprime 15172   pCnt cpc 15328  logclog 24050  θccht 24562
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-inf2 8399  ax-cnex 9849  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870  ax-pre-sup 9871  ax-addf 9872  ax-mulf 9873
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-iin 4452  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-of 6773  df-om 6936  df-1st 7037  df-2nd 7038  df-supp 7161  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-1o 7425  df-2o 7426  df-oadd 7429  df-er 7607  df-map 7724  df-pm 7725  df-ixp 7773  df-en 7820  df-dom 7821  df-sdom 7822  df-fin 7823  df-fsupp 8137  df-fi 8178  df-sup 8209  df-inf 8210  df-oi 8276  df-card 8626  df-cda 8851  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121  df-div 10537  df-nn 10871  df-2 10929  df-3 10930  df-4 10931  df-5 10932  df-6 10933  df-7 10934  df-8 10935  df-9 10936  df-n0 11143  df-z 11214  df-dec 11329  df-uz 11523  df-q 11624  df-rp 11668  df-xneg 11781  df-xadd 11782  df-xmul 11783  df-ioo 12009  df-ioc 12010  df-ico 12011  df-icc 12012  df-fz 12156  df-fzo 12293  df-fl 12413  df-mod 12489  df-seq 12622  df-exp 12681  df-fac 12881  df-bc 12910  df-hash 12938  df-shft 13604  df-cj 13636  df-re 13637  df-im 13638  df-sqrt 13772  df-abs 13773  df-limsup 13999  df-clim 14016  df-rlim 14017  df-sum 14214  df-ef 14586  df-sin 14588  df-cos 14589  df-pi 14591  df-dvds 14771  df-gcd 15004  df-prm 15173  df-pc 15329  df-struct 15646  df-ndx 15647  df-slot 15648  df-base 15649  df-sets 15650  df-ress 15651  df-plusg 15730  df-mulr 15731  df-starv 15732  df-sca 15733  df-vsca 15734  df-ip 15735  df-tset 15736  df-ple 15737  df-ds 15740  df-unif 15741  df-hom 15742  df-cco 15743  df-rest 15855  df-topn 15856  df-0g 15874  df-gsum 15875  df-topgen 15876  df-pt 15877  df-prds 15880  df-xrs 15934  df-qtop 15939  df-imas 15940  df-xps 15942  df-mre 16018  df-mrc 16019  df-acs 16021  df-mgm 17014  df-sgrp 17056  df-mnd 17067  df-submnd 17108  df-mulg 17313  df-cntz 17522  df-cmn 17967  df-psmet 19508  df-xmet 19509  df-met 19510  df-bl 19511  df-mopn 19512  df-fbas 19513  df-fg 19514  df-cnfld 19517  df-top 20469  df-bases 20470  df-topon 20471  df-topsp 20472  df-cld 20581  df-ntr 20582  df-cls 20583  df-nei 20660  df-lp 20698  df-perf 20699  df-cn 20789  df-cnp 20790  df-haus 20877  df-tx 21123  df-hmeo 21316  df-fil 21408  df-fm 21500  df-flim 21501  df-flf 21502  df-xms 21883  df-ms 21884  df-tms 21885  df-cncf 22437  df-limc 23381  df-dv 23382  df-log 24052  df-cht 24568
This theorem is referenced by:  chtub  24682
  Copyright terms: Public domain W3C validator