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	1 3 8 27	4syl	$$⊢\phi \to \frac{P-1}{2}<P$$
29	2 28	eqbrtrid	$$⊢\phi \to H<P$$
30		prmndvdsfaclt	$$⊢\left(P\in \mathbb{P}\wedge H\in {\mathbb{N}}_0\right)\to \left(H<P\to \neg P\parallel H!\right)$$
31	7 29 30	sylc	$$⊢\phi \to \neg P\parallel H!$$
32	6	faccld	$$⊢\phi \to H!\in \mathbb{N}$$
33	32	nnzd	$$⊢\phi \to H!\in \mathbb{Z}$$
34		nnz	$$⊢P\in \mathbb{N}\to P\in \mathbb{Z}$$
35	1 3 8 34	4syl	$$⊢\phi \to P\in \mathbb{Z}$$
36	33 35	gcdcomd	$$⊢\phi \to H!\gcd P=P\gcd H!$$
37	36	eqeq1d	$$⊢\phi \to \left(H!\gcd P=1\leftrightarrow P\gcd H!=1\right)$$
38		coprm	$$⊢\left(P\in \mathbb{P}\wedge H!\in \mathbb{Z}\right)\to \left(\neg P\parallel H!\leftrightarrow P\gcd H!=1\right)$$
39	4 33 38	syl2anc	$$⊢\phi \to \left(\neg P\parallel H!\leftrightarrow P\gcd H!=1\right)$$
40	37 39	bitr4d	$$⊢\phi \to \left(H!\gcd P=1\leftrightarrow \neg P\parallel H!\right)$$
41	31 40	mpbird	$$⊢\phi \to H!\gcd P=1$$