Theorem gausslemma2dlem0c

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

	Ref	Expression
Hypotheses	gausslemma2dlem0a.p	$$⊢\phi \to P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)$$
	gausslemma2dlem0b.h	$$⊢H=\frac{P-1}{2}$$
Assertion	gausslemma2dlem0c	$$⊢\phi \to H!\gcd P=1$$

Proof

Step	Hyp	Ref	Expression
1		gausslemma2dlem0a.p	$$⊢\phi \to P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)$$
2		gausslemma2dlem0b.h	$$⊢H=\frac{P-1}{2}$$
3		eldifi	$$⊢P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\to P\in \mathbb{P}$$
4	1 3	syl	$$⊢\phi \to P\in \mathbb{P}$$
5	1 2	gausslemma2dlem0b	$$⊢\phi \to H\in \mathbb{N}$$
6	5	nnnn0d	$$⊢\phi \to H\in {\mathbb{N}}_0$$
7	4 6	jca	$$⊢\phi \to \left(P\in \mathbb{P}\wedge H\in {\mathbb{N}}_0\right)$$
8		prmnn	$$⊢P\in \mathbb{P}\to P\in \mathbb{N}$$
9		nnre	$$⊢P\in \mathbb{N}\to P\in ℝ$$
10		peano2rem	$$⊢P\in ℝ\to P-1\in ℝ$$
11	9 10	syl	$$⊢P\in \mathbb{N}\to P-1\in ℝ$$
12		2re	$$⊢2\in ℝ$$
13	12	a1i	$$⊢P\in \mathbb{N}\to 2\in ℝ$$
14	13 9	remulcld	$$⊢P\in \mathbb{N}\to 2P\in ℝ$$
15	9	ltm1d	$$⊢P\in \mathbb{N}\to P-1<P$$
16		nnnn0	$$⊢P\in \mathbb{N}\to P\in {\mathbb{N}}_0$$
17	16	nn0ge0d	$$⊢P\in \mathbb{N}\to 0\le P$$
18		1le2	$$⊢1\le 2$$
19	18	a1i	$$⊢P\in \mathbb{N}\to 1\le 2$$
20	9 13 17 19	lemulge12d	$$⊢P\in \mathbb{N}\to P\le 2P$$
21	11 9 14 15 20	ltletrd	$$⊢P\in \mathbb{N}\to P-1<2P$$
22		2pos	$$⊢0<2$$
23	12 22	pm3.2i	$$⊢\left(2\in ℝ\wedge 0<2\right)$$
24	23	a1i	$$⊢P\in \mathbb{N}\to \left(2\in ℝ\wedge 0<2\right)$$
25		ltdivmul	$$⊢\left(P-1\in ℝ\wedge P\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left(\frac{P-1}{2}<P\leftrightarrow P-1<2P\right)$$
26	11 9 24 25	syl3anc	$$⊢P\in \mathbb{N}\to \left(\frac{P-1}{2}<P\leftrightarrow P-1<2P\right)$$
27	21 26	mpbird	$$⊢P\in \mathbb{N}\to \frac{P-1}{2}<P$$
28	3 8 27	3syl	$$⊢P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\to \frac{P-1}{2}<P$$
29	1 28	syl	$$⊢\phi \to \frac{P-1}{2}<P$$
30	2 29	eqbrtrid	$$⊢\phi \to H<P$$
31		prmndvdsfaclt	$$⊢\left(P\in \mathbb{P}\wedge H\in {\mathbb{N}}_0\right)\to \left(H<P\to \neg P\parallel H!\right)$$
32	7 30 31	sylc	$$⊢\phi \to \neg P\parallel H!$$
33	6	faccld	$$⊢\phi \to H!\in \mathbb{N}$$
34	33	nnzd	$$⊢\phi \to H!\in \mathbb{Z}$$
35		nnz	$$⊢P\in \mathbb{N}\to P\in \mathbb{Z}$$
36	3 8 35	3syl	$$⊢P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\to P\in \mathbb{Z}$$
37	1 36	syl	$$⊢\phi \to P\in \mathbb{Z}$$
38	34 37	gcdcomd	$$⊢\phi \to H!\gcd P=P\gcd H!$$
39	38	eqeq1d	$$⊢\phi \to \left(H!\gcd P=1\leftrightarrow P\gcd H!=1\right)$$
40		coprm	$$⊢\left(P\in \mathbb{P}\wedge H!\in \mathbb{Z}\right)\to \left(\neg P\parallel H!\leftrightarrow P\gcd H!=1\right)$$
41	4 34 40	syl2anc	$$⊢\phi \to \left(\neg P\parallel H!\leftrightarrow P\gcd H!=1\right)$$
42	39 41	bitr4d	$$⊢\phi \to \left(H!\gcd P=1\leftrightarrow \neg P\parallel H!\right)$$
43	32 42	mpbird	$$⊢\phi \to H!\gcd P=1$$