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

Theorem pockthlem 12301
Description: Lemma for pockthg 12302. (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
StepHypRef Expression
1 pockthlem.7 . . . . . 6 (𝜑𝑄 ∈ ℙ)
2 prmnn 12057 . . . . . 6 (𝑄 ∈ ℙ → 𝑄 ∈ ℕ)
31, 2syl 14 . . . . 5 (𝜑𝑄 ∈ ℕ)
4 pockthlem.8 . . . . . 6 (𝜑 → (𝑄 pCnt 𝐴) ∈ ℕ)
54nnnn0d 9181 . . . . 5 (𝜑 → (𝑄 pCnt 𝐴) ∈ ℕ0)
63, 5nnexpcld 10624 . . . 4 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∈ ℕ)
76nnzd 9326 . . 3 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∈ ℤ)
8 pockthlem.5 . . . . . 6 (𝜑𝑃 ∈ ℙ)
9 prmnn 12057 . . . . . 6 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
108, 9syl 14 . . . . 5 (𝜑𝑃 ∈ ℕ)
11 pockthlem.9 . . . . 5 (𝜑𝐶 ∈ ℤ)
1210nnzd 9326 . . . . . . . . . 10 (𝜑𝑃 ∈ ℤ)
13 gcddvds 11911 . . . . . . . . . 10 ((𝐶 ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑃))
1411, 12, 13syl2anc 409 . . . . . . . . 9 (𝜑 → ((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑃))
1514simpld 111 . . . . . . . 8 (𝜑 → (𝐶 gcd 𝑃) ∥ 𝐶)
1611, 12gcdcld 11916 . . . . . . . . . 10 (𝜑 → (𝐶 gcd 𝑃) ∈ ℕ0)
1716nn0zd 9325 . . . . . . . . 9 (𝜑 → (𝐶 gcd 𝑃) ∈ ℤ)
18 pockthg.4 . . . . . . . . . . . . . 14 (𝜑𝑁 = ((𝐴 · 𝐵) + 1))
19 pockthg.1 . . . . . . . . . . . . . . . . 17 (𝜑𝐴 ∈ ℕ)
20 pockthg.2 . . . . . . . . . . . . . . . . 17 (𝜑𝐵 ∈ ℕ)
2119, 20nnmulcld 8920 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴 · 𝐵) ∈ ℕ)
22 nnuz 9515 . . . . . . . . . . . . . . . 16 ℕ = (ℤ‘1)
2321, 22eleqtrdi 2263 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 · 𝐵) ∈ (ℤ‘1))
24 eluzp1p1 9505 . . . . . . . . . . . . . . 15 ((𝐴 · 𝐵) ∈ (ℤ‘1) → ((𝐴 · 𝐵) + 1) ∈ (ℤ‘(1 + 1)))
2523, 24syl 14 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴 · 𝐵) + 1) ∈ (ℤ‘(1 + 1)))
2618, 25eqeltrd 2247 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ (ℤ‘(1 + 1)))
27 df-2 8930 . . . . . . . . . . . . . 14 2 = (1 + 1)
2827fveq2i 5497 . . . . . . . . . . . . 13 (ℤ‘2) = (ℤ‘(1 + 1))
2926, 28eleqtrrdi 2264 . . . . . . . . . . . 12 (𝜑𝑁 ∈ (ℤ‘2))
30 eluz2b2 9555 . . . . . . . . . . . 12 (𝑁 ∈ (ℤ‘2) ↔ (𝑁 ∈ ℕ ∧ 1 < 𝑁))
3129, 30sylib 121 . . . . . . . . . . 11 (𝜑 → (𝑁 ∈ ℕ ∧ 1 < 𝑁))
3231simpld 111 . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ)
3332nnzd 9326 . . . . . . . . 9 (𝜑𝑁 ∈ ℤ)
3414simprd 113 . . . . . . . . 9 (𝜑 → (𝐶 gcd 𝑃) ∥ 𝑃)
35 pockthlem.6 . . . . . . . . 9 (𝜑𝑃𝑁)
3617, 12, 33, 34, 35dvdstrd 11785 . . . . . . . 8 (𝜑 → (𝐶 gcd 𝑃) ∥ 𝑁)
3732nnne0d 8916 . . . . . . . . . 10 (𝜑𝑁 ≠ 0)
38 simpr 109 . . . . . . . . . . 11 ((𝐶 = 0 ∧ 𝑁 = 0) → 𝑁 = 0)
3938necon3ai 2389 . . . . . . . . . 10 (𝑁 ≠ 0 → ¬ (𝐶 = 0 ∧ 𝑁 = 0))
4037, 39syl 14 . . . . . . . . 9 (𝜑 → ¬ (𝐶 = 0 ∧ 𝑁 = 0))
41 dvdslegcd 11912 . . . . . . . . 9 ((((𝐶 gcd 𝑃) ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝐶 = 0 ∧ 𝑁 = 0)) → (((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑁) → (𝐶 gcd 𝑃) ≤ (𝐶 gcd 𝑁)))
4217, 11, 33, 40, 41syl31anc 1236 . . . . . . . 8 (𝜑 → (((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑁) → (𝐶 gcd 𝑃) ≤ (𝐶 gcd 𝑁)))
4315, 36, 42mp2and 431 . . . . . . 7 (𝜑 → (𝐶 gcd 𝑃) ≤ (𝐶 gcd 𝑁))
44 pockthlem.10 . . . . . . . . . 10 (𝜑 → ((𝐶↑(𝑁 − 1)) mod 𝑁) = 1)
4544oveq1d 5866 . . . . . . . . 9 (𝜑 → (((𝐶↑(𝑁 − 1)) mod 𝑁) gcd 𝑁) = (1 gcd 𝑁))
46 1z 9231 . . . . . . . . . . . . . 14 1 ∈ ℤ
47 eluzp1m1 9503 . . . . . . . . . . . . . 14 ((1 ∈ ℤ ∧ 𝑁 ∈ (ℤ‘(1 + 1))) → (𝑁 − 1) ∈ (ℤ‘1))
4846, 26, 47sylancr 412 . . . . . . . . . . . . 13 (𝜑 → (𝑁 − 1) ∈ (ℤ‘1))
4948, 22eleqtrrdi 2264 . . . . . . . . . . . 12 (𝜑 → (𝑁 − 1) ∈ ℕ)
5049nnnn0d 9181 . . . . . . . . . . 11 (𝜑 → (𝑁 − 1) ∈ ℕ0)
51 zexpcl 10484 . . . . . . . . . . 11 ((𝐶 ∈ ℤ ∧ (𝑁 − 1) ∈ ℕ0) → (𝐶↑(𝑁 − 1)) ∈ ℤ)
5211, 50, 51syl2anc 409 . . . . . . . . . 10 (𝜑 → (𝐶↑(𝑁 − 1)) ∈ ℤ)
53 modgcd 11939 . . . . . . . . . 10 (((𝐶↑(𝑁 − 1)) ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐶↑(𝑁 − 1)) mod 𝑁) gcd 𝑁) = ((𝐶↑(𝑁 − 1)) gcd 𝑁))
5452, 32, 53syl2anc 409 . . . . . . . . 9 (𝜑 → (((𝐶↑(𝑁 − 1)) mod 𝑁) gcd 𝑁) = ((𝐶↑(𝑁 − 1)) gcd 𝑁))
55 gcdcom 11921 . . . . . . . . . . 11 ((1 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (1 gcd 𝑁) = (𝑁 gcd 1))
5646, 33, 55sylancr 412 . . . . . . . . . 10 (𝜑 → (1 gcd 𝑁) = (𝑁 gcd 1))
57 gcd1 11935 . . . . . . . . . . 11 (𝑁 ∈ ℤ → (𝑁 gcd 1) = 1)
5833, 57syl 14 . . . . . . . . . 10 (𝜑 → (𝑁 gcd 1) = 1)
5956, 58eqtrd 2203 . . . . . . . . 9 (𝜑 → (1 gcd 𝑁) = 1)
6045, 54, 593eqtr3d 2211 . . . . . . . 8 (𝜑 → ((𝐶↑(𝑁 − 1)) gcd 𝑁) = 1)
61 rpexp 12100 . . . . . . . . 9 ((𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁 − 1) ∈ ℕ) → (((𝐶↑(𝑁 − 1)) gcd 𝑁) = 1 ↔ (𝐶 gcd 𝑁) = 1))
6211, 33, 49, 61syl3anc 1233 . . . . . . . 8 (𝜑 → (((𝐶↑(𝑁 − 1)) gcd 𝑁) = 1 ↔ (𝐶 gcd 𝑁) = 1))
6360, 62mpbid 146 . . . . . . 7 (𝜑 → (𝐶 gcd 𝑁) = 1)
6443, 63breqtrd 4013 . . . . . 6 (𝜑 → (𝐶 gcd 𝑃) ≤ 1)
6510nnne0d 8916 . . . . . . . . 9 (𝜑𝑃 ≠ 0)
66 simpr 109 . . . . . . . . . 10 ((𝐶 = 0 ∧ 𝑃 = 0) → 𝑃 = 0)
6766necon3ai 2389 . . . . . . . . 9 (𝑃 ≠ 0 → ¬ (𝐶 = 0 ∧ 𝑃 = 0))
6865, 67syl 14 . . . . . . . 8 (𝜑 → ¬ (𝐶 = 0 ∧ 𝑃 = 0))
69 gcdn0cl 11910 . . . . . . . 8 (((𝐶 ∈ ℤ ∧ 𝑃 ∈ ℤ) ∧ ¬ (𝐶 = 0 ∧ 𝑃 = 0)) → (𝐶 gcd 𝑃) ∈ ℕ)
7011, 12, 68, 69syl21anc 1232 . . . . . . 7 (𝜑 → (𝐶 gcd 𝑃) ∈ ℕ)
71 nnle1eq1 8895 . . . . . . 7 ((𝐶 gcd 𝑃) ∈ ℕ → ((𝐶 gcd 𝑃) ≤ 1 ↔ (𝐶 gcd 𝑃) = 1))
7270, 71syl 14 . . . . . 6 (𝜑 → ((𝐶 gcd 𝑃) ≤ 1 ↔ (𝐶 gcd 𝑃) = 1))
7364, 72mpbid 146 . . . . 5 (𝜑 → (𝐶 gcd 𝑃) = 1)
74 odzcl 12190 . . . . 5 ((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) → ((od𝑃)‘𝐶) ∈ ℕ)
7510, 11, 73, 74syl3anc 1233 . . . 4 (𝜑 → ((od𝑃)‘𝐶) ∈ ℕ)
7675nnzd 9326 . . 3 (𝜑 → ((od𝑃)‘𝐶) ∈ ℤ)
77 prmuz2 12078 . . . . . . . 8 (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ‘2))
788, 77syl 14 . . . . . . 7 (𝜑𝑃 ∈ (ℤ‘2))
7978, 28eleqtrdi 2263 . . . . . 6 (𝜑𝑃 ∈ (ℤ‘(1 + 1)))
80 eluzp1m1 9503 . . . . . 6 ((1 ∈ ℤ ∧ 𝑃 ∈ (ℤ‘(1 + 1))) → (𝑃 − 1) ∈ (ℤ‘1))
8146, 79, 80sylancr 412 . . . . 5 (𝜑 → (𝑃 − 1) ∈ (ℤ‘1))
8281, 22eleqtrrdi 2264 . . . 4 (𝜑 → (𝑃 − 1) ∈ ℕ)
8382nnzd 9326 . . 3 (𝜑 → (𝑃 − 1) ∈ ℤ)
8419nnzd 9326 . . . . . 6 (𝜑𝐴 ∈ ℤ)
8549nnzd 9326 . . . . . 6 (𝜑 → (𝑁 − 1) ∈ ℤ)
86 pcdvds 12261 . . . . . . 7 ((𝑄 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (𝑄↑(𝑄 pCnt 𝐴)) ∥ 𝐴)
871, 19, 86syl2anc 409 . . . . . 6 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ 𝐴)
8820nnzd 9326 . . . . . . . 8 (𝜑𝐵 ∈ ℤ)
89 dvdsmul1 11768 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∥ (𝐴 · 𝐵))
9084, 88, 89syl2anc 409 . . . . . . 7 (𝜑𝐴 ∥ (𝐴 · 𝐵))
9118oveq1d 5866 . . . . . . . 8 (𝜑 → (𝑁 − 1) = (((𝐴 · 𝐵) + 1) − 1))
9221nncnd 8885 . . . . . . . . 9 (𝜑 → (𝐴 · 𝐵) ∈ ℂ)
93 ax-1cn 7860 . . . . . . . . 9 1 ∈ ℂ
94 pncan 8118 . . . . . . . . 9 (((𝐴 · 𝐵) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐴 · 𝐵) + 1) − 1) = (𝐴 · 𝐵))
9592, 93, 94sylancl 411 . . . . . . . 8 (𝜑 → (((𝐴 · 𝐵) + 1) − 1) = (𝐴 · 𝐵))
9691, 95eqtrd 2203 . . . . . . 7 (𝜑 → (𝑁 − 1) = (𝐴 · 𝐵))
9790, 96breqtrrd 4015 . . . . . 6 (𝜑𝐴 ∥ (𝑁 − 1))
987, 84, 85, 87, 97dvdstrd 11785 . . . . 5 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1))
996nnne0d 8916 . . . . . 6 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ≠ 0)
100 dvdsval2 11745 . . . . . 6 (((𝑄↑(𝑄 pCnt 𝐴)) ∈ ℤ ∧ (𝑄↑(𝑄 pCnt 𝐴)) ≠ 0 ∧ (𝑁 − 1) ∈ ℤ) → ((𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ))
1017, 99, 85, 100syl3anc 1233 . . . . 5 (𝜑 → ((𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ))
10298, 101mpbid 146 . . . 4 (𝜑 → ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ)
103 peano2zm 9243 . . . . . . . 8 ((𝐶↑(𝑁 − 1)) ∈ ℤ → ((𝐶↑(𝑁 − 1)) − 1) ∈ ℤ)
10452, 103syl 14 . . . . . . 7 (𝜑 → ((𝐶↑(𝑁 − 1)) − 1) ∈ ℤ)
105 nnq 9585 . . . . . . . . . . 11 (𝑁 ∈ ℕ → 𝑁 ∈ ℚ)
10632, 105syl 14 . . . . . . . . . 10 (𝜑𝑁 ∈ ℚ)
10731simprd 113 . . . . . . . . . 10 (𝜑 → 1 < 𝑁)
108 q1mod 10305 . . . . . . . . . 10 ((𝑁 ∈ ℚ ∧ 1 < 𝑁) → (1 mod 𝑁) = 1)
109106, 107, 108syl2anc 409 . . . . . . . . 9 (𝜑 → (1 mod 𝑁) = 1)
11044, 109eqtr4d 2206 . . . . . . . 8 (𝜑 → ((𝐶↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁))
111 1zzd 9232 . . . . . . . . 9 (𝜑 → 1 ∈ ℤ)
112 moddvds 11754 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ (𝐶↑(𝑁 − 1)) ∈ ℤ ∧ 1 ∈ ℤ) → (((𝐶↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1)))
11332, 52, 111, 112syl3anc 1233 . . . . . . . 8 (𝜑 → (((𝐶↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1)))
114110, 113mpbid 146 . . . . . . 7 (𝜑𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1))
11512, 33, 104, 35, 114dvdstrd 11785 . . . . . 6 (𝜑𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1))
116 odzdvds 12192 . . . . . . 7 (((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) ∧ (𝑁 − 1) ∈ ℕ0) → (𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1) ↔ ((od𝑃)‘𝐶) ∥ (𝑁 − 1)))
11710, 11, 73, 50, 116syl31anc 1236 . . . . . 6 (𝜑 → (𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1) ↔ ((od𝑃)‘𝐶) ∥ (𝑁 − 1)))
118115, 117mpbid 146 . . . . 5 (𝜑 → ((od𝑃)‘𝐶) ∥ (𝑁 − 1))
11949nncnd 8885 . . . . . 6 (𝜑 → (𝑁 − 1) ∈ ℂ)
1206nncnd 8885 . . . . . 6 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∈ ℂ)
1216nnap0d 8917 . . . . . 6 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) # 0)
122119, 120, 121divcanap1d 8701 . . . . 5 (𝜑 → (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) = (𝑁 − 1))
123118, 122breqtrrd 4015 . . . 4 (𝜑 → ((od𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))))
124 nprmdvds1 12087 . . . . . 6 (𝑃 ∈ ℙ → ¬ 𝑃 ∥ 1)
1258, 124syl 14 . . . . 5 (𝜑 → ¬ 𝑃 ∥ 1)
1263nnzd 9326 . . . . . . . . . . . . 13 (𝜑𝑄 ∈ ℤ)
127 iddvdsexp 11770 . . . . . . . . . . . . . 14 ((𝑄 ∈ ℤ ∧ (𝑄 pCnt 𝐴) ∈ ℕ) → 𝑄 ∥ (𝑄↑(𝑄 pCnt 𝐴)))
128126, 4, 127syl2anc 409 . . . . . . . . . . . . 13 (𝜑𝑄 ∥ (𝑄↑(𝑄 pCnt 𝐴)))
129126, 7, 85, 128, 98dvdstrd 11785 . . . . . . . . . . . 12 (𝜑𝑄 ∥ (𝑁 − 1))
1303nnne0d 8916 . . . . . . . . . . . . 13 (𝜑𝑄 ≠ 0)
131 dvdsval2 11745 . . . . . . . . . . . . 13 ((𝑄 ∈ ℤ ∧ 𝑄 ≠ 0 ∧ (𝑁 − 1) ∈ ℤ) → (𝑄 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 𝑄) ∈ ℤ))
132126, 130, 85, 131syl3anc 1233 . . . . . . . . . . . 12 (𝜑 → (𝑄 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 𝑄) ∈ ℤ))
133129, 132mpbid 146 . . . . . . . . . . 11 (𝜑 → ((𝑁 − 1) / 𝑄) ∈ ℤ)
13450nn0ge0d 9184 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (𝑁 − 1))
13549nnred 8884 . . . . . . . . . . . . 13 (𝜑 → (𝑁 − 1) ∈ ℝ)
1363nnred 8884 . . . . . . . . . . . . 13 (𝜑𝑄 ∈ ℝ)
1373nngt0d 8915 . . . . . . . . . . . . 13 (𝜑 → 0 < 𝑄)
138 ge0div 8780 . . . . . . . . . . . . 13 (((𝑁 − 1) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ 0 < 𝑄) → (0 ≤ (𝑁 − 1) ↔ 0 ≤ ((𝑁 − 1) / 𝑄)))
139135, 136, 137, 138syl3anc 1233 . . . . . . . . . . . 12 (𝜑 → (0 ≤ (𝑁 − 1) ↔ 0 ≤ ((𝑁 − 1) / 𝑄)))
140134, 139mpbid 146 . . . . . . . . . . 11 (𝜑 → 0 ≤ ((𝑁 − 1) / 𝑄))
141 elnn0z 9218 . . . . . . . . . . 11 (((𝑁 − 1) / 𝑄) ∈ ℕ0 ↔ (((𝑁 − 1) / 𝑄) ∈ ℤ ∧ 0 ≤ ((𝑁 − 1) / 𝑄)))
142133, 140, 141sylanbrc 415 . . . . . . . . . 10 (𝜑 → ((𝑁 − 1) / 𝑄) ∈ ℕ0)
143 zexpcl 10484 . . . . . . . . . 10 ((𝐶 ∈ ℤ ∧ ((𝑁 − 1) / 𝑄) ∈ ℕ0) → (𝐶↑((𝑁 − 1) / 𝑄)) ∈ ℤ)
14411, 142, 143syl2anc 409 . . . . . . . . 9 (𝜑 → (𝐶↑((𝑁 − 1) / 𝑄)) ∈ ℤ)
145 peano2zm 9243 . . . . . . . . 9 ((𝐶↑((𝑁 − 1) / 𝑄)) ∈ ℤ → ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∈ ℤ)
146144, 145syl 14 . . . . . . . 8 (𝜑 → ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∈ ℤ)
147 dvdsgcd 11960 . . . . . . . 8 ((𝑃 ∈ ℤ ∧ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∧ 𝑃𝑁) → 𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁)))
14812, 146, 33, 147syl3anc 1233 . . . . . . 7 (𝜑 → ((𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∧ 𝑃𝑁) → 𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁)))
14935, 148mpan2d 426 . . . . . 6 (𝜑 → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) → 𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁)))
150 odzdvds 12192 . . . . . . . 8 (((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) ∧ ((𝑁 − 1) / 𝑄) ∈ ℕ0) → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ↔ ((od𝑃)‘𝐶) ∥ ((𝑁 − 1) / 𝑄)))
15110, 11, 73, 142, 150syl31anc 1236 . . . . . . 7 (𝜑 → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ↔ ((od𝑃)‘𝐶) ∥ ((𝑁 − 1) / 𝑄)))
1523nncnd 8885 . . . . . . . . . . 11 (𝜑𝑄 ∈ ℂ)
1533nnap0d 8917 . . . . . . . . . . 11 (𝜑𝑄 # 0)
1544nnzd 9326 . . . . . . . . . . 11 (𝜑 → (𝑄 pCnt 𝐴) ∈ ℤ)
155152, 153, 154expm1apd 10612 . . . . . . . . . 10 (𝜑 → (𝑄↑((𝑄 pCnt 𝐴) − 1)) = ((𝑄↑(𝑄 pCnt 𝐴)) / 𝑄))
156155oveq2d 5867 . . . . . . . . 9 (𝜑 → (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) = (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · ((𝑄↑(𝑄 pCnt 𝐴)) / 𝑄)))
157135, 6nndivred 8921 . . . . . . . . . . 11 (𝜑 → ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℝ)
158157recnd 7941 . . . . . . . . . 10 (𝜑 → ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℂ)
159158, 120, 152, 153divassapd 8736 . . . . . . . . 9 (𝜑 → ((((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) / 𝑄) = (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · ((𝑄↑(𝑄 pCnt 𝐴)) / 𝑄)))
160122oveq1d 5866 . . . . . . . . 9 (𝜑 → ((((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) / 𝑄) = ((𝑁 − 1) / 𝑄))
161156, 159, 1603eqtr2d 2209 . . . . . . . 8 (𝜑 → (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) = ((𝑁 − 1) / 𝑄))
162161breq2d 3999 . . . . . . 7 (𝜑 → (((od𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) ↔ ((od𝑃)‘𝐶) ∥ ((𝑁 − 1) / 𝑄)))
163151, 162bitr4d 190 . . . . . 6 (𝜑 → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ↔ ((od𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1)))))
164 pockthlem.11 . . . . . . 7 (𝜑 → (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁) = 1)
165164breq2d 3999 . . . . . 6 (𝜑 → (𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁) ↔ 𝑃 ∥ 1))
166149, 163, 1653imtr3d 201 . . . . 5 (𝜑 → (((od𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) → 𝑃 ∥ 1))
167125, 166mtod 658 . . . 4 (𝜑 → ¬ ((od𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))))
168 prmpwdvds 12300 . . . 4 (((((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ ∧ ((od𝑃)‘𝐶) ∈ ℤ) ∧ (𝑄 ∈ ℙ ∧ (𝑄 pCnt 𝐴) ∈ ℕ) ∧ (((od𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) ∧ ¬ ((od𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))))) → (𝑄↑(𝑄 pCnt 𝐴)) ∥ ((od𝑃)‘𝐶))
169102, 76, 1, 4, 123, 167, 168syl222anc 1249 . . 3 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ ((od𝑃)‘𝐶))
170 odzphi 12193 . . . . 5 ((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) → ((od𝑃)‘𝐶) ∥ (ϕ‘𝑃))
17110, 11, 73, 170syl3anc 1233 . . . 4 (𝜑 → ((od𝑃)‘𝐶) ∥ (ϕ‘𝑃))
172 phiprm 12170 . . . . 5 (𝑃 ∈ ℙ → (ϕ‘𝑃) = (𝑃 − 1))
1738, 172syl 14 . . . 4 (𝜑 → (ϕ‘𝑃) = (𝑃 − 1))
174171, 173breqtrd 4013 . . 3 (𝜑 → ((od𝑃)‘𝐶) ∥ (𝑃 − 1))
1757, 76, 83, 169, 174dvdstrd 11785 . 2 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1))
176 pcdvdsb 12266 . . 3 ((𝑄 ∈ ℙ ∧ (𝑃 − 1) ∈ ℤ ∧ (𝑄 pCnt 𝐴) ∈ ℕ0) → ((𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1)) ↔ (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1)))
1771, 83, 5, 176syl3anc 1233 . 2 (𝜑 → ((𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1)) ↔ (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1)))
178175, 177mpbird 166 1 (𝜑 → (𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104   = wceq 1348  wcel 2141  wne 2340   class class class wbr 3987  cfv 5196  (class class class)co 5851  cc 7765  cr 7766  0cc0 7767  1c1 7768   + caddc 7770   · cmul 7772   < clt 7947  cle 7948  cmin 8083   / cdiv 8582  cn 8871  2c2 8922  0cn0 9128  cz 9205  cuz 9480  cq 9571   mod cmo 10271  cexp 10468  cdvds 11742   gcd cgcd 11890  cprime 12054  odcodz 12155  ϕcphi 12156   pCnt cpc 12231
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4102  ax-sep 4105  ax-nul 4113  ax-pow 4158  ax-pr 4192  ax-un 4416  ax-setind 4519  ax-iinf 4570  ax-cnex 7858  ax-resscn 7859  ax-1cn 7860  ax-1re 7861  ax-icn 7862  ax-addcl 7863  ax-addrcl 7864  ax-mulcl 7865  ax-mulrcl 7866  ax-addcom 7867  ax-mulcom 7868  ax-addass 7869  ax-mulass 7870  ax-distr 7871  ax-i2m1 7872  ax-0lt1 7873  ax-1rid 7874  ax-0id 7875  ax-rnegex 7876  ax-precex 7877  ax-cnre 7878  ax-pre-ltirr 7879  ax-pre-ltwlin 7880  ax-pre-lttrn 7881  ax-pre-apti 7882  ax-pre-ltadd 7883  ax-pre-mulgt0 7884  ax-pre-mulext 7885  ax-arch 7886  ax-caucvg 7887
This theorem depends on definitions:  df-bi 116  df-stab 826  df-dc 830  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-nel 2436  df-ral 2453  df-rex 2454  df-reu 2455  df-rmo 2456  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-if 3526  df-pw 3566  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-int 3830  df-iun 3873  df-br 3988  df-opab 4049  df-mpt 4050  df-tr 4086  df-id 4276  df-po 4279  df-iso 4280  df-iord 4349  df-on 4351  df-ilim 4352  df-suc 4354  df-iom 4573  df-xp 4615  df-rel 4616  df-cnv 4617  df-co 4618  df-dm 4619  df-rn 4620  df-res 4621  df-ima 4622  df-iota 5158  df-fun 5198  df-fn 5199  df-f 5200  df-f1 5201  df-fo 5202  df-f1o 5203  df-fv 5204  df-isom 5205  df-riota 5807  df-ov 5854  df-oprab 5855  df-mpo 5856  df-1st 6117  df-2nd 6118  df-recs 6282  df-irdg 6347  df-frec 6368  df-1o 6393  df-2o 6394  df-oadd 6397  df-er 6511  df-en 6717  df-dom 6718  df-fin 6719  df-sup 6959  df-inf 6960  df-pnf 7949  df-mnf 7950  df-xr 7951  df-ltxr 7952  df-le 7953  df-sub 8085  df-neg 8086  df-reap 8487  df-ap 8494  df-div 8583  df-inn 8872  df-2 8930  df-3 8931  df-4 8932  df-n0 9129  df-z 9206  df-uz 9481  df-q 9572  df-rp 9604  df-fz 9959  df-fzo 10092  df-fl 10219  df-mod 10272  df-seqfrec 10395  df-exp 10469  df-ihash 10703  df-cj 10799  df-re 10800  df-im 10801  df-rsqrt 10955  df-abs 10956  df-clim 11235  df-proddc 11507  df-dvds 11743  df-gcd 11891  df-prm 12055  df-odz 12157  df-phi 12158  df-pc 12232
This theorem is referenced by:  pockthg  12302
  Copyright terms: Public domain W3C validator