Metamath Proof Explorer

Theorem gausslemma2dlem0c

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

Ref Expression
Hypotheses gausslemma2dlem0a.p ⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
gausslemma2dlem0b.h ⊢ 𝐻 = ( ( 𝑃 − 1 ) / 2 )
Assertion gausslemma2dlem0c ( 𝜑 → ( ( ! ‘ 𝐻 ) gcd 𝑃 ) = 1 )

Proof

Step Hyp Ref Expression
1 gausslemma2dlem0a.p ⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
2 gausslemma2dlem0b.h ⊢ 𝐻 = ( ( 𝑃 − 1 ) / 2 )
3 eldifi ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℙ )
4 1 3 syl ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
5 1 2 gausslemma2dlem0b ⊢ ( 𝜑 → 𝐻 ∈ ℕ )
6 5 nnnn0d ⊢ ( 𝜑 → 𝐻 ∈ ℕ0 )
7 4 6 jca ⊢ ( 𝜑 → ( 𝑃 ∈ ℙ ∧ 𝐻 ∈ ℕ0 ) )
8 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
9 nnre ⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℝ )
10 peano2rem ⊢ ( 𝑃 ∈ ℝ → ( 𝑃 − 1 ) ∈ ℝ )
11 9 10 syl ⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℝ )
12 2re ⊢ 2 ∈ ℝ
13 12 a1i ⊢ ( 𝑃 ∈ ℕ → 2 ∈ ℝ )
14 13 9 remulcld ⊢ ( 𝑃 ∈ ℕ → ( 2 · 𝑃 ) ∈ ℝ )
15 9 ltm1d ⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) < 𝑃 )
16 nnnn0 ⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℕ0 )
17 16 nn0ge0d ⊢ ( 𝑃 ∈ ℕ → 0 ≤ 𝑃 )
18 1le2 ⊢ 1 ≤ 2
19 18 a1i ⊢ ( 𝑃 ∈ ℕ → 1 ≤ 2 )
20 9 13 17 19 lemulge12d ⊢ ( 𝑃 ∈ ℕ → 𝑃 ≤ ( 2 · 𝑃 ) )
21 11 9 14 15 20 ltletrd ⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) < ( 2 · 𝑃 ) )
22 2pos ⊢ 0 < 2
23 12 22 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
24 23 a1i ⊢ ( 𝑃 ∈ ℕ → ( 2 ∈ ℝ ∧ 0 < 2 ) )
25 ltdivmul ⊢ ( ( ( 𝑃 − 1 ) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( ( 𝑃 − 1 ) / 2 ) < 𝑃 ↔ ( 𝑃 − 1 ) < ( 2 · 𝑃 ) ) )
26 11 9 24 25 syl3anc ⊢ ( 𝑃 ∈ ℕ → ( ( ( 𝑃 − 1 ) / 2 ) < 𝑃 ↔ ( 𝑃 − 1 ) < ( 2 · 𝑃 ) ) )
27 21 26 mpbird ⊢ ( 𝑃 ∈ ℕ → ( ( 𝑃 − 1 ) / 2 ) < 𝑃 )
28 1 3 8 27 4syl ⊢ ( 𝜑 → ( ( 𝑃 − 1 ) / 2 ) < 𝑃 )
29 2 28 eqbrtrid ⊢ ( 𝜑 → 𝐻 < 𝑃 )
30 prmndvdsfaclt ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐻 ∈ ℕ0 ) → ( 𝐻 < 𝑃 → ¬ 𝑃 ∥ ( ! ‘ 𝐻 ) ) )
31 7 29 30 sylc ⊢ ( 𝜑 → ¬ 𝑃 ∥ ( ! ‘ 𝐻 ) )
32 6 faccld ⊢ ( 𝜑 → ( ! ‘ 𝐻 ) ∈ ℕ )
33 32 nnzd ⊢ ( 𝜑 → ( ! ‘ 𝐻 ) ∈ ℤ )
34 nnz ⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℤ )
35 1 3 8 34 4syl ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
36 33 35 gcdcomd ⊢ ( 𝜑 → ( ( ! ‘ 𝐻 ) gcd 𝑃 ) = ( 𝑃 gcd ( ! ‘ 𝐻 ) ) )
37 36 eqeq1d ⊢ ( 𝜑 → ( ( ( ! ‘ 𝐻 ) gcd 𝑃 ) = 1 ↔ ( 𝑃 gcd ( ! ‘ 𝐻 ) ) = 1 ) )
38 coprm ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ! ‘ 𝐻 ) ∈ ℤ ) → ( ¬ 𝑃 ∥ ( ! ‘ 𝐻 ) ↔ ( 𝑃 gcd ( ! ‘ 𝐻 ) ) = 1 ) )
39 4 33 38 syl2anc ⊢ ( 𝜑 → ( ¬ 𝑃 ∥ ( ! ‘ 𝐻 ) ↔ ( 𝑃 gcd ( ! ‘ 𝐻 ) ) = 1 ) )
40 37 39 bitr4d ⊢ ( 𝜑 → ( ( ( ! ‘ 𝐻 ) gcd 𝑃 ) = 1 ↔ ¬ 𝑃 ∥ ( ! ‘ 𝐻 ) ) )
41 31 40 mpbird ⊢ ( 𝜑 → ( ( ! ‘ 𝐻 ) gcd 𝑃 ) = 1 )