Metamath Proof Explorer

Theorem zs12negscl

Description: The dyadics are closed under negation. (Contributed by Scott Fenton, 9-Nov-2025)

Ref Expression
Assertion zs12negscl ( 𝐴 ∈ ℤs[1/2] → ( -us ‘ 𝐴 ) ∈ ℤs[1/2] )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝑧 = ( -us ‘ 𝑥 ) → ( 𝑧 /su ( 2s ↑s 𝑦 ) ) = ( ( -us ‘ 𝑥 ) /su ( 2s ↑s 𝑦 ) ) )
2 1 eqeq2d ⊢ ( 𝑧 = ( -us ‘ 𝑥 ) → ( ( -us ‘ ( 𝑥 /su ( 2s ↑s 𝑦 ) ) ) = ( 𝑧 /su ( 2s ↑s 𝑦 ) ) ↔ ( -us ‘ ( 𝑥 /su ( 2s ↑s 𝑦 ) ) ) = ( ( -us ‘ 𝑥 ) /su ( 2s ↑s 𝑦 ) ) ) )
3 znegscl ⊢ ( 𝑥 ∈ ℤs → ( -us ‘ 𝑥 ) ∈ ℤs )
4 3 adantl ⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝑥 ∈ ℤs ) → ( -us ‘ 𝑥 ) ∈ ℤs )
5 zno ⊢ ( 𝑥 ∈ ℤs → 𝑥 ∈ No )
6 5 adantl ⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝑥 ∈ ℤs ) → 𝑥 ∈ No )
7 simpl ⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝑥 ∈ ℤs ) → 𝑦 ∈ ℕ0s )
8 6 7 pw2divsnegd ⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝑥 ∈ ℤs ) → ( -us ‘ ( 𝑥 /su ( 2s ↑s 𝑦 ) ) ) = ( ( -us ‘ 𝑥 ) /su ( 2s ↑s 𝑦 ) ) )
9 2 4 8 rspcedvdw ⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝑥 ∈ ℤs ) → ∃ 𝑧 ∈ ℤs ( -us ‘ ( 𝑥 /su ( 2s ↑s 𝑦 ) ) ) = ( 𝑧 /su ( 2s ↑s 𝑦 ) ) )
10 fveq2 ⊢ ( 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) → ( -us ‘ 𝐴 ) = ( -us ‘ ( 𝑥 /su ( 2s ↑s 𝑦 ) ) ) )
11 10 eqeq1d ⊢ ( 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) → ( ( -us ‘ 𝐴 ) = ( 𝑧 /su ( 2s ↑s 𝑦 ) ) ↔ ( -us ‘ ( 𝑥 /su ( 2s ↑s 𝑦 ) ) ) = ( 𝑧 /su ( 2s ↑s 𝑦 ) ) ) )
12 11 rexbidv ⊢ ( 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) → ( ∃ 𝑧 ∈ ℤs ( -us ‘ 𝐴 ) = ( 𝑧 /su ( 2s ↑s 𝑦 ) ) ↔ ∃ 𝑧 ∈ ℤs ( -us ‘ ( 𝑥 /su ( 2s ↑s 𝑦 ) ) ) = ( 𝑧 /su ( 2s ↑s 𝑦 ) ) ) )
13 9 12 syl5ibrcom ⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝑥 ∈ ℤs ) → ( 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) → ∃ 𝑧 ∈ ℤs ( -us ‘ 𝐴 ) = ( 𝑧 /su ( 2s ↑s 𝑦 ) ) ) )
14 13 rexlimdva ⊢ ( 𝑦 ∈ ℕ0s → ( ∃ 𝑥 ∈ ℤs 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) → ∃ 𝑧 ∈ ℤs ( -us ‘ 𝐴 ) = ( 𝑧 /su ( 2s ↑s 𝑦 ) ) ) )
15 14 reximia ⊢ ( ∃ 𝑦 ∈ ℕ0s ∃ 𝑥 ∈ ℤs 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) → ∃ 𝑦 ∈ ℕ0s ∃ 𝑧 ∈ ℤs ( -us ‘ 𝐴 ) = ( 𝑧 /su ( 2s ↑s 𝑦 ) ) )
16 elzs12 ⊢ ( 𝐴 ∈ ℤs[1/2] ↔ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕ0s 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) )
17 rexcom ⊢ ( ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕ0s 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) ↔ ∃ 𝑦 ∈ ℕ0s ∃ 𝑥 ∈ ℤs 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) )
18 16 17 bitri ⊢ ( 𝐴 ∈ ℤs[1/2] ↔ ∃ 𝑦 ∈ ℕ0s ∃ 𝑥 ∈ ℤs 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) )
19 elzs12 ⊢ ( ( -us ‘ 𝐴 ) ∈ ℤs[1/2] ↔ ∃ 𝑧 ∈ ℤs ∃ 𝑦 ∈ ℕ0s ( -us ‘ 𝐴 ) = ( 𝑧 /su ( 2s ↑s 𝑦 ) ) )
20 rexcom ⊢ ( ∃ 𝑧 ∈ ℤs ∃ 𝑦 ∈ ℕ0s ( -us ‘ 𝐴 ) = ( 𝑧 /su ( 2s ↑s 𝑦 ) ) ↔ ∃ 𝑦 ∈ ℕ0s ∃ 𝑧 ∈ ℤs ( -us ‘ 𝐴 ) = ( 𝑧 /su ( 2s ↑s 𝑦 ) ) )
21 19 20 bitri ⊢ ( ( -us ‘ 𝐴 ) ∈ ℤs[1/2] ↔ ∃ 𝑦 ∈ ℕ0s ∃ 𝑧 ∈ ℤs ( -us ‘ 𝐴 ) = ( 𝑧 /su ( 2s ↑s 𝑦 ) ) )
22 15 18 21 3imtr4i ⊢ ( 𝐴 ∈ ℤs[1/2] → ( -us ‘ 𝐴 ) ∈ ℤs[1/2] )