Metamath Proof Explorer

Theorem z12zsodd

Description: A dyadic fraction is either an integer or an odd number divided by a positive power of two. (Contributed by Scott Fenton, 5-Dec-2025)

Ref Expression
Assertion z12zsodd ( 𝐴 ∈ ℤs[1/2] → ( 𝐴 ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs 𝐴 = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 elz12s ⊢ ( 𝐴 ∈ ℤs[1/2] ↔ ∃ 𝑎 ∈ ℤs ∃ 𝑏 ∈ ℕ0s 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑏 ) ) )
2 oveq2 ⊢ ( 𝑐 = 0s → ( 2s ↑s 𝑐 ) = ( 2s ↑s 0s ) )
3 2no ⊢ 2s ∈ No
4 exps0 ⊢ ( 2s ∈ No → ( 2s ↑s 0s ) = 1s )
5 3 4 ax-mp ⊢ ( 2s ↑s 0s ) = 1s
6 2 5 eqtrdi ⊢ ( 𝑐 = 0s → ( 2s ↑s 𝑐 ) = 1s )
7 6 oveq2d ⊢ ( 𝑐 = 0s → ( 𝑎 /su ( 2s ↑s 𝑐 ) ) = ( 𝑎 /su 1s ) )
8 7 eleq1d ⊢ ( 𝑐 = 0s → ( ( 𝑎 /su ( 2s ↑s 𝑐 ) ) ∈ ℤs ↔ ( 𝑎 /su 1s ) ∈ ℤs ) )
9 7 eqeq1d ⊢ ( 𝑐 = 0s → ( ( 𝑎 /su ( 2s ↑s 𝑐 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ↔ ( 𝑎 /su 1s ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )
10 9 2rexbidv ⊢ ( 𝑐 = 0s → ( ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑐 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ↔ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su 1s ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )
11 8 10 orbi12d ⊢ ( 𝑐 = 0s → ( ( ( 𝑎 /su ( 2s ↑s 𝑐 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑐 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ↔ ( ( 𝑎 /su 1s ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su 1s ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ) )
12 11 ralbidv ⊢ ( 𝑐 = 0s → ( ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su ( 2s ↑s 𝑐 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑐 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ↔ ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su 1s ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su 1s ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ) )
13 oveq2 ⊢ ( 𝑐 = 𝑤 → ( 2s ↑s 𝑐 ) = ( 2s ↑s 𝑤 ) )
14 13 oveq2d ⊢ ( 𝑐 = 𝑤 → ( 𝑎 /su ( 2s ↑s 𝑐 ) ) = ( 𝑎 /su ( 2s ↑s 𝑤 ) ) )
15 14 eleq1d ⊢ ( 𝑐 = 𝑤 → ( ( 𝑎 /su ( 2s ↑s 𝑐 ) ) ∈ ℤs ↔ ( 𝑎 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ) )
16 14 eqeq1d ⊢ ( 𝑐 = 𝑤 → ( ( 𝑎 /su ( 2s ↑s 𝑐 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ↔ ( 𝑎 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )
17 16 2rexbidv ⊢ ( 𝑐 = 𝑤 → ( ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑐 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ↔ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )
18 15 17 orbi12d ⊢ ( 𝑐 = 𝑤 → ( ( ( 𝑎 /su ( 2s ↑s 𝑐 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑐 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ↔ ( ( 𝑎 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ) )
19 18 ralbidv ⊢ ( 𝑐 = 𝑤 → ( ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su ( 2s ↑s 𝑐 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑐 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ↔ ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ) )
20 oveq2 ⊢ ( 𝑐 = ( 𝑤 +s 1s ) → ( 2s ↑s 𝑐 ) = ( 2s ↑s ( 𝑤 +s 1s ) ) )
21 20 oveq2d ⊢ ( 𝑐 = ( 𝑤 +s 1s ) → ( 𝑎 /su ( 2s ↑s 𝑐 ) ) = ( 𝑎 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) )
22 21 eleq1d ⊢ ( 𝑐 = ( 𝑤 +s 1s ) → ( ( 𝑎 /su ( 2s ↑s 𝑐 ) ) ∈ ℤs ↔ ( 𝑎 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ) )
23 21 eqeq1d ⊢ ( 𝑐 = ( 𝑤 +s 1s ) → ( ( 𝑎 /su ( 2s ↑s 𝑐 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ↔ ( 𝑎 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )
24 23 2rexbidv ⊢ ( 𝑐 = ( 𝑤 +s 1s ) → ( ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑐 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ↔ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )
25 22 24 orbi12d ⊢ ( 𝑐 = ( 𝑤 +s 1s ) → ( ( ( 𝑎 /su ( 2s ↑s 𝑐 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑐 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ↔ ( ( 𝑎 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ) )
26 25 ralbidv ⊢ ( 𝑐 = ( 𝑤 +s 1s ) → ( ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su ( 2s ↑s 𝑐 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑐 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ↔ ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ) )
27 oveq1 ⊢ ( 𝑎 = 𝑏 → ( 𝑎 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) )
28 27 eleq1d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑎 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ↔ ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ) )
29 27 eqeq1d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑎 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ↔ ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )
30 29 2rexbidv ⊢ ( 𝑎 = 𝑏 → ( ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ↔ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )
31 oveq2 ⊢ ( 𝑥 = 𝑝 → ( 2s ·s 𝑥 ) = ( 2s ·s 𝑝 ) )
32 31 oveq1d ⊢ ( 𝑥 = 𝑝 → ( ( 2s ·s 𝑥 ) +s 1s ) = ( ( 2s ·s 𝑝 ) +s 1s ) )
33 32 oveq1d ⊢ ( 𝑥 = 𝑝 → ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) )
34 33 eqeq2d ⊢ ( 𝑥 = 𝑝 → ( ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ↔ ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )
35 oveq2 ⊢ ( 𝑦 = 𝑞 → ( 2s ↑s 𝑦 ) = ( 2s ↑s 𝑞 ) )
36 35 oveq2d ⊢ ( 𝑦 = 𝑞 → ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) )
37 36 eqeq2d ⊢ ( 𝑦 = 𝑞 → ( ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ↔ ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) )
38 34 37 cbvrex2vw ⊢ ( ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ↔ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) )
39 30 38 bitrdi ⊢ ( 𝑎 = 𝑏 → ( ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ↔ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) )
40 28 39 orbi12d ⊢ ( 𝑎 = 𝑏 → ( ( ( 𝑎 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ↔ ( ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ∨ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) ) )
41 40 cbvralvw ⊢ ( ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ↔ ∀ 𝑏 ∈ ℤs ( ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ∨ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) )
42 26 41 bitrdi ⊢ ( 𝑐 = ( 𝑤 +s 1s ) → ( ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su ( 2s ↑s 𝑐 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑐 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ↔ ∀ 𝑏 ∈ ℤs ( ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ∨ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) ) )
43 oveq2 ⊢ ( 𝑐 = 𝑏 → ( 2s ↑s 𝑐 ) = ( 2s ↑s 𝑏 ) )
44 43 oveq2d ⊢ ( 𝑐 = 𝑏 → ( 𝑎 /su ( 2s ↑s 𝑐 ) ) = ( 𝑎 /su ( 2s ↑s 𝑏 ) ) )
45 44 eleq1d ⊢ ( 𝑐 = 𝑏 → ( ( 𝑎 /su ( 2s ↑s 𝑐 ) ) ∈ ℤs ↔ ( 𝑎 /su ( 2s ↑s 𝑏 ) ) ∈ ℤs ) )
46 44 eqeq1d ⊢ ( 𝑐 = 𝑏 → ( ( 𝑎 /su ( 2s ↑s 𝑐 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ↔ ( 𝑎 /su ( 2s ↑s 𝑏 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )
47 46 2rexbidv ⊢ ( 𝑐 = 𝑏 → ( ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑐 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ↔ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑏 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )
48 45 47 orbi12d ⊢ ( 𝑐 = 𝑏 → ( ( ( 𝑎 /su ( 2s ↑s 𝑐 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑐 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ↔ ( ( 𝑎 /su ( 2s ↑s 𝑏 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑏 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ) )
49 48 ralbidv ⊢ ( 𝑐 = 𝑏 → ( ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su ( 2s ↑s 𝑐 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑐 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ↔ ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su ( 2s ↑s 𝑏 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑏 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ) )
50 zno ⊢ ( 𝑎 ∈ ℤs → 𝑎 ∈ No )
51 50 divs1d ⊢ ( 𝑎 ∈ ℤs → ( 𝑎 /su 1s ) = 𝑎 )
52 id ⊢ ( 𝑎 ∈ ℤs → 𝑎 ∈ ℤs )
53 51 52 eqeltrd ⊢ ( 𝑎 ∈ ℤs → ( 𝑎 /su 1s ) ∈ ℤs )
54 53 orcd ⊢ ( 𝑎 ∈ ℤs → ( ( 𝑎 /su 1s ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su 1s ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )
55 54 rgen ⊢ ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su 1s ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su 1s ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) )
56 zseo ⊢ ( 𝑏 ∈ ℤs → ( ∃ 𝑐 ∈ ℤs 𝑏 = ( 2s ·s 𝑐 ) ∨ ∃ 𝑐 ∈ ℤs 𝑏 = ( ( 2s ·s 𝑐 ) +s 1s ) ) )
57 oveq1 ⊢ ( 𝑎 = 𝑐 → ( 𝑎 /su ( 2s ↑s 𝑤 ) ) = ( 𝑐 /su ( 2s ↑s 𝑤 ) ) )
58 57 eleq1d ⊢ ( 𝑎 = 𝑐 → ( ( 𝑎 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ↔ ( 𝑐 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ) )
59 57 eqeq1d ⊢ ( 𝑎 = 𝑐 → ( ( 𝑎 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ↔ ( 𝑐 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )
60 59 2rexbidv ⊢ ( 𝑎 = 𝑐 → ( ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ↔ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑐 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )
61 58 60 orbi12d ⊢ ( 𝑎 = 𝑐 → ( ( ( 𝑎 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ↔ ( ( 𝑐 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑐 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ) )
62 61 rspcv ⊢ ( 𝑐 ∈ ℤs → ( ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) → ( ( 𝑐 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑐 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ) )
63 62 adantl ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) → ( ( 𝑐 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑐 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ) )
64 33 eqeq2d ⊢ ( 𝑥 = 𝑝 → ( ( 𝑐 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ↔ ( 𝑐 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )
65 36 eqeq2d ⊢ ( 𝑦 = 𝑞 → ( ( 𝑐 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ↔ ( 𝑐 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) )
66 64 65 cbvrex2vw ⊢ ( ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑐 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ↔ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( 𝑐 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) )
67 66 orbi2i ⊢ ( ( ( 𝑐 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑐 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ↔ ( ( 𝑐 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ∨ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( 𝑐 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) )
68 63 67 imbitrdi ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) → ( ( 𝑐 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ∨ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( 𝑐 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) ) )
69 68 imp ⊢ ( ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) ∧ ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ) → ( ( 𝑐 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ∨ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( 𝑐 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) )
70 69 an32s ⊢ ( ( ( 𝑤 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ) ∧ 𝑐 ∈ ℤs ) → ( ( 𝑐 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ∨ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( 𝑐 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) )
71 simpl ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → 𝑤 ∈ ℕ0s )
72 expsp1 ⊢ ( ( 2s ∈ No ∧ 𝑤 ∈ ℕ0s ) → ( 2s ↑s ( 𝑤 +s 1s ) ) = ( ( 2s ↑s 𝑤 ) ·s 2s ) )
73 3 71 72 sylancr ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( 2s ↑s ( 𝑤 +s 1s ) ) = ( ( 2s ↑s 𝑤 ) ·s 2s ) )
74 73 oveq1d ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( ( 2s ↑s ( 𝑤 +s 1s ) ) ·s 𝑐 ) = ( ( ( 2s ↑s 𝑤 ) ·s 2s ) ·s 𝑐 ) )
75 expscl ⊢ ( ( 2s ∈ No ∧ 𝑤 ∈ ℕ0s ) → ( 2s ↑s 𝑤 ) ∈ No )
76 3 71 75 sylancr ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( 2s ↑s 𝑤 ) ∈ No )
77 3 a1i ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → 2s ∈ No )
78 zno ⊢ ( 𝑐 ∈ ℤs → 𝑐 ∈ No )
79 78 adantl ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → 𝑐 ∈ No )
80 76 77 79 mulsassd ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( ( ( 2s ↑s 𝑤 ) ·s 2s ) ·s 𝑐 ) = ( ( 2s ↑s 𝑤 ) ·s ( 2s ·s 𝑐 ) ) )
81 74 80 eqtrd ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( ( 2s ↑s ( 𝑤 +s 1s ) ) ·s 𝑐 ) = ( ( 2s ↑s 𝑤 ) ·s ( 2s ·s 𝑐 ) ) )
82 81 oveq1d ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( ( ( 2s ↑s ( 𝑤 +s 1s ) ) ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ↑s 𝑤 ) ·s ( 2s ·s 𝑐 ) ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) )
83 peano2n0s ⊢ ( 𝑤 ∈ ℕ0s → ( 𝑤 +s 1s ) ∈ ℕ0s )
84 83 adantr ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( 𝑤 +s 1s ) ∈ ℕ0s )
85 79 84 pw2divscan3d ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( ( ( 2s ↑s ( 𝑤 +s 1s ) ) ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = 𝑐 )
86 77 79 mulscld ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( 2s ·s 𝑐 ) ∈ No )
87 expscl ⊢ ( ( 2s ∈ No ∧ ( 𝑤 +s 1s ) ∈ ℕ0s ) → ( 2s ↑s ( 𝑤 +s 1s ) ) ∈ No )
88 3 84 87 sylancr ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( 2s ↑s ( 𝑤 +s 1s ) ) ∈ No )
89 2ne0s ⊢ 2s ≠ 0s
90 expsne0 ⊢ ( ( 2s ∈ No ∧ 2s ≠ 0s ∧ ( 𝑤 +s 1s ) ∈ ℕ0s ) → ( 2s ↑s ( 𝑤 +s 1s ) ) ≠ 0s )
91 3 89 84 90 mp3an12i ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( 2s ↑s ( 𝑤 +s 1s ) ) ≠ 0s )
92 pw2recs ⊢ ( ( 𝑤 +s 1s ) ∈ ℕ0s → ∃ 𝑥 ∈ No ( ( 2s ↑s ( 𝑤 +s 1s ) ) ·s 𝑥 ) = 1s )
93 84 92 syl ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ∃ 𝑥 ∈ No ( ( 2s ↑s ( 𝑤 +s 1s ) ) ·s 𝑥 ) = 1s )
94 76 86 88 91 93 divsasswd ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( ( ( 2s ↑s 𝑤 ) ·s ( 2s ·s 𝑐 ) ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( 2s ↑s 𝑤 ) ·s ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ) )
95 82 85 94 3eqtr3rd ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( ( 2s ↑s 𝑤 ) ·s ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ) = 𝑐 )
96 86 84 pw2divscld ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ No )
97 79 96 71 pw2divmulsd ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( ( 𝑐 /su ( 2s ↑s 𝑤 ) ) = ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ↔ ( ( 2s ↑s 𝑤 ) ·s ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ) = 𝑐 ) )
98 95 97 mpbird ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( 𝑐 /su ( 2s ↑s 𝑤 ) ) = ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) )
99 98 eqcomd ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( 𝑐 /su ( 2s ↑s 𝑤 ) ) )
100 99 eleq1d ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ↔ ( 𝑐 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ) )
101 99 eqeq1d ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ↔ ( 𝑐 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) )
102 101 2rexbidv ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ↔ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( 𝑐 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) )
103 100 102 orbi12d ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( ( ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ∨ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) ↔ ( ( 𝑐 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ∨ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( 𝑐 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) ) )
104 103 adantlr ⊢ ( ( ( 𝑤 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ) ∧ 𝑐 ∈ ℤs ) → ( ( ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ∨ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) ↔ ( ( 𝑐 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ∨ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( 𝑐 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) ) )
105 70 104 mpbird ⊢ ( ( ( 𝑤 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ) ∧ 𝑐 ∈ ℤs ) → ( ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ∨ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) )
106 oveq1 ⊢ ( 𝑏 = ( 2s ·s 𝑐 ) → ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) )
107 106 eleq1d ⊢ ( 𝑏 = ( 2s ·s 𝑐 ) → ( ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ↔ ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ) )
108 106 eqeq1d ⊢ ( 𝑏 = ( 2s ·s 𝑐 ) → ( ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ↔ ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) )
109 108 2rexbidv ⊢ ( 𝑏 = ( 2s ·s 𝑐 ) → ( ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ↔ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) )
110 107 109 orbi12d ⊢ ( 𝑏 = ( 2s ·s 𝑐 ) → ( ( ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ∨ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) ↔ ( ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ∨ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) ) )
111 105 110 syl5ibrcom ⊢ ( ( ( 𝑤 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ) ∧ 𝑐 ∈ ℤs ) → ( 𝑏 = ( 2s ·s 𝑐 ) → ( ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ∨ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) ) )
112 111 rexlimdva ⊢ ( ( 𝑤 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ) → ( ∃ 𝑐 ∈ ℤs 𝑏 = ( 2s ·s 𝑐 ) → ( ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ∨ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) ) )
113 oveq2 ⊢ ( 𝑝 = 𝑐 → ( 2s ·s 𝑝 ) = ( 2s ·s 𝑐 ) )
114 113 oveq1d ⊢ ( 𝑝 = 𝑐 → ( ( 2s ·s 𝑝 ) +s 1s ) = ( ( 2s ·s 𝑐 ) +s 1s ) )
115 114 oveq1d ⊢ ( 𝑝 = 𝑐 → ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) = ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) )
116 115 eqeq2d ⊢ ( 𝑝 = 𝑐 → ( ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ↔ ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) )
117 oveq2 ⊢ ( 𝑞 = ( 𝑤 +s 1s ) → ( 2s ↑s 𝑞 ) = ( 2s ↑s ( 𝑤 +s 1s ) ) )
118 117 oveq2d ⊢ ( 𝑞 = ( 𝑤 +s 1s ) → ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) = ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) )
119 118 eqeq2d ⊢ ( 𝑞 = ( 𝑤 +s 1s ) → ( ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ↔ ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ) )
120 simpr ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → 𝑐 ∈ ℤs )
121 n0p1nns ⊢ ( 𝑤 ∈ ℕ0s → ( 𝑤 +s 1s ) ∈ ℕs )
122 121 adantr ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( 𝑤 +s 1s ) ∈ ℕs )
123 eqidd ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) )
124 116 119 120 122 123 2rspcedvdw ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) )
125 124 olcd ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ∨ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) )
126 125 adantlr ⊢ ( ( ( 𝑤 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ) ∧ 𝑐 ∈ ℤs ) → ( ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ∨ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) )
127 oveq1 ⊢ ( 𝑏 = ( ( 2s ·s 𝑐 ) +s 1s ) → ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) )
128 127 eleq1d ⊢ ( 𝑏 = ( ( 2s ·s 𝑐 ) +s 1s ) → ( ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ↔ ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ) )
129 127 eqeq1d ⊢ ( 𝑏 = ( ( 2s ·s 𝑐 ) +s 1s ) → ( ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ↔ ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) )
130 129 2rexbidv ⊢ ( 𝑏 = ( ( 2s ·s 𝑐 ) +s 1s ) → ( ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ↔ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) )
131 128 130 orbi12d ⊢ ( 𝑏 = ( ( 2s ·s 𝑐 ) +s 1s ) → ( ( ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ∨ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) ↔ ( ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ∨ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) ) )
132 126 131 syl5ibrcom ⊢ ( ( ( 𝑤 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ) ∧ 𝑐 ∈ ℤs ) → ( 𝑏 = ( ( 2s ·s 𝑐 ) +s 1s ) → ( ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ∨ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) ) )
133 132 rexlimdva ⊢ ( ( 𝑤 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ) → ( ∃ 𝑐 ∈ ℤs 𝑏 = ( ( 2s ·s 𝑐 ) +s 1s ) → ( ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ∨ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) ) )
134 112 133 jaod ⊢ ( ( 𝑤 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ) → ( ( ∃ 𝑐 ∈ ℤs 𝑏 = ( 2s ·s 𝑐 ) ∨ ∃ 𝑐 ∈ ℤs 𝑏 = ( ( 2s ·s 𝑐 ) +s 1s ) ) → ( ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ∨ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) ) )
135 56 134 syl5 ⊢ ( ( 𝑤 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ) → ( 𝑏 ∈ ℤs → ( ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ∨ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) ) )
136 135 ralrimiv ⊢ ( ( 𝑤 ∈ ℕ0s ∧ ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ) → ∀ 𝑏 ∈ ℤs ( ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ∨ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) )
137 136 ex ⊢ ( 𝑤 ∈ ℕ0s → ( ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) → ∀ 𝑏 ∈ ℤs ( ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ∨ ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) ) )
138 12 19 42 49 55 137 n0sind ⊢ ( 𝑏 ∈ ℕ0s → ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su ( 2s ↑s 𝑏 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑏 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )
139 rsp ⊢ ( ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su ( 2s ↑s 𝑏 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑏 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) → ( 𝑎 ∈ ℤs → ( ( 𝑎 /su ( 2s ↑s 𝑏 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑏 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ) )
140 138 139 syl ⊢ ( 𝑏 ∈ ℕ0s → ( 𝑎 ∈ ℤs → ( ( 𝑎 /su ( 2s ↑s 𝑏 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑏 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ) )
141 140 impcom ⊢ ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℕ0s ) → ( ( 𝑎 /su ( 2s ↑s 𝑏 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑏 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )
142 eleq1 ⊢ ( 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑏 ) ) → ( 𝐴 ∈ ℤs ↔ ( 𝑎 /su ( 2s ↑s 𝑏 ) ) ∈ ℤs ) )
143 eqeq1 ⊢ ( 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑏 ) ) → ( 𝐴 = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ↔ ( 𝑎 /su ( 2s ↑s 𝑏 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )
144 143 2rexbidv ⊢ ( 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑏 ) ) → ( ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs 𝐴 = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ↔ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑏 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )
145 142 144 orbi12d ⊢ ( 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑏 ) ) → ( ( 𝐴 ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs 𝐴 = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ↔ ( ( 𝑎 /su ( 2s ↑s 𝑏 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑏 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ) )
146 141 145 syl5ibrcom ⊢ ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℕ0s ) → ( 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑏 ) ) → ( 𝐴 ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs 𝐴 = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ) )
147 146 rexlimivv ⊢ ( ∃ 𝑎 ∈ ℤs ∃ 𝑏 ∈ ℕ0s 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑏 ) ) → ( 𝐴 ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs 𝐴 = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )
148 1 147 sylbi ⊢ ( 𝐴 ∈ ℤs[1/2] → ( 𝐴 ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs 𝐴 = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )