Step | Hyp | Ref
| Expression |
1 | | addscl 27839 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 +s 𝐵) ∈ No
) |
2 | 1 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ((∃𝑛 ∈ ℕs (( -us
‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))}))
∧ (∃𝑚 ∈
ℕs (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚) ∧ 𝐵 = ({𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))} |s
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}))))
→ (𝐴 +s
𝐵) ∈ No ) |
3 | | nnaddscl 28153 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕs
∧ 𝑚 ∈
ℕs) → (𝑛 +s 𝑚) ∈
ℕs) |
4 | 3 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑛 ∈ ℕs
∧ 𝑚 ∈
ℕs) ∧ ((( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚))) → (𝑛 +s 𝑚) ∈
ℕs) |
5 | 4 | adantl 481 |
. . . . . . . 8
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ((𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs)
∧ ((( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚)))) → (𝑛 +s 𝑚) ∈
ℕs) |
6 | | simprll 776 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ((𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs)
∧ ((( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚)))) → 𝑛 ∈ ℕs) |
7 | 6 | nnsnod 28139 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ((𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs)
∧ ((( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚)))) → 𝑛 ∈ No
) |
8 | | simprlr 777 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ((𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs)
∧ ((( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚)))) → 𝑚 ∈ ℕs) |
9 | 8 | nnsnod 28139 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ((𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs)
∧ ((( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚)))) → 𝑚 ∈ No
) |
10 | | negsdi 27903 |
. . . . . . . . . 10
⊢ ((𝑛 ∈
No ∧ 𝑚 ∈
No ) → ( -us ‘(𝑛 +s 𝑚)) = (( -us
‘𝑛) +s (
-us ‘𝑚))) |
11 | 7, 9, 10 | syl2anc 583 |
. . . . . . . . 9
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ((𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs)
∧ ((( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚)))) → ( -us ‘(𝑛 +s 𝑚)) = (( -us
‘𝑛) +s (
-us ‘𝑚))) |
12 | 7 | negscld 27890 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ((𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs)
∧ ((( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚)))) → ( -us ‘𝑛) ∈
No ) |
13 | 9 | negscld 27890 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ((𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs)
∧ ((( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚)))) → ( -us ‘𝑚) ∈
No ) |
14 | | simpll 764 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ((𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs)
∧ ((( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚)))) → 𝐴 ∈ No
) |
15 | | simplr 766 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ((𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs)
∧ ((( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚)))) → 𝐵 ∈ No
) |
16 | | simprll 776 |
. . . . . . . . . . 11
⊢ (((𝑛 ∈ ℕs
∧ 𝑚 ∈
ℕs) ∧ ((( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚))) → ( -us ‘𝑛) <s 𝐴) |
17 | 16 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ((𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs)
∧ ((( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚)))) → ( -us ‘𝑛) <s 𝐴) |
18 | | simprrl 778 |
. . . . . . . . . . 11
⊢ (((𝑛 ∈ ℕs
∧ 𝑚 ∈
ℕs) ∧ ((( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚))) → ( -us ‘𝑚) <s 𝐵) |
19 | 18 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ((𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs)
∧ ((( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚)))) → ( -us ‘𝑚) <s 𝐵) |
20 | 12, 13, 14, 15, 17, 19 | slt2addd 27871 |
. . . . . . . . 9
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ((𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs)
∧ ((( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚)))) → (( -us ‘𝑛) +s ( -us
‘𝑚)) <s (𝐴 +s 𝐵)) |
21 | 11, 20 | eqbrtrd 5161 |
. . . . . . . 8
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ((𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs)
∧ ((( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚)))) → ( -us ‘(𝑛 +s 𝑚)) <s (𝐴 +s 𝐵)) |
22 | | simprlr 777 |
. . . . . . . . . 10
⊢ (((𝑛 ∈ ℕs
∧ 𝑚 ∈
ℕs) ∧ ((( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚))) → 𝐴 <s 𝑛) |
23 | 22 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ((𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs)
∧ ((( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚)))) → 𝐴 <s 𝑛) |
24 | | simprrr 779 |
. . . . . . . . . 10
⊢ (((𝑛 ∈ ℕs
∧ 𝑚 ∈
ℕs) ∧ ((( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚))) → 𝐵 <s 𝑚) |
25 | 24 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ((𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs)
∧ ((( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚)))) → 𝐵 <s 𝑚) |
26 | 14, 15, 7, 9, 23, 25 | slt2addd 27871 |
. . . . . . . 8
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ((𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs)
∧ ((( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚)))) → (𝐴 +s 𝐵) <s (𝑛 +s 𝑚)) |
27 | | fveq2 6882 |
. . . . . . . . . . 11
⊢ (𝑝 = (𝑛 +s 𝑚) → ( -us ‘𝑝) = ( -us
‘(𝑛 +s
𝑚))) |
28 | 27 | breq1d 5149 |
. . . . . . . . . 10
⊢ (𝑝 = (𝑛 +s 𝑚) → (( -us ‘𝑝) <s (𝐴 +s 𝐵) ↔ ( -us ‘(𝑛 +s 𝑚)) <s (𝐴 +s 𝐵))) |
29 | | breq2 5143 |
. . . . . . . . . 10
⊢ (𝑝 = (𝑛 +s 𝑚) → ((𝐴 +s 𝐵) <s 𝑝 ↔ (𝐴 +s 𝐵) <s (𝑛 +s 𝑚))) |
30 | 28, 29 | anbi12d 630 |
. . . . . . . . 9
⊢ (𝑝 = (𝑛 +s 𝑚) → ((( -us ‘𝑝) <s (𝐴 +s 𝐵) ∧ (𝐴 +s 𝐵) <s 𝑝) ↔ (( -us ‘(𝑛 +s 𝑚)) <s (𝐴 +s 𝐵) ∧ (𝐴 +s 𝐵) <s (𝑛 +s 𝑚)))) |
31 | 30 | rspcev 3604 |
. . . . . . . 8
⊢ (((𝑛 +s 𝑚) ∈ ℕs
∧ (( -us ‘(𝑛 +s 𝑚)) <s (𝐴 +s 𝐵) ∧ (𝐴 +s 𝐵) <s (𝑛 +s 𝑚))) → ∃𝑝 ∈ ℕs (( -us
‘𝑝) <s (𝐴 +s 𝐵) ∧ (𝐴 +s 𝐵) <s 𝑝)) |
32 | 5, 21, 26, 31 | syl12anc 834 |
. . . . . . 7
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ((𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs)
∧ ((( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚)))) → ∃𝑝 ∈ ℕs (( -us
‘𝑝) <s (𝐴 +s 𝐵) ∧ (𝐴 +s 𝐵) <s 𝑝)) |
33 | 32 | expr 456 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs))
→ (((( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚)) → ∃𝑝 ∈ ℕs (( -us
‘𝑝) <s (𝐴 +s 𝐵) ∧ (𝐴 +s 𝐵) <s 𝑝))) |
34 | 33 | rexlimdvva 3203 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑛 ∈ ℕs ∃𝑚 ∈ ℕs (((
-us ‘𝑛)
<s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚)) → ∃𝑝 ∈ ℕs (( -us
‘𝑝) <s (𝐴 +s 𝐵) ∧ (𝐴 +s 𝐵) <s 𝑝))) |
35 | | simpl 482 |
. . . . . . 7
⊢
((∃𝑛 ∈
ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))}))
→ ∃𝑛 ∈
ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛)) |
36 | | simpl 482 |
. . . . . . 7
⊢
((∃𝑚 ∈
ℕs (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚) ∧ 𝐵 = ({𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))} |s
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}))
→ ∃𝑚 ∈
ℕs (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚)) |
37 | 35, 36 | anim12i 612 |
. . . . . 6
⊢
(((∃𝑛 ∈
ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))}))
∧ (∃𝑚 ∈
ℕs (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚) ∧ 𝐵 = ({𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))} |s
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))})))
→ (∃𝑛 ∈
ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ ∃𝑚 ∈ ℕs (( -us
‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚))) |
38 | | reeanv 3218 |
. . . . . 6
⊢
(∃𝑛 ∈
ℕs ∃𝑚 ∈ ℕs (((
-us ‘𝑛)
<s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚)) ↔ (∃𝑛 ∈ ℕs (( -us
‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ ∃𝑚 ∈ ℕs (( -us
‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚))) |
39 | 37, 38 | sylibr 233 |
. . . . 5
⊢
(((∃𝑛 ∈
ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))}))
∧ (∃𝑚 ∈
ℕs (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚) ∧ 𝐵 = ({𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))} |s
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))})))
→ ∃𝑛 ∈
ℕs ∃𝑚 ∈ ℕs (((
-us ‘𝑛)
<s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚))) |
40 | 34, 39 | impel 505 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ((∃𝑛 ∈ ℕs (( -us
‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))}))
∧ (∃𝑚 ∈
ℕs (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚) ∧ 𝐵 = ({𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))} |s
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}))))
→ ∃𝑝 ∈
ℕs (( -us ‘𝑝) <s (𝐴 +s 𝐵) ∧ (𝐴 +s 𝐵) <s 𝑝)) |
41 | | simpr 484 |
. . . . . 6
⊢
((∃𝑛 ∈
ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))}))
→ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})) |
42 | | simpr 484 |
. . . . . 6
⊢
((∃𝑚 ∈
ℕs (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚) ∧ 𝐵 = ({𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))} |s
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}))
→ 𝐵 = ({𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))} |s
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))})) |
43 | 41, 42 | anim12i 612 |
. . . . 5
⊢
(((∃𝑛 ∈
ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))}))
∧ (∃𝑚 ∈
ℕs (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚) ∧ 𝐵 = ({𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))} |s
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))})))
→ (𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})
∧ 𝐵 = ({𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))} |s
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}))) |
44 | | simpll 764 |
. . . . . . . 8
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})
∧ 𝐵 = ({𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))} |s
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))})))
→ 𝐴 ∈ No ) |
45 | | recut 28165 |
. . . . . . . 8
⊢ (𝐴 ∈
No → {𝑥
∣ ∃𝑛 ∈
ℕs 𝑥 =
(𝐴 -s (
1s /su 𝑛))} <<s {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}) |
46 | 44, 45 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})
∧ 𝐵 = ({𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))} |s
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))})))
→ {𝑥 ∣
∃𝑛 ∈
ℕs 𝑥 =
(𝐴 -s (
1s /su 𝑛))} <<s {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}) |
47 | | simplr 766 |
. . . . . . . 8
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})
∧ 𝐵 = ({𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))} |s
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))})))
→ 𝐵 ∈ No ) |
48 | | recut 28165 |
. . . . . . . 8
⊢ (𝐵 ∈
No → {𝑦
∣ ∃𝑚 ∈
ℕs 𝑦 =
(𝐵 -s (
1s /su 𝑚))} <<s {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}) |
49 | 47, 48 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})
∧ 𝐵 = ({𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))} |s
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))})))
→ {𝑦 ∣
∃𝑚 ∈
ℕs 𝑦 =
(𝐵 -s (
1s /su 𝑚))} <<s {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}) |
50 | | simprl 768 |
. . . . . . 7
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})
∧ 𝐵 = ({𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))} |s
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))})))
→ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})) |
51 | | simprr 770 |
. . . . . . 7
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})
∧ 𝐵 = ({𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))} |s
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))})))
→ 𝐵 = ({𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))} |s
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))})) |
52 | 46, 49, 50, 51 | addsunif 27860 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})
∧ 𝐵 = ({𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))} |s
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))})))
→ (𝐴 +s
𝐵) = (({𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))}𝑧 = (𝑡 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑡 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = (𝐴 +s 𝑡)}) |s ({𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}𝑧 = (𝑡 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑡 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = (𝐴 +s 𝑡)}))) |
53 | | ovex 7435 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 -s ( 1s
/su 𝑛))
∈ V |
54 | | oveq1 7409 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = (𝐴 -s ( 1s
/su 𝑛))
→ (𝑡 +s
𝐵) = ((𝐴 -s ( 1s
/su 𝑛))
+s 𝐵)) |
55 | 54 | eqeq2d 2735 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = (𝐴 -s ( 1s
/su 𝑛))
→ (𝑧 = (𝑡 +s 𝐵) ↔ 𝑧 = ((𝐴 -s ( 1s
/su 𝑛))
+s 𝐵))) |
56 | 53, 55 | ceqsexv 3518 |
. . . . . . . . . . . . . 14
⊢
(∃𝑡(𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ 𝑧 = (𝑡 +s 𝐵)) ↔ 𝑧 = ((𝐴 -s ( 1s
/su 𝑛))
+s 𝐵)) |
57 | | simpll 764 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) → 𝐴 ∈
No ) |
58 | | simplr 766 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) → 𝐵 ∈
No ) |
59 | | 1sno 27701 |
. . . . . . . . . . . . . . . . . . 19
⊢
1s ∈ No |
60 | 59 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕs
→ 1s ∈ No ) |
61 | | nnsno 28137 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕs
→ 𝑛 ∈ No ) |
62 | | nnne0s 28146 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕs
→ 𝑛 ≠ 0s
) |
63 | 60, 61, 62 | divscld 28063 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕs
→ ( 1s /su 𝑛) ∈ No
) |
64 | 63 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) → (
1s /su 𝑛) ∈ No
) |
65 | 57, 58, 64 | addsubsd 27931 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) → ((𝐴 +s 𝐵) -s ( 1s
/su 𝑛)) =
((𝐴 -s (
1s /su 𝑛)) +s 𝐵)) |
66 | 65 | eqeq2d 2735 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) → (𝑧 = ((𝐴 +s 𝐵) -s ( 1s
/su 𝑛))
↔ 𝑧 = ((𝐴 -s ( 1s
/su 𝑛))
+s 𝐵))) |
67 | 56, 66 | bitr4id 290 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) →
(∃𝑡(𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ 𝑧 = (𝑡 +s 𝐵)) ↔ 𝑧 = ((𝐴 +s 𝐵) -s ( 1s
/su 𝑛)))) |
68 | 67 | rexbidva 3168 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑛 ∈ ℕs ∃𝑡(𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ 𝑧 = (𝑡 +s 𝐵)) ↔ ∃𝑛 ∈ ℕs 𝑧 = ((𝐴 +s 𝐵) -s ( 1s
/su 𝑛)))) |
69 | | r19.41v 3180 |
. . . . . . . . . . . . . 14
⊢
(∃𝑛 ∈
ℕs (𝑡 =
(𝐴 -s (
1s /su 𝑛)) ∧ 𝑧 = (𝑡 +s 𝐵)) ↔ (∃𝑛 ∈ ℕs 𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ 𝑧 = (𝑡 +s 𝐵))) |
70 | 69 | exbii 1842 |
. . . . . . . . . . . . 13
⊢
(∃𝑡∃𝑛 ∈ ℕs (𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ 𝑧 = (𝑡 +s 𝐵)) ↔ ∃𝑡(∃𝑛 ∈ ℕs 𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ 𝑧 = (𝑡 +s 𝐵))) |
71 | | rexcom4 3277 |
. . . . . . . . . . . . 13
⊢
(∃𝑛 ∈
ℕs ∃𝑡(𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ 𝑧 = (𝑡 +s 𝐵)) ↔ ∃𝑡∃𝑛 ∈ ℕs (𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ 𝑧 = (𝑡 +s 𝐵))) |
72 | | eqeq1 2728 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑡 → (𝑥 = (𝐴 -s ( 1s
/su 𝑛))
↔ 𝑡 = (𝐴 -s ( 1s
/su 𝑛)))) |
73 | 72 | rexbidv 3170 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑡 → (∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))
↔ ∃𝑛 ∈
ℕs 𝑡 =
(𝐴 -s (
1s /su 𝑛)))) |
74 | 73 | rexab 3683 |
. . . . . . . . . . . . 13
⊢
(∃𝑡 ∈
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 -s ( 1s
/su 𝑛))}𝑧 = (𝑡 +s 𝐵) ↔ ∃𝑡(∃𝑛 ∈ ℕs 𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ 𝑧 = (𝑡 +s 𝐵))) |
75 | 70, 71, 74 | 3bitr4ri 304 |
. . . . . . . . . . . 12
⊢
(∃𝑡 ∈
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 -s ( 1s
/su 𝑛))}𝑧 = (𝑡 +s 𝐵) ↔ ∃𝑛 ∈ ℕs ∃𝑡(𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ 𝑧 = (𝑡 +s 𝐵))) |
76 | | oveq2 7410 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 𝑛 → ( 1s /su
𝑝) = ( 1s
/su 𝑛)) |
77 | 76 | oveq2d 7418 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 𝑛 → ((𝐴 +s 𝐵) -s ( 1s
/su 𝑝)) =
((𝐴 +s 𝐵) -s ( 1s
/su 𝑛))) |
78 | 77 | eqeq2d 2735 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑛 → (𝑧 = ((𝐴 +s 𝐵) -s ( 1s
/su 𝑝))
↔ 𝑧 = ((𝐴 +s 𝐵) -s ( 1s
/su 𝑛)))) |
79 | 78 | cbvrexvw 3227 |
. . . . . . . . . . . 12
⊢
(∃𝑝 ∈
ℕs 𝑧 =
((𝐴 +s 𝐵) -s ( 1s
/su 𝑝))
↔ ∃𝑛 ∈
ℕs 𝑧 =
((𝐴 +s 𝐵) -s ( 1s
/su 𝑛))) |
80 | 68, 75, 79 | 3bitr4g 314 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))}𝑧 = (𝑡 +s 𝐵) ↔ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 +s 𝐵) -s ( 1s
/su 𝑝)))) |
81 | 80 | abbidv 2793 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → {𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))}𝑧 = (𝑡 +s 𝐵)} = {𝑧 ∣ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 +s 𝐵) -s ( 1s
/su 𝑝))}) |
82 | | ovex 7435 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 -s ( 1s
/su 𝑚))
∈ V |
83 | | oveq2 7410 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = (𝐵 -s ( 1s
/su 𝑚))
→ (𝐴 +s
𝑡) = (𝐴 +s (𝐵 -s ( 1s
/su 𝑚)))) |
84 | 83 | eqeq2d 2735 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = (𝐵 -s ( 1s
/su 𝑚))
→ (𝑧 = (𝐴 +s 𝑡) ↔ 𝑧 = (𝐴 +s (𝐵 -s ( 1s
/su 𝑚))))) |
85 | 82, 84 | ceqsexv 3518 |
. . . . . . . . . . . . . 14
⊢
(∃𝑡(𝑡 = (𝐵 -s ( 1s
/su 𝑚))
∧ 𝑧 = (𝐴 +s 𝑡)) ↔ 𝑧 = (𝐴 +s (𝐵 -s ( 1s
/su 𝑚)))) |
86 | | simpll 764 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑚 ∈ ℕs) → 𝐴 ∈
No ) |
87 | | simplr 766 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑚 ∈ ℕs) → 𝐵 ∈
No ) |
88 | 59 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ ℕs
→ 1s ∈ No ) |
89 | | nnsno 28137 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ ℕs
→ 𝑚 ∈ No ) |
90 | | nnne0s 28146 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ ℕs
→ 𝑚 ≠ 0s
) |
91 | 88, 89, 90 | divscld 28063 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ ℕs
→ ( 1s /su 𝑚) ∈ No
) |
92 | 91 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑚 ∈ ℕs) → (
1s /su 𝑚) ∈ No
) |
93 | 86, 87, 92 | addsubsassd 27930 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑚 ∈ ℕs) → ((𝐴 +s 𝐵) -s ( 1s
/su 𝑚)) =
(𝐴 +s (𝐵 -s ( 1s
/su 𝑚)))) |
94 | 93 | eqeq2d 2735 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑚 ∈ ℕs) → (𝑧 = ((𝐴 +s 𝐵) -s ( 1s
/su 𝑚))
↔ 𝑧 = (𝐴 +s (𝐵 -s ( 1s
/su 𝑚))))) |
95 | 85, 94 | bitr4id 290 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑚 ∈ ℕs) →
(∃𝑡(𝑡 = (𝐵 -s ( 1s
/su 𝑚))
∧ 𝑧 = (𝐴 +s 𝑡)) ↔ 𝑧 = ((𝐴 +s 𝐵) -s ( 1s
/su 𝑚)))) |
96 | 95 | rexbidva 3168 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑚 ∈ ℕs ∃𝑡(𝑡 = (𝐵 -s ( 1s
/su 𝑚))
∧ 𝑧 = (𝐴 +s 𝑡)) ↔ ∃𝑚 ∈ ℕs
𝑧 = ((𝐴 +s 𝐵) -s ( 1s
/su 𝑚)))) |
97 | | r19.41v 3180 |
. . . . . . . . . . . . . 14
⊢
(∃𝑚 ∈
ℕs (𝑡 =
(𝐵 -s (
1s /su 𝑚)) ∧ 𝑧 = (𝐴 +s 𝑡)) ↔ (∃𝑚 ∈ ℕs 𝑡 = (𝐵 -s ( 1s
/su 𝑚))
∧ 𝑧 = (𝐴 +s 𝑡))) |
98 | 97 | exbii 1842 |
. . . . . . . . . . . . 13
⊢
(∃𝑡∃𝑚 ∈ ℕs (𝑡 = (𝐵 -s ( 1s
/su 𝑚))
∧ 𝑧 = (𝐴 +s 𝑡)) ↔ ∃𝑡(∃𝑚 ∈ ℕs 𝑡 = (𝐵 -s ( 1s
/su 𝑚))
∧ 𝑧 = (𝐴 +s 𝑡))) |
99 | | rexcom4 3277 |
. . . . . . . . . . . . 13
⊢
(∃𝑚 ∈
ℕs ∃𝑡(𝑡 = (𝐵 -s ( 1s
/su 𝑚))
∧ 𝑧 = (𝐴 +s 𝑡)) ↔ ∃𝑡∃𝑚 ∈ ℕs (𝑡 = (𝐵 -s ( 1s
/su 𝑚))
∧ 𝑧 = (𝐴 +s 𝑡))) |
100 | | eqeq1 2728 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑡 → (𝑦 = (𝐵 -s ( 1s
/su 𝑚))
↔ 𝑡 = (𝐵 -s ( 1s
/su 𝑚)))) |
101 | 100 | rexbidv 3170 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑡 → (∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))
↔ ∃𝑚 ∈
ℕs 𝑡 =
(𝐵 -s (
1s /su 𝑚)))) |
102 | 101 | rexab 3683 |
. . . . . . . . . . . . 13
⊢
(∃𝑡 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = (𝐴 +s 𝑡) ↔ ∃𝑡(∃𝑚 ∈ ℕs 𝑡 = (𝐵 -s ( 1s
/su 𝑚))
∧ 𝑧 = (𝐴 +s 𝑡))) |
103 | 98, 99, 102 | 3bitr4ri 304 |
. . . . . . . . . . . 12
⊢
(∃𝑡 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = (𝐴 +s 𝑡) ↔ ∃𝑚 ∈ ℕs ∃𝑡(𝑡 = (𝐵 -s ( 1s
/su 𝑚))
∧ 𝑧 = (𝐴 +s 𝑡))) |
104 | | oveq2 7410 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 𝑚 → ( 1s /su
𝑝) = ( 1s
/su 𝑚)) |
105 | 104 | oveq2d 7418 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 𝑚 → ((𝐴 +s 𝐵) -s ( 1s
/su 𝑝)) =
((𝐴 +s 𝐵) -s ( 1s
/su 𝑚))) |
106 | 105 | eqeq2d 2735 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑚 → (𝑧 = ((𝐴 +s 𝐵) -s ( 1s
/su 𝑝))
↔ 𝑧 = ((𝐴 +s 𝐵) -s ( 1s
/su 𝑚)))) |
107 | 106 | cbvrexvw 3227 |
. . . . . . . . . . . 12
⊢
(∃𝑝 ∈
ℕs 𝑧 =
((𝐴 +s 𝐵) -s ( 1s
/su 𝑝))
↔ ∃𝑚 ∈
ℕs 𝑧 =
((𝐴 +s 𝐵) -s ( 1s
/su 𝑚))) |
108 | 96, 103, 107 | 3bitr4g 314 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑡 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = (𝐴 +s 𝑡) ↔ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 +s 𝐵) -s ( 1s
/su 𝑝)))) |
109 | 108 | abbidv 2793 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → {𝑧 ∣ ∃𝑡 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = (𝐴 +s 𝑡)} = {𝑧 ∣ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 +s 𝐵) -s ( 1s
/su 𝑝))}) |
110 | 81, 109 | uneq12d 4157 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ({𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))}𝑧 = (𝑡 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑡 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = (𝐴 +s 𝑡)}) = ({𝑧 ∣ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 +s 𝐵) -s ( 1s
/su 𝑝))}
∪ {𝑧 ∣
∃𝑝 ∈
ℕs 𝑧 =
((𝐴 +s 𝐵) -s ( 1s
/su 𝑝))})) |
111 | | unidm 4145 |
. . . . . . . . 9
⊢ ({𝑧 ∣ ∃𝑝 ∈ ℕs
𝑧 = ((𝐴 +s 𝐵) -s ( 1s
/su 𝑝))}
∪ {𝑧 ∣
∃𝑝 ∈
ℕs 𝑧 =
((𝐴 +s 𝐵) -s ( 1s
/su 𝑝))}) =
{𝑧 ∣ ∃𝑝 ∈ ℕs
𝑧 = ((𝐴 +s 𝐵) -s ( 1s
/su 𝑝))} |
112 | 110, 111 | eqtrdi 2780 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ({𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))}𝑧 = (𝑡 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑡 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = (𝐴 +s 𝑡)}) = {𝑧 ∣ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 +s 𝐵) -s ( 1s
/su 𝑝))}) |
113 | | ovex 7435 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 +s ( 1s
/su 𝑛))
∈ V |
114 | | oveq1 7409 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = (𝐴 +s ( 1s
/su 𝑛))
→ (𝑡 +s
𝐵) = ((𝐴 +s ( 1s
/su 𝑛))
+s 𝐵)) |
115 | 114 | eqeq2d 2735 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = (𝐴 +s ( 1s
/su 𝑛))
→ (𝑧 = (𝑡 +s 𝐵) ↔ 𝑧 = ((𝐴 +s ( 1s
/su 𝑛))
+s 𝐵))) |
116 | 113, 115 | ceqsexv 3518 |
. . . . . . . . . . . . . 14
⊢
(∃𝑡(𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ 𝑧 = (𝑡 +s 𝐵)) ↔ 𝑧 = ((𝐴 +s ( 1s
/su 𝑛))
+s 𝐵)) |
117 | 57, 64, 58 | adds32d 27865 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) → ((𝐴 +s ( 1s
/su 𝑛))
+s 𝐵) = ((𝐴 +s 𝐵) +s ( 1s
/su 𝑛))) |
118 | 117 | eqeq2d 2735 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) → (𝑧 = ((𝐴 +s ( 1s
/su 𝑛))
+s 𝐵) ↔
𝑧 = ((𝐴 +s 𝐵) +s ( 1s
/su 𝑛)))) |
119 | 116, 118 | bitrid 283 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) →
(∃𝑡(𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ 𝑧 = (𝑡 +s 𝐵)) ↔ 𝑧 = ((𝐴 +s 𝐵) +s ( 1s
/su 𝑛)))) |
120 | 119 | rexbidva 3168 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑛 ∈ ℕs ∃𝑡(𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ 𝑧 = (𝑡 +s 𝐵)) ↔ ∃𝑛 ∈ ℕs 𝑧 = ((𝐴 +s 𝐵) +s ( 1s
/su 𝑛)))) |
121 | | r19.41v 3180 |
. . . . . . . . . . . . . 14
⊢
(∃𝑛 ∈
ℕs (𝑡 =
(𝐴 +s (
1s /su 𝑛)) ∧ 𝑧 = (𝑡 +s 𝐵)) ↔ (∃𝑛 ∈ ℕs 𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ 𝑧 = (𝑡 +s 𝐵))) |
122 | 121 | exbii 1842 |
. . . . . . . . . . . . 13
⊢
(∃𝑡∃𝑛 ∈ ℕs (𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ 𝑧 = (𝑡 +s 𝐵)) ↔ ∃𝑡(∃𝑛 ∈ ℕs 𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ 𝑧 = (𝑡 +s 𝐵))) |
123 | | rexcom4 3277 |
. . . . . . . . . . . . 13
⊢
(∃𝑛 ∈
ℕs ∃𝑡(𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ 𝑧 = (𝑡 +s 𝐵)) ↔ ∃𝑡∃𝑛 ∈ ℕs (𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ 𝑧 = (𝑡 +s 𝐵))) |
124 | | eqeq1 2728 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑡 → (𝑥 = (𝐴 +s ( 1s
/su 𝑛))
↔ 𝑡 = (𝐴 +s ( 1s
/su 𝑛)))) |
125 | 124 | rexbidv 3170 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑡 → (∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))
↔ ∃𝑛 ∈
ℕs 𝑡 =
(𝐴 +s (
1s /su 𝑛)))) |
126 | 125 | rexab 3683 |
. . . . . . . . . . . . 13
⊢
(∃𝑡 ∈
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))}𝑧 = (𝑡 +s 𝐵) ↔ ∃𝑡(∃𝑛 ∈ ℕs 𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ 𝑧 = (𝑡 +s 𝐵))) |
127 | 122, 123,
126 | 3bitr4ri 304 |
. . . . . . . . . . . 12
⊢
(∃𝑡 ∈
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))}𝑧 = (𝑡 +s 𝐵) ↔ ∃𝑛 ∈ ℕs ∃𝑡(𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ 𝑧 = (𝑡 +s 𝐵))) |
128 | 76 | oveq2d 7418 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 𝑛 → ((𝐴 +s 𝐵) +s ( 1s
/su 𝑝)) =
((𝐴 +s 𝐵) +s ( 1s
/su 𝑛))) |
129 | 128 | eqeq2d 2735 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑛 → (𝑧 = ((𝐴 +s 𝐵) +s ( 1s
/su 𝑝))
↔ 𝑧 = ((𝐴 +s 𝐵) +s ( 1s
/su 𝑛)))) |
130 | 129 | cbvrexvw 3227 |
. . . . . . . . . . . 12
⊢
(∃𝑝 ∈
ℕs 𝑧 =
((𝐴 +s 𝐵) +s ( 1s
/su 𝑝))
↔ ∃𝑛 ∈
ℕs 𝑧 =
((𝐴 +s 𝐵) +s ( 1s
/su 𝑛))) |
131 | 120, 127,
130 | 3bitr4g 314 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}𝑧 = (𝑡 +s 𝐵) ↔ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 +s 𝐵) +s ( 1s
/su 𝑝)))) |
132 | 131 | abbidv 2793 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → {𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}𝑧 = (𝑡 +s 𝐵)} = {𝑧 ∣ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 +s 𝐵) +s ( 1s
/su 𝑝))}) |
133 | | ovex 7435 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 +s ( 1s
/su 𝑚))
∈ V |
134 | | oveq2 7410 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = (𝐵 +s ( 1s
/su 𝑚))
→ (𝐴 +s
𝑡) = (𝐴 +s (𝐵 +s ( 1s
/su 𝑚)))) |
135 | 134 | eqeq2d 2735 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = (𝐵 +s ( 1s
/su 𝑚))
→ (𝑧 = (𝐴 +s 𝑡) ↔ 𝑧 = (𝐴 +s (𝐵 +s ( 1s
/su 𝑚))))) |
136 | 133, 135 | ceqsexv 3518 |
. . . . . . . . . . . . . 14
⊢
(∃𝑡(𝑡 = (𝐵 +s ( 1s
/su 𝑚))
∧ 𝑧 = (𝐴 +s 𝑡)) ↔ 𝑧 = (𝐴 +s (𝐵 +s ( 1s
/su 𝑚)))) |
137 | 86, 87, 92 | addsassd 27864 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑚 ∈ ℕs) → ((𝐴 +s 𝐵) +s ( 1s
/su 𝑚)) =
(𝐴 +s (𝐵 +s ( 1s
/su 𝑚)))) |
138 | 137 | eqeq2d 2735 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑚 ∈ ℕs) → (𝑧 = ((𝐴 +s 𝐵) +s ( 1s
/su 𝑚))
↔ 𝑧 = (𝐴 +s (𝐵 +s ( 1s
/su 𝑚))))) |
139 | 136, 138 | bitr4id 290 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑚 ∈ ℕs) →
(∃𝑡(𝑡 = (𝐵 +s ( 1s
/su 𝑚))
∧ 𝑧 = (𝐴 +s 𝑡)) ↔ 𝑧 = ((𝐴 +s 𝐵) +s ( 1s
/su 𝑚)))) |
140 | 139 | rexbidva 3168 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑚 ∈ ℕs ∃𝑡(𝑡 = (𝐵 +s ( 1s
/su 𝑚))
∧ 𝑧 = (𝐴 +s 𝑡)) ↔ ∃𝑚 ∈ ℕs
𝑧 = ((𝐴 +s 𝐵) +s ( 1s
/su 𝑚)))) |
141 | | r19.41v 3180 |
. . . . . . . . . . . . . 14
⊢
(∃𝑚 ∈
ℕs (𝑡 =
(𝐵 +s (
1s /su 𝑚)) ∧ 𝑧 = (𝐴 +s 𝑡)) ↔ (∃𝑚 ∈ ℕs 𝑡 = (𝐵 +s ( 1s
/su 𝑚))
∧ 𝑧 = (𝐴 +s 𝑡))) |
142 | 141 | exbii 1842 |
. . . . . . . . . . . . 13
⊢
(∃𝑡∃𝑚 ∈ ℕs (𝑡 = (𝐵 +s ( 1s
/su 𝑚))
∧ 𝑧 = (𝐴 +s 𝑡)) ↔ ∃𝑡(∃𝑚 ∈ ℕs 𝑡 = (𝐵 +s ( 1s
/su 𝑚))
∧ 𝑧 = (𝐴 +s 𝑡))) |
143 | | rexcom4 3277 |
. . . . . . . . . . . . 13
⊢
(∃𝑚 ∈
ℕs ∃𝑡(𝑡 = (𝐵 +s ( 1s
/su 𝑚))
∧ 𝑧 = (𝐴 +s 𝑡)) ↔ ∃𝑡∃𝑚 ∈ ℕs (𝑡 = (𝐵 +s ( 1s
/su 𝑚))
∧ 𝑧 = (𝐴 +s 𝑡))) |
144 | | eqeq1 2728 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑡 → (𝑦 = (𝐵 +s ( 1s
/su 𝑚))
↔ 𝑡 = (𝐵 +s ( 1s
/su 𝑚)))) |
145 | 144 | rexbidv 3170 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑡 → (∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))
↔ ∃𝑚 ∈
ℕs 𝑡 =
(𝐵 +s (
1s /su 𝑚)))) |
146 | 145 | rexab 3683 |
. . . . . . . . . . . . 13
⊢
(∃𝑡 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = (𝐴 +s 𝑡) ↔ ∃𝑡(∃𝑚 ∈ ℕs 𝑡 = (𝐵 +s ( 1s
/su 𝑚))
∧ 𝑧 = (𝐴 +s 𝑡))) |
147 | 142, 143,
146 | 3bitr4ri 304 |
. . . . . . . . . . . 12
⊢
(∃𝑡 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = (𝐴 +s 𝑡) ↔ ∃𝑚 ∈ ℕs ∃𝑡(𝑡 = (𝐵 +s ( 1s
/su 𝑚))
∧ 𝑧 = (𝐴 +s 𝑡))) |
148 | 104 | oveq2d 7418 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 𝑚 → ((𝐴 +s 𝐵) +s ( 1s
/su 𝑝)) =
((𝐴 +s 𝐵) +s ( 1s
/su 𝑚))) |
149 | 148 | eqeq2d 2735 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑚 → (𝑧 = ((𝐴 +s 𝐵) +s ( 1s
/su 𝑝))
↔ 𝑧 = ((𝐴 +s 𝐵) +s ( 1s
/su 𝑚)))) |
150 | 149 | cbvrexvw 3227 |
. . . . . . . . . . . 12
⊢
(∃𝑝 ∈
ℕs 𝑧 =
((𝐴 +s 𝐵) +s ( 1s
/su 𝑝))
↔ ∃𝑚 ∈
ℕs 𝑧 =
((𝐴 +s 𝐵) +s ( 1s
/su 𝑚))) |
151 | 140, 147,
150 | 3bitr4g 314 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑡 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = (𝐴 +s 𝑡) ↔ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 +s 𝐵) +s ( 1s
/su 𝑝)))) |
152 | 151 | abbidv 2793 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → {𝑧 ∣ ∃𝑡 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = (𝐴 +s 𝑡)} = {𝑧 ∣ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 +s 𝐵) +s ( 1s
/su 𝑝))}) |
153 | 132, 152 | uneq12d 4157 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ({𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}𝑧 = (𝑡 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑡 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = (𝐴 +s 𝑡)}) = ({𝑧 ∣ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 +s 𝐵) +s ( 1s
/su 𝑝))}
∪ {𝑧 ∣
∃𝑝 ∈
ℕs 𝑧 =
((𝐴 +s 𝐵) +s ( 1s
/su 𝑝))})) |
154 | | unidm 4145 |
. . . . . . . . 9
⊢ ({𝑧 ∣ ∃𝑝 ∈ ℕs
𝑧 = ((𝐴 +s 𝐵) +s ( 1s
/su 𝑝))}
∪ {𝑧 ∣
∃𝑝 ∈
ℕs 𝑧 =
((𝐴 +s 𝐵) +s ( 1s
/su 𝑝))}) =
{𝑧 ∣ ∃𝑝 ∈ ℕs
𝑧 = ((𝐴 +s 𝐵) +s ( 1s
/su 𝑝))} |
155 | 153, 154 | eqtrdi 2780 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ({𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}𝑧 = (𝑡 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑡 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = (𝐴 +s 𝑡)}) = {𝑧 ∣ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 +s 𝐵) +s ( 1s
/su 𝑝))}) |
156 | 112, 155 | oveq12d 7420 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (({𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))}𝑧 = (𝑡 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑡 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = (𝐴 +s 𝑡)}) |s ({𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}𝑧 = (𝑡 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑡 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = (𝐴 +s 𝑡)})) = ({𝑧 ∣ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 +s 𝐵) -s ( 1s
/su 𝑝))} |s
{𝑧 ∣ ∃𝑝 ∈ ℕs
𝑧 = ((𝐴 +s 𝐵) +s ( 1s
/su 𝑝))})) |
157 | 156 | adantr 480 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})
∧ 𝐵 = ({𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))} |s
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))})))
→ (({𝑧 ∣
∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 -s ( 1s
/su 𝑛))}𝑧 = (𝑡 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑡 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = (𝐴 +s 𝑡)}) |s ({𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}𝑧 = (𝑡 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑡 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = (𝐴 +s 𝑡)})) = ({𝑧 ∣ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 +s 𝐵) -s ( 1s
/su 𝑝))} |s
{𝑧 ∣ ∃𝑝 ∈ ℕs
𝑧 = ((𝐴 +s 𝐵) +s ( 1s
/su 𝑝))})) |
158 | 52, 157 | eqtrd 2764 |
. . . . 5
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})
∧ 𝐵 = ({𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))} |s
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))})))
→ (𝐴 +s
𝐵) = ({𝑧 ∣ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 +s 𝐵) -s ( 1s
/su 𝑝))} |s
{𝑧 ∣ ∃𝑝 ∈ ℕs
𝑧 = ((𝐴 +s 𝐵) +s ( 1s
/su 𝑝))})) |
159 | 43, 158 | sylan2 592 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ((∃𝑛 ∈ ℕs (( -us
‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))}))
∧ (∃𝑚 ∈
ℕs (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚) ∧ 𝐵 = ({𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))} |s
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}))))
→ (𝐴 +s
𝐵) = ({𝑧 ∣ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 +s 𝐵) -s ( 1s
/su 𝑝))} |s
{𝑧 ∣ ∃𝑝 ∈ ℕs
𝑧 = ((𝐴 +s 𝐵) +s ( 1s
/su 𝑝))})) |
160 | 2, 40, 159 | jca32 515 |
. . 3
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ((∃𝑛 ∈ ℕs (( -us
‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))}))
∧ (∃𝑚 ∈
ℕs (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚) ∧ 𝐵 = ({𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))} |s
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}))))
→ ((𝐴 +s
𝐵) ∈ No ∧ (∃𝑝 ∈ ℕs (( -us
‘𝑝) <s (𝐴 +s 𝐵) ∧ (𝐴 +s 𝐵) <s 𝑝) ∧ (𝐴 +s 𝐵) = ({𝑧 ∣ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 +s 𝐵) -s ( 1s
/su 𝑝))} |s
{𝑧 ∣ ∃𝑝 ∈ ℕs
𝑧 = ((𝐴 +s 𝐵) +s ( 1s
/su 𝑝))})))) |
161 | 160 | an4s 657 |
. 2
⊢ (((𝐴 ∈
No ∧ (∃𝑛
∈ ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})))
∧ (𝐵 ∈ No ∧ (∃𝑚 ∈ ℕs (( -us
‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚) ∧ 𝐵 = ({𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))} |s
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}))))
→ ((𝐴 +s
𝐵) ∈ No ∧ (∃𝑝 ∈ ℕs (( -us
‘𝑝) <s (𝐴 +s 𝐵) ∧ (𝐴 +s 𝐵) <s 𝑝) ∧ (𝐴 +s 𝐵) = ({𝑧 ∣ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 +s 𝐵) -s ( 1s
/su 𝑝))} |s
{𝑧 ∣ ∃𝑝 ∈ ℕs
𝑧 = ((𝐴 +s 𝐵) +s ( 1s
/su 𝑝))})))) |
162 | | elreno 28164 |
. . 3
⊢ (𝐴 ∈ ℝs
↔ (𝐴 ∈ No ∧ (∃𝑛 ∈ ℕs (( -us
‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})))) |
163 | | elreno 28164 |
. . 3
⊢ (𝐵 ∈ ℝs
↔ (𝐵 ∈ No ∧ (∃𝑚 ∈ ℕs (( -us
‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚) ∧ 𝐵 = ({𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))} |s
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))})))) |
164 | 162, 163 | anbi12i 626 |
. 2
⊢ ((𝐴 ∈ ℝs
∧ 𝐵 ∈
ℝs) ↔ ((𝐴 ∈ No
∧ (∃𝑛 ∈
ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})))
∧ (𝐵 ∈ No ∧ (∃𝑚 ∈ ℕs (( -us
‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚) ∧ 𝐵 = ({𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))} |s
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}))))) |
165 | | elreno 28164 |
. 2
⊢ ((𝐴 +s 𝐵) ∈ ℝs ↔ ((𝐴 +s 𝐵) ∈ No
∧ (∃𝑝 ∈
ℕs (( -us ‘𝑝) <s (𝐴 +s 𝐵) ∧ (𝐴 +s 𝐵) <s 𝑝) ∧ (𝐴 +s 𝐵) = ({𝑧 ∣ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 +s 𝐵) -s ( 1s
/su 𝑝))} |s
{𝑧 ∣ ∃𝑝 ∈ ℕs
𝑧 = ((𝐴 +s 𝐵) +s ( 1s
/su 𝑝))})))) |
166 | 161, 164,
165 | 3imtr4i 292 |
1
⊢ ((𝐴 ∈ ℝs
∧ 𝐵 ∈
ℝs) → (𝐴 +s 𝐵) ∈
ℝs) |