Theorem nn0xmulclb

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

	Ref	Expression
Assertion	nn0xmulclb	⊢ ( ( ( 𝐴 ∈ ℕ0* ∧ 𝐵 ∈ ℕ0* ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐴 ·e 𝐵 ) ∈ ℕ0 ↔ ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) ) )

Proof

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