Metamath Proof Explorer

Theorem lgsdilem

Description: Lemma for lgsdi and lgsdir : the sign part of the Legendre symbol is multiplicative. (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Assertion lgsdilem ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0→ifN<0∧A⁢B<0−11=ifN<0∧A<0−11⁢ifN<0∧B<0−11

Proof

Step Hyp Ref Expression
1 simplrr ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧A<0→B≠0
2 1 biantrud ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧A<0→0≤B↔0≤B∧B≠0
3 0re ⊢0∈ℝ
4 simpl2 ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0→B∈ℤ
5 4 zred ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0→B∈ℝ
6 5 adantr ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧A<0→B∈ℝ
7 ltlen ⊢0∈ℝ∧B∈ℝ→0<B↔0≤B∧B≠0
8 3 6 7 sylancr ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧A<0→0<B↔0≤B∧B≠0
9 simpl1 ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0→A∈ℤ
10 9 zred ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0→A∈ℝ
11 10 adantr ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧A<0→A∈ℝ
12 11 renegcld ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧A<0→−A∈ℝ
13 12 recnd ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧A<0→−A∈ℂ
14 13 mul01d ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧A<0→−A⋅0=0
15 11 recnd ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧A<0→A∈ℂ
16 6 recnd ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧A<0→B∈ℂ
17 15 16 mulneg1d ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧A<0→−A⁢B=−A⁢B
18 14 17 breq12d ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧A<0→−A⋅0<−A⁢B↔0<−A⁢B
19 0red ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧A<0→0∈ℝ
20 10 lt0neg1d ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0→A<0↔0<−A
21 20 biimpa ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧A<0→0<−A
22 ltmul2 ⊢0∈ℝ∧B∈ℝ∧−A∈ℝ∧0<−A→0<B↔−A⋅0<−A⁢B
23 19 6 12 21 22 syl112anc ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧A<0→0<B↔−A⋅0<−A⁢B
24 10 5 remulcld ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0→A⁢B∈ℝ
25 24 adantr ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧A<0→A⁢B∈ℝ
26 25 lt0neg1d ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧A<0→A⁢B<0↔0<−A⁢B
27 18 23 26 3bitr4d ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧A<0→0<B↔A⁢B<0
28 2 8 27 3bitr2rd ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧A<0→A⁢B<0↔0≤B
29 lenlt ⊢0∈ℝ∧B∈ℝ→0≤B↔¬B<0
30 3 6 29 sylancr ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧A<0→0≤B↔¬B<0
31 28 30 bitrd ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧A<0→A⁢B<0↔¬B<0
32 31 ifbid ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧A<0→ifA⁢B<0−11=if¬B<0−11
33 oveq2 ⊢ifB<0−11=−1→-1⁢ifB<0−11=-1⁢-1
34 neg1mulneg1e1 ⊢-1⁢-1=1
35 33 34 eqtrdi ⊢ifB<0−11=−1→-1⁢ifB<0−11=1
36 oveq2 ⊢ifB<0−11=1→-1⁢ifB<0−11=-1⋅1
37 ax-1cn ⊢1∈ℂ
38 37 mulm1i ⊢-1⋅1=−1
39 36 38 eqtrdi ⊢ifB<0−11=1→-1⁢ifB<0−11=−1
40 35 39 ifsb ⊢-1⁢ifB<0−11=ifB<01−1
41 ifnot ⊢if¬B<0−11=ifB<01−1
42 40 41 eqtr4i ⊢-1⁢ifB<0−11=if¬B<0−11
43 32 42 eqtr4di ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧A<0→ifA⁢B<0−11=-1⁢ifB<0−11
44 iftrue ⊢A<0→ifA<0−11=−1
45 44 adantl ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧A<0→ifA<0−11=−1
46 45 oveq1d ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧A<0→ifA<0−11⁢ifB<0−11=-1⁢ifB<0−11
47 43 46 eqtr4d ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧A<0→ifA⁢B<0−11=ifA<0−11⁢ifB<0−11
48 iffalse ⊢¬A<0→ifA<0−11=1
49 48 adantl ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧¬A<0→ifA<0−11=1
50 49 oveq1d ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧¬A<0→ifA<0−11⁢ifB<0−11=1⁢ifB<0−11
51 neg1cn ⊢−1∈ℂ
52 51 37 ifcli ⊢ifB<0−11∈ℂ
53 52 mullidi ⊢1⁢ifB<0−11=ifB<0−11
54 5 adantr ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧¬A<0→B∈ℝ
55 0red ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧¬A<0→0∈ℝ
56 10 adantr ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧¬A<0→A∈ℝ
57 lenlt ⊢0∈ℝ∧A∈ℝ→0≤A↔¬A<0
58 3 10 57 sylancr ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0→0≤A↔¬A<0
59 58 biimpar ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧¬A<0→0≤A
60 simplrl ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧¬A<0→A≠0
61 56 59 60 ne0gt0d ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧¬A<0→0<A
62 ltmul2 ⊢B∈ℝ∧0∈ℝ∧A∈ℝ∧0<A→B<0↔A⁢B<A⋅0
63 54 55 56 61 62 syl112anc ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧¬A<0→B<0↔A⁢B<A⋅0
64 56 recnd ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧¬A<0→A∈ℂ
65 64 mul01d ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧¬A<0→A⋅0=0
66 65 breq2d ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧¬A<0→A⁢B<A⋅0↔A⁢B<0
67 63 66 bitrd ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧¬A<0→B<0↔A⁢B<0
68 67 ifbid ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧¬A<0→ifB<0−11=ifA⁢B<0−11
69 53 68 eqtrid ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧¬A<0→1⁢ifB<0−11=ifA⁢B<0−11
70 50 69 eqtr2d ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧¬A<0→ifA⁢B<0−11=ifA<0−11⁢ifB<0−11
71 47 70 pm2.61dan ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0→ifA⁢B<0−11=ifA<0−11⁢ifB<0−11
72 71 adantr ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧N<0→ifA⁢B<0−11=ifA<0−11⁢ifB<0−11
73 simpr ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧N<0→N<0
74 73 biantrurd ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧N<0→A⁢B<0↔N<0∧A⁢B<0
75 74 ifbid ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧N<0→ifA⁢B<0−11=ifN<0∧A⁢B<0−11
76 73 biantrurd ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧N<0→A<0↔N<0∧A<0
77 76 ifbid ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧N<0→ifA<0−11=ifN<0∧A<0−11
78 73 biantrurd ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧N<0→B<0↔N<0∧B<0
79 78 ifbid ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧N<0→ifB<0−11=ifN<0∧B<0−11
80 77 79 oveq12d ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧N<0→ifA<0−11⁢ifB<0−11=ifN<0∧A<0−11⁢ifN<0∧B<0−11
81 72 75 80 3eqtr3d ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧N<0→ifN<0∧A⁢B<0−11=ifN<0∧A<0−11⁢ifN<0∧B<0−11
82 simpr ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧¬N<0→¬N<0
83 82 intnanrd ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧¬N<0→¬N<0∧A⁢B<0
84 83 iffalsed ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧¬N<0→ifN<0∧A⁢B<0−11=1
85 1t1e1 ⊢1⋅1=1
86 84 85 eqtr4di ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧¬N<0→ifN<0∧A⁢B<0−11=1⋅1
87 82 intnanrd ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧¬N<0→¬N<0∧A<0
88 87 iffalsed ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧¬N<0→ifN<0∧A<0−11=1
89 82 intnanrd ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧¬N<0→¬N<0∧B<0
90 89 iffalsed ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧¬N<0→ifN<0∧B<0−11=1
91 88 90 oveq12d ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧¬N<0→ifN<0∧A<0−11⁢ifN<0∧B<0−11=1⋅1
92 86 91 eqtr4d ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0∧¬N<0→ifN<0∧A⁢B<0−11=ifN<0∧A<0−11⁢ifN<0∧B<0−11
93 81 92 pm2.61dan ⊢A∈ℤ∧B∈ℤ∧N∈ℤ∧A≠0∧B≠0→ifN<0∧A⁢B<0−11=ifN<0∧A<0−11⁢ifN<0∧B<0−11