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 ∧ 𝐵 = +∞ ) ) ) ) → 𝐴 ∈ ℝ )