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

Theorem wilthlem3 26581
Description: Lemma for wilth 26582. Here we round out the argument of wilthlem2 26580 with the final step of the induction. The induction argument shows that every subset of 1...(𝑃 βˆ’ 1) that is closed under inverse and contains 𝑃 βˆ’ 1 multiplies to -1 mod 𝑃, and clearly 1...(𝑃 βˆ’ 1) itself is such a set. Thus, the product of all the elements is -1, and all that is left is to translate the group sum notation (which we used for its unordered summing capabilities) into an ordered sequence to match the definition of the factorial. (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 𝑃) ∈ π‘₯)}
Assertion
Ref Expression
wilthlem3 (𝑃 ∈ β„™ β†’ 𝑃 βˆ₯ ((!β€˜(𝑃 βˆ’ 1)) + 1))
Distinct variable groups:   π‘₯,𝑦,𝐴   π‘₯,𝑃,𝑦   π‘₯,𝑇,𝑦

Proof of Theorem wilthlem3
Dummy variables 𝑑 𝑠 π‘˜ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prmuz2 16635 . . . . . . . 8 (𝑃 ∈ β„™ β†’ 𝑃 ∈ (β„€β‰₯β€˜2))
2 uz2m1nn 12909 . . . . . . . 8 (𝑃 ∈ (β„€β‰₯β€˜2) β†’ (𝑃 βˆ’ 1) ∈ β„•)
31, 2syl 17 . . . . . . 7 (𝑃 ∈ β„™ β†’ (𝑃 βˆ’ 1) ∈ β„•)
4 nnuz 12867 . . . . . . 7 β„• = (β„€β‰₯β€˜1)
53, 4eleqtrdi 2843 . . . . . 6 (𝑃 ∈ β„™ β†’ (𝑃 βˆ’ 1) ∈ (β„€β‰₯β€˜1))
6 eluzfz2 13511 . . . . . 6 ((𝑃 βˆ’ 1) ∈ (β„€β‰₯β€˜1) β†’ (𝑃 βˆ’ 1) ∈ (1...(𝑃 βˆ’ 1)))
75, 6syl 17 . . . . 5 (𝑃 ∈ β„™ β†’ (𝑃 βˆ’ 1) ∈ (1...(𝑃 βˆ’ 1)))
8 simpl 483 . . . . . . . 8 ((𝑃 ∈ β„™ ∧ 𝑦 ∈ (1...(𝑃 βˆ’ 1))) β†’ 𝑃 ∈ β„™)
9 elfzelz 13503 . . . . . . . . 9 (𝑦 ∈ (1...(𝑃 βˆ’ 1)) β†’ 𝑦 ∈ β„€)
109adantl 482 . . . . . . . 8 ((𝑃 ∈ β„™ ∧ 𝑦 ∈ (1...(𝑃 βˆ’ 1))) β†’ 𝑦 ∈ β„€)
11 prmnn 16613 . . . . . . . . 9 (𝑃 ∈ β„™ β†’ 𝑃 ∈ β„•)
12 fzm1ndvds 16267 . . . . . . . . 9 ((𝑃 ∈ β„• ∧ 𝑦 ∈ (1...(𝑃 βˆ’ 1))) β†’ Β¬ 𝑃 βˆ₯ 𝑦)
1311, 12sylan 580 . . . . . . . 8 ((𝑃 ∈ β„™ ∧ 𝑦 ∈ (1...(𝑃 βˆ’ 1))) β†’ Β¬ 𝑃 βˆ₯ 𝑦)
14 eqid 2732 . . . . . . . . 9 ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) = ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃)
1514prmdiv 16720 . . . . . . . 8 ((𝑃 ∈ β„™ ∧ 𝑦 ∈ β„€ ∧ Β¬ 𝑃 βˆ₯ 𝑦) β†’ (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (1...(𝑃 βˆ’ 1)) ∧ 𝑃 βˆ₯ ((𝑦 Β· ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃)) βˆ’ 1)))
168, 10, 13, 15syl3anc 1371 . . . . . . 7 ((𝑃 ∈ β„™ ∧ 𝑦 ∈ (1...(𝑃 βˆ’ 1))) β†’ (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (1...(𝑃 βˆ’ 1)) ∧ 𝑃 βˆ₯ ((𝑦 Β· ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃)) βˆ’ 1)))
1716simpld 495 . . . . . 6 ((𝑃 ∈ β„™ ∧ 𝑦 ∈ (1...(𝑃 βˆ’ 1))) β†’ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (1...(𝑃 βˆ’ 1)))
1817ralrimiva 3146 . . . . 5 (𝑃 ∈ β„™ β†’ βˆ€π‘¦ ∈ (1...(𝑃 βˆ’ 1))((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (1...(𝑃 βˆ’ 1)))
19 ovex 7444 . . . . . . 7 (1...(𝑃 βˆ’ 1)) ∈ V
2019pwid 4624 . . . . . 6 (1...(𝑃 βˆ’ 1)) ∈ 𝒫 (1...(𝑃 βˆ’ 1))
21 eleq2 2822 . . . . . . . 8 (π‘₯ = (1...(𝑃 βˆ’ 1)) β†’ ((𝑃 βˆ’ 1) ∈ π‘₯ ↔ (𝑃 βˆ’ 1) ∈ (1...(𝑃 βˆ’ 1))))
22 eleq2 2822 . . . . . . . . 9 (π‘₯ = (1...(𝑃 βˆ’ 1)) β†’ (((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ π‘₯ ↔ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (1...(𝑃 βˆ’ 1))))
2322raleqbi1dv 3333 . . . . . . . 8 (π‘₯ = (1...(𝑃 βˆ’ 1)) β†’ (βˆ€π‘¦ ∈ π‘₯ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ π‘₯ ↔ βˆ€π‘¦ ∈ (1...(𝑃 βˆ’ 1))((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (1...(𝑃 βˆ’ 1))))
2421, 23anbi12d 631 . . . . . . 7 (π‘₯ = (1...(𝑃 βˆ’ 1)) β†’ (((𝑃 βˆ’ 1) ∈ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ π‘₯) ↔ ((𝑃 βˆ’ 1) ∈ (1...(𝑃 βˆ’ 1)) ∧ βˆ€π‘¦ ∈ (1...(𝑃 βˆ’ 1))((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (1...(𝑃 βˆ’ 1)))))
25 wilthlem.a . . . . . . 7 𝐴 = {π‘₯ ∈ 𝒫 (1...(𝑃 βˆ’ 1)) ∣ ((𝑃 βˆ’ 1) ∈ π‘₯ ∧ βˆ€π‘¦ ∈ π‘₯ ((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ π‘₯)}
2624, 25elrab2 3686 . . . . . 6 ((1...(𝑃 βˆ’ 1)) ∈ 𝐴 ↔ ((1...(𝑃 βˆ’ 1)) ∈ 𝒫 (1...(𝑃 βˆ’ 1)) ∧ ((𝑃 βˆ’ 1) ∈ (1...(𝑃 βˆ’ 1)) ∧ βˆ€π‘¦ ∈ (1...(𝑃 βˆ’ 1))((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (1...(𝑃 βˆ’ 1)))))
2720, 26mpbiran 707 . . . . 5 ((1...(𝑃 βˆ’ 1)) ∈ 𝐴 ↔ ((𝑃 βˆ’ 1) ∈ (1...(𝑃 βˆ’ 1)) ∧ βˆ€π‘¦ ∈ (1...(𝑃 βˆ’ 1))((𝑦↑(𝑃 βˆ’ 2)) mod 𝑃) ∈ (1...(𝑃 βˆ’ 1))))
287, 18, 27sylanbrc 583 . . . 4 (𝑃 ∈ β„™ β†’ (1...(𝑃 βˆ’ 1)) ∈ 𝐴)
29 fzfi 13939 . . . . 5 (1...(𝑃 βˆ’ 1)) ∈ Fin
30 eleq1 2821 . . . . . . . 8 (𝑠 = 𝑑 β†’ (𝑠 ∈ 𝐴 ↔ 𝑑 ∈ 𝐴))
31 reseq2 5976 . . . . . . . . . . 11 (𝑠 = 𝑑 β†’ ( I β†Ύ 𝑠) = ( I β†Ύ 𝑑))
3231oveq2d 7427 . . . . . . . . . 10 (𝑠 = 𝑑 β†’ (𝑇 Ξ£g ( I β†Ύ 𝑠)) = (𝑇 Ξ£g ( I β†Ύ 𝑑)))
3332oveq1d 7426 . . . . . . . . 9 (𝑠 = 𝑑 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = ((𝑇 Ξ£g ( I β†Ύ 𝑑)) mod 𝑃))
3433eqeq1d 2734 . . . . . . . 8 (𝑠 = 𝑑 β†’ (((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃) ↔ ((𝑇 Ξ£g ( I β†Ύ 𝑑)) mod 𝑃) = (-1 mod 𝑃)))
3530, 34imbi12d 344 . . . . . . 7 (𝑠 = 𝑑 β†’ ((𝑠 ∈ 𝐴 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ↔ (𝑑 ∈ 𝐴 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑑)) mod 𝑃) = (-1 mod 𝑃))))
3635imbi2d 340 . . . . . 6 (𝑠 = 𝑑 β†’ ((𝑃 ∈ β„™ β†’ (𝑠 ∈ 𝐴 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃))) ↔ (𝑃 ∈ β„™ β†’ (𝑑 ∈ 𝐴 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑑)) mod 𝑃) = (-1 mod 𝑃)))))
37 eleq1 2821 . . . . . . . 8 (𝑠 = (1...(𝑃 βˆ’ 1)) β†’ (𝑠 ∈ 𝐴 ↔ (1...(𝑃 βˆ’ 1)) ∈ 𝐴))
38 reseq2 5976 . . . . . . . . . . 11 (𝑠 = (1...(𝑃 βˆ’ 1)) β†’ ( I β†Ύ 𝑠) = ( I β†Ύ (1...(𝑃 βˆ’ 1))))
3938oveq2d 7427 . . . . . . . . . 10 (𝑠 = (1...(𝑃 βˆ’ 1)) β†’ (𝑇 Ξ£g ( I β†Ύ 𝑠)) = (𝑇 Ξ£g ( I β†Ύ (1...(𝑃 βˆ’ 1)))))
4039oveq1d 7426 . . . . . . . . 9 (𝑠 = (1...(𝑃 βˆ’ 1)) β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = ((𝑇 Ξ£g ( I β†Ύ (1...(𝑃 βˆ’ 1)))) mod 𝑃))
4140eqeq1d 2734 . . . . . . . 8 (𝑠 = (1...(𝑃 βˆ’ 1)) β†’ (((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃) ↔ ((𝑇 Ξ£g ( I β†Ύ (1...(𝑃 βˆ’ 1)))) mod 𝑃) = (-1 mod 𝑃)))
4237, 41imbi12d 344 . . . . . . 7 (𝑠 = (1...(𝑃 βˆ’ 1)) β†’ ((𝑠 ∈ 𝐴 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ↔ ((1...(𝑃 βˆ’ 1)) ∈ 𝐴 β†’ ((𝑇 Ξ£g ( I β†Ύ (1...(𝑃 βˆ’ 1)))) mod 𝑃) = (-1 mod 𝑃))))
4342imbi2d 340 . . . . . 6 (𝑠 = (1...(𝑃 βˆ’ 1)) β†’ ((𝑃 ∈ β„™ β†’ (𝑠 ∈ 𝐴 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃))) ↔ (𝑃 ∈ β„™ β†’ ((1...(𝑃 βˆ’ 1)) ∈ 𝐴 β†’ ((𝑇 Ξ£g ( I β†Ύ (1...(𝑃 βˆ’ 1)))) mod 𝑃) = (-1 mod 𝑃)))))
44 bi2.04 388 . . . . . . . . . . 11 ((𝑠 ⊊ 𝑑 β†’ (𝑃 ∈ β„™ β†’ (𝑠 ∈ 𝐴 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))) ↔ (𝑃 ∈ β„™ β†’ (𝑠 ⊊ 𝑑 β†’ (𝑠 ∈ 𝐴 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))))
45 pm2.27 42 . . . . . . . . . . . 12 (𝑃 ∈ β„™ β†’ ((𝑃 ∈ β„™ β†’ (𝑠 ⊊ 𝑑 β†’ (𝑠 ∈ 𝐴 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))) β†’ (𝑠 ⊊ 𝑑 β†’ (𝑠 ∈ 𝐴 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))))
4645com34 91 . . . . . . . . . . 11 (𝑃 ∈ β„™ β†’ ((𝑃 ∈ β„™ β†’ (𝑠 ⊊ 𝑑 β†’ (𝑠 ∈ 𝐴 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))) β†’ (𝑠 ∈ 𝐴 β†’ (𝑠 ⊊ 𝑑 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))))
4744, 46biimtrid 241 . . . . . . . . . 10 (𝑃 ∈ β„™ β†’ ((𝑠 ⊊ 𝑑 β†’ (𝑃 ∈ β„™ β†’ (𝑠 ∈ 𝐴 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))) β†’ (𝑠 ∈ 𝐴 β†’ (𝑠 ⊊ 𝑑 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))))
4847alimdv 1919 . . . . . . . . 9 (𝑃 ∈ β„™ β†’ (βˆ€π‘ (𝑠 ⊊ 𝑑 β†’ (𝑃 ∈ β„™ β†’ (𝑠 ∈ 𝐴 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))) β†’ βˆ€π‘ (𝑠 ∈ 𝐴 β†’ (𝑠 ⊊ 𝑑 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))))
49 df-ral 3062 . . . . . . . . 9 (βˆ€π‘  ∈ 𝐴 (𝑠 ⊊ 𝑑 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ↔ βˆ€π‘ (𝑠 ∈ 𝐴 β†’ (𝑠 ⊊ 𝑑 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃))))
5048, 49imbitrrdi 251 . . . . . . . 8 (𝑃 ∈ β„™ β†’ (βˆ€π‘ (𝑠 ⊊ 𝑑 β†’ (𝑃 ∈ β„™ β†’ (𝑠 ∈ 𝐴 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))) β†’ βˆ€π‘  ∈ 𝐴 (𝑠 ⊊ 𝑑 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃))))
51 wilthlem.t . . . . . . . . . 10 𝑇 = (mulGrpβ€˜β„‚fld)
52 simp1 1136 . . . . . . . . . 10 ((𝑃 ∈ β„™ ∧ βˆ€π‘  ∈ 𝐴 (𝑠 ⊊ 𝑑 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ∧ 𝑑 ∈ 𝐴) β†’ 𝑃 ∈ β„™)
53 simp3 1138 . . . . . . . . . 10 ((𝑃 ∈ β„™ ∧ βˆ€π‘  ∈ 𝐴 (𝑠 ⊊ 𝑑 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ∧ 𝑑 ∈ 𝐴) β†’ 𝑑 ∈ 𝐴)
54 simp2 1137 . . . . . . . . . 10 ((𝑃 ∈ β„™ ∧ βˆ€π‘  ∈ 𝐴 (𝑠 ⊊ 𝑑 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ∧ 𝑑 ∈ 𝐴) β†’ βˆ€π‘  ∈ 𝐴 (𝑠 ⊊ 𝑑 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))
5551, 25, 52, 53, 54wilthlem2 26580 . . . . . . . . 9 ((𝑃 ∈ β„™ ∧ βˆ€π‘  ∈ 𝐴 (𝑠 ⊊ 𝑑 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ∧ 𝑑 ∈ 𝐴) β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑑)) mod 𝑃) = (-1 mod 𝑃))
56553exp 1119 . . . . . . . 8 (𝑃 ∈ β„™ β†’ (βˆ€π‘  ∈ 𝐴 (𝑠 ⊊ 𝑑 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) β†’ (𝑑 ∈ 𝐴 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑑)) mod 𝑃) = (-1 mod 𝑃))))
5750, 56syldc 48 . . . . . . 7 (βˆ€π‘ (𝑠 ⊊ 𝑑 β†’ (𝑃 ∈ β„™ β†’ (𝑠 ∈ 𝐴 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))) β†’ (𝑃 ∈ β„™ β†’ (𝑑 ∈ 𝐴 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑑)) mod 𝑃) = (-1 mod 𝑃))))
5857a1i 11 . . . . . 6 (𝑑 ∈ Fin β†’ (βˆ€π‘ (𝑠 ⊊ 𝑑 β†’ (𝑃 ∈ β„™ β†’ (𝑠 ∈ 𝐴 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))) β†’ (𝑃 ∈ β„™ β†’ (𝑑 ∈ 𝐴 β†’ ((𝑇 Ξ£g ( I β†Ύ 𝑑)) mod 𝑃) = (-1 mod 𝑃)))))
5936, 43, 58findcard3 9287 . . . . 5 ((1...(𝑃 βˆ’ 1)) ∈ Fin β†’ (𝑃 ∈ β„™ β†’ ((1...(𝑃 βˆ’ 1)) ∈ 𝐴 β†’ ((𝑇 Ξ£g ( I β†Ύ (1...(𝑃 βˆ’ 1)))) mod 𝑃) = (-1 mod 𝑃))))
6029, 59ax-mp 5 . . . 4 (𝑃 ∈ β„™ β†’ ((1...(𝑃 βˆ’ 1)) ∈ 𝐴 β†’ ((𝑇 Ξ£g ( I β†Ύ (1...(𝑃 βˆ’ 1)))) mod 𝑃) = (-1 mod 𝑃)))
6128, 60mpd 15 . . 3 (𝑃 ∈ β„™ β†’ ((𝑇 Ξ£g ( I β†Ύ (1...(𝑃 βˆ’ 1)))) mod 𝑃) = (-1 mod 𝑃))
62 cnfld1 20976 . . . . . 6 1 = (1rβ€˜β„‚fld)
6351, 62ringidval 20008 . . . . 5 1 = (0gβ€˜π‘‡)
64 cncrng 20972 . . . . . 6 β„‚fld ∈ CRing
6551crngmgp 20066 . . . . . 6 (β„‚fld ∈ CRing β†’ 𝑇 ∈ CMnd)
6664, 65mp1i 13 . . . . 5 (𝑃 ∈ β„™ β†’ 𝑇 ∈ CMnd)
6729a1i 11 . . . . 5 (𝑃 ∈ β„™ β†’ (1...(𝑃 βˆ’ 1)) ∈ Fin)
68 zsubrg 21004 . . . . . 6 β„€ ∈ (SubRingβ€˜β„‚fld)
6951subrgsubm 20336 . . . . . 6 (β„€ ∈ (SubRingβ€˜β„‚fld) β†’ β„€ ∈ (SubMndβ€˜π‘‡))
7068, 69mp1i 13 . . . . 5 (𝑃 ∈ β„™ β†’ β„€ ∈ (SubMndβ€˜π‘‡))
71 f1oi 6871 . . . . . . . 8 ( I β†Ύ (1...(𝑃 βˆ’ 1))):(1...(𝑃 βˆ’ 1))–1-1-ontoβ†’(1...(𝑃 βˆ’ 1))
72 f1of 6833 . . . . . . . 8 (( I β†Ύ (1...(𝑃 βˆ’ 1))):(1...(𝑃 βˆ’ 1))–1-1-ontoβ†’(1...(𝑃 βˆ’ 1)) β†’ ( I β†Ύ (1...(𝑃 βˆ’ 1))):(1...(𝑃 βˆ’ 1))⟢(1...(𝑃 βˆ’ 1)))
7371, 72ax-mp 5 . . . . . . 7 ( I β†Ύ (1...(𝑃 βˆ’ 1))):(1...(𝑃 βˆ’ 1))⟢(1...(𝑃 βˆ’ 1))
74 fzssz 13505 . . . . . . 7 (1...(𝑃 βˆ’ 1)) βŠ† β„€
75 fss 6734 . . . . . . 7 ((( I β†Ύ (1...(𝑃 βˆ’ 1))):(1...(𝑃 βˆ’ 1))⟢(1...(𝑃 βˆ’ 1)) ∧ (1...(𝑃 βˆ’ 1)) βŠ† β„€) β†’ ( I β†Ύ (1...(𝑃 βˆ’ 1))):(1...(𝑃 βˆ’ 1))βŸΆβ„€)
7673, 74, 75mp2an 690 . . . . . 6 ( I β†Ύ (1...(𝑃 βˆ’ 1))):(1...(𝑃 βˆ’ 1))βŸΆβ„€
7776a1i 11 . . . . 5 (𝑃 ∈ β„™ β†’ ( I β†Ύ (1...(𝑃 βˆ’ 1))):(1...(𝑃 βˆ’ 1))βŸΆβ„€)
78 1ex 11212 . . . . . . 7 1 ∈ V
7978a1i 11 . . . . . 6 (𝑃 ∈ β„™ β†’ 1 ∈ V)
8077, 67, 79fdmfifsupp 9375 . . . . 5 (𝑃 ∈ β„™ β†’ ( I β†Ύ (1...(𝑃 βˆ’ 1))) finSupp 1)
8163, 66, 67, 70, 77, 80gsumsubmcl 19789 . . . 4 (𝑃 ∈ β„™ β†’ (𝑇 Ξ£g ( I β†Ύ (1...(𝑃 βˆ’ 1)))) ∈ β„€)
82 1z 12594 . . . . 5 1 ∈ β„€
83 znegcl 12599 . . . . 5 (1 ∈ β„€ β†’ -1 ∈ β„€)
8482, 83mp1i 13 . . . 4 (𝑃 ∈ β„™ β†’ -1 ∈ β„€)
85 moddvds 16210 . . . 4 ((𝑃 ∈ β„• ∧ (𝑇 Ξ£g ( I β†Ύ (1...(𝑃 βˆ’ 1)))) ∈ β„€ ∧ -1 ∈ β„€) β†’ (((𝑇 Ξ£g ( I β†Ύ (1...(𝑃 βˆ’ 1)))) mod 𝑃) = (-1 mod 𝑃) ↔ 𝑃 βˆ₯ ((𝑇 Ξ£g ( I β†Ύ (1...(𝑃 βˆ’ 1)))) βˆ’ -1)))
8611, 81, 84, 85syl3anc 1371 . . 3 (𝑃 ∈ β„™ β†’ (((𝑇 Ξ£g ( I β†Ύ (1...(𝑃 βˆ’ 1)))) mod 𝑃) = (-1 mod 𝑃) ↔ 𝑃 βˆ₯ ((𝑇 Ξ£g ( I β†Ύ (1...(𝑃 βˆ’ 1)))) βˆ’ -1)))
8761, 86mpbid 231 . 2 (𝑃 ∈ β„™ β†’ 𝑃 βˆ₯ ((𝑇 Ξ£g ( I β†Ύ (1...(𝑃 βˆ’ 1)))) βˆ’ -1))
88 fcoi1 6765 . . . . . . . . . 10 (( I β†Ύ (1...(𝑃 βˆ’ 1))):(1...(𝑃 βˆ’ 1))⟢(1...(𝑃 βˆ’ 1)) β†’ (( I β†Ύ (1...(𝑃 βˆ’ 1))) ∘ ( I β†Ύ (1...(𝑃 βˆ’ 1)))) = ( I β†Ύ (1...(𝑃 βˆ’ 1))))
8973, 88ax-mp 5 . . . . . . . . 9 (( I β†Ύ (1...(𝑃 βˆ’ 1))) ∘ ( I β†Ύ (1...(𝑃 βˆ’ 1)))) = ( I β†Ύ (1...(𝑃 βˆ’ 1)))
9089fveq1i 6892 . . . . . . . 8 ((( I β†Ύ (1...(𝑃 βˆ’ 1))) ∘ ( I β†Ύ (1...(𝑃 βˆ’ 1))))β€˜π‘˜) = (( I β†Ύ (1...(𝑃 βˆ’ 1)))β€˜π‘˜)
91 fvres 6910 . . . . . . . 8 (π‘˜ ∈ (1...(𝑃 βˆ’ 1)) β†’ (( I β†Ύ (1...(𝑃 βˆ’ 1)))β€˜π‘˜) = ( I β€˜π‘˜))
9290, 91eqtrid 2784 . . . . . . 7 (π‘˜ ∈ (1...(𝑃 βˆ’ 1)) β†’ ((( I β†Ύ (1...(𝑃 βˆ’ 1))) ∘ ( I β†Ύ (1...(𝑃 βˆ’ 1))))β€˜π‘˜) = ( I β€˜π‘˜))
9392adantl 482 . . . . . 6 ((𝑃 ∈ β„™ ∧ π‘˜ ∈ (1...(𝑃 βˆ’ 1))) β†’ ((( I β†Ύ (1...(𝑃 βˆ’ 1))) ∘ ( I β†Ύ (1...(𝑃 βˆ’ 1))))β€˜π‘˜) = ( I β€˜π‘˜))
945, 93seqfveq 13994 . . . . 5 (𝑃 ∈ β„™ β†’ (seq1( Β· , (( I β†Ύ (1...(𝑃 βˆ’ 1))) ∘ ( I β†Ύ (1...(𝑃 βˆ’ 1)))))β€˜(𝑃 βˆ’ 1)) = (seq1( Β· , I )β€˜(𝑃 βˆ’ 1)))
95 cnfldbas 20954 . . . . . . 7 β„‚ = (Baseβ€˜β„‚fld)
9651, 95mgpbas 19995 . . . . . 6 β„‚ = (Baseβ€˜π‘‡)
97 cnfldmul 20956 . . . . . . 7 Β· = (.rβ€˜β„‚fld)
9851, 97mgpplusg 19993 . . . . . 6 Β· = (+gβ€˜π‘‡)
99 eqid 2732 . . . . . 6 (Cntzβ€˜π‘‡) = (Cntzβ€˜π‘‡)
100 cnring 20973 . . . . . . 7 β„‚fld ∈ Ring
10151ringmgp 20064 . . . . . . 7 (β„‚fld ∈ Ring β†’ 𝑇 ∈ Mnd)
102100, 101mp1i 13 . . . . . 6 (𝑃 ∈ β„™ β†’ 𝑇 ∈ Mnd)
103 zsscn 12568 . . . . . . . 8 β„€ βŠ† β„‚
104 fss 6734 . . . . . . . 8 ((( I β†Ύ (1...(𝑃 βˆ’ 1))):(1...(𝑃 βˆ’ 1))βŸΆβ„€ ∧ β„€ βŠ† β„‚) β†’ ( I β†Ύ (1...(𝑃 βˆ’ 1))):(1...(𝑃 βˆ’ 1))βŸΆβ„‚)
10576, 103, 104mp2an 690 . . . . . . 7 ( I β†Ύ (1...(𝑃 βˆ’ 1))):(1...(𝑃 βˆ’ 1))βŸΆβ„‚
106105a1i 11 . . . . . 6 (𝑃 ∈ β„™ β†’ ( I β†Ύ (1...(𝑃 βˆ’ 1))):(1...(𝑃 βˆ’ 1))βŸΆβ„‚)
10796, 99, 66, 106cntzcmnf 19715 . . . . . 6 (𝑃 ∈ β„™ β†’ ran ( I β†Ύ (1...(𝑃 βˆ’ 1))) βŠ† ((Cntzβ€˜π‘‡)β€˜ran ( I β†Ύ (1...(𝑃 βˆ’ 1)))))
108 f1of1 6832 . . . . . . 7 (( I β†Ύ (1...(𝑃 βˆ’ 1))):(1...(𝑃 βˆ’ 1))–1-1-ontoβ†’(1...(𝑃 βˆ’ 1)) β†’ ( I β†Ύ (1...(𝑃 βˆ’ 1))):(1...(𝑃 βˆ’ 1))–1-1β†’(1...(𝑃 βˆ’ 1)))
10971, 108mp1i 13 . . . . . 6 (𝑃 ∈ β„™ β†’ ( I β†Ύ (1...(𝑃 βˆ’ 1))):(1...(𝑃 βˆ’ 1))–1-1β†’(1...(𝑃 βˆ’ 1)))
110 suppssdm 8164 . . . . . . . . 9 (( I β†Ύ (1...(𝑃 βˆ’ 1))) supp 1) βŠ† dom ( I β†Ύ (1...(𝑃 βˆ’ 1)))
111 dmresi 6051 . . . . . . . . 9 dom ( I β†Ύ (1...(𝑃 βˆ’ 1))) = (1...(𝑃 βˆ’ 1))
112110, 111sseqtri 4018 . . . . . . . 8 (( I β†Ύ (1...(𝑃 βˆ’ 1))) supp 1) βŠ† (1...(𝑃 βˆ’ 1))
113 rnresi 6074 . . . . . . . 8 ran ( I β†Ύ (1...(𝑃 βˆ’ 1))) = (1...(𝑃 βˆ’ 1))
114112, 113sseqtrri 4019 . . . . . . 7 (( I β†Ύ (1...(𝑃 βˆ’ 1))) supp 1) βŠ† ran ( I β†Ύ (1...(𝑃 βˆ’ 1)))
115114a1i 11 . . . . . 6 (𝑃 ∈ β„™ β†’ (( I β†Ύ (1...(𝑃 βˆ’ 1))) supp 1) βŠ† ran ( I β†Ύ (1...(𝑃 βˆ’ 1))))
116 eqid 2732 . . . . . 6 ((( I β†Ύ (1...(𝑃 βˆ’ 1))) ∘ ( I β†Ύ (1...(𝑃 βˆ’ 1)))) supp 1) = ((( I β†Ύ (1...(𝑃 βˆ’ 1))) ∘ ( I β†Ύ (1...(𝑃 βˆ’ 1)))) supp 1)
11796, 63, 98, 99, 102, 67, 106, 107, 3, 109, 115, 116gsumval3 19777 . . . . 5 (𝑃 ∈ β„™ β†’ (𝑇 Ξ£g ( I β†Ύ (1...(𝑃 βˆ’ 1)))) = (seq1( Β· , (( I β†Ύ (1...(𝑃 βˆ’ 1))) ∘ ( I β†Ύ (1...(𝑃 βˆ’ 1)))))β€˜(𝑃 βˆ’ 1)))
118 facnn 14237 . . . . . 6 ((𝑃 βˆ’ 1) ∈ β„• β†’ (!β€˜(𝑃 βˆ’ 1)) = (seq1( Β· , I )β€˜(𝑃 βˆ’ 1)))
1193, 118syl 17 . . . . 5 (𝑃 ∈ β„™ β†’ (!β€˜(𝑃 βˆ’ 1)) = (seq1( Β· , I )β€˜(𝑃 βˆ’ 1)))
12094, 117, 1193eqtr4d 2782 . . . 4 (𝑃 ∈ β„™ β†’ (𝑇 Ξ£g ( I β†Ύ (1...(𝑃 βˆ’ 1)))) = (!β€˜(𝑃 βˆ’ 1)))
121120oveq1d 7426 . . 3 (𝑃 ∈ β„™ β†’ ((𝑇 Ξ£g ( I β†Ύ (1...(𝑃 βˆ’ 1)))) βˆ’ -1) = ((!β€˜(𝑃 βˆ’ 1)) βˆ’ -1))
122 nnm1nn0 12515 . . . . . . 7 (𝑃 ∈ β„• β†’ (𝑃 βˆ’ 1) ∈ β„•0)
12311, 122syl 17 . . . . . 6 (𝑃 ∈ β„™ β†’ (𝑃 βˆ’ 1) ∈ β„•0)
124123faccld 14246 . . . . 5 (𝑃 ∈ β„™ β†’ (!β€˜(𝑃 βˆ’ 1)) ∈ β„•)
125124nncnd 12230 . . . 4 (𝑃 ∈ β„™ β†’ (!β€˜(𝑃 βˆ’ 1)) ∈ β„‚)
126 ax-1cn 11170 . . . 4 1 ∈ β„‚
127 subneg 11511 . . . 4 (((!β€˜(𝑃 βˆ’ 1)) ∈ β„‚ ∧ 1 ∈ β„‚) β†’ ((!β€˜(𝑃 βˆ’ 1)) βˆ’ -1) = ((!β€˜(𝑃 βˆ’ 1)) + 1))
128125, 126, 127sylancl 586 . . 3 (𝑃 ∈ β„™ β†’ ((!β€˜(𝑃 βˆ’ 1)) βˆ’ -1) = ((!β€˜(𝑃 βˆ’ 1)) + 1))
129121, 128eqtrd 2772 . 2 (𝑃 ∈ β„™ β†’ ((𝑇 Ξ£g ( I β†Ύ (1...(𝑃 βˆ’ 1)))) βˆ’ -1) = ((!β€˜(𝑃 βˆ’ 1)) + 1))
13087, 129breqtrd 5174 1 (𝑃 ∈ β„™ β†’ 𝑃 βˆ₯ ((!β€˜(𝑃 βˆ’ 1)) + 1))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087  βˆ€wal 1539   = wceq 1541   ∈ wcel 2106  βˆ€wral 3061  {crab 3432  Vcvv 3474   βŠ† wss 3948   ⊊ wpss 3949  π’« cpw 4602   class class class wbr 5148   I cid 5573  dom cdm 5676  ran crn 5677   β†Ύ cres 5678   ∘ ccom 5680  βŸΆwf 6539  β€“1-1β†’wf1 6540  β€“1-1-ontoβ†’wf1o 6542  β€˜cfv 6543  (class class class)co 7411   supp csupp 8148  Fincfn 8941  β„‚cc 11110  1c1 11113   + caddc 11115   Β· cmul 11117   βˆ’ cmin 11446  -cneg 11447  β„•cn 12214  2c2 12269  β„•0cn0 12474  β„€cz 12560  β„€β‰₯cuz 12824  ...cfz 13486   mod cmo 13836  seqcseq 13968  β†‘cexp 14029  !cfa 14235   βˆ₯ cdvds 16199  β„™cprime 16610   Ξ£g cgsu 17388  Mndcmnd 18627  SubMndcsubmnd 18672  Cntzccntz 19181  CMndccmn 19650  mulGrpcmgp 19989  Ringcrg 20058  CRingccrg 20059  SubRingcsubrg 20319  β„‚fldccnfld 20950
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 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190  ax-addf 11191  ax-mulf 11192
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 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7672  df-om 7858  df-1st 7977  df-2nd 7978  df-supp 8149  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-2o 8469  df-oadd 8472  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-sup 9439  df-inf 9440  df-oi 9507  df-dju 9898  df-card 9936  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-div 11874  df-nn 12215  df-2 12277  df-3 12278  df-4 12279  df-5 12280  df-6 12281  df-7 12282  df-8 12283  df-9 12284  df-n0 12475  df-xnn0 12547  df-z 12561  df-dec 12680  df-uz 12825  df-rp 12977  df-fz 13487  df-fzo 13630  df-fl 13759  df-mod 13837  df-seq 13969  df-exp 14030  df-fac 14236  df-hash 14293  df-cj 15048  df-re 15049  df-im 15050  df-sqrt 15184  df-abs 15185  df-dvds 16200  df-gcd 16438  df-prm 16611  df-phi 16701  df-struct 17082  df-sets 17099  df-slot 17117  df-ndx 17129  df-base 17147  df-ress 17176  df-plusg 17212  df-mulr 17213  df-starv 17214  df-tset 17218  df-ple 17219  df-ds 17221  df-unif 17222  df-0g 17389  df-gsum 17390  df-mre 17532  df-mrc 17533  df-acs 17535  df-mgm 18563  df-sgrp 18612  df-mnd 18628  df-submnd 18674  df-grp 18824  df-minusg 18825  df-mulg 18953  df-subg 19005  df-cntz 19183  df-cmn 19652  df-mgp 19990  df-ur 20007  df-ring 20060  df-cring 20061  df-subrg 20321  df-cnfld 20951
This theorem is referenced by:  wilth  26582
  Copyright terms: Public domain W3C validator