# Metamath Proof Explorer

## Theorem 2lgslem1a2

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

Ref Expression
Assertion 2lgslem1a2 ${⊢}\left({N}\in ℤ\wedge {I}\in ℤ\right)\to \left(⌊\frac{{N}}{4}⌋<{I}↔\frac{{N}}{2}<{I}\cdot 2\right)$

### Proof

Step Hyp Ref Expression
1 zre ${⊢}{N}\in ℤ\to {N}\in ℝ$
2 1 rehalfcld ${⊢}{N}\in ℤ\to \frac{{N}}{2}\in ℝ$
3 2 adantr ${⊢}\left({N}\in ℤ\wedge {I}\in ℤ\right)\to \frac{{N}}{2}\in ℝ$
4 id ${⊢}{I}\in ℤ\to {I}\in ℤ$
5 2z ${⊢}2\in ℤ$
6 5 a1i ${⊢}{I}\in ℤ\to 2\in ℤ$
7 4 6 zmulcld ${⊢}{I}\in ℤ\to {I}\cdot 2\in ℤ$
8 7 zred ${⊢}{I}\in ℤ\to {I}\cdot 2\in ℝ$
9 8 adantl ${⊢}\left({N}\in ℤ\wedge {I}\in ℤ\right)\to {I}\cdot 2\in ℝ$
10 2re ${⊢}2\in ℝ$
11 2pos ${⊢}0<2$
12 10 11 pm3.2i ${⊢}\left(2\in ℝ\wedge 0<2\right)$
13 12 a1i ${⊢}\left({N}\in ℤ\wedge {I}\in ℤ\right)\to \left(2\in ℝ\wedge 0<2\right)$
14 ltdiv1 ${⊢}\left(\frac{{N}}{2}\in ℝ\wedge {I}\cdot 2\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left(\frac{{N}}{2}<{I}\cdot 2↔\frac{\frac{{N}}{2}}{2}<\frac{{I}\cdot 2}{2}\right)$
15 3 9 13 14 syl3anc ${⊢}\left({N}\in ℤ\wedge {I}\in ℤ\right)\to \left(\frac{{N}}{2}<{I}\cdot 2↔\frac{\frac{{N}}{2}}{2}<\frac{{I}\cdot 2}{2}\right)$
16 zcn ${⊢}{N}\in ℤ\to {N}\in ℂ$
17 16 adantr ${⊢}\left({N}\in ℤ\wedge {I}\in ℤ\right)\to {N}\in ℂ$
18 2cnne0 ${⊢}\left(2\in ℂ\wedge 2\ne 0\right)$
19 18 a1i ${⊢}\left({N}\in ℤ\wedge {I}\in ℤ\right)\to \left(2\in ℂ\wedge 2\ne 0\right)$
20 divdiv1 ${⊢}\left({N}\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\to \frac{\frac{{N}}{2}}{2}=\frac{{N}}{2\cdot 2}$
21 17 19 19 20 syl3anc ${⊢}\left({N}\in ℤ\wedge {I}\in ℤ\right)\to \frac{\frac{{N}}{2}}{2}=\frac{{N}}{2\cdot 2}$
22 2t2e4 ${⊢}2\cdot 2=4$
23 22 oveq2i ${⊢}\frac{{N}}{2\cdot 2}=\frac{{N}}{4}$
24 21 23 eqtrdi ${⊢}\left({N}\in ℤ\wedge {I}\in ℤ\right)\to \frac{\frac{{N}}{2}}{2}=\frac{{N}}{4}$
25 zcn ${⊢}{I}\in ℤ\to {I}\in ℂ$
26 25 adantl ${⊢}\left({N}\in ℤ\wedge {I}\in ℤ\right)\to {I}\in ℂ$
27 2cnd ${⊢}\left({N}\in ℤ\wedge {I}\in ℤ\right)\to 2\in ℂ$
28 2ne0 ${⊢}2\ne 0$
29 28 a1i ${⊢}\left({N}\in ℤ\wedge {I}\in ℤ\right)\to 2\ne 0$
30 26 27 29 divcan4d ${⊢}\left({N}\in ℤ\wedge {I}\in ℤ\right)\to \frac{{I}\cdot 2}{2}={I}$
31 24 30 breq12d ${⊢}\left({N}\in ℤ\wedge {I}\in ℤ\right)\to \left(\frac{\frac{{N}}{2}}{2}<\frac{{I}\cdot 2}{2}↔\frac{{N}}{4}<{I}\right)$
32 4re ${⊢}4\in ℝ$
33 32 a1i ${⊢}{N}\in ℤ\to 4\in ℝ$
34 4ne0 ${⊢}4\ne 0$
35 34 a1i ${⊢}{N}\in ℤ\to 4\ne 0$
36 1 33 35 redivcld ${⊢}{N}\in ℤ\to \frac{{N}}{4}\in ℝ$
37 fllt ${⊢}\left(\frac{{N}}{4}\in ℝ\wedge {I}\in ℤ\right)\to \left(\frac{{N}}{4}<{I}↔⌊\frac{{N}}{4}⌋<{I}\right)$
38 36 37 sylan ${⊢}\left({N}\in ℤ\wedge {I}\in ℤ\right)\to \left(\frac{{N}}{4}<{I}↔⌊\frac{{N}}{4}⌋<{I}\right)$
39 15 31 38 3bitrrd ${⊢}\left({N}\in ℤ\wedge {I}\in ℤ\right)\to \left(⌊\frac{{N}}{4}⌋<{I}↔\frac{{N}}{2}<{I}\cdot 2\right)$