MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  zs12bday Structured version   Visualization version   GIF version

Theorem zs12bday 28442
Description: A dyadic fraction has a finite birthday. (Contributed by Scott Fenton, 20-Aug-2025.)
Assertion
Ref Expression
zs12bday (𝐴 ∈ ℤs[1/2] → ( bday 𝐴) ∈ ω)

Proof of Theorem zs12bday
Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑡 𝑛 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elzs12 28439 . 2 (𝐴 ∈ ℤs[1/2] ↔ ∃𝑥 ∈ ℤs𝑦 ∈ ℕ0s 𝐴 = (𝑥 /su (2ss𝑦)))
2 fvoveq1 7471 . . . . . 6 (𝑧 = 𝑥 → ( bday ‘(𝑧 /su (2ss𝑦))) = ( bday ‘(𝑥 /su (2ss𝑦))))
32eleq1d 2829 . . . . 5 (𝑧 = 𝑥 → (( bday ‘(𝑧 /su (2ss𝑦))) ∈ ω ↔ ( bday ‘(𝑥 /su (2ss𝑦))) ∈ ω))
4 oveq2 7456 . . . . . . . . . . . 12 (𝑚 = 0s → (2ss𝑚) = (2ss 0s ))
5 2sno 28421 . . . . . . . . . . . . 13 2s No
6 exps0 28428 . . . . . . . . . . . . 13 (2s No → (2ss 0s ) = 1s )
75, 6ax-mp 5 . . . . . . . . . . . 12 (2ss 0s ) = 1s
84, 7eqtrdi 2796 . . . . . . . . . . 11 (𝑚 = 0s → (2ss𝑚) = 1s )
98oveq2d 7464 . . . . . . . . . 10 (𝑚 = 0s → (𝑧 /su (2ss𝑚)) = (𝑧 /su 1s ))
109fveq2d 6924 . . . . . . . . 9 (𝑚 = 0s → ( bday ‘(𝑧 /su (2ss𝑚))) = ( bday ‘(𝑧 /su 1s )))
1110eleq1d 2829 . . . . . . . 8 (𝑚 = 0s → (( bday ‘(𝑧 /su (2ss𝑚))) ∈ ω ↔ ( bday ‘(𝑧 /su 1s )) ∈ ω))
1211ralbidv 3184 . . . . . . 7 (𝑚 = 0s → (∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑚))) ∈ ω ↔ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su 1s )) ∈ ω))
13 oveq2 7456 . . . . . . . . . . 11 (𝑚 = 𝑛 → (2ss𝑚) = (2ss𝑛))
1413oveq2d 7464 . . . . . . . . . 10 (𝑚 = 𝑛 → (𝑧 /su (2ss𝑚)) = (𝑧 /su (2ss𝑛)))
1514fveq2d 6924 . . . . . . . . 9 (𝑚 = 𝑛 → ( bday ‘(𝑧 /su (2ss𝑚))) = ( bday ‘(𝑧 /su (2ss𝑛))))
1615eleq1d 2829 . . . . . . . 8 (𝑚 = 𝑛 → (( bday ‘(𝑧 /su (2ss𝑚))) ∈ ω ↔ ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω))
1716ralbidv 3184 . . . . . . 7 (𝑚 = 𝑛 → (∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑚))) ∈ ω ↔ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω))
18 oveq2 7456 . . . . . . . . . . . 12 (𝑚 = (𝑛 +s 1s ) → (2ss𝑚) = (2ss(𝑛 +s 1s )))
1918oveq2d 7464 . . . . . . . . . . 11 (𝑚 = (𝑛 +s 1s ) → (𝑧 /su (2ss𝑚)) = (𝑧 /su (2ss(𝑛 +s 1s ))))
2019fveq2d 6924 . . . . . . . . . 10 (𝑚 = (𝑛 +s 1s ) → ( bday ‘(𝑧 /su (2ss𝑚))) = ( bday ‘(𝑧 /su (2ss(𝑛 +s 1s )))))
2120eleq1d 2829 . . . . . . . . 9 (𝑚 = (𝑛 +s 1s ) → (( bday ‘(𝑧 /su (2ss𝑚))) ∈ ω ↔ ( bday ‘(𝑧 /su (2ss(𝑛 +s 1s )))) ∈ ω))
2221ralbidv 3184 . . . . . . . 8 (𝑚 = (𝑛 +s 1s ) → (∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑚))) ∈ ω ↔ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss(𝑛 +s 1s )))) ∈ ω))
23 fvoveq1 7471 . . . . . . . . . 10 (𝑧 = 𝑤 → ( bday ‘(𝑧 /su (2ss(𝑛 +s 1s )))) = ( bday ‘(𝑤 /su (2ss(𝑛 +s 1s )))))
2423eleq1d 2829 . . . . . . . . 9 (𝑧 = 𝑤 → (( bday ‘(𝑧 /su (2ss(𝑛 +s 1s )))) ∈ ω ↔ ( bday ‘(𝑤 /su (2ss(𝑛 +s 1s )))) ∈ ω))
2524cbvralvw 3243 . . . . . . . 8 (∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss(𝑛 +s 1s )))) ∈ ω ↔ ∀𝑤 ∈ ℤs ( bday ‘(𝑤 /su (2ss(𝑛 +s 1s )))) ∈ ω)
2622, 25bitrdi 287 . . . . . . 7 (𝑚 = (𝑛 +s 1s ) → (∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑚))) ∈ ω ↔ ∀𝑤 ∈ ℤs ( bday ‘(𝑤 /su (2ss(𝑛 +s 1s )))) ∈ ω))
27 oveq2 7456 . . . . . . . . . . 11 (𝑚 = 𝑦 → (2ss𝑚) = (2ss𝑦))
2827oveq2d 7464 . . . . . . . . . 10 (𝑚 = 𝑦 → (𝑧 /su (2ss𝑚)) = (𝑧 /su (2ss𝑦)))
2928fveq2d 6924 . . . . . . . . 9 (𝑚 = 𝑦 → ( bday ‘(𝑧 /su (2ss𝑚))) = ( bday ‘(𝑧 /su (2ss𝑦))))
3029eleq1d 2829 . . . . . . . 8 (𝑚 = 𝑦 → (( bday ‘(𝑧 /su (2ss𝑚))) ∈ ω ↔ ( bday ‘(𝑧 /su (2ss𝑦))) ∈ ω))
3130ralbidv 3184 . . . . . . 7 (𝑚 = 𝑦 → (∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑚))) ∈ ω ↔ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑦))) ∈ ω))
32 zno 28386 . . . . . . . . . . 11 (𝑧 ∈ ℤs𝑧 No )
33 divs1 28247 . . . . . . . . . . 11 (𝑧 No → (𝑧 /su 1s ) = 𝑧)
3432, 33syl 17 . . . . . . . . . 10 (𝑧 ∈ ℤs → (𝑧 /su 1s ) = 𝑧)
3534fveq2d 6924 . . . . . . . . 9 (𝑧 ∈ ℤs → ( bday ‘(𝑧 /su 1s )) = ( bday 𝑧))
36 zsbday 28410 . . . . . . . . 9 (𝑧 ∈ ℤs → ( bday 𝑧) ∈ ω)
3735, 36eqeltrd 2844 . . . . . . . 8 (𝑧 ∈ ℤs → ( bday ‘(𝑧 /su 1s )) ∈ ω)
3837rgen 3069 . . . . . . 7 𝑧 ∈ ℤs ( bday ‘(𝑧 /su 1s )) ∈ ω
39 zseo 28424 . . . . . . . . . 10 (𝑤 ∈ ℤs → (∃𝑡 ∈ ℤs 𝑤 = (2s ·s 𝑡) ∨ ∃𝑡 ∈ ℤs 𝑤 = ((2s ·s 𝑡) +s 1s )))
40 expsp1 28430 . . . . . . . . . . . . . . . . . . . . 21 ((2s No 𝑛 ∈ ℕ0s) → (2ss(𝑛 +s 1s )) = ((2ss𝑛) ·s 2s))
415, 40mpan 689 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ0s → (2ss(𝑛 +s 1s )) = ((2ss𝑛) ·s 2s))
4241adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ0s𝑡 ∈ ℤs) → (2ss(𝑛 +s 1s )) = ((2ss𝑛) ·s 2s))
4342oveq2d 7464 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ0s𝑡 ∈ ℤs) → ((2s ·s 𝑡) /su (2ss(𝑛 +s 1s ))) = ((2s ·s 𝑡) /su ((2ss𝑛) ·s 2s)))
445a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ0s𝑡 ∈ ℤs) → 2s No )
45 zno 28386 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 ∈ ℤs𝑡 No )
4645adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ0s𝑡 ∈ ℤs) → 𝑡 No )
4744, 46mulscld 28179 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ0s𝑡 ∈ ℤs) → (2s ·s 𝑡) ∈ No )
48 expscl 28431 . . . . . . . . . . . . . . . . . . . . 21 ((2s No 𝑛 ∈ ℕ0s) → (2ss𝑛) ∈ No )
495, 48mpan 689 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ0s → (2ss𝑛) ∈ No )
5049adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ0s𝑡 ∈ ℤs) → (2ss𝑛) ∈ No )
51 2ne0s 28422 . . . . . . . . . . . . . . . . . . . . 21 2s ≠ 0s
52 expsne0 28432 . . . . . . . . . . . . . . . . . . . . 21 ((2s No ∧ 2s ≠ 0s𝑛 ∈ ℕ0s) → (2ss𝑛) ≠ 0s )
535, 51, 52mp3an12 1451 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ0s → (2ss𝑛) ≠ 0s )
5453adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ0s𝑡 ∈ ℤs) → (2ss𝑛) ≠ 0s )
5551a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ0s𝑡 ∈ ℤs) → 2s ≠ 0s )
5647, 50, 44, 54, 55divdivs1d 28275 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ0s𝑡 ∈ ℤs) → (((2s ·s 𝑡) /su (2ss𝑛)) /su 2s) = ((2s ·s 𝑡) /su ((2ss𝑛) ·s 2s)))
5744, 46, 50, 54divsassd 28273 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ0s𝑡 ∈ ℤs) → ((2s ·s 𝑡) /su (2ss𝑛)) = (2s ·s (𝑡 /su (2ss𝑛))))
5857oveq1d 7463 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ0s𝑡 ∈ ℤs) → (((2s ·s 𝑡) /su (2ss𝑛)) /su 2s) = ((2s ·s (𝑡 /su (2ss𝑛))) /su 2s))
5943, 56, 583eqtr2d 2786 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ℕ0s𝑡 ∈ ℤs) → ((2s ·s 𝑡) /su (2ss(𝑛 +s 1s ))) = ((2s ·s (𝑡 /su (2ss𝑛))) /su 2s))
6046, 50, 54divscld 28266 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ0s𝑡 ∈ ℤs) → (𝑡 /su (2ss𝑛)) ∈ No )
6160, 44, 55divscan3d 28278 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ℕ0s𝑡 ∈ ℤs) → ((2s ·s (𝑡 /su (2ss𝑛))) /su 2s) = (𝑡 /su (2ss𝑛)))
6259, 61eqtrd 2780 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ℕ0s𝑡 ∈ ℤs) → ((2s ·s 𝑡) /su (2ss(𝑛 +s 1s ))) = (𝑡 /su (2ss𝑛)))
6362fveq2d 6924 . . . . . . . . . . . . . . 15 ((𝑛 ∈ ℕ0s𝑡 ∈ ℤs) → ( bday ‘((2s ·s 𝑡) /su (2ss(𝑛 +s 1s )))) = ( bday ‘(𝑡 /su (2ss𝑛))))
6463adantlr 714 . . . . . . . . . . . . . 14 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ( bday ‘((2s ·s 𝑡) /su (2ss(𝑛 +s 1s )))) = ( bday ‘(𝑡 /su (2ss𝑛))))
65 fvoveq1 7471 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑡 → ( bday ‘(𝑧 /su (2ss𝑛))) = ( bday ‘(𝑡 /su (2ss𝑛))))
6665eleq1d 2829 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑡 → (( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω ↔ ( bday ‘(𝑡 /su (2ss𝑛))) ∈ ω))
6766rspccva 3634 . . . . . . . . . . . . . . 15 ((∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω ∧ 𝑡 ∈ ℤs) → ( bday ‘(𝑡 /su (2ss𝑛))) ∈ ω)
6867adantll 713 . . . . . . . . . . . . . 14 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ( bday ‘(𝑡 /su (2ss𝑛))) ∈ ω)
6964, 68eqeltrd 2844 . . . . . . . . . . . . 13 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ( bday ‘((2s ·s 𝑡) /su (2ss(𝑛 +s 1s )))) ∈ ω)
70 fvoveq1 7471 . . . . . . . . . . . . . 14 (𝑤 = (2s ·s 𝑡) → ( bday ‘(𝑤 /su (2ss(𝑛 +s 1s )))) = ( bday ‘((2s ·s 𝑡) /su (2ss(𝑛 +s 1s )))))
7170eleq1d 2829 . . . . . . . . . . . . 13 (𝑤 = (2s ·s 𝑡) → (( bday ‘(𝑤 /su (2ss(𝑛 +s 1s )))) ∈ ω ↔ ( bday ‘((2s ·s 𝑡) /su (2ss(𝑛 +s 1s )))) ∈ ω))
7269, 71syl5ibrcom 247 . . . . . . . . . . . 12 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → (𝑤 = (2s ·s 𝑡) → ( bday ‘(𝑤 /su (2ss(𝑛 +s 1s )))) ∈ ω))
7372rexlimdva 3161 . . . . . . . . . . 11 ((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) → (∃𝑡 ∈ ℤs 𝑤 = (2s ·s 𝑡) → ( bday ‘(𝑤 /su (2ss(𝑛 +s 1s )))) ∈ ω))
7445adantl 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → 𝑡 No )
75 no2times 28419 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 No → (2s ·s 𝑡) = (𝑡 +s 𝑡))
7674, 75syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → (2s ·s 𝑡) = (𝑡 +s 𝑡))
7776oveq1d 7463 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ((2s ·s 𝑡) +s 1s ) = ((𝑡 +s 𝑡) +s 1s ))
78 1sno 27890 . . . . . . . . . . . . . . . . . . . . 21 1s No
7978a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → 1s No )
8074, 74, 79addsassd 28057 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ((𝑡 +s 𝑡) +s 1s ) = (𝑡 +s (𝑡 +s 1s )))
8177, 80eqtrd 2780 . . . . . . . . . . . . . . . . . 18 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ((2s ·s 𝑡) +s 1s ) = (𝑡 +s (𝑡 +s 1s )))
8281oveq1d 7463 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → (((2s ·s 𝑡) +s 1s ) /su (2ss(𝑛 +s 1s ))) = ((𝑡 +s (𝑡 +s 1s )) /su (2ss(𝑛 +s 1s ))))
8374, 79addscld 28031 . . . . . . . . . . . . . . . . . 18 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → (𝑡 +s 1s ) ∈ No )
84 simpll 766 . . . . . . . . . . . . . . . . . 18 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → 𝑛 ∈ ℕ0s)
8574sltp1d 28066 . . . . . . . . . . . . . . . . . 18 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → 𝑡 <s (𝑡 +s 1s ))
86 2nns 28420 . . . . . . . . . . . . . . . . . . . . . . . . . 26 2s ∈ ℕs
87 nnzs 28390 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (2s ∈ ℕs → 2s ∈ ℤs)
8886, 87mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → 2s ∈ ℤs)
89 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → 𝑡 ∈ ℤs)
9088, 89zmulscld 28401 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → (2s ·s 𝑡) ∈ ℤs)
9190znod 28387 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → (2s ·s 𝑡) ∈ No )
92 pncans 28120 . . . . . . . . . . . . . . . . . . . . . . 23 (((2s ·s 𝑡) ∈ No ∧ 1s No ) → (((2s ·s 𝑡) +s 1s ) -s 1s ) = (2s ·s 𝑡))
9391, 78, 92sylancl 585 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → (((2s ·s 𝑡) +s 1s ) -s 1s ) = (2s ·s 𝑡))
9493eqcomd 2746 . . . . . . . . . . . . . . . . . . . . 21 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → (2s ·s 𝑡) = (((2s ·s 𝑡) +s 1s ) -s 1s ))
9594sneqd 4660 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → {(2s ·s 𝑡)} = {(((2s ·s 𝑡) +s 1s ) -s 1s )})
96 mulsrid 28157 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2s No → (2s ·s 1s ) = 2s)
975, 96ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 (2s ·s 1s ) = 2s
98 1p1e2s 28418 . . . . . . . . . . . . . . . . . . . . . . . 24 ( 1s +s 1s ) = 2s
9997, 98eqtr4i 2771 . . . . . . . . . . . . . . . . . . . . . . 23 (2s ·s 1s ) = ( 1s +s 1s )
10099oveq2i 7459 . . . . . . . . . . . . . . . . . . . . . 22 ((2s ·s 𝑡) +s (2s ·s 1s )) = ((2s ·s 𝑡) +s ( 1s +s 1s ))
1015a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → 2s No )
102101, 74, 79addsdid 28200 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → (2s ·s (𝑡 +s 1s )) = ((2s ·s 𝑡) +s (2s ·s 1s )))
10391, 79, 79addsassd 28057 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → (((2s ·s 𝑡) +s 1s ) +s 1s ) = ((2s ·s 𝑡) +s ( 1s +s 1s )))
104100, 102, 1033eqtr4a 2806 . . . . . . . . . . . . . . . . . . . . 21 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → (2s ·s (𝑡 +s 1s )) = (((2s ·s 𝑡) +s 1s ) +s 1s ))
105104sneqd 4660 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → {(2s ·s (𝑡 +s 1s ))} = {(((2s ·s 𝑡) +s 1s ) +s 1s )})
10695, 105oveq12d 7466 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ({(2s ·s 𝑡)} |s {(2s ·s (𝑡 +s 1s ))}) = ({(((2s ·s 𝑡) +s 1s ) -s 1s )} |s {(((2s ·s 𝑡) +s 1s ) +s 1s )}))
107 1zs 28395 . . . . . . . . . . . . . . . . . . . . . 22 1s ∈ ℤs
108107a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → 1s ∈ ℤs)
10990, 108zaddscld 28399 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ((2s ·s 𝑡) +s 1s ) ∈ ℤs)
110 zscut 28411 . . . . . . . . . . . . . . . . . . . 20 (((2s ·s 𝑡) +s 1s ) ∈ ℤs → ((2s ·s 𝑡) +s 1s ) = ({(((2s ·s 𝑡) +s 1s ) -s 1s )} |s {(((2s ·s 𝑡) +s 1s ) +s 1s )}))
111109, 110syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ((2s ·s 𝑡) +s 1s ) = ({(((2s ·s 𝑡) +s 1s ) -s 1s )} |s {(((2s ·s 𝑡) +s 1s ) +s 1s )}))
112106, 111, 813eqtr2d 2786 . . . . . . . . . . . . . . . . . 18 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ({(2s ·s 𝑡)} |s {(2s ·s (𝑡 +s 1s ))}) = (𝑡 +s (𝑡 +s 1s )))
11374, 83, 84, 85, 112pw2cut 28438 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ({(𝑡 /su (2ss𝑛))} |s {((𝑡 +s 1s ) /su (2ss𝑛))}) = ((𝑡 +s (𝑡 +s 1s )) /su (2ss(𝑛 +s 1s ))))
11482, 113eqtr4d 2783 . . . . . . . . . . . . . . . 16 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → (((2s ·s 𝑡) +s 1s ) /su (2ss(𝑛 +s 1s ))) = ({(𝑡 /su (2ss𝑛))} |s {((𝑡 +s 1s ) /su (2ss𝑛))}))
115114fveq2d 6924 . . . . . . . . . . . . . . 15 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ( bday ‘(((2s ·s 𝑡) +s 1s ) /su (2ss(𝑛 +s 1s )))) = ( bday ‘({(𝑡 /su (2ss𝑛))} |s {((𝑡 +s 1s ) /su (2ss𝑛))})))
11649ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → (2ss𝑛) ∈ No )
11753ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → (2ss𝑛) ≠ 0s )
11874, 116, 117divscld 28266 . . . . . . . . . . . . . . . . . 18 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → (𝑡 /su (2ss𝑛)) ∈ No )
11983, 116, 117divscld 28266 . . . . . . . . . . . . . . . . . 18 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ((𝑡 +s 1s ) /su (2ss𝑛)) ∈ No )
12074, 116, 117divscan2d 28267 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ((2ss𝑛) ·s (𝑡 /su (2ss𝑛))) = 𝑡)
121120, 85eqbrtrd 5188 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ((2ss𝑛) ·s (𝑡 /su (2ss𝑛))) <s (𝑡 +s 1s ))
122 nnsgt0 28360 . . . . . . . . . . . . . . . . . . . . . . 23 (2s ∈ ℕs → 0s <s 2s)
12386, 122ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 0s <s 2s
124 expsgt0 28433 . . . . . . . . . . . . . . . . . . . . . 22 ((2s No 𝑛 ∈ ℕ0s ∧ 0s <s 2s) → 0s <s (2ss𝑛))
1255, 123, 124mp3an13 1452 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ℕ0s → 0s <s (2ss𝑛))
126125ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → 0s <s (2ss𝑛))
127118, 83, 116, 126sltmuldiv2d 28272 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → (((2ss𝑛) ·s (𝑡 /su (2ss𝑛))) <s (𝑡 +s 1s ) ↔ (𝑡 /su (2ss𝑛)) <s ((𝑡 +s 1s ) /su (2ss𝑛))))
128121, 127mpbid 232 . . . . . . . . . . . . . . . . . 18 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → (𝑡 /su (2ss𝑛)) <s ((𝑡 +s 1s ) /su (2ss𝑛)))
129118, 119, 128ssltsn 27855 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → {(𝑡 /su (2ss𝑛))} <<s {((𝑡 +s 1s ) /su (2ss𝑛))})
130 imaundi 6181 . . . . . . . . . . . . . . . . . . . . . 22 ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})) = (( bday “ {(𝑡 /su (2ss𝑛))}) ∪ ( bday “ {((𝑡 +s 1s ) /su (2ss𝑛))}))
131130unieqi 4943 . . . . . . . . . . . . . . . . . . . . 21 ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})) = (( bday “ {(𝑡 /su (2ss𝑛))}) ∪ ( bday “ {((𝑡 +s 1s ) /su (2ss𝑛))}))
132 uniun 4954 . . . . . . . . . . . . . . . . . . . . 21 (( bday “ {(𝑡 /su (2ss𝑛))}) ∪ ( bday “ {((𝑡 +s 1s ) /su (2ss𝑛))})) = ( ( bday “ {(𝑡 /su (2ss𝑛))}) ∪ ( bday “ {((𝑡 +s 1s ) /su (2ss𝑛))}))
133131, 132eqtri 2768 . . . . . . . . . . . . . . . . . . . 20 ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})) = ( ( bday “ {(𝑡 /su (2ss𝑛))}) ∪ ( bday “ {((𝑡 +s 1s ) /su (2ss𝑛))}))
134 bdayfn 27836 . . . . . . . . . . . . . . . . . . . . . . . . 25 bday Fn No
135 fnsnfv 7001 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( bday Fn No ∧ (𝑡 /su (2ss𝑛)) ∈ No ) → {( bday ‘(𝑡 /su (2ss𝑛)))} = ( bday “ {(𝑡 /su (2ss𝑛))}))
136134, 118, 135sylancr 586 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → {( bday ‘(𝑡 /su (2ss𝑛)))} = ( bday “ {(𝑡 /su (2ss𝑛))}))
137136unieqd 4944 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → {( bday ‘(𝑡 /su (2ss𝑛)))} = ( bday “ {(𝑡 /su (2ss𝑛))}))
138 fvex 6933 . . . . . . . . . . . . . . . . . . . . . . . 24 ( bday ‘(𝑡 /su (2ss𝑛))) ∈ V
139138unisn 4950 . . . . . . . . . . . . . . . . . . . . . . 23 {( bday ‘(𝑡 /su (2ss𝑛)))} = ( bday ‘(𝑡 /su (2ss𝑛)))
140137, 139eqtr3di 2795 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ( bday “ {(𝑡 /su (2ss𝑛))}) = ( bday ‘(𝑡 /su (2ss𝑛))))
141140, 68eqeltrd 2844 . . . . . . . . . . . . . . . . . . . . 21 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ( bday “ {(𝑡 /su (2ss𝑛))}) ∈ ω)
142 fnsnfv 7001 . . . . . . . . . . . . . . . . . . . . . . . . 25 (( bday Fn No ∧ ((𝑡 +s 1s ) /su (2ss𝑛)) ∈ No ) → {( bday ‘((𝑡 +s 1s ) /su (2ss𝑛)))} = ( bday “ {((𝑡 +s 1s ) /su (2ss𝑛))}))
143134, 119, 142sylancr 586 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → {( bday ‘((𝑡 +s 1s ) /su (2ss𝑛)))} = ( bday “ {((𝑡 +s 1s ) /su (2ss𝑛))}))
144143unieqd 4944 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → {( bday ‘((𝑡 +s 1s ) /su (2ss𝑛)))} = ( bday “ {((𝑡 +s 1s ) /su (2ss𝑛))}))
145 fvex 6933 . . . . . . . . . . . . . . . . . . . . . . . 24 ( bday ‘((𝑡 +s 1s ) /su (2ss𝑛))) ∈ V
146145unisn 4950 . . . . . . . . . . . . . . . . . . . . . . 23 {( bday ‘((𝑡 +s 1s ) /su (2ss𝑛)))} = ( bday ‘((𝑡 +s 1s ) /su (2ss𝑛)))
147144, 146eqtr3di 2795 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ( bday “ {((𝑡 +s 1s ) /su (2ss𝑛))}) = ( bday ‘((𝑡 +s 1s ) /su (2ss𝑛))))
148 fvoveq1 7471 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = (𝑡 +s 1s ) → ( bday ‘(𝑧 /su (2ss𝑛))) = ( bday ‘((𝑡 +s 1s ) /su (2ss𝑛))))
149148eleq1d 2829 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = (𝑡 +s 1s ) → (( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω ↔ ( bday ‘((𝑡 +s 1s ) /su (2ss𝑛))) ∈ ω))
150 simplr 768 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω)
15189, 108zaddscld 28399 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → (𝑡 +s 1s ) ∈ ℤs)
152149, 150, 151rspcdva 3636 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ( bday ‘((𝑡 +s 1s ) /su (2ss𝑛))) ∈ ω)
153147, 152eqeltrd 2844 . . . . . . . . . . . . . . . . . . . . 21 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ( bday “ {((𝑡 +s 1s ) /su (2ss𝑛))}) ∈ ω)
154 omun 7926 . . . . . . . . . . . . . . . . . . . . 21 (( ( bday “ {(𝑡 /su (2ss𝑛))}) ∈ ω ∧ ( bday “ {((𝑡 +s 1s ) /su (2ss𝑛))}) ∈ ω) → ( ( bday “ {(𝑡 /su (2ss𝑛))}) ∪ ( bday “ {((𝑡 +s 1s ) /su (2ss𝑛))})) ∈ ω)
155141, 153, 154syl2anc 583 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ( ( bday “ {(𝑡 /su (2ss𝑛))}) ∪ ( bday “ {((𝑡 +s 1s ) /su (2ss𝑛))})) ∈ ω)
156133, 155eqeltrid 2848 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})) ∈ ω)
157 peano2 7929 . . . . . . . . . . . . . . . . . . 19 ( ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})) ∈ ω → suc ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})) ∈ ω)
158156, 157syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → suc ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})) ∈ ω)
159 nnon 7909 . . . . . . . . . . . . . . . . . 18 (suc ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})) ∈ ω → suc ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})) ∈ On)
160158, 159syl 17 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → suc ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})) ∈ On)
161 imassrn 6100 . . . . . . . . . . . . . . . . . . 19 ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})) ⊆ ran bday
162 bdayrn 27838 . . . . . . . . . . . . . . . . . . 19 ran bday = On
163161, 162sseqtri 4045 . . . . . . . . . . . . . . . . . 18 ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})) ⊆ On
164 onsucuni 7864 . . . . . . . . . . . . . . . . . 18 (( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})) ⊆ On → ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})) ⊆ suc ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})))
165163, 164mp1i 13 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})) ⊆ suc ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})))
166 scutbdaybnd 27878 . . . . . . . . . . . . . . . . 17 (({(𝑡 /su (2ss𝑛))} <<s {((𝑡 +s 1s ) /su (2ss𝑛))} ∧ suc ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})) ∈ On ∧ ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})) ⊆ suc ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))}))) → ( bday ‘({(𝑡 /su (2ss𝑛))} |s {((𝑡 +s 1s ) /su (2ss𝑛))})) ⊆ suc ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})))
167129, 160, 165, 166syl3anc 1371 . . . . . . . . . . . . . . . 16 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ( bday ‘({(𝑡 /su (2ss𝑛))} |s {((𝑡 +s 1s ) /su (2ss𝑛))})) ⊆ suc ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})))
168 bdayelon 27839 . . . . . . . . . . . . . . . . 17 ( bday ‘({(𝑡 /su (2ss𝑛))} |s {((𝑡 +s 1s ) /su (2ss𝑛))})) ∈ On
169 onsssuc 6485 . . . . . . . . . . . . . . . . 17 ((( bday ‘({(𝑡 /su (2ss𝑛))} |s {((𝑡 +s 1s ) /su (2ss𝑛))})) ∈ On ∧ suc ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})) ∈ On) → (( bday ‘({(𝑡 /su (2ss𝑛))} |s {((𝑡 +s 1s ) /su (2ss𝑛))})) ⊆ suc ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})) ↔ ( bday ‘({(𝑡 /su (2ss𝑛))} |s {((𝑡 +s 1s ) /su (2ss𝑛))})) ∈ suc suc ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))}))))
170168, 160, 169sylancr 586 . . . . . . . . . . . . . . . 16 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → (( bday ‘({(𝑡 /su (2ss𝑛))} |s {((𝑡 +s 1s ) /su (2ss𝑛))})) ⊆ suc ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})) ↔ ( bday ‘({(𝑡 /su (2ss𝑛))} |s {((𝑡 +s 1s ) /su (2ss𝑛))})) ∈ suc suc ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))}))))
171167, 170mpbid 232 . . . . . . . . . . . . . . 15 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ( bday ‘({(𝑡 /su (2ss𝑛))} |s {((𝑡 +s 1s ) /su (2ss𝑛))})) ∈ suc suc ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})))
172115, 171eqeltrd 2844 . . . . . . . . . . . . . 14 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ( bday ‘(((2s ·s 𝑡) +s 1s ) /su (2ss(𝑛 +s 1s )))) ∈ suc suc ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})))
173 peano2 7929 . . . . . . . . . . . . . . 15 (suc ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})) ∈ ω → suc suc ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})) ∈ ω)
174158, 173syl 17 . . . . . . . . . . . . . 14 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → suc suc ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})) ∈ ω)
175 elnn 7914 . . . . . . . . . . . . . 14 ((( bday ‘(((2s ·s 𝑡) +s 1s ) /su (2ss(𝑛 +s 1s )))) ∈ suc suc ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})) ∧ suc suc ( bday “ ({(𝑡 /su (2ss𝑛))} ∪ {((𝑡 +s 1s ) /su (2ss𝑛))})) ∈ ω) → ( bday ‘(((2s ·s 𝑡) +s 1s ) /su (2ss(𝑛 +s 1s )))) ∈ ω)
176172, 174, 175syl2anc 583 . . . . . . . . . . . . 13 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ( bday ‘(((2s ·s 𝑡) +s 1s ) /su (2ss(𝑛 +s 1s )))) ∈ ω)
177 fvoveq1 7471 . . . . . . . . . . . . . 14 (𝑤 = ((2s ·s 𝑡) +s 1s ) → ( bday ‘(𝑤 /su (2ss(𝑛 +s 1s )))) = ( bday ‘(((2s ·s 𝑡) +s 1s ) /su (2ss(𝑛 +s 1s )))))
178177eleq1d 2829 . . . . . . . . . . . . 13 (𝑤 = ((2s ·s 𝑡) +s 1s ) → (( bday ‘(𝑤 /su (2ss(𝑛 +s 1s )))) ∈ ω ↔ ( bday ‘(((2s ·s 𝑡) +s 1s ) /su (2ss(𝑛 +s 1s )))) ∈ ω))
179176, 178syl5ibrcom 247 . . . . . . . . . . . 12 (((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → (𝑤 = ((2s ·s 𝑡) +s 1s ) → ( bday ‘(𝑤 /su (2ss(𝑛 +s 1s )))) ∈ ω))
180179rexlimdva 3161 . . . . . . . . . . 11 ((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) → (∃𝑡 ∈ ℤs 𝑤 = ((2s ·s 𝑡) +s 1s ) → ( bday ‘(𝑤 /su (2ss(𝑛 +s 1s )))) ∈ ω))
18173, 180jaod 858 . . . . . . . . . 10 ((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) → ((∃𝑡 ∈ ℤs 𝑤 = (2s ·s 𝑡) ∨ ∃𝑡 ∈ ℤs 𝑤 = ((2s ·s 𝑡) +s 1s )) → ( bday ‘(𝑤 /su (2ss(𝑛 +s 1s )))) ∈ ω))
18239, 181syl5 34 . . . . . . . . 9 ((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) → (𝑤 ∈ ℤs → ( bday ‘(𝑤 /su (2ss(𝑛 +s 1s )))) ∈ ω))
183182ralrimiv 3151 . . . . . . . 8 ((𝑛 ∈ ℕ0s ∧ ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω) → ∀𝑤 ∈ ℤs ( bday ‘(𝑤 /su (2ss(𝑛 +s 1s )))) ∈ ω)
184183ex 412 . . . . . . 7 (𝑛 ∈ ℕ0s → (∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑛))) ∈ ω → ∀𝑤 ∈ ℤs ( bday ‘(𝑤 /su (2ss(𝑛 +s 1s )))) ∈ ω))
18512, 17, 26, 31, 38, 184n0sind 28355 . . . . . 6 (𝑦 ∈ ℕ0s → ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑦))) ∈ ω)
186185adantl 481 . . . . 5 ((𝑥 ∈ ℤs𝑦 ∈ ℕ0s) → ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su (2ss𝑦))) ∈ ω)
187 simpl 482 . . . . 5 ((𝑥 ∈ ℤs𝑦 ∈ ℕ0s) → 𝑥 ∈ ℤs)
1883, 186, 187rspcdva 3636 . . . 4 ((𝑥 ∈ ℤs𝑦 ∈ ℕ0s) → ( bday ‘(𝑥 /su (2ss𝑦))) ∈ ω)
189 fveq2 6920 . . . . 5 (𝐴 = (𝑥 /su (2ss𝑦)) → ( bday 𝐴) = ( bday ‘(𝑥 /su (2ss𝑦))))
190189eleq1d 2829 . . . 4 (𝐴 = (𝑥 /su (2ss𝑦)) → (( bday 𝐴) ∈ ω ↔ ( bday ‘(𝑥 /su (2ss𝑦))) ∈ ω))
191188, 190syl5ibrcom 247 . . 3 ((𝑥 ∈ ℤs𝑦 ∈ ℕ0s) → (𝐴 = (𝑥 /su (2ss𝑦)) → ( bday 𝐴) ∈ ω))
192191rexlimivv 3207 . 2 (∃𝑥 ∈ ℤs𝑦 ∈ ℕ0s 𝐴 = (𝑥 /su (2ss𝑦)) → ( bday 𝐴) ∈ ω)
1931, 192sylbi 217 1 (𝐴 ∈ ℤs[1/2] → ( bday 𝐴) ∈ ω)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wo 846   = wceq 1537  wcel 2108  wne 2946  wral 3067  wrex 3076  cun 3974  wss 3976  {csn 4648   cuni 4931   class class class wbr 5166  ran crn 5701  cima 5703  Oncon0 6395  suc csuc 6397   Fn wfn 6568  cfv 6573  (class class class)co 7448  ωcom 7903   No csur 27702   <s cslt 27703   bday cbday 27704   <<s csslt 27843   |s cscut 27845   0s c0s 27885   1s c1s 27886   +s cadds 28010   -s csubs 28070   ·s cmuls 28150   /su cdivs 28231  0scnn0s 28336  scnns 28337  sczs 28382  2sc2s 28412  scexps 28414  s[1/2]czs12 28416
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-dc 10515
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-tp 4653  df-op 4655  df-ot 4657  df-uni 4932  df-int 4971  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-1st 8030  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-2o 8523  df-oadd 8526  df-nadd 8722  df-no 27705  df-slt 27706  df-bday 27707  df-sle 27808  df-sslt 27844  df-scut 27846  df-0s 27887  df-1s 27888  df-made 27904  df-old 27905  df-left 27907  df-right 27908  df-norec 27989  df-norec2 28000  df-adds 28011  df-negs 28071  df-subs 28072  df-muls 28151  df-divs 28232  df-seqs 28308  df-n0s 28338  df-nns 28339  df-zs 28383  df-2s 28413  df-exps 28415  df-zs12 28417
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator