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

Theorem wilthlem2 26570
Description: Lemma for wilth 26572: 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 26569 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 485 . . . . . . . . 9 ((πœ‘ ∧ 𝑆 βŠ† {(𝑃 βˆ’ 1)}) β†’ 𝑆 βŠ† {(𝑃 βˆ’ 1)})
2 wilthlem2.s . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑆 ∈ 𝐴)
3 eleq2 2822 . . . . . . . . . . . . . . . 16 (π‘₯ = 𝑆 β†’ ((𝑃 βˆ’ 1) ∈ π‘₯ ↔ (𝑃 βˆ’ 1) ∈ 𝑆))
4 eleq2 2822 . . . . . . . . . . . . . . . . 17 (π‘₯ = 𝑆 β†’ (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ π‘₯ ↔ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ 𝑆))
54raleqbi1dv 3333 . . . . . . . . . . . . . . . 16 (π‘₯ = 𝑆 β†’ (βˆ€π‘¦ ∈ π‘₯ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ π‘₯ ↔ βˆ€π‘¦ ∈ 𝑆 ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ 𝑆))
63, 5anbi12d 631 . . . . . . . . . . . . . . 15 (π‘₯ = 𝑆 β†’ (((𝑃 βˆ’ 1) ∈ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ π‘₯) ↔ ((𝑃 βˆ’ 1) ∈ 𝑆 ∧ βˆ€π‘¦ ∈ 𝑆 ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ 𝑆)))
7 wilthlem.a . . . . . . . . . . . . . . 15 𝐴 = {π‘₯ ∈ 𝒫 (1...(𝑃 βˆ’ 1)) ∣ ((𝑃 βˆ’ 1) ∈ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ π‘₯)}
86, 7elrab2 3686 . . . . . . . . . . . . . 14 (𝑆 ∈ 𝐴 ↔ (𝑆 ∈ 𝒫 (1...(𝑃 βˆ’ 1)) ∧ ((𝑃 βˆ’ 1) ∈ 𝑆 ∧ βˆ€π‘¦ ∈ 𝑆 ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ 𝑆)))
92, 8sylib 217 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑆 ∈ 𝒫 (1...(𝑃 βˆ’ 1)) ∧ ((𝑃 βˆ’ 1) ∈ 𝑆 ∧ βˆ€π‘¦ ∈ 𝑆 ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ 𝑆)))
109simprd 496 . . . . . . . . . . . 12 (πœ‘ β†’ ((𝑃 βˆ’ 1) ∈ 𝑆 ∧ βˆ€π‘¦ ∈ 𝑆 ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ 𝑆))
1110simpld 495 . . . . . . . . . . 11 (πœ‘ β†’ (𝑃 βˆ’ 1) ∈ 𝑆)
1211snssd 4812 . . . . . . . . . 10 (πœ‘ β†’ {(𝑃 βˆ’ 1)} βŠ† 𝑆)
1312adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑆 βŠ† {(𝑃 βˆ’ 1)}) β†’ {(𝑃 βˆ’ 1)} βŠ† 𝑆)
141, 13eqssd 3999 . . . . . . . 8 ((πœ‘ ∧ 𝑆 βŠ† {(𝑃 βˆ’ 1)}) β†’ 𝑆 = {(𝑃 βˆ’ 1)})
1514reseq2d 5981 . . . . . . 7 ((πœ‘ ∧ 𝑆 βŠ† {(𝑃 βˆ’ 1)}) β†’ ( I β†Ύ 𝑆) = ( I β†Ύ {(𝑃 βˆ’ 1)}))
16 mptresid 6050 . . . . . . 7 ( I β†Ύ {(𝑃 βˆ’ 1)}) = (𝑧 ∈ {(𝑃 βˆ’ 1)} ↦ 𝑧)
1715, 16eqtrdi 2788 . . . . . 6 ((πœ‘ ∧ 𝑆 βŠ† {(𝑃 βˆ’ 1)}) β†’ ( I β†Ύ 𝑆) = (𝑧 ∈ {(𝑃 βˆ’ 1)} ↦ 𝑧))
1817oveq2d 7424 . . . . 5 ((πœ‘ ∧ 𝑆 βŠ† {(𝑃 βˆ’ 1)}) β†’ (𝑇 Ξ£g ( I β†Ύ 𝑆)) = (𝑇 Ξ£g (𝑧 ∈ {(𝑃 βˆ’ 1)} ↦ 𝑧)))
1918oveq1d 7423 . . . 4 ((πœ‘ ∧ 𝑆 βŠ† {(𝑃 βˆ’ 1)}) β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑆)) mod 𝑃) = ((𝑇 Ξ£g (𝑧 ∈ {(𝑃 βˆ’ 1)} ↦ 𝑧)) mod 𝑃))
20 wilthlem2.p . . . . . . . . . . . 12 (πœ‘ β†’ 𝑃 ∈ β„™)
21 prmnn 16610 . . . . . . . . . . . 12 (𝑃 ∈ β„™ β†’ 𝑃 ∈ β„•)
2220, 21syl 17 . . . . . . . . . . 11 (πœ‘ β†’ 𝑃 ∈ β„•)
2322nncnd 12227 . . . . . . . . . 10 (πœ‘ β†’ 𝑃 ∈ β„‚)
24 ax-1cn 11167 . . . . . . . . . 10 1 ∈ β„‚
25 negsub 11507 . . . . . . . . . 10 ((𝑃 ∈ β„‚ ∧ 1 ∈ β„‚) β†’ (𝑃 + -1) = (𝑃 βˆ’ 1))
2623, 24, 25sylancl 586 . . . . . . . . 9 (πœ‘ β†’ (𝑃 + -1) = (𝑃 βˆ’ 1))
27 neg1cn 12325 . . . . . . . . . 10 -1 ∈ β„‚
28 addcom 11399 . . . . . . . . . 10 ((𝑃 ∈ β„‚ ∧ -1 ∈ β„‚) β†’ (𝑃 + -1) = (-1 + 𝑃))
2923, 27, 28sylancl 586 . . . . . . . . 9 (πœ‘ β†’ (𝑃 + -1) = (-1 + 𝑃))
3026, 29eqtr3d 2774 . . . . . . . 8 (πœ‘ β†’ (𝑃 βˆ’ 1) = (-1 + 𝑃))
31 cnring 20966 . . . . . . . . . 10 β„‚fld ∈ Ring
32 wilthlem.t . . . . . . . . . . 11 𝑇 = (mulGrpβ€˜β„‚fld)
3332ringmgp 20061 . . . . . . . . . 10 (β„‚fld ∈ Ring β†’ 𝑇 ∈ Mnd)
3431, 33mp1i 13 . . . . . . . . 9 (πœ‘ β†’ 𝑇 ∈ Mnd)
35 nnm1nn0 12512 . . . . . . . . . . 11 (𝑃 ∈ β„• β†’ (𝑃 βˆ’ 1) ∈ β„•0)
3622, 35syl 17 . . . . . . . . . 10 (πœ‘ β†’ (𝑃 βˆ’ 1) ∈ β„•0)
3736nn0cnd 12533 . . . . . . . . 9 (πœ‘ β†’ (𝑃 βˆ’ 1) ∈ β„‚)
38 cnfldbas 20947 . . . . . . . . . . 11 β„‚ = (Baseβ€˜β„‚fld)
3932, 38mgpbas 19992 . . . . . . . . . 10 β„‚ = (Baseβ€˜π‘‡)
40 id 22 . . . . . . . . . 10 (𝑧 = (𝑃 βˆ’ 1) β†’ 𝑧 = (𝑃 βˆ’ 1))
4139, 40gsumsn 19821 . . . . . . . . 9 ((𝑇 ∈ Mnd ∧ (𝑃 βˆ’ 1) ∈ β„‚ ∧ (𝑃 βˆ’ 1) ∈ β„‚) β†’ (𝑇 Ξ£g (𝑧 ∈ {(𝑃 βˆ’ 1)} ↦ 𝑧)) = (𝑃 βˆ’ 1))
4234, 37, 37, 41syl3anc 1371 . . . . . . . 8 (πœ‘ β†’ (𝑇 Ξ£g (𝑧 ∈ {(𝑃 βˆ’ 1)} ↦ 𝑧)) = (𝑃 βˆ’ 1))
4323mullidd 11231 . . . . . . . . 9 (πœ‘ β†’ (1 Β· 𝑃) = 𝑃)
4443oveq2d 7424 . . . . . . . 8 (πœ‘ β†’ (-1 + (1 Β· 𝑃)) = (-1 + 𝑃))
4530, 42, 443eqtr4d 2782 . . . . . . 7 (πœ‘ β†’ (𝑇 Ξ£g (𝑧 ∈ {(𝑃 βˆ’ 1)} ↦ 𝑧)) = (-1 + (1 Β· 𝑃)))
4645oveq1d 7423 . . . . . 6 (πœ‘ β†’ ((𝑇 Ξ£g (𝑧 ∈ {(𝑃 βˆ’ 1)} ↦ 𝑧)) mod 𝑃) = ((-1 + (1 Β· 𝑃)) mod 𝑃))
47 neg1rr 12326 . . . . . . . 8 -1 ∈ ℝ
4847a1i 11 . . . . . . 7 (πœ‘ β†’ -1 ∈ ℝ)
4922nnrpd 13013 . . . . . . 7 (πœ‘ β†’ 𝑃 ∈ ℝ+)
50 1zzd 12592 . . . . . . 7 (πœ‘ β†’ 1 ∈ β„€)
51 modcyc 13870 . . . . . . 7 ((-1 ∈ ℝ ∧ 𝑃 ∈ ℝ+ ∧ 1 ∈ β„€) β†’ ((-1 + (1 Β· 𝑃)) mod 𝑃) = (-1 mod 𝑃))
5248, 49, 50, 51syl3anc 1371 . . . . . 6 (πœ‘ β†’ ((-1 + (1 Β· 𝑃)) mod 𝑃) = (-1 mod 𝑃))
5346, 52eqtrd 2772 . . . . 5 (πœ‘ β†’ ((𝑇 Ξ£g (𝑧 ∈ {(𝑃 βˆ’ 1)} ↦ 𝑧)) mod 𝑃) = (-1 mod 𝑃))
5453adantr 481 . . . 4 ((πœ‘ ∧ 𝑆 βŠ† {(𝑃 βˆ’ 1)}) β†’ ((𝑇 Ξ£g (𝑧 ∈ {(𝑃 βˆ’ 1)} ↦ 𝑧)) mod 𝑃) = (-1 mod 𝑃))
5519, 54eqtrd 2772 . . 3 ((πœ‘ ∧ 𝑆 βŠ† {(𝑃 βˆ’ 1)}) β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑆)) mod 𝑃) = (-1 mod 𝑃))
5655ex 413 . 2 (πœ‘ β†’ (𝑆 βŠ† {(𝑃 βˆ’ 1)} β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑆)) mod 𝑃) = (-1 mod 𝑃)))
57 nss 4046 . . 3 (Β¬ 𝑆 βŠ† {(𝑃 βˆ’ 1)} ↔ βˆƒπ‘§(𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)}))
58 cnfld1 20969 . . . . . . . . . 10 1 = (1rβ€˜β„‚fld)
5932, 58ringidval 20005 . . . . . . . . 9 1 = (0gβ€˜π‘‡)
60 cnfldmul 20949 . . . . . . . . . 10 Β· = (.rβ€˜β„‚fld)
6132, 60mgpplusg 19990 . . . . . . . . 9 Β· = (+gβ€˜π‘‡)
62 cncrng 20965 . . . . . . . . . . 11 β„‚fld ∈ CRing
6332crngmgp 20063 . . . . . . . . . . 11 (β„‚fld ∈ CRing β†’ 𝑇 ∈ CMnd)
6462, 63ax-mp 5 . . . . . . . . . 10 𝑇 ∈ CMnd
6564a1i 11 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑇 ∈ CMnd)
662adantr 481 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑆 ∈ 𝐴)
67 f1oi 6871 . . . . . . . . . . . 12 ( I β†Ύ 𝑆):𝑆–1-1-onto→𝑆
68 f1of 6833 . . . . . . . . . . . 12 (( I β†Ύ 𝑆):𝑆–1-1-onto→𝑆 β†’ ( I β†Ύ 𝑆):π‘†βŸΆπ‘†)
6967, 68ax-mp 5 . . . . . . . . . . 11 ( I β†Ύ 𝑆):π‘†βŸΆπ‘†
709simpld 495 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑆 ∈ 𝒫 (1...(𝑃 βˆ’ 1)))
7170elpwid 4611 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑆 βŠ† (1...(𝑃 βˆ’ 1)))
72 fzssz 13502 . . . . . . . . . . . . 13 (1...(𝑃 βˆ’ 1)) βŠ† β„€
7371, 72sstrdi 3994 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑆 βŠ† β„€)
74 zsscn 12565 . . . . . . . . . . . 12 β„€ βŠ† β„‚
7573, 74sstrdi 3994 . . . . . . . . . . 11 (πœ‘ β†’ 𝑆 βŠ† β„‚)
76 fss 6734 . . . . . . . . . . 11 ((( I β†Ύ 𝑆):π‘†βŸΆπ‘† ∧ 𝑆 βŠ† β„‚) β†’ ( I β†Ύ 𝑆):π‘†βŸΆβ„‚)
7769, 75, 76sylancr 587 . . . . . . . . . 10 (πœ‘ β†’ ( I β†Ύ 𝑆):π‘†βŸΆβ„‚)
7877adantr 481 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ( I β†Ύ 𝑆):π‘†βŸΆβ„‚)
79 fzfi 13936 . . . . . . . . . . . 12 (1...(𝑃 βˆ’ 1)) ∈ Fin
80 ssfi 9172 . . . . . . . . . . . 12 (((1...(𝑃 βˆ’ 1)) ∈ Fin ∧ 𝑆 βŠ† (1...(𝑃 βˆ’ 1))) β†’ 𝑆 ∈ Fin)
8179, 71, 80sylancr 587 . . . . . . . . . . 11 (πœ‘ β†’ 𝑆 ∈ Fin)
82 1ex 11209 . . . . . . . . . . . 12 1 ∈ V
8382a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ 1 ∈ V)
8477, 81, 83fdmfifsupp 9372 . . . . . . . . . 10 (πœ‘ β†’ ( I β†Ύ 𝑆) finSupp 1)
8584adantr 481 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ( I β†Ύ 𝑆) finSupp 1)
86 disjdif 4471 . . . . . . . . . 10 ({𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} ∩ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = βˆ…
8786a1i 11 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ({𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} ∩ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = βˆ…)
88 undif2 4476 . . . . . . . . . 10 ({𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} βˆͺ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = ({𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} βˆͺ 𝑆)
89 simprl 769 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑧 ∈ 𝑆)
90 oveq1 7415 . . . . . . . . . . . . . . 15 (𝑦 = 𝑧 β†’ (𝑦↑(𝑃 βˆ’ 2)) = (𝑧↑(𝑃 βˆ’ 2)))
9190oveq1d 7423 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 β†’ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃))
9291eleq1d 2818 . . . . . . . . . . . . 13 (𝑦 = 𝑧 β†’ (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ 𝑆 ↔ ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ 𝑆))
9310simprd 496 . . . . . . . . . . . . . 14 (πœ‘ β†’ βˆ€π‘¦ ∈ 𝑆 ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ 𝑆)
9493adantr 481 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ βˆ€π‘¦ ∈ 𝑆 ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ 𝑆)
9592, 94, 89rspcdva 3613 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ 𝑆)
9689, 95prssd 4825 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} βŠ† 𝑆)
97 ssequn1 4180 . . . . . . . . . . 11 ({𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} βŠ† 𝑆 ↔ ({𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} βˆͺ 𝑆) = 𝑆)
9896, 97sylib 217 . . . . . . . . . 10 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ({𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} βˆͺ 𝑆) = 𝑆)
9988, 98eqtr2id 2785 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑆 = ({𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} βˆͺ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))
10039, 59, 61, 65, 66, 78, 85, 87, 99gsumsplit 19795 . . . . . . . 8 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑇 Ξ£g ( I β†Ύ 𝑆)) = ((𝑇 Ξ£g (( I β†Ύ 𝑆) β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) Β· (𝑇 Ξ£g (( I β†Ύ 𝑆) β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))))
10196resabs1d 6012 . . . . . . . . . 10 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (( I β†Ύ 𝑆) β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) = ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
102101oveq2d 7424 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑇 Ξ£g (( I β†Ύ 𝑆) β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = (𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))
103 difss 4131 . . . . . . . . . . . 12 (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) βŠ† 𝑆
104 resabs1 6011 . . . . . . . . . . . 12 ((𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) βŠ† 𝑆 β†’ (( I β†Ύ 𝑆) β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))
105103, 104ax-mp 5 . . . . . . . . . . 11 (( I β†Ύ 𝑆) β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
106105oveq2i 7419 . . . . . . . . . 10 (𝑇 Ξ£g (( I β†Ύ 𝑆) β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))) = (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))
107106a1i 11 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑇 Ξ£g (( I β†Ύ 𝑆) β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))) = (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))))
108102, 107oveq12d 7426 . . . . . . . 8 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑇 Ξ£g (( I β†Ύ 𝑆) β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) Β· (𝑇 Ξ£g (( I β†Ύ 𝑆) β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))) = ((𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) Β· (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))))
109100, 108eqtrd 2772 . . . . . . 7 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑇 Ξ£g ( I β†Ύ 𝑆)) = ((𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) Β· (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))))
110109oveq1d 7423 . . . . . 6 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑆)) mod 𝑃) = (((𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) Β· (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))) mod 𝑃))
111 prfi 9321 . . . . . . . . . 10 {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} ∈ Fin
112111a1i 11 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} ∈ Fin)
113 zsubrg 20997 . . . . . . . . . 10 β„€ ∈ (SubRingβ€˜β„‚fld)
11432subrgsubm 20331 . . . . . . . . . 10 (β„€ ∈ (SubRingβ€˜β„‚fld) β†’ β„€ ∈ (SubMndβ€˜π‘‡))
115113, 114mp1i 13 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ β„€ ∈ (SubMndβ€˜π‘‡))
116 f1oi 6871 . . . . . . . . . . 11 ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}–1-1-ontoβ†’{𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}
117 f1of 6833 . . . . . . . . . . 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 481 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑆 βŠ† β„€)
12096, 119sstrd 3992 . . . . . . . . . 10 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} βŠ† β„€)
121 fss 6734 . . . . . . . . . 10 ((( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}⟢{𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} ∧ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} βŠ† β„€) β†’ ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}βŸΆβ„€)
122118, 120, 121sylancr 587 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}βŸΆβ„€)
12382a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 1 ∈ V)
124122, 112, 123fdmfifsupp 9372 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) finSupp 1)
12559, 65, 112, 115, 122, 124gsumsubmcl 19786 . . . . . . . 8 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) ∈ β„€)
126125zred 12665 . . . . . . 7 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) ∈ ℝ)
127 1red 11214 . . . . . . 7 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 1 ∈ ℝ)
12871adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑆 βŠ† (1...(𝑃 βˆ’ 1)))
129128ssdifssd 4142 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) βŠ† (1...(𝑃 βˆ’ 1)))
130 ssfi 9172 . . . . . . . . 9 (((1...(𝑃 βˆ’ 1)) ∈ Fin ∧ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) βŠ† (1...(𝑃 βˆ’ 1))) β†’ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ∈ Fin)
13179, 129, 130sylancr 587 . . . . . . . 8 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ∈ Fin)
132 f1oi 6871 . . . . . . . . . 10 ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})):(𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})–1-1-ontoβ†’(𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})
133 f1of 6833 . . . . . . . . . 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 4142 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) βŠ† β„€)
136 fss 6734 . . . . . . . . 9 ((( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})):(𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})⟢(𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ∧ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) βŠ† β„€) β†’ ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})):(𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})βŸΆβ„€)
137134, 135, 136sylancr 587 . . . . . . . 8 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})):(𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})βŸΆβ„€)
138137, 131, 123fdmfifsupp 9372 . . . . . . . 8 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) finSupp 1)
13959, 65, 131, 115, 137, 138gsumsubmcl 19786 . . . . . . 7 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))) ∈ β„€)
14049adantr 481 . . . . . . 7 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑃 ∈ ℝ+)
14134adantr 481 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑇 ∈ Mnd)
14275adantr 481 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑆 βŠ† β„‚)
143142, 89sseldd 3983 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑧 ∈ β„‚)
144 id 22 . . . . . . . . . . . . 13 (𝑀 = 𝑧 β†’ 𝑀 = 𝑧)
14539, 144gsumsn 19821 . . . . . . . . . . . 12 ((𝑇 ∈ Mnd ∧ 𝑧 ∈ β„‚ ∧ 𝑧 ∈ β„‚) β†’ (𝑇 Ξ£g (𝑀 ∈ {𝑧} ↦ 𝑀)) = 𝑧)
146141, 143, 143, 145syl3anc 1371 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑇 Ξ£g (𝑀 ∈ {𝑧} ↦ 𝑀)) = 𝑧)
147146adantr 481 . . . . . . . . . 10 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 = 1) β†’ (𝑇 Ξ£g (𝑀 ∈ {𝑧} ↦ 𝑀)) = 𝑧)
148 mptresid 6050 . . . . . . . . . . . 12 ( I β†Ύ {𝑧}) = (𝑀 ∈ {𝑧} ↦ 𝑀)
149 dfsn2 4641 . . . . . . . . . . . . . 14 {𝑧} = {𝑧, 𝑧}
150 animorrl 979 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 = 1) β†’ (𝑧 = 1 ∨ 𝑧 = (𝑃 βˆ’ 1)))
15120adantr 481 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑃 ∈ β„™)
152128, 89sseldd 3983 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑧 ∈ (1...(𝑃 βˆ’ 1)))
153 wilthlem1 26569 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ β„™ ∧ 𝑧 ∈ (1...(𝑃 βˆ’ 1))) β†’ (𝑧 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ↔ (𝑧 = 1 ∨ 𝑧 = (𝑃 βˆ’ 1))))
154151, 152, 153syl2anc 584 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑧 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ↔ (𝑧 = 1 ∨ 𝑧 = (𝑃 βˆ’ 1))))
155154biimpar 478 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ (𝑧 = 1 ∨ 𝑧 = (𝑃 βˆ’ 1))) β†’ 𝑧 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃))
156150, 155syldan 591 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 = 1) β†’ 𝑧 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃))
157156preq2d 4744 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 = 1) β†’ {𝑧, 𝑧} = {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})
158149, 157eqtrid 2784 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 = 1) β†’ {𝑧} = {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})
159158reseq2d 5981 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 = 1) β†’ ( I β†Ύ {𝑧}) = ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
160148, 159eqtr3id 2786 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 = 1) β†’ (𝑀 ∈ {𝑧} ↦ 𝑀) = ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
161160oveq2d 7424 . . . . . . . . . 10 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 = 1) β†’ (𝑇 Ξ£g (𝑀 ∈ {𝑧} ↦ 𝑀)) = (𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))
162 simpr 485 . . . . . . . . . 10 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 = 1) β†’ 𝑧 = 1)
163147, 161, 1623eqtr3d 2780 . . . . . . . . 9 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 = 1) β†’ (𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = 1)
164163oveq1d 7423 . . . . . . . 8 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 = 1) β†’ ((𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) mod 𝑃) = (1 mod 𝑃))
165 df-pr 4631 . . . . . . . . . . . . . . 15 {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} = ({𝑧} βˆͺ {((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})
166165reseq2i 5978 . . . . . . . . . . . . . 14 ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) = ( I β†Ύ ({𝑧} βˆͺ {((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
167 mptresid 6050 . . . . . . . . . . . . . 14 ( I β†Ύ ({𝑧} βˆͺ {((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = (𝑀 ∈ ({𝑧} βˆͺ {((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ↦ 𝑀)
168166, 167eqtri 2760 . . . . . . . . . . . . 13 ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) = (𝑀 ∈ ({𝑧} βˆͺ {((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ↦ 𝑀)
169168oveq2i 7419 . . . . . . . . . . . 12 (𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = (𝑇 Ξ£g (𝑀 ∈ ({𝑧} βˆͺ {((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ↦ 𝑀))
17064a1i 11 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) β†’ 𝑇 ∈ CMnd)
171 snfi 9043 . . . . . . . . . . . . . 14 {𝑧} ∈ Fin
172171a1i 11 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) β†’ {𝑧} ∈ Fin)
173 elsni 4645 . . . . . . . . . . . . . . . 16 (𝑀 ∈ {𝑧} β†’ 𝑀 = 𝑧)
174173adantl 482 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑀 ∈ {𝑧}) β†’ 𝑀 = 𝑧)
175143adantr 481 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑀 ∈ {𝑧}) β†’ 𝑧 ∈ β„‚)
176174, 175eqeltrd 2833 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑀 ∈ {𝑧}) β†’ 𝑀 ∈ β„‚)
177176adantlr 713 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) ∧ 𝑀 ∈ {𝑧}) β†’ 𝑀 ∈ β„‚)
178142, 95sseldd 3983 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ β„‚)
179178adantr 481 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) β†’ ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ β„‚)
180 simprr 771 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})
181 velsn 4644 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ {(𝑃 βˆ’ 1)} ↔ 𝑧 = (𝑃 βˆ’ 1))
182180, 181sylnib 327 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ Β¬ 𝑧 = (𝑃 βˆ’ 1))
183 biorf 935 . . . . . . . . . . . . . . . . 17 (Β¬ 𝑧 = (𝑃 βˆ’ 1) β†’ (𝑧 = 1 ↔ (𝑧 = (𝑃 βˆ’ 1) ∨ 𝑧 = 1)))
184182, 183syl 17 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑧 = 1 ↔ (𝑧 = (𝑃 βˆ’ 1) ∨ 𝑧 = 1)))
185 ovex 7441 . . . . . . . . . . . . . . . . . . 19 ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ V
186185elsn 4643 . . . . . . . . . . . . . . . . . 18 (((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ {𝑧} ↔ ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) = 𝑧)
187 eqcom 2739 . . . . . . . . . . . . . . . . . 18 (((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) = 𝑧 ↔ 𝑧 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃))
188186, 187bitri 274 . . . . . . . . . . . . . . . . 17 (((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ {𝑧} ↔ 𝑧 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃))
189 orcom 868 . . . . . . . . . . . . . . . . 17 ((𝑧 = (𝑃 βˆ’ 1) ∨ 𝑧 = 1) ↔ (𝑧 = 1 ∨ 𝑧 = (𝑃 βˆ’ 1)))
190154, 188, 1893bitr4g 313 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ {𝑧} ↔ (𝑧 = (𝑃 βˆ’ 1) ∨ 𝑧 = 1)))
191184, 190bitr4d 281 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑧 = 1 ↔ ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ {𝑧}))
192191necon3abid 2977 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑧 β‰  1 ↔ Β¬ ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ {𝑧}))
193192biimpa 477 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) β†’ Β¬ ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ {𝑧})
194 id 22 . . . . . . . . . . . . 13 (𝑀 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) β†’ 𝑀 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃))
19539, 61, 170, 172, 177, 179, 193, 179, 194gsumunsn 19827 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) β†’ (𝑇 Ξ£g (𝑀 ∈ ({𝑧} βˆͺ {((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ↦ 𝑀)) = ((𝑇 Ξ£g (𝑀 ∈ {𝑧} ↦ 𝑀)) Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)))
196169, 195eqtrid 2784 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) β†’ (𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = ((𝑇 Ξ£g (𝑀 ∈ {𝑧} ↦ 𝑀)) Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)))
197146adantr 481 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) β†’ (𝑇 Ξ£g (𝑀 ∈ {𝑧} ↦ 𝑀)) = 𝑧)
198197oveq1d 7423 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) β†’ ((𝑇 Ξ£g (𝑀 ∈ {𝑧} ↦ 𝑀)) Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) = (𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)))
199196, 198eqtrd 2772 . . . . . . . . . 10 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) β†’ (𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) = (𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)))
200199oveq1d 7423 . . . . . . . . 9 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) β†’ ((𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) mod 𝑃) = ((𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) mod 𝑃))
201152elfzelzd 13501 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑧 ∈ β„€)
20222adantr 481 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑃 ∈ β„•)
203 fzm1ndvds 16264 . . . . . . . . . . . . . 14 ((𝑃 ∈ β„• ∧ 𝑧 ∈ (1...(𝑃 βˆ’ 1))) β†’ Β¬ 𝑃 βˆ₯ 𝑧)
204202, 152, 203syl2anc 584 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ Β¬ 𝑃 βˆ₯ 𝑧)
205 eqid 2732 . . . . . . . . . . . . . 14 ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)
206205prmdiv 16717 . . . . . . . . . . . . 13 ((𝑃 ∈ β„™ ∧ 𝑧 ∈ β„€ ∧ Β¬ 𝑃 βˆ₯ 𝑧) β†’ (((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (1...(𝑃 βˆ’ 1)) ∧ 𝑃 βˆ₯ ((𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) βˆ’ 1)))
207151, 201, 204, 206syl3anc 1371 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (1...(𝑃 βˆ’ 1)) ∧ 𝑃 βˆ₯ ((𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) βˆ’ 1)))
208207simprd 496 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑃 βˆ₯ ((𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) βˆ’ 1))
209 elfznn 13529 . . . . . . . . . . . . . . 15 (𝑧 ∈ (1...(𝑃 βˆ’ 1)) β†’ 𝑧 ∈ β„•)
210152, 209syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑧 ∈ β„•)
211128, 95sseldd 3983 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (1...(𝑃 βˆ’ 1)))
212 elfznn 13529 . . . . . . . . . . . . . . 15 (((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (1...(𝑃 βˆ’ 1)) β†’ ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ β„•)
213211, 212syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ β„•)
214210, 213nnmulcld 12264 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) ∈ β„•)
215214nnzd 12584 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) ∈ β„€)
216 1zzd 12592 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 1 ∈ β„€)
217 moddvds 16207 . . . . . . . . . . . 12 ((𝑃 ∈ β„• ∧ (𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) ∈ β„€ ∧ 1 ∈ β„€) β†’ (((𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 βˆ₯ ((𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) βˆ’ 1)))
218202, 215, 216, 217syl3anc 1371 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (((𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 βˆ₯ ((𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) βˆ’ 1)))
219208, 218mpbird 256 . . . . . . . . . 10 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) mod 𝑃) = (1 mod 𝑃))
220219adantr 481 . . . . . . . . 9 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑧 β‰  1) β†’ ((𝑧 Β· ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) mod 𝑃) = (1 mod 𝑃))
221200, 220eqtrd 2772 . . . . . . . 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 13888 . . . . . . 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 1381 . . . . . 6 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (((𝑇 Ξ£g ( I β†Ύ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) Β· (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))) mod 𝑃) = ((1 Β· (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))) mod 𝑃))
225139zcnd 12666 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))) ∈ β„‚)
226225mullidd 11231 . . . . . . . 8 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (1 Β· (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))) = (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))))
227226oveq1d 7423 . . . . . . 7 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((1 Β· (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))) mod 𝑃) = ((𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))) mod 𝑃))
228 sseqin2 4215 . . . . . . . . . . 11 ({𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} βŠ† 𝑆 ↔ (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) = {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})
22996, 228sylib 217 . . . . . . . . . 10 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) = {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})
230 vex 3478 . . . . . . . . . . . 12 𝑧 ∈ V
231230prnz 4781 . . . . . . . . . . 11 {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} β‰  βˆ…
232231a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} β‰  βˆ…)
233229, 232eqnetrd 3008 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β‰  βˆ…)
234 disj4 4458 . . . . . . . . . 10 ((𝑆 ∩ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) = βˆ… ↔ Β¬ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ⊊ 𝑆)
235234necon2abii 2991 . . . . . . . . 9 ((𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ⊊ 𝑆 ↔ (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β‰  βˆ…)
236233, 235sylibr 233 . . . . . . . 8 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ⊊ 𝑆)
237 psseq1 4087 . . . . . . . . . 10 (𝑠 = (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β†’ (𝑠 ⊊ 𝑆 ↔ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ⊊ 𝑆))
238 reseq2 5976 . . . . . . . . . . . . 13 (𝑠 = (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β†’ ( I β†Ύ 𝑠) = ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))
239238oveq2d 7424 . . . . . . . . . . . 12 (𝑠 = (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β†’ (𝑇 Ξ£g ( I β†Ύ 𝑠)) = (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))))
240239oveq1d 7423 . . . . . . . . . . 11 (𝑠 = (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = ((𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))) mod 𝑃))
241240eqeq1d 2734 . . . . . . . . . 10 (𝑠 = (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β†’ (((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃) ↔ ((𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))) mod 𝑃) = (-1 mod 𝑃)))
242237, 241imbi12d 344 . . . . . . . . 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 481 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ βˆ€π‘  ∈ 𝐴 (𝑠 ⊊ 𝑆 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))
245 ovex 7441 . . . . . . . . . . . 12 (1...(𝑃 βˆ’ 1)) ∈ V
246245elpw2 5345 . . . . . . . . . . 11 ((𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ∈ 𝒫 (1...(𝑃 βˆ’ 1)) ↔ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) βŠ† (1...(𝑃 βˆ’ 1)))
247129, 246sylibr 233 . . . . . . . . . 10 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ∈ 𝒫 (1...(𝑃 βˆ’ 1)))
24811adantr 481 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 βˆ’ 1) ∈ 𝑆)
249 eqcom 2739 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑃 βˆ’ 1) ↔ (𝑃 βˆ’ 1) = 𝑧)
250181, 249bitri 274 . . . . . . . . . . . . . . 15 (𝑧 ∈ {(𝑃 βˆ’ 1)} ↔ (𝑃 βˆ’ 1) = 𝑧)
251180, 250sylnib 327 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ Β¬ (𝑃 βˆ’ 1) = 𝑧)
252 oveq1 7415 . . . . . . . . . . . . . . . . 17 ((𝑃 βˆ’ 1) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) β†’ ((𝑃 βˆ’ 1)↑(𝑃 βˆ’ 2)) = (((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)))
253252oveq1d 7423 . . . . . . . . . . . . . . . 16 ((𝑃 βˆ’ 1) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) β†’ (((𝑃 βˆ’ 1)↑(𝑃 βˆ’ 2)) mod 𝑃) = ((((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) mod 𝑃))
254202, 35syl 17 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 βˆ’ 1) ∈ β„•0)
255 nn0uz 12863 . . . . . . . . . . . . . . . . . . . 20 β„•0 = (β„€β‰₯β€˜0)
256254, 255eleqtrdi 2843 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 βˆ’ 1) ∈ (β„€β‰₯β€˜0))
257 eluzfz2 13508 . . . . . . . . . . . . . . . . . . 19 ((𝑃 βˆ’ 1) ∈ (β„€β‰₯β€˜0) β†’ (𝑃 βˆ’ 1) ∈ (0...(𝑃 βˆ’ 1)))
258256, 257syl 17 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 βˆ’ 1) ∈ (0...(𝑃 βˆ’ 1)))
259 prmz 16611 . . . . . . . . . . . . . . . . . . . . 21 (𝑃 ∈ β„™ β†’ 𝑃 ∈ β„€)
260151, 259syl 17 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑃 ∈ β„€)
261119, 248sseldd 3983 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 βˆ’ 1) ∈ β„€)
262 1z 12591 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ β„€
263 zsubcl 12603 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃 βˆ’ 1) ∈ β„€ ∧ 1 ∈ β„€) β†’ ((𝑃 βˆ’ 1) βˆ’ 1) ∈ β„€)
264261, 262, 263sylancl 586 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑃 βˆ’ 1) βˆ’ 1) ∈ β„€)
265 dvdsmul1 16220 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ β„€ ∧ ((𝑃 βˆ’ 1) βˆ’ 1) ∈ β„€) β†’ 𝑃 βˆ₯ (𝑃 Β· ((𝑃 βˆ’ 1) βˆ’ 1)))
266260, 264, 265syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑃 βˆ₯ (𝑃 Β· ((𝑃 βˆ’ 1) βˆ’ 1)))
267202nncnd 12227 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑃 ∈ β„‚)
268264zcnd 12666 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑃 βˆ’ 1) βˆ’ 1) ∈ β„‚)
269267, 268mulcld 11233 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 Β· ((𝑃 βˆ’ 1) βˆ’ 1)) ∈ β„‚)
270 1cnd 11208 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 1 ∈ β„‚)
271254nn0cnd 12533 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 βˆ’ 1) ∈ β„‚)
272267, 270, 271subdird 11670 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑃 βˆ’ 1) Β· (𝑃 βˆ’ 1)) = ((𝑃 Β· (𝑃 βˆ’ 1)) βˆ’ (1 Β· (𝑃 βˆ’ 1))))
273267, 271mulcld 11233 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 Β· (𝑃 βˆ’ 1)) ∈ β„‚)
274273, 267, 270subsubd 11598 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑃 Β· (𝑃 βˆ’ 1)) βˆ’ (𝑃 βˆ’ 1)) = (((𝑃 Β· (𝑃 βˆ’ 1)) βˆ’ 𝑃) + 1))
275271mullidd 11231 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (1 Β· (𝑃 βˆ’ 1)) = (𝑃 βˆ’ 1))
276275oveq2d 7424 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑃 Β· (𝑃 βˆ’ 1)) βˆ’ (1 Β· (𝑃 βˆ’ 1))) = ((𝑃 Β· (𝑃 βˆ’ 1)) βˆ’ (𝑃 βˆ’ 1)))
277267, 271muls1d 11673 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 Β· ((𝑃 βˆ’ 1) βˆ’ 1)) = ((𝑃 Β· (𝑃 βˆ’ 1)) βˆ’ 𝑃))
278277oveq1d 7423 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑃 Β· ((𝑃 βˆ’ 1) βˆ’ 1)) + 1) = (((𝑃 Β· (𝑃 βˆ’ 1)) βˆ’ 𝑃) + 1))
279274, 276, 2783eqtr4d 2782 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑃 Β· (𝑃 βˆ’ 1)) βˆ’ (1 Β· (𝑃 βˆ’ 1))) = ((𝑃 Β· ((𝑃 βˆ’ 1) βˆ’ 1)) + 1))
280272, 279eqtrd 2772 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑃 βˆ’ 1) Β· (𝑃 βˆ’ 1)) = ((𝑃 Β· ((𝑃 βˆ’ 1) βˆ’ 1)) + 1))
281269, 270, 280mvrraddd 11625 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (((𝑃 βˆ’ 1) Β· (𝑃 βˆ’ 1)) βˆ’ 1) = (𝑃 Β· ((𝑃 βˆ’ 1) βˆ’ 1)))
282266, 281breqtrrd 5176 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑃 βˆ₯ (((𝑃 βˆ’ 1) Β· (𝑃 βˆ’ 1)) βˆ’ 1))
283128, 248sseldd 3983 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 βˆ’ 1) ∈ (1...(𝑃 βˆ’ 1)))
284 fzm1ndvds 16264 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ β„• ∧ (𝑃 βˆ’ 1) ∈ (1...(𝑃 βˆ’ 1))) β†’ Β¬ 𝑃 βˆ₯ (𝑃 βˆ’ 1))
285202, 283, 284syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ Β¬ 𝑃 βˆ₯ (𝑃 βˆ’ 1))
286 eqid 2732 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 βˆ’ 1)↑(𝑃 βˆ’ 2)) mod 𝑃) = (((𝑃 βˆ’ 1)↑(𝑃 βˆ’ 2)) mod 𝑃)
287286prmdiveq 16718 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ β„™ ∧ (𝑃 βˆ’ 1) ∈ β„€ ∧ Β¬ 𝑃 βˆ₯ (𝑃 βˆ’ 1)) β†’ (((𝑃 βˆ’ 1) ∈ (0...(𝑃 βˆ’ 1)) ∧ 𝑃 βˆ₯ (((𝑃 βˆ’ 1) Β· (𝑃 βˆ’ 1)) βˆ’ 1)) ↔ (𝑃 βˆ’ 1) = (((𝑃 βˆ’ 1)↑(𝑃 βˆ’ 2)) mod 𝑃)))
288151, 261, 285, 287syl3anc 1371 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (((𝑃 βˆ’ 1) ∈ (0...(𝑃 βˆ’ 1)) ∧ 𝑃 βˆ₯ (((𝑃 βˆ’ 1) Β· (𝑃 βˆ’ 1)) βˆ’ 1)) ↔ (𝑃 βˆ’ 1) = (((𝑃 βˆ’ 1)↑(𝑃 βˆ’ 2)) mod 𝑃)))
289258, 282, 288mpbi2and 710 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 βˆ’ 1) = (((𝑃 βˆ’ 1)↑(𝑃 βˆ’ 2)) mod 𝑃))
290205prmdivdiv 16719 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ β„™ ∧ 𝑧 ∈ (1...(𝑃 βˆ’ 1))) β†’ 𝑧 = ((((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) mod 𝑃))
291151, 152, 290syl2anc 584 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ 𝑧 = ((((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) mod 𝑃))
292289, 291eqeq12d 2748 . . . . . . . . . . . . . . . 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 982 . . . . . . . . . . . . . 14 (Β¬ ((𝑃 βˆ’ 1) = 𝑧 ∨ (𝑃 βˆ’ 1) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) ↔ (Β¬ (𝑃 βˆ’ 1) = 𝑧 ∧ Β¬ (𝑃 βˆ’ 1) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)))
296251, 294, 295sylanbrc 583 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ Β¬ ((𝑃 βˆ’ 1) = 𝑧 ∨ (𝑃 βˆ’ 1) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)))
297 ovex 7441 . . . . . . . . . . . . . 14 (𝑃 βˆ’ 1) ∈ V
298297elpr 4651 . . . . . . . . . . . . 13 ((𝑃 βˆ’ 1) ∈ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} ↔ ((𝑃 βˆ’ 1) = 𝑧 ∨ (𝑃 βˆ’ 1) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)))
299296, 298sylnibr 328 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ Β¬ (𝑃 βˆ’ 1) ∈ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})
300248, 299eldifd 3959 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑃 βˆ’ 1) ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
301 eldifi 4126 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β†’ 𝑦 ∈ 𝑆)
30294r19.21bi 3248 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ 𝑆) β†’ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ 𝑆)
303301, 302sylan2 593 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) β†’ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ 𝑆)
304 eldif 3958 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ↔ (𝑦 ∈ 𝑆 ∧ Β¬ 𝑦 ∈ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
305151adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ 𝑆) β†’ 𝑃 ∈ β„™)
306128sselda 3982 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ 𝑆) β†’ 𝑦 ∈ (1...(𝑃 βˆ’ 1)))
307 eqid 2732 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃)
308307prmdivdiv 16719 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ β„™ ∧ 𝑦 ∈ (1...(𝑃 βˆ’ 1))) β†’ 𝑦 = ((((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) mod 𝑃))
309305, 306, 308syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ 𝑆) β†’ 𝑦 = ((((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) mod 𝑃))
310 oveq1 7415 . . . . . . . . . . . . . . . . . . . . 21 (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = 𝑧 β†’ (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) = (𝑧↑(𝑃 βˆ’ 2)))
311310oveq1d 7423 . . . . . . . . . . . . . . . . . . . 20 (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = 𝑧 β†’ ((((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) mod 𝑃) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃))
312311eqeq2d 2743 . . . . . . . . . . . . . . . . . . 19 (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = 𝑧 β†’ (𝑦 = ((((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) mod 𝑃) ↔ 𝑦 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)))
313309, 312syl5ibcom 244 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ 𝑆) β†’ (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = 𝑧 β†’ 𝑦 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)))
314 oveq1 7415 . . . . . . . . . . . . . . . . . . . 20 (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) β†’ (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) = (((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)))
315314oveq1d 7423 . . . . . . . . . . . . . . . . . . 19 (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) β†’ ((((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) mod 𝑃) = ((((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) mod 𝑃))
316291adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ 𝑆) β†’ 𝑧 = ((((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) mod 𝑃))
317309, 316eqeq12d 2748 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ 𝑆) β†’ (𝑦 = 𝑧 ↔ ((((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) mod 𝑃) = ((((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)↑(𝑃 βˆ’ 2)) mod 𝑃)))
318315, 317imbitrrid 245 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ 𝑆) β†’ (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) β†’ 𝑦 = 𝑧))
319313, 318orim12d 963 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ 𝑆) β†’ ((((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = 𝑧 ∨ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) β†’ (𝑦 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∨ 𝑦 = 𝑧)))
320 ovex 7441 . . . . . . . . . . . . . . . . . 18 ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ V
321320elpr 4651 . . . . . . . . . . . . . . . . 17 (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} ↔ (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = 𝑧 ∨ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)))
322 vex 3478 . . . . . . . . . . . . . . . . . . 19 𝑦 ∈ V
323322elpr 4651 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} ↔ (𝑦 = 𝑧 ∨ 𝑦 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)))
324 orcom 868 . . . . . . . . . . . . . . . . . 18 ((𝑦 = 𝑧 ∨ 𝑦 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)) ↔ (𝑦 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∨ 𝑦 = 𝑧))
325323, 324bitri 274 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} ↔ (𝑦 = ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃) ∨ 𝑦 = 𝑧))
326319, 321, 3253imtr4g 295 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ 𝑆) β†’ (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} β†’ 𝑦 ∈ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
327326con3d 152 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ 𝑆) β†’ (Β¬ 𝑦 ∈ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)} β†’ Β¬ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
328327impr 455 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ (𝑦 ∈ 𝑆 ∧ Β¬ 𝑦 ∈ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) β†’ Β¬ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})
329304, 328sylan2b 594 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) β†’ Β¬ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})
330303, 329eldifd 3959 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) ∧ 𝑦 ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})) β†’ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
331330ralrimiva 3146 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ βˆ€π‘¦ ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))
332300, 331jca 512 . . . . . . . . . 10 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑃 βˆ’ 1) ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ∧ βˆ€π‘¦ ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))
333 eleq2 2822 . . . . . . . . . . . 12 (π‘₯ = (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β†’ ((𝑃 βˆ’ 1) ∈ π‘₯ ↔ (𝑃 βˆ’ 1) ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))
334 eleq2 2822 . . . . . . . . . . . . 13 (π‘₯ = (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β†’ (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ π‘₯ ↔ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))
335334raleqbi1dv 3333 . . . . . . . . . . . 12 (π‘₯ = (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β†’ (βˆ€π‘¦ ∈ π‘₯ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ π‘₯ ↔ βˆ€π‘¦ ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))
336333, 335anbi12d 631 . . . . . . . . . . 11 (π‘₯ = (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) β†’ (((𝑃 βˆ’ 1) ∈ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ π‘₯) ↔ ((𝑃 βˆ’ 1) ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ∧ βˆ€π‘¦ ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))))
337336, 7elrab2 3686 . . . . . . . . . 10 ((𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ∈ 𝐴 ↔ ((𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ∈ 𝒫 (1...(𝑃 βˆ’ 1)) ∧ ((𝑃 βˆ’ 1) ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ∧ βˆ€π‘¦ ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}))))
338247, 332, 337sylanbrc 583 . . . . . . . . 9 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)}) ∈ 𝐴)
339242, 244, 338rspcdva 3613 . . . . . . . 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 2772 . . . . . 6 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((1 Β· (𝑇 Ξ£g ( I β†Ύ (𝑆 βˆ– {𝑧, ((𝑧↑(𝑃 βˆ’ 2)) mod 𝑃)})))) mod 𝑃) = (-1 mod 𝑃))
342110, 224, 3413eqtrd 2776 . . . . 5 ((πœ‘ ∧ (𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)})) β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑆)) mod 𝑃) = (-1 mod 𝑃))
343342ex 413 . . . 4 (πœ‘ β†’ ((𝑧 ∈ 𝑆 ∧ Β¬ 𝑧 ∈ {(𝑃 βˆ’ 1)}) β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑆)) mod 𝑃) = (-1 mod 𝑃)))
344343exlimdv 1936 . . 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 396   ∨ wo 845   = wceq 1541  βˆƒwex 1781   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061  {crab 3432  Vcvv 3474   βˆ– cdif 3945   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948   ⊊ wpss 3949  βˆ…c0 4322  π’« cpw 4602  {csn 4628  {cpr 4630   class class class wbr 5148   ↦ cmpt 5231   I cid 5573   β†Ύ cres 5678  βŸΆwf 6539  β€“1-1-ontoβ†’wf1o 6542  β€˜cfv 6543  (class class class)co 7408  Fincfn 8938   finSupp cfsupp 9360  β„‚cc 11107  β„cr 11108  0cc0 11109  1c1 11110   + caddc 11112   Β· cmul 11114   βˆ’ cmin 11443  -cneg 11444  β„•cn 12211  2c2 12266  β„•0cn0 12471  β„€cz 12557  β„€β‰₯cuz 12821  β„+crp 12973  ...cfz 13483   mod cmo 13833  β†‘cexp 14026   βˆ₯ cdvds 16196  β„™cprime 16607   Ξ£g cgsu 17385  Mndcmnd 18624  SubMndcsubmnd 18669  CMndccmn 19647  mulGrpcmgp 19986  Ringcrg 20055  CRingccrg 20056  SubRingcsubrg 20314  β„‚fldccnfld 20943
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-cnex 11165  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186  ax-pre-sup 11187  ax-addf 11188  ax-mulf 11189
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7364  df-ov 7411  df-oprab 7412  df-mpo 7413  df-of 7669  df-om 7855  df-1st 7974  df-2nd 7975  df-supp 8146  df-frecs 8265  df-wrecs 8296  df-recs 8370  df-rdg 8409  df-1o 8465  df-2o 8466  df-oadd 8469  df-er 8702  df-en 8939  df-dom 8940  df-sdom 8941  df-fin 8942  df-fsupp 9361  df-sup 9436  df-inf 9437  df-oi 9504  df-dju 9895  df-card 9933  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11445  df-neg 11446  df-div 11871  df-nn 12212  df-2 12274  df-3 12275  df-4 12276  df-5 12277  df-6 12278  df-7 12279  df-8 12280  df-9 12281  df-n0 12472  df-xnn0 12544  df-z 12558  df-dec 12677  df-uz 12822  df-rp 12974  df-fz 13484  df-fzo 13627  df-fl 13756  df-mod 13834  df-seq 13966  df-exp 14027  df-hash 14290  df-cj 15045  df-re 15046  df-im 15047  df-sqrt 15181  df-abs 15182  df-dvds 16197  df-gcd 16435  df-prm 16608  df-phi 16698  df-struct 17079  df-sets 17096  df-slot 17114  df-ndx 17126  df-base 17144  df-ress 17173  df-plusg 17209  df-mulr 17210  df-starv 17211  df-tset 17215  df-ple 17216  df-ds 17218  df-unif 17219  df-0g 17386  df-gsum 17387  df-mre 17529  df-mrc 17530  df-acs 17532  df-mgm 18560  df-sgrp 18609  df-mnd 18625  df-submnd 18671  df-grp 18821  df-minusg 18822  df-mulg 18950  df-subg 19002  df-cntz 19180  df-cmn 19649  df-mgp 19987  df-ur 20004  df-ring 20057  df-cring 20058  df-subrg 20316  df-cnfld 20944
This theorem is referenced by:  wilthlem3  26571
  Copyright terms: Public domain W3C validator