Metamath Proof Explorer

Theorem 2lgslem1a2

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

Ref Expression
Assertion 2lgslem1a2 ( ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) < 𝐼 ↔ ( 𝑁 / 2 ) < ( 𝐼 · 2 ) ) )

Proof

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