Proof of Theorem nn0xmulclb
| Step | Hyp | Ref
| Expression |
| 1 | | simplr 769 |
. . 3
⊢
(((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ·e 𝐵) ∈ ℕ0)
∧ ¬ (𝐴 ∈
ℕ0 ∧ 𝐵
∈ ℕ0)) → (𝐴 ·e 𝐵) ∈
ℕ0) |
| 2 | | simpr 484 |
. . . . . 6
⊢
((((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ·e 𝐵) ∈ ℕ0)
∧ ¬ (𝐴 ∈
ℕ0 ∧ 𝐵
∈ ℕ0)) ∧ 𝐴 = +∞) → 𝐴 = +∞) |
| 3 | 2 | oveq1d 7446 |
. . . . 5
⊢
((((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ·e 𝐵) ∈ ℕ0)
∧ ¬ (𝐴 ∈
ℕ0 ∧ 𝐵
∈ ℕ0)) ∧ 𝐴 = +∞) → (𝐴 ·e 𝐵) = (+∞ ·e 𝐵)) |
| 4 | | xnn0xr 12604 |
. . . . . . . 8
⊢ (𝐵 ∈
ℕ0* → 𝐵 ∈
ℝ*) |
| 5 | 4 | ad5antlr 735 |
. . . . . . 7
⊢
((((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ·e 𝐵) ∈ ℕ0)
∧ ¬ (𝐴 ∈
ℕ0 ∧ 𝐵
∈ ℕ0)) ∧ 𝐴 = +∞) → 𝐵 ∈
ℝ*) |
| 6 | | simp-5r 786 |
. . . . . . . 8
⊢
((((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ·e 𝐵) ∈ ℕ0)
∧ ¬ (𝐴 ∈
ℕ0 ∧ 𝐵
∈ ℕ0)) ∧ 𝐴 = +∞) → 𝐵 ∈
ℕ0*) |
| 7 | | simprr 773 |
. . . . . . . . 9
⊢ (((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐵 ≠ 0) |
| 8 | 7 | ad3antrrr 730 |
. . . . . . . 8
⊢
((((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ·e 𝐵) ∈ ℕ0)
∧ ¬ (𝐴 ∈
ℕ0 ∧ 𝐵
∈ ℕ0)) ∧ 𝐴 = +∞) → 𝐵 ≠ 0) |
| 9 | | xnn0gt0 32773 |
. . . . . . . 8
⊢ ((𝐵 ∈
ℕ0* ∧ 𝐵 ≠ 0) → 0 < 𝐵) |
| 10 | 6, 8, 9 | syl2anc 584 |
. . . . . . 7
⊢
((((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ·e 𝐵) ∈ ℕ0)
∧ ¬ (𝐴 ∈
ℕ0 ∧ 𝐵
∈ ℕ0)) ∧ 𝐴 = +∞) → 0 < 𝐵) |
| 11 | | xmulpnf2 13317 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 0 < 𝐵) →
(+∞ ·e 𝐵) = +∞) |
| 12 | 5, 10, 11 | syl2anc 584 |
. . . . . 6
⊢
((((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ·e 𝐵) ∈ ℕ0)
∧ ¬ (𝐴 ∈
ℕ0 ∧ 𝐵
∈ ℕ0)) ∧ 𝐴 = +∞) → (+∞
·e 𝐵) =
+∞) |
| 13 | | pnfnre2 11303 |
. . . . . . . 8
⊢ ¬
+∞ ∈ ℝ |
| 14 | | nn0re 12535 |
. . . . . . . 8
⊢ (+∞
∈ ℕ0 → +∞ ∈ ℝ) |
| 15 | 13, 14 | mto 197 |
. . . . . . 7
⊢ ¬
+∞ ∈ ℕ0 |
| 16 | 15 | a1i 11 |
. . . . . 6
⊢
((((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ·e 𝐵) ∈ ℕ0)
∧ ¬ (𝐴 ∈
ℕ0 ∧ 𝐵
∈ ℕ0)) ∧ 𝐴 = +∞) → ¬ +∞ ∈
ℕ0) |
| 17 | 12, 16 | eqneltrd 2861 |
. . . . 5
⊢
((((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ·e 𝐵) ∈ ℕ0)
∧ ¬ (𝐴 ∈
ℕ0 ∧ 𝐵
∈ ℕ0)) ∧ 𝐴 = +∞) → ¬ (+∞
·e 𝐵)
∈ ℕ0) |
| 18 | 3, 17 | eqneltrd 2861 |
. . . 4
⊢
((((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ·e 𝐵) ∈ ℕ0)
∧ ¬ (𝐴 ∈
ℕ0 ∧ 𝐵
∈ ℕ0)) ∧ 𝐴 = +∞) → ¬ (𝐴 ·e 𝐵) ∈
ℕ0) |
| 19 | | simpr 484 |
. . . . . 6
⊢
((((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ·e 𝐵) ∈ ℕ0)
∧ ¬ (𝐴 ∈
ℕ0 ∧ 𝐵
∈ ℕ0)) ∧ 𝐵 = +∞) → 𝐵 = +∞) |
| 20 | 19 | oveq2d 7447 |
. . . . 5
⊢
((((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ·e 𝐵) ∈ ℕ0)
∧ ¬ (𝐴 ∈
ℕ0 ∧ 𝐵
∈ ℕ0)) ∧ 𝐵 = +∞) → (𝐴 ·e 𝐵) = (𝐴 ·e
+∞)) |
| 21 | | xnn0xr 12604 |
. . . . . . . 8
⊢ (𝐴 ∈
ℕ0* → 𝐴 ∈
ℝ*) |
| 22 | 21 | ad5antr 734 |
. . . . . . 7
⊢
((((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ·e 𝐵) ∈ ℕ0)
∧ ¬ (𝐴 ∈
ℕ0 ∧ 𝐵
∈ ℕ0)) ∧ 𝐵 = +∞) → 𝐴 ∈
ℝ*) |
| 23 | | simp-5l 785 |
. . . . . . . 8
⊢
((((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ·e 𝐵) ∈ ℕ0)
∧ ¬ (𝐴 ∈
ℕ0 ∧ 𝐵
∈ ℕ0)) ∧ 𝐵 = +∞) → 𝐴 ∈
ℕ0*) |
| 24 | | simprl 771 |
. . . . . . . . 9
⊢ (((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → 𝐴 ≠ 0) |
| 25 | 24 | ad3antrrr 730 |
. . . . . . . 8
⊢
((((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ·e 𝐵) ∈ ℕ0)
∧ ¬ (𝐴 ∈
ℕ0 ∧ 𝐵
∈ ℕ0)) ∧ 𝐵 = +∞) → 𝐴 ≠ 0) |
| 26 | | xnn0gt0 32773 |
. . . . . . . 8
⊢ ((𝐴 ∈
ℕ0* ∧ 𝐴 ≠ 0) → 0 < 𝐴) |
| 27 | 23, 25, 26 | syl2anc 584 |
. . . . . . 7
⊢
((((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ·e 𝐵) ∈ ℕ0)
∧ ¬ (𝐴 ∈
ℕ0 ∧ 𝐵
∈ ℕ0)) ∧ 𝐵 = +∞) → 0 < 𝐴) |
| 28 | | xmulpnf1 13316 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 0 < 𝐴) →
(𝐴 ·e
+∞) = +∞) |
| 29 | 22, 27, 28 | syl2anc 584 |
. . . . . 6
⊢
((((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ·e 𝐵) ∈ ℕ0)
∧ ¬ (𝐴 ∈
ℕ0 ∧ 𝐵
∈ ℕ0)) ∧ 𝐵 = +∞) → (𝐴 ·e +∞) =
+∞) |
| 30 | 15 | a1i 11 |
. . . . . 6
⊢
((((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ·e 𝐵) ∈ ℕ0)
∧ ¬ (𝐴 ∈
ℕ0 ∧ 𝐵
∈ ℕ0)) ∧ 𝐵 = +∞) → ¬ +∞ ∈
ℕ0) |
| 31 | 29, 30 | eqneltrd 2861 |
. . . . 5
⊢
((((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ·e 𝐵) ∈ ℕ0)
∧ ¬ (𝐴 ∈
ℕ0 ∧ 𝐵
∈ ℕ0)) ∧ 𝐵 = +∞) → ¬ (𝐴 ·e +∞) ∈
ℕ0) |
| 32 | 20, 31 | eqneltrd 2861 |
. . . 4
⊢
((((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ·e 𝐵) ∈ ℕ0)
∧ ¬ (𝐴 ∈
ℕ0 ∧ 𝐵
∈ ℕ0)) ∧ 𝐵 = +∞) → ¬ (𝐴 ·e 𝐵) ∈
ℕ0) |
| 33 | | xnn0nnn0pnf 12612 |
. . . . . . . 8
⊢ ((𝐴 ∈
ℕ0* ∧ ¬ 𝐴 ∈ ℕ0) → 𝐴 = +∞) |
| 34 | 33 | ad5ant15 759 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ·e 𝐵) ∈ ℕ0)
∧ ¬ 𝐴 ∈
ℕ0) → 𝐴 = +∞) |
| 35 | 34 | ex 412 |
. . . . . 6
⊢ ((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ·e 𝐵) ∈ ℕ0)
→ (¬ 𝐴 ∈
ℕ0 → 𝐴 = +∞)) |
| 36 | | xnn0nnn0pnf 12612 |
. . . . . . . 8
⊢ ((𝐵 ∈
ℕ0* ∧ ¬ 𝐵 ∈ ℕ0) → 𝐵 = +∞) |
| 37 | 36 | ad5ant25 762 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ·e 𝐵) ∈ ℕ0)
∧ ¬ 𝐵 ∈
ℕ0) → 𝐵 = +∞) |
| 38 | 37 | ex 412 |
. . . . . 6
⊢ ((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ·e 𝐵) ∈ ℕ0)
→ (¬ 𝐵 ∈
ℕ0 → 𝐵 = +∞)) |
| 39 | 35, 38 | orim12d 967 |
. . . . 5
⊢ ((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ·e 𝐵) ∈ ℕ0)
→ ((¬ 𝐴 ∈
ℕ0 ∨ ¬ 𝐵 ∈ ℕ0) → (𝐴 = +∞ ∨ 𝐵 = +∞))) |
| 40 | | pm3.13 997 |
. . . . 5
⊢ (¬
(𝐴 ∈
ℕ0 ∧ 𝐵
∈ ℕ0) → (¬ 𝐴 ∈ ℕ0 ∨ ¬ 𝐵 ∈
ℕ0)) |
| 41 | 39, 40 | impel 505 |
. . . 4
⊢
(((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ·e 𝐵) ∈ ℕ0)
∧ ¬ (𝐴 ∈
ℕ0 ∧ 𝐵
∈ ℕ0)) → (𝐴 = +∞ ∨ 𝐵 = +∞)) |
| 42 | 18, 32, 41 | mpjaodan 961 |
. . 3
⊢
(((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ·e 𝐵) ∈ ℕ0)
∧ ¬ (𝐴 ∈
ℕ0 ∧ 𝐵
∈ ℕ0)) → ¬ (𝐴 ·e 𝐵) ∈
ℕ0) |
| 43 | 1, 42 | condan 818 |
. 2
⊢ ((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ·e 𝐵) ∈ ℕ0)
→ (𝐴 ∈
ℕ0 ∧ 𝐵
∈ ℕ0)) |
| 44 | | nn0re 12535 |
. . . . 5
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℝ) |
| 45 | 44 | ad2antrl 728 |
. . . 4
⊢ ((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ∈ ℕ0
∧ 𝐵 ∈
ℕ0)) → 𝐴 ∈ ℝ) |
| 46 | | nn0re 12535 |
. . . . 5
⊢ (𝐵 ∈ ℕ0
→ 𝐵 ∈
ℝ) |
| 47 | 46 | ad2antll 729 |
. . . 4
⊢ ((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ∈ ℕ0
∧ 𝐵 ∈
ℕ0)) → 𝐵 ∈ ℝ) |
| 48 | | rexmul 13313 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ·e 𝐵) = (𝐴 · 𝐵)) |
| 49 | 45, 47, 48 | syl2anc 584 |
. . 3
⊢ ((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ∈ ℕ0
∧ 𝐵 ∈
ℕ0)) → (𝐴 ·e 𝐵) = (𝐴 · 𝐵)) |
| 50 | | nn0mulcl 12562 |
. . . 4
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈
ℕ0) → (𝐴 · 𝐵) ∈
ℕ0) |
| 51 | 50 | adantl 481 |
. . 3
⊢ ((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ∈ ℕ0
∧ 𝐵 ∈
ℕ0)) → (𝐴 · 𝐵) ∈
ℕ0) |
| 52 | 49, 51 | eqeltrd 2841 |
. 2
⊢ ((((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) ∧ (𝐴 ∈ ℕ0
∧ 𝐵 ∈
ℕ0)) → (𝐴 ·e 𝐵) ∈
ℕ0) |
| 53 | 43, 52 | impbida 801 |
1
⊢ (((𝐴 ∈
ℕ0* ∧ 𝐵 ∈ ℕ0*)
∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴 ·e 𝐵) ∈ ℕ0
↔ (𝐴 ∈
ℕ0 ∧ 𝐵
∈ ℕ0))) |