Metamath Proof Explorer


Theorem 2lgslem1a2

Description: Lemma 2 for 2lgslem1a . (Contributed by AV, 18-Jun-2021)

Ref Expression
Assertion 2lgslem1a2 N I N 4 < I N 2 < I 2

Proof

Step Hyp Ref Expression
1 zre N N
2 1 rehalfcld N N 2
3 2 adantr N I N 2
4 id I I
5 2z 2
6 5 a1i I 2
7 4 6 zmulcld I I 2
8 7 zred I I 2
9 8 adantl N I I 2
10 2re 2
11 2pos 0 < 2
12 10 11 pm3.2i 2 0 < 2
13 12 a1i N I 2 0 < 2
14 ltdiv1 N 2 I 2 2 0 < 2 N 2 < I 2 N 2 2 < I 2 2
15 3 9 13 14 syl3anc N I N 2 < I 2 N 2 2 < I 2 2
16 zcn N N
17 16 adantr N I N
18 2cnne0 2 2 0
19 18 a1i N I 2 2 0
20 divdiv1 N 2 2 0 2 2 0 N 2 2 = N 2 2
21 17 19 19 20 syl3anc N I N 2 2 = N 2 2
22 2t2e4 2 2 = 4
23 22 oveq2i N 2 2 = N 4
24 21 23 eqtrdi N I N 2 2 = N 4
25 zcn I I
26 25 adantl N I I
27 2cnd N I 2
28 2ne0 2 0
29 28 a1i N I 2 0
30 26 27 29 divcan4d N I I 2 2 = I
31 24 30 breq12d N I N 2 2 < I 2 2 N 4 < I
32 4re 4
33 32 a1i N 4
34 4ne0 4 0
35 34 a1i N 4 0
36 1 33 35 redivcld N N 4
37 fllt N 4 I N 4 < I N 4 < I
38 36 37 sylan N I N 4 < I N 4 < I
39 15 31 38 3bitrrd N I N 4 < I N 2 < I 2