Metamath Proof Explorer

Theorem gpg3kgrtriexlem3

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

Ref Expression
Hypothesis gpg3kgrtriex.n 
|- N = ( 3 x. K )
Assertion gpg3kgrtriexlem3 
|- ( K e. NN -> N e. ( ZZ>= ` 3 ) )

Proof

Step Hyp Ref Expression
1 gpg3kgrtriex.n 
 |-  N = ( 3 x. K )
2 3z 
 |-  3 e. ZZ
3 2 a1i 
 |-  ( K e. NN -> 3 e. ZZ )
4 nnz 
 |-  ( K e. NN -> K e. ZZ )
5 3 4 zmulcld 
 |-  ( K e. NN -> ( 3 x. K ) e. ZZ )
6 3t1e3 
 |-  ( 3 x. 1 ) = 3
7 nnge1 
 |-  ( K e. NN -> 1 <_ K )
8 1re 
 |-  1 e. RR
9 nnre 
 |-  ( K e. NN -> K e. RR )
10 3re 
 |-  3 e. RR
11 3pos 
 |-  0 < 3
12 10 11 pm3.2i 
 |-  ( 3 e. RR /\ 0 < 3 )
13 12 a1i 
 |-  ( K e. NN -> ( 3 e. RR /\ 0 < 3 ) )
14 lemul2 
 |-  ( ( 1 e. RR /\ K e. RR /\ ( 3 e. RR /\ 0 < 3 ) ) -> ( 1 <_ K <-> ( 3 x. 1 ) <_ ( 3 x. K ) ) )
15 8 9 13 14 mp3an2i 
 |-  ( K e. NN -> ( 1 <_ K <-> ( 3 x. 1 ) <_ ( 3 x. K ) ) )
16 7 15 mpbid 
 |-  ( K e. NN -> ( 3 x. 1 ) <_ ( 3 x. K ) )
17 6 16 eqbrtrrid 
 |-  ( K e. NN -> 3 <_ ( 3 x. K ) )
18 eluz2 
 |-  ( ( 3 x. K ) e. ( ZZ>= ` 3 ) <-> ( 3 e. ZZ /\ ( 3 x. K ) e. ZZ /\ 3 <_ ( 3 x. K ) ) )
19 3 5 17 18 syl3anbrc 
 |-  ( K e. NN -> ( 3 x. K ) e. ( ZZ>= ` 3 ) )
20 1 19 eqeltrid 
 |-  ( K e. NN -> N e. ( ZZ>= ` 3 ) )