Theorem pw2divscld

Description: Division closure for powers of two. (Contributed by Scott Fenton, 7-Nov-2025)

	Ref	Expression
Hypotheses	pw2divscld.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	pw2divscld.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
Assertion	pw2divscld	⊢ ( 𝜑 → ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ∈ No )

Proof

Step	Hyp	Ref	Expression
1		pw2divscld.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		pw2divscld.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ0s )
3		2sno	⊢ 2s ∈ No
4		expscl	⊢ ( ( 2s ∈ No ∧ 𝑁 ∈ ℕ0s ) → ( 2s ↑s 𝑁 ) ∈ No )
5	3 2 4	sylancr	⊢ ( 𝜑 → ( 2s ↑s 𝑁 ) ∈ No )
6		2ne0s	⊢ 2s ≠ 0s
7		expsne0	⊢ ( ( 2s ∈ No ∧ 2s ≠ 0s ∧ 𝑁 ∈ ℕ0s ) → ( 2s ↑s 𝑁 ) ≠ 0s )
8	3 6 2 7	mp3an12i	⊢ ( 𝜑 → ( 2s ↑s 𝑁 ) ≠ 0s )
9		pw2recs	⊢ ( 𝑁 ∈ ℕ0s → ∃ 𝑥 ∈ No ( ( 2s ↑s 𝑁 ) ·s 𝑥 ) = 1s )
10	2 9	syl	⊢ ( 𝜑 → ∃ 𝑥 ∈ No ( ( 2s ↑s 𝑁 ) ·s 𝑥 ) = 1s )
11	1 5 8 10	divsclwd	⊢ ( 𝜑 → ( 𝐴 /su ( 2s ↑s 𝑁 ) ) ∈ No )