Description: Lemma for wilth : induction step. The "hand proof" version of this theorem works by writing out the list of all numbers from 1 to P - 1 in pairs such that a number is paired with its inverse. Every number has a unique inverse different from itself except 1 and P - 1 , and so each pair multiplies to 1 , and 1 and P - 1 == -u 1 multiply to -u 1 , so the full product is equal to -u 1 . Here we make this precise by doing the product pair by pair.
The induction hypothesis says that every subset S of 1 ... ( P - 1 ) that is closed under inverse (i.e. all pairs are matched up) and contains P - 1 multiplies to -u 1 mod P . Given such a set, we take out one element z =/= P - 1 . If there are no such elements, then S = { P - 1 } which forms the base case. Otherwise, S \ { z , z ^ -u 1 } is also closed under inverse and contains P - 1 , so the induction hypothesis says that this equals -u 1 ; and the remaining two elements are either equal to each other, in which case wilthlem1 gives that z = 1 or P - 1 , and we've already excluded the second case, so the product gives 1 ; or z =/= z ^ -u 1 and their product is 1 . In either case the accumulated product is unaffected. (Contributed by Mario Carneiro, 24-Jan-2015) (Proof shortened by AV, 27-Jul-2019)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | wilthlem.t | ⊢ 𝑇 = ( mulGrp ‘ ℂfld ) | |
| wilthlem.a | ⊢ 𝐴 = { 𝑥 ∈ 𝒫 ( 1 ... ( 𝑃 − 1 ) ) ∣ ( ( 𝑃 − 1 ) ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ 𝑥 ) } | ||
| wilthlem2.p | ⊢ ( 𝜑 → 𝑃 ∈ ℙ ) | ||
| wilthlem2.s | ⊢ ( 𝜑 → 𝑆 ∈ 𝐴 ) | ||
| wilthlem2.r | ⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝐴 ( 𝑠 ⊊ 𝑆 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) | ||
| Assertion | wilthlem2 | ⊢ ( 𝜑 → ( ( 𝑇 Σg ( I ↾ 𝑆 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wilthlem.t | ⊢ 𝑇 = ( mulGrp ‘ ℂfld ) | |
| 2 | wilthlem.a | ⊢ 𝐴 = { 𝑥 ∈ 𝒫 ( 1 ... ( 𝑃 − 1 ) ) ∣ ( ( 𝑃 − 1 ) ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ 𝑥 ) } | |
| 3 | wilthlem2.p | ⊢ ( 𝜑 → 𝑃 ∈ ℙ ) | |
| 4 | wilthlem2.s | ⊢ ( 𝜑 → 𝑆 ∈ 𝐴 ) | |
| 5 | wilthlem2.r | ⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝐴 ( 𝑠 ⊊ 𝑆 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) | |
| 6 | simpr | ⊢ ( ( 𝜑 ∧ 𝑆 ⊆ { ( 𝑃 − 1 ) } ) → 𝑆 ⊆ { ( 𝑃 − 1 ) } ) | |
| 7 | eleq2 | ⊢ ( 𝑥 = 𝑆 → ( ( 𝑃 − 1 ) ∈ 𝑥 ↔ ( 𝑃 − 1 ) ∈ 𝑆 ) ) | |
| 8 | eleq2 | ⊢ ( 𝑥 = 𝑆 → ( ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ 𝑥 ↔ ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ 𝑆 ) ) | |
| 9 | 8 | raleqbi1dv | ⊢ ( 𝑥 = 𝑆 → ( ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ 𝑥 ↔ ∀ 𝑦 ∈ 𝑆 ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ 𝑆 ) ) |
| 10 | 7 9 | anbi12d | ⊢ ( 𝑥 = 𝑆 → ( ( ( 𝑃 − 1 ) ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ 𝑥 ) ↔ ( ( 𝑃 − 1 ) ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ 𝑆 ) ) ) |
| 11 | 10 2 | elrab2 | ⊢ ( 𝑆 ∈ 𝐴 ↔ ( 𝑆 ∈ 𝒫 ( 1 ... ( 𝑃 − 1 ) ) ∧ ( ( 𝑃 − 1 ) ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ 𝑆 ) ) ) |
| 12 | 4 11 | sylib | ⊢ ( 𝜑 → ( 𝑆 ∈ 𝒫 ( 1 ... ( 𝑃 − 1 ) ) ∧ ( ( 𝑃 − 1 ) ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ 𝑆 ) ) ) |
| 13 | 12 | simprd | ⊢ ( 𝜑 → ( ( 𝑃 − 1 ) ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ 𝑆 ) ) |
| 14 | 13 | simpld | ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ 𝑆 ) |
| 15 | 14 | snssd | ⊢ ( 𝜑 → { ( 𝑃 − 1 ) } ⊆ 𝑆 ) |
| 16 | 15 | adantr | ⊢ ( ( 𝜑 ∧ 𝑆 ⊆ { ( 𝑃 − 1 ) } ) → { ( 𝑃 − 1 ) } ⊆ 𝑆 ) |
| 17 | 6 16 | eqssd | ⊢ ( ( 𝜑 ∧ 𝑆 ⊆ { ( 𝑃 − 1 ) } ) → 𝑆 = { ( 𝑃 − 1 ) } ) |
| 18 | 17 | reseq2d | ⊢ ( ( 𝜑 ∧ 𝑆 ⊆ { ( 𝑃 − 1 ) } ) → ( I ↾ 𝑆 ) = ( I ↾ { ( 𝑃 − 1 ) } ) ) |
| 19 | mptresid | ⊢ ( I ↾ { ( 𝑃 − 1 ) } ) = ( 𝑧 ∈ { ( 𝑃 − 1 ) } ↦ 𝑧 ) | |
| 20 | 18 19 | eqtrdi | ⊢ ( ( 𝜑 ∧ 𝑆 ⊆ { ( 𝑃 − 1 ) } ) → ( I ↾ 𝑆 ) = ( 𝑧 ∈ { ( 𝑃 − 1 ) } ↦ 𝑧 ) ) |
| 21 | 20 | oveq2d | ⊢ ( ( 𝜑 ∧ 𝑆 ⊆ { ( 𝑃 − 1 ) } ) → ( 𝑇 Σg ( I ↾ 𝑆 ) ) = ( 𝑇 Σg ( 𝑧 ∈ { ( 𝑃 − 1 ) } ↦ 𝑧 ) ) ) |
| 22 | 21 | oveq1d | ⊢ ( ( 𝜑 ∧ 𝑆 ⊆ { ( 𝑃 − 1 ) } ) → ( ( 𝑇 Σg ( I ↾ 𝑆 ) ) mod 𝑃 ) = ( ( 𝑇 Σg ( 𝑧 ∈ { ( 𝑃 − 1 ) } ↦ 𝑧 ) ) mod 𝑃 ) ) |
| 23 | prmnn | ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ ) | |
| 24 | 3 23 | syl | ⊢ ( 𝜑 → 𝑃 ∈ ℕ ) |
| 25 | 24 | nncnd | ⊢ ( 𝜑 → 𝑃 ∈ ℂ ) |
| 26 | ax-1cn | ⊢ 1 ∈ ℂ | |
| 27 | negsub | ⊢ ( ( 𝑃 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑃 + - 1 ) = ( 𝑃 − 1 ) ) | |
| 28 | 25 26 27 | sylancl | ⊢ ( 𝜑 → ( 𝑃 + - 1 ) = ( 𝑃 − 1 ) ) |
| 29 | neg1cn | ⊢ - 1 ∈ ℂ | |
| 30 | addcom | ⊢ ( ( 𝑃 ∈ ℂ ∧ - 1 ∈ ℂ ) → ( 𝑃 + - 1 ) = ( - 1 + 𝑃 ) ) | |
| 31 | 25 29 30 | sylancl | ⊢ ( 𝜑 → ( 𝑃 + - 1 ) = ( - 1 + 𝑃 ) ) |
| 32 | 28 31 | eqtr3d | ⊢ ( 𝜑 → ( 𝑃 − 1 ) = ( - 1 + 𝑃 ) ) |
| 33 | cnring | ⊢ ℂfld ∈ Ring | |
| 34 | 1 | ringmgp | ⊢ ( ℂfld ∈ Ring → 𝑇 ∈ Mnd ) |
| 35 | 33 34 | mp1i | ⊢ ( 𝜑 → 𝑇 ∈ Mnd ) |
| 36 | nnm1nn0 | ⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ0 ) | |
| 37 | 24 36 | syl | ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℕ0 ) |
| 38 | 37 | nn0cnd | ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℂ ) |
| 39 | cnfldbas | ⊢ ℂ = ( Base ‘ ℂfld ) | |
| 40 | 1 39 | mgpbas | ⊢ ℂ = ( Base ‘ 𝑇 ) |
| 41 | id | ⊢ ( 𝑧 = ( 𝑃 − 1 ) → 𝑧 = ( 𝑃 − 1 ) ) | |
| 42 | 40 41 | gsumsn | ⊢ ( ( 𝑇 ∈ Mnd ∧ ( 𝑃 − 1 ) ∈ ℂ ∧ ( 𝑃 − 1 ) ∈ ℂ ) → ( 𝑇 Σg ( 𝑧 ∈ { ( 𝑃 − 1 ) } ↦ 𝑧 ) ) = ( 𝑃 − 1 ) ) |
| 43 | 35 38 38 42 | syl3anc | ⊢ ( 𝜑 → ( 𝑇 Σg ( 𝑧 ∈ { ( 𝑃 − 1 ) } ↦ 𝑧 ) ) = ( 𝑃 − 1 ) ) |
| 44 | 25 | mulid2d | ⊢ ( 𝜑 → ( 1 · 𝑃 ) = 𝑃 ) |
| 45 | 44 | oveq2d | ⊢ ( 𝜑 → ( - 1 + ( 1 · 𝑃 ) ) = ( - 1 + 𝑃 ) ) |
| 46 | 32 43 45 | 3eqtr4d | ⊢ ( 𝜑 → ( 𝑇 Σg ( 𝑧 ∈ { ( 𝑃 − 1 ) } ↦ 𝑧 ) ) = ( - 1 + ( 1 · 𝑃 ) ) ) |
| 47 | 46 | oveq1d | ⊢ ( 𝜑 → ( ( 𝑇 Σg ( 𝑧 ∈ { ( 𝑃 − 1 ) } ↦ 𝑧 ) ) mod 𝑃 ) = ( ( - 1 + ( 1 · 𝑃 ) ) mod 𝑃 ) ) |
| 48 | neg1rr | ⊢ - 1 ∈ ℝ | |
| 49 | 48 | a1i | ⊢ ( 𝜑 → - 1 ∈ ℝ ) |
| 50 | 24 | nnrpd | ⊢ ( 𝜑 → 𝑃 ∈ ℝ+ ) |
| 51 | 1zzd | ⊢ ( 𝜑 → 1 ∈ ℤ ) | |
| 52 | modcyc | ⊢ ( ( - 1 ∈ ℝ ∧ 𝑃 ∈ ℝ+ ∧ 1 ∈ ℤ ) → ( ( - 1 + ( 1 · 𝑃 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) | |
| 53 | 49 50 51 52 | syl3anc | ⊢ ( 𝜑 → ( ( - 1 + ( 1 · 𝑃 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) |
| 54 | 47 53 | eqtrd | ⊢ ( 𝜑 → ( ( 𝑇 Σg ( 𝑧 ∈ { ( 𝑃 − 1 ) } ↦ 𝑧 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) |
| 55 | 54 | adantr | ⊢ ( ( 𝜑 ∧ 𝑆 ⊆ { ( 𝑃 − 1 ) } ) → ( ( 𝑇 Σg ( 𝑧 ∈ { ( 𝑃 − 1 ) } ↦ 𝑧 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) |
| 56 | 22 55 | eqtrd | ⊢ ( ( 𝜑 ∧ 𝑆 ⊆ { ( 𝑃 − 1 ) } ) → ( ( 𝑇 Σg ( I ↾ 𝑆 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) |
| 57 | 56 | ex | ⊢ ( 𝜑 → ( 𝑆 ⊆ { ( 𝑃 − 1 ) } → ( ( 𝑇 Σg ( I ↾ 𝑆 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) |
| 58 | nss | ⊢ ( ¬ 𝑆 ⊆ { ( 𝑃 − 1 ) } ↔ ∃ 𝑧 ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) | |
| 59 | cnfld1 | ⊢ 1 = ( 1r ‘ ℂfld ) | |
| 60 | 1 59 | ringidval | ⊢ 1 = ( 0g ‘ 𝑇 ) |
| 61 | cnfldmul | ⊢ · = ( .r ‘ ℂfld ) | |
| 62 | 1 61 | mgpplusg | ⊢ · = ( +g ‘ 𝑇 ) |
| 63 | cncrng | ⊢ ℂfld ∈ CRing | |
| 64 | 1 | crngmgp | ⊢ ( ℂfld ∈ CRing → 𝑇 ∈ CMnd ) |
| 65 | 63 64 | ax-mp | ⊢ 𝑇 ∈ CMnd |
| 66 | 65 | a1i | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → 𝑇 ∈ CMnd ) |
| 67 | 4 | adantr | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → 𝑆 ∈ 𝐴 ) |
| 68 | f1oi | ⊢ ( I ↾ 𝑆 ) : 𝑆 –1-1-onto→ 𝑆 | |
| 69 | f1of | ⊢ ( ( I ↾ 𝑆 ) : 𝑆 –1-1-onto→ 𝑆 → ( I ↾ 𝑆 ) : 𝑆 ⟶ 𝑆 ) | |
| 70 | 68 69 | ax-mp | ⊢ ( I ↾ 𝑆 ) : 𝑆 ⟶ 𝑆 |
| 71 | 12 | simpld | ⊢ ( 𝜑 → 𝑆 ∈ 𝒫 ( 1 ... ( 𝑃 − 1 ) ) ) |
| 72 | 71 | elpwid | ⊢ ( 𝜑 → 𝑆 ⊆ ( 1 ... ( 𝑃 − 1 ) ) ) |
| 73 | fzssz | ⊢ ( 1 ... ( 𝑃 − 1 ) ) ⊆ ℤ | |
| 74 | 72 73 | sstrdi | ⊢ ( 𝜑 → 𝑆 ⊆ ℤ ) |
| 75 | zsscn | ⊢ ℤ ⊆ ℂ | |
| 76 | 74 75 | sstrdi | ⊢ ( 𝜑 → 𝑆 ⊆ ℂ ) |
| 77 | fss | ⊢ ( ( ( I ↾ 𝑆 ) : 𝑆 ⟶ 𝑆 ∧ 𝑆 ⊆ ℂ ) → ( I ↾ 𝑆 ) : 𝑆 ⟶ ℂ ) | |
| 78 | 70 76 77 | sylancr | ⊢ ( 𝜑 → ( I ↾ 𝑆 ) : 𝑆 ⟶ ℂ ) |
| 79 | 78 | adantr | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( I ↾ 𝑆 ) : 𝑆 ⟶ ℂ ) |
| 80 | fzfi | ⊢ ( 1 ... ( 𝑃 − 1 ) ) ∈ Fin | |
| 81 | ssfi | ⊢ ( ( ( 1 ... ( 𝑃 − 1 ) ) ∈ Fin ∧ 𝑆 ⊆ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑆 ∈ Fin ) | |
| 82 | 80 72 81 | sylancr | ⊢ ( 𝜑 → 𝑆 ∈ Fin ) |
| 83 | 1ex | ⊢ 1 ∈ V | |
| 84 | 83 | a1i | ⊢ ( 𝜑 → 1 ∈ V ) |
| 85 | 78 82 84 | fdmfifsupp | ⊢ ( 𝜑 → ( I ↾ 𝑆 ) finSupp 1 ) |
| 86 | 85 | adantr | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( I ↾ 𝑆 ) finSupp 1 ) |
| 87 | disjdif | ⊢ ( { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ∩ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) = ∅ | |
| 88 | 87 | a1i | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ∩ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) = ∅ ) |
| 89 | undif2 | ⊢ ( { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ∪ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) = ( { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ∪ 𝑆 ) | |
| 90 | simprl | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → 𝑧 ∈ 𝑆 ) | |
| 91 | oveq1 | ⊢ ( 𝑦 = 𝑧 → ( 𝑦 ↑ ( 𝑃 − 2 ) ) = ( 𝑧 ↑ ( 𝑃 − 2 ) ) ) | |
| 92 | 91 | oveq1d | ⊢ ( 𝑦 = 𝑧 → ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) |
| 93 | 92 | eleq1d | ⊢ ( 𝑦 = 𝑧 → ( ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ 𝑆 ↔ ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ 𝑆 ) ) |
| 94 | 13 | simprd | ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑆 ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ 𝑆 ) |
| 95 | 94 | adantr | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ∀ 𝑦 ∈ 𝑆 ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ 𝑆 ) |
| 96 | 93 95 90 | rspcdva | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ 𝑆 ) |
| 97 | 90 96 | prssd | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ⊆ 𝑆 ) |
| 98 | ssequn1 | ⊢ ( { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ⊆ 𝑆 ↔ ( { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ∪ 𝑆 ) = 𝑆 ) | |
| 99 | 97 98 | sylib | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ∪ 𝑆 ) = 𝑆 ) |
| 100 | 89 99 | eqtr2id | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → 𝑆 = ( { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ∪ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) |
| 101 | 40 60 62 66 67 79 86 88 100 | gsumsplit | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑇 Σg ( I ↾ 𝑆 ) ) = ( ( 𝑇 Σg ( ( I ↾ 𝑆 ) ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) · ( 𝑇 Σg ( ( I ↾ 𝑆 ) ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) ) ) |
| 102 | 97 | resabs1d | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( I ↾ 𝑆 ) ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) = ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) |
| 103 | 102 | oveq2d | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑇 Σg ( ( I ↾ 𝑆 ) ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) = ( 𝑇 Σg ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) |
| 104 | difss | ⊢ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ⊆ 𝑆 | |
| 105 | resabs1 | ⊢ ( ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ⊆ 𝑆 → ( ( I ↾ 𝑆 ) ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) = ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) | |
| 106 | 104 105 | ax-mp | ⊢ ( ( I ↾ 𝑆 ) ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) = ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) |
| 107 | 106 | oveq2i | ⊢ ( 𝑇 Σg ( ( I ↾ 𝑆 ) ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) = ( 𝑇 Σg ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) |
| 108 | 107 | a1i | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑇 Σg ( ( I ↾ 𝑆 ) ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) = ( 𝑇 Σg ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) ) |
| 109 | 103 108 | oveq12d | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( 𝑇 Σg ( ( I ↾ 𝑆 ) ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) · ( 𝑇 Σg ( ( I ↾ 𝑆 ) ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) ) = ( ( 𝑇 Σg ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) · ( 𝑇 Σg ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) ) ) |
| 110 | 101 109 | eqtrd | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑇 Σg ( I ↾ 𝑆 ) ) = ( ( 𝑇 Σg ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) · ( 𝑇 Σg ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) ) ) |
| 111 | 110 | oveq1d | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( 𝑇 Σg ( I ↾ 𝑆 ) ) mod 𝑃 ) = ( ( ( 𝑇 Σg ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) · ( 𝑇 Σg ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) ) mod 𝑃 ) ) |
| 112 | prfi | ⊢ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ∈ Fin | |
| 113 | 112 | a1i | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ∈ Fin ) |
| 114 | zsubrg | ⊢ ℤ ∈ ( SubRing ‘ ℂfld ) | |
| 115 | 1 | subrgsubm | ⊢ ( ℤ ∈ ( SubRing ‘ ℂfld ) → ℤ ∈ ( SubMnd ‘ 𝑇 ) ) |
| 116 | 114 115 | mp1i | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ℤ ∈ ( SubMnd ‘ 𝑇 ) ) |
| 117 | f1oi | ⊢ ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) : { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } –1-1-onto→ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } | |
| 118 | f1of | ⊢ ( ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) : { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } –1-1-onto→ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } → ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) : { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ⟶ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) | |
| 119 | 117 118 | ax-mp | ⊢ ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) : { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ⟶ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } |
| 120 | 74 | adantr | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → 𝑆 ⊆ ℤ ) |
| 121 | 97 120 | sstrd | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ⊆ ℤ ) |
| 122 | fss | ⊢ ( ( ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) : { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ⟶ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ∧ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ⊆ ℤ ) → ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) : { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ⟶ ℤ ) | |
| 123 | 119 121 122 | sylancr | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) : { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ⟶ ℤ ) |
| 124 | 83 | a1i | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → 1 ∈ V ) |
| 125 | 123 113 124 | fdmfifsupp | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) finSupp 1 ) |
| 126 | 60 66 113 116 123 125 | gsumsubmcl | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑇 Σg ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ∈ ℤ ) |
| 127 | 126 | zred | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑇 Σg ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ∈ ℝ ) |
| 128 | 1red | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → 1 ∈ ℝ ) | |
| 129 | 72 | adantr | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → 𝑆 ⊆ ( 1 ... ( 𝑃 − 1 ) ) ) |
| 130 | 129 | ssdifssd | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ⊆ ( 1 ... ( 𝑃 − 1 ) ) ) |
| 131 | ssfi | ⊢ ( ( ( 1 ... ( 𝑃 − 1 ) ) ∈ Fin ∧ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ⊆ ( 1 ... ( 𝑃 − 1 ) ) ) → ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ∈ Fin ) | |
| 132 | 80 130 131 | sylancr | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ∈ Fin ) |
| 133 | f1oi | ⊢ ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) : ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) –1-1-onto→ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) | |
| 134 | f1of | ⊢ ( ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) : ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) –1-1-onto→ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) → ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) : ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ⟶ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) | |
| 135 | 133 134 | ax-mp | ⊢ ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) : ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ⟶ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) |
| 136 | 120 | ssdifssd | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ⊆ ℤ ) |
| 137 | fss | ⊢ ( ( ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) : ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ⟶ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ∧ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ⊆ ℤ ) → ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) : ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ⟶ ℤ ) | |
| 138 | 135 136 137 | sylancr | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) : ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ⟶ ℤ ) |
| 139 | 138 132 124 | fdmfifsupp | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) finSupp 1 ) |
| 140 | 60 66 132 116 138 139 | gsumsubmcl | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑇 Σg ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) ∈ ℤ ) |
| 141 | 50 | adantr | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → 𝑃 ∈ ℝ+ ) |
| 142 | 35 | adantr | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → 𝑇 ∈ Mnd ) |
| 143 | 76 | adantr | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → 𝑆 ⊆ ℂ ) |
| 144 | 143 90 | sseldd | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → 𝑧 ∈ ℂ ) |
| 145 | id | ⊢ ( 𝑤 = 𝑧 → 𝑤 = 𝑧 ) | |
| 146 | 40 145 | gsumsn | ⊢ ( ( 𝑇 ∈ Mnd ∧ 𝑧 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑇 Σg ( 𝑤 ∈ { 𝑧 } ↦ 𝑤 ) ) = 𝑧 ) |
| 147 | 142 144 144 146 | syl3anc | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑇 Σg ( 𝑤 ∈ { 𝑧 } ↦ 𝑤 ) ) = 𝑧 ) |
| 148 | 147 | adantr | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑧 = 1 ) → ( 𝑇 Σg ( 𝑤 ∈ { 𝑧 } ↦ 𝑤 ) ) = 𝑧 ) |
| 149 | mptresid | ⊢ ( I ↾ { 𝑧 } ) = ( 𝑤 ∈ { 𝑧 } ↦ 𝑤 ) | |
| 150 | dfsn2 | ⊢ { 𝑧 } = { 𝑧 , 𝑧 } | |
| 151 | animorrl | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑧 = 1 ) → ( 𝑧 = 1 ∨ 𝑧 = ( 𝑃 − 1 ) ) ) | |
| 152 | 3 | adantr | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → 𝑃 ∈ ℙ ) |
| 153 | 129 90 | sseldd | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → 𝑧 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) |
| 154 | wilthlem1 | ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑧 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( 𝑧 = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ↔ ( 𝑧 = 1 ∨ 𝑧 = ( 𝑃 − 1 ) ) ) ) | |
| 155 | 152 153 154 | syl2anc | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑧 = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ↔ ( 𝑧 = 1 ∨ 𝑧 = ( 𝑃 − 1 ) ) ) ) |
| 156 | 155 | biimpar | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ ( 𝑧 = 1 ∨ 𝑧 = ( 𝑃 − 1 ) ) ) → 𝑧 = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) |
| 157 | 151 156 | syldan | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑧 = 1 ) → 𝑧 = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) |
| 158 | 157 | preq2d | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑧 = 1 ) → { 𝑧 , 𝑧 } = { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) |
| 159 | 150 158 | syl5eq | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑧 = 1 ) → { 𝑧 } = { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) |
| 160 | 159 | reseq2d | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑧 = 1 ) → ( I ↾ { 𝑧 } ) = ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) |
| 161 | 149 160 | eqtr3id | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑧 = 1 ) → ( 𝑤 ∈ { 𝑧 } ↦ 𝑤 ) = ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) |
| 162 | 161 | oveq2d | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑧 = 1 ) → ( 𝑇 Σg ( 𝑤 ∈ { 𝑧 } ↦ 𝑤 ) ) = ( 𝑇 Σg ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) |
| 163 | simpr | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑧 = 1 ) → 𝑧 = 1 ) | |
| 164 | 148 162 163 | 3eqtr3d | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑧 = 1 ) → ( 𝑇 Σg ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) = 1 ) |
| 165 | 164 | oveq1d | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑧 = 1 ) → ( ( 𝑇 Σg ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) mod 𝑃 ) = ( 1 mod 𝑃 ) ) |
| 166 | df-pr | ⊢ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } = ( { 𝑧 } ∪ { ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) | |
| 167 | 166 | reseq2i | ⊢ ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) = ( I ↾ ( { 𝑧 } ∪ { ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) |
| 168 | mptresid | ⊢ ( I ↾ ( { 𝑧 } ∪ { ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) = ( 𝑤 ∈ ( { 𝑧 } ∪ { ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ↦ 𝑤 ) | |
| 169 | 167 168 | eqtri | ⊢ ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) = ( 𝑤 ∈ ( { 𝑧 } ∪ { ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ↦ 𝑤 ) |
| 170 | 169 | oveq2i | ⊢ ( 𝑇 Σg ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) = ( 𝑇 Σg ( 𝑤 ∈ ( { 𝑧 } ∪ { ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ↦ 𝑤 ) ) |
| 171 | 65 | a1i | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑧 ≠ 1 ) → 𝑇 ∈ CMnd ) |
| 172 | snfi | ⊢ { 𝑧 } ∈ Fin | |
| 173 | 172 | a1i | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑧 ≠ 1 ) → { 𝑧 } ∈ Fin ) |
| 174 | elsni | ⊢ ( 𝑤 ∈ { 𝑧 } → 𝑤 = 𝑧 ) | |
| 175 | 174 | adantl | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑤 ∈ { 𝑧 } ) → 𝑤 = 𝑧 ) |
| 176 | 144 | adantr | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑤 ∈ { 𝑧 } ) → 𝑧 ∈ ℂ ) |
| 177 | 175 176 | eqeltrd | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑤 ∈ { 𝑧 } ) → 𝑤 ∈ ℂ ) |
| 178 | 177 | adantlr | ⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑧 ≠ 1 ) ∧ 𝑤 ∈ { 𝑧 } ) → 𝑤 ∈ ℂ ) |
| 179 | 143 96 | sseldd | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ℂ ) |
| 180 | 179 | adantr | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑧 ≠ 1 ) → ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ℂ ) |
| 181 | simprr | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) | |
| 182 | velsn | ⊢ ( 𝑧 ∈ { ( 𝑃 − 1 ) } ↔ 𝑧 = ( 𝑃 − 1 ) ) | |
| 183 | 181 182 | sylnib | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ¬ 𝑧 = ( 𝑃 − 1 ) ) |
| 184 | biorf | ⊢ ( ¬ 𝑧 = ( 𝑃 − 1 ) → ( 𝑧 = 1 ↔ ( 𝑧 = ( 𝑃 − 1 ) ∨ 𝑧 = 1 ) ) ) | |
| 185 | 183 184 | syl | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑧 = 1 ↔ ( 𝑧 = ( 𝑃 − 1 ) ∨ 𝑧 = 1 ) ) ) |
| 186 | ovex | ⊢ ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ V | |
| 187 | 186 | elsn | ⊢ ( ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ { 𝑧 } ↔ ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = 𝑧 ) |
| 188 | eqcom | ⊢ ( ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = 𝑧 ↔ 𝑧 = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) | |
| 189 | 187 188 | bitri | ⊢ ( ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ { 𝑧 } ↔ 𝑧 = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) |
| 190 | orcom | ⊢ ( ( 𝑧 = ( 𝑃 − 1 ) ∨ 𝑧 = 1 ) ↔ ( 𝑧 = 1 ∨ 𝑧 = ( 𝑃 − 1 ) ) ) | |
| 191 | 155 189 190 | 3bitr4g | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ { 𝑧 } ↔ ( 𝑧 = ( 𝑃 − 1 ) ∨ 𝑧 = 1 ) ) ) |
| 192 | 185 191 | bitr4d | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑧 = 1 ↔ ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ { 𝑧 } ) ) |
| 193 | 192 | necon3abid | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑧 ≠ 1 ↔ ¬ ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ { 𝑧 } ) ) |
| 194 | 193 | biimpa | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑧 ≠ 1 ) → ¬ ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ { 𝑧 } ) |
| 195 | id | ⊢ ( 𝑤 = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) → 𝑤 = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) | |
| 196 | 40 62 171 173 178 180 194 180 195 | gsumunsn | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑧 ≠ 1 ) → ( 𝑇 Σg ( 𝑤 ∈ ( { 𝑧 } ∪ { ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ↦ 𝑤 ) ) = ( ( 𝑇 Σg ( 𝑤 ∈ { 𝑧 } ↦ 𝑤 ) ) · ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) ) |
| 197 | 170 196 | syl5eq | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑧 ≠ 1 ) → ( 𝑇 Σg ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) = ( ( 𝑇 Σg ( 𝑤 ∈ { 𝑧 } ↦ 𝑤 ) ) · ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) ) |
| 198 | 147 | adantr | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑧 ≠ 1 ) → ( 𝑇 Σg ( 𝑤 ∈ { 𝑧 } ↦ 𝑤 ) ) = 𝑧 ) |
| 199 | 198 | oveq1d | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑧 ≠ 1 ) → ( ( 𝑇 Σg ( 𝑤 ∈ { 𝑧 } ↦ 𝑤 ) ) · ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) = ( 𝑧 · ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) ) |
| 200 | 197 199 | eqtrd | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑧 ≠ 1 ) → ( 𝑇 Σg ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) = ( 𝑧 · ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) ) |
| 201 | 200 | oveq1d | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑧 ≠ 1 ) → ( ( 𝑇 Σg ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) mod 𝑃 ) = ( ( 𝑧 · ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) ) |
| 202 | 153 | elfzelzd | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → 𝑧 ∈ ℤ ) |
| 203 | 24 | adantr | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → 𝑃 ∈ ℕ ) |
| 204 | fzm1ndvds | ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑧 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ¬ 𝑃 ∥ 𝑧 ) | |
| 205 | 203 153 204 | syl2anc | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ¬ 𝑃 ∥ 𝑧 ) |
| 206 | eqid | ⊢ ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) | |
| 207 | 206 | prmdiv | ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑧 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑧 ) → ( ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝑧 · ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) − 1 ) ) ) |
| 208 | 152 202 205 207 | syl3anc | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝑧 · ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) − 1 ) ) ) |
| 209 | 208 | simprd | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → 𝑃 ∥ ( ( 𝑧 · ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) − 1 ) ) |
| 210 | elfznn | ⊢ ( 𝑧 ∈ ( 1 ... ( 𝑃 − 1 ) ) → 𝑧 ∈ ℕ ) | |
| 211 | 153 210 | syl | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → 𝑧 ∈ ℕ ) |
| 212 | 129 96 | sseldd | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ) |
| 213 | elfznn | ⊢ ( ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) → ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ℕ ) | |
| 214 | 212 213 | syl | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ℕ ) |
| 215 | 211 214 | nnmulcld | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑧 · ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) ∈ ℕ ) |
| 216 | 215 | nnzd | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑧 · ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) ∈ ℤ ) |
| 217 | 1zzd | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → 1 ∈ ℤ ) | |
| 218 | moddvds | ⊢ ( ( 𝑃 ∈ ℕ ∧ ( 𝑧 · ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) ∈ ℤ ∧ 1 ∈ ℤ ) → ( ( ( 𝑧 · ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) = ( 1 mod 𝑃 ) ↔ 𝑃 ∥ ( ( 𝑧 · ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) − 1 ) ) ) | |
| 219 | 203 216 217 218 | syl3anc | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( ( 𝑧 · ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) = ( 1 mod 𝑃 ) ↔ 𝑃 ∥ ( ( 𝑧 · ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) − 1 ) ) ) |
| 220 | 209 219 | mpbird | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( 𝑧 · ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) = ( 1 mod 𝑃 ) ) |
| 221 | 220 | adantr | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑧 ≠ 1 ) → ( ( 𝑧 · ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) mod 𝑃 ) = ( 1 mod 𝑃 ) ) |
| 222 | 201 221 | eqtrd | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑧 ≠ 1 ) → ( ( 𝑇 Σg ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) mod 𝑃 ) = ( 1 mod 𝑃 ) ) |
| 223 | 165 222 | pm2.61dane | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( 𝑇 Σg ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) mod 𝑃 ) = ( 1 mod 𝑃 ) ) |
| 224 | modmul1 | ⊢ ( ( ( ( 𝑇 Σg ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ∈ ℝ ∧ 1 ∈ ℝ ) ∧ ( ( 𝑇 Σg ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) ∈ ℤ ∧ 𝑃 ∈ ℝ+ ) ∧ ( ( 𝑇 Σg ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) mod 𝑃 ) = ( 1 mod 𝑃 ) ) → ( ( ( 𝑇 Σg ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) · ( 𝑇 Σg ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) ) mod 𝑃 ) = ( ( 1 · ( 𝑇 Σg ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) ) mod 𝑃 ) ) | |
| 225 | 127 128 140 141 223 224 | syl221anc | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( ( 𝑇 Σg ( I ↾ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) · ( 𝑇 Σg ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) ) mod 𝑃 ) = ( ( 1 · ( 𝑇 Σg ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) ) mod 𝑃 ) ) |
| 226 | 140 | zcnd | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑇 Σg ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) ∈ ℂ ) |
| 227 | 226 | mulid2d | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 1 · ( 𝑇 Σg ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) ) = ( 𝑇 Σg ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) ) |
| 228 | 227 | oveq1d | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( 1 · ( 𝑇 Σg ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) ) mod 𝑃 ) = ( ( 𝑇 Σg ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) mod 𝑃 ) ) |
| 229 | sseqin2 | ⊢ ( { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ⊆ 𝑆 ↔ ( 𝑆 ∩ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) = { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) | |
| 230 | 97 229 | sylib | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑆 ∩ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) = { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) |
| 231 | vex | ⊢ 𝑧 ∈ V | |
| 232 | 231 | prnz | ⊢ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ≠ ∅ |
| 233 | 232 | a1i | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ≠ ∅ ) |
| 234 | 230 233 | eqnetrd | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑆 ∩ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ≠ ∅ ) |
| 235 | disj4 | ⊢ ( ( 𝑆 ∩ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) = ∅ ↔ ¬ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ⊊ 𝑆 ) | |
| 236 | 235 | necon2abii | ⊢ ( ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ⊊ 𝑆 ↔ ( 𝑆 ∩ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ≠ ∅ ) |
| 237 | 234 236 | sylibr | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ⊊ 𝑆 ) |
| 238 | psseq1 | ⊢ ( 𝑠 = ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) → ( 𝑠 ⊊ 𝑆 ↔ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ⊊ 𝑆 ) ) | |
| 239 | reseq2 | ⊢ ( 𝑠 = ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) → ( I ↾ 𝑠 ) = ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) | |
| 240 | 239 | oveq2d | ⊢ ( 𝑠 = ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) → ( 𝑇 Σg ( I ↾ 𝑠 ) ) = ( 𝑇 Σg ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) ) |
| 241 | 240 | oveq1d | ⊢ ( 𝑠 = ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( ( 𝑇 Σg ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) mod 𝑃 ) ) |
| 242 | 241 | eqeq1d | ⊢ ( 𝑠 = ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) → ( ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ↔ ( ( 𝑇 Σg ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) |
| 243 | 238 242 | imbi12d | ⊢ ( 𝑠 = ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) → ( ( 𝑠 ⊊ 𝑆 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ↔ ( ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ⊊ 𝑆 → ( ( 𝑇 Σg ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) |
| 244 | 5 | adantr | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ∀ 𝑠 ∈ 𝐴 ( 𝑠 ⊊ 𝑆 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) |
| 245 | ovex | ⊢ ( 1 ... ( 𝑃 − 1 ) ) ∈ V | |
| 246 | 245 | elpw2 | ⊢ ( ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ∈ 𝒫 ( 1 ... ( 𝑃 − 1 ) ) ↔ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ⊆ ( 1 ... ( 𝑃 − 1 ) ) ) |
| 247 | 130 246 | sylibr | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ∈ 𝒫 ( 1 ... ( 𝑃 − 1 ) ) ) |
| 248 | 14 | adantr | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑃 − 1 ) ∈ 𝑆 ) |
| 249 | eqcom | ⊢ ( 𝑧 = ( 𝑃 − 1 ) ↔ ( 𝑃 − 1 ) = 𝑧 ) | |
| 250 | 182 249 | bitri | ⊢ ( 𝑧 ∈ { ( 𝑃 − 1 ) } ↔ ( 𝑃 − 1 ) = 𝑧 ) |
| 251 | 181 250 | sylnib | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ¬ ( 𝑃 − 1 ) = 𝑧 ) |
| 252 | oveq1 | ⊢ ( ( 𝑃 − 1 ) = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) → ( ( 𝑃 − 1 ) ↑ ( 𝑃 − 2 ) ) = ( ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ↑ ( 𝑃 − 2 ) ) ) | |
| 253 | 252 | oveq1d | ⊢ ( ( 𝑃 − 1 ) = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) → ( ( ( 𝑃 − 1 ) ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = ( ( ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) |
| 254 | 203 36 | syl | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑃 − 1 ) ∈ ℕ0 ) |
| 255 | nn0uz | ⊢ ℕ0 = ( ℤ≥ ‘ 0 ) | |
| 256 | 254 255 | eleqtrdi | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑃 − 1 ) ∈ ( ℤ≥ ‘ 0 ) ) |
| 257 | eluzfz2 | ⊢ ( ( 𝑃 − 1 ) ∈ ( ℤ≥ ‘ 0 ) → ( 𝑃 − 1 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) ) | |
| 258 | 256 257 | syl | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑃 − 1 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) ) |
| 259 | prmz | ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ ) | |
| 260 | 152 259 | syl | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → 𝑃 ∈ ℤ ) |
| 261 | 120 248 | sseldd | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑃 − 1 ) ∈ ℤ ) |
| 262 | 1z | ⊢ 1 ∈ ℤ | |
| 263 | zsubcl | ⊢ ( ( ( 𝑃 − 1 ) ∈ ℤ ∧ 1 ∈ ℤ ) → ( ( 𝑃 − 1 ) − 1 ) ∈ ℤ ) | |
| 264 | 261 262 263 | sylancl | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( 𝑃 − 1 ) − 1 ) ∈ ℤ ) |
| 265 | dvdsmul1 | ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 𝑃 − 1 ) − 1 ) ∈ ℤ ) → 𝑃 ∥ ( 𝑃 · ( ( 𝑃 − 1 ) − 1 ) ) ) | |
| 266 | 260 264 265 | syl2anc | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → 𝑃 ∥ ( 𝑃 · ( ( 𝑃 − 1 ) − 1 ) ) ) |
| 267 | 203 | nncnd | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → 𝑃 ∈ ℂ ) |
| 268 | 264 | zcnd | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( 𝑃 − 1 ) − 1 ) ∈ ℂ ) |
| 269 | 267 268 | mulcld | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑃 · ( ( 𝑃 − 1 ) − 1 ) ) ∈ ℂ ) |
| 270 | 1cnd | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → 1 ∈ ℂ ) | |
| 271 | 254 | nn0cnd | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑃 − 1 ) ∈ ℂ ) |
| 272 | 267 270 271 | subdird | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( 𝑃 − 1 ) · ( 𝑃 − 1 ) ) = ( ( 𝑃 · ( 𝑃 − 1 ) ) − ( 1 · ( 𝑃 − 1 ) ) ) ) |
| 273 | 267 271 | mulcld | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑃 · ( 𝑃 − 1 ) ) ∈ ℂ ) |
| 274 | 273 267 270 | subsubd | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( 𝑃 · ( 𝑃 − 1 ) ) − ( 𝑃 − 1 ) ) = ( ( ( 𝑃 · ( 𝑃 − 1 ) ) − 𝑃 ) + 1 ) ) |
| 275 | 271 | mulid2d | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 1 · ( 𝑃 − 1 ) ) = ( 𝑃 − 1 ) ) |
| 276 | 275 | oveq2d | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( 𝑃 · ( 𝑃 − 1 ) ) − ( 1 · ( 𝑃 − 1 ) ) ) = ( ( 𝑃 · ( 𝑃 − 1 ) ) − ( 𝑃 − 1 ) ) ) |
| 277 | 267 271 | muls1d | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑃 · ( ( 𝑃 − 1 ) − 1 ) ) = ( ( 𝑃 · ( 𝑃 − 1 ) ) − 𝑃 ) ) |
| 278 | 277 | oveq1d | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( 𝑃 · ( ( 𝑃 − 1 ) − 1 ) ) + 1 ) = ( ( ( 𝑃 · ( 𝑃 − 1 ) ) − 𝑃 ) + 1 ) ) |
| 279 | 274 276 278 | 3eqtr4d | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( 𝑃 · ( 𝑃 − 1 ) ) − ( 1 · ( 𝑃 − 1 ) ) ) = ( ( 𝑃 · ( ( 𝑃 − 1 ) − 1 ) ) + 1 ) ) |
| 280 | 272 279 | eqtrd | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( 𝑃 − 1 ) · ( 𝑃 − 1 ) ) = ( ( 𝑃 · ( ( 𝑃 − 1 ) − 1 ) ) + 1 ) ) |
| 281 | 269 270 280 | mvrraddd | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( ( 𝑃 − 1 ) · ( 𝑃 − 1 ) ) − 1 ) = ( 𝑃 · ( ( 𝑃 − 1 ) − 1 ) ) ) |
| 282 | 266 281 | breqtrrd | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → 𝑃 ∥ ( ( ( 𝑃 − 1 ) · ( 𝑃 − 1 ) ) − 1 ) ) |
| 283 | 129 248 | sseldd | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑃 − 1 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ) |
| 284 | fzm1ndvds | ⊢ ( ( 𝑃 ∈ ℕ ∧ ( 𝑃 − 1 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ¬ 𝑃 ∥ ( 𝑃 − 1 ) ) | |
| 285 | 203 283 284 | syl2anc | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ¬ 𝑃 ∥ ( 𝑃 − 1 ) ) |
| 286 | eqid | ⊢ ( ( ( 𝑃 − 1 ) ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = ( ( ( 𝑃 − 1 ) ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) | |
| 287 | 286 | prmdiveq | ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 − 1 ) ∈ ℤ ∧ ¬ 𝑃 ∥ ( 𝑃 − 1 ) ) → ( ( ( 𝑃 − 1 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( ( 𝑃 − 1 ) · ( 𝑃 − 1 ) ) − 1 ) ) ↔ ( 𝑃 − 1 ) = ( ( ( 𝑃 − 1 ) ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) ) |
| 288 | 152 261 285 287 | syl3anc | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( ( 𝑃 − 1 ) ∈ ( 0 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( ( 𝑃 − 1 ) · ( 𝑃 − 1 ) ) − 1 ) ) ↔ ( 𝑃 − 1 ) = ( ( ( 𝑃 − 1 ) ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) ) |
| 289 | 258 282 288 | mpbi2and | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑃 − 1 ) = ( ( ( 𝑃 − 1 ) ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) |
| 290 | 206 | prmdivdiv | ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑧 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑧 = ( ( ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) |
| 291 | 152 153 290 | syl2anc | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → 𝑧 = ( ( ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) |
| 292 | 289 291 | eqeq12d | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( 𝑃 − 1 ) = 𝑧 ↔ ( ( ( 𝑃 − 1 ) ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = ( ( ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) ) |
| 293 | 253 292 | syl5ibr | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( 𝑃 − 1 ) = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) → ( 𝑃 − 1 ) = 𝑧 ) ) |
| 294 | 251 293 | mtod | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ¬ ( 𝑃 − 1 ) = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) |
| 295 | ioran | ⊢ ( ¬ ( ( 𝑃 − 1 ) = 𝑧 ∨ ( 𝑃 − 1 ) = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) ↔ ( ¬ ( 𝑃 − 1 ) = 𝑧 ∧ ¬ ( 𝑃 − 1 ) = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) ) | |
| 296 | 251 294 295 | sylanbrc | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ¬ ( ( 𝑃 − 1 ) = 𝑧 ∨ ( 𝑃 − 1 ) = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) ) |
| 297 | ovex | ⊢ ( 𝑃 − 1 ) ∈ V | |
| 298 | 297 | elpr | ⊢ ( ( 𝑃 − 1 ) ∈ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ↔ ( ( 𝑃 − 1 ) = 𝑧 ∨ ( 𝑃 − 1 ) = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) ) |
| 299 | 296 298 | sylnibr | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ¬ ( 𝑃 − 1 ) ∈ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) |
| 300 | 248 299 | eldifd | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑃 − 1 ) ∈ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) |
| 301 | eldifi | ⊢ ( 𝑦 ∈ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) → 𝑦 ∈ 𝑆 ) | |
| 302 | 95 | r19.21bi | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ 𝑆 ) |
| 303 | 301 302 | sylan2 | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑦 ∈ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) → ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ 𝑆 ) |
| 304 | eldif | ⊢ ( 𝑦 ∈ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ↔ ( 𝑦 ∈ 𝑆 ∧ ¬ 𝑦 ∈ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) | |
| 305 | 152 | adantr | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑦 ∈ 𝑆 ) → 𝑃 ∈ ℙ ) |
| 306 | 129 | sselda | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) |
| 307 | eqid | ⊢ ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) | |
| 308 | 307 | prmdivdiv | ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑦 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑦 = ( ( ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) |
| 309 | 305 306 308 | syl2anc | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 = ( ( ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) |
| 310 | oveq1 | ⊢ ( ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = 𝑧 → ( ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ↑ ( 𝑃 − 2 ) ) = ( 𝑧 ↑ ( 𝑃 − 2 ) ) ) | |
| 311 | 310 | oveq1d | ⊢ ( ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = 𝑧 → ( ( ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) |
| 312 | 311 | eqeq2d | ⊢ ( ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = 𝑧 → ( 𝑦 = ( ( ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ↔ 𝑦 = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) ) |
| 313 | 309 312 | syl5ibcom | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑦 ∈ 𝑆 ) → ( ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = 𝑧 → 𝑦 = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) ) |
| 314 | oveq1 | ⊢ ( ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) → ( ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ↑ ( 𝑃 − 2 ) ) = ( ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ↑ ( 𝑃 − 2 ) ) ) | |
| 315 | 314 | oveq1d | ⊢ ( ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) → ( ( ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = ( ( ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) |
| 316 | 291 | adantr | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑦 ∈ 𝑆 ) → 𝑧 = ( ( ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) |
| 317 | 309 316 | eqeq12d | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝑦 = 𝑧 ↔ ( ( ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = ( ( ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) ) |
| 318 | 315 317 | syl5ibr | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑦 ∈ 𝑆 ) → ( ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) → 𝑦 = 𝑧 ) ) |
| 319 | 313 318 | orim12d | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑦 ∈ 𝑆 ) → ( ( ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = 𝑧 ∨ ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) → ( 𝑦 = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∨ 𝑦 = 𝑧 ) ) ) |
| 320 | ovex | ⊢ ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ V | |
| 321 | 320 | elpr | ⊢ ( ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ↔ ( ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = 𝑧 ∨ ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) ) |
| 322 | vex | ⊢ 𝑦 ∈ V | |
| 323 | 322 | elpr | ⊢ ( 𝑦 ∈ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ↔ ( 𝑦 = 𝑧 ∨ 𝑦 = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) ) |
| 324 | orcom | ⊢ ( ( 𝑦 = 𝑧 ∨ 𝑦 = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) ↔ ( 𝑦 = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∨ 𝑦 = 𝑧 ) ) | |
| 325 | 323 324 | bitri | ⊢ ( 𝑦 ∈ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ↔ ( 𝑦 = ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∨ 𝑦 = 𝑧 ) ) |
| 326 | 319 321 325 | 3imtr4g | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑦 ∈ 𝑆 ) → ( ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } → 𝑦 ∈ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) |
| 327 | 326 | con3d | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑦 ∈ 𝑆 ) → ( ¬ 𝑦 ∈ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } → ¬ ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) |
| 328 | 327 | impr | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ ¬ 𝑦 ∈ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) → ¬ ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) |
| 329 | 304 328 | sylan2b | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑦 ∈ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) → ¬ ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) |
| 330 | 303 329 | eldifd | ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) ∧ 𝑦 ∈ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) → ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) |
| 331 | 330 | ralrimiva | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ∀ 𝑦 ∈ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) |
| 332 | 300 331 | jca | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( 𝑃 − 1 ) ∈ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ∧ ∀ 𝑦 ∈ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) |
| 333 | eleq2 | ⊢ ( 𝑥 = ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) → ( ( 𝑃 − 1 ) ∈ 𝑥 ↔ ( 𝑃 − 1 ) ∈ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) | |
| 334 | eleq2 | ⊢ ( 𝑥 = ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) → ( ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ 𝑥 ↔ ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) | |
| 335 | 334 | raleqbi1dv | ⊢ ( 𝑥 = ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) → ( ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ 𝑥 ↔ ∀ 𝑦 ∈ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) |
| 336 | 333 335 | anbi12d | ⊢ ( 𝑥 = ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) → ( ( ( 𝑃 − 1 ) ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ 𝑥 ) ↔ ( ( 𝑃 − 1 ) ∈ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ∧ ∀ 𝑦 ∈ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) ) |
| 337 | 336 2 | elrab2 | ⊢ ( ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ∈ 𝐴 ↔ ( ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ∈ 𝒫 ( 1 ... ( 𝑃 − 1 ) ) ∧ ( ( 𝑃 − 1 ) ∈ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ∧ ∀ 𝑦 ∈ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) ) |
| 338 | 247 332 337 | sylanbrc | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ∈ 𝐴 ) |
| 339 | 243 244 338 | rspcdva | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ⊊ 𝑆 → ( ( 𝑇 Σg ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) |
| 340 | 237 339 | mpd | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( 𝑇 Σg ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) |
| 341 | 228 340 | eqtrd | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( 1 · ( 𝑇 Σg ( I ↾ ( 𝑆 ∖ { 𝑧 , ( ( 𝑧 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) } ) ) ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) |
| 342 | 111 225 341 | 3eqtrd | ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) ) → ( ( 𝑇 Σg ( I ↾ 𝑆 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) |
| 343 | 342 | ex | ⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) → ( ( 𝑇 Σg ( I ↾ 𝑆 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) |
| 344 | 343 | exlimdv | ⊢ ( 𝜑 → ( ∃ 𝑧 ( 𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ { ( 𝑃 − 1 ) } ) → ( ( 𝑇 Σg ( I ↾ 𝑆 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) |
| 345 | 58 344 | syl5bi | ⊢ ( 𝜑 → ( ¬ 𝑆 ⊆ { ( 𝑃 − 1 ) } → ( ( 𝑇 Σg ( I ↾ 𝑆 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) |
| 346 | 57 345 | pm2.61d | ⊢ ( 𝜑 → ( ( 𝑇 Σg ( I ↾ 𝑆 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) |