Metamath Proof Explorer

Theorem z12sge0

Description: An expression for non-negative dyadic rationals. (Contributed by Scott Fenton, 8-Nov-2025)

Ref Expression
Assertion z12sge0 ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) → ( 𝐴 ∈ ℤs[1/2] ↔ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) ) )

Proof

Step Hyp Ref Expression
1 simprl ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝑧 ∈ ℤs ∧ 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) ) ) → 𝑧 ∈ ℤs )
2 simpllr ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝑧 ∈ ℤs ∧ 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) ) ) → 0s ≤s 𝐴 )
3 simprr ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝑧 ∈ ℤs ∧ 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) ) ) → 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) )
4 2 3 breqtrd ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝑧 ∈ ℤs ∧ 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) ) ) → 0s ≤s ( 𝑧 /su ( 2s ↑s 𝑝 ) ) )
5 1 znod ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝑧 ∈ ℤs ∧ 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) ) ) → 𝑧 ∈ No )
6 simplr ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝑧 ∈ ℤs ∧ 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) ) ) → 𝑝 ∈ ℕ0s )
7 5 6 pw2ge0divsd ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝑧 ∈ ℤs ∧ 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) ) ) → ( 0s ≤s 𝑧 ↔ 0s ≤s ( 𝑧 /su ( 2s ↑s 𝑝 ) ) ) )
8 4 7 mpbird ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝑧 ∈ ℤs ∧ 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) ) ) → 0s ≤s 𝑧 )
9 eln0zs ⊢ ( 𝑧 ∈ ℕ0s ↔ ( 𝑧 ∈ ℤs ∧ 0s ≤s 𝑧 ) )
10 1 8 9 sylanbrc ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝑧 ∈ ℤs ∧ 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) ) ) → 𝑧 ∈ ℕ0s )
11 simpr ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑧 ∈ ℕ0s ) → 𝑧 ∈ ℕ0s )
12 2nns ⊢ 2s ∈ ℕs
13 simplr ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑧 ∈ ℕ0s ) → 𝑝 ∈ ℕ0s )
14 nnexpscl ⊢ ( ( 2s ∈ ℕs ∧ 𝑝 ∈ ℕ0s ) → ( 2s ↑s 𝑝 ) ∈ ℕs )
15 12 13 14 sylancr ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑧 ∈ ℕ0s ) → ( 2s ↑s 𝑝 ) ∈ ℕs )
16 eucliddivs ⊢ ( ( 𝑧 ∈ ℕ0s ∧ ( 2s ↑s 𝑝 ) ∈ ℕs ) → ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ( 𝑧 = ( ( ( 2s ↑s 𝑝 ) ·s 𝑥 ) +s 𝑦 ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) )
17 11 15 16 syl2anc ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑧 ∈ ℕ0s ) → ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ( 𝑧 = ( ( ( 2s ↑s 𝑝 ) ·s 𝑥 ) +s 𝑦 ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) )
18 2no ⊢ 2s ∈ No
19 simpllr ⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑧 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → 𝑝 ∈ ℕ0s )
20 expscl ⊢ ( ( 2s ∈ No ∧ 𝑝 ∈ ℕ0s ) → ( 2s ↑s 𝑝 ) ∈ No )
21 18 19 20 sylancr ⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑧 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → ( 2s ↑s 𝑝 ) ∈ No )
22 simprl ⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑧 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → 𝑥 ∈ ℕ0s )
23 22 n0nod ⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑧 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → 𝑥 ∈ No )
24 simprr ⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑧 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → 𝑦 ∈ ℕ0s )
25 24 n0nod ⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑧 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → 𝑦 ∈ No )
26 25 19 pw2divscld ⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑧 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ∈ No )
27 21 23 26 addsdid ⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑧 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → ( ( 2s ↑s 𝑝 ) ·s ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) = ( ( ( 2s ↑s 𝑝 ) ·s 𝑥 ) +s ( ( 2s ↑s 𝑝 ) ·s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) )
28 25 19 pw2divscan2d ⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑧 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → ( ( 2s ↑s 𝑝 ) ·s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) = 𝑦 )
29 28 oveq2d ⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑧 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → ( ( ( 2s ↑s 𝑝 ) ·s 𝑥 ) +s ( ( 2s ↑s 𝑝 ) ·s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) = ( ( ( 2s ↑s 𝑝 ) ·s 𝑥 ) +s 𝑦 ) )
30 27 29 eqtrd ⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑧 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → ( ( 2s ↑s 𝑝 ) ·s ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) = ( ( ( 2s ↑s 𝑝 ) ·s 𝑥 ) +s 𝑦 ) )
31 30 eqeq2d ⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑧 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → ( 𝑧 = ( ( 2s ↑s 𝑝 ) ·s ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) ↔ 𝑧 = ( ( ( 2s ↑s 𝑝 ) ·s 𝑥 ) +s 𝑦 ) ) )
32 eqcom ⊢ ( 𝑧 = ( ( 2s ↑s 𝑝 ) ·s ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) ↔ ( ( 2s ↑s 𝑝 ) ·s ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) = 𝑧 )
33 31 32 bitr3di ⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑧 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → ( 𝑧 = ( ( ( 2s ↑s 𝑝 ) ·s 𝑥 ) +s 𝑦 ) ↔ ( ( 2s ↑s 𝑝 ) ·s ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) = 𝑧 ) )
34 simplr ⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑧 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → 𝑧 ∈ ℕ0s )
35 34 n0nod ⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑧 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → 𝑧 ∈ No )
36 23 26 addscld ⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑧 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∈ No )
37 35 36 19 pw2divmulsd ⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑧 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → ( ( 𝑧 /su ( 2s ↑s 𝑝 ) ) = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ↔ ( ( 2s ↑s 𝑝 ) ·s ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) = 𝑧 ) )
38 33 37 bitr4d ⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑧 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → ( 𝑧 = ( ( ( 2s ↑s 𝑝 ) ·s 𝑥 ) +s 𝑦 ) ↔ ( 𝑧 /su ( 2s ↑s 𝑝 ) ) = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) )
39 38 anbi1d ⊢ ( ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑧 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → ( ( 𝑧 = ( ( ( 2s ↑s 𝑝 ) ·s 𝑥 ) +s 𝑦 ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) ↔ ( ( 𝑧 /su ( 2s ↑s 𝑝 ) ) = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) ) )
40 39 2rexbidva ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑧 ∈ ℕ0s ) → ( ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ( 𝑧 = ( ( ( 2s ↑s 𝑝 ) ·s 𝑥 ) +s 𝑦 ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) ↔ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ( ( 𝑧 /su ( 2s ↑s 𝑝 ) ) = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) ) )
41 17 40 mpbid ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑧 ∈ ℕ0s ) → ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ( ( 𝑧 /su ( 2s ↑s 𝑝 ) ) = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) )
42 41 adantrl ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) ∧ 𝑧 ∈ ℕ0s ) ) → ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ( ( 𝑧 /su ( 2s ↑s 𝑝 ) ) = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) )
43 simprl ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) ∧ 𝑧 ∈ ℕ0s ) ) → 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) )
44 43 eqeq1d ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) ∧ 𝑧 ∈ ℕ0s ) ) → ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ↔ ( 𝑧 /su ( 2s ↑s 𝑝 ) ) = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) )
45 44 anbi1d ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) ∧ 𝑧 ∈ ℕ0s ) ) → ( ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) ↔ ( ( 𝑧 /su ( 2s ↑s 𝑝 ) ) = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) ) )
46 45 2rexbidv ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) ∧ 𝑧 ∈ ℕ0s ) ) → ( ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) ↔ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ( ( 𝑧 /su ( 2s ↑s 𝑝 ) ) = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) ) )
47 42 46 mpbird ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) ∧ 𝑧 ∈ ℕ0s ) ) → ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) )
48 47 expr ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) ) → ( 𝑧 ∈ ℕ0s → ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) ) )
49 48 adantrl ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝑧 ∈ ℤs ∧ 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) ) ) → ( 𝑧 ∈ ℕ0s → ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) ) )
50 10 49 mpd ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝑧 ∈ ℤs ∧ 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) ) ) → ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) )
51 50 rexlimdvaa ⊢ ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) → ( ∃ 𝑧 ∈ ℤs 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) → ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) ) )
52 oveq1 ⊢ ( 𝑧 = ( ( ( 2s ↑s 𝑝 ) ·s 𝑥 ) +s 𝑦 ) → ( 𝑧 /su ( 2s ↑s 𝑝 ) ) = ( ( ( ( 2s ↑s 𝑝 ) ·s 𝑥 ) +s 𝑦 ) /su ( 2s ↑s 𝑝 ) ) )
53 52 eqeq2d ⊢ ( 𝑧 = ( ( ( 2s ↑s 𝑝 ) ·s 𝑥 ) +s 𝑦 ) → ( ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) ↔ ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) = ( ( ( ( 2s ↑s 𝑝 ) ·s 𝑥 ) +s 𝑦 ) /su ( 2s ↑s 𝑝 ) ) ) )
54 nnn0s ⊢ ( 2s ∈ ℕs → 2s ∈ ℕ0s )
55 12 54 ax-mp ⊢ 2s ∈ ℕ0s
56 simplr ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → 𝑝 ∈ ℕ0s )
57 n0expscl ⊢ ( ( 2s ∈ ℕ0s ∧ 𝑝 ∈ ℕ0s ) → ( 2s ↑s 𝑝 ) ∈ ℕ0s )
58 55 56 57 sylancr ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → ( 2s ↑s 𝑝 ) ∈ ℕ0s )
59 simprl ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → 𝑥 ∈ ℕ0s )
60 n0mulscl ⊢ ( ( ( 2s ↑s 𝑝 ) ∈ ℕ0s ∧ 𝑥 ∈ ℕ0s ) → ( ( 2s ↑s 𝑝 ) ·s 𝑥 ) ∈ ℕ0s )
61 58 59 60 syl2anc ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → ( ( 2s ↑s 𝑝 ) ·s 𝑥 ) ∈ ℕ0s )
62 simprr ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → 𝑦 ∈ ℕ0s )
63 n0addscl ⊢ ( ( ( ( 2s ↑s 𝑝 ) ·s 𝑥 ) ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) → ( ( ( 2s ↑s 𝑝 ) ·s 𝑥 ) +s 𝑦 ) ∈ ℕ0s )
64 61 62 63 syl2anc ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → ( ( ( 2s ↑s 𝑝 ) ·s 𝑥 ) +s 𝑦 ) ∈ ℕ0s )
65 64 n0zsd ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → ( ( ( 2s ↑s 𝑝 ) ·s 𝑥 ) +s 𝑦 ) ∈ ℤs )
66 59 n0nod ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → 𝑥 ∈ No )
67 66 56 pw2divscan3d ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → ( ( ( 2s ↑s 𝑝 ) ·s 𝑥 ) /su ( 2s ↑s 𝑝 ) ) = 𝑥 )
68 67 eqcomd ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → 𝑥 = ( ( ( 2s ↑s 𝑝 ) ·s 𝑥 ) /su ( 2s ↑s 𝑝 ) ) )
69 68 oveq1d ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) = ( ( ( ( 2s ↑s 𝑝 ) ·s 𝑥 ) /su ( 2s ↑s 𝑝 ) ) +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) )
70 18 56 20 sylancr ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → ( 2s ↑s 𝑝 ) ∈ No )
71 70 66 mulscld ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → ( ( 2s ↑s 𝑝 ) ·s 𝑥 ) ∈ No )
72 62 n0nod ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → 𝑦 ∈ No )
73 71 72 56 pw2divsdird ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → ( ( ( ( 2s ↑s 𝑝 ) ·s 𝑥 ) +s 𝑦 ) /su ( 2s ↑s 𝑝 ) ) = ( ( ( ( 2s ↑s 𝑝 ) ·s 𝑥 ) /su ( 2s ↑s 𝑝 ) ) +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) )
74 69 73 eqtr4d ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) = ( ( ( ( 2s ↑s 𝑝 ) ·s 𝑥 ) +s 𝑦 ) /su ( 2s ↑s 𝑝 ) ) )
75 53 65 74 rspcedvdw ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → ∃ 𝑧 ∈ ℤs ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) )
76 eqeq1 ⊢ ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) → ( 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) ↔ ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) ) )
77 76 rexbidv ⊢ ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) → ( ∃ 𝑧 ∈ ℤs 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) ↔ ∃ 𝑧 ∈ ℤs ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) ) )
78 75 77 syl5ibrcom ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) → ∃ 𝑧 ∈ ℤs 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) ) )
79 78 adantrd ⊢ ( ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) ∧ ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ) → ( ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) → ∃ 𝑧 ∈ ℤs 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) ) )
80 79 rexlimdvva ⊢ ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) → ( ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) → ∃ 𝑧 ∈ ℤs 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) ) )
81 51 80 impbid ⊢ ( ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) ∧ 𝑝 ∈ ℕ0s ) → ( ∃ 𝑧 ∈ ℤs 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) ↔ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) ) )
82 81 rexbidva ⊢ ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) → ( ∃ 𝑝 ∈ ℕ0s ∃ 𝑧 ∈ ℤs 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) ↔ ∃ 𝑝 ∈ ℕ0s ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) ) )
83 elz12s ⊢ ( 𝐴 ∈ ℤs[1/2] ↔ ∃ 𝑧 ∈ ℤs ∃ 𝑝 ∈ ℕ0s 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) )
84 rexcom ⊢ ( ∃ 𝑧 ∈ ℤs ∃ 𝑝 ∈ ℕ0s 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) ↔ ∃ 𝑝 ∈ ℕ0s ∃ 𝑧 ∈ ℤs 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) )
85 83 84 bitri ⊢ ( 𝐴 ∈ ℤs[1/2] ↔ ∃ 𝑝 ∈ ℕ0s ∃ 𝑧 ∈ ℤs 𝐴 = ( 𝑧 /su ( 2s ↑s 𝑝 ) ) )
86 rexcom ⊢ ( ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) ↔ ∃ 𝑝 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) )
87 86 rexbii ⊢ ( ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) ↔ ∃ 𝑥 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) )
88 rexcom ⊢ ( ∃ 𝑥 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) ↔ ∃ 𝑝 ∈ ℕ0s ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) )
89 87 88 bitri ⊢ ( ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) ↔ ∃ 𝑝 ∈ ℕ0s ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) )
90 82 85 89 3bitr4g ⊢ ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) → ( 𝐴 ∈ ℤs[1/2] ↔ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) ) )