Metamath Proof Explorer

Theorem 2lgslem1a2

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

Ref Expression
Assertion 2lgslem1a2 ⊢N∈ℤ∧I∈ℤ→N4<I↔N2< I⋅2

Proof

Step Hyp Ref Expression
1 zre ⊢N∈ℤ→N∈ℝ
2 1 rehalfcld ⊢N∈ℤ→N2∈ℝ
3 2 adantr ⊢N∈ℤ∧I∈ℤ→N2∈ℝ
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 ⊢N2∈ℝ∧ I⋅2∈ℝ∧2∈ℝ∧0<2→N2< I⋅2↔N22< I⋅22
15 3 9 13 14 syl3anc ⊢N∈ℤ∧I∈ℤ→N2< I⋅2↔N22< I⋅22
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→N22=N2⋅2
21 17 19 19 20 syl3anc ⊢N∈ℤ∧I∈ℤ→N22=N2⋅2
22 2t2e4 ⊢2⋅2=4
23 22 oveq2i ⊢N2⋅2=N4
24 21 23 eqtrdi ⊢N∈ℤ∧I∈ℤ→N22=N4
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⋅22=I
31 24 30 breq12d ⊢N∈ℤ∧I∈ℤ→N22< I⋅22↔N4<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∈ℤ→N4∈ℝ
37 fllt ⊢N4∈ℝ∧I∈ℤ→N4<I↔N4<I
38 36 37 sylan ⊢N∈ℤ∧I∈ℤ→N4<I↔N4<I
39 15 31 38 3bitrrd ⊢N∈ℤ∧I∈ℤ→N4<I↔N2< I⋅2