Theorem jm3.1lem1

Description: Lemma for jm3.1 . (Contributed by Stefan O'Rear, 16-Oct-2014)

	Ref	Expression
Hypotheses	jm3.1.a	⊢ ( 𝜑 → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
	jm3.1.b	⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 2 ) )
	jm3.1.c	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	jm3.1.d	⊢ ( 𝜑 → ( 𝐾 Yrm ( 𝑁 + 1 ) ) ≤ 𝐴 )
Assertion	jm3.1lem1	⊢ ( 𝜑 → ( 𝐾 ↑ 𝑁 ) < 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		jm3.1.a	⊢ ( 𝜑 → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
2		jm3.1.b	⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 2 ) )
3		jm3.1.c	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4		jm3.1.d	⊢ ( 𝜑 → ( 𝐾 Yrm ( 𝑁 + 1 ) ) ≤ 𝐴 )
5		eluzelre	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) → 𝐾 ∈ ℝ )
6	2 5	syl	⊢ ( 𝜑 → 𝐾 ∈ ℝ )
7	3	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
8	6 7	reexpcld	⊢ ( 𝜑 → ( 𝐾 ↑ 𝑁 ) ∈ ℝ )
9		2z	⊢ 2 ∈ ℤ
10		uzid	⊢ ( 2 ∈ ℤ → 2 ∈ ( ℤ≥ ‘ 2 ) )
11	9 10	ax-mp	⊢ 2 ∈ ( ℤ≥ ‘ 2 )
12		uz2mulcl	⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) → ( 2 · 𝐾 ) ∈ ( ℤ≥ ‘ 2 ) )
13	11 2 12	sylancr	⊢ ( 𝜑 → ( 2 · 𝐾 ) ∈ ( ℤ≥ ‘ 2 ) )
14		uz2m1nn	⊢ ( ( 2 · 𝐾 ) ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 · 𝐾 ) − 1 ) ∈ ℕ )
15	13 14	syl	⊢ ( 𝜑 → ( ( 2 · 𝐾 ) − 1 ) ∈ ℕ )
16	15	nnred	⊢ ( 𝜑 → ( ( 2 · 𝐾 ) − 1 ) ∈ ℝ )
17	16 7	reexpcld	⊢ ( 𝜑 → ( ( ( 2 · 𝐾 ) − 1 ) ↑ 𝑁 ) ∈ ℝ )
18		eluzelre	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℝ )
19	1 18	syl	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
20		uz2m1nn	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐾 − 1 ) ∈ ℕ )
21	2 20	syl	⊢ ( 𝜑 → ( 𝐾 − 1 ) ∈ ℕ )
22	21	nngt0d	⊢ ( 𝜑 → 0 < ( 𝐾 − 1 ) )
23		2cn	⊢ 2 ∈ ℂ
24	6	recnd	⊢ ( 𝜑 → 𝐾 ∈ ℂ )
25		mulcl	⊢ ( ( 2 ∈ ℂ ∧ 𝐾 ∈ ℂ ) → ( 2 · 𝐾 ) ∈ ℂ )
26	23 24 25	sylancr	⊢ ( 𝜑 → ( 2 · 𝐾 ) ∈ ℂ )
27		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
28	26 27 24	sub32d	⊢ ( 𝜑 → ( ( ( 2 · 𝐾 ) − 1 ) − 𝐾 ) = ( ( ( 2 · 𝐾 ) − 𝐾 ) − 1 ) )
29	24	2timesd	⊢ ( 𝜑 → ( 2 · 𝐾 ) = ( 𝐾 + 𝐾 ) )
30	24 24 29	mvrladdd	⊢ ( 𝜑 → ( ( 2 · 𝐾 ) − 𝐾 ) = 𝐾 )
31	30	oveq1d	⊢ ( 𝜑 → ( ( ( 2 · 𝐾 ) − 𝐾 ) − 1 ) = ( 𝐾 − 1 ) )
32	28 31	eqtrd	⊢ ( 𝜑 → ( ( ( 2 · 𝐾 ) − 1 ) − 𝐾 ) = ( 𝐾 − 1 ) )
33	22 32	breqtrrd	⊢ ( 𝜑 → 0 < ( ( ( 2 · 𝐾 ) − 1 ) − 𝐾 ) )
34	6 16	posdifd	⊢ ( 𝜑 → ( 𝐾 < ( ( 2 · 𝐾 ) − 1 ) ↔ 0 < ( ( ( 2 · 𝐾 ) − 1 ) − 𝐾 ) ) )
35	33 34	mpbird	⊢ ( 𝜑 → 𝐾 < ( ( 2 · 𝐾 ) − 1 ) )
36		eluz2nn	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) → 𝐾 ∈ ℕ )
37	2 36	syl	⊢ ( 𝜑 → 𝐾 ∈ ℕ )
38	37	nnrpd	⊢ ( 𝜑 → 𝐾 ∈ ℝ+ )
39	15	nnrpd	⊢ ( 𝜑 → ( ( 2 · 𝐾 ) − 1 ) ∈ ℝ+ )
40		rpexpmord	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℝ+ ∧ ( ( 2 · 𝐾 ) − 1 ) ∈ ℝ+ ) → ( 𝐾 < ( ( 2 · 𝐾 ) − 1 ) ↔ ( 𝐾 ↑ 𝑁 ) < ( ( ( 2 · 𝐾 ) − 1 ) ↑ 𝑁 ) ) )
41	3 38 39 40	syl3anc	⊢ ( 𝜑 → ( 𝐾 < ( ( 2 · 𝐾 ) − 1 ) ↔ ( 𝐾 ↑ 𝑁 ) < ( ( ( 2 · 𝐾 ) − 1 ) ↑ 𝑁 ) ) )
42	35 41	mpbid	⊢ ( 𝜑 → ( 𝐾 ↑ 𝑁 ) < ( ( ( 2 · 𝐾 ) − 1 ) ↑ 𝑁 ) )
43	3	nnzd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
44	43	peano2zd	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℤ )
45		frmy	⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
46	45	fovcl	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 + 1 ) ∈ ℤ ) → ( 𝐾 Yrm ( 𝑁 + 1 ) ) ∈ ℤ )
47	2 44 46	syl2anc	⊢ ( 𝜑 → ( 𝐾 Yrm ( 𝑁 + 1 ) ) ∈ ℤ )
48	47	zred	⊢ ( 𝜑 → ( 𝐾 Yrm ( 𝑁 + 1 ) ) ∈ ℝ )
49		jm2.17a	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 2 · 𝐾 ) − 1 ) ↑ 𝑁 ) ≤ ( 𝐾 Yrm ( 𝑁 + 1 ) ) )
50	2 7 49	syl2anc	⊢ ( 𝜑 → ( ( ( 2 · 𝐾 ) − 1 ) ↑ 𝑁 ) ≤ ( 𝐾 Yrm ( 𝑁 + 1 ) ) )
51	17 48 19 50 4	letrd	⊢ ( 𝜑 → ( ( ( 2 · 𝐾 ) − 1 ) ↑ 𝑁 ) ≤ 𝐴 )
52	8 17 19 42 51	ltletrd	⊢ ( 𝜑 → ( 𝐾 ↑ 𝑁 ) < 𝐴 )