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

Theorem wilthlem2 26573
Description: Lemma for wilth 26575: induction step. The "hand proof" version of this theorem works by writing out the list of all numbers from 1 to 𝑃 βˆ’ 1 in pairs such that a number is paired with its inverse. Every number has a unique inverse different from itself except 1 and 𝑃 βˆ’ 1, and so each pair multiplies to 1, and 1 and 𝑃 βˆ’ 1≑-1 multiply to -1, so the full product is equal to -1. Here we make this precise by doing the product pair by pair.

The induction hypothesis says that every subset 𝑆 of 1...(𝑃 βˆ’ 1) that is closed under inverse (i.e. all pairs are matched up) and contains 𝑃 βˆ’ 1 multiplies to -1 mod 𝑃. Given such a set, we take out one element 𝑧 β‰  𝑃 βˆ’ 1. If there are no such elements, then 𝑆 = {𝑃 βˆ’ 1} which forms the base case. Otherwise, 𝑆 βˆ– {𝑧, 𝑧↑-1} is also closed under inverse and contains 𝑃 βˆ’ 1, so the induction hypothesis says that this equals -1; and the remaining two elements are either equal to each other, in which case wilthlem1 26572 gives that 𝑧 = 1 or 𝑃 βˆ’ 1, and we've already excluded the second case, so the product gives 1; or 𝑧 β‰  𝑧↑-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.)

Hypotheses
Ref Expression
wilthlem.t 𝑇 = (mulGrpβ€˜β„‚fld)
wilthlem.a 𝐴 = {π‘₯ ∈ 𝒫 (1...(𝑃 βˆ’ 1)) ∣ ((𝑃 βˆ’ 1) ∈ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ π‘₯)}
wilthlem2.p (πœ‘ β†’ 𝑃 ∈ β„™)
wilthlem2.s (πœ‘ β†’ 𝑆 ∈ 𝐴)
wilthlem2.r (πœ‘ β†’ βˆ€π‘  ∈ 𝐴 (𝑠 ⊊ 𝑆 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))
Assertion
Ref Expression
wilthlem2 (πœ‘ β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑆)) mod 𝑃) = (-1 mod 𝑃))
Distinct variable groups:   π‘₯,𝑠,𝑦,𝐴   𝑃,𝑠,π‘₯,𝑦   πœ‘,π‘₯,𝑦   𝑆,𝑠,π‘₯,𝑦   𝑇,𝑠,π‘₯,𝑦
Allowed substitution hint:   πœ‘(𝑠)

Proof of Theorem wilthlem2
Dummy variables 𝑀 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 486 . . . . . . . . 9 ((πœ‘ ∧ 𝑆 βŠ† {(𝑃 βˆ’ 1)}) β†’ 𝑆 βŠ† {(𝑃 βˆ’ 1)})
2 wilthlem2.s . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑆 ∈ 𝐴)
3 eleq2 2823 . . . . . . . . . . . . . . . 16 (π‘₯ = 𝑆 β†’ ((𝑃 βˆ’ 1) ∈ π‘₯ ↔ (𝑃 βˆ’ 1) ∈ 𝑆))
4 eleq2 2823 . . . . . . . . . . . . . . . . 17 (π‘₯ = 𝑆 β†’ (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ π‘₯ ↔ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ 𝑆))
54raleqbi1dv 3334 . . . . . . . . . . . . . . . 16 (π‘₯ = 𝑆 β†’ (βˆ€π‘¦ ∈ π‘₯ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ π‘₯ ↔ βˆ€π‘¦ ∈ 𝑆 ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ 𝑆))
63, 5anbi12d 632 . . . . . . . . . . . . . . 15 (π‘₯ = 𝑆 β†’ (((𝑃 βˆ’ 1) ∈ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ π‘₯) ↔ ((𝑃 βˆ’ 1) ∈ 𝑆 ∧ βˆ€π‘¦ ∈ 𝑆 ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ 𝑆)))
7 wilthlem.a . . . . . . . . . . . . . . 15 𝐴 = {π‘₯ ∈ 𝒫 (1...(𝑃 βˆ’ 1)) ∣ ((𝑃 βˆ’ 1) ∈ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ π‘₯)}
86, 7elrab2 3687 . . . . . . . . . . . . . 14 (𝑆 ∈ 𝐴 ↔ (𝑆 ∈ 𝒫 (1...(𝑃 βˆ’ 1)) ∧ ((𝑃 βˆ’ 1) ∈ 𝑆 ∧ βˆ€π‘¦ ∈ 𝑆 ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ 𝑆)))
92, 8sylib 217 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑆 ∈ 𝒫 (1...(𝑃 βˆ’ 1)) ∧ ((𝑃 βˆ’ 1) ∈ 𝑆 ∧ βˆ€π‘¦ ∈ 𝑆 ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ 𝑆)))
109simprd 497 . . . . . . . . . . . 12 (πœ‘ β†’ ((𝑃 βˆ’ 1) ∈ 𝑆 ∧ βˆ€π‘¦ ∈ 𝑆 ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ 𝑆))
1110simpld 496 . . . . . . . . . . 11 (πœ‘ β†’ (𝑃 βˆ’ 1) ∈ 𝑆)
1211snssd 4813 . . . . . . . . . 10 (πœ‘ β†’ {(𝑃 βˆ’ 1)} βŠ† 𝑆)
1312adantr 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑆 βŠ† {(𝑃 βˆ’ 1)}) β†’ {(𝑃 βˆ’ 1)} βŠ† 𝑆)
141, 13eqssd 4000 . . . . . . . 8 ((πœ‘ ∧ 𝑆 βŠ† {(𝑃 βˆ’ 1)}) β†’ 𝑆 = {(𝑃 βˆ’ 1)})
1514reseq2d 5982 . . . . . . 7 ((πœ‘ ∧ 𝑆 βŠ† {(𝑃 βˆ’ 1)}) β†’ ( I β†Ύ 𝑆) = ( I β†Ύ {(𝑃 βˆ’ 1)}))
16 mptresid 6051 . . . . . . 7 ( I β†Ύ {(𝑃 βˆ’ 1)}) = (𝑧 ∈ {(𝑃 βˆ’ 1)} ↦ 𝑧)
1715, 16eqtrdi 2789 . . . . . 6 ((πœ‘ ∧ 𝑆 βŠ† {(𝑃 βˆ’ 1)}) β†’ ( I β†Ύ 𝑆) = (𝑧 ∈ {(𝑃 βˆ’ 1)} ↦ 𝑧))
1817oveq2d 7425 . . . . 5 ((πœ‘ ∧ 𝑆 βŠ† {(𝑃 βˆ’ 1)}) β†’ (𝑇 Ξ£g ( I β†Ύ 𝑆)) = (𝑇 Ξ£g (𝑧 ∈ {(𝑃 βˆ’ 1)} ↦ 𝑧)))
1918oveq1d 7424 . . . 4 ((πœ‘ ∧ 𝑆 βŠ† {(𝑃 βˆ’ 1)}) β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑆)) mod 𝑃) = ((𝑇 Ξ£g (𝑧 ∈ {(𝑃 βˆ’ 1)} ↦ 𝑧)) mod 𝑃))
20 wilthlem2.p . . . . . . . . . . . 12 (πœ‘ β†’ 𝑃 ∈ β„™)
21 prmnn 16611 . . . . . . . . . . . 12 (𝑃 ∈ β„™ β†’ 𝑃 ∈ β„•)
2220, 21syl 17 . . . . . . . . . . 11 (πœ‘ β†’ 𝑃 ∈ β„•)
2322nncnd 12228 . . . . . . . . . 10 (πœ‘ β†’ 𝑃 ∈ β„‚)
24 ax-1cn 11168 . . . . . . . . . 10 1 ∈ β„‚
25 negsub 11508 . . . . . . . . . 10 ((𝑃 ∈ β„‚ ∧ 1 ∈ β„‚) β†’ (𝑃 + -1) = (𝑃 βˆ’ 1))
2623, 24, 25sylancl 587 . . . . . . . . 9 (πœ‘ β†’ (𝑃 + -1) = (𝑃 βˆ’ 1))
27 neg1cn 12326 . . . . . . . . . 10 -1 ∈ β„‚
28 addcom 11400 . . . . . . . . . 10 ((𝑃 ∈ β„‚ ∧ -1 ∈ β„‚) β†’ (𝑃 + -1) = (-1 + 𝑃))
2923, 27, 28sylancl 587 . . . . . . . . 9 (πœ‘ β†’ (𝑃 + -1) = (-1 + 𝑃))
3026, 29eqtr3d 2775 . . . . . . . 8 (πœ‘ β†’ (𝑃 βˆ’ 1) = (-1 + 𝑃))
31 cnring 20967 . . . . . . . . . 10 β„‚fld ∈ Ring
32 wilthlem.t . . . . . . . . . . 11 𝑇 = (mulGrpβ€˜β„‚fld)
3332ringmgp 20062 . . . . . . . . . 10 (β„‚fld ∈ Ring β†’ 𝑇 ∈ Mnd)
3431, 33mp1i 13 . . . . . . . . 9 (πœ‘ β†’ 𝑇 ∈ Mnd)
35 nnm1nn0 12513 . . . . . . . . . . 11 (𝑃 ∈ β„• β†’ (𝑃 βˆ’ 1) ∈ β„•0)
3622, 35syl 17 . . . . . . . . . 10 (πœ‘ β†’ (𝑃 βˆ’ 1) ∈ β„•0)
3736nn0cnd 12534 . . . . . . . . 9 (πœ‘ β†’ (𝑃 βˆ’ 1) ∈ β„‚)
38 cnfldbas 20948 . . . . . . . . . . 11 β„‚ = (Baseβ€˜β„‚fld)
3932, 38mgpbas 19993 . . . . . . . . . 10 β„‚ = (Baseβ€˜π‘‡)
40 id 22 . . . . . . . . . 10 (𝑧 = (𝑃 βˆ’ 1) β†’ 𝑧 = (𝑃 βˆ’ 1))
4139, 40gsumsn 19822 . . . . . . . . 9 ((𝑇 ∈ Mnd ∧ (𝑃 βˆ’ 1) ∈ β„‚ ∧ (𝑃 βˆ’ 1) ∈ β„‚) β†’ (𝑇 Ξ£g (𝑧 ∈ {(𝑃 βˆ’ 1)} ↦ 𝑧)) = (𝑃 βˆ’ 1))
4234, 37, 37, 41syl3anc 1372 . . . . . . . 8 (πœ‘ β†’ (𝑇 Ξ£g (𝑧 ∈ {(𝑃 βˆ’ 1)} ↦ 𝑧)) = (𝑃 βˆ’ 1))
4323mullidd 11232 . . . . . . . . 9 (πœ‘ β†’ (1 Β· 𝑃) = 𝑃)
4443oveq2d 7425 . . . . . . . 8 (πœ‘ β†’ (-1 + (1 Β· 𝑃)) = (-1 + 𝑃))
4530, 42, 443eqtr4d 2783 . . . . . . 7 (πœ‘ β†’ (𝑇 Ξ£g (𝑧 ∈ {(𝑃 βˆ’ 1)} ↦ 𝑧)) = (-1 + (1 Β· 𝑃)))
4645oveq1d 7424 . . . . . 6 (πœ‘ β†’ ((𝑇 Ξ£g (𝑧 ∈ {(𝑃 βˆ’ 1)} ↦ 𝑧)) mod 𝑃) = ((-1 + (1 Β· 𝑃)) mod 𝑃))
47 neg1rr 12327 . . . . . . . 8 -1 ∈ ℝ
4847a1i 11 . . . . . . 7 (πœ‘ β†’ -1 ∈ ℝ)
4922nnrpd 13014 . . . . . . 7 (πœ‘ β†’ 𝑃 ∈ ℝ+)
50 1zzd 12593 . . . . . . 7 (πœ‘ β†’ 1 ∈ β„€)
51 modcyc 13871 . . . . . . 7 ((-1 ∈ ℝ ∧ 𝑃 ∈ ℝ+ ∧ 1 ∈ β„€) β†’ ((-1 + (1 Β· 𝑃)) mod 𝑃) = (-1 mod 𝑃))
5248, 49, 50, 51syl3anc 1372 . . . . . 6 (πœ‘ β†’ ((-1 + (1 Β· 𝑃)) mod 𝑃) = (-1 mod 𝑃))
5346, 52eqtrd 2773 . . . . 5 (πœ‘ β†’ ((𝑇 Ξ£g (𝑧 ∈ {(𝑃 βˆ’ 1)} ↦ 𝑧)) mod 𝑃) = (-1 mod 𝑃))
5453adantr 482 . . . 4 ((πœ‘ ∧ 𝑆 βŠ† {(𝑃 βˆ’ 1)}) β†’ ((𝑇 Ξ£g (𝑧 ∈ {(𝑃 βˆ’ 1)} ↦ 𝑧)) mod 𝑃) = (-1 mod 𝑃))
5519, 54eqtrd 2773 . . 3 ((πœ‘ ∧ 𝑆 βŠ† {(𝑃 βˆ’ 1)}) β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑆)) mod 𝑃) = (-1 mod 𝑃))
5655ex 414 . 2 (πœ‘ β†’ (𝑆 βŠ† {(𝑃 βˆ’ 1)} β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑆)) mod 𝑃) = (-1 mod 𝑃)))
57 nss 4047 . . 3 (Β¬ 𝑆 βŠ† {(𝑃 βˆ’ 1)} ↔ βˆƒπ‘§(𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)}))
58 cnfld1 20970 . . . . . . . . . 10 1 = (1rβ€˜β„‚fld)
5932, 58ringidval 20006 . . . . . . . . 9 1 = (0gβ€˜π‘‡)
60 cnfldmul 20950 . . . . . . . . . 10 Β· = (.rβ€˜β„‚fld)
6132, 60mgpplusg 19991 . . . . . . . . 9 Β· = (+gβ€˜π‘‡)
62 cncrng 20966 . . . . . . . . . . 11 β„‚fld ∈ CRing
6332crngmgp 20064 . . . . . . . . . . 11 (β„‚fld ∈ CRing β†’ 𝑇 ∈ CMnd)
6462, 63ax-mp 5 . . . . . . . . . 10 𝑇 ∈ CMnd
6564a1i 11 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑇 ∈ CMnd)
662adantr 482 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑆 ∈ 𝐴)
67 f1oi 6872 . . . . . . . . . . . 12 ( I β†Ύ 𝑆):𝑆–1-1-onto→𝑆
68 f1of 6834 . . . . . . . . . . . 12 (( I β†Ύ 𝑆):𝑆–1-1-onto→𝑆 β†’ ( I β†Ύ 𝑆):π‘†βŸΆπ‘†)
6967, 68ax-mp 5 . . . . . . . . . . 11 ( I β†Ύ 𝑆):π‘†βŸΆπ‘†
709simpld 496 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑆 ∈ 𝒫 (1...(𝑃 βˆ’ 1)))
7170elpwid 4612 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑆 βŠ† (1...(𝑃 βˆ’ 1)))
72 fzssz 13503 . . . . . . . . . . . . 13 (1...(𝑃 βˆ’ 1)) βŠ† β„€
7371, 72sstrdi 3995 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑆 βŠ† β„€)
74 zsscn 12566 . . . . . . . . . . . 12 β„€ βŠ† β„‚
7573, 74sstrdi 3995 . . . . . . . . . . 11 (πœ‘ β†’ 𝑆 βŠ† β„‚)
76 fss 6735 . . . . . . . . . . 11 ((( I β†Ύ 𝑆):π‘†βŸΆπ‘† ∧ 𝑆 βŠ† β„‚) β†’ ( I β†Ύ 𝑆):π‘†βŸΆβ„‚)
7769, 75, 76sylancr 588 . . . . . . . . . 10 (πœ‘ β†’ ( I β†Ύ 𝑆):π‘†βŸΆβ„‚)
7877adantr 482 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ( I β†Ύ 𝑆):π‘†βŸΆβ„‚)
79 fzfi 13937 . . . . . . . . . . . 12 (1...(𝑃 βˆ’ 1)) ∈ Fin
80 ssfi 9173 . . . . . . . . . . . 12 (((1...(𝑃 βˆ’ 1)) ∈ Fin ∧ 𝑆 βŠ† (1...(𝑃 βˆ’ 1))) β†’ 𝑆 ∈ Fin)
8179, 71, 80sylancr 588 . . . . . . . . . . 11 (πœ‘ β†’ 𝑆 ∈ Fin)
82 1ex 11210 . . . . . . . . . . . 12 1 ∈ V
8382a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ 1 ∈ V)
8477, 81, 83fdmfifsupp 9373 . . . . . . . . . 10 (πœ‘ β†’ ( I β†Ύ 𝑆) finSupp 1)
8584adantr 482 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ( I β†Ύ 𝑆) finSupp 1)
86 disjdif 4472 . . . . . . . . . 10 ({𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} ∩ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = βˆ…
8786a1i 11 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ({𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} ∩ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = βˆ…)
88 undif2 4477 . . . . . . . . . 10 ({𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} βˆͺ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = ({𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} βˆͺ 𝑆)
89 simprl 770 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑧 ∈ 𝑆)
90 oveq1 7416 . . . . . . . . . . . . . . 15 (𝑦 = 𝑧 β†’ (𝑦↑(𝑃 βˆ’ 2)) = (𝑧↑(𝑃 βˆ’ 2)))
9190oveq1d 7424 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 β†’ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃))
9291eleq1d 2819 . . . . . . . . . . . . 13 (𝑦 = 𝑧 β†’ (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ 𝑆 ↔ ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ 𝑆))
9310simprd 497 . . . . . . . . . . . . . 14 (πœ‘ β†’ βˆ€π‘¦ ∈ 𝑆 ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ 𝑆)
9493adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ βˆ€π‘¦ ∈ 𝑆 ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ 𝑆)
9592, 94, 89rspcdva 3614 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ 𝑆)
9689, 95prssd 4826 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} βŠ† 𝑆)
97 ssequn1 4181 . . . . . . . . . . 11 ({𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} βŠ† 𝑆 ↔ ({𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} βˆͺ 𝑆) = 𝑆)
9896, 97sylib 217 . . . . . . . . . 10 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ({𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} βˆͺ 𝑆) = 𝑆)
9988, 98eqtr2id 2786 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑆 = ({𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} βˆͺ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))
10039, 59, 61, 65, 66, 78, 85, 87, 99gsumsplit 19796 . . . . . . . 8 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑇 Ξ£g ( I β†Ύ 𝑆)) = ((𝑇 Ξ£g (( I β†Ύ 𝑆) β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) Β· (𝑇 Ξ£g (( I β†Ύ 𝑆) β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))))
10196resabs1d 6013 . . . . . . . . . 10 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (( I β†Ύ 𝑆) β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) = ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
102101oveq2d 7425 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑇 Ξ£g (( I β†Ύ 𝑆) β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = (𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))
103 difss 4132 . . . . . . . . . . . 12 (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) βŠ† 𝑆
104 resabs1 6012 . . . . . . . . . . . 12 ((𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) βŠ† 𝑆 β†’ (( I β†Ύ 𝑆) β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))
105103, 104ax-mp 5 . . . . . . . . . . 11 (( I β†Ύ 𝑆) β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
106105oveq2i 7420 . . . . . . . . . 10 (𝑇 Ξ£g (( I β†Ύ 𝑆) β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))) = (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))
107106a1i 11 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑇 Ξ£g (( I β†Ύ 𝑆) β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))) = (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))))
108102, 107oveq12d 7427 . . . . . . . 8 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑇 Ξ£g (( I β†Ύ 𝑆) β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) Β· (𝑇 Ξ£g (( I β†Ύ 𝑆) β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))) = ((𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) Β· (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))))
109100, 108eqtrd 2773 . . . . . . 7 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑇 Ξ£g ( I β†Ύ 𝑆)) = ((𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) Β· (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))))
110109oveq1d 7424 . . . . . 6 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑆)) mod 𝑃) = (((𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) Β· (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))) mod 𝑃))
111 prfi 9322 . . . . . . . . . 10 {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} ∈ Fin
112111a1i 11 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} ∈ Fin)
113 zsubrg 20998 . . . . . . . . . 10 β„€ ∈ (SubRingβ€˜β„‚fld)
11432subrgsubm 20332 . . . . . . . . . 10 (β„€ ∈ (SubRingβ€˜β„‚fld) β†’ β„€ ∈ (SubMndβ€˜π‘‡))
115113, 114mp1i 13 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ β„€ ∈ (SubMndβ€˜π‘‡))
116 f1oi 6872 . . . . . . . . . . 11 ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}–1-1-ontoβ†’{𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}
117 f1of 6834 . . . . . . . . . . 11 (( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}–1-1-ontoβ†’{𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} β†’ ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}⟢{𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})
118116, 117ax-mp 5 . . . . . . . . . 10 ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}⟢{𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}
11973adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑆 βŠ† β„€)
12096, 119sstrd 3993 . . . . . . . . . 10 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} βŠ† β„€)
121 fss 6735 . . . . . . . . . 10 ((( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}⟢{𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} ∧ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} βŠ† β„€) β†’ ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}βŸΆβ„€)
122118, 120, 121sylancr 588 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}βŸΆβ„€)
12382a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 1 ∈ V)
124122, 112, 123fdmfifsupp 9373 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) finSupp 1)
12559, 65, 112, 115, 122, 124gsumsubmcl 19787 . . . . . . . 8 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) ∈ β„€)
126125zred 12666 . . . . . . 7 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) ∈ ℝ)
127 1red 11215 . . . . . . 7 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 1 ∈ ℝ)
12871adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑆 βŠ† (1...(𝑃 βˆ’ 1)))
129128ssdifssd 4143 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) βŠ† (1...(𝑃 βˆ’ 1)))
130 ssfi 9173 . . . . . . . . 9 (((1...(𝑃 βˆ’ 1)) ∈ Fin ∧ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) βŠ† (1...(𝑃 βˆ’ 1))) β†’ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ∈ Fin)
13179, 129, 130sylancr 588 . . . . . . . 8 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ∈ Fin)
132 f1oi 6872 . . . . . . . . . 10 ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})):(𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})–1-1-ontoβ†’(𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})
133 f1of 6834 . . . . . . . . . 10 (( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})):(𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})–1-1-ontoβ†’(𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β†’ ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})):(𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})⟢(𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
134132, 133ax-mp 5 . . . . . . . . 9 ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})):(𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})⟢(𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})
135119ssdifssd 4143 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) βŠ† β„€)
136 fss 6735 . . . . . . . . 9 ((( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})):(𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})⟢(𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ∧ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) βŠ† β„€) β†’ ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})):(𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})βŸΆβ„€)
137134, 135, 136sylancr 588 . . . . . . . 8 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})):(𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})βŸΆβ„€)
138137, 131, 123fdmfifsupp 9373 . . . . . . . 8 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) finSupp 1)
13959, 65, 131, 115, 137, 138gsumsubmcl 19787 . . . . . . 7 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))) ∈ β„€)
14049adantr 482 . . . . . . 7 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑃 ∈ ℝ+)
14134adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑇 ∈ Mnd)
14275adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑆 βŠ† β„‚)
143142, 89sseldd 3984 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑧 ∈ β„‚)
144 id 22 . . . . . . . . . . . . 13 (𝑀 = 𝑧 β†’ 𝑀 = 𝑧)
14539, 144gsumsn 19822 . . . . . . . . . . . 12 ((𝑇 ∈ Mnd ∧ 𝑧 ∈ β„‚ ∧ 𝑧 ∈ β„‚) β†’ (𝑇 Ξ£g (𝑀 ∈ {𝑧} ↦ 𝑀)) = 𝑧)
146141, 143, 143, 145syl3anc 1372 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑇 Ξ£g (𝑀 ∈ {𝑧} ↦ 𝑀)) = 𝑧)
147146adantr 482 . . . . . . . . . 10 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 = 1) β†’ (𝑇 Ξ£g (𝑀 ∈ {𝑧} ↦ 𝑀)) = 𝑧)
148 mptresid 6051 . . . . . . . . . . . 12 ( I β†Ύ {𝑧}) = (𝑀 ∈ {𝑧} ↦ 𝑀)
149 dfsn2 4642 . . . . . . . . . . . . . 14 {𝑧} = {𝑧, 𝑧}
150 animorrl 980 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 = 1) β†’ (𝑧 = 1 ∨ 𝑧 = (𝑃 βˆ’ 1)))
15120adantr 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑃 ∈ β„™)
152128, 89sseldd 3984 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑧 ∈ (1...(𝑃 βˆ’ 1)))
153 wilthlem1 26572 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ β„™ ∧ 𝑧 ∈ (1...(𝑃 βˆ’ 1))) β†’ (𝑧 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ↔ (𝑧 = 1 ∨ 𝑧 = (𝑃 βˆ’ 1))))
154151, 152, 153syl2anc 585 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑧 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ↔ (𝑧 = 1 ∨ 𝑧 = (𝑃 βˆ’ 1))))
155154biimpar 479 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ (𝑧 = 1 ∨ 𝑧 = (𝑃 βˆ’ 1))) β†’ 𝑧 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃))
156150, 155syldan 592 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 = 1) β†’ 𝑧 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃))
157156preq2d 4745 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 = 1) β†’ {𝑧, 𝑧} = {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})
158149, 157eqtrid 2785 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 = 1) β†’ {𝑧} = {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})
159158reseq2d 5982 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 = 1) β†’ ( I β†Ύ {𝑧}) = ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
160148, 159eqtr3id 2787 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 = 1) β†’ (𝑀 ∈ {𝑧} ↦ 𝑀) = ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
161160oveq2d 7425 . . . . . . . . . 10 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 = 1) β†’ (𝑇 Ξ£g (𝑀 ∈ {𝑧} ↦ 𝑀)) = (𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))
162 simpr 486 . . . . . . . . . 10 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 = 1) β†’ 𝑧 = 1)
163147, 161, 1623eqtr3d 2781 . . . . . . . . 9 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 = 1) β†’ (𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = 1)
164163oveq1d 7424 . . . . . . . 8 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 = 1) β†’ ((𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) mod 𝑃) = (1 mod 𝑃))
165 df-pr 4632 . . . . . . . . . . . . . . 15 {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} = ({𝑧} βˆͺ {((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})
166165reseq2i 5979 . . . . . . . . . . . . . 14 ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) = ( I β†Ύ ({𝑧} βˆͺ {((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
167 mptresid 6051 . . . . . . . . . . . . . 14 ( I β†Ύ ({𝑧} βˆͺ {((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = (𝑀 ∈ ({𝑧} βˆͺ {((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ↦ 𝑀)
168166, 167eqtri 2761 . . . . . . . . . . . . 13 ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) = (𝑀 ∈ ({𝑧} βˆͺ {((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ↦ 𝑀)
169168oveq2i 7420 . . . . . . . . . . . 12 (𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = (𝑇 Ξ£g (𝑀 ∈ ({𝑧} βˆͺ {((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ↦ 𝑀))
17064a1i 11 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) β†’ 𝑇 ∈ CMnd)
171 snfi 9044 . . . . . . . . . . . . . 14 {𝑧} ∈ Fin
172171a1i 11 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) β†’ {𝑧} ∈ Fin)
173 elsni 4646 . . . . . . . . . . . . . . . 16 (𝑀 ∈ {𝑧} β†’ 𝑀 = 𝑧)
174173adantl 483 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑀 ∈ {𝑧}) β†’ 𝑀 = 𝑧)
175143adantr 482 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑀 ∈ {𝑧}) β†’ 𝑧 ∈ β„‚)
176174, 175eqeltrd 2834 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑀 ∈ {𝑧}) β†’ 𝑀 ∈ β„‚)
177176adantlr 714 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) ∧ 𝑀 ∈ {𝑧}) β†’ 𝑀 ∈ β„‚)
178142, 95sseldd 3984 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ β„‚)
179178adantr 482 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) β†’ ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ β„‚)
180 simprr 772 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})
181 velsn 4645 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ {(𝑃 βˆ’ 1)} ↔ 𝑧 = (𝑃 βˆ’ 1))
182180, 181sylnib 328 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ Β¬ 𝑧 = (𝑃 βˆ’ 1))
183 biorf 936 . . . . . . . . . . . . . . . . 17 (Β¬ 𝑧 = (𝑃 βˆ’ 1) β†’ (𝑧 = 1 ↔ (𝑧 = (𝑃 βˆ’ 1) ∨ 𝑧 = 1)))
184182, 183syl 17 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑧 = 1 ↔ (𝑧 = (𝑃 βˆ’ 1) ∨ 𝑧 = 1)))
185 ovex 7442 . . . . . . . . . . . . . . . . . . 19 ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ V
186185elsn 4644 . . . . . . . . . . . . . . . . . 18 (((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ {𝑧} ↔ ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) = 𝑧)
187 eqcom 2740 . . . . . . . . . . . . . . . . . 18 (((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) = 𝑧 ↔ 𝑧 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃))
188186, 187bitri 275 . . . . . . . . . . . . . . . . 17 (((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ {𝑧} ↔ 𝑧 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃))
189 orcom 869 . . . . . . . . . . . . . . . . 17 ((𝑧 = (𝑃 βˆ’ 1) ∨ 𝑧 = 1) ↔ (𝑧 = 1 ∨ 𝑧 = (𝑃 βˆ’ 1)))
190154, 188, 1893bitr4g 314 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ {𝑧} ↔ (𝑧 = (𝑃 βˆ’ 1) ∨ 𝑧 = 1)))
191184, 190bitr4d 282 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑧 = 1 ↔ ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ {𝑧}))
192191necon3abid 2978 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑧 β‰  1 ↔ Β¬ ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ {𝑧}))
193192biimpa 478 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) β†’ Β¬ ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ {𝑧})
194 id 22 . . . . . . . . . . . . 13 (𝑀 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) β†’ 𝑀 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃))
19539, 61, 170, 172, 177, 179, 193, 179, 194gsumunsn 19828 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) β†’ (𝑇 Ξ£g (𝑀 ∈ ({𝑧} βˆͺ {((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ↦ 𝑀)) = ((𝑇 Ξ£g (𝑀 ∈ {𝑧} ↦ 𝑀)) Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)))
196169, 195eqtrid 2785 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) β†’ (𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = ((𝑇 Ξ£g (𝑀 ∈ {𝑧} ↦ 𝑀)) Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)))
197146adantr 482 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) β†’ (𝑇 Ξ£g (𝑀 ∈ {𝑧} ↦ 𝑀)) = 𝑧)
198197oveq1d 7424 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) β†’ ((𝑇 Ξ£g (𝑀 ∈ {𝑧} ↦ 𝑀)) Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) = (𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)))
199196, 198eqtrd 2773 . . . . . . . . . 10 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) β†’ (𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = (𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)))
200199oveq1d 7424 . . . . . . . . 9 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) β†’ ((𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) mod 𝑃) = ((𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) mod 𝑃))
201152elfzelzd 13502 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑧 ∈ β„€)
20222adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑃 ∈ β„•)
203 fzm1ndvds 16265 . . . . . . . . . . . . . 14 ((𝑃 ∈ β„• ∧ 𝑧 ∈ (1...(𝑃 βˆ’ 1))) β†’ Β¬ 𝑃 βˆ₯ 𝑧)
204202, 152, 203syl2anc 585 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ Β¬ 𝑃 βˆ₯ 𝑧)
205 eqid 2733 . . . . . . . . . . . . . 14 ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)
206205prmdiv 16718 . . . . . . . . . . . . 13 ((𝑃 ∈ β„™ ∧ 𝑧 ∈ β„€ ∧ Β¬ 𝑃 βˆ₯ 𝑧) β†’ (((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (1...(𝑃 βˆ’ 1)) ∧ 𝑃 βˆ₯ ((𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) βˆ’ 1)))
207151, 201, 204, 206syl3anc 1372 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (1...(𝑃 βˆ’ 1)) ∧ 𝑃 βˆ₯ ((𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) βˆ’ 1)))
208207simprd 497 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑃 βˆ₯ ((𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) βˆ’ 1))
209 elfznn 13530 . . . . . . . . . . . . . . 15 (𝑧 ∈ (1...(𝑃 βˆ’ 1)) β†’ 𝑧 ∈ β„•)
210152, 209syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑧 ∈ β„•)
211128, 95sseldd 3984 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (1...(𝑃 βˆ’ 1)))
212 elfznn 13530 . . . . . . . . . . . . . . 15 (((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (1...(𝑃 βˆ’ 1)) β†’ ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ β„•)
213211, 212syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ β„•)
214210, 213nnmulcld 12265 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) ∈ β„•)
215214nnzd 12585 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) ∈ β„€)
216 1zzd 12593 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 1 ∈ β„€)
217 moddvds 16208 . . . . . . . . . . . 12 ((𝑃 ∈ β„• ∧ (𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) ∈ β„€ ∧ 1 ∈ β„€) β†’ (((𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 βˆ₯ ((𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) βˆ’ 1)))
218202, 215, 216, 217syl3anc 1372 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (((𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 βˆ₯ ((𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) βˆ’ 1)))
219208, 218mpbird 257 . . . . . . . . . 10 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) mod 𝑃) = (1 mod 𝑃))
220219adantr 482 . . . . . . . . 9 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) β†’ ((𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) mod 𝑃) = (1 mod 𝑃))
221200, 220eqtrd 2773 . . . . . . . 8 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) β†’ ((𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) mod 𝑃) = (1 mod 𝑃))
222164, 221pm2.61dane 3030 . . . . . . 7 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) mod 𝑃) = (1 mod 𝑃))
223 modmul1 13889 . . . . . . 7 ((((𝑇 Ξ£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 𝑃))
224126, 127, 139, 140, 222, 223syl221anc 1382 . . . . . 6 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (((𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) Β· (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))) mod 𝑃) = ((1 Β· (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))) mod 𝑃))
225139zcnd 12667 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))) ∈ β„‚)
226225mullidd 11232 . . . . . . . 8 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (1 Β· (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))) = (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))))
227226oveq1d 7424 . . . . . . 7 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((1 Β· (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))) mod 𝑃) = ((𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))) mod 𝑃))
228 sseqin2 4216 . . . . . . . . . . 11 ({𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} βŠ† 𝑆 ↔ (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) = {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})
22996, 228sylib 217 . . . . . . . . . 10 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) = {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})
230 vex 3479 . . . . . . . . . . . 12 𝑧 ∈ V
231230prnz 4782 . . . . . . . . . . 11 {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} β‰  βˆ…
232231a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} β‰  βˆ…)
233229, 232eqnetrd 3009 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β‰  βˆ…)
234 disj4 4459 . . . . . . . . . 10 ((𝑆 ∩ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) = βˆ… ↔ Β¬ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ⊊ 𝑆)
235234necon2abii 2992 . . . . . . . . 9 ((𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ⊊ 𝑆 ↔ (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β‰  βˆ…)
236233, 235sylibr 233 . . . . . . . 8 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ⊊ 𝑆)
237 psseq1 4088 . . . . . . . . . 10 (𝑠 = (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β†’ (𝑠 ⊊ 𝑆 ↔ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ⊊ 𝑆))
238 reseq2 5977 . . . . . . . . . . . . 13 (𝑠 = (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β†’ ( I β†Ύ 𝑠) = ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))
239238oveq2d 7425 . . . . . . . . . . . 12 (𝑠 = (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β†’ (𝑇 Ξ£g ( I β†Ύ 𝑠)) = (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))))
240239oveq1d 7424 . . . . . . . . . . 11 (𝑠 = (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = ((𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))) mod 𝑃))
241240eqeq1d 2735 . . . . . . . . . 10 (𝑠 = (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β†’ (((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃) ↔ ((𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))) mod 𝑃) = (-1 mod 𝑃)))
242237, 241imbi12d 345 . . . . . . . . 9 (𝑠 = (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β†’ ((𝑠 ⊊ 𝑆 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ↔ ((𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ⊊ 𝑆 β†’ ((𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))) mod 𝑃) = (-1 mod 𝑃))))
243 wilthlem2.r . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘  ∈ 𝐴 (𝑠 ⊊ 𝑆 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))
244243adantr 482 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ βˆ€π‘  ∈ 𝐴 (𝑠 ⊊ 𝑆 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))
245 ovex 7442 . . . . . . . . . . . 12 (1...(𝑃 βˆ’ 1)) ∈ V
246245elpw2 5346 . . . . . . . . . . 11 ((𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ∈ 𝒫 (1...(𝑃 βˆ’ 1)) ↔ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) βŠ† (1...(𝑃 βˆ’ 1)))
247129, 246sylibr 233 . . . . . . . . . 10 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ∈ 𝒫 (1...(𝑃 βˆ’ 1)))
24811adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 βˆ’ 1) ∈ 𝑆)
249 eqcom 2740 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑃 βˆ’ 1) ↔ (𝑃 βˆ’ 1) = 𝑧)
250181, 249bitri 275 . . . . . . . . . . . . . . 15 (𝑧 ∈ {(𝑃 βˆ’ 1)} ↔ (𝑃 βˆ’ 1) = 𝑧)
251180, 250sylnib 328 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ Β¬ (𝑃 βˆ’ 1) = 𝑧)
252 oveq1 7416 . . . . . . . . . . . . . . . . 17 ((𝑃 βˆ’ 1) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) β†’ ((𝑃 βˆ’ 1)↑(𝑃 βˆ’ 2)) = (((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)))
253252oveq1d 7424 . . . . . . . . . . . . . . . 16 ((𝑃 βˆ’ 1) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) β†’ (((𝑃 βˆ’ 1)↑(𝑃 βˆ’ 2)) mod 𝑃) = ((((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) mod 𝑃))
254202, 35syl 17 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 βˆ’ 1) ∈ β„•0)
255 nn0uz 12864 . . . . . . . . . . . . . . . . . . . 20 β„•0 = (β„€β‰₯β€˜0)
256254, 255eleqtrdi 2844 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 βˆ’ 1) ∈ (β„€β‰₯β€˜0))
257 eluzfz2 13509 . . . . . . . . . . . . . . . . . . 19 ((𝑃 βˆ’ 1) ∈ (β„€β‰₯β€˜0) β†’ (𝑃 βˆ’ 1) ∈ (0...(𝑃 βˆ’ 1)))
258256, 257syl 17 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 βˆ’ 1) ∈ (0...(𝑃 βˆ’ 1)))
259 prmz 16612 . . . . . . . . . . . . . . . . . . . . 21 (𝑃 ∈ β„™ β†’ 𝑃 ∈ β„€)
260151, 259syl 17 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑃 ∈ β„€)
261119, 248sseldd 3984 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 βˆ’ 1) ∈ β„€)
262 1z 12592 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ β„€
263 zsubcl 12604 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃 βˆ’ 1) ∈ β„€ ∧ 1 ∈ β„€) β†’ ((𝑃 βˆ’ 1) βˆ’ 1) ∈ β„€)
264261, 262, 263sylancl 587 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑃 βˆ’ 1) βˆ’ 1) ∈ β„€)
265 dvdsmul1 16221 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ β„€ ∧ ((𝑃 βˆ’ 1) βˆ’ 1) ∈ β„€) β†’ 𝑃 βˆ₯ (𝑃 Β· ((𝑃 βˆ’ 1) βˆ’ 1)))
266260, 264, 265syl2anc 585 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑃 βˆ₯ (𝑃 Β· ((𝑃 βˆ’ 1) βˆ’ 1)))
267202nncnd 12228 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑃 ∈ β„‚)
268264zcnd 12667 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑃 βˆ’ 1) βˆ’ 1) ∈ β„‚)
269267, 268mulcld 11234 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 Β· ((𝑃 βˆ’ 1) βˆ’ 1)) ∈ β„‚)
270 1cnd 11209 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 1 ∈ β„‚)
271254nn0cnd 12534 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 βˆ’ 1) ∈ β„‚)
272267, 270, 271subdird 11671 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑃 βˆ’ 1) Β· (𝑃 βˆ’ 1)) = ((𝑃 Β· (𝑃 βˆ’ 1)) βˆ’ (1 Β· (𝑃 βˆ’ 1))))
273267, 271mulcld 11234 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 Β· (𝑃 βˆ’ 1)) ∈ β„‚)
274273, 267, 270subsubd 11599 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑃 Β· (𝑃 βˆ’ 1)) βˆ’ (𝑃 βˆ’ 1)) = (((𝑃 Β· (𝑃 βˆ’ 1)) βˆ’ 𝑃) + 1))
275271mullidd 11232 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (1 Β· (𝑃 βˆ’ 1)) = (𝑃 βˆ’ 1))
276275oveq2d 7425 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑃 Β· (𝑃 βˆ’ 1)) βˆ’ (1 Β· (𝑃 βˆ’ 1))) = ((𝑃 Β· (𝑃 βˆ’ 1)) βˆ’ (𝑃 βˆ’ 1)))
277267, 271muls1d 11674 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 Β· ((𝑃 βˆ’ 1) βˆ’ 1)) = ((𝑃 Β· (𝑃 βˆ’ 1)) βˆ’ 𝑃))
278277oveq1d 7424 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑃 Β· ((𝑃 βˆ’ 1) βˆ’ 1)) + 1) = (((𝑃 Β· (𝑃 βˆ’ 1)) βˆ’ 𝑃) + 1))
279274, 276, 2783eqtr4d 2783 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑃 Β· (𝑃 βˆ’ 1)) βˆ’ (1 Β· (𝑃 βˆ’ 1))) = ((𝑃 Β· ((𝑃 βˆ’ 1) βˆ’ 1)) + 1))
280272, 279eqtrd 2773 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑃 βˆ’ 1) Β· (𝑃 βˆ’ 1)) = ((𝑃 Β· ((𝑃 βˆ’ 1) βˆ’ 1)) + 1))
281269, 270, 280mvrraddd 11626 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (((𝑃 βˆ’ 1) Β· (𝑃 βˆ’ 1)) βˆ’ 1) = (𝑃 Β· ((𝑃 βˆ’ 1) βˆ’ 1)))
282266, 281breqtrrd 5177 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑃 βˆ₯ (((𝑃 βˆ’ 1) Β· (𝑃 βˆ’ 1)) βˆ’ 1))
283128, 248sseldd 3984 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 βˆ’ 1) ∈ (1...(𝑃 βˆ’ 1)))
284 fzm1ndvds 16265 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ β„• ∧ (𝑃 βˆ’ 1) ∈ (1...(𝑃 βˆ’ 1))) β†’ Β¬ 𝑃 βˆ₯ (𝑃 βˆ’ 1))
285202, 283, 284syl2anc 585 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ Β¬ 𝑃 βˆ₯ (𝑃 βˆ’ 1))
286 eqid 2733 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 βˆ’ 1)↑(𝑃 βˆ’ 2)) mod 𝑃) = (((𝑃 βˆ’ 1)↑(𝑃 βˆ’ 2)) mod 𝑃)
287286prmdiveq 16719 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ β„™ ∧ (𝑃 βˆ’ 1) ∈ β„€ ∧ Β¬ 𝑃 βˆ₯ (𝑃 βˆ’ 1)) β†’ (((𝑃 βˆ’ 1) ∈ (0...(𝑃 βˆ’ 1)) ∧ 𝑃 βˆ₯ (((𝑃 βˆ’ 1) Β· (𝑃 βˆ’ 1)) βˆ’ 1)) ↔ (𝑃 βˆ’ 1) = (((𝑃 βˆ’ 1)↑(𝑃 βˆ’ 2)) mod 𝑃)))
288151, 261, 285, 287syl3anc 1372 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (((𝑃 βˆ’ 1) ∈ (0...(𝑃 βˆ’ 1)) ∧ 𝑃 βˆ₯ (((𝑃 βˆ’ 1) Β· (𝑃 βˆ’ 1)) βˆ’ 1)) ↔ (𝑃 βˆ’ 1) = (((𝑃 βˆ’ 1)↑(𝑃 βˆ’ 2)) mod 𝑃)))
289258, 282, 288mpbi2and 711 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 βˆ’ 1) = (((𝑃 βˆ’ 1)↑(𝑃 βˆ’ 2)) mod 𝑃))
290205prmdivdiv 16720 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ β„™ ∧ 𝑧 ∈ (1...(𝑃 βˆ’ 1))) β†’ 𝑧 = ((((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) mod 𝑃))
291151, 152, 290syl2anc 585 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑧 = ((((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) mod 𝑃))
292289, 291eqeq12d 2749 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑃 βˆ’ 1) = 𝑧 ↔ (((𝑃 βˆ’ 1)↑(𝑃 βˆ’ 2)) mod 𝑃) = ((((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) mod 𝑃)))
293253, 292imbitrrid 245 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑃 βˆ’ 1) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) β†’ (𝑃 βˆ’ 1) = 𝑧))
294251, 293mtod 197 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ Β¬ (𝑃 βˆ’ 1) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃))
295 ioran 983 . . . . . . . . . . . . . 14 (Β¬ ((𝑃 βˆ’ 1) = 𝑧 ∨ (𝑃 βˆ’ 1) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) ↔ (Β¬ (𝑃 βˆ’ 1) = 𝑧 ∧ Β¬ (𝑃 βˆ’ 1) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)))
296251, 294, 295sylanbrc 584 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ Β¬ ((𝑃 βˆ’ 1) = 𝑧 ∨ (𝑃 βˆ’ 1) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)))
297 ovex 7442 . . . . . . . . . . . . . 14 (𝑃 βˆ’ 1) ∈ V
298297elpr 4652 . . . . . . . . . . . . 13 ((𝑃 βˆ’ 1) ∈ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} ↔ ((𝑃 βˆ’ 1) = 𝑧 ∨ (𝑃 βˆ’ 1) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)))
299296, 298sylnibr 329 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ Β¬ (𝑃 βˆ’ 1) ∈ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})
300248, 299eldifd 3960 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 βˆ’ 1) ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
301 eldifi 4127 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β†’ 𝑦 ∈ 𝑆)
30294r19.21bi 3249 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ 𝑆) β†’ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ 𝑆)
303301, 302sylan2 594 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) β†’ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ 𝑆)
304 eldif 3959 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ↔ (𝑦 ∈ 𝑆 ∧ Β¬ 𝑦 ∈ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
305151adantr 482 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ 𝑆) β†’ 𝑃 ∈ β„™)
306128sselda 3983 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ 𝑆) β†’ 𝑦 ∈ (1...(𝑃 βˆ’ 1)))
307 eqid 2733 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃)
308307prmdivdiv 16720 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ β„™ ∧ 𝑦 ∈ (1...(𝑃 βˆ’ 1))) β†’ 𝑦 = ((((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) mod 𝑃))
309305, 306, 308syl2anc 585 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ 𝑆) β†’ 𝑦 = ((((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) mod 𝑃))
310 oveq1 7416 . . . . . . . . . . . . . . . . . . . . 21 (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = 𝑧 β†’ (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) = (𝑧↑(𝑃 βˆ’ 2)))
311310oveq1d 7424 . . . . . . . . . . . . . . . . . . . 20 (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = 𝑧 β†’ ((((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) mod 𝑃) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃))
312311eqeq2d 2744 . . . . . . . . . . . . . . . . . . 19 (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = 𝑧 β†’ (𝑦 = ((((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) mod 𝑃) ↔ 𝑦 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)))
313309, 312syl5ibcom 244 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ 𝑆) β†’ (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = 𝑧 β†’ 𝑦 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)))
314 oveq1 7416 . . . . . . . . . . . . . . . . . . . 20 (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) β†’ (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) = (((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)))
315314oveq1d 7424 . . . . . . . . . . . . . . . . . . 19 (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) β†’ ((((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) mod 𝑃) = ((((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) mod 𝑃))
316291adantr 482 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ 𝑆) β†’ 𝑧 = ((((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) mod 𝑃))
317309, 316eqeq12d 2749 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ 𝑆) β†’ (𝑦 = 𝑧 ↔ ((((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) mod 𝑃) = ((((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) mod 𝑃)))
318315, 317imbitrrid 245 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ 𝑆) β†’ (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) β†’ 𝑦 = 𝑧))
319313, 318orim12d 964 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ 𝑆) β†’ ((((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = 𝑧 ∨ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) β†’ (𝑦 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∨ 𝑦 = 𝑧)))
320 ovex 7442 . . . . . . . . . . . . . . . . . 18 ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ V
321320elpr 4652 . . . . . . . . . . . . . . . . 17 (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} ↔ (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = 𝑧 ∨ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)))
322 vex 3479 . . . . . . . . . . . . . . . . . . 19 𝑦 ∈ V
323322elpr 4652 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} ↔ (𝑦 = 𝑧 ∨ 𝑦 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)))
324 orcom 869 . . . . . . . . . . . . . . . . . 18 ((𝑦 = 𝑧 ∨ 𝑦 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) ↔ (𝑦 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∨ 𝑦 = 𝑧))
325323, 324bitri 275 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} ↔ (𝑦 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∨ 𝑦 = 𝑧))
326319, 321, 3253imtr4g 296 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ 𝑆) β†’ (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} β†’ 𝑦 ∈ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
327326con3d 152 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ 𝑆) β†’ (Β¬ 𝑦 ∈ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} β†’ Β¬ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
328327impr 456 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ (𝑦 ∈ 𝑆 ∧ Β¬ 𝑦 ∈ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) β†’ Β¬ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})
329304, 328sylan2b 595 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) β†’ Β¬ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})
330303, 329eldifd 3960 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) β†’ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
331330ralrimiva 3147 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ βˆ€π‘¦ ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
332300, 331jca 513 . . . . . . . . . 10 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑃 βˆ’ 1) ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ∧ βˆ€π‘¦ ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))
333 eleq2 2823 . . . . . . . . . . . 12 (π‘₯ = (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β†’ ((𝑃 βˆ’ 1) ∈ π‘₯ ↔ (𝑃 βˆ’ 1) ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))
334 eleq2 2823 . . . . . . . . . . . . 13 (π‘₯ = (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β†’ (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ π‘₯ ↔ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))
335334raleqbi1dv 3334 . . . . . . . . . . . 12 (π‘₯ = (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β†’ (βˆ€π‘¦ ∈ π‘₯ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ π‘₯ ↔ βˆ€π‘¦ ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))
336333, 335anbi12d 632 . . . . . . . . . . 11 (π‘₯ = (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β†’ (((𝑃 βˆ’ 1) ∈ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ π‘₯) ↔ ((𝑃 βˆ’ 1) ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ∧ βˆ€π‘¦ ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))))
337336, 7elrab2 3687 . . . . . . . . . 10 ((𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ∈ 𝐴 ↔ ((𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ∈ 𝒫 (1...(𝑃 βˆ’ 1)) ∧ ((𝑃 βˆ’ 1) ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ∧ βˆ€π‘¦ ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))))
338247, 332, 337sylanbrc 584 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ∈ 𝐴)
339242, 244, 338rspcdva 3614 . . . . . . . 8 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ⊊ 𝑆 β†’ ((𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))) mod 𝑃) = (-1 mod 𝑃)))
340236, 339mpd 15 . . . . . . 7 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))) mod 𝑃) = (-1 mod 𝑃))
341227, 340eqtrd 2773 . . . . . 6 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((1 Β· (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))) mod 𝑃) = (-1 mod 𝑃))
342110, 224, 3413eqtrd 2777 . . . . 5 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑆)) mod 𝑃) = (-1 mod 𝑃))
343342ex 414 . . . 4 (πœ‘ β†’ ((𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)}) β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑆)) mod 𝑃) = (-1 mod 𝑃)))
344343exlimdv 1937 . . 3 (πœ‘ β†’ (βˆƒπ‘§(𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)}) β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑆)) mod 𝑃) = (-1 mod 𝑃)))
34557, 344biimtrid 241 . 2 (πœ‘ β†’ (Β¬ 𝑆 βŠ† {(𝑃 βˆ’ 1)} β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑆)) mod 𝑃) = (-1 mod 𝑃)))
34656, 345pm2.61d 179 1 (πœ‘ β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑆)) mod 𝑃) = (-1 mod 𝑃))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107   β‰  wne 2941  βˆ€wral 3062  {crab 3433  Vcvv 3475   βˆ– cdif 3946   βˆͺ cun 3947   ∩ cin 3948   βŠ† wss 3949   ⊊ wpss 3950  βˆ…c0 4323  π’« cpw 4603  {csn 4629  {cpr 4631   class class class wbr 5149   ↦ cmpt 5232   I cid 5574   β†Ύ cres 5679  βŸΆwf 6540  β€“1-1-ontoβ†’wf1o 6543  β€˜cfv 6544  (class class class)co 7409  Fincfn 8939   finSupp cfsupp 9361  β„‚cc 11108  β„cr 11109  0cc0 11110  1c1 11111   + caddc 11113   Β· cmul 11115   βˆ’ cmin 11444  -cneg 11445  β„•cn 12212  2c2 12267  β„•0cn0 12472  β„€cz 12558  β„€β‰₯cuz 12822  β„+crp 12974  ...cfz 13484   mod cmo 13834  β†‘cexp 14027   βˆ₯ cdvds 16197  β„™cprime 16608   Ξ£g cgsu 17386  Mndcmnd 18625  SubMndcsubmnd 18670  CMndccmn 19648  mulGrpcmgp 19987  Ringcrg 20056  CRingccrg 20057  SubRingcsubrg 20315  β„‚fldccnfld 20944
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188  ax-addf 11189  ax-mulf 11190
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-of 7670  df-om 7856  df-1st 7975  df-2nd 7976  df-supp 8147  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-2o 8467  df-oadd 8470  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-fsupp 9362  df-sup 9437  df-inf 9438  df-oi 9505  df-dju 9896  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-3 12276  df-4 12277  df-5 12278  df-6 12279  df-7 12280  df-8 12281  df-9 12282  df-n0 12473  df-xnn0 12545  df-z 12559  df-dec 12678  df-uz 12823  df-rp 12975  df-fz 13485  df-fzo 13628  df-fl 13757  df-mod 13835  df-seq 13967  df-exp 14028  df-hash 14291  df-cj 15046  df-re 15047  df-im 15048  df-sqrt 15182  df-abs 15183  df-dvds 16198  df-gcd 16436  df-prm 16609  df-phi 16699  df-struct 17080  df-sets 17097  df-slot 17115  df-ndx 17127  df-base 17145  df-ress 17174  df-plusg 17210  df-mulr 17211  df-starv 17212  df-tset 17216  df-ple 17217  df-ds 17219  df-unif 17220  df-0g 17387  df-gsum 17388  df-mre 17530  df-mrc 17531  df-acs 17533  df-mgm 18561  df-sgrp 18610  df-mnd 18626  df-submnd 18672  df-grp 18822  df-minusg 18823  df-mulg 18951  df-subg 19003  df-cntz 19181  df-cmn 19650  df-mgp 19988  df-ur 20005  df-ring 20058  df-cring 20059  df-subrg 20317  df-cnfld 20945
This theorem is referenced by:  wilthlem3  26574
  Copyright terms: Public domain W3C validator