Metamath Proof Explorer

Theorem xmullem2

Description: Lemma for xmulneg1 . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmullem2 ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) → ¬ ( ( ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mnfnepnf ⊢ -∞ ≠ +∞
2 eqeq1 ⊢ ( 𝐴 = -∞ → ( 𝐴 = +∞ ↔ -∞ = +∞ ) )
3 2 necon3bbid ⊢ ( 𝐴 = -∞ → ( ¬ 𝐴 = +∞ ↔ -∞ ≠ +∞ ) )
4 1 3 mpbiri ⊢ ( 𝐴 = -∞ → ¬ 𝐴 = +∞ )
5 4 con2i ⊢ ( 𝐴 = +∞ → ¬ 𝐴 = -∞ )
6 5 adantl ⊢ ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) → ¬ 𝐴 = -∞ )
7 0xr ⊢ 0 ∈ ℝ*
8 nltmnf ⊢ ( 0 ∈ ℝ* → ¬ 0 < -∞ )
9 7 8 ax-mp ⊢ ¬ 0 < -∞
10 breq2 ⊢ ( 𝐴 = -∞ → ( 0 < 𝐴 ↔ 0 < -∞ ) )
11 9 10 mtbiri ⊢ ( 𝐴 = -∞ → ¬ 0 < 𝐴 )
12 11 con2i ⊢ ( 0 < 𝐴 → ¬ 𝐴 = -∞ )
13 12 adantr ⊢ ( ( 0 < 𝐴 ∧ 𝐵 = +∞ ) → ¬ 𝐴 = -∞ )
14 6 13 jaoi ⊢ ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ) → ¬ 𝐴 = -∞ )
15 14 a1i ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ) → ¬ 𝐴 = -∞ ) )
16 simpr ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → 𝐵 ∈ ℝ* )
17 xrltnsym ⊢ ( ( 𝐵 ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( 𝐵 < 0 → ¬ 0 < 𝐵 ) )
18 16 7 17 sylancl ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐵 < 0 → ¬ 0 < 𝐵 ) )
19 18 adantrd ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐵 < 0 ∧ 𝐴 = -∞ ) → ¬ 0 < 𝐵 ) )
20 breq2 ⊢ ( 𝐵 = -∞ → ( 0 < 𝐵 ↔ 0 < -∞ ) )
21 9 20 mtbiri ⊢ ( 𝐵 = -∞ → ¬ 0 < 𝐵 )
22 21 adantl ⊢ ( ( 𝐴 < 0 ∧ 𝐵 = -∞ ) → ¬ 0 < 𝐵 )
23 22 a1i ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 < 0 ∧ 𝐵 = -∞ ) → ¬ 0 < 𝐵 ) )
24 19 23 jaod ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) → ¬ 0 < 𝐵 ) )
25 15 24 orim12d ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ) ∨ ( ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) → ( ¬ 𝐴 = -∞ ∨ ¬ 0 < 𝐵 ) ) )
26 ianor ⊢ ( ¬ ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ↔ ( ¬ 0 < 𝐵 ∨ ¬ 𝐴 = -∞ ) )
27 orcom ⊢ ( ( ¬ 0 < 𝐵 ∨ ¬ 𝐴 = -∞ ) ↔ ( ¬ 𝐴 = -∞ ∨ ¬ 0 < 𝐵 ) )
28 26 27 bitri ⊢ ( ¬ ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ↔ ( ¬ 𝐴 = -∞ ∨ ¬ 0 < 𝐵 ) )
29 25 28 syl6ibr ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ) ∨ ( ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) → ¬ ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ) )
30 18 con2d ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 0 < 𝐵 → ¬ 𝐵 < 0 ) )
31 30 adantrd ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) → ¬ 𝐵 < 0 ) )
32 pnfnlt ⊢ ( 0 ∈ ℝ* → ¬ +∞ < 0 )
33 7 32 ax-mp ⊢ ¬ +∞ < 0
34 simpr ⊢ ( ( 0 < 𝐴 ∧ 𝐵 = +∞ ) → 𝐵 = +∞ )
35 34 breq1d ⊢ ( ( 0 < 𝐴 ∧ 𝐵 = +∞ ) → ( 𝐵 < 0 ↔ +∞ < 0 ) )
36 33 35 mtbiri ⊢ ( ( 0 < 𝐴 ∧ 𝐵 = +∞ ) → ¬ 𝐵 < 0 )
37 36 a1i ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 0 < 𝐴 ∧ 𝐵 = +∞ ) → ¬ 𝐵 < 0 ) )
38 31 37 jaod ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ) → ¬ 𝐵 < 0 ) )
39 4 a1i ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 = -∞ → ¬ 𝐴 = +∞ ) )
40 39 adantld ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐵 < 0 ∧ 𝐴 = -∞ ) → ¬ 𝐴 = +∞ ) )
41 breq1 ⊢ ( 𝐴 = +∞ → ( 𝐴 < 0 ↔ +∞ < 0 ) )
42 33 41 mtbiri ⊢ ( 𝐴 = +∞ → ¬ 𝐴 < 0 )
43 42 con2i ⊢ ( 𝐴 < 0 → ¬ 𝐴 = +∞ )
44 43 adantr ⊢ ( ( 𝐴 < 0 ∧ 𝐵 = -∞ ) → ¬ 𝐴 = +∞ )
45 44 a1i ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 < 0 ∧ 𝐵 = -∞ ) → ¬ 𝐴 = +∞ ) )
46 40 45 jaod ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) → ¬ 𝐴 = +∞ ) )
47 38 46 orim12d ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ) ∨ ( ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) → ( ¬ 𝐵 < 0 ∨ ¬ 𝐴 = +∞ ) ) )
48 ianor ⊢ ( ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ↔ ( ¬ 𝐵 < 0 ∨ ¬ 𝐴 = +∞ ) )
49 47 48 syl6ibr ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ) ∨ ( ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) → ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) )
50 29 49 jcad ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ) ∨ ( ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) → ( ¬ ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ) )
51 ioran ⊢ ( ¬ ( ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ↔ ( ¬ ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) )
52 50 51 syl6ibr ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ) ∨ ( ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) → ¬ ( ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ) )
53 21 con2i ⊢ ( 0 < 𝐵 → ¬ 𝐵 = -∞ )
54 53 adantr ⊢ ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) → ¬ 𝐵 = -∞ )
55 54 a1i ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) → ¬ 𝐵 = -∞ ) )
56 pnfnemnf ⊢ +∞ ≠ -∞
57 eqeq1 ⊢ ( 𝐵 = +∞ → ( 𝐵 = -∞ ↔ +∞ = -∞ ) )
58 57 necon3bbid ⊢ ( 𝐵 = +∞ → ( ¬ 𝐵 = -∞ ↔ +∞ ≠ -∞ ) )
59 56 58 mpbiri ⊢ ( 𝐵 = +∞ → ¬ 𝐵 = -∞ )
60 59 adantl ⊢ ( ( 0 < 𝐴 ∧ 𝐵 = +∞ ) → ¬ 𝐵 = -∞ )
61 60 a1i ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 0 < 𝐴 ∧ 𝐵 = +∞ ) → ¬ 𝐵 = -∞ ) )
62 55 61 jaod ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ) → ¬ 𝐵 = -∞ ) )
63 11 adantl ⊢ ( ( 𝐵 < 0 ∧ 𝐴 = -∞ ) → ¬ 0 < 𝐴 )
64 63 a1i ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐵 < 0 ∧ 𝐴 = -∞ ) → ¬ 0 < 𝐴 ) )
65 simpl ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → 𝐴 ∈ ℝ* )
66 xrltnsym ⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( 𝐴 < 0 → ¬ 0 < 𝐴 ) )
67 65 7 66 sylancl ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 0 → ¬ 0 < 𝐴 ) )
68 67 adantrd ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 < 0 ∧ 𝐵 = -∞ ) → ¬ 0 < 𝐴 ) )
69 64 68 jaod ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) → ¬ 0 < 𝐴 ) )
70 62 69 orim12d ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ) ∨ ( ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) → ( ¬ 𝐵 = -∞ ∨ ¬ 0 < 𝐴 ) ) )
71 ianor ⊢ ( ¬ ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ↔ ( ¬ 0 < 𝐴 ∨ ¬ 𝐵 = -∞ ) )
72 orcom ⊢ ( ( ¬ 0 < 𝐴 ∨ ¬ 𝐵 = -∞ ) ↔ ( ¬ 𝐵 = -∞ ∨ ¬ 0 < 𝐴 ) )
73 71 72 bitri ⊢ ( ¬ ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ↔ ( ¬ 𝐵 = -∞ ∨ ¬ 0 < 𝐴 ) )
74 70 73 syl6ibr ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ) ∨ ( ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) → ¬ ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ) )
75 42 adantl ⊢ ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) → ¬ 𝐴 < 0 )
76 75 a1i ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) → ¬ 𝐴 < 0 ) )
77 67 con2d ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 0 < 𝐴 → ¬ 𝐴 < 0 ) )
78 77 adantrd ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 0 < 𝐴 ∧ 𝐵 = +∞ ) → ¬ 𝐴 < 0 ) )
79 76 78 jaod ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ) → ¬ 𝐴 < 0 ) )
80 breq1 ⊢ ( 𝐵 = +∞ → ( 𝐵 < 0 ↔ +∞ < 0 ) )
81 33 80 mtbiri ⊢ ( 𝐵 = +∞ → ¬ 𝐵 < 0 )
82 81 con2i ⊢ ( 𝐵 < 0 → ¬ 𝐵 = +∞ )
83 82 adantr ⊢ ( ( 𝐵 < 0 ∧ 𝐴 = -∞ ) → ¬ 𝐵 = +∞ )
84 59 con2i ⊢ ( 𝐵 = -∞ → ¬ 𝐵 = +∞ )
85 84 adantl ⊢ ( ( 𝐴 < 0 ∧ 𝐵 = -∞ ) → ¬ 𝐵 = +∞ )
86 83 85 jaoi ⊢ ( ( ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) → ¬ 𝐵 = +∞ )
87 86 a1i ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) → ¬ 𝐵 = +∞ ) )
88 79 87 orim12d ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ) ∨ ( ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) → ( ¬ 𝐴 < 0 ∨ ¬ 𝐵 = +∞ ) ) )
89 ianor ⊢ ( ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ↔ ( ¬ 𝐴 < 0 ∨ ¬ 𝐵 = +∞ ) )
90 88 89 syl6ibr ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ) ∨ ( ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) → ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) )
91 74 90 jcad ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ) ∨ ( ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) → ( ¬ ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) )
92 ioran ⊢ ( ¬ ( ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ↔ ( ¬ ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) )
93 91 92 syl6ibr ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ) ∨ ( ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) → ¬ ( ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) )
94 52 93 jcad ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ) ∨ ( ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) → ( ¬ ( ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ¬ ( ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) )
95 or4 ⊢ ( ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ↔ ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ) ∨ ( ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) )
96 ioran ⊢ ( ¬ ( ( ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ↔ ( ¬ ( ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ¬ ( ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) )
97 94 95 96 3imtr4g ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( ( ( 0 < 𝐵 ∧ 𝐴 = +∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = +∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) → ¬ ( ( ( 0 < 𝐵 ∧ 𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴 ∧ 𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) )