Theorem pw2divsidd

Description: Identity law for division over powers of two. (Contributed by Scott Fenton, 21-Feb-2026)

	Ref	Expression
Hypothesis	pw2divs0d.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
Assertion	pw2divsidd	⊢ ( 𝜑 → ( ( 2s ↑s 𝑁 ) /su ( 2s ↑s 𝑁 ) ) = 1s )

Proof

Step	Hyp	Ref	Expression
1		pw2divs0d.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
2		2sno	⊢ 2s ∈ No
3		expscl	⊢ ( ( 2s ∈ No ∧ 𝑁 ∈ ℕ0s ) → ( 2s ↑s 𝑁 ) ∈ No )
4	2 1 3	sylancr	⊢ ( 𝜑 → ( 2s ↑s 𝑁 ) ∈ No )
5	4	mulsridd	⊢ ( 𝜑 → ( ( 2s ↑s 𝑁 ) ·s 1s ) = ( 2s ↑s 𝑁 ) )
6		1sno	⊢ 1s ∈ No
7	6	a1i	⊢ ( 𝜑 → 1s ∈ No )
8	4 7 1	pw2divsmuld	⊢ ( 𝜑 → ( ( ( 2s ↑s 𝑁 ) /su ( 2s ↑s 𝑁 ) ) = 1s ↔ ( ( 2s ↑s 𝑁 ) ·s 1s ) = ( 2s ↑s 𝑁 ) ) )
9	5 8	mpbird	⊢ ( 𝜑 → ( ( 2s ↑s 𝑁 ) /su ( 2s ↑s 𝑁 ) ) = 1s )