MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pockthlem Structured version   Visualization version   GIF version

Theorem pockthlem 16491
Description: Lemma for pockthg 16492. (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 16264 . . . . . 6 (𝑄 ∈ ℙ → 𝑄 ∈ ℕ)
31, 2syl 17 . . . . 5 (𝜑𝑄 ∈ ℕ)
4 pockthlem.8 . . . . . 6 (𝜑 → (𝑄 pCnt 𝐴) ∈ ℕ)
54nnnn0d 12180 . . . . 5 (𝜑 → (𝑄 pCnt 𝐴) ∈ ℕ0)
63, 5nnexpcld 13845 . . . 4 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∈ ℕ)
76nnzd 12311 . . 3 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∈ ℤ)
8 pockthlem.5 . . . . . 6 (𝜑𝑃 ∈ ℙ)
9 prmnn 16264 . . . . . 6 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
108, 9syl 17 . . . . 5 (𝜑𝑃 ∈ ℕ)
11 pockthlem.9 . . . . 5 (𝜑𝐶 ∈ ℤ)
1210nnzd 12311 . . . . . . . . . 10 (𝜑𝑃 ∈ ℤ)
13 gcddvds 16095 . . . . . . . . . 10 ((𝐶 ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑃))
1411, 12, 13syl2anc 587 . . . . . . . . 9 (𝜑 → ((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑃))
1514simpld 498 . . . . . . . 8 (𝜑 → (𝐶 gcd 𝑃) ∥ 𝐶)
1611, 12gcdcld 16100 . . . . . . . . . 10 (𝜑 → (𝐶 gcd 𝑃) ∈ ℕ0)
1716nn0zd 12310 . . . . . . . . 9 (𝜑 → (𝐶 gcd 𝑃) ∈ ℤ)
18 pockthg.4 . . . . . . . . . . . . . 14 (𝜑𝑁 = ((𝐴 · 𝐵) + 1))
19 pockthg.1 . . . . . . . . . . . . . . . . 17 (𝜑𝐴 ∈ ℕ)
20 pockthg.2 . . . . . . . . . . . . . . . . 17 (𝜑𝐵 ∈ ℕ)
2119, 20nnmulcld 11913 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴 · 𝐵) ∈ ℕ)
22 nnuz 12507 . . . . . . . . . . . . . . . 16 ℕ = (ℤ‘1)
2321, 22eleqtrdi 2850 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 · 𝐵) ∈ (ℤ‘1))
24 eluzp1p1 12496 . . . . . . . . . . . . . . 15 ((𝐴 · 𝐵) ∈ (ℤ‘1) → ((𝐴 · 𝐵) + 1) ∈ (ℤ‘(1 + 1)))
2523, 24syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴 · 𝐵) + 1) ∈ (ℤ‘(1 + 1)))
2618, 25eqeltrd 2840 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ (ℤ‘(1 + 1)))
27 df-2 11923 . . . . . . . . . . . . . 14 2 = (1 + 1)
2827fveq2i 6742 . . . . . . . . . . . . 13 (ℤ‘2) = (ℤ‘(1 + 1))
2926, 28eleqtrrdi 2851 . . . . . . . . . . . 12 (𝜑𝑁 ∈ (ℤ‘2))
30 eluz2b2 12547 . . . . . . . . . . . 12 (𝑁 ∈ (ℤ‘2) ↔ (𝑁 ∈ ℕ ∧ 1 < 𝑁))
3129, 30sylib 221 . . . . . . . . . . 11 (𝜑 → (𝑁 ∈ ℕ ∧ 1 < 𝑁))
3231simpld 498 . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ)
3332nnzd 12311 . . . . . . . . 9 (𝜑𝑁 ∈ ℤ)
3414simprd 499 . . . . . . . . 9 (𝜑 → (𝐶 gcd 𝑃) ∥ 𝑃)
35 pockthlem.6 . . . . . . . . 9 (𝜑𝑃𝑁)
3617, 12, 33, 34, 35dvdstrd 15889 . . . . . . . 8 (𝜑 → (𝐶 gcd 𝑃) ∥ 𝑁)
3732nnne0d 11910 . . . . . . . . . 10 (𝜑𝑁 ≠ 0)
38 simpr 488 . . . . . . . . . . 11 ((𝐶 = 0 ∧ 𝑁 = 0) → 𝑁 = 0)
3938necon3ai 2968 . . . . . . . . . 10 (𝑁 ≠ 0 → ¬ (𝐶 = 0 ∧ 𝑁 = 0))
4037, 39syl 17 . . . . . . . . 9 (𝜑 → ¬ (𝐶 = 0 ∧ 𝑁 = 0))
41 dvdslegcd 16096 . . . . . . . . 9 ((((𝐶 gcd 𝑃) ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝐶 = 0 ∧ 𝑁 = 0)) → (((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑁) → (𝐶 gcd 𝑃) ≤ (𝐶 gcd 𝑁)))
4217, 11, 33, 40, 41syl31anc 1375 . . . . . . . 8 (𝜑 → (((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑁) → (𝐶 gcd 𝑃) ≤ (𝐶 gcd 𝑁)))
4315, 36, 42mp2and 699 . . . . . . 7 (𝜑 → (𝐶 gcd 𝑃) ≤ (𝐶 gcd 𝑁))
44 pockthlem.10 . . . . . . . . . 10 (𝜑 → ((𝐶↑(𝑁 − 1)) mod 𝑁) = 1)
4544oveq1d 7250 . . . . . . . . 9 (𝜑 → (((𝐶↑(𝑁 − 1)) mod 𝑁) gcd 𝑁) = (1 gcd 𝑁))
46 1z 12237 . . . . . . . . . . . . . 14 1 ∈ ℤ
47 eluzp1m1 12494 . . . . . . . . . . . . . 14 ((1 ∈ ℤ ∧ 𝑁 ∈ (ℤ‘(1 + 1))) → (𝑁 − 1) ∈ (ℤ‘1))
4846, 26, 47sylancr 590 . . . . . . . . . . . . 13 (𝜑 → (𝑁 − 1) ∈ (ℤ‘1))
4948, 22eleqtrrdi 2851 . . . . . . . . . . . 12 (𝜑 → (𝑁 − 1) ∈ ℕ)
5049nnnn0d 12180 . . . . . . . . . . 11 (𝜑 → (𝑁 − 1) ∈ ℕ0)
51 zexpcl 13682 . . . . . . . . . . 11 ((𝐶 ∈ ℤ ∧ (𝑁 − 1) ∈ ℕ0) → (𝐶↑(𝑁 − 1)) ∈ ℤ)
5211, 50, 51syl2anc 587 . . . . . . . . . 10 (𝜑 → (𝐶↑(𝑁 − 1)) ∈ ℤ)
53 modgcd 16125 . . . . . . . . . 10 (((𝐶↑(𝑁 − 1)) ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐶↑(𝑁 − 1)) mod 𝑁) gcd 𝑁) = ((𝐶↑(𝑁 − 1)) gcd 𝑁))
5452, 32, 53syl2anc 587 . . . . . . . . 9 (𝜑 → (((𝐶↑(𝑁 − 1)) mod 𝑁) gcd 𝑁) = ((𝐶↑(𝑁 − 1)) gcd 𝑁))
55 gcdcom 16105 . . . . . . . . . . 11 ((1 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (1 gcd 𝑁) = (𝑁 gcd 1))
5646, 33, 55sylancr 590 . . . . . . . . . 10 (𝜑 → (1 gcd 𝑁) = (𝑁 gcd 1))
57 gcd1 16120 . . . . . . . . . . 11 (𝑁 ∈ ℤ → (𝑁 gcd 1) = 1)
5833, 57syl 17 . . . . . . . . . 10 (𝜑 → (𝑁 gcd 1) = 1)
5956, 58eqtrd 2779 . . . . . . . . 9 (𝜑 → (1 gcd 𝑁) = 1)
6045, 54, 593eqtr3d 2787 . . . . . . . 8 (𝜑 → ((𝐶↑(𝑁 − 1)) gcd 𝑁) = 1)
61 rpexp 16312 . . . . . . . . 9 ((𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁 − 1) ∈ ℕ) → (((𝐶↑(𝑁 − 1)) gcd 𝑁) = 1 ↔ (𝐶 gcd 𝑁) = 1))
6211, 33, 49, 61syl3anc 1373 . . . . . . . 8 (𝜑 → (((𝐶↑(𝑁 − 1)) gcd 𝑁) = 1 ↔ (𝐶 gcd 𝑁) = 1))
6360, 62mpbid 235 . . . . . . 7 (𝜑 → (𝐶 gcd 𝑁) = 1)
6443, 63breqtrd 5096 . . . . . 6 (𝜑 → (𝐶 gcd 𝑃) ≤ 1)
6510nnne0d 11910 . . . . . . . . 9 (𝜑𝑃 ≠ 0)
66 simpr 488 . . . . . . . . . 10 ((𝐶 = 0 ∧ 𝑃 = 0) → 𝑃 = 0)
6766necon3ai 2968 . . . . . . . . 9 (𝑃 ≠ 0 → ¬ (𝐶 = 0 ∧ 𝑃 = 0))
6865, 67syl 17 . . . . . . . 8 (𝜑 → ¬ (𝐶 = 0 ∧ 𝑃 = 0))
69 gcdn0cl 16094 . . . . . . . 8 (((𝐶 ∈ ℤ ∧ 𝑃 ∈ ℤ) ∧ ¬ (𝐶 = 0 ∧ 𝑃 = 0)) → (𝐶 gcd 𝑃) ∈ ℕ)
7011, 12, 68, 69syl21anc 838 . . . . . . 7 (𝜑 → (𝐶 gcd 𝑃) ∈ ℕ)
71 nnle1eq1 11890 . . . . . . 7 ((𝐶 gcd 𝑃) ∈ ℕ → ((𝐶 gcd 𝑃) ≤ 1 ↔ (𝐶 gcd 𝑃) = 1))
7270, 71syl 17 . . . . . 6 (𝜑 → ((𝐶 gcd 𝑃) ≤ 1 ↔ (𝐶 gcd 𝑃) = 1))
7364, 72mpbid 235 . . . . 5 (𝜑 → (𝐶 gcd 𝑃) = 1)
74 odzcl 16379 . . . . 5 ((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) → ((od𝑃)‘𝐶) ∈ ℕ)
7510, 11, 73, 74syl3anc 1373 . . . 4 (𝜑 → ((od𝑃)‘𝐶) ∈ ℕ)
7675nnzd 12311 . . 3 (𝜑 → ((od𝑃)‘𝐶) ∈ ℤ)
77 prmuz2 16286 . . . . . . . 8 (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ‘2))
788, 77syl 17 . . . . . . 7 (𝜑𝑃 ∈ (ℤ‘2))
7978, 28eleqtrdi 2850 . . . . . 6 (𝜑𝑃 ∈ (ℤ‘(1 + 1)))
80 eluzp1m1 12494 . . . . . 6 ((1 ∈ ℤ ∧ 𝑃 ∈ (ℤ‘(1 + 1))) → (𝑃 − 1) ∈ (ℤ‘1))
8146, 79, 80sylancr 590 . . . . 5 (𝜑 → (𝑃 − 1) ∈ (ℤ‘1))
8281, 22eleqtrrdi 2851 . . . 4 (𝜑 → (𝑃 − 1) ∈ ℕ)
8382nnzd 12311 . . 3 (𝜑 → (𝑃 − 1) ∈ ℤ)
8419nnzd 12311 . . . . . 6 (𝜑𝐴 ∈ ℤ)
8549nnzd 12311 . . . . . 6 (𝜑 → (𝑁 − 1) ∈ ℤ)
86 pcdvds 16450 . . . . . . 7 ((𝑄 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (𝑄↑(𝑄 pCnt 𝐴)) ∥ 𝐴)
871, 19, 86syl2anc 587 . . . . . 6 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ 𝐴)
8820nnzd 12311 . . . . . . . 8 (𝜑𝐵 ∈ ℤ)
89 dvdsmul1 15872 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∥ (𝐴 · 𝐵))
9084, 88, 89syl2anc 587 . . . . . . 7 (𝜑𝐴 ∥ (𝐴 · 𝐵))
9118oveq1d 7250 . . . . . . . 8 (𝜑 → (𝑁 − 1) = (((𝐴 · 𝐵) + 1) − 1))
9221nncnd 11876 . . . . . . . . 9 (𝜑 → (𝐴 · 𝐵) ∈ ℂ)
93 ax-1cn 10817 . . . . . . . . 9 1 ∈ ℂ
94 pncan 11114 . . . . . . . . 9 (((𝐴 · 𝐵) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐴 · 𝐵) + 1) − 1) = (𝐴 · 𝐵))
9592, 93, 94sylancl 589 . . . . . . . 8 (𝜑 → (((𝐴 · 𝐵) + 1) − 1) = (𝐴 · 𝐵))
9691, 95eqtrd 2779 . . . . . . 7 (𝜑 → (𝑁 − 1) = (𝐴 · 𝐵))
9790, 96breqtrrd 5098 . . . . . 6 (𝜑𝐴 ∥ (𝑁 − 1))
987, 84, 85, 87, 97dvdstrd 15889 . . . . 5 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1))
996nnne0d 11910 . . . . . 6 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ≠ 0)
100 dvdsval2 15851 . . . . . 6 (((𝑄↑(𝑄 pCnt 𝐴)) ∈ ℤ ∧ (𝑄↑(𝑄 pCnt 𝐴)) ≠ 0 ∧ (𝑁 − 1) ∈ ℤ) → ((𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ))
1017, 99, 85, 100syl3anc 1373 . . . . 5 (𝜑 → ((𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ))
10298, 101mpbid 235 . . . 4 (𝜑 → ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ)
103 peano2zm 12250 . . . . . . . 8 ((𝐶↑(𝑁 − 1)) ∈ ℤ → ((𝐶↑(𝑁 − 1)) − 1) ∈ ℤ)
10452, 103syl 17 . . . . . . 7 (𝜑 → ((𝐶↑(𝑁 − 1)) − 1) ∈ ℤ)
10532nnred 11875 . . . . . . . . . 10 (𝜑𝑁 ∈ ℝ)
10631simprd 499 . . . . . . . . . 10 (𝜑 → 1 < 𝑁)
107 1mod 13508 . . . . . . . . . 10 ((𝑁 ∈ ℝ ∧ 1 < 𝑁) → (1 mod 𝑁) = 1)
108105, 106, 107syl2anc 587 . . . . . . . . 9 (𝜑 → (1 mod 𝑁) = 1)
10944, 108eqtr4d 2782 . . . . . . . 8 (𝜑 → ((𝐶↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁))
110 1zzd 12238 . . . . . . . . 9 (𝜑 → 1 ∈ ℤ)
111 moddvds 15859 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ (𝐶↑(𝑁 − 1)) ∈ ℤ ∧ 1 ∈ ℤ) → (((𝐶↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1)))
11232, 52, 110, 111syl3anc 1373 . . . . . . . 8 (𝜑 → (((𝐶↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1)))
113109, 112mpbid 235 . . . . . . 7 (𝜑𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1))
11412, 33, 104, 35, 113dvdstrd 15889 . . . . . 6 (𝜑𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1))
115 odzdvds 16381 . . . . . . 7 (((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) ∧ (𝑁 − 1) ∈ ℕ0) → (𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1) ↔ ((od𝑃)‘𝐶) ∥ (𝑁 − 1)))
11610, 11, 73, 50, 115syl31anc 1375 . . . . . 6 (𝜑 → (𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1) ↔ ((od𝑃)‘𝐶) ∥ (𝑁 − 1)))
117114, 116mpbid 235 . . . . 5 (𝜑 → ((od𝑃)‘𝐶) ∥ (𝑁 − 1))
11849nncnd 11876 . . . . . 6 (𝜑 → (𝑁 − 1) ∈ ℂ)
1196nncnd 11876 . . . . . 6 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∈ ℂ)
120118, 119, 99divcan1d 11639 . . . . 5 (𝜑 → (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) = (𝑁 − 1))
121117, 120breqtrrd 5098 . . . 4 (𝜑 → ((od𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))))
122 nprmdvds1 16296 . . . . . 6 (𝑃 ∈ ℙ → ¬ 𝑃 ∥ 1)
1238, 122syl 17 . . . . 5 (𝜑 → ¬ 𝑃 ∥ 1)
1243nnzd 12311 . . . . . . . . . . . . 13 (𝜑𝑄 ∈ ℤ)
125 iddvdsexp 15874 . . . . . . . . . . . . . 14 ((𝑄 ∈ ℤ ∧ (𝑄 pCnt 𝐴) ∈ ℕ) → 𝑄 ∥ (𝑄↑(𝑄 pCnt 𝐴)))
126124, 4, 125syl2anc 587 . . . . . . . . . . . . 13 (𝜑𝑄 ∥ (𝑄↑(𝑄 pCnt 𝐴)))
127124, 7, 85, 126, 98dvdstrd 15889 . . . . . . . . . . . 12 (𝜑𝑄 ∥ (𝑁 − 1))
1283nnne0d 11910 . . . . . . . . . . . . 13 (𝜑𝑄 ≠ 0)
129 dvdsval2 15851 . . . . . . . . . . . . 13 ((𝑄 ∈ ℤ ∧ 𝑄 ≠ 0 ∧ (𝑁 − 1) ∈ ℤ) → (𝑄 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 𝑄) ∈ ℤ))
130124, 128, 85, 129syl3anc 1373 . . . . . . . . . . . 12 (𝜑 → (𝑄 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 𝑄) ∈ ℤ))
131127, 130mpbid 235 . . . . . . . . . . 11 (𝜑 → ((𝑁 − 1) / 𝑄) ∈ ℤ)
13250nn0ge0d 12183 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (𝑁 − 1))
13349nnred 11875 . . . . . . . . . . . . 13 (𝜑 → (𝑁 − 1) ∈ ℝ)
1343nnred 11875 . . . . . . . . . . . . 13 (𝜑𝑄 ∈ ℝ)
1353nngt0d 11909 . . . . . . . . . . . . 13 (𝜑 → 0 < 𝑄)
136 ge0div 11729 . . . . . . . . . . . . 13 (((𝑁 − 1) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ 0 < 𝑄) → (0 ≤ (𝑁 − 1) ↔ 0 ≤ ((𝑁 − 1) / 𝑄)))
137133, 134, 135, 136syl3anc 1373 . . . . . . . . . . . 12 (𝜑 → (0 ≤ (𝑁 − 1) ↔ 0 ≤ ((𝑁 − 1) / 𝑄)))
138132, 137mpbid 235 . . . . . . . . . . 11 (𝜑 → 0 ≤ ((𝑁 − 1) / 𝑄))
139 elnn0z 12219 . . . . . . . . . . 11 (((𝑁 − 1) / 𝑄) ∈ ℕ0 ↔ (((𝑁 − 1) / 𝑄) ∈ ℤ ∧ 0 ≤ ((𝑁 − 1) / 𝑄)))
140131, 138, 139sylanbrc 586 . . . . . . . . . 10 (𝜑 → ((𝑁 − 1) / 𝑄) ∈ ℕ0)
141 zexpcl 13682 . . . . . . . . . 10 ((𝐶 ∈ ℤ ∧ ((𝑁 − 1) / 𝑄) ∈ ℕ0) → (𝐶↑((𝑁 − 1) / 𝑄)) ∈ ℤ)
14211, 140, 141syl2anc 587 . . . . . . . . 9 (𝜑 → (𝐶↑((𝑁 − 1) / 𝑄)) ∈ ℤ)
143 peano2zm 12250 . . . . . . . . 9 ((𝐶↑((𝑁 − 1) / 𝑄)) ∈ ℤ → ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∈ ℤ)
144142, 143syl 17 . . . . . . . 8 (𝜑 → ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∈ ℤ)
145 dvdsgcd 16137 . . . . . . . 8 ((𝑃 ∈ ℤ ∧ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∧ 𝑃𝑁) → 𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁)))
14612, 144, 33, 145syl3anc 1373 . . . . . . 7 (𝜑 → ((𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∧ 𝑃𝑁) → 𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁)))
14735, 146mpan2d 694 . . . . . 6 (𝜑 → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) → 𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁)))
148 odzdvds 16381 . . . . . . . 8 (((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) ∧ ((𝑁 − 1) / 𝑄) ∈ ℕ0) → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ↔ ((od𝑃)‘𝐶) ∥ ((𝑁 − 1) / 𝑄)))
14910, 11, 73, 140, 148syl31anc 1375 . . . . . . 7 (𝜑 → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ↔ ((od𝑃)‘𝐶) ∥ ((𝑁 − 1) / 𝑄)))
1503nncnd 11876 . . . . . . . . . . 11 (𝜑𝑄 ∈ ℂ)
1514nnzd 12311 . . . . . . . . . . 11 (𝜑 → (𝑄 pCnt 𝐴) ∈ ℤ)
152150, 128, 151expm1d 13759 . . . . . . . . . 10 (𝜑 → (𝑄↑((𝑄 pCnt 𝐴) − 1)) = ((𝑄↑(𝑄 pCnt 𝐴)) / 𝑄))
153152oveq2d 7251 . . . . . . . . 9 (𝜑 → (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) = (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · ((𝑄↑(𝑄 pCnt 𝐴)) / 𝑄)))
154133, 6nndivred 11914 . . . . . . . . . . 11 (𝜑 → ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℝ)
155154recnd 10891 . . . . . . . . . 10 (𝜑 → ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℂ)
156155, 119, 150, 128divassd 11673 . . . . . . . . 9 (𝜑 → ((((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) / 𝑄) = (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · ((𝑄↑(𝑄 pCnt 𝐴)) / 𝑄)))
157120oveq1d 7250 . . . . . . . . 9 (𝜑 → ((((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) / 𝑄) = ((𝑁 − 1) / 𝑄))
158153, 156, 1573eqtr2d 2785 . . . . . . . 8 (𝜑 → (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) = ((𝑁 − 1) / 𝑄))
159158breq2d 5082 . . . . . . 7 (𝜑 → (((od𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) ↔ ((od𝑃)‘𝐶) ∥ ((𝑁 − 1) / 𝑄)))
160149, 159bitr4d 285 . . . . . 6 (𝜑 → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ↔ ((od𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1)))))
161 pockthlem.11 . . . . . . 7 (𝜑 → (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁) = 1)
162161breq2d 5082 . . . . . 6 (𝜑 → (𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁) ↔ 𝑃 ∥ 1))
163147, 160, 1623imtr3d 296 . . . . 5 (𝜑 → (((od𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) → 𝑃 ∥ 1))
164123, 163mtod 201 . . . 4 (𝜑 → ¬ ((od𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))))
165 prmpwdvds 16490 . . . 4 (((((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ ∧ ((od𝑃)‘𝐶) ∈ ℤ) ∧ (𝑄 ∈ ℙ ∧ (𝑄 pCnt 𝐴) ∈ ℕ) ∧ (((od𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) ∧ ¬ ((od𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))))) → (𝑄↑(𝑄 pCnt 𝐴)) ∥ ((od𝑃)‘𝐶))
166102, 76, 1, 4, 121, 164, 165syl222anc 1388 . . 3 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ ((od𝑃)‘𝐶))
167 odzphi 16382 . . . . 5 ((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) → ((od𝑃)‘𝐶) ∥ (ϕ‘𝑃))
16810, 11, 73, 167syl3anc 1373 . . . 4 (𝜑 → ((od𝑃)‘𝐶) ∥ (ϕ‘𝑃))
169 phiprm 16363 . . . . 5 (𝑃 ∈ ℙ → (ϕ‘𝑃) = (𝑃 − 1))
1708, 169syl 17 . . . 4 (𝜑 → (ϕ‘𝑃) = (𝑃 − 1))
171168, 170breqtrd 5096 . . 3 (𝜑 → ((od𝑃)‘𝐶) ∥ (𝑃 − 1))
1727, 76, 83, 166, 171dvdstrd 15889 . 2 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1))
173 pcdvdsb 16455 . . 3 ((𝑄 ∈ ℙ ∧ (𝑃 − 1) ∈ ℤ ∧ (𝑄 pCnt 𝐴) ∈ ℕ0) → ((𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1)) ↔ (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1)))
1741, 83, 5, 173syl3anc 1373 . 2 (𝜑 → ((𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1)) ↔ (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1)))
175172, 174mpbird 260 1 (𝜑 → (𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399   = wceq 1543  wcel 2112  wne 2943   class class class wbr 5070  cfv 6401  (class class class)co 7235  cc 10757  cr 10758  0cc0 10759  1c1 10760   + caddc 10762   · cmul 10764   < clt 10897  cle 10898  cmin 11092   / cdiv 11519  cn 11860  2c2 11915  0cn0 12120  cz 12206  cuz 12468   mod cmo 13474  cexp 13667  cdvds 15848   gcd cgcd 16086  cprime 16261  odcodz 16349  ϕcphi 16350   pCnt cpc 16422
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-rep 5196  ax-sep 5209  ax-nul 5216  ax-pow 5275  ax-pr 5339  ax-un 7545  ax-cnex 10815  ax-resscn 10816  ax-1cn 10817  ax-icn 10818  ax-addcl 10819  ax-addrcl 10820  ax-mulcl 10821  ax-mulrcl 10822  ax-mulcom 10823  ax-addass 10824  ax-mulass 10825  ax-distr 10826  ax-i2m1 10827  ax-1ne0 10828  ax-1rid 10829  ax-rnegex 10830  ax-rrecex 10831  ax-cnre 10832  ax-pre-lttri 10833  ax-pre-lttrn 10834  ax-pre-ltadd 10835  ax-pre-mulgt0 10836  ax-pre-sup 10837
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3425  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4255  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-int 4877  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5153  df-tr 5179  df-id 5472  df-eprel 5478  df-po 5486  df-so 5487  df-fr 5527  df-we 5529  df-xp 5575  df-rel 5576  df-cnv 5577  df-co 5578  df-dm 5579  df-rn 5580  df-res 5581  df-ima 5582  df-pred 6179  df-ord 6237  df-on 6238  df-lim 6239  df-suc 6240  df-iota 6359  df-fun 6403  df-fn 6404  df-f 6405  df-f1 6406  df-fo 6407  df-f1o 6408  df-fv 6409  df-riota 7192  df-ov 7238  df-oprab 7239  df-mpo 7240  df-om 7667  df-1st 7783  df-2nd 7784  df-wrecs 8071  df-recs 8132  df-rdg 8170  df-1o 8226  df-2o 8227  df-oadd 8230  df-er 8415  df-map 8534  df-en 8651  df-dom 8652  df-sdom 8653  df-fin 8654  df-sup 9088  df-inf 9089  df-dju 9547  df-card 9585  df-pnf 10899  df-mnf 10900  df-xr 10901  df-ltxr 10902  df-le 10903  df-sub 11094  df-neg 11095  df-div 11520  df-nn 11861  df-2 11923  df-3 11924  df-n0 12121  df-xnn0 12193  df-z 12207  df-uz 12469  df-q 12575  df-rp 12617  df-fz 13126  df-fzo 13269  df-fl 13397  df-mod 13475  df-seq 13607  df-exp 13668  df-hash 13930  df-cj 14695  df-re 14696  df-im 14697  df-sqrt 14831  df-abs 14832  df-dvds 15849  df-gcd 16087  df-prm 16262  df-odz 16351  df-phi 16352  df-pc 16423
This theorem is referenced by:  pockthg  16492
  Copyright terms: Public domain W3C validator