pockthlem

	Ref	Expression
Hypotheses	pockthg.1	$⊢ φ \to A \in ℕ$
	pockthg.2	$⊢ φ \to B \in ℕ$
	pockthg.3	$⊢ φ \to B < A$
	pockthg.4	$⊢ φ \to N = A B + 1$
	pockthlem.5	$⊢ φ \to P \in ℙ$
	pockthlem.6	$⊢ φ \to P ∥ N$
	pockthlem.7	$⊢ φ \to Q \in ℙ$
	pockthlem.8	$⊢ φ \to Q pCnt A \in ℕ$
	pockthlem.9	$⊢ φ \to C \in ℤ$
	pockthlem.10	$⊢ φ \to C^{N - 1} \mod N = 1$
	pockthlem.11	$⊢ φ \to (C^{\frac{N - 1}{Q}} - 1) \gcd N = 1$
Assertion	pockthlem	$⊢ φ \to Q pCnt A \leq Q pCnt (P - 1)$

Proof

Step	Hyp	Ref	Expression
1		pockthg.1	$⊢ φ \to A \in ℕ$
2		pockthg.2	$⊢ φ \to B \in ℕ$
3		pockthg.3	$⊢ φ \to B < A$
4		pockthg.4	$⊢ φ \to N = A B + 1$
5		pockthlem.5	$⊢ φ \to P \in ℙ$
6		pockthlem.6	$⊢ φ \to P ∥ N$
7		pockthlem.7	$⊢ φ \to Q \in ℙ$
8		pockthlem.8	$⊢ φ \to Q pCnt A \in ℕ$
9		pockthlem.9	$⊢ φ \to C \in ℤ$
10		pockthlem.10	$⊢ φ \to C^{N - 1} \mod N = 1$
11		pockthlem.11	$⊢ φ \to (C^{\frac{N - 1}{Q}} - 1) \gcd N = 1$
12		prmnn	$⊢ Q \in ℙ \to Q \in ℕ$
13	7 12	syl	$⊢ φ \to Q \in ℕ$
14	8	nnnn0d	$⊢ φ \to Q pCnt A \in ℕ_{0}$
15	13 14	nnexpcld	$⊢ φ \to Q^{Q pCnt A} \in ℕ$
16	15	nnzd	$⊢ φ \to Q^{Q pCnt A} \in ℤ$
17		prmnn	$⊢ P \in ℙ \to P \in ℕ$
18	5 17	syl	$⊢ φ \to P \in ℕ$
19	18	nnzd	$⊢ φ \to P \in ℤ$
20		gcddvds	$⊢ (C \in ℤ \land P \in ℤ) \to ((C \gcd P) ∥ C \land (C \gcd P) ∥ P)$
21	9 19 20	syl2anc	$⊢ φ \to ((C \gcd P) ∥ C \land (C \gcd P) ∥ P)$
22	21	simpld	$⊢ φ \to (C \gcd P) ∥ C$
23	9 19	gcdcld	$⊢ φ \to C \gcd P \in ℕ_{0}$
24	23	nn0zd	$⊢ φ \to C \gcd P \in ℤ$
25	1 2	nnmulcld	$⊢ φ \to A B \in ℕ$
26		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
27	25 26	eleqtrdi	$⊢ φ \to A B \in ℤ_{\geq 1}$
28		eluzp1p1	$⊢ A B \in ℤ_{\geq 1} \to A B + 1 \in ℤ_{\geq (1 + 1)}$
29	27 28	syl	$⊢ φ \to A B + 1 \in ℤ_{\geq (1 + 1)}$
30	4 29	eqeltrd	$⊢ φ \to N \in ℤ_{\geq (1 + 1)}$
31		df-2	$⊢ 2 = 1 + 1$
32	31	fveq2i	$⊢ ℤ_{\geq 2} = ℤ_{\geq (1 + 1)}$
33	30 32	eleqtrrdi	$⊢ φ \to N \in ℤ_{\geq 2}$
34		eluz2b2	$⊢ N \in ℤ_{\geq 2} \leftrightarrow (N \in ℕ \land 1 < N)$
35	33 34	sylib	$⊢ φ \to (N \in ℕ \land 1 < N)$
36	35	simpld	$⊢ φ \to N \in ℕ$
37	36	nnzd	$⊢ φ \to N \in ℤ$
38	21	simprd	$⊢ φ \to (C \gcd P) ∥ P$
39	24 19 37 38 6	dvdstrd	$⊢ φ \to (C \gcd P) ∥ N$
40	36	nnne0d	$⊢ φ \to N \neq 0$
41		simpr	$⊢ (C = 0 \land N = 0) \to N = 0$
42	41	necon3ai	$⊢ N \neq 0 \to \neg (C = 0 \land N = 0)$
43	40 42	syl	$⊢ φ \to \neg (C = 0 \land N = 0)$
44		dvdslegcd	$⊢ ((C \gcd P \in ℤ \land C \in ℤ \land N \in ℤ) \land \neg (C = 0 \land N = 0)) \to (((C \gcd P) ∥ C \land (C \gcd P) ∥ N) \to C \gcd P \leq C \gcd N)$
45	24 9 37 43 44	syl31anc	$⊢ φ \to (((C \gcd P) ∥ C \land (C \gcd P) ∥ N) \to C \gcd P \leq C \gcd N)$
46	22 39 45	mp2and	$⊢ φ \to C \gcd P \leq C \gcd N$
47	10	oveq1d	$⊢ φ \to (C^{N - 1} \mod N) \gcd N = 1 \gcd N$
48		1z	$⊢ 1 \in ℤ$
49		eluzp1m1	$⊢ (1 \in ℤ \land N \in ℤ_{\geq (1 + 1)}) \to N - 1 \in ℤ_{\geq 1}$
50	48 30 49	sylancr	$⊢ φ \to N - 1 \in ℤ_{\geq 1}$
51	50 26	eleqtrrdi	$⊢ φ \to N - 1 \in ℕ$
52	51	nnnn0d	$⊢ φ \to N - 1 \in ℕ_{0}$
53		zexpcl	$⊢ (C \in ℤ \land N - 1 \in ℕ_{0}) \to C^{N - 1} \in ℤ$
54	9 52 53	syl2anc	$⊢ φ \to C^{N - 1} \in ℤ$
55		modgcd	$⊢ (C^{N - 1} \in ℤ \land N \in ℕ) \to (C^{N - 1} \mod N) \gcd N = C^{N - 1} \gcd N$
56	54 36 55	syl2anc	$⊢ φ \to (C^{N - 1} \mod N) \gcd N = C^{N - 1} \gcd N$
57		gcdcom	$⊢ (1 \in ℤ \land N \in ℤ) \to 1 \gcd N = N \gcd 1$
58	48 37 57	sylancr	$⊢ φ \to 1 \gcd N = N \gcd 1$
59		gcd1	$⊢ N \in ℤ \to N \gcd 1 = 1$
60	37 59	syl	$⊢ φ \to N \gcd 1 = 1$
61	58 60	eqtrd	$⊢ φ \to 1 \gcd N = 1$
62	47 56 61	3eqtr3d	$⊢ φ \to C^{N - 1} \gcd N = 1$
63		rpexp	$⊢ (C \in ℤ \land N \in ℤ \land N - 1 \in ℕ) \to (C^{N - 1} \gcd N = 1 \leftrightarrow C \gcd N = 1)$
64	9 37 51 63	syl3anc	$⊢ φ \to (C^{N - 1} \gcd N = 1 \leftrightarrow C \gcd N = 1)$
65	62 64	mpbid	$⊢ φ \to C \gcd N = 1$
66	46 65	breqtrd	$⊢ φ \to C \gcd P \leq 1$
67	18	nnne0d	$⊢ φ \to P \neq 0$
68		simpr	$⊢ (C = 0 \land P = 0) \to P = 0$
69	68	necon3ai	$⊢ P \neq 0 \to \neg (C = 0 \land P = 0)$
70	67 69	syl	$⊢ φ \to \neg (C = 0 \land P = 0)$
71		gcdn0cl	$⊢ ((C \in ℤ \land P \in ℤ) \land \neg (C = 0 \land P = 0)) \to C \gcd P \in ℕ$
72	9 19 70 71	syl21anc	$⊢ φ \to C \gcd P \in ℕ$
73		nnle1eq1	$⊢ C \gcd P \in ℕ \to (C \gcd P \leq 1 \leftrightarrow C \gcd P = 1)$
74	72 73	syl	$⊢ φ \to (C \gcd P \leq 1 \leftrightarrow C \gcd P = 1)$
75	66 74	mpbid	$⊢ φ \to C \gcd P = 1$
76		odzcl	$⊢ (P \in ℕ \land C \in ℤ \land C \gcd P = 1) \to {od}_{ℤ} (P) (C) \in ℕ$
77	18 9 75 76	syl3anc	$⊢ φ \to {od}_{ℤ} (P) (C) \in ℕ$
78	77	nnzd	$⊢ φ \to {od}_{ℤ} (P) (C) \in ℤ$
79		prmuz2	$⊢ P \in ℙ \to P \in ℤ_{\geq 2}$
80	5 79	syl	$⊢ φ \to P \in ℤ_{\geq 2}$
81	80 32	eleqtrdi	$⊢ φ \to P \in ℤ_{\geq (1 + 1)}$
82		eluzp1m1	$⊢ (1 \in ℤ \land P \in ℤ_{\geq (1 + 1)}) \to P - 1 \in ℤ_{\geq 1}$
83	48 81 82	sylancr	$⊢ φ \to P - 1 \in ℤ_{\geq 1}$
84	83 26	eleqtrrdi	$⊢ φ \to P - 1 \in ℕ$
85	84	nnzd	$⊢ φ \to P - 1 \in ℤ$
86	1	nnzd	$⊢ φ \to A \in ℤ$
87	51	nnzd	$⊢ φ \to N - 1 \in ℤ$
88		pcdvds	$⊢ (Q \in ℙ \land A \in ℕ) \to Q^{Q pCnt A} ∥ A$
89	7 1 88	syl2anc	$⊢ φ \to Q^{Q pCnt A} ∥ A$
90	2	nnzd	$⊢ φ \to B \in ℤ$
91		dvdsmul1	$⊢ (A \in ℤ \land B \in ℤ) \to A ∥ A B$
92	86 90 91	syl2anc	$⊢ φ \to A ∥ A B$
93	4	oveq1d	$⊢ φ \to N - 1 = A B + 1 - 1$
94	25	nncnd	$⊢ φ \to A B \in ℂ$
95		ax-1cn	$⊢ 1 \in ℂ$
96		pncan	$⊢ (A B \in ℂ \land 1 \in ℂ) \to A B + 1 - 1 = A B$
97	94 95 96	sylancl	$⊢ φ \to A B + 1 - 1 = A B$
98	93 97	eqtrd	$⊢ φ \to N - 1 = A B$
99	92 98	breqtrrd	$⊢ φ \to A ∥ (N - 1)$
100	16 86 87 89 99	dvdstrd	$⊢ φ \to Q^{Q pCnt A} ∥ (N - 1)$
101	15	nnne0d	$⊢ φ \to Q^{Q pCnt A} \neq 0$
102		dvdsval2	$⊢ (Q^{Q pCnt A} \in ℤ \land Q^{Q pCnt A} \neq 0 \land N - 1 \in ℤ) \to (Q^{Q pCnt A} ∥ (N - 1) \leftrightarrow \frac{N - 1}{Q^{Q pCnt A}} \in ℤ)$
103	16 101 87 102	syl3anc	$⊢ φ \to (Q^{Q pCnt A} ∥ (N - 1) \leftrightarrow \frac{N - 1}{Q^{Q pCnt A}} \in ℤ)$
104	100 103	mpbid	$⊢ φ \to \frac{N - 1}{Q^{Q pCnt A}} \in ℤ$
105		peano2zm	$⊢ C^{N - 1} \in ℤ \to C^{N - 1} - 1 \in ℤ$
106	54 105	syl	$⊢ φ \to C^{N - 1} - 1 \in ℤ$
107	36	nnred	$⊢ φ \to N \in ℝ$
108	35	simprd	$⊢ φ \to 1 < N$
109		1mod	$⊢ (N \in ℝ \land 1 < N) \to 1 \mod N = 1$
110	107 108 109	syl2anc	$⊢ φ \to 1 \mod N = 1$
111	10 110	eqtr4d	$⊢ φ \to C^{N - 1} \mod N = 1 \mod N$
112		1zzd	$⊢ φ \to 1 \in ℤ$
113		moddvds	$⊢ (N \in ℕ \land C^{N - 1} \in ℤ \land 1 \in ℤ) \to (C^{N - 1} \mod N = 1 \mod N \leftrightarrow N ∥ (C^{N - 1} - 1))$
114	36 54 112 113	syl3anc	$⊢ φ \to (C^{N - 1} \mod N = 1 \mod N \leftrightarrow N ∥ (C^{N - 1} - 1))$
115	111 114	mpbid	$⊢ φ \to N ∥ (C^{N - 1} - 1)$
116	19 37 106 6 115	dvdstrd	$⊢ φ \to P ∥ (C^{N - 1} - 1)$
117		odzdvds	$⊢ ((P \in ℕ \land C \in ℤ \land C \gcd P = 1) \land N - 1 \in ℕ_{0}) \to (P ∥ (C^{N - 1} - 1) \leftrightarrow {od}_{ℤ} (P) (C) ∥ (N - 1))$
118	18 9 75 52 117	syl31anc	$⊢ φ \to (P ∥ (C^{N - 1} - 1) \leftrightarrow {od}_{ℤ} (P) (C) ∥ (N - 1))$
119	116 118	mpbid	$⊢ φ \to {od}_{ℤ} (P) (C) ∥ (N - 1)$
120	51	nncnd	$⊢ φ \to N - 1 \in ℂ$
121	15	nncnd	$⊢ φ \to Q^{Q pCnt A} \in ℂ$
122	120 121 101	divcan1d	$⊢ φ \to (\frac{N - 1}{Q^{Q pCnt A}}) Q^{Q pCnt A} = N - 1$
123	119 122	breqtrrd	$⊢ φ \to {od}_{ℤ} (P) (C) ∥ (\frac{N - 1}{Q^{Q pCnt A}}) Q^{Q pCnt A}$
124		nprmdvds1	$⊢ P \in ℙ \to \neg P ∥ 1$
125	5 124	syl	$⊢ φ \to \neg P ∥ 1$
126	13	nnzd	$⊢ φ \to Q \in ℤ$
127		iddvdsexp	$⊢ (Q \in ℤ \land Q pCnt A \in ℕ) \to Q ∥ Q^{Q pCnt A}$
128	126 8 127	syl2anc	$⊢ φ \to Q ∥ Q^{Q pCnt A}$
129	126 16 87 128 100	dvdstrd	$⊢ φ \to Q ∥ (N - 1)$
130	13	nnne0d	$⊢ φ \to Q \neq 0$
131		dvdsval2	$⊢ (Q \in ℤ \land Q \neq 0 \land N - 1 \in ℤ) \to (Q ∥ (N - 1) \leftrightarrow \frac{N - 1}{Q} \in ℤ)$
132	126 130 87 131	syl3anc	$⊢ φ \to (Q ∥ (N - 1) \leftrightarrow \frac{N - 1}{Q} \in ℤ)$
133	129 132	mpbid	$⊢ φ \to \frac{N - 1}{Q} \in ℤ$
134	52	nn0ge0d	$⊢ φ \to 0 \leq N - 1$
135	51	nnred	$⊢ φ \to N - 1 \in ℝ$
136	13	nnred	$⊢ φ \to Q \in ℝ$
137	13	nngt0d	$⊢ φ \to 0 < Q$
138		ge0div	$⊢ (N - 1 \in ℝ \land Q \in ℝ \land 0 < Q) \to (0 \leq N - 1 \leftrightarrow 0 \leq \frac{N - 1}{Q})$
139	135 136 137 138	syl3anc	$⊢ φ \to (0 \leq N - 1 \leftrightarrow 0 \leq \frac{N - 1}{Q})$
140	134 139	mpbid	$⊢ φ \to 0 \leq \frac{N - 1}{Q}$
141		elnn0z	$⊢ \frac{N - 1}{Q} \in ℕ_{0} \leftrightarrow (\frac{N - 1}{Q} \in ℤ \land 0 \leq \frac{N - 1}{Q})$
142	133 140 141	sylanbrc	$⊢ φ \to \frac{N - 1}{Q} \in ℕ_{0}$
143		zexpcl	$⊢ (C \in ℤ \land \frac{N - 1}{Q} \in ℕ_{0}) \to C^{\frac{N - 1}{Q}} \in ℤ$
144	9 142 143	syl2anc	$⊢ φ \to C^{\frac{N - 1}{Q}} \in ℤ$
145		peano2zm	$⊢ C^{\frac{N - 1}{Q}} \in ℤ \to C^{\frac{N - 1}{Q}} - 1 \in ℤ$
146	144 145	syl	$⊢ φ \to C^{\frac{N - 1}{Q}} - 1 \in ℤ$
147		dvdsgcd	$⊢ (P \in ℤ \land C^{\frac{N - 1}{Q}} - 1 \in ℤ \land N \in ℤ) \to ((P ∥ (C^{\frac{N - 1}{Q}} - 1) \land P ∥ N) \to P ∥ ((C^{\frac{N - 1}{Q}} - 1) \gcd N))$
148	19 146 37 147	syl3anc	$⊢ φ \to ((P ∥ (C^{\frac{N - 1}{Q}} - 1) \land P ∥ N) \to P ∥ ((C^{\frac{N - 1}{Q}} - 1) \gcd N))$
149	6 148	mpan2d	$⊢ φ \to (P ∥ (C^{\frac{N - 1}{Q}} - 1) \to P ∥ ((C^{\frac{N - 1}{Q}} - 1) \gcd N))$
150		odzdvds	$⊢ ((P \in ℕ \land C \in ℤ \land C \gcd P = 1) \land \frac{N - 1}{Q} \in ℕ_{0}) \to (P ∥ (C^{\frac{N - 1}{Q}} - 1) \leftrightarrow {od}_{ℤ} (P) (C) ∥ (\frac{N - 1}{Q}))$
151	18 9 75 142 150	syl31anc	$⊢ φ \to (P ∥ (C^{\frac{N - 1}{Q}} - 1) \leftrightarrow {od}_{ℤ} (P) (C) ∥ (\frac{N - 1}{Q}))$
152	13	nncnd	$⊢ φ \to Q \in ℂ$
153	8	nnzd	$⊢ φ \to Q pCnt A \in ℤ$
154	152 130 153	expm1d	$⊢ φ \to Q^{(Q pCnt A) - 1} = \frac{Q^{Q pCnt A}}{Q}$
155	154	oveq2d	$⊢ φ \to (\frac{N - 1}{Q^{Q pCnt A}}) Q^{(Q pCnt A) - 1} = (\frac{N - 1}{Q^{Q pCnt A}}) (\frac{Q^{Q pCnt A}}{Q})$
156	135 15	nndivred	$⊢ φ \to \frac{N - 1}{Q^{Q pCnt A}} \in ℝ$
157	156	recnd	$⊢ φ \to \frac{N - 1}{Q^{Q pCnt A}} \in ℂ$
158	157 121 152 130	divassd	$⊢ φ \to \frac{(\frac{N - 1}{Q^{Q pCnt A}}) Q^{Q pCnt A}}{Q} = (\frac{N - 1}{Q^{Q pCnt A}}) (\frac{Q^{Q pCnt A}}{Q})$
159	122	oveq1d	$⊢ φ \to \frac{(\frac{N - 1}{Q^{Q pCnt A}}) Q^{Q pCnt A}}{Q} = \frac{N - 1}{Q}$
160	155 158 159	3eqtr2d	$⊢ φ \to (\frac{N - 1}{Q^{Q pCnt A}}) Q^{(Q pCnt A) - 1} = \frac{N - 1}{Q}$
161	160	breq2d	$⊢ φ \to ({od}_{ℤ} (P) (C) ∥ (\frac{N - 1}{Q^{Q pCnt A}}) Q^{(Q pCnt A) - 1} \leftrightarrow {od}_{ℤ} (P) (C) ∥ (\frac{N - 1}{Q}))$
162	151 161	bitr4d	$⊢ φ \to (P ∥ (C^{\frac{N - 1}{Q}} - 1) \leftrightarrow {od}_{ℤ} (P) (C) ∥ (\frac{N - 1}{Q^{Q pCnt A}}) Q^{(Q pCnt A) - 1})$
163	11	breq2d	$⊢ φ \to (P ∥ ((C^{\frac{N - 1}{Q}} - 1) \gcd N) \leftrightarrow P ∥ 1)$
164	149 162 163	3imtr3d	$⊢ φ \to ({od}_{ℤ} (P) (C) ∥ (\frac{N - 1}{Q^{Q pCnt A}}) Q^{(Q pCnt A) - 1} \to P ∥ 1)$
165	125 164	mtod	$⊢ φ \to \neg {od}_{ℤ} (P) (C) ∥ (\frac{N - 1}{Q^{Q pCnt A}}) Q^{(Q pCnt A) - 1}$
166		prmpwdvds	$⊢ ((\frac{N - 1}{Q^{Q pCnt A}} \in ℤ \land {od}_{ℤ} (P) (C) \in ℤ) \land (Q \in ℙ \land Q pCnt A \in ℕ) \land ({od}_{ℤ} (P) (C) ∥ (\frac{N - 1}{Q^{Q pCnt A}}) Q^{Q pCnt A} \land \neg {od}_{ℤ} (P) (C) ∥ (\frac{N - 1}{Q^{Q pCnt A}}) Q^{(Q pCnt A) - 1})) \to Q^{Q pCnt A} ∥ {od}_{ℤ} (P) (C)$
167	104 78 7 8 123 165 166	syl222anc	$⊢ φ \to Q^{Q pCnt A} ∥ {od}_{ℤ} (P) (C)$
168		odzphi	$⊢ (P \in ℕ \land C \in ℤ \land C \gcd P = 1) \to {od}_{ℤ} (P) (C) ∥ ϕ (P)$
169	18 9 75 168	syl3anc	$⊢ φ \to {od}_{ℤ} (P) (C) ∥ ϕ (P)$
170		phiprm	$⊢ P \in ℙ \to ϕ (P) = P - 1$
171	5 170	syl	$⊢ φ \to ϕ (P) = P - 1$
172	169 171	breqtrd	$⊢ φ \to {od}_{ℤ} (P) (C) ∥ (P - 1)$
173	16 78 85 167 172	dvdstrd	$⊢ φ \to Q^{Q pCnt A} ∥ (P - 1)$
174		pcdvdsb	$⊢ (Q \in ℙ \land P - 1 \in ℤ \land Q pCnt A \in ℕ_{0}) \to (Q pCnt A \leq Q pCnt (P - 1) \leftrightarrow Q^{Q pCnt A} ∥ (P - 1))$
175	7 85 14 174	syl3anc	$⊢ φ \to (Q pCnt A \leq Q pCnt (P - 1) \leftrightarrow Q^{Q pCnt A} ∥ (P - 1))$
176	173 175	mpbird	$⊢ φ \to Q pCnt A \leq Q pCnt (P - 1)$

Metamath Proof Explorer

Theorem pockthlem

Proof