Step | Hyp | Ref
| Expression |
1 | | addhalfcut.1 |
. . . 4
⊢ (𝜑 → 𝐴 ∈
ℕ0s) |
2 | 1 | n0snod 28339 |
. . 3
⊢ (𝜑 → 𝐴 ∈ No
) |
3 | | 1sno 27881 |
. . . . 5
⊢
1s ∈ No |
4 | 3 | a1i 11 |
. . . 4
⊢ (𝜑 → 1s ∈ No ) |
5 | 2, 4 | addscld 28022 |
. . 3
⊢ (𝜑 → (𝐴 +s 1s ) ∈ No ) |
6 | 2 | sltp1d 28057 |
. . 3
⊢ (𝜑 → 𝐴 <s (𝐴 +s 1s
)) |
7 | | no2times 28410 |
. . . . . . 7
⊢ (𝐴 ∈
No → (2s ·s 𝐴) = (𝐴 +s 𝐴)) |
8 | 2, 7 | syl 17 |
. . . . . 6
⊢ (𝜑 → (2s
·s 𝐴) =
(𝐴 +s 𝐴)) |
9 | 8 | oveq1d 7460 |
. . . . 5
⊢ (𝜑 → ((2s
·s 𝐴)
+s 1s ) = ((𝐴 +s 𝐴) +s 1s
)) |
10 | 2, 2, 4 | addsassd 28048 |
. . . . 5
⊢ (𝜑 → ((𝐴 +s 𝐴) +s 1s ) = (𝐴 +s (𝐴 +s 1s
))) |
11 | 9, 10 | eqtr2d 2775 |
. . . 4
⊢ (𝜑 → (𝐴 +s (𝐴 +s 1s )) =
((2s ·s 𝐴) +s 1s
)) |
12 | | 2nns 28411 |
. . . . . . . . . 10
⊢
2s ∈ ℕs |
13 | | nnn0s 28341 |
. . . . . . . . . 10
⊢
(2s ∈ ℕs → 2s ∈
ℕ0s) |
14 | 12, 13 | ax-mp 5 |
. . . . . . . . 9
⊢
2s ∈ ℕ0s |
15 | 14 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 2s ∈
ℕ0s) |
16 | | n0mulscl 28357 |
. . . . . . . 8
⊢
((2s ∈ ℕ0s ∧ 𝐴 ∈ ℕ0s) →
(2s ·s 𝐴) ∈
ℕ0s) |
17 | 15, 1, 16 | syl2anc 583 |
. . . . . . 7
⊢ (𝜑 → (2s
·s 𝐴)
∈ ℕ0s) |
18 | | 1n0s 28360 |
. . . . . . . 8
⊢
1s ∈ ℕ0s |
19 | 18 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 1s ∈
ℕ0s) |
20 | | n0addscl 28356 |
. . . . . . 7
⊢
(((2s ·s 𝐴) ∈ ℕ0s ∧
1s ∈ ℕ0s) → ((2s
·s 𝐴)
+s 1s ) ∈ ℕ0s) |
21 | 17, 19, 20 | syl2anc 583 |
. . . . . 6
⊢ (𝜑 → ((2s
·s 𝐴)
+s 1s ) ∈ ℕ0s) |
22 | | n0scut 28347 |
. . . . . 6
⊢
(((2s ·s 𝐴) +s 1s ) ∈
ℕ0s → ((2s ·s 𝐴) +s 1s )
= ({(((2s ·s 𝐴) +s 1s )
-s 1s )} |s ∅)) |
23 | 21, 22 | syl 17 |
. . . . 5
⊢ (𝜑 → ((2s
·s 𝐴)
+s 1s ) = ({(((2s ·s 𝐴) +s 1s )
-s 1s )} |s ∅)) |
24 | | 2sno 28412 |
. . . . . . . . . 10
⊢
2s ∈ No |
25 | 24 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 2s ∈ No ) |
26 | 25, 2 | mulscld 28170 |
. . . . . . . 8
⊢ (𝜑 → (2s
·s 𝐴)
∈ No ) |
27 | | pncans 28111 |
. . . . . . . 8
⊢
(((2s ·s 𝐴) ∈ No
∧ 1s ∈ No ) →
(((2s ·s 𝐴) +s 1s )
-s 1s ) = (2s ·s 𝐴)) |
28 | 26, 4, 27 | syl2anc 583 |
. . . . . . 7
⊢ (𝜑 → (((2s
·s 𝐴)
+s 1s ) -s 1s ) = (2s
·s 𝐴)) |
29 | 28 | sneqd 4660 |
. . . . . 6
⊢ (𝜑 → {(((2s
·s 𝐴)
+s 1s ) -s 1s )} = {(2s
·s 𝐴)}) |
30 | 29 | oveq1d 7460 |
. . . . 5
⊢ (𝜑 → ({(((2s
·s 𝐴)
+s 1s ) -s 1s )} |s ∅) =
({(2s ·s 𝐴)} |s ∅)) |
31 | 23, 30 | eqtrd 2774 |
. . . 4
⊢ (𝜑 → ((2s
·s 𝐴)
+s 1s ) = ({(2s ·s 𝐴)} |s ∅)) |
32 | | snelpwi 5466 |
. . . . . 6
⊢
((2s ·s 𝐴) ∈ No
→ {(2s ·s 𝐴)} ∈ 𝒫
No ) |
33 | | nulssgt 27852 |
. . . . . 6
⊢
({(2s ·s 𝐴)} ∈ 𝒫
No → {(2s ·s 𝐴)} <<s ∅) |
34 | 26, 32, 33 | 3syl 18 |
. . . . 5
⊢ (𝜑 → {(2s
·s 𝐴)}
<<s ∅) |
35 | | slerflex 27817 |
. . . . . . 7
⊢
((2s ·s 𝐴) ∈ No
→ (2s ·s 𝐴) ≤s (2s ·s
𝐴)) |
36 | 26, 35 | syl 17 |
. . . . . 6
⊢ (𝜑 → (2s
·s 𝐴)
≤s (2s ·s 𝐴)) |
37 | | ovex 7478 |
. . . . . . . . 9
⊢
(2s ·s 𝐴) ∈ V |
38 | | breq2 5173 |
. . . . . . . . 9
⊢ (𝑦 = (2s
·s 𝐴)
→ (𝑥 ≤s 𝑦 ↔ 𝑥 ≤s (2s ·s
𝐴))) |
39 | 37, 38 | rexsn 4706 |
. . . . . . . 8
⊢
(∃𝑦 ∈
{(2s ·s 𝐴)}𝑥 ≤s 𝑦 ↔ 𝑥 ≤s (2s ·s
𝐴)) |
40 | 39 | ralbii 3095 |
. . . . . . 7
⊢
(∀𝑥 ∈
{(2s ·s 𝐴)}∃𝑦 ∈ {(2s ·s
𝐴)}𝑥 ≤s 𝑦 ↔ ∀𝑥 ∈ {(2s ·s
𝐴)}𝑥 ≤s (2s ·s
𝐴)) |
41 | | breq1 5172 |
. . . . . . . 8
⊢ (𝑥 = (2s
·s 𝐴)
→ (𝑥 ≤s
(2s ·s 𝐴) ↔ (2s ·s
𝐴) ≤s (2s
·s 𝐴))) |
42 | 37, 41 | ralsn 4705 |
. . . . . . 7
⊢
(∀𝑥 ∈
{(2s ·s 𝐴)}𝑥 ≤s (2s ·s
𝐴) ↔ (2s
·s 𝐴)
≤s (2s ·s 𝐴)) |
43 | 40, 42 | bitri 275 |
. . . . . 6
⊢
(∀𝑥 ∈
{(2s ·s 𝐴)}∃𝑦 ∈ {(2s ·s
𝐴)}𝑥 ≤s 𝑦 ↔ (2s ·s
𝐴) ≤s (2s
·s 𝐴)) |
44 | 36, 43 | sylibr 234 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ {(2s ·s
𝐴)}∃𝑦 ∈ {(2s
·s 𝐴)}𝑥 ≤s 𝑦) |
45 | | ral0 4532 |
. . . . . 6
⊢
∀𝑥 ∈
∅ ∃𝑦 ∈
{(2s ·s (𝐴 +s 1s ))}𝑦 ≤s 𝑥 |
46 | 45 | a1i 11 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ ∅ ∃𝑦 ∈ {(2s ·s
(𝐴 +s
1s ))}𝑦 ≤s
𝑥) |
47 | 26, 4 | addscld 28022 |
. . . . . . 7
⊢ (𝜑 → ((2s
·s 𝐴)
+s 1s ) ∈ No
) |
48 | 26 | sltp1d 28057 |
. . . . . . 7
⊢ (𝜑 → (2s
·s 𝐴)
<s ((2s ·s 𝐴) +s 1s
)) |
49 | 26, 47, 48 | ssltsn 27846 |
. . . . . 6
⊢ (𝜑 → {(2s
·s 𝐴)}
<<s {((2s ·s 𝐴) +s 1s
)}) |
50 | 31 | sneqd 4660 |
. . . . . 6
⊢ (𝜑 → {((2s
·s 𝐴)
+s 1s )} = {({(2s ·s 𝐴)} |s
∅)}) |
51 | 49, 50 | breqtrd 5195 |
. . . . 5
⊢ (𝜑 → {(2s
·s 𝐴)}
<<s {({(2s ·s 𝐴)} |s ∅)}) |
52 | 25, 5 | mulscld 28170 |
. . . . . . 7
⊢ (𝜑 → (2s
·s (𝐴
+s 1s )) ∈ No
) |
53 | 4 | sltp1d 28057 |
. . . . . . . . . 10
⊢ (𝜑 → 1s <s (
1s +s 1s )) |
54 | | 1p1e2s 28409 |
. . . . . . . . . 10
⊢ (
1s +s 1s ) = 2s |
55 | 53, 54 | breqtrdi 5210 |
. . . . . . . . 9
⊢ (𝜑 → 1s <s
2s) |
56 | 4, 25, 26 | sltadd2d 28039 |
. . . . . . . . 9
⊢ (𝜑 → ( 1s <s
2s ↔ ((2s ·s 𝐴) +s 1s ) <s
((2s ·s 𝐴) +s
2s))) |
57 | 55, 56 | mpbid 232 |
. . . . . . . 8
⊢ (𝜑 → ((2s
·s 𝐴)
+s 1s ) <s ((2s ·s 𝐴) +s
2s)) |
58 | 25, 2, 4 | addsdid 28191 |
. . . . . . . . 9
⊢ (𝜑 → (2s
·s (𝐴
+s 1s )) = ((2s ·s 𝐴) +s (2s
·s 1s ))) |
59 | | mulsrid 28148 |
. . . . . . . . . . 11
⊢
(2s ∈ No →
(2s ·s 1s ) =
2s) |
60 | 24, 59 | ax-mp 5 |
. . . . . . . . . 10
⊢
(2s ·s 1s ) =
2s |
61 | 60 | oveq2i 7456 |
. . . . . . . . 9
⊢
((2s ·s 𝐴) +s (2s
·s 1s )) = ((2s ·s
𝐴) +s
2s) |
62 | 58, 61 | eqtrdi 2790 |
. . . . . . . 8
⊢ (𝜑 → (2s
·s (𝐴
+s 1s )) = ((2s ·s 𝐴) +s
2s)) |
63 | 57, 62 | breqtrrd 5197 |
. . . . . . 7
⊢ (𝜑 → ((2s
·s 𝐴)
+s 1s ) <s (2s ·s (𝐴 +s 1s
))) |
64 | 47, 52, 63 | ssltsn 27846 |
. . . . . 6
⊢ (𝜑 → {((2s
·s 𝐴)
+s 1s )} <<s {(2s ·s
(𝐴 +s
1s ))}) |
65 | 50, 64 | eqbrtrrd 5193 |
. . . . 5
⊢ (𝜑 → {({(2s
·s 𝐴)} |s
∅)} <<s {(2s ·s (𝐴 +s 1s
))}) |
66 | 34, 44, 46, 51, 65 | cofcut1d 27964 |
. . . 4
⊢ (𝜑 → ({(2s
·s 𝐴)} |s
∅) = ({(2s ·s 𝐴)} |s {(2s ·s
(𝐴 +s
1s ))})) |
67 | 11, 31, 66 | 3eqtrrd 2779 |
. . 3
⊢ (𝜑 → ({(2s
·s 𝐴)} |s
{(2s ·s (𝐴 +s 1s ))}) = (𝐴 +s (𝐴 +s 1s
))) |
68 | | eqid 2734 |
. . 3
⊢ ({𝐴} |s {(𝐴 +s 1s )}) = ({𝐴} |s {(𝐴 +s 1s
)}) |
69 | 2, 5, 6, 67, 68 | halfcut 28425 |
. 2
⊢ (𝜑 → ({𝐴} |s {(𝐴 +s 1s )}) = ((𝐴 +s (𝐴 +s 1s ))
/su 2s)) |
70 | 11 | oveq1d 7460 |
. 2
⊢ (𝜑 → ((𝐴 +s (𝐴 +s 1s ))
/su 2s) = (((2s ·s 𝐴) +s 1s )
/su 2s)) |
71 | | 2ne0s 28413 |
. . . . 5
⊢
2s ≠ 0s |
72 | 71 | a1i 11 |
. . . 4
⊢ (𝜑 → 2s ≠
0s ) |
73 | 26, 4, 25, 72 | divsdird 28268 |
. . 3
⊢ (𝜑 → (((2s
·s 𝐴)
+s 1s ) /su 2s) =
(((2s ·s 𝐴) /su 2s)
+s ( 1s /su
2s))) |
74 | 2, 25, 72 | divscan3d 28269 |
. . . 4
⊢ (𝜑 → ((2s
·s 𝐴)
/su 2s) = 𝐴) |
75 | 74 | oveq1d 7460 |
. . 3
⊢ (𝜑 → (((2s
·s 𝐴)
/su 2s) +s ( 1s
/su 2s)) = (𝐴 +s ( 1s
/su 2s))) |
76 | 73, 75 | eqtrd 2774 |
. 2
⊢ (𝜑 → (((2s
·s 𝐴)
+s 1s ) /su 2s) = (𝐴 +s ( 1s
/su 2s))) |
77 | 69, 70, 76 | 3eqtrd 2778 |
1
⊢ (𝜑 → ({𝐴} |s {(𝐴 +s 1s )}) = (𝐴 +s ( 1s
/su 2s))) |