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 0 * B 0 * A 0 B 0 A 𝑒 B 0 A 0 B 0

Proof

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