Step | Hyp | Ref
| Expression |
1 | | elzs 28379 |
. 2
⊢ (𝑁 ∈ ℤs
↔ ∃𝑦 ∈
ℕs ∃𝑧 ∈ ℕs 𝑁 = (𝑦 -s 𝑧)) |
2 | | nnn0s 28341 |
. . . . . 6
⊢ (𝑦 ∈ ℕs
→ 𝑦 ∈
ℕ0s) |
3 | | n0seo 28414 |
. . . . . 6
⊢ (𝑦 ∈ ℕ0s
→ (∃𝑤 ∈
ℕ0s 𝑦 =
(2s ·s 𝑤) ∨ ∃𝑤 ∈ ℕ0s 𝑦 = ((2s
·s 𝑤)
+s 1s ))) |
4 | 2, 3 | syl 17 |
. . . . 5
⊢ (𝑦 ∈ ℕs
→ (∃𝑤 ∈
ℕ0s 𝑦 =
(2s ·s 𝑤) ∨ ∃𝑤 ∈ ℕ0s 𝑦 = ((2s
·s 𝑤)
+s 1s ))) |
5 | | nnn0s 28341 |
. . . . . 6
⊢ (𝑧 ∈ ℕs
→ 𝑧 ∈
ℕ0s) |
6 | | n0seo 28414 |
. . . . . 6
⊢ (𝑧 ∈ ℕ0s
→ (∃𝑡 ∈
ℕ0s 𝑧 =
(2s ·s 𝑡) ∨ ∃𝑡 ∈ ℕ0s 𝑧 = ((2s
·s 𝑡)
+s 1s ))) |
7 | 5, 6 | syl 17 |
. . . . 5
⊢ (𝑧 ∈ ℕs
→ (∃𝑡 ∈
ℕ0s 𝑧 =
(2s ·s 𝑡) ∨ ∃𝑡 ∈ ℕ0s 𝑧 = ((2s
·s 𝑡)
+s 1s ))) |
8 | | reeanv 3230 |
. . . . . . . 8
⊢
(∃𝑤 ∈
ℕ0s ∃𝑡 ∈ ℕ0s (𝑦 = (2s
·s 𝑤)
∧ 𝑧 = (2s
·s 𝑡))
↔ (∃𝑤 ∈
ℕ0s 𝑦 =
(2s ·s 𝑤) ∧ ∃𝑡 ∈ ℕ0s 𝑧 = (2s
·s 𝑡))) |
9 | | n0zs 28384 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ ℕ0s
→ 𝑤 ∈
ℤs) |
10 | 9 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → 𝑤 ∈ ℤs) |
11 | | n0zs 28384 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ ℕ0s
→ 𝑡 ∈
ℤs) |
12 | 11 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → 𝑡 ∈ ℤs) |
13 | 10, 12 | zsubscld 28391 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → (𝑤 -s 𝑡) ∈
ℤs) |
14 | | 2sno 28412 |
. . . . . . . . . . . . . 14
⊢
2s ∈ No |
15 | 14 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → 2s ∈ No
) |
16 | | n0sno 28337 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ℕ0s
→ 𝑤 ∈ No ) |
17 | 16 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → 𝑤 ∈ No
) |
18 | | n0sno 28337 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∈ ℕ0s
→ 𝑡 ∈ No ) |
19 | 18 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → 𝑡 ∈ No
) |
20 | 15, 17, 19 | subsdid 28193 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → (2s ·s (𝑤 -s 𝑡)) = ((2s
·s 𝑤)
-s (2s ·s 𝑡))) |
21 | 20 | eqcomd 2740 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → ((2s ·s 𝑤) -s (2s
·s 𝑡)) =
(2s ·s (𝑤 -s 𝑡))) |
22 | | oveq2 7453 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑤 -s 𝑡) → (2s ·s
𝑥) = (2s
·s (𝑤
-s 𝑡))) |
23 | 22 | rspceeqv 3653 |
. . . . . . . . . . 11
⊢ (((𝑤 -s 𝑡) ∈ ℤs
∧ ((2s ·s 𝑤) -s (2s
·s 𝑡)) =
(2s ·s (𝑤 -s 𝑡))) → ∃𝑥 ∈ ℤs ((2s
·s 𝑤)
-s (2s ·s 𝑡)) = (2s ·s
𝑥)) |
24 | 13, 21, 23 | syl2anc 583 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → ∃𝑥 ∈ ℤs ((2s
·s 𝑤)
-s (2s ·s 𝑡)) = (2s ·s
𝑥)) |
25 | | oveq12 7454 |
. . . . . . . . . . . 12
⊢ ((𝑦 = (2s
·s 𝑤)
∧ 𝑧 = (2s
·s 𝑡))
→ (𝑦 -s
𝑧) = ((2s
·s 𝑤)
-s (2s ·s 𝑡))) |
26 | 25 | eqeq1d 2736 |
. . . . . . . . . . 11
⊢ ((𝑦 = (2s
·s 𝑤)
∧ 𝑧 = (2s
·s 𝑡))
→ ((𝑦 -s
𝑧) = (2s
·s 𝑥)
↔ ((2s ·s 𝑤) -s (2s
·s 𝑡)) =
(2s ·s 𝑥))) |
27 | 26 | rexbidv 3181 |
. . . . . . . . . 10
⊢ ((𝑦 = (2s
·s 𝑤)
∧ 𝑧 = (2s
·s 𝑡))
→ (∃𝑥 ∈
ℤs (𝑦
-s 𝑧) =
(2s ·s 𝑥) ↔ ∃𝑥 ∈ ℤs ((2s
·s 𝑤)
-s (2s ·s 𝑡)) = (2s ·s
𝑥))) |
28 | 24, 27 | syl5ibrcom 247 |
. . . . . . . . 9
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → ((𝑦 = (2s ·s 𝑤) ∧ 𝑧 = (2s ·s 𝑡)) → ∃𝑥 ∈ ℤs
(𝑦 -s 𝑧) = (2s
·s 𝑥))) |
29 | 28 | rexlimivv 3203 |
. . . . . . . 8
⊢
(∃𝑤 ∈
ℕ0s ∃𝑡 ∈ ℕ0s (𝑦 = (2s
·s 𝑤)
∧ 𝑧 = (2s
·s 𝑡))
→ ∃𝑥 ∈
ℤs (𝑦
-s 𝑧) =
(2s ·s 𝑥)) |
30 | 8, 29 | sylbir 235 |
. . . . . . 7
⊢
((∃𝑤 ∈
ℕ0s 𝑦 =
(2s ·s 𝑤) ∧ ∃𝑡 ∈ ℕ0s 𝑧 = (2s
·s 𝑡))
→ ∃𝑥 ∈
ℤs (𝑦
-s 𝑧) =
(2s ·s 𝑥)) |
31 | 30 | orcd 872 |
. . . . . 6
⊢
((∃𝑤 ∈
ℕ0s 𝑦 =
(2s ·s 𝑤) ∧ ∃𝑡 ∈ ℕ0s 𝑧 = (2s
·s 𝑡))
→ (∃𝑥 ∈
ℤs (𝑦
-s 𝑧) =
(2s ·s 𝑥) ∨ ∃𝑥 ∈ ℤs (𝑦 -s 𝑧) = ((2s
·s 𝑥)
+s 1s ))) |
32 | | reeanv 3230 |
. . . . . . . 8
⊢
(∃𝑤 ∈
ℕ0s ∃𝑡 ∈ ℕ0s (𝑦 = ((2s
·s 𝑤)
+s 1s ) ∧ 𝑧 = (2s ·s 𝑡)) ↔ (∃𝑤 ∈ ℕ0s
𝑦 = ((2s
·s 𝑤)
+s 1s ) ∧ ∃𝑡 ∈ ℕ0s 𝑧 = (2s
·s 𝑡))) |
33 | 15, 17 | mulscld 28170 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → (2s ·s 𝑤) ∈
No ) |
34 | | 1sno 27881 |
. . . . . . . . . . . . . 14
⊢
1s ∈ No |
35 | 34 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → 1s ∈ No
) |
36 | 15, 19 | mulscld 28170 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → (2s ·s 𝑡) ∈
No ) |
37 | 33, 35, 36 | addsubsd 28121 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → (((2s ·s 𝑤) +s 1s )
-s (2s ·s 𝑡)) = (((2s ·s
𝑤) -s
(2s ·s 𝑡)) +s 1s
)) |
38 | 21 | oveq1d 7460 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → (((2s ·s 𝑤) -s (2s
·s 𝑡))
+s 1s ) = ((2s ·s (𝑤 -s 𝑡)) +s 1s
)) |
39 | 37, 38 | eqtrd 2774 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → (((2s ·s 𝑤) +s 1s )
-s (2s ·s 𝑡)) = ((2s ·s
(𝑤 -s 𝑡)) +s 1s
)) |
40 | 22 | oveq1d 7460 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑤 -s 𝑡) → ((2s ·s
𝑥) +s
1s ) = ((2s ·s (𝑤 -s 𝑡)) +s 1s
)) |
41 | 40 | rspceeqv 3653 |
. . . . . . . . . . 11
⊢ (((𝑤 -s 𝑡) ∈ ℤs
∧ (((2s ·s 𝑤) +s 1s ) -s
(2s ·s 𝑡)) = ((2s ·s
(𝑤 -s 𝑡)) +s 1s
)) → ∃𝑥 ∈
ℤs (((2s ·s 𝑤) +s 1s ) -s
(2s ·s 𝑡)) = ((2s ·s
𝑥) +s
1s )) |
42 | 13, 39, 41 | syl2anc 583 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → ∃𝑥 ∈ ℤs (((2s
·s 𝑤)
+s 1s ) -s (2s ·s
𝑡)) = ((2s
·s 𝑥)
+s 1s )) |
43 | | oveq12 7454 |
. . . . . . . . . . . 12
⊢ ((𝑦 = ((2s
·s 𝑤)
+s 1s ) ∧ 𝑧 = (2s ·s 𝑡)) → (𝑦 -s 𝑧) = (((2s ·s
𝑤) +s
1s ) -s (2s ·s 𝑡))) |
44 | 43 | eqeq1d 2736 |
. . . . . . . . . . 11
⊢ ((𝑦 = ((2s
·s 𝑤)
+s 1s ) ∧ 𝑧 = (2s ·s 𝑡)) → ((𝑦 -s 𝑧) = ((2s ·s
𝑥) +s
1s ) ↔ (((2s ·s 𝑤) +s 1s ) -s
(2s ·s 𝑡)) = ((2s ·s
𝑥) +s
1s ))) |
45 | 44 | rexbidv 3181 |
. . . . . . . . . 10
⊢ ((𝑦 = ((2s
·s 𝑤)
+s 1s ) ∧ 𝑧 = (2s ·s 𝑡)) → (∃𝑥 ∈ ℤs
(𝑦 -s 𝑧) = ((2s
·s 𝑥)
+s 1s ) ↔ ∃𝑥 ∈ ℤs (((2s
·s 𝑤)
+s 1s ) -s (2s ·s
𝑡)) = ((2s
·s 𝑥)
+s 1s ))) |
46 | 42, 45 | syl5ibrcom 247 |
. . . . . . . . 9
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → ((𝑦 = ((2s ·s 𝑤) +s 1s )
∧ 𝑧 = (2s
·s 𝑡))
→ ∃𝑥 ∈
ℤs (𝑦
-s 𝑧) =
((2s ·s 𝑥) +s 1s
))) |
47 | 46 | rexlimivv 3203 |
. . . . . . . 8
⊢
(∃𝑤 ∈
ℕ0s ∃𝑡 ∈ ℕ0s (𝑦 = ((2s
·s 𝑤)
+s 1s ) ∧ 𝑧 = (2s ·s 𝑡)) → ∃𝑥 ∈ ℤs
(𝑦 -s 𝑧) = ((2s
·s 𝑥)
+s 1s )) |
48 | 32, 47 | sylbir 235 |
. . . . . . 7
⊢
((∃𝑤 ∈
ℕ0s 𝑦 =
((2s ·s 𝑤) +s 1s ) ∧
∃𝑡 ∈
ℕ0s 𝑧 =
(2s ·s 𝑡)) → ∃𝑥 ∈ ℤs (𝑦 -s 𝑧) = ((2s
·s 𝑥)
+s 1s )) |
49 | 48 | olcd 873 |
. . . . . 6
⊢
((∃𝑤 ∈
ℕ0s 𝑦 =
((2s ·s 𝑤) +s 1s ) ∧
∃𝑡 ∈
ℕ0s 𝑧 =
(2s ·s 𝑡)) → (∃𝑥 ∈ ℤs (𝑦 -s 𝑧) = (2s
·s 𝑥)
∨ ∃𝑥 ∈
ℤs (𝑦
-s 𝑧) =
((2s ·s 𝑥) +s 1s
))) |
50 | | reeanv 3230 |
. . . . . . . 8
⊢
(∃𝑤 ∈
ℕ0s ∃𝑡 ∈ ℕ0s (𝑦 = (2s
·s 𝑤)
∧ 𝑧 = ((2s
·s 𝑡)
+s 1s )) ↔ (∃𝑤 ∈ ℕ0s 𝑦 = (2s
·s 𝑤)
∧ ∃𝑡 ∈
ℕ0s 𝑧 =
((2s ·s 𝑡) +s 1s
))) |
51 | | 1zs 28386 |
. . . . . . . . . . . . 13
⊢
1s ∈ ℤs |
52 | 51 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → 1s ∈
ℤs) |
53 | 13, 52 | zsubscld 28391 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → ((𝑤 -s 𝑡) -s 1s ) ∈
ℤs) |
54 | 13 | znod 28378 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → (𝑤 -s 𝑡) ∈ No
) |
55 | 15, 54, 35 | subsdid 28193 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → (2s ·s ((𝑤 -s 𝑡) -s 1s ))
= ((2s ·s (𝑤 -s 𝑡)) -s (2s
·s 1s ))) |
56 | 55 | oveq1d 7460 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → ((2s ·s ((𝑤 -s 𝑡) -s 1s ))
+s 1s ) = (((2s ·s (𝑤 -s 𝑡)) -s (2s
·s 1s )) +s 1s
)) |
57 | | mulsrid 28148 |
. . . . . . . . . . . . . . . . 17
⊢
(2s ∈ No →
(2s ·s 1s ) =
2s) |
58 | 14, 57 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(2s ·s 1s ) =
2s |
59 | 58 | oveq2i 7456 |
. . . . . . . . . . . . . . 15
⊢
((2s ·s (𝑤 -s 𝑡)) -s (2s
·s 1s )) = ((2s ·s
(𝑤 -s 𝑡)) -s
2s) |
60 | 59 | oveq1i 7455 |
. . . . . . . . . . . . . 14
⊢
(((2s ·s (𝑤 -s 𝑡)) -s (2s
·s 1s )) +s 1s ) =
(((2s ·s (𝑤 -s 𝑡)) -s 2s) +s
1s ) |
61 | 15, 54 | mulscld 28170 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → (2s ·s (𝑤 -s 𝑡)) ∈
No ) |
62 | 61, 35, 15 | addsubsd 28121 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → (((2s ·s (𝑤 -s 𝑡)) +s 1s )
-s 2s) = (((2s ·s (𝑤 -s 𝑡)) -s 2s)
+s 1s )) |
63 | 61, 35, 15 | addsubsassd 28120 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → (((2s ·s (𝑤 -s 𝑡)) +s 1s )
-s 2s) = ((2s ·s (𝑤 -s 𝑡)) +s ( 1s
-s 2s))) |
64 | 62, 63 | eqtr3d 2776 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → (((2s ·s (𝑤 -s 𝑡)) -s 2s)
+s 1s ) = ((2s ·s (𝑤 -s 𝑡)) +s ( 1s
-s 2s))) |
65 | 60, 64 | eqtrid 2786 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → (((2s ·s (𝑤 -s 𝑡)) -s (2s
·s 1s )) +s 1s ) =
((2s ·s (𝑤 -s 𝑡)) +s ( 1s
-s 2s))) |
66 | 56, 65 | eqtrd 2774 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → ((2s ·s ((𝑤 -s 𝑡) -s 1s ))
+s 1s ) = ((2s ·s (𝑤 -s 𝑡)) +s ( 1s
-s 2s))) |
67 | | subscl 28101 |
. . . . . . . . . . . . . . . . . 18
⊢ ((
1s ∈ No ∧ 2s
∈ No ) → ( 1s -s
2s) ∈ No ) |
68 | 34, 14, 67 | mp2an 691 |
. . . . . . . . . . . . . . . . 17
⊢ (
1s -s 2s) ∈ No
|
69 | | negnegs 28085 |
. . . . . . . . . . . . . . . . 17
⊢ ((
1s -s 2s) ∈ No
→ ( -us ‘( -us ‘( 1s
-s 2s))) = ( 1s -s
2s)) |
70 | 68, 69 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (
-us ‘( -us ‘( 1s -s
2s))) = ( 1s -s
2s) |
71 | 34 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (⊤
→ 1s ∈ No ) |
72 | 14 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (⊤
→ 2s ∈ No ) |
73 | 71, 72 | negsubsdi2d 28119 |
. . . . . . . . . . . . . . . . . . 19
⊢ (⊤
→ ( -us ‘( 1s -s 2s)) =
(2s -s 1s )) |
74 | 73 | mptru 1544 |
. . . . . . . . . . . . . . . . . 18
⊢ (
-us ‘( 1s -s 2s)) =
(2s -s 1s ) |
75 | | 1p1e2s 28409 |
. . . . . . . . . . . . . . . . . . 19
⊢ (
1s +s 1s ) = 2s |
76 | | subadds 28109 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((2s ∈ No ∧
1s ∈ No ∧ 1s
∈ No ) → ((2s -s
1s ) = 1s ↔ ( 1s +s
1s ) = 2s)) |
77 | 14, 34, 34, 76 | mp3an 1461 |
. . . . . . . . . . . . . . . . . . 19
⊢
((2s -s 1s ) = 1s ↔ (
1s +s 1s ) = 2s) |
78 | 75, 77 | mpbir 231 |
. . . . . . . . . . . . . . . . . 18
⊢
(2s -s 1s ) =
1s |
79 | 74, 78 | eqtri 2762 |
. . . . . . . . . . . . . . . . 17
⊢ (
-us ‘( 1s -s 2s)) =
1s |
80 | 79 | fveq2i 6922 |
. . . . . . . . . . . . . . . 16
⊢ (
-us ‘( -us ‘( 1s -s
2s))) = ( -us ‘ 1s ) |
81 | 70, 80 | eqtr3i 2764 |
. . . . . . . . . . . . . . 15
⊢ (
1s -s 2s) = ( -us ‘
1s ) |
82 | 81 | oveq2i 7456 |
. . . . . . . . . . . . . 14
⊢
((2s ·s (𝑤 -s 𝑡)) +s ( 1s
-s 2s)) = ((2s ·s (𝑤 -s 𝑡)) +s (
-us ‘ 1s )) |
83 | 61, 35 | subsvald 28100 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → ((2s ·s (𝑤 -s 𝑡)) -s 1s )
= ((2s ·s (𝑤 -s 𝑡)) +s ( -us ‘
1s ))) |
84 | 82, 83 | eqtr4id 2793 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → ((2s ·s (𝑤 -s 𝑡)) +s ( 1s
-s 2s)) = ((2s ·s (𝑤 -s 𝑡)) -s 1s
)) |
85 | 20 | oveq1d 7460 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → ((2s ·s (𝑤 -s 𝑡)) -s 1s )
= (((2s ·s 𝑤) -s (2s
·s 𝑡))
-s 1s )) |
86 | 84, 85 | eqtrd 2774 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → ((2s ·s (𝑤 -s 𝑡)) +s ( 1s
-s 2s)) = (((2s ·s 𝑤) -s (2s
·s 𝑡))
-s 1s )) |
87 | 33, 36, 35 | subsubs4d 28133 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → (((2s ·s 𝑤) -s (2s
·s 𝑡))
-s 1s ) = ((2s ·s 𝑤) -s ((2s
·s 𝑡)
+s 1s ))) |
88 | 66, 86, 87 | 3eqtrrd 2779 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → ((2s ·s 𝑤) -s ((2s
·s 𝑡)
+s 1s )) = ((2s ·s ((𝑤 -s 𝑡) -s 1s ))
+s 1s )) |
89 | | oveq2 7453 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ((𝑤 -s 𝑡) -s 1s ) →
(2s ·s 𝑥) = (2s ·s
((𝑤 -s 𝑡) -s 1s
))) |
90 | 89 | oveq1d 7460 |
. . . . . . . . . . . 12
⊢ (𝑥 = ((𝑤 -s 𝑡) -s 1s ) →
((2s ·s 𝑥) +s 1s ) =
((2s ·s ((𝑤 -s 𝑡) -s 1s ))
+s 1s )) |
91 | 90 | rspceeqv 3653 |
. . . . . . . . . . 11
⊢ ((((𝑤 -s 𝑡) -s 1s )
∈ ℤs ∧ ((2s ·s 𝑤) -s ((2s
·s 𝑡)
+s 1s )) = ((2s ·s ((𝑤 -s 𝑡) -s 1s ))
+s 1s )) → ∃𝑥 ∈ ℤs ((2s
·s 𝑤)
-s ((2s ·s 𝑡) +s 1s )) =
((2s ·s 𝑥) +s 1s
)) |
92 | 53, 88, 91 | syl2anc 583 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → ∃𝑥 ∈ ℤs ((2s
·s 𝑤)
-s ((2s ·s 𝑡) +s 1s )) =
((2s ·s 𝑥) +s 1s
)) |
93 | | oveq12 7454 |
. . . . . . . . . . . 12
⊢ ((𝑦 = (2s
·s 𝑤)
∧ 𝑧 = ((2s
·s 𝑡)
+s 1s )) → (𝑦 -s 𝑧) = ((2s ·s
𝑤) -s
((2s ·s 𝑡) +s 1s
))) |
94 | 93 | eqeq1d 2736 |
. . . . . . . . . . 11
⊢ ((𝑦 = (2s
·s 𝑤)
∧ 𝑧 = ((2s
·s 𝑡)
+s 1s )) → ((𝑦 -s 𝑧) = ((2s ·s
𝑥) +s
1s ) ↔ ((2s ·s 𝑤) -s ((2s
·s 𝑡)
+s 1s )) = ((2s ·s 𝑥) +s 1s
))) |
95 | 94 | rexbidv 3181 |
. . . . . . . . . 10
⊢ ((𝑦 = (2s
·s 𝑤)
∧ 𝑧 = ((2s
·s 𝑡)
+s 1s )) → (∃𝑥 ∈ ℤs (𝑦 -s 𝑧) = ((2s
·s 𝑥)
+s 1s ) ↔ ∃𝑥 ∈ ℤs ((2s
·s 𝑤)
-s ((2s ·s 𝑡) +s 1s )) =
((2s ·s 𝑥) +s 1s
))) |
96 | 92, 95 | syl5ibrcom 247 |
. . . . . . . . 9
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → ((𝑦 = (2s ·s 𝑤) ∧ 𝑧 = ((2s ·s 𝑡) +s 1s ))
→ ∃𝑥 ∈
ℤs (𝑦
-s 𝑧) =
((2s ·s 𝑥) +s 1s
))) |
97 | 96 | rexlimivv 3203 |
. . . . . . . 8
⊢
(∃𝑤 ∈
ℕ0s ∃𝑡 ∈ ℕ0s (𝑦 = (2s
·s 𝑤)
∧ 𝑧 = ((2s
·s 𝑡)
+s 1s )) → ∃𝑥 ∈ ℤs (𝑦 -s 𝑧) = ((2s
·s 𝑥)
+s 1s )) |
98 | 50, 97 | sylbir 235 |
. . . . . . 7
⊢
((∃𝑤 ∈
ℕ0s 𝑦 =
(2s ·s 𝑤) ∧ ∃𝑡 ∈ ℕ0s 𝑧 = ((2s
·s 𝑡)
+s 1s )) → ∃𝑥 ∈ ℤs (𝑦 -s 𝑧) = ((2s
·s 𝑥)
+s 1s )) |
99 | 98 | olcd 873 |
. . . . . 6
⊢
((∃𝑤 ∈
ℕ0s 𝑦 =
(2s ·s 𝑤) ∧ ∃𝑡 ∈ ℕ0s 𝑧 = ((2s
·s 𝑡)
+s 1s )) → (∃𝑥 ∈ ℤs (𝑦 -s 𝑧) = (2s
·s 𝑥)
∨ ∃𝑥 ∈
ℤs (𝑦
-s 𝑧) =
((2s ·s 𝑥) +s 1s
))) |
100 | | reeanv 3230 |
. . . . . . . 8
⊢
(∃𝑤 ∈
ℕ0s ∃𝑡 ∈ ℕ0s (𝑦 = ((2s
·s 𝑤)
+s 1s ) ∧ 𝑧 = ((2s ·s 𝑡) +s 1s ))
↔ (∃𝑤 ∈
ℕ0s 𝑦 =
((2s ·s 𝑤) +s 1s ) ∧
∃𝑡 ∈
ℕ0s 𝑧 =
((2s ·s 𝑡) +s 1s
))) |
101 | 33, 35, 36, 35 | addsubs4d 28139 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → (((2s ·s 𝑤) +s 1s )
-s ((2s ·s 𝑡) +s 1s )) =
(((2s ·s 𝑤) -s (2s
·s 𝑡))
+s ( 1s -s 1s ))) |
102 | | subsid 28108 |
. . . . . . . . . . . . . . 15
⊢ (
1s ∈ No → ( 1s
-s 1s ) = 0s ) |
103 | 34, 102 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (
1s -s 1s ) = 0s |
104 | 103 | oveq2i 7456 |
. . . . . . . . . . . . 13
⊢
(((2s ·s 𝑤) -s (2s
·s 𝑡))
+s ( 1s -s 1s )) = (((2s
·s 𝑤)
-s (2s ·s 𝑡)) +s 0s
) |
105 | 33, 36 | subscld 28102 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → ((2s ·s 𝑤) -s (2s
·s 𝑡))
∈ No ) |
106 | 105 | addsridd 28007 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → (((2s ·s 𝑤) -s (2s
·s 𝑡))
+s 0s ) = ((2s ·s 𝑤) -s (2s
·s 𝑡))) |
107 | 106, 21 | eqtrd 2774 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → (((2s ·s 𝑤) -s (2s
·s 𝑡))
+s 0s ) = (2s ·s (𝑤 -s 𝑡))) |
108 | 104, 107 | eqtrid 2786 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → (((2s ·s 𝑤) -s (2s
·s 𝑡))
+s ( 1s -s 1s )) = (2s
·s (𝑤
-s 𝑡))) |
109 | 101, 108 | eqtrd 2774 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → (((2s ·s 𝑤) +s 1s )
-s ((2s ·s 𝑡) +s 1s )) =
(2s ·s (𝑤 -s 𝑡))) |
110 | 22 | rspceeqv 3653 |
. . . . . . . . . . 11
⊢ (((𝑤 -s 𝑡) ∈ ℤs
∧ (((2s ·s 𝑤) +s 1s ) -s
((2s ·s 𝑡) +s 1s )) =
(2s ·s (𝑤 -s 𝑡))) → ∃𝑥 ∈ ℤs (((2s
·s 𝑤)
+s 1s ) -s ((2s
·s 𝑡)
+s 1s )) = (2s ·s 𝑥)) |
111 | 13, 109, 110 | syl2anc 583 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → ∃𝑥 ∈ ℤs (((2s
·s 𝑤)
+s 1s ) -s ((2s
·s 𝑡)
+s 1s )) = (2s ·s 𝑥)) |
112 | | oveq12 7454 |
. . . . . . . . . . . 12
⊢ ((𝑦 = ((2s
·s 𝑤)
+s 1s ) ∧ 𝑧 = ((2s ·s 𝑡) +s 1s ))
→ (𝑦 -s
𝑧) = (((2s
·s 𝑤)
+s 1s ) -s ((2s
·s 𝑡)
+s 1s ))) |
113 | 112 | eqeq1d 2736 |
. . . . . . . . . . 11
⊢ ((𝑦 = ((2s
·s 𝑤)
+s 1s ) ∧ 𝑧 = ((2s ·s 𝑡) +s 1s ))
→ ((𝑦 -s
𝑧) = (2s
·s 𝑥)
↔ (((2s ·s 𝑤) +s 1s ) -s
((2s ·s 𝑡) +s 1s )) =
(2s ·s 𝑥))) |
114 | 113 | rexbidv 3181 |
. . . . . . . . . 10
⊢ ((𝑦 = ((2s
·s 𝑤)
+s 1s ) ∧ 𝑧 = ((2s ·s 𝑡) +s 1s ))
→ (∃𝑥 ∈
ℤs (𝑦
-s 𝑧) =
(2s ·s 𝑥) ↔ ∃𝑥 ∈ ℤs (((2s
·s 𝑤)
+s 1s ) -s ((2s
·s 𝑡)
+s 1s )) = (2s ·s 𝑥))) |
115 | 111, 114 | syl5ibrcom 247 |
. . . . . . . . 9
⊢ ((𝑤 ∈ ℕ0s
∧ 𝑡 ∈
ℕ0s) → ((𝑦 = ((2s ·s 𝑤) +s 1s )
∧ 𝑧 = ((2s
·s 𝑡)
+s 1s )) → ∃𝑥 ∈ ℤs (𝑦 -s 𝑧) = (2s
·s 𝑥))) |
116 | 115 | rexlimivv 3203 |
. . . . . . . 8
⊢
(∃𝑤 ∈
ℕ0s ∃𝑡 ∈ ℕ0s (𝑦 = ((2s
·s 𝑤)
+s 1s ) ∧ 𝑧 = ((2s ·s 𝑡) +s 1s ))
→ ∃𝑥 ∈
ℤs (𝑦
-s 𝑧) =
(2s ·s 𝑥)) |
117 | 100, 116 | sylbir 235 |
. . . . . . 7
⊢
((∃𝑤 ∈
ℕ0s 𝑦 =
((2s ·s 𝑤) +s 1s ) ∧
∃𝑡 ∈
ℕ0s 𝑧 =
((2s ·s 𝑡) +s 1s )) →
∃𝑥 ∈
ℤs (𝑦
-s 𝑧) =
(2s ·s 𝑥)) |
118 | 117 | orcd 872 |
. . . . . 6
⊢
((∃𝑤 ∈
ℕ0s 𝑦 =
((2s ·s 𝑤) +s 1s ) ∧
∃𝑡 ∈
ℕ0s 𝑧 =
((2s ·s 𝑡) +s 1s )) →
(∃𝑥 ∈
ℤs (𝑦
-s 𝑧) =
(2s ·s 𝑥) ∨ ∃𝑥 ∈ ℤs (𝑦 -s 𝑧) = ((2s
·s 𝑥)
+s 1s ))) |
119 | 31, 49, 99, 118 | ccase 1038 |
. . . . 5
⊢
(((∃𝑤 ∈
ℕ0s 𝑦 =
(2s ·s 𝑤) ∨ ∃𝑤 ∈ ℕ0s 𝑦 = ((2s
·s 𝑤)
+s 1s )) ∧ (∃𝑡 ∈ ℕ0s 𝑧 = (2s
·s 𝑡)
∨ ∃𝑡 ∈
ℕ0s 𝑧 =
((2s ·s 𝑡) +s 1s ))) →
(∃𝑥 ∈
ℤs (𝑦
-s 𝑧) =
(2s ·s 𝑥) ∨ ∃𝑥 ∈ ℤs (𝑦 -s 𝑧) = ((2s
·s 𝑥)
+s 1s ))) |
120 | 4, 7, 119 | syl2an 595 |
. . . 4
⊢ ((𝑦 ∈ ℕs
∧ 𝑧 ∈
ℕs) → (∃𝑥 ∈ ℤs (𝑦 -s 𝑧) = (2s
·s 𝑥)
∨ ∃𝑥 ∈
ℤs (𝑦
-s 𝑧) =
((2s ·s 𝑥) +s 1s
))) |
121 | | eqeq1 2738 |
. . . . . 6
⊢ (𝑁 = (𝑦 -s 𝑧) → (𝑁 = (2s ·s 𝑥) ↔ (𝑦 -s 𝑧) = (2s ·s 𝑥))) |
122 | 121 | rexbidv 3181 |
. . . . 5
⊢ (𝑁 = (𝑦 -s 𝑧) → (∃𝑥 ∈ ℤs 𝑁 = (2s ·s 𝑥) ↔ ∃𝑥 ∈ ℤs
(𝑦 -s 𝑧) = (2s
·s 𝑥))) |
123 | | eqeq1 2738 |
. . . . . 6
⊢ (𝑁 = (𝑦 -s 𝑧) → (𝑁 = ((2s ·s
𝑥) +s
1s ) ↔ (𝑦
-s 𝑧) =
((2s ·s 𝑥) +s 1s
))) |
124 | 123 | rexbidv 3181 |
. . . . 5
⊢ (𝑁 = (𝑦 -s 𝑧) → (∃𝑥 ∈ ℤs 𝑁 = ((2s ·s
𝑥) +s
1s ) ↔ ∃𝑥 ∈ ℤs (𝑦 -s 𝑧) = ((2s
·s 𝑥)
+s 1s ))) |
125 | 122, 124 | orbi12d 917 |
. . . 4
⊢ (𝑁 = (𝑦 -s 𝑧) → ((∃𝑥 ∈ ℤs 𝑁 = (2s ·s 𝑥) ∨ ∃𝑥 ∈ ℤs 𝑁 = ((2s ·s
𝑥) +s
1s )) ↔ (∃𝑥 ∈ ℤs (𝑦 -s 𝑧) = (2s
·s 𝑥)
∨ ∃𝑥 ∈
ℤs (𝑦
-s 𝑧) =
((2s ·s 𝑥) +s 1s
)))) |
126 | 120, 125 | syl5ibrcom 247 |
. . 3
⊢ ((𝑦 ∈ ℕs
∧ 𝑧 ∈
ℕs) → (𝑁 = (𝑦 -s 𝑧) → (∃𝑥 ∈ ℤs 𝑁 = (2s ·s 𝑥) ∨ ∃𝑥 ∈ ℤs 𝑁 = ((2s ·s
𝑥) +s
1s )))) |
127 | 126 | rexlimivv 3203 |
. 2
⊢
(∃𝑦 ∈
ℕs ∃𝑧 ∈ ℕs 𝑁 = (𝑦 -s 𝑧) → (∃𝑥 ∈ ℤs 𝑁 = (2s ·s 𝑥) ∨ ∃𝑥 ∈ ℤs 𝑁 = ((2s ·s
𝑥) +s
1s ))) |
128 | 1, 127 | sylbi 217 |
1
⊢ (𝑁 ∈ ℤs
→ (∃𝑥 ∈
ℤs 𝑁 =
(2s ·s 𝑥) ∨ ∃𝑥 ∈ ℤs 𝑁 = ((2s ·s
𝑥) +s
1s ))) |