Description: Extend lgsquad to coprime odd integers (the domain of the Jacobi symbol). (Contributed by Mario Carneiro, 19-Jun-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lgsquad2.1 | |
|
lgsquad2.2 | |
||
lgsquad2.3 | |
||
lgsquad2.4 | |
||
lgsquad2.5 | |
||
Assertion | lgsquad2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lgsquad2.1 | |
|
2 | lgsquad2.2 | |
|
3 | lgsquad2.3 | |
|
4 | lgsquad2.4 | |
|
5 | lgsquad2.5 | |
|
6 | 3 | adantr | |
7 | 4 | adantr | |
8 | simprl | |
|
9 | eldifi | |
|
10 | 8 9 | syl | |
11 | prmnn | |
|
12 | 10 11 | syl | |
13 | eldifsni | |
|
14 | 8 13 | syl | |
15 | 14 | necomd | |
16 | 15 | neneqd | |
17 | 2z | |
|
18 | uzid | |
|
19 | 17 18 | ax-mp | |
20 | dvdsprm | |
|
21 | 19 10 20 | sylancr | |
22 | 16 21 | mtbird | |
23 | 6 | nnzd | |
24 | 12 | nnzd | |
25 | 23 24 | gcdcomd | |
26 | simprr | |
|
27 | 25 26 | eqtrd | |
28 | simprl | |
|
29 | 8 | adantr | |
30 | eldifi | |
|
31 | prmrp | |
|
32 | 30 10 31 | syl2anr | |
33 | 32 | biimpd | |
34 | 33 | impr | |
35 | lgsquad | |
|
36 | 28 29 34 35 | syl3anc | |
37 | biid | |
|
38 | 6 7 12 22 27 36 37 | lgsquad2lem2 | |
39 | lgscl | |
|
40 | 24 23 39 | syl2anc | |
41 | lgscl | |
|
42 | 23 24 41 | syl2anc | |
43 | zcn | |
|
44 | zcn | |
|
45 | mulcom | |
|
46 | 43 44 45 | syl2an | |
47 | 40 42 46 | syl2anc | |
48 | 12 | nncnd | |
49 | ax-1cn | |
|
50 | subcl | |
|
51 | 48 49 50 | sylancl | |
52 | 51 | halfcld | |
53 | 6 | nncnd | |
54 | subcl | |
|
55 | 53 49 54 | sylancl | |
56 | 55 | halfcld | |
57 | 52 56 | mulcomd | |
58 | 57 | oveq2d | |
59 | 38 47 58 | 3eqtr4d | |
60 | biid | |
|
61 | 1 2 3 4 5 59 60 | lgsquad2lem2 | |