Step | Hyp | Ref
| Expression |
1 | | zmulscld.1 |
. . 3
⊢ (𝜑 → 𝐴 ∈
ℤs) |
2 | | elzs 28379 |
. . 3
⊢ (𝐴 ∈ ℤs
↔ ∃𝑥 ∈
ℕs ∃𝑦 ∈ ℕs 𝐴 = (𝑥 -s 𝑦)) |
3 | 1, 2 | sylib 218 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ ℕs ∃𝑦 ∈ ℕs
𝐴 = (𝑥 -s 𝑦)) |
4 | | zmulscld.2 |
. . 3
⊢ (𝜑 → 𝐵 ∈
ℤs) |
5 | | elzs 28379 |
. . 3
⊢ (𝐵 ∈ ℤs
↔ ∃𝑧 ∈
ℕs ∃𝑤 ∈ ℕs 𝐵 = (𝑧 -s 𝑤)) |
6 | 4, 5 | sylib 218 |
. 2
⊢ (𝜑 → ∃𝑧 ∈ ℕs ∃𝑤 ∈ ℕs
𝐵 = (𝑧 -s 𝑤)) |
7 | | reeanv 3230 |
. . . . 5
⊢
(∃𝑦 ∈
ℕs ∃𝑤 ∈ ℕs (𝐴 = (𝑥 -s 𝑦) ∧ 𝐵 = (𝑧 -s 𝑤)) ↔ (∃𝑦 ∈ ℕs 𝐴 = (𝑥 -s 𝑦) ∧ ∃𝑤 ∈ ℕs 𝐵 = (𝑧 -s 𝑤))) |
8 | 7 | 2rexbii 3131 |
. . . 4
⊢
(∃𝑥 ∈
ℕs ∃𝑧 ∈ ℕs ∃𝑦 ∈ ℕs
∃𝑤 ∈
ℕs (𝐴 =
(𝑥 -s 𝑦) ∧ 𝐵 = (𝑧 -s 𝑤)) ↔ ∃𝑥 ∈ ℕs ∃𝑧 ∈ ℕs
(∃𝑦 ∈
ℕs 𝐴 =
(𝑥 -s 𝑦) ∧ ∃𝑤 ∈ ℕs
𝐵 = (𝑧 -s 𝑤))) |
9 | | reeanv 3230 |
. . . 4
⊢
(∃𝑥 ∈
ℕs ∃𝑧 ∈ ℕs (∃𝑦 ∈ ℕs
𝐴 = (𝑥 -s 𝑦) ∧ ∃𝑤 ∈ ℕs 𝐵 = (𝑧 -s 𝑤)) ↔ (∃𝑥 ∈ ℕs ∃𝑦 ∈ ℕs
𝐴 = (𝑥 -s 𝑦) ∧ ∃𝑧 ∈ ℕs ∃𝑤 ∈ ℕs
𝐵 = (𝑧 -s 𝑤))) |
10 | 8, 9 | bitri 275 |
. . 3
⊢
(∃𝑥 ∈
ℕs ∃𝑧 ∈ ℕs ∃𝑦 ∈ ℕs
∃𝑤 ∈
ℕs (𝐴 =
(𝑥 -s 𝑦) ∧ 𝐵 = (𝑧 -s 𝑤)) ↔ (∃𝑥 ∈ ℕs ∃𝑦 ∈ ℕs
𝐴 = (𝑥 -s 𝑦) ∧ ∃𝑧 ∈ ℕs ∃𝑤 ∈ ℕs
𝐵 = (𝑧 -s 𝑤))) |
11 | | nnsno 28338 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℕs
→ 𝑥 ∈ No ) |
12 | 11 | ad2antrr 725 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs))
→ 𝑥 ∈ No ) |
13 | | nnsno 28338 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕs
→ 𝑦 ∈ No ) |
14 | 13 | ad2antrl 727 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs))
→ 𝑦 ∈ No ) |
15 | 12, 14 | subscld 28102 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs))
→ (𝑥 -s
𝑦) ∈ No ) |
16 | | nnsno 28338 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℕs
→ 𝑧 ∈ No ) |
17 | 16 | ad2antlr 726 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs))
→ 𝑧 ∈ No ) |
18 | | nnsno 28338 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ℕs
→ 𝑤 ∈ No ) |
19 | 18 | ad2antll 728 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs))
→ 𝑤 ∈ No ) |
20 | 15, 17, 19 | subsdid 28193 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs))
→ ((𝑥 -s
𝑦) ·s
(𝑧 -s 𝑤)) = (((𝑥 -s 𝑦) ·s 𝑧) -s ((𝑥 -s 𝑦) ·s 𝑤))) |
21 | | nnmulscl 28359 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) → (𝑥 ·s 𝑧) ∈
ℕs) |
22 | 21 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs))
→ (𝑥
·s 𝑧)
∈ ℕs) |
23 | 22 | nnsnod 28340 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs))
→ (𝑥
·s 𝑧)
∈ No ) |
24 | | simprl 770 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs))
→ 𝑦 ∈
ℕs) |
25 | | simplr 768 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs))
→ 𝑧 ∈
ℕs) |
26 | | nnmulscl 28359 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕs
∧ 𝑧 ∈
ℕs) → (𝑦 ·s 𝑧) ∈
ℕs) |
27 | 24, 25, 26 | syl2anc 583 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs))
→ (𝑦
·s 𝑧)
∈ ℕs) |
28 | 27 | nnsnod 28340 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs))
→ (𝑦
·s 𝑧)
∈ No ) |
29 | 23, 28 | subscld 28102 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs))
→ ((𝑥
·s 𝑧)
-s (𝑦
·s 𝑧))
∈ No ) |
30 | | nnmulscl 28359 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℕs
∧ 𝑤 ∈
ℕs) → (𝑥 ·s 𝑤) ∈
ℕs) |
31 | 30 | ad2ant2rl 748 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs))
→ (𝑥
·s 𝑤)
∈ ℕs) |
32 | 31 | nnsnod 28340 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs))
→ (𝑥
·s 𝑤)
∈ No ) |
33 | | nnmulscl 28359 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕs
∧ 𝑤 ∈
ℕs) → (𝑦 ·s 𝑤) ∈
ℕs) |
34 | 33 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs))
→ (𝑦
·s 𝑤)
∈ ℕs) |
35 | 34 | nnsnod 28340 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs))
→ (𝑦
·s 𝑤)
∈ No ) |
36 | 29, 32, 35 | subsubs2d 28134 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs))
→ (((𝑥
·s 𝑧)
-s (𝑦
·s 𝑧))
-s ((𝑥
·s 𝑤)
-s (𝑦
·s 𝑤))) =
(((𝑥 ·s
𝑧) -s (𝑦 ·s 𝑧)) +s ((𝑦 ·s 𝑤) -s (𝑥 ·s 𝑤)))) |
37 | 12, 14, 17 | subsdird 28194 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs))
→ ((𝑥 -s
𝑦) ·s
𝑧) = ((𝑥 ·s 𝑧) -s (𝑦 ·s 𝑧))) |
38 | 12, 14, 19 | subsdird 28194 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs))
→ ((𝑥 -s
𝑦) ·s
𝑤) = ((𝑥 ·s 𝑤) -s (𝑦 ·s 𝑤))) |
39 | 37, 38 | oveq12d 7463 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs))
→ (((𝑥 -s
𝑦) ·s
𝑧) -s ((𝑥 -s 𝑦) ·s 𝑤)) = (((𝑥 ·s 𝑧) -s (𝑦 ·s 𝑧)) -s ((𝑥 ·s 𝑤) -s (𝑦 ·s 𝑤)))) |
40 | 23, 35, 28, 32 | addsubs4d 28139 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs))
→ (((𝑥
·s 𝑧)
+s (𝑦
·s 𝑤))
-s ((𝑦
·s 𝑧)
+s (𝑥
·s 𝑤))) =
(((𝑥 ·s
𝑧) -s (𝑦 ·s 𝑧)) +s ((𝑦 ·s 𝑤) -s (𝑥 ·s 𝑤)))) |
41 | 36, 39, 40 | 3eqtr4d 2784 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs))
→ (((𝑥 -s
𝑦) ·s
𝑧) -s ((𝑥 -s 𝑦) ·s 𝑤)) = (((𝑥 ·s 𝑧) +s (𝑦 ·s 𝑤)) -s ((𝑦 ·s 𝑧) +s (𝑥 ·s 𝑤)))) |
42 | 20, 41 | eqtrd 2774 |
. . . . . . 7
⊢ (((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs))
→ ((𝑥 -s
𝑦) ·s
(𝑧 -s 𝑤)) = (((𝑥 ·s 𝑧) +s (𝑦 ·s 𝑤)) -s ((𝑦 ·s 𝑧) +s (𝑥 ·s 𝑤)))) |
43 | | nnaddscl 28358 |
. . . . . . . . . 10
⊢ (((𝑥 ·s 𝑧) ∈ ℕs
∧ (𝑦
·s 𝑤)
∈ ℕs) → ((𝑥 ·s 𝑧) +s (𝑦 ·s 𝑤)) ∈
ℕs) |
44 | 22, 34, 43 | syl2anc 583 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs))
→ ((𝑥
·s 𝑧)
+s (𝑦
·s 𝑤))
∈ ℕs) |
45 | | nnaddscl 28358 |
. . . . . . . . . 10
⊢ (((𝑦 ·s 𝑧) ∈ ℕs
∧ (𝑥
·s 𝑤)
∈ ℕs) → ((𝑦 ·s 𝑧) +s (𝑥 ·s 𝑤)) ∈
ℕs) |
46 | 27, 31, 45 | syl2anc 583 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs))
→ ((𝑦
·s 𝑧)
+s (𝑥
·s 𝑤))
∈ ℕs) |
47 | | eqid 2734 |
. . . . . . . . . 10
⊢ (((𝑥 ·s 𝑧) +s (𝑦 ·s 𝑤)) -s ((𝑦 ·s 𝑧) +s (𝑥 ·s 𝑤))) = (((𝑥 ·s 𝑧) +s (𝑦 ·s 𝑤)) -s ((𝑦 ·s 𝑧) +s (𝑥 ·s 𝑤))) |
48 | | rspceov 7493 |
. . . . . . . . . 10
⊢ ((((𝑥 ·s 𝑧) +s (𝑦 ·s 𝑤)) ∈ ℕs
∧ ((𝑦
·s 𝑧)
+s (𝑥
·s 𝑤))
∈ ℕs ∧ (((𝑥 ·s 𝑧) +s (𝑦 ·s 𝑤)) -s ((𝑦 ·s 𝑧) +s (𝑥 ·s 𝑤))) = (((𝑥 ·s 𝑧) +s (𝑦 ·s 𝑤)) -s ((𝑦 ·s 𝑧) +s (𝑥 ·s 𝑤)))) → ∃𝑡 ∈ ℕs ∃𝑢 ∈ ℕs
(((𝑥 ·s
𝑧) +s (𝑦 ·s 𝑤)) -s ((𝑦 ·s 𝑧) +s (𝑥 ·s 𝑤))) = (𝑡 -s 𝑢)) |
49 | 47, 48 | mp3an3 1450 |
. . . . . . . . 9
⊢ ((((𝑥 ·s 𝑧) +s (𝑦 ·s 𝑤)) ∈ ℕs
∧ ((𝑦
·s 𝑧)
+s (𝑥
·s 𝑤))
∈ ℕs) → ∃𝑡 ∈ ℕs ∃𝑢 ∈ ℕs
(((𝑥 ·s
𝑧) +s (𝑦 ·s 𝑤)) -s ((𝑦 ·s 𝑧) +s (𝑥 ·s 𝑤))) = (𝑡 -s 𝑢)) |
50 | 44, 46, 49 | syl2anc 583 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs))
→ ∃𝑡 ∈
ℕs ∃𝑢 ∈ ℕs (((𝑥 ·s 𝑧) +s (𝑦 ·s 𝑤)) -s ((𝑦 ·s 𝑧) +s (𝑥 ·s 𝑤))) = (𝑡 -s 𝑢)) |
51 | | elzs 28379 |
. . . . . . . 8
⊢ ((((𝑥 ·s 𝑧) +s (𝑦 ·s 𝑤)) -s ((𝑦 ·s 𝑧) +s (𝑥 ·s 𝑤))) ∈ ℤs
↔ ∃𝑡 ∈
ℕs ∃𝑢 ∈ ℕs (((𝑥 ·s 𝑧) +s (𝑦 ·s 𝑤)) -s ((𝑦 ·s 𝑧) +s (𝑥 ·s 𝑤))) = (𝑡 -s 𝑢)) |
52 | 50, 51 | sylibr 234 |
. . . . . . 7
⊢ (((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs))
→ (((𝑥
·s 𝑧)
+s (𝑦
·s 𝑤))
-s ((𝑦
·s 𝑧)
+s (𝑥
·s 𝑤)))
∈ ℤs) |
53 | 42, 52 | eqeltrd 2838 |
. . . . . 6
⊢ (((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs))
→ ((𝑥 -s
𝑦) ·s
(𝑧 -s 𝑤)) ∈
ℤs) |
54 | | oveq12 7454 |
. . . . . . 7
⊢ ((𝐴 = (𝑥 -s 𝑦) ∧ 𝐵 = (𝑧 -s 𝑤)) → (𝐴 ·s 𝐵) = ((𝑥 -s 𝑦) ·s (𝑧 -s 𝑤))) |
55 | 54 | eleq1d 2823 |
. . . . . 6
⊢ ((𝐴 = (𝑥 -s 𝑦) ∧ 𝐵 = (𝑧 -s 𝑤)) → ((𝐴 ·s 𝐵) ∈ ℤs ↔ ((𝑥 -s 𝑦) ·s (𝑧 -s 𝑤)) ∈
ℤs)) |
56 | 53, 55 | syl5ibrcom 247 |
. . . . 5
⊢ (((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) ∧ (𝑦 ∈ ℕs ∧ 𝑤 ∈ ℕs))
→ ((𝐴 = (𝑥 -s 𝑦) ∧ 𝐵 = (𝑧 -s 𝑤)) → (𝐴 ·s 𝐵) ∈
ℤs)) |
57 | 56 | rexlimdvva 3215 |
. . . 4
⊢ ((𝑥 ∈ ℕs
∧ 𝑧 ∈
ℕs) → (∃𝑦 ∈ ℕs ∃𝑤 ∈ ℕs
(𝐴 = (𝑥 -s 𝑦) ∧ 𝐵 = (𝑧 -s 𝑤)) → (𝐴 ·s 𝐵) ∈
ℤs)) |
58 | 57 | rexlimivv 3203 |
. . 3
⊢
(∃𝑥 ∈
ℕs ∃𝑧 ∈ ℕs ∃𝑦 ∈ ℕs
∃𝑤 ∈
ℕs (𝐴 =
(𝑥 -s 𝑦) ∧ 𝐵 = (𝑧 -s 𝑤)) → (𝐴 ·s 𝐵) ∈
ℤs) |
59 | 10, 58 | sylbir 235 |
. 2
⊢
((∃𝑥 ∈
ℕs ∃𝑦 ∈ ℕs 𝐴 = (𝑥 -s 𝑦) ∧ ∃𝑧 ∈ ℕs ∃𝑤 ∈ ℕs
𝐵 = (𝑧 -s 𝑤)) → (𝐴 ·s 𝐵) ∈
ℤs) |
60 | 3, 6, 59 | syl2anc 583 |
1
⊢ (𝜑 → (𝐴 ·s 𝐵) ∈
ℤs) |