Metamath Proof Explorer

Theorem nn0xmulclb

Description: Finite multiplication in the extended nonnegative integers. (Contributed by Thierry Arnoux, 30-Jul-2023)

Ref Expression
Assertion nn0xmulclb 
|- ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> ( ( A *e B ) e. NN0 <-> ( A e. NN0 /\ B e. NN0 ) ) )

Proof

Step Hyp Ref Expression
1 simplr 
 |-  ( ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A *e B ) e. NN0 ) /\ -. ( A e. NN0 /\ B e. NN0 ) ) -> ( A *e B ) e. NN0 )
2 simpr 
 |-  ( ( ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A *e B ) e. NN0 ) /\ -. ( A e. NN0 /\ B e. NN0 ) ) /\ A = +oo ) -> A = +oo )
3 2 oveq1d 
 |-  ( ( ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A *e B ) e. NN0 ) /\ -. ( A e. NN0 /\ B e. NN0 ) ) /\ A = +oo ) -> ( A *e B ) = ( +oo *e B ) )
4 xnn0xr 
 |-  ( B e. NN0* -> B e. RR* )
5 4 ad5antlr 
 |-  ( ( ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A *e B ) e. NN0 ) /\ -. ( A e. NN0 /\ B e. NN0 ) ) /\ A = +oo ) -> B e. RR* )
6 simp-5r 
 |-  ( ( ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A *e B ) e. NN0 ) /\ -. ( A e. NN0 /\ B e. NN0 ) ) /\ A = +oo ) -> B e. NN0* )
7 simprr 
 |-  ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> B =/= 0 )
8 7 ad3antrrr 
 |-  ( ( ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A *e B ) e. NN0 ) /\ -. ( A e. NN0 /\ B e. NN0 ) ) /\ A = +oo ) -> B =/= 0 )
9 xnn0gt0 
 |-  ( ( B e. NN0* /\ B =/= 0 ) -> 0 < B )
10 6 8 9 syl2anc 
 |-  ( ( ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A *e B ) e. NN0 ) /\ -. ( A e. NN0 /\ B e. NN0 ) ) /\ A = +oo ) -> 0 < B )
11 xmulpnf2 
 |-  ( ( B e. RR* /\ 0 < B ) -> ( +oo *e B ) = +oo )
12 5 10 11 syl2anc 
 |-  ( ( ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A *e B ) e. NN0 ) /\ -. ( A e. NN0 /\ B e. NN0 ) ) /\ A = +oo ) -> ( +oo *e B ) = +oo )
13 pnfnre2 
 |-  -. +oo e. RR
14 nn0re 
 |-  ( +oo e. NN0 -> +oo e. RR )
15 13 14 mto 
 |-  -. +oo e. NN0
16 15 a1i 
 |-  ( ( ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A *e B ) e. NN0 ) /\ -. ( A e. NN0 /\ B e. NN0 ) ) /\ A = +oo ) -> -. +oo e. NN0 )
17 12 16 eqneltrd 
 |-  ( ( ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A *e B ) e. NN0 ) /\ -. ( A e. NN0 /\ B e. NN0 ) ) /\ A = +oo ) -> -. ( +oo *e B ) e. NN0 )
18 3 17 eqneltrd 
 |-  ( ( ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A *e B ) e. NN0 ) /\ -. ( A e. NN0 /\ B e. NN0 ) ) /\ A = +oo ) -> -. ( A *e B ) e. NN0 )
19 simpr 
 |-  ( ( ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A *e B ) e. NN0 ) /\ -. ( A e. NN0 /\ B e. NN0 ) ) /\ B = +oo ) -> B = +oo )
20 19 oveq2d 
 |-  ( ( ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A *e B ) e. NN0 ) /\ -. ( A e. NN0 /\ B e. NN0 ) ) /\ B = +oo ) -> ( A *e B ) = ( A *e +oo ) )
21 xnn0xr 
 |-  ( A e. NN0* -> A e. RR* )
22 21 ad5antr 
 |-  ( ( ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A *e B ) e. NN0 ) /\ -. ( A e. NN0 /\ B e. NN0 ) ) /\ B = +oo ) -> A e. RR* )
23 simp-5l 
 |-  ( ( ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A *e B ) e. NN0 ) /\ -. ( A e. NN0 /\ B e. NN0 ) ) /\ B = +oo ) -> A e. NN0* )
24 simprl 
 |-  ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> A =/= 0 )
25 24 ad3antrrr 
 |-  ( ( ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A *e B ) e. NN0 ) /\ -. ( A e. NN0 /\ B e. NN0 ) ) /\ B = +oo ) -> A =/= 0 )
26 xnn0gt0 
 |-  ( ( A e. NN0* /\ A =/= 0 ) -> 0 < A )
27 23 25 26 syl2anc 
 |-  ( ( ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A *e B ) e. NN0 ) /\ -. ( A e. NN0 /\ B e. NN0 ) ) /\ B = +oo ) -> 0 < A )
28 xmulpnf1 
 |-  ( ( A e. RR* /\ 0 < A ) -> ( A *e +oo ) = +oo )
29 22 27 28 syl2anc 
 |-  ( ( ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A *e B ) e. NN0 ) /\ -. ( A e. NN0 /\ B e. NN0 ) ) /\ B = +oo ) -> ( A *e +oo ) = +oo )
30 15 a1i 
 |-  ( ( ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A *e B ) e. NN0 ) /\ -. ( A e. NN0 /\ B e. NN0 ) ) /\ B = +oo ) -> -. +oo e. NN0 )
31 29 30 eqneltrd 
 |-  ( ( ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A *e B ) e. NN0 ) /\ -. ( A e. NN0 /\ B e. NN0 ) ) /\ B = +oo ) -> -. ( A *e +oo ) e. NN0 )
32 20 31 eqneltrd 
 |-  ( ( ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A *e B ) e. NN0 ) /\ -. ( A e. NN0 /\ B e. NN0 ) ) /\ B = +oo ) -> -. ( A *e B ) e. NN0 )
33 xnn0nnn0pnf 
 |-  ( ( A e. NN0* /\ -. A e. NN0 ) -> A = +oo )
34 33 ad5ant15 
 |-  ( ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A *e B ) e. NN0 ) /\ -. A e. NN0 ) -> A = +oo )
35 34 ex 
 |-  ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A *e B ) e. NN0 ) -> ( -. A e. NN0 -> A = +oo ) )
36 xnn0nnn0pnf 
 |-  ( ( B e. NN0* /\ -. B e. NN0 ) -> B = +oo )
37 36 ad5ant25 
 |-  ( ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A *e B ) e. NN0 ) /\ -. B e. NN0 ) -> B = +oo )
38 37 ex 
 |-  ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A *e B ) e. NN0 ) -> ( -. B e. NN0 -> B = +oo ) )
39 35 38 orim12d 
 |-  ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A *e B ) e. NN0 ) -> ( ( -. A e. NN0 \/ -. B e. NN0 ) -> ( A = +oo \/ B = +oo ) ) )
40 pm3.13 
 |-  ( -. ( A e. NN0 /\ B e. NN0 ) -> ( -. A e. NN0 \/ -. B e. NN0 ) )
41 39 40 impel 
 |-  ( ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A *e B ) e. NN0 ) /\ -. ( A e. NN0 /\ B e. NN0 ) ) -> ( A = +oo \/ B = +oo ) )
42 18 32 41 mpjaodan 
 |-  ( ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A *e B ) e. NN0 ) /\ -. ( A e. NN0 /\ B e. NN0 ) ) -> -. ( A *e B ) e. NN0 )
43 1 42 condan 
 |-  ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A *e B ) e. NN0 ) -> ( A e. NN0 /\ B e. NN0 ) )
44 nn0re 
 |-  ( A e. NN0 -> A e. RR )
45 44 ad2antrl 
 |-  ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A e. NN0 /\ B e. NN0 ) ) -> A e. RR )
46 nn0re 
 |-  ( B e. NN0 -> B e. RR )
47 46 ad2antll 
 |-  ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A e. NN0 /\ B e. NN0 ) ) -> B e. RR )
48 rexmul 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A *e B ) = ( A x. B ) )
49 45 47 48 syl2anc 
 |-  ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A e. NN0 /\ B e. NN0 ) ) -> ( A *e B ) = ( A x. B ) )
50 nn0mulcl 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( A x. B ) e. NN0 )
51 50 adantl 
 |-  ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A e. NN0 /\ B e. NN0 ) ) -> ( A x. B ) e. NN0 )
52 49 51 eqeltrd 
 |-  ( ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) /\ ( A e. NN0 /\ B e. NN0 ) ) -> ( A *e B ) e. NN0 )
53 43 52 impbida 
 |-  ( ( ( A e. NN0* /\ B e. NN0* ) /\ ( A =/= 0 /\ B =/= 0 ) ) -> ( ( A *e B ) e. NN0 <-> ( A e. NN0 /\ B e. NN0 ) ) )