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

Theorem pockthlem 15980
Description: Lemma for pockthg 15981. (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 15939 . . . . . . 7 ((𝑄 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (𝑄↑(𝑄 pCnt 𝐴)) ∥ 𝐴)
41, 2, 3syl2anc 581 . . . . . 6 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ 𝐴)
52nnzd 11809 . . . . . . . 8 (𝜑𝐴 ∈ ℤ)
6 pockthg.2 . . . . . . . . 9 (𝜑𝐵 ∈ ℕ)
76nnzd 11809 . . . . . . . 8 (𝜑𝐵 ∈ ℤ)
8 dvdsmul1 15380 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∥ (𝐴 · 𝐵))
95, 7, 8syl2anc 581 . . . . . . 7 (𝜑𝐴 ∥ (𝐴 · 𝐵))
10 pockthg.4 . . . . . . . . 9 (𝜑𝑁 = ((𝐴 · 𝐵) + 1))
1110oveq1d 6920 . . . . . . . 8 (𝜑 → (𝑁 − 1) = (((𝐴 · 𝐵) + 1) − 1))
122, 6nnmulcld 11404 . . . . . . . . . 10 (𝜑 → (𝐴 · 𝐵) ∈ ℕ)
1312nncnd 11368 . . . . . . . . 9 (𝜑 → (𝐴 · 𝐵) ∈ ℂ)
14 ax-1cn 10310 . . . . . . . . 9 1 ∈ ℂ
15 pncan 10607 . . . . . . . . 9 (((𝐴 · 𝐵) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐴 · 𝐵) + 1) − 1) = (𝐴 · 𝐵))
1613, 14, 15sylancl 582 . . . . . . . 8 (𝜑 → (((𝐴 · 𝐵) + 1) − 1) = (𝐴 · 𝐵))
1711, 16eqtrd 2861 . . . . . . 7 (𝜑 → (𝑁 − 1) = (𝐴 · 𝐵))
189, 17breqtrrd 4901 . . . . . 6 (𝜑𝐴 ∥ (𝑁 − 1))
19 prmnn 15760 . . . . . . . . . 10 (𝑄 ∈ ℙ → 𝑄 ∈ ℕ)
201, 19syl 17 . . . . . . . . 9 (𝜑𝑄 ∈ ℕ)
21 pockthlem.8 . . . . . . . . . 10 (𝜑 → (𝑄 pCnt 𝐴) ∈ ℕ)
2221nnnn0d 11678 . . . . . . . . 9 (𝜑 → (𝑄 pCnt 𝐴) ∈ ℕ0)
2320, 22nnexpcld 13326 . . . . . . . 8 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∈ ℕ)
2423nnzd 11809 . . . . . . 7 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∈ ℤ)
25 1z 11735 . . . . . . . . . 10 1 ∈ ℤ
26 nnuz 12005 . . . . . . . . . . . . 13 ℕ = (ℤ‘1)
2712, 26syl6eleq 2916 . . . . . . . . . . . 12 (𝜑 → (𝐴 · 𝐵) ∈ (ℤ‘1))
28 eluzp1p1 11994 . . . . . . . . . . . 12 ((𝐴 · 𝐵) ∈ (ℤ‘1) → ((𝐴 · 𝐵) + 1) ∈ (ℤ‘(1 + 1)))
2927, 28syl 17 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝐵) + 1) ∈ (ℤ‘(1 + 1)))
3010, 29eqeltrd 2906 . . . . . . . . . 10 (𝜑𝑁 ∈ (ℤ‘(1 + 1)))
31 eluzp1m1 11992 . . . . . . . . . 10 ((1 ∈ ℤ ∧ 𝑁 ∈ (ℤ‘(1 + 1))) → (𝑁 − 1) ∈ (ℤ‘1))
3225, 30, 31sylancr 583 . . . . . . . . 9 (𝜑 → (𝑁 − 1) ∈ (ℤ‘1))
3332, 26syl6eleqr 2917 . . . . . . . 8 (𝜑 → (𝑁 − 1) ∈ ℕ)
3433nnzd 11809 . . . . . . 7 (𝜑 → (𝑁 − 1) ∈ ℤ)
35 dvdstr 15395 . . . . . . 7 (((𝑄↑(𝑄 pCnt 𝐴)) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (((𝑄↑(𝑄 pCnt 𝐴)) ∥ 𝐴𝐴 ∥ (𝑁 − 1)) → (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1)))
3624, 5, 34, 35syl3anc 1496 . . . . . 6 (𝜑 → (((𝑄↑(𝑄 pCnt 𝐴)) ∥ 𝐴𝐴 ∥ (𝑁 − 1)) → (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1)))
374, 18, 36mp2and 692 . . . . 5 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1))
3823nnne0d 11401 . . . . . 6 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ≠ 0)
39 dvdsval2 15360 . . . . . 6 (((𝑄↑(𝑄 pCnt 𝐴)) ∈ ℤ ∧ (𝑄↑(𝑄 pCnt 𝐴)) ≠ 0 ∧ (𝑁 − 1) ∈ ℤ) → ((𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ))
4024, 38, 34, 39syl3anc 1496 . . . . 5 (𝜑 → ((𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ))
4137, 40mpbid 224 . . . 4 (𝜑 → ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ)
42 pockthlem.5 . . . . . . 7 (𝜑𝑃 ∈ ℙ)
43 prmnn 15760 . . . . . . 7 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
4442, 43syl 17 . . . . . 6 (𝜑𝑃 ∈ ℕ)
45 pockthlem.9 . . . . . 6 (𝜑𝐶 ∈ ℤ)
4644nnzd 11809 . . . . . . . . . . 11 (𝜑𝑃 ∈ ℤ)
47 gcddvds 15598 . . . . . . . . . . 11 ((𝐶 ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑃))
4845, 46, 47syl2anc 581 . . . . . . . . . 10 (𝜑 → ((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑃))
4948simpld 490 . . . . . . . . 9 (𝜑 → (𝐶 gcd 𝑃) ∥ 𝐶)
5048simprd 491 . . . . . . . . . 10 (𝜑 → (𝐶 gcd 𝑃) ∥ 𝑃)
51 pockthlem.6 . . . . . . . . . 10 (𝜑𝑃𝑁)
5245, 46gcdcld 15603 . . . . . . . . . . . 12 (𝜑 → (𝐶 gcd 𝑃) ∈ ℕ0)
5352nn0zd 11808 . . . . . . . . . . 11 (𝜑 → (𝐶 gcd 𝑃) ∈ ℤ)
54 df-2 11414 . . . . . . . . . . . . . . . 16 2 = (1 + 1)
5554fveq2i 6436 . . . . . . . . . . . . . . 15 (ℤ‘2) = (ℤ‘(1 + 1))
5630, 55syl6eleqr 2917 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ (ℤ‘2))
57 eluz2b2 12044 . . . . . . . . . . . . . 14 (𝑁 ∈ (ℤ‘2) ↔ (𝑁 ∈ ℕ ∧ 1 < 𝑁))
5856, 57sylib 210 . . . . . . . . . . . . 13 (𝜑 → (𝑁 ∈ ℕ ∧ 1 < 𝑁))
5958simpld 490 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℕ)
6059nnzd 11809 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℤ)
61 dvdstr 15395 . . . . . . . . . . 11 (((𝐶 gcd 𝑃) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝐶 gcd 𝑃) ∥ 𝑃𝑃𝑁) → (𝐶 gcd 𝑃) ∥ 𝑁))
6253, 46, 60, 61syl3anc 1496 . . . . . . . . . 10 (𝜑 → (((𝐶 gcd 𝑃) ∥ 𝑃𝑃𝑁) → (𝐶 gcd 𝑃) ∥ 𝑁))
6350, 51, 62mp2and 692 . . . . . . . . 9 (𝜑 → (𝐶 gcd 𝑃) ∥ 𝑁)
6459nnne0d 11401 . . . . . . . . . . 11 (𝜑𝑁 ≠ 0)
65 simpr 479 . . . . . . . . . . . 12 ((𝐶 = 0 ∧ 𝑁 = 0) → 𝑁 = 0)
6665necon3ai 3024 . . . . . . . . . . 11 (𝑁 ≠ 0 → ¬ (𝐶 = 0 ∧ 𝑁 = 0))
6764, 66syl 17 . . . . . . . . . 10 (𝜑 → ¬ (𝐶 = 0 ∧ 𝑁 = 0))
68 dvdslegcd 15599 . . . . . . . . . 10 ((((𝐶 gcd 𝑃) ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝐶 = 0 ∧ 𝑁 = 0)) → (((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑁) → (𝐶 gcd 𝑃) ≤ (𝐶 gcd 𝑁)))
6953, 45, 60, 67, 68syl31anc 1498 . . . . . . . . 9 (𝜑 → (((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑁) → (𝐶 gcd 𝑃) ≤ (𝐶 gcd 𝑁)))
7049, 63, 69mp2and 692 . . . . . . . 8 (𝜑 → (𝐶 gcd 𝑃) ≤ (𝐶 gcd 𝑁))
71 pockthlem.10 . . . . . . . . . . 11 (𝜑 → ((𝐶↑(𝑁 − 1)) mod 𝑁) = 1)
7271oveq1d 6920 . . . . . . . . . 10 (𝜑 → (((𝐶↑(𝑁 − 1)) mod 𝑁) gcd 𝑁) = (1 gcd 𝑁))
7333nnnn0d 11678 . . . . . . . . . . . 12 (𝜑 → (𝑁 − 1) ∈ ℕ0)
74 zexpcl 13169 . . . . . . . . . . . 12 ((𝐶 ∈ ℤ ∧ (𝑁 − 1) ∈ ℕ0) → (𝐶↑(𝑁 − 1)) ∈ ℤ)
7545, 73, 74syl2anc 581 . . . . . . . . . . 11 (𝜑 → (𝐶↑(𝑁 − 1)) ∈ ℤ)
76 modgcd 15626 . . . . . . . . . . 11 (((𝐶↑(𝑁 − 1)) ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐶↑(𝑁 − 1)) mod 𝑁) gcd 𝑁) = ((𝐶↑(𝑁 − 1)) gcd 𝑁))
7775, 59, 76syl2anc 581 . . . . . . . . . 10 (𝜑 → (((𝐶↑(𝑁 − 1)) mod 𝑁) gcd 𝑁) = ((𝐶↑(𝑁 − 1)) gcd 𝑁))
78 gcdcom 15608 . . . . . . . . . . . 12 ((1 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (1 gcd 𝑁) = (𝑁 gcd 1))
7925, 60, 78sylancr 583 . . . . . . . . . . 11 (𝜑 → (1 gcd 𝑁) = (𝑁 gcd 1))
80 gcd1 15622 . . . . . . . . . . . 12 (𝑁 ∈ ℤ → (𝑁 gcd 1) = 1)
8160, 80syl 17 . . . . . . . . . . 11 (𝜑 → (𝑁 gcd 1) = 1)
8279, 81eqtrd 2861 . . . . . . . . . 10 (𝜑 → (1 gcd 𝑁) = 1)
8372, 77, 823eqtr3d 2869 . . . . . . . . 9 (𝜑 → ((𝐶↑(𝑁 − 1)) gcd 𝑁) = 1)
84 rpexp 15803 . . . . . . . . . 10 ((𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁 − 1) ∈ ℕ) → (((𝐶↑(𝑁 − 1)) gcd 𝑁) = 1 ↔ (𝐶 gcd 𝑁) = 1))
8545, 60, 33, 84syl3anc 1496 . . . . . . . . 9 (𝜑 → (((𝐶↑(𝑁 − 1)) gcd 𝑁) = 1 ↔ (𝐶 gcd 𝑁) = 1))
8683, 85mpbid 224 . . . . . . . 8 (𝜑 → (𝐶 gcd 𝑁) = 1)
8770, 86breqtrd 4899 . . . . . . 7 (𝜑 → (𝐶 gcd 𝑃) ≤ 1)
8844nnne0d 11401 . . . . . . . . . 10 (𝜑𝑃 ≠ 0)
89 simpr 479 . . . . . . . . . . 11 ((𝐶 = 0 ∧ 𝑃 = 0) → 𝑃 = 0)
9089necon3ai 3024 . . . . . . . . . 10 (𝑃 ≠ 0 → ¬ (𝐶 = 0 ∧ 𝑃 = 0))
9188, 90syl 17 . . . . . . . . 9 (𝜑 → ¬ (𝐶 = 0 ∧ 𝑃 = 0))
92 gcdn0cl 15597 . . . . . . . . 9 (((𝐶 ∈ ℤ ∧ 𝑃 ∈ ℤ) ∧ ¬ (𝐶 = 0 ∧ 𝑃 = 0)) → (𝐶 gcd 𝑃) ∈ ℕ)
9345, 46, 91, 92syl21anc 873 . . . . . . . 8 (𝜑 → (𝐶 gcd 𝑃) ∈ ℕ)
94 nnle1eq1 11382 . . . . . . . 8 ((𝐶 gcd 𝑃) ∈ ℕ → ((𝐶 gcd 𝑃) ≤ 1 ↔ (𝐶 gcd 𝑃) = 1))
9593, 94syl 17 . . . . . . 7 (𝜑 → ((𝐶 gcd 𝑃) ≤ 1 ↔ (𝐶 gcd 𝑃) = 1))
9687, 95mpbid 224 . . . . . 6 (𝜑 → (𝐶 gcd 𝑃) = 1)
97 odzcl 15869 . . . . . 6 ((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) → ((od𝑃)‘𝐶) ∈ ℕ)
9844, 45, 96, 97syl3anc 1496 . . . . 5 (𝜑 → ((od𝑃)‘𝐶) ∈ ℕ)
9998nnzd 11809 . . . 4 (𝜑 → ((od𝑃)‘𝐶) ∈ ℤ)
10059nnred 11367 . . . . . . . . . 10 (𝜑𝑁 ∈ ℝ)
10158simprd 491 . . . . . . . . . 10 (𝜑 → 1 < 𝑁)
102 1mod 12997 . . . . . . . . . 10 ((𝑁 ∈ ℝ ∧ 1 < 𝑁) → (1 mod 𝑁) = 1)
103100, 101, 102syl2anc 581 . . . . . . . . 9 (𝜑 → (1 mod 𝑁) = 1)
10471, 103eqtr4d 2864 . . . . . . . 8 (𝜑 → ((𝐶↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁))
105 1zzd 11736 . . . . . . . . 9 (𝜑 → 1 ∈ ℤ)
106 moddvds 15368 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ (𝐶↑(𝑁 − 1)) ∈ ℤ ∧ 1 ∈ ℤ) → (((𝐶↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1)))
10759, 75, 105, 106syl3anc 1496 . . . . . . . 8 (𝜑 → (((𝐶↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1)))
108104, 107mpbid 224 . . . . . . 7 (𝜑𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1))
109 peano2zm 11748 . . . . . . . . 9 ((𝐶↑(𝑁 − 1)) ∈ ℤ → ((𝐶↑(𝑁 − 1)) − 1) ∈ ℤ)
11075, 109syl 17 . . . . . . . 8 (𝜑 → ((𝐶↑(𝑁 − 1)) − 1) ∈ ℤ)
111 dvdstr 15395 . . . . . . . 8 ((𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝐶↑(𝑁 − 1)) − 1) ∈ ℤ) → ((𝑃𝑁𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1)) → 𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1)))
11246, 60, 110, 111syl3anc 1496 . . . . . . 7 (𝜑 → ((𝑃𝑁𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1)) → 𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1)))
11351, 108, 112mp2and 692 . . . . . 6 (𝜑𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1))
114 odzdvds 15871 . . . . . . 7 (((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) ∧ (𝑁 − 1) ∈ ℕ0) → (𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1) ↔ ((od𝑃)‘𝐶) ∥ (𝑁 − 1)))
11544, 45, 96, 73, 114syl31anc 1498 . . . . . 6 (𝜑 → (𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1) ↔ ((od𝑃)‘𝐶) ∥ (𝑁 − 1)))
116113, 115mpbid 224 . . . . 5 (𝜑 → ((od𝑃)‘𝐶) ∥ (𝑁 − 1))
11733nncnd 11368 . . . . . 6 (𝜑 → (𝑁 − 1) ∈ ℂ)
11823nncnd 11368 . . . . . 6 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∈ ℂ)
119117, 118, 38divcan1d 11128 . . . . 5 (𝜑 → (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) = (𝑁 − 1))
120116, 119breqtrrd 4901 . . . 4 (𝜑 → ((od𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))))
121 nprmdvds1 15789 . . . . . 6 (𝑃 ∈ ℙ → ¬ 𝑃 ∥ 1)
12242, 121syl 17 . . . . 5 (𝜑 → ¬ 𝑃 ∥ 1)
12320nnzd 11809 . . . . . . . . . . . . . 14 (𝜑𝑄 ∈ ℤ)
124 iddvdsexp 15382 . . . . . . . . . . . . . 14 ((𝑄 ∈ ℤ ∧ (𝑄 pCnt 𝐴) ∈ ℕ) → 𝑄 ∥ (𝑄↑(𝑄 pCnt 𝐴)))
125123, 21, 124syl2anc 581 . . . . . . . . . . . . 13 (𝜑𝑄 ∥ (𝑄↑(𝑄 pCnt 𝐴)))
126 dvdstr 15395 . . . . . . . . . . . . . 14 ((𝑄 ∈ ℤ ∧ (𝑄↑(𝑄 pCnt 𝐴)) ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → ((𝑄 ∥ (𝑄↑(𝑄 pCnt 𝐴)) ∧ (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1)) → 𝑄 ∥ (𝑁 − 1)))
127123, 24, 34, 126syl3anc 1496 . . . . . . . . . . . . 13 (𝜑 → ((𝑄 ∥ (𝑄↑(𝑄 pCnt 𝐴)) ∧ (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1)) → 𝑄 ∥ (𝑁 − 1)))
128125, 37, 127mp2and 692 . . . . . . . . . . . 12 (𝜑𝑄 ∥ (𝑁 − 1))
12920nnne0d 11401 . . . . . . . . . . . . 13 (𝜑𝑄 ≠ 0)
130 dvdsval2 15360 . . . . . . . . . . . . 13 ((𝑄 ∈ ℤ ∧ 𝑄 ≠ 0 ∧ (𝑁 − 1) ∈ ℤ) → (𝑄 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 𝑄) ∈ ℤ))
131123, 129, 34, 130syl3anc 1496 . . . . . . . . . . . 12 (𝜑 → (𝑄 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 𝑄) ∈ ℤ))
132128, 131mpbid 224 . . . . . . . . . . 11 (𝜑 → ((𝑁 − 1) / 𝑄) ∈ ℤ)
13373nn0ge0d 11681 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (𝑁 − 1))
13433nnred 11367 . . . . . . . . . . . . 13 (𝜑 → (𝑁 − 1) ∈ ℝ)
13520nnred 11367 . . . . . . . . . . . . 13 (𝜑𝑄 ∈ ℝ)
13620nngt0d 11400 . . . . . . . . . . . . 13 (𝜑 → 0 < 𝑄)
137 ge0div 11220 . . . . . . . . . . . . 13 (((𝑁 − 1) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ 0 < 𝑄) → (0 ≤ (𝑁 − 1) ↔ 0 ≤ ((𝑁 − 1) / 𝑄)))
138134, 135, 136, 137syl3anc 1496 . . . . . . . . . . . 12 (𝜑 → (0 ≤ (𝑁 − 1) ↔ 0 ≤ ((𝑁 − 1) / 𝑄)))
139133, 138mpbid 224 . . . . . . . . . . 11 (𝜑 → 0 ≤ ((𝑁 − 1) / 𝑄))
140 elnn0z 11717 . . . . . . . . . . 11 (((𝑁 − 1) / 𝑄) ∈ ℕ0 ↔ (((𝑁 − 1) / 𝑄) ∈ ℤ ∧ 0 ≤ ((𝑁 − 1) / 𝑄)))
141132, 139, 140sylanbrc 580 . . . . . . . . . 10 (𝜑 → ((𝑁 − 1) / 𝑄) ∈ ℕ0)
142 zexpcl 13169 . . . . . . . . . 10 ((𝐶 ∈ ℤ ∧ ((𝑁 − 1) / 𝑄) ∈ ℕ0) → (𝐶↑((𝑁 − 1) / 𝑄)) ∈ ℤ)
14345, 141, 142syl2anc 581 . . . . . . . . 9 (𝜑 → (𝐶↑((𝑁 − 1) / 𝑄)) ∈ ℤ)
144 peano2zm 11748 . . . . . . . . 9 ((𝐶↑((𝑁 − 1) / 𝑄)) ∈ ℤ → ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∈ ℤ)
145143, 144syl 17 . . . . . . . 8 (𝜑 → ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∈ ℤ)
146 dvdsgcd 15634 . . . . . . . 8 ((𝑃 ∈ ℤ ∧ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∧ 𝑃𝑁) → 𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁)))
14746, 145, 60, 146syl3anc 1496 . . . . . . 7 (𝜑 → ((𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∧ 𝑃𝑁) → 𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁)))
14851, 147mpan2d 687 . . . . . 6 (𝜑 → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) → 𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁)))
149 odzdvds 15871 . . . . . . . 8 (((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) ∧ ((𝑁 − 1) / 𝑄) ∈ ℕ0) → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ↔ ((od𝑃)‘𝐶) ∥ ((𝑁 − 1) / 𝑄)))
15044, 45, 96, 141, 149syl31anc 1498 . . . . . . 7 (𝜑 → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ↔ ((od𝑃)‘𝐶) ∥ ((𝑁 − 1) / 𝑄)))
15120nncnd 11368 . . . . . . . . . . 11 (𝜑𝑄 ∈ ℂ)
15221nnzd 11809 . . . . . . . . . . 11 (𝜑 → (𝑄 pCnt 𝐴) ∈ ℤ)
153151, 129, 152expm1d 13312 . . . . . . . . . 10 (𝜑 → (𝑄↑((𝑄 pCnt 𝐴) − 1)) = ((𝑄↑(𝑄 pCnt 𝐴)) / 𝑄))
154153oveq2d 6921 . . . . . . . . 9 (𝜑 → (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) = (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · ((𝑄↑(𝑄 pCnt 𝐴)) / 𝑄)))
155134, 23nndivred 11405 . . . . . . . . . . 11 (𝜑 → ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℝ)
156155recnd 10385 . . . . . . . . . 10 (𝜑 → ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℂ)
157156, 118, 151, 129divassd 11162 . . . . . . . . 9 (𝜑 → ((((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) / 𝑄) = (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · ((𝑄↑(𝑄 pCnt 𝐴)) / 𝑄)))
158119oveq1d 6920 . . . . . . . . 9 (𝜑 → ((((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) / 𝑄) = ((𝑁 − 1) / 𝑄))
159154, 157, 1583eqtr2d 2867 . . . . . . . 8 (𝜑 → (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) = ((𝑁 − 1) / 𝑄))
160159breq2d 4885 . . . . . . 7 (𝜑 → (((od𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) ↔ ((od𝑃)‘𝐶) ∥ ((𝑁 − 1) / 𝑄)))
161150, 160bitr4d 274 . . . . . 6 (𝜑 → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ↔ ((od𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1)))))
162 pockthlem.11 . . . . . . 7 (𝜑 → (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁) = 1)
163162breq2d 4885 . . . . . 6 (𝜑 → (𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁) ↔ 𝑃 ∥ 1))
164148, 161, 1633imtr3d 285 . . . . 5 (𝜑 → (((od𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) → 𝑃 ∥ 1))
165122, 164mtod 190 . . . 4 (𝜑 → ¬ ((od𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))))
166 prmpwdvds 15979 . . . 4 (((((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ ∧ ((od𝑃)‘𝐶) ∈ ℤ) ∧ (𝑄 ∈ ℙ ∧ (𝑄 pCnt 𝐴) ∈ ℕ) ∧ (((od𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) ∧ ¬ ((od𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))))) → (𝑄↑(𝑄 pCnt 𝐴)) ∥ ((od𝑃)‘𝐶))
16741, 99, 1, 21, 120, 165, 166syl222anc 1511 . . 3 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ ((od𝑃)‘𝐶))
168 odzphi 15872 . . . . 5 ((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) → ((od𝑃)‘𝐶) ∥ (ϕ‘𝑃))
16944, 45, 96, 168syl3anc 1496 . . . 4 (𝜑 → ((od𝑃)‘𝐶) ∥ (ϕ‘𝑃))
170 phiprm 15853 . . . . 5 (𝑃 ∈ ℙ → (ϕ‘𝑃) = (𝑃 − 1))
17142, 170syl 17 . . . 4 (𝜑 → (ϕ‘𝑃) = (𝑃 − 1))
172169, 171breqtrd 4899 . . 3 (𝜑 → ((od𝑃)‘𝐶) ∥ (𝑃 − 1))
173 prmuz2 15780 . . . . . . . . 9 (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ‘2))
17442, 173syl 17 . . . . . . . 8 (𝜑𝑃 ∈ (ℤ‘2))
175174, 55syl6eleq 2916 . . . . . . 7 (𝜑𝑃 ∈ (ℤ‘(1 + 1)))
176 eluzp1m1 11992 . . . . . . 7 ((1 ∈ ℤ ∧ 𝑃 ∈ (ℤ‘(1 + 1))) → (𝑃 − 1) ∈ (ℤ‘1))
17725, 175, 176sylancr 583 . . . . . 6 (𝜑 → (𝑃 − 1) ∈ (ℤ‘1))
178177, 26syl6eleqr 2917 . . . . 5 (𝜑 → (𝑃 − 1) ∈ ℕ)
179178nnzd 11809 . . . 4 (𝜑 → (𝑃 − 1) ∈ ℤ)
180 dvdstr 15395 . . . 4 (((𝑄↑(𝑄 pCnt 𝐴)) ∈ ℤ ∧ ((od𝑃)‘𝐶) ∈ ℤ ∧ (𝑃 − 1) ∈ ℤ) → (((𝑄↑(𝑄 pCnt 𝐴)) ∥ ((od𝑃)‘𝐶) ∧ ((od𝑃)‘𝐶) ∥ (𝑃 − 1)) → (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1)))
18124, 99, 179, 180syl3anc 1496 . . 3 (𝜑 → (((𝑄↑(𝑄 pCnt 𝐴)) ∥ ((od𝑃)‘𝐶) ∧ ((od𝑃)‘𝐶) ∥ (𝑃 − 1)) → (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1)))
182167, 172, 181mp2and 692 . 2 (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1))
183 pcdvdsb 15944 . . 3 ((𝑄 ∈ ℙ ∧ (𝑃 − 1) ∈ ℤ ∧ (𝑄 pCnt 𝐴) ∈ ℕ0) → ((𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1)) ↔ (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1)))
1841, 179, 22, 183syl3anc 1496 . 2 (𝜑 → ((𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1)) ↔ (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1)))
185182, 184mpbird 249 1 (𝜑 → (𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386   = wceq 1658  wcel 2166  wne 2999   class class class wbr 4873  cfv 6123  (class class class)co 6905  cc 10250  cr 10251  0cc0 10252  1c1 10253   + caddc 10255   · cmul 10257   < clt 10391  cle 10392  cmin 10585   / cdiv 11009  cn 11350  2c2 11406  0cn0 11618  cz 11704  cuz 11968   mod cmo 12963  cexp 13154  cdvds 15357   gcd cgcd 15589  cprime 15757  odcodz 15839  ϕcphi 15840   pCnt cpc 15912
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-rep 4994  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209  ax-cnex 10308  ax-resscn 10309  ax-1cn 10310  ax-icn 10311  ax-addcl 10312  ax-addrcl 10313  ax-mulcl 10314  ax-mulrcl 10315  ax-mulcom 10316  ax-addass 10317  ax-mulass 10318  ax-distr 10319  ax-i2m1 10320  ax-1ne0 10321  ax-1rid 10322  ax-rnegex 10323  ax-rrecex 10324  ax-cnre 10325  ax-pre-lttri 10326  ax-pre-lttrn 10327  ax-pre-ltadd 10328  ax-pre-mulgt0 10329  ax-pre-sup 10330
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4659  df-int 4698  df-iun 4742  df-br 4874  df-opab 4936  df-mpt 4953  df-tr 4976  df-id 5250  df-eprel 5255  df-po 5263  df-so 5264  df-fr 5301  df-we 5303  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-pred 5920  df-ord 5966  df-on 5967  df-lim 5968  df-suc 5969  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-riota 6866  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-om 7327  df-1st 7428  df-2nd 7429  df-wrecs 7672  df-recs 7734  df-rdg 7772  df-1o 7826  df-2o 7827  df-oadd 7830  df-er 8009  df-map 8124  df-en 8223  df-dom 8224  df-sdom 8225  df-fin 8226  df-sup 8617  df-inf 8618  df-card 9078  df-cda 9305  df-pnf 10393  df-mnf 10394  df-xr 10395  df-ltxr 10396  df-le 10397  df-sub 10587  df-neg 10588  df-div 11010  df-nn 11351  df-2 11414  df-3 11415  df-n0 11619  df-xnn0 11691  df-z 11705  df-uz 11969  df-q 12072  df-rp 12113  df-fz 12620  df-fzo 12761  df-fl 12888  df-mod 12964  df-seq 13096  df-exp 13155  df-hash 13411  df-cj 14216  df-re 14217  df-im 14218  df-sqrt 14352  df-abs 14353  df-dvds 15358  df-gcd 15590  df-prm 15758  df-odz 15841  df-phi 15842  df-pc 15913
This theorem is referenced by:  pockthg  15981
  Copyright terms: Public domain W3C validator