Metamath Proof Explorer

Theorem z12bdaylem

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

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

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐴 ∈ ℤs[1/2] ∧ 0s ≤s 𝐴 ) → 𝐴 ∈ ℤs[1/2] )
2 z12no ⊢ ( 𝐴 ∈ ℤs[1/2] → 𝐴 ∈ No )
3 z12sge0 ⊢ ( ( 𝐴 ∈ No ∧ 0s ≤s 𝐴 ) → ( 𝐴 ∈ ℤs[1/2] ↔ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) ) )
4 2 3 sylan ⊢ ( ( 𝐴 ∈ ℤs[1/2] ∧ 0s ≤s 𝐴 ) → ( 𝐴 ∈ ℤs[1/2] ↔ ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) ) )
5 1 4 mpbid ⊢ ( ( 𝐴 ∈ ℤs[1/2] ∧ 0s ≤s 𝐴 ) → ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) )
6 simpl1 ⊢ ( ( ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) → 𝑥 ∈ ℕ0s )
7 6 n0nod ⊢ ( ( ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) → 𝑥 ∈ No )
8 simpl2 ⊢ ( ( ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) → 𝑦 ∈ ℕ0s )
9 8 n0nod ⊢ ( ( ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) → 𝑦 ∈ No )
10 simpl3 ⊢ ( ( ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) → 𝑝 ∈ ℕ0s )
11 9 10 pw2divscld ⊢ ( ( ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) → ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ∈ No )
12 addbday ⊢ ( ( 𝑥 ∈ No ∧ ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ∈ No ) → ( bday ‘ ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) )
13 7 11 12 syl2anc ⊢ ( ( ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) → ( bday ‘ ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) )
14 n0bday ⊢ ( 𝑥 ∈ ℕ0s → ( bday ‘ 𝑥 ) ∈ ω )
15 6 14 syl ⊢ ( ( ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) → ( bday ‘ 𝑥 ) ∈ ω )
16 simpr ⊢ ( ( ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) → 𝑦 <s ( 2s ↑s 𝑝 ) )
17 bdaypw2n0bnd ⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝑝 ∈ ℕ0s ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) → ( bday ‘ ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ⊆ suc ( bday ‘ 𝑝 ) )
18 8 10 16 17 syl3anc ⊢ ( ( ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) → ( bday ‘ ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ⊆ suc ( bday ‘ 𝑝 ) )
19 n0bday ⊢ ( 𝑝 ∈ ℕ0s → ( bday ‘ 𝑝 ) ∈ ω )
20 peano2 ⊢ ( ( bday ‘ 𝑝 ) ∈ ω → suc ( bday ‘ 𝑝 ) ∈ ω )
21 19 20 syl ⊢ ( 𝑝 ∈ ℕ0s → suc ( bday ‘ 𝑝 ) ∈ ω )
22 21 3ad2ant3 ⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ∧ 𝑝 ∈ ℕ0s ) → suc ( bday ‘ 𝑝 ) ∈ ω )
23 22 adantr ⊢ ( ( ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) → suc ( bday ‘ 𝑝 ) ∈ ω )
24 bdayon ⊢ ( bday ‘ ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∈ On
25 24 onordi ⊢ Ord ( bday ‘ ( 𝑦 /su ( 2s ↑s 𝑝 ) ) )
26 ordom ⊢ Ord ω
27 ordtr2 ⊢ ( ( Ord ( bday ‘ ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ Ord ω ) → ( ( ( bday ‘ ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ⊆ suc ( bday ‘ 𝑝 ) ∧ suc ( bday ‘ 𝑝 ) ∈ ω ) → ( bday ‘ ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∈ ω ) )
28 25 26 27 mp2an ⊢ ( ( ( bday ‘ ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ⊆ suc ( bday ‘ 𝑝 ) ∧ suc ( bday ‘ 𝑝 ) ∈ ω ) → ( bday ‘ ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∈ ω )
29 18 23 28 syl2anc ⊢ ( ( ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) → ( bday ‘ ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∈ ω )
30 omnaddcl ⊢ ( ( ( bday ‘ 𝑥 ) ∈ ω ∧ ( bday ‘ ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∈ ω ) → ( ( bday ‘ 𝑥 ) +no ( bday ‘ ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) ∈ ω )
31 15 29 30 syl2anc ⊢ ( ( ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) → ( ( bday ‘ 𝑥 ) +no ( bday ‘ ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) ∈ ω )
32 bdayon ⊢ ( bday ‘ ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) ∈ On
33 32 onordi ⊢ Ord ( bday ‘ ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) )
34 ordtr2 ⊢ ( ( Ord ( bday ‘ ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) ∧ Ord ω ) → ( ( ( bday ‘ ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) ∧ ( ( bday ‘ 𝑥 ) +no ( bday ‘ ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) ∈ ω ) → ( bday ‘ ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) ∈ ω ) )
35 33 26 34 mp2an ⊢ ( ( ( bday ‘ ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) ∧ ( ( bday ‘ 𝑥 ) +no ( bday ‘ ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) ∈ ω ) → ( bday ‘ ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) ∈ ω )
36 13 31 35 syl2anc ⊢ ( ( ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) → ( bday ‘ ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) ∈ ω )
37 fveq2 ⊢ ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) → ( bday ‘ 𝐴 ) = ( bday ‘ ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) )
38 37 eleq1d ⊢ ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) → ( ( bday ‘ 𝐴 ) ∈ ω ↔ ( bday ‘ ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ) ∈ ω ) )
39 36 38 syl5ibrcom ⊢ ( ( ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ∧ 𝑝 ∈ ℕ0s ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) → ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) → ( bday ‘ 𝐴 ) ∈ ω ) )
40 39 ex ⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ∧ 𝑝 ∈ ℕ0s ) → ( 𝑦 <s ( 2s ↑s 𝑝 ) → ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) → ( bday ‘ 𝐴 ) ∈ ω ) ) )
41 40 impcomd ⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ∧ 𝑝 ∈ ℕ0s ) → ( ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) → ( bday ‘ 𝐴 ) ∈ ω ) )
42 41 3expa ⊢ ( ( ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) ∧ 𝑝 ∈ ℕ0s ) → ( ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) → ( bday ‘ 𝐴 ) ∈ ω ) )
43 42 rexlimdva ⊢ ( ( 𝑥 ∈ ℕ0s ∧ 𝑦 ∈ ℕ0s ) → ( ∃ 𝑝 ∈ ℕ0s ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) → ( bday ‘ 𝐴 ) ∈ ω ) )
44 43 rexlimivv ⊢ ( ∃ 𝑥 ∈ ℕ0s ∃ 𝑦 ∈ ℕ0s ∃ 𝑝 ∈ ℕ0s ( 𝐴 = ( 𝑥 +s ( 𝑦 /su ( 2s ↑s 𝑝 ) ) ) ∧ 𝑦 <s ( 2s ↑s 𝑝 ) ) → ( bday ‘ 𝐴 ) ∈ ω )
45 5 44 syl ⊢ ( ( 𝐴 ∈ ℤs[1/2] ∧ 0s ≤s 𝐴 ) → ( bday ‘ 𝐴 ) ∈ ω )