Metamath Proof Explorer

Theorem 2lgslem1a2

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

Ref Expression
Assertion 2lgslem1a2 
|- ( ( N e. ZZ /\ I e. ZZ ) -> ( ( |_ ` ( N / 4 ) ) < I <-> ( N / 2 ) < ( I x. 2 ) ) )

Proof

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