Metamath Proof Explorer

Theorem zs12zodd

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 zs12zodd ( 𝐴 ∈ ℤs[1/2] → ( 𝐴 ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs 𝐴 = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 elzs12 ⊢ ( 𝐴 ∈ ℤs[1/2] ↔ ∃ 𝑎 ∈ ℤs ∃ 𝑏 ∈ ℕ0s 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑏 ) ) )
2 oveq2 ⊢ ( 𝑐 = 0s → ( 2s ↑s 𝑐 ) = ( 2s ↑s 0s ) )
3 2sno ⊢ 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 divs1 ⊢ ( 𝑎 ∈ No → ( 𝑎 /su 1s ) = 𝑎 )
52 50 51 syl ⊢ ( 𝑎 ∈ ℤs → ( 𝑎 /su 1s ) = 𝑎 )
53 id ⊢ ( 𝑎 ∈ ℤs → 𝑎 ∈ ℤs )
54 52 53 eqeltrd ⊢ ( 𝑎 ∈ ℤs → ( 𝑎 /su 1s ) ∈ ℤs )
55 54 orcd ⊢ ( 𝑎 ∈ ℤs → ( ( 𝑎 /su 1s ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su 1s ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )
56 55 rgen ⊢ ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su 1s ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su 1s ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) )
57 zseo ⊢ ( 𝑏 ∈ ℤs → ( ∃ 𝑐 ∈ ℤs 𝑏 = ( 2s ·s 𝑐 ) ∨ ∃ 𝑐 ∈ ℤs 𝑏 = ( ( 2s ·s 𝑐 ) +s 1s ) ) )
58 oveq1 ⊢ ( 𝑎 = 𝑐 → ( 𝑎 /su ( 2s ↑s 𝑤 ) ) = ( 𝑐 /su ( 2s ↑s 𝑤 ) ) )
59 58 eleq1d ⊢ ( 𝑎 = 𝑐 → ( ( 𝑎 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ↔ ( 𝑐 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ) )
60 58 eqeq1d ⊢ ( 𝑎 = 𝑐 → ( ( 𝑎 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ↔ ( 𝑐 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )
61 60 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 𝑦 ) ) ) )
62 59 61 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 𝑦 ) ) ) ) )
63 62 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 𝑦 ) ) ) ) )
64 63 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 𝑦 ) ) ) ) )
65 33 eqeq2d ⊢ ( 𝑥 = 𝑝 → ( ( 𝑐 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ↔ ( 𝑐 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )
66 36 eqeq2d ⊢ ( 𝑦 = 𝑞 → ( ( 𝑐 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ↔ ( 𝑐 /su ( 2s ↑s 𝑤 ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) ) )
67 65 66 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 𝑞 ) ) )
68 67 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 𝑞 ) ) ) )
69 64 68 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 𝑞 ) ) ) ) )
70 69 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 𝑞 ) ) ) )
71 70 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 𝑞 ) ) ) )
72 simpl ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → 𝑤 ∈ ℕ0s )
73 expsp1 ⊢ ( ( 2s ∈ No ∧ 𝑤 ∈ ℕ0s ) → ( 2s ↑s ( 𝑤 +s 1s ) ) = ( ( 2s ↑s 𝑤 ) ·s 2s ) )
74 3 72 73 sylancr ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( 2s ↑s ( 𝑤 +s 1s ) ) = ( ( 2s ↑s 𝑤 ) ·s 2s ) )
75 74 oveq1d ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( ( 2s ↑s ( 𝑤 +s 1s ) ) ·s 𝑐 ) = ( ( ( 2s ↑s 𝑤 ) ·s 2s ) ·s 𝑐 ) )
76 expscl ⊢ ( ( 2s ∈ No ∧ 𝑤 ∈ ℕ0s ) → ( 2s ↑s 𝑤 ) ∈ No )
77 3 72 76 sylancr ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( 2s ↑s 𝑤 ) ∈ No )
78 3 a1i ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → 2s ∈ No )
79 zno ⊢ ( 𝑐 ∈ ℤs → 𝑐 ∈ No )
80 79 adantl ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → 𝑐 ∈ No )
81 77 78 80 mulsassd ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( ( ( 2s ↑s 𝑤 ) ·s 2s ) ·s 𝑐 ) = ( ( 2s ↑s 𝑤 ) ·s ( 2s ·s 𝑐 ) ) )
82 75 81 eqtrd ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( ( 2s ↑s ( 𝑤 +s 1s ) ) ·s 𝑐 ) = ( ( 2s ↑s 𝑤 ) ·s ( 2s ·s 𝑐 ) ) )
83 82 oveq1d ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( ( ( 2s ↑s ( 𝑤 +s 1s ) ) ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ↑s 𝑤 ) ·s ( 2s ·s 𝑐 ) ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) )
84 peano2n0s ⊢ ( 𝑤 ∈ ℕ0s → ( 𝑤 +s 1s ) ∈ ℕ0s )
85 84 adantr ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( 𝑤 +s 1s ) ∈ ℕ0s )
86 80 85 pw2divscan3d ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( ( ( 2s ↑s ( 𝑤 +s 1s ) ) ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = 𝑐 )
87 78 80 mulscld ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( 2s ·s 𝑐 ) ∈ No )
88 expscl ⊢ ( ( 2s ∈ No ∧ ( 𝑤 +s 1s ) ∈ ℕ0s ) → ( 2s ↑s ( 𝑤 +s 1s ) ) ∈ No )
89 3 85 88 sylancr ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( 2s ↑s ( 𝑤 +s 1s ) ) ∈ No )
90 2ne0s ⊢ 2s ≠ 0s
91 expsne0 ⊢ ( ( 2s ∈ No ∧ 2s ≠ 0s ∧ ( 𝑤 +s 1s ) ∈ ℕ0s ) → ( 2s ↑s ( 𝑤 +s 1s ) ) ≠ 0s )
92 3 90 85 91 mp3an12i ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( 2s ↑s ( 𝑤 +s 1s ) ) ≠ 0s )
93 pw2recs ⊢ ( ( 𝑤 +s 1s ) ∈ ℕ0s → ∃ 𝑥 ∈ No ( ( 2s ↑s ( 𝑤 +s 1s ) ) ·s 𝑥 ) = 1s )
94 85 93 syl ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ∃ 𝑥 ∈ No ( ( 2s ↑s ( 𝑤 +s 1s ) ) ·s 𝑥 ) = 1s )
95 77 87 89 92 94 divsasswd ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( ( ( 2s ↑s 𝑤 ) ·s ( 2s ·s 𝑐 ) ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( 2s ↑s 𝑤 ) ·s ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ) )
96 83 86 95 3eqtr3rd ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( ( 2s ↑s 𝑤 ) ·s ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ) = 𝑐 )
97 87 85 pw2divscld ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ No )
98 80 97 72 pw2divsmuld ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( ( 𝑐 /su ( 2s ↑s 𝑤 ) ) = ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ↔ ( ( 2s ↑s 𝑤 ) ·s ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ) = 𝑐 ) )
99 96 98 mpbird ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( 𝑐 /su ( 2s ↑s 𝑤 ) ) = ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) )
100 99 eqcomd ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( 𝑐 /su ( 2s ↑s 𝑤 ) ) )
101 100 eleq1d ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ↔ ( 𝑐 /su ( 2s ↑s 𝑤 ) ) ∈ ℤs ) )
102 100 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 𝑞 ) ) ) )
103 102 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 𝑞 ) ) ) )
104 101 103 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 𝑞 ) ) ) ) )
105 104 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 𝑞 ) ) ) ) )
106 71 105 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 𝑞 ) ) ) )
107 oveq1 ⊢ ( 𝑏 = ( 2s ·s 𝑐 ) → ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) )
108 107 eleq1d ⊢ ( 𝑏 = ( 2s ·s 𝑐 ) → ( ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ↔ ( ( 2s ·s 𝑐 ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ) )
109 107 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 𝑞 ) ) ) )
110 109 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 𝑞 ) ) ) )
111 108 110 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 𝑞 ) ) ) ) )
112 106 111 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 𝑞 ) ) ) ) )
113 112 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 𝑞 ) ) ) ) )
114 oveq2 ⊢ ( 𝑝 = 𝑐 → ( 2s ·s 𝑝 ) = ( 2s ·s 𝑐 ) )
115 114 oveq1d ⊢ ( 𝑝 = 𝑐 → ( ( 2s ·s 𝑝 ) +s 1s ) = ( ( 2s ·s 𝑐 ) +s 1s ) )
116 115 oveq1d ⊢ ( 𝑝 = 𝑐 → ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) = ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) )
117 116 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 𝑞 ) ) ) )
118 oveq2 ⊢ ( 𝑞 = ( 𝑤 +s 1s ) → ( 2s ↑s 𝑞 ) = ( 2s ↑s ( 𝑤 +s 1s ) ) )
119 118 oveq2d ⊢ ( 𝑞 = ( 𝑤 +s 1s ) → ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) = ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) )
120 119 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 ) ) ) ) )
121 simpr ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → 𝑐 ∈ ℤs )
122 n0p1nns ⊢ ( 𝑤 ∈ ℕ0s → ( 𝑤 +s 1s ) ∈ ℕs )
123 122 adantr ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( 𝑤 +s 1s ) ∈ ℕs )
124 eqidd ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) )
125 117 120 121 123 124 2rspcedvdw ⊢ ( ( 𝑤 ∈ ℕ0s ∧ 𝑐 ∈ ℤs ) → ∃ 𝑝 ∈ ℤs ∃ 𝑞 ∈ ℕs ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑝 ) +s 1s ) /su ( 2s ↑s 𝑞 ) ) )
126 125 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 𝑞 ) ) ) )
127 126 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 𝑞 ) ) ) )
128 oveq1 ⊢ ( 𝑏 = ( ( 2s ·s 𝑐 ) +s 1s ) → ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) = ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) )
129 128 eleq1d ⊢ ( 𝑏 = ( ( 2s ·s 𝑐 ) +s 1s ) → ( ( 𝑏 /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ↔ ( ( ( 2s ·s 𝑐 ) +s 1s ) /su ( 2s ↑s ( 𝑤 +s 1s ) ) ) ∈ ℤs ) )
130 128 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 𝑞 ) ) ) )
131 130 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 𝑞 ) ) ) )
132 129 131 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 𝑞 ) ) ) ) )
133 127 132 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 𝑞 ) ) ) ) )
134 133 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 𝑞 ) ) ) ) )
135 113 134 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 𝑞 ) ) ) ) )
136 57 135 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 𝑞 ) ) ) ) )
137 136 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 𝑞 ) ) ) )
138 137 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 𝑞 ) ) ) ) )
139 12 19 42 49 56 138 n0sind ⊢ ( 𝑏 ∈ ℕ0s → ∀ 𝑎 ∈ ℤs ( ( 𝑎 /su ( 2s ↑s 𝑏 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑏 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )
140 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 𝑦 ) ) ) ) )
141 139 140 syl ⊢ ( 𝑏 ∈ ℕ0s → ( 𝑎 ∈ ℤs → ( ( 𝑎 /su ( 2s ↑s 𝑏 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑏 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ) )
142 141 impcom ⊢ ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℕ0s ) → ( ( 𝑎 /su ( 2s ↑s 𝑏 ) ) ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs ( 𝑎 /su ( 2s ↑s 𝑏 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )
143 eleq1 ⊢ ( 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑏 ) ) → ( 𝐴 ∈ ℤs ↔ ( 𝑎 /su ( 2s ↑s 𝑏 ) ) ∈ ℤs ) )
144 eqeq1 ⊢ ( 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑏 ) ) → ( 𝐴 = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ↔ ( 𝑎 /su ( 2s ↑s 𝑏 ) ) = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )
145 144 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 𝑦 ) ) ) )
146 143 145 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 𝑦 ) ) ) ) )
147 142 146 syl5ibrcom ⊢ ( ( 𝑎 ∈ ℤs ∧ 𝑏 ∈ ℕ0s ) → ( 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑏 ) ) → ( 𝐴 ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs 𝐴 = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) ) )
148 147 rexlimivv ⊢ ( ∃ 𝑎 ∈ ℤs ∃ 𝑏 ∈ ℕ0s 𝐴 = ( 𝑎 /su ( 2s ↑s 𝑏 ) ) → ( 𝐴 ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs 𝐴 = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )
149 1 148 sylbi ⊢ ( 𝐴 ∈ ℤs[1/2] → ( 𝐴 ∈ ℤs ∨ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕs 𝐴 = ( ( ( 2s ·s 𝑥 ) +s 1s ) /su ( 2s ↑s 𝑦 ) ) ) )