Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sgnmul Structured version   Visualization version   GIF version

Theorem sgnmul 34545
Description: Signum of a product. (Contributed by Thierry Arnoux, 2-Oct-2018.)
Assertion
Ref Expression
sgnmul ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (sgn‘(𝐴 · 𝐵)) = ((sgn‘𝐴) · (sgn‘𝐵)))

Proof of Theorem sgnmul
StepHypRef Expression
1 remulcl 11240 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
21rexrd 11311 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ*)
3 eqeq1 2741 . 2 ((sgn‘(𝐴 · 𝐵)) = 0 → ((sgn‘(𝐴 · 𝐵)) = ((sgn‘𝐴) · (sgn‘𝐵)) ↔ 0 = ((sgn‘𝐴) · (sgn‘𝐵))))
4 eqeq1 2741 . 2 ((sgn‘(𝐴 · 𝐵)) = 1 → ((sgn‘(𝐴 · 𝐵)) = ((sgn‘𝐴) · (sgn‘𝐵)) ↔ 1 = ((sgn‘𝐴) · (sgn‘𝐵))))
5 eqeq1 2741 . 2 ((sgn‘(𝐴 · 𝐵)) = -1 → ((sgn‘(𝐴 · 𝐵)) = ((sgn‘𝐴) · (sgn‘𝐵)) ↔ -1 = ((sgn‘𝐴) · (sgn‘𝐵))))
6 fveq2 6906 . . . . . . 7 (𝐴 = 0 → (sgn‘𝐴) = (sgn‘0))
7 sgn0 15128 . . . . . . 7 (sgn‘0) = 0
86, 7eqtrdi 2793 . . . . . 6 (𝐴 = 0 → (sgn‘𝐴) = 0)
98oveq1d 7446 . . . . 5 (𝐴 = 0 → ((sgn‘𝐴) · (sgn‘𝐵)) = (0 · (sgn‘𝐵)))
109adantl 481 . . . 4 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) = 0) ∧ 𝐴 = 0) → ((sgn‘𝐴) · (sgn‘𝐵)) = (0 · (sgn‘𝐵)))
11 sgnclre 34542 . . . . . . 7 (𝐵 ∈ ℝ → (sgn‘𝐵) ∈ ℝ)
1211recnd 11289 . . . . . 6 (𝐵 ∈ ℝ → (sgn‘𝐵) ∈ ℂ)
1312mul02d 11459 . . . . 5 (𝐵 ∈ ℝ → (0 · (sgn‘𝐵)) = 0)
1413ad3antlr 731 . . . 4 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) = 0) ∧ 𝐴 = 0) → (0 · (sgn‘𝐵)) = 0)
1510, 14eqtr2d 2778 . . 3 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) = 0) ∧ 𝐴 = 0) → 0 = ((sgn‘𝐴) · (sgn‘𝐵)))
16 fveq2 6906 . . . . . . 7 (𝐵 = 0 → (sgn‘𝐵) = (sgn‘0))
1716, 7eqtrdi 2793 . . . . . 6 (𝐵 = 0 → (sgn‘𝐵) = 0)
1817oveq2d 7447 . . . . 5 (𝐵 = 0 → ((sgn‘𝐴) · (sgn‘𝐵)) = ((sgn‘𝐴) · 0))
1918adantl 481 . . . 4 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) = 0) ∧ 𝐵 = 0) → ((sgn‘𝐴) · (sgn‘𝐵)) = ((sgn‘𝐴) · 0))
20 sgnclre 34542 . . . . . . 7 (𝐴 ∈ ℝ → (sgn‘𝐴) ∈ ℝ)
2120recnd 11289 . . . . . 6 (𝐴 ∈ ℝ → (sgn‘𝐴) ∈ ℂ)
2221mul01d 11460 . . . . 5 (𝐴 ∈ ℝ → ((sgn‘𝐴) · 0) = 0)
2322ad3antrrr 730 . . . 4 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) = 0) ∧ 𝐵 = 0) → ((sgn‘𝐴) · 0) = 0)
2419, 23eqtr2d 2778 . . 3 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) = 0) ∧ 𝐵 = 0) → 0 = ((sgn‘𝐴) · (sgn‘𝐵)))
25 simpl 482 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ∈ ℝ)
2625recnd 11289 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ∈ ℂ)
27 simpr 484 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ∈ ℝ)
2827recnd 11289 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ∈ ℂ)
2926, 28mul0ord 11913 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 · 𝐵) = 0 ↔ (𝐴 = 0 ∨ 𝐵 = 0)))
3029biimpa 476 . . 3 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) = 0) → (𝐴 = 0 ∨ 𝐵 = 0))
3115, 24, 30mpjaodan 961 . 2 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) = 0) → 0 = ((sgn‘𝐴) · (sgn‘𝐵)))
32 simpll 767 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) → 𝐴 ∈ ℝ)
3332rexrd 11311 . . 3 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) → 𝐴 ∈ ℝ*)
34 oveq1 7438 . . . 4 ((sgn‘𝐴) = 0 → ((sgn‘𝐴) · (sgn‘𝐵)) = (0 · (sgn‘𝐵)))
3534eqeq2d 2748 . . 3 ((sgn‘𝐴) = 0 → (1 = ((sgn‘𝐴) · (sgn‘𝐵)) ↔ 1 = (0 · (sgn‘𝐵))))
36 oveq1 7438 . . . 4 ((sgn‘𝐴) = 1 → ((sgn‘𝐴) · (sgn‘𝐵)) = (1 · (sgn‘𝐵)))
3736eqeq2d 2748 . . 3 ((sgn‘𝐴) = 1 → (1 = ((sgn‘𝐴) · (sgn‘𝐵)) ↔ 1 = (1 · (sgn‘𝐵))))
38 oveq1 7438 . . . 4 ((sgn‘𝐴) = -1 → ((sgn‘𝐴) · (sgn‘𝐵)) = (-1 · (sgn‘𝐵)))
3938eqeq2d 2748 . . 3 ((sgn‘𝐴) = -1 → (1 = ((sgn‘𝐴) · (sgn‘𝐵)) ↔ 1 = (-1 · (sgn‘𝐵))))
40 simpr 484 . . . 4 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 = 0) → 𝐴 = 0)
4126adantr 480 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) → 𝐴 ∈ ℂ)
4228adantr 480 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) → 𝐵 ∈ ℂ)
43 simpr 484 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) → 0 < (𝐴 · 𝐵))
4443gt0ne0d 11827 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) → (𝐴 · 𝐵) ≠ 0)
4541, 42, 44mulne0bad 11918 . . . . . 6 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) → 𝐴 ≠ 0)
4645neneqd 2945 . . . . 5 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) → ¬ 𝐴 = 0)
4746adantr 480 . . . 4 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 = 0) → ¬ 𝐴 = 0)
4840, 47pm2.21dd 195 . . 3 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 = 0) → 1 = (0 · (sgn‘𝐵)))
4927ad2antrr 726 . . . . . . 7 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 0 < 𝐴) → 𝐵 ∈ ℝ)
5049rexrd 11311 . . . . . 6 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 0 < 𝐴) → 𝐵 ∈ ℝ*)
51 simpll 767 . . . . . . 7 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 0 < 𝐴) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
52 0red 11264 . . . . . . . 8 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 0 < 𝐴) → 0 ∈ ℝ)
53 simplll 775 . . . . . . . 8 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 0 < 𝐴) → 𝐴 ∈ ℝ)
54 simpr 484 . . . . . . . 8 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 0 < 𝐴) → 0 < 𝐴)
5552, 53, 54ltled 11409 . . . . . . 7 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 0 < 𝐴) → 0 ≤ 𝐴)
56 simplr 769 . . . . . . 7 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 0 < 𝐴) → 0 < (𝐴 · 𝐵))
57 prodgt0 12114 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 0 < (𝐴 · 𝐵))) → 0 < 𝐵)
5851, 55, 56, 57syl12anc 837 . . . . . 6 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 0 < 𝐴) → 0 < 𝐵)
59 sgnp 15129 . . . . . 6 ((𝐵 ∈ ℝ* ∧ 0 < 𝐵) → (sgn‘𝐵) = 1)
6050, 58, 59syl2anc 584 . . . . 5 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 0 < 𝐴) → (sgn‘𝐵) = 1)
6160oveq2d 7447 . . . 4 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 0 < 𝐴) → (1 · (sgn‘𝐵)) = (1 · 1))
62 1t1e1 12428 . . . 4 (1 · 1) = 1
6361, 62eqtr2di 2794 . . 3 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 0 < 𝐴) → 1 = (1 · (sgn‘𝐵)))
6427ad2antrr 726 . . . . . . 7 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → 𝐵 ∈ ℝ)
6564rexrd 11311 . . . . . 6 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → 𝐵 ∈ ℝ*)
66 simplll 775 . . . . . . . . 9 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → 𝐴 ∈ ℝ)
6766renegcld 11690 . . . . . . . 8 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → -𝐴 ∈ ℝ)
6864renegcld 11690 . . . . . . . 8 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → -𝐵 ∈ ℝ)
69 0red 11264 . . . . . . . . 9 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → 0 ∈ ℝ)
70 simpr 484 . . . . . . . . . 10 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → 𝐴 < 0)
7125lt0neg1d 11832 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 0 ↔ 0 < -𝐴))
7271ad2antrr 726 . . . . . . . . . 10 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → (𝐴 < 0 ↔ 0 < -𝐴))
7370, 72mpbid 232 . . . . . . . . 9 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → 0 < -𝐴)
7469, 67, 73ltled 11409 . . . . . . . 8 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → 0 ≤ -𝐴)
75 simplr 769 . . . . . . . . 9 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → 0 < (𝐴 · 𝐵))
7626ad2antrr 726 . . . . . . . . . 10 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → 𝐴 ∈ ℂ)
7728ad2antrr 726 . . . . . . . . . 10 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → 𝐵 ∈ ℂ)
7876, 77mul2negd 11718 . . . . . . . . 9 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → (-𝐴 · -𝐵) = (𝐴 · 𝐵))
7975, 78breqtrrd 5171 . . . . . . . 8 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → 0 < (-𝐴 · -𝐵))
80 prodgt0 12114 . . . . . . . 8 (((-𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) ∧ (0 ≤ -𝐴 ∧ 0 < (-𝐴 · -𝐵))) → 0 < -𝐵)
8167, 68, 74, 79, 80syl22anc 839 . . . . . . 7 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → 0 < -𝐵)
8227lt0neg1d 11832 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 < 0 ↔ 0 < -𝐵))
8382ad2antrr 726 . . . . . . 7 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → (𝐵 < 0 ↔ 0 < -𝐵))
8481, 83mpbird 257 . . . . . 6 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → 𝐵 < 0)
85 sgnn 15133 . . . . . 6 ((𝐵 ∈ ℝ*𝐵 < 0) → (sgn‘𝐵) = -1)
8665, 84, 85syl2anc 584 . . . . 5 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → (sgn‘𝐵) = -1)
8786oveq2d 7447 . . . 4 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → (-1 · (sgn‘𝐵)) = (-1 · -1))
88 neg1mulneg1e1 12479 . . . 4 (-1 · -1) = 1
8987, 88eqtr2di 2794 . . 3 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) ∧ 𝐴 < 0) → 1 = (-1 · (sgn‘𝐵)))
9033, 35, 37, 39, 48, 63, 89sgn3da 34544 . 2 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 < (𝐴 · 𝐵)) → 1 = ((sgn‘𝐴) · (sgn‘𝐵)))
91 simpll 767 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) → 𝐴 ∈ ℝ)
9291rexrd 11311 . . 3 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) → 𝐴 ∈ ℝ*)
9334eqeq2d 2748 . . 3 ((sgn‘𝐴) = 0 → (-1 = ((sgn‘𝐴) · (sgn‘𝐵)) ↔ -1 = (0 · (sgn‘𝐵))))
9436eqeq2d 2748 . . 3 ((sgn‘𝐴) = 1 → (-1 = ((sgn‘𝐴) · (sgn‘𝐵)) ↔ -1 = (1 · (sgn‘𝐵))))
9538eqeq2d 2748 . . 3 ((sgn‘𝐴) = -1 → (-1 = ((sgn‘𝐴) · (sgn‘𝐵)) ↔ -1 = (-1 · (sgn‘𝐵))))
96 simpr 484 . . . 4 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 = 0) → 𝐴 = 0)
9726ad2antrr 726 . . . . . 6 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 = 0) → 𝐴 ∈ ℂ)
9828ad2antrr 726 . . . . . 6 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 = 0) → 𝐵 ∈ ℂ)
99 simplr 769 . . . . . . 7 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 = 0) → (𝐴 · 𝐵) < 0)
10099lt0ne0d 11828 . . . . . 6 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 = 0) → (𝐴 · 𝐵) ≠ 0)
10197, 98, 100mulne0bad 11918 . . . . 5 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 = 0) → 𝐴 ≠ 0)
102101neneqd 2945 . . . 4 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 = 0) → ¬ 𝐴 = 0)
10396, 102pm2.21dd 195 . . 3 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 = 0) → -1 = (0 · (sgn‘𝐵)))
10427ad2antrr 726 . . . . . . 7 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 0 < 𝐴) → 𝐵 ∈ ℝ)
105104rexrd 11311 . . . . . 6 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 0 < 𝐴) → 𝐵 ∈ ℝ*)
106 simplr 769 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) → 𝐵 ∈ ℝ)
10726, 28mulcomd 11282 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
108107breq1d 5153 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 · 𝐵) < 0 ↔ (𝐵 · 𝐴) < 0))
109108biimpa 476 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) → (𝐵 · 𝐴) < 0)
110106, 91, 109mul2lt0rgt0 13138 . . . . . 6 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 0 < 𝐴) → 𝐵 < 0)
111105, 110, 85syl2anc 584 . . . . 5 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 0 < 𝐴) → (sgn‘𝐵) = -1)
112111oveq2d 7447 . . . 4 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 0 < 𝐴) → (1 · (sgn‘𝐵)) = (1 · -1))
113 neg1cn 12380 . . . . 5 -1 ∈ ℂ
114113mullidi 11266 . . . 4 (1 · -1) = -1
115112, 114eqtr2di 2794 . . 3 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 0 < 𝐴) → -1 = (1 · (sgn‘𝐵)))
116106adantr 480 . . . . . . 7 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 < 0) → 𝐵 ∈ ℝ)
117116rexrd 11311 . . . . . 6 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 < 0) → 𝐵 ∈ ℝ*)
118106, 91, 109mul2lt0rlt0 13137 . . . . . 6 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 < 0) → 0 < 𝐵)
119117, 118, 59syl2anc 584 . . . . 5 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 < 0) → (sgn‘𝐵) = 1)
120119oveq2d 7447 . . . 4 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 < 0) → (-1 · (sgn‘𝐵)) = (-1 · 1))
121113mulridi 11265 . . . 4 (-1 · 1) = -1
122120, 121eqtr2di 2794 . . 3 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 < 0) → -1 = (-1 · (sgn‘𝐵)))
12392, 93, 94, 95, 103, 115, 122sgn3da 34544 . 2 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) → -1 = ((sgn‘𝐴) · (sgn‘𝐵)))
1242, 3, 4, 5, 31, 90, 123sgn3da 34544 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (sgn‘(𝐴 · 𝐵)) = ((sgn‘𝐴) · (sgn‘𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 848   = wceq 1540  wcel 2108   class class class wbr 5143  cfv 6561  (class class class)co 7431  cc 11153  cr 11154  0cc0 11155  1c1 11156   · cmul 11160  *cxr 11294   < clt 11295  cle 11296  -cneg 11493  sgncsgn 15125
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-po 5592  df-so 5593  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-rp 13035  df-sgn 15126
This theorem is referenced by:  sgnmulrp2  34546  sgnmulsgn  34552  sgnmulsgp  34553
  Copyright terms: Public domain W3C validator