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 ) ≤ ( 𝑁 − 𝑀 ) ) )