Theorem gpg3kgrtriexlem4

Description: Lemma 4 for gpg3kgrtriex . (Contributed by AV, 1-Oct-2025)

	Ref	Expression
Hypothesis	gpg3kgrtriex.n	|- N = ( 3 x. K )
Assertion	gpg3kgrtriexlem4	|- ( K e. NN -> K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		gpg3kgrtriex.n	|- N = ( 3 x. K )
2		id	|- ( K e. NN -> K e. NN )
3	1	oveq1i	|- ( N / 2 ) = ( ( 3 x. K ) / 2 )
4		3re	|- 3 e. RR
5	4	a1i	|- ( K e. NN -> 3 e. RR )
6		nnre	|- ( K e. NN -> K e. RR )
7	5 6	remulcld	|- ( K e. NN -> ( 3 x. K ) e. RR )
8	7	rehalfcld	|- ( K e. NN -> ( ( 3 x. K ) / 2 ) e. RR )
9	3 8	eqeltrid	|- ( K e. NN -> ( N / 2 ) e. RR )
10	9	ceilcld	|- ( K e. NN -> ( |^ ` ( N / 2 ) ) e. ZZ )
11		1red	|- ( K e. NN -> 1 e. RR )
12	1 7	eqeltrid	|- ( K e. NN -> N e. RR )
13	12	rehalfcld	|- ( K e. NN -> ( N / 2 ) e. RR )
14	13	ceilcld	|- ( K e. NN -> ( |^ ` ( N / 2 ) ) e. ZZ )
15	14	zred	|- ( K e. NN -> ( |^ ` ( N / 2 ) ) e. RR )
16		nnge1	|- ( K e. NN -> 1 <_ K )
17	8	ceilcld	|- ( K e. NN -> ( |^ ` ( ( 3 x. K ) / 2 ) ) e. ZZ )
18	17	zred	|- ( K e. NN -> ( |^ ` ( ( 3 x. K ) / 2 ) ) e. RR )
19		gpg3kgrtriexlem1	|- ( K e. NN -> K < ( |^ ` ( ( 3 x. K ) / 2 ) ) )
20	6 18 19	ltled	|- ( K e. NN -> K <_ ( |^ ` ( ( 3 x. K ) / 2 ) ) )
21	3	fveq2i	|- ( |^ ` ( N / 2 ) ) = ( |^ ` ( ( 3 x. K ) / 2 ) )
22	20 21	breqtrrdi	|- ( K e. NN -> K <_ ( |^ ` ( N / 2 ) ) )
23	11 6 15 16 22	letrd	|- ( K e. NN -> 1 <_ ( |^ ` ( N / 2 ) ) )
24		elnnz1	|- ( ( |^ ` ( N / 2 ) ) e. NN <-> ( ( |^ ` ( N / 2 ) ) e. ZZ /\ 1 <_ ( |^ ` ( N / 2 ) ) ) )
25	10 23 24	sylanbrc	|- ( K e. NN -> ( |^ ` ( N / 2 ) ) e. NN )
26	19 21	breqtrrdi	|- ( K e. NN -> K < ( |^ ` ( N / 2 ) ) )
27		elfzo1	|- ( K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) <-> ( K e. NN /\ ( |^ ` ( N / 2 ) ) e. NN /\ K < ( |^ ` ( N / 2 ) ) ) )
28	2 25 26 27	syl3anbrc	|- ( K e. NN -> K e. ( 1 ..^ ( |^ ` ( N / 2 ) ) ) )