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

Theorem wilthlem2 26434
Description: Lemma for wilth 26436: 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 26433 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 3306 . . . . . . . . . . . . . . . 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 3649 . . . . . . . . . . . . . 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 4770 . . . . . . . . . 10 (πœ‘ β†’ {(𝑃 βˆ’ 1)} βŠ† 𝑆)
1312adantr 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑆 βŠ† {(𝑃 βˆ’ 1)}) β†’ {(𝑃 βˆ’ 1)} βŠ† 𝑆)
141, 13eqssd 3962 . . . . . . . 8 ((πœ‘ ∧ 𝑆 βŠ† {(𝑃 βˆ’ 1)}) β†’ 𝑆 = {(𝑃 βˆ’ 1)})
1514reseq2d 5938 . . . . . . 7 ((πœ‘ ∧ 𝑆 βŠ† {(𝑃 βˆ’ 1)}) β†’ ( I β†Ύ 𝑆) = ( I β†Ύ {(𝑃 βˆ’ 1)}))
16 mptresid 6005 . . . . . . 7 ( I β†Ύ {(𝑃 βˆ’ 1)}) = (𝑧 ∈ {(𝑃 βˆ’ 1)} ↦ 𝑧)
1715, 16eqtrdi 2789 . . . . . 6 ((πœ‘ ∧ 𝑆 βŠ† {(𝑃 βˆ’ 1)}) β†’ ( I β†Ύ 𝑆) = (𝑧 ∈ {(𝑃 βˆ’ 1)} ↦ 𝑧))
1817oveq2d 7374 . . . . 5 ((πœ‘ ∧ 𝑆 βŠ† {(𝑃 βˆ’ 1)}) β†’ (𝑇 Ξ£g ( I β†Ύ 𝑆)) = (𝑇 Ξ£g (𝑧 ∈ {(𝑃 βˆ’ 1)} ↦ 𝑧)))
1918oveq1d 7373 . . . 4 ((πœ‘ ∧ 𝑆 βŠ† {(𝑃 βˆ’ 1)}) β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑆)) mod 𝑃) = ((𝑇 Ξ£g (𝑧 ∈ {(𝑃 βˆ’ 1)} ↦ 𝑧)) mod 𝑃))
20 wilthlem2.p . . . . . . . . . . . 12 (πœ‘ β†’ 𝑃 ∈ β„™)
21 prmnn 16555 . . . . . . . . . . . 12 (𝑃 ∈ β„™ β†’ 𝑃 ∈ β„•)
2220, 21syl 17 . . . . . . . . . . 11 (πœ‘ β†’ 𝑃 ∈ β„•)
2322nncnd 12174 . . . . . . . . . 10 (πœ‘ β†’ 𝑃 ∈ β„‚)
24 ax-1cn 11114 . . . . . . . . . 10 1 ∈ β„‚
25 negsub 11454 . . . . . . . . . 10 ((𝑃 ∈ β„‚ ∧ 1 ∈ β„‚) β†’ (𝑃 + -1) = (𝑃 βˆ’ 1))
2623, 24, 25sylancl 587 . . . . . . . . 9 (πœ‘ β†’ (𝑃 + -1) = (𝑃 βˆ’ 1))
27 neg1cn 12272 . . . . . . . . . 10 -1 ∈ β„‚
28 addcom 11346 . . . . . . . . . 10 ((𝑃 ∈ β„‚ ∧ -1 ∈ β„‚) β†’ (𝑃 + -1) = (-1 + 𝑃))
2923, 27, 28sylancl 587 . . . . . . . . 9 (πœ‘ β†’ (𝑃 + -1) = (-1 + 𝑃))
3026, 29eqtr3d 2775 . . . . . . . 8 (πœ‘ β†’ (𝑃 βˆ’ 1) = (-1 + 𝑃))
31 cnring 20835 . . . . . . . . . 10 β„‚fld ∈ Ring
32 wilthlem.t . . . . . . . . . . 11 𝑇 = (mulGrpβ€˜β„‚fld)
3332ringmgp 19975 . . . . . . . . . 10 (β„‚fld ∈ Ring β†’ 𝑇 ∈ Mnd)
3431, 33mp1i 13 . . . . . . . . 9 (πœ‘ β†’ 𝑇 ∈ Mnd)
35 nnm1nn0 12459 . . . . . . . . . . 11 (𝑃 ∈ β„• β†’ (𝑃 βˆ’ 1) ∈ β„•0)
3622, 35syl 17 . . . . . . . . . 10 (πœ‘ β†’ (𝑃 βˆ’ 1) ∈ β„•0)
3736nn0cnd 12480 . . . . . . . . 9 (πœ‘ β†’ (𝑃 βˆ’ 1) ∈ β„‚)
38 cnfldbas 20816 . . . . . . . . . . 11 β„‚ = (Baseβ€˜β„‚fld)
3932, 38mgpbas 19907 . . . . . . . . . 10 β„‚ = (Baseβ€˜π‘‡)
40 id 22 . . . . . . . . . 10 (𝑧 = (𝑃 βˆ’ 1) β†’ 𝑧 = (𝑃 βˆ’ 1))
4139, 40gsumsn 19736 . . . . . . . . 9 ((𝑇 ∈ Mnd ∧ (𝑃 βˆ’ 1) ∈ β„‚ ∧ (𝑃 βˆ’ 1) ∈ β„‚) β†’ (𝑇 Ξ£g (𝑧 ∈ {(𝑃 βˆ’ 1)} ↦ 𝑧)) = (𝑃 βˆ’ 1))
4234, 37, 37, 41syl3anc 1372 . . . . . . . 8 (πœ‘ β†’ (𝑇 Ξ£g (𝑧 ∈ {(𝑃 βˆ’ 1)} ↦ 𝑧)) = (𝑃 βˆ’ 1))
4323mulid2d 11178 . . . . . . . . 9 (πœ‘ β†’ (1 Β· 𝑃) = 𝑃)
4443oveq2d 7374 . . . . . . . 8 (πœ‘ β†’ (-1 + (1 Β· 𝑃)) = (-1 + 𝑃))
4530, 42, 443eqtr4d 2783 . . . . . . 7 (πœ‘ β†’ (𝑇 Ξ£g (𝑧 ∈ {(𝑃 βˆ’ 1)} ↦ 𝑧)) = (-1 + (1 Β· 𝑃)))
4645oveq1d 7373 . . . . . 6 (πœ‘ β†’ ((𝑇 Ξ£g (𝑧 ∈ {(𝑃 βˆ’ 1)} ↦ 𝑧)) mod 𝑃) = ((-1 + (1 Β· 𝑃)) mod 𝑃))
47 neg1rr 12273 . . . . . . . 8 -1 ∈ ℝ
4847a1i 11 . . . . . . 7 (πœ‘ β†’ -1 ∈ ℝ)
4922nnrpd 12960 . . . . . . 7 (πœ‘ β†’ 𝑃 ∈ ℝ+)
50 1zzd 12539 . . . . . . 7 (πœ‘ β†’ 1 ∈ β„€)
51 modcyc 13817 . . . . . . 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 4007 . . 3 (Β¬ 𝑆 βŠ† {(𝑃 βˆ’ 1)} ↔ βˆƒπ‘§(𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)}))
58 cnfld1 20838 . . . . . . . . . 10 1 = (1rβ€˜β„‚fld)
5932, 58ringidval 19920 . . . . . . . . 9 1 = (0gβ€˜π‘‡)
60 cnfldmul 20818 . . . . . . . . . 10 Β· = (.rβ€˜β„‚fld)
6132, 60mgpplusg 19905 . . . . . . . . 9 Β· = (+gβ€˜π‘‡)
62 cncrng 20834 . . . . . . . . . . 11 β„‚fld ∈ CRing
6332crngmgp 19977 . . . . . . . . . . 11 (β„‚fld ∈ CRing β†’ 𝑇 ∈ CMnd)
6462, 63ax-mp 5 . . . . . . . . . 10 𝑇 ∈ CMnd
6564a1i 11 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑇 ∈ CMnd)
662adantr 482 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑆 ∈ 𝐴)
67 f1oi 6823 . . . . . . . . . . . 12 ( I β†Ύ 𝑆):𝑆–1-1-onto→𝑆
68 f1of 6785 . . . . . . . . . . . 12 (( I β†Ύ 𝑆):𝑆–1-1-onto→𝑆 β†’ ( I β†Ύ 𝑆):π‘†βŸΆπ‘†)
6967, 68ax-mp 5 . . . . . . . . . . 11 ( I β†Ύ 𝑆):π‘†βŸΆπ‘†
709simpld 496 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑆 ∈ 𝒫 (1...(𝑃 βˆ’ 1)))
7170elpwid 4570 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑆 βŠ† (1...(𝑃 βˆ’ 1)))
72 fzssz 13449 . . . . . . . . . . . . 13 (1...(𝑃 βˆ’ 1)) βŠ† β„€
7371, 72sstrdi 3957 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑆 βŠ† β„€)
74 zsscn 12512 . . . . . . . . . . . 12 β„€ βŠ† β„‚
7573, 74sstrdi 3957 . . . . . . . . . . 11 (πœ‘ β†’ 𝑆 βŠ† β„‚)
76 fss 6686 . . . . . . . . . . 11 ((( I β†Ύ 𝑆):π‘†βŸΆπ‘† ∧ 𝑆 βŠ† β„‚) β†’ ( I β†Ύ 𝑆):π‘†βŸΆβ„‚)
7769, 75, 76sylancr 588 . . . . . . . . . 10 (πœ‘ β†’ ( I β†Ύ 𝑆):π‘†βŸΆβ„‚)
7877adantr 482 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ( I β†Ύ 𝑆):π‘†βŸΆβ„‚)
79 fzfi 13883 . . . . . . . . . . . 12 (1...(𝑃 βˆ’ 1)) ∈ Fin
80 ssfi 9120 . . . . . . . . . . . 12 (((1...(𝑃 βˆ’ 1)) ∈ Fin ∧ 𝑆 βŠ† (1...(𝑃 βˆ’ 1))) β†’ 𝑆 ∈ Fin)
8179, 71, 80sylancr 588 . . . . . . . . . . 11 (πœ‘ β†’ 𝑆 ∈ Fin)
82 1ex 11156 . . . . . . . . . . . 12 1 ∈ V
8382a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ 1 ∈ V)
8477, 81, 83fdmfifsupp 9320 . . . . . . . . . 10 (πœ‘ β†’ ( I β†Ύ 𝑆) finSupp 1)
8584adantr 482 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ( I β†Ύ 𝑆) finSupp 1)
86 disjdif 4432 . . . . . . . . . 10 ({𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} ∩ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = βˆ…
8786a1i 11 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ({𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} ∩ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = βˆ…)
88 undif2 4437 . . . . . . . . . 10 ({𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} βˆͺ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = ({𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} βˆͺ 𝑆)
89 simprl 770 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑧 ∈ 𝑆)
90 oveq1 7365 . . . . . . . . . . . . . . 15 (𝑦 = 𝑧 β†’ (𝑦↑(𝑃 βˆ’ 2)) = (𝑧↑(𝑃 βˆ’ 2)))
9190oveq1d 7373 . . . . . . . . . . . . . 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 3581 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ 𝑆)
9689, 95prssd 4783 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} βŠ† 𝑆)
97 ssequn1 4141 . . . . . . . . . . 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 19710 . . . . . . . 8 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑇 Ξ£g ( I β†Ύ 𝑆)) = ((𝑇 Ξ£g (( I β†Ύ 𝑆) β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) Β· (𝑇 Ξ£g (( I β†Ύ 𝑆) β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))))
10196resabs1d 5969 . . . . . . . . . 10 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (( I β†Ύ 𝑆) β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) = ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
102101oveq2d 7374 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑇 Ξ£g (( I β†Ύ 𝑆) β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = (𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))
103 difss 4092 . . . . . . . . . . . 12 (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) βŠ† 𝑆
104 resabs1 5968 . . . . . . . . . . . 12 ((𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) βŠ† 𝑆 β†’ (( I β†Ύ 𝑆) β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))
105103, 104ax-mp 5 . . . . . . . . . . 11 (( I β†Ύ 𝑆) β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
106105oveq2i 7369 . . . . . . . . . 10 (𝑇 Ξ£g (( I β†Ύ 𝑆) β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))) = (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))
107106a1i 11 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑇 Ξ£g (( I β†Ύ 𝑆) β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))) = (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))))
108102, 107oveq12d 7376 . . . . . . . 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 7373 . . . . . 6 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑆)) mod 𝑃) = (((𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) Β· (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))) mod 𝑃))
111 prfi 9269 . . . . . . . . . 10 {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} ∈ Fin
112111a1i 11 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} ∈ Fin)
113 zsubrg 20866 . . . . . . . . . 10 β„€ ∈ (SubRingβ€˜β„‚fld)
11432subrgsubm 20249 . . . . . . . . . 10 (β„€ ∈ (SubRingβ€˜β„‚fld) β†’ β„€ ∈ (SubMndβ€˜π‘‡))
115113, 114mp1i 13 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ β„€ ∈ (SubMndβ€˜π‘‡))
116 f1oi 6823 . . . . . . . . . . 11 ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}–1-1-ontoβ†’{𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}
117 f1of 6785 . . . . . . . . . . 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 3955 . . . . . . . . . 10 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} βŠ† β„€)
121 fss 6686 . . . . . . . . . 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 9320 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) finSupp 1)
12559, 65, 112, 115, 122, 124gsumsubmcl 19701 . . . . . . . 8 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) ∈ β„€)
126125zred 12612 . . . . . . 7 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) ∈ ℝ)
127 1red 11161 . . . . . . 7 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 1 ∈ ℝ)
12871adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑆 βŠ† (1...(𝑃 βˆ’ 1)))
129128ssdifssd 4103 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) βŠ† (1...(𝑃 βˆ’ 1)))
130 ssfi 9120 . . . . . . . . 9 (((1...(𝑃 βˆ’ 1)) ∈ Fin ∧ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) βŠ† (1...(𝑃 βˆ’ 1))) β†’ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ∈ Fin)
13179, 129, 130sylancr 588 . . . . . . . 8 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ∈ Fin)
132 f1oi 6823 . . . . . . . . . 10 ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})):(𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})–1-1-ontoβ†’(𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})
133 f1of 6785 . . . . . . . . . 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 4103 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) βŠ† β„€)
136 fss 6686 . . . . . . . . 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 9320 . . . . . . . 8 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) finSupp 1)
13959, 65, 131, 115, 137, 138gsumsubmcl 19701 . . . . . . 7 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))) ∈ β„€)
14049adantr 482 . . . . . . 7 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑃 ∈ ℝ+)
14134adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑇 ∈ Mnd)
14275adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑆 βŠ† β„‚)
143142, 89sseldd 3946 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑧 ∈ β„‚)
144 id 22 . . . . . . . . . . . . 13 (𝑀 = 𝑧 β†’ 𝑀 = 𝑧)
14539, 144gsumsn 19736 . . . . . . . . . . . 12 ((𝑇 ∈ Mnd ∧ 𝑧 ∈ β„‚ ∧ 𝑧 ∈ β„‚) β†’ (𝑇 Ξ£g (𝑀 ∈ {𝑧} ↦ 𝑀)) = 𝑧)
146141, 143, 143, 145syl3anc 1372 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑇 Ξ£g (𝑀 ∈ {𝑧} ↦ 𝑀)) = 𝑧)
147146adantr 482 . . . . . . . . . 10 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 = 1) β†’ (𝑇 Ξ£g (𝑀 ∈ {𝑧} ↦ 𝑀)) = 𝑧)
148 mptresid 6005 . . . . . . . . . . . 12 ( I β†Ύ {𝑧}) = (𝑀 ∈ {𝑧} ↦ 𝑀)
149 dfsn2 4600 . . . . . . . . . . . . . 14 {𝑧} = {𝑧, 𝑧}
150 animorrl 980 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 = 1) β†’ (𝑧 = 1 ∨ 𝑧 = (𝑃 βˆ’ 1)))
15120adantr 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑃 ∈ β„™)
152128, 89sseldd 3946 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑧 ∈ (1...(𝑃 βˆ’ 1)))
153 wilthlem1 26433 . . . . . . . . . . . . . . . . . 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 4702 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 = 1) β†’ {𝑧, 𝑧} = {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})
158149, 157eqtrid 2785 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 = 1) β†’ {𝑧} = {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})
159158reseq2d 5938 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 = 1) β†’ ( I β†Ύ {𝑧}) = ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
160148, 159eqtr3id 2787 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 = 1) β†’ (𝑀 ∈ {𝑧} ↦ 𝑀) = ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
161160oveq2d 7374 . . . . . . . . . 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 7373 . . . . . . . 8 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 = 1) β†’ ((𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) mod 𝑃) = (1 mod 𝑃))
165 df-pr 4590 . . . . . . . . . . . . . . 15 {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} = ({𝑧} βˆͺ {((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})
166165reseq2i 5935 . . . . . . . . . . . . . 14 ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) = ( I β†Ύ ({𝑧} βˆͺ {((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
167 mptresid 6005 . . . . . . . . . . . . . 14 ( I β†Ύ ({𝑧} βˆͺ {((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = (𝑀 ∈ ({𝑧} βˆͺ {((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ↦ 𝑀)
168166, 167eqtri 2761 . . . . . . . . . . . . 13 ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) = (𝑀 ∈ ({𝑧} βˆͺ {((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ↦ 𝑀)
169168oveq2i 7369 . . . . . . . . . . . 12 (𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = (𝑇 Ξ£g (𝑀 ∈ ({𝑧} βˆͺ {((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ↦ 𝑀))
17064a1i 11 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) β†’ 𝑇 ∈ CMnd)
171 snfi 8991 . . . . . . . . . . . . . 14 {𝑧} ∈ Fin
172171a1i 11 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) β†’ {𝑧} ∈ Fin)
173 elsni 4604 . . . . . . . . . . . . . . . 16 (𝑀 ∈ {𝑧} β†’ 𝑀 = 𝑧)
174173adantl 483 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑀 ∈ {𝑧}) β†’ 𝑀 = 𝑧)
175143adantr 482 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑀 ∈ {𝑧}) β†’ 𝑧 ∈ β„‚)
176174, 175eqeltrd 2834 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑀 ∈ {𝑧}) β†’ 𝑀 ∈ β„‚)
177176adantlr 714 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) ∧ 𝑀 ∈ {𝑧}) β†’ 𝑀 ∈ β„‚)
178142, 95sseldd 3946 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ β„‚)
179178adantr 482 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) β†’ ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ β„‚)
180 simprr 772 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})
181 velsn 4603 . . . . . . . . . . . . . . . . . 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 7391 . . . . . . . . . . . . . . . . . . 19 ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ V
186185elsn 4602 . . . . . . . . . . . . . . . . . 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 2977 . . . . . . . . . . . . . 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 19742 . . . . . . . . . . . 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 7373 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) β†’ ((𝑇 Ξ£g (𝑀 ∈ {𝑧} ↦ 𝑀)) Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) = (𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)))
199196, 198eqtrd 2773 . . . . . . . . . 10 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) β†’ (𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = (𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)))
200199oveq1d 7373 . . . . . . . . 9 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) β†’ ((𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) mod 𝑃) = ((𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) mod 𝑃))
201152elfzelzd 13448 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑧 ∈ β„€)
20222adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑃 ∈ β„•)
203 fzm1ndvds 16209 . . . . . . . . . . . . . 14 ((𝑃 ∈ β„• ∧ 𝑧 ∈ (1...(𝑃 βˆ’ 1))) β†’ Β¬ 𝑃 βˆ₯ 𝑧)
204202, 152, 203syl2anc 585 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ Β¬ 𝑃 βˆ₯ 𝑧)
205 eqid 2733 . . . . . . . . . . . . . 14 ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)
206205prmdiv 16662 . . . . . . . . . . . . 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 13476 . . . . . . . . . . . . . . 15 (𝑧 ∈ (1...(𝑃 βˆ’ 1)) β†’ 𝑧 ∈ β„•)
210152, 209syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑧 ∈ β„•)
211128, 95sseldd 3946 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (1...(𝑃 βˆ’ 1)))
212 elfznn 13476 . . . . . . . . . . . . . . 15 (((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (1...(𝑃 βˆ’ 1)) β†’ ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ β„•)
213211, 212syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ β„•)
214210, 213nnmulcld 12211 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) ∈ β„•)
215214nnzd 12531 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) ∈ β„€)
216 1zzd 12539 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 1 ∈ β„€)
217 moddvds 16152 . . . . . . . . . . . 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 3029 . . . . . . 7 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) mod 𝑃) = (1 mod 𝑃))
223 modmul1 13835 . . . . . . 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 12613 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))) ∈ β„‚)
226225mulid2d 11178 . . . . . . . 8 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (1 Β· (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))) = (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))))
227226oveq1d 7373 . . . . . . 7 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((1 Β· (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))) mod 𝑃) = ((𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))) mod 𝑃))
228 sseqin2 4176 . . . . . . . . . . 11 ({𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} βŠ† 𝑆 ↔ (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) = {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})
22996, 228sylib 217 . . . . . . . . . 10 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) = {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})
230 vex 3448 . . . . . . . . . . . 12 𝑧 ∈ V
231230prnz 4739 . . . . . . . . . . 11 {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} β‰  βˆ…
232231a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} β‰  βˆ…)
233229, 232eqnetrd 3008 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β‰  βˆ…)
234 disj4 4419 . . . . . . . . . 10 ((𝑆 ∩ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) = βˆ… ↔ Β¬ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ⊊ 𝑆)
235234necon2abii 2991 . . . . . . . . 9 ((𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ⊊ 𝑆 ↔ (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β‰  βˆ…)
236233, 235sylibr 233 . . . . . . . 8 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ⊊ 𝑆)
237 psseq1 4048 . . . . . . . . . 10 (𝑠 = (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β†’ (𝑠 ⊊ 𝑆 ↔ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ⊊ 𝑆))
238 reseq2 5933 . . . . . . . . . . . . 13 (𝑠 = (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β†’ ( I β†Ύ 𝑠) = ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))
239238oveq2d 7374 . . . . . . . . . . . 12 (𝑠 = (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β†’ (𝑇 Ξ£g ( I β†Ύ 𝑠)) = (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))))
240239oveq1d 7373 . . . . . . . . . . 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 7391 . . . . . . . . . . . 12 (1...(𝑃 βˆ’ 1)) ∈ V
246245elpw2 5303 . . . . . . . . . . 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 7365 . . . . . . . . . . . . . . . . 17 ((𝑃 βˆ’ 1) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) β†’ ((𝑃 βˆ’ 1)↑(𝑃 βˆ’ 2)) = (((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)))
253252oveq1d 7373 . . . . . . . . . . . . . . . 16 ((𝑃 βˆ’ 1) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) β†’ (((𝑃 βˆ’ 1)↑(𝑃 βˆ’ 2)) mod 𝑃) = ((((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) mod 𝑃))
254202, 35syl 17 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 βˆ’ 1) ∈ β„•0)
255 nn0uz 12810 . . . . . . . . . . . . . . . . . . . 20 β„•0 = (β„€β‰₯β€˜0)
256254, 255eleqtrdi 2844 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 βˆ’ 1) ∈ (β„€β‰₯β€˜0))
257 eluzfz2 13455 . . . . . . . . . . . . . . . . . . 19 ((𝑃 βˆ’ 1) ∈ (β„€β‰₯β€˜0) β†’ (𝑃 βˆ’ 1) ∈ (0...(𝑃 βˆ’ 1)))
258256, 257syl 17 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 βˆ’ 1) ∈ (0...(𝑃 βˆ’ 1)))
259 prmz 16556 . . . . . . . . . . . . . . . . . . . . 21 (𝑃 ∈ β„™ β†’ 𝑃 ∈ β„€)
260151, 259syl 17 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑃 ∈ β„€)
261119, 248sseldd 3946 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 βˆ’ 1) ∈ β„€)
262 1z 12538 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ β„€
263 zsubcl 12550 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃 βˆ’ 1) ∈ β„€ ∧ 1 ∈ β„€) β†’ ((𝑃 βˆ’ 1) βˆ’ 1) ∈ β„€)
264261, 262, 263sylancl 587 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑃 βˆ’ 1) βˆ’ 1) ∈ β„€)
265 dvdsmul1 16165 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ β„€ ∧ ((𝑃 βˆ’ 1) βˆ’ 1) ∈ β„€) β†’ 𝑃 βˆ₯ (𝑃 Β· ((𝑃 βˆ’ 1) βˆ’ 1)))
266260, 264, 265syl2anc 585 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑃 βˆ₯ (𝑃 Β· ((𝑃 βˆ’ 1) βˆ’ 1)))
267202nncnd 12174 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑃 ∈ β„‚)
268264zcnd 12613 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑃 βˆ’ 1) βˆ’ 1) ∈ β„‚)
269267, 268mulcld 11180 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 Β· ((𝑃 βˆ’ 1) βˆ’ 1)) ∈ β„‚)
270 1cnd 11155 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 1 ∈ β„‚)
271254nn0cnd 12480 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 βˆ’ 1) ∈ β„‚)
272267, 270, 271subdird 11617 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑃 βˆ’ 1) Β· (𝑃 βˆ’ 1)) = ((𝑃 Β· (𝑃 βˆ’ 1)) βˆ’ (1 Β· (𝑃 βˆ’ 1))))
273267, 271mulcld 11180 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 Β· (𝑃 βˆ’ 1)) ∈ β„‚)
274273, 267, 270subsubd 11545 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑃 Β· (𝑃 βˆ’ 1)) βˆ’ (𝑃 βˆ’ 1)) = (((𝑃 Β· (𝑃 βˆ’ 1)) βˆ’ 𝑃) + 1))
275271mulid2d 11178 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (1 Β· (𝑃 βˆ’ 1)) = (𝑃 βˆ’ 1))
276275oveq2d 7374 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑃 Β· (𝑃 βˆ’ 1)) βˆ’ (1 Β· (𝑃 βˆ’ 1))) = ((𝑃 Β· (𝑃 βˆ’ 1)) βˆ’ (𝑃 βˆ’ 1)))
277267, 271muls1d 11620 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 Β· ((𝑃 βˆ’ 1) βˆ’ 1)) = ((𝑃 Β· (𝑃 βˆ’ 1)) βˆ’ 𝑃))
278277oveq1d 7373 . . . . . . . . . . . . . . . . . . . . . 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 11572 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (((𝑃 βˆ’ 1) Β· (𝑃 βˆ’ 1)) βˆ’ 1) = (𝑃 Β· ((𝑃 βˆ’ 1) βˆ’ 1)))
282266, 281breqtrrd 5134 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑃 βˆ₯ (((𝑃 βˆ’ 1) Β· (𝑃 βˆ’ 1)) βˆ’ 1))
283128, 248sseldd 3946 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 βˆ’ 1) ∈ (1...(𝑃 βˆ’ 1)))
284 fzm1ndvds 16209 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ β„• ∧ (𝑃 βˆ’ 1) ∈ (1...(𝑃 βˆ’ 1))) β†’ Β¬ 𝑃 βˆ₯ (𝑃 βˆ’ 1))
285202, 283, 284syl2anc 585 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ Β¬ 𝑃 βˆ₯ (𝑃 βˆ’ 1))
286 eqid 2733 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 βˆ’ 1)↑(𝑃 βˆ’ 2)) mod 𝑃) = (((𝑃 βˆ’ 1)↑(𝑃 βˆ’ 2)) mod 𝑃)
287286prmdiveq 16663 . . . . . . . . . . . . . . . . . . 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 16664 . . . . . . . . . . . . . . . . . 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, 292syl5ibr 246 . . . . . . . . . . . . . . 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 7391 . . . . . . . . . . . . . 14 (𝑃 βˆ’ 1) ∈ V
298297elpr 4610 . . . . . . . . . . . . 13 ((𝑃 βˆ’ 1) ∈ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} ↔ ((𝑃 βˆ’ 1) = 𝑧 ∨ (𝑃 βˆ’ 1) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)))
299296, 298sylnibr 329 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ Β¬ (𝑃 βˆ’ 1) ∈ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})
300248, 299eldifd 3922 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 βˆ’ 1) ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
301 eldifi 4087 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β†’ 𝑦 ∈ 𝑆)
30294r19.21bi 3233 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ 𝑆) β†’ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ 𝑆)
303301, 302sylan2 594 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) β†’ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ 𝑆)
304 eldif 3921 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ↔ (𝑦 ∈ 𝑆 ∧ Β¬ 𝑦 ∈ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
305151adantr 482 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ 𝑆) β†’ 𝑃 ∈ β„™)
306128sselda 3945 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ 𝑆) β†’ 𝑦 ∈ (1...(𝑃 βˆ’ 1)))
307 eqid 2733 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃)
308307prmdivdiv 16664 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ β„™ ∧ 𝑦 ∈ (1...(𝑃 βˆ’ 1))) β†’ 𝑦 = ((((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) mod 𝑃))
309305, 306, 308syl2anc 585 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ 𝑆) β†’ 𝑦 = ((((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) mod 𝑃))
310 oveq1 7365 . . . . . . . . . . . . . . . . . . . . 21 (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = 𝑧 β†’ (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) = (𝑧↑(𝑃 βˆ’ 2)))
311310oveq1d 7373 . . . . . . . . . . . . . . . . . . . 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 7365 . . . . . . . . . . . . . . . . . . . 20 (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) β†’ (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) = (((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)))
315314oveq1d 7373 . . . . . . . . . . . . . . . . . . 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, 317syl5ibr 246 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ 𝑆) β†’ (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) β†’ 𝑦 = 𝑧))
319313, 318orim12d 964 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ 𝑆) β†’ ((((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = 𝑧 ∨ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) β†’ (𝑦 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∨ 𝑦 = 𝑧)))
320 ovex 7391 . . . . . . . . . . . . . . . . . 18 ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ V
321320elpr 4610 . . . . . . . . . . . . . . . . 17 (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} ↔ (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = 𝑧 ∨ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)))
322 vex 3448 . . . . . . . . . . . . . . . . . . 19 𝑦 ∈ V
323322elpr 4610 . . . . . . . . . . . . . . . . . 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 3922 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) β†’ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
331330ralrimiva 3140 . . . . . . . . . . 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 3306 . . . . . . . . . . . 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 3649 . . . . . . . . . 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 3581 . . . . . . . 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 2940  βˆ€wral 3061  {crab 3406  Vcvv 3444   βˆ– cdif 3908   βˆͺ cun 3909   ∩ cin 3910   βŠ† wss 3911   ⊊ wpss 3912  βˆ…c0 4283  π’« cpw 4561  {csn 4587  {cpr 4589   class class class wbr 5106   ↦ cmpt 5189   I cid 5531   β†Ύ cres 5636  βŸΆwf 6493  β€“1-1-ontoβ†’wf1o 6496  β€˜cfv 6497  (class class class)co 7358  Fincfn 8886   finSupp cfsupp 9308  β„‚cc 11054  β„cr 11055  0cc0 11056  1c1 11057   + caddc 11059   Β· cmul 11061   βˆ’ cmin 11390  -cneg 11391  β„•cn 12158  2c2 12213  β„•0cn0 12418  β„€cz 12504  β„€β‰₯cuz 12768  β„+crp 12920  ...cfz 13430   mod cmo 13780  β†‘cexp 13973   βˆ₯ cdvds 16141  β„™cprime 16552   Ξ£g cgsu 17327  Mndcmnd 18561  SubMndcsubmnd 18605  CMndccmn 19567  mulGrpcmgp 19901  Ringcrg 19969  CRingccrg 19970  SubRingcsubrg 20232  β„‚fldccnfld 20812
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 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-cnex 11112  ax-resscn 11113  ax-1cn 11114  ax-icn 11115  ax-addcl 11116  ax-addrcl 11117  ax-mulcl 11118  ax-mulrcl 11119  ax-mulcom 11120  ax-addass 11121  ax-mulass 11122  ax-distr 11123  ax-i2m1 11124  ax-1ne0 11125  ax-1rid 11126  ax-rnegex 11127  ax-rrecex 11128  ax-cnre 11129  ax-pre-lttri 11130  ax-pre-lttrn 11131  ax-pre-ltadd 11132  ax-pre-mulgt0 11133  ax-pre-sup 11134  ax-addf 11135  ax-mulf 11136
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 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-iin 4958  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-of 7618  df-om 7804  df-1st 7922  df-2nd 7923  df-supp 8094  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-2o 8414  df-oadd 8417  df-er 8651  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-fsupp 9309  df-sup 9383  df-inf 9384  df-oi 9451  df-dju 9842  df-card 9880  df-pnf 11196  df-mnf 11197  df-xr 11198  df-ltxr 11199  df-le 11200  df-sub 11392  df-neg 11393  df-div 11818  df-nn 12159  df-2 12221  df-3 12222  df-4 12223  df-5 12224  df-6 12225  df-7 12226  df-8 12227  df-9 12228  df-n0 12419  df-xnn0 12491  df-z 12505  df-dec 12624  df-uz 12769  df-rp 12921  df-fz 13431  df-fzo 13574  df-fl 13703  df-mod 13781  df-seq 13913  df-exp 13974  df-hash 14237  df-cj 14990  df-re 14991  df-im 14992  df-sqrt 15126  df-abs 15127  df-dvds 16142  df-gcd 16380  df-prm 16553  df-phi 16643  df-struct 17024  df-sets 17041  df-slot 17059  df-ndx 17071  df-base 17089  df-ress 17118  df-plusg 17151  df-mulr 17152  df-starv 17153  df-tset 17157  df-ple 17158  df-ds 17160  df-unif 17161  df-0g 17328  df-gsum 17329  df-mre 17471  df-mrc 17472  df-acs 17474  df-mgm 18502  df-sgrp 18551  df-mnd 18562  df-submnd 18607  df-grp 18756  df-minusg 18757  df-mulg 18878  df-subg 18930  df-cntz 19102  df-cmn 19569  df-mgp 19902  df-ur 19919  df-ring 19971  df-cring 19972  df-subrg 20234  df-cnfld 20813
This theorem is referenced by:  wilthlem3  26435
  Copyright terms: Public domain W3C validator