Metamath Proof Explorer

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 ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑋 < ( 𝐾 ↑ 𝐽 ) ∧ ( 𝐾 ↑ 𝐽 ) ≤ ( √ ‘ 𝑍 ) ) )