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

Theorem lgseisenlem3 25516
Description: Lemma for lgseisen 25518. (Contributed by Mario Carneiro, 17-Jun-2015.) (Proof shortened by AV, 28-Jul-2019.)
Hypotheses
Ref Expression
lgseisen.1 (𝜑𝑃 ∈ (ℙ ∖ {2}))
lgseisen.2 (𝜑𝑄 ∈ (ℙ ∖ {2}))
lgseisen.3 (𝜑𝑃𝑄)
lgseisen.4 𝑅 = ((𝑄 · (2 · 𝑥)) mod 𝑃)
lgseisen.5 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
lgseisen.6 𝑆 = ((𝑄 · (2 · 𝑦)) mod 𝑃)
lgseisen.7 𝑌 = (ℤ/nℤ‘𝑃)
lgseisen.8 𝐺 = (mulGrp‘𝑌)
lgseisen.9 𝐿 = (ℤRHom‘𝑌)
Assertion
Ref Expression
lgseisenlem3 (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (1r𝑌))
Distinct variable groups:   𝑥,𝐺   𝑥,𝐿   𝑥,𝑦,𝑃   𝜑,𝑥,𝑦   𝑦,𝑀   𝑥,𝑄,𝑦   𝑥,𝑌   𝑥,𝑆
Allowed substitution hints:   𝑅(𝑥,𝑦)   𝑆(𝑦)   𝐺(𝑦)   𝐿(𝑦)   𝑀(𝑥)   𝑌(𝑦)

Proof of Theorem lgseisenlem3
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 oveq2 6914 . . . . . . . . 9 (𝑘 = 𝑥 → (2 · 𝑘) = (2 · 𝑥))
21fveq2d 6438 . . . . . . . 8 (𝑘 = 𝑥 → (𝐿‘(2 · 𝑘)) = (𝐿‘(2 · 𝑥)))
32cbvmptv 4974 . . . . . . 7 (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))
43oveq2i 6917 . . . . . 6 (𝐺 Σg (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘)))) = (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))
5 lgseisen.8 . . . . . . . 8 𝐺 = (mulGrp‘𝑌)
6 eqid 2826 . . . . . . . 8 (Base‘𝑌) = (Base‘𝑌)
75, 6mgpbas 18850 . . . . . . 7 (Base‘𝑌) = (Base‘𝐺)
8 eqid 2826 . . . . . . 7 (0g𝐺) = (0g𝐺)
9 lgseisen.1 . . . . . . . . . . 11 (𝜑𝑃 ∈ (ℙ ∖ {2}))
109eldifad 3811 . . . . . . . . . 10 (𝜑𝑃 ∈ ℙ)
11 lgseisen.7 . . . . . . . . . . 11 𝑌 = (ℤ/nℤ‘𝑃)
1211znfld 20269 . . . . . . . . . 10 (𝑃 ∈ ℙ → 𝑌 ∈ Field)
1310, 12syl 17 . . . . . . . . 9 (𝜑𝑌 ∈ Field)
14 isfld 19113 . . . . . . . . . 10 (𝑌 ∈ Field ↔ (𝑌 ∈ DivRing ∧ 𝑌 ∈ CRing))
1514simprbi 492 . . . . . . . . 9 (𝑌 ∈ Field → 𝑌 ∈ CRing)
1613, 15syl 17 . . . . . . . 8 (𝜑𝑌 ∈ CRing)
175crngmgp 18910 . . . . . . . 8 (𝑌 ∈ CRing → 𝐺 ∈ CMnd)
1816, 17syl 17 . . . . . . 7 (𝜑𝐺 ∈ CMnd)
19 fzfid 13068 . . . . . . 7 (𝜑 → (1...((𝑃 − 1) / 2)) ∈ Fin)
20 crngring 18913 . . . . . . . . . . . 12 (𝑌 ∈ CRing → 𝑌 ∈ Ring)
2116, 20syl 17 . . . . . . . . . . 11 (𝜑𝑌 ∈ Ring)
22 lgseisen.9 . . . . . . . . . . . 12 𝐿 = (ℤRHom‘𝑌)
2322zrhrhm 20221 . . . . . . . . . . 11 (𝑌 ∈ Ring → 𝐿 ∈ (ℤring RingHom 𝑌))
2421, 23syl 17 . . . . . . . . . 10 (𝜑𝐿 ∈ (ℤring RingHom 𝑌))
25 zringbas 20185 . . . . . . . . . . 11 ℤ = (Base‘ℤring)
2625, 6rhmf 19083 . . . . . . . . . 10 (𝐿 ∈ (ℤring RingHom 𝑌) → 𝐿:ℤ⟶(Base‘𝑌))
2724, 26syl 17 . . . . . . . . 9 (𝜑𝐿:ℤ⟶(Base‘𝑌))
28 2z 11738 . . . . . . . . . 10 2 ∈ ℤ
29 elfzelz 12636 . . . . . . . . . 10 (𝑘 ∈ (1...((𝑃 − 1) / 2)) → 𝑘 ∈ ℤ)
30 zmulcl 11755 . . . . . . . . . 10 ((2 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (2 · 𝑘) ∈ ℤ)
3128, 29, 30sylancr 583 . . . . . . . . 9 (𝑘 ∈ (1...((𝑃 − 1) / 2)) → (2 · 𝑘) ∈ ℤ)
32 ffvelrn 6607 . . . . . . . . 9 ((𝐿:ℤ⟶(Base‘𝑌) ∧ (2 · 𝑘) ∈ ℤ) → (𝐿‘(2 · 𝑘)) ∈ (Base‘𝑌))
3327, 31, 32syl2an 591 . . . . . . . 8 ((𝜑𝑘 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑘)) ∈ (Base‘𝑌))
3433fmpttd 6635 . . . . . . 7 (𝜑 → (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))):(1...((𝑃 − 1) / 2))⟶(Base‘𝑌))
35 eqid 2826 . . . . . . . 8 (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) = (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘)))
36 fvexd 6449 . . . . . . . 8 ((𝜑𝑘 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑘)) ∈ V)
37 fvexd 6449 . . . . . . . 8 (𝜑 → (0g𝐺) ∈ V)
3835, 19, 36, 37fsuppmptdm 8556 . . . . . . 7 (𝜑 → (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) finSupp (0g𝐺))
39 lgseisen.2 . . . . . . . 8 (𝜑𝑄 ∈ (ℙ ∖ {2}))
40 lgseisen.3 . . . . . . . 8 (𝜑𝑃𝑄)
41 lgseisen.4 . . . . . . . 8 𝑅 = ((𝑄 · (2 · 𝑥)) mod 𝑃)
42 lgseisen.5 . . . . . . . 8 𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))
43 lgseisen.6 . . . . . . . 8 𝑆 = ((𝑄 · (2 · 𝑦)) mod 𝑃)
449, 39, 40, 41, 42, 43lgseisenlem2 25515 . . . . . . 7 (𝜑𝑀:(1...((𝑃 − 1) / 2))–1-1-onto→(1...((𝑃 − 1) / 2)))
457, 8, 18, 19, 34, 38, 44gsumf1o 18671 . . . . . 6 (𝜑 → (𝐺 Σg (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘)))) = (𝐺 Σg ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀)))
464, 45syl5eqr 2876 . . . . 5 (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = (𝐺 Σg ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀)))
479, 39, 40, 41, 42lgseisenlem1 25514 . . . . . . . 8 (𝜑𝑀:(1...((𝑃 − 1) / 2))⟶(1...((𝑃 − 1) / 2)))
4842fmpt 6630 . . . . . . . 8 (∀𝑥 ∈ (1...((𝑃 − 1) / 2))((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ (1...((𝑃 − 1) / 2)) ↔ 𝑀:(1...((𝑃 − 1) / 2))⟶(1...((𝑃 − 1) / 2)))
4947, 48sylibr 226 . . . . . . 7 (𝜑 → ∀𝑥 ∈ (1...((𝑃 − 1) / 2))((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ (1...((𝑃 − 1) / 2)))
5042a1i 11 . . . . . . 7 (𝜑𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))
51 eqidd 2827 . . . . . . 7 (𝜑 → (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) = (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))))
52 oveq2 6914 . . . . . . . 8 (𝑘 = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) → (2 · 𝑘) = (2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))
5352fveq2d 6438 . . . . . . 7 (𝑘 = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) → (𝐿‘(2 · 𝑘)) = (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))))
5449, 50, 51, 53fmptcof 6648 . . . . . 6 (𝜑 → ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))))
5554oveq2d 6922 . . . . 5 (𝜑 → (𝐺 Σg ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀)) = (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))))))
5639eldifad 3811 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑄 ∈ ℙ)
5756adantr 474 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℙ)
58 prmz 15762 . . . . . . . . . . . . . . . . . . . 20 (𝑄 ∈ ℙ → 𝑄 ∈ ℤ)
5957, 58syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℤ)
60 2nn 11425 . . . . . . . . . . . . . . . . . . . . 21 2 ∈ ℕ
61 elfznn 12664 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ)
6261adantl 475 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℕ)
63 nnmulcl 11376 . . . . . . . . . . . . . . . . . . . . 21 ((2 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (2 · 𝑥) ∈ ℕ)
6460, 62, 63sylancr 583 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℕ)
6564nnzd 11810 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℤ)
6659, 65zmulcld 11817 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℤ)
6710adantr 474 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℙ)
68 prmnn 15761 . . . . . . . . . . . . . . . . . . 19 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
6967, 68syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ)
7066, 69zmodcld 12987 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) ∈ ℕ0)
7141, 70syl5eqel 2911 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℕ0)
7271nn0zd 11809 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℤ)
73 m1expcl 13178 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℤ → (-1↑𝑅) ∈ ℤ)
7472, 73syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈ ℤ)
7574, 72zmulcld 11817 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑅) ∈ ℤ)
7675, 69zmodcld 12987 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ0)
7776nn0cnd 11681 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℂ)
78 2cnd 11430 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈ ℂ)
79 2ne0 11463 . . . . . . . . . . . 12 2 ≠ 0
8079a1i 11 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ≠ 0)
8177, 78, 80divcan2d 11130 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)) = (((-1↑𝑅) · 𝑅) mod 𝑃))
8281fveq2d 6438 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))) = (𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃)))
8369nnrpd 12155 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℝ+)
84 eqidd 2827 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) mod 𝑃) = ((-1↑𝑅) mod 𝑃))
8541oveq1i 6916 . . . . . . . . . . . . . 14 (𝑅 mod 𝑃) = (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃)
8666zred 11811 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℝ)
87 modabs2 13000 . . . . . . . . . . . . . . 15 (((𝑄 · (2 · 𝑥)) ∈ ℝ ∧ 𝑃 ∈ ℝ+) → (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃))
8886, 83, 87syl2anc 581 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃))
8985, 88syl5eq 2874 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑅 mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃))
9074, 74, 72, 66, 83, 84, 89modmul12d 13020 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃))
9175zred 11811 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑅) ∈ ℝ)
92 modabs2 13000 . . . . . . . . . . . . 13 ((((-1↑𝑅) · 𝑅) ∈ ℝ ∧ 𝑃 ∈ ℝ+) → ((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = (((-1↑𝑅) · 𝑅) mod 𝑃))
9391, 83, 92syl2anc 581 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = (((-1↑𝑅) · 𝑅) mod 𝑃))
9474zcnd 11812 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈ ℂ)
9559zcnd 11812 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℂ)
9665zcnd 11812 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℂ)
9794, 95, 96mulassd 10381 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) = ((-1↑𝑅) · (𝑄 · (2 · 𝑥))))
9897oveq1d 6921 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃))
9990, 93, 983eqtr4d 2872 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃))
10010, 68syl 17 . . . . . . . . . . . . 13 (𝜑𝑃 ∈ ℕ)
101100adantr 474 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ)
10276nn0zd 11809 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℤ)
10374, 59zmulcld 11817 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑄) ∈ ℤ)
104103, 65zmulcld 11817 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) ∈ ℤ)
105 moddvds 15369 . . . . . . . . . . . 12 ((𝑃 ∈ ℕ ∧ (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℤ ∧ (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) ∈ ℤ) → (((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃) ↔ 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥)))))
106101, 102, 104, 105syl3anc 1496 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃) ↔ 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥)))))
10799, 106mpbid 224 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥))))
10869nnnn0d 11679 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ0)
10911, 22zndvds 20258 . . . . . . . . . . 11 ((𝑃 ∈ ℕ0 ∧ (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℤ ∧ (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) ∈ ℤ) → ((𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃)) = (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) ↔ 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥)))))
110108, 102, 104, 109syl3anc 1496 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃)) = (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) ↔ 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥)))))
111107, 110mpbird 249 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃)) = (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))))
11224adantr 474 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝐿 ∈ (ℤring RingHom 𝑌))
113 zringmulr 20188 . . . . . . . . . . 11 · = (.r‘ℤring)
114 eqid 2826 . . . . . . . . . . 11 (.r𝑌) = (.r𝑌)
11525, 113, 114rhmmul 19084 . . . . . . . . . 10 ((𝐿 ∈ (ℤring RingHom 𝑌) ∧ ((-1↑𝑅) · 𝑄) ∈ ℤ ∧ (2 · 𝑥) ∈ ℤ) → (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) = ((𝐿‘((-1↑𝑅) · 𝑄))(.r𝑌)(𝐿‘(2 · 𝑥))))
116112, 103, 65, 115syl3anc 1496 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) = ((𝐿‘((-1↑𝑅) · 𝑄))(.r𝑌)(𝐿‘(2 · 𝑥))))
11782, 111, 1163eqtrd 2866 . . . . . . . 8 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))) = ((𝐿‘((-1↑𝑅) · 𝑄))(.r𝑌)(𝐿‘(2 · 𝑥))))
118117mpteq2dva 4968 . . . . . . 7 (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((𝐿‘((-1↑𝑅) · 𝑄))(.r𝑌)(𝐿‘(2 · 𝑥)))))
11927adantr 474 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝐿:ℤ⟶(Base‘𝑌))
120119, 103ffvelrnd 6610 . . . . . . . 8 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑𝑅) · 𝑄)) ∈ (Base‘𝑌))
121119, 65ffvelrnd 6610 . . . . . . . 8 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑥)) ∈ (Base‘𝑌))
122 eqidd 2827 . . . . . . . 8 (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))
123 eqidd 2827 . . . . . . . 8 (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))
12419, 120, 121, 122, 123offval2 7175 . . . . . . 7 (𝜑 → ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘𝑓 (.r𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((𝐿‘((-1↑𝑅) · 𝑄))(.r𝑌)(𝐿‘(2 · 𝑥)))))
125118, 124eqtr4d 2865 . . . . . 6 (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))) = ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘𝑓 (.r𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))))
126125oveq2d 6922 . . . . 5 (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))))) = (𝐺 Σg ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘𝑓 (.r𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))))
12746, 55, 1263eqtrd 2866 . . . 4 (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = (𝐺 Σg ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘𝑓 (.r𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))))
1285, 114mgpplusg 18848 . . . . 5 (.r𝑌) = (+g𝐺)
129 eqid 2826 . . . . 5 (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))
130 eqid 2826 . . . . 5 (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))
1317, 128, 18, 19, 120, 121, 129, 130gsummptfidmadd2 18680 . . . 4 (𝜑 → (𝐺 Σg ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘𝑓 (.r𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))(.r𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))))
132127, 131eqtrd 2862 . . 3 (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))(.r𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))))
133132oveq1d 6921 . 2 (𝜑 → ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))(/r𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = (((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))(.r𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))))(/r𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))))
134 eqid 2826 . . . . . 6 (Unit‘𝑌) = (Unit‘𝑌)
135134, 5unitsubm 19025 . . . . 5 (𝑌 ∈ Ring → (Unit‘𝑌) ∈ (SubMnd‘𝐺))
13621, 135syl 17 . . . 4 (𝜑 → (Unit‘𝑌) ∈ (SubMnd‘𝐺))
137 elfzle2 12639 . . . . . . . . . . 11 (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ≤ ((𝑃 − 1) / 2))
138137adantl 475 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ≤ ((𝑃 − 1) / 2))
13962nnred 11368 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℝ)
140 prmuz2 15781 . . . . . . . . . . . . 13 (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ‘2))
141 uz2m1nn 12047 . . . . . . . . . . . . 13 (𝑃 ∈ (ℤ‘2) → (𝑃 − 1) ∈ ℕ)
14267, 140, 1413syl 18 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℕ)
143142nnred 11368 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℝ)
144 2re 11426 . . . . . . . . . . . 12 2 ∈ ℝ
145144a1i 11 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈ ℝ)
146 2pos 11462 . . . . . . . . . . . 12 0 < 2
147146a1i 11 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 < 2)
148 lemuldiv2 11235 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑥) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
149139, 143, 145, 147, 148syl112anc 1499 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((2 · 𝑥) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
150138, 149mpbird 249 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ≤ (𝑃 − 1))
151 prmz 15762 . . . . . . . . . . . 12 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
15267, 151syl 17 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℤ)
153 peano2zm 11749 . . . . . . . . . . 11 (𝑃 ∈ ℤ → (𝑃 − 1) ∈ ℤ)
154152, 153syl 17 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℤ)
155 fznn 12703 . . . . . . . . . 10 ((𝑃 − 1) ∈ ℤ → ((2 · 𝑥) ∈ (1...(𝑃 − 1)) ↔ ((2 · 𝑥) ∈ ℕ ∧ (2 · 𝑥) ≤ (𝑃 − 1))))
156154, 155syl 17 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((2 · 𝑥) ∈ (1...(𝑃 − 1)) ↔ ((2 · 𝑥) ∈ ℕ ∧ (2 · 𝑥) ≤ (𝑃 − 1))))
15764, 150, 156mpbir2and 706 . . . . . . . 8 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ (1...(𝑃 − 1)))
158 fzm1ndvds 15422 . . . . . . . 8 ((𝑃 ∈ ℕ ∧ (2 · 𝑥) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (2 · 𝑥))
15969, 157, 158syl2anc 581 . . . . . . 7 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ (2 · 𝑥))
160 eqid 2826 . . . . . . . . . 10 (0g𝑌) = (0g𝑌)
16111, 22, 160zndvds0 20259 . . . . . . . . 9 ((𝑃 ∈ ℕ0 ∧ (2 · 𝑥) ∈ ℤ) → ((𝐿‘(2 · 𝑥)) = (0g𝑌) ↔ 𝑃 ∥ (2 · 𝑥)))
162108, 65, 161syl2anc 581 . . . . . . . 8 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(2 · 𝑥)) = (0g𝑌) ↔ 𝑃 ∥ (2 · 𝑥)))
163162necon3abid 3036 . . . . . . 7 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(2 · 𝑥)) ≠ (0g𝑌) ↔ ¬ 𝑃 ∥ (2 · 𝑥)))
164159, 163mpbird 249 . . . . . 6 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑥)) ≠ (0g𝑌))
16514simplbi 493 . . . . . . . . 9 (𝑌 ∈ Field → 𝑌 ∈ DivRing)
16613, 165syl 17 . . . . . . . 8 (𝜑𝑌 ∈ DivRing)
167166adantr 474 . . . . . . 7 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑌 ∈ DivRing)
1686, 134, 160drngunit 19109 . . . . . . 7 (𝑌 ∈ DivRing → ((𝐿‘(2 · 𝑥)) ∈ (Unit‘𝑌) ↔ ((𝐿‘(2 · 𝑥)) ∈ (Base‘𝑌) ∧ (𝐿‘(2 · 𝑥)) ≠ (0g𝑌))))
169167, 168syl 17 . . . . . 6 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(2 · 𝑥)) ∈ (Unit‘𝑌) ↔ ((𝐿‘(2 · 𝑥)) ∈ (Base‘𝑌) ∧ (𝐿‘(2 · 𝑥)) ≠ (0g𝑌))))
170121, 164, 169mpbir2and 706 . . . . 5 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑥)) ∈ (Unit‘𝑌))
171170fmpttd 6635 . . . 4 (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))):(1...((𝑃 − 1) / 2))⟶(Unit‘𝑌))
172 fvexd 6449 . . . . 5 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑥)) ∈ V)
173130, 19, 172, 37fsuppmptdm 8556 . . . 4 (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))) finSupp (0g𝐺))
1748, 18, 19, 136, 171, 173gsumsubmcl 18673 . . 3 (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) ∈ (Unit‘𝑌))
175 eqid 2826 . . . 4 (/r𝑌) = (/r𝑌)
176 eqid 2826 . . . 4 (1r𝑌) = (1r𝑌)
177134, 175, 176dvrid 19043 . . 3 ((𝑌 ∈ Ring ∧ (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) ∈ (Unit‘𝑌)) → ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))(/r𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = (1r𝑌))
17821, 174, 177syl2anc 581 . 2 (𝜑 → ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))(/r𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = (1r𝑌))
179120fmpttd 6635 . . . 4 (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))):(1...((𝑃 − 1) / 2))⟶(Base‘𝑌))
180 fvexd 6449 . . . . 5 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑𝑅) · 𝑄)) ∈ V)
181129, 19, 180, 37fsuppmptdm 8556 . . . 4 (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) finSupp (0g𝐺))
1827, 8, 18, 19, 179, 181gsumcl 18670 . . 3 (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) ∈ (Base‘𝑌))
1836, 134, 175, 114dvrcan3 19047 . . 3 ((𝑌 ∈ Ring ∧ (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) ∈ (Base‘𝑌) ∧ (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) ∈ (Unit‘𝑌)) → (((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))(.r𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))))(/r𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))))
18421, 182, 174, 183syl3anc 1496 . 2 (𝜑 → (((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))(.r𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))))(/r𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))))
185133, 178, 1843eqtr3rd 2871 1 (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (1r𝑌))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386   = wceq 1658  wcel 2166  wne 3000  wral 3118  Vcvv 3415  cdif 3796  {csn 4398   class class class wbr 4874  cmpt 4953  ccom 5347  wf 6120  cfv 6124  (class class class)co 6906  𝑓 cof 7156  Fincfn 8223  cr 10252  0cc0 10253  1c1 10254   · cmul 10258   < clt 10392  cle 10393  cmin 10586  -cneg 10587   / cdiv 11010  cn 11351  2c2 11407  0cn0 11619  cz 11705  cuz 11969  +crp 12113  ...cfz 12620   mod cmo 12964  cexp 13155  cdvds 15358  cprime 15758  Basecbs 16223  .rcmulr 16307  0gc0g 16454   Σg cgsu 16455  SubMndcsubmnd 17688  CMndccmn 18547  mulGrpcmgp 18844  1rcur 18856  Ringcrg 18902  CRingccrg 18903  Unitcui 18994  /rcdvr 19037   RingHom crh 19069  DivRingcdr 19104  Fieldcfield 19105  ringzring 20179  ℤRHomczrh 20209  ℤ/nczn 20212
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804  ax-rep 4995  ax-sep 5006  ax-nul 5014  ax-pow 5066  ax-pr 5128  ax-un 7210  ax-inf2 8816  ax-cnex 10309  ax-resscn 10310  ax-1cn 10311  ax-icn 10312  ax-addcl 10313  ax-addrcl 10314  ax-mulcl 10315  ax-mulrcl 10316  ax-mulcom 10317  ax-addass 10318  ax-mulass 10319  ax-distr 10320  ax-i2m1 10321  ax-1ne0 10322  ax-1rid 10323  ax-rnegex 10324  ax-rrecex 10325  ax-cnre 10326  ax-pre-lttri 10327  ax-pre-lttrn 10328  ax-pre-ltadd 10329  ax-pre-mulgt0 10330  ax-pre-sup 10331  ax-addf 10332  ax-mulf 10333
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2606  df-eu 2641  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-ne 3001  df-nel 3104  df-ral 3123  df-rex 3124  df-reu 3125  df-rmo 3126  df-rab 3127  df-v 3417  df-sbc 3664  df-csb 3759  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-pss 3815  df-nul 4146  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4660  df-int 4699  df-iun 4743  df-br 4875  df-opab 4937  df-mpt 4954  df-tr 4977  df-id 5251  df-eprel 5256  df-po 5264  df-so 5265  df-fr 5302  df-se 5303  df-we 5304  df-xp 5349  df-rel 5350  df-cnv 5351  df-co 5352  df-dm 5353  df-rn 5354  df-res 5355  df-ima 5356  df-pred 5921  df-ord 5967  df-on 5968  df-lim 5969  df-suc 5970  df-iota 6087  df-fun 6126  df-fn 6127  df-f 6128  df-f1 6129  df-fo 6130  df-f1o 6131  df-fv 6132  df-isom 6133  df-riota 6867  df-ov 6909  df-oprab 6910  df-mpt2 6911  df-of 7158  df-om 7328  df-1st 7429  df-2nd 7430  df-supp 7561  df-tpos 7618  df-wrecs 7673  df-recs 7735  df-rdg 7773  df-1o 7827  df-2o 7828  df-oadd 7831  df-er 8010  df-ec 8012  df-qs 8016  df-map 8125  df-en 8224  df-dom 8225  df-sdom 8226  df-fin 8227  df-fsupp 8546  df-sup 8618  df-inf 8619  df-oi 8685  df-card 9079  df-cda 9306  df-pnf 10394  df-mnf 10395  df-xr 10396  df-ltxr 10397  df-le 10398  df-sub 10588  df-neg 10589  df-div 11011  df-nn 11352  df-2 11415  df-3 11416  df-4 11417  df-5 11418  df-6 11419  df-7 11420  df-8 11421  df-9 11422  df-n0 11620  df-xnn0 11692  df-z 11706  df-dec 11823  df-uz 11970  df-rp 12114  df-fz 12621  df-fzo 12762  df-fl 12889  df-mod 12965  df-seq 13097  df-exp 13156  df-hash 13412  df-cj 14217  df-re 14218  df-im 14219  df-sqrt 14353  df-abs 14354  df-dvds 15359  df-gcd 15591  df-prm 15759  df-struct 16225  df-ndx 16226  df-slot 16227  df-base 16229  df-sets 16230  df-ress 16231  df-plusg 16319  df-mulr 16320  df-starv 16321  df-sca 16322  df-vsca 16323  df-ip 16324  df-tset 16325  df-ple 16326  df-ds 16328  df-unif 16329  df-0g 16456  df-gsum 16457  df-imas 16522  df-qus 16523  df-mgm 17596  df-sgrp 17638  df-mnd 17649  df-mhm 17689  df-submnd 17690  df-grp 17780  df-minusg 17781  df-sbg 17782  df-mulg 17896  df-subg 17943  df-nsg 17944  df-eqg 17945  df-ghm 18010  df-cntz 18101  df-cmn 18549  df-abl 18550  df-mgp 18845  df-ur 18857  df-ring 18904  df-cring 18905  df-oppr 18978  df-dvdsr 18996  df-unit 18997  df-invr 19027  df-dvr 19038  df-rnghom 19072  df-drng 19106  df-field 19107  df-subrg 19135  df-lmod 19222  df-lss 19290  df-lsp 19332  df-sra 19534  df-rgmod 19535  df-lidl 19536  df-rsp 19537  df-2idl 19594  df-nzr 19620  df-rlreg 19645  df-domn 19646  df-idom 19647  df-cnfld 20108  df-zring 20180  df-zrh 20213  df-zn 20216
This theorem is referenced by:  lgseisenlem4  25517
  Copyright terms: Public domain W3C validator