Metamath Proof Explorer

Theorem zs12bday

Description: A dyadic fraction has a finite birthday. (Contributed by Scott Fenton, 20-Aug-2025)

Ref Expression
Assertion zs12bday ( 𝐴 ∈ ℤs[1/2] → ( bday ‘ 𝐴 ) ∈ ω )

Proof

Step Hyp Ref Expression
1 elzs12 ⊢ ( 𝐴 ∈ ℤs[1/2] ↔ ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕ0s 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) )
2 fvoveq1 ⊢ ( 𝑧 = 𝑥 → ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑦 ) ) ) = ( bday ‘ ( 𝑥 /su ( 2s ↑s 𝑦 ) ) ) )
3 2 eleq1d ⊢ ( 𝑧 = 𝑥 → ( ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑦 ) ) ) ∈ ω ↔ ( bday ‘ ( 𝑥 /su ( 2s ↑s 𝑦 ) ) ) ∈ ω ) )
4 oveq2 ⊢ ( 𝑚 = 0s → ( 2s ↑s 𝑚 ) = ( 2s ↑s 0s ) )
5 2sno ⊢ 2s ∈ No
6 exps0 ⊢ ( 2s ∈ No → ( 2s ↑s 0s ) = 1s )
7 5 6 ax-mp ⊢ ( 2s ↑s 0s ) = 1s
8 4 7 eqtrdi ⊢ ( 𝑚 = 0s → ( 2s ↑s 𝑚 ) = 1s )
9 8 oveq2d ⊢ ( 𝑚 = 0s → ( 𝑧 /su ( 2s ↑s 𝑚 ) ) = ( 𝑧 /su 1s ) )
10 9 fveq2d ⊢ ( 𝑚 = 0s → ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑚 ) ) ) = ( bday ‘ ( 𝑧 /su 1s ) ) )
11 10 eleq1d ⊢ ( 𝑚 = 0s → ( ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑚 ) ) ) ∈ ω ↔ ( bday ‘ ( 𝑧 /su 1s ) ) ∈ ω ) )
12 11 ralbidv ⊢ ( 𝑚 = 0s → ( ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑚 ) ) ) ∈ ω ↔ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su 1s ) ) ∈ ω ) )
13 oveq2 ⊢ ( 𝑚 = 𝑛 → ( 2s ↑s 𝑚 ) = ( 2s ↑s 𝑛 ) )
14 13 oveq2d ⊢ ( 𝑚 = 𝑛 → ( 𝑧 /su ( 2s ↑s 𝑚 ) ) = ( 𝑧 /su ( 2s ↑s 𝑛 ) ) )
15 14 fveq2d ⊢ ( 𝑚 = 𝑛 → ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑚 ) ) ) = ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) )
16 15 eleq1d ⊢ ( 𝑚 = 𝑛 → ( ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑚 ) ) ) ∈ ω ↔ ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) )
17 16 ralbidv ⊢ ( 𝑚 = 𝑛 → ( ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑚 ) ) ) ∈ ω ↔ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) )
18 oveq2 ⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( 2s ↑s 𝑚 ) = ( 2s ↑s ( 𝑛 +s 1s ) ) )
19 18 oveq2d ⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( 𝑧 /su ( 2s ↑s 𝑚 ) ) = ( 𝑧 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
20 19 fveq2d ⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑚 ) ) ) = ( bday ‘ ( 𝑧 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
21 20 eleq1d ⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑚 ) ) ) ∈ ω ↔ ( bday ‘ ( 𝑧 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ ω ) )
22 21 ralbidv ⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑚 ) ) ) ∈ ω ↔ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ ω ) )
23 fvoveq1 ⊢ ( 𝑧 = 𝑤 → ( bday ‘ ( 𝑧 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) = ( bday ‘ ( 𝑤 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
24 23 eleq1d ⊢ ( 𝑧 = 𝑤 → ( ( bday ‘ ( 𝑧 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ ω ↔ ( bday ‘ ( 𝑤 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ ω ) )
25 24 cbvralvw ⊢ ( ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ ω ↔ ∀ 𝑤 ∈ ℤs ( bday ‘ ( 𝑤 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ ω )
26 22 25 bitrdi ⊢ ( 𝑚 = ( 𝑛 +s 1s ) → ( ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑚 ) ) ) ∈ ω ↔ ∀ 𝑤 ∈ ℤs ( bday ‘ ( 𝑤 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ ω ) )
27 oveq2 ⊢ ( 𝑚 = 𝑦 → ( 2s ↑s 𝑚 ) = ( 2s ↑s 𝑦 ) )
28 27 oveq2d ⊢ ( 𝑚 = 𝑦 → ( 𝑧 /su ( 2s ↑s 𝑚 ) ) = ( 𝑧 /su ( 2s ↑s 𝑦 ) ) )
29 28 fveq2d ⊢ ( 𝑚 = 𝑦 → ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑚 ) ) ) = ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑦 ) ) ) )
30 29 eleq1d ⊢ ( 𝑚 = 𝑦 → ( ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑚 ) ) ) ∈ ω ↔ ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑦 ) ) ) ∈ ω ) )
31 30 ralbidv ⊢ ( 𝑚 = 𝑦 → ( ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑚 ) ) ) ∈ ω ↔ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑦 ) ) ) ∈ ω ) )
32 zno ⊢ ( 𝑧 ∈ ℤs → 𝑧 ∈ No )
33 divs1 ⊢ ( 𝑧 ∈ No → ( 𝑧 /su 1s ) = 𝑧 )
34 32 33 syl ⊢ ( 𝑧 ∈ ℤs → ( 𝑧 /su 1s ) = 𝑧 )
35 34 fveq2d ⊢ ( 𝑧 ∈ ℤs → ( bday ‘ ( 𝑧 /su 1s ) ) = ( bday ‘ 𝑧 ) )
36 zsbday ⊢ ( 𝑧 ∈ ℤs → ( bday ‘ 𝑧 ) ∈ ω )
37 35 36 eqeltrd ⊢ ( 𝑧 ∈ ℤs → ( bday ‘ ( 𝑧 /su 1s ) ) ∈ ω )
38 37 rgen ⊢ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su 1s ) ) ∈ ω
39 zseo ⊢ ( 𝑤 ∈ ℤs → ( ∃ 𝑡 ∈ ℤs 𝑤 = ( 2s ·s 𝑡 ) ∨ ∃ 𝑡 ∈ ℤs 𝑤 = ( ( 2s ·s 𝑡 ) +s 1s ) ) )
40 expsp1 ⊢ ( ( 2s ∈ No ∧ 𝑛 ∈ ℕ0s ) → ( 2s ↑s ( 𝑛 +s 1s ) ) = ( ( 2s ↑s 𝑛 ) ·s 2s ) )
41 5 40 mpan ⊢ ( 𝑛 ∈ ℕ0s → ( 2s ↑s ( 𝑛 +s 1s ) ) = ( ( 2s ↑s 𝑛 ) ·s 2s ) )
42 41 adantr ⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝑡 ∈ ℤs ) → ( 2s ↑s ( 𝑛 +s 1s ) ) = ( ( 2s ↑s 𝑛 ) ·s 2s ) )
43 42 oveq2d ⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝑡 ∈ ℤs ) → ( ( 2s ·s 𝑡 ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( ( 2s ·s 𝑡 ) /su ( ( 2s ↑s 𝑛 ) ·s 2s ) ) )
44 5 a1i ⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝑡 ∈ ℤs ) → 2s ∈ No )
45 zno ⊢ ( 𝑡 ∈ ℤs → 𝑡 ∈ No )
46 45 adantl ⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝑡 ∈ ℤs ) → 𝑡 ∈ No )
47 44 46 mulscld ⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝑡 ∈ ℤs ) → ( 2s ·s 𝑡 ) ∈ No )
48 expscl ⊢ ( ( 2s ∈ No ∧ 𝑛 ∈ ℕ0s ) → ( 2s ↑s 𝑛 ) ∈ No )
49 5 48 mpan ⊢ ( 𝑛 ∈ ℕ0s → ( 2s ↑s 𝑛 ) ∈ No )
50 49 adantr ⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝑡 ∈ ℤs ) → ( 2s ↑s 𝑛 ) ∈ No )
51 2ne0s ⊢ 2s ≠ 0s
52 expsne0 ⊢ ( ( 2s ∈ No ∧ 2s ≠ 0s ∧ 𝑛 ∈ ℕ0s ) → ( 2s ↑s 𝑛 ) ≠ 0s )
53 5 51 52 mp3an12 ⊢ ( 𝑛 ∈ ℕ0s → ( 2s ↑s 𝑛 ) ≠ 0s )
54 53 adantr ⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝑡 ∈ ℤs ) → ( 2s ↑s 𝑛 ) ≠ 0s )
55 51 a1i ⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝑡 ∈ ℤs ) → 2s ≠ 0s )
56 47 50 44 54 55 divdivs1d ⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝑡 ∈ ℤs ) → ( ( ( 2s ·s 𝑡 ) /su ( 2s ↑s 𝑛 ) ) /su 2s ) = ( ( 2s ·s 𝑡 ) /su ( ( 2s ↑s 𝑛 ) ·s 2s ) ) )
57 44 46 50 54 divsassd ⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝑡 ∈ ℤs ) → ( ( 2s ·s 𝑡 ) /su ( 2s ↑s 𝑛 ) ) = ( 2s ·s ( 𝑡 /su ( 2s ↑s 𝑛 ) ) ) )
58 57 oveq1d ⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝑡 ∈ ℤs ) → ( ( ( 2s ·s 𝑡 ) /su ( 2s ↑s 𝑛 ) ) /su 2s ) = ( ( 2s ·s ( 𝑡 /su ( 2s ↑s 𝑛 ) ) ) /su 2s ) )
59 43 56 58 3eqtr2d ⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝑡 ∈ ℤs ) → ( ( 2s ·s 𝑡 ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( ( 2s ·s ( 𝑡 /su ( 2s ↑s 𝑛 ) ) ) /su 2s ) )
60 46 50 54 divscld ⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝑡 ∈ ℤs ) → ( 𝑡 /su ( 2s ↑s 𝑛 ) ) ∈ No )
61 60 44 55 divscan3d ⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝑡 ∈ ℤs ) → ( ( 2s ·s ( 𝑡 /su ( 2s ↑s 𝑛 ) ) ) /su 2s ) = ( 𝑡 /su ( 2s ↑s 𝑛 ) ) )
62 59 61 eqtrd ⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝑡 ∈ ℤs ) → ( ( 2s ·s 𝑡 ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( 𝑡 /su ( 2s ↑s 𝑛 ) ) )
63 62 fveq2d ⊢ ( ( 𝑛 ∈ ℕ0s ∧ 𝑡 ∈ ℤs ) → ( bday ‘ ( ( 2s ·s 𝑡 ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) = ( bday ‘ ( 𝑡 /su ( 2s ↑s 𝑛 ) ) ) )
64 63 adantlr ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( bday ‘ ( ( 2s ·s 𝑡 ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) = ( bday ‘ ( 𝑡 /su ( 2s ↑s 𝑛 ) ) ) )
65 fvoveq1 ⊢ ( 𝑧 = 𝑡 → ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) = ( bday ‘ ( 𝑡 /su ( 2s ↑s 𝑛 ) ) ) )
66 65 eleq1d ⊢ ( 𝑧 = 𝑡 → ( ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ↔ ( bday ‘ ( 𝑡 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) )
67 66 rspccva ⊢ ( ( ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ∧ 𝑡 ∈ ℤs ) → ( bday ‘ ( 𝑡 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω )
68 67 adantll ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( bday ‘ ( 𝑡 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω )
69 64 68 eqeltrd ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( bday ‘ ( ( 2s ·s 𝑡 ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ ω )
70 fvoveq1 ⊢ ( 𝑤 = ( 2s ·s 𝑡 ) → ( bday ‘ ( 𝑤 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) = ( bday ‘ ( ( 2s ·s 𝑡 ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
71 70 eleq1d ⊢ ( 𝑤 = ( 2s ·s 𝑡 ) → ( ( bday ‘ ( 𝑤 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ ω ↔ ( bday ‘ ( ( 2s ·s 𝑡 ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ ω ) )
72 69 71 syl5ibrcom ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( 𝑤 = ( 2s ·s 𝑡 ) → ( bday ‘ ( 𝑤 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ ω ) )
73 72 rexlimdva ⊢ ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) → ( ∃ 𝑡 ∈ ℤs 𝑤 = ( 2s ·s 𝑡 ) → ( bday ‘ ( 𝑤 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ ω ) )
74 45 adantl ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → 𝑡 ∈ No )
75 no2times ⊢ ( 𝑡 ∈ No → ( 2s ·s 𝑡 ) = ( 𝑡 +s 𝑡 ) )
76 74 75 syl ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( 2s ·s 𝑡 ) = ( 𝑡 +s 𝑡 ) )
77 76 oveq1d ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( ( 2s ·s 𝑡 ) +s 1s ) = ( ( 𝑡 +s 𝑡 ) +s 1s ) )
78 1sno ⊢ 1s ∈ No
79 78 a1i ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → 1s ∈ No )
80 74 74 79 addsassd ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( ( 𝑡 +s 𝑡 ) +s 1s ) = ( 𝑡 +s ( 𝑡 +s 1s ) ) )
81 77 80 eqtrd ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( ( 2s ·s 𝑡 ) +s 1s ) = ( 𝑡 +s ( 𝑡 +s 1s ) ) )
82 81 oveq1d ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( ( ( 2s ·s 𝑡 ) +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( ( 𝑡 +s ( 𝑡 +s 1s ) ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
83 74 79 addscld ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( 𝑡 +s 1s ) ∈ No )
84 simpll ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → 𝑛 ∈ ℕ0s )
85 74 sltp1d ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → 𝑡 <s ( 𝑡 +s 1s ) )
86 2nns ⊢ 2s ∈ ℕs
87 nnzs ⊢ ( 2s ∈ ℕs → 2s ∈ ℤs )
88 86 87 mp1i ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → 2s ∈ ℤs )
89 simpr ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → 𝑡 ∈ ℤs )
90 88 89 zmulscld ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( 2s ·s 𝑡 ) ∈ ℤs )
91 90 znod ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( 2s ·s 𝑡 ) ∈ No )
92 pncans ⊢ ( ( ( 2s ·s 𝑡 ) ∈ No ∧ 1s ∈ No ) → ( ( ( 2s ·s 𝑡 ) +s 1s ) -s 1s ) = ( 2s ·s 𝑡 ) )
93 91 78 92 sylancl ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( ( ( 2s ·s 𝑡 ) +s 1s ) -s 1s ) = ( 2s ·s 𝑡 ) )
94 93 eqcomd ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( 2s ·s 𝑡 ) = ( ( ( 2s ·s 𝑡 ) +s 1s ) -s 1s ) )
95 94 sneqd ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → { ( 2s ·s 𝑡 ) } = { ( ( ( 2s ·s 𝑡 ) +s 1s ) -s 1s ) } )
96 mulsrid ⊢ ( 2s ∈ No → ( 2s ·s 1s ) = 2s )
97 5 96 ax-mp ⊢ ( 2s ·s 1s ) = 2s
98 1p1e2s ⊢ ( 1s +s 1s ) = 2s
99 97 98 eqtr4i ⊢ ( 2s ·s 1s ) = ( 1s +s 1s )
100 99 oveq2i ⊢ ( ( 2s ·s 𝑡 ) +s ( 2s ·s 1s ) ) = ( ( 2s ·s 𝑡 ) +s ( 1s +s 1s ) )
101 5 a1i ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → 2s ∈ No )
102 101 74 79 addsdid ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( 2s ·s ( 𝑡 +s 1s ) ) = ( ( 2s ·s 𝑡 ) +s ( 2s ·s 1s ) ) )
103 91 79 79 addsassd ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( ( ( 2s ·s 𝑡 ) +s 1s ) +s 1s ) = ( ( 2s ·s 𝑡 ) +s ( 1s +s 1s ) ) )
104 100 102 103 3eqtr4a ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( 2s ·s ( 𝑡 +s 1s ) ) = ( ( ( 2s ·s 𝑡 ) +s 1s ) +s 1s ) )
105 104 sneqd ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → { ( 2s ·s ( 𝑡 +s 1s ) ) } = { ( ( ( 2s ·s 𝑡 ) +s 1s ) +s 1s ) } )
106 95 105 oveq12d ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( { ( 2s ·s 𝑡 ) } |s { ( 2s ·s ( 𝑡 +s 1s ) ) } ) = ( { ( ( ( 2s ·s 𝑡 ) +s 1s ) -s 1s ) } |s { ( ( ( 2s ·s 𝑡 ) +s 1s ) +s 1s ) } ) )
107 1zs ⊢ 1s ∈ ℤs
108 107 a1i ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → 1s ∈ ℤs )
109 90 108 zaddscld ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( ( 2s ·s 𝑡 ) +s 1s ) ∈ ℤs )
110 zscut ⊢ ( ( ( 2s ·s 𝑡 ) +s 1s ) ∈ ℤs → ( ( 2s ·s 𝑡 ) +s 1s ) = ( { ( ( ( 2s ·s 𝑡 ) +s 1s ) -s 1s ) } |s { ( ( ( 2s ·s 𝑡 ) +s 1s ) +s 1s ) } ) )
111 109 110 syl ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( ( 2s ·s 𝑡 ) +s 1s ) = ( { ( ( ( 2s ·s 𝑡 ) +s 1s ) -s 1s ) } |s { ( ( ( 2s ·s 𝑡 ) +s 1s ) +s 1s ) } ) )
112 106 111 81 3eqtr2d ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( { ( 2s ·s 𝑡 ) } |s { ( 2s ·s ( 𝑡 +s 1s ) ) } ) = ( 𝑡 +s ( 𝑡 +s 1s ) ) )
113 74 83 84 85 112 pw2cut ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) = ( ( 𝑡 +s ( 𝑡 +s 1s ) ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) )
114 82 113 eqtr4d ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( ( ( 2s ·s 𝑡 ) +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) = ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) )
115 114 fveq2d ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( bday ‘ ( ( ( 2s ·s 𝑡 ) +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) = ( bday ‘ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) )
116 49 ad2antrr ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( 2s ↑s 𝑛 ) ∈ No )
117 53 ad2antrr ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( 2s ↑s 𝑛 ) ≠ 0s )
118 74 116 117 divscld ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( 𝑡 /su ( 2s ↑s 𝑛 ) ) ∈ No )
119 83 116 117 divscld ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) ∈ No )
120 74 116 117 divscan2d ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( ( 2s ↑s 𝑛 ) ·s ( 𝑡 /su ( 2s ↑s 𝑛 ) ) ) = 𝑡 )
121 120 85 eqbrtrd ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( ( 2s ↑s 𝑛 ) ·s ( 𝑡 /su ( 2s ↑s 𝑛 ) ) ) <s ( 𝑡 +s 1s ) )
122 nnsgt0 ⊢ ( 2s ∈ ℕs → 0s <s 2s )
123 86 122 ax-mp ⊢ 0s <s 2s
124 expsgt0 ⊢ ( ( 2s ∈ No ∧ 𝑛 ∈ ℕ0s ∧ 0s <s 2s ) → 0s <s ( 2s ↑s 𝑛 ) )
125 5 123 124 mp3an13 ⊢ ( 𝑛 ∈ ℕ0s → 0s <s ( 2s ↑s 𝑛 ) )
126 125 ad2antrr ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → 0s <s ( 2s ↑s 𝑛 ) )
127 118 83 116 126 sltmuldiv2d ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( ( ( 2s ↑s 𝑛 ) ·s ( 𝑡 /su ( 2s ↑s 𝑛 ) ) ) <s ( 𝑡 +s 1s ) ↔ ( 𝑡 /su ( 2s ↑s 𝑛 ) ) <s ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) ) )
128 121 127 mpbid ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( 𝑡 /su ( 2s ↑s 𝑛 ) ) <s ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) )
129 118 119 128 ssltsn ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } <<s { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } )
130 imaundi ⊢ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) = ( ( bday “ { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ) ∪ ( bday “ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) )
131 130 unieqi ⊢ ∪ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) = ∪ ( ( bday “ { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ) ∪ ( bday “ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) )
132 uniun ⊢ ∪ ( ( bday “ { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ) ∪ ( bday “ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) = ( ∪ ( bday “ { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ) ∪ ∪ ( bday “ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) )
133 131 132 eqtri ⊢ ∪ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) = ( ∪ ( bday “ { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ) ∪ ∪ ( bday “ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) )
134 bdayfn ⊢ bday Fn No
135 fnsnfv ⊢ ( ( bday Fn No ∧ ( 𝑡 /su ( 2s ↑s 𝑛 ) ) ∈ No ) → { ( bday ‘ ( 𝑡 /su ( 2s ↑s 𝑛 ) ) ) } = ( bday “ { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ) )
136 134 118 135 sylancr ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → { ( bday ‘ ( 𝑡 /su ( 2s ↑s 𝑛 ) ) ) } = ( bday “ { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ) )
137 136 unieqd ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ∪ { ( bday ‘ ( 𝑡 /su ( 2s ↑s 𝑛 ) ) ) } = ∪ ( bday “ { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ) )
138 fvex ⊢ ( bday ‘ ( 𝑡 /su ( 2s ↑s 𝑛 ) ) ) ∈ V
139 138 unisn ⊢ ∪ { ( bday ‘ ( 𝑡 /su ( 2s ↑s 𝑛 ) ) ) } = ( bday ‘ ( 𝑡 /su ( 2s ↑s 𝑛 ) ) )
140 137 139 eqtr3di ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ∪ ( bday “ { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ) = ( bday ‘ ( 𝑡 /su ( 2s ↑s 𝑛 ) ) ) )
141 140 68 eqeltrd ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ∪ ( bday “ { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ) ∈ ω )
142 fnsnfv ⊢ ( ( bday Fn No ∧ ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) ∈ No ) → { ( bday ‘ ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) ) } = ( bday “ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) )
143 134 119 142 sylancr ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → { ( bday ‘ ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) ) } = ( bday “ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) )
144 143 unieqd ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ∪ { ( bday ‘ ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) ) } = ∪ ( bday “ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) )
145 fvex ⊢ ( bday ‘ ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) ) ∈ V
146 145 unisn ⊢ ∪ { ( bday ‘ ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) ) } = ( bday ‘ ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) )
147 144 146 eqtr3di ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ∪ ( bday “ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) = ( bday ‘ ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) ) )
148 fvoveq1 ⊢ ( 𝑧 = ( 𝑡 +s 1s ) → ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) = ( bday ‘ ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) ) )
149 148 eleq1d ⊢ ( 𝑧 = ( 𝑡 +s 1s ) → ( ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ↔ ( bday ‘ ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) )
150 simplr ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω )
151 89 108 zaddscld ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( 𝑡 +s 1s ) ∈ ℤs )
152 149 150 151 rspcdva ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( bday ‘ ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) ) ∈ ω )
153 147 152 eqeltrd ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ∪ ( bday “ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ∈ ω )
154 omun ⊢ ( ( ∪ ( bday “ { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ) ∈ ω ∧ ∪ ( bday “ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ∈ ω ) → ( ∪ ( bday “ { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ) ∪ ∪ ( bday “ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ∈ ω )
155 141 153 154 syl2anc ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( ∪ ( bday “ { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ) ∪ ∪ ( bday “ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ∈ ω )
156 133 155 eqeltrid ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ∪ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ∈ ω )
157 peano2 ⊢ ( ∪ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ∈ ω → suc ∪ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ∈ ω )
158 156 157 syl ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → suc ∪ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ∈ ω )
159 nnon ⊢ ( suc ∪ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ∈ ω → suc ∪ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ∈ On )
160 158 159 syl ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → suc ∪ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ∈ On )
161 imassrn ⊢ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ⊆ ran bday
162 bdayrn ⊢ ran bday = On
163 161 162 sseqtri ⊢ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ⊆ On
164 onsucuni ⊢ ( ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ⊆ On → ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ⊆ suc ∪ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) )
165 163 164 mp1i ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ⊆ suc ∪ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) )
166 scutbdaybnd ⊢ ( ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } <<s { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ∧ suc ∪ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ∈ On ∧ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ⊆ suc ∪ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ) → ( bday ‘ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ⊆ suc ∪ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) )
167 129 160 165 166 syl3anc ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( bday ‘ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ⊆ suc ∪ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) )
168 bdayelon ⊢ ( bday ‘ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ∈ On
169 onsssuc ⊢ ( ( ( bday ‘ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ∈ On ∧ suc ∪ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ∈ On ) → ( ( bday ‘ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ⊆ suc ∪ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ↔ ( bday ‘ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ∈ suc suc ∪ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ) )
170 168 160 169 sylancr ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( ( bday ‘ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ⊆ suc ∪ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ↔ ( bday ‘ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ∈ suc suc ∪ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ) )
171 167 170 mpbid ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( bday ‘ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } |s { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ∈ suc suc ∪ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) )
172 115 171 eqeltrd ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( bday ‘ ( ( ( 2s ·s 𝑡 ) +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ suc suc ∪ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) )
173 peano2 ⊢ ( suc ∪ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ∈ ω → suc suc ∪ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ∈ ω )
174 158 173 syl ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → suc suc ∪ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ∈ ω )
175 elnn ⊢ ( ( ( bday ‘ ( ( ( 2s ·s 𝑡 ) +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ suc suc ∪ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ∧ suc suc ∪ ( bday “ ( { ( 𝑡 /su ( 2s ↑s 𝑛 ) ) } ∪ { ( ( 𝑡 +s 1s ) /su ( 2s ↑s 𝑛 ) ) } ) ) ∈ ω ) → ( bday ‘ ( ( ( 2s ·s 𝑡 ) +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ ω )
176 172 174 175 syl2anc ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( bday ‘ ( ( ( 2s ·s 𝑡 ) +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ ω )
177 fvoveq1 ⊢ ( 𝑤 = ( ( 2s ·s 𝑡 ) +s 1s ) → ( bday ‘ ( 𝑤 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) = ( bday ‘ ( ( ( 2s ·s 𝑡 ) +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) )
178 177 eleq1d ⊢ ( 𝑤 = ( ( 2s ·s 𝑡 ) +s 1s ) → ( ( bday ‘ ( 𝑤 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ ω ↔ ( bday ‘ ( ( ( 2s ·s 𝑡 ) +s 1s ) /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ ω ) )
179 176 178 syl5ibrcom ⊢ ( ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) ∧ 𝑡 ∈ ℤs ) → ( 𝑤 = ( ( 2s ·s 𝑡 ) +s 1s ) → ( bday ‘ ( 𝑤 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ ω ) )
180 179 rexlimdva ⊢ ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) → ( ∃ 𝑡 ∈ ℤs 𝑤 = ( ( 2s ·s 𝑡 ) +s 1s ) → ( bday ‘ ( 𝑤 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ ω ) )
181 73 180 jaod ⊢ ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) → ( ( ∃ 𝑡 ∈ ℤs 𝑤 = ( 2s ·s 𝑡 ) ∨ ∃ 𝑡 ∈ ℤs 𝑤 = ( ( 2s ·s 𝑡 ) +s 1s ) ) → ( bday ‘ ( 𝑤 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ ω ) )
182 39 181 syl5 ⊢ ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) → ( 𝑤 ∈ ℤs → ( bday ‘ ( 𝑤 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ ω ) )
183 182 ralrimiv ⊢ ( ( 𝑛 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω ) → ∀ 𝑤 ∈ ℤs ( bday ‘ ( 𝑤 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ ω )
184 183 ex ⊢ ( 𝑛 ∈ ℕ0s → ( ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑛 ) ) ) ∈ ω → ∀ 𝑤 ∈ ℤs ( bday ‘ ( 𝑤 /su ( 2s ↑s ( 𝑛 +s 1s ) ) ) ) ∈ ω ) )
185 12 17 26 31 38 184 n0sind ⊢ ( 𝑦 ∈ ℕ0s → ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑦 ) ) ) ∈ ω )
186 185 adantl ⊢ ( ( 𝑥 ∈ ℤs ∧ 𝑦 ∈ ℕ0s ) → ∀ 𝑧 ∈ ℤs ( bday ‘ ( 𝑧 /su ( 2s ↑s 𝑦 ) ) ) ∈ ω )
187 simpl ⊢ ( ( 𝑥 ∈ ℤs ∧ 𝑦 ∈ ℕ0s ) → 𝑥 ∈ ℤs )
188 3 186 187 rspcdva ⊢ ( ( 𝑥 ∈ ℤs ∧ 𝑦 ∈ ℕ0s ) → ( bday ‘ ( 𝑥 /su ( 2s ↑s 𝑦 ) ) ) ∈ ω )
189 fveq2 ⊢ ( 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) → ( bday ‘ 𝐴 ) = ( bday ‘ ( 𝑥 /su ( 2s ↑s 𝑦 ) ) ) )
190 189 eleq1d ⊢ ( 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) → ( ( bday ‘ 𝐴 ) ∈ ω ↔ ( bday ‘ ( 𝑥 /su ( 2s ↑s 𝑦 ) ) ) ∈ ω ) )
191 188 190 syl5ibrcom ⊢ ( ( 𝑥 ∈ ℤs ∧ 𝑦 ∈ ℕ0s ) → ( 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) → ( bday ‘ 𝐴 ) ∈ ω ) )
192 191 rexlimivv ⊢ ( ∃ 𝑥 ∈ ℤs ∃ 𝑦 ∈ ℕ0s 𝐴 = ( 𝑥 /su ( 2s ↑s 𝑦 ) ) → ( bday ‘ 𝐴 ) ∈ ω )
193 1 192 sylbi ⊢ ( 𝐴 ∈ ℤs[1/2] → ( bday ‘ 𝐴 ) ∈ ω )