pockthlem - Intuitionistic Logic Explorer

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

Theorem pockthlem 12887

Description: Lemma for pockthg 12888. (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 12640	. . . . . 6 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ ℕ)
3	1, 2	syl 14	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ ℕ)
4		pockthlem.8	. . . . . 6 ⊢ (𝜑 → (𝑄 pCnt 𝐴) ∈ ℕ)
5	4	nnnn0d 9430	. . . . 5 ⊢ (𝜑 → (𝑄 pCnt 𝐴) ∈ ℕ₀)
6	3, 5	nnexpcld 10925	. . . 4 ⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∈ ℕ)
7	6	nnzd 9576	. . 3 ⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∈ ℤ)
8		pockthlem.5	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ ℙ)
9		prmnn 12640	. . . . . 6 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
10	8, 9	syl 14	. . . . 5 ⊢ (𝜑 → 𝑃 ∈ ℕ)
11		pockthlem.9	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ ℤ)
12	10	nnzd 9576	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ ℤ)
13		gcddvds 12492	. . . . . . . . . 10 ⊢ ((𝐶 ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑃))
14	11, 12, 13	syl2anc 411	. . . . . . . . 9 ⊢ (𝜑 → ((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑃))
15	14	simpld 112	. . . . . . . 8 ⊢ (𝜑 → (𝐶 gcd 𝑃) ∥ 𝐶)
16	11, 12	gcdcld 12497	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶 gcd 𝑃) ∈ ℕ₀)
17	16	nn0zd 9575	. . . . . . . . 9 ⊢ (𝜑 → (𝐶 gcd 𝑃) ∈ ℤ)
18		pockthg.4	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 = ((𝐴 · 𝐵) + 1))
19		pockthg.1	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ℕ)
20		pockthg.2	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ ℕ)
21	19, 20	nnmulcld 9167	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ)
22		nnuz 9766	. . . . . . . . . . . . . . . 16 ⊢ ℕ = (ℤ_≥‘1)
23	21, 22	eleqtrdi 2322	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ (ℤ_≥‘1))
24		eluzp1p1 9756	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 · 𝐵) ∈ (ℤ_≥‘1) → ((𝐴 · 𝐵) + 1) ∈ (ℤ_≥‘(1 + 1)))
25	23, 24	syl 14	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 · 𝐵) + 1) ∈ (ℤ_≥‘(1 + 1)))
26	18, 25	eqeltrd 2306	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(1 + 1)))
27		df-2 9177	. . . . . . . . . . . . . 14 ⊢ 2 = (1 + 1)
28	27	fveq2i 5632	. . . . . . . . . . . . 13 ⊢ (ℤ_≥‘2) = (ℤ_≥‘(1 + 1))
29	26, 28	eleqtrrdi 2323	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘2))
30		eluz2b2 9806	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘2) ↔ (𝑁 ∈ ℕ ∧ 1 < 𝑁))
31	29, 30	sylib 122	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 1 < 𝑁))
32	31	simpld 112	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℕ)
33	32	nnzd 9576	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℤ)
34	14	simprd 114	. . . . . . . . 9 ⊢ (𝜑 → (𝐶 gcd 𝑃) ∥ 𝑃)
35		pockthlem.6	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 ∥ 𝑁)
36	17, 12, 33, 34, 35	dvdstrd 12349	. . . . . . . 8 ⊢ (𝜑 → (𝐶 gcd 𝑃) ∥ 𝑁)
37	32	nnne0d 9163	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ≠ 0)
38		simpr 110	. . . . . . . . . . 11 ⊢ ((𝐶 = 0 ∧ 𝑁 = 0) → 𝑁 = 0)
39	38	necon3ai 2449	. . . . . . . . . 10 ⊢ (𝑁 ≠ 0 → ¬ (𝐶 = 0 ∧ 𝑁 = 0))
40	37, 39	syl 14	. . . . . . . . 9 ⊢ (𝜑 → ¬ (𝐶 = 0 ∧ 𝑁 = 0))
41		dvdslegcd 12493	. . . . . . . . 9 ⊢ ((((𝐶 gcd 𝑃) ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝐶 = 0 ∧ 𝑁 = 0)) → (((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑁) → (𝐶 gcd 𝑃) ≤ (𝐶 gcd 𝑁)))
42	17, 11, 33, 40, 41	syl31anc 1274	. . . . . . . 8 ⊢ (𝜑 → (((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑁) → (𝐶 gcd 𝑃) ≤ (𝐶 gcd 𝑁)))
43	15, 36, 42	mp2and 433	. . . . . . 7 ⊢ (𝜑 → (𝐶 gcd 𝑃) ≤ (𝐶 gcd 𝑁))
44		pockthlem.10	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) mod 𝑁) = 1)
45	44	oveq1d 6022	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶↑(𝑁 − 1)) mod 𝑁) gcd 𝑁) = (1 gcd 𝑁))
46		1z 9480	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℤ
47		eluzp1m1 9754	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℤ ∧ 𝑁 ∈ (ℤ_≥‘(1 + 1))) → (𝑁 − 1) ∈ (ℤ_≥‘1))
48	46, 26, 47	sylancr 414	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 − 1) ∈ (ℤ_≥‘1))
49	48, 22	eleqtrrdi 2323	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 − 1) ∈ ℕ)
50	49	nnnn0d 9430	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 − 1) ∈ ℕ₀)
51		zexpcl 10784	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ ℤ ∧ (𝑁 − 1) ∈ ℕ₀) → (𝐶↑(𝑁 − 1)) ∈ ℤ)
52	11, 50, 51	syl2anc 411	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶↑(𝑁 − 1)) ∈ ℤ)
53		modgcd 12520	. . . . . . . . . 10 ⊢ (((𝐶↑(𝑁 − 1)) ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐶↑(𝑁 − 1)) mod 𝑁) gcd 𝑁) = ((𝐶↑(𝑁 − 1)) gcd 𝑁))
54	52, 32, 53	syl2anc 411	. . . . . . . . 9 ⊢ (𝜑 → (((𝐶↑(𝑁 − 1)) mod 𝑁) gcd 𝑁) = ((𝐶↑(𝑁 − 1)) gcd 𝑁))
55		gcdcom 12502	. . . . . . . . . . 11 ⊢ ((1 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (1 gcd 𝑁) = (𝑁 gcd 1))
56	46, 33, 55	sylancr 414	. . . . . . . . . 10 ⊢ (𝜑 → (1 gcd 𝑁) = (𝑁 gcd 1))
57		gcd1 12516	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℤ → (𝑁 gcd 1) = 1)
58	33, 57	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 gcd 1) = 1)
59	56, 58	eqtrd 2262	. . . . . . . . 9 ⊢ (𝜑 → (1 gcd 𝑁) = 1)
60	45, 54, 59	3eqtr3d 2270	. . . . . . . 8 ⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) gcd 𝑁) = 1)
61		rpexp 12683	. . . . . . . . 9 ⊢ ((𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁 − 1) ∈ ℕ) → (((𝐶↑(𝑁 − 1)) gcd 𝑁) = 1 ↔ (𝐶 gcd 𝑁) = 1))
62	11, 33, 49, 61	syl3anc 1271	. . . . . . . 8 ⊢ (𝜑 → (((𝐶↑(𝑁 − 1)) gcd 𝑁) = 1 ↔ (𝐶 gcd 𝑁) = 1))
63	60, 62	mpbid 147	. . . . . . 7 ⊢ (𝜑 → (𝐶 gcd 𝑁) = 1)
64	43, 63	breqtrd 4109	. . . . . 6 ⊢ (𝜑 → (𝐶 gcd 𝑃) ≤ 1)
65	10	nnne0d 9163	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 ≠ 0)
66		simpr 110	. . . . . . . . . 10 ⊢ ((𝐶 = 0 ∧ 𝑃 = 0) → 𝑃 = 0)
67	66	necon3ai 2449	. . . . . . . . 9 ⊢ (𝑃 ≠ 0 → ¬ (𝐶 = 0 ∧ 𝑃 = 0))
68	65, 67	syl 14	. . . . . . . 8 ⊢ (𝜑 → ¬ (𝐶 = 0 ∧ 𝑃 = 0))
69		gcdn0cl 12491	. . . . . . . 8 ⊢ (((𝐶 ∈ ℤ ∧ 𝑃 ∈ ℤ) ∧ ¬ (𝐶 = 0 ∧ 𝑃 = 0)) → (𝐶 gcd 𝑃) ∈ ℕ)
70	11, 12, 68, 69	syl21anc 1270	. . . . . . 7 ⊢ (𝜑 → (𝐶 gcd 𝑃) ∈ ℕ)
71		nnle1eq1 9142	. . . . . . 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 12774	. . . . 5 ⊢ ((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) → ((od_ℤ‘𝑃)‘𝐶) ∈ ℕ)
75	10, 11, 73, 74	syl3anc 1271	. . . 4 ⊢ (𝜑 → ((od_ℤ‘𝑃)‘𝐶) ∈ ℕ)
76	75	nnzd 9576	. . 3 ⊢ (𝜑 → ((od_ℤ‘𝑃)‘𝐶) ∈ ℤ)
77		prmuz2 12661	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ_≥‘2))
78	8, 77	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ (ℤ_≥‘2))
79	78, 28	eleqtrdi 2322	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ (ℤ_≥‘(1 + 1)))
80		eluzp1m1 9754	. . . . . 6 ⊢ ((1 ∈ ℤ ∧ 𝑃 ∈ (ℤ_≥‘(1 + 1))) → (𝑃 − 1) ∈ (ℤ_≥‘1))
81	46, 79, 80	sylancr 414	. . . . 5 ⊢ (𝜑 → (𝑃 − 1) ∈ (ℤ_≥‘1))
82	81, 22	eleqtrrdi 2323	. . . 4 ⊢ (𝜑 → (𝑃 − 1) ∈ ℕ)
83	82	nnzd 9576	. . 3 ⊢ (𝜑 → (𝑃 − 1) ∈ ℤ)
84	19	nnzd 9576	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ ℤ)
85	49	nnzd 9576	. . . . . 6 ⊢ (𝜑 → (𝑁 − 1) ∈ ℤ)
86		pcdvds 12846	. . . . . . 7 ⊢ ((𝑄 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (𝑄↑(𝑄 pCnt 𝐴)) ∥ 𝐴)
87	1, 19, 86	syl2anc 411	. . . . . 6 ⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ 𝐴)
88	20	nnzd 9576	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ ℤ)
89		dvdsmul1 12332	. . . . . . . 8 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∥ (𝐴 · 𝐵))
90	84, 88, 89	syl2anc 411	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∥ (𝐴 · 𝐵))
91	18	oveq1d 6022	. . . . . . . 8 ⊢ (𝜑 → (𝑁 − 1) = (((𝐴 · 𝐵) + 1) − 1))
92	21	nncnd 9132	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ)
93		ax-1cn 8100	. . . . . . . . 9 ⊢ 1 ∈ ℂ
94		pncan 8360	. . . . . . . . 9 ⊢ (((𝐴 · 𝐵) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐴 · 𝐵) + 1) − 1) = (𝐴 · 𝐵))
95	92, 93, 94	sylancl 413	. . . . . . . 8 ⊢ (𝜑 → (((𝐴 · 𝐵) + 1) − 1) = (𝐴 · 𝐵))
96	91, 95	eqtrd 2262	. . . . . . 7 ⊢ (𝜑 → (𝑁 − 1) = (𝐴 · 𝐵))
97	90, 96	breqtrrd 4111	. . . . . 6 ⊢ (𝜑 → 𝐴 ∥ (𝑁 − 1))
98	7, 84, 85, 87, 97	dvdstrd 12349	. . . . 5 ⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1))
99	6	nnne0d 9163	. . . . . 6 ⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ≠ 0)
100		dvdsval2 12309	. . . . . 6 ⊢ (((𝑄↑(𝑄 pCnt 𝐴)) ∈ ℤ ∧ (𝑄↑(𝑄 pCnt 𝐴)) ≠ 0 ∧ (𝑁 − 1) ∈ ℤ) → ((𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ))
101	7, 99, 85, 100	syl3anc 1271	. . . . 5 ⊢ (𝜑 → ((𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ))
102	98, 101	mpbid 147	. . . 4 ⊢ (𝜑 → ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ)
103		peano2zm 9492	. . . . . . . 8 ⊢ ((𝐶↑(𝑁 − 1)) ∈ ℤ → ((𝐶↑(𝑁 − 1)) − 1) ∈ ℤ)
104	52, 103	syl 14	. . . . . . 7 ⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) − 1) ∈ ℤ)
105		nnq 9836	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℚ)
106	32, 105	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℚ)
107	31	simprd 114	. . . . . . . . . 10 ⊢ (𝜑 → 1 < 𝑁)
108		q1mod 10586	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℚ ∧ 1 < 𝑁) → (1 mod 𝑁) = 1)
109	106, 107, 108	syl2anc 411	. . . . . . . . 9 ⊢ (𝜑 → (1 mod 𝑁) = 1)
110	44, 109	eqtr4d 2265	. . . . . . . 8 ⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁))
111		1zzd 9481	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℤ)
112		moddvds 12318	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ (𝐶↑(𝑁 − 1)) ∈ ℤ ∧ 1 ∈ ℤ) → (((𝐶↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1)))
113	32, 52, 111, 112	syl3anc 1271	. . . . . . . 8 ⊢ (𝜑 → (((𝐶↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1)))
114	110, 113	mpbid 147	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1))
115	12, 33, 104, 35, 114	dvdstrd 12349	. . . . . 6 ⊢ (𝜑 → 𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1))
116		odzdvds 12776	. . . . . . 7 ⊢ (((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) ∧ (𝑁 − 1) ∈ ℕ₀) → (𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1) ↔ ((od_ℤ‘𝑃)‘𝐶) ∥ (𝑁 − 1)))
117	10, 11, 73, 50, 116	syl31anc 1274	. . . . . 6 ⊢ (𝜑 → (𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1) ↔ ((od_ℤ‘𝑃)‘𝐶) ∥ (𝑁 − 1)))
118	115, 117	mpbid 147	. . . . 5 ⊢ (𝜑 → ((od_ℤ‘𝑃)‘𝐶) ∥ (𝑁 − 1))
119	49	nncnd 9132	. . . . . 6 ⊢ (𝜑 → (𝑁 − 1) ∈ ℂ)
120	6	nncnd 9132	. . . . . 6 ⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∈ ℂ)
121	6	nnap0d 9164	. . . . . 6 ⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) # 0)
122	119, 120, 121	divcanap1d 8946	. . . . 5 ⊢ (𝜑 → (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) = (𝑁 − 1))
123	118, 122	breqtrrd 4111	. . . 4 ⊢ (𝜑 → ((od_ℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))))
124		nprmdvds1 12670	. . . . . 6 ⊢ (𝑃 ∈ ℙ → ¬ 𝑃 ∥ 1)
125	8, 124	syl 14	. . . . 5 ⊢ (𝜑 → ¬ 𝑃 ∥ 1)
126	3	nnzd 9576	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 ∈ ℤ)
127		iddvdsexp 12334	. . . . . . . . . . . . . 14 ⊢ ((𝑄 ∈ ℤ ∧ (𝑄 pCnt 𝐴) ∈ ℕ) → 𝑄 ∥ (𝑄↑(𝑄 pCnt 𝐴)))
128	126, 4, 127	syl2anc 411	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 ∥ (𝑄↑(𝑄 pCnt 𝐴)))
129	126, 7, 85, 128, 98	dvdstrd 12349	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∥ (𝑁 − 1))
130	3	nnne0d 9163	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 ≠ 0)
131		dvdsval2 12309	. . . . . . . . . . . . 13 ⊢ ((𝑄 ∈ ℤ ∧ 𝑄 ≠ 0 ∧ (𝑁 − 1) ∈ ℤ) → (𝑄 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 𝑄) ∈ ℤ))
132	126, 130, 85, 131	syl3anc 1271	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 𝑄) ∈ ℤ))
133	129, 132	mpbid 147	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑁 − 1) / 𝑄) ∈ ℤ)
134	50	nn0ge0d 9433	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≤ (𝑁 − 1))
135	49	nnred 9131	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 − 1) ∈ ℝ)
136	3	nnred 9131	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 ∈ ℝ)
137	3	nngt0d 9162	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < 𝑄)
138		ge0div 9026	. . . . . . . . . . . . 13 ⊢ (((𝑁 − 1) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ 0 < 𝑄) → (0 ≤ (𝑁 − 1) ↔ 0 ≤ ((𝑁 − 1) / 𝑄)))
139	135, 136, 137, 138	syl3anc 1271	. . . . . . . . . . . 12 ⊢ (𝜑 → (0 ≤ (𝑁 − 1) ↔ 0 ≤ ((𝑁 − 1) / 𝑄)))
140	134, 139	mpbid 147	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ ((𝑁 − 1) / 𝑄))
141		elnn0z 9467	. . . . . . . . . . 11 ⊢ (((𝑁 − 1) / 𝑄) ∈ ℕ₀ ↔ (((𝑁 − 1) / 𝑄) ∈ ℤ ∧ 0 ≤ ((𝑁 − 1) / 𝑄)))
142	133, 140, 141	sylanbrc 417	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁 − 1) / 𝑄) ∈ ℕ₀)
143		zexpcl 10784	. . . . . . . . . 10 ⊢ ((𝐶 ∈ ℤ ∧ ((𝑁 − 1) / 𝑄) ∈ ℕ₀) → (𝐶↑((𝑁 − 1) / 𝑄)) ∈ ℤ)
144	11, 142, 143	syl2anc 411	. . . . . . . . 9 ⊢ (𝜑 → (𝐶↑((𝑁 − 1) / 𝑄)) ∈ ℤ)
145		peano2zm 9492	. . . . . . . . 9 ⊢ ((𝐶↑((𝑁 − 1) / 𝑄)) ∈ ℤ → ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∈ ℤ)
146	144, 145	syl 14	. . . . . . . 8 ⊢ (𝜑 → ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∈ ℤ)
147		dvdsgcd 12541	. . . . . . . 8 ⊢ ((𝑃 ∈ ℤ ∧ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∧ 𝑃 ∥ 𝑁) → 𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁)))
148	12, 146, 33, 147	syl3anc 1271	. . . . . . 7 ⊢ (𝜑 → ((𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∧ 𝑃 ∥ 𝑁) → 𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁)))
149	35, 148	mpan2d 428	. . . . . 6 ⊢ (𝜑 → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) → 𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁)))
150		odzdvds 12776	. . . . . . . 8 ⊢ (((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) ∧ ((𝑁 − 1) / 𝑄) ∈ ℕ₀) → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ↔ ((od_ℤ‘𝑃)‘𝐶) ∥ ((𝑁 − 1) / 𝑄)))
151	10, 11, 73, 142, 150	syl31anc 1274	. . . . . . 7 ⊢ (𝜑 → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ↔ ((od_ℤ‘𝑃)‘𝐶) ∥ ((𝑁 − 1) / 𝑄)))
152	3	nncnd 9132	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 ∈ ℂ)
153	3	nnap0d 9164	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄 # 0)
154	4	nnzd 9576	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑄 pCnt 𝐴) ∈ ℤ)
155	152, 153, 154	expm1apd 10913	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄↑((𝑄 pCnt 𝐴) − 1)) = ((𝑄↑(𝑄 pCnt 𝐴)) / 𝑄))
156	155	oveq2d 6023	. . . . . . . . 9 ⊢ (𝜑 → (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) = (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · ((𝑄↑(𝑄 pCnt 𝐴)) / 𝑄)))
157	135, 6	nndivred 9168	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℝ)
158	157	recnd 8183	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℂ)
159	158, 120, 152, 153	divassapd 8981	. . . . . . . . 9 ⊢ (𝜑 → ((((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) / 𝑄) = (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · ((𝑄↑(𝑄 pCnt 𝐴)) / 𝑄)))
160	122	oveq1d 6022	. . . . . . . . 9 ⊢ (𝜑 → ((((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) / 𝑄) = ((𝑁 − 1) / 𝑄))
161	156, 159, 160	3eqtr2d 2268	. . . . . . . 8 ⊢ (𝜑 → (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) = ((𝑁 − 1) / 𝑄))
162	161	breq2d 4095	. . . . . . 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 4095	. . . . . 6 ⊢ (𝜑 → (𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁) ↔ 𝑃 ∥ 1))
166	149, 163, 165	3imtr3d 202	. . . . 5 ⊢ (𝜑 → (((od_ℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) → 𝑃 ∥ 1))
167	125, 166	mtod 667	. . . 4 ⊢ (𝜑 → ¬ ((od_ℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))))
168		prmpwdvds 12886	. . . 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 1287	. . 3 ⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ ((od_ℤ‘𝑃)‘𝐶))
170		odzphi 12777	. . . . 5 ⊢ ((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) → ((od_ℤ‘𝑃)‘𝐶) ∥ (ϕ‘𝑃))
171	10, 11, 73, 170	syl3anc 1271	. . . 4 ⊢ (𝜑 → ((od_ℤ‘𝑃)‘𝐶) ∥ (ϕ‘𝑃))
172		phiprm 12753	. . . . 5 ⊢ (𝑃 ∈ ℙ → (ϕ‘𝑃) = (𝑃 − 1))
173	8, 172	syl 14	. . . 4 ⊢ (𝜑 → (ϕ‘𝑃) = (𝑃 − 1))
174	171, 173	breqtrd 4109	. . 3 ⊢ (𝜑 → ((od_ℤ‘𝑃)‘𝐶) ∥ (𝑃 − 1))
175	7, 76, 83, 169, 174	dvdstrd 12349	. 2 ⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1))
176		pcdvdsb 12851	. . 3 ⊢ ((𝑄 ∈ ℙ ∧ (𝑃 − 1) ∈ ℤ ∧ (𝑄 pCnt 𝐴) ∈ ℕ₀) → ((𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1)) ↔ (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1)))
177	1, 83, 5, 176	syl3anc 1271	. 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 1395 ∈ wcel 2200 ≠ wne 2400 class class class wbr 4083 ‘cfv 5318 (class class class)co 6007 ℂcc 8005 ℝcr 8006 0cc0 8007 1c1 8008 + caddc 8010 · cmul 8012 < clt 8189 ≤ cle 8190 − cmin 8325 / cdiv 8827 ℕcn 9118 2c2 9169 ℕ₀cn0 9377 ℤcz 9454 ℤ_≥cuz 9730 ℚcq 9822 mod cmo 10552 ↑cexp 10768 ∥ cdvds 12306 gcd cgcd 12482 ℙcprime 12637 od_ℤcodz 12738 ϕcphi 12739 pCnt cpc 12815

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 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-coll 4199 ax-sep 4202 ax-nul 4210 ax-pow 4258 ax-pr 4293 ax-un 4524 ax-setind 4629 ax-iinf 4680 ax-cnex 8098 ax-resscn 8099 ax-1cn 8100 ax-1re 8101 ax-icn 8102 ax-addcl 8103 ax-addrcl 8104 ax-mulcl 8105 ax-mulrcl 8106 ax-addcom 8107 ax-mulcom 8108 ax-addass 8109 ax-mulass 8110 ax-distr 8111 ax-i2m1 8112 ax-0lt1 8113 ax-1rid 8114 ax-0id 8115 ax-rnegex 8116 ax-precex 8117 ax-cnre 8118 ax-pre-ltirr 8119 ax-pre-ltwlin 8120 ax-pre-lttrn 8121 ax-pre-apti 8122 ax-pre-ltadd 8123 ax-pre-mulgt0 8124 ax-pre-mulext 8125 ax-arch 8126 ax-caucvg 8127

This theorem depends on definitions: df-bi 117 df-stab 836 df-dc 840 df-3or 1003 df-3an 1004 df-tru 1398 df-fal 1401 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ne 2401 df-nel 2496 df-ral 2513 df-rex 2514 df-reu 2515 df-rmo 2516 df-rab 2517 df-v 2801 df-sbc 3029 df-csb 3125 df-dif 3199 df-un 3201 df-in 3203 df-ss 3210 df-nul 3492 df-if 3603 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3889 df-int 3924 df-iun 3967 df-br 4084 df-opab 4146 df-mpt 4147 df-tr 4183 df-id 4384 df-po 4387 df-iso 4388 df-iord 4457 df-on 4459 df-ilim 4460 df-suc 4462 df-iom 4683 df-xp 4725 df-rel 4726 df-cnv 4727 df-co 4728 df-dm 4729 df-rn 4730 df-res 4731 df-ima 4732 df-iota 5278 df-fun 5320 df-fn 5321 df-f 5322 df-f1 5323 df-fo 5324 df-f1o 5325 df-fv 5326 df-isom 5327 df-riota 5960 df-ov 6010 df-oprab 6011 df-mpo 6012 df-1st 6292 df-2nd 6293 df-recs 6457 df-irdg 6522 df-frec 6543 df-1o 6568 df-2o 6569 df-oadd 6572 df-er 6688 df-en 6896 df-dom 6897 df-fin 6898 df-sup 7159 df-inf 7160 df-pnf 8191 df-mnf 8192 df-xr 8193 df-ltxr 8194 df-le 8195 df-sub 8327 df-neg 8328 df-reap 8730 df-ap 8737 df-div 8828 df-inn 9119 df-2 9177 df-3 9178 df-4 9179 df-n0 9378 df-z 9455 df-uz 9731 df-q 9823 df-rp 9858 df-fz 10213 df-fzo 10347 df-fl 10498 df-mod 10553 df-seqfrec 10678 df-exp 10769 df-ihash 11006 df-cj 11361 df-re 11362 df-im 11363 df-rsqrt 11517 df-abs 11518 df-clim 11798 df-proddc 12070 df-dvds 12307 df-gcd 12483 df-prm 12638 df-odz 12740 df-phi 12741 df-pc 12816

This theorem is referenced by: pockthg 12888

W3C validator