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 syl6eq ⊢ 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