| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 0sno 27871 | . 2
⊢ 
0s ∈  No | 
| 2 |  | 1nns 28352 | . . . 4
⊢ 
1s ∈ ℕs | 
| 3 |  | 0slt1s 27874 | . . . . . . 7
⊢ 
0s <s 1s | 
| 4 |  | 1sno 27872 | . . . . . . . 8
⊢ 
1s ∈  No | 
| 5 |  | sltneg 28077 | . . . . . . . 8
⊢ ((
0s ∈  No  ∧ 1s
∈  No ) → ( 0s <s
1s ↔ ( -us ‘ 1s ) <s (
-us ‘ 0s ))) | 
| 6 | 1, 4, 5 | mp2an 692 | . . . . . . 7
⊢ (
0s <s 1s ↔ ( -us ‘ 1s
) <s ( -us ‘ 0s )) | 
| 7 | 3, 6 | mpbi 230 | . . . . . 6
⊢ (
-us ‘ 1s ) <s ( -us ‘
0s ) | 
| 8 |  | negs0s 28058 | . . . . . 6
⊢ (
-us ‘ 0s ) = 0s | 
| 9 | 7, 8 | breqtri 5168 | . . . . 5
⊢ (
-us ‘ 1s ) <s 0s | 
| 10 | 9, 3 | pm3.2i 470 | . . . 4
⊢ ((
-us ‘ 1s ) <s 0s ∧ 0s
<s 1s ) | 
| 11 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑛 = 1s → (
-us ‘𝑛) =
( -us ‘ 1s )) | 
| 12 | 11 | breq1d 5153 | . . . . . 6
⊢ (𝑛 = 1s → ((
-us ‘𝑛)
<s 0s ↔ ( -us ‘ 1s ) <s
0s )) | 
| 13 |  | breq2 5147 | . . . . . 6
⊢ (𝑛 = 1s → (
0s <s 𝑛
↔ 0s <s 1s )) | 
| 14 | 12, 13 | anbi12d 632 | . . . . 5
⊢ (𝑛 = 1s → (((
-us ‘𝑛)
<s 0s ∧ 0s <s 𝑛) ↔ (( -us ‘
1s ) <s 0s ∧ 0s <s 1s
))) | 
| 15 | 14 | rspcev 3622 | . . . 4
⊢ ((
1s ∈ ℕs ∧ (( -us ‘
1s ) <s 0s ∧ 0s <s 1s ))
→ ∃𝑛 ∈
ℕs (( -us ‘𝑛) <s 0s ∧ 0s
<s 𝑛)) | 
| 16 | 2, 10, 15 | mp2an 692 | . . 3
⊢
∃𝑛 ∈
ℕs (( -us ‘𝑛) <s 0s ∧ 0s
<s 𝑛) | 
| 17 | 4 | a1i 11 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕs
→ 1s ∈  No ) | 
| 18 |  | nnsno 28329 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕs
→ 𝑛 ∈  No ) | 
| 19 |  | nnne0s 28340 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕs
→ 𝑛 ≠ 0s
) | 
| 20 | 17, 18, 19 | divscld 28248 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕs
→ ( 1s /su 𝑛) ∈  No
) | 
| 21 | 20 | negsval2d 28097 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕs
→ ( -us ‘( 1s /su 𝑛)) = ( 0s
-s ( 1s /su 𝑛))) | 
| 22 | 21 | eqeq2d 2748 | . . . . . . . 8
⊢ (𝑛 ∈ ℕs
→ (𝑥 = (
-us ‘( 1s /su 𝑛)) ↔ 𝑥 = ( 0s -s (
1s /su 𝑛)))) | 
| 23 | 22 | bicomd 223 | . . . . . . 7
⊢ (𝑛 ∈ ℕs
→ (𝑥 = ( 0s
-s ( 1s /su 𝑛)) ↔ 𝑥 = ( -us ‘( 1s
/su 𝑛)))) | 
| 24 | 23 | rexbiia 3092 | . . . . . 6
⊢
(∃𝑛 ∈
ℕs 𝑥 = (
0s -s ( 1s /su 𝑛)) ↔ ∃𝑛 ∈ ℕs
𝑥 = ( -us
‘( 1s /su 𝑛))) | 
| 25 | 24 | abbii 2809 | . . . . 5
⊢ {𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = ( 0s
-s ( 1s /su 𝑛))} = {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( -us ‘(
1s /su 𝑛))} | 
| 26 |  | addslid 28001 | . . . . . . . . 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 2748 | . . . . . . 7
⊢ (𝑛 ∈ ℕs
→ (𝑥 = ( 0s
+s ( 1s /su 𝑛)) ↔ 𝑥 = ( 1s /su 𝑛))) | 
| 29 | 28 | rexbiia 3092 | . . . . . 6
⊢
(∃𝑛 ∈
ℕs 𝑥 = (
0s +s ( 1s /su 𝑛)) ↔ ∃𝑛 ∈ ℕs
𝑥 = ( 1s
/su 𝑛)) | 
| 30 | 29 | abbii 2809 | . . . . 5
⊢ {𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = ( 0s
+s ( 1s /su 𝑛))} = {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( 1s
/su 𝑛)} | 
| 31 | 25, 30 | oveq12i 7443 | . . . 4
⊢ ({𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = ( 0s
-s ( 1s /su 𝑛))} |s {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( 0s +s
( 1s /su 𝑛))}) = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( -us ‘(
1s /su 𝑛))} |s {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( 1s
/su 𝑛)}) | 
| 32 |  | nnsex 28323 | . . . . . . . . 9
⊢
ℕs ∈ V | 
| 33 | 32 | abrexex 7987 | . . . . . . . 8
⊢ {𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = ( -us
‘( 1s /su 𝑛))} ∈ V | 
| 34 | 33 | a1i 11 | . . . . . . 7
⊢ (⊤
→ {𝑥 ∣
∃𝑛 ∈
ℕs 𝑥 = (
-us ‘( 1s /su 𝑛))} ∈ V) | 
| 35 |  | snex 5436 | . . . . . . . 8
⊢ {
0s } ∈ V | 
| 36 | 35 | a1i 11 | . . . . . . 7
⊢ (⊤
→ { 0s } ∈ V) | 
| 37 | 20 | negscld 28069 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕs
→ ( -us ‘( 1s /su 𝑛)) ∈ 
No ) | 
| 38 |  | eleq1 2829 | . . . . . . . . . . 11
⊢ (𝑥 = ( -us ‘(
1s /su 𝑛)) → (𝑥 ∈  No 
↔ ( -us ‘( 1s /su 𝑛)) ∈ 
No )) | 
| 39 | 37, 38 | syl5ibrcom 247 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕs
→ (𝑥 = (
-us ‘( 1s /su 𝑛)) → 𝑥 ∈  No
)) | 
| 40 | 39 | rexlimiv 3148 | . . . . . . . . 9
⊢
(∃𝑛 ∈
ℕs 𝑥 = (
-us ‘( 1s /su 𝑛)) → 𝑥 ∈  No
) | 
| 41 | 40 | a1i 11 | . . . . . . . 8
⊢ (⊤
→ (∃𝑛 ∈
ℕs 𝑥 = (
-us ‘( 1s /su 𝑛)) → 𝑥 ∈  No
)) | 
| 42 | 41 | abssdv 4068 | . . . . . . 7
⊢ (⊤
→ {𝑥 ∣
∃𝑛 ∈
ℕs 𝑥 = (
-us ‘( 1s /su 𝑛))} ⊆  No
) | 
| 43 | 1 | a1i 11 | . . . . . . . 8
⊢ (⊤
→ 0s ∈  No ) | 
| 44 | 43 | snssd 4809 | . . . . . . 7
⊢ (⊤
→ { 0s } ⊆  No
) | 
| 45 |  | vex 3484 | . . . . . . . . . . . 12
⊢ 𝑧 ∈ V | 
| 46 |  | eqeq1 2741 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → (𝑥 = ( -us ‘( 1s
/su 𝑛))
↔ 𝑧 = ( -us
‘( 1s /su 𝑛)))) | 
| 47 | 46 | rexbidv 3179 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (∃𝑛 ∈ ℕs 𝑥 = ( -us ‘(
1s /su 𝑛)) ↔ ∃𝑛 ∈ ℕs 𝑧 = ( -us ‘(
1s /su 𝑛)))) | 
| 48 | 45, 47 | elab 3679 | . . . . . . . . . . 11
⊢ (𝑧 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( -us ‘(
1s /su 𝑛))} ↔ ∃𝑛 ∈ ℕs 𝑧 = ( -us ‘(
1s /su 𝑛))) | 
| 49 |  | velsn 4642 | . . . . . . . . . . 11
⊢ (𝑦 ∈ { 0s } ↔
𝑦 = 0s
) | 
| 50 | 48, 49 | anbi12i 628 | . . . . . . . . . 10
⊢ ((𝑧 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( -us ‘(
1s /su 𝑛))} ∧ 𝑦 ∈ { 0s }) ↔
(∃𝑛 ∈
ℕs 𝑧 = (
-us ‘( 1s /su 𝑛)) ∧ 𝑦 = 0s )) | 
| 51 |  | r19.41v 3189 | . . . . . . . . . 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 28167 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ 
No  → ( 0s ·s 𝑛) = 0s ) | 
| 54 | 18, 53 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕs
→ ( 0s ·s 𝑛) = 0s ) | 
| 55 | 54, 3 | eqbrtrdi 5182 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕs
→ ( 0s ·s 𝑛) <s 1s ) | 
| 56 | 1 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕs
→ 0s ∈  No ) | 
| 57 |  | nnsgt0 28342 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕs
→ 0s <s 𝑛) | 
| 58 | 56, 17, 18, 57 | sltmuldivd 28253 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕs
→ (( 0s ·s 𝑛) <s 1s ↔ 0s
<s ( 1s /su 𝑛))) | 
| 59 | 55, 58 | mpbid 232 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕs
→ 0s <s ( 1s /su 𝑛)) | 
| 60 | 20 | slt0neg2d 28083 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕs
→ ( 0s <s ( 1s /su 𝑛) ↔ ( -us
‘( 1s /su 𝑛)) <s 0s )) | 
| 61 | 59, 60 | mpbid 232 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕs
→ ( -us ‘( 1s /su 𝑛)) <s 0s
) | 
| 62 |  | breq12 5148 | . . . . . . . . . . 11
⊢ ((𝑧 = ( -us ‘(
1s /su 𝑛)) ∧ 𝑦 = 0s ) → (𝑧 <s 𝑦 ↔ ( -us ‘(
1s /su 𝑛)) <s 0s )) | 
| 63 | 61, 62 | syl5ibrcom 247 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕs
→ ((𝑧 = (
-us ‘( 1s /su 𝑛)) ∧ 𝑦 = 0s ) → 𝑧 <s 𝑦)) | 
| 64 | 63 | rexlimiv 3148 | . . . . . . . . 9
⊢
(∃𝑛 ∈
ℕs (𝑧 = (
-us ‘( 1s /su 𝑛)) ∧ 𝑦 = 0s ) → 𝑧 <s 𝑦) | 
| 65 | 52, 64 | sylbi 217 | . . . . . . . 8
⊢ ((𝑧 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( -us ‘(
1s /su 𝑛))} ∧ 𝑦 ∈ { 0s }) → 𝑧 <s 𝑦) | 
| 66 | 65 | 3adant1 1131 | . . . . . . 7
⊢
((⊤ ∧ 𝑧
∈ {𝑥 ∣
∃𝑛 ∈
ℕs 𝑥 = (
-us ‘( 1s /su 𝑛))} ∧ 𝑦 ∈ { 0s }) → 𝑧 <s 𝑦) | 
| 67 | 34, 36, 42, 44, 66 | ssltd 27836 | . . . . . 6
⊢ (⊤
→ {𝑥 ∣
∃𝑛 ∈
ℕs 𝑥 = (
-us ‘( 1s /su 𝑛))} <<s { 0s
}) | 
| 68 | 32 | abrexex 7987 | . . . . . . . 8
⊢ {𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = ( 1s
/su 𝑛)}
∈ V | 
| 69 | 68 | a1i 11 | . . . . . . 7
⊢ (⊤
→ {𝑥 ∣
∃𝑛 ∈
ℕs 𝑥 = (
1s /su 𝑛)} ∈ V) | 
| 70 |  | eleq1 2829 | . . . . . . . . . . 11
⊢ (𝑥 = ( 1s
/su 𝑛)
→ (𝑥 ∈  No  ↔ ( 1s /su 𝑛) ∈ 
No )) | 
| 71 | 20, 70 | syl5ibrcom 247 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕs
→ (𝑥 = ( 1s
/su 𝑛)
→ 𝑥 ∈  No )) | 
| 72 | 71 | rexlimiv 3148 | . . . . . . . . 9
⊢
(∃𝑛 ∈
ℕs 𝑥 = (
1s /su 𝑛) → 𝑥 ∈  No
) | 
| 73 | 72 | a1i 11 | . . . . . . . 8
⊢ (⊤
→ (∃𝑛 ∈
ℕs 𝑥 = (
1s /su 𝑛) → 𝑥 ∈  No
)) | 
| 74 | 73 | abssdv 4068 | . . . . . . 7
⊢ (⊤
→ {𝑥 ∣
∃𝑛 ∈
ℕs 𝑥 = (
1s /su 𝑛)} ⊆  No
) | 
| 75 |  | eqeq1 2741 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → (𝑥 = ( 1s /su 𝑛) ↔ 𝑧 = ( 1s /su 𝑛))) | 
| 76 | 75 | rexbidv 3179 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (∃𝑛 ∈ ℕs 𝑥 = ( 1s
/su 𝑛)
↔ ∃𝑛 ∈
ℕs 𝑧 = (
1s /su 𝑛))) | 
| 77 | 45, 76 | elab 3679 | . . . . . . . . . . 11
⊢ (𝑧 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( 1s
/su 𝑛)}
↔ ∃𝑛 ∈
ℕs 𝑧 = (
1s /su 𝑛)) | 
| 78 | 49, 77 | anbi12i 628 | . . . . . . . . . 10
⊢ ((𝑦 ∈ { 0s } ∧
𝑧 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = ( 1s
/su 𝑛)})
↔ (𝑦 = 0s
∧ ∃𝑛 ∈
ℕs 𝑧 = (
1s /su 𝑛))) | 
| 79 |  | r19.42v 3191 | . . . . . . . . . 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 5148 | . . . . . . . . . . . 12
⊢ ((𝑦 = 0s ∧ 𝑧 = ( 1s
/su 𝑛))
→ (𝑦 <s 𝑧 ↔ 0s <s (
1s /su 𝑛))) | 
| 82 | 59, 81 | syl5ibrcom 247 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕs
→ ((𝑦 = 0s
∧ 𝑧 = ( 1s
/su 𝑛))
→ 𝑦 <s 𝑧)) | 
| 83 | 82 | rexlimiv 3148 | . . . . . . . . . 10
⊢
(∃𝑛 ∈
ℕs (𝑦 =
0s ∧ 𝑧 = (
1s /su 𝑛)) → 𝑦 <s 𝑧) | 
| 84 | 83 | a1i 11 | . . . . . . . . 9
⊢ (⊤
→ (∃𝑛 ∈
ℕs (𝑦 =
0s ∧ 𝑧 = (
1s /su 𝑛)) → 𝑦 <s 𝑧)) | 
| 85 | 80, 84 | biimtrid 242 | . . . . . . . 8
⊢ (⊤
→ ((𝑦 ∈ {
0s } ∧ 𝑧
∈ {𝑥 ∣
∃𝑛 ∈
ℕs 𝑥 = (
1s /su 𝑛)}) → 𝑦 <s 𝑧)) | 
| 86 | 85 | 3impib 1117 | . . . . . . 7
⊢
((⊤ ∧ 𝑦
∈ { 0s } ∧ 𝑧 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( 1s
/su 𝑛)})
→ 𝑦 <s 𝑧) | 
| 87 | 36, 69, 44, 74, 86 | ssltd 27836 | . . . . . 6
⊢ (⊤
→ { 0s } <<s {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( 1s
/su 𝑛)}) | 
| 88 | 67, 87 | cuteq0 27877 | . . . . 5
⊢ (⊤
→ ({𝑥 ∣
∃𝑛 ∈
ℕs 𝑥 = (
-us ‘( 1s /su 𝑛))} |s {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( 1s
/su 𝑛)}) =
0s ) | 
| 89 | 88 | mptru 1547 | . . . 4
⊢ ({𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = ( -us
‘( 1s /su 𝑛))} |s {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = ( 1s
/su 𝑛)}) =
0s | 
| 90 | 31, 89 | eqtr2i 2766 | . . 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 28427 | . 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 711 | 1
⊢ 
0s ∈ ℝs |