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

Theorem wilthlem2 27112
Description: Lemma for wilth 27114: 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 27111 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 484 . . . . . . . . 9 ((𝜑𝑆 ⊆ {(𝑃 − 1)}) → 𝑆 ⊆ {(𝑃 − 1)})
2 wilthlem2.s . . . . . . . . . . . . . 14 (𝜑𝑆𝐴)
3 eleq2 2830 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑆 → ((𝑃 − 1) ∈ 𝑥 ↔ (𝑃 − 1) ∈ 𝑆))
4 eleq2 2830 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑆 → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥 ↔ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆))
54raleqbi1dv 3338 . . . . . . . . . . . . . . . 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 3695 . . . . . . . . . . . . . 14 (𝑆𝐴 ↔ (𝑆 ∈ 𝒫 (1...(𝑃 − 1)) ∧ ((𝑃 − 1) ∈ 𝑆 ∧ ∀𝑦𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)))
92, 8sylib 218 . . . . . . . . . . . . 13 (𝜑 → (𝑆 ∈ 𝒫 (1...(𝑃 − 1)) ∧ ((𝑃 − 1) ∈ 𝑆 ∧ ∀𝑦𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)))
109simprd 495 . . . . . . . . . . . 12 (𝜑 → ((𝑃 − 1) ∈ 𝑆 ∧ ∀𝑦𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆))
1110simpld 494 . . . . . . . . . . 11 (𝜑 → (𝑃 − 1) ∈ 𝑆)
1211snssd 4809 . . . . . . . . . 10 (𝜑 → {(𝑃 − 1)} ⊆ 𝑆)
1312adantr 480 . . . . . . . . 9 ((𝜑𝑆 ⊆ {(𝑃 − 1)}) → {(𝑃 − 1)} ⊆ 𝑆)
141, 13eqssd 4001 . . . . . . . 8 ((𝜑𝑆 ⊆ {(𝑃 − 1)}) → 𝑆 = {(𝑃 − 1)})
1514reseq2d 5997 . . . . . . 7 ((𝜑𝑆 ⊆ {(𝑃 − 1)}) → ( I ↾ 𝑆) = ( I ↾ {(𝑃 − 1)}))
16 mptresid 6069 . . . . . . 7 ( I ↾ {(𝑃 − 1)}) = (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)
1715, 16eqtrdi 2793 . . . . . 6 ((𝜑𝑆 ⊆ {(𝑃 − 1)}) → ( I ↾ 𝑆) = (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧))
1817oveq2d 7447 . . . . 5 ((𝜑𝑆 ⊆ {(𝑃 − 1)}) → (𝑇 Σg ( I ↾ 𝑆)) = (𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)))
1918oveq1d 7446 . . . 4 ((𝜑𝑆 ⊆ {(𝑃 − 1)}) → ((𝑇 Σg ( I ↾ 𝑆)) mod 𝑃) = ((𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) mod 𝑃))
20 wilthlem2.p . . . . . . . . . . . 12 (𝜑𝑃 ∈ ℙ)
21 prmnn 16711 . . . . . . . . . . . 12 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
2220, 21syl 17 . . . . . . . . . . 11 (𝜑𝑃 ∈ ℕ)
2322nncnd 12282 . . . . . . . . . 10 (𝜑𝑃 ∈ ℂ)
24 ax-1cn 11213 . . . . . . . . . 10 1 ∈ ℂ
25 negsub 11557 . . . . . . . . . 10 ((𝑃 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑃 + -1) = (𝑃 − 1))
2623, 24, 25sylancl 586 . . . . . . . . 9 (𝜑 → (𝑃 + -1) = (𝑃 − 1))
27 neg1cn 12380 . . . . . . . . . 10 -1 ∈ ℂ
28 addcom 11447 . . . . . . . . . 10 ((𝑃 ∈ ℂ ∧ -1 ∈ ℂ) → (𝑃 + -1) = (-1 + 𝑃))
2923, 27, 28sylancl 586 . . . . . . . . 9 (𝜑 → (𝑃 + -1) = (-1 + 𝑃))
3026, 29eqtr3d 2779 . . . . . . . 8 (𝜑 → (𝑃 − 1) = (-1 + 𝑃))
31 cnring 21403 . . . . . . . . . 10 fld ∈ Ring
32 wilthlem.t . . . . . . . . . . 11 𝑇 = (mulGrp‘ℂfld)
3332ringmgp 20236 . . . . . . . . . 10 (ℂfld ∈ Ring → 𝑇 ∈ Mnd)
3431, 33mp1i 13 . . . . . . . . 9 (𝜑𝑇 ∈ Mnd)
35 nnm1nn0 12567 . . . . . . . . . . 11 (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ0)
3622, 35syl 17 . . . . . . . . . 10 (𝜑 → (𝑃 − 1) ∈ ℕ0)
3736nn0cnd 12589 . . . . . . . . 9 (𝜑 → (𝑃 − 1) ∈ ℂ)
38 cnfldbas 21368 . . . . . . . . . . 11 ℂ = (Base‘ℂfld)
3932, 38mgpbas 20142 . . . . . . . . . 10 ℂ = (Base‘𝑇)
40 id 22 . . . . . . . . . 10 (𝑧 = (𝑃 − 1) → 𝑧 = (𝑃 − 1))
4139, 40gsumsn 19972 . . . . . . . . 9 ((𝑇 ∈ Mnd ∧ (𝑃 − 1) ∈ ℂ ∧ (𝑃 − 1) ∈ ℂ) → (𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) = (𝑃 − 1))
4234, 37, 37, 41syl3anc 1373 . . . . . . . 8 (𝜑 → (𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) = (𝑃 − 1))
4323mullidd 11279 . . . . . . . . 9 (𝜑 → (1 · 𝑃) = 𝑃)
4443oveq2d 7447 . . . . . . . 8 (𝜑 → (-1 + (1 · 𝑃)) = (-1 + 𝑃))
4530, 42, 443eqtr4d 2787 . . . . . . 7 (𝜑 → (𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) = (-1 + (1 · 𝑃)))
4645oveq1d 7446 . . . . . 6 (𝜑 → ((𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) mod 𝑃) = ((-1 + (1 · 𝑃)) mod 𝑃))
47 neg1rr 12381 . . . . . . . 8 -1 ∈ ℝ
4847a1i 11 . . . . . . 7 (𝜑 → -1 ∈ ℝ)
4922nnrpd 13075 . . . . . . 7 (𝜑𝑃 ∈ ℝ+)
50 1zzd 12648 . . . . . . 7 (𝜑 → 1 ∈ ℤ)
51 modcyc 13946 . . . . . . 7 ((-1 ∈ ℝ ∧ 𝑃 ∈ ℝ+ ∧ 1 ∈ ℤ) → ((-1 + (1 · 𝑃)) mod 𝑃) = (-1 mod 𝑃))
5248, 49, 50, 51syl3anc 1373 . . . . . 6 (𝜑 → ((-1 + (1 · 𝑃)) mod 𝑃) = (-1 mod 𝑃))
5346, 52eqtrd 2777 . . . . 5 (𝜑 → ((𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) mod 𝑃) = (-1 mod 𝑃))
5453adantr 480 . . . 4 ((𝜑𝑆 ⊆ {(𝑃 − 1)}) → ((𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) mod 𝑃) = (-1 mod 𝑃))
5519, 54eqtrd 2777 . . 3 ((𝜑𝑆 ⊆ {(𝑃 − 1)}) → ((𝑇 Σg ( I ↾ 𝑆)) mod 𝑃) = (-1 mod 𝑃))
5655ex 412 . 2 (𝜑 → (𝑆 ⊆ {(𝑃 − 1)} → ((𝑇 Σg ( I ↾ 𝑆)) mod 𝑃) = (-1 mod 𝑃)))
57 nss 4048 . . 3 𝑆 ⊆ {(𝑃 − 1)} ↔ ∃𝑧(𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)}))
58 cnfld1 21406 . . . . . . . . . 10 1 = (1r‘ℂfld)
5932, 58ringidval 20180 . . . . . . . . 9 1 = (0g𝑇)
60 cnfldmul 21372 . . . . . . . . . 10 · = (.r‘ℂfld)
6132, 60mgpplusg 20141 . . . . . . . . 9 · = (+g𝑇)
62 cncrng 21401 . . . . . . . . . . 11 fld ∈ CRing
6332crngmgp 20238 . . . . . . . . . . 11 (ℂfld ∈ CRing → 𝑇 ∈ CMnd)
6462, 63ax-mp 5 . . . . . . . . . 10 𝑇 ∈ CMnd
6564a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑇 ∈ CMnd)
662adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑆𝐴)
67 f1oi 6886 . . . . . . . . . . . 12 ( I ↾ 𝑆):𝑆1-1-onto𝑆
68 f1of 6848 . . . . . . . . . . . 12 (( I ↾ 𝑆):𝑆1-1-onto𝑆 → ( I ↾ 𝑆):𝑆𝑆)
6967, 68ax-mp 5 . . . . . . . . . . 11 ( I ↾ 𝑆):𝑆𝑆
709simpld 494 . . . . . . . . . . . . . 14 (𝜑𝑆 ∈ 𝒫 (1...(𝑃 − 1)))
7170elpwid 4609 . . . . . . . . . . . . 13 (𝜑𝑆 ⊆ (1...(𝑃 − 1)))
72 fzssz 13566 . . . . . . . . . . . . 13 (1...(𝑃 − 1)) ⊆ ℤ
7371, 72sstrdi 3996 . . . . . . . . . . . 12 (𝜑𝑆 ⊆ ℤ)
74 zsscn 12621 . . . . . . . . . . . 12 ℤ ⊆ ℂ
7573, 74sstrdi 3996 . . . . . . . . . . 11 (𝜑𝑆 ⊆ ℂ)
76 fss 6752 . . . . . . . . . . 11 ((( I ↾ 𝑆):𝑆𝑆𝑆 ⊆ ℂ) → ( I ↾ 𝑆):𝑆⟶ℂ)
7769, 75, 76sylancr 587 . . . . . . . . . 10 (𝜑 → ( I ↾ 𝑆):𝑆⟶ℂ)
7877adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ( I ↾ 𝑆):𝑆⟶ℂ)
79 fzfi 14013 . . . . . . . . . . . 12 (1...(𝑃 − 1)) ∈ Fin
80 ssfi 9213 . . . . . . . . . . . 12 (((1...(𝑃 − 1)) ∈ Fin ∧ 𝑆 ⊆ (1...(𝑃 − 1))) → 𝑆 ∈ Fin)
8179, 71, 80sylancr 587 . . . . . . . . . . 11 (𝜑𝑆 ∈ Fin)
82 1ex 11257 . . . . . . . . . . . 12 1 ∈ V
8382a1i 11 . . . . . . . . . . 11 (𝜑 → 1 ∈ V)
8477, 81, 83fdmfifsupp 9415 . . . . . . . . . 10 (𝜑 → ( I ↾ 𝑆) finSupp 1)
8584adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ( I ↾ 𝑆) finSupp 1)
86 disjdif 4472 . . . . . . . . . 10 ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∩ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = ∅
8786a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∩ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = ∅)
88 undif2 4477 . . . . . . . . . 10 ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∪ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∪ 𝑆)
89 simprl 771 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑧𝑆)
90 oveq1 7438 . . . . . . . . . . . . . . 15 (𝑦 = 𝑧 → (𝑦↑(𝑃 − 2)) = (𝑧↑(𝑃 − 2)))
9190oveq1d 7446 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 → ((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃))
9291eleq1d 2826 . . . . . . . . . . . . 13 (𝑦 = 𝑧 → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆 ↔ ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆))
9310simprd 495 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑦𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)
9493adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ∀𝑦𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)
9592, 94, 89rspcdva 3623 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)
9689, 95prssd 4822 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ⊆ 𝑆)
97 ssequn1 4186 . . . . . . . . . . 11 ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ⊆ 𝑆 ↔ ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∪ 𝑆) = 𝑆)
9896, 97sylib 218 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∪ 𝑆) = 𝑆)
9988, 98eqtr2id 2790 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑆 = ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∪ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))
10039, 59, 61, 65, 66, 78, 85, 87, 99gsumsplit 19946 . . . . . . . 8 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg ( I ↾ 𝑆)) = ((𝑇 Σg (( I ↾ 𝑆) ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg (( I ↾ 𝑆) ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))))
10196resabs1d 6026 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (( I ↾ 𝑆) ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) = ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
102101oveq2d 7447 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg (( I ↾ 𝑆) ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = (𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))
103 difss 4136 . . . . . . . . . . . 12 (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ 𝑆
104 resabs1 6024 . . . . . . . . . . . 12 ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ 𝑆 → (( I ↾ 𝑆) ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))
105103, 104ax-mp 5 . . . . . . . . . . 11 (( I ↾ 𝑆) ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
106105oveq2i 7442 . . . . . . . . . 10 (𝑇 Σg (( I ↾ 𝑆) ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) = (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))
107106a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg (( I ↾ 𝑆) ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) = (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))))
108102, 107oveq12d 7449 . . . . . . . 8 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑇 Σg (( I ↾ 𝑆) ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg (( I ↾ 𝑆) ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) = ((𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))))
109100, 108eqtrd 2777 . . . . . . 7 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg ( I ↾ 𝑆)) = ((𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))))
110109oveq1d 7446 . . . . . 6 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑇 Σg ( I ↾ 𝑆)) mod 𝑃) = (((𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) mod 𝑃))
111 prfi 9363 . . . . . . . . . 10 {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∈ Fin
112111a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∈ Fin)
113 zsubrg 21438 . . . . . . . . . 10 ℤ ∈ (SubRing‘ℂfld)
11432subrgsubm 20585 . . . . . . . . . 10 (ℤ ∈ (SubRing‘ℂfld) → ℤ ∈ (SubMnd‘𝑇))
115113, 114mp1i 13 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ℤ ∈ (SubMnd‘𝑇))
116 f1oi 6886 . . . . . . . . . . 11 ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}–1-1-onto→{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}
117 f1of 6848 . . . . . . . . . . 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 480 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑆 ⊆ ℤ)
12096, 119sstrd 3994 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ⊆ ℤ)
121 fss 6752 . . . . . . . . . 10 ((( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}⟶{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∧ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ⊆ ℤ) → ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}⟶ℤ)
122118, 120, 121sylancr 587 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}⟶ℤ)
12382a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 1 ∈ V)
124122, 112, 123fdmfifsupp 9415 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) finSupp 1)
12559, 65, 112, 115, 122, 124gsumsubmcl 19937 . . . . . . . 8 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) ∈ ℤ)
126125zred 12722 . . . . . . 7 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) ∈ ℝ)
127 1red 11262 . . . . . . 7 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 1 ∈ ℝ)
12871adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑆 ⊆ (1...(𝑃 − 1)))
129128ssdifssd 4147 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ (1...(𝑃 − 1)))
130 ssfi 9213 . . . . . . . . 9 (((1...(𝑃 − 1)) ∈ Fin ∧ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ (1...(𝑃 − 1))) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ Fin)
13179, 129, 130sylancr 587 . . . . . . . 8 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ Fin)
132 f1oi 6886 . . . . . . . . . 10 ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})):(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})–1-1-onto→(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})
133 f1of 6848 . . . . . . . . . 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 4147 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ ℤ)
136 fss 6752 . . . . . . . . 9 ((( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})):(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})⟶(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∧ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ ℤ) → ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})):(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})⟶ℤ)
137134, 135, 136sylancr 587 . . . . . . . 8 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})):(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})⟶ℤ)
138137, 131, 123fdmfifsupp 9415 . . . . . . . 8 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) finSupp 1)
13959, 65, 131, 115, 137, 138gsumsubmcl 19937 . . . . . . 7 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) ∈ ℤ)
14049adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∈ ℝ+)
14134adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑇 ∈ Mnd)
14275adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑆 ⊆ ℂ)
143142, 89sseldd 3984 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑧 ∈ ℂ)
144 id 22 . . . . . . . . . . . . 13 (𝑤 = 𝑧𝑤 = 𝑧)
14539, 144gsumsn 19972 . . . . . . . . . . . 12 ((𝑇 ∈ Mnd ∧ 𝑧 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) = 𝑧)
146141, 143, 143, 145syl3anc 1373 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) = 𝑧)
147146adantr 480 . . . . . . . . . 10 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → (𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) = 𝑧)
148 mptresid 6069 . . . . . . . . . . . 12 ( I ↾ {𝑧}) = (𝑤 ∈ {𝑧} ↦ 𝑤)
149 dfsn2 4639 . . . . . . . . . . . . . 14 {𝑧} = {𝑧, 𝑧}
150 animorrl 983 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → (𝑧 = 1 ∨ 𝑧 = (𝑃 − 1)))
15120adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∈ ℙ)
152128, 89sseldd 3984 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑧 ∈ (1...(𝑃 − 1)))
153 wilthlem1 27111 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ ℙ ∧ 𝑧 ∈ (1...(𝑃 − 1))) → (𝑧 = ((𝑧↑(𝑃 − 2)) mod 𝑃) ↔ (𝑧 = 1 ∨ 𝑧 = (𝑃 − 1))))
154151, 152, 153syl2anc 584 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑧 = ((𝑧↑(𝑃 − 2)) mod 𝑃) ↔ (𝑧 = 1 ∨ 𝑧 = (𝑃 − 1))))
155154biimpar 477 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ (𝑧 = 1 ∨ 𝑧 = (𝑃 − 1))) → 𝑧 = ((𝑧↑(𝑃 − 2)) mod 𝑃))
156150, 155syldan 591 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → 𝑧 = ((𝑧↑(𝑃 − 2)) mod 𝑃))
157156preq2d 4740 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → {𝑧, 𝑧} = {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})
158149, 157eqtrid 2789 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → {𝑧} = {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})
159158reseq2d 5997 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → ( I ↾ {𝑧}) = ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
160148, 159eqtr3id 2791 . . . . . . . . . . 11 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → (𝑤 ∈ {𝑧} ↦ 𝑤) = ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
161160oveq2d 7447 . . . . . . . . . 10 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → (𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) = (𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))
162 simpr 484 . . . . . . . . . 10 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → 𝑧 = 1)
163147, 161, 1623eqtr3d 2785 . . . . . . . . 9 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → (𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = 1)
164163oveq1d 7446 . . . . . . . 8 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → ((𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) mod 𝑃) = (1 mod 𝑃))
165 df-pr 4629 . . . . . . . . . . . . . . 15 {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} = ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)})
166165reseq2i 5994 . . . . . . . . . . . . . 14 ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) = ( I ↾ ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)}))
167 mptresid 6069 . . . . . . . . . . . . . 14 ( I ↾ ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)})) = (𝑤 ∈ ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)}) ↦ 𝑤)
168166, 167eqtri 2765 . . . . . . . . . . . . 13 ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) = (𝑤 ∈ ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)}) ↦ 𝑤)
169168oveq2i 7442 . . . . . . . . . . . 12 (𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = (𝑇 Σg (𝑤 ∈ ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)}) ↦ 𝑤))
17064a1i 11 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → 𝑇 ∈ CMnd)
171 snfi 9083 . . . . . . . . . . . . . 14 {𝑧} ∈ Fin
172171a1i 11 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → {𝑧} ∈ Fin)
173 elsni 4643 . . . . . . . . . . . . . . . 16 (𝑤 ∈ {𝑧} → 𝑤 = 𝑧)
174173adantl 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑤 ∈ {𝑧}) → 𝑤 = 𝑧)
175143adantr 480 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑤 ∈ {𝑧}) → 𝑧 ∈ ℂ)
176174, 175eqeltrd 2841 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑤 ∈ {𝑧}) → 𝑤 ∈ ℂ)
177176adantlr 715 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) ∧ 𝑤 ∈ {𝑧}) → 𝑤 ∈ ℂ)
178142, 95sseldd 3984 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ ℂ)
179178adantr 480 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ ℂ)
180 simprr 773 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ 𝑧 ∈ {(𝑃 − 1)})
181 velsn 4642 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ {(𝑃 − 1)} ↔ 𝑧 = (𝑃 − 1))
182180, 181sylnib 328 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ 𝑧 = (𝑃 − 1))
183 biorf 937 . . . . . . . . . . . . . . . . 17 𝑧 = (𝑃 − 1) → (𝑧 = 1 ↔ (𝑧 = (𝑃 − 1) ∨ 𝑧 = 1)))
184182, 183syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑧 = 1 ↔ (𝑧 = (𝑃 − 1) ∨ 𝑧 = 1)))
185 ovex 7464 . . . . . . . . . . . . . . . . . . 19 ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ V
186185elsn 4641 . . . . . . . . . . . . . . . . . 18 (((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧} ↔ ((𝑧↑(𝑃 − 2)) mod 𝑃) = 𝑧)
187 eqcom 2744 . . . . . . . . . . . . . . . . . 18 (((𝑧↑(𝑃 − 2)) mod 𝑃) = 𝑧𝑧 = ((𝑧↑(𝑃 − 2)) mod 𝑃))
188186, 187bitri 275 . . . . . . . . . . . . . . . . 17 (((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧} ↔ 𝑧 = ((𝑧↑(𝑃 − 2)) mod 𝑃))
189 orcom 871 . . . . . . . . . . . . . . . . 17 ((𝑧 = (𝑃 − 1) ∨ 𝑧 = 1) ↔ (𝑧 = 1 ∨ 𝑧 = (𝑃 − 1)))
190154, 188, 1893bitr4g 314 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧} ↔ (𝑧 = (𝑃 − 1) ∨ 𝑧 = 1)))
191184, 190bitr4d 282 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑧 = 1 ↔ ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧}))
192191necon3abid 2977 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑧 ≠ 1 ↔ ¬ ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧}))
193192biimpa 476 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → ¬ ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧})
194 id 22 . . . . . . . . . . . . 13 (𝑤 = ((𝑧↑(𝑃 − 2)) mod 𝑃) → 𝑤 = ((𝑧↑(𝑃 − 2)) mod 𝑃))
19539, 61, 170, 172, 177, 179, 193, 179, 194gsumunsn 19978 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → (𝑇 Σg (𝑤 ∈ ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)}) ↦ 𝑤)) = ((𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) · ((𝑧↑(𝑃 − 2)) mod 𝑃)))
196169, 195eqtrid 2789 . . . . . . . . . . 11 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → (𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = ((𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) · ((𝑧↑(𝑃 − 2)) mod 𝑃)))
197146adantr 480 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → (𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) = 𝑧)
198197oveq1d 7446 . . . . . . . . . . 11 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → ((𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) · ((𝑧↑(𝑃 − 2)) mod 𝑃)) = (𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)))
199196, 198eqtrd 2777 . . . . . . . . . 10 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → (𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = (𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)))
200199oveq1d 7446 . . . . . . . . 9 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → ((𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) mod 𝑃) = ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) mod 𝑃))
201152elfzelzd 13565 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑧 ∈ ℤ)
20222adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∈ ℕ)
203 fzm1ndvds 16359 . . . . . . . . . . . . . 14 ((𝑃 ∈ ℕ ∧ 𝑧 ∈ (1...(𝑃 − 1))) → ¬ 𝑃𝑧)
204202, 152, 203syl2anc 584 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ 𝑃𝑧)
205 eqid 2737 . . . . . . . . . . . . . 14 ((𝑧↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃)
206205prmdiv 16822 . . . . . . . . . . . . 13 ((𝑃 ∈ ℙ ∧ 𝑧 ∈ ℤ ∧ ¬ 𝑃𝑧) → (((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) − 1)))
207151, 201, 204, 206syl3anc 1373 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) − 1)))
208207simprd 495 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∥ ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) − 1))
209 elfznn 13593 . . . . . . . . . . . . . . 15 (𝑧 ∈ (1...(𝑃 − 1)) → 𝑧 ∈ ℕ)
210152, 209syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑧 ∈ ℕ)
211128, 95sseldd 3984 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)))
212 elfznn 13593 . . . . . . . . . . . . . . 15 (((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ ℕ)
213211, 212syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ ℕ)
214210, 213nnmulcld 12319 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) ∈ ℕ)
215214nnzd 12640 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) ∈ ℤ)
216 1zzd 12648 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 1 ∈ ℤ)
217 moddvds 16301 . . . . . . . . . . . 12 ((𝑃 ∈ ℕ ∧ (𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) ∈ ℤ ∧ 1 ∈ ℤ) → (((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) − 1)))
218202, 215, 216, 217syl3anc 1373 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) − 1)))
219208, 218mpbird 257 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = (1 mod 𝑃))
220219adantr 480 . . . . . . . . 9 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = (1 mod 𝑃))
221200, 220eqtrd 2777 . . . . . . . 8 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → ((𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) mod 𝑃) = (1 mod 𝑃))
222164, 221pm2.61dane 3029 . . . . . . 7 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) mod 𝑃) = (1 mod 𝑃))
223 modmul1 13965 . . . . . . 7 ((((𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) ∈ ℝ ∧ 1 ∈ ℝ) ∧ ((𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) ∈ ℤ ∧ 𝑃 ∈ ℝ+) ∧ ((𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) mod 𝑃) = (1 mod 𝑃)) → (((𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) mod 𝑃) = ((1 · (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) mod 𝑃))
224126, 127, 139, 140, 222, 223syl221anc 1383 . . . . . 6 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑇 Σg ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) mod 𝑃) = ((1 · (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) mod 𝑃))
225139zcnd 12723 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) ∈ ℂ)
226225mullidd 11279 . . . . . . . 8 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (1 · (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) = (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))))
227226oveq1d 7446 . . . . . . 7 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((1 · (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) mod 𝑃) = ((𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) mod 𝑃))
228 sseqin2 4223 . . . . . . . . . . 11 ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ⊆ 𝑆 ↔ (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) = {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})
22996, 228sylib 218 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) = {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})
230 vex 3484 . . . . . . . . . . . 12 𝑧 ∈ V
231230prnz 4777 . . . . . . . . . . 11 {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ≠ ∅
232231a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ≠ ∅)
233229, 232eqnetrd 3008 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ≠ ∅)
234 disj4 4459 . . . . . . . . . 10 ((𝑆 ∩ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) = ∅ ↔ ¬ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊊ 𝑆)
235234necon2abii 2991 . . . . . . . . 9 ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊊ 𝑆 ↔ (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ≠ ∅)
236233, 235sylibr 234 . . . . . . . 8 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊊ 𝑆)
237 psseq1 4090 . . . . . . . . . 10 (𝑠 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → (𝑠𝑆 ↔ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊊ 𝑆))
238 reseq2 5992 . . . . . . . . . . . . 13 (𝑠 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → ( I ↾ 𝑠) = ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))
239238oveq2d 7447 . . . . . . . . . . . 12 (𝑠 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → (𝑇 Σg ( I ↾ 𝑠)) = (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))))
240239oveq1d 7446 . . . . . . . . . . 11 (𝑠 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → ((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = ((𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) mod 𝑃))
241240eqeq1d 2739 . . . . . . . . . 10 (𝑠 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → (((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃) ↔ ((𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) mod 𝑃) = (-1 mod 𝑃)))
242237, 241imbi12d 344 . . . . . . . . 9 (𝑠 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → ((𝑠𝑆 → ((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ↔ ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊊ 𝑆 → ((𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) mod 𝑃) = (-1 mod 𝑃))))
243 wilthlem2.r . . . . . . . . . 10 (𝜑 → ∀𝑠𝐴 (𝑠𝑆 → ((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))
244243adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ∀𝑠𝐴 (𝑠𝑆 → ((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))
245 ovex 7464 . . . . . . . . . . . 12 (1...(𝑃 − 1)) ∈ V
246245elpw2 5334 . . . . . . . . . . 11 ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ 𝒫 (1...(𝑃 − 1)) ↔ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ (1...(𝑃 − 1)))
247129, 246sylibr 234 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ 𝒫 (1...(𝑃 − 1)))
24811adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ 𝑆)
249 eqcom 2744 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑃 − 1) ↔ (𝑃 − 1) = 𝑧)
250181, 249bitri 275 . . . . . . . . . . . . . . 15 (𝑧 ∈ {(𝑃 − 1)} ↔ (𝑃 − 1) = 𝑧)
251180, 250sylnib 328 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ (𝑃 − 1) = 𝑧)
252 oveq1 7438 . . . . . . . . . . . . . . . . 17 ((𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃) → ((𝑃 − 1)↑(𝑃 − 2)) = (((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)))
253252oveq1d 7446 . . . . . . . . . . . . . . . 16 ((𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃) → (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃) = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃))
254202, 35syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ ℕ0)
255 nn0uz 12920 . . . . . . . . . . . . . . . . . . . 20 0 = (ℤ‘0)
256254, 255eleqtrdi 2851 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ (ℤ‘0))
257 eluzfz2 13572 . . . . . . . . . . . . . . . . . . 19 ((𝑃 − 1) ∈ (ℤ‘0) → (𝑃 − 1) ∈ (0...(𝑃 − 1)))
258256, 257syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ (0...(𝑃 − 1)))
259 prmz 16712 . . . . . . . . . . . . . . . . . . . . 21 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
260151, 259syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∈ ℤ)
261119, 248sseldd 3984 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ ℤ)
262 1z 12647 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℤ
263 zsubcl 12659 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃 − 1) ∈ ℤ ∧ 1 ∈ ℤ) → ((𝑃 − 1) − 1) ∈ ℤ)
264261, 262, 263sylancl 586 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) − 1) ∈ ℤ)
265 dvdsmul1 16315 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ ℤ ∧ ((𝑃 − 1) − 1) ∈ ℤ) → 𝑃 ∥ (𝑃 · ((𝑃 − 1) − 1)))
266260, 264, 265syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∥ (𝑃 · ((𝑃 − 1) − 1)))
267202nncnd 12282 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∈ ℂ)
268264zcnd 12723 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) − 1) ∈ ℂ)
269267, 268mulcld 11281 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 · ((𝑃 − 1) − 1)) ∈ ℂ)
270 1cnd 11256 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 1 ∈ ℂ)
271254nn0cnd 12589 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ ℂ)
272267, 270, 271subdird 11720 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) · (𝑃 − 1)) = ((𝑃 · (𝑃 − 1)) − (1 · (𝑃 − 1))))
273267, 271mulcld 11281 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 · (𝑃 − 1)) ∈ ℂ)
274273, 267, 270subsubd 11648 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 · (𝑃 − 1)) − (𝑃 − 1)) = (((𝑃 · (𝑃 − 1)) − 𝑃) + 1))
275271mullidd 11279 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (1 · (𝑃 − 1)) = (𝑃 − 1))
276275oveq2d 7447 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 · (𝑃 − 1)) − (1 · (𝑃 − 1))) = ((𝑃 · (𝑃 − 1)) − (𝑃 − 1)))
277267, 271muls1d 11723 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 · ((𝑃 − 1) − 1)) = ((𝑃 · (𝑃 − 1)) − 𝑃))
278277oveq1d 7446 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 · ((𝑃 − 1) − 1)) + 1) = (((𝑃 · (𝑃 − 1)) − 𝑃) + 1))
279274, 276, 2783eqtr4d 2787 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 · (𝑃 − 1)) − (1 · (𝑃 − 1))) = ((𝑃 · ((𝑃 − 1) − 1)) + 1))
280272, 279eqtrd 2777 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) · (𝑃 − 1)) = ((𝑃 · ((𝑃 − 1) − 1)) + 1))
281269, 270, 280mvrraddd 11675 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑃 − 1) · (𝑃 − 1)) − 1) = (𝑃 · ((𝑃 − 1) − 1)))
282266, 281breqtrrd 5171 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∥ (((𝑃 − 1) · (𝑃 − 1)) − 1))
283128, 248sseldd 3984 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ (1...(𝑃 − 1)))
284 fzm1ndvds 16359 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ ℕ ∧ (𝑃 − 1) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (𝑃 − 1))
285202, 283, 284syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ 𝑃 ∥ (𝑃 − 1))
286 eqid 2737 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃) = (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃)
287286prmdiveq 16823 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ ℙ ∧ (𝑃 − 1) ∈ ℤ ∧ ¬ 𝑃 ∥ (𝑃 − 1)) → (((𝑃 − 1) ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ (((𝑃 − 1) · (𝑃 − 1)) − 1)) ↔ (𝑃 − 1) = (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃)))
288151, 261, 285, 287syl3anc 1373 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑃 − 1) ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ (((𝑃 − 1) · (𝑃 − 1)) − 1)) ↔ (𝑃 − 1) = (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃)))
289258, 282, 288mpbi2and 712 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) = (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃))
290205prmdivdiv 16824 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ ℙ ∧ 𝑧 ∈ (1...(𝑃 − 1))) → 𝑧 = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃))
291151, 152, 290syl2anc 584 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑧 = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃))
292289, 291eqeq12d 2753 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) = 𝑧 ↔ (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃) = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃)))
293253, 292imbitrrid 246 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃) → (𝑃 − 1) = 𝑧))
294251, 293mtod 198 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ (𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃))
295 ioran 986 . . . . . . . . . . . . . 14 (¬ ((𝑃 − 1) = 𝑧 ∨ (𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃)) ↔ (¬ (𝑃 − 1) = 𝑧 ∧ ¬ (𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃)))
296251, 294, 295sylanbrc 583 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ ((𝑃 − 1) = 𝑧 ∨ (𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃)))
297 ovex 7464 . . . . . . . . . . . . . 14 (𝑃 − 1) ∈ V
298297elpr 4650 . . . . . . . . . . . . 13 ((𝑃 − 1) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ↔ ((𝑃 − 1) = 𝑧 ∨ (𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃)))
299296, 298sylnibr 329 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ (𝑃 − 1) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})
300248, 299eldifd 3962 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
301 eldifi 4131 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → 𝑦𝑆)
30294r19.21bi 3251 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)
303301, 302sylan2 593 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) → ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)
304 eldif 3961 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ↔ (𝑦𝑆 ∧ ¬ 𝑦 ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
305151adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → 𝑃 ∈ ℙ)
306128sselda 3983 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → 𝑦 ∈ (1...(𝑃 − 1)))
307 eqid 2737 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑦↑(𝑃 − 2)) mod 𝑃)
308307prmdivdiv 16824 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ ℙ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → 𝑦 = ((((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃))
309305, 306, 308syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → 𝑦 = ((((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃))
310 oveq1 7438 . . . . . . . . . . . . . . . . . . . . 21 (((𝑦↑(𝑃 − 2)) mod 𝑃) = 𝑧 → (((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) = (𝑧↑(𝑃 − 2)))
311310oveq1d 7446 . . . . . . . . . . . . . . . . . . . 20 (((𝑦↑(𝑃 − 2)) mod 𝑃) = 𝑧 → ((((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃))
312311eqeq2d 2748 . . . . . . . . . . . . . . . . . . 19 (((𝑦↑(𝑃 − 2)) mod 𝑃) = 𝑧 → (𝑦 = ((((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃) ↔ 𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃)))
313309, 312syl5ibcom 245 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → (((𝑦↑(𝑃 − 2)) mod 𝑃) = 𝑧𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃)))
314 oveq1 7438 . . . . . . . . . . . . . . . . . . . 20 (((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃) → (((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) = (((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)))
315314oveq1d 7446 . . . . . . . . . . . . . . . . . . 19 (((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃) → ((((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃) = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃))
316291adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → 𝑧 = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃))
317309, 316eqeq12d 2753 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → (𝑦 = 𝑧 ↔ ((((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃) = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃)))
318315, 317imbitrrid 246 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → (((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃) → 𝑦 = 𝑧))
319313, 318orim12d 967 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → ((((𝑦↑(𝑃 − 2)) mod 𝑃) = 𝑧 ∨ ((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃)) → (𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃) ∨ 𝑦 = 𝑧)))
320 ovex 7464 . . . . . . . . . . . . . . . . . 18 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ V
321320elpr 4650 . . . . . . . . . . . . . . . . 17 (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ↔ (((𝑦↑(𝑃 − 2)) mod 𝑃) = 𝑧 ∨ ((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃)))
322 vex 3484 . . . . . . . . . . . . . . . . . . 19 𝑦 ∈ V
323322elpr 4650 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ↔ (𝑦 = 𝑧𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃)))
324 orcom 871 . . . . . . . . . . . . . . . . . 18 ((𝑦 = 𝑧𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃)) ↔ (𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃) ∨ 𝑦 = 𝑧))
325323, 324bitri 275 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ↔ (𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃) ∨ 𝑦 = 𝑧))
326319, 321, 3253imtr4g 296 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} → 𝑦 ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
327326con3d 152 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦𝑆) → (¬ 𝑦 ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} → ¬ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
328327impr 454 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ (𝑦𝑆 ∧ ¬ 𝑦 ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) → ¬ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})
329304, 328sylan2b 594 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) → ¬ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})
330303, 329eldifd 3962 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) → ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
331330ralrimiva 3146 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ∀𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))
332300, 331jca 511 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∧ ∀𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))
333 eleq2 2830 . . . . . . . . . . . 12 (𝑥 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → ((𝑃 − 1) ∈ 𝑥 ↔ (𝑃 − 1) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))
334 eleq2 2830 . . . . . . . . . . . . 13 (𝑥 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥 ↔ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))
335334raleqbi1dv 3338 . . . . . . . . . . . 12 (𝑥 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → (∀𝑦𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥 ↔ ∀𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))
336333, 335anbi12d 632 . . . . . . . . . . 11 (𝑥 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → (((𝑃 − 1) ∈ 𝑥 ∧ ∀𝑦𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥) ↔ ((𝑃 − 1) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∧ ∀𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))))
337336, 7elrab2 3695 . . . . . . . . . 10 ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ 𝐴 ↔ ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ 𝒫 (1...(𝑃 − 1)) ∧ ((𝑃 − 1) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∧ ∀𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))))
338247, 332, 337sylanbrc 583 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ 𝐴)
339242, 244, 338rspcdva 3623 . . . . . . . 8 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊊ 𝑆 → ((𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) mod 𝑃) = (-1 mod 𝑃)))
340236, 339mpd 15 . . . . . . 7 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) mod 𝑃) = (-1 mod 𝑃))
341227, 340eqtrd 2777 . . . . . 6 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((1 · (𝑇 Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) mod 𝑃) = (-1 mod 𝑃))
342110, 224, 3413eqtrd 2781 . . . . 5 ((𝜑 ∧ (𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑇 Σg ( I ↾ 𝑆)) mod 𝑃) = (-1 mod 𝑃))
343342ex 412 . . . 4 (𝜑 → ((𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)}) → ((𝑇 Σg ( I ↾ 𝑆)) mod 𝑃) = (-1 mod 𝑃)))
344343exlimdv 1933 . . 3 (𝜑 → (∃𝑧(𝑧𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)}) → ((𝑇 Σg ( I ↾ 𝑆)) mod 𝑃) = (-1 mod 𝑃)))
34557, 344biimtrid 242 . 2 (𝜑 → (¬ 𝑆 ⊆ {(𝑃 − 1)} → ((𝑇 Σg ( I ↾ 𝑆)) mod 𝑃) = (-1 mod 𝑃)))
34656, 345pm2.61d 179 1 (𝜑 → ((𝑇 Σg ( I ↾ 𝑆)) mod 𝑃) = (-1 mod 𝑃))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 848   = wceq 1540  wex 1779  wcel 2108  wne 2940  wral 3061  {crab 3436  Vcvv 3480  cdif 3948  cun 3949  cin 3950  wss 3951  wpss 3952  c0 4333  𝒫 cpw 4600  {csn 4626  {cpr 4628   class class class wbr 5143  cmpt 5225   I cid 5577  cres 5687  wf 6557  1-1-ontowf1o 6560  cfv 6561  (class class class)co 7431  Fincfn 8985   finSupp cfsupp 9401  cc 11153  cr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160  cmin 11492  -cneg 11493  cn 12266  2c2 12321  0cn0 12526  cz 12613  cuz 12878  +crp 13034  ...cfz 13547   mod cmo 13909  cexp 14102  cdvds 16290  cprime 16708   Σg cgsu 17485  Mndcmnd 18747  SubMndcsubmnd 18795  CMndccmn 19798  mulGrpcmgp 20137  Ringcrg 20230  CRingccrg 20231  SubRingcsubrg 20569  fldccnfld 21364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233  ax-addf 11234  ax-mulf 11235
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8014  df-2nd 8015  df-supp 8186  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-oadd 8510  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fsupp 9402  df-sup 9482  df-inf 9483  df-oi 9550  df-dju 9941  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-xnn0 12600  df-z 12614  df-dec 12734  df-uz 12879  df-rp 13035  df-fz 13548  df-fzo 13695  df-fl 13832  df-mod 13910  df-seq 14043  df-exp 14103  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-dvds 16291  df-gcd 16532  df-prm 16709  df-phi 16803  df-struct 17184  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-mulr 17311  df-starv 17312  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-0g 17486  df-gsum 17487  df-mre 17629  df-mrc 17630  df-acs 17632  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-submnd 18797  df-grp 18954  df-minusg 18955  df-mulg 19086  df-subg 19141  df-cntz 19335  df-cmn 19800  df-abl 19801  df-mgp 20138  df-rng 20150  df-ur 20179  df-ring 20232  df-cring 20233  df-subrng 20546  df-subrg 20570  df-cnfld 21365
This theorem is referenced by:  wilthlem3  27113
  Copyright terms: Public domain W3C validator