Metamath Proof Explorer


Theorem gpg3kgrtriexlem3

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

Ref Expression
Hypothesis gpg3kgrtriex.n N = 3 K
Assertion gpg3kgrtriexlem3 K N 3

Proof

Step Hyp Ref Expression
1 gpg3kgrtriex.n N = 3 K
2 3z 3
3 2 a1i K 3
4 nnz K K
5 3 4 zmulcld K 3 K
6 3t1e3 3 1 = 3
7 nnge1 K 1 K
8 1re 1
9 nnre K K
10 3re 3
11 3pos 0 < 3
12 10 11 pm3.2i 3 0 < 3
13 12 a1i K 3 0 < 3
14 lemul2 1 K 3 0 < 3 1 K 3 1 3 K
15 8 9 13 14 mp3an2i K 1 K 3 1 3 K
16 7 15 mpbid K 3 1 3 K
17 6 16 eqbrtrrid K 3 3 K
18 eluz2 3 K 3 3 3 K 3 3 K
19 3 5 17 18 syl3anbrc K 3 K 3
20 1 19 eqeltrid K N 3