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 ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → if ( ( 𝑁 < 0 ∧ ( 𝐴 · 𝐵 ) < 0 ) , - 1 , 1 ) = ( if ( ( 𝑁 < 0 ∧ 𝐴 < 0 ) , - 1 , 1 ) · if ( ( 𝑁 < 0 ∧ 𝐵 < 0 ) , - 1 , 1 ) ) )

Proof

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