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

Theorem wilthlem2 25638
 Description: Lemma for wilth 25640: 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 25637 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 487 . . . . . . . . 9 ((𝜑𝑆 ⊆ {(𝑃 − 1)}) → 𝑆 ⊆ {(𝑃 − 1)})
2 wilthlem2.s . . . . . . . . . . . . . 14 (𝜑𝑆𝐴)
3 eleq2 2899 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑆 → ((𝑃 − 1) ∈ 𝑥 ↔ (𝑃 − 1) ∈ 𝑆))
4 eleq2 2899 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑆 → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥 ↔ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆))
54raleqbi1dv 3402 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑆 → (∀𝑦𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥 ↔ ∀𝑦𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆))
63, 5anbi12d 632 . . . . . . . . . . . . . . 15 (𝑥 = 𝑆 → (((𝑃 − 1) ∈ 𝑥 ∧ ∀𝑦𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥) ↔ ((𝑃 − 1) ∈ 𝑆 ∧ ∀𝑦𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)))
7 wilthlem.a . . . . . . . . . . . . . . 15 𝐴 = {𝑥 ∈ 𝒫 (1...(𝑃 − 1)) ∣ ((𝑃 − 1) ∈ 𝑥 ∧ ∀𝑦𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥)}
86, 7elrab2 3681 . . . . . . . . . . . . . 14 (𝑆𝐴 ↔ (𝑆 ∈ 𝒫 (1...(𝑃 − 1)) ∧ ((𝑃 − 1) ∈ 𝑆 ∧ ∀𝑦𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)))
92, 8sylib 220 . . . . . . . . . . . . 13 (𝜑 → (𝑆 ∈ 𝒫 (1...(𝑃 − 1)) ∧ ((𝑃 − 1) ∈ 𝑆 ∧ ∀𝑦𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)))
109simprd 498 . . . . . . . . . . . 12 (𝜑 → ((𝑃 − 1) ∈ 𝑆 ∧ ∀𝑦𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆))
1110simpld 497 . . . . . . . . . . 11 (𝜑 → (𝑃 − 1) ∈ 𝑆)
1211snssd 4734 . . . . . . . . . 10 (𝜑 → {(𝑃 − 1)} ⊆ 𝑆)
1312adantr 483 . . . . . . . . 9 ((𝜑𝑆 ⊆ {(𝑃 − 1)}) → {(𝑃 − 1)} ⊆ 𝑆)
141, 13eqssd 3982 . . . . . . . 8 ((𝜑𝑆 ⊆ {(𝑃 − 1)}) → 𝑆 = {(𝑃 − 1)})
1514reseq2d 5846 . . . . . . 7 ((𝜑𝑆 ⊆ {(𝑃 − 1)}) → ( I ↾ 𝑆) = ( I ↾ {(𝑃 − 1)}))
16 mptresid 5911 . . . . . . 7 ( I ↾ {(𝑃 − 1)}) = (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)
1715, 16syl6eq 2870 . . . . . 6 ((𝜑𝑆 ⊆ {(𝑃 − 1)}) → ( I ↾ 𝑆) = (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧))
1817oveq2d 7164 . . . . 5 ((𝜑𝑆 ⊆ {(𝑃 − 1)}) → (𝑇 Σg ( I ↾ 𝑆)) = (𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)))
1918oveq1d 7163 . . . 4 ((𝜑𝑆 ⊆ {(𝑃 − 1)}) → ((𝑇 Σg ( I ↾ 𝑆)) mod 𝑃) = ((𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) mod 𝑃))
20 wilthlem2.p . . . . . . . . . . . 12 (𝜑𝑃 ∈ ℙ)
21 prmnn 16010 . . . . . . . . . . . 12 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
2220, 21syl 17 . . . . . . . . . . 11 (𝜑𝑃 ∈ ℕ)
2322nncnd 11646 . . . . . . . . . 10 (𝜑𝑃 ∈ ℂ)
24 ax-1cn 10587 . . . . . . . . . 10 1 ∈ ℂ
25 negsub 10926 . . . . . . . . . 10 ((𝑃 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑃 + -1) = (𝑃 − 1))
2623, 24, 25sylancl 588 . . . . . . . . 9 (𝜑 → (𝑃 + -1) = (𝑃 − 1))
27 neg1cn 11743 . . . . . . . . . 10 -1 ∈ ℂ
28 addcom 10818 . . . . . . . . . 10 ((𝑃 ∈ ℂ ∧ -1 ∈ ℂ) → (𝑃 + -1) = (-1 + 𝑃))
2923, 27, 28sylancl 588 . . . . . . . . 9 (𝜑 → (𝑃 + -1) = (-1 + 𝑃))
3026, 29eqtr3d 2856 . . . . . . . 8 (𝜑 → (𝑃 − 1) = (-1 + 𝑃))
31 cnring 20559 . . . . . . . . . 10 fld ∈ Ring
32 wilthlem.t . . . . . . . . . . 11 𝑇 = (mulGrp‘ℂfld)
3332ringmgp 19295 . . . . . . . . . 10 (ℂfld ∈ Ring → 𝑇 ∈ Mnd)
3431, 33mp1i 13 . . . . . . . . 9 (𝜑𝑇 ∈ Mnd)
35 nnm1nn0 11930 . . . . . . . . . . 11 (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ0)
3622, 35syl 17 . . . . . . . . . 10 (𝜑 → (𝑃 − 1) ∈ ℕ0)
3736nn0cnd 11949 . . . . . . . . 9 (𝜑 → (𝑃 − 1) ∈ ℂ)
38 cnfldbas 20541 . . . . . . . . . . 11 ℂ = (Base‘ℂfld)
3932, 38mgpbas 19237 . . . . . . . . . 10 ℂ = (Base‘𝑇)
40 id 22 . . . . . . . . . 10 (𝑧 = (𝑃 − 1) → 𝑧 = (𝑃 − 1))
4139, 40gsumsn 19066 . . . . . . . . 9 ((𝑇 ∈ Mnd ∧ (𝑃 − 1) ∈ ℂ ∧ (𝑃 − 1) ∈ ℂ) → (𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) = (𝑃 − 1))
4234, 37, 37, 41syl3anc 1365 . . . . . . . 8 (𝜑 → (𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) = (𝑃 − 1))
4323mulid2d 10651 . . . . . . . . 9 (𝜑 → (1 · 𝑃) = 𝑃)
4443oveq2d 7164 . . . . . . . 8 (𝜑 → (-1 + (1 · 𝑃)) = (-1 + 𝑃))
4530, 42, 443eqtr4d 2864 . . . . . . 7 (𝜑 → (𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) = (-1 + (1 · 𝑃)))
4645oveq1d 7163 . . . . . 6 (𝜑 → ((𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) mod 𝑃) = ((-1 + (1 · 𝑃)) mod 𝑃))
47 neg1rr 11744 . . . . . . . 8 -1 ∈ ℝ
4847a1i 11 . . . . . . 7 (𝜑 → -1 ∈ ℝ)
4922nnrpd 12421 . . . . . . 7 (𝜑𝑃 ∈ ℝ+)
50 1zzd 12005 . . . . . . 7 (𝜑 → 1 ∈ ℤ)
51 modcyc 13266 . . . . . . 7 ((-1 ∈ ℝ ∧ 𝑃 ∈ ℝ+ ∧ 1 ∈ ℤ) → ((-1 + (1 · 𝑃)) mod 𝑃) = (-1 mod 𝑃))
5248, 49, 50, 51syl3anc 1365 . . . . . 6 (𝜑 → ((-1 + (1 · 𝑃)) mod 𝑃) = (-1 mod 𝑃))
5346, 52eqtrd 2854 . . . . 5 (𝜑 → ((𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) mod 𝑃) = (-1 mod 𝑃))
5453adantr 483 . . . 4 ((𝜑𝑆 ⊆ {(𝑃 − 1)}) → ((𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) mod 𝑃) = (-1 mod 𝑃))
5519, 54eqtrd 2854 . . 3 ((𝜑𝑆 ⊆ {(𝑃 − 1)}) → ((𝑇 Σg ( I ↾ 𝑆)) mod 𝑃) = (-1 mod 𝑃))
5655ex 415 . 2 (𝜑 → (𝑆 ⊆ {(𝑃 − 1)} → ((𝑇 Σg ( I ↾ 𝑆)) mod 𝑃) = (-1 mod 𝑃)))
57 nss 4027 . . 3 𝑆 ⊆ {(𝑃 − 1)} ↔ ∃𝑧(𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)}))
58 cnfld1 20562 . . . . . . . . . 10 1 = (1r‘ℂfld)
5932, 58ringidval 19245 . . . . . . . . 9 1 = (0g𝑇)
60 cnfldmul 20543 . . . . . . . . . 10 · = (.r‘ℂfld)
6132, 60mgpplusg 19235 . . . . . . . . 9 · = (+g𝑇)
62 cncrng 20558 . . . . . . . . . . 11 fld ∈ CRing
6332crngmgp 19297 . . . . . . . . . . 11 (ℂfld ∈ CRing → 𝑇 ∈ CMnd)
6462, 63ax-mp 5 . . . . . . . . . 10 𝑇 ∈ CMnd
6564a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑇 ∈ CMnd)
662adantr 483 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑆𝐴)
67 f1oi 6645 . . . . . . . . . . . 12 ( I ↾ 𝑆):𝑆1-1-onto𝑆
68 f1of 6608 . . . . . . . . . . . 12 (( I ↾ 𝑆):𝑆1-1-onto𝑆 → ( I ↾ 𝑆):𝑆𝑆)
6967, 68ax-mp 5 . . . . . . . . . . 11 ( I ↾ 𝑆):𝑆𝑆
709simpld 497 . . . . . . . . . . . . . 14 (𝜑𝑆 ∈ 𝒫 (1...(𝑃 − 1)))
7170elpwid 4551 . . . . . . . . . . . . 13 (𝜑𝑆 ⊆ (1...(𝑃 − 1)))
72 fzssz 12901 . . . . . . . . . . . . 13 (1...(𝑃 − 1)) ⊆ ℤ
7371, 72sstrdi 3977 . . . . . . . . . . . 12 (𝜑𝑆 ⊆ ℤ)
74 zsscn 11981 . . . . . . . . . . . 12 ℤ ⊆ ℂ
7573, 74sstrdi 3977 . . . . . . . . . . 11 (𝜑𝑆 ⊆ ℂ)
76 fss 6520 . . . . . . . . . . 11 ((( I ↾ 𝑆):𝑆𝑆𝑆 ⊆ ℂ) → ( I ↾ 𝑆):𝑆⟶ℂ)
7769, 75, 76sylancr 589 . . . . . . . . . 10 (𝜑 → ( I ↾ 𝑆):𝑆⟶ℂ)
7877adantr 483 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ( I ↾ 𝑆):𝑆⟶ℂ)
79 fzfi 13332 . . . . . . . . . . . 12 (1...(𝑃 − 1)) ∈ Fin
80 ssfi 8730 . . . . . . . . . . . 12 (((1...(𝑃 − 1)) ∈ Fin ∧ 𝑆 ⊆ (1...(𝑃 − 1))) → 𝑆 ∈ Fin)
8179, 71, 80sylancr 589 . . . . . . . . . . 11 (𝜑𝑆 ∈ Fin)
82 1ex 10629 . . . . . . . . . . . 12 1 ∈ V
8382a1i 11 . . . . . . . . . . 11 (𝜑 → 1 ∈ V)
8477, 81, 83fdmfifsupp 8835 . . . . . . . . . 10 (𝜑 → ( I ↾ 𝑆) finSupp 1)
8584adantr 483 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ( I ↾ 𝑆) finSupp 1)
86 disjdif 4419 . . . . . . . . . 10 ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∩ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = ∅
8786a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∩ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = ∅)
88 undif2 4423 . . . . . . . . . 10 ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∪ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∪ 𝑆)
89 simprl 769 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑧𝑆)
90 oveq1 7155 . . . . . . . . . . . . . . 15 (𝑦 = 𝑧 → (𝑦↑(𝑃 − 2)) = (𝑧↑(𝑃 − 2)))
9190oveq1d 7163 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 → ((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃))
9291eleq1d 2895 . . . . . . . . . . . . 13 (𝑦 = 𝑧 → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆 ↔ ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆))
9310simprd 498 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑦𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)
9493adantr 483 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ∀𝑦𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)
9592, 94, 89rspcdva 3623 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)
9689, 95prssd 4747 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ⊆ 𝑆)
97 ssequn1 4154 . . . . . . . . . . 11 ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ⊆ 𝑆 ↔ ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∪ 𝑆) = 𝑆)
9896, 97sylib 220 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∪ 𝑆) = 𝑆)
9988, 98syl5req 2867 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑆 = ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∪ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))
10039, 59, 61, 65, 66, 78, 85, 87, 99gsumsplit 19040 . . . . . . . 8 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg ( I ↾ 𝑆)) = ((𝑇 Σg (( I ↾ 𝑆) ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg (( I ↾ 𝑆) ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))))
10196resabs1d 5877 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (( I ↾ 𝑆) ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) = ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
102101oveq2d 7164 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg (( I ↾ 𝑆) ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = (𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))
103 difss 4106 . . . . . . . . . . . 12 (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ 𝑆
104 resabs1 5876 . . . . . . . . . . . 12 ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ 𝑆 → (( I ↾ 𝑆) ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))
105103, 104ax-mp 5 . . . . . . . . . . 11 (( I ↾ 𝑆) ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
106105oveq2i 7159 . . . . . . . . . 10 (𝑇 Σg (( I ↾ 𝑆) ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) = (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))
107106a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg (( I ↾ 𝑆) ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) = (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))))
108102, 107oveq12d 7166 . . . . . . . 8 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑇 Σg (( I ↾ 𝑆) ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg (( I ↾ 𝑆) ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) = ((𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))))
109100, 108eqtrd 2854 . . . . . . 7 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg ( I ↾ 𝑆)) = ((𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))))
110109oveq1d 7163 . . . . . 6 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑇 Σg ( I ↾ 𝑆)) mod 𝑃) = (((𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) mod 𝑃))
111 prfi 8785 . . . . . . . . . 10 {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∈ Fin
112111a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∈ Fin)
113 zsubrg 20590 . . . . . . . . . 10 ℤ ∈ (SubRing‘ℂfld)
11432subrgsubm 19540 . . . . . . . . . 10 (ℤ ∈ (SubRing‘ℂfld) → ℤ ∈ (SubMnd‘𝑇))
115113, 114mp1i 13 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ℤ ∈ (SubMnd‘𝑇))
116 f1oi 6645 . . . . . . . . . . 11 ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}–1-1-onto→{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}
117 f1of 6608 . . . . . . . . . . 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 483 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑆 ⊆ ℤ)
12096, 119sstrd 3975 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ⊆ ℤ)
121 fss 6520 . . . . . . . . . 10 ((( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}⟶{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∧ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ⊆ ℤ) → ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}⟶ℤ)
122118, 120, 121sylancr 589 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}⟶ℤ)
12382a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 1 ∈ V)
124122, 112, 123fdmfifsupp 8835 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) finSupp 1)
12559, 65, 112, 115, 122, 124gsumsubmcl 19031 . . . . . . . 8 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) ∈ ℤ)
126125zred 12079 . . . . . . 7 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) ∈ ℝ)
127 1red 10634 . . . . . . 7 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 1 ∈ ℝ)
12871adantr 483 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑆 ⊆ (1...(𝑃 − 1)))
129128ssdifssd 4117 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ (1...(𝑃 − 1)))
130 ssfi 8730 . . . . . . . . 9 (((1...(𝑃 − 1)) ∈ Fin ∧ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ (1...(𝑃 − 1))) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ Fin)
13179, 129, 130sylancr 589 . . . . . . . 8 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ Fin)
132 f1oi 6645 . . . . . . . . . 10 ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})):(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})–1-1-onto→(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})
133 f1of 6608 . . . . . . . . . 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 4117 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ ℤ)
136 fss 6520 . . . . . . . . 9 ((( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})):(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})⟶(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∧ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ ℤ) → ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})):(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})⟶ℤ)
137134, 135, 136sylancr 589 . . . . . . . 8 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})):(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})⟶ℤ)
138137, 131, 123fdmfifsupp 8835 . . . . . . . 8 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) finSupp 1)
13959, 65, 131, 115, 137, 138gsumsubmcl 19031 . . . . . . 7 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) ∈ ℤ)
14049adantr 483 . . . . . . 7 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∈ ℝ+)
14134adantr 483 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑇 ∈ Mnd)
14275adantr 483 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑆 ⊆ ℂ)
143142, 89sseldd 3966 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑧 ∈ ℂ)
144 id 22 . . . . . . . . . . . . 13 (𝑤 = 𝑧𝑤 = 𝑧)
14539, 144gsumsn 19066 . . . . . . . . . . . 12 ((𝑇 ∈ Mnd ∧ 𝑧 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) = 𝑧)
146141, 143, 143, 145syl3anc 1365 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) = 𝑧)
147146adantr 483 . . . . . . . . . 10 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → (𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) = 𝑧)
148 mptresid 5911 . . . . . . . . . . . 12 ( I ↾ {𝑧}) = (𝑤 ∈ {𝑧} ↦ 𝑤)
149 dfsn2 4572 . . . . . . . . . . . . . 14 {𝑧} = {𝑧, 𝑧}
150 animorrl 976 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → (𝑧 = 1 ∨ 𝑧 = (𝑃 − 1)))
15120adantr 483 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∈ ℙ)
152128, 89sseldd 3966 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑧 ∈ (1...(𝑃 − 1)))
153 wilthlem1 25637 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ ℙ ∧ 𝑧 ∈ (1...(𝑃 − 1))) → (𝑧 = ((𝑧↑(𝑃 − 2)) mod 𝑃) ↔ (𝑧 = 1 ∨ 𝑧 = (𝑃 − 1))))
154151, 152, 153syl2anc 586 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑧 = ((𝑧↑(𝑃 − 2)) mod 𝑃) ↔ (𝑧 = 1 ∨ 𝑧 = (𝑃 − 1))))
155154biimpar 480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ (𝑧 = 1 ∨ 𝑧 = (𝑃 − 1))) → 𝑧 = ((𝑧↑(𝑃 − 2)) mod 𝑃))
156150, 155syldan 593 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → 𝑧 = ((𝑧↑(𝑃 − 2)) mod 𝑃))
157156preq2d 4668 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → {𝑧, 𝑧} = {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})
158149, 157syl5eq 2866 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → {𝑧} = {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})
159158reseq2d 5846 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → ( I ↾ {𝑧}) = ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
160148, 159syl5eqr 2868 . . . . . . . . . . 11 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → (𝑤 ∈ {𝑧} ↦ 𝑤) = ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
161160oveq2d 7164 . . . . . . . . . 10 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → (𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) = (𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))
162 simpr 487 . . . . . . . . . 10 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → 𝑧 = 1)
163147, 161, 1623eqtr3d 2862 . . . . . . . . 9 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → (𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = 1)
164163oveq1d 7163 . . . . . . . 8 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → ((𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) mod 𝑃) = (1 mod 𝑃))
165 df-pr 4562 . . . . . . . . . . . . . . 15 {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} = ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)})
166165reseq2i 5843 . . . . . . . . . . . . . 14 ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) = ( I ↾ ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)}))
167 mptresid 5911 . . . . . . . . . . . . . 14 ( I ↾ ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)})) = (𝑤 ∈ ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)}) ↦ 𝑤)
168166, 167eqtri 2842 . . . . . . . . . . . . 13 ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) = (𝑤 ∈ ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)}) ↦ 𝑤)
169168oveq2i 7159 . . . . . . . . . . . 12 (𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = (𝑇 Σg (𝑤 ∈ ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)}) ↦ 𝑤))
17064a1i 11 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → 𝑇 ∈ CMnd)
171 snfi 8586 . . . . . . . . . . . . . 14 {𝑧} ∈ Fin
172171a1i 11 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → {𝑧} ∈ Fin)
173 elsni 4576 . . . . . . . . . . . . . . . 16 (𝑤 ∈ {𝑧} → 𝑤 = 𝑧)
174173adantl 484 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑤 ∈ {𝑧}) → 𝑤 = 𝑧)
175143adantr 483 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑤 ∈ {𝑧}) → 𝑧 ∈ ℂ)
176174, 175eqeltrd 2911 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑤 ∈ {𝑧}) → 𝑤 ∈ ℂ)
177176adantlr 713 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) ∧ 𝑤 ∈ {𝑧}) → 𝑤 ∈ ℂ)
178142, 95sseldd 3966 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ ℂ)
179178adantr 483 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ ℂ)
180 simprr 771 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ 𝑧 ∈ {(𝑃 − 1)})
181 velsn 4575 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ {(𝑃 − 1)} ↔ 𝑧 = (𝑃 − 1))
182180, 181sylnib 330 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ 𝑧 = (𝑃 − 1))
183 biorf 932 . . . . . . . . . . . . . . . . 17 𝑧 = (𝑃 − 1) → (𝑧 = 1 ↔ (𝑧 = (𝑃 − 1) ∨ 𝑧 = 1)))
184182, 183syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑧 = 1 ↔ (𝑧 = (𝑃 − 1) ∨ 𝑧 = 1)))
185 ovex 7181 . . . . . . . . . . . . . . . . . . 19 ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ V
186185elsn 4574 . . . . . . . . . . . . . . . . . 18 (((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧} ↔ ((𝑧↑(𝑃 − 2)) mod 𝑃) = 𝑧)
187 eqcom 2826 . . . . . . . . . . . . . . . . . 18 (((𝑧↑(𝑃 − 2)) mod 𝑃) = 𝑧𝑧 = ((𝑧↑(𝑃 − 2)) mod 𝑃))
188186, 187bitri 277 . . . . . . . . . . . . . . . . 17 (((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧} ↔ 𝑧 = ((𝑧↑(𝑃 − 2)) mod 𝑃))
189 orcom 866 . . . . . . . . . . . . . . . . 17 ((𝑧 = (𝑃 − 1) ∨ 𝑧 = 1) ↔ (𝑧 = 1 ∨ 𝑧 = (𝑃 − 1)))
190154, 188, 1893bitr4g 316 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧} ↔ (𝑧 = (𝑃 − 1) ∨ 𝑧 = 1)))
191184, 190bitr4d 284 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑧 = 1 ↔ ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧}))
192191necon3abid 3050 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑧 ≠ 1 ↔ ¬ ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧}))
193192biimpa 479 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → ¬ ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧})
194 id 22 . . . . . . . . . . . . 13 (𝑤 = ((𝑧↑(𝑃 − 2)) mod 𝑃) → 𝑤 = ((𝑧↑(𝑃 − 2)) mod 𝑃))
19539, 61, 170, 172, 177, 179, 193, 179, 194gsumunsn 19072 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → (𝑇 Σg (𝑤 ∈ ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)}) ↦ 𝑤)) = ((𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) · ((𝑧↑(𝑃 − 2)) mod 𝑃)))
196169, 195syl5eq 2866 . . . . . . . . . . 11 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → (𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = ((𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) · ((𝑧↑(𝑃 − 2)) mod 𝑃)))
197146adantr 483 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → (𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) = 𝑧)
198197oveq1d 7163 . . . . . . . . . . 11 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → ((𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) · ((𝑧↑(𝑃 − 2)) mod 𝑃)) = (𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)))
199196, 198eqtrd 2854 . . . . . . . . . 10 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → (𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = (𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)))
200199oveq1d 7163 . . . . . . . . 9 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → ((𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) mod 𝑃) = ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) mod 𝑃))
201 elfzelz 12900 . . . . . . . . . . . . . 14 (𝑧 ∈ (1...(𝑃 − 1)) → 𝑧 ∈ ℤ)
202152, 201syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑧 ∈ ℤ)
20322adantr 483 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∈ ℕ)
204 fzm1ndvds 15664 . . . . . . . . . . . . . 14 ((𝑃 ∈ ℕ ∧ 𝑧 ∈ (1...(𝑃 − 1))) → ¬ 𝑃𝑧)
205203, 152, 204syl2anc 586 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ 𝑃𝑧)
206 eqid 2819 . . . . . . . . . . . . . 14 ((𝑧↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃)
207206prmdiv 16114 . . . . . . . . . . . . 13 ((𝑃 ∈ ℙ ∧ 𝑧 ∈ ℤ ∧ ¬ 𝑃𝑧) → (((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) − 1)))
208151, 202, 205, 207syl3anc 1365 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) − 1)))
209208simprd 498 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∥ ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) − 1))
210 elfznn 12928 . . . . . . . . . . . . . . 15 (𝑧 ∈ (1...(𝑃 − 1)) → 𝑧 ∈ ℕ)
211152, 210syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑧 ∈ ℕ)
212128, 95sseldd 3966 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)))
213 elfznn 12928 . . . . . . . . . . . . . . 15 (((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ ℕ)
214212, 213syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ ℕ)
215211, 214nnmulcld 11682 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) ∈ ℕ)
216215nnzd 12078 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) ∈ ℤ)
217 1zzd 12005 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 1 ∈ ℤ)
218 moddvds 15610 . . . . . . . . . . . 12 ((𝑃 ∈ ℕ ∧ (𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) ∈ ℤ ∧ 1 ∈ ℤ) → (((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) − 1)))
219203, 216, 217, 218syl3anc 1365 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) − 1)))
220209, 219mpbird 259 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = (1 mod 𝑃))
221220adantr 483 . . . . . . . . 9 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = (1 mod 𝑃))
222200, 221eqtrd 2854 . . . . . . . 8 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → ((𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) mod 𝑃) = (1 mod 𝑃))
223164, 222pm2.61dane 3102 . . . . . . 7 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) mod 𝑃) = (1 mod 𝑃))
224 modmul1 13284 . . . . . . 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 𝑃))
225126, 127, 139, 140, 223, 224syl221anc 1375 . . . . . 6 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) mod 𝑃) = ((1 · (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) mod 𝑃))
226139zcnd 12080 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) ∈ ℂ)
227226mulid2d 10651 . . . . . . . 8 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (1 · (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) = (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))))
228227oveq1d 7163 . . . . . . 7 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((1 · (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) mod 𝑃) = ((𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) mod 𝑃))
229 sseqin2 4190 . . . . . . . . . . 11 ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ⊆ 𝑆 ↔ (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) = {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})
23096, 229sylib 220 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) = {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})
231 vex 3496 . . . . . . . . . . . 12 𝑧 ∈ V
232231prnz 4704 . . . . . . . . . . 11 {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ≠ ∅
233232a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ≠ ∅)
234230, 233eqnetrd 3081 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ≠ ∅)
235 disj4 4406 . . . . . . . . . 10 ((𝑆 ∩ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) = ∅ ↔ ¬ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊊ 𝑆)
236235necon2abii 3064 . . . . . . . . 9 ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊊ 𝑆 ↔ (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ≠ ∅)
237234, 236sylibr 236 . . . . . . . 8 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊊ 𝑆)
238 psseq1 4062 . . . . . . . . . 10 (𝑠 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → (𝑠𝑆 ↔ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊊ 𝑆))
239 reseq2 5841 . . . . . . . . . . . . 13 (𝑠 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → ( I ↾ 𝑠) = ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))
240239oveq2d 7164 . . . . . . . . . . . 12 (𝑠 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → (𝑇 Σg ( I ↾ 𝑠)) = (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))))
241240oveq1d 7163 . . . . . . . . . . 11 (𝑠 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → ((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = ((𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) mod 𝑃))
242241eqeq1d 2821 . . . . . . . . . 10 (𝑠 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → (((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃) ↔ ((𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) mod 𝑃) = (-1 mod 𝑃)))
243238, 242imbi12d 347 . . . . . . . . 9 (𝑠 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → ((𝑠𝑆 → ((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ↔ ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊊ 𝑆 → ((𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) mod 𝑃) = (-1 mod 𝑃))))
244 wilthlem2.r . . . . . . . . . 10 (𝜑 → ∀𝑠𝐴 (𝑠𝑆 → ((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))
245244adantr 483 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ∀𝑠𝐴 (𝑠𝑆 → ((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))
246 ovex 7181 . . . . . . . . . . . 12 (1...(𝑃 − 1)) ∈ V
247246elpw2 5239 . . . . . . . . . . 11 ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ 𝒫 (1...(𝑃 − 1)) ↔ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ (1...(𝑃 − 1)))
248129, 247sylibr 236 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ 𝒫 (1...(𝑃 − 1)))
24911adantr 483 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ 𝑆)
250 eqcom 2826 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑃 − 1) ↔ (𝑃 − 1) = 𝑧)
251181, 250bitri 277 . . . . . . . . . . . . . . 15 (𝑧 ∈ {(𝑃 − 1)} ↔ (𝑃 − 1) = 𝑧)
252180, 251sylnib 330 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ (𝑃 − 1) = 𝑧)
253 oveq1 7155 . . . . . . . . . . . . . . . . 17 ((𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃) → ((𝑃 − 1)↑(𝑃 − 2)) = (((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)))
254253oveq1d 7163 . . . . . . . . . . . . . . . 16 ((𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃) → (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃) = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃))
255203, 35syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ ℕ0)
256 nn0uz 12272 . . . . . . . . . . . . . . . . . . . 20 0 = (ℤ‘0)
257255, 256eleqtrdi 2921 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ (ℤ‘0))
258 eluzfz2 12907 . . . . . . . . . . . . . . . . . . 19 ((𝑃 − 1) ∈ (ℤ‘0) → (𝑃 − 1) ∈ (0...(𝑃 − 1)))
259257, 258syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ (0...(𝑃 − 1)))
260 prmz 16011 . . . . . . . . . . . . . . . . . . . . 21 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
261151, 260syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∈ ℤ)
262119, 249sseldd 3966 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ ℤ)
263 1z 12004 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℤ
264 zsubcl 12016 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃 − 1) ∈ ℤ ∧ 1 ∈ ℤ) → ((𝑃 − 1) − 1) ∈ ℤ)
265262, 263, 264sylancl 588 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) − 1) ∈ ℤ)
266 dvdsmul1 15623 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ ℤ ∧ ((𝑃 − 1) − 1) ∈ ℤ) → 𝑃 ∥ (𝑃 · ((𝑃 − 1) − 1)))
267261, 265, 266syl2anc 586 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∥ (𝑃 · ((𝑃 − 1) − 1)))
268203nncnd 11646 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∈ ℂ)
269265zcnd 12080 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) − 1) ∈ ℂ)
270268, 269mulcld 10653 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 · ((𝑃 − 1) − 1)) ∈ ℂ)
271 1cnd 10628 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 1 ∈ ℂ)
272255nn0cnd 11949 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ ℂ)
273268, 271, 272subdird 11089 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) · (𝑃 − 1)) = ((𝑃 · (𝑃 − 1)) − (1 · (𝑃 − 1))))
274268, 272mulcld 10653 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 · (𝑃 − 1)) ∈ ℂ)
275274, 268, 271subsubd 11017 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 · (𝑃 − 1)) − (𝑃 − 1)) = (((𝑃 · (𝑃 − 1)) − 𝑃) + 1))
276272mulid2d 10651 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (1 · (𝑃 − 1)) = (𝑃 − 1))
277276oveq2d 7164 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 · (𝑃 − 1)) − (1 · (𝑃 − 1))) = ((𝑃 · (𝑃 − 1)) − (𝑃 − 1)))
278268, 272muls1d 11092 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 · ((𝑃 − 1) − 1)) = ((𝑃 · (𝑃 − 1)) − 𝑃))
279278oveq1d 7163 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 · ((𝑃 − 1) − 1)) + 1) = (((𝑃 · (𝑃 − 1)) − 𝑃) + 1))
280275, 277, 2793eqtr4d 2864 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 · (𝑃 − 1)) − (1 · (𝑃 − 1))) = ((𝑃 · ((𝑃 − 1) − 1)) + 1))
281273, 280eqtrd 2854 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) · (𝑃 − 1)) = ((𝑃 · ((𝑃 − 1) − 1)) + 1))
282270, 271, 281mvrraddd 11044 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑃 − 1) · (𝑃 − 1)) − 1) = (𝑃 · ((𝑃 − 1) − 1)))
283267, 282breqtrrd 5085 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∥ (((𝑃 − 1) · (𝑃 − 1)) − 1))
284128, 249sseldd 3966 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ (1...(𝑃 − 1)))
285 fzm1ndvds 15664 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ ℕ ∧ (𝑃 − 1) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (𝑃 − 1))
286203, 284, 285syl2anc 586 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ 𝑃 ∥ (𝑃 − 1))
287 eqid 2819 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃) = (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃)
288287prmdiveq 16115 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ ℙ ∧ (𝑃 − 1) ∈ ℤ ∧ ¬ 𝑃 ∥ (𝑃 − 1)) → (((𝑃 − 1) ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ (((𝑃 − 1) · (𝑃 − 1)) − 1)) ↔ (𝑃 − 1) = (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃)))
289151, 262, 286, 288syl3anc 1365 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑃 − 1) ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ (((𝑃 − 1) · (𝑃 − 1)) − 1)) ↔ (𝑃 − 1) = (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃)))
290259, 283, 289mpbi2and 710 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) = (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃))
291206prmdivdiv 16116 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ ℙ ∧ 𝑧 ∈ (1...(𝑃 − 1))) → 𝑧 = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃))
292151, 152, 291syl2anc 586 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑧 = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃))
293290, 292eqeq12d 2835 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) = 𝑧 ↔ (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃) = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃)))
294254, 293syl5ibr 248 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃) → (𝑃 − 1) = 𝑧))
295252, 294mtod 200 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ (𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃))
296 ioran 979 . . . . . . . . . . . . . 14 (¬ ((𝑃 − 1) = 𝑧 ∨ (𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃)) ↔ (¬ (𝑃 − 1) = 𝑧 ∧ ¬ (𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃)))
297252, 295, 296sylanbrc 585 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ ((𝑃 − 1) = 𝑧 ∨ (𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃)))
298 ovex 7181 . . . . . . . . . . . . . 14 (𝑃 − 1) ∈ V
299298elpr 4582 . . . . . . . . . . . . 13 ((𝑃 − 1) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ↔ ((𝑃 − 1) = 𝑧 ∨ (𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃)))
300297, 299sylnibr 331 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ (𝑃 − 1) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})
301249, 300eldifd 3945 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
302 eldifi 4101 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → 𝑦𝑆)
30394r19.21bi 3206 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)
304302, 303sylan2 594 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) → ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)
305 eldif 3944 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ↔ (𝑦𝑆 ∧ ¬ 𝑦 ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
306151adantr 483 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → 𝑃 ∈ ℙ)
307128sselda 3965 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → 𝑦 ∈ (1...(𝑃 − 1)))
308 eqid 2819 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑦↑(𝑃 − 2)) mod 𝑃)
309308prmdivdiv 16116 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ ℙ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → 𝑦 = ((((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃))
310306, 307, 309syl2anc 586 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → 𝑦 = ((((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃))
311 oveq1 7155 . . . . . . . . . . . . . . . . . . . . 21 (((𝑦↑(𝑃 − 2)) mod 𝑃) = 𝑧 → (((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) = (𝑧↑(𝑃 − 2)))
312311oveq1d 7163 . . . . . . . . . . . . . . . . . . . 20 (((𝑦↑(𝑃 − 2)) mod 𝑃) = 𝑧 → ((((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃))
313312eqeq2d 2830 . . . . . . . . . . . . . . . . . . 19 (((𝑦↑(𝑃 − 2)) mod 𝑃) = 𝑧 → (𝑦 = ((((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃) ↔ 𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃)))
314310, 313syl5ibcom 247 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → (((𝑦↑(𝑃 − 2)) mod 𝑃) = 𝑧𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃)))
315 oveq1 7155 . . . . . . . . . . . . . . . . . . . 20 (((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃) → (((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) = (((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)))
316315oveq1d 7163 . . . . . . . . . . . . . . . . . . 19 (((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃) → ((((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃) = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃))
317292adantr 483 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → 𝑧 = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃))
318310, 317eqeq12d 2835 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → (𝑦 = 𝑧 ↔ ((((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃) = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃)))
319316, 318syl5ibr 248 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → (((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃) → 𝑦 = 𝑧))
320314, 319orim12d 960 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → ((((𝑦↑(𝑃 − 2)) mod 𝑃) = 𝑧 ∨ ((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃)) → (𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃) ∨ 𝑦 = 𝑧)))
321 ovex 7181 . . . . . . . . . . . . . . . . . 18 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ V
322321elpr 4582 . . . . . . . . . . . . . . . . 17 (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ↔ (((𝑦↑(𝑃 − 2)) mod 𝑃) = 𝑧 ∨ ((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃)))
323 vex 3496 . . . . . . . . . . . . . . . . . . 19 𝑦 ∈ V
324323elpr 4582 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ↔ (𝑦 = 𝑧𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃)))
325 orcom 866 . . . . . . . . . . . . . . . . . 18 ((𝑦 = 𝑧𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃)) ↔ (𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃) ∨ 𝑦 = 𝑧))
326324, 325bitri 277 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ↔ (𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃) ∨ 𝑦 = 𝑧))
327320, 322, 3263imtr4g 298 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} → 𝑦 ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
328327con3d 155 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → (¬ 𝑦 ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} → ¬ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
329328impr 457 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ (𝑦𝑆 ∧ ¬ 𝑦 ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) → ¬ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})
330305, 329sylan2b 595 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) → ¬ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})
331304, 330eldifd 3945 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) → ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
332331ralrimiva 3180 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ∀𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
333301, 332jca 514 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∧ ∀𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))
334 eleq2 2899 . . . . . . . . . . . 12 (𝑥 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → ((𝑃 − 1) ∈ 𝑥 ↔ (𝑃 − 1) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))
335 eleq2 2899 . . . . . . . . . . . . 13 (𝑥 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥 ↔ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))
336335raleqbi1dv 3402 . . . . . . . . . . . 12 (𝑥 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → (∀𝑦𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥 ↔ ∀𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))
337334, 336anbi12d 632 . . . . . . . . . . 11 (𝑥 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → (((𝑃 − 1) ∈ 𝑥 ∧ ∀𝑦𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥) ↔ ((𝑃 − 1) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∧ ∀𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))))
338337, 7elrab2 3681 . . . . . . . . . 10 ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ 𝐴 ↔ ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ 𝒫 (1...(𝑃 − 1)) ∧ ((𝑃 − 1) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∧ ∀𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))))
339248, 333, 338sylanbrc 585 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ 𝐴)
340243, 245, 339rspcdva 3623 . . . . . . . 8 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊊ 𝑆 → ((𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) mod 𝑃) = (-1 mod 𝑃)))
341237, 340mpd 15 . . . . . . 7 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) mod 𝑃) = (-1 mod 𝑃))
342228, 341eqtrd 2854 . . . . . 6 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((1 · (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) mod 𝑃) = (-1 mod 𝑃))
343110, 225, 3423eqtrd 2858 . . . . 5 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑇 Σg ( I ↾ 𝑆)) mod 𝑃) = (-1 mod 𝑃))
344343ex 415 . . . 4 (𝜑 → ((𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)}) → ((𝑇 Σg ( I ↾ 𝑆)) mod 𝑃) = (-1 mod 𝑃)))
345344exlimdv 1927 . . 3 (𝜑 → (∃𝑧(𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)}) → ((𝑇 Σg ( I ↾ 𝑆)) mod 𝑃) = (-1 mod 𝑃)))
34657, 345syl5bi 244 . 2 (𝜑 → (¬ 𝑆 ⊆ {(𝑃 − 1)} → ((𝑇 Σg ( I ↾ 𝑆)) mod 𝑃) = (-1 mod 𝑃)))
34756, 346pm2.61d 181 1 (𝜑 → ((𝑇 Σg ( I ↾ 𝑆)) mod 𝑃) = (-1 mod 𝑃))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   = wceq 1530  ∃wex 1773   ∈ wcel 2107   ≠ wne 3014  ∀wral 3136  {crab 3140  Vcvv 3493   ∖ cdif 3931   ∪ cun 3932   ∩ cin 3933   ⊆ wss 3934   ⊊ wpss 3935  ∅c0 4289  𝒫 cpw 4537  {csn 4559  {cpr 4561   class class class wbr 5057   ↦ cmpt 5137   I cid 5452   ↾ cres 5550  ⟶wf 6344  –1-1-onto→wf1o 6347  ‘cfv 6348  (class class class)co 7148  Fincfn 8501   finSupp cfsupp 8825  ℂcc 10527  ℝcr 10528  0cc0 10529  1c1 10530   + caddc 10532   · cmul 10534   − cmin 10862  -cneg 10863  ℕcn 11630  2c2 11684  ℕ0cn0 11889  ℤcz 11973  ℤ≥cuz 12235  ℝ+crp 12381  ...cfz 12884   mod cmo 13229  ↑cexp 13421   ∥ cdvds 15599  ℙcprime 16007   Σg cgsu 16706  Mndcmnd 17903  SubMndcsubmnd 17947  CMndccmn 18898  mulGrpcmgp 19231  Ringcrg 19289  CRingccrg 19290  SubRingcsubrg 19523  ℂfldccnfld 20537 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 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607  ax-addf 10608  ax-mulf 10609 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rmo 3144  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-int 4868  df-iun 4912  df-iin 4913  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-of 7401  df-om 7573  df-1st 7681  df-2nd 7682  df-supp 7823  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-1o 8094  df-2o 8095  df-oadd 8098  df-er 8281  df-map 8400  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-fsupp 8826  df-sup 8898  df-inf 8899  df-oi 8966  df-dju 9322  df-card 9360  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-xnn0 11960  df-z 11974  df-dec 12091  df-uz 12236  df-rp 12382  df-fz 12885  df-fzo 13026  df-fl 13154  df-mod 13230  df-seq 13362  df-exp 13422  df-hash 13683  df-cj 14450  df-re 14451  df-im 14452  df-sqrt 14586  df-abs 14587  df-dvds 15600  df-gcd 15836  df-prm 16008  df-phi 16095  df-struct 16477  df-ndx 16478  df-slot 16479  df-base 16481  df-sets 16482  df-ress 16483  df-plusg 16570  df-mulr 16571  df-starv 16572  df-tset 16576  df-ple 16577  df-ds 16579  df-unif 16580  df-0g 16707  df-gsum 16708  df-mre 16849  df-mrc 16850  df-acs 16852  df-mgm 17844  df-sgrp 17893  df-mnd 17904  df-submnd 17949  df-grp 18098  df-minusg 18099  df-mulg 18217  df-subg 18268  df-cntz 18439  df-cmn 18900  df-mgp 19232  df-ur 19244  df-ring 19291  df-cring 19292  df-subrg 19525  df-cnfld 20538 This theorem is referenced by:  wilthlem3  25639
 Copyright terms: Public domain W3C validator