Metamath Proof Explorer

Theorem aks4d1p1p5

Description: Show inequality for existence of a non-divisor. (Contributed by metakunt, 19-Aug-2024)

Ref Expression
Hypotheses aks4d1p1p5.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
aks4d1p1p5.2 ⊢ 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) )
aks4d1p1p5.3 ⊢ 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) )
aks4d1p1p5.4 ⊢ ( 𝜑 → 4 ≤ 𝑁 )
aks4d1p1p5.5 ⊢ 𝐶 = ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) )
aks4d1p1p5.6 ⊢ 𝐷 = ( ( 2 logb 𝑁 ) ↑ 2 )
aks4d1p1p5.7 ⊢ 𝐸 = ( ( 2 logb 𝑁 ) ↑ 4 )
Assertion aks4d1p1p5 ( 𝜑 → 𝐴 < ( 2 ↑ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 aks4d1p1p5.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 aks4d1p1p5.2 ⊢ 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) )
3 aks4d1p1p5.3 ⊢ 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) )
4 aks4d1p1p5.4 ⊢ ( 𝜑 → 4 ≤ 𝑁 )
5 aks4d1p1p5.5 ⊢ 𝐶 = ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) )
6 aks4d1p1p5.6 ⊢ 𝐷 = ( ( 2 logb 𝑁 ) ↑ 2 )
7 aks4d1p1p5.7 ⊢ 𝐸 = ( ( 2 logb 𝑁 ) ↑ 4 )
8 3re ⊢ 3 ∈ ℝ
9 8 a1i ⊢ ( 𝜑 → 3 ∈ ℝ )
10 4re ⊢ 4 ∈ ℝ
11 10 a1i ⊢ ( 𝜑 → 4 ∈ ℝ )
12 1 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
13 9 lep1d ⊢ ( 𝜑 → 3 ≤ ( 3 + 1 ) )
14 3p1e4 ⊢ ( 3 + 1 ) = 4
15 13 14 breqtrdi ⊢ ( 𝜑 → 3 ≤ 4 )
16 9 11 12 15 4 letrd ⊢ ( 𝜑 → 3 ≤ 𝑁 )
17 2re ⊢ 2 ∈ ℝ
18 17 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → 2 ∈ ℝ )
19 2pos ⊢ 0 < 2
20 19 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → 0 < 2 )
21 elicc2 ⊢ ( ( 4 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑥 ∈ ( 4 [,] 𝑁 ) ↔ ( 𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁 ) ) )
22 11 12 21 syl2anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 4 [,] 𝑁 ) ↔ ( 𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁 ) ) )
23 22 biimpd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 4 [,] 𝑁 ) → ( 𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁 ) ) )
24 23 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → ( 𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁 ) )
25 24 simp1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → 𝑥 ∈ ℝ )
26 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → 0 ∈ ℝ )
28 10 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → 4 ∈ ℝ )
29 4pos ⊢ 0 < 4
30 29 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → 0 < 4 )
31 24 simp2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → 4 ≤ 𝑥 )
32 27 28 25 30 31 ltletrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → 0 < 𝑥 )
33 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
34 1lt2 ⊢ 1 < 2
35 34 a1i ⊢ ( 𝜑 → 1 < 2 )
36 33 35 ltned ⊢ ( 𝜑 → 1 ≠ 2 )
37 36 necomd ⊢ ( 𝜑 → 2 ≠ 1 )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → 2 ≠ 1 )
39 18 20 25 32 38 relogbcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → ( 2 logb 𝑥 ) ∈ ℝ )
40 5nn0 ⊢ 5 ∈ ℕ0
41 40 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → 5 ∈ ℕ0 )
42 39 41 reexpcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → ( ( 2 logb 𝑥 ) ↑ 5 ) ∈ ℝ )
43 1red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → 1 ∈ ℝ )
44 42 43 readdcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ∈ ℝ )
45 27 43 readdcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → ( 0 + 1 ) ∈ ℝ )
46 27 ltp1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → 0 < ( 0 + 1 ) )
47 41 nn0zd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → 5 ∈ ℤ )
48 ax-resscn ⊢ ℝ ⊆ ℂ
49 48 18 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → 2 ∈ ℂ )
50 27 20 gtned ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → 2 ≠ 0 )
51 logb1 ⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1 ) → ( 2 logb 1 ) = 0 )
52 49 50 38 51 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → ( 2 logb 1 ) = 0 )
53 1lt4 ⊢ 1 < 4
54 53 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → 1 < 4 )
55 43 28 25 54 31 ltletrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → 1 < 𝑥 )
56 2z ⊢ 2 ∈ ℤ
57 56 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → 2 ∈ ℤ )
58 57 uzidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → 2 ∈ ( ℤ≥ ‘ 2 ) )
59 1rp ⊢ 1 ∈ ℝ+
60 59 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → 1 ∈ ℝ+ )
61 25 32 elrpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → 𝑥 ∈ ℝ+ )
62 logblt ⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ 1 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) → ( 1 < 𝑥 ↔ ( 2 logb 1 ) < ( 2 logb 𝑥 ) ) )
63 58 60 61 62 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → ( 1 < 𝑥 ↔ ( 2 logb 1 ) < ( 2 logb 𝑥 ) ) )
64 55 63 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → ( 2 logb 1 ) < ( 2 logb 𝑥 ) )
65 52 64 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → 0 < ( 2 logb 𝑥 ) )
66 expgt0 ⊢ ( ( ( 2 logb 𝑥 ) ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < ( 2 logb 𝑥 ) ) → 0 < ( ( 2 logb 𝑥 ) ↑ 5 ) )
67 39 47 65 66 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → 0 < ( ( 2 logb 𝑥 ) ↑ 5 ) )
68 27 42 43 67 ltadd1dd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → ( 0 + 1 ) < ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) )
69 27 45 44 46 68 lttrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → 0 < ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) )
70 18 20 44 69 38 relogbcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ∈ ℝ )
71 18 70 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) ∈ ℝ )
72 0red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → 0 ∈ ℝ )
73 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → 𝑥 ∈ ( 4 [,] 𝑁 ) )
74 11 12 jca ⊢ ( 𝜑 → ( 4 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
75 74 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → ( 4 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
76 75 21 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → ( 𝑥 ∈ ( 4 [,] 𝑁 ) ↔ ( 𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁 ) ) )
77 73 76 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → ( 𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁 ) )
78 77 simp2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → 4 ≤ 𝑥 )
79 72 28 25 30 78 ltletrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → 0 < 𝑥 )
80 18 20 25 79 38 relogbcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → ( 2 logb 𝑥 ) ∈ ℝ )
81 80 resqcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → ( ( 2 logb 𝑥 ) ↑ 2 ) ∈ ℝ )
82 71 81 readdcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) ∈ ℝ )
83 82 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 4 [,] 𝑁 ) ↦ ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) ) : ( 4 [,] 𝑁 ) ⟶ ℝ )
84 48 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
85 3lt4 ⊢ 3 < 4
86 85 a1i ⊢ ( 𝜑 → 3 < 4 )
87 12 33 readdcld ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℝ )
88 12 ltp1d ⊢ ( 𝜑 → 𝑁 < ( 𝑁 + 1 ) )
89 11 12 87 4 88 lelttrd ⊢ ( 𝜑 → 4 < ( 𝑁 + 1 ) )
90 86 89 jca ⊢ ( 𝜑 → ( 3 < 4 ∧ 4 < ( 𝑁 + 1 ) ) )
91 9 rexrd ⊢ ( 𝜑 → 3 ∈ ℝ* )
92 87 rexrd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℝ* )
93 11 rexrd ⊢ ( 𝜑 → 4 ∈ ℝ* )
94 elioo5 ⊢ ( ( 3 ∈ ℝ* ∧ ( 𝑁 + 1 ) ∈ ℝ* ∧ 4 ∈ ℝ* ) → ( 4 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↔ ( 3 < 4 ∧ 4 < ( 𝑁 + 1 ) ) ) )
95 91 92 93 94 syl3anc ⊢ ( 𝜑 → ( 4 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↔ ( 3 < 4 ∧ 4 < ( 𝑁 + 1 ) ) ) )
96 90 95 mpbird ⊢ ( 𝜑 → 4 ∈ ( 3 (,) ( 𝑁 + 1 ) ) )
97 9 11 12 86 4 ltletrd ⊢ ( 𝜑 → 3 < 𝑁 )
98 97 88 jca ⊢ ( 𝜑 → ( 3 < 𝑁 ∧ 𝑁 < ( 𝑁 + 1 ) ) )
99 12 rexrd ⊢ ( 𝜑 → 𝑁 ∈ ℝ* )
100 elioo5 ⊢ ( ( 3 ∈ ℝ* ∧ ( 𝑁 + 1 ) ∈ ℝ* ∧ 𝑁 ∈ ℝ* ) → ( 𝑁 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↔ ( 3 < 𝑁 ∧ 𝑁 < ( 𝑁 + 1 ) ) ) )
101 91 92 99 100 syl3anc ⊢ ( 𝜑 → ( 𝑁 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↔ ( 3 < 𝑁 ∧ 𝑁 < ( 𝑁 + 1 ) ) ) )
102 98 101 mpbird ⊢ ( 𝜑 → 𝑁 ∈ ( 3 (,) ( 𝑁 + 1 ) ) )
103 iccssioo2 ⊢ ( ( 4 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ∧ 𝑁 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( 4 [,] 𝑁 ) ⊆ ( 3 (,) ( 𝑁 + 1 ) ) )
104 96 102 103 syl2anc ⊢ ( 𝜑 → ( 4 [,] 𝑁 ) ⊆ ( 3 (,) ( 𝑁 + 1 ) ) )
105 104 resmptd ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) ) ↾ ( 4 [,] 𝑁 ) ) = ( 𝑥 ∈ ( 4 [,] 𝑁 ) ↦ ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) ) )
106 2cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 2 ∈ ℂ )
107 17 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 2 ∈ ℝ )
108 19 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 0 < 2 )
109 elioore ⊢ ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) → 𝑥 ∈ ℝ )
110 109 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 𝑥 ∈ ℝ )
111 0red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 0 ∈ ℝ )
112 8 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 3 ∈ ℝ )
113 3pos ⊢ 0 < 3
114 113 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 0 < 3 )
115 eliooord ⊢ ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) → ( 3 < 𝑥 ∧ 𝑥 < ( 𝑁 + 1 ) ) )
116 simpl ⊢ ( ( 3 < 𝑥 ∧ 𝑥 < ( 𝑁 + 1 ) ) → 3 < 𝑥 )
117 115 116 syl ⊢ ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) → 3 < 𝑥 )
118 117 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 3 < 𝑥 )
119 111 112 110 114 118 lttrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 0 < 𝑥 )
120 37 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 2 ≠ 1 )
121 107 108 110 119 120 relogbcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( 2 logb 𝑥 ) ∈ ℝ )
122 40 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 5 ∈ ℕ0 )
123 121 122 reexpcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( ( 2 logb 𝑥 ) ↑ 5 ) ∈ ℝ )
124 1red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 1 ∈ ℝ )
125 123 124 readdcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ∈ ℝ )
126 111 124 readdcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( 0 + 1 ) ∈ ℝ )
127 111 ltp1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 0 < ( 0 + 1 ) )
128 122 nn0zd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 5 ∈ ℤ )
129 34 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 1 < 2 )
130 2lt3 ⊢ 2 < 3
131 130 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 2 < 3 )
132 124 107 112 129 131 lttrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 1 < 3 )
133 124 112 110 132 118 lttrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 1 < 𝑥 )
134 110 119 elrpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 𝑥 ∈ ℝ+ )
135 2rp ⊢ 2 ∈ ℝ+
136 135 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 2 ∈ ℝ+ )
137 134 136 129 jca32 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( 𝑥 ∈ ℝ+ ∧ ( 2 ∈ ℝ+ ∧ 1 < 2 ) ) )
138 logbgt0b ⊢ ( ( 𝑥 ∈ ℝ+ ∧ ( 2 ∈ ℝ+ ∧ 1 < 2 ) ) → ( 0 < ( 2 logb 𝑥 ) ↔ 1 < 𝑥 ) )
139 137 138 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( 0 < ( 2 logb 𝑥 ) ↔ 1 < 𝑥 ) )
140 133 139 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 0 < ( 2 logb 𝑥 ) )
141 121 128 140 66 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 0 < ( ( 2 logb 𝑥 ) ↑ 5 ) )
142 111 123 124 141 ltadd1dd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( 0 + 1 ) < ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) )
143 111 126 125 127 142 lttrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 0 < ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) )
144 124 129 ltned ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 1 ≠ 2 )
145 144 necomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 2 ≠ 1 )
146 107 108 125 143 145 relogbcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ∈ ℝ )
147 146 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ∈ ℂ )
148 106 147 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) ∈ ℂ )
149 48 121 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( 2 logb 𝑥 ) ∈ ℂ )
150 149 sqcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( ( 2 logb 𝑥 ) ↑ 2 ) ∈ ℂ )
151 148 150 addcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) ∈ ℂ )
152 151 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) ) : ( 3 (,) ( 𝑁 + 1 ) ) ⟶ ℂ )
153 ioossre ⊢ ( 3 (,) ( 𝑁 + 1 ) ) ⊆ ℝ
154 153 a1i ⊢ ( 𝜑 → ( 3 (,) ( 𝑁 + 1 ) ) ⊆ ℝ )
155 84 152 154 3jca ⊢ ( 𝜑 → ( ℝ ⊆ ℂ ∧ ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) ) : ( 3 (,) ( 𝑁 + 1 ) ) ⟶ ℂ ∧ ( 3 (,) ( 𝑁 + 1 ) ) ⊆ ℝ ) )
156 136 relogcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( log ‘ 2 ) ∈ ℝ )
157 125 156 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) ∈ ℝ )
158 48 123 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( ( 2 logb 𝑥 ) ↑ 5 ) ∈ ℂ )
159 1cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 1 ∈ ℂ )
160 158 159 addcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ∈ ℂ )
161 111 108 gtned ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 2 ≠ 0 )
162 106 161 logcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( log ‘ 2 ) ∈ ℂ )
163 111 143 gtned ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ≠ 0 )
164 loggt0b ⊢ ( 2 ∈ ℝ+ → ( 0 < ( log ‘ 2 ) ↔ 1 < 2 ) )
165 135 164 ax-mp ⊢ ( 0 < ( log ‘ 2 ) ↔ 1 < 2 )
166 35 165 sylibr ⊢ ( 𝜑 → 0 < ( log ‘ 2 ) )
167 26 166 ltned ⊢ ( 𝜑 → 0 ≠ ( log ‘ 2 ) )
168 167 necomd ⊢ ( 𝜑 → ( log ‘ 2 ) ≠ 0 )
169 168 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( log ‘ 2 ) ≠ 0 )
170 160 162 163 169 mulne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) ≠ 0 )
171 124 157 170 redivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( 1 / ( ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) ) ∈ ℝ )
172 5re ⊢ 5 ∈ ℝ
173 172 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 5 ∈ ℝ )
174 4nn0 ⊢ 4 ∈ ℕ0
175 174 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 4 ∈ ℕ0 )
176 121 175 reexpcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( ( 2 logb 𝑥 ) ↑ 4 ) ∈ ℝ )
177 173 176 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( 5 · ( ( 2 logb 𝑥 ) ↑ 4 ) ) ∈ ℝ )
178 110 156 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( 𝑥 · ( log ‘ 2 ) ) ∈ ℝ )
179 48 110 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 𝑥 ∈ ℂ )
180 111 119 gtned ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 𝑥 ≠ 0 )
181 179 162 180 169 mulne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( 𝑥 · ( log ‘ 2 ) ) ≠ 0 )
182 124 178 181 redivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) ∈ ℝ )
183 177 182 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( ( 5 · ( ( 2 logb 𝑥 ) ↑ 4 ) ) · ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) ) ∈ ℝ )
184 183 111 readdcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( ( ( 5 · ( ( 2 logb 𝑥 ) ↑ 4 ) ) · ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) ) + 0 ) ∈ ℝ )
185 171 184 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( ( 1 / ( ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( ( 5 · ( ( 2 logb 𝑥 ) ↑ 4 ) ) · ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) ) + 0 ) ) ∈ ℝ )
186 107 185 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( 2 · ( ( 1 / ( ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( ( 5 · ( ( 2 logb 𝑥 ) ↑ 4 ) ) · ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) ) + 0 ) ) ) ∈ ℝ )
187 156 resqcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( ( log ‘ 2 ) ↑ 2 ) ∈ ℝ )
188 56 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 2 ∈ ℤ )
189 162 169 188 expne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( ( log ‘ 2 ) ↑ 2 ) ≠ 0 )
190 107 187 189 redivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) ∈ ℝ )
191 134 relogcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( log ‘ 𝑥 ) ∈ ℝ )
192 2m1e1 ⊢ ( 2 − 1 ) = 1
193 1nn0 ⊢ 1 ∈ ℕ0
194 192 193 eqeltri ⊢ ( 2 − 1 ) ∈ ℕ0
195 194 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( 2 − 1 ) ∈ ℕ0 )
196 191 195 reexpcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( ( log ‘ 𝑥 ) ↑ ( 2 − 1 ) ) ∈ ℝ )
197 196 110 180 redivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( ( ( log ‘ 𝑥 ) ↑ ( 2 − 1 ) ) / 𝑥 ) ∈ ℝ )
198 190 197 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) · ( ( ( log ‘ 𝑥 ) ↑ ( 2 − 1 ) ) / 𝑥 ) ) ∈ ℝ )
199 186 198 readdcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( ( 2 · ( ( 1 / ( ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( ( 5 · ( ( 2 logb 𝑥 ) ↑ 4 ) ) · ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) ) + 0 ) ) ) + ( ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) · ( ( ( log ‘ 𝑥 ) ↑ ( 2 − 1 ) ) / 𝑥 ) ) ) ∈ ℝ )
200 199 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ( ( 2 · ( ( 1 / ( ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( ( 5 · ( ( 2 logb 𝑥 ) ↑ 4 ) ) · ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) ) + 0 ) ) ) + ( ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) · ( ( ( log ‘ 𝑥 ) ↑ ( 2 − 1 ) ) / 𝑥 ) ) ) ∈ ℝ )
201 nfcv ⊢ Ⅎ 𝑥 ( 3 (,) ( 𝑁 + 1 ) )
202 201 fnmptf ⊢ ( ∀ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ( ( 2 · ( ( 1 / ( ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( ( 5 · ( ( 2 logb 𝑥 ) ↑ 4 ) ) · ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) ) + 0 ) ) ) + ( ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) · ( ( ( log ‘ 𝑥 ) ↑ ( 2 − 1 ) ) / 𝑥 ) ) ) ∈ ℝ → ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 · ( ( 1 / ( ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( ( 5 · ( ( 2 logb 𝑥 ) ↑ 4 ) ) · ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) ) + 0 ) ) ) + ( ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) · ( ( ( log ‘ 𝑥 ) ↑ ( 2 − 1 ) ) / 𝑥 ) ) ) ) Fn ( 3 (,) ( 𝑁 + 1 ) ) )
203 200 202 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 · ( ( 1 / ( ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( ( 5 · ( ( 2 logb 𝑥 ) ↑ 4 ) ) · ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) ) + 0 ) ) ) + ( ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) · ( ( ( log ‘ 𝑥 ) ↑ ( 2 − 1 ) ) / 𝑥 ) ) ) ) Fn ( 3 (,) ( 𝑁 + 1 ) ) )
204 9 leidd ⊢ ( 𝜑 → 3 ≤ 3 )
205 12 lep1d ⊢ ( 𝜑 → 𝑁 ≤ ( 𝑁 + 1 ) )
206 9 12 87 16 205 letrd ⊢ ( 𝜑 → 3 ≤ ( 𝑁 + 1 ) )
207 9 87 204 206 aks4d1p1p6 ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) ) ) = ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 · ( ( 1 / ( ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( ( 5 · ( ( 2 logb 𝑥 ) ↑ 4 ) ) · ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) ) + 0 ) ) ) + ( ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) · ( ( ( log ‘ 𝑥 ) ↑ ( 2 − 1 ) ) / 𝑥 ) ) ) ) )
208 207 fneq1d ⊢ ( 𝜑 → ( ( ℝ D ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) ) ) Fn ( 3 (,) ( 𝑁 + 1 ) ) ↔ ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 · ( ( 1 / ( ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( ( 5 · ( ( 2 logb 𝑥 ) ↑ 4 ) ) · ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) ) + 0 ) ) ) + ( ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) · ( ( ( log ‘ 𝑥 ) ↑ ( 2 − 1 ) ) / 𝑥 ) ) ) ) Fn ( 3 (,) ( 𝑁 + 1 ) ) ) )
209 203 208 mpbird ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) ) ) Fn ( 3 (,) ( 𝑁 + 1 ) ) )
210 209 fndmd ⊢ ( 𝜑 → dom ( ℝ D ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) ) ) = ( 3 (,) ( 𝑁 + 1 ) ) )
211 dvcn ⊢ ( ( ( ℝ ⊆ ℂ ∧ ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) ) : ( 3 (,) ( 𝑁 + 1 ) ) ⟶ ℂ ∧ ( 3 (,) ( 𝑁 + 1 ) ) ⊆ ℝ ) ∧ dom ( ℝ D ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) ) ) = ( 3 (,) ( 𝑁 + 1 ) ) ) → ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) ) ∈ ( ( 3 (,) ( 𝑁 + 1 ) ) –cn→ ℂ ) )
212 155 210 211 syl2anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) ) ∈ ( ( 3 (,) ( 𝑁 + 1 ) ) –cn→ ℂ ) )
213 rescncf ⊢ ( ( 4 [,] 𝑁 ) ⊆ ( 3 (,) ( 𝑁 + 1 ) ) → ( ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) ) ∈ ( ( 3 (,) ( 𝑁 + 1 ) ) –cn→ ℂ ) → ( ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) ) ↾ ( 4 [,] 𝑁 ) ) ∈ ( ( 4 [,] 𝑁 ) –cn→ ℂ ) ) )
214 104 213 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) ) ∈ ( ( 3 (,) ( 𝑁 + 1 ) ) –cn→ ℂ ) → ( ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) ) ↾ ( 4 [,] 𝑁 ) ) ∈ ( ( 4 [,] 𝑁 ) –cn→ ℂ ) ) )
215 212 214 mpd ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) ) ↾ ( 4 [,] 𝑁 ) ) ∈ ( ( 4 [,] 𝑁 ) –cn→ ℂ ) )
216 105 215 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 4 [,] 𝑁 ) ↦ ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) ) ∈ ( ( 4 [,] 𝑁 ) –cn→ ℂ ) )
217 cncffvrn ⊢ ( ( ℝ ⊆ ℂ ∧ ( 𝑥 ∈ ( 4 [,] 𝑁 ) ↦ ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) ) ∈ ( ( 4 [,] 𝑁 ) –cn→ ℂ ) ) → ( ( 𝑥 ∈ ( 4 [,] 𝑁 ) ↦ ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) ) ∈ ( ( 4 [,] 𝑁 ) –cn→ ℝ ) ↔ ( 𝑥 ∈ ( 4 [,] 𝑁 ) ↦ ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) ) : ( 4 [,] 𝑁 ) ⟶ ℝ ) )
218 84 216 217 syl2anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 4 [,] 𝑁 ) ↦ ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) ) ∈ ( ( 4 [,] 𝑁 ) –cn→ ℝ ) ↔ ( 𝑥 ∈ ( 4 [,] 𝑁 ) ↦ ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) ) : ( 4 [,] 𝑁 ) ⟶ ℝ ) )
219 83 218 mpbird ⊢ ( 𝜑 → ( 𝑥 ∈ ( 4 [,] 𝑁 ) ↦ ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) ) ∈ ( ( 4 [,] 𝑁 ) –cn→ ℝ ) )
220 174 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → 4 ∈ ℕ0 )
221 39 220 reexpcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 [,] 𝑁 ) ) → ( ( 2 logb 𝑥 ) ↑ 4 ) ∈ ℝ )
222 221 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 4 [,] 𝑁 ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) ) : ( 4 [,] 𝑁 ) ⟶ ℝ )
223 104 resmptd ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) ) ↾ ( 4 [,] 𝑁 ) ) = ( 𝑥 ∈ ( 4 [,] 𝑁 ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) ) )
224 48 176 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( ( 2 logb 𝑥 ) ↑ 4 ) ∈ ℂ )
225 224 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) ) : ( 3 (,) ( 𝑁 + 1 ) ) ⟶ ℂ )
226 84 225 154 3jca ⊢ ( 𝜑 → ( ℝ ⊆ ℂ ∧ ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) ) : ( 3 (,) ( 𝑁 + 1 ) ) ⟶ ℂ ∧ ( 3 (,) ( 𝑁 + 1 ) ) ⊆ ℝ ) )
227 10 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 4 ∈ ℝ )
228 156 175 reexpcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( ( log ‘ 2 ) ↑ 4 ) ∈ ℝ )
229 4z ⊢ 4 ∈ ℤ
230 229 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → 4 ∈ ℤ )
231 162 169 230 expne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( ( log ‘ 2 ) ↑ 4 ) ≠ 0 )
232 227 228 231 redivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( 4 / ( ( log ‘ 2 ) ↑ 4 ) ) ∈ ℝ )
233 4m1e3 ⊢ ( 4 − 1 ) = 3
234 3nn0 ⊢ 3 ∈ ℕ0
235 233 234 eqeltri ⊢ ( 4 − 1 ) ∈ ℕ0
236 235 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( 4 − 1 ) ∈ ℕ0 )
237 191 236 reexpcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( ( log ‘ 𝑥 ) ↑ ( 4 − 1 ) ) ∈ ℝ )
238 237 110 180 redivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( ( ( log ‘ 𝑥 ) ↑ ( 4 − 1 ) ) / 𝑥 ) ∈ ℝ )
239 232 238 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ) → ( ( 4 / ( ( log ‘ 2 ) ↑ 4 ) ) · ( ( ( log ‘ 𝑥 ) ↑ ( 4 − 1 ) ) / 𝑥 ) ) ∈ ℝ )
240 239 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ( ( 4 / ( ( log ‘ 2 ) ↑ 4 ) ) · ( ( ( log ‘ 𝑥 ) ↑ ( 4 − 1 ) ) / 𝑥 ) ) ∈ ℝ )
241 201 fnmptf ⊢ ( ∀ 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ( ( 4 / ( ( log ‘ 2 ) ↑ 4 ) ) · ( ( ( log ‘ 𝑥 ) ↑ ( 4 − 1 ) ) / 𝑥 ) ) ∈ ℝ → ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 4 / ( ( log ‘ 2 ) ↑ 4 ) ) · ( ( ( log ‘ 𝑥 ) ↑ ( 4 − 1 ) ) / 𝑥 ) ) ) Fn ( 3 (,) ( 𝑁 + 1 ) ) )
242 240 241 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 4 / ( ( log ‘ 2 ) ↑ 4 ) ) · ( ( ( log ‘ 𝑥 ) ↑ ( 4 − 1 ) ) / 𝑥 ) ) ) Fn ( 3 (,) ( 𝑁 + 1 ) ) )
243 113 a1i ⊢ ( 𝜑 → 0 < 3 )
244 eqid ⊢ ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) ) = ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) )
245 eqid ⊢ ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 4 / ( ( log ‘ 2 ) ↑ 4 ) ) · ( ( ( log ‘ 𝑥 ) ↑ ( 4 − 1 ) ) / 𝑥 ) ) ) = ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 4 / ( ( log ‘ 2 ) ↑ 4 ) ) · ( ( ( log ‘ 𝑥 ) ↑ ( 4 − 1 ) ) / 𝑥 ) ) )
246 eqid ⊢ ( 4 / ( ( log ‘ 2 ) ↑ 4 ) ) = ( 4 / ( ( log ‘ 2 ) ↑ 4 ) )
247 4nn ⊢ 4 ∈ ℕ
248 247 a1i ⊢ ( 𝜑 → 4 ∈ ℕ )
249 9 87 243 206 244 245 246 248 dvrelogpow2b ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) ) ) = ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 4 / ( ( log ‘ 2 ) ↑ 4 ) ) · ( ( ( log ‘ 𝑥 ) ↑ ( 4 − 1 ) ) / 𝑥 ) ) ) )
250 249 fneq1d ⊢ ( 𝜑 → ( ( ℝ D ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) ) ) Fn ( 3 (,) ( 𝑁 + 1 ) ) ↔ ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 4 / ( ( log ‘ 2 ) ↑ 4 ) ) · ( ( ( log ‘ 𝑥 ) ↑ ( 4 − 1 ) ) / 𝑥 ) ) ) Fn ( 3 (,) ( 𝑁 + 1 ) ) ) )
251 242 250 mpbird ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) ) ) Fn ( 3 (,) ( 𝑁 + 1 ) ) )
252 251 fndmd ⊢ ( 𝜑 → dom ( ℝ D ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) ) ) = ( 3 (,) ( 𝑁 + 1 ) ) )
253 dvcn ⊢ ( ( ( ℝ ⊆ ℂ ∧ ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) ) : ( 3 (,) ( 𝑁 + 1 ) ) ⟶ ℂ ∧ ( 3 (,) ( 𝑁 + 1 ) ) ⊆ ℝ ) ∧ dom ( ℝ D ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) ) ) = ( 3 (,) ( 𝑁 + 1 ) ) ) → ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) ) ∈ ( ( 3 (,) ( 𝑁 + 1 ) ) –cn→ ℂ ) )
254 226 252 253 syl2anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) ) ∈ ( ( 3 (,) ( 𝑁 + 1 ) ) –cn→ ℂ ) )
255 rescncf ⊢ ( ( 4 [,] 𝑁 ) ⊆ ( 3 (,) ( 𝑁 + 1 ) ) → ( ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) ) ∈ ( ( 3 (,) ( 𝑁 + 1 ) ) –cn→ ℂ ) → ( ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) ) ↾ ( 4 [,] 𝑁 ) ) ∈ ( ( 4 [,] 𝑁 ) –cn→ ℂ ) ) )
256 104 255 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) ) ∈ ( ( 3 (,) ( 𝑁 + 1 ) ) –cn→ ℂ ) → ( ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) ) ↾ ( 4 [,] 𝑁 ) ) ∈ ( ( 4 [,] 𝑁 ) –cn→ ℂ ) ) )
257 254 256 mpd ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 3 (,) ( 𝑁 + 1 ) ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) ) ↾ ( 4 [,] 𝑁 ) ) ∈ ( ( 4 [,] 𝑁 ) –cn→ ℂ ) )
258 223 257 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 4 [,] 𝑁 ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) ) ∈ ( ( 4 [,] 𝑁 ) –cn→ ℂ ) )
259 cncffvrn ⊢ ( ( ℝ ⊆ ℂ ∧ ( 𝑥 ∈ ( 4 [,] 𝑁 ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) ) ∈ ( ( 4 [,] 𝑁 ) –cn→ ℂ ) ) → ( ( 𝑥 ∈ ( 4 [,] 𝑁 ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) ) ∈ ( ( 4 [,] 𝑁 ) –cn→ ℝ ) ↔ ( 𝑥 ∈ ( 4 [,] 𝑁 ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) ) : ( 4 [,] 𝑁 ) ⟶ ℝ ) )
260 84 258 259 syl2anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 4 [,] 𝑁 ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) ) ∈ ( ( 4 [,] 𝑁 ) –cn→ ℝ ) ↔ ( 𝑥 ∈ ( 4 [,] 𝑁 ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) ) : ( 4 [,] 𝑁 ) ⟶ ℝ ) )
261 222 260 mpbird ⊢ ( 𝜑 → ( 𝑥 ∈ ( 4 [,] 𝑁 ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) ) ∈ ( ( 4 [,] 𝑁 ) –cn→ ℝ ) )
262 11 12 15 4 aks4d1p1p6 ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 4 (,) 𝑁 ) ↦ ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) ) ) = ( 𝑥 ∈ ( 4 (,) 𝑁 ) ↦ ( ( 2 · ( ( 1 / ( ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( ( 5 · ( ( 2 logb 𝑥 ) ↑ 4 ) ) · ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) ) + 0 ) ) ) + ( ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) · ( ( ( log ‘ 𝑥 ) ↑ ( 2 − 1 ) ) / 𝑥 ) ) ) ) )
263 29 a1i ⊢ ( 𝜑 → 0 < 4 )
264 eqid ⊢ ( 𝑥 ∈ ( 4 (,) 𝑁 ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) ) = ( 𝑥 ∈ ( 4 (,) 𝑁 ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) )
265 eqid ⊢ ( 𝑥 ∈ ( 4 (,) 𝑁 ) ↦ ( ( 4 / ( ( log ‘ 2 ) ↑ 4 ) ) · ( ( ( log ‘ 𝑥 ) ↑ ( 4 − 1 ) ) / 𝑥 ) ) ) = ( 𝑥 ∈ ( 4 (,) 𝑁 ) ↦ ( ( 4 / ( ( log ‘ 2 ) ↑ 4 ) ) · ( ( ( log ‘ 𝑥 ) ↑ ( 4 − 1 ) ) / 𝑥 ) ) )
266 11 12 263 4 264 265 246 248 dvrelogpow2b ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 4 (,) 𝑁 ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) ) ) = ( 𝑥 ∈ ( 4 (,) 𝑁 ) ↦ ( ( 4 / ( ( log ‘ 2 ) ↑ 4 ) ) · ( ( ( log ‘ 𝑥 ) ↑ ( 4 − 1 ) ) / 𝑥 ) ) ) )
267 233 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 (,) 𝑁 ) ) → ( 4 − 1 ) = 3 )
268 267 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 (,) 𝑁 ) ) → ( ( log ‘ 𝑥 ) ↑ ( 4 − 1 ) ) = ( ( log ‘ 𝑥 ) ↑ 3 ) )
269 268 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 (,) 𝑁 ) ) → ( ( ( log ‘ 𝑥 ) ↑ ( 4 − 1 ) ) / 𝑥 ) = ( ( ( log ‘ 𝑥 ) ↑ 3 ) / 𝑥 ) )
270 269 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 (,) 𝑁 ) ) → ( ( 4 / ( ( log ‘ 2 ) ↑ 4 ) ) · ( ( ( log ‘ 𝑥 ) ↑ ( 4 − 1 ) ) / 𝑥 ) ) = ( ( 4 / ( ( log ‘ 2 ) ↑ 4 ) ) · ( ( ( log ‘ 𝑥 ) ↑ 3 ) / 𝑥 ) ) )
271 270 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 4 (,) 𝑁 ) ↦ ( ( 4 / ( ( log ‘ 2 ) ↑ 4 ) ) · ( ( ( log ‘ 𝑥 ) ↑ ( 4 − 1 ) ) / 𝑥 ) ) ) = ( 𝑥 ∈ ( 4 (,) 𝑁 ) ↦ ( ( 4 / ( ( log ‘ 2 ) ↑ 4 ) ) · ( ( ( log ‘ 𝑥 ) ↑ 3 ) / 𝑥 ) ) ) )
272 266 271 eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 4 (,) 𝑁 ) ↦ ( ( 2 logb 𝑥 ) ↑ 4 ) ) ) = ( 𝑥 ∈ ( 4 (,) 𝑁 ) ↦ ( ( 4 / ( ( log ‘ 2 ) ↑ 4 ) ) · ( ( ( log ‘ 𝑥 ) ↑ 3 ) / 𝑥 ) ) ) )
273 elioore ⊢ ( 𝑥 ∈ ( 4 (,) 𝑁 ) → 𝑥 ∈ ℝ )
274 273 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 (,) 𝑁 ) ) → 𝑥 ∈ ℝ )
275 10 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 (,) 𝑁 ) ) → 4 ∈ ℝ )
276 eliooord ⊢ ( 𝑥 ∈ ( 4 (,) 𝑁 ) → ( 4 < 𝑥 ∧ 𝑥 < 𝑁 ) )
277 276 simpld ⊢ ( 𝑥 ∈ ( 4 (,) 𝑁 ) → 4 < 𝑥 )
278 277 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 (,) 𝑁 ) ) → 4 < 𝑥 )
279 275 274 278 ltled ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 (,) 𝑁 ) ) → 4 ≤ 𝑥 )
280 274 279 aks4d1p1p7 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 4 (,) 𝑁 ) ) → ( ( 2 · ( ( 1 / ( ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( ( 5 · ( ( 2 logb 𝑥 ) ↑ 4 ) ) · ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) ) + 0 ) ) ) + ( ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) · ( ( ( log ‘ 𝑥 ) ↑ ( 2 − 1 ) ) / 𝑥 ) ) ) ≤ ( ( 4 / ( ( log ‘ 2 ) ↑ 4 ) ) · ( ( ( log ‘ 𝑥 ) ↑ 3 ) / 𝑥 ) ) )
281 oveq2 ⊢ ( 𝑥 = 4 → ( 2 logb 𝑥 ) = ( 2 logb 4 ) )
282 281 oveq1d ⊢ ( 𝑥 = 4 → ( ( 2 logb 𝑥 ) ↑ 5 ) = ( ( 2 logb 4 ) ↑ 5 ) )
283 282 oveq1d ⊢ ( 𝑥 = 4 → ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) = ( ( ( 2 logb 4 ) ↑ 5 ) + 1 ) )
284 283 oveq2d ⊢ ( 𝑥 = 4 → ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) = ( 2 logb ( ( ( 2 logb 4 ) ↑ 5 ) + 1 ) ) )
285 284 oveq2d ⊢ ( 𝑥 = 4 → ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) = ( 2 · ( 2 logb ( ( ( 2 logb 4 ) ↑ 5 ) + 1 ) ) ) )
286 281 oveq1d ⊢ ( 𝑥 = 4 → ( ( 2 logb 𝑥 ) ↑ 2 ) = ( ( 2 logb 4 ) ↑ 2 ) )
287 285 286 oveq12d ⊢ ( 𝑥 = 4 → ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) = ( ( 2 · ( 2 logb ( ( ( 2 logb 4 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 4 ) ↑ 2 ) ) )
288 281 oveq1d ⊢ ( 𝑥 = 4 → ( ( 2 logb 𝑥 ) ↑ 4 ) = ( ( 2 logb 4 ) ↑ 4 ) )
289 oveq2 ⊢ ( 𝑥 = 𝑁 → ( 2 logb 𝑥 ) = ( 2 logb 𝑁 ) )
290 289 oveq1d ⊢ ( 𝑥 = 𝑁 → ( ( 2 logb 𝑥 ) ↑ 5 ) = ( ( 2 logb 𝑁 ) ↑ 5 ) )
291 290 oveq1d ⊢ ( 𝑥 = 𝑁 → ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) = ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) )
292 291 oveq2d ⊢ ( 𝑥 = 𝑁 → ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) = ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) )
293 292 oveq2d ⊢ ( 𝑥 = 𝑁 → ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) = ( 2 · ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) )
294 5 a1i ⊢ ( 𝑥 = 𝑁 → 𝐶 = ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) )
295 294 oveq2d ⊢ ( 𝑥 = 𝑁 → ( 2 · 𝐶 ) = ( 2 · ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) )
296 295 eqcomd ⊢ ( 𝑥 = 𝑁 → ( 2 · ( 2 logb ( ( ( 2 logb 𝑁 ) ↑ 5 ) + 1 ) ) ) = ( 2 · 𝐶 ) )
297 293 296 eqtrd ⊢ ( 𝑥 = 𝑁 → ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) = ( 2 · 𝐶 ) )
298 289 oveq1d ⊢ ( 𝑥 = 𝑁 → ( ( 2 logb 𝑥 ) ↑ 2 ) = ( ( 2 logb 𝑁 ) ↑ 2 ) )
299 6 a1i ⊢ ( 𝑥 = 𝑁 → 𝐷 = ( ( 2 logb 𝑁 ) ↑ 2 ) )
300 299 eqcomd ⊢ ( 𝑥 = 𝑁 → ( ( 2 logb 𝑁 ) ↑ 2 ) = 𝐷 )
301 298 300 eqtrd ⊢ ( 𝑥 = 𝑁 → ( ( 2 logb 𝑥 ) ↑ 2 ) = 𝐷 )
302 297 301 oveq12d ⊢ ( 𝑥 = 𝑁 → ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) = ( ( 2 · 𝐶 ) + 𝐷 ) )
303 289 oveq1d ⊢ ( 𝑥 = 𝑁 → ( ( 2 logb 𝑥 ) ↑ 4 ) = ( ( 2 logb 𝑁 ) ↑ 4 ) )
304 7 a1i ⊢ ( 𝑥 = 𝑁 → 𝐸 = ( ( 2 logb 𝑁 ) ↑ 4 ) )
305 304 eqcomd ⊢ ( 𝑥 = 𝑁 → ( ( 2 logb 𝑁 ) ↑ 4 ) = 𝐸 )
306 303 305 eqtrd ⊢ ( 𝑥 = 𝑁 → ( ( 2 logb 𝑥 ) ↑ 4 ) = 𝐸 )
307 sq2 ⊢ ( 2 ↑ 2 ) = 4
308 307 oveq2i ⊢ ( 2 logb ( 2 ↑ 2 ) ) = ( 2 logb 4 )
309 308 a1i ⊢ ( 𝜑 → ( 2 logb ( 2 ↑ 2 ) ) = ( 2 logb 4 ) )
310 309 eqcomd ⊢ ( 𝜑 → ( 2 logb 4 ) = ( 2 logb ( 2 ↑ 2 ) ) )
311 135 a1i ⊢ ( 𝜑 → 2 ∈ ℝ+ )
312 56 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
313 relogbexp ⊢ ( ( 2 ∈ ℝ+ ∧ 2 ≠ 1 ∧ 2 ∈ ℤ ) → ( 2 logb ( 2 ↑ 2 ) ) = 2 )
314 311 37 312 313 syl3anc ⊢ ( 𝜑 → ( 2 logb ( 2 ↑ 2 ) ) = 2 )
315 310 314 eqtrd ⊢ ( 𝜑 → ( 2 logb 4 ) = 2 )
316 315 oveq1d ⊢ ( 𝜑 → ( ( 2 logb 4 ) ↑ 5 ) = ( 2 ↑ 5 ) )
317 316 oveq1d ⊢ ( 𝜑 → ( ( ( 2 logb 4 ) ↑ 5 ) + 1 ) = ( ( 2 ↑ 5 ) + 1 ) )
318 317 oveq2d ⊢ ( 𝜑 → ( 2 logb ( ( ( 2 logb 4 ) ↑ 5 ) + 1 ) ) = ( 2 logb ( ( 2 ↑ 5 ) + 1 ) ) )
319 17 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
320 319 leidd ⊢ ( 𝜑 → 2 ≤ 2 )
321 315 319 eqeltrd ⊢ ( 𝜑 → ( 2 logb 4 ) ∈ ℝ )
322 40 a1i ⊢ ( 𝜑 → 5 ∈ ℕ0 )
323 321 322 reexpcld ⊢ ( 𝜑 → ( ( 2 logb 4 ) ↑ 5 ) ∈ ℝ )
324 316 323 eqeltrrd ⊢ ( 𝜑 → ( 2 ↑ 5 ) ∈ ℝ )
325 324 33 readdcld ⊢ ( 𝜑 → ( ( 2 ↑ 5 ) + 1 ) ∈ ℝ )
326 322 nn0zd ⊢ ( 𝜑 → 5 ∈ ℤ )
327 19 a1i ⊢ ( 𝜑 → 0 < 2 )
328 327 315 breqtrrd ⊢ ( 𝜑 → 0 < ( 2 logb 4 ) )
329 321 326 328 3jca ⊢ ( 𝜑 → ( ( 2 logb 4 ) ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < ( 2 logb 4 ) ) )
330 expgt0 ⊢ ( ( ( 2 logb 4 ) ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < ( 2 logb 4 ) ) → 0 < ( ( 2 logb 4 ) ↑ 5 ) )
331 329 330 syl ⊢ ( 𝜑 → 0 < ( ( 2 logb 4 ) ↑ 5 ) )
332 331 316 breqtrd ⊢ ( 𝜑 → 0 < ( 2 ↑ 5 ) )
333 324 ltp1d ⊢ ( 𝜑 → ( 2 ↑ 5 ) < ( ( 2 ↑ 5 ) + 1 ) )
334 26 324 325 332 333 lttrd ⊢ ( 𝜑 → 0 < ( ( 2 ↑ 5 ) + 1 ) )
335 6nn0 ⊢ 6 ∈ ℕ0
336 335 a1i ⊢ ( 𝜑 → 6 ∈ ℕ0 )
337 319 336 reexpcld ⊢ ( 𝜑 → ( 2 ↑ 6 ) ∈ ℝ )
338 336 nn0zd ⊢ ( 𝜑 → 6 ∈ ℤ )
339 expgt0 ⊢ ( ( 2 ∈ ℝ ∧ 6 ∈ ℤ ∧ 0 < 2 ) → 0 < ( 2 ↑ 6 ) )
340 319 338 327 339 syl3anc ⊢ ( 𝜑 → 0 < ( 2 ↑ 6 ) )
341 324 324 readdcld ⊢ ( 𝜑 → ( ( 2 ↑ 5 ) + ( 2 ↑ 5 ) ) ∈ ℝ )
342 33 319 35 ltled ⊢ ( 𝜑 → 1 ≤ 2 )
343 319 322 342 expge1d ⊢ ( 𝜑 → 1 ≤ ( 2 ↑ 5 ) )
344 33 324 324 343 leadd2dd ⊢ ( 𝜑 → ( ( 2 ↑ 5 ) + 1 ) ≤ ( ( 2 ↑ 5 ) + ( 2 ↑ 5 ) ) )
345 341 leidd ⊢ ( 𝜑 → ( ( 2 ↑ 5 ) + ( 2 ↑ 5 ) ) ≤ ( ( 2 ↑ 5 ) + ( 2 ↑ 5 ) ) )
346 df-6 ⊢ 6 = ( 5 + 1 )
347 346 a1i ⊢ ( 𝜑 → 6 = ( 5 + 1 ) )
348 347 oveq2d ⊢ ( 𝜑 → ( 2 ↑ 6 ) = ( 2 ↑ ( 5 + 1 ) ) )
349 2cn ⊢ 2 ∈ ℂ
350 349 a1i ⊢ ( 𝜑 → 2 ∈ ℂ )
351 193 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
352 350 351 322 expaddd ⊢ ( 𝜑 → ( 2 ↑ ( 5 + 1 ) ) = ( ( 2 ↑ 5 ) · ( 2 ↑ 1 ) ) )
353 348 352 eqtrd ⊢ ( 𝜑 → ( 2 ↑ 6 ) = ( ( 2 ↑ 5 ) · ( 2 ↑ 1 ) ) )
354 350 exp1d ⊢ ( 𝜑 → ( 2 ↑ 1 ) = 2 )
355 354 oveq2d ⊢ ( 𝜑 → ( ( 2 ↑ 5 ) · ( 2 ↑ 1 ) ) = ( ( 2 ↑ 5 ) · 2 ) )
356 353 355 eqtrd ⊢ ( 𝜑 → ( 2 ↑ 6 ) = ( ( 2 ↑ 5 ) · 2 ) )
357 48 324 sselid ⊢ ( 𝜑 → ( 2 ↑ 5 ) ∈ ℂ )
358 357 times2d ⊢ ( 𝜑 → ( ( 2 ↑ 5 ) · 2 ) = ( ( 2 ↑ 5 ) + ( 2 ↑ 5 ) ) )
359 356 358 eqtrd ⊢ ( 𝜑 → ( 2 ↑ 6 ) = ( ( 2 ↑ 5 ) + ( 2 ↑ 5 ) ) )
360 359 eqcomd ⊢ ( 𝜑 → ( ( 2 ↑ 5 ) + ( 2 ↑ 5 ) ) = ( 2 ↑ 6 ) )
361 345 360 breqtrd ⊢ ( 𝜑 → ( ( 2 ↑ 5 ) + ( 2 ↑ 5 ) ) ≤ ( 2 ↑ 6 ) )
362 325 341 337 344 361 letrd ⊢ ( 𝜑 → ( ( 2 ↑ 5 ) + 1 ) ≤ ( 2 ↑ 6 ) )
363 312 320 325 334 337 340 362 logblebd ⊢ ( 𝜑 → ( 2 logb ( ( 2 ↑ 5 ) + 1 ) ) ≤ ( 2 logb ( 2 ↑ 6 ) ) )
364 311 37 338 relogbexpd ⊢ ( 𝜑 → ( 2 logb ( 2 ↑ 6 ) ) = 6 )
365 363 364 breqtrd ⊢ ( 𝜑 → ( 2 logb ( ( 2 ↑ 5 ) + 1 ) ) ≤ 6 )
366 318 365 eqbrtrd ⊢ ( 𝜑 → ( 2 logb ( ( ( 2 logb 4 ) ↑ 5 ) + 1 ) ) ≤ 6 )
367 6t2e12 ⊢ ( 6 · 2 ) = 1 2
368 6cn ⊢ 6 ∈ ℂ
369 368 a1i ⊢ ( 𝜑 → 6 ∈ ℂ )
370 2nn ⊢ 2 ∈ ℕ
371 193 370 decnncl ⊢ 1 2 ∈ ℕ
372 371 a1i ⊢ ( 𝜑 → 1 2 ∈ ℕ )
373 372 nnred ⊢ ( 𝜑 → 1 2 ∈ ℝ )
374 373 recnd ⊢ ( 𝜑 → 1 2 ∈ ℂ )
375 26 327 gtned ⊢ ( 𝜑 → 2 ≠ 0 )
376 369 350 374 375 ldiv ⊢ ( 𝜑 → ( ( 6 · 2 ) = 1 2 ↔ 6 = ( 1 2 / 2 ) ) )
377 367 376 mpbii ⊢ ( 𝜑 → 6 = ( 1 2 / 2 ) )
378 366 377 breqtrd ⊢ ( 𝜑 → ( 2 logb ( ( ( 2 logb 4 ) ↑ 5 ) + 1 ) ) ≤ ( 1 2 / 2 ) )
379 323 33 readdcld ⊢ ( 𝜑 → ( ( ( 2 logb 4 ) ↑ 5 ) + 1 ) ∈ ℝ )
380 26 33 readdcld ⊢ ( 𝜑 → ( 0 + 1 ) ∈ ℝ )
381 26 ltp1d ⊢ ( 𝜑 → 0 < ( 0 + 1 ) )
382 26 323 33 331 ltadd1dd ⊢ ( 𝜑 → ( 0 + 1 ) < ( ( ( 2 logb 4 ) ↑ 5 ) + 1 ) )
383 26 380 379 381 382 lttrd ⊢ ( 𝜑 → 0 < ( ( ( 2 logb 4 ) ↑ 5 ) + 1 ) )
384 319 327 379 383 37 relogbcld ⊢ ( 𝜑 → ( 2 logb ( ( ( 2 logb 4 ) ↑ 5 ) + 1 ) ) ∈ ℝ )
385 384 373 311 lemuldiv2d ⊢ ( 𝜑 → ( ( 2 · ( 2 logb ( ( ( 2 logb 4 ) ↑ 5 ) + 1 ) ) ) ≤ 1 2 ↔ ( 2 logb ( ( ( 2 logb 4 ) ↑ 5 ) + 1 ) ) ≤ ( 1 2 / 2 ) ) )
386 378 385 mpbird ⊢ ( 𝜑 → ( 2 · ( 2 logb ( ( ( 2 logb 4 ) ↑ 5 ) + 1 ) ) ) ≤ 1 2 )
387 315 oveq1d ⊢ ( 𝜑 → ( ( 2 logb 4 ) ↑ 2 ) = ( 2 ↑ 2 ) )
388 387 307 eqtrdi ⊢ ( 𝜑 → ( ( 2 logb 4 ) ↑ 2 ) = 4 )
389 388 oveq2d ⊢ ( 𝜑 → ( 1 6 − ( ( 2 logb 4 ) ↑ 2 ) ) = ( 1 6 − 4 ) )
390 2nn0 ⊢ 2 ∈ ℕ0
391 eqid ⊢ 1 2 = 1 2
392 4cn ⊢ 4 ∈ ℂ
393 4p2e6 ⊢ ( 4 + 2 ) = 6
394 392 349 393 addcomli ⊢ ( 2 + 4 ) = 6
395 193 390 174 391 394 decaddi ⊢ ( 1 2 + 4 ) = 1 6
396 392 a1i ⊢ ( 𝜑 → 4 ∈ ℂ )
397 6nn ⊢ 6 ∈ ℕ
398 193 397 decnncl ⊢ 1 6 ∈ ℕ
399 398 a1i ⊢ ( 𝜑 → 1 6 ∈ ℕ )
400 399 nnred ⊢ ( 𝜑 → 1 6 ∈ ℝ )
401 48 400 sselid ⊢ ( 𝜑 → 1 6 ∈ ℂ )
402 374 396 401 addlsub ⊢ ( 𝜑 → ( ( 1 2 + 4 ) = 1 6 ↔ 1 2 = ( 1 6 − 4 ) ) )
403 395 402 mpbii ⊢ ( 𝜑 → 1 2 = ( 1 6 − 4 ) )
404 389 403 eqtr4d ⊢ ( 𝜑 → ( 1 6 − ( ( 2 logb 4 ) ↑ 2 ) ) = 1 2 )
405 404 eqcomd ⊢ ( 𝜑 → 1 2 = ( 1 6 − ( ( 2 logb 4 ) ↑ 2 ) ) )
406 386 405 breqtrd ⊢ ( 𝜑 → ( 2 · ( 2 logb ( ( ( 2 logb 4 ) ↑ 5 ) + 1 ) ) ) ≤ ( 1 6 − ( ( 2 logb 4 ) ↑ 2 ) ) )
407 319 384 remulcld ⊢ ( 𝜑 → ( 2 · ( 2 logb ( ( ( 2 logb 4 ) ↑ 5 ) + 1 ) ) ) ∈ ℝ )
408 321 resqcld ⊢ ( 𝜑 → ( ( 2 logb 4 ) ↑ 2 ) ∈ ℝ )
409 leaddsub ⊢ ( ( ( 2 · ( 2 logb ( ( ( 2 logb 4 ) ↑ 5 ) + 1 ) ) ) ∈ ℝ ∧ ( ( 2 logb 4 ) ↑ 2 ) ∈ ℝ ∧ 1 6 ∈ ℝ ) → ( ( ( 2 · ( 2 logb ( ( ( 2 logb 4 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 4 ) ↑ 2 ) ) ≤ 1 6 ↔ ( 2 · ( 2 logb ( ( ( 2 logb 4 ) ↑ 5 ) + 1 ) ) ) ≤ ( 1 6 − ( ( 2 logb 4 ) ↑ 2 ) ) ) )
410 407 408 400 409 syl3anc ⊢ ( 𝜑 → ( ( ( 2 · ( 2 logb ( ( ( 2 logb 4 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 4 ) ↑ 2 ) ) ≤ 1 6 ↔ ( 2 · ( 2 logb ( ( ( 2 logb 4 ) ↑ 5 ) + 1 ) ) ) ≤ ( 1 6 − ( ( 2 logb 4 ) ↑ 2 ) ) ) )
411 406 410 mpbird ⊢ ( 𝜑 → ( ( 2 · ( 2 logb ( ( ( 2 logb 4 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 4 ) ↑ 2 ) ) ≤ 1 6 )
412 315 oveq1d ⊢ ( 𝜑 → ( ( 2 logb 4 ) ↑ 4 ) = ( 2 ↑ 4 ) )
413 2exp4 ⊢ ( 2 ↑ 4 ) = 1 6
414 412 413 eqtrdi ⊢ ( 𝜑 → ( ( 2 logb 4 ) ↑ 4 ) = 1 6 )
415 414 eqcomd ⊢ ( 𝜑 → 1 6 = ( ( 2 logb 4 ) ↑ 4 ) )
416 411 415 breqtrd ⊢ ( 𝜑 → ( ( 2 · ( 2 logb ( ( ( 2 logb 4 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 4 ) ↑ 2 ) ) ≤ ( ( 2 logb 4 ) ↑ 4 ) )
417 11 12 219 261 262 272 280 287 288 302 306 416 4 dvle2 ⊢ ( 𝜑 → ( ( 2 · 𝐶 ) + 𝐷 ) ≤ 𝐸 )
418 1 2 3 16 5 6 7 417 aks4d1p1p4 ⊢ ( 𝜑 → 𝐴 < ( 2 ↑ 𝐵 ) )