Metamath Proof Explorer

Theorem chtublem

Description: Lemma for chtub . (Contributed by Mario Carneiro, 13-Mar-2014)

Ref Expression
Assertion chtublem ( 𝑁 ∈ ℕ → ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ≤ ( ( θ ‘ 𝑁 ) + ( ( log ‘ 4 ) · ( 𝑁 − 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 2nn ⊢ 2 ∈ ℕ
2 nnmulcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 2 · 𝑁 ) ∈ ℕ )
3 1 2 mpan ⊢ ( 𝑁 ∈ ℕ → ( 2 · 𝑁 ) ∈ ℕ )
4 3 nnred ⊢ ( 𝑁 ∈ ℕ → ( 2 · 𝑁 ) ∈ ℝ )
5 peano2rem ⊢ ( ( 2 · 𝑁 ) ∈ ℝ → ( ( 2 · 𝑁 ) − 1 ) ∈ ℝ )
6 4 5 syl ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) − 1 ) ∈ ℝ )
7 chtcl ⊢ ( ( ( 2 · 𝑁 ) − 1 ) ∈ ℝ → ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ∈ ℝ )
8 6 7 syl ⊢ ( 𝑁 ∈ ℕ → ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ∈ ℝ )
9 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
10 chtcl ⊢ ( 𝑁 ∈ ℝ → ( θ ‘ 𝑁 ) ∈ ℝ )
11 9 10 syl ⊢ ( 𝑁 ∈ ℕ → ( θ ‘ 𝑁 ) ∈ ℝ )
12 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
13 2m1e1 ⊢ ( 2 − 1 ) = 1
14 13 oveq2i ⊢ ( ( 2 · 𝑁 ) − ( 2 − 1 ) ) = ( ( 2 · 𝑁 ) − 1 )
15 3 nncnd ⊢ ( 𝑁 ∈ ℕ → ( 2 · 𝑁 ) ∈ ℂ )
16 2cn ⊢ 2 ∈ ℂ
17 ax-1cn ⊢ 1 ∈ ℂ
18 subsub ⊢ ( ( ( 2 · 𝑁 ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 2 · 𝑁 ) − ( 2 − 1 ) ) = ( ( ( 2 · 𝑁 ) − 2 ) + 1 ) )
19 16 17 18 mp3an23 ⊢ ( ( 2 · 𝑁 ) ∈ ℂ → ( ( 2 · 𝑁 ) − ( 2 − 1 ) ) = ( ( ( 2 · 𝑁 ) − 2 ) + 1 ) )
20 15 19 syl ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) − ( 2 − 1 ) ) = ( ( ( 2 · 𝑁 ) − 2 ) + 1 ) )
21 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
22 subdi ⊢ ( ( 2 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 2 · ( 𝑁 − 1 ) ) = ( ( 2 · 𝑁 ) − ( 2 · 1 ) ) )
23 16 17 22 mp3an13 ⊢ ( 𝑁 ∈ ℂ → ( 2 · ( 𝑁 − 1 ) ) = ( ( 2 · 𝑁 ) − ( 2 · 1 ) ) )
24 21 23 syl ⊢ ( 𝑁 ∈ ℕ → ( 2 · ( 𝑁 − 1 ) ) = ( ( 2 · 𝑁 ) − ( 2 · 1 ) ) )
25 2t1e2 ⊢ ( 2 · 1 ) = 2
26 25 oveq2i ⊢ ( ( 2 · 𝑁 ) − ( 2 · 1 ) ) = ( ( 2 · 𝑁 ) − 2 )
27 24 26 eqtrdi ⊢ ( 𝑁 ∈ ℕ → ( 2 · ( 𝑁 − 1 ) ) = ( ( 2 · 𝑁 ) − 2 ) )
28 27 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · ( 𝑁 − 1 ) ) + 1 ) = ( ( ( 2 · 𝑁 ) − 2 ) + 1 ) )
29 20 28 eqtr4d ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) − ( 2 − 1 ) ) = ( ( 2 · ( 𝑁 − 1 ) ) + 1 ) )
30 14 29 eqtr3id ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) − 1 ) = ( ( 2 · ( 𝑁 − 1 ) ) + 1 ) )
31 2nn0 ⊢ 2 ∈ ℕ0
32 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
33 nn0mulcl ⊢ ( ( 2 ∈ ℕ0 ∧ ( 𝑁 − 1 ) ∈ ℕ0 ) → ( 2 · ( 𝑁 − 1 ) ) ∈ ℕ0 )
34 31 32 33 sylancr ⊢ ( 𝑁 ∈ ℕ → ( 2 · ( 𝑁 − 1 ) ) ∈ ℕ0 )
35 nn0p1nn ⊢ ( ( 2 · ( 𝑁 − 1 ) ) ∈ ℕ0 → ( ( 2 · ( 𝑁 − 1 ) ) + 1 ) ∈ ℕ )
36 34 35 syl ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · ( 𝑁 − 1 ) ) + 1 ) ∈ ℕ )
37 30 36 eqeltrd ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) − 1 ) ∈ ℕ )
38 nnnn0 ⊢ ( ( ( 2 · 𝑁 ) − 1 ) ∈ ℕ → ( ( 2 · 𝑁 ) − 1 ) ∈ ℕ0 )
39 37 38 syl ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) − 1 ) ∈ ℕ0 )
40 1re ⊢ 1 ∈ ℝ
41 40 a1i ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℝ )
42 nnge1 ⊢ ( 𝑁 ∈ ℕ → 1 ≤ 𝑁 )
43 41 9 9 42 leadd2dd ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ≤ ( 𝑁 + 𝑁 ) )
44 21 2timesd ⊢ ( 𝑁 ∈ ℕ → ( 2 · 𝑁 ) = ( 𝑁 + 𝑁 ) )
45 43 44 breqtrrd ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ≤ ( 2 · 𝑁 ) )
46 leaddsub ⊢ ( ( 𝑁 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 2 · 𝑁 ) ∈ ℝ ) → ( ( 𝑁 + 1 ) ≤ ( 2 · 𝑁 ) ↔ 𝑁 ≤ ( ( 2 · 𝑁 ) − 1 ) ) )
47 9 41 4 46 syl3anc ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) ≤ ( 2 · 𝑁 ) ↔ 𝑁 ≤ ( ( 2 · 𝑁 ) − 1 ) ) )
48 45 47 mpbid ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≤ ( ( 2 · 𝑁 ) − 1 ) )
49 elfz2nn0 ⊢ ( 𝑁 ∈ ( 0 ... ( ( 2 · 𝑁 ) − 1 ) ) ↔ ( 𝑁 ∈ ℕ0 ∧ ( ( 2 · 𝑁 ) − 1 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ( 2 · 𝑁 ) − 1 ) ) )
50 12 39 48 49 syl3anbrc ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( 0 ... ( ( 2 · 𝑁 ) − 1 ) ) )
51 bccl2 ⊢ ( 𝑁 ∈ ( 0 ... ( ( 2 · 𝑁 ) − 1 ) ) → ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ∈ ℕ )
52 50 51 syl ⊢ ( 𝑁 ∈ ℕ → ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ∈ ℕ )
53 52 nnrpd ⊢ ( 𝑁 ∈ ℕ → ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ∈ ℝ+ )
54 53 relogcld ⊢ ( 𝑁 ∈ ℕ → ( log ‘ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ∈ ℝ )
55 11 54 readdcld ⊢ ( 𝑁 ∈ ℕ → ( ( θ ‘ 𝑁 ) + ( log ‘ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) ∈ ℝ )
56 4re ⊢ 4 ∈ ℝ
57 4pos ⊢ 0 < 4
58 56 57 elrpii ⊢ 4 ∈ ℝ+
59 relogcl ⊢ ( 4 ∈ ℝ+ → ( log ‘ 4 ) ∈ ℝ )
60 58 59 ax-mp ⊢ ( log ‘ 4 ) ∈ ℝ
61 32 nn0red ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℝ )
62 remulcl ⊢ ( ( ( log ‘ 4 ) ∈ ℝ ∧ ( 𝑁 − 1 ) ∈ ℝ ) → ( ( log ‘ 4 ) · ( 𝑁 − 1 ) ) ∈ ℝ )
63 60 61 62 sylancr ⊢ ( 𝑁 ∈ ℕ → ( ( log ‘ 4 ) · ( 𝑁 − 1 ) ) ∈ ℝ )
64 11 63 readdcld ⊢ ( 𝑁 ∈ ℕ → ( ( θ ‘ 𝑁 ) + ( ( log ‘ 4 ) · ( 𝑁 − 1 ) ) ) ∈ ℝ )
65 iftrue ⊢ ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) → if ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) , 1 , 0 ) = 1 )
66 65 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ) → if ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) , 1 , 0 ) = 1 )
67 simpr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℙ )
68 52 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ∈ ℕ )
69 67 68 pccld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ∈ ℕ0 )
70 nn0addge1 ⊢ ( ( 1 ∈ ℝ ∧ ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ∈ ℕ0 ) → 1 ≤ ( 1 + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) )
71 40 69 70 sylancr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → 1 ≤ ( 1 + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) )
72 iftrue ⊢ ( 𝑝 ≤ 𝑁 → if ( 𝑝 ≤ 𝑁 , 1 , 0 ) = 1 )
73 72 oveq1d ⊢ ( 𝑝 ≤ 𝑁 → ( if ( 𝑝 ≤ 𝑁 , 1 , 0 ) + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) = ( 1 + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) )
74 73 breq2d ⊢ ( 𝑝 ≤ 𝑁 → ( 1 ≤ ( if ( 𝑝 ≤ 𝑁 , 1 , 0 ) + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) ↔ 1 ≤ ( 1 + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) ) )
75 71 74 syl5ibrcom ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ≤ 𝑁 → 1 ≤ ( if ( 𝑝 ≤ 𝑁 , 1 , 0 ) + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) ) )
76 75 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ) → ( 𝑝 ≤ 𝑁 → 1 ≤ ( if ( 𝑝 ≤ 𝑁 , 1 , 0 ) + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) ) )
77 prmnn ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
78 77 ad2antlr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ∧ ¬ 𝑝 ≤ 𝑁 ) ) → 𝑝 ∈ ℕ )
79 simprl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ∧ ¬ 𝑝 ≤ 𝑁 ) ) → 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) )
80 prmz ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
81 37 nnzd ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) − 1 ) ∈ ℤ )
82 eluz ⊢ ( ( 𝑝 ∈ ℤ ∧ ( ( 2 · 𝑁 ) − 1 ) ∈ ℤ ) → ( ( ( 2 · 𝑁 ) − 1 ) ∈ ( ℤ≥ ‘ 𝑝 ) ↔ 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ) )
83 80 81 82 syl2anr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ( ( 2 · 𝑁 ) − 1 ) ∈ ( ℤ≥ ‘ 𝑝 ) ↔ 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ) )
84 83 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ∧ ¬ 𝑝 ≤ 𝑁 ) ) → ( ( ( 2 · 𝑁 ) − 1 ) ∈ ( ℤ≥ ‘ 𝑝 ) ↔ 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ) )
85 79 84 mpbird ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ∧ ¬ 𝑝 ≤ 𝑁 ) ) → ( ( 2 · 𝑁 ) − 1 ) ∈ ( ℤ≥ ‘ 𝑝 ) )
86 dvdsfac ⊢ ( ( 𝑝 ∈ ℕ ∧ ( ( 2 · 𝑁 ) − 1 ) ∈ ( ℤ≥ ‘ 𝑝 ) ) → 𝑝 ∥ ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) )
87 78 85 86 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ∧ ¬ 𝑝 ≤ 𝑁 ) ) → 𝑝 ∥ ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) )
88 id ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℙ )
89 39 faccld ⊢ ( 𝑁 ∈ ℕ → ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ∈ ℕ )
90 pcelnn ⊢ ( ( 𝑝 ∈ ℙ ∧ ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ∈ ℕ ) → ( ( 𝑝 pCnt ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) ∈ ℕ ↔ 𝑝 ∥ ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) )
91 88 89 90 syl2anr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 pCnt ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) ∈ ℕ ↔ 𝑝 ∥ ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) )
92 91 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ∧ ¬ 𝑝 ≤ 𝑁 ) ) → ( ( 𝑝 pCnt ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) ∈ ℕ ↔ 𝑝 ∥ ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) )
93 87 92 mpbird ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ∧ ¬ 𝑝 ≤ 𝑁 ) ) → ( 𝑝 pCnt ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) ∈ ℕ )
94 93 nnge1d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ∧ ¬ 𝑝 ≤ 𝑁 ) ) → 1 ≤ ( 𝑝 pCnt ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) )
95 iffalse ⊢ ( ¬ 𝑝 ≤ 𝑁 → if ( 𝑝 ≤ 𝑁 , 1 , 0 ) = 0 )
96 95 oveq1d ⊢ ( ¬ 𝑝 ≤ 𝑁 → ( if ( 𝑝 ≤ 𝑁 , 1 , 0 ) + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) = ( 0 + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) )
97 96 ad2antll ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ∧ ¬ 𝑝 ≤ 𝑁 ) ) → ( if ( 𝑝 ≤ 𝑁 , 1 , 0 ) + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) = ( 0 + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) )
98 69 nn0cnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ∈ ℂ )
99 98 addid2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 0 + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) = ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) )
100 99 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ∧ ¬ 𝑝 ≤ 𝑁 ) ) → ( 0 + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) = ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) )
101 bcval2 ⊢ ( 𝑁 ∈ ( 0 ... ( ( 2 · 𝑁 ) − 1 ) ) → ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) = ( ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) / ( ( ! ‘ ( ( ( 2 · 𝑁 ) − 1 ) − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ) )
102 50 101 syl ⊢ ( 𝑁 ∈ ℕ → ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) = ( ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) / ( ( ! ‘ ( ( ( 2 · 𝑁 ) − 1 ) − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ) )
103 32 nn0cnd ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℂ )
104 17 a1i ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℂ )
105 44 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) − 1 ) = ( ( 𝑁 + 𝑁 ) − 1 ) )
106 21 21 104 105 assraddsubd ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) − 1 ) = ( 𝑁 + ( 𝑁 − 1 ) ) )
107 21 103 106 mvrladdd ⊢ ( 𝑁 ∈ ℕ → ( ( ( 2 · 𝑁 ) − 1 ) − 𝑁 ) = ( 𝑁 − 1 ) )
108 107 fveq2d ⊢ ( 𝑁 ∈ ℕ → ( ! ‘ ( ( ( 2 · 𝑁 ) − 1 ) − 𝑁 ) ) = ( ! ‘ ( 𝑁 − 1 ) ) )
109 108 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( ! ‘ ( ( ( 2 · 𝑁 ) − 1 ) − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) = ( ( ! ‘ ( 𝑁 − 1 ) ) · ( ! ‘ 𝑁 ) ) )
110 109 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) / ( ( ! ‘ ( ( ( 2 · 𝑁 ) − 1 ) − 𝑁 ) ) · ( ! ‘ 𝑁 ) ) ) = ( ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) / ( ( ! ‘ ( 𝑁 − 1 ) ) · ( ! ‘ 𝑁 ) ) ) )
111 102 110 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) = ( ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) / ( ( ! ‘ ( 𝑁 − 1 ) ) · ( ! ‘ 𝑁 ) ) ) )
112 111 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) = ( ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) / ( ( ! ‘ ( 𝑁 − 1 ) ) · ( ! ‘ 𝑁 ) ) ) )
113 112 oveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) = ( 𝑝 pCnt ( ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) / ( ( ! ‘ ( 𝑁 − 1 ) ) · ( ! ‘ 𝑁 ) ) ) ) )
114 nnz ⊢ ( ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ∈ ℕ → ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ∈ ℤ )
115 nnne0 ⊢ ( ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ∈ ℕ → ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ≠ 0 )
116 114 115 jca ⊢ ( ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ∈ ℕ → ( ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ∈ ℤ ∧ ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ≠ 0 ) )
117 89 116 syl ⊢ ( 𝑁 ∈ ℕ → ( ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ∈ ℤ ∧ ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ≠ 0 ) )
118 117 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ∈ ℤ ∧ ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ≠ 0 ) )
119 32 faccld ⊢ ( 𝑁 ∈ ℕ → ( ! ‘ ( 𝑁 − 1 ) ) ∈ ℕ )
120 12 faccld ⊢ ( 𝑁 ∈ ℕ → ( ! ‘ 𝑁 ) ∈ ℕ )
121 119 120 nnmulcld ⊢ ( 𝑁 ∈ ℕ → ( ( ! ‘ ( 𝑁 − 1 ) ) · ( ! ‘ 𝑁 ) ) ∈ ℕ )
122 121 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ( ! ‘ ( 𝑁 − 1 ) ) · ( ! ‘ 𝑁 ) ) ∈ ℕ )
123 pcdiv ⊢ ( ( 𝑝 ∈ ℙ ∧ ( ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ∈ ℤ ∧ ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ≠ 0 ) ∧ ( ( ! ‘ ( 𝑁 − 1 ) ) · ( ! ‘ 𝑁 ) ) ∈ ℕ ) → ( 𝑝 pCnt ( ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) / ( ( ! ‘ ( 𝑁 − 1 ) ) · ( ! ‘ 𝑁 ) ) ) ) = ( ( 𝑝 pCnt ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) − ( 𝑝 pCnt ( ( ! ‘ ( 𝑁 − 1 ) ) · ( ! ‘ 𝑁 ) ) ) ) )
124 67 118 122 123 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) / ( ( ! ‘ ( 𝑁 − 1 ) ) · ( ! ‘ 𝑁 ) ) ) ) = ( ( 𝑝 pCnt ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) − ( 𝑝 pCnt ( ( ! ‘ ( 𝑁 − 1 ) ) · ( ! ‘ 𝑁 ) ) ) ) )
125 nnz ⊢ ( ( ! ‘ ( 𝑁 − 1 ) ) ∈ ℕ → ( ! ‘ ( 𝑁 − 1 ) ) ∈ ℤ )
126 nnne0 ⊢ ( ( ! ‘ ( 𝑁 − 1 ) ) ∈ ℕ → ( ! ‘ ( 𝑁 − 1 ) ) ≠ 0 )
127 125 126 jca ⊢ ( ( ! ‘ ( 𝑁 − 1 ) ) ∈ ℕ → ( ( ! ‘ ( 𝑁 − 1 ) ) ∈ ℤ ∧ ( ! ‘ ( 𝑁 − 1 ) ) ≠ 0 ) )
128 119 127 syl ⊢ ( 𝑁 ∈ ℕ → ( ( ! ‘ ( 𝑁 − 1 ) ) ∈ ℤ ∧ ( ! ‘ ( 𝑁 − 1 ) ) ≠ 0 ) )
129 128 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ( ! ‘ ( 𝑁 − 1 ) ) ∈ ℤ ∧ ( ! ‘ ( 𝑁 − 1 ) ) ≠ 0 ) )
130 nnz ⊢ ( ( ! ‘ 𝑁 ) ∈ ℕ → ( ! ‘ 𝑁 ) ∈ ℤ )
131 nnne0 ⊢ ( ( ! ‘ 𝑁 ) ∈ ℕ → ( ! ‘ 𝑁 ) ≠ 0 )
132 130 131 jca ⊢ ( ( ! ‘ 𝑁 ) ∈ ℕ → ( ( ! ‘ 𝑁 ) ∈ ℤ ∧ ( ! ‘ 𝑁 ) ≠ 0 ) )
133 120 132 syl ⊢ ( 𝑁 ∈ ℕ → ( ( ! ‘ 𝑁 ) ∈ ℤ ∧ ( ! ‘ 𝑁 ) ≠ 0 ) )
134 133 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ( ! ‘ 𝑁 ) ∈ ℤ ∧ ( ! ‘ 𝑁 ) ≠ 0 ) )
135 pcmul ⊢ ( ( 𝑝 ∈ ℙ ∧ ( ( ! ‘ ( 𝑁 − 1 ) ) ∈ ℤ ∧ ( ! ‘ ( 𝑁 − 1 ) ) ≠ 0 ) ∧ ( ( ! ‘ 𝑁 ) ∈ ℤ ∧ ( ! ‘ 𝑁 ) ≠ 0 ) ) → ( 𝑝 pCnt ( ( ! ‘ ( 𝑁 − 1 ) ) · ( ! ‘ 𝑁 ) ) ) = ( ( 𝑝 pCnt ( ! ‘ ( 𝑁 − 1 ) ) ) + ( 𝑝 pCnt ( ! ‘ 𝑁 ) ) ) )
136 67 129 134 135 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( ( ! ‘ ( 𝑁 − 1 ) ) · ( ! ‘ 𝑁 ) ) ) = ( ( 𝑝 pCnt ( ! ‘ ( 𝑁 − 1 ) ) ) + ( 𝑝 pCnt ( ! ‘ 𝑁 ) ) ) )
137 136 oveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 pCnt ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) − ( 𝑝 pCnt ( ( ! ‘ ( 𝑁 − 1 ) ) · ( ! ‘ 𝑁 ) ) ) ) = ( ( 𝑝 pCnt ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) − ( ( 𝑝 pCnt ( ! ‘ ( 𝑁 − 1 ) ) ) + ( 𝑝 pCnt ( ! ‘ 𝑁 ) ) ) ) )
138 113 124 137 3eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) = ( ( 𝑝 pCnt ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) − ( ( 𝑝 pCnt ( ! ‘ ( 𝑁 − 1 ) ) ) + ( 𝑝 pCnt ( ! ‘ 𝑁 ) ) ) ) )
139 138 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ∧ ¬ 𝑝 ≤ 𝑁 ) ) → ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) = ( ( 𝑝 pCnt ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) − ( ( 𝑝 pCnt ( ! ‘ ( 𝑁 − 1 ) ) ) + ( 𝑝 pCnt ( ! ‘ 𝑁 ) ) ) ) )
140 simprr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ∧ ¬ 𝑝 ≤ 𝑁 ) ) → ¬ 𝑝 ≤ 𝑁 )
141 prmfac1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑝 ∈ ℙ ∧ 𝑝 ∥ ( ! ‘ 𝑁 ) ) → 𝑝 ≤ 𝑁 )
142 141 3expia ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( ! ‘ 𝑁 ) → 𝑝 ≤ 𝑁 ) )
143 12 142 sylan ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( ! ‘ 𝑁 ) → 𝑝 ≤ 𝑁 ) )
144 143 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ∧ ¬ 𝑝 ≤ 𝑁 ) ) → ( 𝑝 ∥ ( ! ‘ 𝑁 ) → 𝑝 ≤ 𝑁 ) )
145 140 144 mtod ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ∧ ¬ 𝑝 ≤ 𝑁 ) ) → ¬ 𝑝 ∥ ( ! ‘ 𝑁 ) )
146 80 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℤ )
147 129 simpld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ! ‘ ( 𝑁 − 1 ) ) ∈ ℤ )
148 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
149 148 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → 𝑁 ∈ ℤ )
150 dvdsmultr1 ⊢ ( ( 𝑝 ∈ ℤ ∧ ( ! ‘ ( 𝑁 − 1 ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑝 ∥ ( ! ‘ ( 𝑁 − 1 ) ) → 𝑝 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) · 𝑁 ) ) )
151 146 147 149 150 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( ! ‘ ( 𝑁 − 1 ) ) → 𝑝 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) · 𝑁 ) ) )
152 facnn2 ⊢ ( 𝑁 ∈ ℕ → ( ! ‘ 𝑁 ) = ( ( ! ‘ ( 𝑁 − 1 ) ) · 𝑁 ) )
153 152 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ! ‘ 𝑁 ) = ( ( ! ‘ ( 𝑁 − 1 ) ) · 𝑁 ) )
154 153 breq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( ! ‘ 𝑁 ) ↔ 𝑝 ∥ ( ( ! ‘ ( 𝑁 − 1 ) ) · 𝑁 ) ) )
155 151 154 sylibrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( ! ‘ ( 𝑁 − 1 ) ) → 𝑝 ∥ ( ! ‘ 𝑁 ) ) )
156 155 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ∧ ¬ 𝑝 ≤ 𝑁 ) ) → ( 𝑝 ∥ ( ! ‘ ( 𝑁 − 1 ) ) → 𝑝 ∥ ( ! ‘ 𝑁 ) ) )
157 145 156 mtod ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ∧ ¬ 𝑝 ≤ 𝑁 ) ) → ¬ 𝑝 ∥ ( ! ‘ ( 𝑁 − 1 ) ) )
158 pceq0 ⊢ ( ( 𝑝 ∈ ℙ ∧ ( ! ‘ ( 𝑁 − 1 ) ) ∈ ℕ ) → ( ( 𝑝 pCnt ( ! ‘ ( 𝑁 − 1 ) ) ) = 0 ↔ ¬ 𝑝 ∥ ( ! ‘ ( 𝑁 − 1 ) ) ) )
159 88 119 158 syl2anr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 pCnt ( ! ‘ ( 𝑁 − 1 ) ) ) = 0 ↔ ¬ 𝑝 ∥ ( ! ‘ ( 𝑁 − 1 ) ) ) )
160 159 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ∧ ¬ 𝑝 ≤ 𝑁 ) ) → ( ( 𝑝 pCnt ( ! ‘ ( 𝑁 − 1 ) ) ) = 0 ↔ ¬ 𝑝 ∥ ( ! ‘ ( 𝑁 − 1 ) ) ) )
161 157 160 mpbird ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ∧ ¬ 𝑝 ≤ 𝑁 ) ) → ( 𝑝 pCnt ( ! ‘ ( 𝑁 − 1 ) ) ) = 0 )
162 pceq0 ⊢ ( ( 𝑝 ∈ ℙ ∧ ( ! ‘ 𝑁 ) ∈ ℕ ) → ( ( 𝑝 pCnt ( ! ‘ 𝑁 ) ) = 0 ↔ ¬ 𝑝 ∥ ( ! ‘ 𝑁 ) ) )
163 88 120 162 syl2anr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 pCnt ( ! ‘ 𝑁 ) ) = 0 ↔ ¬ 𝑝 ∥ ( ! ‘ 𝑁 ) ) )
164 163 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ∧ ¬ 𝑝 ≤ 𝑁 ) ) → ( ( 𝑝 pCnt ( ! ‘ 𝑁 ) ) = 0 ↔ ¬ 𝑝 ∥ ( ! ‘ 𝑁 ) ) )
165 145 164 mpbird ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ∧ ¬ 𝑝 ≤ 𝑁 ) ) → ( 𝑝 pCnt ( ! ‘ 𝑁 ) ) = 0 )
166 161 165 oveq12d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ∧ ¬ 𝑝 ≤ 𝑁 ) ) → ( ( 𝑝 pCnt ( ! ‘ ( 𝑁 − 1 ) ) ) + ( 𝑝 pCnt ( ! ‘ 𝑁 ) ) ) = ( 0 + 0 ) )
167 00id ⊢ ( 0 + 0 ) = 0
168 166 167 eqtrdi ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ∧ ¬ 𝑝 ≤ 𝑁 ) ) → ( ( 𝑝 pCnt ( ! ‘ ( 𝑁 − 1 ) ) ) + ( 𝑝 pCnt ( ! ‘ 𝑁 ) ) ) = 0 )
169 168 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ∧ ¬ 𝑝 ≤ 𝑁 ) ) → ( ( 𝑝 pCnt ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) − ( ( 𝑝 pCnt ( ! ‘ ( 𝑁 − 1 ) ) ) + ( 𝑝 pCnt ( ! ‘ 𝑁 ) ) ) ) = ( ( 𝑝 pCnt ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) − 0 ) )
170 pccl ⊢ ( ( 𝑝 ∈ ℙ ∧ ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ∈ ℕ ) → ( 𝑝 pCnt ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) ∈ ℕ0 )
171 88 89 170 syl2anr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) ∈ ℕ0 )
172 171 nn0cnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) ∈ ℂ )
173 172 subid1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 pCnt ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) − 0 ) = ( 𝑝 pCnt ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) )
174 173 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ∧ ¬ 𝑝 ≤ 𝑁 ) ) → ( ( 𝑝 pCnt ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) − 0 ) = ( 𝑝 pCnt ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) )
175 139 169 174 3eqtrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ∧ ¬ 𝑝 ≤ 𝑁 ) ) → ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) = ( 𝑝 pCnt ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) )
176 97 100 175 3eqtrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ∧ ¬ 𝑝 ≤ 𝑁 ) ) → ( if ( 𝑝 ≤ 𝑁 , 1 , 0 ) + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) = ( 𝑝 pCnt ( ! ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) )
177 94 176 breqtrrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ∧ ¬ 𝑝 ≤ 𝑁 ) ) → 1 ≤ ( if ( 𝑝 ≤ 𝑁 , 1 , 0 ) + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) )
178 177 expr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ) → ( ¬ 𝑝 ≤ 𝑁 → 1 ≤ ( if ( 𝑝 ≤ 𝑁 , 1 , 0 ) + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) ) )
179 76 178 pm2.61d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ) → 1 ≤ ( if ( 𝑝 ≤ 𝑁 , 1 , 0 ) + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) )
180 66 179 eqbrtrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) ) → if ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) , 1 , 0 ) ≤ ( if ( 𝑝 ≤ 𝑁 , 1 , 0 ) + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) )
181 180 ex ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) → if ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) , 1 , 0 ) ≤ ( if ( 𝑝 ≤ 𝑁 , 1 , 0 ) + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) ) )
182 1nn0 ⊢ 1 ∈ ℕ0
183 0nn0 ⊢ 0 ∈ ℕ0
184 182 183 ifcli ⊢ if ( 𝑝 ≤ 𝑁 , 1 , 0 ) ∈ ℕ0
185 nn0addcl ⊢ ( ( if ( 𝑝 ≤ 𝑁 , 1 , 0 ) ∈ ℕ0 ∧ ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ∈ ℕ0 ) → ( if ( 𝑝 ≤ 𝑁 , 1 , 0 ) + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) ∈ ℕ0 )
186 184 69 185 sylancr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( if ( 𝑝 ≤ 𝑁 , 1 , 0 ) + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) ∈ ℕ0 )
187 186 nn0ge0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → 0 ≤ ( if ( 𝑝 ≤ 𝑁 , 1 , 0 ) + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) )
188 iffalse ⊢ ( ¬ 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) → if ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) , 1 , 0 ) = 0 )
189 188 breq1d ⊢ ( ¬ 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) → ( if ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) , 1 , 0 ) ≤ ( if ( 𝑝 ≤ 𝑁 , 1 , 0 ) + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) ↔ 0 ≤ ( if ( 𝑝 ≤ 𝑁 , 1 , 0 ) + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) ) )
190 187 189 syl5ibrcom ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ¬ 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) → if ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) , 1 , 0 ) ≤ ( if ( 𝑝 ≤ 𝑁 , 1 , 0 ) + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) ) )
191 181 190 pm2.61d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → if ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) , 1 , 0 ) ≤ ( if ( 𝑝 ≤ 𝑁 , 1 , 0 ) + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) )
192 eqid ⊢ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) )
193 192 prmorcht ⊢ ( ( ( 2 · 𝑁 ) − 1 ) ∈ ℕ → ( exp ‘ ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) ) ) ‘ ( ( 2 · 𝑁 ) − 1 ) ) )
194 37 193 syl ⊢ ( 𝑁 ∈ ℕ → ( exp ‘ ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) ) ) ‘ ( ( 2 · 𝑁 ) − 1 ) ) )
195 194 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( 𝑝 pCnt ( exp ‘ ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) ) = ( 𝑝 pCnt ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) ) ) ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) )
196 195 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( exp ‘ ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) ) = ( 𝑝 pCnt ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) ) ) ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) )
197 nncn ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
198 197 exp1d ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 ↑ 1 ) = 𝑛 )
199 198 ifeq1d ⊢ ( 𝑛 ∈ ℕ → if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ 1 ) , 1 ) = if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) )
200 199 mpteq2ia ⊢ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ 1 ) , 1 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) )
201 200 eqcomi ⊢ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ 1 ) , 1 ) )
202 182 a1i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑛 ∈ ℙ ) → 1 ∈ ℕ0 )
203 202 ralrimiva ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ∀ 𝑛 ∈ ℙ 1 ∈ ℕ0 )
204 37 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ( 2 · 𝑁 ) − 1 ) ∈ ℕ )
205 eqidd ⊢ ( 𝑛 = 𝑝 → 1 = 1 )
206 201 203 204 67 205 pcmpt ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) ) ) ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) = if ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) , 1 , 0 ) )
207 196 206 eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( exp ‘ ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) ) = if ( 𝑝 ≤ ( ( 2 · 𝑁 ) − 1 ) , 1 , 0 ) )
208 efchtcl ⊢ ( 𝑁 ∈ ℝ → ( exp ‘ ( θ ‘ 𝑁 ) ) ∈ ℕ )
209 9 208 syl ⊢ ( 𝑁 ∈ ℕ → ( exp ‘ ( θ ‘ 𝑁 ) ) ∈ ℕ )
210 209 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( exp ‘ ( θ ‘ 𝑁 ) ) ∈ ℕ )
211 nnz ⊢ ( ( exp ‘ ( θ ‘ 𝑁 ) ) ∈ ℕ → ( exp ‘ ( θ ‘ 𝑁 ) ) ∈ ℤ )
212 nnne0 ⊢ ( ( exp ‘ ( θ ‘ 𝑁 ) ) ∈ ℕ → ( exp ‘ ( θ ‘ 𝑁 ) ) ≠ 0 )
213 211 212 jca ⊢ ( ( exp ‘ ( θ ‘ 𝑁 ) ) ∈ ℕ → ( ( exp ‘ ( θ ‘ 𝑁 ) ) ∈ ℤ ∧ ( exp ‘ ( θ ‘ 𝑁 ) ) ≠ 0 ) )
214 210 213 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ( exp ‘ ( θ ‘ 𝑁 ) ) ∈ ℤ ∧ ( exp ‘ ( θ ‘ 𝑁 ) ) ≠ 0 ) )
215 nnz ⊢ ( ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ∈ ℕ → ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ∈ ℤ )
216 nnne0 ⊢ ( ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ∈ ℕ → ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ≠ 0 )
217 215 216 jca ⊢ ( ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ∈ ℕ → ( ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ∈ ℤ ∧ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ≠ 0 ) )
218 68 217 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ∈ ℤ ∧ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ≠ 0 ) )
219 pcmul ⊢ ( ( 𝑝 ∈ ℙ ∧ ( ( exp ‘ ( θ ‘ 𝑁 ) ) ∈ ℤ ∧ ( exp ‘ ( θ ‘ 𝑁 ) ) ≠ 0 ) ∧ ( ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ∈ ℤ ∧ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ≠ 0 ) ) → ( 𝑝 pCnt ( ( exp ‘ ( θ ‘ 𝑁 ) ) · ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) = ( ( 𝑝 pCnt ( exp ‘ ( θ ‘ 𝑁 ) ) ) + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) )
220 67 214 218 219 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( ( exp ‘ ( θ ‘ 𝑁 ) ) · ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) = ( ( 𝑝 pCnt ( exp ‘ ( θ ‘ 𝑁 ) ) ) + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) )
221 192 prmorcht ⊢ ( 𝑁 ∈ ℕ → ( exp ‘ ( θ ‘ 𝑁 ) ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) ) ) ‘ 𝑁 ) )
222 221 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( 𝑝 pCnt ( exp ‘ ( θ ‘ 𝑁 ) ) ) = ( 𝑝 pCnt ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) ) ) ‘ 𝑁 ) ) )
223 222 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( exp ‘ ( θ ‘ 𝑁 ) ) ) = ( 𝑝 pCnt ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) ) ) ‘ 𝑁 ) ) )
224 simpl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → 𝑁 ∈ ℕ )
225 201 203 224 67 205 pcmpt ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , 𝑛 , 1 ) ) ) ‘ 𝑁 ) ) = if ( 𝑝 ≤ 𝑁 , 1 , 0 ) )
226 223 225 eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( exp ‘ ( θ ‘ 𝑁 ) ) ) = if ( 𝑝 ≤ 𝑁 , 1 , 0 ) )
227 226 oveq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 pCnt ( exp ‘ ( θ ‘ 𝑁 ) ) ) + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) = ( if ( 𝑝 ≤ 𝑁 , 1 , 0 ) + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) )
228 220 227 eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( ( exp ‘ ( θ ‘ 𝑁 ) ) · ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) = ( if ( 𝑝 ≤ 𝑁 , 1 , 0 ) + ( 𝑝 pCnt ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) )
229 191 207 228 3brtr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( exp ‘ ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) ) ≤ ( 𝑝 pCnt ( ( exp ‘ ( θ ‘ 𝑁 ) ) · ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) )
230 229 ralrimiva ⊢ ( 𝑁 ∈ ℕ → ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt ( exp ‘ ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) ) ≤ ( 𝑝 pCnt ( ( exp ‘ ( θ ‘ 𝑁 ) ) · ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) )
231 efchtcl ⊢ ( ( ( 2 · 𝑁 ) − 1 ) ∈ ℝ → ( exp ‘ ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) ∈ ℕ )
232 6 231 syl ⊢ ( 𝑁 ∈ ℕ → ( exp ‘ ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) ∈ ℕ )
233 232 nnzd ⊢ ( 𝑁 ∈ ℕ → ( exp ‘ ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) ∈ ℤ )
234 209 52 nnmulcld ⊢ ( 𝑁 ∈ ℕ → ( ( exp ‘ ( θ ‘ 𝑁 ) ) · ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ∈ ℕ )
235 234 nnzd ⊢ ( 𝑁 ∈ ℕ → ( ( exp ‘ ( θ ‘ 𝑁 ) ) · ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ∈ ℤ )
236 pc2dvds ⊢ ( ( ( exp ‘ ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) ∈ ℤ ∧ ( ( exp ‘ ( θ ‘ 𝑁 ) ) · ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ∈ ℤ ) → ( ( exp ‘ ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) ∥ ( ( exp ‘ ( θ ‘ 𝑁 ) ) · ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt ( exp ‘ ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) ) ≤ ( 𝑝 pCnt ( ( exp ‘ ( θ ‘ 𝑁 ) ) · ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) ) )
237 233 235 236 syl2anc ⊢ ( 𝑁 ∈ ℕ → ( ( exp ‘ ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) ∥ ( ( exp ‘ ( θ ‘ 𝑁 ) ) · ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt ( exp ‘ ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) ) ≤ ( 𝑝 pCnt ( ( exp ‘ ( θ ‘ 𝑁 ) ) · ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) ) )
238 230 237 mpbird ⊢ ( 𝑁 ∈ ℕ → ( exp ‘ ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) ∥ ( ( exp ‘ ( θ ‘ 𝑁 ) ) · ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) )
239 dvdsle ⊢ ( ( ( exp ‘ ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) ∈ ℤ ∧ ( ( exp ‘ ( θ ‘ 𝑁 ) ) · ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ∈ ℕ ) → ( ( exp ‘ ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) ∥ ( ( exp ‘ ( θ ‘ 𝑁 ) ) · ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) → ( exp ‘ ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) ≤ ( ( exp ‘ ( θ ‘ 𝑁 ) ) · ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) )
240 233 234 239 syl2anc ⊢ ( 𝑁 ∈ ℕ → ( ( exp ‘ ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) ∥ ( ( exp ‘ ( θ ‘ 𝑁 ) ) · ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) → ( exp ‘ ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) ≤ ( ( exp ‘ ( θ ‘ 𝑁 ) ) · ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) )
241 238 240 mpd ⊢ ( 𝑁 ∈ ℕ → ( exp ‘ ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) ≤ ( ( exp ‘ ( θ ‘ 𝑁 ) ) · ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) )
242 11 recnd ⊢ ( 𝑁 ∈ ℕ → ( θ ‘ 𝑁 ) ∈ ℂ )
243 54 recnd ⊢ ( 𝑁 ∈ ℕ → ( log ‘ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ∈ ℂ )
244 efadd ⊢ ( ( ( θ ‘ 𝑁 ) ∈ ℂ ∧ ( log ‘ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ∈ ℂ ) → ( exp ‘ ( ( θ ‘ 𝑁 ) + ( log ‘ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) ) = ( ( exp ‘ ( θ ‘ 𝑁 ) ) · ( exp ‘ ( log ‘ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) ) )
245 242 243 244 syl2anc ⊢ ( 𝑁 ∈ ℕ → ( exp ‘ ( ( θ ‘ 𝑁 ) + ( log ‘ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) ) = ( ( exp ‘ ( θ ‘ 𝑁 ) ) · ( exp ‘ ( log ‘ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) ) )
246 53 reeflogd ⊢ ( 𝑁 ∈ ℕ → ( exp ‘ ( log ‘ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) = ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) )
247 246 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( ( exp ‘ ( θ ‘ 𝑁 ) ) · ( exp ‘ ( log ‘ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) ) = ( ( exp ‘ ( θ ‘ 𝑁 ) ) · ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) )
248 245 247 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( exp ‘ ( ( θ ‘ 𝑁 ) + ( log ‘ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) ) = ( ( exp ‘ ( θ ‘ 𝑁 ) ) · ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) )
249 241 248 breqtrrd ⊢ ( 𝑁 ∈ ℕ → ( exp ‘ ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) ≤ ( exp ‘ ( ( θ ‘ 𝑁 ) + ( log ‘ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) ) )
250 efle ⊢ ( ( ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ∈ ℝ ∧ ( ( θ ‘ 𝑁 ) + ( log ‘ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) ∈ ℝ ) → ( ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ≤ ( ( θ ‘ 𝑁 ) + ( log ‘ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) ↔ ( exp ‘ ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) ≤ ( exp ‘ ( ( θ ‘ 𝑁 ) + ( log ‘ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) ) ) )
251 8 55 250 syl2anc ⊢ ( 𝑁 ∈ ℕ → ( ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ≤ ( ( θ ‘ 𝑁 ) + ( log ‘ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) ↔ ( exp ‘ ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ) ≤ ( exp ‘ ( ( θ ‘ 𝑁 ) + ( log ‘ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) ) ) )
252 249 251 mpbird ⊢ ( 𝑁 ∈ ℕ → ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ≤ ( ( θ ‘ 𝑁 ) + ( log ‘ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) )
253 fzfid ⊢ ( 𝑁 ∈ ℕ → ( 0 ... ( ( 2 · 𝑁 ) − 1 ) ) ∈ Fin )
254 elfzelz ⊢ ( 𝑘 ∈ ( 0 ... ( ( 2 · 𝑁 ) − 1 ) ) → 𝑘 ∈ ℤ )
255 bccl ⊢ ( ( ( ( 2 · 𝑁 ) − 1 ) ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( ( ( 2 · 𝑁 ) − 1 ) C 𝑘 ) ∈ ℕ0 )
256 39 254 255 syl2an ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... ( ( 2 · 𝑁 ) − 1 ) ) ) → ( ( ( 2 · 𝑁 ) − 1 ) C 𝑘 ) ∈ ℕ0 )
257 256 nn0red ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... ( ( 2 · 𝑁 ) − 1 ) ) ) → ( ( ( 2 · 𝑁 ) − 1 ) C 𝑘 ) ∈ ℝ )
258 256 nn0ge0d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... ( ( 2 · 𝑁 ) − 1 ) ) ) → 0 ≤ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑘 ) )
259 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
260 32 259 eleqtrdi ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
261 fzss1 ⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 0 ) → ( ( 𝑁 − 1 ) ... 𝑁 ) ⊆ ( 0 ... 𝑁 ) )
262 260 261 syl ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) ... 𝑁 ) ⊆ ( 0 ... 𝑁 ) )
263 eluz ⊢ ( ( 𝑁 ∈ ℤ ∧ ( ( 2 · 𝑁 ) − 1 ) ∈ ℤ ) → ( ( ( 2 · 𝑁 ) − 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ↔ 𝑁 ≤ ( ( 2 · 𝑁 ) − 1 ) ) )
264 148 81 263 syl2anc ⊢ ( 𝑁 ∈ ℕ → ( ( ( 2 · 𝑁 ) − 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ↔ 𝑁 ≤ ( ( 2 · 𝑁 ) − 1 ) ) )
265 48 264 mpbird ⊢ ( 𝑁 ∈ ℕ → ( ( 2 · 𝑁 ) − 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
266 fzss2 ⊢ ( ( ( 2 · 𝑁 ) − 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) → ( 0 ... 𝑁 ) ⊆ ( 0 ... ( ( 2 · 𝑁 ) − 1 ) ) )
267 265 266 syl ⊢ ( 𝑁 ∈ ℕ → ( 0 ... 𝑁 ) ⊆ ( 0 ... ( ( 2 · 𝑁 ) − 1 ) ) )
268 262 267 sstrd ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) ... 𝑁 ) ⊆ ( 0 ... ( ( 2 · 𝑁 ) − 1 ) ) )
269 253 257 258 268 fsumless ⊢ ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( ( 𝑁 − 1 ) ... 𝑁 ) ( ( ( 2 · 𝑁 ) − 1 ) C 𝑘 ) ≤ Σ 𝑘 ∈ ( 0 ... ( ( 2 · 𝑁 ) − 1 ) ) ( ( ( 2 · 𝑁 ) − 1 ) C 𝑘 ) )
270 32 nn0zd ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℤ )
271 bccmpl ⊢ ( ( ( ( 2 · 𝑁 ) − 1 ) ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) → ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) = ( ( ( 2 · 𝑁 ) − 1 ) C ( ( ( 2 · 𝑁 ) − 1 ) − 𝑁 ) ) )
272 39 148 271 syl2anc ⊢ ( 𝑁 ∈ ℕ → ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) = ( ( ( 2 · 𝑁 ) − 1 ) C ( ( ( 2 · 𝑁 ) − 1 ) − 𝑁 ) ) )
273 107 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( ( ( 2 · 𝑁 ) − 1 ) C ( ( ( 2 · 𝑁 ) − 1 ) − 𝑁 ) ) = ( ( ( 2 · 𝑁 ) − 1 ) C ( 𝑁 − 1 ) ) )
274 272 273 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) = ( ( ( 2 · 𝑁 ) − 1 ) C ( 𝑁 − 1 ) ) )
275 52 nncnd ⊢ ( 𝑁 ∈ ℕ → ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ∈ ℂ )
276 274 275 eqeltrrd ⊢ ( 𝑁 ∈ ℕ → ( ( ( 2 · 𝑁 ) − 1 ) C ( 𝑁 − 1 ) ) ∈ ℂ )
277 oveq2 ⊢ ( 𝑘 = ( 𝑁 − 1 ) → ( ( ( 2 · 𝑁 ) − 1 ) C 𝑘 ) = ( ( ( 2 · 𝑁 ) − 1 ) C ( 𝑁 − 1 ) ) )
278 277 fsum1 ⊢ ( ( ( 𝑁 − 1 ) ∈ ℤ ∧ ( ( ( 2 · 𝑁 ) − 1 ) C ( 𝑁 − 1 ) ) ∈ ℂ ) → Σ 𝑘 ∈ ( ( 𝑁 − 1 ) ... ( 𝑁 − 1 ) ) ( ( ( 2 · 𝑁 ) − 1 ) C 𝑘 ) = ( ( ( 2 · 𝑁 ) − 1 ) C ( 𝑁 − 1 ) ) )
279 270 276 278 syl2anc ⊢ ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( ( 𝑁 − 1 ) ... ( 𝑁 − 1 ) ) ( ( ( 2 · 𝑁 ) − 1 ) C 𝑘 ) = ( ( ( 2 · 𝑁 ) − 1 ) C ( 𝑁 − 1 ) ) )
280 279 274 eqtr4d ⊢ ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( ( 𝑁 − 1 ) ... ( 𝑁 − 1 ) ) ( ( ( 2 · 𝑁 ) − 1 ) C 𝑘 ) = ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) )
281 280 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑘 ∈ ( ( 𝑁 − 1 ) ... ( 𝑁 − 1 ) ) ( ( ( 2 · 𝑁 ) − 1 ) C 𝑘 ) + ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) = ( ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) + ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) )
282 21 104 npcand ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
283 uzid ⊢ ( ( 𝑁 − 1 ) ∈ ℤ → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
284 270 283 syl ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
285 peano2uz ⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
286 284 285 syl ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
287 282 286 eqeltrrd ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
288 268 sselda ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( ( 𝑁 − 1 ) ... 𝑁 ) ) → 𝑘 ∈ ( 0 ... ( ( 2 · 𝑁 ) − 1 ) ) )
289 256 nn0cnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... ( ( 2 · 𝑁 ) − 1 ) ) ) → ( ( ( 2 · 𝑁 ) − 1 ) C 𝑘 ) ∈ ℂ )
290 288 289 syldan ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( ( 𝑁 − 1 ) ... 𝑁 ) ) → ( ( ( 2 · 𝑁 ) − 1 ) C 𝑘 ) ∈ ℂ )
291 oveq2 ⊢ ( 𝑘 = 𝑁 → ( ( ( 2 · 𝑁 ) − 1 ) C 𝑘 ) = ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) )
292 287 290 291 fsumm1 ⊢ ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( ( 𝑁 − 1 ) ... 𝑁 ) ( ( ( 2 · 𝑁 ) − 1 ) C 𝑘 ) = ( Σ 𝑘 ∈ ( ( 𝑁 − 1 ) ... ( 𝑁 − 1 ) ) ( ( ( 2 · 𝑁 ) − 1 ) C 𝑘 ) + ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) )
293 275 2timesd ⊢ ( 𝑁 ∈ ℕ → ( 2 · ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) = ( ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) + ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) )
294 281 292 293 3eqtr4rd ⊢ ( 𝑁 ∈ ℕ → ( 2 · ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) = Σ 𝑘 ∈ ( ( 𝑁 − 1 ) ... 𝑁 ) ( ( ( 2 · 𝑁 ) − 1 ) C 𝑘 ) )
295 binom11 ⊢ ( ( ( 2 · 𝑁 ) − 1 ) ∈ ℕ0 → ( 2 ↑ ( ( 2 · 𝑁 ) − 1 ) ) = Σ 𝑘 ∈ ( 0 ... ( ( 2 · 𝑁 ) − 1 ) ) ( ( ( 2 · 𝑁 ) − 1 ) C 𝑘 ) )
296 39 295 syl ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( ( 2 · 𝑁 ) − 1 ) ) = Σ 𝑘 ∈ ( 0 ... ( ( 2 · 𝑁 ) − 1 ) ) ( ( ( 2 · 𝑁 ) − 1 ) C 𝑘 ) )
297 269 294 296 3brtr4d ⊢ ( 𝑁 ∈ ℕ → ( 2 · ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ≤ ( 2 ↑ ( ( 2 · 𝑁 ) − 1 ) ) )
298 mulcom ⊢ ( ( 2 ∈ ℂ ∧ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ∈ ℂ ) → ( 2 · ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) = ( ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) · 2 ) )
299 16 275 298 sylancr ⊢ ( 𝑁 ∈ ℕ → ( 2 · ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) = ( ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) · 2 ) )
300 30 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( ( 2 · 𝑁 ) − 1 ) ) = ( 2 ↑ ( ( 2 · ( 𝑁 − 1 ) ) + 1 ) ) )
301 expp1 ⊢ ( ( 2 ∈ ℂ ∧ ( 2 · ( 𝑁 − 1 ) ) ∈ ℕ0 ) → ( 2 ↑ ( ( 2 · ( 𝑁 − 1 ) ) + 1 ) ) = ( ( 2 ↑ ( 2 · ( 𝑁 − 1 ) ) ) · 2 ) )
302 16 34 301 sylancr ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( ( 2 · ( 𝑁 − 1 ) ) + 1 ) ) = ( ( 2 ↑ ( 2 · ( 𝑁 − 1 ) ) ) · 2 ) )
303 16 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℂ )
304 31 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℕ0 )
305 303 32 304 expmuld ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( 2 · ( 𝑁 − 1 ) ) ) = ( ( 2 ↑ 2 ) ↑ ( 𝑁 − 1 ) ) )
306 sq2 ⊢ ( 2 ↑ 2 ) = 4
307 306 oveq1i ⊢ ( ( 2 ↑ 2 ) ↑ ( 𝑁 − 1 ) ) = ( 4 ↑ ( 𝑁 − 1 ) )
308 305 307 eqtrdi ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( 2 · ( 𝑁 − 1 ) ) ) = ( 4 ↑ ( 𝑁 − 1 ) ) )
309 308 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( 2 ↑ ( 2 · ( 𝑁 − 1 ) ) ) · 2 ) = ( ( 4 ↑ ( 𝑁 − 1 ) ) · 2 ) )
310 300 302 309 3eqtrd ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( ( 2 · 𝑁 ) − 1 ) ) = ( ( 4 ↑ ( 𝑁 − 1 ) ) · 2 ) )
311 297 299 310 3brtr3d ⊢ ( 𝑁 ∈ ℕ → ( ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) · 2 ) ≤ ( ( 4 ↑ ( 𝑁 − 1 ) ) · 2 ) )
312 52 nnred ⊢ ( 𝑁 ∈ ℕ → ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ∈ ℝ )
313 reexpcl ⊢ ( ( 4 ∈ ℝ ∧ ( 𝑁 − 1 ) ∈ ℕ0 ) → ( 4 ↑ ( 𝑁 − 1 ) ) ∈ ℝ )
314 56 32 313 sylancr ⊢ ( 𝑁 ∈ ℕ → ( 4 ↑ ( 𝑁 − 1 ) ) ∈ ℝ )
315 2re ⊢ 2 ∈ ℝ
316 2pos ⊢ 0 < 2
317 315 316 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
318 317 a1i ⊢ ( 𝑁 ∈ ℕ → ( 2 ∈ ℝ ∧ 0 < 2 ) )
319 lemul1 ⊢ ( ( ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ∈ ℝ ∧ ( 4 ↑ ( 𝑁 − 1 ) ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ≤ ( 4 ↑ ( 𝑁 − 1 ) ) ↔ ( ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) · 2 ) ≤ ( ( 4 ↑ ( 𝑁 − 1 ) ) · 2 ) ) )
320 312 314 318 319 syl3anc ⊢ ( 𝑁 ∈ ℕ → ( ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ≤ ( 4 ↑ ( 𝑁 − 1 ) ) ↔ ( ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) · 2 ) ≤ ( ( 4 ↑ ( 𝑁 − 1 ) ) · 2 ) ) )
321 311 320 mpbird ⊢ ( 𝑁 ∈ ℕ → ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ≤ ( 4 ↑ ( 𝑁 − 1 ) ) )
322 60 recni ⊢ ( log ‘ 4 ) ∈ ℂ
323 mulcom ⊢ ( ( ( log ‘ 4 ) ∈ ℂ ∧ ( 𝑁 − 1 ) ∈ ℂ ) → ( ( log ‘ 4 ) · ( 𝑁 − 1 ) ) = ( ( 𝑁 − 1 ) · ( log ‘ 4 ) ) )
324 322 103 323 sylancr ⊢ ( 𝑁 ∈ ℕ → ( ( log ‘ 4 ) · ( 𝑁 − 1 ) ) = ( ( 𝑁 − 1 ) · ( log ‘ 4 ) ) )
325 324 fveq2d ⊢ ( 𝑁 ∈ ℕ → ( exp ‘ ( ( log ‘ 4 ) · ( 𝑁 − 1 ) ) ) = ( exp ‘ ( ( 𝑁 − 1 ) · ( log ‘ 4 ) ) ) )
326 reexplog ⊢ ( ( 4 ∈ ℝ+ ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( 4 ↑ ( 𝑁 − 1 ) ) = ( exp ‘ ( ( 𝑁 − 1 ) · ( log ‘ 4 ) ) ) )
327 58 270 326 sylancr ⊢ ( 𝑁 ∈ ℕ → ( 4 ↑ ( 𝑁 − 1 ) ) = ( exp ‘ ( ( 𝑁 − 1 ) · ( log ‘ 4 ) ) ) )
328 325 327 eqtr4d ⊢ ( 𝑁 ∈ ℕ → ( exp ‘ ( ( log ‘ 4 ) · ( 𝑁 − 1 ) ) ) = ( 4 ↑ ( 𝑁 − 1 ) ) )
329 321 246 328 3brtr4d ⊢ ( 𝑁 ∈ ℕ → ( exp ‘ ( log ‘ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) ≤ ( exp ‘ ( ( log ‘ 4 ) · ( 𝑁 − 1 ) ) ) )
330 efle ⊢ ( ( ( log ‘ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ∈ ℝ ∧ ( ( log ‘ 4 ) · ( 𝑁 − 1 ) ) ∈ ℝ ) → ( ( log ‘ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ≤ ( ( log ‘ 4 ) · ( 𝑁 − 1 ) ) ↔ ( exp ‘ ( log ‘ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) ≤ ( exp ‘ ( ( log ‘ 4 ) · ( 𝑁 − 1 ) ) ) ) )
331 54 63 330 syl2anc ⊢ ( 𝑁 ∈ ℕ → ( ( log ‘ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ≤ ( ( log ‘ 4 ) · ( 𝑁 − 1 ) ) ↔ ( exp ‘ ( log ‘ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) ≤ ( exp ‘ ( ( log ‘ 4 ) · ( 𝑁 − 1 ) ) ) ) )
332 329 331 mpbird ⊢ ( 𝑁 ∈ ℕ → ( log ‘ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ≤ ( ( log ‘ 4 ) · ( 𝑁 − 1 ) ) )
333 54 63 11 332 leadd2dd ⊢ ( 𝑁 ∈ ℕ → ( ( θ ‘ 𝑁 ) + ( log ‘ ( ( ( 2 · 𝑁 ) − 1 ) C 𝑁 ) ) ) ≤ ( ( θ ‘ 𝑁 ) + ( ( log ‘ 4 ) · ( 𝑁 − 1 ) ) ) )
334 8 55 64 252 333 letrd ⊢ ( 𝑁 ∈ ℕ → ( θ ‘ ( ( 2 · 𝑁 ) − 1 ) ) ≤ ( ( θ ‘ 𝑁 ) + ( ( log ‘ 4 ) · ( 𝑁 − 1 ) ) ) )