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

Theorem 2sqreultlem 26130
 Description: Lemma for 2sqreult 26141. (Contributed by AV, 8-Jun-2023.) (Proposed by GL, 8-Jun-2023.)
Assertion
Ref Expression
2sqreultlem ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))
Distinct variable group:   𝑃,𝑎,𝑏

Proof of Theorem 2sqreultlem
StepHypRef Expression
1 2sqreulem1 26129 . 2 ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))
2 oveq1 7157 . . . . . . . . . . . . . . 15 (𝑏 = 𝑎 → (𝑏↑2) = (𝑎↑2))
32oveq2d 7166 . . . . . . . . . . . . . 14 (𝑏 = 𝑎 → ((𝑎↑2) + (𝑏↑2)) = ((𝑎↑2) + (𝑎↑2)))
43adantr 484 . . . . . . . . . . . . 13 ((𝑏 = 𝑎 ∧ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℕ0)) → ((𝑎↑2) + (𝑏↑2)) = ((𝑎↑2) + (𝑎↑2)))
5 nn0cn 11944 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ ℕ0𝑎 ∈ ℂ)
65sqcld 13558 . . . . . . . . . . . . . . . 16 (𝑎 ∈ ℕ0 → (𝑎↑2) ∈ ℂ)
7 2times 11810 . . . . . . . . . . . . . . . . 17 ((𝑎↑2) ∈ ℂ → (2 · (𝑎↑2)) = ((𝑎↑2) + (𝑎↑2)))
87eqcomd 2764 . . . . . . . . . . . . . . . 16 ((𝑎↑2) ∈ ℂ → ((𝑎↑2) + (𝑎↑2)) = (2 · (𝑎↑2)))
96, 8syl 17 . . . . . . . . . . . . . . 15 (𝑎 ∈ ℕ0 → ((𝑎↑2) + (𝑎↑2)) = (2 · (𝑎↑2)))
109adantl 485 . . . . . . . . . . . . . 14 (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0) → ((𝑎↑2) + (𝑎↑2)) = (2 · (𝑎↑2)))
1110ad2antrl 727 . . . . . . . . . . . . 13 ((𝑏 = 𝑎 ∧ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℕ0)) → ((𝑎↑2) + (𝑎↑2)) = (2 · (𝑎↑2)))
124, 11eqtrd 2793 . . . . . . . . . . . 12 ((𝑏 = 𝑎 ∧ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℕ0)) → ((𝑎↑2) + (𝑏↑2)) = (2 · (𝑎↑2)))
1312eqeq1d 2760 . . . . . . . . . . 11 ((𝑏 = 𝑎 ∧ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℕ0)) → (((𝑎↑2) + (𝑏↑2)) = 𝑃 ↔ (2 · (𝑎↑2)) = 𝑃))
14 oveq1 7157 . . . . . . . . . . . . . . . . . . . 20 (𝑃 = (2 · (𝑎↑2)) → (𝑃 mod 4) = ((2 · (𝑎↑2)) mod 4))
1514eqeq1d 2760 . . . . . . . . . . . . . . . . . . 19 (𝑃 = (2 · (𝑎↑2)) → ((𝑃 mod 4) = 1 ↔ ((2 · (𝑎↑2)) mod 4) = 1))
16 eleq1 2839 . . . . . . . . . . . . . . . . . . 19 (𝑃 = (2 · (𝑎↑2)) → (𝑃 ∈ ℙ ↔ (2 · (𝑎↑2)) ∈ ℙ))
1715, 16anbi12d 633 . . . . . . . . . . . . . . . . . 18 (𝑃 = (2 · (𝑎↑2)) → (((𝑃 mod 4) = 1 ∧ 𝑃 ∈ ℙ) ↔ (((2 · (𝑎↑2)) mod 4) = 1 ∧ (2 · (𝑎↑2)) ∈ ℙ)))
18 nn0z 12044 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 ∈ ℕ0𝑎 ∈ ℤ)
19 2nn0 11951 . . . . . . . . . . . . . . . . . . . . . . 23 2 ∈ ℕ0
20 zexpcl 13494 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎 ∈ ℤ ∧ 2 ∈ ℕ0) → (𝑎↑2) ∈ ℤ)
2118, 19, 20sylancl 589 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 ∈ ℕ0 → (𝑎↑2) ∈ ℤ)
22 2mulprm 16089 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎↑2) ∈ ℤ → ((2 · (𝑎↑2)) ∈ ℙ ↔ (𝑎↑2) = 1))
2321, 22syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 ∈ ℕ0 → ((2 · (𝑎↑2)) ∈ ℙ ↔ (𝑎↑2) = 1))
24 oveq2 7158 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎↑2) = 1 → (2 · (𝑎↑2)) = (2 · 1))
25 2t1e2 11837 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (2 · 1) = 2
2624, 25eqtrdi 2809 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎↑2) = 1 → (2 · (𝑎↑2)) = 2)
2726oveq1d 7165 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎↑2) = 1 → ((2 · (𝑎↑2)) mod 4) = (2 mod 4))
28 2re 11748 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ∈ ℝ
29 4nn 11757 . . . . . . . . . . . . . . . . . . . . . . . . . 26 4 ∈ ℕ
30 nnrp 12441 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (4 ∈ ℕ → 4 ∈ ℝ+)
3129, 30ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25 4 ∈ ℝ+
32 0le2 11776 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 ≤ 2
33 2lt4 11849 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 < 4
34 modid 13313 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((2 ∈ ℝ ∧ 4 ∈ ℝ+) ∧ (0 ≤ 2 ∧ 2 < 4)) → (2 mod 4) = 2)
3528, 31, 32, 33, 34mp4an 692 . . . . . . . . . . . . . . . . . . . . . . . 24 (2 mod 4) = 2
3627, 35eqtrdi 2809 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎↑2) = 1 → ((2 · (𝑎↑2)) mod 4) = 2)
3736eqeq1d 2760 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎↑2) = 1 → (((2 · (𝑎↑2)) mod 4) = 1 ↔ 2 = 1))
38 1ne2 11882 . . . . . . . . . . . . . . . . . . . . . . 23 1 ≠ 2
39 eqcom 2765 . . . . . . . . . . . . . . . . . . . . . . . 24 (2 = 1 ↔ 1 = 2)
40 eqneqall 2962 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 = 2 → (1 ≠ 2 → (𝑎𝑏𝑏𝑎)))
4140com12 32 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 ≠ 2 → (1 = 2 → (𝑎𝑏𝑏𝑎)))
4239, 41syl5bi 245 . . . . . . . . . . . . . . . . . . . . . . 23 (1 ≠ 2 → (2 = 1 → (𝑎𝑏𝑏𝑎)))
4338, 42ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (2 = 1 → (𝑎𝑏𝑏𝑎))
4437, 43syl6bi 256 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎↑2) = 1 → (((2 · (𝑎↑2)) mod 4) = 1 → (𝑎𝑏𝑏𝑎)))
4523, 44syl6bi 256 . . . . . . . . . . . . . . . . . . . 20 (𝑎 ∈ ℕ0 → ((2 · (𝑎↑2)) ∈ ℙ → (((2 · (𝑎↑2)) mod 4) = 1 → (𝑎𝑏𝑏𝑎))))
4645impcomd 415 . . . . . . . . . . . . . . . . . . 19 (𝑎 ∈ ℕ0 → ((((2 · (𝑎↑2)) mod 4) = 1 ∧ (2 · (𝑎↑2)) ∈ ℙ) → (𝑎𝑏𝑏𝑎)))
4746com12 32 . . . . . . . . . . . . . . . . . 18 ((((2 · (𝑎↑2)) mod 4) = 1 ∧ (2 · (𝑎↑2)) ∈ ℙ) → (𝑎 ∈ ℕ0 → (𝑎𝑏𝑏𝑎)))
4817, 47syl6bi 256 . . . . . . . . . . . . . . . . 17 (𝑃 = (2 · (𝑎↑2)) → (((𝑃 mod 4) = 1 ∧ 𝑃 ∈ ℙ) → (𝑎 ∈ ℕ0 → (𝑎𝑏𝑏𝑎))))
4948expd 419 . . . . . . . . . . . . . . . 16 (𝑃 = (2 · (𝑎↑2)) → ((𝑃 mod 4) = 1 → (𝑃 ∈ ℙ → (𝑎 ∈ ℕ0 → (𝑎𝑏𝑏𝑎)))))
5049com34 91 . . . . . . . . . . . . . . 15 (𝑃 = (2 · (𝑎↑2)) → ((𝑃 mod 4) = 1 → (𝑎 ∈ ℕ0 → (𝑃 ∈ ℙ → (𝑎𝑏𝑏𝑎)))))
5150eqcoms 2766 . . . . . . . . . . . . . 14 ((2 · (𝑎↑2)) = 𝑃 → ((𝑃 mod 4) = 1 → (𝑎 ∈ ℕ0 → (𝑃 ∈ ℙ → (𝑎𝑏𝑏𝑎)))))
5251com14 96 . . . . . . . . . . . . 13 (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 → (𝑎 ∈ ℕ0 → ((2 · (𝑎↑2)) = 𝑃 → (𝑎𝑏𝑏𝑎)))))
5352imp31 421 . . . . . . . . . . . 12 (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0) → ((2 · (𝑎↑2)) = 𝑃 → (𝑎𝑏𝑏𝑎)))
5453ad2antrl 727 . . . . . . . . . . 11 ((𝑏 = 𝑎 ∧ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℕ0)) → ((2 · (𝑎↑2)) = 𝑃 → (𝑎𝑏𝑏𝑎)))
5513, 54sylbid 243 . . . . . . . . . 10 ((𝑏 = 𝑎 ∧ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℕ0)) → (((𝑎↑2) + (𝑏↑2)) = 𝑃 → (𝑎𝑏𝑏𝑎)))
5655expimpd 457 . . . . . . . . 9 (𝑏 = 𝑎 → (((((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℕ0) ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) → (𝑎𝑏𝑏𝑎)))
57 2a1 28 . . . . . . . . 9 (𝑏𝑎 → (((((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℕ0) ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) → (𝑎𝑏𝑏𝑎)))
5856, 57pm2.61ine 3034 . . . . . . . 8 (((((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℕ0) ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) → (𝑎𝑏𝑏𝑎))
5958pm4.71d 565 . . . . . . 7 (((((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℕ0) ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) → (𝑎𝑏 ↔ (𝑎𝑏𝑏𝑎)))
60 nn0re 11943 . . . . . . . . . . 11 (𝑎 ∈ ℕ0𝑎 ∈ ℝ)
6160adantl 485 . . . . . . . . . 10 (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0) → 𝑎 ∈ ℝ)
62 nn0re 11943 . . . . . . . . . 10 (𝑏 ∈ ℕ0𝑏 ∈ ℝ)
63 ltlen 10779 . . . . . . . . . 10 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑎 < 𝑏 ↔ (𝑎𝑏𝑏𝑎)))
6461, 62, 63syl2an 598 . . . . . . . . 9 ((((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℕ0) → (𝑎 < 𝑏 ↔ (𝑎𝑏𝑏𝑎)))
6564bibi2d 346 . . . . . . . 8 ((((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℕ0) → ((𝑎𝑏𝑎 < 𝑏) ↔ (𝑎𝑏 ↔ (𝑎𝑏𝑏𝑎))))
6665adantr 484 . . . . . . 7 (((((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℕ0) ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) → ((𝑎𝑏𝑎 < 𝑏) ↔ (𝑎𝑏 ↔ (𝑎𝑏𝑏𝑎))))
6759, 66mpbird 260 . . . . . 6 (((((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℕ0) ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) → (𝑎𝑏𝑎 < 𝑏))
6867ex 416 . . . . 5 ((((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℕ0) → (((𝑎↑2) + (𝑏↑2)) = 𝑃 → (𝑎𝑏𝑎 < 𝑏)))
6968pm5.32rd 581 . . . 4 ((((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℕ0) → ((𝑎𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) ↔ (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)))
7069reubidva 3306 . . 3 (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) ∧ 𝑎 ∈ ℕ0) → (∃!𝑏 ∈ ℕ0 (𝑎𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) ↔ ∃!𝑏 ∈ ℕ0 (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)))
7170reubidva 3306 . 2 ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → (∃!𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃) ↔ ∃!𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃)))
721, 71mpbid 235 1 ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑎 ∈ ℕ0 ∃!𝑏 ∈ ℕ0 (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ≠ wne 2951  ∃!wreu 3072   class class class wbr 5032  (class class class)co 7150  ℂcc 10573  ℝcr 10574  0cc0 10575  1c1 10576   + caddc 10578   · cmul 10580   < clt 10713   ≤ cle 10714  ℕcn 11674  2c2 11729  4c4 11731  ℕ0cn0 11934  ℤcz 12020  ℝ+crp 12430   mod cmo 13286  ↑cexp 13479  ℙcprime 16067 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5156  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459  ax-cnex 10631  ax-resscn 10632  ax-1cn 10633  ax-icn 10634  ax-addcl 10635  ax-addrcl 10636  ax-mulcl 10637  ax-mulrcl 10638  ax-mulcom 10639  ax-addass 10640  ax-mulass 10641  ax-distr 10642  ax-i2m1 10643  ax-1ne0 10644  ax-1rid 10645  ax-rnegex 10646  ax-rrecex 10647  ax-cnre 10648  ax-pre-lttri 10649  ax-pre-lttrn 10650  ax-pre-ltadd 10651  ax-pre-mulgt0 10652  ax-pre-sup 10653  ax-addf 10654  ax-mulf 10655 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-tp 4527  df-op 4529  df-uni 4799  df-int 4839  df-iun 4885  df-iin 4886  df-br 5033  df-opab 5095  df-mpt 5113  df-tr 5139  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5483  df-se 5484  df-we 5485  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-isom 6344  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-of 7405  df-ofr 7406  df-om 7580  df-1st 7693  df-2nd 7694  df-supp 7836  df-tpos 7902  df-wrecs 7957  df-recs 8018  df-rdg 8056  df-1o 8112  df-2o 8113  df-oadd 8116  df-er 8299  df-ec 8301  df-qs 8305  df-map 8418  df-pm 8419  df-ixp 8480  df-en 8528  df-dom 8529  df-sdom 8530  df-fin 8531  df-fsupp 8867  df-sup 8939  df-inf 8940  df-oi 9007  df-dju 9363  df-card 9401  df-pnf 10715  df-mnf 10716  df-xr 10717  df-ltxr 10718  df-le 10719  df-sub 10910  df-neg 10911  df-div 11336  df-nn 11675  df-2 11737  df-3 11738  df-4 11739  df-5 11740  df-6 11741  df-7 11742  df-8 11743  df-9 11744  df-n0 11935  df-xnn0 12007  df-z 12021  df-dec 12138  df-uz 12283  df-q 12389  df-rp 12431  df-fz 12940  df-fzo 13083  df-fl 13211  df-mod 13287  df-seq 13419  df-exp 13480  df-hash 13741  df-cj 14506  df-re 14507  df-im 14508  df-sqrt 14642  df-abs 14643  df-dvds 15656  df-gcd 15894  df-prm 16068  df-phi 16158  df-pc 16229  df-gz 16321  df-struct 16543  df-ndx 16544  df-slot 16545  df-base 16547  df-sets 16548  df-ress 16549  df-plusg 16636  df-mulr 16637  df-starv 16638  df-sca 16639  df-vsca 16640  df-ip 16641  df-tset 16642  df-ple 16643  df-ds 16645  df-unif 16646  df-hom 16647  df-cco 16648  df-0g 16773  df-gsum 16774  df-prds 16779  df-pws 16781  df-imas 16839  df-qus 16840  df-mre 16915  df-mrc 16916  df-acs 16918  df-mgm 17918  df-sgrp 17967  df-mnd 17978  df-mhm 18022  df-submnd 18023  df-grp 18172  df-minusg 18173  df-sbg 18174  df-mulg 18292  df-subg 18343  df-nsg 18344  df-eqg 18345  df-ghm 18423  df-cntz 18514  df-cmn 18975  df-abl 18976  df-mgp 19308  df-ur 19320  df-srg 19324  df-ring 19367  df-cring 19368  df-oppr 19444  df-dvdsr 19462  df-unit 19463  df-invr 19493  df-dvr 19504  df-rnghom 19538  df-drng 19572  df-field 19573  df-subrg 19601  df-lmod 19704  df-lss 19772  df-lsp 19812  df-sra 20012  df-rgmod 20013  df-lidl 20014  df-rsp 20015  df-2idl 20073  df-nzr 20099  df-rlreg 20124  df-domn 20125  df-idom 20126  df-cnfld 20167  df-zring 20239  df-zrh 20273  df-zn 20276  df-assa 20618  df-asp 20619  df-ascl 20620  df-psr 20671  df-mvr 20672  df-mpl 20673  df-opsr 20675  df-evls 20835  df-evl 20836  df-psr1 20904  df-vr1 20905  df-ply1 20906  df-coe1 20907  df-evl1 21035  df-mdeg 24752  df-deg1 24753  df-mon1 24830  df-uc1p 24831  df-q1p 24832  df-r1p 24833  df-lgs 25978 This theorem is referenced by:  2sqreultblem  26131  2sqreult  26141
 Copyright terms: Public domain W3C validator