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

Theorem lgseisenlem3 26282
Description: Lemma for lgseisen 26284. (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 7239 . . . . . . . . 9 (𝑘 = 𝑥 → (2 · 𝑘) = (2 · 𝑥))
21fveq2d 6739 . . . . . . . 8 (𝑘 = 𝑥 → (𝐿‘(2 · 𝑘)) = (𝐿‘(2 · 𝑥)))
32cbvmptv 5172 . . . . . . 7 (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))
43oveq2i 7242 . . . . . 6 (𝐺 Σg (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘)))) = (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))
5 lgseisen.8 . . . . . . . 8 𝐺 = (mulGrp‘𝑌)
6 eqid 2738 . . . . . . . 8 (Base‘𝑌) = (Base‘𝑌)
75, 6mgpbas 19534 . . . . . . 7 (Base‘𝑌) = (Base‘𝐺)
8 eqid 2738 . . . . . . 7 (0g𝐺) = (0g𝐺)
9 lgseisen.1 . . . . . . . . . . 11 (𝜑𝑃 ∈ (ℙ ∖ {2}))
109eldifad 3892 . . . . . . . . . 10 (𝜑𝑃 ∈ ℙ)
11 lgseisen.7 . . . . . . . . . . 11 𝑌 = (ℤ/nℤ‘𝑃)
1211znfld 20549 . . . . . . . . . 10 (𝑃 ∈ ℙ → 𝑌 ∈ Field)
1310, 12syl 17 . . . . . . . . 9 (𝜑𝑌 ∈ Field)
14 isfld 19800 . . . . . . . . . 10 (𝑌 ∈ Field ↔ (𝑌 ∈ DivRing ∧ 𝑌 ∈ CRing))
1514simprbi 500 . . . . . . . . 9 (𝑌 ∈ Field → 𝑌 ∈ CRing)
1613, 15syl 17 . . . . . . . 8 (𝜑𝑌 ∈ CRing)
175crngmgp 19594 . . . . . . . 8 (𝑌 ∈ CRing → 𝐺 ∈ CMnd)
1816, 17syl 17 . . . . . . 7 (𝜑𝐺 ∈ CMnd)
19 fzfid 13570 . . . . . . 7 (𝜑 → (1...((𝑃 − 1) / 2)) ∈ Fin)
20 crngring 19598 . . . . . . . . . . . 12 (𝑌 ∈ CRing → 𝑌 ∈ Ring)
2116, 20syl 17 . . . . . . . . . . 11 (𝜑𝑌 ∈ Ring)
22 lgseisen.9 . . . . . . . . . . . 12 𝐿 = (ℤRHom‘𝑌)
2322zrhrhm 20502 . . . . . . . . . . 11 (𝑌 ∈ Ring → 𝐿 ∈ (ℤring RingHom 𝑌))
2421, 23syl 17 . . . . . . . . . 10 (𝜑𝐿 ∈ (ℤring RingHom 𝑌))
25 zringbas 20465 . . . . . . . . . . 11 ℤ = (Base‘ℤring)
2625, 6rhmf 19770 . . . . . . . . . 10 (𝐿 ∈ (ℤring RingHom 𝑌) → 𝐿:ℤ⟶(Base‘𝑌))
2724, 26syl 17 . . . . . . . . 9 (𝜑𝐿:ℤ⟶(Base‘𝑌))
28 2z 12233 . . . . . . . . . 10 2 ∈ ℤ
29 elfzelz 13136 . . . . . . . . . 10 (𝑘 ∈ (1...((𝑃 − 1) / 2)) → 𝑘 ∈ ℤ)
30 zmulcl 12250 . . . . . . . . . 10 ((2 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (2 · 𝑘) ∈ ℤ)
3128, 29, 30sylancr 590 . . . . . . . . 9 (𝑘 ∈ (1...((𝑃 − 1) / 2)) → (2 · 𝑘) ∈ ℤ)
32 ffvelrn 6920 . . . . . . . . 9 ((𝐿:ℤ⟶(Base‘𝑌) ∧ (2 · 𝑘) ∈ ℤ) → (𝐿‘(2 · 𝑘)) ∈ (Base‘𝑌))
3327, 31, 32syl2an 599 . . . . . . . 8 ((𝜑𝑘 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑘)) ∈ (Base‘𝑌))
3433fmpttd 6950 . . . . . . 7 (𝜑 → (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))):(1...((𝑃 − 1) / 2))⟶(Base‘𝑌))
35 eqid 2738 . . . . . . . 8 (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) = (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘)))
36 fvexd 6750 . . . . . . . 8 ((𝜑𝑘 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑘)) ∈ V)
37 fvexd 6750 . . . . . . . 8 (𝜑 → (0g𝐺) ∈ V)
3835, 19, 36, 37fsuppmptdm 9020 . . . . . . 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 26281 . . . . . . 7 (𝜑𝑀:(1...((𝑃 − 1) / 2))–1-1-onto→(1...((𝑃 − 1) / 2)))
457, 8, 18, 19, 34, 38, 44gsumf1o 19325 . . . . . 6 (𝜑 → (𝐺 Σg (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘)))) = (𝐺 Σg ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀)))
464, 45eqtr3id 2793 . . . . 5 (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = (𝐺 Σg ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀)))
479, 39, 40, 41, 42lgseisenlem1 26280 . . . . . . . 8 (𝜑𝑀:(1...((𝑃 − 1) / 2))⟶(1...((𝑃 − 1) / 2)))
4842fmpt 6945 . . . . . . . 8 (∀𝑥 ∈ (1...((𝑃 − 1) / 2))((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ (1...((𝑃 − 1) / 2)) ↔ 𝑀:(1...((𝑃 − 1) / 2))⟶(1...((𝑃 − 1) / 2)))
4947, 48sylibr 237 . . . . . . 7 (𝜑 → ∀𝑥 ∈ (1...((𝑃 − 1) / 2))((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) ∈ (1...((𝑃 − 1) / 2)))
5042a1i 11 . . . . . . 7 (𝜑𝑀 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))
51 eqidd 2739 . . . . . . 7 (𝜑 → (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) = (𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))))
52 oveq2 7239 . . . . . . . 8 (𝑘 = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) → (2 · 𝑘) = (2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))
5352fveq2d 6739 . . . . . . 7 (𝑘 = ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2) → (𝐿‘(2 · 𝑘)) = (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))))
5449, 50, 51, 53fmptcof 6963 . . . . . 6 (𝜑 → ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))))
5554oveq2d 7247 . . . . 5 (𝜑 → (𝐺 Σg ((𝑘 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑘))) ∘ 𝑀)) = (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))))))
5639eldifad 3892 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑄 ∈ ℙ)
5756adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℙ)
58 prmz 16256 . . . . . . . . . . . . . . . . . . . 20 (𝑄 ∈ ℙ → 𝑄 ∈ ℤ)
5957, 58syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℤ)
60 2nn 11927 . . . . . . . . . . . . . . . . . . . . 21 2 ∈ ℕ
61 elfznn 13165 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ)
6261adantl 485 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℕ)
63 nnmulcl 11878 . . . . . . . . . . . . . . . . . . . . 21 ((2 ∈ ℕ ∧ 𝑥 ∈ ℕ) → (2 · 𝑥) ∈ ℕ)
6460, 62, 63sylancr 590 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℕ)
6564nnzd 12305 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℤ)
6659, 65zmulcld 12312 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℤ)
6710adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℙ)
68 prmnn 16255 . . . . . . . . . . . . . . . . . . 19 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
6967, 68syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ)
7066, 69zmodcld 13489 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝑄 · (2 · 𝑥)) mod 𝑃) ∈ ℕ0)
7141, 70eqeltrid 2843 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℕ0)
7271nn0zd 12304 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑅 ∈ ℤ)
73 m1expcl 13682 . . . . . . . . . . . . . . 15 (𝑅 ∈ ℤ → (-1↑𝑅) ∈ ℤ)
7472, 73syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈ ℤ)
7574, 72zmulcld 12312 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑅) ∈ ℤ)
7675, 69zmodcld 13489 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℕ0)
7776nn0cnd 12176 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℂ)
78 2cnd 11932 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈ ℂ)
79 2ne0 11958 . . . . . . . . . . . 12 2 ≠ 0
8079a1i 11 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ≠ 0)
8177, 78, 80divcan2d 11634 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)) = (((-1↑𝑅) · 𝑅) mod 𝑃))
8281fveq2d 6739 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))) = (𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃)))
8369nnrpd 12650 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℝ+)
84 eqidd 2739 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) mod 𝑃) = ((-1↑𝑅) mod 𝑃))
8541oveq1i 7241 . . . . . . . . . . . . . 14 (𝑅 mod 𝑃) = (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃)
8666zred 12306 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑄 · (2 · 𝑥)) ∈ ℝ)
87 modabs2 13502 . . . . . . . . . . . . . . 15 (((𝑄 · (2 · 𝑥)) ∈ ℝ ∧ 𝑃 ∈ ℝ+) → (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃))
8886, 83, 87syl2anc 587 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((𝑄 · (2 · 𝑥)) mod 𝑃) mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃))
8985, 88syl5eq 2791 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑅 mod 𝑃) = ((𝑄 · (2 · 𝑥)) mod 𝑃))
9074, 74, 72, 66, 83, 84, 89modmul12d 13522 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃))
9175zred 12306 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑅) ∈ ℝ)
92 modabs2 13502 . . . . . . . . . . . . 13 ((((-1↑𝑅) · 𝑅) ∈ ℝ ∧ 𝑃 ∈ ℝ+) → ((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = (((-1↑𝑅) · 𝑅) mod 𝑃))
9391, 83, 92syl2anc 587 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = (((-1↑𝑅) · 𝑅) mod 𝑃))
9474zcnd 12307 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (-1↑𝑅) ∈ ℂ)
9559zcnd 12307 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑄 ∈ ℂ)
9665zcnd 12307 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ ℂ)
9794, 95, 96mulassd 10880 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) = ((-1↑𝑅) · (𝑄 · (2 · 𝑥))))
9897oveq1d 7246 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃) = (((-1↑𝑅) · (𝑄 · (2 · 𝑥))) mod 𝑃))
9990, 93, 983eqtr4d 2788 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃))
10010, 68syl 17 . . . . . . . . . . . . 13 (𝜑𝑃 ∈ ℕ)
101100adantr 484 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ)
10276nn0zd 12304 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℤ)
10374, 59zmulcld 12312 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((-1↑𝑅) · 𝑄) ∈ ℤ)
104103, 65zmulcld 12312 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) ∈ ℤ)
105 moddvds 15850 . . . . . . . . . . . 12 ((𝑃 ∈ ℕ ∧ (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℤ ∧ (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) ∈ ℤ) → (((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃) ↔ 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥)))))
106101, 102, 104, 105syl3anc 1373 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (((((-1↑𝑅) · 𝑅) mod 𝑃) mod 𝑃) = ((((-1↑𝑅) · 𝑄) · (2 · 𝑥)) mod 𝑃) ↔ 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥)))))
10799, 106mpbid 235 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥))))
10869nnnn0d 12174 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ0)
10911, 22zndvds 20538 . . . . . . . . . . 11 ((𝑃 ∈ ℕ0 ∧ (((-1↑𝑅) · 𝑅) mod 𝑃) ∈ ℤ ∧ (((-1↑𝑅) · 𝑄) · (2 · 𝑥)) ∈ ℤ) → ((𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃)) = (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) ↔ 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥)))))
110108, 102, 104, 109syl3anc 1373 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃)) = (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) ↔ 𝑃 ∥ ((((-1↑𝑅) · 𝑅) mod 𝑃) − (((-1↑𝑅) · 𝑄) · (2 · 𝑥)))))
111107, 110mpbird 260 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(((-1↑𝑅) · 𝑅) mod 𝑃)) = (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))))
11224adantr 484 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝐿 ∈ (ℤring RingHom 𝑌))
113 zringmulr 20468 . . . . . . . . . . 11 · = (.r‘ℤring)
114 eqid 2738 . . . . . . . . . . 11 (.r𝑌) = (.r𝑌)
11525, 113, 114rhmmul 19771 . . . . . . . . . 10 ((𝐿 ∈ (ℤring RingHom 𝑌) ∧ ((-1↑𝑅) · 𝑄) ∈ ℤ ∧ (2 · 𝑥) ∈ ℤ) → (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) = ((𝐿‘((-1↑𝑅) · 𝑄))(.r𝑌)(𝐿‘(2 · 𝑥))))
116112, 103, 65, 115syl3anc 1373 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(((-1↑𝑅) · 𝑄) · (2 · 𝑥))) = ((𝐿‘((-1↑𝑅) · 𝑄))(.r𝑌)(𝐿‘(2 · 𝑥))))
11782, 111, 1163eqtrd 2782 . . . . . . . 8 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))) = ((𝐿‘((-1↑𝑅) · 𝑄))(.r𝑌)(𝐿‘(2 · 𝑥))))
118117mpteq2dva 5164 . . . . . . 7 (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((𝐿‘((-1↑𝑅) · 𝑄))(.r𝑌)(𝐿‘(2 · 𝑥)))))
11927adantr 484 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝐿:ℤ⟶(Base‘𝑌))
120119, 103ffvelrnd 6923 . . . . . . . 8 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑𝑅) · 𝑄)) ∈ (Base‘𝑌))
121119, 65ffvelrnd 6923 . . . . . . . 8 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑥)) ∈ (Base‘𝑌))
122 eqidd 2739 . . . . . . . 8 (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))
123 eqidd 2739 . . . . . . . 8 (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))
12419, 120, 121, 122, 123offval2 7506 . . . . . . 7 (𝜑 → ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘f (.r𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ ((𝐿‘((-1↑𝑅) · 𝑄))(.r𝑌)(𝐿‘(2 · 𝑥)))))
125118, 124eqtr4d 2781 . . . . . 6 (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2)))) = ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘f (.r𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))))
126125oveq2d 7247 . . . . 5 (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · ((((-1↑𝑅) · 𝑅) mod 𝑃) / 2))))) = (𝐺 Σg ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘f (.r𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))))
12746, 55, 1263eqtrd 2782 . . . 4 (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = (𝐺 Σg ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘f (.r𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))))
1285, 114mgpplusg 19532 . . . . 5 (.r𝑌) = (+g𝐺)
129 eqid 2738 . . . . 5 (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))
130 eqid 2738 . . . . 5 (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))
1317, 128, 18, 19, 120, 121, 129, 130gsummptfidmadd2 19335 . . . 4 (𝜑 → (𝐺 Σg ((𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) ∘f (.r𝑌)(𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))(.r𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))))
132127, 131eqtrd 2778 . . 3 (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) = ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))))(.r𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))))
133132oveq1d 7246 . 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 2738 . . . . . 6 (Unit‘𝑌) = (Unit‘𝑌)
135134, 5unitsubm 19712 . . . . 5 (𝑌 ∈ Ring → (Unit‘𝑌) ∈ (SubMnd‘𝐺))
13621, 135syl 17 . . . 4 (𝜑 → (Unit‘𝑌) ∈ (SubMnd‘𝐺))
137 elfzle2 13140 . . . . . . . . . . 11 (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ≤ ((𝑃 − 1) / 2))
138137adantl 485 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ≤ ((𝑃 − 1) / 2))
13962nnred 11869 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑥 ∈ ℝ)
140 prmuz2 16277 . . . . . . . . . . . . 13 (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ‘2))
141 uz2m1nn 12543 . . . . . . . . . . . . 13 (𝑃 ∈ (ℤ‘2) → (𝑃 − 1) ∈ ℕ)
14267, 140, 1413syl 18 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℕ)
143142nnred 11869 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℝ)
144 2re 11928 . . . . . . . . . . . 12 2 ∈ ℝ
145144a1i 11 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈ ℝ)
146 2pos 11957 . . . . . . . . . . . 12 0 < 2
147146a1i 11 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 0 < 2)
148 lemuldiv2 11737 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑥) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
149139, 143, 145, 147, 148syl112anc 1376 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((2 · 𝑥) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
150138, 149mpbird 260 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ≤ (𝑃 − 1))
151 prmz 16256 . . . . . . . . . . . 12 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
15267, 151syl 17 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℤ)
153 peano2zm 12244 . . . . . . . . . . 11 (𝑃 ∈ ℤ → (𝑃 − 1) ∈ ℤ)
154152, 153syl 17 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 − 1) ∈ ℤ)
155 fznn 13204 . . . . . . . . . 10 ((𝑃 − 1) ∈ ℤ → ((2 · 𝑥) ∈ (1...(𝑃 − 1)) ↔ ((2 · 𝑥) ∈ ℕ ∧ (2 · 𝑥) ≤ (𝑃 − 1))))
156154, 155syl 17 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((2 · 𝑥) ∈ (1...(𝑃 − 1)) ↔ ((2 · 𝑥) ∈ ℕ ∧ (2 · 𝑥) ≤ (𝑃 − 1))))
15764, 150, 156mpbir2and 713 . . . . . . . 8 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (2 · 𝑥) ∈ (1...(𝑃 − 1)))
158 fzm1ndvds 15907 . . . . . . . 8 ((𝑃 ∈ ℕ ∧ (2 · 𝑥) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (2 · 𝑥))
15969, 157, 158syl2anc 587 . . . . . . 7 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ (2 · 𝑥))
160 eqid 2738 . . . . . . . . . 10 (0g𝑌) = (0g𝑌)
16111, 22, 160zndvds0 20539 . . . . . . . . 9 ((𝑃 ∈ ℕ0 ∧ (2 · 𝑥) ∈ ℤ) → ((𝐿‘(2 · 𝑥)) = (0g𝑌) ↔ 𝑃 ∥ (2 · 𝑥)))
162108, 65, 161syl2anc 587 . . . . . . . 8 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(2 · 𝑥)) = (0g𝑌) ↔ 𝑃 ∥ (2 · 𝑥)))
163162necon3abid 2978 . . . . . . 7 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(2 · 𝑥)) ≠ (0g𝑌) ↔ ¬ 𝑃 ∥ (2 · 𝑥)))
164159, 163mpbird 260 . . . . . 6 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑥)) ≠ (0g𝑌))
16514simplbi 501 . . . . . . . . 9 (𝑌 ∈ Field → 𝑌 ∈ DivRing)
16613, 165syl 17 . . . . . . . 8 (𝜑𝑌 ∈ DivRing)
167166adantr 484 . . . . . . 7 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → 𝑌 ∈ DivRing)
1686, 134, 160drngunit 19796 . . . . . . 7 (𝑌 ∈ DivRing → ((𝐿‘(2 · 𝑥)) ∈ (Unit‘𝑌) ↔ ((𝐿‘(2 · 𝑥)) ∈ (Base‘𝑌) ∧ (𝐿‘(2 · 𝑥)) ≠ (0g𝑌))))
169167, 168syl 17 . . . . . 6 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(2 · 𝑥)) ∈ (Unit‘𝑌) ↔ ((𝐿‘(2 · 𝑥)) ∈ (Base‘𝑌) ∧ (𝐿‘(2 · 𝑥)) ≠ (0g𝑌))))
170121, 164, 169mpbir2and 713 . . . . 5 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑥)) ∈ (Unit‘𝑌))
171170fmpttd 6950 . . . 4 (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))):(1...((𝑃 − 1) / 2))⟶(Unit‘𝑌))
172 fvexd 6750 . . . . 5 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(2 · 𝑥)) ∈ V)
173130, 19, 172, 37fsuppmptdm 9020 . . . 4 (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))) finSupp (0g𝐺))
1748, 18, 19, 136, 171, 173gsumsubmcl 19328 . . 3 (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) ∈ (Unit‘𝑌))
175 eqid 2738 . . . 4 (/r𝑌) = (/r𝑌)
176 eqid 2738 . . . 4 (1r𝑌) = (1r𝑌)
177134, 175, 176dvrid 19730 . . 3 ((𝑌 ∈ Ring ∧ (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥)))) ∈ (Unit‘𝑌)) → ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))(/r𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = (1r𝑌))
17821, 174, 177syl2anc 587 . 2 (𝜑 → ((𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))(/r𝑌)(𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(2 · 𝑥))))) = (1r𝑌))
179120fmpttd 6950 . . . 4 (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))):(1...((𝑃 − 1) / 2))⟶(Base‘𝑌))
180 fvexd 6750 . . . . 5 ((𝜑𝑥 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘((-1↑𝑅) · 𝑄)) ∈ V)
181129, 19, 180, 37fsuppmptdm 9020 . . . 4 (𝜑 → (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄))) finSupp (0g𝐺))
1827, 8, 18, 19, 179, 181gsumcl 19324 . . 3 (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) ∈ (Base‘𝑌))
1836, 134, 175, 114dvrcan3 19734 . . 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 1373 . 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 2787 1 (𝜑 → (𝐺 Σg (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘((-1↑𝑅) · 𝑄)))) = (1r𝑌))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399   = wceq 1543  wcel 2111  wne 2941  wral 3062  Vcvv 3420  cdif 3877  {csn 4555   class class class wbr 5067  cmpt 5149  ccom 5569  wf 6393  cfv 6397  (class class class)co 7231  f cof 7485  Fincfn 8646  cr 10752  0cc0 10753  1c1 10754   · cmul 10758   < clt 10891  cle 10892  cmin 11086  -cneg 11087   / cdiv 11513  cn 11854  2c2 11909  0cn0 12114  cz 12200  cuz 12462  +crp 12610  ...cfz 13119   mod cmo 13466  cexp 13659  cdvds 15839  cprime 16252  Basecbs 16784  .rcmulr 16827  0gc0g 16968   Σg cgsu 16969  SubMndcsubmnd 18241  CMndccmn 19194  mulGrpcmgp 19528  1rcur 19540  Ringcrg 19586  CRingccrg 19587  Unitcui 19681  /rcdvr 19724   RingHom crh 19756  DivRingcdr 19791  Fieldcfield 19792  ringzring 20459  ℤRHomczrh 20490  ℤ/nczn 20493
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-rep 5193  ax-sep 5206  ax-nul 5213  ax-pow 5272  ax-pr 5336  ax-un 7541  ax-cnex 10809  ax-resscn 10810  ax-1cn 10811  ax-icn 10812  ax-addcl 10813  ax-addrcl 10814  ax-mulcl 10815  ax-mulrcl 10816  ax-mulcom 10817  ax-addass 10818  ax-mulass 10819  ax-distr 10820  ax-i2m1 10821  ax-1ne0 10822  ax-1rid 10823  ax-rnegex 10824  ax-rrecex 10825  ax-cnre 10826  ax-pre-lttri 10827  ax-pre-lttrn 10828  ax-pre-ltadd 10829  ax-pre-mulgt0 10830  ax-pre-sup 10831  ax-addf 10832  ax-mulf 10833
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-reu 3069  df-rmo 3070  df-rab 3071  df-v 3422  df-sbc 3709  df-csb 3826  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-pss 3899  df-nul 4252  df-if 4454  df-pw 4529  df-sn 4556  df-pr 4558  df-tp 4560  df-op 4562  df-uni 4834  df-int 4874  df-iun 4920  df-br 5068  df-opab 5130  df-mpt 5150  df-tr 5176  df-id 5469  df-eprel 5474  df-po 5482  df-so 5483  df-fr 5523  df-se 5524  df-we 5525  df-xp 5571  df-rel 5572  df-cnv 5573  df-co 5574  df-dm 5575  df-rn 5576  df-res 5577  df-ima 5578  df-pred 6175  df-ord 6233  df-on 6234  df-lim 6235  df-suc 6236  df-iota 6355  df-fun 6399  df-fn 6400  df-f 6401  df-f1 6402  df-fo 6403  df-f1o 6404  df-fv 6405  df-isom 6406  df-riota 7188  df-ov 7234  df-oprab 7235  df-mpo 7236  df-of 7487  df-om 7663  df-1st 7779  df-2nd 7780  df-supp 7924  df-tpos 7988  df-wrecs 8067  df-recs 8128  df-rdg 8166  df-1o 8222  df-2o 8223  df-oadd 8226  df-er 8411  df-ec 8413  df-qs 8417  df-map 8530  df-en 8647  df-dom 8648  df-sdom 8649  df-fin 8650  df-fsupp 9010  df-sup 9082  df-inf 9083  df-oi 9150  df-dju 9541  df-card 9579  df-pnf 10893  df-mnf 10894  df-xr 10895  df-ltxr 10896  df-le 10897  df-sub 11088  df-neg 11089  df-div 11514  df-nn 11855  df-2 11917  df-3 11918  df-4 11919  df-5 11920  df-6 11921  df-7 11922  df-8 11923  df-9 11924  df-n0 12115  df-xnn0 12187  df-z 12201  df-dec 12318  df-uz 12463  df-rp 12611  df-fz 13120  df-fzo 13263  df-fl 13391  df-mod 13467  df-seq 13599  df-exp 13660  df-hash 13921  df-cj 14686  df-re 14687  df-im 14688  df-sqrt 14822  df-abs 14823  df-dvds 15840  df-gcd 16078  df-prm 16253  df-struct 16724  df-sets 16741  df-slot 16759  df-ndx 16769  df-base 16785  df-ress 16809  df-plusg 16839  df-mulr 16840  df-starv 16841  df-sca 16842  df-vsca 16843  df-ip 16844  df-tset 16845  df-ple 16846  df-ds 16848  df-unif 16849  df-0g 16970  df-gsum 16971  df-imas 17037  df-qus 17038  df-mgm 18138  df-sgrp 18187  df-mnd 18198  df-mhm 18242  df-submnd 18243  df-grp 18392  df-minusg 18393  df-sbg 18394  df-mulg 18513  df-subg 18564  df-nsg 18565  df-eqg 18566  df-ghm 18644  df-cntz 18735  df-cmn 19196  df-abl 19197  df-mgp 19529  df-ur 19541  df-ring 19588  df-cring 19589  df-oppr 19665  df-dvdsr 19683  df-unit 19684  df-invr 19714  df-dvr 19725  df-rnghom 19759  df-drng 19793  df-field 19794  df-subrg 19822  df-lmod 19925  df-lss 19993  df-lsp 20033  df-sra 20233  df-rgmod 20234  df-lidl 20235  df-rsp 20236  df-2idl 20294  df-nzr 20320  df-rlreg 20345  df-domn 20346  df-idom 20347  df-cnfld 20388  df-zring 20460  df-zrh 20494  df-zn 20497
This theorem is referenced by:  lgseisenlem4  26283
  Copyright terms: Public domain W3C validator