| Step | Hyp | Ref
| Expression |
| 1 | | negscl 28068 |
. . . 4
⊢ (𝐴 ∈
No → ( -us ‘𝐴) ∈ No
) |
| 2 | 1 | adantr 480 |
. . 3
⊢ ((𝐴 ∈
No ∧ (∃𝑛
∈ ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})))
→ ( -us ‘𝐴) ∈ No
) |
| 3 | | nnsno 28329 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕs
→ 𝑛 ∈ No ) |
| 4 | 3 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → 𝑛 ∈ No
) |
| 5 | 4 | negscld 28069 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → ( -us ‘𝑛) ∈ No
) |
| 6 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → 𝐴 ∈ No
) |
| 7 | 5, 6 | sltnegd 28079 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → (( -us ‘𝑛) <s 𝐴 ↔ ( -us ‘𝐴) <s ( -us
‘( -us ‘𝑛)))) |
| 8 | | negnegs 28076 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
No → ( -us ‘( -us ‘𝑛)) = 𝑛) |
| 9 | 4, 8 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → ( -us ‘( -us
‘𝑛)) = 𝑛) |
| 10 | 9 | breq2d 5155 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → (( -us ‘𝐴) <s ( -us ‘(
-us ‘𝑛))
↔ ( -us ‘𝐴) <s 𝑛)) |
| 11 | 7, 10 | bitrd 279 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → (( -us ‘𝑛) <s 𝐴 ↔ ( -us ‘𝐴) <s 𝑛)) |
| 12 | 6, 4 | sltnegd 28079 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → (𝐴 <s 𝑛 ↔ ( -us ‘𝑛) <s ( -us
‘𝐴))) |
| 13 | 11, 12 | anbi12d 632 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → ((( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ↔ (( -us ‘𝐴) <s 𝑛 ∧ ( -us ‘𝑛) <s ( -us
‘𝐴)))) |
| 14 | 13 | biancomd 463 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → ((( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ↔ (( -us ‘𝑛) <s ( -us
‘𝐴) ∧ (
-us ‘𝐴)
<s 𝑛))) |
| 15 | 14 | rexbidva 3177 |
. . . . 5
⊢ (𝐴 ∈
No → (∃𝑛
∈ ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ↔ ∃𝑛 ∈ ℕs (( -us
‘𝑛) <s (
-us ‘𝐴)
∧ ( -us ‘𝐴) <s 𝑛))) |
| 16 | 15 | biimpa 476 |
. . . 4
⊢ ((𝐴 ∈
No ∧ ∃𝑛
∈ ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛)) → ∃𝑛 ∈ ℕs (( -us
‘𝑛) <s (
-us ‘𝐴)
∧ ( -us ‘𝐴) <s 𝑛)) |
| 17 | 16 | adantrr 717 |
. . 3
⊢ ((𝐴 ∈
No ∧ (∃𝑛
∈ ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})))
→ ∃𝑛 ∈
ℕs (( -us ‘𝑛) <s ( -us ‘𝐴) ∧ ( -us
‘𝐴) <s 𝑛)) |
| 18 | | recut 28428 |
. . . . . 6
⊢ (𝐴 ∈
No → {𝑥
∣ ∃𝑛 ∈
ℕs 𝑥 =
(𝐴 -s (
1s /su 𝑛))} <<s {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}) |
| 19 | 18 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ (∃𝑛
∈ ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})))
→ {𝑥 ∣
∃𝑛 ∈
ℕs 𝑥 =
(𝐴 -s (
1s /su 𝑛))} <<s {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}) |
| 20 | | simprr 773 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ (∃𝑛
∈ ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})))
→ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})) |
| 21 | 19, 20 | negsunif 28087 |
. . . 4
⊢ ((𝐴 ∈
No ∧ (∃𝑛
∈ ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})))
→ ( -us ‘𝐴) = (( -us “ {𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))}) |s
( -us “ {𝑥
∣ ∃𝑛 ∈
ℕs 𝑥 =
(𝐴 -s (
1s /su 𝑛))}))) |
| 22 | | negsfn 28055 |
. . . . . . . . 9
⊢
-us Fn No |
| 23 | | ssltss2 27834 |
. . . . . . . . . 10
⊢ ({𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 -s ( 1s
/su 𝑛))}
<<s {𝑥 ∣
∃𝑛 ∈
ℕs 𝑥 =
(𝐴 +s (
1s /su 𝑛))} → {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}
⊆ No ) |
| 24 | 18, 23 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈
No → {𝑥
∣ ∃𝑛 ∈
ℕs 𝑥 =
(𝐴 +s (
1s /su 𝑛))} ⊆ No
) |
| 25 | | fvelimab 6981 |
. . . . . . . . 9
⊢ ((
-us Fn No ∧ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}
⊆ No ) → (𝑦 ∈ ( -us “ {𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})
↔ ∃𝑧 ∈
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))} (
-us ‘𝑧) =
𝑦)) |
| 26 | 22, 24, 25 | sylancr 587 |
. . . . . . . 8
⊢ (𝐴 ∈
No → (𝑦 ∈
( -us “ {𝑥
∣ ∃𝑛 ∈
ℕs 𝑥 =
(𝐴 +s (
1s /su 𝑛))}) ↔ ∃𝑧 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))} (
-us ‘𝑧) =
𝑦)) |
| 27 | | eqeq1 2741 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝑥 = (𝐴 +s ( 1s
/su 𝑛))
↔ 𝑧 = (𝐴 +s ( 1s
/su 𝑛)))) |
| 28 | 27 | rexbidv 3179 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))
↔ ∃𝑛 ∈
ℕs 𝑧 =
(𝐴 +s (
1s /su 𝑛)))) |
| 29 | 28 | rexab 3700 |
. . . . . . . . . 10
⊢
(∃𝑧 ∈
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))} (
-us ‘𝑧) =
𝑦 ↔ ∃𝑧(∃𝑛 ∈ ℕs 𝑧 = (𝐴 +s ( 1s
/su 𝑛))
∧ ( -us ‘𝑧) = 𝑦)) |
| 30 | | rexcom4 3288 |
. . . . . . . . . . 11
⊢
(∃𝑛 ∈
ℕs ∃𝑧(𝑧 = (𝐴 +s ( 1s
/su 𝑛))
∧ ( -us ‘𝑧) = 𝑦) ↔ ∃𝑧∃𝑛 ∈ ℕs (𝑧 = (𝐴 +s ( 1s
/su 𝑛))
∧ ( -us ‘𝑧) = 𝑦)) |
| 31 | | ovex 7464 |
. . . . . . . . . . . . 13
⊢ (𝐴 +s ( 1s
/su 𝑛))
∈ V |
| 32 | | fveqeq2 6915 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝐴 +s ( 1s
/su 𝑛))
→ (( -us ‘𝑧) = 𝑦 ↔ ( -us ‘(𝐴 +s ( 1s
/su 𝑛))) =
𝑦)) |
| 33 | 31, 32 | ceqsexv 3532 |
. . . . . . . . . . . 12
⊢
(∃𝑧(𝑧 = (𝐴 +s ( 1s
/su 𝑛))
∧ ( -us ‘𝑧) = 𝑦) ↔ ( -us ‘(𝐴 +s ( 1s
/su 𝑛))) =
𝑦) |
| 34 | 33 | rexbii 3094 |
. . . . . . . . . . 11
⊢
(∃𝑛 ∈
ℕs ∃𝑧(𝑧 = (𝐴 +s ( 1s
/su 𝑛))
∧ ( -us ‘𝑧) = 𝑦) ↔ ∃𝑛 ∈ ℕs ( -us
‘(𝐴 +s (
1s /su 𝑛))) = 𝑦) |
| 35 | | r19.41v 3189 |
. . . . . . . . . . . 12
⊢
(∃𝑛 ∈
ℕs (𝑧 =
(𝐴 +s (
1s /su 𝑛)) ∧ ( -us ‘𝑧) = 𝑦) ↔ (∃𝑛 ∈ ℕs 𝑧 = (𝐴 +s ( 1s
/su 𝑛))
∧ ( -us ‘𝑧) = 𝑦)) |
| 36 | 35 | exbii 1848 |
. . . . . . . . . . 11
⊢
(∃𝑧∃𝑛 ∈ ℕs (𝑧 = (𝐴 +s ( 1s
/su 𝑛))
∧ ( -us ‘𝑧) = 𝑦) ↔ ∃𝑧(∃𝑛 ∈ ℕs 𝑧 = (𝐴 +s ( 1s
/su 𝑛))
∧ ( -us ‘𝑧) = 𝑦)) |
| 37 | 30, 34, 36 | 3bitr3ri 302 |
. . . . . . . . . 10
⊢
(∃𝑧(∃𝑛 ∈ ℕs 𝑧 = (𝐴 +s ( 1s
/su 𝑛))
∧ ( -us ‘𝑧) = 𝑦) ↔ ∃𝑛 ∈ ℕs ( -us
‘(𝐴 +s (
1s /su 𝑛))) = 𝑦) |
| 38 | 29, 37 | bitri 275 |
. . . . . . . . 9
⊢
(∃𝑧 ∈
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))} (
-us ‘𝑧) =
𝑦 ↔ ∃𝑛 ∈ ℕs (
-us ‘(𝐴
+s ( 1s /su 𝑛))) = 𝑦) |
| 39 | | 1sno 27872 |
. . . . . . . . . . . . . . . . 17
⊢
1s ∈ No |
| 40 | 39 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕs
→ 1s ∈ No ) |
| 41 | | nnne0s 28340 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕs
→ 𝑛 ≠ 0s
) |
| 42 | 40, 3, 41 | divscld 28248 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕs
→ ( 1s /su 𝑛) ∈ No
) |
| 43 | 42 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → ( 1s /su 𝑛) ∈
No ) |
| 44 | | negsdi 28082 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
No ∧ ( 1s /su 𝑛) ∈ No )
→ ( -us ‘(𝐴 +s ( 1s
/su 𝑛))) =
(( -us ‘𝐴)
+s ( -us ‘( 1s /su 𝑛)))) |
| 45 | 43, 44 | syldan 591 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → ( -us ‘(𝐴 +s ( 1s
/su 𝑛))) =
(( -us ‘𝐴)
+s ( -us ‘( 1s /su 𝑛)))) |
| 46 | 1 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → ( -us ‘𝐴) ∈ No
) |
| 47 | 46, 43 | subsvald 28091 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → (( -us ‘𝐴) -s ( 1s
/su 𝑛)) = ((
-us ‘𝐴)
+s ( -us ‘( 1s /su 𝑛)))) |
| 48 | 45, 47 | eqtr4d 2780 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → ( -us ‘(𝐴 +s ( 1s
/su 𝑛))) =
(( -us ‘𝐴)
-s ( 1s /su 𝑛))) |
| 49 | 48 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → (( -us ‘(𝐴 +s ( 1s
/su 𝑛))) =
𝑦 ↔ (( -us
‘𝐴) -s (
1s /su 𝑛)) = 𝑦)) |
| 50 | | eqcom 2744 |
. . . . . . . . . . 11
⊢ (((
-us ‘𝐴)
-s ( 1s /su 𝑛)) = 𝑦 ↔ 𝑦 = (( -us ‘𝐴) -s ( 1s
/su 𝑛))) |
| 51 | 49, 50 | bitrdi 287 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → (( -us ‘(𝐴 +s ( 1s
/su 𝑛))) =
𝑦 ↔ 𝑦 = (( -us ‘𝐴) -s ( 1s
/su 𝑛)))) |
| 52 | 51 | rexbidva 3177 |
. . . . . . . . 9
⊢ (𝐴 ∈
No → (∃𝑛
∈ ℕs ( -us ‘(𝐴 +s ( 1s
/su 𝑛))) =
𝑦 ↔ ∃𝑛 ∈ ℕs
𝑦 = (( -us
‘𝐴) -s (
1s /su 𝑛)))) |
| 53 | 38, 52 | bitrid 283 |
. . . . . . . 8
⊢ (𝐴 ∈
No → (∃𝑧
∈ {𝑥 ∣
∃𝑛 ∈
ℕs 𝑥 =
(𝐴 +s (
1s /su 𝑛))} ( -us ‘𝑧) = 𝑦 ↔ ∃𝑛 ∈ ℕs 𝑦 = (( -us
‘𝐴) -s (
1s /su 𝑛)))) |
| 54 | 26, 53 | bitrd 279 |
. . . . . . 7
⊢ (𝐴 ∈
No → (𝑦 ∈
( -us “ {𝑥
∣ ∃𝑛 ∈
ℕs 𝑥 =
(𝐴 +s (
1s /su 𝑛))}) ↔ ∃𝑛 ∈ ℕs 𝑦 = (( -us
‘𝐴) -s (
1s /su 𝑛)))) |
| 55 | 54 | eqabdv 2875 |
. . . . . 6
⊢ (𝐴 ∈
No → ( -us “ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}) =
{𝑦 ∣ ∃𝑛 ∈ ℕs
𝑦 = (( -us
‘𝐴) -s (
1s /su 𝑛))}) |
| 56 | | ssltss1 27833 |
. . . . . . . . . 10
⊢ ({𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 -s ( 1s
/su 𝑛))}
<<s {𝑥 ∣
∃𝑛 ∈
ℕs 𝑥 =
(𝐴 +s (
1s /su 𝑛))} → {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))}
⊆ No ) |
| 57 | 18, 56 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈
No → {𝑥
∣ ∃𝑛 ∈
ℕs 𝑥 =
(𝐴 -s (
1s /su 𝑛))} ⊆ No
) |
| 58 | | fvelimab 6981 |
. . . . . . . . 9
⊢ ((
-us Fn No ∧ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))}
⊆ No ) → (𝑦 ∈ ( -us “ {𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 -s ( 1s
/su 𝑛))})
↔ ∃𝑧 ∈
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 -s ( 1s
/su 𝑛))} (
-us ‘𝑧) =
𝑦)) |
| 59 | 22, 57, 58 | sylancr 587 |
. . . . . . . 8
⊢ (𝐴 ∈
No → (𝑦 ∈
( -us “ {𝑥
∣ ∃𝑛 ∈
ℕs 𝑥 =
(𝐴 -s (
1s /su 𝑛))}) ↔ ∃𝑧 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} (
-us ‘𝑧) =
𝑦)) |
| 60 | | eqeq1 2741 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝑥 = (𝐴 -s ( 1s
/su 𝑛))
↔ 𝑧 = (𝐴 -s ( 1s
/su 𝑛)))) |
| 61 | 60 | rexbidv 3179 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))
↔ ∃𝑛 ∈
ℕs 𝑧 =
(𝐴 -s (
1s /su 𝑛)))) |
| 62 | 61 | rexab 3700 |
. . . . . . . . . 10
⊢
(∃𝑧 ∈
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 -s ( 1s
/su 𝑛))} (
-us ‘𝑧) =
𝑦 ↔ ∃𝑧(∃𝑛 ∈ ℕs 𝑧 = (𝐴 -s ( 1s
/su 𝑛))
∧ ( -us ‘𝑧) = 𝑦)) |
| 63 | | rexcom4 3288 |
. . . . . . . . . . 11
⊢
(∃𝑛 ∈
ℕs ∃𝑧(𝑧 = (𝐴 -s ( 1s
/su 𝑛))
∧ ( -us ‘𝑧) = 𝑦) ↔ ∃𝑧∃𝑛 ∈ ℕs (𝑧 = (𝐴 -s ( 1s
/su 𝑛))
∧ ( -us ‘𝑧) = 𝑦)) |
| 64 | | ovex 7464 |
. . . . . . . . . . . . 13
⊢ (𝐴 -s ( 1s
/su 𝑛))
∈ V |
| 65 | | fveqeq2 6915 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝐴 -s ( 1s
/su 𝑛))
→ (( -us ‘𝑧) = 𝑦 ↔ ( -us ‘(𝐴 -s ( 1s
/su 𝑛))) =
𝑦)) |
| 66 | 64, 65 | ceqsexv 3532 |
. . . . . . . . . . . 12
⊢
(∃𝑧(𝑧 = (𝐴 -s ( 1s
/su 𝑛))
∧ ( -us ‘𝑧) = 𝑦) ↔ ( -us ‘(𝐴 -s ( 1s
/su 𝑛))) =
𝑦) |
| 67 | 66 | rexbii 3094 |
. . . . . . . . . . 11
⊢
(∃𝑛 ∈
ℕs ∃𝑧(𝑧 = (𝐴 -s ( 1s
/su 𝑛))
∧ ( -us ‘𝑧) = 𝑦) ↔ ∃𝑛 ∈ ℕs ( -us
‘(𝐴 -s (
1s /su 𝑛))) = 𝑦) |
| 68 | | r19.41v 3189 |
. . . . . . . . . . . 12
⊢
(∃𝑛 ∈
ℕs (𝑧 =
(𝐴 -s (
1s /su 𝑛)) ∧ ( -us ‘𝑧) = 𝑦) ↔ (∃𝑛 ∈ ℕs 𝑧 = (𝐴 -s ( 1s
/su 𝑛))
∧ ( -us ‘𝑧) = 𝑦)) |
| 69 | 68 | exbii 1848 |
. . . . . . . . . . 11
⊢
(∃𝑧∃𝑛 ∈ ℕs (𝑧 = (𝐴 -s ( 1s
/su 𝑛))
∧ ( -us ‘𝑧) = 𝑦) ↔ ∃𝑧(∃𝑛 ∈ ℕs 𝑧 = (𝐴 -s ( 1s
/su 𝑛))
∧ ( -us ‘𝑧) = 𝑦)) |
| 70 | 63, 67, 69 | 3bitr3ri 302 |
. . . . . . . . . 10
⊢
(∃𝑧(∃𝑛 ∈ ℕs 𝑧 = (𝐴 -s ( 1s
/su 𝑛))
∧ ( -us ‘𝑧) = 𝑦) ↔ ∃𝑛 ∈ ℕs ( -us
‘(𝐴 -s (
1s /su 𝑛))) = 𝑦) |
| 71 | 62, 70 | bitri 275 |
. . . . . . . . 9
⊢
(∃𝑧 ∈
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 -s ( 1s
/su 𝑛))} (
-us ‘𝑧) =
𝑦 ↔ ∃𝑛 ∈ ℕs (
-us ‘(𝐴
-s ( 1s /su 𝑛))) = 𝑦) |
| 72 | 6, 43 | subsvald 28091 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → (𝐴 -s ( 1s
/su 𝑛)) =
(𝐴 +s (
-us ‘( 1s /su 𝑛)))) |
| 73 | 72 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → ( -us ‘(𝐴 -s ( 1s
/su 𝑛))) = (
-us ‘(𝐴
+s ( -us ‘( 1s /su 𝑛))))) |
| 74 | 43 | negscld 28069 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → ( -us ‘( 1s
/su 𝑛))
∈ No ) |
| 75 | | negsdi 28082 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
No ∧ ( -us ‘( 1s /su
𝑛)) ∈ No ) → ( -us ‘(𝐴 +s ( -us ‘(
1s /su 𝑛)))) = (( -us ‘𝐴) +s ( -us
‘( -us ‘( 1s /su 𝑛))))) |
| 76 | 74, 75 | syldan 591 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → ( -us ‘(𝐴 +s ( -us ‘(
1s /su 𝑛)))) = (( -us ‘𝐴) +s ( -us
‘( -us ‘( 1s /su 𝑛))))) |
| 77 | | negnegs 28076 |
. . . . . . . . . . . . . . 15
⊢ ((
1s /su 𝑛) ∈ No
→ ( -us ‘( -us ‘( 1s
/su 𝑛))) = (
1s /su 𝑛)) |
| 78 | 43, 77 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → ( -us ‘( -us ‘(
1s /su 𝑛))) = ( 1s /su
𝑛)) |
| 79 | 78 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → (( -us ‘𝐴) +s ( -us ‘(
-us ‘( 1s /su 𝑛)))) = (( -us ‘𝐴) +s ( 1s
/su 𝑛))) |
| 80 | 73, 76, 79 | 3eqtrd 2781 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → ( -us ‘(𝐴 -s ( 1s
/su 𝑛))) =
(( -us ‘𝐴)
+s ( 1s /su 𝑛))) |
| 81 | 80 | eqeq1d 2739 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → (( -us ‘(𝐴 -s ( 1s
/su 𝑛))) =
𝑦 ↔ (( -us
‘𝐴) +s (
1s /su 𝑛)) = 𝑦)) |
| 82 | | eqcom 2744 |
. . . . . . . . . . 11
⊢ (((
-us ‘𝐴)
+s ( 1s /su 𝑛)) = 𝑦 ↔ 𝑦 = (( -us ‘𝐴) +s ( 1s
/su 𝑛))) |
| 83 | 81, 82 | bitrdi 287 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → (( -us ‘(𝐴 -s ( 1s
/su 𝑛))) =
𝑦 ↔ 𝑦 = (( -us ‘𝐴) +s ( 1s
/su 𝑛)))) |
| 84 | 83 | rexbidva 3177 |
. . . . . . . . 9
⊢ (𝐴 ∈
No → (∃𝑛
∈ ℕs ( -us ‘(𝐴 -s ( 1s
/su 𝑛))) =
𝑦 ↔ ∃𝑛 ∈ ℕs
𝑦 = (( -us
‘𝐴) +s (
1s /su 𝑛)))) |
| 85 | 71, 84 | bitrid 283 |
. . . . . . . 8
⊢ (𝐴 ∈
No → (∃𝑧
∈ {𝑥 ∣
∃𝑛 ∈
ℕs 𝑥 =
(𝐴 -s (
1s /su 𝑛))} ( -us ‘𝑧) = 𝑦 ↔ ∃𝑛 ∈ ℕs 𝑦 = (( -us
‘𝐴) +s (
1s /su 𝑛)))) |
| 86 | 59, 85 | bitrd 279 |
. . . . . . 7
⊢ (𝐴 ∈
No → (𝑦 ∈
( -us “ {𝑥
∣ ∃𝑛 ∈
ℕs 𝑥 =
(𝐴 -s (
1s /su 𝑛))}) ↔ ∃𝑛 ∈ ℕs 𝑦 = (( -us
‘𝐴) +s (
1s /su 𝑛)))) |
| 87 | 86 | eqabdv 2875 |
. . . . . 6
⊢ (𝐴 ∈
No → ( -us “ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))}) =
{𝑦 ∣ ∃𝑛 ∈ ℕs
𝑦 = (( -us
‘𝐴) +s (
1s /su 𝑛))}) |
| 88 | 55, 87 | oveq12d 7449 |
. . . . 5
⊢ (𝐴 ∈
No → (( -us “ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}) |s
( -us “ {𝑥
∣ ∃𝑛 ∈
ℕs 𝑥 =
(𝐴 -s (
1s /su 𝑛))})) = ({𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (( -us
‘𝐴) -s (
1s /su 𝑛))} |s {𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (( -us
‘𝐴) +s (
1s /su 𝑛))})) |
| 89 | 88 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈
No ∧ (∃𝑛
∈ ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})))
→ (( -us “ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}) |s
( -us “ {𝑥
∣ ∃𝑛 ∈
ℕs 𝑥 =
(𝐴 -s (
1s /su 𝑛))})) = ({𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (( -us
‘𝐴) -s (
1s /su 𝑛))} |s {𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (( -us
‘𝐴) +s (
1s /su 𝑛))})) |
| 90 | 21, 89 | eqtrd 2777 |
. . 3
⊢ ((𝐴 ∈
No ∧ (∃𝑛
∈ ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})))
→ ( -us ‘𝐴) = ({𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (( -us
‘𝐴) -s (
1s /su 𝑛))} |s {𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (( -us
‘𝐴) +s (
1s /su 𝑛))})) |
| 91 | 2, 17, 90 | jca32 515 |
. 2
⊢ ((𝐴 ∈
No ∧ (∃𝑛
∈ ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})))
→ (( -us ‘𝐴) ∈ No
∧ (∃𝑛 ∈
ℕs (( -us ‘𝑛) <s ( -us ‘𝐴) ∧ ( -us
‘𝐴) <s 𝑛) ∧ ( -us
‘𝐴) = ({𝑦 ∣ ∃𝑛 ∈ ℕs
𝑦 = (( -us
‘𝐴) -s (
1s /su 𝑛))} |s {𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (( -us
‘𝐴) +s (
1s /su 𝑛))})))) |
| 92 | | elreno 28427 |
. 2
⊢ (𝐴 ∈ ℝs
↔ (𝐴 ∈ No ∧ (∃𝑛 ∈ ℕs (( -us
‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})))) |
| 93 | | elreno 28427 |
. 2
⊢ ((
-us ‘𝐴)
∈ ℝs ↔ (( -us ‘𝐴) ∈ No
∧ (∃𝑛 ∈
ℕs (( -us ‘𝑛) <s ( -us ‘𝐴) ∧ ( -us
‘𝐴) <s 𝑛) ∧ ( -us
‘𝐴) = ({𝑦 ∣ ∃𝑛 ∈ ℕs
𝑦 = (( -us
‘𝐴) -s (
1s /su 𝑛))} |s {𝑦 ∣ ∃𝑛 ∈ ℕs 𝑦 = (( -us
‘𝐴) +s (
1s /su 𝑛))})))) |
| 94 | 91, 92, 93 | 3imtr4i 292 |
1
⊢ (𝐴 ∈ ℝs
→ ( -us ‘𝐴) ∈
ℝs) |