Metamath Proof Explorer

Theorem 2lgslem1c

Description: Lemma 3 for 2lgslem1 . (Contributed by AV, 19-Jun-2021)

Ref Expression
Assertion 2lgslem1c 
|- ( ( P e. Prime /\ -. 2 || P ) -> ( |_ ` ( P / 4 ) ) <_ ( ( P - 1 ) / 2 ) )

Proof

Step Hyp Ref Expression
1 prmnn 
 |-  ( P e. Prime -> P e. NN )
2 nnnn0 
 |-  ( P e. NN -> P e. NN0 )
3 oddnn02np1 
 |-  ( P e. NN0 -> ( -. 2 || P <-> E. n e. NN0 ( ( 2 x. n ) + 1 ) = P ) )
4 1 2 3 3syl 
 |-  ( P e. Prime -> ( -. 2 || P <-> E. n e. NN0 ( ( 2 x. n ) + 1 ) = P ) )
5 iftrue 
 |-  ( 2 || n -> if ( 2 || n , ( n / 2 ) , ( ( n - 1 ) / 2 ) ) = ( n / 2 ) )
6 5 adantr 
 |-  ( ( 2 || n /\ n e. NN0 ) -> if ( 2 || n , ( n / 2 ) , ( ( n - 1 ) / 2 ) ) = ( n / 2 ) )
7 2nn 
 |-  2 e. NN
8 nn0ledivnn 
 |-  ( ( n e. NN0 /\ 2 e. NN ) -> ( n / 2 ) <_ n )
9 7 8 mpan2 
 |-  ( n e. NN0 -> ( n / 2 ) <_ n )
10 9 adantl 
 |-  ( ( 2 || n /\ n e. NN0 ) -> ( n / 2 ) <_ n )
11 6 10 eqbrtrd 
 |-  ( ( 2 || n /\ n e. NN0 ) -> if ( 2 || n , ( n / 2 ) , ( ( n - 1 ) / 2 ) ) <_ n )
12 iffalse 
 |-  ( -. 2 || n -> if ( 2 || n , ( n / 2 ) , ( ( n - 1 ) / 2 ) ) = ( ( n - 1 ) / 2 ) )
13 12 adantr 
 |-  ( ( -. 2 || n /\ n e. NN0 ) -> if ( 2 || n , ( n / 2 ) , ( ( n - 1 ) / 2 ) ) = ( ( n - 1 ) / 2 ) )
14 nn0re 
 |-  ( n e. NN0 -> n e. RR )
15 peano2rem 
 |-  ( n e. RR -> ( n - 1 ) e. RR )
16 15 rehalfcld 
 |-  ( n e. RR -> ( ( n - 1 ) / 2 ) e. RR )
17 14 16 syl 
 |-  ( n e. NN0 -> ( ( n - 1 ) / 2 ) e. RR )
18 14 rehalfcld 
 |-  ( n e. NN0 -> ( n / 2 ) e. RR )
19 14 lem1d 
 |-  ( n e. NN0 -> ( n - 1 ) <_ n )
20 14 15 syl 
 |-  ( n e. NN0 -> ( n - 1 ) e. RR )
21 2re 
 |-  2 e. RR
22 2pos 
 |-  0 < 2
23 21 22 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
24 23 a1i 
 |-  ( n e. NN0 -> ( 2 e. RR /\ 0 < 2 ) )
25 lediv1 
 |-  ( ( ( n - 1 ) e. RR /\ n e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( n - 1 ) <_ n <-> ( ( n - 1 ) / 2 ) <_ ( n / 2 ) ) )
26 20 14 24 25 syl3anc 
 |-  ( n e. NN0 -> ( ( n - 1 ) <_ n <-> ( ( n - 1 ) / 2 ) <_ ( n / 2 ) ) )
27 19 26 mpbid 
 |-  ( n e. NN0 -> ( ( n - 1 ) / 2 ) <_ ( n / 2 ) )
28 17 18 14 27 9 letrd 
 |-  ( n e. NN0 -> ( ( n - 1 ) / 2 ) <_ n )
29 28 adantl 
 |-  ( ( -. 2 || n /\ n e. NN0 ) -> ( ( n - 1 ) / 2 ) <_ n )
30 13 29 eqbrtrd 
 |-  ( ( -. 2 || n /\ n e. NN0 ) -> if ( 2 || n , ( n / 2 ) , ( ( n - 1 ) / 2 ) ) <_ n )
31 11 30 pm2.61ian 
 |-  ( n e. NN0 -> if ( 2 || n , ( n / 2 ) , ( ( n - 1 ) / 2 ) ) <_ n )
32 31 ad2antlr 
 |-  ( ( ( P e. Prime /\ n e. NN0 ) /\ ( ( 2 x. n ) + 1 ) = P ) -> if ( 2 || n , ( n / 2 ) , ( ( n - 1 ) / 2 ) ) <_ n )
33 nn0z 
 |-  ( n e. NN0 -> n e. ZZ )
34 33 adantl 
 |-  ( ( P e. Prime /\ n e. NN0 ) -> n e. ZZ )
35 eqcom 
 |-  ( ( ( 2 x. n ) + 1 ) = P <-> P = ( ( 2 x. n ) + 1 ) )
36 35 biimpi 
 |-  ( ( ( 2 x. n ) + 1 ) = P -> P = ( ( 2 x. n ) + 1 ) )
37 flodddiv4 
 |-  ( ( n e. ZZ /\ P = ( ( 2 x. n ) + 1 ) ) -> ( |_ ` ( P / 4 ) ) = if ( 2 || n , ( n / 2 ) , ( ( n - 1 ) / 2 ) ) )
38 34 36 37 syl2an 
 |-  ( ( ( P e. Prime /\ n e. NN0 ) /\ ( ( 2 x. n ) + 1 ) = P ) -> ( |_ ` ( P / 4 ) ) = if ( 2 || n , ( n / 2 ) , ( ( n - 1 ) / 2 ) ) )
39 oveq1 
 |-  ( P = ( ( 2 x. n ) + 1 ) -> ( P - 1 ) = ( ( ( 2 x. n ) + 1 ) - 1 ) )
40 39 eqcoms 
 |-  ( ( ( 2 x. n ) + 1 ) = P -> ( P - 1 ) = ( ( ( 2 x. n ) + 1 ) - 1 ) )
41 40 adantl 
 |-  ( ( ( P e. Prime /\ n e. NN0 ) /\ ( ( 2 x. n ) + 1 ) = P ) -> ( P - 1 ) = ( ( ( 2 x. n ) + 1 ) - 1 ) )
42 2nn0 
 |-  2 e. NN0
43 42 a1i 
 |-  ( n e. NN0 -> 2 e. NN0 )
44 id 
 |-  ( n e. NN0 -> n e. NN0 )
45 43 44 nn0mulcld 
 |-  ( n e. NN0 -> ( 2 x. n ) e. NN0 )
46 45 nn0cnd 
 |-  ( n e. NN0 -> ( 2 x. n ) e. CC )
47 pncan1 
 |-  ( ( 2 x. n ) e. CC -> ( ( ( 2 x. n ) + 1 ) - 1 ) = ( 2 x. n ) )
48 46 47 syl 
 |-  ( n e. NN0 -> ( ( ( 2 x. n ) + 1 ) - 1 ) = ( 2 x. n ) )
49 48 ad2antlr 
 |-  ( ( ( P e. Prime /\ n e. NN0 ) /\ ( ( 2 x. n ) + 1 ) = P ) -> ( ( ( 2 x. n ) + 1 ) - 1 ) = ( 2 x. n ) )
50 41 49 eqtrd 
 |-  ( ( ( P e. Prime /\ n e. NN0 ) /\ ( ( 2 x. n ) + 1 ) = P ) -> ( P - 1 ) = ( 2 x. n ) )
51 50 oveq1d 
 |-  ( ( ( P e. Prime /\ n e. NN0 ) /\ ( ( 2 x. n ) + 1 ) = P ) -> ( ( P - 1 ) / 2 ) = ( ( 2 x. n ) / 2 ) )
52 nn0cn 
 |-  ( n e. NN0 -> n e. CC )
53 2cnd 
 |-  ( n e. NN0 -> 2 e. CC )
54 2ne0 
 |-  2 =/= 0
55 54 a1i 
 |-  ( n e. NN0 -> 2 =/= 0 )
56 52 53 55 divcan3d 
 |-  ( n e. NN0 -> ( ( 2 x. n ) / 2 ) = n )
57 56 ad2antlr 
 |-  ( ( ( P e. Prime /\ n e. NN0 ) /\ ( ( 2 x. n ) + 1 ) = P ) -> ( ( 2 x. n ) / 2 ) = n )
58 51 57 eqtrd 
 |-  ( ( ( P e. Prime /\ n e. NN0 ) /\ ( ( 2 x. n ) + 1 ) = P ) -> ( ( P - 1 ) / 2 ) = n )
59 32 38 58 3brtr4d 
 |-  ( ( ( P e. Prime /\ n e. NN0 ) /\ ( ( 2 x. n ) + 1 ) = P ) -> ( |_ ` ( P / 4 ) ) <_ ( ( P - 1 ) / 2 ) )
60 59 rexlimdva2 
 |-  ( P e. Prime -> ( E. n e. NN0 ( ( 2 x. n ) + 1 ) = P -> ( |_ ` ( P / 4 ) ) <_ ( ( P - 1 ) / 2 ) ) )
61 4 60 sylbid 
 |-  ( P e. Prime -> ( -. 2 || P -> ( |_ ` ( P / 4 ) ) <_ ( ( P - 1 ) / 2 ) ) )
62 61 imp 
 |-  ( ( P e. Prime /\ -. 2 || P ) -> ( |_ ` ( P / 4 ) ) <_ ( ( P - 1 ) / 2 ) )