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

Theorem lgsval 25791
Description: Value of the Legendre symbol at an arbitrary integer. (Contributed by Mario Carneiro, 4-Feb-2015.)
Hypothesis
Ref Expression
lgsval.1 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1))
Assertion
Ref Expression
lgsval ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) = if(𝑁 = 0, if((𝐴↑2) = 1, 1, 0), (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁)))))
Distinct variable groups:   𝐴,𝑛   𝑛,𝑁
Allowed substitution hint:   𝐹(𝑛)

Proof of Theorem lgsval
Dummy variables 𝑎 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 485 . . . 4 ((𝑎 = 𝐴𝑚 = 𝑁) → 𝑚 = 𝑁)
21eqeq1d 2828 . . 3 ((𝑎 = 𝐴𝑚 = 𝑁) → (𝑚 = 0 ↔ 𝑁 = 0))
3 simpl 483 . . . . . 6 ((𝑎 = 𝐴𝑚 = 𝑁) → 𝑎 = 𝐴)
43oveq1d 7163 . . . . 5 ((𝑎 = 𝐴𝑚 = 𝑁) → (𝑎↑2) = (𝐴↑2))
54eqeq1d 2828 . . . 4 ((𝑎 = 𝐴𝑚 = 𝑁) → ((𝑎↑2) = 1 ↔ (𝐴↑2) = 1))
65ifbid 4492 . . 3 ((𝑎 = 𝐴𝑚 = 𝑁) → if((𝑎↑2) = 1, 1, 0) = if((𝐴↑2) = 1, 1, 0))
71breq1d 5073 . . . . . 6 ((𝑎 = 𝐴𝑚 = 𝑁) → (𝑚 < 0 ↔ 𝑁 < 0))
83breq1d 5073 . . . . . 6 ((𝑎 = 𝐴𝑚 = 𝑁) → (𝑎 < 0 ↔ 𝐴 < 0))
97, 8anbi12d 630 . . . . 5 ((𝑎 = 𝐴𝑚 = 𝑁) → ((𝑚 < 0 ∧ 𝑎 < 0) ↔ (𝑁 < 0 ∧ 𝐴 < 0)))
109ifbid 4492 . . . 4 ((𝑎 = 𝐴𝑚 = 𝑁) → if((𝑚 < 0 ∧ 𝑎 < 0), -1, 1) = if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1))
113breq2d 5075 . . . . . . . . . . . 12 ((𝑎 = 𝐴𝑚 = 𝑁) → (2 ∥ 𝑎 ↔ 2 ∥ 𝐴))
123oveq1d 7163 . . . . . . . . . . . . . 14 ((𝑎 = 𝐴𝑚 = 𝑁) → (𝑎 mod 8) = (𝐴 mod 8))
1312eleq1d 2902 . . . . . . . . . . . . 13 ((𝑎 = 𝐴𝑚 = 𝑁) → ((𝑎 mod 8) ∈ {1, 7} ↔ (𝐴 mod 8) ∈ {1, 7}))
1413ifbid 4492 . . . . . . . . . . . 12 ((𝑎 = 𝐴𝑚 = 𝑁) → if((𝑎 mod 8) ∈ {1, 7}, 1, -1) = if((𝐴 mod 8) ∈ {1, 7}, 1, -1))
1511, 14ifbieq2d 4495 . . . . . . . . . . 11 ((𝑎 = 𝐴𝑚 = 𝑁) → if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)) = if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)))
163oveq1d 7163 . . . . . . . . . . . . . 14 ((𝑎 = 𝐴𝑚 = 𝑁) → (𝑎↑((𝑛 − 1) / 2)) = (𝐴↑((𝑛 − 1) / 2)))
1716oveq1d 7163 . . . . . . . . . . . . 13 ((𝑎 = 𝐴𝑚 = 𝑁) → ((𝑎↑((𝑛 − 1) / 2)) + 1) = ((𝐴↑((𝑛 − 1) / 2)) + 1))
1817oveq1d 7163 . . . . . . . . . . . 12 ((𝑎 = 𝐴𝑚 = 𝑁) → (((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) = (((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛))
1918oveq1d 7163 . . . . . . . . . . 11 ((𝑎 = 𝐴𝑚 = 𝑁) → ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1) = ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))
2015, 19ifeq12d 4490 . . . . . . . . . 10 ((𝑎 = 𝐴𝑚 = 𝑁) → if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1)) = if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1)))
211oveq2d 7164 . . . . . . . . . 10 ((𝑎 = 𝐴𝑚 = 𝑁) → (𝑛 pCnt 𝑚) = (𝑛 pCnt 𝑁))
2220, 21oveq12d 7166 . . . . . . . . 9 ((𝑎 = 𝐴𝑚 = 𝑁) → (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)) = (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)))
2322ifeq1d 4488 . . . . . . . 8 ((𝑎 = 𝐴𝑚 = 𝑁) → if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1) = if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1))
2423mpteq2dv 5159 . . . . . . 7 ((𝑎 = 𝐴𝑚 = 𝑁) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1)))
25 lgsval.1 . . . . . . 7 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑁)), 1))
2624, 25syl6eqr 2879 . . . . . 6 ((𝑎 = 𝐴𝑚 = 𝑁) → (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1)) = 𝐹)
2726seqeq3d 13367 . . . . 5 ((𝑎 = 𝐴𝑚 = 𝑁) → seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1))) = seq1( · , 𝐹))
281fveq2d 6671 . . . . 5 ((𝑎 = 𝐴𝑚 = 𝑁) → (abs‘𝑚) = (abs‘𝑁))
2927, 28fveq12d 6674 . . . 4 ((𝑎 = 𝐴𝑚 = 𝑁) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1)))‘(abs‘𝑚)) = (seq1( · , 𝐹)‘(abs‘𝑁)))
3010, 29oveq12d 7166 . . 3 ((𝑎 = 𝐴𝑚 = 𝑁) → (if((𝑚 < 0 ∧ 𝑎 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1)))‘(abs‘𝑚))) = (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁))))
312, 6, 30ifbieq12d 4497 . 2 ((𝑎 = 𝐴𝑚 = 𝑁) → if(𝑚 = 0, if((𝑎↑2) = 1, 1, 0), (if((𝑚 < 0 ∧ 𝑎 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1)))‘(abs‘𝑚)))) = if(𝑁 = 0, if((𝐴↑2) = 1, 1, 0), (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁)))))
32 df-lgs 25785 . 2 /L = (𝑎 ∈ ℤ, 𝑚 ∈ ℤ ↦ if(𝑚 = 0, if((𝑎↑2) = 1, 1, 0), (if((𝑚 < 0 ∧ 𝑎 < 0), -1, 1) · (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (if(𝑛 = 2, if(2 ∥ 𝑎, 0, if((𝑎 mod 8) ∈ {1, 7}, 1, -1)), ((((𝑎↑((𝑛 − 1) / 2)) + 1) mod 𝑛) − 1))↑(𝑛 pCnt 𝑚)), 1)))‘(abs‘𝑚)))))
33 1nn0 11902 . . . . 5 1 ∈ ℕ0
34 0nn0 11901 . . . . 5 0 ∈ ℕ0
3533, 34ifcli 4516 . . . 4 if((𝐴↑2) = 1, 1, 0) ∈ ℕ0
3635elexi 3519 . . 3 if((𝐴↑2) = 1, 1, 0) ∈ V
37 ovex 7181 . . 3 (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁))) ∈ V
3836, 37ifex 4518 . 2 if(𝑁 = 0, if((𝐴↑2) = 1, 1, 0), (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁)))) ∈ V
3931, 32, 38ovmpoa 7295 1 ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 /L 𝑁) = if(𝑁 = 0, if((𝐴↑2) = 1, 1, 0), (if((𝑁 < 0 ∧ 𝐴 < 0), -1, 1) · (seq1( · , 𝐹)‘(abs‘𝑁)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1530  wcel 2107  ifcif 4470  {cpr 4566   class class class wbr 5063  cmpt 5143  cfv 6352  (class class class)co 7148  0cc0 10526  1c1 10527   + caddc 10529   · cmul 10531   < clt 10664  cmin 10859  -cneg 10860   / cdiv 11286  cn 11627  2c2 11681  7c7 11686  8c8 11687  0cn0 11886  cz 11970   mod cmo 13227  seqcseq 13359  cexp 13419  abscabs 14583  cdvds 15597  cprime 16005   pCnt cpc 16163   /L clgs 25784
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7451  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-mulcl 10588  ax-i2m1 10594
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-ral 3148  df-rex 3149  df-reu 3150  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6146  df-ord 6192  df-on 6193  df-lim 6194  df-suc 6195  df-iota 6312  df-fun 6354  df-fn 6355  df-f 6356  df-f1 6357  df-fo 6358  df-f1o 6359  df-fv 6360  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7569  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-nn 11628  df-n0 11887  df-seq 13360  df-lgs 25785
This theorem is referenced by:  lgscllem  25794  lgsval2lem  25797  lgs0  25800  lgsval4  25807
  Copyright terms: Public domain W3C validator