Metamath Proof Explorer


Theorem gpg3kgrtriexlem1

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

Ref Expression
Assertion gpg3kgrtriexlem1 K K < 3 K 2

Proof

Step Hyp Ref Expression
1 nnre K K
2 3re 3
3 2 a1i K 3
4 3 1 remulcld K 3 K
5 4 rehalfcld K 3 K 2
6 5 ceilcld K 3 K 2
7 6 zred K 3 K 2
8 2re 2
9 8 a1i K 2
10 nnrp K K +
11 2lt3 2 < 3
12 11 a1i K 2 < 3
13 9 3 10 12 ltmul1dd K 2 K < 3 K
14 2pos 0 < 2
15 14 a1i K 0 < 2
16 ltmuldiv2 K 3 K 2 0 < 2 2 K < 3 K K < 3 K 2
17 1 4 9 15 16 syl112anc K 2 K < 3 K K < 3 K 2
18 13 17 mpbid K K < 3 K 2
19 5 ceilged K 3 K 2 3 K 2
20 1 5 7 18 19 ltletrd K K < 3 K 2