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

Theorem wilthlem2 24708
 Description: Lemma for wilth 24710: 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 24707 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 477 . . . . . . . . 9 ((𝜑𝑆 ⊆ {(𝑃 − 1)}) → 𝑆 ⊆ {(𝑃 − 1)})
2 wilthlem2.s . . . . . . . . . . . . . 14 (𝜑𝑆𝐴)
3 eleq2 2687 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑆 → ((𝑃 − 1) ∈ 𝑥 ↔ (𝑃 − 1) ∈ 𝑆))
4 eleq2 2687 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑆 → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥 ↔ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆))
54raleqbi1dv 3138 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑆 → (∀𝑦𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥 ↔ ∀𝑦𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆))
63, 5anbi12d 746 . . . . . . . . . . . . . . 15 (𝑥 = 𝑆 → (((𝑃 − 1) ∈ 𝑥 ∧ ∀𝑦𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥) ↔ ((𝑃 − 1) ∈ 𝑆 ∧ ∀𝑦𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)))
7 wilthlem.a . . . . . . . . . . . . . . 15 𝐴 = {𝑥 ∈ 𝒫 (1...(𝑃 − 1)) ∣ ((𝑃 − 1) ∈ 𝑥 ∧ ∀𝑦𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥)}
86, 7elrab2 3352 . . . . . . . . . . . . . 14 (𝑆𝐴 ↔ (𝑆 ∈ 𝒫 (1...(𝑃 − 1)) ∧ ((𝑃 − 1) ∈ 𝑆 ∧ ∀𝑦𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)))
92, 8sylib 208 . . . . . . . . . . . . 13 (𝜑 → (𝑆 ∈ 𝒫 (1...(𝑃 − 1)) ∧ ((𝑃 − 1) ∈ 𝑆 ∧ ∀𝑦𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)))
109simprd 479 . . . . . . . . . . . 12 (𝜑 → ((𝑃 − 1) ∈ 𝑆 ∧ ∀𝑦𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆))
1110simpld 475 . . . . . . . . . . 11 (𝜑 → (𝑃 − 1) ∈ 𝑆)
1211snssd 4314 . . . . . . . . . 10 (𝜑 → {(𝑃 − 1)} ⊆ 𝑆)
1312adantr 481 . . . . . . . . 9 ((𝜑𝑆 ⊆ {(𝑃 − 1)}) → {(𝑃 − 1)} ⊆ 𝑆)
141, 13eqssd 3604 . . . . . . . 8 ((𝜑𝑆 ⊆ {(𝑃 − 1)}) → 𝑆 = {(𝑃 − 1)})
1514reseq2d 5361 . . . . . . 7 ((𝜑𝑆 ⊆ {(𝑃 − 1)}) → ( I ↾ 𝑆) = ( I ↾ {(𝑃 − 1)}))
16 mptresid 5420 . . . . . . 7 (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧) = ( I ↾ {(𝑃 − 1)})
1715, 16syl6eqr 2673 . . . . . 6 ((𝜑𝑆 ⊆ {(𝑃 − 1)}) → ( I ↾ 𝑆) = (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧))
1817oveq2d 6626 . . . . 5 ((𝜑𝑆 ⊆ {(𝑃 − 1)}) → (𝑇 Σg ( I ↾ 𝑆)) = (𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)))
1918oveq1d 6625 . . . 4 ((𝜑𝑆 ⊆ {(𝑃 − 1)}) → ((𝑇 Σg ( I ↾ 𝑆)) mod 𝑃) = ((𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) mod 𝑃))
20 wilthlem2.p . . . . . . . . . . . 12 (𝜑𝑃 ∈ ℙ)
21 prmnn 15319 . . . . . . . . . . . 12 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
2220, 21syl 17 . . . . . . . . . . 11 (𝜑𝑃 ∈ ℕ)
2322nncnd 10987 . . . . . . . . . 10 (𝜑𝑃 ∈ ℂ)
24 ax-1cn 9945 . . . . . . . . . 10 1 ∈ ℂ
25 negsub 10280 . . . . . . . . . 10 ((𝑃 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑃 + -1) = (𝑃 − 1))
2623, 24, 25sylancl 693 . . . . . . . . 9 (𝜑 → (𝑃 + -1) = (𝑃 − 1))
27 neg1cn 11075 . . . . . . . . . 10 -1 ∈ ℂ
28 addcom 10173 . . . . . . . . . 10 ((𝑃 ∈ ℂ ∧ -1 ∈ ℂ) → (𝑃 + -1) = (-1 + 𝑃))
2923, 27, 28sylancl 693 . . . . . . . . 9 (𝜑 → (𝑃 + -1) = (-1 + 𝑃))
3026, 29eqtr3d 2657 . . . . . . . 8 (𝜑 → (𝑃 − 1) = (-1 + 𝑃))
31 cnring 19696 . . . . . . . . . 10 fld ∈ Ring
32 wilthlem.t . . . . . . . . . . 11 𝑇 = (mulGrp‘ℂfld)
3332ringmgp 18481 . . . . . . . . . 10 (ℂfld ∈ Ring → 𝑇 ∈ Mnd)
3431, 33mp1i 13 . . . . . . . . 9 (𝜑𝑇 ∈ Mnd)
35 nnm1nn0 11285 . . . . . . . . . . 11 (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ0)
3622, 35syl 17 . . . . . . . . . 10 (𝜑 → (𝑃 − 1) ∈ ℕ0)
3736nn0cnd 11304 . . . . . . . . 9 (𝜑 → (𝑃 − 1) ∈ ℂ)
38 cnfldbas 19678 . . . . . . . . . . 11 ℂ = (Base‘ℂfld)
3932, 38mgpbas 18423 . . . . . . . . . 10 ℂ = (Base‘𝑇)
40 id 22 . . . . . . . . . 10 (𝑧 = (𝑃 − 1) → 𝑧 = (𝑃 − 1))
4139, 40gsumsn 18282 . . . . . . . . 9 ((𝑇 ∈ Mnd ∧ (𝑃 − 1) ∈ ℂ ∧ (𝑃 − 1) ∈ ℂ) → (𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) = (𝑃 − 1))
4234, 37, 37, 41syl3anc 1323 . . . . . . . 8 (𝜑 → (𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) = (𝑃 − 1))
4323mulid2d 10009 . . . . . . . . 9 (𝜑 → (1 · 𝑃) = 𝑃)
4443oveq2d 6626 . . . . . . . 8 (𝜑 → (-1 + (1 · 𝑃)) = (-1 + 𝑃))
4530, 42, 443eqtr4d 2665 . . . . . . 7 (𝜑 → (𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) = (-1 + (1 · 𝑃)))
4645oveq1d 6625 . . . . . 6 (𝜑 → ((𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) mod 𝑃) = ((-1 + (1 · 𝑃)) mod 𝑃))
47 neg1rr 11076 . . . . . . . 8 -1 ∈ ℝ
4847a1i 11 . . . . . . 7 (𝜑 → -1 ∈ ℝ)
4922nnrpd 11821 . . . . . . 7 (𝜑𝑃 ∈ ℝ+)
50 1zzd 11359 . . . . . . 7 (𝜑 → 1 ∈ ℤ)
51 modcyc 12652 . . . . . . 7 ((-1 ∈ ℝ ∧ 𝑃 ∈ ℝ+ ∧ 1 ∈ ℤ) → ((-1 + (1 · 𝑃)) mod 𝑃) = (-1 mod 𝑃))
5248, 49, 50, 51syl3anc 1323 . . . . . 6 (𝜑 → ((-1 + (1 · 𝑃)) mod 𝑃) = (-1 mod 𝑃))
5346, 52eqtrd 2655 . . . . 5 (𝜑 → ((𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) mod 𝑃) = (-1 mod 𝑃))
5453adantr 481 . . . 4 ((𝜑𝑆 ⊆ {(𝑃 − 1)}) → ((𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) mod 𝑃) = (-1 mod 𝑃))
5519, 54eqtrd 2655 . . 3 ((𝜑𝑆 ⊆ {(𝑃 − 1)}) → ((𝑇 Σg ( I ↾ 𝑆)) mod 𝑃) = (-1 mod 𝑃))
5655ex 450 . 2 (𝜑 → (𝑆 ⊆ {(𝑃 − 1)} → ((𝑇 Σg ( I ↾ 𝑆)) mod 𝑃) = (-1 mod 𝑃)))
57 nss 3647 . . 3 𝑆 ⊆ {(𝑃 − 1)} ↔ ∃𝑧(𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)}))
58 cnfld1 19699 . . . . . . . . . 10 1 = (1r‘ℂfld)
5932, 58ringidval 18431 . . . . . . . . 9 1 = (0g𝑇)
60 cnfldmul 19680 . . . . . . . . . 10 · = (.r‘ℂfld)
6132, 60mgpplusg 18421 . . . . . . . . 9 · = (+g𝑇)
62 cncrng 19695 . . . . . . . . . . 11 fld ∈ CRing
6332crngmgp 18483 . . . . . . . . . . 11 (ℂfld ∈ CRing → 𝑇 ∈ CMnd)
6462, 63ax-mp 5 . . . . . . . . . 10 𝑇 ∈ CMnd
6564a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑇 ∈ CMnd)
662adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑆𝐴)
67 f1oi 6136 . . . . . . . . . . . 12 ( I ↾ 𝑆):𝑆1-1-onto𝑆
68 f1of 6099 . . . . . . . . . . . 12 (( I ↾ 𝑆):𝑆1-1-onto𝑆 → ( I ↾ 𝑆):𝑆𝑆)
6967, 68ax-mp 5 . . . . . . . . . . 11 ( I ↾ 𝑆):𝑆𝑆
709simpld 475 . . . . . . . . . . . . . 14 (𝜑𝑆 ∈ 𝒫 (1...(𝑃 − 1)))
7170elpwid 4146 . . . . . . . . . . . . 13 (𝜑𝑆 ⊆ (1...(𝑃 − 1)))
72 elfzelz 12291 . . . . . . . . . . . . . 14 (𝑧 ∈ (1...(𝑃 − 1)) → 𝑧 ∈ ℤ)
7372ssriv 3591 . . . . . . . . . . . . 13 (1...(𝑃 − 1)) ⊆ ℤ
7471, 73syl6ss 3599 . . . . . . . . . . . 12 (𝜑𝑆 ⊆ ℤ)
75 zsscn 11336 . . . . . . . . . . . 12 ℤ ⊆ ℂ
7674, 75syl6ss 3599 . . . . . . . . . . 11 (𝜑𝑆 ⊆ ℂ)
77 fss 6018 . . . . . . . . . . 11 ((( I ↾ 𝑆):𝑆𝑆𝑆 ⊆ ℂ) → ( I ↾ 𝑆):𝑆⟶ℂ)
7869, 76, 77sylancr 694 . . . . . . . . . 10 (𝜑 → ( I ↾ 𝑆):𝑆⟶ℂ)
7978adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ( I ↾ 𝑆):𝑆⟶ℂ)
80 fzfi 12718 . . . . . . . . . . . 12 (1...(𝑃 − 1)) ∈ Fin
81 ssfi 8131 . . . . . . . . . . . 12 (((1...(𝑃 − 1)) ∈ Fin ∧ 𝑆 ⊆ (1...(𝑃 − 1))) → 𝑆 ∈ Fin)
8280, 71, 81sylancr 694 . . . . . . . . . . 11 (𝜑𝑆 ∈ Fin)
83 1ex 9986 . . . . . . . . . . . 12 1 ∈ V
8483a1i 11 . . . . . . . . . . 11 (𝜑 → 1 ∈ V)
8578, 82, 84fdmfifsupp 8236 . . . . . . . . . 10 (𝜑 → ( I ↾ 𝑆) finSupp 1)
8685adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ( I ↾ 𝑆) finSupp 1)
87 disjdif 4017 . . . . . . . . . 10 ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∩ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = ∅
8887a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∩ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = ∅)
89 undif2 4021 . . . . . . . . . 10 ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∪ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∪ 𝑆)
90 simprl 793 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑧𝑆)
9110simprd 479 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑦𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)
9291adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ∀𝑦𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)
93 oveq1 6617 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑧 → (𝑦↑(𝑃 − 2)) = (𝑧↑(𝑃 − 2)))
9493oveq1d 6625 . . . . . . . . . . . . . . 15 (𝑦 = 𝑧 → ((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃))
9594eleq1d 2683 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆 ↔ ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆))
9695rspcv 3294 . . . . . . . . . . . . 13 (𝑧𝑆 → (∀𝑦𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆 → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆))
9790, 92, 96sylc 65 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)
98 prssi 4326 . . . . . . . . . . . 12 ((𝑧𝑆 ∧ ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆) → {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ⊆ 𝑆)
9990, 97, 98syl2anc 692 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ⊆ 𝑆)
100 ssequn1 3766 . . . . . . . . . . 11 ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ⊆ 𝑆 ↔ ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∪ 𝑆) = 𝑆)
10199, 100sylib 208 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∪ 𝑆) = 𝑆)
10289, 101syl5req 2668 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑆 = ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∪ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))
10339, 59, 61, 65, 66, 79, 86, 88, 102gsumsplit 18256 . . . . . . . 8 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg ( I ↾ 𝑆)) = ((𝑇 Σg (( I ↾ 𝑆) ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg (( I ↾ 𝑆) ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))))
10499resabs1d 5392 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (( I ↾ 𝑆) ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) = ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
105104oveq2d 6626 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg (( I ↾ 𝑆) ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = (𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))
106 difss 3720 . . . . . . . . . . . 12 (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ 𝑆
107 resabs1 5391 . . . . . . . . . . . 12 ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ 𝑆 → (( I ↾ 𝑆) ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))
108106, 107ax-mp 5 . . . . . . . . . . 11 (( I ↾ 𝑆) ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
109108oveq2i 6621 . . . . . . . . . 10 (𝑇 Σg (( I ↾ 𝑆) ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) = (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))
110109a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg (( I ↾ 𝑆) ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) = (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))))
111105, 110oveq12d 6628 . . . . . . . 8 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑇 Σg (( I ↾ 𝑆) ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg (( I ↾ 𝑆) ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) = ((𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))))
112103, 111eqtrd 2655 . . . . . . 7 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg ( I ↾ 𝑆)) = ((𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))))
113112oveq1d 6625 . . . . . 6 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑇 Σg ( I ↾ 𝑆)) mod 𝑃) = (((𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) mod 𝑃))
114 prfi 8186 . . . . . . . . . 10 {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∈ Fin
115114a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∈ Fin)
116 zsubrg 19727 . . . . . . . . . 10 ℤ ∈ (SubRing‘ℂfld)
11732subrgsubm 18721 . . . . . . . . . 10 (ℤ ∈ (SubRing‘ℂfld) → ℤ ∈ (SubMnd‘𝑇))
118116, 117mp1i 13 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ℤ ∈ (SubMnd‘𝑇))
119 f1oi 6136 . . . . . . . . . . 11 ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}–1-1-onto→{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}
120 f1of 6099 . . . . . . . . . . 11 (( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}–1-1-onto→{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} → ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}⟶{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})
121119, 120ax-mp 5 . . . . . . . . . 10 ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}⟶{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}
12274adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑆 ⊆ ℤ)
12399, 122sstrd 3597 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ⊆ ℤ)
124 fss 6018 . . . . . . . . . 10 ((( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}⟶{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∧ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ⊆ ℤ) → ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}⟶ℤ)
125121, 123, 124sylancr 694 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}⟶ℤ)
12683a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 1 ∈ V)
127125, 115, 126fdmfifsupp 8236 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) finSupp 1)
12859, 65, 115, 118, 125, 127gsumsubmcl 18247 . . . . . . . 8 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) ∈ ℤ)
129128zred 11433 . . . . . . 7 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) ∈ ℝ)
130 1red 10006 . . . . . . 7 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 1 ∈ ℝ)
13171adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑆 ⊆ (1...(𝑃 − 1)))
132131ssdifssd 3731 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ (1...(𝑃 − 1)))
133 ssfi 8131 . . . . . . . . 9 (((1...(𝑃 − 1)) ∈ Fin ∧ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ (1...(𝑃 − 1))) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ Fin)
13480, 132, 133sylancr 694 . . . . . . . 8 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ Fin)
135 f1oi 6136 . . . . . . . . . 10 ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})):(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})–1-1-onto→(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})
136 f1of 6099 . . . . . . . . . 10 (( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})):(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})–1-1-onto→(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})):(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})⟶(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
137135, 136ax-mp 5 . . . . . . . . 9 ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})):(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})⟶(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})
138122ssdifssd 3731 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ ℤ)
139 fss 6018 . . . . . . . . 9 ((( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})):(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})⟶(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∧ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ ℤ) → ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})):(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})⟶ℤ)
140137, 138, 139sylancr 694 . . . . . . . 8 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})):(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})⟶ℤ)
141140, 134, 126fdmfifsupp 8236 . . . . . . . 8 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) finSupp 1)
14259, 65, 134, 118, 140, 141gsumsubmcl 18247 . . . . . . 7 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) ∈ ℤ)
14349adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∈ ℝ+)
14434adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑇 ∈ Mnd)
14576adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑆 ⊆ ℂ)
146145, 90sseldd 3588 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑧 ∈ ℂ)
147 id 22 . . . . . . . . . . . . 13 (𝑤 = 𝑧𝑤 = 𝑧)
14839, 147gsumsn 18282 . . . . . . . . . . . 12 ((𝑇 ∈ Mnd ∧ 𝑧 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) = 𝑧)
149144, 146, 146, 148syl3anc 1323 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) = 𝑧)
150149adantr 481 . . . . . . . . . 10 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → (𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) = 𝑧)
151 mptresid 5420 . . . . . . . . . . . 12 (𝑤 ∈ {𝑧} ↦ 𝑤) = ( I ↾ {𝑧})
152 dfsn2 4166 . . . . . . . . . . . . . 14 {𝑧} = {𝑧, 𝑧}
153 simpr 477 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → 𝑧 = 1)
154153orcd 407 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → (𝑧 = 1 ∨ 𝑧 = (𝑃 − 1)))
15520adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∈ ℙ)
156131, 90sseldd 3588 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑧 ∈ (1...(𝑃 − 1)))
157 wilthlem1 24707 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ ℙ ∧ 𝑧 ∈ (1...(𝑃 − 1))) → (𝑧 = ((𝑧↑(𝑃 − 2)) mod 𝑃) ↔ (𝑧 = 1 ∨ 𝑧 = (𝑃 − 1))))
158155, 156, 157syl2anc 692 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑧 = ((𝑧↑(𝑃 − 2)) mod 𝑃) ↔ (𝑧 = 1 ∨ 𝑧 = (𝑃 − 1))))
159158biimpar 502 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ (𝑧 = 1 ∨ 𝑧 = (𝑃 − 1))) → 𝑧 = ((𝑧↑(𝑃 − 2)) mod 𝑃))
160154, 159syldan 487 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → 𝑧 = ((𝑧↑(𝑃 − 2)) mod 𝑃))
161160preq2d 4250 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → {𝑧, 𝑧} = {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})
162152, 161syl5eq 2667 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → {𝑧} = {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})
163162reseq2d 5361 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → ( I ↾ {𝑧}) = ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
164151, 163syl5eq 2667 . . . . . . . . . . 11 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → (𝑤 ∈ {𝑧} ↦ 𝑤) = ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
165164oveq2d 6626 . . . . . . . . . 10 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → (𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) = (𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))
166150, 165, 1533eqtr3d 2663 . . . . . . . . 9 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → (𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = 1)
167166oveq1d 6625 . . . . . . . 8 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → ((𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) mod 𝑃) = (1 mod 𝑃))
168 df-pr 4156 . . . . . . . . . . . . . . 15 {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} = ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)})
169168reseq2i 5358 . . . . . . . . . . . . . 14 ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) = ( I ↾ ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)}))
170 mptresid 5420 . . . . . . . . . . . . . 14 (𝑤 ∈ ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)}) ↦ 𝑤) = ( I ↾ ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)}))
171169, 170eqtr4i 2646 . . . . . . . . . . . . 13 ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) = (𝑤 ∈ ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)}) ↦ 𝑤)
172171oveq2i 6621 . . . . . . . . . . . 12 (𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = (𝑇 Σg (𝑤 ∈ ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)}) ↦ 𝑤))
17364a1i 11 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → 𝑇 ∈ CMnd)
174 snfi 7989 . . . . . . . . . . . . . 14 {𝑧} ∈ Fin
175174a1i 11 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → {𝑧} ∈ Fin)
176 elsni 4170 . . . . . . . . . . . . . . . 16 (𝑤 ∈ {𝑧} → 𝑤 = 𝑧)
177176adantl 482 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑤 ∈ {𝑧}) → 𝑤 = 𝑧)
178146adantr 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑤 ∈ {𝑧}) → 𝑧 ∈ ℂ)
179177, 178eqeltrd 2698 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑤 ∈ {𝑧}) → 𝑤 ∈ ℂ)
180179adantlr 750 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) ∧ 𝑤 ∈ {𝑧}) → 𝑤 ∈ ℂ)
181145, 97sseldd 3588 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ ℂ)
182181adantr 481 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ ℂ)
183 simprr 795 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ 𝑧 ∈ {(𝑃 − 1)})
184 velsn 4169 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ {(𝑃 − 1)} ↔ 𝑧 = (𝑃 − 1))
185183, 184sylnib 318 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ 𝑧 = (𝑃 − 1))
186 biorf 420 . . . . . . . . . . . . . . . . 17 𝑧 = (𝑃 − 1) → (𝑧 = 1 ↔ (𝑧 = (𝑃 − 1) ∨ 𝑧 = 1)))
187185, 186syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑧 = 1 ↔ (𝑧 = (𝑃 − 1) ∨ 𝑧 = 1)))
188 ovex 6638 . . . . . . . . . . . . . . . . . . 19 ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ V
189188elsn 4168 . . . . . . . . . . . . . . . . . 18 (((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧} ↔ ((𝑧↑(𝑃 − 2)) mod 𝑃) = 𝑧)
190 eqcom 2628 . . . . . . . . . . . . . . . . . 18 (((𝑧↑(𝑃 − 2)) mod 𝑃) = 𝑧𝑧 = ((𝑧↑(𝑃 − 2)) mod 𝑃))
191189, 190bitri 264 . . . . . . . . . . . . . . . . 17 (((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧} ↔ 𝑧 = ((𝑧↑(𝑃 − 2)) mod 𝑃))
192 orcom 402 . . . . . . . . . . . . . . . . 17 ((𝑧 = (𝑃 − 1) ∨ 𝑧 = 1) ↔ (𝑧 = 1 ∨ 𝑧 = (𝑃 − 1)))
193158, 191, 1923bitr4g 303 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧} ↔ (𝑧 = (𝑃 − 1) ∨ 𝑧 = 1)))
194187, 193bitr4d 271 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑧 = 1 ↔ ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧}))
195194necon3abid 2826 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑧 ≠ 1 ↔ ¬ ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧}))
196195biimpa 501 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → ¬ ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧})
197 id 22 . . . . . . . . . . . . 13 (𝑤 = ((𝑧↑(𝑃 − 2)) mod 𝑃) → 𝑤 = ((𝑧↑(𝑃 − 2)) mod 𝑃))
19839, 61, 173, 175, 180, 182, 196, 182, 197gsumunsn 18287 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → (𝑇 Σg (𝑤 ∈ ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)}) ↦ 𝑤)) = ((𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) · ((𝑧↑(𝑃 − 2)) mod 𝑃)))
199172, 198syl5eq 2667 . . . . . . . . . . 11 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → (𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = ((𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) · ((𝑧↑(𝑃 − 2)) mod 𝑃)))
200149adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → (𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) = 𝑧)
201200oveq1d 6625 . . . . . . . . . . 11 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → ((𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) · ((𝑧↑(𝑃 − 2)) mod 𝑃)) = (𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)))
202199, 201eqtrd 2655 . . . . . . . . . 10 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → (𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = (𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)))
203202oveq1d 6625 . . . . . . . . 9 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → ((𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) mod 𝑃) = ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) mod 𝑃))
204156, 72syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑧 ∈ ℤ)
20522adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∈ ℕ)
206 fzm1ndvds 14975 . . . . . . . . . . . . . 14 ((𝑃 ∈ ℕ ∧ 𝑧 ∈ (1...(𝑃 − 1))) → ¬ 𝑃𝑧)
207205, 156, 206syl2anc 692 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ 𝑃𝑧)
208 eqid 2621 . . . . . . . . . . . . . 14 ((𝑧↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃)
209208prmdiv 15421 . . . . . . . . . . . . 13 ((𝑃 ∈ ℙ ∧ 𝑧 ∈ ℤ ∧ ¬ 𝑃𝑧) → (((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) − 1)))
210155, 204, 207, 209syl3anc 1323 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) − 1)))
211210simprd 479 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∥ ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) − 1))
212 elfznn 12319 . . . . . . . . . . . . . . 15 (𝑧 ∈ (1...(𝑃 − 1)) → 𝑧 ∈ ℕ)
213156, 212syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑧 ∈ ℕ)
214131, 97sseldd 3588 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)))
215 elfznn 12319 . . . . . . . . . . . . . . 15 (((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ ℕ)
216214, 215syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ ℕ)
217213, 216nnmulcld 11019 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) ∈ ℕ)
218217nnzd 11432 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) ∈ ℤ)
219 1zzd 11359 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 1 ∈ ℤ)
220 moddvds 14922 . . . . . . . . . . . 12 ((𝑃 ∈ ℕ ∧ (𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) ∈ ℤ ∧ 1 ∈ ℤ) → (((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) − 1)))
221205, 218, 219, 220syl3anc 1323 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) − 1)))
222211, 221mpbird 247 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = (1 mod 𝑃))
223222adantr 481 . . . . . . . . 9 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = (1 mod 𝑃))
224203, 223eqtrd 2655 . . . . . . . 8 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → ((𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) mod 𝑃) = (1 mod 𝑃))
225167, 224pm2.61dane 2877 . . . . . . 7 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) mod 𝑃) = (1 mod 𝑃))
226 modmul1 12670 . . . . . . 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 𝑃))
227129, 130, 142, 143, 225, 226syl221anc 1334 . . . . . 6 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) mod 𝑃) = ((1 · (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) mod 𝑃))
228142zcnd 11434 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) ∈ ℂ)
229228mulid2d 10009 . . . . . . . 8 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (1 · (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) = (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))))
230229oveq1d 6625 . . . . . . 7 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((1 · (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) mod 𝑃) = ((𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) mod 𝑃))
231 ovex 6638 . . . . . . . . . . 11 (1...(𝑃 − 1)) ∈ V
232231elpw2 4793 . . . . . . . . . 10 ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ 𝒫 (1...(𝑃 − 1)) ↔ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ (1...(𝑃 − 1)))
233132, 232sylibr 224 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ 𝒫 (1...(𝑃 − 1)))
23411adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ 𝑆)
235 eqcom 2628 . . . . . . . . . . . . . . 15 (𝑧 = (𝑃 − 1) ↔ (𝑃 − 1) = 𝑧)
236184, 235bitri 264 . . . . . . . . . . . . . 14 (𝑧 ∈ {(𝑃 − 1)} ↔ (𝑃 − 1) = 𝑧)
237183, 236sylnib 318 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ (𝑃 − 1) = 𝑧)
238 oveq1 6617 . . . . . . . . . . . . . . . 16 ((𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃) → ((𝑃 − 1)↑(𝑃 − 2)) = (((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)))
239238oveq1d 6625 . . . . . . . . . . . . . . 15 ((𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃) → (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃) = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃))
240205, 35syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ ℕ0)
241 nn0uz 11673 . . . . . . . . . . . . . . . . . . 19 0 = (ℤ‘0)
242240, 241syl6eleq 2708 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ (ℤ‘0))
243 eluzfz2 12298 . . . . . . . . . . . . . . . . . 18 ((𝑃 − 1) ∈ (ℤ‘0) → (𝑃 − 1) ∈ (0...(𝑃 − 1)))
244242, 243syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ (0...(𝑃 − 1)))
245 prmz 15320 . . . . . . . . . . . . . . . . . . . 20 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
246155, 245syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∈ ℤ)
247122, 234sseldd 3588 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ ℤ)
248 1z 11358 . . . . . . . . . . . . . . . . . . . 20 1 ∈ ℤ
249 zsubcl 11370 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 − 1) ∈ ℤ ∧ 1 ∈ ℤ) → ((𝑃 − 1) − 1) ∈ ℤ)
250247, 248, 249sylancl 693 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) − 1) ∈ ℤ)
251 dvdsmul1 14934 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ ℤ ∧ ((𝑃 − 1) − 1) ∈ ℤ) → 𝑃 ∥ (𝑃 · ((𝑃 − 1) − 1)))
252246, 250, 251syl2anc 692 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∥ (𝑃 · ((𝑃 − 1) − 1)))
253205nncnd 10987 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∈ ℂ)
25424a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 1 ∈ ℂ)
255240nn0cnd 11304 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ ℂ)
256253, 254, 255subdird 10438 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) · (𝑃 − 1)) = ((𝑃 · (𝑃 − 1)) − (1 · (𝑃 − 1))))
257253, 255mulcld 10011 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 · (𝑃 − 1)) ∈ ℂ)
258257, 253, 254subsubd 10371 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 · (𝑃 − 1)) − (𝑃 − 1)) = (((𝑃 · (𝑃 − 1)) − 𝑃) + 1))
259255mulid2d 10009 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (1 · (𝑃 − 1)) = (𝑃 − 1))
260259oveq2d 6626 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 · (𝑃 − 1)) − (1 · (𝑃 − 1))) = ((𝑃 · (𝑃 − 1)) − (𝑃 − 1)))
261253, 255, 254subdid 10437 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 · ((𝑃 − 1) − 1)) = ((𝑃 · (𝑃 − 1)) − (𝑃 · 1)))
262253mulid1d 10008 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 · 1) = 𝑃)
263262oveq2d 6626 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 · (𝑃 − 1)) − (𝑃 · 1)) = ((𝑃 · (𝑃 − 1)) − 𝑃))
264261, 263eqtrd 2655 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 · ((𝑃 − 1) − 1)) = ((𝑃 · (𝑃 − 1)) − 𝑃))
265264oveq1d 6625 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 · ((𝑃 − 1) − 1)) + 1) = (((𝑃 · (𝑃 − 1)) − 𝑃) + 1))
266258, 260, 2653eqtr4d 2665 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 · (𝑃 − 1)) − (1 · (𝑃 − 1))) = ((𝑃 · ((𝑃 − 1) − 1)) + 1))
267256, 266eqtrd 2655 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) · (𝑃 − 1)) = ((𝑃 · ((𝑃 − 1) − 1)) + 1))
268267oveq1d 6625 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑃 − 1) · (𝑃 − 1)) − 1) = (((𝑃 · ((𝑃 − 1) − 1)) + 1) − 1))
269250zcnd 11434 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) − 1) ∈ ℂ)
270253, 269mulcld 10011 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 · ((𝑃 − 1) − 1)) ∈ ℂ)
271 pncan 10238 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 · ((𝑃 − 1) − 1)) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑃 · ((𝑃 − 1) − 1)) + 1) − 1) = (𝑃 · ((𝑃 − 1) − 1)))
272270, 24, 271sylancl 693 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑃 · ((𝑃 − 1) − 1)) + 1) − 1) = (𝑃 · ((𝑃 − 1) − 1)))
273268, 272eqtrd 2655 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑃 − 1) · (𝑃 − 1)) − 1) = (𝑃 · ((𝑃 − 1) − 1)))
274252, 273breqtrrd 4646 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∥ (((𝑃 − 1) · (𝑃 − 1)) − 1))
275131, 234sseldd 3588 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ (1...(𝑃 − 1)))
276 fzm1ndvds 14975 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ ℕ ∧ (𝑃 − 1) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (𝑃 − 1))
277205, 275, 276syl2anc 692 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ 𝑃 ∥ (𝑃 − 1))
278 eqid 2621 . . . . . . . . . . . . . . . . . . 19 (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃) = (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃)
279278prmdiveq 15422 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ ℙ ∧ (𝑃 − 1) ∈ ℤ ∧ ¬ 𝑃 ∥ (𝑃 − 1)) → (((𝑃 − 1) ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ (((𝑃 − 1) · (𝑃 − 1)) − 1)) ↔ (𝑃 − 1) = (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃)))
280155, 247, 277, 279syl3anc 1323 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑃 − 1) ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ (((𝑃 − 1) · (𝑃 − 1)) − 1)) ↔ (𝑃 − 1) = (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃)))
281244, 274, 280mpbi2and 955 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) = (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃))
282208prmdivdiv 15423 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ ℙ ∧ 𝑧 ∈ (1...(𝑃 − 1))) → 𝑧 = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃))
283155, 156, 282syl2anc 692 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑧 = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃))
284281, 283eqeq12d 2636 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) = 𝑧 ↔ (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃) = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃)))
285239, 284syl5ibr 236 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃) → (𝑃 − 1) = 𝑧))
286237, 285mtod 189 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ (𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃))
287 ioran 511 . . . . . . . . . . . . 13 (¬ ((𝑃 − 1) = 𝑧 ∨ (𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃)) ↔ (¬ (𝑃 − 1) = 𝑧 ∧ ¬ (𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃)))
288237, 286, 287sylanbrc 697 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ ((𝑃 − 1) = 𝑧 ∨ (𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃)))
289 ovex 6638 . . . . . . . . . . . . 13 (𝑃 − 1) ∈ V
290289elpr 4174 . . . . . . . . . . . 12 ((𝑃 − 1) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ↔ ((𝑃 − 1) = 𝑧 ∨ (𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃)))
291288, 290sylnibr 319 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ (𝑃 − 1) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})
292234, 291eldifd 3570 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
293 eldifi 3715 . . . . . . . . . . . . 13 (𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → 𝑦𝑆)
29492r19.21bi 2927 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)
295293, 294sylan2 491 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) → ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)
296 eldif 3569 . . . . . . . . . . . . 13 (𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ↔ (𝑦𝑆 ∧ ¬ 𝑦 ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
297155adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → 𝑃 ∈ ℙ)
298131sselda 3587 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → 𝑦 ∈ (1...(𝑃 − 1)))
299 eqid 2621 . . . . . . . . . . . . . . . . . . . 20 ((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑦↑(𝑃 − 2)) mod 𝑃)
300299prmdivdiv 15423 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ ℙ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → 𝑦 = ((((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃))
301297, 298, 300syl2anc 692 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → 𝑦 = ((((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃))
302 oveq1 6617 . . . . . . . . . . . . . . . . . . . 20 (((𝑦↑(𝑃 − 2)) mod 𝑃) = 𝑧 → (((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) = (𝑧↑(𝑃 − 2)))
303302oveq1d 6625 . . . . . . . . . . . . . . . . . . 19 (((𝑦↑(𝑃 − 2)) mod 𝑃) = 𝑧 → ((((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃))
304303eqeq2d 2631 . . . . . . . . . . . . . . . . . 18 (((𝑦↑(𝑃 − 2)) mod 𝑃) = 𝑧 → (𝑦 = ((((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃) ↔ 𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃)))
305301, 304syl5ibcom 235 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → (((𝑦↑(𝑃 − 2)) mod 𝑃) = 𝑧𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃)))
306 oveq1 6617 . . . . . . . . . . . . . . . . . . 19 (((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃) → (((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) = (((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)))
307306oveq1d 6625 . . . . . . . . . . . . . . . . . 18 (((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃) → ((((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃) = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃))
308283adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → 𝑧 = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃))
309301, 308eqeq12d 2636 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → (𝑦 = 𝑧 ↔ ((((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃) = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃)))
310307, 309syl5ibr 236 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → (((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃) → 𝑦 = 𝑧))
311305, 310orim12d 882 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → ((((𝑦↑(𝑃 − 2)) mod 𝑃) = 𝑧 ∨ ((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃)) → (𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃) ∨ 𝑦 = 𝑧)))
312 ovex 6638 . . . . . . . . . . . . . . . . 17 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ V
313312elpr 4174 . . . . . . . . . . . . . . . 16 (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ↔ (((𝑦↑(𝑃 − 2)) mod 𝑃) = 𝑧 ∨ ((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃)))
314 vex 3192 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
315314elpr 4174 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ↔ (𝑦 = 𝑧𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃)))
316 orcom 402 . . . . . . . . . . . . . . . . 17 ((𝑦 = 𝑧𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃)) ↔ (𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃) ∨ 𝑦 = 𝑧))
317315, 316bitri 264 . . . . . . . . . . . . . . . 16 (𝑦 ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ↔ (𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃) ∨ 𝑦 = 𝑧))
318311, 313, 3173imtr4g 285 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} → 𝑦 ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
319318con3d 148 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → (¬ 𝑦 ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} → ¬ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
320319impr 648 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ (𝑦𝑆 ∧ ¬ 𝑦 ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) → ¬ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})
321296, 320sylan2b 492 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) → ¬ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})
322295, 321eldifd 3570 . . . . . . . . . . 11 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) → ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
323322ralrimiva 2961 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ∀𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
324292, 323jca 554 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∧ ∀𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))
325 eleq2 2687 . . . . . . . . . . 11 (𝑥 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → ((𝑃 − 1) ∈ 𝑥 ↔ (𝑃 − 1) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))
326 eleq2 2687 . . . . . . . . . . . 12 (𝑥 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥 ↔ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))
327326raleqbi1dv 3138 . . . . . . . . . . 11 (𝑥 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → (∀𝑦𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥 ↔ ∀𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))
328325, 327anbi12d 746 . . . . . . . . . 10 (𝑥 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → (((𝑃 − 1) ∈ 𝑥 ∧ ∀𝑦𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥) ↔ ((𝑃 − 1) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∧ ∀𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))))
329328, 7elrab2 3352 . . . . . . . . 9 ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ 𝐴 ↔ ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ 𝒫 (1...(𝑃 − 1)) ∧ ((𝑃 − 1) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∧ ∀𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))))
330233, 324, 329sylanbrc 697 . . . . . . . 8 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ 𝐴)
331 wilthlem2.r . . . . . . . . 9 (𝜑 → ∀𝑠𝐴 (𝑠𝑆 → ((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))
332331adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ∀𝑠𝐴 (𝑠𝑆 → ((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))
333 sseqin2 3800 . . . . . . . . . . 11 ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ⊆ 𝑆 ↔ (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) = {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})
33499, 333sylib 208 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) = {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})
335 vex 3192 . . . . . . . . . . . 12 𝑧 ∈ V
336335prnz 4285 . . . . . . . . . . 11 {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ≠ ∅
337336a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ≠ ∅)
338334, 337eqnetrd 2857 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ≠ ∅)
339 disj4 4002 . . . . . . . . . 10 ((𝑆 ∩ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) = ∅ ↔ ¬ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊊ 𝑆)
340339necon2abii 2840 . . . . . . . . 9 ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊊ 𝑆 ↔ (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ≠ ∅)
341338, 340sylibr 224 . . . . . . . 8 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊊ 𝑆)
342 psseq1 3677 . . . . . . . . . 10 (𝑠 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → (𝑠𝑆 ↔ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊊ 𝑆))
343 reseq2 5356 . . . . . . . . . . . . 13 (𝑠 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → ( I ↾ 𝑠) = ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))
344343oveq2d 6626 . . . . . . . . . . . 12 (𝑠 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → (𝑇 Σg ( I ↾ 𝑠)) = (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))))
345344oveq1d 6625 . . . . . . . . . . 11 (𝑠 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → ((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = ((𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) mod 𝑃))
346345eqeq1d 2623 . . . . . . . . . 10 (𝑠 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → (((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃) ↔ ((𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) mod 𝑃) = (-1 mod 𝑃)))
347342, 346imbi12d 334 . . . . . . . . 9 (𝑠 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → ((𝑠𝑆 → ((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ↔ ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊊ 𝑆 → ((𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) mod 𝑃) = (-1 mod 𝑃))))
348347rspcv 3294 . . . . . . . 8 ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ 𝐴 → (∀𝑠𝐴 (𝑠𝑆 → ((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) → ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊊ 𝑆 → ((𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) mod 𝑃) = (-1 mod 𝑃))))
349330, 332, 341, 348syl3c 66 . . . . . . 7 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) mod 𝑃) = (-1 mod 𝑃))
350230, 349eqtrd 2655 . . . . . 6 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((1 · (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) mod 𝑃) = (-1 mod 𝑃))
351113, 227, 3503eqtrd 2659 . . . . 5 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑇 Σg ( I ↾ 𝑆)) mod 𝑃) = (-1 mod 𝑃))
352351ex 450 . . . 4 (𝜑 → ((𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)}) → ((𝑇 Σg ( I ↾ 𝑆)) mod 𝑃) = (-1 mod 𝑃)))
353352exlimdv 1858 . . 3 (𝜑 → (∃𝑧(𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)}) → ((𝑇 Σg ( I ↾ 𝑆)) mod 𝑃) = (-1 mod 𝑃)))
35457, 353syl5bi 232 . 2 (𝜑 → (¬ 𝑆 ⊆ {(𝑃 − 1)} → ((𝑇 Σg ( I ↾ 𝑆)) mod 𝑃) = (-1 mod 𝑃)))
35556, 354pm2.61d 170 1 (𝜑 → ((𝑇 Σg ( I ↾ 𝑆)) mod 𝑃) = (-1 mod 𝑃))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   = wceq 1480  ∃wex 1701   ∈ wcel 1987   ≠ wne 2790  ∀wral 2907  {crab 2911  Vcvv 3189   ∖ cdif 3556   ∪ cun 3557   ∩ cin 3558   ⊆ wss 3559   ⊊ wpss 3560  ∅c0 3896  𝒫 cpw 4135  {csn 4153  {cpr 4155   class class class wbr 4618   ↦ cmpt 4678   I cid 4989   ↾ cres 5081  ⟶wf 5848  –1-1-onto→wf1o 5851  ‘cfv 5852  (class class class)co 6610  Fincfn 7906   finSupp cfsupp 8226  ℂcc 9885  ℝcr 9886  0cc0 9887  1c1 9888   + caddc 9890   · cmul 9892   − cmin 10217  -cneg 10218  ℕcn 10971  2c2 11021  ℕ0cn0 11243  ℤcz 11328  ℤ≥cuz 11638  ℝ+crp 11783  ...cfz 12275   mod cmo 12615  ↑cexp 12807   ∥ cdvds 14914  ℙcprime 15316   Σg cgsu 16029  Mndcmnd 17222  SubMndcsubmnd 17262  CMndccmn 18121  mulGrpcmgp 18417  Ringcrg 18475  CRingccrg 18476  SubRingcsubrg 18704  ℂfldccnfld 19674 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-inf2 8489  ax-cnex 9943  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964  ax-pre-sup 9965  ax-addf 9966  ax-mulf 9967 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-iin 4493  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-of 6857  df-om 7020  df-1st 7120  df-2nd 7121  df-supp 7248  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-2o 7513  df-oadd 7516  df-er 7694  df-map 7811  df-en 7907  df-dom 7908  df-sdom 7909  df-fin 7910  df-fsupp 8227  df-sup 8299  df-inf 8300  df-oi 8366  df-card 8716  df-cda 8941  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-div 10636  df-nn 10972  df-2 11030  df-3 11031  df-4 11032  df-5 11033  df-6 11034  df-7 11035  df-8 11036  df-9 11037  df-n0 11244  df-xnn0 11315  df-z 11329  df-dec 11445  df-uz 11639  df-rp 11784  df-fz 12276  df-fzo 12414  df-fl 12540  df-mod 12616  df-seq 12749  df-exp 12808  df-hash 13065  df-cj 13780  df-re 13781  df-im 13782  df-sqrt 13916  df-abs 13917  df-dvds 14915  df-gcd 15148  df-prm 15317  df-phi 15402  df-struct 15790  df-ndx 15791  df-slot 15792  df-base 15793  df-sets 15794  df-ress 15795  df-plusg 15882  df-mulr 15883  df-starv 15884  df-tset 15888  df-ple 15889  df-ds 15892  df-unif 15893  df-0g 16030  df-gsum 16031  df-mre 16174  df-mrc 16175  df-acs 16177  df-mgm 17170  df-sgrp 17212  df-mnd 17223  df-submnd 17264  df-grp 17353  df-minusg 17354  df-mulg 17469  df-subg 17519  df-cntz 17678  df-cmn 18123  df-mgp 18418  df-ur 18430  df-ring 18477  df-cring 18478  df-subrg 18706  df-cnfld 19675 This theorem is referenced by:  wilthlem3  24709
 Copyright terms: Public domain W3C validator