Step | Hyp | Ref
| Expression |
1 | | elzs12 28430 |
. 2
⊢ (𝐴 ∈ ℤs[1/2]
↔ ∃𝑥 ∈
ℤs ∃𝑦 ∈ ℕ0s 𝐴 = (𝑥 /su
(2s↑s𝑦))) |
2 | | fvoveq1 7468 |
. . . . . 6
⊢ (𝑧 = 𝑥 → ( bday
‘(𝑧
/su (2s↑s𝑦))) = ( bday
‘(𝑥
/su (2s↑s𝑦)))) |
3 | 2 | eleq1d 2823 |
. . . . 5
⊢ (𝑧 = 𝑥 → (( bday
‘(𝑧
/su (2s↑s𝑦))) ∈ ω ↔ ( bday ‘(𝑥 /su
(2s↑s𝑦))) ∈ ω)) |
4 | | oveq2 7453 |
. . . . . . . . . . . 12
⊢ (𝑚 = 0s →
(2s↑s𝑚) = (2s↑s
0s )) |
5 | | 2sno 28412 |
. . . . . . . . . . . . 13
⊢
2s ∈ No |
6 | | exps0 28419 |
. . . . . . . . . . . . 13
⊢
(2s ∈ No →
(2s↑s 0s ) = 1s
) |
7 | 5, 6 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(2s↑s 0s ) =
1s |
8 | 4, 7 | eqtrdi 2790 |
. . . . . . . . . . 11
⊢ (𝑚 = 0s →
(2s↑s𝑚) = 1s ) |
9 | 8 | oveq2d 7461 |
. . . . . . . . . 10
⊢ (𝑚 = 0s → (𝑧 /su
(2s↑s𝑚)) = (𝑧 /su 1s
)) |
10 | 9 | fveq2d 6923 |
. . . . . . . . 9
⊢ (𝑚 = 0s → ( bday ‘(𝑧 /su
(2s↑s𝑚))) = ( bday
‘(𝑧
/su 1s ))) |
11 | 10 | eleq1d 2823 |
. . . . . . . 8
⊢ (𝑚 = 0s → (( bday ‘(𝑧 /su
(2s↑s𝑚))) ∈ ω ↔ ( bday ‘(𝑧 /su 1s )) ∈
ω)) |
12 | 11 | ralbidv 3180 |
. . . . . . 7
⊢ (𝑚 = 0s →
(∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑚))) ∈ ω ↔ ∀𝑧 ∈ ℤs
( bday ‘(𝑧 /su 1s )) ∈
ω)) |
13 | | oveq2 7453 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (2s↑s𝑚) =
(2s↑s𝑛)) |
14 | 13 | oveq2d 7461 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (𝑧 /su
(2s↑s𝑚)) = (𝑧 /su
(2s↑s𝑛))) |
15 | 14 | fveq2d 6923 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → ( bday
‘(𝑧
/su (2s↑s𝑚))) = ( bday
‘(𝑧
/su (2s↑s𝑛)))) |
16 | 15 | eleq1d 2823 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → (( bday
‘(𝑧
/su (2s↑s𝑚))) ∈ ω ↔ ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω)) |
17 | 16 | ralbidv 3180 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su
(2s↑s𝑚))) ∈ ω ↔ ∀𝑧 ∈ ℤs
( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω)) |
18 | | oveq2 7453 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑛 +s 1s ) →
(2s↑s𝑚) = (2s↑s(𝑛 +s 1s
))) |
19 | 18 | oveq2d 7461 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛 +s 1s ) → (𝑧 /su
(2s↑s𝑚)) = (𝑧 /su
(2s↑s(𝑛 +s 1s
)))) |
20 | 19 | fveq2d 6923 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑛 +s 1s ) → ( bday ‘(𝑧 /su
(2s↑s𝑚))) = ( bday
‘(𝑧
/su (2s↑s(𝑛 +s 1s
))))) |
21 | 20 | eleq1d 2823 |
. . . . . . . . 9
⊢ (𝑚 = (𝑛 +s 1s ) → (( bday ‘(𝑧 /su
(2s↑s𝑚))) ∈ ω ↔ ( bday ‘(𝑧 /su
(2s↑s(𝑛 +s 1s )))) ∈
ω)) |
22 | 21 | ralbidv 3180 |
. . . . . . . 8
⊢ (𝑚 = (𝑛 +s 1s ) →
(∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑚))) ∈ ω ↔ ∀𝑧 ∈ ℤs
( bday ‘(𝑧 /su
(2s↑s(𝑛 +s 1s )))) ∈
ω)) |
23 | | fvoveq1 7468 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑤 → ( bday
‘(𝑧
/su (2s↑s(𝑛 +s 1s )))) = ( bday ‘(𝑤 /su
(2s↑s(𝑛 +s 1s
))))) |
24 | 23 | eleq1d 2823 |
. . . . . . . . 9
⊢ (𝑧 = 𝑤 → (( bday
‘(𝑧
/su (2s↑s(𝑛 +s 1s )))) ∈
ω ↔ ( bday ‘(𝑤 /su
(2s↑s(𝑛 +s 1s )))) ∈
ω)) |
25 | 24 | cbvralvw 3238 |
. . . . . . . 8
⊢
(∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s(𝑛 +s 1s )))) ∈
ω ↔ ∀𝑤
∈ ℤs ( bday ‘(𝑤 /su
(2s↑s(𝑛 +s 1s )))) ∈
ω) |
26 | 22, 25 | bitrdi 287 |
. . . . . . 7
⊢ (𝑚 = (𝑛 +s 1s ) →
(∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑚))) ∈ ω ↔ ∀𝑤 ∈ ℤs
( bday ‘(𝑤 /su
(2s↑s(𝑛 +s 1s )))) ∈
ω)) |
27 | | oveq2 7453 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑦 → (2s↑s𝑚) =
(2s↑s𝑦)) |
28 | 27 | oveq2d 7461 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑦 → (𝑧 /su
(2s↑s𝑚)) = (𝑧 /su
(2s↑s𝑦))) |
29 | 28 | fveq2d 6923 |
. . . . . . . . 9
⊢ (𝑚 = 𝑦 → ( bday
‘(𝑧
/su (2s↑s𝑚))) = ( bday
‘(𝑧
/su (2s↑s𝑦)))) |
30 | 29 | eleq1d 2823 |
. . . . . . . 8
⊢ (𝑚 = 𝑦 → (( bday
‘(𝑧
/su (2s↑s𝑚))) ∈ ω ↔ ( bday ‘(𝑧 /su
(2s↑s𝑦))) ∈ ω)) |
31 | 30 | ralbidv 3180 |
. . . . . . 7
⊢ (𝑚 = 𝑦 → (∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su
(2s↑s𝑚))) ∈ ω ↔ ∀𝑧 ∈ ℤs
( bday ‘(𝑧 /su
(2s↑s𝑦))) ∈ ω)) |
32 | | zno 28377 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℤs
→ 𝑧 ∈ No ) |
33 | | divs1 28238 |
. . . . . . . . . . 11
⊢ (𝑧 ∈
No → (𝑧
/su 1s ) = 𝑧) |
34 | 32, 33 | syl 17 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℤs
→ (𝑧
/su 1s ) = 𝑧) |
35 | 34 | fveq2d 6923 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℤs
→ ( bday ‘(𝑧 /su 1s )) = ( bday ‘𝑧)) |
36 | | zsbday 28401 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℤs
→ ( bday ‘𝑧) ∈ ω) |
37 | 35, 36 | eqeltrd 2838 |
. . . . . . . 8
⊢ (𝑧 ∈ ℤs
→ ( bday ‘(𝑧 /su 1s )) ∈
ω) |
38 | 37 | rgen 3065 |
. . . . . . 7
⊢
∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
1s )) ∈ ω |
39 | | zseo 28415 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ℤs
→ (∃𝑡 ∈
ℤs 𝑤 =
(2s ·s 𝑡) ∨ ∃𝑡 ∈ ℤs 𝑤 = ((2s
·s 𝑡)
+s 1s ))) |
40 | | expsp1 28421 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((2s ∈ No ∧ 𝑛 ∈ ℕ0s)
→ (2s↑s(𝑛 +s 1s )) =
((2s↑s𝑛) ·s
2s)) |
41 | 5, 40 | mpan 689 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℕ0s
→ (2s↑s(𝑛 +s 1s )) =
((2s↑s𝑛) ·s
2s)) |
42 | 41 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ ℕ0s
∧ 𝑡 ∈
ℤs) → (2s↑s(𝑛 +s 1s )) =
((2s↑s𝑛) ·s
2s)) |
43 | 42 | oveq2d 7461 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ ℕ0s
∧ 𝑡 ∈
ℤs) → ((2s ·s 𝑡) /su
(2s↑s(𝑛 +s 1s ))) =
((2s ·s 𝑡) /su
((2s↑s𝑛) ·s
2s))) |
44 | 5 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ ℕ0s
∧ 𝑡 ∈
ℤs) → 2s ∈ No
) |
45 | | zno 28377 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 ∈ ℤs
→ 𝑡 ∈ No ) |
46 | 45 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ ℕ0s
∧ 𝑡 ∈
ℤs) → 𝑡 ∈ No
) |
47 | 44, 46 | mulscld 28170 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ ℕ0s
∧ 𝑡 ∈
ℤs) → (2s ·s 𝑡) ∈
No ) |
48 | | expscl 28422 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((2s ∈ No ∧ 𝑛 ∈ ℕ0s)
→ (2s↑s𝑛) ∈ No
) |
49 | 5, 48 | mpan 689 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℕ0s
→ (2s↑s𝑛) ∈ No
) |
50 | 49 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ ℕ0s
∧ 𝑡 ∈
ℤs) → (2s↑s𝑛) ∈ No
) |
51 | | 2ne0s 28413 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
2s ≠ 0s |
52 | | expsne0 28423 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((2s ∈ No ∧
2s ≠ 0s ∧ 𝑛 ∈ ℕ0s) →
(2s↑s𝑛) ≠ 0s ) |
53 | 5, 51, 52 | mp3an12 1451 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℕ0s
→ (2s↑s𝑛) ≠ 0s ) |
54 | 53 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ ℕ0s
∧ 𝑡 ∈
ℤs) → (2s↑s𝑛) ≠ 0s ) |
55 | 51 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ ℕ0s
∧ 𝑡 ∈
ℤs) → 2s ≠ 0s ) |
56 | 47, 50, 44, 54, 55 | divdivs1d 28266 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ ℕ0s
∧ 𝑡 ∈
ℤs) → (((2s ·s 𝑡) /su
(2s↑s𝑛)) /su 2s) =
((2s ·s 𝑡) /su
((2s↑s𝑛) ·s
2s))) |
57 | 44, 46, 50, 54 | divsassd 28264 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ ℕ0s
∧ 𝑡 ∈
ℤs) → ((2s ·s 𝑡) /su
(2s↑s𝑛)) = (2s ·s
(𝑡 /su
(2s↑s𝑛)))) |
58 | 57 | oveq1d 7460 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ ℕ0s
∧ 𝑡 ∈
ℤs) → (((2s ·s 𝑡) /su
(2s↑s𝑛)) /su 2s) =
((2s ·s (𝑡 /su
(2s↑s𝑛))) /su
2s)) |
59 | 43, 56, 58 | 3eqtr2d 2780 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℕ0s
∧ 𝑡 ∈
ℤs) → ((2s ·s 𝑡) /su
(2s↑s(𝑛 +s 1s ))) =
((2s ·s (𝑡 /su
(2s↑s𝑛))) /su
2s)) |
60 | 46, 50, 54 | divscld 28257 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ ℕ0s
∧ 𝑡 ∈
ℤs) → (𝑡 /su
(2s↑s𝑛)) ∈ No
) |
61 | 60, 44, 55 | divscan3d 28269 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℕ0s
∧ 𝑡 ∈
ℤs) → ((2s ·s (𝑡 /su
(2s↑s𝑛))) /su 2s) =
(𝑡 /su
(2s↑s𝑛))) |
62 | 59, 61 | eqtrd 2774 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ℕ0s
∧ 𝑡 ∈
ℤs) → ((2s ·s 𝑡) /su
(2s↑s(𝑛 +s 1s ))) = (𝑡 /su
(2s↑s𝑛))) |
63 | 62 | fveq2d 6923 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℕ0s
∧ 𝑡 ∈
ℤs) → ( bday
‘((2s ·s 𝑡) /su
(2s↑s(𝑛 +s 1s )))) = ( bday ‘(𝑡 /su
(2s↑s𝑛)))) |
64 | 63 | adantlr 714 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ( bday ‘((2s ·s 𝑡) /su
(2s↑s(𝑛 +s 1s )))) = ( bday ‘(𝑡 /su
(2s↑s𝑛)))) |
65 | | fvoveq1 7468 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑡 → ( bday
‘(𝑧
/su (2s↑s𝑛))) = ( bday
‘(𝑡
/su (2s↑s𝑛)))) |
66 | 65 | eleq1d 2823 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑡 → (( bday
‘(𝑧
/su (2s↑s𝑛))) ∈ ω ↔ ( bday ‘(𝑡 /su
(2s↑s𝑛))) ∈ ω)) |
67 | 66 | rspccva 3630 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω ∧ 𝑡 ∈ ℤs) → ( bday ‘(𝑡 /su
(2s↑s𝑛))) ∈ ω) |
68 | 67 | adantll 713 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ( bday ‘(𝑡 /su
(2s↑s𝑛))) ∈ ω) |
69 | 64, 68 | eqeltrd 2838 |
. . . . . . . . . . . . 13
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ( bday ‘((2s ·s 𝑡) /su
(2s↑s(𝑛 +s 1s )))) ∈
ω) |
70 | | fvoveq1 7468 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = (2s
·s 𝑡)
→ ( bday ‘(𝑤 /su
(2s↑s(𝑛 +s 1s )))) = ( bday ‘((2s ·s 𝑡) /su
(2s↑s(𝑛 +s 1s
))))) |
71 | 70 | eleq1d 2823 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (2s
·s 𝑡)
→ (( bday ‘(𝑤 /su
(2s↑s(𝑛 +s 1s )))) ∈
ω ↔ ( bday ‘((2s
·s 𝑡)
/su (2s↑s(𝑛 +s 1s )))) ∈
ω)) |
72 | 69, 71 | syl5ibrcom 247 |
. . . . . . . . . . . 12
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → (𝑤 = (2s
·s 𝑡)
→ ( bday ‘(𝑤 /su
(2s↑s(𝑛 +s 1s )))) ∈
ω)) |
73 | 72 | rexlimdva 3157 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) → (∃𝑡 ∈ ℤs
𝑤 = (2s
·s 𝑡)
→ ( bday ‘(𝑤 /su
(2s↑s(𝑛 +s 1s )))) ∈
ω)) |
74 | 45 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → 𝑡 ∈
No ) |
75 | | no2times 28410 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 ∈
No → (2s ·s 𝑡) = (𝑡 +s 𝑡)) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) →
(2s ·s 𝑡) = (𝑡 +s 𝑡)) |
77 | 76 | oveq1d 7460 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) →
((2s ·s 𝑡) +s 1s ) = ((𝑡 +s 𝑡) +s 1s
)) |
78 | | 1sno 27881 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
1s ∈ No |
79 | 78 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) →
1s ∈ No ) |
80 | 74, 74, 79 | addsassd 28048 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ((𝑡 +s 𝑡) +s 1s )
= (𝑡 +s (𝑡 +s 1s
))) |
81 | 77, 80 | eqtrd 2774 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) →
((2s ·s 𝑡) +s 1s ) = (𝑡 +s (𝑡 +s 1s
))) |
82 | 81 | oveq1d 7460 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑛 ∈ ℕ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 28022 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → (𝑡 +s 1s )
∈ No ) |
84 | | simpll 766 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → 𝑛 ∈
ℕ0s) |
85 | 74 | sltp1d 28057 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → 𝑡 <s (𝑡 +s 1s
)) |
86 | | 2nns 28411 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
2s ∈ ℕs |
87 | | nnzs 28381 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(2s ∈ ℕs → 2s ∈
ℤs) |
88 | 86, 87 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) →
2s ∈ ℤs) |
89 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → 𝑡 ∈
ℤs) |
90 | 88, 89 | zmulscld 28392 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) →
(2s ·s 𝑡) ∈
ℤs) |
91 | 90 | znod 28378 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) →
(2s ·s 𝑡) ∈ No
) |
92 | | pncans 28111 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((2s ·s 𝑡) ∈ No
∧ 1s ∈ No ) →
(((2s ·s 𝑡) +s 1s ) -s
1s ) = (2s ·s 𝑡)) |
93 | 91, 78, 92 | sylancl 585 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) →
(((2s ·s 𝑡) +s 1s ) -s
1s ) = (2s ·s 𝑡)) |
94 | 93 | eqcomd 2740 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) →
(2s ·s 𝑡) = (((2s ·s
𝑡) +s
1s ) -s 1s )) |
95 | 94 | sneqd 4660 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) →
{(2s ·s 𝑡)} = {(((2s ·s
𝑡) +s
1s ) -s 1s )}) |
96 | | mulsrid 28148 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(2s ∈ No →
(2s ·s 1s ) =
2s) |
97 | 5, 96 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(2s ·s 1s ) =
2s |
98 | | 1p1e2s 28409 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (
1s +s 1s ) = 2s |
99 | 97, 98 | eqtr4i 2765 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(2s ·s 1s ) = ( 1s
+s 1s ) |
100 | 99 | oveq2i 7456 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((2s ·s 𝑡) +s (2s
·s 1s )) = ((2s ·s
𝑡) +s (
1s +s 1s )) |
101 | 5 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) →
2s ∈ No ) |
102 | 101, 74, 79 | addsdid 28191 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) →
(2s ·s (𝑡 +s 1s )) =
((2s ·s 𝑡) +s (2s
·s 1s ))) |
103 | 91, 79, 79 | addsassd 28048 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) →
(((2s ·s 𝑡) +s 1s ) +s
1s ) = ((2s ·s 𝑡) +s ( 1s +s
1s ))) |
104 | 100, 102,
103 | 3eqtr4a 2800 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) →
(2s ·s (𝑡 +s 1s )) =
(((2s ·s 𝑡) +s 1s ) +s
1s )) |
105 | 104 | sneqd 4660 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) →
{(2s ·s (𝑡 +s 1s ))} =
{(((2s ·s 𝑡) +s 1s ) +s
1s )}) |
106 | 95, 105 | oveq12d 7463 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ ℕ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 28386 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
1s ∈ ℤs |
108 | 107 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) →
1s ∈ ℤs) |
109 | 90, 108 | zaddscld 28390 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) →
((2s ·s 𝑡) +s 1s ) ∈
ℤs) |
110 | | zscut 28402 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((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 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ ℕ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 2780 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) →
({(2s ·s 𝑡)} |s {(2s ·s
(𝑡 +s
1s ))}) = (𝑡
+s (𝑡
+s 1s ))) |
113 | 74, 83, 84, 85, 112 | pw2cut 28429 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑛 ∈ ℕ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 2777 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 ∈ ℕ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 6923 |
. . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ ℕ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 725 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) →
(2s↑s𝑛) ∈ No
) |
117 | 53 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) →
(2s↑s𝑛) ≠ 0s ) |
118 | 74, 116, 117 | divscld 28257 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → (𝑡 /su
(2s↑s𝑛)) ∈ No
) |
119 | 83, 116, 117 | divscld 28257 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ((𝑡 +s 1s )
/su (2s↑s𝑛)) ∈ No
) |
120 | 74, 116, 117 | divscan2d 28258 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) →
((2s↑s𝑛) ·s (𝑡 /su
(2s↑s𝑛))) = 𝑡) |
121 | 120, 85 | eqbrtrd 5191 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) →
((2s↑s𝑛) ·s (𝑡 /su
(2s↑s𝑛))) <s (𝑡 +s 1s
)) |
122 | | nnsgt0 28351 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(2s ∈ ℕs → 0s <s
2s) |
123 | 86, 122 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
0s <s 2s |
124 | | expsgt0 28424 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((2s ∈ No ∧ 𝑛 ∈ ℕ0s
∧ 0s <s 2s) → 0s <s
(2s↑s𝑛)) |
125 | 5, 123, 124 | mp3an13 1452 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ ℕ0s
→ 0s <s (2s↑s𝑛)) |
126 | 125 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) →
0s <s (2s↑s𝑛)) |
127 | 118, 83, 116, 126 | sltmuldiv2d 28263 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ ℕ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 232 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → (𝑡 /su
(2s↑s𝑛)) <s ((𝑡 +s 1s )
/su (2s↑s𝑛))) |
129 | 118, 119,
128 | ssltsn 27846 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → {(𝑡 /su
(2s↑s𝑛))} <<s {((𝑡 +s 1s )
/su (2s↑s𝑛))}) |
130 | | imaundi 6180 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ( bday “ ({(𝑡 /su
(2s↑s𝑛))} ∪ {((𝑡 +s 1s )
/su (2s↑s𝑛))})) = (( bday
“ {(𝑡
/su (2s↑s𝑛))}) ∪ ( bday
“ {((𝑡
+s 1s ) /su
(2s↑s𝑛))})) |
131 | 130 | unieqi 4943 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ∪ ( bday “ ({(𝑡 /su
(2s↑s𝑛))} ∪ {((𝑡 +s 1s )
/su (2s↑s𝑛))})) = ∪ (( bday “ {(𝑡 /su
(2s↑s𝑛))}) ∪ ( bday
“ {((𝑡
+s 1s ) /su
(2s↑s𝑛))})) |
132 | | uniun 4956 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ∪ (( bday “ {(𝑡 /su
(2s↑s𝑛))}) ∪ ( bday
“ {((𝑡
+s 1s ) /su
(2s↑s𝑛))})) = (∪ ( bday “ {(𝑡 /su
(2s↑s𝑛))}) ∪ ∪
( bday “ {((𝑡 +s 1s )
/su (2s↑s𝑛))})) |
133 | 131, 132 | eqtri 2762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∪ ( bday “ ({(𝑡 /su
(2s↑s𝑛))} ∪ {((𝑡 +s 1s )
/su (2s↑s𝑛))})) = (∪ ( bday “ {(𝑡 /su
(2s↑s𝑛))}) ∪ ∪
( bday “ {((𝑡 +s 1s )
/su (2s↑s𝑛))})) |
134 | | bdayfn 27827 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ bday Fn No
|
135 | | fnsnfv 6999 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (( bday Fn No ∧ (𝑡 /su
(2s↑s𝑛)) ∈ No )
→ {( bday ‘(𝑡 /su
(2s↑s𝑛)))} = ( bday
“ {(𝑡
/su (2s↑s𝑛))})) |
136 | 134, 118,
135 | sylancr 586 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → {( bday ‘(𝑡 /su
(2s↑s𝑛)))} = ( bday
“ {(𝑡
/su (2s↑s𝑛))})) |
137 | 136 | unieqd 4944 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ∪ {( bday ‘(𝑡 /su
(2s↑s𝑛)))} = ∪ ( bday “ {(𝑡 /su
(2s↑s𝑛))})) |
138 | | fvex 6932 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ( bday ‘(𝑡 /su
(2s↑s𝑛))) ∈ V |
139 | 138 | unisn 4952 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ∪ {( bday ‘(𝑡 /su
(2s↑s𝑛)))} = ( bday
‘(𝑡
/su (2s↑s𝑛))) |
140 | 137, 139 | eqtr3di 2789 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ∪ ( bday “ {(𝑡 /su
(2s↑s𝑛))}) = ( bday
‘(𝑡
/su (2s↑s𝑛)))) |
141 | 140, 68 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ∪ ( bday “ {(𝑡 /su
(2s↑s𝑛))}) ∈ ω) |
142 | | fnsnfv 6999 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (( 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 586 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → {( bday ‘((𝑡 +s 1s )
/su (2s↑s𝑛)))} = ( bday
“ {((𝑡 +s
1s ) /su (2s↑s𝑛))})) |
144 | 143 | unieqd 4944 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ∪ {( bday ‘((𝑡 +s 1s )
/su (2s↑s𝑛)))} = ∪ ( bday “ {((𝑡 +s 1s )
/su (2s↑s𝑛))})) |
145 | | fvex 6932 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ( bday ‘((𝑡 +s 1s )
/su (2s↑s𝑛))) ∈ V |
146 | 145 | unisn 4952 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ∪ {( bday ‘((𝑡 +s 1s )
/su (2s↑s𝑛)))} = ( bday
‘((𝑡
+s 1s ) /su
(2s↑s𝑛))) |
147 | 144, 146 | eqtr3di 2789 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ∪ ( bday “ {((𝑡 +s 1s )
/su (2s↑s𝑛))}) = ( bday
‘((𝑡
+s 1s ) /su
(2s↑s𝑛)))) |
148 | | fvoveq1 7468 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 = (𝑡 +s 1s ) → ( bday ‘(𝑧 /su
(2s↑s𝑛))) = ( bday
‘((𝑡
+s 1s ) /su
(2s↑s𝑛)))) |
149 | 148 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = (𝑡 +s 1s ) → (( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω ↔ ( bday ‘((𝑡 +s 1s )
/su (2s↑s𝑛))) ∈ ω)) |
150 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) →
∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) |
151 | 89, 108 | zaddscld 28390 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → (𝑡 +s 1s )
∈ ℤs) |
152 | 149, 150,
151 | rspcdva 3632 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ( bday ‘((𝑡 +s 1s )
/su (2s↑s𝑛))) ∈ ω) |
153 | 147, 152 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ∪ ( bday “ {((𝑡 +s 1s )
/su (2s↑s𝑛))}) ∈ ω) |
154 | | omun 7922 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((∪ ( 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 583 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → (∪ ( bday “ {(𝑡 /su
(2s↑s𝑛))}) ∪ ∪
( bday “ {((𝑡 +s 1s )
/su (2s↑s𝑛))})) ∈ ω) |
156 | 133, 155 | eqeltrid 2842 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ∪ ( bday “ ({(𝑡 /su
(2s↑s𝑛))} ∪ {((𝑡 +s 1s )
/su (2s↑s𝑛))})) ∈ ω) |
157 | | peano2 7925 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∪ ( bday “ ({(𝑡 /su
(2s↑s𝑛))} ∪ {((𝑡 +s 1s )
/su (2s↑s𝑛))})) ∈ ω → suc ∪ ( bday “ ({(𝑡 /su
(2s↑s𝑛))} ∪ {((𝑡 +s 1s )
/su (2s↑s𝑛))})) ∈ ω) |
158 | 156, 157 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → suc ∪ ( bday “ ({(𝑡 /su
(2s↑s𝑛))} ∪ {((𝑡 +s 1s )
/su (2s↑s𝑛))})) ∈ ω) |
159 | | nnon 7905 |
. . . . . . . . . . . . . . . . . 18
⊢ (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 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → suc ∪ ( bday “ ({(𝑡 /su
(2s↑s𝑛))} ∪ {((𝑡 +s 1s )
/su (2s↑s𝑛))})) ∈ On) |
161 | | imassrn 6099 |
. . . . . . . . . . . . . . . . . . 19
⊢ ( bday “ ({(𝑡 /su
(2s↑s𝑛))} ∪ {((𝑡 +s 1s )
/su (2s↑s𝑛))})) ⊆ ran bday
|
162 | | bdayrn 27829 |
. . . . . . . . . . . . . . . . . . 19
⊢ ran bday = On |
163 | 161, 162 | sseqtri 4039 |
. . . . . . . . . . . . . . . . . 18
⊢ ( bday “ ({(𝑡 /su
(2s↑s𝑛))} ∪ {((𝑡 +s 1s )
/su (2s↑s𝑛))})) ⊆ On |
164 | | onsucuni 7860 |
. . . . . . . . . . . . . . . . . 18
⊢ (( 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 13 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑛 ∈ ℕ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 27869 |
. . . . . . . . . . . . . . . . 17
⊢ (({(𝑡 /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 1371 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 ∈ ℕ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 27830 |
. . . . . . . . . . . . . . . . 17
⊢ ( bday ‘({(𝑡 /su
(2s↑s𝑛))} |s {((𝑡 +s 1s )
/su (2s↑s𝑛))})) ∈ On |
169 | | onsssuc 6484 |
. . . . . . . . . . . . . . . . 17
⊢ ((( 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 586 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 ∈ ℕ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 232 |
. . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ ℕ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 2838 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ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 7925 |
. . . . . . . . . . . . . . 15
⊢ (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 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → suc suc
∪ ( bday “
({(𝑡 /su
(2s↑s𝑛))} ∪ {((𝑡 +s 1s )
/su (2s↑s𝑛))})) ∈ ω) |
175 | | elnn 7910 |
. . . . . . . . . . . . . 14
⊢ ((( 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 583 |
. . . . . . . . . . . . 13
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → ( bday ‘(((2s ·s 𝑡) +s 1s )
/su (2s↑s(𝑛 +s 1s )))) ∈
ω) |
177 | | fvoveq1 7468 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = ((2s
·s 𝑡)
+s 1s ) → ( bday
‘(𝑤
/su (2s↑s(𝑛 +s 1s )))) = ( bday ‘(((2s ·s 𝑡) +s 1s )
/su (2s↑s(𝑛 +s 1s
))))) |
178 | 177 | eleq1d 2823 |
. . . . . . . . . . . . 13
⊢ (𝑤 = ((2s
·s 𝑡)
+s 1s ) → (( bday
‘(𝑤
/su (2s↑s(𝑛 +s 1s )))) ∈
ω ↔ ( bday ‘(((2s
·s 𝑡)
+s 1s ) /su
(2s↑s(𝑛 +s 1s )))) ∈
ω)) |
179 | 176, 178 | syl5ibrcom 247 |
. . . . . . . . . . . 12
⊢ (((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) ∧ 𝑡 ∈ ℤs) → (𝑤 = ((2s
·s 𝑡)
+s 1s ) → ( bday
‘(𝑤
/su (2s↑s(𝑛 +s 1s )))) ∈
ω)) |
180 | 179 | rexlimdva 3157 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) → (∃𝑡 ∈ ℤs
𝑤 = ((2s
·s 𝑡)
+s 1s ) → ( bday
‘(𝑤
/su (2s↑s(𝑛 +s 1s )))) ∈
ω)) |
181 | 73, 180 | jaod 858 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) → ((∃𝑡 ∈ ℤs
𝑤 = (2s
·s 𝑡)
∨ ∃𝑡 ∈
ℤs 𝑤 =
((2s ·s 𝑡) +s 1s )) →
( bday ‘(𝑤 /su
(2s↑s(𝑛 +s 1s )))) ∈
ω)) |
182 | 39, 181 | syl5 34 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) → (𝑤 ∈ ℤs
→ ( bday ‘(𝑤 /su
(2s↑s(𝑛 +s 1s )))) ∈
ω)) |
183 | 182 | ralrimiv 3147 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ0s
∧ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω) → ∀𝑤 ∈ ℤs
( bday ‘(𝑤 /su
(2s↑s(𝑛 +s 1s )))) ∈
ω) |
184 | 183 | ex 412 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0s
→ (∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑛))) ∈ ω → ∀𝑤 ∈ ℤs
( bday ‘(𝑤 /su
(2s↑s(𝑛 +s 1s )))) ∈
ω)) |
185 | 12, 17, 26, 31, 38, 184 | n0sind 28346 |
. . . . . 6
⊢ (𝑦 ∈ ℕ0s
→ ∀𝑧 ∈
ℤs ( bday ‘(𝑧 /su
(2s↑s𝑦))) ∈ ω) |
186 | 185 | adantl 481 |
. . . . 5
⊢ ((𝑥 ∈ ℤs
∧ 𝑦 ∈
ℕ0s) → ∀𝑧 ∈ ℤs ( bday ‘(𝑧 /su
(2s↑s𝑦))) ∈ ω) |
187 | | simpl 482 |
. . . . 5
⊢ ((𝑥 ∈ ℤs
∧ 𝑦 ∈
ℕ0s) → 𝑥 ∈ ℤs) |
188 | 3, 186, 187 | rspcdva 3632 |
. . . 4
⊢ ((𝑥 ∈ ℤs
∧ 𝑦 ∈
ℕ0s) → ( bday ‘(𝑥 /su
(2s↑s𝑦))) ∈ ω) |
189 | | fveq2 6919 |
. . . . 5
⊢ (𝐴 = (𝑥 /su
(2s↑s𝑦)) → ( bday
‘𝐴) = ( bday ‘(𝑥 /su
(2s↑s𝑦)))) |
190 | 189 | eleq1d 2823 |
. . . 4
⊢ (𝐴 = (𝑥 /su
(2s↑s𝑦)) → (( bday
‘𝐴) ∈
ω ↔ ( bday ‘(𝑥 /su
(2s↑s𝑦))) ∈ ω)) |
191 | 188, 190 | syl5ibrcom 247 |
. . 3
⊢ ((𝑥 ∈ ℤs
∧ 𝑦 ∈
ℕ0s) → (𝐴 = (𝑥 /su
(2s↑s𝑦)) → ( bday
‘𝐴) ∈
ω)) |
192 | 191 | rexlimivv 3203 |
. 2
⊢
(∃𝑥 ∈
ℤs ∃𝑦 ∈ ℕ0s 𝐴 = (𝑥 /su
(2s↑s𝑦)) → ( bday
‘𝐴) ∈
ω) |
193 | 1, 192 | sylbi 217 |
1
⊢ (𝐴 ∈ ℤs[1/2]
→ ( bday ‘𝐴) ∈ ω) |