Step | Hyp | Ref
| Expression |
1 | | 0sno 27772 |
. 2
⊢
0s ∈ No |
2 | | 1nns 28228 |
. . . 4
⊢
1s ∈ ℕs |
3 | | 0slt1s 27775 |
. . . . . . 7
⊢
0s <s 1s |
4 | | 1sno 27773 |
. . . . . . . 8
⊢
1s ∈ No |
5 | | sltneg 27970 |
. . . . . . . 8
⊢ ((
0s ∈ No ∧ 1s
∈ No ) → ( 0s <s
1s ↔ ( -us ‘ 1s ) <s (
-us ‘ 0s ))) |
6 | 1, 4, 5 | mp2an 691 |
. . . . . . 7
⊢ (
0s <s 1s ↔ ( -us ‘ 1s
) <s ( -us ‘ 0s )) |
7 | 3, 6 | mpbi 229 |
. . . . . 6
⊢ (
-us ‘ 1s ) <s ( -us ‘
0s ) |
8 | | negs0s 27952 |
. . . . . 6
⊢ (
-us ‘ 0s ) = 0s |
9 | 7, 8 | breqtri 5173 |
. . . . 5
⊢ (
-us ‘ 1s ) <s 0s |
10 | 9, 3 | pm3.2i 470 |
. . . 4
⊢ ((
-us ‘ 1s ) <s 0s ∧ 0s
<s 1s ) |
11 | | fveq2 6897 |
. . . . . . 7
⊢ (𝑛 = 1s → (
-us ‘𝑛) =
( -us ‘ 1s )) |
12 | 11 | breq1d 5158 |
. . . . . 6
⊢ (𝑛 = 1s → ((
-us ‘𝑛)
<s 0s ↔ ( -us ‘ 1s ) <s
0s )) |
13 | | breq2 5152 |
. . . . . 6
⊢ (𝑛 = 1s → (
0s <s 𝑛
↔ 0s <s 1s )) |
14 | 12, 13 | anbi12d 631 |
. . . . 5
⊢ (𝑛 = 1s → (((
-us ‘𝑛)
<s 0s ∧ 0s <s 𝑛) ↔ (( -us ‘
1s ) <s 0s ∧ 0s <s 1s
))) |
15 | 14 | rspcev 3609 |
. . . 4
⊢ ((
1s ∈ ℕs ∧ (( -us ‘
1s ) <s 0s ∧ 0s <s 1s ))
→ ∃𝑛 ∈
ℕs (( -us ‘𝑛) <s 0s ∧ 0s
<s 𝑛)) |
16 | 2, 10, 15 | mp2an 691 |
. . 3
⊢
∃𝑛 ∈
ℕs (( -us ‘𝑛) <s 0s ∧ 0s
<s 𝑛) |
17 | 4 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕs
→ 1s ∈ No ) |
18 | | nnsno 28209 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕs
→ 𝑛 ∈ No ) |
19 | | nnne0s 28218 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕs
→ 𝑛 ≠ 0s
) |
20 | 17, 18, 19 | divscld 28135 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕs
→ ( 1s /su 𝑛) ∈ No
) |
21 | 20 | negsval2d 27988 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕs
→ ( -us ‘( 1s /su 𝑛)) = ( 0s
-s ( 1s /su 𝑛))) |
22 | 21 | eqeq2d 2739 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕs
→ (𝑥 = (
-us ‘( 1s /su 𝑛)) ↔ 𝑥 = ( 0s -s (
1s /su 𝑛)))) |
23 | 22 | bicomd 222 |
. . . . . . 7
⊢ (𝑛 ∈ ℕs
→ (𝑥 = ( 0s
-s ( 1s /su 𝑛)) ↔ 𝑥 = ( -us ‘( 1s
/su 𝑛)))) |
24 | 23 | rexbiia 3089 |
. . . . . 6
⊢
(∃𝑛 ∈
ℕs 𝑥 = (
0s -s ( 1s /su 𝑛)) ↔ ∃𝑛 ∈ ℕs
𝑥 = ( -us
‘( 1s /su 𝑛))) |
25 | 24 | abbii 2798 |
. . . . 5
⊢ {𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = ( 0s
-s ( 1s /su 𝑛))} = {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( -us ‘(
1s /su 𝑛))} |
26 | | addslid 27898 |
. . . . . . . . 9
⊢ ((
1s /su 𝑛) ∈ No
→ ( 0s +s ( 1s /su 𝑛)) = ( 1s
/su 𝑛)) |
27 | 20, 26 | syl 17 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕs
→ ( 0s +s ( 1s /su 𝑛)) = ( 1s
/su 𝑛)) |
28 | 27 | eqeq2d 2739 |
. . . . . . 7
⊢ (𝑛 ∈ ℕs
→ (𝑥 = ( 0s
+s ( 1s /su 𝑛)) ↔ 𝑥 = ( 1s /su 𝑛))) |
29 | 28 | rexbiia 3089 |
. . . . . 6
⊢
(∃𝑛 ∈
ℕs 𝑥 = (
0s +s ( 1s /su 𝑛)) ↔ ∃𝑛 ∈ ℕs
𝑥 = ( 1s
/su 𝑛)) |
30 | 29 | abbii 2798 |
. . . . 5
⊢ {𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = ( 0s
+s ( 1s /su 𝑛))} = {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( 1s
/su 𝑛)} |
31 | 25, 30 | oveq12i 7432 |
. . . 4
⊢ ({𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = ( 0s
-s ( 1s /su 𝑛))} |s {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( 0s +s
( 1s /su 𝑛))}) = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( -us ‘(
1s /su 𝑛))} |s {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( 1s
/su 𝑛)}) |
32 | | nnsex 28203 |
. . . . . . . . 9
⊢
ℕs ∈ V |
33 | 32 | abrexex 7966 |
. . . . . . . 8
⊢ {𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = ( -us
‘( 1s /su 𝑛))} ∈ V |
34 | 33 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ {𝑥 ∣
∃𝑛 ∈
ℕs 𝑥 = (
-us ‘( 1s /su 𝑛))} ∈ V) |
35 | | snex 5433 |
. . . . . . . 8
⊢ {
0s } ∈ V |
36 | 35 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ { 0s } ∈ V) |
37 | 20 | negscld 27962 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕs
→ ( -us ‘( 1s /su 𝑛)) ∈
No ) |
38 | | eleq1 2817 |
. . . . . . . . . . 11
⊢ (𝑥 = ( -us ‘(
1s /su 𝑛)) → (𝑥 ∈ No
↔ ( -us ‘( 1s /su 𝑛)) ∈
No )) |
39 | 37, 38 | syl5ibrcom 246 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕs
→ (𝑥 = (
-us ‘( 1s /su 𝑛)) → 𝑥 ∈ No
)) |
40 | 39 | rexlimiv 3145 |
. . . . . . . . 9
⊢
(∃𝑛 ∈
ℕs 𝑥 = (
-us ‘( 1s /su 𝑛)) → 𝑥 ∈ No
) |
41 | 40 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ (∃𝑛 ∈
ℕs 𝑥 = (
-us ‘( 1s /su 𝑛)) → 𝑥 ∈ No
)) |
42 | 41 | abssdv 4063 |
. . . . . . 7
⊢ (⊤
→ {𝑥 ∣
∃𝑛 ∈
ℕs 𝑥 = (
-us ‘( 1s /su 𝑛))} ⊆ No
) |
43 | 1 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ 0s ∈ No ) |
44 | 43 | snssd 4813 |
. . . . . . 7
⊢ (⊤
→ { 0s } ⊆ No
) |
45 | | vex 3475 |
. . . . . . . . . . . 12
⊢ 𝑧 ∈ V |
46 | | eqeq1 2732 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → (𝑥 = ( -us ‘( 1s
/su 𝑛))
↔ 𝑧 = ( -us
‘( 1s /su 𝑛)))) |
47 | 46 | rexbidv 3175 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (∃𝑛 ∈ ℕs 𝑥 = ( -us ‘(
1s /su 𝑛)) ↔ ∃𝑛 ∈ ℕs 𝑧 = ( -us ‘(
1s /su 𝑛)))) |
48 | 45, 47 | elab 3667 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( -us ‘(
1s /su 𝑛))} ↔ ∃𝑛 ∈ ℕs 𝑧 = ( -us ‘(
1s /su 𝑛))) |
49 | | velsn 4645 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ { 0s } ↔
𝑦 = 0s
) |
50 | 48, 49 | anbi12i 627 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( -us ‘(
1s /su 𝑛))} ∧ 𝑦 ∈ { 0s }) ↔
(∃𝑛 ∈
ℕs 𝑧 = (
-us ‘( 1s /su 𝑛)) ∧ 𝑦 = 0s )) |
51 | | r19.41v 3185 |
. . . . . . . . . 10
⊢
(∃𝑛 ∈
ℕs (𝑧 = (
-us ‘( 1s /su 𝑛)) ∧ 𝑦 = 0s ) ↔ (∃𝑛 ∈ ℕs
𝑧 = ( -us
‘( 1s /su 𝑛)) ∧ 𝑦 = 0s )) |
52 | 50, 51 | bitr4i 278 |
. . . . . . . . 9
⊢ ((𝑧 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( -us ‘(
1s /su 𝑛))} ∧ 𝑦 ∈ { 0s }) ↔
∃𝑛 ∈
ℕs (𝑧 = (
-us ‘( 1s /su 𝑛)) ∧ 𝑦 = 0s )) |
53 | | muls02 28054 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈
No → ( 0s ·s 𝑛) = 0s ) |
54 | 18, 53 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕs
→ ( 0s ·s 𝑛) = 0s ) |
55 | 54, 3 | eqbrtrdi 5187 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕs
→ ( 0s ·s 𝑛) <s 1s ) |
56 | 1 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕs
→ 0s ∈ No ) |
57 | | nnsgt0 28220 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕs
→ 0s <s 𝑛) |
58 | 56, 17, 18, 57 | sltmuldivd 28140 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕs
→ (( 0s ·s 𝑛) <s 1s ↔ 0s
<s ( 1s /su 𝑛))) |
59 | 55, 58 | mpbid 231 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕs
→ 0s <s ( 1s /su 𝑛)) |
60 | 20 | slt0neg2d 27976 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕs
→ ( 0s <s ( 1s /su 𝑛) ↔ ( -us
‘( 1s /su 𝑛)) <s 0s )) |
61 | 59, 60 | mpbid 231 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕs
→ ( -us ‘( 1s /su 𝑛)) <s 0s
) |
62 | | breq12 5153 |
. . . . . . . . . . 11
⊢ ((𝑧 = ( -us ‘(
1s /su 𝑛)) ∧ 𝑦 = 0s ) → (𝑧 <s 𝑦 ↔ ( -us ‘(
1s /su 𝑛)) <s 0s )) |
63 | 61, 62 | syl5ibrcom 246 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕs
→ ((𝑧 = (
-us ‘( 1s /su 𝑛)) ∧ 𝑦 = 0s ) → 𝑧 <s 𝑦)) |
64 | 63 | rexlimiv 3145 |
. . . . . . . . 9
⊢
(∃𝑛 ∈
ℕs (𝑧 = (
-us ‘( 1s /su 𝑛)) ∧ 𝑦 = 0s ) → 𝑧 <s 𝑦) |
65 | 52, 64 | sylbi 216 |
. . . . . . . 8
⊢ ((𝑧 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( -us ‘(
1s /su 𝑛))} ∧ 𝑦 ∈ { 0s }) → 𝑧 <s 𝑦) |
66 | 65 | 3adant1 1128 |
. . . . . . 7
⊢
((⊤ ∧ 𝑧
∈ {𝑥 ∣
∃𝑛 ∈
ℕs 𝑥 = (
-us ‘( 1s /su 𝑛))} ∧ 𝑦 ∈ { 0s }) → 𝑧 <s 𝑦) |
67 | 34, 36, 42, 44, 66 | ssltd 27737 |
. . . . . 6
⊢ (⊤
→ {𝑥 ∣
∃𝑛 ∈
ℕs 𝑥 = (
-us ‘( 1s /su 𝑛))} <<s { 0s
}) |
68 | 32 | abrexex 7966 |
. . . . . . . 8
⊢ {𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = ( 1s
/su 𝑛)}
∈ V |
69 | 68 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ {𝑥 ∣
∃𝑛 ∈
ℕs 𝑥 = (
1s /su 𝑛)} ∈ V) |
70 | | eleq1 2817 |
. . . . . . . . . . 11
⊢ (𝑥 = ( 1s
/su 𝑛)
→ (𝑥 ∈ No ↔ ( 1s /su 𝑛) ∈
No )) |
71 | 20, 70 | syl5ibrcom 246 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕs
→ (𝑥 = ( 1s
/su 𝑛)
→ 𝑥 ∈ No )) |
72 | 71 | rexlimiv 3145 |
. . . . . . . . 9
⊢
(∃𝑛 ∈
ℕs 𝑥 = (
1s /su 𝑛) → 𝑥 ∈ No
) |
73 | 72 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ (∃𝑛 ∈
ℕs 𝑥 = (
1s /su 𝑛) → 𝑥 ∈ No
)) |
74 | 73 | abssdv 4063 |
. . . . . . 7
⊢ (⊤
→ {𝑥 ∣
∃𝑛 ∈
ℕs 𝑥 = (
1s /su 𝑛)} ⊆ No
) |
75 | | eqeq1 2732 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → (𝑥 = ( 1s /su 𝑛) ↔ 𝑧 = ( 1s /su 𝑛))) |
76 | 75 | rexbidv 3175 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (∃𝑛 ∈ ℕs 𝑥 = ( 1s
/su 𝑛)
↔ ∃𝑛 ∈
ℕs 𝑧 = (
1s /su 𝑛))) |
77 | 45, 76 | elab 3667 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( 1s
/su 𝑛)}
↔ ∃𝑛 ∈
ℕs 𝑧 = (
1s /su 𝑛)) |
78 | 49, 77 | anbi12i 627 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ { 0s } ∧
𝑧 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = ( 1s
/su 𝑛)})
↔ (𝑦 = 0s
∧ ∃𝑛 ∈
ℕs 𝑧 = (
1s /su 𝑛))) |
79 | | r19.42v 3187 |
. . . . . . . . . 10
⊢
(∃𝑛 ∈
ℕs (𝑦 =
0s ∧ 𝑧 = (
1s /su 𝑛)) ↔ (𝑦 = 0s ∧ ∃𝑛 ∈ ℕs
𝑧 = ( 1s
/su 𝑛))) |
80 | 78, 79 | bitr4i 278 |
. . . . . . . . 9
⊢ ((𝑦 ∈ { 0s } ∧
𝑧 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = ( 1s
/su 𝑛)})
↔ ∃𝑛 ∈
ℕs (𝑦 =
0s ∧ 𝑧 = (
1s /su 𝑛))) |
81 | | breq12 5153 |
. . . . . . . . . . . 12
⊢ ((𝑦 = 0s ∧ 𝑧 = ( 1s
/su 𝑛))
→ (𝑦 <s 𝑧 ↔ 0s <s (
1s /su 𝑛))) |
82 | 59, 81 | syl5ibrcom 246 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕs
→ ((𝑦 = 0s
∧ 𝑧 = ( 1s
/su 𝑛))
→ 𝑦 <s 𝑧)) |
83 | 82 | rexlimiv 3145 |
. . . . . . . . . 10
⊢
(∃𝑛 ∈
ℕs (𝑦 =
0s ∧ 𝑧 = (
1s /su 𝑛)) → 𝑦 <s 𝑧) |
84 | 83 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ (∃𝑛 ∈
ℕs (𝑦 =
0s ∧ 𝑧 = (
1s /su 𝑛)) → 𝑦 <s 𝑧)) |
85 | 80, 84 | biimtrid 241 |
. . . . . . . 8
⊢ (⊤
→ ((𝑦 ∈ {
0s } ∧ 𝑧
∈ {𝑥 ∣
∃𝑛 ∈
ℕs 𝑥 = (
1s /su 𝑛)}) → 𝑦 <s 𝑧)) |
86 | 85 | 3impib 1114 |
. . . . . . 7
⊢
((⊤ ∧ 𝑦
∈ { 0s } ∧ 𝑧 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( 1s
/su 𝑛)})
→ 𝑦 <s 𝑧) |
87 | 36, 69, 44, 74, 86 | ssltd 27737 |
. . . . . 6
⊢ (⊤
→ { 0s } <<s {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( 1s
/su 𝑛)}) |
88 | 67, 87 | cuteq0 27778 |
. . . . 5
⊢ (⊤
→ ({𝑥 ∣
∃𝑛 ∈
ℕs 𝑥 = (
-us ‘( 1s /su 𝑛))} |s {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( 1s
/su 𝑛)}) =
0s ) |
89 | 88 | mptru 1541 |
. . . 4
⊢ ({𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = ( -us
‘( 1s /su 𝑛))} |s {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( 1s
/su 𝑛)}) =
0s |
90 | 31, 89 | eqtr2i 2757 |
. . 3
⊢
0s = ({𝑥 ∣
∃𝑛 ∈
ℕs 𝑥 = (
0s -s ( 1s /su 𝑛))} |s {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( 0s +s
( 1s /su 𝑛))}) |
91 | 16, 90 | pm3.2i 470 |
. 2
⊢
(∃𝑛 ∈
ℕs (( -us ‘𝑛) <s 0s ∧ 0s
<s 𝑛) ∧
0s = ({𝑥 ∣
∃𝑛 ∈
ℕs 𝑥 = (
0s -s ( 1s /su 𝑛))} |s {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( 0s +s
( 1s /su 𝑛))})) |
92 | | elreno 28236 |
. 2
⊢ (
0s ∈ ℝs ↔ ( 0s ∈ No ∧ (∃𝑛 ∈ ℕs (( -us
‘𝑛) <s
0s ∧ 0s <s 𝑛) ∧ 0s = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( 0s -s
( 1s /su 𝑛))} |s {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( 0s +s
( 1s /su 𝑛))})))) |
93 | 1, 91, 92 | mpbir2an 710 |
1
⊢
0s ∈ ℝs |