Theorem pntlemh

Description: Lemma for pnt . Bounds on the subintervals in the induction. (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	pntlemh	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑋 < ( 𝐾 ↑ 𝐽 ) ∧ ( 𝐾 ↑ 𝐽 ) ≤ ( √ ‘ 𝑍 ) ) )

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	adantr	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑋 ∈ ℝ+ )
20	19	relogcld	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( log ‘ 𝑋 ) ∈ ℝ )
21	1 2 3 4 5 6 7 8 9 10	pntlemc	⊢ ( 𝜑 → ( 𝐸 ∈ ℝ+ ∧ 𝐾 ∈ ℝ+ ∧ ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈 − 𝐸 ) ∈ ℝ+ ) ) )
22	21	simp2d	⊢ ( 𝜑 → 𝐾 ∈ ℝ+ )
23	22	rpred	⊢ ( 𝜑 → 𝐾 ∈ ℝ )
24	21	simp3d	⊢ ( 𝜑 → ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈 − 𝐸 ) ∈ ℝ+ ) )
25	24	simp2d	⊢ ( 𝜑 → 1 < 𝐾 )
26	23 25	rplogcld	⊢ ( 𝜑 → ( log ‘ 𝐾 ) ∈ ℝ+ )
27	26	adantr	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( log ‘ 𝐾 ) ∈ ℝ+ )
28	20 27	rerpdivcld	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ∈ ℝ )
29	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	pntlemg	⊢ ( 𝜑 → ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ≤ ( 𝑁 − 𝑀 ) ) )
30	29	simp1d	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
31	30	adantr	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑀 ∈ ℕ )
32	31	nnred	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑀 ∈ ℝ )
33		elfzuz	⊢ ( 𝐽 ∈ ( 𝑀 ... 𝑁 ) → 𝐽 ∈ ( ℤ≥ ‘ 𝑀 ) )
34		eluznn	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝐽 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝐽 ∈ ℕ )
35	30 33 34	syl2an	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐽 ∈ ℕ )
36	35	nnred	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐽 ∈ ℝ )
37		flltp1	⊢ ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ∈ ℝ → ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) < ( ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) + 1 ) )
38	28 37	syl	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) < ( ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) + 1 ) )
39	38 16	breqtrrdi	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) < 𝑀 )
40		elfzle1	⊢ ( 𝐽 ∈ ( 𝑀 ... 𝑁 ) → 𝑀 ≤ 𝐽 )
41	40	adantl	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑀 ≤ 𝐽 )
42	28 32 36 39 41	ltletrd	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) < 𝐽 )
43	20 36 27	ltdivmul2d	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) < 𝐽 ↔ ( log ‘ 𝑋 ) < ( 𝐽 · ( log ‘ 𝐾 ) ) ) )
44	42 43	mpbid	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( log ‘ 𝑋 ) < ( 𝐽 · ( log ‘ 𝐾 ) ) )
45	22	adantr	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐾 ∈ ℝ+ )
46		elfzelz	⊢ ( 𝐽 ∈ ( 𝑀 ... 𝑁 ) → 𝐽 ∈ ℤ )
47	46	adantl	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐽 ∈ ℤ )
48		relogexp	⊢ ( ( 𝐾 ∈ ℝ+ ∧ 𝐽 ∈ ℤ ) → ( log ‘ ( 𝐾 ↑ 𝐽 ) ) = ( 𝐽 · ( log ‘ 𝐾 ) ) )
49	45 47 48	syl2anc	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( log ‘ ( 𝐾 ↑ 𝐽 ) ) = ( 𝐽 · ( log ‘ 𝐾 ) ) )
50	44 49	breqtrrd	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( log ‘ 𝑋 ) < ( log ‘ ( 𝐾 ↑ 𝐽 ) ) )
51	45 47	rpexpcld	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐾 ↑ 𝐽 ) ∈ ℝ+ )
52		logltb	⊢ ( ( 𝑋 ∈ ℝ+ ∧ ( 𝐾 ↑ 𝐽 ) ∈ ℝ+ ) → ( 𝑋 < ( 𝐾 ↑ 𝐽 ) ↔ ( log ‘ 𝑋 ) < ( log ‘ ( 𝐾 ↑ 𝐽 ) ) ) )
53	19 51 52	syl2anc	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑋 < ( 𝐾 ↑ 𝐽 ) ↔ ( log ‘ 𝑋 ) < ( log ‘ ( 𝐾 ↑ 𝐽 ) ) ) )
54	50 53	mpbird	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑋 < ( 𝐾 ↑ 𝐽 ) )
55	49	oveq2d	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( 2 · ( log ‘ ( 𝐾 ↑ 𝐽 ) ) ) = ( 2 · ( 𝐽 · ( log ‘ 𝐾 ) ) ) )
56		2z	⊢ 2 ∈ ℤ
57		relogexp	⊢ ( ( ( 𝐾 ↑ 𝐽 ) ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( log ‘ ( ( 𝐾 ↑ 𝐽 ) ↑ 2 ) ) = ( 2 · ( log ‘ ( 𝐾 ↑ 𝐽 ) ) ) )
58	51 56 57	sylancl	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( log ‘ ( ( 𝐾 ↑ 𝐽 ) ↑ 2 ) ) = ( 2 · ( log ‘ ( 𝐾 ↑ 𝐽 ) ) ) )
59		2cnd	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → 2 ∈ ℂ )
60	36	recnd	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐽 ∈ ℂ )
61	45	relogcld	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( log ‘ 𝐾 ) ∈ ℝ )
62	61	recnd	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( log ‘ 𝐾 ) ∈ ℂ )
63	59 60 62	mulassd	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 2 · 𝐽 ) · ( log ‘ 𝐾 ) ) = ( 2 · ( 𝐽 · ( log ‘ 𝐾 ) ) ) )
64	55 58 63	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( log ‘ ( ( 𝐾 ↑ 𝐽 ) ↑ 2 ) ) = ( ( 2 · 𝐽 ) · ( log ‘ 𝐾 ) ) )
65		elfzle2	⊢ ( 𝐽 ∈ ( 𝑀 ... 𝑁 ) → 𝐽 ≤ 𝑁 )
66	65	adantl	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐽 ≤ 𝑁 )
67	66 17	breqtrdi	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐽 ≤ ( ⌊ ‘ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) ) )
68	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 ‘ 𝑍 ) ) ) ) )
69	68	simp1d	⊢ ( 𝜑 → 𝑍 ∈ ℝ+ )
70	69	adantr	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑍 ∈ ℝ+ )
71	70	relogcld	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( log ‘ 𝑍 ) ∈ ℝ )
72	71 27	rerpdivcld	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) ∈ ℝ )
73	72	rehalfcld	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) ∈ ℝ )
74		flge	⊢ ( ( ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) ∈ ℝ ∧ 𝐽 ∈ ℤ ) → ( 𝐽 ≤ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) ↔ 𝐽 ≤ ( ⌊ ‘ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) ) ) )
75	73 47 74	syl2anc	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐽 ≤ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) ↔ 𝐽 ≤ ( ⌊ ‘ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) ) ) )
76	67 75	mpbird	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐽 ≤ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) )
77		2re	⊢ 2 ∈ ℝ
78	77	a1i	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → 2 ∈ ℝ )
79		2pos	⊢ 0 < 2
80	79	a1i	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → 0 < 2 )
81		lemuldiv2	⊢ ( ( 𝐽 ∈ ℝ ∧ ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 2 · 𝐽 ) ≤ ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) ↔ 𝐽 ≤ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) ) )
82	36 72 78 80 81	syl112anc	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 2 · 𝐽 ) ≤ ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) ↔ 𝐽 ≤ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) ) )
83	76 82	mpbird	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( 2 · 𝐽 ) ≤ ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) )
84		remulcl	⊢ ( ( 2 ∈ ℝ ∧ 𝐽 ∈ ℝ ) → ( 2 · 𝐽 ) ∈ ℝ )
85	77 36 84	sylancr	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( 2 · 𝐽 ) ∈ ℝ )
86	85 71 27	lemuldivd	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( ( 2 · 𝐽 ) · ( log ‘ 𝐾 ) ) ≤ ( log ‘ 𝑍 ) ↔ ( 2 · 𝐽 ) ≤ ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) ) )
87	83 86	mpbird	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 2 · 𝐽 ) · ( log ‘ 𝐾 ) ) ≤ ( log ‘ 𝑍 ) )
88	64 87	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( log ‘ ( ( 𝐾 ↑ 𝐽 ) ↑ 2 ) ) ≤ ( log ‘ 𝑍 ) )
89		rpexpcl	⊢ ( ( ( 𝐾 ↑ 𝐽 ) ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( ( 𝐾 ↑ 𝐽 ) ↑ 2 ) ∈ ℝ+ )
90	51 56 89	sylancl	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝐾 ↑ 𝐽 ) ↑ 2 ) ∈ ℝ+ )
91	90 70	logled	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( ( 𝐾 ↑ 𝐽 ) ↑ 2 ) ≤ 𝑍 ↔ ( log ‘ ( ( 𝐾 ↑ 𝐽 ) ↑ 2 ) ) ≤ ( log ‘ 𝑍 ) ) )
92	88 91	mpbird	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝐾 ↑ 𝐽 ) ↑ 2 ) ≤ 𝑍 )
93	70	rprege0d	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑍 ∈ ℝ ∧ 0 ≤ 𝑍 ) )
94		resqrtth	⊢ ( ( 𝑍 ∈ ℝ ∧ 0 ≤ 𝑍 ) → ( ( √ ‘ 𝑍 ) ↑ 2 ) = 𝑍 )
95	93 94	syl	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( √ ‘ 𝑍 ) ↑ 2 ) = 𝑍 )
96	92 95	breqtrrd	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝐾 ↑ 𝐽 ) ↑ 2 ) ≤ ( ( √ ‘ 𝑍 ) ↑ 2 ) )
97	51	rprege0d	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝐾 ↑ 𝐽 ) ∈ ℝ ∧ 0 ≤ ( 𝐾 ↑ 𝐽 ) ) )
98	70	rpsqrtcld	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( √ ‘ 𝑍 ) ∈ ℝ+ )
99	98	rprege0d	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( √ ‘ 𝑍 ) ∈ ℝ ∧ 0 ≤ ( √ ‘ 𝑍 ) ) )
100		le2sq	⊢ ( ( ( ( 𝐾 ↑ 𝐽 ) ∈ ℝ ∧ 0 ≤ ( 𝐾 ↑ 𝐽 ) ) ∧ ( ( √ ‘ 𝑍 ) ∈ ℝ ∧ 0 ≤ ( √ ‘ 𝑍 ) ) ) → ( ( 𝐾 ↑ 𝐽 ) ≤ ( √ ‘ 𝑍 ) ↔ ( ( 𝐾 ↑ 𝐽 ) ↑ 2 ) ≤ ( ( √ ‘ 𝑍 ) ↑ 2 ) ) )
101	97 99 100	syl2anc	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝐾 ↑ 𝐽 ) ≤ ( √ ‘ 𝑍 ) ↔ ( ( 𝐾 ↑ 𝐽 ) ↑ 2 ) ≤ ( ( √ ‘ 𝑍 ) ↑ 2 ) ) )
102	96 101	mpbird	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐾 ↑ 𝐽 ) ≤ ( √ ‘ 𝑍 ) )
103	54 102	jca	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑋 < ( 𝐾 ↑ 𝐽 ) ∧ ( 𝐾 ↑ 𝐽 ) ≤ ( √ ‘ 𝑍 ) ) )