nn0xmulclb

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

		Ref	Expression
	Assertion	nn0xmulclb	$⊢ ((A \in ℕ_{0}^{} \land B \in ℕ_{0}^{}) \land (A \neq 0 \land B \neq 0)) \to (A \cdot_{𝑒} B \in ℕ_{0} \leftrightarrow (A \in ℕ_{0} \land B \in ℕ_{0}))$

Proof

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

Metamath Proof Explorer

Theorem nn0xmulclb

Proof