This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )