Step | Hyp | Ref
| Expression |
1 | | negscl 27889 |
. . . 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 28137 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕs
→ 𝑛 ∈ No ) |
4 | 3 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → 𝑛 ∈ No
) |
5 | 4 | negscld 27890 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → ( -us ‘𝑛) ∈ No
) |
6 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → 𝐴 ∈ No
) |
7 | 5, 6 | sltnegd 27900 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → (( -us ‘𝑛) <s 𝐴 ↔ ( -us ‘𝐴) <s ( -us
‘( -us ‘𝑛)))) |
8 | | negnegs 27897 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
No → ( -us ‘( -us ‘𝑛)) = 𝑛) |
9 | 4, 8 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → ( -us ‘( -us
‘𝑛)) = 𝑛) |
10 | 9 | breq2d 5151 |
. . . . . . . . 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 27900 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → (𝐴 <s 𝑛 ↔ ( -us ‘𝑛) <s ( -us
‘𝐴))) |
13 | 11, 12 | anbi12d 630 |
. . . . . . 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 3168 |
. . . . 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 714 |
. . 3
⊢ ((𝐴 ∈
No ∧ (∃𝑛
∈ ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})))
→ ∃𝑛 ∈
ℕs (( -us ‘𝑛) <s ( -us ‘𝐴) ∧ ( -us
‘𝐴) <s 𝑛)) |
18 | | recut 28165 |
. . . . . 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 770 |
. . . . 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 27908 |
. . . 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 27877 |
. . . . . . . . 9
⊢
-us Fn No |
23 | | ssltss2 27663 |
. . . . . . . . . 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 6955 |
. . . . . . . . 9
⊢ ((
-us Fn No ∧ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}
⊆ No ) → (𝑦 ∈ ( -us “ {𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})
↔ ∃𝑧 ∈
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))} (
-us ‘𝑧) =
𝑦)) |
26 | 22, 24, 25 | sylancr 586 |
. . . . . . . 8
⊢ (𝐴 ∈
No → (𝑦 ∈
( -us “ {𝑥
∣ ∃𝑛 ∈
ℕs 𝑥 =
(𝐴 +s (
1s /su 𝑛))}) ↔ ∃𝑧 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))} (
-us ‘𝑧) =
𝑦)) |
27 | | eqeq1 2728 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝑥 = (𝐴 +s ( 1s
/su 𝑛))
↔ 𝑧 = (𝐴 +s ( 1s
/su 𝑛)))) |
28 | 27 | rexbidv 3170 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))
↔ ∃𝑛 ∈
ℕs 𝑧 =
(𝐴 +s (
1s /su 𝑛)))) |
29 | 28 | rexab 3683 |
. . . . . . . . . 10
⊢
(∃𝑧 ∈
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))} (
-us ‘𝑧) =
𝑦 ↔ ∃𝑧(∃𝑛 ∈ ℕs 𝑧 = (𝐴 +s ( 1s
/su 𝑛))
∧ ( -us ‘𝑧) = 𝑦)) |
30 | | rexcom4 3277 |
. . . . . . . . . . 11
⊢
(∃𝑛 ∈
ℕs ∃𝑧(𝑧 = (𝐴 +s ( 1s
/su 𝑛))
∧ ( -us ‘𝑧) = 𝑦) ↔ ∃𝑧∃𝑛 ∈ ℕs (𝑧 = (𝐴 +s ( 1s
/su 𝑛))
∧ ( -us ‘𝑧) = 𝑦)) |
31 | | ovex 7435 |
. . . . . . . . . . . . 13
⊢ (𝐴 +s ( 1s
/su 𝑛))
∈ V |
32 | | fveqeq2 6891 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝐴 +s ( 1s
/su 𝑛))
→ (( -us ‘𝑧) = 𝑦 ↔ ( -us ‘(𝐴 +s ( 1s
/su 𝑛))) =
𝑦)) |
33 | 31, 32 | ceqsexv 3518 |
. . . . . . . . . . . 12
⊢
(∃𝑧(𝑧 = (𝐴 +s ( 1s
/su 𝑛))
∧ ( -us ‘𝑧) = 𝑦) ↔ ( -us ‘(𝐴 +s ( 1s
/su 𝑛))) =
𝑦) |
34 | 33 | rexbii 3086 |
. . . . . . . . . . 11
⊢
(∃𝑛 ∈
ℕs ∃𝑧(𝑧 = (𝐴 +s ( 1s
/su 𝑛))
∧ ( -us ‘𝑧) = 𝑦) ↔ ∃𝑛 ∈ ℕs ( -us
‘(𝐴 +s (
1s /su 𝑛))) = 𝑦) |
35 | | r19.41v 3180 |
. . . . . . . . . . . 12
⊢
(∃𝑛 ∈
ℕs (𝑧 =
(𝐴 +s (
1s /su 𝑛)) ∧ ( -us ‘𝑧) = 𝑦) ↔ (∃𝑛 ∈ ℕs 𝑧 = (𝐴 +s ( 1s
/su 𝑛))
∧ ( -us ‘𝑧) = 𝑦)) |
36 | 35 | exbii 1842 |
. . . . . . . . . . 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 27701 |
. . . . . . . . . . . . . . . . 17
⊢
1s ∈ No |
40 | 39 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕs
→ 1s ∈ No ) |
41 | | nnne0s 28146 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕs
→ 𝑛 ≠ 0s
) |
42 | 40, 3, 41 | divscld 28063 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕs
→ ( 1s /su 𝑛) ∈ No
) |
43 | 42 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → ( 1s /su 𝑛) ∈
No ) |
44 | | negsdi 27903 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
No ∧ ( 1s /su 𝑛) ∈ No )
→ ( -us ‘(𝐴 +s ( 1s
/su 𝑛))) =
(( -us ‘𝐴)
+s ( -us ‘( 1s /su 𝑛)))) |
45 | 43, 44 | syldan 590 |
. . . . . . . . . . . . 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 27912 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → (( -us ‘𝐴) -s ( 1s
/su 𝑛)) = ((
-us ‘𝐴)
+s ( -us ‘( 1s /su 𝑛)))) |
48 | 45, 47 | eqtr4d 2767 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → ( -us ‘(𝐴 +s ( 1s
/su 𝑛))) =
(( -us ‘𝐴)
-s ( 1s /su 𝑛))) |
49 | 48 | eqeq1d 2726 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → (( -us ‘(𝐴 +s ( 1s
/su 𝑛))) =
𝑦 ↔ (( -us
‘𝐴) -s (
1s /su 𝑛)) = 𝑦)) |
50 | | eqcom 2731 |
. . . . . . . . . . 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 3168 |
. . . . . . . . 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 2859 |
. . . . . 6
⊢ (𝐴 ∈
No → ( -us “ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}) =
{𝑦 ∣ ∃𝑛 ∈ ℕs
𝑦 = (( -us
‘𝐴) -s (
1s /su 𝑛))}) |
56 | | ssltss1 27662 |
. . . . . . . . . 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 6955 |
. . . . . . . . 9
⊢ ((
-us Fn No ∧ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))}
⊆ No ) → (𝑦 ∈ ( -us “ {𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 -s ( 1s
/su 𝑛))})
↔ ∃𝑧 ∈
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 -s ( 1s
/su 𝑛))} (
-us ‘𝑧) =
𝑦)) |
59 | 22, 57, 58 | sylancr 586 |
. . . . . . . 8
⊢ (𝐴 ∈
No → (𝑦 ∈
( -us “ {𝑥
∣ ∃𝑛 ∈
ℕs 𝑥 =
(𝐴 -s (
1s /su 𝑛))}) ↔ ∃𝑧 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} (
-us ‘𝑧) =
𝑦)) |
60 | | eqeq1 2728 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝑥 = (𝐴 -s ( 1s
/su 𝑛))
↔ 𝑧 = (𝐴 -s ( 1s
/su 𝑛)))) |
61 | 60 | rexbidv 3170 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))
↔ ∃𝑛 ∈
ℕs 𝑧 =
(𝐴 -s (
1s /su 𝑛)))) |
62 | 61 | rexab 3683 |
. . . . . . . . . 10
⊢
(∃𝑧 ∈
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 -s ( 1s
/su 𝑛))} (
-us ‘𝑧) =
𝑦 ↔ ∃𝑧(∃𝑛 ∈ ℕs 𝑧 = (𝐴 -s ( 1s
/su 𝑛))
∧ ( -us ‘𝑧) = 𝑦)) |
63 | | rexcom4 3277 |
. . . . . . . . . . 11
⊢
(∃𝑛 ∈
ℕs ∃𝑧(𝑧 = (𝐴 -s ( 1s
/su 𝑛))
∧ ( -us ‘𝑧) = 𝑦) ↔ ∃𝑧∃𝑛 ∈ ℕs (𝑧 = (𝐴 -s ( 1s
/su 𝑛))
∧ ( -us ‘𝑧) = 𝑦)) |
64 | | ovex 7435 |
. . . . . . . . . . . . 13
⊢ (𝐴 -s ( 1s
/su 𝑛))
∈ V |
65 | | fveqeq2 6891 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝐴 -s ( 1s
/su 𝑛))
→ (( -us ‘𝑧) = 𝑦 ↔ ( -us ‘(𝐴 -s ( 1s
/su 𝑛))) =
𝑦)) |
66 | 64, 65 | ceqsexv 3518 |
. . . . . . . . . . . 12
⊢
(∃𝑧(𝑧 = (𝐴 -s ( 1s
/su 𝑛))
∧ ( -us ‘𝑧) = 𝑦) ↔ ( -us ‘(𝐴 -s ( 1s
/su 𝑛))) =
𝑦) |
67 | 66 | rexbii 3086 |
. . . . . . . . . . 11
⊢
(∃𝑛 ∈
ℕs ∃𝑧(𝑧 = (𝐴 -s ( 1s
/su 𝑛))
∧ ( -us ‘𝑧) = 𝑦) ↔ ∃𝑛 ∈ ℕs ( -us
‘(𝐴 -s (
1s /su 𝑛))) = 𝑦) |
68 | | r19.41v 3180 |
. . . . . . . . . . . 12
⊢
(∃𝑛 ∈
ℕs (𝑧 =
(𝐴 -s (
1s /su 𝑛)) ∧ ( -us ‘𝑧) = 𝑦) ↔ (∃𝑛 ∈ ℕs 𝑧 = (𝐴 -s ( 1s
/su 𝑛))
∧ ( -us ‘𝑧) = 𝑦)) |
69 | 68 | exbii 1842 |
. . . . . . . . . . 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 27912 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → (𝐴 -s ( 1s
/su 𝑛)) =
(𝐴 +s (
-us ‘( 1s /su 𝑛)))) |
73 | 72 | fveq2d 6886 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → ( -us ‘(𝐴 -s ( 1s
/su 𝑛))) = (
-us ‘(𝐴
+s ( -us ‘( 1s /su 𝑛))))) |
74 | 43 | negscld 27890 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → ( -us ‘( 1s
/su 𝑛))
∈ No ) |
75 | | negsdi 27903 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
No ∧ ( -us ‘( 1s /su
𝑛)) ∈ No ) → ( -us ‘(𝐴 +s ( -us ‘(
1s /su 𝑛)))) = (( -us ‘𝐴) +s ( -us
‘( -us ‘( 1s /su 𝑛))))) |
76 | 74, 75 | syldan 590 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → ( -us ‘(𝐴 +s ( -us ‘(
1s /su 𝑛)))) = (( -us ‘𝐴) +s ( -us
‘( -us ‘( 1s /su 𝑛))))) |
77 | | negnegs 27897 |
. . . . . . . . . . . . . . 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 7418 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → (( -us ‘𝐴) +s ( -us ‘(
-us ‘( 1s /su 𝑛)))) = (( -us ‘𝐴) +s ( 1s
/su 𝑛))) |
80 | 73, 76, 79 | 3eqtrd 2768 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → ( -us ‘(𝐴 -s ( 1s
/su 𝑛))) =
(( -us ‘𝐴)
+s ( 1s /su 𝑛))) |
81 | 80 | eqeq1d 2726 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
No ∧ 𝑛 ∈
ℕs) → (( -us ‘(𝐴 -s ( 1s
/su 𝑛))) =
𝑦 ↔ (( -us
‘𝐴) +s (
1s /su 𝑛)) = 𝑦)) |
82 | | eqcom 2731 |
. . . . . . . . . . 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 3168 |
. . . . . . . . 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 2859 |
. . . . . 6
⊢ (𝐴 ∈
No → ( -us “ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))}) =
{𝑦 ∣ ∃𝑛 ∈ ℕs
𝑦 = (( -us
‘𝐴) +s (
1s /su 𝑛))}) |
88 | 55, 87 | oveq12d 7420 |
. . . . 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 2764 |
. . 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 28164 |
. 2
⊢ (𝐴 ∈ ℝs
↔ (𝐴 ∈ No ∧ (∃𝑛 ∈ ℕs (( -us
‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})))) |
93 | | elreno 28164 |
. 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) |