Step | Hyp | Ref
| Expression |
1 | | pw2cut.3 |
. 2
⊢ (𝜑 → 𝑁 ∈
ℕ0s) |
2 | | oveq2 7453 |
. . . . . . . . 9
⊢ (𝑥 = 0s →
(2s↑s𝑥) = (2s↑s
0s )) |
3 | | 2sno 28412 |
. . . . . . . . . 10
⊢
2s ∈ No |
4 | | exps0 28419 |
. . . . . . . . . 10
⊢
(2s ∈ No →
(2s↑s 0s ) = 1s
) |
5 | 3, 4 | ax-mp 5 |
. . . . . . . . 9
⊢
(2s↑s 0s ) =
1s |
6 | 2, 5 | eqtrdi 2790 |
. . . . . . . 8
⊢ (𝑥 = 0s →
(2s↑s𝑥) = 1s ) |
7 | 6 | oveq2d 7461 |
. . . . . . 7
⊢ (𝑥 = 0s → (𝐴 /su
(2s↑s𝑥)) = (𝐴 /su 1s
)) |
8 | 7 | sneqd 4660 |
. . . . . 6
⊢ (𝑥 = 0s → {(𝐴 /su
(2s↑s𝑥))} = {(𝐴 /su 1s
)}) |
9 | 6 | oveq2d 7461 |
. . . . . . 7
⊢ (𝑥 = 0s → (𝐵 /su
(2s↑s𝑥)) = (𝐵 /su 1s
)) |
10 | 9 | sneqd 4660 |
. . . . . 6
⊢ (𝑥 = 0s → {(𝐵 /su
(2s↑s𝑥))} = {(𝐵 /su 1s
)}) |
11 | 8, 10 | oveq12d 7463 |
. . . . 5
⊢ (𝑥 = 0s → ({(𝐴 /su
(2s↑s𝑥))} |s {(𝐵 /su
(2s↑s𝑥))}) = ({(𝐴 /su 1s )} |s
{(𝐵 /su
1s )})) |
12 | | oveq1 7452 |
. . . . . . . . 9
⊢ (𝑥 = 0s → (𝑥 +s 1s ) =
( 0s +s 1s )) |
13 | | 1sno 27881 |
. . . . . . . . . 10
⊢
1s ∈ No |
14 | | addslid 28010 |
. . . . . . . . . 10
⊢ (
1s ∈ No → ( 0s
+s 1s ) = 1s ) |
15 | 13, 14 | ax-mp 5 |
. . . . . . . . 9
⊢ (
0s +s 1s ) = 1s |
16 | 12, 15 | eqtrdi 2790 |
. . . . . . . 8
⊢ (𝑥 = 0s → (𝑥 +s 1s ) =
1s ) |
17 | 16 | oveq2d 7461 |
. . . . . . 7
⊢ (𝑥 = 0s →
(2s↑s(𝑥 +s 1s )) =
(2s↑s 1s )) |
18 | | exps1 28420 |
. . . . . . . 8
⊢
(2s ∈ No →
(2s↑s 1s ) =
2s) |
19 | 3, 18 | ax-mp 5 |
. . . . . . 7
⊢
(2s↑s 1s ) =
2s |
20 | 17, 19 | eqtrdi 2790 |
. . . . . 6
⊢ (𝑥 = 0s →
(2s↑s(𝑥 +s 1s )) =
2s) |
21 | 20 | oveq2d 7461 |
. . . . 5
⊢ (𝑥 = 0s → ((𝐴 +s 𝐵) /su
(2s↑s(𝑥 +s 1s ))) = ((𝐴 +s 𝐵) /su
2s)) |
22 | 11, 21 | eqeq12d 2750 |
. . . 4
⊢ (𝑥 = 0s →
(({(𝐴 /su
(2s↑s𝑥))} |s {(𝐵 /su
(2s↑s𝑥))}) = ((𝐴 +s 𝐵) /su
(2s↑s(𝑥 +s 1s ))) ↔
({(𝐴 /su
1s )} |s {(𝐵
/su 1s )}) = ((𝐴 +s 𝐵) /su
2s))) |
23 | 22 | imbi2d 340 |
. . 3
⊢ (𝑥 = 0s → ((𝜑 → ({(𝐴 /su
(2s↑s𝑥))} |s {(𝐵 /su
(2s↑s𝑥))}) = ((𝐴 +s 𝐵) /su
(2s↑s(𝑥 +s 1s )))) ↔
(𝜑 → ({(𝐴 /su
1s )} |s {(𝐵
/su 1s )}) = ((𝐴 +s 𝐵) /su
2s)))) |
24 | | oveq2 7453 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (2s↑s𝑥) =
(2s↑s𝑦)) |
25 | 24 | oveq2d 7461 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝐴 /su
(2s↑s𝑥)) = (𝐴 /su
(2s↑s𝑦))) |
26 | 25 | sneqd 4660 |
. . . . . 6
⊢ (𝑥 = 𝑦 → {(𝐴 /su
(2s↑s𝑥))} = {(𝐴 /su
(2s↑s𝑦))}) |
27 | 24 | oveq2d 7461 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝐵 /su
(2s↑s𝑥)) = (𝐵 /su
(2s↑s𝑦))) |
28 | 27 | sneqd 4660 |
. . . . . 6
⊢ (𝑥 = 𝑦 → {(𝐵 /su
(2s↑s𝑥))} = {(𝐵 /su
(2s↑s𝑦))}) |
29 | 26, 28 | oveq12d 7463 |
. . . . 5
⊢ (𝑥 = 𝑦 → ({(𝐴 /su
(2s↑s𝑥))} |s {(𝐵 /su
(2s↑s𝑥))}) = ({(𝐴 /su
(2s↑s𝑦))} |s {(𝐵 /su
(2s↑s𝑦))})) |
30 | | oveq1 7452 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 +s 1s ) = (𝑦 +s 1s
)) |
31 | 30 | oveq2d 7461 |
. . . . . 6
⊢ (𝑥 = 𝑦 →
(2s↑s(𝑥 +s 1s )) =
(2s↑s(𝑦 +s 1s
))) |
32 | 31 | oveq2d 7461 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝐴 +s 𝐵) /su
(2s↑s(𝑥 +s 1s ))) = ((𝐴 +s 𝐵) /su
(2s↑s(𝑦 +s 1s
)))) |
33 | 29, 32 | eqeq12d 2750 |
. . . 4
⊢ (𝑥 = 𝑦 → (({(𝐴 /su
(2s↑s𝑥))} |s {(𝐵 /su
(2s↑s𝑥))}) = ((𝐴 +s 𝐵) /su
(2s↑s(𝑥 +s 1s ))) ↔
({(𝐴 /su
(2s↑s𝑦))} |s {(𝐵 /su
(2s↑s𝑦))}) = ((𝐴 +s 𝐵) /su
(2s↑s(𝑦 +s 1s
))))) |
34 | 33 | imbi2d 340 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝜑 → ({(𝐴 /su
(2s↑s𝑥))} |s {(𝐵 /su
(2s↑s𝑥))}) = ((𝐴 +s 𝐵) /su
(2s↑s(𝑥 +s 1s )))) ↔
(𝜑 → ({(𝐴 /su
(2s↑s𝑦))} |s {(𝐵 /su
(2s↑s𝑦))}) = ((𝐴 +s 𝐵) /su
(2s↑s(𝑦 +s 1s
)))))) |
35 | | oveq2 7453 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 +s 1s ) →
(2s↑s𝑥) = (2s↑s(𝑦 +s 1s
))) |
36 | 35 | oveq2d 7461 |
. . . . . . 7
⊢ (𝑥 = (𝑦 +s 1s ) → (𝐴 /su
(2s↑s𝑥)) = (𝐴 /su
(2s↑s(𝑦 +s 1s
)))) |
37 | 36 | sneqd 4660 |
. . . . . 6
⊢ (𝑥 = (𝑦 +s 1s ) → {(𝐴 /su
(2s↑s𝑥))} = {(𝐴 /su
(2s↑s(𝑦 +s 1s
)))}) |
38 | 35 | oveq2d 7461 |
. . . . . . 7
⊢ (𝑥 = (𝑦 +s 1s ) → (𝐵 /su
(2s↑s𝑥)) = (𝐵 /su
(2s↑s(𝑦 +s 1s
)))) |
39 | 38 | sneqd 4660 |
. . . . . 6
⊢ (𝑥 = (𝑦 +s 1s ) → {(𝐵 /su
(2s↑s𝑥))} = {(𝐵 /su
(2s↑s(𝑦 +s 1s
)))}) |
40 | 37, 39 | oveq12d 7463 |
. . . . 5
⊢ (𝑥 = (𝑦 +s 1s ) →
({(𝐴 /su
(2s↑s𝑥))} |s {(𝐵 /su
(2s↑s𝑥))}) = ({(𝐴 /su
(2s↑s(𝑦 +s 1s )))} |s {(𝐵 /su
(2s↑s(𝑦 +s 1s
)))})) |
41 | | oveq1 7452 |
. . . . . . 7
⊢ (𝑥 = (𝑦 +s 1s ) → (𝑥 +s 1s ) =
((𝑦 +s
1s ) +s 1s )) |
42 | 41 | oveq2d 7461 |
. . . . . 6
⊢ (𝑥 = (𝑦 +s 1s ) →
(2s↑s(𝑥 +s 1s )) =
(2s↑s((𝑦 +s 1s ) +s
1s ))) |
43 | 42 | oveq2d 7461 |
. . . . 5
⊢ (𝑥 = (𝑦 +s 1s ) → ((𝐴 +s 𝐵) /su
(2s↑s(𝑥 +s 1s ))) = ((𝐴 +s 𝐵) /su
(2s↑s((𝑦 +s 1s ) +s
1s )))) |
44 | 40, 43 | eqeq12d 2750 |
. . . 4
⊢ (𝑥 = (𝑦 +s 1s ) →
(({(𝐴 /su
(2s↑s𝑥))} |s {(𝐵 /su
(2s↑s𝑥))}) = ((𝐴 +s 𝐵) /su
(2s↑s(𝑥 +s 1s ))) ↔
({(𝐴 /su
(2s↑s(𝑦 +s 1s )))} |s {(𝐵 /su
(2s↑s(𝑦 +s 1s )))}) = ((𝐴 +s 𝐵) /su
(2s↑s((𝑦 +s 1s ) +s
1s ))))) |
45 | 44 | imbi2d 340 |
. . 3
⊢ (𝑥 = (𝑦 +s 1s ) → ((𝜑 → ({(𝐴 /su
(2s↑s𝑥))} |s {(𝐵 /su
(2s↑s𝑥))}) = ((𝐴 +s 𝐵) /su
(2s↑s(𝑥 +s 1s )))) ↔
(𝜑 → ({(𝐴 /su
(2s↑s(𝑦 +s 1s )))} |s {(𝐵 /su
(2s↑s(𝑦 +s 1s )))}) = ((𝐴 +s 𝐵) /su
(2s↑s((𝑦 +s 1s ) +s
1s )))))) |
46 | | oveq2 7453 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 →
(2s↑s𝑥) = (2s↑s𝑁)) |
47 | 46 | oveq2d 7461 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (𝐴 /su
(2s↑s𝑥)) = (𝐴 /su
(2s↑s𝑁))) |
48 | 47 | sneqd 4660 |
. . . . . 6
⊢ (𝑥 = 𝑁 → {(𝐴 /su
(2s↑s𝑥))} = {(𝐴 /su
(2s↑s𝑁))}) |
49 | 46 | oveq2d 7461 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (𝐵 /su
(2s↑s𝑥)) = (𝐵 /su
(2s↑s𝑁))) |
50 | 49 | sneqd 4660 |
. . . . . 6
⊢ (𝑥 = 𝑁 → {(𝐵 /su
(2s↑s𝑥))} = {(𝐵 /su
(2s↑s𝑁))}) |
51 | 48, 50 | oveq12d 7463 |
. . . . 5
⊢ (𝑥 = 𝑁 → ({(𝐴 /su
(2s↑s𝑥))} |s {(𝐵 /su
(2s↑s𝑥))}) = ({(𝐴 /su
(2s↑s𝑁))} |s {(𝐵 /su
(2s↑s𝑁))})) |
52 | | oveq1 7452 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (𝑥 +s 1s ) = (𝑁 +s 1s
)) |
53 | 52 | oveq2d 7461 |
. . . . . 6
⊢ (𝑥 = 𝑁 →
(2s↑s(𝑥 +s 1s )) =
(2s↑s(𝑁 +s 1s
))) |
54 | 53 | oveq2d 7461 |
. . . . 5
⊢ (𝑥 = 𝑁 → ((𝐴 +s 𝐵) /su
(2s↑s(𝑥 +s 1s ))) = ((𝐴 +s 𝐵) /su
(2s↑s(𝑁 +s 1s
)))) |
55 | 51, 54 | eqeq12d 2750 |
. . . 4
⊢ (𝑥 = 𝑁 → (({(𝐴 /su
(2s↑s𝑥))} |s {(𝐵 /su
(2s↑s𝑥))}) = ((𝐴 +s 𝐵) /su
(2s↑s(𝑥 +s 1s ))) ↔
({(𝐴 /su
(2s↑s𝑁))} |s {(𝐵 /su
(2s↑s𝑁))}) = ((𝐴 +s 𝐵) /su
(2s↑s(𝑁 +s 1s
))))) |
56 | 55 | imbi2d 340 |
. . 3
⊢ (𝑥 = 𝑁 → ((𝜑 → ({(𝐴 /su
(2s↑s𝑥))} |s {(𝐵 /su
(2s↑s𝑥))}) = ((𝐴 +s 𝐵) /su
(2s↑s(𝑥 +s 1s )))) ↔
(𝜑 → ({(𝐴 /su
(2s↑s𝑁))} |s {(𝐵 /su
(2s↑s𝑁))}) = ((𝐴 +s 𝐵) /su
(2s↑s(𝑁 +s 1s
)))))) |
57 | | pw2cut.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ No
) |
58 | | divs1 28238 |
. . . . . . 7
⊢ (𝐴 ∈
No → (𝐴
/su 1s ) = 𝐴) |
59 | 57, 58 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐴 /su 1s ) = 𝐴) |
60 | 59 | sneqd 4660 |
. . . . 5
⊢ (𝜑 → {(𝐴 /su 1s )} =
{𝐴}) |
61 | | pw2cut.2 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ No
) |
62 | | divs1 28238 |
. . . . . . 7
⊢ (𝐵 ∈
No → (𝐵
/su 1s ) = 𝐵) |
63 | 61, 62 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐵 /su 1s ) = 𝐵) |
64 | 63 | sneqd 4660 |
. . . . 5
⊢ (𝜑 → {(𝐵 /su 1s )} =
{𝐵}) |
65 | 60, 64 | oveq12d 7463 |
. . . 4
⊢ (𝜑 → ({(𝐴 /su 1s )} |s
{(𝐵 /su
1s )}) = ({𝐴} |s
{𝐵})) |
66 | | pw2cut.4 |
. . . . 5
⊢ (𝜑 → 𝐴 <s 𝐵) |
67 | | pw2cut.5 |
. . . . 5
⊢ (𝜑 → ({(2s
·s 𝐴)} |s
{(2s ·s 𝐵)}) = (𝐴 +s 𝐵)) |
68 | | eqid 2734 |
. . . . 5
⊢ ({𝐴} |s {𝐵}) = ({𝐴} |s {𝐵}) |
69 | 57, 61, 66, 67, 68 | halfcut 28425 |
. . . 4
⊢ (𝜑 → ({𝐴} |s {𝐵}) = ((𝐴 +s 𝐵) /su
2s)) |
70 | 65, 69 | eqtrd 2774 |
. . 3
⊢ (𝜑 → ({(𝐴 /su 1s )} |s
{(𝐵 /su
1s )}) = ((𝐴
+s 𝐵)
/su 2s)) |
71 | 57 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) → 𝐴 ∈
No ) |
72 | | peano2n0s 28344 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ0s
→ (𝑦 +s
1s ) ∈ ℕ0s) |
73 | | expscl 28422 |
. . . . . . . . . . . 12
⊢
((2s ∈ No ∧ (𝑦 +s 1s )
∈ ℕ0s) → (2s↑s(𝑦 +s 1s ))
∈ No ) |
74 | 3, 72, 73 | sylancr 586 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ0s
→ (2s↑s(𝑦 +s 1s )) ∈ No ) |
75 | 74 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) →
(2s↑s(𝑦 +s 1s )) ∈ No ) |
76 | | 2ne0s 28413 |
. . . . . . . . . . . . 13
⊢
2s ≠ 0s |
77 | | expsne0 28423 |
. . . . . . . . . . . . 13
⊢
((2s ∈ No ∧
2s ≠ 0s ∧ (𝑦 +s 1s ) ∈
ℕ0s) → (2s↑s(𝑦 +s 1s ))
≠ 0s ) |
78 | 3, 76, 77 | mp3an12 1451 |
. . . . . . . . . . . 12
⊢ ((𝑦 +s 1s )
∈ ℕ0s → (2s↑s(𝑦 +s 1s ))
≠ 0s ) |
79 | 72, 78 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ0s
→ (2s↑s(𝑦 +s 1s )) ≠
0s ) |
80 | 79 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) →
(2s↑s(𝑦 +s 1s )) ≠
0s ) |
81 | 71, 75, 80 | divscld 28257 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) → (𝐴 /su
(2s↑s(𝑦 +s 1s ))) ∈ No ) |
82 | 81 | 3adant3 1132 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑 ∧ ({(𝐴 /su
(2s↑s𝑦))} |s {(𝐵 /su
(2s↑s𝑦))}) = ((𝐴 +s 𝐵) /su
(2s↑s(𝑦 +s 1s )))) →
(𝐴 /su
(2s↑s(𝑦 +s 1s ))) ∈ No ) |
83 | 61 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) → 𝐵 ∈
No ) |
84 | 83, 75, 80 | divscld 28257 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) → (𝐵 /su
(2s↑s(𝑦 +s 1s ))) ∈ No ) |
85 | 84 | 3adant3 1132 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑 ∧ ({(𝐴 /su
(2s↑s𝑦))} |s {(𝐵 /su
(2s↑s𝑦))}) = ((𝐴 +s 𝐵) /su
(2s↑s(𝑦 +s 1s )))) →
(𝐵 /su
(2s↑s(𝑦 +s 1s ))) ∈ No ) |
86 | 71, 75, 80 | divscan1d 28259 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) → ((𝐴 /su
(2s↑s(𝑦 +s 1s )))
·s (2s↑s(𝑦 +s 1s ))) = 𝐴) |
87 | 66 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) → 𝐴 <s 𝐵) |
88 | 86, 87 | eqbrtrd 5191 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) → ((𝐴 /su
(2s↑s(𝑦 +s 1s )))
·s (2s↑s(𝑦 +s 1s ))) <s 𝐵) |
89 | | 2nns 28411 |
. . . . . . . . . . . . . . 15
⊢
2s ∈ ℕs |
90 | | nnsgt0 28351 |
. . . . . . . . . . . . . . 15
⊢
(2s ∈ ℕs → 0s <s
2s) |
91 | 89, 90 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
0s <s 2s |
92 | | expsgt0 28424 |
. . . . . . . . . . . . . 14
⊢
((2s ∈ No ∧ (𝑦 +s 1s )
∈ ℕ0s ∧ 0s <s 2s) →
0s <s (2s↑s(𝑦 +s 1s
))) |
93 | 3, 91, 92 | mp3an13 1452 |
. . . . . . . . . . . . 13
⊢ ((𝑦 +s 1s )
∈ ℕ0s → 0s <s
(2s↑s(𝑦 +s 1s
))) |
94 | 72, 93 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ0s
→ 0s <s (2s↑s(𝑦 +s 1s
))) |
95 | 94 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) → 0s
<s (2s↑s(𝑦 +s 1s
))) |
96 | 81, 83, 75, 95 | sltmuldivd 28262 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) → (((𝐴 /su
(2s↑s(𝑦 +s 1s )))
·s (2s↑s(𝑦 +s 1s ))) <s 𝐵 ↔ (𝐴 /su
(2s↑s(𝑦 +s 1s ))) <s (𝐵 /su
(2s↑s(𝑦 +s 1s
))))) |
97 | 88, 96 | mpbid 232 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) → (𝐴 /su
(2s↑s(𝑦 +s 1s ))) <s (𝐵 /su
(2s↑s(𝑦 +s 1s
)))) |
98 | 97 | 3adant3 1132 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑 ∧ ({(𝐴 /su
(2s↑s𝑦))} |s {(𝐵 /su
(2s↑s𝑦))}) = ((𝐴 +s 𝐵) /su
(2s↑s(𝑦 +s 1s )))) →
(𝐴 /su
(2s↑s(𝑦 +s 1s ))) <s (𝐵 /su
(2s↑s(𝑦 +s 1s
)))) |
99 | | expsp1 28421 |
. . . . . . . . . . . . . . . . . . 19
⊢
((2s ∈ No ∧ 𝑦 ∈ ℕ0s)
→ (2s↑s(𝑦 +s 1s )) =
((2s↑s𝑦) ·s
2s)) |
100 | 3, 99 | mpan 689 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℕ0s
→ (2s↑s(𝑦 +s 1s )) =
((2s↑s𝑦) ·s
2s)) |
101 | 100 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) →
(2s↑s(𝑦 +s 1s )) =
((2s↑s𝑦) ·s
2s)) |
102 | 101 | oveq2d 7461 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) → (𝐴 /su
(2s↑s(𝑦 +s 1s ))) = (𝐴 /su
((2s↑s𝑦) ·s
2s))) |
103 | | expscl 28422 |
. . . . . . . . . . . . . . . . . . 19
⊢
((2s ∈ No ∧ 𝑦 ∈ ℕ0s)
→ (2s↑s𝑦) ∈ No
) |
104 | 3, 103 | mpan 689 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℕ0s
→ (2s↑s𝑦) ∈ No
) |
105 | 104 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) →
(2s↑s𝑦) ∈ No
) |
106 | 3 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) → 2s
∈ No ) |
107 | | expsne0 28423 |
. . . . . . . . . . . . . . . . . . 19
⊢
((2s ∈ No ∧
2s ≠ 0s ∧ 𝑦 ∈ ℕ0s) →
(2s↑s𝑦) ≠ 0s ) |
108 | 3, 76, 107 | mp3an12 1451 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℕ0s
→ (2s↑s𝑦) ≠ 0s ) |
109 | 108 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) →
(2s↑s𝑦) ≠ 0s ) |
110 | 76 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) → 2s
≠ 0s ) |
111 | 71, 105, 106, 109, 110 | divdivs1d 28266 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) → ((𝐴 /su
(2s↑s𝑦)) /su 2s) = (𝐴 /su
((2s↑s𝑦) ·s
2s))) |
112 | 102, 111 | eqtr4d 2777 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) → (𝐴 /su
(2s↑s(𝑦 +s 1s ))) = ((𝐴 /su
(2s↑s𝑦)) /su
2s)) |
113 | 112 | oveq2d 7461 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) →
(2s ·s (𝐴 /su
(2s↑s(𝑦 +s 1s )))) =
(2s ·s ((𝐴 /su
(2s↑s𝑦)) /su
2s))) |
114 | 71, 105, 109 | divscld 28257 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) → (𝐴 /su
(2s↑s𝑦)) ∈ No
) |
115 | 114, 106,
110 | divscan2d 28258 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) →
(2s ·s ((𝐴 /su
(2s↑s𝑦)) /su 2s)) =
(𝐴 /su
(2s↑s𝑦))) |
116 | 113, 115 | eqtrd 2774 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) →
(2s ·s (𝐴 /su
(2s↑s(𝑦 +s 1s )))) = (𝐴 /su
(2s↑s𝑦))) |
117 | 116 | sneqd 4660 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) →
{(2s ·s (𝐴 /su
(2s↑s(𝑦 +s 1s ))))} = {(𝐴 /su
(2s↑s𝑦))}) |
118 | 101 | oveq2d 7461 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) → (𝐵 /su
(2s↑s(𝑦 +s 1s ))) = (𝐵 /su
((2s↑s𝑦) ·s
2s))) |
119 | 83, 105, 106, 109, 110 | divdivs1d 28266 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) → ((𝐵 /su
(2s↑s𝑦)) /su 2s) = (𝐵 /su
((2s↑s𝑦) ·s
2s))) |
120 | 118, 119 | eqtr4d 2777 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) → (𝐵 /su
(2s↑s(𝑦 +s 1s ))) = ((𝐵 /su
(2s↑s𝑦)) /su
2s)) |
121 | 120 | oveq2d 7461 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) →
(2s ·s (𝐵 /su
(2s↑s(𝑦 +s 1s )))) =
(2s ·s ((𝐵 /su
(2s↑s𝑦)) /su
2s))) |
122 | 83, 105, 109 | divscld 28257 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) → (𝐵 /su
(2s↑s𝑦)) ∈ No
) |
123 | 122, 106,
110 | divscan2d 28258 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) →
(2s ·s ((𝐵 /su
(2s↑s𝑦)) /su 2s)) =
(𝐵 /su
(2s↑s𝑦))) |
124 | 121, 123 | eqtrd 2774 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) →
(2s ·s (𝐵 /su
(2s↑s(𝑦 +s 1s )))) = (𝐵 /su
(2s↑s𝑦))) |
125 | 124 | sneqd 4660 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) →
{(2s ·s (𝐵 /su
(2s↑s(𝑦 +s 1s ))))} = {(𝐵 /su
(2s↑s𝑦))}) |
126 | 117, 125 | oveq12d 7463 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) →
({(2s ·s (𝐴 /su
(2s↑s(𝑦 +s 1s ))))} |s
{(2s ·s (𝐵 /su
(2s↑s(𝑦 +s 1s ))))}) =
({(𝐴 /su
(2s↑s𝑦))} |s {(𝐵 /su
(2s↑s𝑦))})) |
127 | 126 | eqcomd 2740 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) → ({(𝐴 /su
(2s↑s𝑦))} |s {(𝐵 /su
(2s↑s𝑦))}) = ({(2s ·s
(𝐴 /su
(2s↑s(𝑦 +s 1s ))))} |s
{(2s ·s (𝐵 /su
(2s↑s(𝑦 +s 1s
))))})) |
128 | 71, 83, 75, 80 | divsdird 28268 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) → ((𝐴 +s 𝐵) /su
(2s↑s(𝑦 +s 1s ))) = ((𝐴 /su
(2s↑s(𝑦 +s 1s )))
+s (𝐵
/su (2s↑s(𝑦 +s 1s
))))) |
129 | 127, 128 | eqeq12d 2750 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) → (({(𝐴 /su
(2s↑s𝑦))} |s {(𝐵 /su
(2s↑s𝑦))}) = ((𝐴 +s 𝐵) /su
(2s↑s(𝑦 +s 1s ))) ↔
({(2s ·s (𝐴 /su
(2s↑s(𝑦 +s 1s ))))} |s
{(2s ·s (𝐵 /su
(2s↑s(𝑦 +s 1s ))))}) = ((𝐴 /su
(2s↑s(𝑦 +s 1s )))
+s (𝐵
/su (2s↑s(𝑦 +s 1s
)))))) |
130 | 129 | biimp3a 1469 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑 ∧ ({(𝐴 /su
(2s↑s𝑦))} |s {(𝐵 /su
(2s↑s𝑦))}) = ((𝐴 +s 𝐵) /su
(2s↑s(𝑦 +s 1s )))) →
({(2s ·s (𝐴 /su
(2s↑s(𝑦 +s 1s ))))} |s
{(2s ·s (𝐵 /su
(2s↑s(𝑦 +s 1s ))))}) = ((𝐴 /su
(2s↑s(𝑦 +s 1s )))
+s (𝐵
/su (2s↑s(𝑦 +s 1s
))))) |
131 | | eqid 2734 |
. . . . . . . 8
⊢ ({(𝐴 /su
(2s↑s(𝑦 +s 1s )))} |s {(𝐵 /su
(2s↑s(𝑦 +s 1s )))}) = ({(𝐴 /su
(2s↑s(𝑦 +s 1s )))} |s {(𝐵 /su
(2s↑s(𝑦 +s 1s
)))}) |
132 | 82, 85, 98, 130, 131 | halfcut 28425 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑 ∧ ({(𝐴 /su
(2s↑s𝑦))} |s {(𝐵 /su
(2s↑s𝑦))}) = ((𝐴 +s 𝐵) /su
(2s↑s(𝑦 +s 1s )))) →
({(𝐴 /su
(2s↑s(𝑦 +s 1s )))} |s {(𝐵 /su
(2s↑s(𝑦 +s 1s )))}) = (((𝐴 /su
(2s↑s(𝑦 +s 1s )))
+s (𝐵
/su (2s↑s(𝑦 +s 1s ))))
/su 2s)) |
133 | 128 | oveq1d 7460 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) → (((𝐴 +s 𝐵) /su
(2s↑s(𝑦 +s 1s )))
/su 2s) = (((𝐴 /su
(2s↑s(𝑦 +s 1s )))
+s (𝐵
/su (2s↑s(𝑦 +s 1s ))))
/su 2s)) |
134 | 133 | 3adant3 1132 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑 ∧ ({(𝐴 /su
(2s↑s𝑦))} |s {(𝐵 /su
(2s↑s𝑦))}) = ((𝐴 +s 𝐵) /su
(2s↑s(𝑦 +s 1s )))) →
(((𝐴 +s 𝐵) /su
(2s↑s(𝑦 +s 1s )))
/su 2s) = (((𝐴 /su
(2s↑s(𝑦 +s 1s )))
+s (𝐵
/su (2s↑s(𝑦 +s 1s ))))
/su 2s)) |
135 | 132, 134 | eqtr4d 2777 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑 ∧ ({(𝐴 /su
(2s↑s𝑦))} |s {(𝐵 /su
(2s↑s𝑦))}) = ((𝐴 +s 𝐵) /su
(2s↑s(𝑦 +s 1s )))) →
({(𝐴 /su
(2s↑s(𝑦 +s 1s )))} |s {(𝐵 /su
(2s↑s(𝑦 +s 1s )))}) = (((𝐴 +s 𝐵) /su
(2s↑s(𝑦 +s 1s )))
/su 2s)) |
136 | | expsp1 28421 |
. . . . . . . . . . 11
⊢
((2s ∈ No ∧ (𝑦 +s 1s )
∈ ℕ0s) → (2s↑s((𝑦 +s 1s )
+s 1s )) = ((2s↑s(𝑦 +s 1s ))
·s 2s)) |
137 | 3, 72, 136 | sylancr 586 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ0s
→ (2s↑s((𝑦 +s 1s ) +s
1s )) = ((2s↑s(𝑦 +s 1s ))
·s 2s)) |
138 | 137 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) →
(2s↑s((𝑦 +s 1s ) +s
1s )) = ((2s↑s(𝑦 +s 1s ))
·s 2s)) |
139 | 138 | oveq2d 7461 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) → ((𝐴 +s 𝐵) /su
(2s↑s((𝑦 +s 1s ) +s
1s ))) = ((𝐴
+s 𝐵)
/su ((2s↑s(𝑦 +s 1s ))
·s 2s))) |
140 | 71, 83 | addscld 28022 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) → (𝐴 +s 𝐵) ∈ No
) |
141 | 140, 75, 106, 80, 110 | divdivs1d 28266 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) → (((𝐴 +s 𝐵) /su
(2s↑s(𝑦 +s 1s )))
/su 2s) = ((𝐴 +s 𝐵) /su
((2s↑s(𝑦 +s 1s ))
·s 2s))) |
142 | 139, 141 | eqtr4d 2777 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑) → ((𝐴 +s 𝐵) /su
(2s↑s((𝑦 +s 1s ) +s
1s ))) = (((𝐴
+s 𝐵)
/su (2s↑s(𝑦 +s 1s )))
/su 2s)) |
143 | 142 | 3adant3 1132 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑 ∧ ({(𝐴 /su
(2s↑s𝑦))} |s {(𝐵 /su
(2s↑s𝑦))}) = ((𝐴 +s 𝐵) /su
(2s↑s(𝑦 +s 1s )))) →
((𝐴 +s 𝐵) /su
(2s↑s((𝑦 +s 1s ) +s
1s ))) = (((𝐴
+s 𝐵)
/su (2s↑s(𝑦 +s 1s )))
/su 2s)) |
144 | 135, 143 | eqtr4d 2777 |
. . . . 5
⊢ ((𝑦 ∈ ℕ0s
∧ 𝜑 ∧ ({(𝐴 /su
(2s↑s𝑦))} |s {(𝐵 /su
(2s↑s𝑦))}) = ((𝐴 +s 𝐵) /su
(2s↑s(𝑦 +s 1s )))) →
({(𝐴 /su
(2s↑s(𝑦 +s 1s )))} |s {(𝐵 /su
(2s↑s(𝑦 +s 1s )))}) = ((𝐴 +s 𝐵) /su
(2s↑s((𝑦 +s 1s ) +s
1s )))) |
145 | 144 | 3exp 1119 |
. . . 4
⊢ (𝑦 ∈ ℕ0s
→ (𝜑 → (({(𝐴 /su
(2s↑s𝑦))} |s {(𝐵 /su
(2s↑s𝑦))}) = ((𝐴 +s 𝐵) /su
(2s↑s(𝑦 +s 1s ))) →
({(𝐴 /su
(2s↑s(𝑦 +s 1s )))} |s {(𝐵 /su
(2s↑s(𝑦 +s 1s )))}) = ((𝐴 +s 𝐵) /su
(2s↑s((𝑦 +s 1s ) +s
1s )))))) |
146 | 145 | a2d 29 |
. . 3
⊢ (𝑦 ∈ ℕ0s
→ ((𝜑 → ({(𝐴 /su
(2s↑s𝑦))} |s {(𝐵 /su
(2s↑s𝑦))}) = ((𝐴 +s 𝐵) /su
(2s↑s(𝑦 +s 1s )))) →
(𝜑 → ({(𝐴 /su
(2s↑s(𝑦 +s 1s )))} |s {(𝐵 /su
(2s↑s(𝑦 +s 1s )))}) = ((𝐴 +s 𝐵) /su
(2s↑s((𝑦 +s 1s ) +s
1s )))))) |
147 | 23, 34, 45, 56, 70, 146 | n0sind 28346 |
. 2
⊢ (𝑁 ∈ ℕ0s
→ (𝜑 → ({(𝐴 /su
(2s↑s𝑁))} |s {(𝐵 /su
(2s↑s𝑁))}) = ((𝐴 +s 𝐵) /su
(2s↑s(𝑁 +s 1s
))))) |
148 | 1, 147 | mpcom 38 |
1
⊢ (𝜑 → ({(𝐴 /su
(2s↑s𝑁))} |s {(𝐵 /su
(2s↑s𝑁))}) = ((𝐴 +s 𝐵) /su
(2s↑s(𝑁 +s 1s
)))) |