Metamath Proof Explorer

Theorem lgsval2lem

Description: Lemma for lgsval2 . (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Hypothesis lgsval.1 ⊢F=n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN1
Assertion lgsval2lem ⊢A∈ℤ∧N∈ℙ→A/LN=ifN=2if2∥A0ifAmod8∈171−1AN−12+1modN−1

Proof

Step Hyp Ref Expression
1 lgsval.1 ⊢F=n∈ℕ⟼ifn∈ℙifn=2if2∥A0ifAmod8∈171−1An−12+1modn−1npCntN1
2 prmz ⊢N∈ℙ→N∈ℤ
3 1 lgsval ⊢A∈ℤ∧N∈ℤ→A/LN=ifN=0ifA2=110ifN<0∧A<0−11⁢seq1×F⁡N
4 2 3 sylan2 ⊢A∈ℤ∧N∈ℙ→A/LN=ifN=0ifA2=110ifN<0∧A<0−11⁢seq1×F⁡N
5 prmnn ⊢N∈ℙ→N∈ℕ
6 5 adantl ⊢A∈ℤ∧N∈ℙ→N∈ℕ
7 6 nnne0d ⊢A∈ℤ∧N∈ℙ→N≠0
8 7 neneqd ⊢A∈ℤ∧N∈ℙ→¬N=0
9 8 iffalsed ⊢A∈ℤ∧N∈ℙ→ifN=0ifA2=110ifN<0∧A<0−11⁢seq1×F⁡N=ifN<0∧A<0−11⁢seq1×F⁡N
10 6 nnnn0d ⊢A∈ℤ∧N∈ℙ→N∈ℕ0
11 10 nn0ge0d ⊢A∈ℤ∧N∈ℙ→0≤N
12 0re ⊢0∈ℝ
13 6 nnred ⊢A∈ℤ∧N∈ℙ→N∈ℝ
14 lenlt ⊢0∈ℝ∧N∈ℝ→0≤N↔¬N<0
15 12 13 14 sylancr ⊢A∈ℤ∧N∈ℙ→0≤N↔¬N<0
16 11 15 mpbid ⊢A∈ℤ∧N∈ℙ→¬N<0
17 16 intnanrd ⊢A∈ℤ∧N∈ℙ→¬N<0∧A<0
18 17 iffalsed ⊢A∈ℤ∧N∈ℙ→ifN<0∧A<0−11=1
19 13 11 absidd ⊢A∈ℤ∧N∈ℙ→N=N
20 19 fveq2d ⊢A∈ℤ∧N∈ℙ→seq1×F⁡N=seq1×F⁡N
21 1z ⊢1∈ℤ
22 prmuz2 ⊢N∈ℙ→N∈ℤ≥2
23 22 adantl ⊢A∈ℤ∧N∈ℙ→N∈ℤ≥2
24 df-2 ⊢2=1+1
25 24 fveq2i ⊢ℤ≥2=ℤ≥1+1
26 23 25 eleqtrdi ⊢A∈ℤ∧N∈ℙ→N∈ℤ≥1+1
27 seqm1 ⊢1∈ℤ∧N∈ℤ≥1+1→seq1×F⁡N=seq1×F⁡N−1⁢F⁡N
28 21 26 27 sylancr ⊢A∈ℤ∧N∈ℙ→seq1×F⁡N=seq1×F⁡N−1⁢F⁡N
29 1t1e1 ⊢1⋅1=1
30 29 a1i ⊢A∈ℤ∧N∈ℙ→1⋅1=1
31 uz2m1nn ⊢N∈ℤ≥2→N−1∈ℕ
32 23 31 syl ⊢A∈ℤ∧N∈ℙ→N−1∈ℕ
33 nnuz ⊢ℕ=ℤ≥1
34 32 33 eleqtrdi ⊢A∈ℤ∧N∈ℙ→N−1∈ℤ≥1
35 elfznn ⊢x∈1…N−1→x∈ℕ
36 35 adantl ⊢A∈ℤ∧N∈ℙ∧x∈1…N−1→x∈ℕ
37 1 lgsfval ⊢x∈ℕ→F⁡x=ifx∈ℙifx=2if2∥A0ifAmod8∈171−1Ax−12+1modx−1xpCntN1
38 36 37 syl ⊢A∈ℤ∧N∈ℙ∧x∈1…N−1→F⁡x=ifx∈ℙifx=2if2∥A0ifAmod8∈171−1Ax−12+1modx−1xpCntN1
39 elfzelz ⊢N∈1…N−1→N∈ℤ
40 39 zred ⊢N∈1…N−1→N∈ℝ
41 40 ltm1d ⊢N∈1…N−1→N−1<N
42 peano2rem ⊢N∈ℝ→N−1∈ℝ
43 40 42 syl ⊢N∈1…N−1→N−1∈ℝ
44 elfzle2 ⊢N∈1…N−1→N≤N−1
45 40 43 44 lensymd ⊢N∈1…N−1→¬N−1<N
46 41 45 pm2.65i ⊢¬N∈1…N−1
47 eleq1 ⊢x=N→x∈1…N−1↔N∈1…N−1
48 46 47 mtbiri ⊢x=N→¬x∈1…N−1
49 48 con2i ⊢x∈1…N−1→¬x=N
50 49 ad2antlr ⊢A∈ℤ∧N∈ℙ∧x∈1…N−1∧x∈ℙ→¬x=N
51 prmuz2 ⊢x∈ℙ→x∈ℤ≥2
52 simpllr ⊢A∈ℤ∧N∈ℙ∧x∈1…N−1∧x∈ℙ→N∈ℙ
53 dvdsprm ⊢x∈ℤ≥2∧N∈ℙ→x∥N↔x=N
54 51 52 53 syl2an2 ⊢A∈ℤ∧N∈ℙ∧x∈1…N−1∧x∈ℙ→x∥N↔x=N
55 50 54 mtbird ⊢A∈ℤ∧N∈ℙ∧x∈1…N−1∧x∈ℙ→¬x∥N
56 simpr ⊢A∈ℤ∧N∈ℙ∧x∈1…N−1∧x∈ℙ→x∈ℙ
57 6 ad2antrr ⊢A∈ℤ∧N∈ℙ∧x∈1…N−1∧x∈ℙ→N∈ℕ
58 pceq0 ⊢x∈ℙ∧N∈ℕ→xpCntN=0↔¬x∥N
59 56 57 58 syl2anc ⊢A∈ℤ∧N∈ℙ∧x∈1…N−1∧x∈ℙ→xpCntN=0↔¬x∥N
60 55 59 mpbird ⊢A∈ℤ∧N∈ℙ∧x∈1…N−1∧x∈ℙ→xpCntN=0
61 60 oveq2d ⊢A∈ℤ∧N∈ℙ∧x∈1…N−1∧x∈ℙ→ifx=2if2∥A0ifAmod8∈171−1Ax−12+1modx−1xpCntN=ifx=2if2∥A0ifAmod8∈171−1Ax−12+1modx−10
62 0z ⊢0∈ℤ
63 neg1z ⊢−1∈ℤ
64 21 63 ifcli ⊢ifAmod8∈171−1∈ℤ
65 62 64 ifcli ⊢if2∥A0ifAmod8∈171−1∈ℤ
66 65 a1i ⊢A∈ℤ∧N∈ℙ∧x∈ℙ∧x=2→if2∥A0ifAmod8∈171−1∈ℤ
67 simpl ⊢A∈ℤ∧N∈ℙ→A∈ℤ
68 67 ad2antrr ⊢A∈ℤ∧N∈ℙ∧x∈ℙ∧¬x=2→A∈ℤ
69 simplr ⊢A∈ℤ∧N∈ℙ∧x∈ℙ∧¬x=2→x∈ℙ
70 simpr ⊢A∈ℤ∧N∈ℙ∧x∈ℙ∧¬x=2→¬x=2
71 70 neqned ⊢A∈ℤ∧N∈ℙ∧x∈ℙ∧¬x=2→x≠2
72 eldifsn ⊢x∈ℙ∖2↔x∈ℙ∧x≠2
73 69 71 72 sylanbrc ⊢A∈ℤ∧N∈ℙ∧x∈ℙ∧¬x=2→x∈ℙ∖2
74 oddprm ⊢x∈ℙ∖2→x−12∈ℕ
75 73 74 syl ⊢A∈ℤ∧N∈ℙ∧x∈ℙ∧¬x=2→x−12∈ℕ
76 75 nnnn0d ⊢A∈ℤ∧N∈ℙ∧x∈ℙ∧¬x=2→x−12∈ℕ0
77 zexpcl ⊢A∈ℤ∧x−12∈ℕ0→Ax−12∈ℤ
78 68 76 77 syl2anc ⊢A∈ℤ∧N∈ℙ∧x∈ℙ∧¬x=2→Ax−12∈ℤ
79 78 peano2zd ⊢A∈ℤ∧N∈ℙ∧x∈ℙ∧¬x=2→Ax−12+1∈ℤ
80 prmnn ⊢x∈ℙ→x∈ℕ
81 80 ad2antlr ⊢A∈ℤ∧N∈ℙ∧x∈ℙ∧¬x=2→x∈ℕ
82 79 81 zmodcld ⊢A∈ℤ∧N∈ℙ∧x∈ℙ∧¬x=2→Ax−12+1modx∈ℕ0
83 82 nn0zd ⊢A∈ℤ∧N∈ℙ∧x∈ℙ∧¬x=2→Ax−12+1modx∈ℤ
84 peano2zm ⊢Ax−12+1modx∈ℤ→Ax−12+1modx−1∈ℤ
85 83 84 syl ⊢A∈ℤ∧N∈ℙ∧x∈ℙ∧¬x=2→Ax−12+1modx−1∈ℤ
86 66 85 ifclda ⊢A∈ℤ∧N∈ℙ∧x∈ℙ→ifx=2if2∥A0ifAmod8∈171−1Ax−12+1modx−1∈ℤ
87 86 zcnd ⊢A∈ℤ∧N∈ℙ∧x∈ℙ→ifx=2if2∥A0ifAmod8∈171−1Ax−12+1modx−1∈ℂ
88 87 adantlr ⊢A∈ℤ∧N∈ℙ∧x∈1…N−1∧x∈ℙ→ifx=2if2∥A0ifAmod8∈171−1Ax−12+1modx−1∈ℂ
89 88 exp0d ⊢A∈ℤ∧N∈ℙ∧x∈1…N−1∧x∈ℙ→ifx=2if2∥A0ifAmod8∈171−1Ax−12+1modx−10=1
90 61 89 eqtrd ⊢A∈ℤ∧N∈ℙ∧x∈1…N−1∧x∈ℙ→ifx=2if2∥A0ifAmod8∈171−1Ax−12+1modx−1xpCntN=1
91 90 ifeq1da ⊢A∈ℤ∧N∈ℙ∧x∈1…N−1→ifx∈ℙifx=2if2∥A0ifAmod8∈171−1Ax−12+1modx−1xpCntN1=ifx∈ℙ11
92 ifid ⊢ifx∈ℙ11=1
93 91 92 eqtrdi ⊢A∈ℤ∧N∈ℙ∧x∈1…N−1→ifx∈ℙifx=2if2∥A0ifAmod8∈171−1Ax−12+1modx−1xpCntN1=1
94 38 93 eqtrd ⊢A∈ℤ∧N∈ℙ∧x∈1…N−1→F⁡x=1
95 30 34 94 seqid3 ⊢A∈ℤ∧N∈ℙ→seq1×F⁡N−1=1
96 95 oveq1d ⊢A∈ℤ∧N∈ℙ→seq1×F⁡N−1⁢F⁡N=1⁢F⁡N
97 2 adantl ⊢A∈ℤ∧N∈ℙ→N∈ℤ
98 1 lgsfcl ⊢A∈ℤ∧N∈ℤ∧N≠0→F:ℕ⟶ℤ
99 67 97 7 98 syl3anc ⊢A∈ℤ∧N∈ℙ→F:ℕ⟶ℤ
100 99 6 ffvelcdmd ⊢A∈ℤ∧N∈ℙ→F⁡N∈ℤ
101 100 zcnd ⊢A∈ℤ∧N∈ℙ→F⁡N∈ℂ
102 101 mullidd ⊢A∈ℤ∧N∈ℙ→1⁢F⁡N=F⁡N
103 28 96 102 3eqtrd ⊢A∈ℤ∧N∈ℙ→seq1×F⁡N=F⁡N
104 20 103 eqtrd ⊢A∈ℤ∧N∈ℙ→seq1×F⁡N=F⁡N
105 18 104 oveq12d ⊢A∈ℤ∧N∈ℙ→ifN<0∧A<0−11⁢seq1×F⁡N=1⁢F⁡N
106 1 lgsfval ⊢N∈ℕ→F⁡N=ifN∈ℙifN=2if2∥A0ifAmod8∈171−1AN−12+1modN−1NpCntN1
107 6 106 syl ⊢A∈ℤ∧N∈ℙ→F⁡N=ifN∈ℙifN=2if2∥A0ifAmod8∈171−1AN−12+1modN−1NpCntN1
108 iftrue ⊢N∈ℙ→ifN∈ℙifN=2if2∥A0ifAmod8∈171−1AN−12+1modN−1NpCntN1=ifN=2if2∥A0ifAmod8∈171−1AN−12+1modN−1NpCntN
109 108 adantl ⊢A∈ℤ∧N∈ℙ→ifN∈ℙifN=2if2∥A0ifAmod8∈171−1AN−12+1modN−1NpCntN1=ifN=2if2∥A0ifAmod8∈171−1AN−12+1modN−1NpCntN
110 6 nncnd ⊢A∈ℤ∧N∈ℙ→N∈ℂ
111 110 exp1d ⊢A∈ℤ∧N∈ℙ→N1=N
112 111 oveq2d ⊢A∈ℤ∧N∈ℙ→NpCntN1=NpCntN
113 simpr ⊢A∈ℤ∧N∈ℙ→N∈ℙ
114 pcid ⊢N∈ℙ∧1∈ℤ→NpCntN1=1
115 113 21 114 sylancl ⊢A∈ℤ∧N∈ℙ→NpCntN1=1
116 112 115 eqtr3d ⊢A∈ℤ∧N∈ℙ→NpCntN=1
117 116 oveq2d ⊢A∈ℤ∧N∈ℙ→ifN=2if2∥A0ifAmod8∈171−1AN−12+1modN−1NpCntN=ifN=2if2∥A0ifAmod8∈171−1AN−12+1modN−11
118 eqeq1 ⊢x=N→x=2↔N=2
119 oveq1 ⊢x=N→x−1=N−1
120 119 oveq1d ⊢x=N→x−12=N−12
121 120 oveq2d ⊢x=N→Ax−12=AN−12
122 121 oveq1d ⊢x=N→Ax−12+1=AN−12+1
123 id ⊢x=N→x=N
124 122 123 oveq12d ⊢x=N→Ax−12+1modx=AN−12+1modN
125 124 oveq1d ⊢x=N→Ax−12+1modx−1=AN−12+1modN−1
126 118 125 ifbieq2d ⊢x=N→ifx=2if2∥A0ifAmod8∈171−1Ax−12+1modx−1=ifN=2if2∥A0ifAmod8∈171−1AN−12+1modN−1
127 126 eleq1d ⊢x=N→ifx=2if2∥A0ifAmod8∈171−1Ax−12+1modx−1∈ℂ↔ifN=2if2∥A0ifAmod8∈171−1AN−12+1modN−1∈ℂ
128 87 ralrimiva ⊢A∈ℤ∧N∈ℙ→∀x∈ℙifx=2if2∥A0ifAmod8∈171−1Ax−12+1modx−1∈ℂ
129 127 128 113 rspcdva ⊢A∈ℤ∧N∈ℙ→ifN=2if2∥A0ifAmod8∈171−1AN−12+1modN−1∈ℂ
130 129 exp1d ⊢A∈ℤ∧N∈ℙ→ifN=2if2∥A0ifAmod8∈171−1AN−12+1modN−11=ifN=2if2∥A0ifAmod8∈171−1AN−12+1modN−1
131 117 130 eqtrd ⊢A∈ℤ∧N∈ℙ→ifN=2if2∥A0ifAmod8∈171−1AN−12+1modN−1NpCntN=ifN=2if2∥A0ifAmod8∈171−1AN−12+1modN−1
132 107 109 131 3eqtrd ⊢A∈ℤ∧N∈ℙ→F⁡N=ifN=2if2∥A0ifAmod8∈171−1AN−12+1modN−1
133 105 102 132 3eqtrd ⊢A∈ℤ∧N∈ℙ→ifN<0∧A<0−11⁢seq1×F⁡N=ifN=2if2∥A0ifAmod8∈171−1AN−12+1modN−1
134 4 9 133 3eqtrd ⊢A∈ℤ∧N∈ℙ→A/LN=ifN=2if2∥A0ifAmod8∈171−1AN−12+1modN−1