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	3 8 27	3syl	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑃 − 1 ) / 2 ) < 𝑃 )
29	1 28	syl	⊢ ( 𝜑 → ( ( 𝑃 − 1 ) / 2 ) < 𝑃 )
30	2 29	eqbrtrid	⊢ ( 𝜑 → 𝐻 < 𝑃 )
31		prmndvdsfaclt	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐻 ∈ ℕ0 ) → ( 𝐻 < 𝑃 → ¬ 𝑃 ∥ ( ! ‘ 𝐻 ) ) )
32	7 30 31	sylc	⊢ ( 𝜑 → ¬ 𝑃 ∥ ( ! ‘ 𝐻 ) )
33	6	faccld	⊢ ( 𝜑 → ( ! ‘ 𝐻 ) ∈ ℕ )
34	33	nnzd	⊢ ( 𝜑 → ( ! ‘ 𝐻 ) ∈ ℤ )
35		nnz	⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℤ )
36	3 8 35	3syl	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℤ )
37	1 36	syl	⊢ ( 𝜑 → 𝑃 ∈ ℤ )
38	34 37	gcdcomd	⊢ ( 𝜑 → ( ( ! ‘ 𝐻 ) gcd 𝑃 ) = ( 𝑃 gcd ( ! ‘ 𝐻 ) ) )
39	38	eqeq1d	⊢ ( 𝜑 → ( ( ( ! ‘ 𝐻 ) gcd 𝑃 ) = 1 ↔ ( 𝑃 gcd ( ! ‘ 𝐻 ) ) = 1 ) )
40		coprm	⊢ ( ( 𝑃 ∈ ℙ ∧ ( ! ‘ 𝐻 ) ∈ ℤ ) → ( ¬ 𝑃 ∥ ( ! ‘ 𝐻 ) ↔ ( 𝑃 gcd ( ! ‘ 𝐻 ) ) = 1 ) )
41	4 34 40	syl2anc	⊢ ( 𝜑 → ( ¬ 𝑃 ∥ ( ! ‘ 𝐻 ) ↔ ( 𝑃 gcd ( ! ‘ 𝐻 ) ) = 1 ) )
42	39 41	bitr4d	⊢ ( 𝜑 → ( ( ( ! ‘ 𝐻 ) gcd 𝑃 ) = 1 ↔ ¬ 𝑃 ∥ ( ! ‘ 𝐻 ) ) )
43	32 42	mpbird	⊢ ( 𝜑 → ( ( ! ‘ 𝐻 ) gcd 𝑃 ) = 1 )