Metamath Proof Explorer

Theorem gausslemma2dlem0c

Description: Auxiliary lemma 3 for gausslemma2d . (Contributed by AV, 13-Jul-2021)

Ref Expression
Hypotheses gausslemma2dlem0a.p 
|- ( ph -> P e. ( Prime \ { 2 } ) )
gausslemma2dlem0b.h 
|- H = ( ( P - 1 ) / 2 )
Assertion gausslemma2dlem0c 
|- ( ph -> ( ( ! ` H ) gcd P ) = 1 )

Proof

Step Hyp Ref Expression
1 gausslemma2dlem0a.p 
 |-  ( ph -> P e. ( Prime \ { 2 } ) )
2 gausslemma2dlem0b.h 
 |-  H = ( ( P - 1 ) / 2 )
3 eldifi 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. Prime )
4 1 3 syl 
 |-  ( ph -> P e. Prime )
5 1 2 gausslemma2dlem0b 
 |-  ( ph -> H e. NN )
6 5 nnnn0d 
 |-  ( ph -> H e. NN0 )
7 4 6 jca 
 |-  ( ph -> ( P e. Prime /\ H e. NN0 ) )
8 prmnn 
 |-  ( P e. Prime -> P e. NN )
9 nnre 
 |-  ( P e. NN -> P e. RR )
10 peano2rem 
 |-  ( P e. RR -> ( P - 1 ) e. RR )
11 9 10 syl 
 |-  ( P e. NN -> ( P - 1 ) e. RR )
12 2re 
 |-  2 e. RR
13 12 a1i 
 |-  ( P e. NN -> 2 e. RR )
14 13 9 remulcld 
 |-  ( P e. NN -> ( 2 x. P ) e. RR )
15 9 ltm1d 
 |-  ( P e. NN -> ( P - 1 ) < P )
16 nnnn0 
 |-  ( P e. NN -> P e. NN0 )
17 16 nn0ge0d 
 |-  ( P e. NN -> 0 <_ P )
18 1le2 
 |-  1 <_ 2
19 18 a1i 
 |-  ( P e. NN -> 1 <_ 2 )
20 9 13 17 19 lemulge12d 
 |-  ( P e. NN -> P <_ ( 2 x. P ) )
21 11 9 14 15 20 ltletrd 
 |-  ( P e. NN -> ( P - 1 ) < ( 2 x. P ) )
22 2pos 
 |-  0 < 2
23 12 22 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
24 23 a1i 
 |-  ( P e. NN -> ( 2 e. RR /\ 0 < 2 ) )
25 ltdivmul 
 |-  ( ( ( P - 1 ) e. RR /\ P e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( ( P - 1 ) / 2 ) < P <-> ( P - 1 ) < ( 2 x. P ) ) )
26 11 9 24 25 syl3anc 
 |-  ( P e. NN -> ( ( ( P - 1 ) / 2 ) < P <-> ( P - 1 ) < ( 2 x. P ) ) )
27 21 26 mpbird 
 |-  ( P e. NN -> ( ( P - 1 ) / 2 ) < P )
28 3 8 27 3syl 
 |-  ( P e. ( Prime \ { 2 } ) -> ( ( P - 1 ) / 2 ) < P )
29 1 28 syl 
 |-  ( ph -> ( ( P - 1 ) / 2 ) < P )
30 2 29 eqbrtrid 
 |-  ( ph -> H < P )
31 prmndvdsfaclt 
 |-  ( ( P e. Prime /\ H e. NN0 ) -> ( H < P -> -. P || ( ! ` H ) ) )
32 7 30 31 sylc 
 |-  ( ph -> -. P || ( ! ` H ) )
33 6 faccld 
 |-  ( ph -> ( ! ` H ) e. NN )
34 33 nnzd 
 |-  ( ph -> ( ! ` H ) e. ZZ )
35 nnz 
 |-  ( P e. NN -> P e. ZZ )
36 3 8 35 3syl 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. ZZ )
37 1 36 syl 
 |-  ( ph -> P e. ZZ )
38 34 37 gcdcomd 
 |-  ( ph -> ( ( ! ` H ) gcd P ) = ( P gcd ( ! ` H ) ) )
39 38 eqeq1d 
 |-  ( ph -> ( ( ( ! ` H ) gcd P ) = 1 <-> ( P gcd ( ! ` H ) ) = 1 ) )
40 coprm 
 |-  ( ( P e. Prime /\ ( ! ` H ) e. ZZ ) -> ( -. P || ( ! ` H ) <-> ( P gcd ( ! ` H ) ) = 1 ) )
41 4 34 40 syl2anc 
 |-  ( ph -> ( -. P || ( ! ` H ) <-> ( P gcd ( ! ` H ) ) = 1 ) )
42 39 41 bitr4d 
 |-  ( ph -> ( ( ( ! ` H ) gcd P ) = 1 <-> -. P || ( ! ` H ) ) )
43 32 42 mpbird 
 |-  ( ph -> ( ( ! ` H ) gcd P ) = 1 )