Metamath Proof Explorer


Theorem xmullem

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

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

Proof

Step Hyp Ref Expression
1 ioran ( ¬ ( 𝐴 = 0 ∨ 𝐵 = 0 ) ↔ ( ¬ 𝐴 = 0 ∧ ¬ 𝐵 = 0 ) )
2 1 anbi2i ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ¬ ( 𝐴 = 0 ∨ 𝐵 = 0 ) ) ↔ ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( ¬ 𝐴 = 0 ∧ ¬ 𝐵 = 0 ) ) )
3 ioran ( ¬ ( ( ( 0 < 𝐵𝐴 = +∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴𝐵 = +∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ↔ ( ¬ ( ( 0 < 𝐵𝐴 = +∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ¬ ( ( 0 < 𝐴𝐵 = +∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) )
4 ioran ( ¬ ( ( 0 < 𝐵𝐴 = +∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ↔ ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) )
5 ioran ( ¬ ( ( 0 < 𝐴𝐵 = +∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ↔ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) )
6 4 5 anbi12i ( ( ¬ ( ( 0 < 𝐵𝐴 = +∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ¬ ( ( 0 < 𝐴𝐵 = +∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ↔ ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) )
7 3 6 bitri ( ¬ ( ( ( 0 < 𝐵𝐴 = +∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴𝐵 = +∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ↔ ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) )
8 ioran ( ¬ ( ( ( 0 < 𝐵𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ↔ ( ¬ ( ( 0 < 𝐵𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ¬ ( ( 0 < 𝐴𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) )
9 ioran ( ¬ ( ( 0 < 𝐵𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ↔ ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) )
10 ioran ( ¬ ( ( 0 < 𝐴𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ↔ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) )
11 9 10 anbi12i ( ( ¬ ( ( 0 < 𝐵𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ¬ ( ( 0 < 𝐴𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ↔ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) )
12 8 11 bitri ( ¬ ( ( ( 0 < 𝐵𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ↔ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) )
13 7 12 anbi12i ( ( ¬ ( ( ( 0 < 𝐵𝐴 = +∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴𝐵 = +∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ¬ ( ( ( 0 < 𝐵𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) ↔ ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) )
14 simplll ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( ¬ 𝐴 = 0 ∧ ¬ 𝐵 = 0 ) ) ∧ ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) ) → 𝐴 ∈ ℝ* )
15 elxr ( 𝐴 ∈ ℝ* ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) )
16 14 15 sylib ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( ¬ 𝐴 = 0 ∧ ¬ 𝐵 = 0 ) ) ∧ ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) ) → ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) )
17 idd ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( ¬ 𝐴 = 0 ∧ ¬ 𝐵 = 0 ) ) ∧ ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) ) → ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ ) )
18 simprlr ( ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) → ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) )
19 18 adantl ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( ¬ 𝐴 = 0 ∧ ¬ 𝐵 = 0 ) ) ∧ ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) ) → ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) )
20 19 pm2.21d ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( ¬ 𝐴 = 0 ∧ ¬ 𝐵 = 0 ) ) ∧ ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) ) → ( ( 𝐵 < 0 ∧ 𝐴 = +∞ ) → 𝐴 ∈ ℝ ) )
21 20 expdimp ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( ¬ 𝐴 = 0 ∧ ¬ 𝐵 = 0 ) ) ∧ ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) ) ∧ 𝐵 < 0 ) → ( 𝐴 = +∞ → 𝐴 ∈ ℝ ) )
22 simplrr ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( ¬ 𝐴 = 0 ∧ ¬ 𝐵 = 0 ) ) ∧ ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) ) → ¬ 𝐵 = 0 )
23 22 pm2.21d ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( ¬ 𝐴 = 0 ∧ ¬ 𝐵 = 0 ) ) ∧ ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) ) → ( 𝐵 = 0 → ( 𝐴 = +∞ → 𝐴 ∈ ℝ ) ) )
24 23 imp ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( ¬ 𝐴 = 0 ∧ ¬ 𝐵 = 0 ) ) ∧ ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) ) ∧ 𝐵 = 0 ) → ( 𝐴 = +∞ → 𝐴 ∈ ℝ ) )
25 simplll ( ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) → ¬ ( 0 < 𝐵𝐴 = +∞ ) )
26 25 adantl ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( ¬ 𝐴 = 0 ∧ ¬ 𝐵 = 0 ) ) ∧ ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) ) → ¬ ( 0 < 𝐵𝐴 = +∞ ) )
27 26 pm2.21d ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( ¬ 𝐴 = 0 ∧ ¬ 𝐵 = 0 ) ) ∧ ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) ) → ( ( 0 < 𝐵𝐴 = +∞ ) → 𝐴 ∈ ℝ ) )
28 27 expdimp ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( ¬ 𝐴 = 0 ∧ ¬ 𝐵 = 0 ) ) ∧ ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) ) ∧ 0 < 𝐵 ) → ( 𝐴 = +∞ → 𝐴 ∈ ℝ ) )
29 simpllr ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( ¬ 𝐴 = 0 ∧ ¬ 𝐵 = 0 ) ) ∧ ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) ) → 𝐵 ∈ ℝ* )
30 0xr 0 ∈ ℝ*
31 xrltso < Or ℝ*
32 solin ( ( < Or ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ∈ ℝ* ) ) → ( 𝐵 < 0 ∨ 𝐵 = 0 ∨ 0 < 𝐵 ) )
33 31 32 mpan ( ( 𝐵 ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( 𝐵 < 0 ∨ 𝐵 = 0 ∨ 0 < 𝐵 ) )
34 29 30 33 sylancl ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( ¬ 𝐴 = 0 ∧ ¬ 𝐵 = 0 ) ) ∧ ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) ) → ( 𝐵 < 0 ∨ 𝐵 = 0 ∨ 0 < 𝐵 ) )
35 21 24 28 34 mpjao3dan ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( ¬ 𝐴 = 0 ∧ ¬ 𝐵 = 0 ) ) ∧ ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) ) → ( 𝐴 = +∞ → 𝐴 ∈ ℝ ) )
36 simpllr ( ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) → ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) )
37 36 adantl ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( ¬ 𝐴 = 0 ∧ ¬ 𝐵 = 0 ) ) ∧ ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) ) → ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) )
38 37 pm2.21d ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( ¬ 𝐴 = 0 ∧ ¬ 𝐵 = 0 ) ) ∧ ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) ) → ( ( 𝐵 < 0 ∧ 𝐴 = -∞ ) → 𝐴 ∈ ℝ ) )
39 38 expdimp ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( ¬ 𝐴 = 0 ∧ ¬ 𝐵 = 0 ) ) ∧ ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) ) ∧ 𝐵 < 0 ) → ( 𝐴 = -∞ → 𝐴 ∈ ℝ ) )
40 22 pm2.21d ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( ¬ 𝐴 = 0 ∧ ¬ 𝐵 = 0 ) ) ∧ ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) ) → ( 𝐵 = 0 → ( 𝐴 = -∞ → 𝐴 ∈ ℝ ) ) )
41 40 imp ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( ¬ 𝐴 = 0 ∧ ¬ 𝐵 = 0 ) ) ∧ ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) ) ∧ 𝐵 = 0 ) → ( 𝐴 = -∞ → 𝐴 ∈ ℝ ) )
42 simprll ( ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) → ¬ ( 0 < 𝐵𝐴 = -∞ ) )
43 42 adantl ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( ¬ 𝐴 = 0 ∧ ¬ 𝐵 = 0 ) ) ∧ ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) ) → ¬ ( 0 < 𝐵𝐴 = -∞ ) )
44 43 pm2.21d ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( ¬ 𝐴 = 0 ∧ ¬ 𝐵 = 0 ) ) ∧ ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) ) → ( ( 0 < 𝐵𝐴 = -∞ ) → 𝐴 ∈ ℝ ) )
45 44 expdimp ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( ¬ 𝐴 = 0 ∧ ¬ 𝐵 = 0 ) ) ∧ ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) ) ∧ 0 < 𝐵 ) → ( 𝐴 = -∞ → 𝐴 ∈ ℝ ) )
46 39 41 45 34 mpjao3dan ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( ¬ 𝐴 = 0 ∧ ¬ 𝐵 = 0 ) ) ∧ ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) ) → ( 𝐴 = -∞ → 𝐴 ∈ ℝ ) )
47 17 35 46 3jaod ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( ¬ 𝐴 = 0 ∧ ¬ 𝐵 = 0 ) ) ∧ ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) ) → ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) → 𝐴 ∈ ℝ ) )
48 16 47 mpd ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( ¬ 𝐴 = 0 ∧ ¬ 𝐵 = 0 ) ) ∧ ( ( ( ¬ ( 0 < 𝐵𝐴 = +∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = +∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ( ( ¬ ( 0 < 𝐵𝐴 = -∞ ) ∧ ¬ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∧ ( ¬ ( 0 < 𝐴𝐵 = -∞ ) ∧ ¬ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) ) → 𝐴 ∈ ℝ )
49 2 13 48 syl2anb ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ¬ ( 𝐴 = 0 ∨ 𝐵 = 0 ) ) ∧ ( ¬ ( ( ( 0 < 𝐵𝐴 = +∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴𝐵 = +∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ∧ ¬ ( ( ( 0 < 𝐵𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) ) → 𝐴 ∈ ℝ )
50 49 anassrs ( ( ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ¬ ( 𝐴 = 0 ∨ 𝐵 = 0 ) ) ∧ ¬ ( ( ( 0 < 𝐵𝐴 = +∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = -∞ ) ) ∨ ( ( 0 < 𝐴𝐵 = +∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = -∞ ) ) ) ) ∧ ¬ ( ( ( 0 < 𝐵𝐴 = -∞ ) ∨ ( 𝐵 < 0 ∧ 𝐴 = +∞ ) ) ∨ ( ( 0 < 𝐴𝐵 = -∞ ) ∨ ( 𝐴 < 0 ∧ 𝐵 = +∞ ) ) ) ) → 𝐴 ∈ ℝ )