Step |
Hyp |
Ref |
Expression |
1 |
|
recnaddnred.a |
|- ( ph -> A e. RR ) |
2 |
|
recnaddnred.b |
|- ( ph -> B e. ( CC \ RR ) ) |
3 |
|
cndivrenred.n |
|- ( ph -> A =/= 0 ) |
4 |
2
|
eldifbd |
|- ( ph -> -. B e. RR ) |
5 |
|
df-nel |
|- ( ( A x. B ) e/ RR <-> -. ( A x. B ) e. RR ) |
6 |
2
|
eldifad |
|- ( ph -> B e. CC ) |
7 |
|
mulre |
|- ( ( B e. CC /\ A e. RR /\ A =/= 0 ) -> ( B e. RR <-> ( A x. B ) e. RR ) ) |
8 |
6 1 3 7
|
syl3anc |
|- ( ph -> ( B e. RR <-> ( A x. B ) e. RR ) ) |
9 |
8
|
bicomd |
|- ( ph -> ( ( A x. B ) e. RR <-> B e. RR ) ) |
10 |
9
|
notbid |
|- ( ph -> ( -. ( A x. B ) e. RR <-> -. B e. RR ) ) |
11 |
5 10
|
syl5bb |
|- ( ph -> ( ( A x. B ) e/ RR <-> -. B e. RR ) ) |
12 |
4 11
|
mpbird |
|- ( ph -> ( A x. B ) e/ RR ) |