Metamath Proof Explorer

Theorem gpg3kgrtriexlem1

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

Ref Expression
Assertion gpg3kgrtriexlem1 
|- ( K e. NN -> K < ( |^ ` ( ( 3 x. K ) / 2 ) ) )

Proof

Step Hyp Ref Expression
1 nnre 
 |-  ( K e. NN -> K e. RR )
2 3re 
 |-  3 e. RR
3 2 a1i 
 |-  ( K e. NN -> 3 e. RR )
4 3 1 remulcld 
 |-  ( K e. NN -> ( 3 x. K ) e. RR )
5 4 rehalfcld 
 |-  ( K e. NN -> ( ( 3 x. K ) / 2 ) e. RR )
6 5 ceilcld 
 |-  ( K e. NN -> ( |^ ` ( ( 3 x. K ) / 2 ) ) e. ZZ )
7 6 zred 
 |-  ( K e. NN -> ( |^ ` ( ( 3 x. K ) / 2 ) ) e. RR )
8 2re 
 |-  2 e. RR
9 8 a1i 
 |-  ( K e. NN -> 2 e. RR )
10 nnrp 
 |-  ( K e. NN -> K e. RR+ )
11 2lt3 
 |-  2 < 3
12 11 a1i 
 |-  ( K e. NN -> 2 < 3 )
13 9 3 10 12 ltmul1dd 
 |-  ( K e. NN -> ( 2 x. K ) < ( 3 x. K ) )
14 2pos 
 |-  0 < 2
15 14 a1i 
 |-  ( K e. NN -> 0 < 2 )
16 ltmuldiv2 
 |-  ( ( K e. RR /\ ( 3 x. K ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. K ) < ( 3 x. K ) <-> K < ( ( 3 x. K ) / 2 ) ) )
17 1 4 9 15 16 syl112anc 
 |-  ( K e. NN -> ( ( 2 x. K ) < ( 3 x. K ) <-> K < ( ( 3 x. K ) / 2 ) ) )
18 13 17 mpbid 
 |-  ( K e. NN -> K < ( ( 3 x. K ) / 2 ) )
19 5 ceilged 
 |-  ( K e. NN -> ( ( 3 x. K ) / 2 ) <_ ( |^ ` ( ( 3 x. K ) / 2 ) ) )
20 1 5 7 18 19 ltletrd 
 |-  ( K e. NN -> K < ( |^ ` ( ( 3 x. K ) / 2 ) ) )