Theorem pockthlem

Description: Lemma for pockthg . (Contributed by Mario Carneiro, 2-Mar-2014)

	Ref	Expression
Hypotheses	pockthg.1	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
	pockthg.2	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
	pockthg.3	⊢ ( 𝜑 → 𝐵 < 𝐴 )
	pockthg.4	⊢ ( 𝜑 → 𝑁 = ( ( 𝐴 · 𝐵 ) + 1 ) )
	pockthlem.5	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	pockthlem.6	⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
	pockthlem.7	⊢ ( 𝜑 → 𝑄 ∈ ℙ )
	pockthlem.8	⊢ ( 𝜑 → ( 𝑄 pCnt 𝐴 ) ∈ ℕ )
	pockthlem.9	⊢ ( 𝜑 → 𝐶 ∈ ℤ )
	pockthlem.10	⊢ ( 𝜑 → ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) = 1 )
	pockthlem.11	⊢ ( 𝜑 → ( ( ( 𝐶 ↑ ( ( 𝑁 − 1 ) / 𝑄 ) ) − 1 ) gcd 𝑁 ) = 1 )
Assertion	pockthlem	⊢ ( 𝜑 → ( 𝑄 pCnt 𝐴 ) ≤ ( 𝑄 pCnt ( 𝑃 − 1 ) ) )

Proof

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