Metamath Proof Explorer

Theorem bdayfinlem

Description: Lemma for bdayfin . Handle the non-negative case. (Contributed by Scott Fenton, 26-Feb-2026)

Ref Expression
Assertion bdayfinlem ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ∧ ( bday ‘ 𝐴 ) ∈ ω ) → 𝐴 ∈ ℤs[1/2] )

Proof

Step Hyp Ref Expression
1 bdayn0sf1o ⊢ ( bday ↾ ℕ0s ) : ℕ0s –1-1-onto→ ω
2 f1ocnvdm ⊢ ( ( ( bday ↾ ℕ0s ) : ℕ0s –1-1-onto→ ω ∧ ( bday ‘ 𝐴 ) ∈ ω ) → ( ◡ ( bday ↾ ℕ0s ) ‘ ( bday ‘ 𝐴 ) ) ∈ ℕ0s )
3 1 2 mpan ⊢ ( ( bday ‘ 𝐴 ) ∈ ω → ( ◡ ( bday ↾ ℕ0s ) ‘ ( bday ‘ 𝐴 ) ) ∈ ℕ0s )
4 3 3ad2ant3 ⊢ ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ∧ ( bday ‘ 𝐴 ) ∈ ω ) → ( ◡ ( bday ↾ ℕ0s ) ‘ ( bday ‘ 𝐴 ) ) ∈ ℕ0s )
5 4 n0zsd ⊢ ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ∧ ( bday ‘ 𝐴 ) ∈ ω ) → ( ◡ ( bday ↾ ℕ0s ) ‘ ( bday ‘ 𝐴 ) ) ∈ ℤs )
6 zzs12 ⊢ ( ( ◡ ( bday ↾ ℕ0s ) ‘ ( bday ‘ 𝐴 ) ) ∈ ℤs → ( ◡ ( bday ↾ ℕ0s ) ‘ ( bday ‘ 𝐴 ) ) ∈ ℤs[1/2] )
7 5 6 syl ⊢ ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ∧ ( bday ‘ 𝐴 ) ∈ ω ) → ( ◡ ( bday ↾ ℕ0s ) ‘ ( bday ‘ 𝐴 ) ) ∈ ℤs[1/2] )
8 eleq1 ⊢ ( 𝐴 = ( ◡ ( bday ↾ ℕ0s ) ‘ ( bday ‘ 𝐴 ) ) → ( 𝐴 ∈ ℤs[1/2] ↔ ( ◡ ( bday ↾ ℕ0s ) ‘ ( bday ‘ 𝐴 ) ) ∈ ℤs[1/2] ) )
9 7 8 syl5ibrcom ⊢ ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ∧ ( bday ‘ 𝐴 ) ∈ ω ) → ( 𝐴 = ( ◡ ( bday ↾ ℕ0s ) ‘ ( bday ‘ 𝐴 ) ) → 𝐴 ∈ ℤs[1/2] ) )
10 n0zs ⊢ ( 𝑥 ∈ ℕ0s → 𝑥 ∈ ℤs )
11 zzs12 ⊢ ( 𝑥 ∈ ℤs → 𝑥 ∈ ℤs[1/2] )
12 10 11 syl ⊢ ( 𝑥 ∈ ℕ0s → 𝑥 ∈ ℤs[1/2] )
13 12 adantr ⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) → 𝑥 ∈ ℤs[1/2] )
14 n0zs ⊢ ( 𝑦 ∈ ℕ0s → 𝑦 ∈ ℤs )
15 elzs12i ⊢ ( ( 𝑦 ∈ ℤs ∧ 𝑧 ∈ ℕ0s ) → ( 𝑦 /su ( 2s ↑s 𝑧 ) ) ∈ ℤs[1/2] )
16 14 15 sylan ⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝑧 ∈ ℕ0s ) → ( 𝑦 /su ( 2s ↑s 𝑧 ) ) ∈ ℤs[1/2] )
17 16 adantll ⊢ ( ( ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ∧ 𝑧 ∈ ℕ0s ) → ( 𝑦 /su ( 2s ↑s 𝑧 ) ) ∈ ℤs[1/2] )
18 zs12addscl ⊢ ( ( 𝑥 ∈ ℤs[1/2] ∧ ( 𝑦 /su ( 2s ↑s 𝑧 ) ) ∈ ℤs[1/2] ) → ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑧 ) ) ) ∈ ℤs[1/2] )
19 13 17 18 syl2an2r ⊢ ( ( ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ∧ 𝑧 ∈ ℕ0s ) → ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑧 ) ) ) ∈ ℤs[1/2] )
20 eleq1 ⊢ ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑧 ) ) ) → ( 𝐴 ∈ ℤs[1/2] ↔ ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑧 ) ) ) ∈ ℤs[1/2] ) )
21 20 3ad2ant1 ⊢ ( ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑧 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑧 ) ∧ ( 𝑥 +s 𝑧 ) <s ( ◡ ( bday ↾ ℕ0s ) ‘ ( bday ‘ 𝐴 ) ) ) → ( 𝐴 ∈ ℤs[1/2] ↔ ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑧 ) ) ) ∈ ℤs[1/2] ) )
22 19 21 syl5ibrcom ⊢ ( ( ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ∧ 𝑧 ∈ ℕ0s ) → ( ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑧 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑧 ) ∧ ( 𝑥 +s 𝑧 ) <s ( ◡ ( bday ↾ ℕ0s ) ‘ ( bday ‘ 𝐴 ) ) ) → 𝐴 ∈ ℤs[1/2] ) )
23 22 rexlimdva ⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) → ( ∃ 𝑧 ∈ ℕ0s ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑧 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑧 ) ∧ ( 𝑥 +s 𝑧 ) <s ( ◡ ( bday ↾ ℕ0s ) ‘ ( bday ‘ 𝐴 ) ) ) → 𝐴 ∈ ℤs[1/2] ) )
24 23 rexlimivv ⊢ ( ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑧 ∈ ℕ0s ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑧 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑧 ) ∧ ( 𝑥 +s 𝑧 ) <s ( ◡ ( bday ↾ ℕ0s ) ‘ ( bday ‘ 𝐴 ) ) ) → 𝐴 ∈ ℤs[1/2] )
25 24 a1i ⊢ ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ∧ ( bday ‘ 𝐴 ) ∈ ω ) → ( ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑧 ∈ ℕ0s ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑧 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑧 ) ∧ ( 𝑥 +s 𝑧 ) <s ( ◡ ( bday ↾ ℕ0s ) ‘ ( bday ‘ 𝐴 ) ) ) → 𝐴 ∈ ℤs[1/2] ) )
26 simp1 ⊢ ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ∧ ( bday ‘ 𝐴 ) ∈ ω ) → 𝐴 ∈ No )
27 4 fvresd ⊢ ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ∧ ( bday ‘ 𝐴 ) ∈ ω ) → ( ( bday ↾ ℕ0s ) ‘ ( ◡ ( bday ↾ ℕ0s ) ‘ ( bday ‘ 𝐴 ) ) ) = ( bday ‘ ( ◡ ( bday ↾ ℕ0s ) ‘ ( bday ‘ 𝐴 ) ) ) )
28 f1ocnvfv2 ⊢ ( ( ( bday ↾ ℕ0s ) : ℕ0s –1-1-onto→ ω ∧ ( bday ‘ 𝐴 ) ∈ ω ) → ( ( bday ↾ ℕ0s ) ‘ ( ◡ ( bday ↾ ℕ0s ) ‘ ( bday ‘ 𝐴 ) ) ) = ( bday ‘ 𝐴 ) )
29 1 28 mpan ⊢ ( ( bday ‘ 𝐴 ) ∈ ω → ( ( bday ↾ ℕ0s ) ‘ ( ◡ ( bday ↾ ℕ0s ) ‘ ( bday ‘ 𝐴 ) ) ) = ( bday ‘ 𝐴 ) )
30 29 3ad2ant3 ⊢ ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ∧ ( bday ‘ 𝐴 ) ∈ ω ) → ( ( bday ↾ ℕ0s ) ‘ ( ◡ ( bday ↾ ℕ0s ) ‘ ( bday ‘ 𝐴 ) ) ) = ( bday ‘ 𝐴 ) )
31 27 30 eqtr3d ⊢ ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ∧ ( bday ‘ 𝐴 ) ∈ ω ) → ( bday ‘ ( ◡ ( bday ↾ ℕ0s ) ‘ ( bday ‘ 𝐴 ) ) ) = ( bday ‘ 𝐴 ) )
32 31 eqimsscd ⊢ ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ∧ ( bday ‘ 𝐴 ) ∈ ω ) → ( bday ‘ 𝐴 ) ⊆ ( bday ‘ ( ◡ ( bday ↾ ℕ0s ) ‘ ( bday ‘ 𝐴 ) ) ) )
33 simp2 ⊢ ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ∧ ( bday ‘ 𝐴 ) ∈ ω ) → 0s ≤s 𝐴 )
34 4 26 32 33 bdayfinbnd ⊢ ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ∧ ( bday ‘ 𝐴 ) ∈ ω ) → ( 𝐴 = ( ◡ ( bday ↾ ℕ0s ) ‘ ( bday ‘ 𝐴 ) ) ∨ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑧 ∈ ℕ0s ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑧 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑧 ) ∧ ( 𝑥 +s 𝑧 ) <s ( ◡ ( bday ↾ ℕ0s ) ‘ ( bday ‘ 𝐴 ) ) ) ) )
35 9 25 34 mpjaod ⊢ ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ∧ ( bday ‘ 𝐴 ) ∈ ω ) → 𝐴 ∈ ℤs[1/2] )