pockthlem - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > pockthlem		GIF version

Theorem pockthlem 13082

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

**Hypotheses**
Ref	Expression
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**
Ref	Expression
pockthlem	⊢ (𝜑 → (𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1)))

**Proof of Theorem pockthlem**
Step	Hyp	Ref	Expression
1		pockthlem.7	. . . . . 6 ⊢ (𝜑 → 𝑄 ∈ ℙ)
2		prmnn 12835	. . . . . 6 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ ℕ)
3	1, 2	syl 14	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ ℕ)
4		pockthlem.8	. . . . . 6 ⊢ (𝜑 → (𝑄 pCnt 𝐴) ∈ ℕ)
5	4	nnnn0d 9573	. . . . 5 ⊢ (𝜑 → (𝑄 pCnt 𝐴) ∈ ℕ₀)
6	3, 5	nnexpcld 11085	. . . 4 ⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∈ ℕ)
7	6	nnzd 9720	. . 3 ⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∈ ℤ)
8		pockthlem.5	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ ℙ)
9		prmnn 12835	. . . . . 6 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
10	8, 9	syl 14	. . . . 5 ⊢ (𝜑 → 𝑃 ∈ ℕ)
11		pockthlem.9	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ ℤ)
12	10	nnzd 9720	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ ℤ)
13		gcddvds 12687	. . . . . . . . . 10 ⊢ ((𝐶 ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑃))
14	11, 12, 13	syl2anc 411	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑃))
15	14	simpld 112	. . . . . . . 8 ⊢ (𝜑 → (𝐶 gcd 𝑃) ∥ 𝐶)
16	11, 12	gcdcld 12692	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶 gcd 𝑃) ∈ ℕ₀)
17	16	nn0zd 9719	. . . . . . . . 9 ⊢ (𝜑 → (𝐶 gcd 𝑃) ∈ ℤ)
18		pockthg.4	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 = ((𝐴 · 𝐵) + 1))
19		pockthg.1	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ℕ)
20		pockthg.2	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ ℕ)
21	19, 20	nnmulcld 9306	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ)
22		nnuz 9911	. . . . . . . . . . . . . . . 16 ⊢ ℕ = (ℤ_≥‘1)
23	21, 22	eleqtrdi 2327	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ (ℤ_≥‘1))
24		eluzp1p1 9901	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 · 𝐵) ∈ (ℤ_≥‘1) → ((𝐴 · 𝐵) + 1) ∈ (ℤ_≥‘(1 + 1)))
25	23, 24	syl 14	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 · 𝐵) + 1) ∈ (ℤ_≥‘(1 + 1)))
26	18, 25	eqeltrd 2311	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(1 + 1)))
27		df-2 9316	. . . . . . . . . . . . . 14 ⊢ 2 = (1 + 1)
28	27	fveq2i 5678	. . . . . . . . . . . . 13 ⊢ (ℤ_≥‘2) = (ℤ_≥‘(1 + 1))
29	26, 28	eleqtrrdi 2328	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘2))
30		eluz2b2 9956	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘2) ↔ (𝑁 ∈ ℕ ∧ 1 < 𝑁))
31	29, 30	sylib 122	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 1 < 𝑁))
32	31	simpld 112	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℕ)
33	32	nnzd 9720	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℤ)
34	14	simprd 114	. . . . . . . . 9 ⊢ (𝜑 → (𝐶 gcd 𝑃) ∥ 𝑃)
35		pockthlem.6	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 ∥ 𝑁)
36	17, 12, 33, 34, 35	dvdstrd 12544	. . . . . . . 8 ⊢ (𝜑 → (𝐶 gcd 𝑃) ∥ 𝑁)
37	32	nnne0d 9302	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ≠ 0)
38		simpr 110	. . . . . . . . . . 11 ⊢ ((𝐶 = 0 ∧ 𝑁 = 0) → 𝑁 = 0)
39	38	necon3ai 2463	. . . . . . . . . 10 ⊢ (𝑁 ≠ 0 → ¬ (𝐶 = 0 ∧ 𝑁 = 0))
40	37, 39	syl 14	. . . . . . . . 9 ⊢ (𝜑 → ¬ (𝐶 = 0 ∧ 𝑁 = 0))
41		dvdslegcd 12688	. . . . . . . . 9 ⊢ ((((𝐶 gcd 𝑃) ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝐶 = 0 ∧ 𝑁 = 0)) → (((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑁) → (𝐶 gcd 𝑃) ≤ (𝐶 gcd 𝑁)))
42	17, 11, 33, 40, 41	syl31anc 1277	. . . . . . . 8 ⊢ (𝜑 → (((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑁) → (𝐶 gcd 𝑃) ≤ (𝐶 gcd 𝑁)))
43	15, 36, 42	mp2and 433	. . . . . . 7 ⊢ (𝜑 → (𝐶 gcd 𝑃) ≤ (𝐶 gcd 𝑁))
44		pockthlem.10	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) mod 𝑁) = 1)
45	44	oveq1d 6073	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶↑(𝑁 − 1)) mod 𝑁) gcd 𝑁) = (1 gcd 𝑁))
46		1z 9623	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℤ
47		eluzp1m1 9899	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℤ ∧ 𝑁 ∈ (ℤ_≥‘(1 + 1))) → (𝑁 − 1) ∈ (ℤ_≥‘1))
48	46, 26, 47	sylancr 414	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 − 1) ∈ (ℤ_≥‘1))
49	48, 22	eleqtrrdi 2328	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 − 1) ∈ ℕ)
50	49	nnnn0d 9573	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 − 1) ∈ ℕ₀)
51		zexpcl 10943	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ ℤ ∧ (𝑁 − 1) ∈ ℕ₀) → (𝐶↑(𝑁 − 1)) ∈ ℤ)
52	11, 50, 51	syl2anc 411	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶↑(𝑁 − 1)) ∈ ℤ)
53		modgcd 12715	. . . . . . . . . 10 ⊢ (((𝐶↑(𝑁 − 1)) ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐶↑(𝑁 − 1)) mod 𝑁) gcd 𝑁) = ((𝐶↑(𝑁 − 1)) gcd 𝑁))
54	52, 32, 53	syl2anc 411	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶↑(𝑁 − 1)) mod 𝑁) gcd 𝑁) = ((𝐶↑(𝑁 − 1)) gcd 𝑁))
55		gcdcom 12697	. . . . . . . . . . 11 ⊢ ((1 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (1 gcd 𝑁) = (𝑁 gcd 1))
56	46, 33, 55	sylancr 414	. . . . . . . . . 10 ⊢ (𝜑 → (1 gcd 𝑁) = (𝑁 gcd 1))
57		gcd1 12711	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℤ → (𝑁 gcd 1) = 1)
58	33, 57	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 gcd 1) = 1)
59	56, 58	eqtrd 2267	. . . . . . . . 9 ⊢ (𝜑 → (1 gcd 𝑁) = 1)
60	45, 54, 59	3eqtr3d 2275	. . . . . . . 8 ⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) gcd 𝑁) = 1)
61		rpexp 12878	. . . . . . . . 9 ⊢ ((𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁 − 1) ∈ ℕ) → (((𝐶↑(𝑁 − 1)) gcd 𝑁) = 1 ↔ (𝐶 gcd 𝑁) = 1))
62	11, 33, 49, 61	syl3anc 1274	. . . . . . . 8 ⊢ (𝜑 → (((𝐶↑(𝑁 − 1)) gcd 𝑁) = 1 ↔ (𝐶 gcd 𝑁) = 1))
63	60, 62	mpbid 147	. . . . . . 7 ⊢ (𝜑 → (𝐶 gcd 𝑁) = 1)
64	43, 63	breqtrd 4140	. . . . . 6 ⊢ (𝜑 → (𝐶 gcd 𝑃) ≤ 1)
65	10	nnne0d 9302	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 ≠ 0)
66		simpr 110	. . . . . . . . . 10 ⊢ ((𝐶 = 0 ∧ 𝑃 = 0) → 𝑃 = 0)
67	66	necon3ai 2463	. . . . . . . . 9 ⊢ (𝑃 ≠ 0 → ¬ (𝐶 = 0 ∧ 𝑃 = 0))
68	65, 67	syl 14	. . . . . . . 8 ⊢ (𝜑 → ¬ (𝐶 = 0 ∧ 𝑃 = 0))
69		gcdn0cl 12686	. . . . . . . 8 ⊢ (((𝐶 ∈ ℤ ∧ 𝑃 ∈ ℤ) ∧ ¬ (𝐶 = 0 ∧ 𝑃 = 0)) → (𝐶 gcd 𝑃) ∈ ℕ)
70	11, 12, 68, 69	syl21anc 1273	. . . . . . 7 ⊢ (𝜑 → (𝐶 gcd 𝑃) ∈ ℕ)
71		nnle1eq1 9281	. . . . . . 7 ⊢ ((𝐶 gcd 𝑃) ∈ ℕ → ((𝐶 gcd 𝑃) ≤ 1 ↔ (𝐶 gcd 𝑃) = 1))
72	70, 71	syl 14	. . . . . 6 ⊢ (𝜑 → ((𝐶 gcd 𝑃) ≤ 1 ↔ (𝐶 gcd 𝑃) = 1))
73	64, 72	mpbid 147	. . . . 5 ⊢ (𝜑 → (𝐶 gcd 𝑃) = 1)
74		odzcl 12969	. . . . 5 ⊢ ((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) → ((od_ℤ‘𝑃)‘𝐶) ∈ ℕ)
75	10, 11, 73, 74	syl3anc 1274	. . . 4 ⊢ (𝜑 → ((od_ℤ‘𝑃)‘𝐶) ∈ ℕ)
76	75	nnzd 9720	. . 3 ⊢ (𝜑 → ((od_ℤ‘𝑃)‘𝐶) ∈ ℤ)
77		prmuz2 12856	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ_≥‘2))
78	8, 77	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ (ℤ_≥‘2))
79	78, 28	eleqtrdi 2327	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ (ℤ_≥‘(1 + 1)))
80		eluzp1m1 9899	. . . . . 6 ⊢ ((1 ∈ ℤ ∧ 𝑃 ∈ (ℤ_≥‘(1 + 1))) → (𝑃 − 1) ∈ (ℤ_≥‘1))
81	46, 79, 80	sylancr 414	. . . . 5 ⊢ (𝜑 → (𝑃 − 1) ∈ (ℤ_≥‘1))
82	81, 22	eleqtrrdi 2328	. . . 4 ⊢ (𝜑 → (𝑃 − 1) ∈ ℕ)
83	82	nnzd 9720	. . 3 ⊢ (𝜑 → (𝑃 − 1) ∈ ℤ)
84	19	nnzd 9720	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ ℤ)
85	49	nnzd 9720	. . . . . 6 ⊢ (𝜑 → (𝑁 − 1) ∈ ℤ)
86		pcdvds 13041	. . . . . . 7 ⊢ ((𝑄 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (𝑄↑(𝑄 pCnt 𝐴)) ∥ 𝐴)
87	1, 19, 86	syl2anc 411	. . . . . 6 ⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ 𝐴)
88	20	nnzd 9720	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ ℤ)
89		dvdsmul1 12527	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∥ (𝐴 · 𝐵))
90	84, 88, 89	syl2anc 411	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∥ (𝐴 · 𝐵))
91	18	oveq1d 6073	. . . . . . . 8 ⊢ (𝜑 → (𝑁 − 1) = (((𝐴 · 𝐵) + 1) − 1))
92	21	nncnd 9271	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ)
93		ax-1cn 8236	. . . . . . . . 9 ⊢ 1 ∈ ℂ
94		pncan 8496	. . . . . . . . 9 ⊢ (((𝐴 · 𝐵) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐴 · 𝐵) + 1) − 1) = (𝐴 · 𝐵))
95	92, 93, 94	sylancl 413	. . . . . . . 8 ⊢ (𝜑 → (((𝐴 · 𝐵) + 1) − 1) = (𝐴 · 𝐵))
96	91, 95	eqtrd 2267	. . . . . . 7 ⊢ (𝜑 → (𝑁 − 1) = (𝐴 · 𝐵))
97	90, 96	breqtrrd 4142	. . . . . 6 ⊢ (𝜑 → 𝐴 ∥ (𝑁 − 1))
98	7, 84, 85, 87, 97	dvdstrd 12544	. . . . 5 ⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1))
99	6	nnne0d 9302	. . . . . 6 ⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ≠ 0)
100		dvdsval2 12504	. . . . . 6 ⊢ (((𝑄↑(𝑄 pCnt 𝐴)) ∈ ℤ ∧ (𝑄↑(𝑄 pCnt 𝐴)) ≠ 0 ∧ (𝑁 − 1) ∈ ℤ) → ((𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ))
101	7, 99, 85, 100	syl3anc 1274	. . . . 5 ⊢ (𝜑 → ((𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ))
102	98, 101	mpbid 147	. . . 4 ⊢ (𝜑 → ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ)
103		peano2zm 9635	. . . . . . . 8 ⊢ ((𝐶↑(𝑁 − 1)) ∈ ℤ → ((𝐶↑(𝑁 − 1)) − 1) ∈ ℤ)
104	52, 103	syl 14	. . . . . . 7 ⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) − 1) ∈ ℤ)
105		nnq 9986	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℚ)
106	32, 105	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℚ)
107	31	simprd 114	. . . . . . . . . 10 ⊢ (𝜑 → 1 < 𝑁)
108		q1mod 10745	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 1 < 𝑁) → (1 mod 𝑁) = 1)
109	106, 107, 108	syl2anc 411	. . . . . . . . 9 ⊢ (𝜑 → (1 mod 𝑁) = 1)
110	44, 109	eqtr4d 2270	. . . . . . . 8 ⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁))
111		1zzd 9624	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℤ)
112		moddvds 12513	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ (𝐶↑(𝑁 − 1)) ∈ ℤ ∧ 1 ∈ ℤ) → (((𝐶↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1)))
113	32, 52, 111, 112	syl3anc 1274	. . . . . . . 8 ⊢ (𝜑 → (((𝐶↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1)))
114	110, 113	mpbid 147	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1))
115	12, 33, 104, 35, 114	dvdstrd 12544	. . . . . 6 ⊢ (𝜑 → 𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1))
116		odzdvds 12971	. . . . . . 7 ⊢ (((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) ∧ (𝑁 − 1) ∈ ℕ₀) → (𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1) ↔ ((od_ℤ‘𝑃)‘𝐶) ∥ (𝑁 − 1)))
117	10, 11, 73, 50, 116	syl31anc 1277	. . . . . 6 ⊢ (𝜑 → (𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1) ↔ ((od_ℤ‘𝑃)‘𝐶) ∥ (𝑁 − 1)))
118	115, 117	mpbid 147	. . . . 5 ⊢ (𝜑 → ((od_ℤ‘𝑃)‘𝐶) ∥ (𝑁 − 1))
119	49	nncnd 9271	. . . . . 6 ⊢ (𝜑 → (𝑁 − 1) ∈ ℂ)
120	6	nncnd 9271	. . . . . 6 ⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∈ ℂ)
121	6	nnap0d 9303	. . . . . 6 ⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) # 0)
122	119, 120, 121	divcanap1d 9085	. . . . 5 ⊢ (𝜑 → (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) = (𝑁 − 1))
123	118, 122	breqtrrd 4142	. . . 4 ⊢ (𝜑 → ((od_ℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))))
124		nprmdvds1 12865	. . . . . 6 ⊢ (𝑃 ∈ ℙ → ¬ 𝑃 ∥ 1)
125	8, 124	syl 14	. . . . 5 ⊢ (𝜑 → ¬ 𝑃 ∥ 1)
126	3	nnzd 9720	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 ∈ ℤ)
127		iddvdsexp 12529	. . . . . . . . . . . . . 14 ⊢ ((𝑄 ∈ ℤ ∧ (𝑄 pCnt 𝐴) ∈ ℕ) → 𝑄 ∥ (𝑄↑(𝑄 pCnt 𝐴)))
128	126, 4, 127	syl2anc 411	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 ∥ (𝑄↑(𝑄 pCnt 𝐴)))
129	126, 7, 85, 128, 98	dvdstrd 12544	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∥ (𝑁 − 1))
130	3	nnne0d 9302	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 ≠ 0)
131		dvdsval2 12504	. . . . . . . . . . . . 13 ⊢ ((𝑄 ∈ ℤ ∧ 𝑄 ≠ 0 ∧ (𝑁 − 1) ∈ ℤ) → (𝑄 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 𝑄) ∈ ℤ))
132	126, 130, 85, 131	syl3anc 1274	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 𝑄) ∈ ℤ))
133	129, 132	mpbid 147	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑁 − 1) / 𝑄) ∈ ℤ)
134	50	nn0ge0d 9576	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≤ (𝑁 − 1))
135	49	nnred 9270	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 − 1) ∈ ℝ)
136	3	nnred 9270	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 ∈ ℝ)
137	3	nngt0d 9301	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < 𝑄)
138		ge0div 9165	. . . . . . . . . . . . 13 ⊢ (((𝑁 − 1) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ 0 < 𝑄) → (0 ≤ (𝑁 − 1) ↔ 0 ≤ ((𝑁 − 1) / 𝑄)))
139	135, 136, 137, 138	syl3anc 1274	. . . . . . . . . . . 12 ⊢ (𝜑 → (0 ≤ (𝑁 − 1) ↔ 0 ≤ ((𝑁 − 1) / 𝑄)))
140	134, 139	mpbid 147	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ ((𝑁 − 1) / 𝑄))
141		elnn0z 9610	. . . . . . . . . . 11 ⊢ (((𝑁 − 1) / 𝑄) ∈ ℕ₀ ↔ (((𝑁 − 1) / 𝑄) ∈ ℤ ∧ 0 ≤ ((𝑁 − 1) / 𝑄)))
142	133, 140, 141	sylanbrc 417	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁 − 1) / 𝑄) ∈ ℕ₀)
143		zexpcl 10943	. . . . . . . . . 10 ⊢ ((𝐶 ∈ ℤ ∧ ((𝑁 − 1) / 𝑄) ∈ ℕ₀) → (𝐶↑((𝑁 − 1) / 𝑄)) ∈ ℤ)
144	11, 142, 143	syl2anc 411	. . . . . . . . 9 ⊢ (𝜑 → (𝐶↑((𝑁 − 1) / 𝑄)) ∈ ℤ)
145		peano2zm 9635	. . . . . . . . 9 ⊢ ((𝐶↑((𝑁 − 1) / 𝑄)) ∈ ℤ → ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∈ ℤ)
146	144, 145	syl 14	. . . . . . . 8 ⊢ (𝜑 → ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∈ ℤ)
147		dvdsgcd 12736	. . . . . . . 8 ⊢ ((𝑃 ∈ ℤ ∧ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∧ 𝑃 ∥ 𝑁) → 𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁)))
148	12, 146, 33, 147	syl3anc 1274	. . . . . . 7 ⊢ (𝜑 → ((𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∧ 𝑃 ∥ 𝑁) → 𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁)))
149	35, 148	mpan2d 428	. . . . . 6 ⊢ (𝜑 → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) → 𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁)))
150		odzdvds 12971	. . . . . . . 8 ⊢ (((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) ∧ ((𝑁 − 1) / 𝑄) ∈ ℕ₀) → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ↔ ((od_ℤ‘𝑃)‘𝐶) ∥ ((𝑁 − 1) / 𝑄)))
151	10, 11, 73, 142, 150	syl31anc 1277	. . . . . . 7 ⊢ (𝜑 → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ↔ ((od_ℤ‘𝑃)‘𝐶) ∥ ((𝑁 − 1) / 𝑄)))
152	3	nncnd 9271	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ∈ ℂ)
153	3	nnap0d 9303	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 # 0)
154	4	nnzd 9720	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑄 pCnt 𝐴) ∈ ℤ)
155	152, 153, 154	expm1apd 11073	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄↑((𝑄 pCnt 𝐴) − 1)) = ((𝑄↑(𝑄 pCnt 𝐴)) / 𝑄))
156	155	oveq2d 6074	. . . . . . . . 9 ⊢ (𝜑 → (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) = (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · ((𝑄↑(𝑄 pCnt 𝐴)) / 𝑄)))
157	135, 6	nndivred 9307	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℝ)
158	157	recnd 8318	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℂ)
159	158, 120, 152, 153	divassapd 9120	. . . . . . . . 9 ⊢ (𝜑 → ((((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) / 𝑄) = (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · ((𝑄↑(𝑄 pCnt 𝐴)) / 𝑄)))
160	122	oveq1d 6073	. . . . . . . . 9 ⊢ (𝜑 → ((((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) / 𝑄) = ((𝑁 − 1) / 𝑄))
161	156, 159, 160	3eqtr2d 2273	. . . . . . . 8 ⊢ (𝜑 → (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) = ((𝑁 − 1) / 𝑄))
162	161	breq2d 4126	. . . . . . 7 ⊢ (𝜑 → (((od_ℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) ↔ ((od_ℤ‘𝑃)‘𝐶) ∥ ((𝑁 − 1) / 𝑄)))
163	151, 162	bitr4d 191	. . . . . 6 ⊢ (𝜑 → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ↔ ((od_ℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1)))))
164		pockthlem.11	. . . . . . 7 ⊢ (𝜑 → (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁) = 1)
165	164	breq2d 4126	. . . . . 6 ⊢ (𝜑 → (𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁) ↔ 𝑃 ∥ 1))
166	149, 163, 165	3imtr3d 202	. . . . 5 ⊢ (𝜑 → (((od_ℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) → 𝑃 ∥ 1))
167	125, 166	mtod 669	. . . 4 ⊢ (𝜑 → ¬ ((od_ℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))))
168		prmpwdvds 13081	. . . 4 ⊢ (((((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ ∧ ((od_ℤ‘𝑃)‘𝐶) ∈ ℤ) ∧ (𝑄 ∈ ℙ ∧ (𝑄 pCnt 𝐴) ∈ ℕ) ∧ (((od_ℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) ∧ ¬ ((od_ℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))))) → (𝑄↑(𝑄 pCnt 𝐴)) ∥ ((od_ℤ‘𝑃)‘𝐶))
169	102, 76, 1, 4, 123, 167, 168	syl222anc 1290	. . 3 ⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ ((od_ℤ‘𝑃)‘𝐶))
170		odzphi 12972	. . . . 5 ⊢ ((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) → ((od_ℤ‘𝑃)‘𝐶) ∥ (ϕ‘𝑃))
171	10, 11, 73, 170	syl3anc 1274	. . . 4 ⊢ (𝜑 → ((od_ℤ‘𝑃)‘𝐶) ∥ (ϕ‘𝑃))
172		phiprm 12948	. . . . 5 ⊢ (𝑃 ∈ ℙ → (ϕ‘𝑃) = (𝑃 − 1))
173	8, 172	syl 14	. . . 4 ⊢ (𝜑 → (ϕ‘𝑃) = (𝑃 − 1))
174	171, 173	breqtrd 4140	. . 3 ⊢ (𝜑 → ((od_ℤ‘𝑃)‘𝐶) ∥ (𝑃 − 1))
175	7, 76, 83, 169, 174	dvdstrd 12544	. 2 ⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1))
176		pcdvdsb 13046	. . 3 ⊢ ((𝑄 ∈ ℙ ∧ (𝑃 − 1) ∈ ℤ ∧ (𝑄 pCnt 𝐴) ∈ ℕ₀) → ((𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1)) ↔ (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1)))
177	1, 83, 5, 176	syl3anc 1274	. 2 ⊢ (𝜑 → ((𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1)) ↔ (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1)))
178	175, 177	mpbird 167	1 ⊢ (𝜑 → (𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1)))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 = wceq 1398 ∈ wcel 2205 ≠ wne 2414 class class class wbr 4114 ‘cfv 5357 (class class class)co 6058 ℂcc 8141 ℝcr 8142 0cc0 8143 1c1 8144 + caddc 8146 · cmul 8148 < clt 8324 ≤ cle 8325 − cmin 8461 / cdiv 8966 ℕcn 9257 2c2 9308 ℕ₀cn0 9516 ℤcz 9597 ℤ_≥cuz 9874 ℚcq 9972 mod cmo 10711 ↑cexp 10927 ∥ cdvds 12501 gcd cgcd 12677 ℙcprime 12832 od_ℤcodz 12933 ϕcphi 12934 pCnt cpc 13010

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2207 ax-14 2208 ax-ext 2216 ax-coll 4230 ax-sep 4233 ax-nul 4241 ax-pow 4292 ax-pr 4327 ax-un 4559 ax-setind 4664 ax-iinf 4715 ax-cnex 8234 ax-resscn 8235 ax-1cn 8236 ax-1re 8237 ax-icn 8238 ax-addcl 8239 ax-addrcl 8240 ax-mulcl 8241 ax-mulrcl 8242 ax-addcom 8243 ax-mulcom 8244 ax-addass 8245 ax-mulass 8246 ax-distr 8247 ax-i2m1 8248 ax-0lt1 8249 ax-1rid 8250 ax-0id 8251 ax-rnegex 8252 ax-precex 8253 ax-cnre 8254 ax-pre-ltirr 8255 ax-pre-ltwlin 8256 ax-pre-lttrn 8257 ax-pre-apti 8258 ax-pre-ltadd 8259 ax-pre-mulgt0 8260 ax-pre-mulext 8261 ax-arch 8262 ax-caucvg 8263

This theorem depends on definitions: df-bi 117 df-stab 839 df-dc 843 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1812 df-eu 2085 df-mo 2086 df-clab 2221 df-cleq 2227 df-clel 2230 df-nfc 2375 df-ne 2415 df-nel 2510 df-ral 2527 df-rex 2528 df-reu 2529 df-rmo 2530 df-rab 2531 df-v 2817 df-sbc 3046 df-csb 3142 df-dif 3216 df-un 3218 df-in 3220 df-ss 3227 df-nul 3513 df-if 3625 df-pw 3676 df-sn 3700 df-pr 3701 df-op 3703 df-uni 3920 df-int 3955 df-iun 3998 df-br 4115 df-opab 4177 df-mpt 4178 df-tr 4214 df-id 4419 df-po 4422 df-iso 4423 df-iord 4492 df-on 4494 df-ilim 4495 df-suc 4497 df-iom 4718 df-xp 4760 df-rel 4761 df-cnv 4762 df-co 4763 df-dm 4764 df-rn 4765 df-res 4766 df-ima 4767 df-iota 5317 df-fun 5359 df-fn 5360 df-f 5361 df-f1 5362 df-fo 5363 df-f1o 5364 df-fv 5365 df-isom 5366 df-riota 6011 df-ov 6061 df-oprab 6062 df-mpo 6063 df-1st 6347 df-2nd 6348 df-recs 6549 df-irdg 6614 df-frec 6635 df-1o 6660 df-2o 6661 df-oadd 6664 df-er 6780 df-en 6989 df-dom 6990 df-fin 6991 df-sup 7288 df-inf 7289 df-pnf 8326 df-mnf 8327 df-xr 8328 df-ltxr 8329 df-le 8330 df-sub 8463 df-neg 8464 df-reap 8867 df-ap 8874 df-div 8967 df-inn 9258 df-2 9316 df-3 9317 df-4 9318 df-n0 9517 df-z 9598 df-uz 9875 df-q 9973 df-rp 10008 df-fz 10365 df-fzo 10502 df-fl 10657 df-mod 10712 df-seqfrec 10837 df-exp 10928 df-ihash 11167 df-cj 11555 df-re 11556 df-im 11557 df-rsqrt 11711 df-abs 11712 df-clim 11992 df-proddc 12265 df-dvds 12502 df-gcd 12678 df-prm 12833 df-odz 12935 df-phi 12936 df-pc 13011

This theorem is referenced by: pockthg 13083

W3C validator