Metamath Proof Explorer

Theorem pntlemg

Description: Lemma for pnt . Closure for the constants used in the proof. For comparison with Equation 10.6.27 of Shapiro, p. 434, M is j^* and N is ĵ. (Contributed by Mario Carneiro, 13-Apr-2016)

Ref Expression
Hypotheses pntlem1.r ⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
pntlem1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
pntlem1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
pntlem1.l ⊢ ( 𝜑 → 𝐿 ∈ ( 0 (,) 1 ) )
pntlem1.d ⊢ 𝐷 = ( 𝐴 + 1 )
pntlem1.f ⊢ 𝐹 = ( ( 1 − ( 1 / 𝐷 ) ) · ( ( 𝐿 / ( 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) )
pntlem1.u ⊢ ( 𝜑 → 𝑈 ∈ ℝ+ )
pntlem1.u2 ⊢ ( 𝜑 → 𝑈 ≤ 𝐴 )
pntlem1.e ⊢ 𝐸 = ( 𝑈 / 𝐷 )
pntlem1.k ⊢ 𝐾 = ( exp ‘ ( 𝐵 / 𝐸 ) )
pntlem1.y ⊢ ( 𝜑 → ( 𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌 ) )
pntlem1.x ⊢ ( 𝜑 → ( 𝑋 ∈ ℝ+ ∧ 𝑌 < 𝑋 ) )
pntlem1.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
pntlem1.w ⊢ 𝑊 = ( ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) + ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ) )
pntlem1.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑊 [,) +∞ ) )
pntlem1.m ⊢ 𝑀 = ( ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) + 1 )
pntlem1.n ⊢ 𝑁 = ( ⌊ ‘ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) )
Assertion pntlemg ( 𝜑 → ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ≤ ( 𝑁 − 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 pntlem1.r ⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
2 pntlem1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
3 pntlem1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
4 pntlem1.l ⊢ ( 𝜑 → 𝐿 ∈ ( 0 (,) 1 ) )
5 pntlem1.d ⊢ 𝐷 = ( 𝐴 + 1 )
6 pntlem1.f ⊢ 𝐹 = ( ( 1 − ( 1 / 𝐷 ) ) · ( ( 𝐿 / ( 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) )
7 pntlem1.u ⊢ ( 𝜑 → 𝑈 ∈ ℝ+ )
8 pntlem1.u2 ⊢ ( 𝜑 → 𝑈 ≤ 𝐴 )
9 pntlem1.e ⊢ 𝐸 = ( 𝑈 / 𝐷 )
10 pntlem1.k ⊢ 𝐾 = ( exp ‘ ( 𝐵 / 𝐸 ) )
11 pntlem1.y ⊢ ( 𝜑 → ( 𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌 ) )
12 pntlem1.x ⊢ ( 𝜑 → ( 𝑋 ∈ ℝ+ ∧ 𝑌 < 𝑋 ) )
13 pntlem1.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
14 pntlem1.w ⊢ 𝑊 = ( ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) + ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ) )
15 pntlem1.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑊 [,) +∞ ) )
16 pntlem1.m ⊢ 𝑀 = ( ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) + 1 )
17 pntlem1.n ⊢ 𝑁 = ( ⌊ ‘ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) )
18 12 simpld ⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
19 18 rpred ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
20 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
21 11 simpld ⊢ ( 𝜑 → 𝑌 ∈ ℝ+ )
22 21 rpred ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
23 11 simprd ⊢ ( 𝜑 → 1 ≤ 𝑌 )
24 12 simprd ⊢ ( 𝜑 → 𝑌 < 𝑋 )
25 20 22 19 23 24 lelttrd ⊢ ( 𝜑 → 1 < 𝑋 )
26 19 25 rplogcld ⊢ ( 𝜑 → ( log ‘ 𝑋 ) ∈ ℝ+ )
27 1 2 3 4 5 6 7 8 9 10 pntlemc ⊢ ( 𝜑 → ( 𝐸 ∈ ℝ+ ∧ 𝐾 ∈ ℝ+ ∧ ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈 − 𝐸 ) ∈ ℝ+ ) ) )
28 27 simp2d ⊢ ( 𝜑 → 𝐾 ∈ ℝ+ )
29 28 rpred ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
30 27 simp3d ⊢ ( 𝜑 → ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈 − 𝐸 ) ∈ ℝ+ ) )
31 30 simp2d ⊢ ( 𝜑 → 1 < 𝐾 )
32 29 31 rplogcld ⊢ ( 𝜑 → ( log ‘ 𝐾 ) ∈ ℝ+ )
33 26 32 rpdivcld ⊢ ( 𝜑 → ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ∈ ℝ+ )
34 33 rprege0d ⊢ ( 𝜑 → ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ∈ ℝ ∧ 0 ≤ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) )
35 flge0nn0 ⊢ ( ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ∈ ℝ ∧ 0 ≤ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) → ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) ∈ ℕ0 )
36 nn0p1nn ⊢ ( ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) ∈ ℕ0 → ( ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) + 1 ) ∈ ℕ )
37 34 35 36 3syl ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) + 1 ) ∈ ℕ )
38 16 37 eqeltrid ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
39 38 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
40 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 pntlemb ⊢ ( 𝜑 → ( 𝑍 ∈ ℝ+ ∧ ( 1 < 𝑍 ∧ e ≤ ( √ ‘ 𝑍 ) ∧ ( √ ‘ 𝑍 ) ≤ ( 𝑍 / 𝑌 ) ) ∧ ( ( 4 / ( 𝐿 · 𝐸 ) ) ≤ ( √ ‘ 𝑍 ) ∧ ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) + 2 ) ≤ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ∧ ( ( 𝑈 · 3 ) + 𝐶 ) ≤ ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ) )
41 40 simp1d ⊢ ( 𝜑 → 𝑍 ∈ ℝ+ )
42 41 relogcld ⊢ ( 𝜑 → ( log ‘ 𝑍 ) ∈ ℝ )
43 42 32 rerpdivcld ⊢ ( 𝜑 → ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) ∈ ℝ )
44 43 rehalfcld ⊢ ( 𝜑 → ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) ∈ ℝ )
45 44 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) ) ∈ ℤ )
46 17 45 eqeltrid ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
47 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
48 4nn ⊢ 4 ∈ ℕ
49 nndivre ⊢ ( ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) ∈ ℝ ∧ 4 ∈ ℕ ) → ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ∈ ℝ )
50 43 48 49 sylancl ⊢ ( 𝜑 → ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ∈ ℝ )
51 46 zred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
52 38 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
53 51 52 resubcld ⊢ ( 𝜑 → ( 𝑁 − 𝑀 ) ∈ ℝ )
54 41 rpred ⊢ ( 𝜑 → 𝑍 ∈ ℝ )
55 40 simp2d ⊢ ( 𝜑 → ( 1 < 𝑍 ∧ e ≤ ( √ ‘ 𝑍 ) ∧ ( √ ‘ 𝑍 ) ≤ ( 𝑍 / 𝑌 ) ) )
56 55 simp1d ⊢ ( 𝜑 → 1 < 𝑍 )
57 54 56 rplogcld ⊢ ( 𝜑 → ( log ‘ 𝑍 ) ∈ ℝ+ )
58 57 32 rpdivcld ⊢ ( 𝜑 → ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) ∈ ℝ+ )
59 4re ⊢ 4 ∈ ℝ
60 4pos ⊢ 0 < 4
61 59 60 elrpii ⊢ 4 ∈ ℝ+
62 rpdivcl ⊢ ( ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) ∈ ℝ+ ∧ 4 ∈ ℝ+ ) → ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ∈ ℝ+ )
63 58 61 62 sylancl ⊢ ( 𝜑 → ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ∈ ℝ+ )
64 63 rpge0d ⊢ ( 𝜑 → 0 ≤ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) )
65 50 recnd ⊢ ( 𝜑 → ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ∈ ℂ )
66 38 nncnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
67 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
68 65 66 67 addassd ⊢ ( 𝜑 → ( ( ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) + 𝑀 ) + 1 ) = ( ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) + ( 𝑀 + 1 ) ) )
69 52 20 readdcld ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℝ )
70 50 69 readdcld ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) + ( 𝑀 + 1 ) ) ∈ ℝ )
71 peano2re ⊢ ( 𝑁 ∈ ℝ → ( 𝑁 + 1 ) ∈ ℝ )
72 51 71 syl ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℝ )
73 33 rpred ⊢ ( 𝜑 → ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ∈ ℝ )
74 2re ⊢ 2 ∈ ℝ
75 74 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
76 73 75 readdcld ⊢ ( 𝜑 → ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) + 2 ) ∈ ℝ )
77 reflcl ⊢ ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ∈ ℝ → ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) ∈ ℝ )
78 73 77 syl ⊢ ( 𝜑 → ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) ∈ ℝ )
79 78 recnd ⊢ ( 𝜑 → ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) ∈ ℂ )
80 79 67 67 addassd ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) + 1 ) + 1 ) = ( ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) + ( 1 + 1 ) ) )
81 16 oveq1i ⊢ ( 𝑀 + 1 ) = ( ( ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) + 1 ) + 1 )
82 df-2 ⊢ 2 = ( 1 + 1 )
83 82 oveq2i ⊢ ( ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) + 2 ) = ( ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) + ( 1 + 1 ) )
84 80 81 83 3eqtr4g ⊢ ( 𝜑 → ( 𝑀 + 1 ) = ( ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) + 2 ) )
85 flle ⊢ ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ∈ ℝ → ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) ≤ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) )
86 73 85 syl ⊢ ( 𝜑 → ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) ≤ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) )
87 78 73 75 86 leadd1dd ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) + 2 ) ≤ ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) + 2 ) )
88 84 87 eqbrtrd ⊢ ( 𝜑 → ( 𝑀 + 1 ) ≤ ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) + 2 ) )
89 40 simp3d ⊢ ( 𝜑 → ( ( 4 / ( 𝐿 · 𝐸 ) ) ≤ ( √ ‘ 𝑍 ) ∧ ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) + 2 ) ≤ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ∧ ( ( 𝑈 · 3 ) + 𝐶 ) ≤ ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) )
90 89 simp2d ⊢ ( 𝜑 → ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) + 2 ) ≤ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) )
91 69 76 50 88 90 letrd ⊢ ( 𝜑 → ( 𝑀 + 1 ) ≤ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) )
92 69 50 50 91 leadd2dd ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) + ( 𝑀 + 1 ) ) ≤ ( ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) + ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ) )
93 43 recnd ⊢ ( 𝜑 → ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) ∈ ℂ )
94 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
95 2ne0 ⊢ 2 ≠ 0
96 95 a1i ⊢ ( 𝜑 → 2 ≠ 0 )
97 93 94 94 96 96 divdiv1d ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) / 2 ) = ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / ( 2 · 2 ) ) )
98 2t2e4 ⊢ ( 2 · 2 ) = 4
99 98 oveq2i ⊢ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / ( 2 · 2 ) ) = ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 )
100 97 99 eqtrdi ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) / 2 ) = ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) )
101 100 oveq2d ⊢ ( 𝜑 → ( 2 · ( ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) / 2 ) ) = ( 2 · ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ) )
102 44 recnd ⊢ ( 𝜑 → ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) ∈ ℂ )
103 102 94 96 divcan2d ⊢ ( 𝜑 → ( 2 · ( ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) / 2 ) ) = ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) )
104 65 2timesd ⊢ ( 𝜑 → ( 2 · ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ) = ( ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) + ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ) )
105 101 103 104 3eqtr3d ⊢ ( 𝜑 → ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) = ( ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) + ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ) )
106 92 105 breqtrrd ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) + ( 𝑀 + 1 ) ) ≤ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) )
107 fllep1 ⊢ ( ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) ∈ ℝ → ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) ≤ ( ( ⌊ ‘ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) ) + 1 ) )
108 44 107 syl ⊢ ( 𝜑 → ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) ≤ ( ( ⌊ ‘ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) ) + 1 ) )
109 17 oveq1i ⊢ ( 𝑁 + 1 ) = ( ( ⌊ ‘ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) ) + 1 )
110 108 109 breqtrrdi ⊢ ( 𝜑 → ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) ≤ ( 𝑁 + 1 ) )
111 70 44 72 106 110 letrd ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) + ( 𝑀 + 1 ) ) ≤ ( 𝑁 + 1 ) )
112 68 111 eqbrtrd ⊢ ( 𝜑 → ( ( ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) + 𝑀 ) + 1 ) ≤ ( 𝑁 + 1 ) )
113 50 52 readdcld ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) + 𝑀 ) ∈ ℝ )
114 113 51 20 leadd1d ⊢ ( 𝜑 → ( ( ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) + 𝑀 ) ≤ 𝑁 ↔ ( ( ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) + 𝑀 ) + 1 ) ≤ ( 𝑁 + 1 ) ) )
115 112 114 mpbird ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) + 𝑀 ) ≤ 𝑁 )
116 leaddsub ⊢ ( ( ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) + 𝑀 ) ≤ 𝑁 ↔ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ≤ ( 𝑁 − 𝑀 ) ) )
117 50 52 51 116 syl3anc ⊢ ( 𝜑 → ( ( ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) + 𝑀 ) ≤ 𝑁 ↔ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ≤ ( 𝑁 − 𝑀 ) ) )
118 115 117 mpbid ⊢ ( 𝜑 → ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ≤ ( 𝑁 − 𝑀 ) )
119 47 50 53 64 118 letrd ⊢ ( 𝜑 → 0 ≤ ( 𝑁 − 𝑀 ) )
120 51 52 subge0d ⊢ ( 𝜑 → ( 0 ≤ ( 𝑁 − 𝑀 ) ↔ 𝑀 ≤ 𝑁 ) )
121 119 120 mpbid ⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
122 eluz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) )
123 39 46 121 122 syl3anbrc ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
124 38 123 118 3jca ⊢ ( 𝜑 → ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ≤ ( 𝑁 − 𝑀 ) ) )