Metamath Proof Explorer

Theorem pockthlem

Description: Lemma for pockthg . (Contributed by Mario Carneiro, 2-Mar-2014)

Ref Expression
Hypotheses 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 pockthlem ( 𝜑 → ( 𝑄 pCnt 𝐴 ) ≤ ( 𝑄 pCnt ( 𝑃 − 1 ) ) )

Proof

Step Hyp Ref Expression
1 pockthg.1 ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
2 pockthg.2 ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
3 pockthg.3 ⊢ ( 𝜑 → 𝐵 < 𝐴 )
4 pockthg.4 ⊢ ( 𝜑 → 𝑁 = ( ( 𝐴 · 𝐵 ) + 1 ) )
5 pockthlem.5 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
6 pockthlem.6 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
7 pockthlem.7 ⊢ ( 𝜑 → 𝑄 ∈ ℙ )
8 pockthlem.8 ⊢ ( 𝜑 → ( 𝑄 pCnt 𝐴 ) ∈ ℕ )
9 pockthlem.9 ⊢ ( 𝜑 → 𝐶 ∈ ℤ )
10 pockthlem.10 ⊢ ( 𝜑 → ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) = 1 )
11 pockthlem.11 ⊢ ( 𝜑 → ( ( ( 𝐶 ↑ ( ( 𝑁 − 1 ) / 𝑄 ) ) − 1 ) gcd 𝑁 ) = 1 )
12 prmnn ⊢ ( 𝑄 ∈ ℙ → 𝑄 ∈ ℕ )
13 7 12 syl ⊢ ( 𝜑 → 𝑄 ∈ ℕ )
14 8 nnnn0d ⊢ ( 𝜑 → ( 𝑄 pCnt 𝐴 ) ∈ ℕ0 )
15 13 14 nnexpcld ⊢ ( 𝜑 → ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ∈ ℕ )
16 15 nnzd ⊢ ( 𝜑 → ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ∈ ℤ )
17 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
18 5 17 syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
19 18 nnzd ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
20 gcddvds ⊢ ( ( 𝐶 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 𝐶 gcd 𝑃 ) ∥ 𝐶 ∧ ( 𝐶 gcd 𝑃 ) ∥ 𝑃 ) )
21 9 19 20 syl2anc ⊢ ( 𝜑 → ( ( 𝐶 gcd 𝑃 ) ∥ 𝐶 ∧ ( 𝐶 gcd 𝑃 ) ∥ 𝑃 ) )
22 21 simpld ⊢ ( 𝜑 → ( 𝐶 gcd 𝑃 ) ∥ 𝐶 )
23 9 19 gcdcld ⊢ ( 𝜑 → ( 𝐶 gcd 𝑃 ) ∈ ℕ0 )
24 23 nn0zd ⊢ ( 𝜑 → ( 𝐶 gcd 𝑃 ) ∈ ℤ )
25 1 2 nnmulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ∈ ℕ )
26 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
27 25 26 eleqtrdi ⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) )
28 eluzp1p1 ⊢ ( ( 𝐴 · 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) → ( ( 𝐴 · 𝐵 ) + 1 ) ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) )
29 27 28 syl ⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) + 1 ) ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) )
30 4 29 eqeltrd ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) )
31 df-2 ⊢ 2 = ( 1 + 1 )
32 31 fveq2i ⊢ ( ℤ≥ ‘ 2 ) = ( ℤ≥ ‘ ( 1 + 1 ) )
33 30 32 eleqtrrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
34 eluz2b2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑁 ∈ ℕ ∧ 1 < 𝑁 ) )
35 33 34 sylib ⊢ ( 𝜑 → ( 𝑁 ∈ ℕ ∧ 1 < 𝑁 ) )
36 35 simpld ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
37 36 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
38 21 simprd ⊢ ( 𝜑 → ( 𝐶 gcd 𝑃 ) ∥ 𝑃 )
39 24 19 37 38 6 dvdstrd ⊢ ( 𝜑 → ( 𝐶 gcd 𝑃 ) ∥ 𝑁 )
40 36 nnne0d ⊢ ( 𝜑 → 𝑁 ≠ 0 )
41 simpr ⊢ ( ( 𝐶 = 0 ∧ 𝑁 = 0 ) → 𝑁 = 0 )
42 41 necon3ai ⊢ ( 𝑁 ≠ 0 → ¬ ( 𝐶 = 0 ∧ 𝑁 = 0 ) )
43 40 42 syl ⊢ ( 𝜑 → ¬ ( 𝐶 = 0 ∧ 𝑁 = 0 ) )
44 dvdslegcd ⊢ ( ( ( ( 𝐶 gcd 𝑃 ) ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝐶 = 0 ∧ 𝑁 = 0 ) ) → ( ( ( 𝐶 gcd 𝑃 ) ∥ 𝐶 ∧ ( 𝐶 gcd 𝑃 ) ∥ 𝑁 ) → ( 𝐶 gcd 𝑃 ) ≤ ( 𝐶 gcd 𝑁 ) ) )
45 24 9 37 43 44 syl31anc ⊢ ( 𝜑 → ( ( ( 𝐶 gcd 𝑃 ) ∥ 𝐶 ∧ ( 𝐶 gcd 𝑃 ) ∥ 𝑁 ) → ( 𝐶 gcd 𝑃 ) ≤ ( 𝐶 gcd 𝑁 ) ) )
46 22 39 45 mp2and ⊢ ( 𝜑 → ( 𝐶 gcd 𝑃 ) ≤ ( 𝐶 gcd 𝑁 ) )
47 10 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) gcd 𝑁 ) = ( 1 gcd 𝑁 ) )
48 1z ⊢ 1 ∈ ℤ
49 eluzp1m1 ⊢ ( ( 1 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 1 ) )
50 48 30 49 sylancr ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 1 ) )
51 50 26 eleqtrrdi ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℕ )
52 51 nnnn0d ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℕ0 )
53 zexpcl ⊢ ( ( 𝐶 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℕ0 ) → ( 𝐶 ↑ ( 𝑁 − 1 ) ) ∈ ℤ )
54 9 52 53 syl2anc ⊢ ( 𝜑 → ( 𝐶 ↑ ( 𝑁 − 1 ) ) ∈ ℤ )
55 modgcd ⊢ ( ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) gcd 𝑁 ) = ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) gcd 𝑁 ) )
56 54 36 55 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) gcd 𝑁 ) = ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) gcd 𝑁 ) )
57 gcdcom ⊢ ( ( 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 1 gcd 𝑁 ) = ( 𝑁 gcd 1 ) )
58 48 37 57 sylancr ⊢ ( 𝜑 → ( 1 gcd 𝑁 ) = ( 𝑁 gcd 1 ) )
59 gcd1 ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 gcd 1 ) = 1 )
60 37 59 syl ⊢ ( 𝜑 → ( 𝑁 gcd 1 ) = 1 )
61 58 60 eqtrd ⊢ ( 𝜑 → ( 1 gcd 𝑁 ) = 1 )
62 47 56 61 3eqtr3d ⊢ ( 𝜑 → ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) gcd 𝑁 ) = 1 )
63 rpexp ⊢ ( ( 𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℕ ) → ( ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) gcd 𝑁 ) = 1 ↔ ( 𝐶 gcd 𝑁 ) = 1 ) )
64 9 37 51 63 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) gcd 𝑁 ) = 1 ↔ ( 𝐶 gcd 𝑁 ) = 1 ) )
65 62 64 mpbid ⊢ ( 𝜑 → ( 𝐶 gcd 𝑁 ) = 1 )
66 46 65 breqtrd ⊢ ( 𝜑 → ( 𝐶 gcd 𝑃 ) ≤ 1 )
67 18 nnne0d ⊢ ( 𝜑 → 𝑃 ≠ 0 )
68 simpr ⊢ ( ( 𝐶 = 0 ∧ 𝑃 = 0 ) → 𝑃 = 0 )
69 68 necon3ai ⊢ ( 𝑃 ≠ 0 → ¬ ( 𝐶 = 0 ∧ 𝑃 = 0 ) )
70 67 69 syl ⊢ ( 𝜑 → ¬ ( 𝐶 = 0 ∧ 𝑃 = 0 ) )
71 gcdn0cl ⊢ ( ( ( 𝐶 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ∧ ¬ ( 𝐶 = 0 ∧ 𝑃 = 0 ) ) → ( 𝐶 gcd 𝑃 ) ∈ ℕ )
72 9 19 70 71 syl21anc ⊢ ( 𝜑 → ( 𝐶 gcd 𝑃 ) ∈ ℕ )
73 nnle1eq1 ⊢ ( ( 𝐶 gcd 𝑃 ) ∈ ℕ → ( ( 𝐶 gcd 𝑃 ) ≤ 1 ↔ ( 𝐶 gcd 𝑃 ) = 1 ) )
74 72 73 syl ⊢ ( 𝜑 → ( ( 𝐶 gcd 𝑃 ) ≤ 1 ↔ ( 𝐶 gcd 𝑃 ) = 1 ) )
75 66 74 mpbid ⊢ ( 𝜑 → ( 𝐶 gcd 𝑃 ) = 1 )
76 odzcl ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ ( 𝐶 gcd 𝑃 ) = 1 ) → ( ( odℤ ‘ 𝑃 ) ‘ 𝐶 ) ∈ ℕ )
77 18 9 75 76 syl3anc ⊢ ( 𝜑 → ( ( odℤ ‘ 𝑃 ) ‘ 𝐶 ) ∈ ℕ )
78 77 nnzd ⊢ ( 𝜑 → ( ( odℤ ‘ 𝑃 ) ‘ 𝐶 ) ∈ ℤ )
79 prmuz2 ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
80 5 79 syl ⊢ ( 𝜑 → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
81 80 32 eleqtrdi ⊢ ( 𝜑 → 𝑃 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) )
82 eluzp1m1 ⊢ ( ( 1 ∈ ℤ ∧ 𝑃 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( 𝑃 − 1 ) ∈ ( ℤ≥ ‘ 1 ) )
83 48 81 82 sylancr ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ( ℤ≥ ‘ 1 ) )
84 83 26 eleqtrrdi ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℕ )
85 84 nnzd ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℤ )
86 1 nnzd ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
87 51 nnzd ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℤ )
88 pcdvds ⊢ ( ( 𝑄 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ∥ 𝐴 )
89 7 1 88 syl2anc ⊢ ( 𝜑 → ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ∥ 𝐴 )
90 2 nnzd ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
91 dvdsmul1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐴 ∥ ( 𝐴 · 𝐵 ) )
92 86 90 91 syl2anc ⊢ ( 𝜑 → 𝐴 ∥ ( 𝐴 · 𝐵 ) )
93 4 oveq1d ⊢ ( 𝜑 → ( 𝑁 − 1 ) = ( ( ( 𝐴 · 𝐵 ) + 1 ) − 1 ) )
94 25 nncnd ⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ∈ ℂ )
95 ax-1cn ⊢ 1 ∈ ℂ
96 pncan ⊢ ( ( ( 𝐴 · 𝐵 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 𝐴 · 𝐵 ) + 1 ) − 1 ) = ( 𝐴 · 𝐵 ) )
97 94 95 96 sylancl ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐵 ) + 1 ) − 1 ) = ( 𝐴 · 𝐵 ) )
98 93 97 eqtrd ⊢ ( 𝜑 → ( 𝑁 − 1 ) = ( 𝐴 · 𝐵 ) )
99 92 98 breqtrrd ⊢ ( 𝜑 → 𝐴 ∥ ( 𝑁 − 1 ) )
100 16 86 87 89 99 dvdstrd ⊢ ( 𝜑 → ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ∥ ( 𝑁 − 1 ) )
101 15 nnne0d ⊢ ( 𝜑 → ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ≠ 0 )
102 dvdsval2 ⊢ ( ( ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ∈ ℤ ∧ ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ≠ 0 ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ∥ ( 𝑁 − 1 ) ↔ ( ( 𝑁 − 1 ) / ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ) ∈ ℤ ) )
103 16 101 87 102 syl3anc ⊢ ( 𝜑 → ( ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ∥ ( 𝑁 − 1 ) ↔ ( ( 𝑁 − 1 ) / ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ) ∈ ℤ ) )
104 100 103 mpbid ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) / ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ) ∈ ℤ )
105 peano2zm ⊢ ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) ∈ ℤ → ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) − 1 ) ∈ ℤ )
106 54 105 syl ⊢ ( 𝜑 → ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) − 1 ) ∈ ℤ )
107 36 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
108 35 simprd ⊢ ( 𝜑 → 1 < 𝑁 )
109 1mod ⊢ ( ( 𝑁 ∈ ℝ ∧ 1 < 𝑁 ) → ( 1 mod 𝑁 ) = 1 )
110 107 108 109 syl2anc ⊢ ( 𝜑 → ( 1 mod 𝑁 ) = 1 )
111 10 110 eqtr4d ⊢ ( 𝜑 → ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) = ( 1 mod 𝑁 ) )
112 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
113 moddvds ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ↑ ( 𝑁 − 1 ) ) ∈ ℤ ∧ 1 ∈ ℤ ) → ( ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) = ( 1 mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) − 1 ) ) )
114 36 54 112 113 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) mod 𝑁 ) = ( 1 mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) − 1 ) ) )
115 111 114 mpbid ⊢ ( 𝜑 → 𝑁 ∥ ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) − 1 ) )
116 19 37 106 6 115 dvdstrd ⊢ ( 𝜑 → 𝑃 ∥ ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) − 1 ) )
117 odzdvds ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ ( 𝐶 gcd 𝑃 ) = 1 ) ∧ ( 𝑁 − 1 ) ∈ ℕ0 ) → ( 𝑃 ∥ ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) − 1 ) ↔ ( ( odℤ ‘ 𝑃 ) ‘ 𝐶 ) ∥ ( 𝑁 − 1 ) ) )
118 18 9 75 52 117 syl31anc ⊢ ( 𝜑 → ( 𝑃 ∥ ( ( 𝐶 ↑ ( 𝑁 − 1 ) ) − 1 ) ↔ ( ( odℤ ‘ 𝑃 ) ‘ 𝐶 ) ∥ ( 𝑁 − 1 ) ) )
119 116 118 mpbid ⊢ ( 𝜑 → ( ( odℤ ‘ 𝑃 ) ‘ 𝐶 ) ∥ ( 𝑁 − 1 ) )
120 51 nncnd ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℂ )
121 15 nncnd ⊢ ( 𝜑 → ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ∈ ℂ )
122 120 121 101 divcan1d ⊢ ( 𝜑 → ( ( ( 𝑁 − 1 ) / ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ) · ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ) = ( 𝑁 − 1 ) )
123 119 122 breqtrrd ⊢ ( 𝜑 → ( ( odℤ ‘ 𝑃 ) ‘ 𝐶 ) ∥ ( ( ( 𝑁 − 1 ) / ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ) · ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ) )
124 nprmdvds1 ⊢ ( 𝑃 ∈ ℙ → ¬ 𝑃 ∥ 1 )
125 5 124 syl ⊢ ( 𝜑 → ¬ 𝑃 ∥ 1 )
126 13 nnzd ⊢ ( 𝜑 → 𝑄 ∈ ℤ )
127 iddvdsexp ⊢ ( ( 𝑄 ∈ ℤ ∧ ( 𝑄 pCnt 𝐴 ) ∈ ℕ ) → 𝑄 ∥ ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) )
128 126 8 127 syl2anc ⊢ ( 𝜑 → 𝑄 ∥ ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) )
129 126 16 87 128 100 dvdstrd ⊢ ( 𝜑 → 𝑄 ∥ ( 𝑁 − 1 ) )
130 13 nnne0d ⊢ ( 𝜑 → 𝑄 ≠ 0 )
131 dvdsval2 ⊢ ( ( 𝑄 ∈ ℤ ∧ 𝑄 ≠ 0 ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( 𝑄 ∥ ( 𝑁 − 1 ) ↔ ( ( 𝑁 − 1 ) / 𝑄 ) ∈ ℤ ) )
132 126 130 87 131 syl3anc ⊢ ( 𝜑 → ( 𝑄 ∥ ( 𝑁 − 1 ) ↔ ( ( 𝑁 − 1 ) / 𝑄 ) ∈ ℤ ) )
133 129 132 mpbid ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) / 𝑄 ) ∈ ℤ )
134 52 nn0ge0d ⊢ ( 𝜑 → 0 ≤ ( 𝑁 − 1 ) )
135 51 nnred ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℝ )
136 13 nnred ⊢ ( 𝜑 → 𝑄 ∈ ℝ )
137 13 nngt0d ⊢ ( 𝜑 → 0 < 𝑄 )
138 ge0div ⊢ ( ( ( 𝑁 − 1 ) ∈ ℝ ∧ 𝑄 ∈ ℝ ∧ 0 < 𝑄 ) → ( 0 ≤ ( 𝑁 − 1 ) ↔ 0 ≤ ( ( 𝑁 − 1 ) / 𝑄 ) ) )
139 135 136 137 138 syl3anc ⊢ ( 𝜑 → ( 0 ≤ ( 𝑁 − 1 ) ↔ 0 ≤ ( ( 𝑁 − 1 ) / 𝑄 ) ) )
140 134 139 mpbid ⊢ ( 𝜑 → 0 ≤ ( ( 𝑁 − 1 ) / 𝑄 ) )
141 elnn0z ⊢ ( ( ( 𝑁 − 1 ) / 𝑄 ) ∈ ℕ0 ↔ ( ( ( 𝑁 − 1 ) / 𝑄 ) ∈ ℤ ∧ 0 ≤ ( ( 𝑁 − 1 ) / 𝑄 ) ) )
142 133 140 141 sylanbrc ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) / 𝑄 ) ∈ ℕ0 )
143 zexpcl ⊢ ( ( 𝐶 ∈ ℤ ∧ ( ( 𝑁 − 1 ) / 𝑄 ) ∈ ℕ0 ) → ( 𝐶 ↑ ( ( 𝑁 − 1 ) / 𝑄 ) ) ∈ ℤ )
144 9 142 143 syl2anc ⊢ ( 𝜑 → ( 𝐶 ↑ ( ( 𝑁 − 1 ) / 𝑄 ) ) ∈ ℤ )
145 peano2zm ⊢ ( ( 𝐶 ↑ ( ( 𝑁 − 1 ) / 𝑄 ) ) ∈ ℤ → ( ( 𝐶 ↑ ( ( 𝑁 − 1 ) / 𝑄 ) ) − 1 ) ∈ ℤ )
146 144 145 syl ⊢ ( 𝜑 → ( ( 𝐶 ↑ ( ( 𝑁 − 1 ) / 𝑄 ) ) − 1 ) ∈ ℤ )
147 dvdsgcd ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 𝐶 ↑ ( ( 𝑁 − 1 ) / 𝑄 ) ) − 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑃 ∥ ( ( 𝐶 ↑ ( ( 𝑁 − 1 ) / 𝑄 ) ) − 1 ) ∧ 𝑃 ∥ 𝑁 ) → 𝑃 ∥ ( ( ( 𝐶 ↑ ( ( 𝑁 − 1 ) / 𝑄 ) ) − 1 ) gcd 𝑁 ) ) )
148 19 146 37 147 syl3anc ⊢ ( 𝜑 → ( ( 𝑃 ∥ ( ( 𝐶 ↑ ( ( 𝑁 − 1 ) / 𝑄 ) ) − 1 ) ∧ 𝑃 ∥ 𝑁 ) → 𝑃 ∥ ( ( ( 𝐶 ↑ ( ( 𝑁 − 1 ) / 𝑄 ) ) − 1 ) gcd 𝑁 ) ) )
149 6 148 mpan2d ⊢ ( 𝜑 → ( 𝑃 ∥ ( ( 𝐶 ↑ ( ( 𝑁 − 1 ) / 𝑄 ) ) − 1 ) → 𝑃 ∥ ( ( ( 𝐶 ↑ ( ( 𝑁 − 1 ) / 𝑄 ) ) − 1 ) gcd 𝑁 ) ) )
150 odzdvds ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ ( 𝐶 gcd 𝑃 ) = 1 ) ∧ ( ( 𝑁 − 1 ) / 𝑄 ) ∈ ℕ0 ) → ( 𝑃 ∥ ( ( 𝐶 ↑ ( ( 𝑁 − 1 ) / 𝑄 ) ) − 1 ) ↔ ( ( odℤ ‘ 𝑃 ) ‘ 𝐶 ) ∥ ( ( 𝑁 − 1 ) / 𝑄 ) ) )
151 18 9 75 142 150 syl31anc ⊢ ( 𝜑 → ( 𝑃 ∥ ( ( 𝐶 ↑ ( ( 𝑁 − 1 ) / 𝑄 ) ) − 1 ) ↔ ( ( odℤ ‘ 𝑃 ) ‘ 𝐶 ) ∥ ( ( 𝑁 − 1 ) / 𝑄 ) ) )
152 13 nncnd ⊢ ( 𝜑 → 𝑄 ∈ ℂ )
153 8 nnzd ⊢ ( 𝜑 → ( 𝑄 pCnt 𝐴 ) ∈ ℤ )
154 152 130 153 expm1d ⊢ ( 𝜑 → ( 𝑄 ↑ ( ( 𝑄 pCnt 𝐴 ) − 1 ) ) = ( ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) / 𝑄 ) )
155 154 oveq2d ⊢ ( 𝜑 → ( ( ( 𝑁 − 1 ) / ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ) · ( 𝑄 ↑ ( ( 𝑄 pCnt 𝐴 ) − 1 ) ) ) = ( ( ( 𝑁 − 1 ) / ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ) · ( ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) / 𝑄 ) ) )
156 135 15 nndivred ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) / ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ) ∈ ℝ )
157 156 recnd ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) / ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ) ∈ ℂ )
158 157 121 152 130 divassd ⊢ ( 𝜑 → ( ( ( ( 𝑁 − 1 ) / ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ) · ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ) / 𝑄 ) = ( ( ( 𝑁 − 1 ) / ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ) · ( ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) / 𝑄 ) ) )
159 122 oveq1d ⊢ ( 𝜑 → ( ( ( ( 𝑁 − 1 ) / ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ) · ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ) / 𝑄 ) = ( ( 𝑁 − 1 ) / 𝑄 ) )
160 155 158 159 3eqtr2d ⊢ ( 𝜑 → ( ( ( 𝑁 − 1 ) / ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ) · ( 𝑄 ↑ ( ( 𝑄 pCnt 𝐴 ) − 1 ) ) ) = ( ( 𝑁 − 1 ) / 𝑄 ) )
161 160 breq2d ⊢ ( 𝜑 → ( ( ( odℤ ‘ 𝑃 ) ‘ 𝐶 ) ∥ ( ( ( 𝑁 − 1 ) / ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ) · ( 𝑄 ↑ ( ( 𝑄 pCnt 𝐴 ) − 1 ) ) ) ↔ ( ( odℤ ‘ 𝑃 ) ‘ 𝐶 ) ∥ ( ( 𝑁 − 1 ) / 𝑄 ) ) )
162 151 161 bitr4d ⊢ ( 𝜑 → ( 𝑃 ∥ ( ( 𝐶 ↑ ( ( 𝑁 − 1 ) / 𝑄 ) ) − 1 ) ↔ ( ( odℤ ‘ 𝑃 ) ‘ 𝐶 ) ∥ ( ( ( 𝑁 − 1 ) / ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ) · ( 𝑄 ↑ ( ( 𝑄 pCnt 𝐴 ) − 1 ) ) ) ) )
163 11 breq2d ⊢ ( 𝜑 → ( 𝑃 ∥ ( ( ( 𝐶 ↑ ( ( 𝑁 − 1 ) / 𝑄 ) ) − 1 ) gcd 𝑁 ) ↔ 𝑃 ∥ 1 ) )
164 149 162 163 3imtr3d ⊢ ( 𝜑 → ( ( ( odℤ ‘ 𝑃 ) ‘ 𝐶 ) ∥ ( ( ( 𝑁 − 1 ) / ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ) · ( 𝑄 ↑ ( ( 𝑄 pCnt 𝐴 ) − 1 ) ) ) → 𝑃 ∥ 1 ) )
165 125 164 mtod ⊢ ( 𝜑 → ¬ ( ( odℤ ‘ 𝑃 ) ‘ 𝐶 ) ∥ ( ( ( 𝑁 − 1 ) / ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ) · ( 𝑄 ↑ ( ( 𝑄 pCnt 𝐴 ) − 1 ) ) ) )
166 prmpwdvds ⊢ ( ( ( ( ( 𝑁 − 1 ) / ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ) ∈ ℤ ∧ ( ( odℤ ‘ 𝑃 ) ‘ 𝐶 ) ∈ ℤ ) ∧ ( 𝑄 ∈ ℙ ∧ ( 𝑄 pCnt 𝐴 ) ∈ ℕ ) ∧ ( ( ( odℤ ‘ 𝑃 ) ‘ 𝐶 ) ∥ ( ( ( 𝑁 − 1 ) / ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ) · ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ) ∧ ¬ ( ( odℤ ‘ 𝑃 ) ‘ 𝐶 ) ∥ ( ( ( 𝑁 − 1 ) / ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ) · ( 𝑄 ↑ ( ( 𝑄 pCnt 𝐴 ) − 1 ) ) ) ) ) → ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ∥ ( ( odℤ ‘ 𝑃 ) ‘ 𝐶 ) )
167 104 78 7 8 123 165 166 syl222anc ⊢ ( 𝜑 → ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ∥ ( ( odℤ ‘ 𝑃 ) ‘ 𝐶 ) )
168 odzphi ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ ( 𝐶 gcd 𝑃 ) = 1 ) → ( ( odℤ ‘ 𝑃 ) ‘ 𝐶 ) ∥ ( ϕ ‘ 𝑃 ) )
169 18 9 75 168 syl3anc ⊢ ( 𝜑 → ( ( odℤ ‘ 𝑃 ) ‘ 𝐶 ) ∥ ( ϕ ‘ 𝑃 ) )
170 phiprm ⊢ ( 𝑃 ∈ ℙ → ( ϕ ‘ 𝑃 ) = ( 𝑃 − 1 ) )
171 5 170 syl ⊢ ( 𝜑 → ( ϕ ‘ 𝑃 ) = ( 𝑃 − 1 ) )
172 169 171 breqtrd ⊢ ( 𝜑 → ( ( odℤ ‘ 𝑃 ) ‘ 𝐶 ) ∥ ( 𝑃 − 1 ) )
173 16 78 85 167 172 dvdstrd ⊢ ( 𝜑 → ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ∥ ( 𝑃 − 1 ) )
174 pcdvdsb ⊢ ( ( 𝑄 ∈ ℙ ∧ ( 𝑃 − 1 ) ∈ ℤ ∧ ( 𝑄 pCnt 𝐴 ) ∈ ℕ0 ) → ( ( 𝑄 pCnt 𝐴 ) ≤ ( 𝑄 pCnt ( 𝑃 − 1 ) ) ↔ ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ∥ ( 𝑃 − 1 ) ) )
175 7 85 14 174 syl3anc ⊢ ( 𝜑 → ( ( 𝑄 pCnt 𝐴 ) ≤ ( 𝑄 pCnt ( 𝑃 − 1 ) ) ↔ ( 𝑄 ↑ ( 𝑄 pCnt 𝐴 ) ) ∥ ( 𝑃 − 1 ) ) )
176 173 175 mpbird ⊢ ( 𝜑 → ( 𝑄 pCnt 𝐴 ) ≤ ( 𝑄 pCnt ( 𝑃 − 1 ) ) )