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

Theorem pockthlem 15826
Description: Lemma for pockthg 15827. (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 . . . . . . 7 (𝜑𝑄 ∈ ℙ)
2 pockthg.1 . . . . . . 7 (𝜑𝐴 ∈ ℕ)
3 pcdvds 15785 . . . . . . 7 ((𝑄 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (𝑄↑(𝑄 pCnt 𝐴)) ∥ 𝐴)
41, 2, 3syl2anc 575 . . . . . 6 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ 𝐴)
52nnzd 11747 . . . . . . . 8 (𝜑𝐴 ∈ ℤ)
6 pockthg.2 . . . . . . . . 9 (𝜑𝐵 ∈ ℕ)
76nnzd 11747 . . . . . . . 8 (𝜑𝐵 ∈ ℤ)
8 dvdsmul1 15226 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∥ (𝐴 · 𝐵))
95, 7, 8syl2anc 575 . . . . . . 7 (𝜑𝐴 ∥ (𝐴 · 𝐵))
10 pockthg.4 . . . . . . . . 9 (𝜑𝑁 = ((𝐴 · 𝐵) + 1))
1110oveq1d 6889 . . . . . . . 8 (𝜑 → (𝑁 − 1) = (((𝐴 · 𝐵) + 1) − 1))
122, 6nnmulcld 11354 . . . . . . . . . 10 (𝜑 → (𝐴 · 𝐵) ∈ ℕ)
1312nncnd 11321 . . . . . . . . 9 (𝜑 → (𝐴 · 𝐵) ∈ ℂ)
14 ax-1cn 10279 . . . . . . . . 9 1 ∈ ℂ
15 pncan 10572 . . . . . . . . 9 (((𝐴 · 𝐵) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐴 · 𝐵) + 1) − 1) = (𝐴 · 𝐵))
1613, 14, 15sylancl 576 . . . . . . . 8 (𝜑 → (((𝐴 · 𝐵) + 1) − 1) = (𝐴 · 𝐵))
1711, 16eqtrd 2840 . . . . . . 7 (𝜑 → (𝑁 − 1) = (𝐴 · 𝐵))
189, 17breqtrrd 4872 . . . . . 6 (𝜑𝐴 ∥ (𝑁 − 1))
19 prmnn 15606 . . . . . . . . . 10 (𝑄 ∈ ℙ → 𝑄 ∈ ℕ)
201, 19syl 17 . . . . . . . . 9 (𝜑𝑄 ∈ ℕ)
21 pockthlem.8 . . . . . . . . . 10 (𝜑 → (𝑄 pCnt 𝐴) ∈ ℕ)
2221nnnn0d 11617 . . . . . . . . 9 (𝜑 → (𝑄 pCnt 𝐴) ∈ ℕ0)
2320, 22nnexpcld 13253 . . . . . . . 8 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∈ ℕ)
2423nnzd 11747 . . . . . . 7 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∈ ℤ)
25 1z 11673 . . . . . . . . . 10 1 ∈ ℤ
26 nnuz 11941 . . . . . . . . . . . . 13 ℕ = (ℤ‘1)
2712, 26syl6eleq 2895 . . . . . . . . . . . 12 (𝜑 → (𝐴 · 𝐵) ∈ (ℤ‘1))
28 eluzp1p1 11930 . . . . . . . . . . . 12 ((𝐴 · 𝐵) ∈ (ℤ‘1) → ((𝐴 · 𝐵) + 1) ∈ (ℤ‘(1 + 1)))
2927, 28syl 17 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝐵) + 1) ∈ (ℤ‘(1 + 1)))
3010, 29eqeltrd 2885 . . . . . . . . . 10 (𝜑𝑁 ∈ (ℤ‘(1 + 1)))
31 eluzp1m1 11928 . . . . . . . . . 10 ((1 ∈ ℤ ∧ 𝑁 ∈ (ℤ‘(1 + 1))) → (𝑁 − 1) ∈ (ℤ‘1))
3225, 30, 31sylancr 577 . . . . . . . . 9 (𝜑 → (𝑁 − 1) ∈ (ℤ‘1))
3332, 26syl6eleqr 2896 . . . . . . . 8 (𝜑 → (𝑁 − 1) ∈ ℕ)
3433nnzd 11747 . . . . . . 7 (𝜑 → (𝑁 − 1) ∈ ℤ)
35 dvdstr 15241 . . . . . . 7 (((𝑄↑(𝑄 pCnt 𝐴)) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (((𝑄↑(𝑄 pCnt 𝐴)) ∥ 𝐴𝐴 ∥ (𝑁 − 1)) → (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1)))
3624, 5, 34, 35syl3anc 1483 . . . . . 6 (𝜑 → (((𝑄↑(𝑄 pCnt 𝐴)) ∥ 𝐴𝐴 ∥ (𝑁 − 1)) → (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1)))
374, 18, 36mp2and 682 . . . . 5 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1))
3823nnne0d 11351 . . . . . 6 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ≠ 0)
39 dvdsval2 15206 . . . . . 6 (((𝑄↑(𝑄 pCnt 𝐴)) ∈ ℤ ∧ (𝑄↑(𝑄 pCnt 𝐴)) ≠ 0 ∧ (𝑁 − 1) ∈ ℤ) → ((𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ))
4024, 38, 34, 39syl3anc 1483 . . . . 5 (𝜑 → ((𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ))
4137, 40mpbid 223 . . . 4 (𝜑 → ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ)
42 pockthlem.5 . . . . . . 7 (𝜑𝑃 ∈ ℙ)
43 prmnn 15606 . . . . . . 7 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
4442, 43syl 17 . . . . . 6 (𝜑𝑃 ∈ ℕ)
45 pockthlem.9 . . . . . 6 (𝜑𝐶 ∈ ℤ)
4644nnzd 11747 . . . . . . . . . . 11 (𝜑𝑃 ∈ ℤ)
47 gcddvds 15444 . . . . . . . . . . 11 ((𝐶 ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑃))
4845, 46, 47syl2anc 575 . . . . . . . . . 10 (𝜑 → ((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑃))
4948simpld 484 . . . . . . . . 9 (𝜑 → (𝐶 gcd 𝑃) ∥ 𝐶)
5048simprd 485 . . . . . . . . . 10 (𝜑 → (𝐶 gcd 𝑃) ∥ 𝑃)
51 pockthlem.6 . . . . . . . . . 10 (𝜑𝑃𝑁)
5245, 46gcdcld 15449 . . . . . . . . . . . 12 (𝜑 → (𝐶 gcd 𝑃) ∈ ℕ0)
5352nn0zd 11746 . . . . . . . . . . 11 (𝜑 → (𝐶 gcd 𝑃) ∈ ℤ)
54 df-2 11364 . . . . . . . . . . . . . . . 16 2 = (1 + 1)
5554fveq2i 6411 . . . . . . . . . . . . . . 15 (ℤ‘2) = (ℤ‘(1 + 1))
5630, 55syl6eleqr 2896 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ (ℤ‘2))
57 eluz2b2 11980 . . . . . . . . . . . . . 14 (𝑁 ∈ (ℤ‘2) ↔ (𝑁 ∈ ℕ ∧ 1 < 𝑁))
5856, 57sylib 209 . . . . . . . . . . . . 13 (𝜑 → (𝑁 ∈ ℕ ∧ 1 < 𝑁))
5958simpld 484 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℕ)
6059nnzd 11747 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℤ)
61 dvdstr 15241 . . . . . . . . . . 11 (((𝐶 gcd 𝑃) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝐶 gcd 𝑃) ∥ 𝑃𝑃𝑁) → (𝐶 gcd 𝑃) ∥ 𝑁))
6253, 46, 60, 61syl3anc 1483 . . . . . . . . . 10 (𝜑 → (((𝐶 gcd 𝑃) ∥ 𝑃𝑃𝑁) → (𝐶 gcd 𝑃) ∥ 𝑁))
6350, 51, 62mp2and 682 . . . . . . . . 9 (𝜑 → (𝐶 gcd 𝑃) ∥ 𝑁)
6459nnne0d 11351 . . . . . . . . . . 11 (𝜑𝑁 ≠ 0)
65 simpr 473 . . . . . . . . . . . 12 ((𝐶 = 0 ∧ 𝑁 = 0) → 𝑁 = 0)
6665necon3ai 3003 . . . . . . . . . . 11 (𝑁 ≠ 0 → ¬ (𝐶 = 0 ∧ 𝑁 = 0))
6764, 66syl 17 . . . . . . . . . 10 (𝜑 → ¬ (𝐶 = 0 ∧ 𝑁 = 0))
68 dvdslegcd 15445 . . . . . . . . . 10 ((((𝐶 gcd 𝑃) ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝐶 = 0 ∧ 𝑁 = 0)) → (((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑁) → (𝐶 gcd 𝑃) ≤ (𝐶 gcd 𝑁)))
6953, 45, 60, 67, 68syl31anc 1485 . . . . . . . . 9 (𝜑 → (((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑁) → (𝐶 gcd 𝑃) ≤ (𝐶 gcd 𝑁)))
7049, 63, 69mp2and 682 . . . . . . . 8 (𝜑 → (𝐶 gcd 𝑃) ≤ (𝐶 gcd 𝑁))
71 pockthlem.10 . . . . . . . . . . 11 (𝜑 → ((𝐶↑(𝑁 − 1)) mod 𝑁) = 1)
7271oveq1d 6889 . . . . . . . . . 10 (𝜑 → (((𝐶↑(𝑁 − 1)) mod 𝑁) gcd 𝑁) = (1 gcd 𝑁))
7333nnnn0d 11617 . . . . . . . . . . . 12 (𝜑 → (𝑁 − 1) ∈ ℕ0)
74 zexpcl 13098 . . . . . . . . . . . 12 ((𝐶 ∈ ℤ ∧ (𝑁 − 1) ∈ ℕ0) → (𝐶↑(𝑁 − 1)) ∈ ℤ)
7545, 73, 74syl2anc 575 . . . . . . . . . . 11 (𝜑 → (𝐶↑(𝑁 − 1)) ∈ ℤ)
76 modgcd 15472 . . . . . . . . . . 11 (((𝐶↑(𝑁 − 1)) ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐶↑(𝑁 − 1)) mod 𝑁) gcd 𝑁) = ((𝐶↑(𝑁 − 1)) gcd 𝑁))
7775, 59, 76syl2anc 575 . . . . . . . . . 10 (𝜑 → (((𝐶↑(𝑁 − 1)) mod 𝑁) gcd 𝑁) = ((𝐶↑(𝑁 − 1)) gcd 𝑁))
78 gcdcom 15454 . . . . . . . . . . . 12 ((1 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (1 gcd 𝑁) = (𝑁 gcd 1))
7925, 60, 78sylancr 577 . . . . . . . . . . 11 (𝜑 → (1 gcd 𝑁) = (𝑁 gcd 1))
80 gcd1 15468 . . . . . . . . . . . 12 (𝑁 ∈ ℤ → (𝑁 gcd 1) = 1)
8160, 80syl 17 . . . . . . . . . . 11 (𝜑 → (𝑁 gcd 1) = 1)
8279, 81eqtrd 2840 . . . . . . . . . 10 (𝜑 → (1 gcd 𝑁) = 1)
8372, 77, 823eqtr3d 2848 . . . . . . . . 9 (𝜑 → ((𝐶↑(𝑁 − 1)) gcd 𝑁) = 1)
84 rpexp 15649 . . . . . . . . . 10 ((𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁 − 1) ∈ ℕ) → (((𝐶↑(𝑁 − 1)) gcd 𝑁) = 1 ↔ (𝐶 gcd 𝑁) = 1))
8545, 60, 33, 84syl3anc 1483 . . . . . . . . 9 (𝜑 → (((𝐶↑(𝑁 − 1)) gcd 𝑁) = 1 ↔ (𝐶 gcd 𝑁) = 1))
8683, 85mpbid 223 . . . . . . . 8 (𝜑 → (𝐶 gcd 𝑁) = 1)
8770, 86breqtrd 4870 . . . . . . 7 (𝜑 → (𝐶 gcd 𝑃) ≤ 1)
8844nnne0d 11351 . . . . . . . . . 10 (𝜑𝑃 ≠ 0)
89 simpr 473 . . . . . . . . . . 11 ((𝐶 = 0 ∧ 𝑃 = 0) → 𝑃 = 0)
9089necon3ai 3003 . . . . . . . . . 10 (𝑃 ≠ 0 → ¬ (𝐶 = 0 ∧ 𝑃 = 0))
9188, 90syl 17 . . . . . . . . 9 (𝜑 → ¬ (𝐶 = 0 ∧ 𝑃 = 0))
92 gcdn0cl 15443 . . . . . . . . 9 (((𝐶 ∈ ℤ ∧ 𝑃 ∈ ℤ) ∧ ¬ (𝐶 = 0 ∧ 𝑃 = 0)) → (𝐶 gcd 𝑃) ∈ ℕ)
9345, 46, 91, 92syl21anc 857 . . . . . . . 8 (𝜑 → (𝐶 gcd 𝑃) ∈ ℕ)
94 nnle1eq1 11334 . . . . . . . 8 ((𝐶 gcd 𝑃) ∈ ℕ → ((𝐶 gcd 𝑃) ≤ 1 ↔ (𝐶 gcd 𝑃) = 1))
9593, 94syl 17 . . . . . . 7 (𝜑 → ((𝐶 gcd 𝑃) ≤ 1 ↔ (𝐶 gcd 𝑃) = 1))
9687, 95mpbid 223 . . . . . 6 (𝜑 → (𝐶 gcd 𝑃) = 1)
97 odzcl 15715 . . . . . 6 ((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) → ((od𝑃)‘𝐶) ∈ ℕ)
9844, 45, 96, 97syl3anc 1483 . . . . 5 (𝜑 → ((od𝑃)‘𝐶) ∈ ℕ)
9998nnzd 11747 . . . 4 (𝜑 → ((od𝑃)‘𝐶) ∈ ℤ)
10059nnred 11320 . . . . . . . . . 10 (𝜑𝑁 ∈ ℝ)
10158simprd 485 . . . . . . . . . 10 (𝜑 → 1 < 𝑁)
102 1mod 12926 . . . . . . . . . 10 ((𝑁 ∈ ℝ ∧ 1 < 𝑁) → (1 mod 𝑁) = 1)
103100, 101, 102syl2anc 575 . . . . . . . . 9 (𝜑 → (1 mod 𝑁) = 1)
10471, 103eqtr4d 2843 . . . . . . . 8 (𝜑 → ((𝐶↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁))
105 1zzd 11674 . . . . . . . . 9 (𝜑 → 1 ∈ ℤ)
106 moddvds 15214 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ (𝐶↑(𝑁 − 1)) ∈ ℤ ∧ 1 ∈ ℤ) → (((𝐶↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1)))
10759, 75, 105, 106syl3anc 1483 . . . . . . . 8 (𝜑 → (((𝐶↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1)))
108104, 107mpbid 223 . . . . . . 7 (𝜑𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1))
109 peano2zm 11686 . . . . . . . . 9 ((𝐶↑(𝑁 − 1)) ∈ ℤ → ((𝐶↑(𝑁 − 1)) − 1) ∈ ℤ)
11075, 109syl 17 . . . . . . . 8 (𝜑 → ((𝐶↑(𝑁 − 1)) − 1) ∈ ℤ)
111 dvdstr 15241 . . . . . . . 8 ((𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝐶↑(𝑁 − 1)) − 1) ∈ ℤ) → ((𝑃𝑁𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1)) → 𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1)))
11246, 60, 110, 111syl3anc 1483 . . . . . . 7 (𝜑 → ((𝑃𝑁𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1)) → 𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1)))
11351, 108, 112mp2and 682 . . . . . 6 (𝜑𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1))
114 odzdvds 15717 . . . . . . 7 (((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) ∧ (𝑁 − 1) ∈ ℕ0) → (𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1) ↔ ((od𝑃)‘𝐶) ∥ (𝑁 − 1)))
11544, 45, 96, 73, 114syl31anc 1485 . . . . . 6 (𝜑 → (𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1) ↔ ((od𝑃)‘𝐶) ∥ (𝑁 − 1)))
116113, 115mpbid 223 . . . . 5 (𝜑 → ((od𝑃)‘𝐶) ∥ (𝑁 − 1))
11733nncnd 11321 . . . . . 6 (𝜑 → (𝑁 − 1) ∈ ℂ)
11823nncnd 11321 . . . . . 6 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∈ ℂ)
119117, 118, 38divcan1d 11087 . . . . 5 (𝜑 → (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) = (𝑁 − 1))
120116, 119breqtrrd 4872 . . . 4 (𝜑 → ((od𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))))
121 nprmdvds1 15635 . . . . . 6 (𝑃 ∈ ℙ → ¬ 𝑃 ∥ 1)
12242, 121syl 17 . . . . 5 (𝜑 → ¬ 𝑃 ∥ 1)
12320nnzd 11747 . . . . . . . . . . . . . 14 (𝜑𝑄 ∈ ℤ)
124 iddvdsexp 15228 . . . . . . . . . . . . . 14 ((𝑄 ∈ ℤ ∧ (𝑄 pCnt 𝐴) ∈ ℕ) → 𝑄 ∥ (𝑄↑(𝑄 pCnt 𝐴)))
125123, 21, 124syl2anc 575 . . . . . . . . . . . . 13 (𝜑𝑄 ∥ (𝑄↑(𝑄 pCnt 𝐴)))
126 dvdstr 15241 . . . . . . . . . . . . . 14 ((𝑄 ∈ ℤ ∧ (𝑄↑(𝑄 pCnt 𝐴)) ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → ((𝑄 ∥ (𝑄↑(𝑄 pCnt 𝐴)) ∧ (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1)) → 𝑄 ∥ (𝑁 − 1)))
127123, 24, 34, 126syl3anc 1483 . . . . . . . . . . . . 13 (𝜑 → ((𝑄 ∥ (𝑄↑(𝑄 pCnt 𝐴)) ∧ (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1)) → 𝑄 ∥ (𝑁 − 1)))
128125, 37, 127mp2and 682 . . . . . . . . . . . 12 (𝜑𝑄 ∥ (𝑁 − 1))
12920nnne0d 11351 . . . . . . . . . . . . 13 (𝜑𝑄 ≠ 0)
130 dvdsval2 15206 . . . . . . . . . . . . 13 ((𝑄 ∈ ℤ ∧ 𝑄 ≠ 0 ∧ (𝑁 − 1) ∈ ℤ) → (𝑄 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 𝑄) ∈ ℤ))
131123, 129, 34, 130syl3anc 1483 . . . . . . . . . . . 12 (𝜑 → (𝑄 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 𝑄) ∈ ℤ))
132128, 131mpbid 223 . . . . . . . . . . 11 (𝜑 → ((𝑁 − 1) / 𝑄) ∈ ℤ)
13373nn0ge0d 11620 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (𝑁 − 1))
13433nnred 11320 . . . . . . . . . . . . 13 (𝜑 → (𝑁 − 1) ∈ ℝ)
13520nnred 11320 . . . . . . . . . . . . 13 (𝜑𝑄 ∈ ℝ)
13620nngt0d 11350 . . . . . . . . . . . . 13 (𝜑 → 0 < 𝑄)
137 ge0div 11175 . . . . . . . . . . . . 13 (((𝑁 − 1) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ 0 < 𝑄) → (0 ≤ (𝑁 − 1) ↔ 0 ≤ ((𝑁 − 1) / 𝑄)))
138134, 135, 136, 137syl3anc 1483 . . . . . . . . . . . 12 (𝜑 → (0 ≤ (𝑁 − 1) ↔ 0 ≤ ((𝑁 − 1) / 𝑄)))
139133, 138mpbid 223 . . . . . . . . . . 11 (𝜑 → 0 ≤ ((𝑁 − 1) / 𝑄))
140 elnn0z 11656 . . . . . . . . . . 11 (((𝑁 − 1) / 𝑄) ∈ ℕ0 ↔ (((𝑁 − 1) / 𝑄) ∈ ℤ ∧ 0 ≤ ((𝑁 − 1) / 𝑄)))
141132, 139, 140sylanbrc 574 . . . . . . . . . 10 (𝜑 → ((𝑁 − 1) / 𝑄) ∈ ℕ0)
142 zexpcl 13098 . . . . . . . . . 10 ((𝐶 ∈ ℤ ∧ ((𝑁 − 1) / 𝑄) ∈ ℕ0) → (𝐶↑((𝑁 − 1) / 𝑄)) ∈ ℤ)
14345, 141, 142syl2anc 575 . . . . . . . . 9 (𝜑 → (𝐶↑((𝑁 − 1) / 𝑄)) ∈ ℤ)
144 peano2zm 11686 . . . . . . . . 9 ((𝐶↑((𝑁 − 1) / 𝑄)) ∈ ℤ → ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∈ ℤ)
145143, 144syl 17 . . . . . . . 8 (𝜑 → ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∈ ℤ)
146 dvdsgcd 15480 . . . . . . . 8 ((𝑃 ∈ ℤ ∧ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∧ 𝑃𝑁) → 𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁)))
14746, 145, 60, 146syl3anc 1483 . . . . . . 7 (𝜑 → ((𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∧ 𝑃𝑁) → 𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁)))
14851, 147mpan2d 677 . . . . . 6 (𝜑 → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) → 𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁)))
149 odzdvds 15717 . . . . . . . 8 (((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) ∧ ((𝑁 − 1) / 𝑄) ∈ ℕ0) → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ↔ ((od𝑃)‘𝐶) ∥ ((𝑁 − 1) / 𝑄)))
15044, 45, 96, 141, 149syl31anc 1485 . . . . . . 7 (𝜑 → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ↔ ((od𝑃)‘𝐶) ∥ ((𝑁 − 1) / 𝑄)))
15120nncnd 11321 . . . . . . . . . . 11 (𝜑𝑄 ∈ ℂ)
15221nnzd 11747 . . . . . . . . . . 11 (𝜑 → (𝑄 pCnt 𝐴) ∈ ℤ)
153151, 129, 152expm1d 13241 . . . . . . . . . 10 (𝜑 → (𝑄↑((𝑄 pCnt 𝐴) − 1)) = ((𝑄↑(𝑄 pCnt 𝐴)) / 𝑄))
154153oveq2d 6890 . . . . . . . . 9 (𝜑 → (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) = (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · ((𝑄↑(𝑄 pCnt 𝐴)) / 𝑄)))
155134, 23nndivred 11355 . . . . . . . . . . 11 (𝜑 → ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℝ)
156155recnd 10353 . . . . . . . . . 10 (𝜑 → ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℂ)
157156, 118, 151, 129divassd 11121 . . . . . . . . 9 (𝜑 → ((((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) / 𝑄) = (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · ((𝑄↑(𝑄 pCnt 𝐴)) / 𝑄)))
158119oveq1d 6889 . . . . . . . . 9 (𝜑 → ((((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) / 𝑄) = ((𝑁 − 1) / 𝑄))
159154, 157, 1583eqtr2d 2846 . . . . . . . 8 (𝜑 → (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) = ((𝑁 − 1) / 𝑄))
160159breq2d 4856 . . . . . . 7 (𝜑 → (((od𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) ↔ ((od𝑃)‘𝐶) ∥ ((𝑁 − 1) / 𝑄)))
161150, 160bitr4d 273 . . . . . 6 (𝜑 → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ↔ ((od𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1)))))
162 pockthlem.11 . . . . . . 7 (𝜑 → (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁) = 1)
163162breq2d 4856 . . . . . 6 (𝜑 → (𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁) ↔ 𝑃 ∥ 1))
164148, 161, 1633imtr3d 284 . . . . 5 (𝜑 → (((od𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) → 𝑃 ∥ 1))
165122, 164mtod 189 . . . 4 (𝜑 → ¬ ((od𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))))
166 prmpwdvds 15825 . . . 4 (((((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ ∧ ((od𝑃)‘𝐶) ∈ ℤ) ∧ (𝑄 ∈ ℙ ∧ (𝑄 pCnt 𝐴) ∈ ℕ) ∧ (((od𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) ∧ ¬ ((od𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))))) → (𝑄↑(𝑄 pCnt 𝐴)) ∥ ((od𝑃)‘𝐶))
16741, 99, 1, 21, 120, 165, 166syl222anc 1498 . . 3 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ ((od𝑃)‘𝐶))
168 odzphi 15718 . . . . 5 ((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) → ((od𝑃)‘𝐶) ∥ (ϕ‘𝑃))
16944, 45, 96, 168syl3anc 1483 . . . 4 (𝜑 → ((od𝑃)‘𝐶) ∥ (ϕ‘𝑃))
170 phiprm 15699 . . . . 5 (𝑃 ∈ ℙ → (ϕ‘𝑃) = (𝑃 − 1))
17142, 170syl 17 . . . 4 (𝜑 → (ϕ‘𝑃) = (𝑃 − 1))
172169, 171breqtrd 4870 . . 3 (𝜑 → ((od𝑃)‘𝐶) ∥ (𝑃 − 1))
173 prmuz2 15626 . . . . . . . . 9 (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ‘2))
17442, 173syl 17 . . . . . . . 8 (𝜑𝑃 ∈ (ℤ‘2))
175174, 55syl6eleq 2895 . . . . . . 7 (𝜑𝑃 ∈ (ℤ‘(1 + 1)))
176 eluzp1m1 11928 . . . . . . 7 ((1 ∈ ℤ ∧ 𝑃 ∈ (ℤ‘(1 + 1))) → (𝑃 − 1) ∈ (ℤ‘1))
17725, 175, 176sylancr 577 . . . . . 6 (𝜑 → (𝑃 − 1) ∈ (ℤ‘1))
178177, 26syl6eleqr 2896 . . . . 5 (𝜑 → (𝑃 − 1) ∈ ℕ)
179178nnzd 11747 . . . 4 (𝜑 → (𝑃 − 1) ∈ ℤ)
180 dvdstr 15241 . . . 4 (((𝑄↑(𝑄 pCnt 𝐴)) ∈ ℤ ∧ ((od𝑃)‘𝐶) ∈ ℤ ∧ (𝑃 − 1) ∈ ℤ) → (((𝑄↑(𝑄 pCnt 𝐴)) ∥ ((od𝑃)‘𝐶) ∧ ((od𝑃)‘𝐶) ∥ (𝑃 − 1)) → (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1)))
18124, 99, 179, 180syl3anc 1483 . . 3 (𝜑 → (((𝑄↑(𝑄 pCnt 𝐴)) ∥ ((od𝑃)‘𝐶) ∧ ((od𝑃)‘𝐶) ∥ (𝑃 − 1)) → (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1)))
182167, 172, 181mp2and 682 . 2 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1))
183 pcdvdsb 15790 . . 3 ((𝑄 ∈ ℙ ∧ (𝑃 − 1) ∈ ℤ ∧ (𝑄 pCnt 𝐴) ∈ ℕ0) → ((𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1)) ↔ (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1)))
1841, 179, 22, 183syl3anc 1483 . 2 (𝜑 → ((𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1)) ↔ (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1)))
185182, 184mpbird 248 1 (𝜑 → (𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1637  wcel 2156  wne 2978   class class class wbr 4844  cfv 6101  (class class class)co 6874  cc 10219  cr 10220  0cc0 10221  1c1 10222   + caddc 10224   · cmul 10226   < clt 10359  cle 10360  cmin 10551   / cdiv 10969  cn 11305  2c2 11356  0cn0 11559  cz 11643  cuz 11904   mod cmo 12892  cexp 13083  cdvds 15203   gcd cgcd 15435  cprime 15603  odcodz 15685  ϕcphi 15686   pCnt cpc 15758
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179  ax-cnex 10277  ax-resscn 10278  ax-1cn 10279  ax-icn 10280  ax-addcl 10281  ax-addrcl 10282  ax-mulcl 10283  ax-mulrcl 10284  ax-mulcom 10285  ax-addass 10286  ax-mulass 10287  ax-distr 10288  ax-i2m1 10289  ax-1ne0 10290  ax-1rid 10291  ax-rnegex 10292  ax-rrecex 10293  ax-cnre 10294  ax-pre-lttri 10295  ax-pre-lttrn 10296  ax-pre-ltadd 10297  ax-pre-mulgt0 10298  ax-pre-sup 10299
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-riota 6835  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-om 7296  df-1st 7398  df-2nd 7399  df-wrecs 7642  df-recs 7704  df-rdg 7742  df-1o 7796  df-2o 7797  df-oadd 7800  df-er 7979  df-map 8094  df-en 8193  df-dom 8194  df-sdom 8195  df-fin 8196  df-sup 8587  df-inf 8588  df-card 9048  df-cda 9275  df-pnf 10361  df-mnf 10362  df-xr 10363  df-ltxr 10364  df-le 10365  df-sub 10553  df-neg 10554  df-div 10970  df-nn 11306  df-2 11364  df-3 11365  df-n0 11560  df-xnn0 11630  df-z 11644  df-uz 11905  df-q 12008  df-rp 12047  df-fz 12550  df-fzo 12690  df-fl 12817  df-mod 12893  df-seq 13025  df-exp 13084  df-hash 13338  df-cj 14062  df-re 14063  df-im 14064  df-sqrt 14198  df-abs 14199  df-dvds 15204  df-gcd 15436  df-prm 15604  df-odz 15687  df-phi 15688  df-pc 15759
This theorem is referenced by:  pockthg  15827
  Copyright terms: Public domain W3C validator