| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq1 7438 | . . . . . . 7
⊢ (𝑚 = 0s → (𝑚 +s 1s ) =
( 0s +s 1s )) | 
| 2 |  | 1sno 27872 | . . . . . . . 8
⊢ 
1s ∈  No | 
| 3 |  | addslid 28001 | . . . . . . . 8
⊢ (
1s ∈  No  → ( 0s
+s 1s ) = 1s ) | 
| 4 | 2, 3 | ax-mp 5 | . . . . . . 7
⊢ (
0s +s 1s ) = 1s | 
| 5 | 1, 4 | eqtrdi 2793 | . . . . . 6
⊢ (𝑚 = 0s → (𝑚 +s 1s ) =
1s ) | 
| 6 | 5 | oveq2d 7447 | . . . . 5
⊢ (𝑚 = 0s →
(2s↑s(𝑚 +s 1s )) =
(2s↑s 1s )) | 
| 7 |  | 2sno 28403 | . . . . . 6
⊢
2s ∈  No | 
| 8 |  | exps1 28411 | . . . . . 6
⊢
(2s ∈  No  →
(2s↑s 1s ) =
2s) | 
| 9 | 7, 8 | ax-mp 5 | . . . . 5
⊢
(2s↑s 1s ) =
2s | 
| 10 | 6, 9 | eqtrdi 2793 | . . . 4
⊢ (𝑚 = 0s →
(2s↑s(𝑚 +s 1s )) =
2s) | 
| 11 | 10 | oveq2d 7447 | . . 3
⊢ (𝑚 = 0s → (
1s /su (2s↑s(𝑚 +s 1s )))
= ( 1s /su 2s)) | 
| 12 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑚 = 0s →
(2s↑s𝑚) = (2s↑s
0s )) | 
| 13 |  | exps0 28410 | . . . . . . . . 9
⊢
(2s ∈  No  →
(2s↑s 0s ) = 1s
) | 
| 14 | 7, 13 | ax-mp 5 | . . . . . . . 8
⊢
(2s↑s 0s ) =
1s | 
| 15 | 12, 14 | eqtrdi 2793 | . . . . . . 7
⊢ (𝑚 = 0s →
(2s↑s𝑚) = 1s ) | 
| 16 | 15 | oveq2d 7447 | . . . . . 6
⊢ (𝑚 = 0s → (
1s /su (2s↑s𝑚)) = ( 1s
/su 1s )) | 
| 17 |  | divs1 28229 | . . . . . . 7
⊢ (
1s ∈  No  → ( 1s
/su 1s ) = 1s ) | 
| 18 | 2, 17 | ax-mp 5 | . . . . . 6
⊢ (
1s /su 1s ) =
1s | 
| 19 | 16, 18 | eqtrdi 2793 | . . . . 5
⊢ (𝑚 = 0s → (
1s /su (2s↑s𝑚)) = 1s
) | 
| 20 | 19 | sneqd 4638 | . . . 4
⊢ (𝑚 = 0s → {(
1s /su (2s↑s𝑚))} = { 1s
}) | 
| 21 | 20 | oveq2d 7447 | . . 3
⊢ (𝑚 = 0s → ({
0s } |s {( 1s /su
(2s↑s𝑚))}) = ({ 0s } |s { 1s
})) | 
| 22 | 11, 21 | eqeq12d 2753 | . 2
⊢ (𝑚 = 0s → ((
1s /su (2s↑s(𝑚 +s 1s )))
= ({ 0s } |s {( 1s /su
(2s↑s𝑚))}) ↔ ( 1s
/su 2s) = ({ 0s } |s { 1s
}))) | 
| 23 |  | oveq1 7438 | . . . . 5
⊢ (𝑚 = 𝑛 → (𝑚 +s 1s ) = (𝑛 +s 1s
)) | 
| 24 | 23 | oveq2d 7447 | . . . 4
⊢ (𝑚 = 𝑛 →
(2s↑s(𝑚 +s 1s )) =
(2s↑s(𝑛 +s 1s
))) | 
| 25 | 24 | oveq2d 7447 | . . 3
⊢ (𝑚 = 𝑛 → ( 1s /su
(2s↑s(𝑚 +s 1s ))) = (
1s /su (2s↑s(𝑛 +s 1s
)))) | 
| 26 |  | oveq2 7439 | . . . . . 6
⊢ (𝑚 = 𝑛 → (2s↑s𝑚) =
(2s↑s𝑛)) | 
| 27 | 26 | oveq2d 7447 | . . . . 5
⊢ (𝑚 = 𝑛 → ( 1s /su
(2s↑s𝑚)) = ( 1s /su
(2s↑s𝑛))) | 
| 28 | 27 | sneqd 4638 | . . . 4
⊢ (𝑚 = 𝑛 → {( 1s /su
(2s↑s𝑚))} = {( 1s /su
(2s↑s𝑛))}) | 
| 29 | 28 | oveq2d 7447 | . . 3
⊢ (𝑚 = 𝑛 → ({ 0s } |s {(
1s /su (2s↑s𝑚))}) = ({ 0s } |s {(
1s /su (2s↑s𝑛))})) | 
| 30 | 25, 29 | eqeq12d 2753 | . 2
⊢ (𝑚 = 𝑛 → (( 1s /su
(2s↑s(𝑚 +s 1s ))) = ({
0s } |s {( 1s /su
(2s↑s𝑚))}) ↔ ( 1s
/su (2s↑s(𝑛 +s 1s ))) = ({
0s } |s {( 1s /su
(2s↑s𝑛))}))) | 
| 31 |  | oveq1 7438 | . . . . 5
⊢ (𝑚 = (𝑛 +s 1s ) → (𝑚 +s 1s ) =
((𝑛 +s
1s ) +s 1s )) | 
| 32 | 31 | oveq2d 7447 | . . . 4
⊢ (𝑚 = (𝑛 +s 1s ) →
(2s↑s(𝑚 +s 1s )) =
(2s↑s((𝑛 +s 1s ) +s
1s ))) | 
| 33 | 32 | oveq2d 7447 | . . 3
⊢ (𝑚 = (𝑛 +s 1s ) → (
1s /su (2s↑s(𝑚 +s 1s )))
= ( 1s /su (2s↑s((𝑛 +s 1s )
+s 1s )))) | 
| 34 |  | oveq2 7439 | . . . . . 6
⊢ (𝑚 = (𝑛 +s 1s ) →
(2s↑s𝑚) = (2s↑s(𝑛 +s 1s
))) | 
| 35 | 34 | oveq2d 7447 | . . . . 5
⊢ (𝑚 = (𝑛 +s 1s ) → (
1s /su (2s↑s𝑚)) = ( 1s
/su (2s↑s(𝑛 +s 1s
)))) | 
| 36 | 35 | sneqd 4638 | . . . 4
⊢ (𝑚 = (𝑛 +s 1s ) → {(
1s /su (2s↑s𝑚))} = {( 1s
/su (2s↑s(𝑛 +s 1s
)))}) | 
| 37 | 36 | oveq2d 7447 | . . 3
⊢ (𝑚 = (𝑛 +s 1s ) → ({
0s } |s {( 1s /su
(2s↑s𝑚))}) = ({ 0s } |s {( 1s
/su (2s↑s(𝑛 +s 1s
)))})) | 
| 38 | 33, 37 | eqeq12d 2753 | . 2
⊢ (𝑚 = (𝑛 +s 1s ) → ((
1s /su (2s↑s(𝑚 +s 1s )))
= ({ 0s } |s {( 1s /su
(2s↑s𝑚))}) ↔ ( 1s
/su (2s↑s((𝑛 +s 1s ) +s
1s ))) = ({ 0s } |s {( 1s /su
(2s↑s(𝑛 +s 1s
)))}))) | 
| 39 |  | oveq1 7438 | . . . . 5
⊢ (𝑚 = 𝑁 → (𝑚 +s 1s ) = (𝑁 +s 1s
)) | 
| 40 | 39 | oveq2d 7447 | . . . 4
⊢ (𝑚 = 𝑁 →
(2s↑s(𝑚 +s 1s )) =
(2s↑s(𝑁 +s 1s
))) | 
| 41 | 40 | oveq2d 7447 | . . 3
⊢ (𝑚 = 𝑁 → ( 1s /su
(2s↑s(𝑚 +s 1s ))) = (
1s /su (2s↑s(𝑁 +s 1s
)))) | 
| 42 |  | oveq2 7439 | . . . . . 6
⊢ (𝑚 = 𝑁 →
(2s↑s𝑚) = (2s↑s𝑁)) | 
| 43 | 42 | oveq2d 7447 | . . . . 5
⊢ (𝑚 = 𝑁 → ( 1s /su
(2s↑s𝑚)) = ( 1s /su
(2s↑s𝑁))) | 
| 44 | 43 | sneqd 4638 | . . . 4
⊢ (𝑚 = 𝑁 → {( 1s /su
(2s↑s𝑚))} = {( 1s /su
(2s↑s𝑁))}) | 
| 45 | 44 | oveq2d 7447 | . . 3
⊢ (𝑚 = 𝑁 → ({ 0s } |s {(
1s /su (2s↑s𝑚))}) = ({ 0s } |s {(
1s /su (2s↑s𝑁))})) | 
| 46 | 41, 45 | eqeq12d 2753 | . 2
⊢ (𝑚 = 𝑁 → (( 1s /su
(2s↑s(𝑚 +s 1s ))) = ({
0s } |s {( 1s /su
(2s↑s𝑚))}) ↔ ( 1s
/su (2s↑s(𝑁 +s 1s ))) = ({
0s } |s {( 1s /su
(2s↑s𝑁))}))) | 
| 47 |  | nohalf 28407 | . 2
⊢ (
1s /su 2s) = ({ 0s } |s {
1s }) | 
| 48 |  | peano2n0s 28335 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ0s
→ (𝑛 +s
1s ) ∈ ℕ0s) | 
| 49 |  | expsp1 28412 | . . . . . . . . . 10
⊢
((2s ∈  No  ∧ (𝑛 +s 1s )
∈ ℕ0s) → (2s↑s((𝑛 +s 1s )
+s 1s )) = ((2s↑s(𝑛 +s 1s ))
·s 2s)) | 
| 50 | 7, 49 | mpan 690 | . . . . . . . . 9
⊢ ((𝑛 +s 1s )
∈ ℕ0s → (2s↑s((𝑛 +s 1s )
+s 1s )) = ((2s↑s(𝑛 +s 1s ))
·s 2s)) | 
| 51 | 48, 50 | syl 17 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ0s
→ (2s↑s((𝑛 +s 1s ) +s
1s )) = ((2s↑s(𝑛 +s 1s ))
·s 2s)) | 
| 52 | 51 | oveq2d 7447 | . . . . . . 7
⊢ (𝑛 ∈ ℕ0s
→ ( 1s /su
(2s↑s((𝑛 +s 1s ) +s
1s ))) = ( 1s /su
((2s↑s(𝑛 +s 1s ))
·s 2s))) | 
| 53 | 2 | a1i 11 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ0s
→ 1s ∈  No ) | 
| 54 |  | expscl 28413 | . . . . . . . . . 10
⊢
((2s ∈  No  ∧ (𝑛 +s 1s )
∈ ℕ0s) → (2s↑s(𝑛 +s 1s ))
∈  No ) | 
| 55 | 7, 54 | mpan 690 | . . . . . . . . 9
⊢ ((𝑛 +s 1s )
∈ ℕ0s → (2s↑s(𝑛 +s 1s ))
∈  No ) | 
| 56 | 48, 55 | syl 17 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ0s
→ (2s↑s(𝑛 +s 1s )) ∈  No ) | 
| 57 | 7 | a1i 11 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ0s
→ 2s ∈  No ) | 
| 58 |  | 2ne0s 28404 | . . . . . . . . . 10
⊢
2s ≠ 0s | 
| 59 |  | expsne0 28414 | . . . . . . . . . 10
⊢
((2s ∈  No  ∧
2s ≠ 0s ∧ (𝑛 +s 1s ) ∈
ℕ0s) → (2s↑s(𝑛 +s 1s ))
≠ 0s ) | 
| 60 | 7, 58, 59 | mp3an12 1453 | . . . . . . . . 9
⊢ ((𝑛 +s 1s )
∈ ℕ0s → (2s↑s(𝑛 +s 1s ))
≠ 0s ) | 
| 61 | 48, 60 | syl 17 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ0s
→ (2s↑s(𝑛 +s 1s )) ≠
0s ) | 
| 62 | 58 | a1i 11 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ0s
→ 2s ≠ 0s ) | 
| 63 | 53, 56, 57, 61, 62 | divdivs1d 28257 | . . . . . . 7
⊢ (𝑛 ∈ ℕ0s
→ (( 1s /su
(2s↑s(𝑛 +s 1s )))
/su 2s) = ( 1s /su
((2s↑s(𝑛 +s 1s ))
·s 2s))) | 
| 64 | 52, 63 | eqtr4d 2780 | . . . . . 6
⊢ (𝑛 ∈ ℕ0s
→ ( 1s /su
(2s↑s((𝑛 +s 1s ) +s
1s ))) = (( 1s /su
(2s↑s(𝑛 +s 1s )))
/su 2s)) | 
| 65 | 53, 56, 61 | divscld 28248 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ0s
→ ( 1s /su
(2s↑s(𝑛 +s 1s ))) ∈  No ) | 
| 66 |  | addslid 28001 | . . . . . . . 8
⊢ ((
1s /su (2s↑s(𝑛 +s 1s )))
∈  No  → ( 0s +s (
1s /su (2s↑s(𝑛 +s 1s
)))) = ( 1s /su
(2s↑s(𝑛 +s 1s
)))) | 
| 67 | 65, 66 | syl 17 | . . . . . . 7
⊢ (𝑛 ∈ ℕ0s
→ ( 0s +s ( 1s /su
(2s↑s(𝑛 +s 1s )))) = (
1s /su (2s↑s(𝑛 +s 1s
)))) | 
| 68 | 67 | oveq1d 7446 | . . . . . 6
⊢ (𝑛 ∈ ℕ0s
→ (( 0s +s ( 1s /su
(2s↑s(𝑛 +s 1s ))))
/su 2s) = (( 1s /su
(2s↑s(𝑛 +s 1s )))
/su 2s)) | 
| 69 | 64, 68 | eqtr4d 2780 | . . . . 5
⊢ (𝑛 ∈ ℕ0s
→ ( 1s /su
(2s↑s((𝑛 +s 1s ) +s
1s ))) = (( 0s +s ( 1s
/su (2s↑s(𝑛 +s 1s ))))
/su 2s)) | 
| 70 | 69 | adantr 480 | . . . 4
⊢ ((𝑛 ∈ ℕ0s
∧ ( 1s /su (2s↑s(𝑛 +s 1s )))
= ({ 0s } |s {( 1s /su
(2s↑s𝑛))})) → ( 1s
/su (2s↑s((𝑛 +s 1s ) +s
1s ))) = (( 0s +s ( 1s
/su (2s↑s(𝑛 +s 1s ))))
/su 2s)) | 
| 71 |  | 0sno 27871 | . . . . . 6
⊢ 
0s ∈  No | 
| 72 | 71 | a1i 11 | . . . . 5
⊢ ((𝑛 ∈ ℕ0s
∧ ( 1s /su (2s↑s(𝑛 +s 1s )))
= ({ 0s } |s {( 1s /su
(2s↑s𝑛))})) → 0s ∈  No ) | 
| 73 | 2 | a1i 11 | . . . . . 6
⊢ ((𝑛 ∈ ℕ0s
∧ ( 1s /su (2s↑s(𝑛 +s 1s )))
= ({ 0s } |s {( 1s /su
(2s↑s𝑛))})) → 1s ∈  No ) | 
| 74 | 56 | adantr 480 | . . . . . 6
⊢ ((𝑛 ∈ ℕ0s
∧ ( 1s /su (2s↑s(𝑛 +s 1s )))
= ({ 0s } |s {( 1s /su
(2s↑s𝑛))})) →
(2s↑s(𝑛 +s 1s )) ∈  No ) | 
| 75 | 61 | adantr 480 | . . . . . 6
⊢ ((𝑛 ∈ ℕ0s
∧ ( 1s /su (2s↑s(𝑛 +s 1s )))
= ({ 0s } |s {( 1s /su
(2s↑s𝑛))})) →
(2s↑s(𝑛 +s 1s )) ≠
0s ) | 
| 76 | 73, 74, 75 | divscld 28248 | . . . . 5
⊢ ((𝑛 ∈ ℕ0s
∧ ( 1s /su (2s↑s(𝑛 +s 1s )))
= ({ 0s } |s {( 1s /su
(2s↑s𝑛))})) → ( 1s
/su (2s↑s(𝑛 +s 1s ))) ∈  No ) | 
| 77 |  | muls02 28167 | . . . . . . . 8
⊢
((2s↑s(𝑛 +s 1s )) ∈  No  → ( 0s ·s
(2s↑s(𝑛 +s 1s ))) =
0s ) | 
| 78 | 74, 77 | syl 17 | . . . . . . 7
⊢ ((𝑛 ∈ ℕ0s
∧ ( 1s /su (2s↑s(𝑛 +s 1s )))
= ({ 0s } |s {( 1s /su
(2s↑s𝑛))})) → ( 0s
·s (2s↑s(𝑛 +s 1s ))) =
0s ) | 
| 79 |  | 0slt1s 27874 | . . . . . . 7
⊢ 
0s <s 1s | 
| 80 | 78, 79 | eqbrtrdi 5182 | . . . . . 6
⊢ ((𝑛 ∈ ℕ0s
∧ ( 1s /su (2s↑s(𝑛 +s 1s )))
= ({ 0s } |s {( 1s /su
(2s↑s𝑛))})) → ( 0s
·s (2s↑s(𝑛 +s 1s ))) <s
1s ) | 
| 81 |  | 2nns 28402 | . . . . . . . . . . 11
⊢
2s ∈ ℕs | 
| 82 |  | nnsgt0 28342 | . . . . . . . . . . 11
⊢
(2s ∈ ℕs → 0s <s
2s) | 
| 83 | 81, 82 | ax-mp 5 | . . . . . . . . . 10
⊢ 
0s <s 2s | 
| 84 |  | expsgt0 28415 | . . . . . . . . . 10
⊢
((2s ∈  No  ∧ (𝑛 +s 1s )
∈ ℕ0s ∧ 0s <s 2s) →
0s <s (2s↑s(𝑛 +s 1s
))) | 
| 85 | 7, 83, 84 | mp3an13 1454 | . . . . . . . . 9
⊢ ((𝑛 +s 1s )
∈ ℕ0s → 0s <s
(2s↑s(𝑛 +s 1s
))) | 
| 86 | 48, 85 | syl 17 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ0s
→ 0s <s (2s↑s(𝑛 +s 1s
))) | 
| 87 | 86 | adantr 480 | . . . . . . 7
⊢ ((𝑛 ∈ ℕ0s
∧ ( 1s /su (2s↑s(𝑛 +s 1s )))
= ({ 0s } |s {( 1s /su
(2s↑s𝑛))})) → 0s <s
(2s↑s(𝑛 +s 1s
))) | 
| 88 | 72, 73, 74, 87 | sltmuldivd 28253 | . . . . . 6
⊢ ((𝑛 ∈ ℕ0s
∧ ( 1s /su (2s↑s(𝑛 +s 1s )))
= ({ 0s } |s {( 1s /su
(2s↑s𝑛))})) → (( 0s
·s (2s↑s(𝑛 +s 1s ))) <s
1s ↔ 0s <s ( 1s /su
(2s↑s(𝑛 +s 1s
))))) | 
| 89 | 80, 88 | mpbid 232 | . . . . 5
⊢ ((𝑛 ∈ ℕ0s
∧ ( 1s /su (2s↑s(𝑛 +s 1s )))
= ({ 0s } |s {( 1s /su
(2s↑s𝑛))})) → 0s <s (
1s /su (2s↑s(𝑛 +s 1s
)))) | 
| 90 |  | muls01 28138 | . . . . . . . . . . 11
⊢
(2s ∈  No  →
(2s ·s 0s ) = 0s
) | 
| 91 | 7, 90 | ax-mp 5 | . . . . . . . . . 10
⊢
(2s ·s 0s ) =
0s | 
| 92 | 91 | sneqi 4637 | . . . . . . . . 9
⊢
{(2s ·s 0s )} = { 0s
} | 
| 93 | 92 | a1i 11 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ0s
→ {(2s ·s 0s )} = { 0s
}) | 
| 94 |  | expsp1 28412 | . . . . . . . . . . . . . 14
⊢
((2s ∈  No  ∧ 𝑛 ∈ ℕ0s)
→ (2s↑s(𝑛 +s 1s )) =
((2s↑s𝑛) ·s
2s)) | 
| 95 | 7, 94 | mpan 690 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ0s
→ (2s↑s(𝑛 +s 1s )) =
((2s↑s𝑛) ·s
2s)) | 
| 96 | 95 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0s
→ ( 1s /su
(2s↑s(𝑛 +s 1s ))) = (
1s /su ((2s↑s𝑛) ·s
2s))) | 
| 97 |  | expscl 28413 | . . . . . . . . . . . . . 14
⊢
((2s ∈  No  ∧ 𝑛 ∈ ℕ0s)
→ (2s↑s𝑛) ∈  No
) | 
| 98 | 7, 97 | mpan 690 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ0s
→ (2s↑s𝑛) ∈  No
) | 
| 99 |  | expsne0 28414 | . . . . . . . . . . . . . 14
⊢
((2s ∈  No  ∧
2s ≠ 0s ∧ 𝑛 ∈ ℕ0s) →
(2s↑s𝑛) ≠ 0s ) | 
| 100 | 7, 58, 99 | mp3an12 1453 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ0s
→ (2s↑s𝑛) ≠ 0s ) | 
| 101 | 53, 98, 57, 100, 62 | divdivs1d 28257 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0s
→ (( 1s /su
(2s↑s𝑛)) /su 2s) = (
1s /su ((2s↑s𝑛) ·s
2s))) | 
| 102 | 96, 101 | eqtr4d 2780 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0s
→ ( 1s /su
(2s↑s(𝑛 +s 1s ))) = ((
1s /su (2s↑s𝑛)) /su
2s)) | 
| 103 | 102 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0s
→ (2s ·s ( 1s /su
(2s↑s(𝑛 +s 1s )))) =
(2s ·s (( 1s /su
(2s↑s𝑛)) /su
2s))) | 
| 104 | 53, 98, 100 | divscld 28248 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0s
→ ( 1s /su (2s↑s𝑛)) ∈ 
No ) | 
| 105 | 104, 57, 62 | divscan2d 28249 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0s
→ (2s ·s (( 1s /su
(2s↑s𝑛)) /su 2s)) = (
1s /su (2s↑s𝑛))) | 
| 106 | 103, 105 | eqtrd 2777 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ0s
→ (2s ·s ( 1s /su
(2s↑s(𝑛 +s 1s )))) = (
1s /su (2s↑s𝑛))) | 
| 107 | 106 | sneqd 4638 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ0s
→ {(2s ·s ( 1s /su
(2s↑s(𝑛 +s 1s ))))} = {(
1s /su (2s↑s𝑛))}) | 
| 108 | 93, 107 | oveq12d 7449 | . . . . . . 7
⊢ (𝑛 ∈ ℕ0s
→ ({(2s ·s 0s )} |s
{(2s ·s ( 1s /su
(2s↑s(𝑛 +s 1s ))))}) = ({
0s } |s {( 1s /su
(2s↑s𝑛))})) | 
| 109 |  | eqcom 2744 | . . . . . . . 8
⊢ ((
1s /su (2s↑s(𝑛 +s 1s )))
= ({ 0s } |s {( 1s /su
(2s↑s𝑛))}) ↔ ({ 0s } |s {(
1s /su (2s↑s𝑛))}) = ( 1s
/su (2s↑s(𝑛 +s 1s
)))) | 
| 110 | 109 | biimpi 216 | . . . . . . 7
⊢ ((
1s /su (2s↑s(𝑛 +s 1s )))
= ({ 0s } |s {( 1s /su
(2s↑s𝑛))}) → ({ 0s } |s {(
1s /su (2s↑s𝑛))}) = ( 1s
/su (2s↑s(𝑛 +s 1s
)))) | 
| 111 | 108, 110 | sylan9eq 2797 | . . . . . 6
⊢ ((𝑛 ∈ ℕ0s
∧ ( 1s /su (2s↑s(𝑛 +s 1s )))
= ({ 0s } |s {( 1s /su
(2s↑s𝑛))})) → ({(2s
·s 0s )} |s {(2s ·s (
1s /su (2s↑s(𝑛 +s 1s
))))}) = ( 1s /su
(2s↑s(𝑛 +s 1s
)))) | 
| 112 | 76, 66 | syl 17 | . . . . . 6
⊢ ((𝑛 ∈ ℕ0s
∧ ( 1s /su (2s↑s(𝑛 +s 1s )))
= ({ 0s } |s {( 1s /su
(2s↑s𝑛))})) → ( 0s +s (
1s /su (2s↑s(𝑛 +s 1s
)))) = ( 1s /su
(2s↑s(𝑛 +s 1s
)))) | 
| 113 | 111, 112 | eqtr4d 2780 | . . . . 5
⊢ ((𝑛 ∈ ℕ0s
∧ ( 1s /su (2s↑s(𝑛 +s 1s )))
= ({ 0s } |s {( 1s /su
(2s↑s𝑛))})) → ({(2s
·s 0s )} |s {(2s ·s (
1s /su (2s↑s(𝑛 +s 1s
))))}) = ( 0s +s ( 1s /su
(2s↑s(𝑛 +s 1s
))))) | 
| 114 |  | eqid 2737 | . . . . 5
⊢ ({
0s } |s {( 1s /su
(2s↑s(𝑛 +s 1s )))}) = ({
0s } |s {( 1s /su
(2s↑s(𝑛 +s 1s
)))}) | 
| 115 | 72, 76, 89, 113, 114 | halfcut 28416 | . . . 4
⊢ ((𝑛 ∈ ℕ0s
∧ ( 1s /su (2s↑s(𝑛 +s 1s )))
= ({ 0s } |s {( 1s /su
(2s↑s𝑛))})) → ({ 0s } |s {(
1s /su (2s↑s(𝑛 +s 1s
)))}) = (( 0s +s ( 1s /su
(2s↑s(𝑛 +s 1s ))))
/su 2s)) | 
| 116 | 70, 115 | eqtr4d 2780 | . . 3
⊢ ((𝑛 ∈ ℕ0s
∧ ( 1s /su (2s↑s(𝑛 +s 1s )))
= ({ 0s } |s {( 1s /su
(2s↑s𝑛))})) → ( 1s
/su (2s↑s((𝑛 +s 1s ) +s
1s ))) = ({ 0s } |s {( 1s /su
(2s↑s(𝑛 +s 1s
)))})) | 
| 117 | 116 | ex 412 | . 2
⊢ (𝑛 ∈ ℕ0s
→ (( 1s /su
(2s↑s(𝑛 +s 1s ))) = ({
0s } |s {( 1s /su
(2s↑s𝑛))}) → ( 1s
/su (2s↑s((𝑛 +s 1s ) +s
1s ))) = ({ 0s } |s {( 1s /su
(2s↑s(𝑛 +s 1s
)))}))) | 
| 118 | 22, 30, 38, 46, 47, 117 | n0sind 28337 | 1
⊢ (𝑁 ∈ ℕ0s
→ ( 1s /su
(2s↑s(𝑁 +s 1s ))) = ({
0s } |s {( 1s /su
(2s↑s𝑁))})) |