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

Theorem chtublem 27060
Description: Lemma for chtub 27061. (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 12282 . . . . . 6 2 ∈ ℕ
2 nnmulcl 12233 . . . . . 6 ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 · 𝑁) ∈ ℕ)
31, 2mpan 687 . . . . 5 (𝑁 ∈ ℕ → (2 · 𝑁) ∈ ℕ)
43nnred 12224 . . . 4 (𝑁 ∈ ℕ → (2 · 𝑁) ∈ ℝ)
5 peano2rem 11524 . . . 4 ((2 · 𝑁) ∈ ℝ → ((2 · 𝑁) − 1) ∈ ℝ)
64, 5syl 17 . . 3 (𝑁 ∈ ℕ → ((2 · 𝑁) − 1) ∈ ℝ)
7 chtcl 26957 . . 3 (((2 · 𝑁) − 1) ∈ ℝ → (θ‘((2 · 𝑁) − 1)) ∈ ℝ)
86, 7syl 17 . 2 (𝑁 ∈ ℕ → (θ‘((2 · 𝑁) − 1)) ∈ ℝ)
9 nnre 12216 . . . 4 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
10 chtcl 26957 . . . 4 (𝑁 ∈ ℝ → (θ‘𝑁) ∈ ℝ)
119, 10syl 17 . . 3 (𝑁 ∈ ℕ → (θ‘𝑁) ∈ ℝ)
12 nnnn0 12476 . . . . . . 7 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
13 2m1e1 12335 . . . . . . . . . . 11 (2 − 1) = 1
1413oveq2i 7412 . . . . . . . . . 10 ((2 · 𝑁) − (2 − 1)) = ((2 · 𝑁) − 1)
153nncnd 12225 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (2 · 𝑁) ∈ ℂ)
16 2cn 12284 . . . . . . . . . . . . 13 2 ∈ ℂ
17 ax-1cn 11164 . . . . . . . . . . . . 13 1 ∈ ℂ
18 subsub 11487 . . . . . . . . . . . . 13 (((2 · 𝑁) ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ) → ((2 · 𝑁) − (2 − 1)) = (((2 · 𝑁) − 2) + 1))
1916, 17, 18mp3an23 1449 . . . . . . . . . . . 12 ((2 · 𝑁) ∈ ℂ → ((2 · 𝑁) − (2 − 1)) = (((2 · 𝑁) − 2) + 1))
2015, 19syl 17 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((2 · 𝑁) − (2 − 1)) = (((2 · 𝑁) − 2) + 1))
21 nncn 12217 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
22 subdi 11644 . . . . . . . . . . . . . . 15 ((2 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → (2 · (𝑁 − 1)) = ((2 · 𝑁) − (2 · 1)))
2316, 17, 22mp3an13 1448 . . . . . . . . . . . . . 14 (𝑁 ∈ ℂ → (2 · (𝑁 − 1)) = ((2 · 𝑁) − (2 · 1)))
2421, 23syl 17 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (2 · (𝑁 − 1)) = ((2 · 𝑁) − (2 · 1)))
25 2t1e2 12372 . . . . . . . . . . . . . 14 (2 · 1) = 2
2625oveq2i 7412 . . . . . . . . . . . . 13 ((2 · 𝑁) − (2 · 1)) = ((2 · 𝑁) − 2)
2724, 26eqtrdi 2780 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (2 · (𝑁 − 1)) = ((2 · 𝑁) − 2))
2827oveq1d 7416 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((2 · (𝑁 − 1)) + 1) = (((2 · 𝑁) − 2) + 1))
2920, 28eqtr4d 2767 . . . . . . . . . 10 (𝑁 ∈ ℕ → ((2 · 𝑁) − (2 − 1)) = ((2 · (𝑁 − 1)) + 1))
3014, 29eqtr3id 2778 . . . . . . . . 9 (𝑁 ∈ ℕ → ((2 · 𝑁) − 1) = ((2 · (𝑁 − 1)) + 1))
31 2nn0 12486 . . . . . . . . . . 11 2 ∈ ℕ0
32 nnm1nn0 12510 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
33 nn0mulcl 12505 . . . . . . . . . . 11 ((2 ∈ ℕ0 ∧ (𝑁 − 1) ∈ ℕ0) → (2 · (𝑁 − 1)) ∈ ℕ0)
3431, 32, 33sylancr 586 . . . . . . . . . 10 (𝑁 ∈ ℕ → (2 · (𝑁 − 1)) ∈ ℕ0)
35 nn0p1nn 12508 . . . . . . . . . 10 ((2 · (𝑁 − 1)) ∈ ℕ0 → ((2 · (𝑁 − 1)) + 1) ∈ ℕ)
3634, 35syl 17 . . . . . . . . 9 (𝑁 ∈ ℕ → ((2 · (𝑁 − 1)) + 1) ∈ ℕ)
3730, 36eqeltrd 2825 . . . . . . . 8 (𝑁 ∈ ℕ → ((2 · 𝑁) − 1) ∈ ℕ)
38 nnnn0 12476 . . . . . . . 8 (((2 · 𝑁) − 1) ∈ ℕ → ((2 · 𝑁) − 1) ∈ ℕ0)
3937, 38syl 17 . . . . . . 7 (𝑁 ∈ ℕ → ((2 · 𝑁) − 1) ∈ ℕ0)
40 1re 11211 . . . . . . . . . . 11 1 ∈ ℝ
4140a1i 11 . . . . . . . . . 10 (𝑁 ∈ ℕ → 1 ∈ ℝ)
42 nnge1 12237 . . . . . . . . . 10 (𝑁 ∈ ℕ → 1 ≤ 𝑁)
4341, 9, 9, 42leadd2dd 11826 . . . . . . . . 9 (𝑁 ∈ ℕ → (𝑁 + 1) ≤ (𝑁 + 𝑁))
44212timesd 12452 . . . . . . . . 9 (𝑁 ∈ ℕ → (2 · 𝑁) = (𝑁 + 𝑁))
4543, 44breqtrrd 5166 . . . . . . . 8 (𝑁 ∈ ℕ → (𝑁 + 1) ≤ (2 · 𝑁))
46 leaddsub 11687 . . . . . . . . 9 ((𝑁 ∈ ℝ ∧ 1 ∈ ℝ ∧ (2 · 𝑁) ∈ ℝ) → ((𝑁 + 1) ≤ (2 · 𝑁) ↔ 𝑁 ≤ ((2 · 𝑁) − 1)))
479, 41, 4, 46syl3anc 1368 . . . . . . . 8 (𝑁 ∈ ℕ → ((𝑁 + 1) ≤ (2 · 𝑁) ↔ 𝑁 ≤ ((2 · 𝑁) − 1)))
4845, 47mpbid 231 . . . . . . 7 (𝑁 ∈ ℕ → 𝑁 ≤ ((2 · 𝑁) − 1))
49 elfz2nn0 13589 . . . . . . 7 (𝑁 ∈ (0...((2 · 𝑁) − 1)) ↔ (𝑁 ∈ ℕ0 ∧ ((2 · 𝑁) − 1) ∈ ℕ0𝑁 ≤ ((2 · 𝑁) − 1)))
5012, 39, 48, 49syl3anbrc 1340 . . . . . 6 (𝑁 ∈ ℕ → 𝑁 ∈ (0...((2 · 𝑁) − 1)))
51 bccl2 14280 . . . . . 6 (𝑁 ∈ (0...((2 · 𝑁) − 1)) → (((2 · 𝑁) − 1)C𝑁) ∈ ℕ)
5250, 51syl 17 . . . . 5 (𝑁 ∈ ℕ → (((2 · 𝑁) − 1)C𝑁) ∈ ℕ)
5352nnrpd 13011 . . . 4 (𝑁 ∈ ℕ → (((2 · 𝑁) − 1)C𝑁) ∈ ℝ+)
5453relogcld 26473 . . 3 (𝑁 ∈ ℕ → (log‘(((2 · 𝑁) − 1)C𝑁)) ∈ ℝ)
5511, 54readdcld 11240 . 2 (𝑁 ∈ ℕ → ((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁))) ∈ ℝ)
56 4re 12293 . . . . . 6 4 ∈ ℝ
57 4pos 12316 . . . . . 6 0 < 4
5856, 57elrpii 12974 . . . . 5 4 ∈ ℝ+
59 relogcl 26426 . . . . 5 (4 ∈ ℝ+ → (log‘4) ∈ ℝ)
6058, 59ax-mp 5 . . . 4 (log‘4) ∈ ℝ
6132nn0red 12530 . . . 4 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℝ)
62 remulcl 11191 . . . 4 (((log‘4) ∈ ℝ ∧ (𝑁 − 1) ∈ ℝ) → ((log‘4) · (𝑁 − 1)) ∈ ℝ)
6360, 61, 62sylancr 586 . . 3 (𝑁 ∈ ℕ → ((log‘4) · (𝑁 − 1)) ∈ ℝ)
6411, 63readdcld 11240 . 2 (𝑁 ∈ ℕ → ((θ‘𝑁) + ((log‘4) · (𝑁 − 1))) ∈ ℝ)
65 iftrue 4526 . . . . . . . . . . . 12 (𝑝 ≤ ((2 · 𝑁) − 1) → if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) = 1)
6665adantl 481 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ ((2 · 𝑁) − 1)) → if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) = 1)
67 simpr 484 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℙ)
6852adantr 480 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (((2 · 𝑁) − 1)C𝑁) ∈ ℕ)
6967, 68pccld 16782 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)) ∈ ℕ0)
70 nn0addge1 12515 . . . . . . . . . . . . . . 15 ((1 ∈ ℝ ∧ (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)) ∈ ℕ0) → 1 ≤ (1 + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))
7140, 69, 70sylancr 586 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 1 ≤ (1 + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))
72 iftrue 4526 . . . . . . . . . . . . . . . 16 (𝑝𝑁 → if(𝑝𝑁, 1, 0) = 1)
7372oveq1d 7416 . . . . . . . . . . . . . . 15 (𝑝𝑁 → (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) = (1 + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))
7473breq2d 5150 . . . . . . . . . . . . . 14 (𝑝𝑁 → (1 ≤ (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) ↔ 1 ≤ (1 + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))))
7571, 74syl5ibrcom 246 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝𝑁 → 1 ≤ (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))))
7675adantr 480 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ ((2 · 𝑁) − 1)) → (𝑝𝑁 → 1 ≤ (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))))
77 prmnn 16608 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
7877ad2antlr 724 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → 𝑝 ∈ ℕ)
79 simprl 768 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → 𝑝 ≤ ((2 · 𝑁) − 1))
80 prmz 16609 . . . . . . . . . . . . . . . . . . . 20 (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
8137nnzd 12582 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ → ((2 · 𝑁) − 1) ∈ ℤ)
82 eluz 12833 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 ∈ ℤ ∧ ((2 · 𝑁) − 1) ∈ ℤ) → (((2 · 𝑁) − 1) ∈ (ℤ𝑝) ↔ 𝑝 ≤ ((2 · 𝑁) − 1)))
8380, 81, 82syl2anr 596 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (((2 · 𝑁) − 1) ∈ (ℤ𝑝) ↔ 𝑝 ≤ ((2 · 𝑁) − 1)))
8483adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → (((2 · 𝑁) − 1) ∈ (ℤ𝑝) ↔ 𝑝 ≤ ((2 · 𝑁) − 1)))
8579, 84mpbird 257 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → ((2 · 𝑁) − 1) ∈ (ℤ𝑝))
86 dvdsfac 16266 . . . . . . . . . . . . . . . . 17 ((𝑝 ∈ ℕ ∧ ((2 · 𝑁) − 1) ∈ (ℤ𝑝)) → 𝑝 ∥ (!‘((2 · 𝑁) − 1)))
8778, 85, 86syl2anc 583 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → 𝑝 ∥ (!‘((2 · 𝑁) − 1)))
88 id 22 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ ℙ → 𝑝 ∈ ℙ)
8939faccld 14241 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → (!‘((2 · 𝑁) − 1)) ∈ ℕ)
90 pcelnn 16802 . . . . . . . . . . . . . . . . . 18 ((𝑝 ∈ ℙ ∧ (!‘((2 · 𝑁) − 1)) ∈ ℕ) → ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) ∈ ℕ ↔ 𝑝 ∥ (!‘((2 · 𝑁) − 1))))
9188, 89, 90syl2anr 596 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) ∈ ℕ ↔ 𝑝 ∥ (!‘((2 · 𝑁) − 1))))
9291adantr 480 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) ∈ ℕ ↔ 𝑝 ∥ (!‘((2 · 𝑁) − 1))))
9387, 92mpbird 257 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → (𝑝 pCnt (!‘((2 · 𝑁) − 1))) ∈ ℕ)
9493nnge1d 12257 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → 1 ≤ (𝑝 pCnt (!‘((2 · 𝑁) − 1))))
95 iffalse 4529 . . . . . . . . . . . . . . . . 17 𝑝𝑁 → if(𝑝𝑁, 1, 0) = 0)
9695oveq1d 7416 . . . . . . . . . . . . . . . 16 𝑝𝑁 → (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) = (0 + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))
9796ad2antll 726 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) = (0 + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))
9869nn0cnd 12531 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)) ∈ ℂ)
9998addlidd 11412 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (0 + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) = (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))
10099adantr 480 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → (0 + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) = (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))
101 bcval2 14262 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ (0...((2 · 𝑁) − 1)) → (((2 · 𝑁) − 1)C𝑁) = ((!‘((2 · 𝑁) − 1)) / ((!‘(((2 · 𝑁) − 1) − 𝑁)) · (!‘𝑁))))
10250, 101syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ → (((2 · 𝑁) − 1)C𝑁) = ((!‘((2 · 𝑁) − 1)) / ((!‘(((2 · 𝑁) − 1) − 𝑁)) · (!‘𝑁))))
10332nn0cnd 12531 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℂ)
10417a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℕ → 1 ∈ ℂ)
10544oveq1d 7416 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℕ → ((2 · 𝑁) − 1) = ((𝑁 + 𝑁) − 1))
10621, 21, 104, 105assraddsubd 11625 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ → ((2 · 𝑁) − 1) = (𝑁 + (𝑁 − 1)))
10721, 103, 106mvrladdd 11624 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ → (((2 · 𝑁) − 1) − 𝑁) = (𝑁 − 1))
108107fveq2d 6885 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ ℕ → (!‘(((2 · 𝑁) − 1) − 𝑁)) = (!‘(𝑁 − 1)))
109108oveq1d 7416 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ ℕ → ((!‘(((2 · 𝑁) − 1) − 𝑁)) · (!‘𝑁)) = ((!‘(𝑁 − 1)) · (!‘𝑁)))
110109oveq2d 7417 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ → ((!‘((2 · 𝑁) − 1)) / ((!‘(((2 · 𝑁) − 1) − 𝑁)) · (!‘𝑁))) = ((!‘((2 · 𝑁) − 1)) / ((!‘(𝑁 − 1)) · (!‘𝑁))))
111102, 110eqtrd 2764 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ → (((2 · 𝑁) − 1)C𝑁) = ((!‘((2 · 𝑁) − 1)) / ((!‘(𝑁 − 1)) · (!‘𝑁))))
112111adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (((2 · 𝑁) − 1)C𝑁) = ((!‘((2 · 𝑁) − 1)) / ((!‘(𝑁 − 1)) · (!‘𝑁))))
113112oveq2d 7417 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)) = (𝑝 pCnt ((!‘((2 · 𝑁) − 1)) / ((!‘(𝑁 − 1)) · (!‘𝑁)))))
114 nnz 12576 . . . . . . . . . . . . . . . . . . . . . 22 ((!‘((2 · 𝑁) − 1)) ∈ ℕ → (!‘((2 · 𝑁) − 1)) ∈ ℤ)
115 nnne0 12243 . . . . . . . . . . . . . . . . . . . . . 22 ((!‘((2 · 𝑁) − 1)) ∈ ℕ → (!‘((2 · 𝑁) − 1)) ≠ 0)
116114, 115jca 511 . . . . . . . . . . . . . . . . . . . . 21 ((!‘((2 · 𝑁) − 1)) ∈ ℕ → ((!‘((2 · 𝑁) − 1)) ∈ ℤ ∧ (!‘((2 · 𝑁) − 1)) ≠ 0))
11789, 116syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ → ((!‘((2 · 𝑁) − 1)) ∈ ℤ ∧ (!‘((2 · 𝑁) − 1)) ≠ 0))
118117adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((!‘((2 · 𝑁) − 1)) ∈ ℤ ∧ (!‘((2 · 𝑁) − 1)) ≠ 0))
11932faccld 14241 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ → (!‘(𝑁 − 1)) ∈ ℕ)
12012faccld 14241 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ → (!‘𝑁) ∈ ℕ)
121119, 120nnmulcld 12262 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ → ((!‘(𝑁 − 1)) · (!‘𝑁)) ∈ ℕ)
122121adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((!‘(𝑁 − 1)) · (!‘𝑁)) ∈ ℕ)
123 pcdiv 16784 . . . . . . . . . . . . . . . . . . 19 ((𝑝 ∈ ℙ ∧ ((!‘((2 · 𝑁) − 1)) ∈ ℤ ∧ (!‘((2 · 𝑁) − 1)) ≠ 0) ∧ ((!‘(𝑁 − 1)) · (!‘𝑁)) ∈ ℕ) → (𝑝 pCnt ((!‘((2 · 𝑁) − 1)) / ((!‘(𝑁 − 1)) · (!‘𝑁)))) = ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − (𝑝 pCnt ((!‘(𝑁 − 1)) · (!‘𝑁)))))
12467, 118, 122, 123syl3anc 1368 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((!‘((2 · 𝑁) − 1)) / ((!‘(𝑁 − 1)) · (!‘𝑁)))) = ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − (𝑝 pCnt ((!‘(𝑁 − 1)) · (!‘𝑁)))))
125 nnz 12576 . . . . . . . . . . . . . . . . . . . . . . 23 ((!‘(𝑁 − 1)) ∈ ℕ → (!‘(𝑁 − 1)) ∈ ℤ)
126 nnne0 12243 . . . . . . . . . . . . . . . . . . . . . . 23 ((!‘(𝑁 − 1)) ∈ ℕ → (!‘(𝑁 − 1)) ≠ 0)
127125, 126jca 511 . . . . . . . . . . . . . . . . . . . . . 22 ((!‘(𝑁 − 1)) ∈ ℕ → ((!‘(𝑁 − 1)) ∈ ℤ ∧ (!‘(𝑁 − 1)) ≠ 0))
128119, 127syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ → ((!‘(𝑁 − 1)) ∈ ℤ ∧ (!‘(𝑁 − 1)) ≠ 0))
129128adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((!‘(𝑁 − 1)) ∈ ℤ ∧ (!‘(𝑁 − 1)) ≠ 0))
130 nnz 12576 . . . . . . . . . . . . . . . . . . . . . . 23 ((!‘𝑁) ∈ ℕ → (!‘𝑁) ∈ ℤ)
131 nnne0 12243 . . . . . . . . . . . . . . . . . . . . . . 23 ((!‘𝑁) ∈ ℕ → (!‘𝑁) ≠ 0)
132130, 131jca 511 . . . . . . . . . . . . . . . . . . . . . 22 ((!‘𝑁) ∈ ℕ → ((!‘𝑁) ∈ ℤ ∧ (!‘𝑁) ≠ 0))
133120, 132syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ → ((!‘𝑁) ∈ ℤ ∧ (!‘𝑁) ≠ 0))
134133adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((!‘𝑁) ∈ ℤ ∧ (!‘𝑁) ≠ 0))
135 pcmul 16783 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 ∈ ℙ ∧ ((!‘(𝑁 − 1)) ∈ ℤ ∧ (!‘(𝑁 − 1)) ≠ 0) ∧ ((!‘𝑁) ∈ ℤ ∧ (!‘𝑁) ≠ 0)) → (𝑝 pCnt ((!‘(𝑁 − 1)) · (!‘𝑁))) = ((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁))))
13667, 129, 134, 135syl3anc 1368 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((!‘(𝑁 − 1)) · (!‘𝑁))) = ((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁))))
137136oveq2d 7417 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − (𝑝 pCnt ((!‘(𝑁 − 1)) · (!‘𝑁)))) = ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − ((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁)))))
138113, 124, 1373eqtrd 2768 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)) = ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − ((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁)))))
139138adantr 480 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)) = ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − ((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁)))))
140 simprr 770 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → ¬ 𝑝𝑁)
141 prmfac1 16655 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑁 ∈ ℕ0𝑝 ∈ ℙ ∧ 𝑝 ∥ (!‘𝑁)) → 𝑝𝑁)
1421413expia 1118 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑁 ∈ ℕ0𝑝 ∈ ℙ) → (𝑝 ∥ (!‘𝑁) → 𝑝𝑁))
14312, 142sylan 579 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (!‘𝑁) → 𝑝𝑁))
144143adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → (𝑝 ∥ (!‘𝑁) → 𝑝𝑁))
145140, 144mtod 197 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → ¬ 𝑝 ∥ (!‘𝑁))
14680adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℤ)
147129simpld 494 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (!‘(𝑁 − 1)) ∈ ℤ)
148 nnz 12576 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
149148adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑁 ∈ ℤ)
150 dvdsmultr1 16236 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑝 ∈ ℤ ∧ (!‘(𝑁 − 1)) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑝 ∥ (!‘(𝑁 − 1)) → 𝑝 ∥ ((!‘(𝑁 − 1)) · 𝑁)))
151146, 147, 149, 150syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (!‘(𝑁 − 1)) → 𝑝 ∥ ((!‘(𝑁 − 1)) · 𝑁)))
152 facnn2 14239 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ → (!‘𝑁) = ((!‘(𝑁 − 1)) · 𝑁))
153152adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (!‘𝑁) = ((!‘(𝑁 − 1)) · 𝑁))
154153breq2d 5150 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (!‘𝑁) ↔ 𝑝 ∥ ((!‘(𝑁 − 1)) · 𝑁)))
155151, 154sylibrd 259 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (!‘(𝑁 − 1)) → 𝑝 ∥ (!‘𝑁)))
156155adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → (𝑝 ∥ (!‘(𝑁 − 1)) → 𝑝 ∥ (!‘𝑁)))
157145, 156mtod 197 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → ¬ 𝑝 ∥ (!‘(𝑁 − 1)))
158 pceq0 16803 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑝 ∈ ℙ ∧ (!‘(𝑁 − 1)) ∈ ℕ) → ((𝑝 pCnt (!‘(𝑁 − 1))) = 0 ↔ ¬ 𝑝 ∥ (!‘(𝑁 − 1))))
15988, 119, 158syl2anr 596 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt (!‘(𝑁 − 1))) = 0 ↔ ¬ 𝑝 ∥ (!‘(𝑁 − 1))))
160159adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → ((𝑝 pCnt (!‘(𝑁 − 1))) = 0 ↔ ¬ 𝑝 ∥ (!‘(𝑁 − 1))))
161157, 160mpbird 257 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → (𝑝 pCnt (!‘(𝑁 − 1))) = 0)
162 pceq0 16803 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑝 ∈ ℙ ∧ (!‘𝑁) ∈ ℕ) → ((𝑝 pCnt (!‘𝑁)) = 0 ↔ ¬ 𝑝 ∥ (!‘𝑁)))
16388, 120, 162syl2anr 596 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt (!‘𝑁)) = 0 ↔ ¬ 𝑝 ∥ (!‘𝑁)))
164163adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → ((𝑝 pCnt (!‘𝑁)) = 0 ↔ ¬ 𝑝 ∥ (!‘𝑁)))
165145, 164mpbird 257 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → (𝑝 pCnt (!‘𝑁)) = 0)
166161, 165oveq12d 7419 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → ((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁))) = (0 + 0))
167 00id 11386 . . . . . . . . . . . . . . . . . 18 (0 + 0) = 0
168166, 167eqtrdi 2780 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → ((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁))) = 0)
169168oveq2d 7417 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − ((𝑝 pCnt (!‘(𝑁 − 1))) + (𝑝 pCnt (!‘𝑁)))) = ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − 0))
170 pccl 16781 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 ∈ ℙ ∧ (!‘((2 · 𝑁) − 1)) ∈ ℕ) → (𝑝 pCnt (!‘((2 · 𝑁) − 1))) ∈ ℕ0)
17188, 89, 170syl2anr 596 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (!‘((2 · 𝑁) − 1))) ∈ ℕ0)
172171nn0cnd 12531 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (!‘((2 · 𝑁) − 1))) ∈ ℂ)
173172subid1d 11557 . . . . . . . . . . . . . . . . 17 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − 0) = (𝑝 pCnt (!‘((2 · 𝑁) − 1))))
174173adantr 480 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → ((𝑝 pCnt (!‘((2 · 𝑁) − 1))) − 0) = (𝑝 pCnt (!‘((2 · 𝑁) − 1))))
175139, 169, 1743eqtrd 2768 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)) = (𝑝 pCnt (!‘((2 · 𝑁) − 1))))
17697, 100, 1753eqtrd 2768 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) = (𝑝 pCnt (!‘((2 · 𝑁) − 1))))
17794, 176breqtrrd 5166 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ ((2 · 𝑁) − 1) ∧ ¬ 𝑝𝑁)) → 1 ≤ (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))
178177expr 456 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ ((2 · 𝑁) − 1)) → (¬ 𝑝𝑁 → 1 ≤ (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))))
17976, 178pm2.61d 179 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ ((2 · 𝑁) − 1)) → 1 ≤ (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))
18066, 179eqbrtrd 5160 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ ((2 · 𝑁) − 1)) → if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) ≤ (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))
181180ex 412 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 ≤ ((2 · 𝑁) − 1) → if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) ≤ (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))))
182 1nn0 12485 . . . . . . . . . . . . 13 1 ∈ ℕ0
183 0nn0 12484 . . . . . . . . . . . . 13 0 ∈ ℕ0
184182, 183ifcli 4567 . . . . . . . . . . . 12 if(𝑝𝑁, 1, 0) ∈ ℕ0
185 nn0addcl 12504 . . . . . . . . . . . 12 ((if(𝑝𝑁, 1, 0) ∈ ℕ0 ∧ (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)) ∈ ℕ0) → (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) ∈ ℕ0)
186184, 69, 185sylancr 586 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) ∈ ℕ0)
187186nn0ge0d 12532 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 0 ≤ (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))
188 iffalse 4529 . . . . . . . . . . 11 𝑝 ≤ ((2 · 𝑁) − 1) → if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) = 0)
189188breq1d 5148 . . . . . . . . . 10 𝑝 ≤ ((2 · 𝑁) − 1) → (if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) ≤ (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) ↔ 0 ≤ (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))))
190187, 189syl5ibrcom 246 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (¬ 𝑝 ≤ ((2 · 𝑁) − 1) → if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) ≤ (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁)))))
191181, 190pm2.61d 179 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0) ≤ (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))
192 eqid 2724 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1))
193192prmorcht 27026 . . . . . . . . . . . 12 (((2 · 𝑁) − 1) ∈ ℕ → (exp‘(θ‘((2 · 𝑁) − 1))) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘((2 · 𝑁) − 1)))
19437, 193syl 17 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (exp‘(θ‘((2 · 𝑁) − 1))) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘((2 · 𝑁) − 1)))
195194oveq2d 7417 . . . . . . . . . 10 (𝑁 ∈ ℕ → (𝑝 pCnt (exp‘(θ‘((2 · 𝑁) − 1)))) = (𝑝 pCnt (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘((2 · 𝑁) − 1))))
196195adantr 480 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (exp‘(θ‘((2 · 𝑁) − 1)))) = (𝑝 pCnt (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘((2 · 𝑁) − 1))))
197 nncn 12217 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
198197exp1d 14103 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (𝑛↑1) = 𝑛)
199198ifeq1d 4539 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → if(𝑛 ∈ ℙ, (𝑛↑1), 1) = if(𝑛 ∈ ℙ, 𝑛, 1))
200199mpteq2ia 5241 . . . . . . . . . . 11 (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑1), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1))
201200eqcomi 2733 . . . . . . . . . 10 (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑1), 1))
202182a1i 11 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑛 ∈ ℙ) → 1 ∈ ℕ0)
203202ralrimiva 3138 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ∀𝑛 ∈ ℙ 1 ∈ ℕ0)
20437adantr 480 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((2 · 𝑁) − 1) ∈ ℕ)
205 eqidd 2725 . . . . . . . . . 10 (𝑛 = 𝑝 → 1 = 1)
206201, 203, 204, 67, 205pcmpt 16824 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘((2 · 𝑁) − 1))) = if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0))
207196, 206eqtrd 2764 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (exp‘(θ‘((2 · 𝑁) − 1)))) = if(𝑝 ≤ ((2 · 𝑁) − 1), 1, 0))
208 efchtcl 26959 . . . . . . . . . . . . 13 (𝑁 ∈ ℝ → (exp‘(θ‘𝑁)) ∈ ℕ)
2099, 208syl 17 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (exp‘(θ‘𝑁)) ∈ ℕ)
210209adantr 480 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (exp‘(θ‘𝑁)) ∈ ℕ)
211 nnz 12576 . . . . . . . . . . . 12 ((exp‘(θ‘𝑁)) ∈ ℕ → (exp‘(θ‘𝑁)) ∈ ℤ)
212 nnne0 12243 . . . . . . . . . . . 12 ((exp‘(θ‘𝑁)) ∈ ℕ → (exp‘(θ‘𝑁)) ≠ 0)
213211, 212jca 511 . . . . . . . . . . 11 ((exp‘(θ‘𝑁)) ∈ ℕ → ((exp‘(θ‘𝑁)) ∈ ℤ ∧ (exp‘(θ‘𝑁)) ≠ 0))
214210, 213syl 17 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((exp‘(θ‘𝑁)) ∈ ℤ ∧ (exp‘(θ‘𝑁)) ≠ 0))
215 nnz 12576 . . . . . . . . . . . 12 ((((2 · 𝑁) − 1)C𝑁) ∈ ℕ → (((2 · 𝑁) − 1)C𝑁) ∈ ℤ)
216 nnne0 12243 . . . . . . . . . . . 12 ((((2 · 𝑁) − 1)C𝑁) ∈ ℕ → (((2 · 𝑁) − 1)C𝑁) ≠ 0)
217215, 216jca 511 . . . . . . . . . . 11 ((((2 · 𝑁) − 1)C𝑁) ∈ ℕ → ((((2 · 𝑁) − 1)C𝑁) ∈ ℤ ∧ (((2 · 𝑁) − 1)C𝑁) ≠ 0))
21868, 217syl 17 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((((2 · 𝑁) − 1)C𝑁) ∈ ℤ ∧ (((2 · 𝑁) − 1)C𝑁) ≠ 0))
219 pcmul 16783 . . . . . . . . . 10 ((𝑝 ∈ ℙ ∧ ((exp‘(θ‘𝑁)) ∈ ℤ ∧ (exp‘(θ‘𝑁)) ≠ 0) ∧ ((((2 · 𝑁) − 1)C𝑁) ∈ ℤ ∧ (((2 · 𝑁) − 1)C𝑁) ≠ 0)) → (𝑝 pCnt ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))) = ((𝑝 pCnt (exp‘(θ‘𝑁))) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))
22067, 214, 218, 219syl3anc 1368 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))) = ((𝑝 pCnt (exp‘(θ‘𝑁))) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))
221192prmorcht 27026 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (exp‘(θ‘𝑁)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑁))
222221oveq2d 7417 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (𝑝 pCnt (exp‘(θ‘𝑁))) = (𝑝 pCnt (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑁)))
223222adantr 480 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (exp‘(θ‘𝑁))) = (𝑝 pCnt (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑁)))
224 simpl 482 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑁 ∈ ℕ)
225201, 203, 224, 67, 205pcmpt 16824 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑁)) = if(𝑝𝑁, 1, 0))
226223, 225eqtrd 2764 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (exp‘(θ‘𝑁))) = if(𝑝𝑁, 1, 0))
227226oveq1d 7416 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt (exp‘(θ‘𝑁))) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))) = (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))
228220, 227eqtrd 2764 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))) = (if(𝑝𝑁, 1, 0) + (𝑝 pCnt (((2 · 𝑁) − 1)C𝑁))))
229191, 207, 2283brtr4d 5170 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (exp‘(θ‘((2 · 𝑁) − 1)))) ≤ (𝑝 pCnt ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))))
230229ralrimiva 3138 . . . . . 6 (𝑁 ∈ ℕ → ∀𝑝 ∈ ℙ (𝑝 pCnt (exp‘(θ‘((2 · 𝑁) − 1)))) ≤ (𝑝 pCnt ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))))
231 efchtcl 26959 . . . . . . . . 9 (((2 · 𝑁) − 1) ∈ ℝ → (exp‘(θ‘((2 · 𝑁) − 1))) ∈ ℕ)
2326, 231syl 17 . . . . . . . 8 (𝑁 ∈ ℕ → (exp‘(θ‘((2 · 𝑁) − 1))) ∈ ℕ)
233232nnzd 12582 . . . . . . 7 (𝑁 ∈ ℕ → (exp‘(θ‘((2 · 𝑁) − 1))) ∈ ℤ)
234209, 52nnmulcld 12262 . . . . . . . 8 (𝑁 ∈ ℕ → ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) ∈ ℕ)
235234nnzd 12582 . . . . . . 7 (𝑁 ∈ ℕ → ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) ∈ ℤ)
236 pc2dvds 16811 . . . . . . 7 (((exp‘(θ‘((2 · 𝑁) − 1))) ∈ ℤ ∧ ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) ∈ ℤ) → ((exp‘(θ‘((2 · 𝑁) − 1))) ∥ ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt (exp‘(θ‘((2 · 𝑁) − 1)))) ≤ (𝑝 pCnt ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)))))
237233, 235, 236syl2anc 583 . . . . . 6 (𝑁 ∈ ℕ → ((exp‘(θ‘((2 · 𝑁) − 1))) ∥ ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt (exp‘(θ‘((2 · 𝑁) − 1)))) ≤ (𝑝 pCnt ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)))))
238230, 237mpbird 257 . . . . 5 (𝑁 ∈ ℕ → (exp‘(θ‘((2 · 𝑁) − 1))) ∥ ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)))
239 dvdsle 16250 . . . . . 6 (((exp‘(θ‘((2 · 𝑁) − 1))) ∈ ℤ ∧ ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) ∈ ℕ) → ((exp‘(θ‘((2 · 𝑁) − 1))) ∥ ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) → (exp‘(θ‘((2 · 𝑁) − 1))) ≤ ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))))
240233, 234, 239syl2anc 583 . . . . 5 (𝑁 ∈ ℕ → ((exp‘(θ‘((2 · 𝑁) − 1))) ∥ ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)) → (exp‘(θ‘((2 · 𝑁) − 1))) ≤ ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁))))
241238, 240mpd 15 . . . 4 (𝑁 ∈ ℕ → (exp‘(θ‘((2 · 𝑁) − 1))) ≤ ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)))
24211recnd 11239 . . . . . 6 (𝑁 ∈ ℕ → (θ‘𝑁) ∈ ℂ)
24354recnd 11239 . . . . . 6 (𝑁 ∈ ℕ → (log‘(((2 · 𝑁) − 1)C𝑁)) ∈ ℂ)
244 efadd 16034 . . . . . 6 (((θ‘𝑁) ∈ ℂ ∧ (log‘(((2 · 𝑁) − 1)C𝑁)) ∈ ℂ) → (exp‘((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁)))) = ((exp‘(θ‘𝑁)) · (exp‘(log‘(((2 · 𝑁) − 1)C𝑁)))))
245242, 243, 244syl2anc 583 . . . . 5 (𝑁 ∈ ℕ → (exp‘((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁)))) = ((exp‘(θ‘𝑁)) · (exp‘(log‘(((2 · 𝑁) − 1)C𝑁)))))
24653reeflogd 26474 . . . . . 6 (𝑁 ∈ ℕ → (exp‘(log‘(((2 · 𝑁) − 1)C𝑁))) = (((2 · 𝑁) − 1)C𝑁))
247246oveq2d 7417 . . . . 5 (𝑁 ∈ ℕ → ((exp‘(θ‘𝑁)) · (exp‘(log‘(((2 · 𝑁) − 1)C𝑁)))) = ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)))
248245, 247eqtrd 2764 . . . 4 (𝑁 ∈ ℕ → (exp‘((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁)))) = ((exp‘(θ‘𝑁)) · (((2 · 𝑁) − 1)C𝑁)))
249241, 248breqtrrd 5166 . . 3 (𝑁 ∈ ℕ → (exp‘(θ‘((2 · 𝑁) − 1))) ≤ (exp‘((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁)))))
250 efle 16058 . . . 4 (((θ‘((2 · 𝑁) − 1)) ∈ ℝ ∧ ((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁))) ∈ ℝ) → ((θ‘((2 · 𝑁) − 1)) ≤ ((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁))) ↔ (exp‘(θ‘((2 · 𝑁) − 1))) ≤ (exp‘((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁))))))
2518, 55, 250syl2anc 583 . . 3 (𝑁 ∈ ℕ → ((θ‘((2 · 𝑁) − 1)) ≤ ((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁))) ↔ (exp‘(θ‘((2 · 𝑁) − 1))) ≤ (exp‘((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁))))))
252249, 251mpbird 257 . 2 (𝑁 ∈ ℕ → (θ‘((2 · 𝑁) − 1)) ≤ ((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁))))
253 fzfid 13935 . . . . . . . . 9 (𝑁 ∈ ℕ → (0...((2 · 𝑁) − 1)) ∈ Fin)
254 elfzelz 13498 . . . . . . . . . . 11 (𝑘 ∈ (0...((2 · 𝑁) − 1)) → 𝑘 ∈ ℤ)
255 bccl 14279 . . . . . . . . . . 11 ((((2 · 𝑁) − 1) ∈ ℕ0𝑘 ∈ ℤ) → (((2 · 𝑁) − 1)C𝑘) ∈ ℕ0)
25639, 254, 255syl2an 595 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...((2 · 𝑁) − 1))) → (((2 · 𝑁) − 1)C𝑘) ∈ ℕ0)
257256nn0red 12530 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...((2 · 𝑁) − 1))) → (((2 · 𝑁) − 1)C𝑘) ∈ ℝ)
258256nn0ge0d 12532 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...((2 · 𝑁) − 1))) → 0 ≤ (((2 · 𝑁) − 1)C𝑘))
259 nn0uz 12861 . . . . . . . . . . . 12 0 = (ℤ‘0)
26032, 259eleqtrdi 2835 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (ℤ‘0))
261 fzss1 13537 . . . . . . . . . . 11 ((𝑁 − 1) ∈ (ℤ‘0) → ((𝑁 − 1)...𝑁) ⊆ (0...𝑁))
262260, 261syl 17 . . . . . . . . . 10 (𝑁 ∈ ℕ → ((𝑁 − 1)...𝑁) ⊆ (0...𝑁))
263 eluz 12833 . . . . . . . . . . . . 13 ((𝑁 ∈ ℤ ∧ ((2 · 𝑁) − 1) ∈ ℤ) → (((2 · 𝑁) − 1) ∈ (ℤ𝑁) ↔ 𝑁 ≤ ((2 · 𝑁) − 1)))
264148, 81, 263syl2anc 583 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (((2 · 𝑁) − 1) ∈ (ℤ𝑁) ↔ 𝑁 ≤ ((2 · 𝑁) − 1)))
26548, 264mpbird 257 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((2 · 𝑁) − 1) ∈ (ℤ𝑁))
266 fzss2 13538 . . . . . . . . . . 11 (((2 · 𝑁) − 1) ∈ (ℤ𝑁) → (0...𝑁) ⊆ (0...((2 · 𝑁) − 1)))
267265, 266syl 17 . . . . . . . . . 10 (𝑁 ∈ ℕ → (0...𝑁) ⊆ (0...((2 · 𝑁) − 1)))
268262, 267sstrd 3984 . . . . . . . . 9 (𝑁 ∈ ℕ → ((𝑁 − 1)...𝑁) ⊆ (0...((2 · 𝑁) − 1)))
269253, 257, 258, 268fsumless 15739 . . . . . . . 8 (𝑁 ∈ ℕ → Σ𝑘 ∈ ((𝑁 − 1)...𝑁)(((2 · 𝑁) − 1)C𝑘) ≤ Σ𝑘 ∈ (0...((2 · 𝑁) − 1))(((2 · 𝑁) − 1)C𝑘))
27032nn0zd 12581 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℤ)
271 bccmpl 14266 . . . . . . . . . . . . . . 15 ((((2 · 𝑁) − 1) ∈ ℕ0𝑁 ∈ ℤ) → (((2 · 𝑁) − 1)C𝑁) = (((2 · 𝑁) − 1)C(((2 · 𝑁) − 1) − 𝑁)))
27239, 148, 271syl2anc 583 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → (((2 · 𝑁) − 1)C𝑁) = (((2 · 𝑁) − 1)C(((2 · 𝑁) − 1) − 𝑁)))
273107oveq2d 7417 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → (((2 · 𝑁) − 1)C(((2 · 𝑁) − 1) − 𝑁)) = (((2 · 𝑁) − 1)C(𝑁 − 1)))
274272, 273eqtrd 2764 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (((2 · 𝑁) − 1)C𝑁) = (((2 · 𝑁) − 1)C(𝑁 − 1)))
27552nncnd 12225 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (((2 · 𝑁) − 1)C𝑁) ∈ ℂ)
276274, 275eqeltrrd 2826 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (((2 · 𝑁) − 1)C(𝑁 − 1)) ∈ ℂ)
277 oveq2 7409 . . . . . . . . . . . . 13 (𝑘 = (𝑁 − 1) → (((2 · 𝑁) − 1)C𝑘) = (((2 · 𝑁) − 1)C(𝑁 − 1)))
278277fsum1 15690 . . . . . . . . . . . 12 (((𝑁 − 1) ∈ ℤ ∧ (((2 · 𝑁) − 1)C(𝑁 − 1)) ∈ ℂ) → Σ𝑘 ∈ ((𝑁 − 1)...(𝑁 − 1))(((2 · 𝑁) − 1)C𝑘) = (((2 · 𝑁) − 1)C(𝑁 − 1)))
279270, 276, 278syl2anc 583 . . . . . . . . . . 11 (𝑁 ∈ ℕ → Σ𝑘 ∈ ((𝑁 − 1)...(𝑁 − 1))(((2 · 𝑁) − 1)C𝑘) = (((2 · 𝑁) − 1)C(𝑁 − 1)))
280279, 274eqtr4d 2767 . . . . . . . . . 10 (𝑁 ∈ ℕ → Σ𝑘 ∈ ((𝑁 − 1)...(𝑁 − 1))(((2 · 𝑁) − 1)C𝑘) = (((2 · 𝑁) − 1)C𝑁))
281280oveq1d 7416 . . . . . . . . 9 (𝑁 ∈ ℕ → (Σ𝑘 ∈ ((𝑁 − 1)...(𝑁 − 1))(((2 · 𝑁) − 1)C𝑘) + (((2 · 𝑁) − 1)C𝑁)) = ((((2 · 𝑁) − 1)C𝑁) + (((2 · 𝑁) − 1)C𝑁)))
28221, 104npcand 11572 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((𝑁 − 1) + 1) = 𝑁)
283 uzid 12834 . . . . . . . . . . . . 13 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
284270, 283syl 17 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
285 peano2uz 12882 . . . . . . . . . . . 12 ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
286284, 285syl 17 . . . . . . . . . . 11 (𝑁 ∈ ℕ → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
287282, 286eqeltrrd 2826 . . . . . . . . . 10 (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ‘(𝑁 − 1)))
288268sselda 3974 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ((𝑁 − 1)...𝑁)) → 𝑘 ∈ (0...((2 · 𝑁) − 1)))
289256nn0cnd 12531 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...((2 · 𝑁) − 1))) → (((2 · 𝑁) − 1)C𝑘) ∈ ℂ)
290288, 289syldan 590 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ((𝑁 − 1)...𝑁)) → (((2 · 𝑁) − 1)C𝑘) ∈ ℂ)
291 oveq2 7409 . . . . . . . . . 10 (𝑘 = 𝑁 → (((2 · 𝑁) − 1)C𝑘) = (((2 · 𝑁) − 1)C𝑁))
292287, 290, 291fsumm1 15694 . . . . . . . . 9 (𝑁 ∈ ℕ → Σ𝑘 ∈ ((𝑁 − 1)...𝑁)(((2 · 𝑁) − 1)C𝑘) = (Σ𝑘 ∈ ((𝑁 − 1)...(𝑁 − 1))(((2 · 𝑁) − 1)C𝑘) + (((2 · 𝑁) − 1)C𝑁)))
2932752timesd 12452 . . . . . . . . 9 (𝑁 ∈ ℕ → (2 · (((2 · 𝑁) − 1)C𝑁)) = ((((2 · 𝑁) − 1)C𝑁) + (((2 · 𝑁) − 1)C𝑁)))
294281, 292, 2933eqtr4rd 2775 . . . . . . . 8 (𝑁 ∈ ℕ → (2 · (((2 · 𝑁) − 1)C𝑁)) = Σ𝑘 ∈ ((𝑁 − 1)...𝑁)(((2 · 𝑁) − 1)C𝑘))
295 binom11 15775 . . . . . . . . 9 (((2 · 𝑁) − 1) ∈ ℕ0 → (2↑((2 · 𝑁) − 1)) = Σ𝑘 ∈ (0...((2 · 𝑁) − 1))(((2 · 𝑁) − 1)C𝑘))
29639, 295syl 17 . . . . . . . 8 (𝑁 ∈ ℕ → (2↑((2 · 𝑁) − 1)) = Σ𝑘 ∈ (0...((2 · 𝑁) − 1))(((2 · 𝑁) − 1)C𝑘))
297269, 294, 2963brtr4d 5170 . . . . . . 7 (𝑁 ∈ ℕ → (2 · (((2 · 𝑁) − 1)C𝑁)) ≤ (2↑((2 · 𝑁) − 1)))
298 mulcom 11192 . . . . . . . 8 ((2 ∈ ℂ ∧ (((2 · 𝑁) − 1)C𝑁) ∈ ℂ) → (2 · (((2 · 𝑁) − 1)C𝑁)) = ((((2 · 𝑁) − 1)C𝑁) · 2))
29916, 275, 298sylancr 586 . . . . . . 7 (𝑁 ∈ ℕ → (2 · (((2 · 𝑁) − 1)C𝑁)) = ((((2 · 𝑁) − 1)C𝑁) · 2))
30030oveq2d 7417 . . . . . . . 8 (𝑁 ∈ ℕ → (2↑((2 · 𝑁) − 1)) = (2↑((2 · (𝑁 − 1)) + 1)))
301 expp1 14031 . . . . . . . . 9 ((2 ∈ ℂ ∧ (2 · (𝑁 − 1)) ∈ ℕ0) → (2↑((2 · (𝑁 − 1)) + 1)) = ((2↑(2 · (𝑁 − 1))) · 2))
30216, 34, 301sylancr 586 . . . . . . . 8 (𝑁 ∈ ℕ → (2↑((2 · (𝑁 − 1)) + 1)) = ((2↑(2 · (𝑁 − 1))) · 2))
30316a1i 11 . . . . . . . . . . 11 (𝑁 ∈ ℕ → 2 ∈ ℂ)
30431a1i 11 . . . . . . . . . . 11 (𝑁 ∈ ℕ → 2 ∈ ℕ0)
305303, 32, 304expmuld 14111 . . . . . . . . . 10 (𝑁 ∈ ℕ → (2↑(2 · (𝑁 − 1))) = ((2↑2)↑(𝑁 − 1)))
306 sq2 14158 . . . . . . . . . . 11 (2↑2) = 4
307306oveq1i 7411 . . . . . . . . . 10 ((2↑2)↑(𝑁 − 1)) = (4↑(𝑁 − 1))
308305, 307eqtrdi 2780 . . . . . . . . 9 (𝑁 ∈ ℕ → (2↑(2 · (𝑁 − 1))) = (4↑(𝑁 − 1)))
309308oveq1d 7416 . . . . . . . 8 (𝑁 ∈ ℕ → ((2↑(2 · (𝑁 − 1))) · 2) = ((4↑(𝑁 − 1)) · 2))
310300, 302, 3093eqtrd 2768 . . . . . . 7 (𝑁 ∈ ℕ → (2↑((2 · 𝑁) − 1)) = ((4↑(𝑁 − 1)) · 2))
311297, 299, 3103brtr3d 5169 . . . . . 6 (𝑁 ∈ ℕ → ((((2 · 𝑁) − 1)C𝑁) · 2) ≤ ((4↑(𝑁 − 1)) · 2))
31252nnred 12224 . . . . . . 7 (𝑁 ∈ ℕ → (((2 · 𝑁) − 1)C𝑁) ∈ ℝ)
313 reexpcl 14041 . . . . . . . 8 ((4 ∈ ℝ ∧ (𝑁 − 1) ∈ ℕ0) → (4↑(𝑁 − 1)) ∈ ℝ)
31456, 32, 313sylancr 586 . . . . . . 7 (𝑁 ∈ ℕ → (4↑(𝑁 − 1)) ∈ ℝ)
315 2re 12283 . . . . . . . . 9 2 ∈ ℝ
316 2pos 12312 . . . . . . . . 9 0 < 2
317315, 316pm3.2i 470 . . . . . . . 8 (2 ∈ ℝ ∧ 0 < 2)
318317a1i 11 . . . . . . 7 (𝑁 ∈ ℕ → (2 ∈ ℝ ∧ 0 < 2))
319 lemul1 12063 . . . . . . 7 (((((2 · 𝑁) − 1)C𝑁) ∈ ℝ ∧ (4↑(𝑁 − 1)) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((((2 · 𝑁) − 1)C𝑁) ≤ (4↑(𝑁 − 1)) ↔ ((((2 · 𝑁) − 1)C𝑁) · 2) ≤ ((4↑(𝑁 − 1)) · 2)))
320312, 314, 318, 319syl3anc 1368 . . . . . 6 (𝑁 ∈ ℕ → ((((2 · 𝑁) − 1)C𝑁) ≤ (4↑(𝑁 − 1)) ↔ ((((2 · 𝑁) − 1)C𝑁) · 2) ≤ ((4↑(𝑁 − 1)) · 2)))
321311, 320mpbird 257 . . . . 5 (𝑁 ∈ ℕ → (((2 · 𝑁) − 1)C𝑁) ≤ (4↑(𝑁 − 1)))
32260recni 11225 . . . . . . . 8 (log‘4) ∈ ℂ
323 mulcom 11192 . . . . . . . 8 (((log‘4) ∈ ℂ ∧ (𝑁 − 1) ∈ ℂ) → ((log‘4) · (𝑁 − 1)) = ((𝑁 − 1) · (log‘4)))
324322, 103, 323sylancr 586 . . . . . . 7 (𝑁 ∈ ℕ → ((log‘4) · (𝑁 − 1)) = ((𝑁 − 1) · (log‘4)))
325324fveq2d 6885 . . . . . 6 (𝑁 ∈ ℕ → (exp‘((log‘4) · (𝑁 − 1))) = (exp‘((𝑁 − 1) · (log‘4))))
326 reexplog 26445 . . . . . . 7 ((4 ∈ ℝ+ ∧ (𝑁 − 1) ∈ ℤ) → (4↑(𝑁 − 1)) = (exp‘((𝑁 − 1) · (log‘4))))
32758, 270, 326sylancr 586 . . . . . 6 (𝑁 ∈ ℕ → (4↑(𝑁 − 1)) = (exp‘((𝑁 − 1) · (log‘4))))
328325, 327eqtr4d 2767 . . . . 5 (𝑁 ∈ ℕ → (exp‘((log‘4) · (𝑁 − 1))) = (4↑(𝑁 − 1)))
329321, 246, 3283brtr4d 5170 . . . 4 (𝑁 ∈ ℕ → (exp‘(log‘(((2 · 𝑁) − 1)C𝑁))) ≤ (exp‘((log‘4) · (𝑁 − 1))))
330 efle 16058 . . . . 5 (((log‘(((2 · 𝑁) − 1)C𝑁)) ∈ ℝ ∧ ((log‘4) · (𝑁 − 1)) ∈ ℝ) → ((log‘(((2 · 𝑁) − 1)C𝑁)) ≤ ((log‘4) · (𝑁 − 1)) ↔ (exp‘(log‘(((2 · 𝑁) − 1)C𝑁))) ≤ (exp‘((log‘4) · (𝑁 − 1)))))
33154, 63, 330syl2anc 583 . . . 4 (𝑁 ∈ ℕ → ((log‘(((2 · 𝑁) − 1)C𝑁)) ≤ ((log‘4) · (𝑁 − 1)) ↔ (exp‘(log‘(((2 · 𝑁) − 1)C𝑁))) ≤ (exp‘((log‘4) · (𝑁 − 1)))))
332329, 331mpbird 257 . . 3 (𝑁 ∈ ℕ → (log‘(((2 · 𝑁) − 1)C𝑁)) ≤ ((log‘4) · (𝑁 − 1)))
33354, 63, 11, 332leadd2dd 11826 . 2 (𝑁 ∈ ℕ → ((θ‘𝑁) + (log‘(((2 · 𝑁) − 1)C𝑁))) ≤ ((θ‘𝑁) + ((log‘4) · (𝑁 − 1))))
3348, 55, 64, 252, 333letrd 11368 1 (𝑁 ∈ ℕ → (θ‘((2 · 𝑁) − 1)) ≤ ((θ‘𝑁) + ((log‘4) · (𝑁 − 1))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395   = wceq 1533  wcel 2098  wne 2932  wral 3053  wss 3940  ifcif 4520   class class class wbr 5138  cmpt 5221  cfv 6533  (class class class)co 7401  cc 11104  cr 11105  0cc0 11106  1c1 11107   + caddc 11109   · cmul 11111   < clt 11245  cle 11246  cmin 11441   / cdiv 11868  cn 12209  2c2 12264  4c4 12266  0cn0 12469  cz 12555  cuz 12819  +crp 12971  ...cfz 13481  seqcseq 13963  cexp 14024  !cfa 14230  Ccbc 14259  Σcsu 15629  expce 16002  cdvds 16194  cprime 16605   pCnt cpc 16768  logclog 26405  θccht 26939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-addf 11185
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-tp 4625  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-iin 4990  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-of 7663  df-om 7849  df-1st 7968  df-2nd 7969  df-supp 8141  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-er 8699  df-map 8818  df-pm 8819  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-fi 9402  df-sup 9433  df-inf 9434  df-oi 9501  df-card 9930  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-5 12275  df-6 12276  df-7 12277  df-8 12278  df-9 12279  df-n0 12470  df-z 12556  df-dec 12675  df-uz 12820  df-q 12930  df-rp 12972  df-xneg 13089  df-xadd 13090  df-xmul 13091  df-ioo 13325  df-ioc 13326  df-ico 13327  df-icc 13328  df-fz 13482  df-fzo 13625  df-fl 13754  df-mod 13832  df-seq 13964  df-exp 14025  df-fac 14231  df-bc 14260  df-hash 14288  df-shft 15011  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-limsup 15412  df-clim 15429  df-rlim 15430  df-sum 15630  df-ef 16008  df-sin 16010  df-cos 16011  df-pi 16013  df-dvds 16195  df-gcd 16433  df-prm 16606  df-pc 16769  df-struct 17079  df-sets 17096  df-slot 17114  df-ndx 17126  df-base 17144  df-ress 17173  df-plusg 17209  df-mulr 17210  df-starv 17211  df-sca 17212  df-vsca 17213  df-ip 17214  df-tset 17215  df-ple 17216  df-ds 17218  df-unif 17219  df-hom 17220  df-cco 17221  df-rest 17367  df-topn 17368  df-0g 17386  df-gsum 17387  df-topgen 17388  df-pt 17389  df-prds 17392  df-xrs 17447  df-qtop 17452  df-imas 17453  df-xps 17455  df-mre 17529  df-mrc 17530  df-acs 17532  df-mgm 18563  df-sgrp 18642  df-mnd 18658  df-submnd 18704  df-mulg 18986  df-cntz 19223  df-cmn 19692  df-psmet 21220  df-xmet 21221  df-met 21222  df-bl 21223  df-mopn 21224  df-fbas 21225  df-fg 21226  df-cnfld 21229  df-top 22718  df-topon 22735  df-topsp 22757  df-bases 22771  df-cld 22845  df-ntr 22846  df-cls 22847  df-nei 22924  df-lp 22962  df-perf 22963  df-cn 23053  df-cnp 23054  df-haus 23141  df-tx 23388  df-hmeo 23581  df-fil 23672  df-fm 23764  df-flim 23765  df-flf 23766  df-xms 24148  df-ms 24149  df-tms 24150  df-cncf 24720  df-limc 25717  df-dv 25718  df-log 26407  df-cht 26945
This theorem is referenced by:  chtub  27061
  Copyright terms: Public domain W3C validator