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

Theorem wilthlem3 27022
Description: Lemma for wilth 27023. Here we round out the argument of wilthlem2 27021 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 16674 . . . . . . . 8 (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ‘2))
2 uz2m1nn 12945 . . . . . . . 8 (𝑃 ∈ (ℤ‘2) → (𝑃 − 1) ∈ ℕ)
31, 2syl 17 . . . . . . 7 (𝑃 ∈ ℙ → (𝑃 − 1) ∈ ℕ)
4 nnuz 12903 . . . . . . 7 ℕ = (ℤ‘1)
53, 4eleqtrdi 2839 . . . . . 6 (𝑃 ∈ ℙ → (𝑃 − 1) ∈ (ℤ‘1))
6 eluzfz2 13549 . . . . . 6 ((𝑃 − 1) ∈ (ℤ‘1) → (𝑃 − 1) ∈ (1...(𝑃 − 1)))
75, 6syl 17 . . . . 5 (𝑃 ∈ ℙ → (𝑃 − 1) ∈ (1...(𝑃 − 1)))
8 simpl 481 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → 𝑃 ∈ ℙ)
9 elfzelz 13541 . . . . . . . . 9 (𝑦 ∈ (1...(𝑃 − 1)) → 𝑦 ∈ ℤ)
109adantl 480 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → 𝑦 ∈ ℤ)
11 prmnn 16652 . . . . . . . . 9 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
12 fzm1ndvds 16306 . . . . . . . . 9 ((𝑃 ∈ ℕ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → ¬ 𝑃𝑦)
1311, 12sylan 578 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → ¬ 𝑃𝑦)
14 eqid 2728 . . . . . . . . 9 ((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑦↑(𝑃 − 2)) mod 𝑃)
1514prmdiv 16761 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ 𝑦 ∈ ℤ ∧ ¬ 𝑃𝑦) → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑦 · ((𝑦↑(𝑃 − 2)) mod 𝑃)) − 1)))
168, 10, 13, 15syl3anc 1368 . . . . . . 7 ((𝑃 ∈ ℙ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑦 · ((𝑦↑(𝑃 − 2)) mod 𝑃)) − 1)))
1716simpld 493 . . . . . 6 ((𝑃 ∈ ℙ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)))
1817ralrimiva 3143 . . . . 5 (𝑃 ∈ ℙ → ∀𝑦 ∈ (1...(𝑃 − 1))((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)))
19 ovex 7459 . . . . . . 7 (1...(𝑃 − 1)) ∈ V
2019pwid 4628 . . . . . 6 (1...(𝑃 − 1)) ∈ 𝒫 (1...(𝑃 − 1))
21 eleq2 2818 . . . . . . . 8 (𝑥 = (1...(𝑃 − 1)) → ((𝑃 − 1) ∈ 𝑥 ↔ (𝑃 − 1) ∈ (1...(𝑃 − 1))))
22 eleq2 2818 . . . . . . . . 9 (𝑥 = (1...(𝑃 − 1)) → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥 ↔ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1))))
2322raleqbi1dv 3331 . . . . . . . 8 (𝑥 = (1...(𝑃 − 1)) → (∀𝑦𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥 ↔ ∀𝑦 ∈ (1...(𝑃 − 1))((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1))))
2421, 23anbi12d 630 . . . . . . 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 3687 . . . . . 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 581 . . . 4 (𝑃 ∈ ℙ → (1...(𝑃 − 1)) ∈ 𝐴)
29 fzfi 13977 . . . . 5 (1...(𝑃 − 1)) ∈ Fin
30 eleq1 2817 . . . . . . . 8 (𝑠 = 𝑡 → (𝑠𝐴𝑡𝐴))
31 reseq2 5984 . . . . . . . . . . 11 (𝑠 = 𝑡 → ( I ↾ 𝑠) = ( I ↾ 𝑡))
3231oveq2d 7442 . . . . . . . . . 10 (𝑠 = 𝑡 → (𝑇 Σg ( I ↾ 𝑠)) = (𝑇 Σg ( I ↾ 𝑡)))
3332oveq1d 7441 . . . . . . . . 9 (𝑠 = 𝑡 → ((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = ((𝑇 Σg ( I ↾ 𝑡)) mod 𝑃))
3433eqeq1d 2730 . . . . . . . 8 (𝑠 = 𝑡 → (((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃) ↔ ((𝑇 Σg ( I ↾ 𝑡)) mod 𝑃) = (-1 mod 𝑃)))
3530, 34imbi12d 343 . . . . . . 7 (𝑠 = 𝑡 → ((𝑠𝐴 → ((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ↔ (𝑡𝐴 → ((𝑇 Σg ( I ↾ 𝑡)) mod 𝑃) = (-1 mod 𝑃))))
3635imbi2d 339 . . . . . 6 (𝑠 = 𝑡 → ((𝑃 ∈ ℙ → (𝑠𝐴 → ((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃))) ↔ (𝑃 ∈ ℙ → (𝑡𝐴 → ((𝑇 Σg ( I ↾ 𝑡)) mod 𝑃) = (-1 mod 𝑃)))))
37 eleq1 2817 . . . . . . . 8 (𝑠 = (1...(𝑃 − 1)) → (𝑠𝐴 ↔ (1...(𝑃 − 1)) ∈ 𝐴))
38 reseq2 5984 . . . . . . . . . . 11 (𝑠 = (1...(𝑃 − 1)) → ( I ↾ 𝑠) = ( I ↾ (1...(𝑃 − 1))))
3938oveq2d 7442 . . . . . . . . . 10 (𝑠 = (1...(𝑃 − 1)) → (𝑇 Σg ( I ↾ 𝑠)) = (𝑇 Σg ( I ↾ (1...(𝑃 − 1)))))
4039oveq1d 7441 . . . . . . . . 9 (𝑠 = (1...(𝑃 − 1)) → ((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = ((𝑇 Σg ( I ↾ (1...(𝑃 − 1)))) mod 𝑃))
4140eqeq1d 2730 . . . . . . . 8 (𝑠 = (1...(𝑃 − 1)) → (((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃) ↔ ((𝑇 Σg ( I ↾ (1...(𝑃 − 1)))) mod 𝑃) = (-1 mod 𝑃)))
4237, 41imbi12d 343 . . . . . . 7 (𝑠 = (1...(𝑃 − 1)) → ((𝑠𝐴 → ((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ↔ ((1...(𝑃 − 1)) ∈ 𝐴 → ((𝑇 Σg ( I ↾ (1...(𝑃 − 1)))) mod 𝑃) = (-1 mod 𝑃))))
4342imbi2d 339 . . . . . 6 (𝑠 = (1...(𝑃 − 1)) → ((𝑃 ∈ ℙ → (𝑠𝐴 → ((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃))) ↔ (𝑃 ∈ ℙ → ((1...(𝑃 − 1)) ∈ 𝐴 → ((𝑇 Σg ( I ↾ (1...(𝑃 − 1)))) mod 𝑃) = (-1 mod 𝑃)))))
44 bi2.04 386 . . . . . . . . . . 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 1911 . . . . . . . . 9 (𝑃 ∈ ℙ → (∀𝑠(𝑠𝑡 → (𝑃 ∈ ℙ → (𝑠𝐴 → ((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))) → ∀𝑠(𝑠𝐴 → (𝑠𝑡 → ((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))))
49 df-ral 3059 . . . . . . . . 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 1133 . . . . . . . . . 10 ((𝑃 ∈ ℙ ∧ ∀𝑠𝐴 (𝑠𝑡 → ((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ∧ 𝑡𝐴) → 𝑃 ∈ ℙ)
53 simp3 1135 . . . . . . . . . 10 ((𝑃 ∈ ℙ ∧ ∀𝑠𝐴 (𝑠𝑡 → ((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ∧ 𝑡𝐴) → 𝑡𝐴)
54 simp2 1134 . . . . . . . . . 10 ((𝑃 ∈ ℙ ∧ ∀𝑠𝐴 (𝑠𝑡 → ((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ∧ 𝑡𝐴) → ∀𝑠𝐴 (𝑠𝑡 → ((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))
5551, 25, 52, 53, 54wilthlem2 27021 . . . . . . . . 9 ((𝑃 ∈ ℙ ∧ ∀𝑠𝐴 (𝑠𝑡 → ((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ∧ 𝑡𝐴) → ((𝑇 Σg ( I ↾ 𝑡)) mod 𝑃) = (-1 mod 𝑃))
56553exp 1116 . . . . . . . 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 9316 . . . . 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 21328 . . . . . 6 1 = (1r‘ℂfld)
6351, 62ringidval 20130 . . . . 5 1 = (0g𝑇)
64 cncrng 21323 . . . . . 6 fld ∈ CRing
6551crngmgp 20188 . . . . . 6 (ℂfld ∈ CRing → 𝑇 ∈ CMnd)
6664, 65mp1i 13 . . . . 5 (𝑃 ∈ ℙ → 𝑇 ∈ CMnd)
6729a1i 11 . . . . 5 (𝑃 ∈ ℙ → (1...(𝑃 − 1)) ∈ Fin)
68 zsubrg 21360 . . . . . 6 ℤ ∈ (SubRing‘ℂfld)
6951subrgsubm 20531 . . . . . 6 (ℤ ∈ (SubRing‘ℂfld) → ℤ ∈ (SubMnd‘𝑇))
7068, 69mp1i 13 . . . . 5 (𝑃 ∈ ℙ → ℤ ∈ (SubMnd‘𝑇))
71 f1oi 6882 . . . . . . . 8 ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))–1-1-onto→(1...(𝑃 − 1))
72 f1of 6844 . . . . . . . 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 13543 . . . . . . 7 (1...(𝑃 − 1)) ⊆ ℤ
75 fss 6744 . . . . . . 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 11248 . . . . . . 7 1 ∈ V
7978a1i 11 . . . . . 6 (𝑃 ∈ ℙ → 1 ∈ V)
8077, 67, 79fdmfifsupp 9406 . . . . 5 (𝑃 ∈ ℙ → ( I ↾ (1...(𝑃 − 1))) finSupp 1)
8163, 66, 67, 70, 77, 80gsumsubmcl 19881 . . . 4 (𝑃 ∈ ℙ → (𝑇 Σg ( I ↾ (1...(𝑃 − 1)))) ∈ ℤ)
82 1z 12630 . . . . 5 1 ∈ ℤ
83 znegcl 12635 . . . . 5 (1 ∈ ℤ → -1 ∈ ℤ)
8482, 83mp1i 13 . . . 4 (𝑃 ∈ ℙ → -1 ∈ ℤ)
85 moddvds 16249 . . . 4 ((𝑃 ∈ ℕ ∧ (𝑇 Σg ( I ↾ (1...(𝑃 − 1)))) ∈ ℤ ∧ -1 ∈ ℤ) → (((𝑇 Σg ( I ↾ (1...(𝑃 − 1)))) mod 𝑃) = (-1 mod 𝑃) ↔ 𝑃 ∥ ((𝑇 Σg ( I ↾ (1...(𝑃 − 1)))) − -1)))
8611, 81, 84, 85syl3anc 1368 . . 3 (𝑃 ∈ ℙ → (((𝑇 Σg ( I ↾ (1...(𝑃 − 1)))) mod 𝑃) = (-1 mod 𝑃) ↔ 𝑃 ∥ ((𝑇 Σg ( I ↾ (1...(𝑃 − 1)))) − -1)))
8761, 86mpbid 231 . 2 (𝑃 ∈ ℙ → 𝑃 ∥ ((𝑇 Σg ( I ↾ (1...(𝑃 − 1)))) − -1))
88 fcoi1 6776 . . . . . . . . . 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 6903 . . . . . . . 8 ((( I ↾ (1...(𝑃 − 1))) ∘ ( I ↾ (1...(𝑃 − 1))))‘𝑘) = (( I ↾ (1...(𝑃 − 1)))‘𝑘)
91 fvres 6921 . . . . . . . 8 (𝑘 ∈ (1...(𝑃 − 1)) → (( I ↾ (1...(𝑃 − 1)))‘𝑘) = ( I ‘𝑘))
9290, 91eqtrid 2780 . . . . . . 7 (𝑘 ∈ (1...(𝑃 − 1)) → ((( I ↾ (1...(𝑃 − 1))) ∘ ( I ↾ (1...(𝑃 − 1))))‘𝑘) = ( I ‘𝑘))
9392adantl 480 . . . . . 6 ((𝑃 ∈ ℙ ∧ 𝑘 ∈ (1...(𝑃 − 1))) → ((( I ↾ (1...(𝑃 − 1))) ∘ ( I ↾ (1...(𝑃 − 1))))‘𝑘) = ( I ‘𝑘))
945, 93seqfveq 14031 . . . . 5 (𝑃 ∈ ℙ → (seq1( · , (( I ↾ (1...(𝑃 − 1))) ∘ ( I ↾ (1...(𝑃 − 1)))))‘(𝑃 − 1)) = (seq1( · , I )‘(𝑃 − 1)))
95 cnfldbas 21290 . . . . . . 7 ℂ = (Base‘ℂfld)
9651, 95mgpbas 20087 . . . . . 6 ℂ = (Base‘𝑇)
97 cnfldmul 21294 . . . . . . 7 · = (.r‘ℂfld)
9851, 97mgpplusg 20085 . . . . . 6 · = (+g𝑇)
99 eqid 2728 . . . . . 6 (Cntz‘𝑇) = (Cntz‘𝑇)
100 cnring 21325 . . . . . . 7 fld ∈ Ring
10151ringmgp 20186 . . . . . . 7 (ℂfld ∈ Ring → 𝑇 ∈ Mnd)
102100, 101mp1i 13 . . . . . 6 (𝑃 ∈ ℙ → 𝑇 ∈ Mnd)
103 zsscn 12604 . . . . . . . 8 ℤ ⊆ ℂ
104 fss 6744 . . . . . . . 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 19807 . . . . . 6 (𝑃 ∈ ℙ → ran ( I ↾ (1...(𝑃 − 1))) ⊆ ((Cntz‘𝑇)‘ran ( I ↾ (1...(𝑃 − 1)))))
108 f1of1 6843 . . . . . . 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 8188 . . . . . . . . 9 (( I ↾ (1...(𝑃 − 1))) supp 1) ⊆ dom ( I ↾ (1...(𝑃 − 1)))
111 dmresi 6060 . . . . . . . . 9 dom ( I ↾ (1...(𝑃 − 1))) = (1...(𝑃 − 1))
112110, 111sseqtri 4018 . . . . . . . 8 (( I ↾ (1...(𝑃 − 1))) supp 1) ⊆ (1...(𝑃 − 1))
113 rnresi 6083 . . . . . . . 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 2728 . . . . . 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 19869 . . . . 5 (𝑃 ∈ ℙ → (𝑇 Σg ( I ↾ (1...(𝑃 − 1)))) = (seq1( · , (( I ↾ (1...(𝑃 − 1))) ∘ ( I ↾ (1...(𝑃 − 1)))))‘(𝑃 − 1)))
118 facnn 14274 . . . . . 6 ((𝑃 − 1) ∈ ℕ → (!‘(𝑃 − 1)) = (seq1( · , I )‘(𝑃 − 1)))
1193, 118syl 17 . . . . 5 (𝑃 ∈ ℙ → (!‘(𝑃 − 1)) = (seq1( · , I )‘(𝑃 − 1)))
12094, 117, 1193eqtr4d 2778 . . . 4 (𝑃 ∈ ℙ → (𝑇 Σg ( I ↾ (1...(𝑃 − 1)))) = (!‘(𝑃 − 1)))
121120oveq1d 7441 . . 3 (𝑃 ∈ ℙ → ((𝑇 Σg ( I ↾ (1...(𝑃 − 1)))) − -1) = ((!‘(𝑃 − 1)) − -1))
122 nnm1nn0 12551 . . . . . . 7 (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ0)
12311, 122syl 17 . . . . . 6 (𝑃 ∈ ℙ → (𝑃 − 1) ∈ ℕ0)
124123faccld 14283 . . . . 5 (𝑃 ∈ ℙ → (!‘(𝑃 − 1)) ∈ ℕ)
125124nncnd 12266 . . . 4 (𝑃 ∈ ℙ → (!‘(𝑃 − 1)) ∈ ℂ)
126 ax-1cn 11204 . . . 4 1 ∈ ℂ
127 subneg 11547 . . . 4 (((!‘(𝑃 − 1)) ∈ ℂ ∧ 1 ∈ ℂ) → ((!‘(𝑃 − 1)) − -1) = ((!‘(𝑃 − 1)) + 1))
128125, 126, 127sylancl 584 . . 3 (𝑃 ∈ ℙ → ((!‘(𝑃 − 1)) − -1) = ((!‘(𝑃 − 1)) + 1))
129121, 128eqtrd 2768 . 2 (𝑃 ∈ ℙ → ((𝑇 Σg ( I ↾ (1...(𝑃 − 1)))) − -1) = ((!‘(𝑃 − 1)) + 1))
13087, 129breqtrd 5178 1 (𝑃 ∈ ℙ → 𝑃 ∥ ((!‘(𝑃 − 1)) + 1))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  w3a 1084  wal 1531   = wceq 1533  wcel 2098  wral 3058  {crab 3430  Vcvv 3473  wss 3949  wpss 3950  𝒫 cpw 4606   class class class wbr 5152   I cid 5579  dom cdm 5682  ran crn 5683  cres 5684  ccom 5686  wf 6549  1-1wf1 6550  1-1-ontowf1o 6552  cfv 6553  (class class class)co 7426   supp csupp 8171  Fincfn 8970  cc 11144  1c1 11147   + caddc 11149   · cmul 11151  cmin 11482  -cneg 11483  cn 12250  2c2 12305  0cn0 12510  cz 12596  cuz 12860  ...cfz 13524   mod cmo 13874  seqcseq 14006  cexp 14066  !cfa 14272  cdvds 16238  cprime 16649   Σg cgsu 17429  Mndcmnd 18701  SubMndcsubmnd 18746  Cntzccntz 19273  CMndccmn 19742  mulGrpcmgp 20081  Ringcrg 20180  CRingccrg 20181  SubRingcsubrg 20513  fldccnfld 21286
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-cnex 11202  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222  ax-pre-mulgt0 11223  ax-pre-sup 11224  ax-addf 11225  ax-mulf 11226
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-tp 4637  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-iin 5003  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-se 5638  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-isom 6562  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-of 7691  df-om 7877  df-1st 7999  df-2nd 8000  df-supp 8172  df-frecs 8293  df-wrecs 8324  df-recs 8398  df-rdg 8437  df-1o 8493  df-2o 8494  df-oadd 8497  df-er 8731  df-en 8971  df-dom 8972  df-sdom 8973  df-fin 8974  df-fsupp 9394  df-sup 9473  df-inf 9474  df-oi 9541  df-dju 9932  df-card 9970  df-pnf 11288  df-mnf 11289  df-xr 11290  df-ltxr 11291  df-le 11292  df-sub 11484  df-neg 11485  df-div 11910  df-nn 12251  df-2 12313  df-3 12314  df-4 12315  df-5 12316  df-6 12317  df-7 12318  df-8 12319  df-9 12320  df-n0 12511  df-xnn0 12583  df-z 12597  df-dec 12716  df-uz 12861  df-rp 13015  df-fz 13525  df-fzo 13668  df-fl 13797  df-mod 13875  df-seq 14007  df-exp 14067  df-fac 14273  df-hash 14330  df-cj 15086  df-re 15087  df-im 15088  df-sqrt 15222  df-abs 15223  df-dvds 16239  df-gcd 16477  df-prm 16650  df-phi 16742  df-struct 17123  df-sets 17140  df-slot 17158  df-ndx 17170  df-base 17188  df-ress 17217  df-plusg 17253  df-mulr 17254  df-starv 17255  df-tset 17259  df-ple 17260  df-ds 17262  df-unif 17263  df-0g 17430  df-gsum 17431  df-mre 17573  df-mrc 17574  df-acs 17576  df-mgm 18607  df-sgrp 18686  df-mnd 18702  df-submnd 18748  df-grp 18900  df-minusg 18901  df-mulg 19031  df-subg 19085  df-cntz 19275  df-cmn 19744  df-abl 19745  df-mgp 20082  df-rng 20100  df-ur 20129  df-ring 20182  df-cring 20183  df-subrng 20490  df-subrg 20515  df-cnfld 21287
This theorem is referenced by:  wilth  27023
  Copyright terms: Public domain W3C validator