Step | Hyp | Ref
| Expression |
1 | | mulscl 28047 |
. . . . 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 | | remulscllem2 28242 |
. . . . . . 7
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ((𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs)
∧ ((( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚)))) → ∃𝑝 ∈ ℕs (( -us
‘𝑝) <s (𝐴 ·s 𝐵) ∧ (𝐴 ·s 𝐵) <s 𝑝)) |
4 | 3 | expr 456 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (𝑛 ∈ ℕs ∧ 𝑚 ∈ ℕs))
→ (((( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚)) → ∃𝑝 ∈ ℕs (( -us
‘𝑝) <s (𝐴 ·s 𝐵) ∧ (𝐴 ·s 𝐵) <s 𝑝))) |
5 | 4 | rexlimdvva 3208 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑛 ∈ ℕs ∃𝑚 ∈ ℕs (((
-us ‘𝑛)
<s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚)) → ∃𝑝 ∈ ℕs (( -us
‘𝑝) <s (𝐴 ·s 𝐵) ∧ (𝐴 ·s 𝐵) <s 𝑝))) |
6 | | simpl 482 |
. . . . . . 7
⊢
((∃𝑛 ∈
ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))}))
→ ∃𝑛 ∈
ℕs (( -us ‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛)) |
7 | | simpl 482 |
. . . . . . 7
⊢
((∃𝑚 ∈
ℕs (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚) ∧ 𝐵 = ({𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))} |s
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}))
→ ∃𝑚 ∈
ℕs (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚)) |
8 | 6, 7 | 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 𝑚))) |
9 | | reeanv 3223 |
. . . . . 6
⊢
(∃𝑛 ∈
ℕs ∃𝑚 ∈ ℕs (((
-us ‘𝑛)
<s 𝐴 ∧ 𝐴 <s 𝑛) ∧ (( -us ‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚)) ↔ (∃𝑛 ∈ ℕs (( -us
‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ ∃𝑚 ∈ ℕs (( -us
‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚))) |
10 | 8, 9 | 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 𝑚))) |
11 | 5, 10 | 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 𝑝)) |
12 | | 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 𝑛))})) |
13 | | 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 𝑚))})) |
14 | 12, 13 | 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 𝑚))}))) |
15 | | recut 28237 |
. . . . . . . . 9
⊢ (𝐴 ∈
No → {𝑥
∣ ∃𝑛 ∈
ℕs 𝑥 =
(𝐴 -s (
1s /su 𝑛))} <<s {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}) |
16 | 15 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))}
<<s {𝑥 ∣
∃𝑛 ∈
ℕs 𝑥 =
(𝐴 +s (
1s /su 𝑛))}) |
17 | 16 | adantr 480 |
. . . . . . 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 𝑛))}) |
18 | | recut 28237 |
. . . . . . . 8
⊢ (𝐵 ∈
No → {𝑦
∣ ∃𝑚 ∈
ℕs 𝑦 =
(𝐵 -s (
1s /su 𝑚))} <<s {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}) |
19 | 18 | ad2antlr 726 |
. . . . . . 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 𝑚))}) |
20 | | simprl 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 𝑛))})) |
21 | | simprr 772 |
. . . . . . 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 𝑚))})) |
22 | 17, 19, 20, 21 | mulsunif2 28083 |
. . . . . 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 ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑡) ·s (𝐵 -s 𝑢)))} ∪ {𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝑡 -s 𝐴) ·s (𝑢 -s 𝐵)))}) |s ({𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)))} ∪ {𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝑡 -s 𝐴) ·s (𝐵 -s 𝑢)))}))) |
23 | | r19.41v 3185 |
. . . . . . . . . . . . . 14
⊢
(∃𝑛 ∈
ℕs (𝑡 =
(𝐴 -s (
1s /su 𝑛)) ∧ ∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑡) ·s (𝐵 -s 𝑢)))) ↔ (∃𝑛 ∈ ℕs 𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑡) ·s (𝐵 -s 𝑢))))) |
24 | 23 | exbii 1843 |
. . . . . . . . . . . . 13
⊢
(∃𝑡∃𝑛 ∈ ℕs (𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑡) ·s (𝐵 -s 𝑢)))) ↔ ∃𝑡(∃𝑛 ∈ ℕs 𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑡) ·s (𝐵 -s 𝑢))))) |
25 | | rexcom4 3282 |
. . . . . . . . . . . . 13
⊢
(∃𝑛 ∈
ℕs ∃𝑡(𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑡) ·s (𝐵 -s 𝑢)))) ↔ ∃𝑡∃𝑛 ∈ ℕs (𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑡) ·s (𝐵 -s 𝑢))))) |
26 | | eqeq1 2732 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑡 → (𝑥 = (𝐴 -s ( 1s
/su 𝑛))
↔ 𝑡 = (𝐴 -s ( 1s
/su 𝑛)))) |
27 | 26 | rexbidv 3175 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑡 → (∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))
↔ ∃𝑛 ∈
ℕs 𝑡 =
(𝐴 -s (
1s /su 𝑛)))) |
28 | 27 | rexab 3689 |
. . . . . . . . . . . . 13
⊢
(∃𝑡 ∈
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 -s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑡) ·s (𝐵 -s 𝑢))) ↔ ∃𝑡(∃𝑛 ∈ ℕs 𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑡) ·s (𝐵 -s 𝑢))))) |
29 | 24, 25, 28 | 3bitr4ri 304 |
. . . . . . . . . . . 12
⊢
(∃𝑡 ∈
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 -s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑡) ·s (𝐵 -s 𝑢))) ↔ ∃𝑛 ∈ ℕs ∃𝑡(𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑡) ·s (𝐵 -s 𝑢))))) |
30 | | ovex 7453 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 -s ( 1s
/su 𝑛))
∈ V |
31 | | oveq2 7428 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = (𝐴 -s ( 1s
/su 𝑛))
→ (𝐴 -s
𝑡) = (𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))) |
32 | 31 | oveq1d 7435 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = (𝐴 -s ( 1s
/su 𝑛))
→ ((𝐴 -s
𝑡) ·s
(𝐵 -s 𝑢)) = ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝐵
-s 𝑢))) |
33 | 32 | oveq2d 7436 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = (𝐴 -s ( 1s
/su 𝑛))
→ ((𝐴
·s 𝐵)
-s ((𝐴
-s 𝑡)
·s (𝐵
-s 𝑢))) =
((𝐴 ·s
𝐵) -s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝐵
-s 𝑢)))) |
34 | 33 | eqeq2d 2739 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = (𝐴 -s ( 1s
/su 𝑛))
→ (𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑡) ·s (𝐵 -s 𝑢))) ↔ 𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝐵
-s 𝑢))))) |
35 | 34 | rexbidv 3175 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (𝐴 -s ( 1s
/su 𝑛))
→ (∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑡) ·s (𝐵 -s 𝑢))) ↔ ∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝐵
-s 𝑢))))) |
36 | 30, 35 | ceqsexv 3523 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑡(𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑡) ·s (𝐵 -s 𝑢)))) ↔ ∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝐵
-s 𝑢)))) |
37 | | r19.41v 3185 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑚 ∈
ℕs (𝑢 =
(𝐵 -s (
1s /su 𝑚)) ∧ 𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝐵
-s 𝑢)))) ↔
(∃𝑚 ∈
ℕs 𝑢 =
(𝐵 -s (
1s /su 𝑚)) ∧ 𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝐵
-s 𝑢))))) |
38 | 37 | exbii 1843 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑢∃𝑚 ∈ ℕs (𝑢 = (𝐵 -s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝐵
-s 𝑢)))) ↔
∃𝑢(∃𝑚 ∈ ℕs
𝑢 = (𝐵 -s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝐵
-s 𝑢))))) |
39 | | rexcom4 3282 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑚 ∈
ℕs ∃𝑢(𝑢 = (𝐵 -s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝐵
-s 𝑢)))) ↔
∃𝑢∃𝑚 ∈ ℕs
(𝑢 = (𝐵 -s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝐵
-s 𝑢))))) |
40 | | eqeq1 2732 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑢 → (𝑦 = (𝐵 -s ( 1s
/su 𝑚))
↔ 𝑢 = (𝐵 -s ( 1s
/su 𝑚)))) |
41 | 40 | rexbidv 3175 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑢 → (∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))
↔ ∃𝑚 ∈
ℕs 𝑢 =
(𝐵 -s (
1s /su 𝑚)))) |
42 | 41 | rexab 3689 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝐵
-s 𝑢))) ↔
∃𝑢(∃𝑚 ∈ ℕs
𝑢 = (𝐵 -s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝐵
-s 𝑢))))) |
43 | 38, 39, 42 | 3bitr4ri 304 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝐵
-s 𝑢))) ↔
∃𝑚 ∈
ℕs ∃𝑢(𝑢 = (𝐵 -s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝐵
-s 𝑢))))) |
44 | 36, 43 | bitri 275 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑡(𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑡) ·s (𝐵 -s 𝑢)))) ↔ ∃𝑚 ∈ ℕs ∃𝑢(𝑢 = (𝐵 -s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝐵
-s 𝑢))))) |
45 | | ovex 7453 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐵 -s ( 1s
/su 𝑚))
∈ V |
46 | | oveq2 7428 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 = (𝐵 -s ( 1s
/su 𝑚))
→ (𝐵 -s
𝑢) = (𝐵 -s (𝐵 -s ( 1s
/su 𝑚)))) |
47 | 46 | oveq2d 7436 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 = (𝐵 -s ( 1s
/su 𝑚))
→ ((𝐴 -s
(𝐴 -s (
1s /su 𝑛))) ·s (𝐵 -s 𝑢)) = ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝐵
-s (𝐵
-s ( 1s /su 𝑚))))) |
48 | 47 | oveq2d 7436 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = (𝐵 -s ( 1s
/su 𝑚))
→ ((𝐴
·s 𝐵)
-s ((𝐴
-s (𝐴
-s ( 1s /su 𝑛))) ·s (𝐵 -s 𝑢))) = ((𝐴 ·s 𝐵) -s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝐵
-s (𝐵
-s ( 1s /su 𝑚)))))) |
49 | 48 | eqeq2d 2739 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = (𝐵 -s ( 1s
/su 𝑚))
→ (𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝐵
-s 𝑢))) ↔
𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝐵
-s (𝐵
-s ( 1s /su 𝑚))))))) |
50 | 45, 49 | ceqsexv 3523 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑢(𝑢 = (𝐵 -s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝐵
-s 𝑢)))) ↔
𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝐵
-s (𝐵
-s ( 1s /su 𝑚)))))) |
51 | | simplll 774 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) ∧ 𝑚 ∈ ℕs)
→ 𝐴 ∈ No ) |
52 | | 1sno 27773 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
1s ∈ No |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) ∧ 𝑚 ∈ ℕs)
→ 1s ∈ No ) |
54 | | nnsno 28209 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ ℕs
→ 𝑛 ∈ No ) |
55 | 54 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) ∧ 𝑚 ∈ ℕs)
→ 𝑛 ∈ No ) |
56 | | nnne0s 28218 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ ℕs
→ 𝑛 ≠ 0s
) |
57 | 56 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) ∧ 𝑚 ∈ ℕs)
→ 𝑛 ≠ 0s
) |
58 | 53, 55, 57 | divscld 28135 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) ∧ 𝑚 ∈ ℕs)
→ ( 1s /su 𝑛) ∈ No
) |
59 | 51, 58 | nncansd 28016 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) ∧ 𝑚 ∈ ℕs)
→ (𝐴 -s
(𝐴 -s (
1s /su 𝑛))) = ( 1s /su
𝑛)) |
60 | | simpllr 775 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) ∧ 𝑚 ∈ ℕs)
→ 𝐵 ∈ No ) |
61 | | nnsno 28209 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 ∈ ℕs
→ 𝑚 ∈ No ) |
62 | 61 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) ∧ 𝑚 ∈ ℕs)
→ 𝑚 ∈ No ) |
63 | | nnne0s 28218 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 ∈ ℕs
→ 𝑚 ≠ 0s
) |
64 | 63 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) ∧ 𝑚 ∈ ℕs)
→ 𝑚 ≠ 0s
) |
65 | 53, 62, 64 | divscld 28135 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) ∧ 𝑚 ∈ ℕs)
→ ( 1s /su 𝑚) ∈ No
) |
66 | 60, 65 | nncansd 28016 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) ∧ 𝑚 ∈ ℕs)
→ (𝐵 -s
(𝐵 -s (
1s /su 𝑚))) = ( 1s /su
𝑚)) |
67 | 59, 66 | oveq12d 7438 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) ∧ 𝑚 ∈ ℕs)
→ ((𝐴 -s
(𝐴 -s (
1s /su 𝑛))) ·s (𝐵 -s (𝐵 -s ( 1s
/su 𝑚)))) =
(( 1s /su 𝑛) ·s ( 1s
/su 𝑚))) |
68 | 67 | oveq2d 7436 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) ∧ 𝑚 ∈ ℕs)
→ ((𝐴
·s 𝐵)
-s ((𝐴
-s (𝐴
-s ( 1s /su 𝑛))) ·s (𝐵 -s (𝐵 -s ( 1s
/su 𝑚))))) =
((𝐴 ·s
𝐵) -s ((
1s /su 𝑛) ·s ( 1s
/su 𝑚)))) |
69 | 68 | eqeq2d 2739 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) ∧ 𝑚 ∈ ℕs)
→ (𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝐵
-s (𝐵
-s ( 1s /su 𝑚))))) ↔ 𝑧 = ((𝐴 ·s 𝐵) -s (( 1s
/su 𝑛)
·s ( 1s /su 𝑚))))) |
70 | 50, 69 | bitrid 283 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) ∧ 𝑚 ∈ ℕs)
→ (∃𝑢(𝑢 = (𝐵 -s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝐵
-s 𝑢)))) ↔
𝑧 = ((𝐴 ·s 𝐵) -s (( 1s
/su 𝑛)
·s ( 1s /su 𝑚))))) |
71 | 70 | rexbidva 3173 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) →
(∃𝑚 ∈
ℕs ∃𝑢(𝑢 = (𝐵 -s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝐵
-s 𝑢)))) ↔
∃𝑚 ∈
ℕs 𝑧 =
((𝐴 ·s
𝐵) -s ((
1s /su 𝑛) ·s ( 1s
/su 𝑚))))) |
72 | 44, 71 | bitrid 283 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) →
(∃𝑡(𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑡) ·s (𝐵 -s 𝑢)))) ↔ ∃𝑚 ∈ ℕs 𝑧 = ((𝐴 ·s 𝐵) -s (( 1s
/su 𝑛)
·s ( 1s /su 𝑚))))) |
73 | 72 | rexbidva 3173 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑛 ∈ ℕs ∃𝑡(𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑡) ·s (𝐵 -s 𝑢)))) ↔ ∃𝑛 ∈ ℕs ∃𝑚 ∈ ℕs
𝑧 = ((𝐴 ·s 𝐵) -s (( 1s
/su 𝑛)
·s ( 1s /su 𝑚))))) |
74 | | remulscllem1 28241 |
. . . . . . . . . . . . 13
⊢
(∃𝑛 ∈
ℕs ∃𝑚 ∈ ℕs 𝑧 = ((𝐴 ·s 𝐵) -s (( 1s
/su 𝑛)
·s ( 1s /su 𝑚))) ↔ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 ·s 𝐵) -s ( 1s
/su 𝑝))) |
75 | 73, 74 | bitrdi 287 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑛 ∈ ℕs ∃𝑡(𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑡) ·s (𝐵 -s 𝑢)))) ↔ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 ·s 𝐵) -s ( 1s
/su 𝑝)))) |
76 | 29, 75 | bitrid 283 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑡) ·s (𝐵 -s 𝑢))) ↔ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 ·s 𝐵) -s ( 1s
/su 𝑝)))) |
77 | 76 | abbidv 2797 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → {𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑡) ·s (𝐵 -s 𝑢)))} = {𝑧 ∣ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 ·s 𝐵) -s ( 1s
/su 𝑝))}) |
78 | | r19.41v 3185 |
. . . . . . . . . . . . . 14
⊢
(∃𝑛 ∈
ℕs (𝑡 =
(𝐴 +s (
1s /su 𝑛)) ∧ ∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝑡 -s 𝐴) ·s (𝑢 -s 𝐵)))) ↔ (∃𝑛 ∈ ℕs 𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝑡 -s 𝐴) ·s (𝑢 -s 𝐵))))) |
79 | 78 | exbii 1843 |
. . . . . . . . . . . . 13
⊢
(∃𝑡∃𝑛 ∈ ℕs (𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝑡 -s 𝐴) ·s (𝑢 -s 𝐵)))) ↔ ∃𝑡(∃𝑛 ∈ ℕs 𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝑡 -s 𝐴) ·s (𝑢 -s 𝐵))))) |
80 | | rexcom4 3282 |
. . . . . . . . . . . . 13
⊢
(∃𝑛 ∈
ℕs ∃𝑡(𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝑡 -s 𝐴) ·s (𝑢 -s 𝐵)))) ↔ ∃𝑡∃𝑛 ∈ ℕs (𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝑡 -s 𝐴) ·s (𝑢 -s 𝐵))))) |
81 | | eqeq1 2732 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑡 → (𝑥 = (𝐴 +s ( 1s
/su 𝑛))
↔ 𝑡 = (𝐴 +s ( 1s
/su 𝑛)))) |
82 | 81 | rexbidv 3175 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑡 → (∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))
↔ ∃𝑛 ∈
ℕs 𝑡 =
(𝐴 +s (
1s /su 𝑛)))) |
83 | 82 | rexab 3689 |
. . . . . . . . . . . . 13
⊢
(∃𝑡 ∈
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝑡 -s 𝐴) ·s (𝑢 -s 𝐵))) ↔ ∃𝑡(∃𝑛 ∈ ℕs 𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝑡 -s 𝐴) ·s (𝑢 -s 𝐵))))) |
84 | 79, 80, 83 | 3bitr4ri 304 |
. . . . . . . . . . . 12
⊢
(∃𝑡 ∈
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝑡 -s 𝐴) ·s (𝑢 -s 𝐵))) ↔ ∃𝑛 ∈ ℕs ∃𝑡(𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝑡 -s 𝐴) ·s (𝑢 -s 𝐵))))) |
85 | | ovex 7453 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 +s ( 1s
/su 𝑛))
∈ V |
86 | | oveq1 7427 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = (𝐴 +s ( 1s
/su 𝑛))
→ (𝑡 -s
𝐴) = ((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)) |
87 | 86 | oveq1d 7435 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = (𝐴 +s ( 1s
/su 𝑛))
→ ((𝑡 -s
𝐴) ·s
(𝑢 -s 𝐵)) = (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝑢
-s 𝐵))) |
88 | 87 | oveq2d 7436 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = (𝐴 +s ( 1s
/su 𝑛))
→ ((𝐴
·s 𝐵)
-s ((𝑡
-s 𝐴)
·s (𝑢
-s 𝐵))) =
((𝐴 ·s
𝐵) -s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝑢
-s 𝐵)))) |
89 | 88 | eqeq2d 2739 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = (𝐴 +s ( 1s
/su 𝑛))
→ (𝑧 = ((𝐴 ·s 𝐵) -s ((𝑡 -s 𝐴) ·s (𝑢 -s 𝐵))) ↔ 𝑧 = ((𝐴 ·s 𝐵) -s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝑢
-s 𝐵))))) |
90 | 89 | rexbidv 3175 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (𝐴 +s ( 1s
/su 𝑛))
→ (∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝑡 -s 𝐴) ·s (𝑢 -s 𝐵))) ↔ ∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝑢
-s 𝐵))))) |
91 | 85, 90 | ceqsexv 3523 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑡(𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝑡 -s 𝐴) ·s (𝑢 -s 𝐵)))) ↔ ∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝑢
-s 𝐵)))) |
92 | | r19.41v 3185 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑚 ∈
ℕs (𝑢 =
(𝐵 +s (
1s /su 𝑚)) ∧ 𝑧 = ((𝐴 ·s 𝐵) -s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝑢
-s 𝐵)))) ↔
(∃𝑚 ∈
ℕs 𝑢 =
(𝐵 +s (
1s /su 𝑚)) ∧ 𝑧 = ((𝐴 ·s 𝐵) -s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝑢
-s 𝐵))))) |
93 | 92 | exbii 1843 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑢∃𝑚 ∈ ℕs (𝑢 = (𝐵 +s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) -s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝑢
-s 𝐵)))) ↔
∃𝑢(∃𝑚 ∈ ℕs
𝑢 = (𝐵 +s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) -s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝑢
-s 𝐵))))) |
94 | | rexcom4 3282 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑚 ∈
ℕs ∃𝑢(𝑢 = (𝐵 +s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) -s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝑢
-s 𝐵)))) ↔
∃𝑢∃𝑚 ∈ ℕs
(𝑢 = (𝐵 +s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) -s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝑢
-s 𝐵))))) |
95 | | eqeq1 2732 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑢 → (𝑦 = (𝐵 +s ( 1s
/su 𝑚))
↔ 𝑢 = (𝐵 +s ( 1s
/su 𝑚)))) |
96 | 95 | rexbidv 3175 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑢 → (∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))
↔ ∃𝑚 ∈
ℕs 𝑢 =
(𝐵 +s (
1s /su 𝑚)))) |
97 | 96 | rexab 3689 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝑢
-s 𝐵))) ↔
∃𝑢(∃𝑚 ∈ ℕs
𝑢 = (𝐵 +s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) -s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝑢
-s 𝐵))))) |
98 | 93, 94, 97 | 3bitr4ri 304 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝑢
-s 𝐵))) ↔
∃𝑚 ∈
ℕs ∃𝑢(𝑢 = (𝐵 +s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) -s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝑢
-s 𝐵))))) |
99 | 91, 98 | bitri 275 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑡(𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝑡 -s 𝐴) ·s (𝑢 -s 𝐵)))) ↔ ∃𝑚 ∈ ℕs ∃𝑢(𝑢 = (𝐵 +s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) -s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝑢
-s 𝐵))))) |
100 | | ovex 7453 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐵 +s ( 1s
/su 𝑚))
∈ V |
101 | | oveq1 7427 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 = (𝐵 +s ( 1s
/su 𝑚))
→ (𝑢 -s
𝐵) = ((𝐵 +s ( 1s
/su 𝑚))
-s 𝐵)) |
102 | 101 | oveq2d 7436 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 = (𝐵 +s ( 1s
/su 𝑚))
→ (((𝐴 +s (
1s /su 𝑛)) -s 𝐴) ·s (𝑢 -s 𝐵)) = (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s ((𝐵
+s ( 1s /su 𝑚)) -s 𝐵))) |
103 | 102 | oveq2d 7436 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = (𝐵 +s ( 1s
/su 𝑚))
→ ((𝐴
·s 𝐵)
-s (((𝐴
+s ( 1s /su 𝑛)) -s 𝐴) ·s (𝑢 -s 𝐵))) = ((𝐴 ·s 𝐵) -s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s ((𝐵
+s ( 1s /su 𝑚)) -s 𝐵)))) |
104 | 103 | eqeq2d 2739 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = (𝐵 +s ( 1s
/su 𝑚))
→ (𝑧 = ((𝐴 ·s 𝐵) -s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝑢
-s 𝐵))) ↔
𝑧 = ((𝐴 ·s 𝐵) -s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s ((𝐵
+s ( 1s /su 𝑚)) -s 𝐵))))) |
105 | 100, 104 | ceqsexv 3523 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑢(𝑢 = (𝐵 +s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) -s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝑢
-s 𝐵)))) ↔
𝑧 = ((𝐴 ·s 𝐵) -s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s ((𝐵
+s ( 1s /su 𝑚)) -s 𝐵)))) |
106 | | pncan2s 27995 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈
No ∧ ( 1s /su 𝑛) ∈ No )
→ ((𝐴 +s (
1s /su 𝑛)) -s 𝐴) = ( 1s /su 𝑛)) |
107 | 51, 58, 106 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) ∧ 𝑚 ∈ ℕs)
→ ((𝐴 +s (
1s /su 𝑛)) -s 𝐴) = ( 1s /su 𝑛)) |
108 | | pncan2s 27995 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐵 ∈
No ∧ ( 1s /su 𝑚) ∈ No )
→ ((𝐵 +s (
1s /su 𝑚)) -s 𝐵) = ( 1s /su 𝑚)) |
109 | 60, 65, 108 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) ∧ 𝑚 ∈ ℕs)
→ ((𝐵 +s (
1s /su 𝑚)) -s 𝐵) = ( 1s /su 𝑚)) |
110 | 107, 109 | oveq12d 7438 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) ∧ 𝑚 ∈ ℕs)
→ (((𝐴 +s (
1s /su 𝑛)) -s 𝐴) ·s ((𝐵 +s ( 1s
/su 𝑚))
-s 𝐵)) = ((
1s /su 𝑛) ·s ( 1s
/su 𝑚))) |
111 | 110 | oveq2d 7436 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) ∧ 𝑚 ∈ ℕs)
→ ((𝐴
·s 𝐵)
-s (((𝐴
+s ( 1s /su 𝑛)) -s 𝐴) ·s ((𝐵 +s ( 1s
/su 𝑚))
-s 𝐵))) =
((𝐴 ·s
𝐵) -s ((
1s /su 𝑛) ·s ( 1s
/su 𝑚)))) |
112 | 111 | eqeq2d 2739 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) ∧ 𝑚 ∈ ℕs)
→ (𝑧 = ((𝐴 ·s 𝐵) -s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s ((𝐵
+s ( 1s /su 𝑚)) -s 𝐵))) ↔ 𝑧 = ((𝐴 ·s 𝐵) -s (( 1s
/su 𝑛)
·s ( 1s /su 𝑚))))) |
113 | 105, 112 | bitrid 283 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) ∧ 𝑚 ∈ ℕs)
→ (∃𝑢(𝑢 = (𝐵 +s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) -s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝑢
-s 𝐵)))) ↔
𝑧 = ((𝐴 ·s 𝐵) -s (( 1s
/su 𝑛)
·s ( 1s /su 𝑚))))) |
114 | 113 | rexbidva 3173 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) →
(∃𝑚 ∈
ℕs ∃𝑢(𝑢 = (𝐵 +s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) -s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝑢
-s 𝐵)))) ↔
∃𝑚 ∈
ℕs 𝑧 =
((𝐴 ·s
𝐵) -s ((
1s /su 𝑛) ·s ( 1s
/su 𝑚))))) |
115 | 99, 114 | bitrid 283 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) →
(∃𝑡(𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝑡 -s 𝐴) ·s (𝑢 -s 𝐵)))) ↔ ∃𝑚 ∈ ℕs 𝑧 = ((𝐴 ·s 𝐵) -s (( 1s
/su 𝑛)
·s ( 1s /su 𝑚))))) |
116 | 115 | rexbidva 3173 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑛 ∈ ℕs ∃𝑡(𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝑡 -s 𝐴) ·s (𝑢 -s 𝐵)))) ↔ ∃𝑛 ∈ ℕs ∃𝑚 ∈ ℕs
𝑧 = ((𝐴 ·s 𝐵) -s (( 1s
/su 𝑛)
·s ( 1s /su 𝑚))))) |
117 | 116, 74 | bitrdi 287 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑛 ∈ ℕs ∃𝑡(𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝑡 -s 𝐴) ·s (𝑢 -s 𝐵)))) ↔ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 ·s 𝐵) -s ( 1s
/su 𝑝)))) |
118 | 84, 117 | bitrid 283 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝑡 -s 𝐴) ·s (𝑢 -s 𝐵))) ↔ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 ·s 𝐵) -s ( 1s
/su 𝑝)))) |
119 | 118 | abbidv 2797 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → {𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝑡 -s 𝐴) ·s (𝑢 -s 𝐵)))} = {𝑧 ∣ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 ·s 𝐵) -s ( 1s
/su 𝑝))}) |
120 | 77, 119 | uneq12d 4163 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ({𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑡) ·s (𝐵 -s 𝑢)))} ∪ {𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝑡 -s 𝐴) ·s (𝑢 -s 𝐵)))}) = ({𝑧 ∣ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 ·s 𝐵) -s ( 1s
/su 𝑝))}
∪ {𝑧 ∣
∃𝑝 ∈
ℕs 𝑧 =
((𝐴 ·s
𝐵) -s (
1s /su 𝑝))})) |
121 | | unidm 4151 |
. . . . . . . . 9
⊢ ({𝑧 ∣ ∃𝑝 ∈ ℕs
𝑧 = ((𝐴 ·s 𝐵) -s ( 1s
/su 𝑝))}
∪ {𝑧 ∣
∃𝑝 ∈
ℕs 𝑧 =
((𝐴 ·s
𝐵) -s (
1s /su 𝑝))}) = {𝑧 ∣ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 ·s 𝐵) -s ( 1s
/su 𝑝))} |
122 | 120, 121 | eqtrdi 2784 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ({𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑡) ·s (𝐵 -s 𝑢)))} ∪ {𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝑡 -s 𝐴) ·s (𝑢 -s 𝐵)))}) = {𝑧 ∣ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 ·s 𝐵) -s ( 1s
/su 𝑝))}) |
123 | | r19.41v 3185 |
. . . . . . . . . . . . . 14
⊢
(∃𝑛 ∈
ℕs (𝑡 =
(𝐴 -s (
1s /su 𝑛)) ∧ ∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)))) ↔ (∃𝑛 ∈ ℕs 𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵))))) |
124 | 123 | exbii 1843 |
. . . . . . . . . . . . 13
⊢
(∃𝑡∃𝑛 ∈ ℕs (𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)))) ↔ ∃𝑡(∃𝑛 ∈ ℕs 𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵))))) |
125 | | rexcom4 3282 |
. . . . . . . . . . . . 13
⊢
(∃𝑛 ∈
ℕs ∃𝑡(𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)))) ↔ ∃𝑡∃𝑛 ∈ ℕs (𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵))))) |
126 | 27 | rexab 3689 |
. . . . . . . . . . . . 13
⊢
(∃𝑡 ∈
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 -s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵))) ↔ ∃𝑡(∃𝑛 ∈ ℕs 𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵))))) |
127 | 124, 125,
126 | 3bitr4ri 304 |
. . . . . . . . . . . 12
⊢
(∃𝑡 ∈
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 -s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵))) ↔ ∃𝑛 ∈ ℕs ∃𝑡(𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵))))) |
128 | 31 | oveq1d 7435 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = (𝐴 -s ( 1s
/su 𝑛))
→ ((𝐴 -s
𝑡) ·s
(𝑢 -s 𝐵)) = ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝑢
-s 𝐵))) |
129 | 128 | oveq2d 7436 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = (𝐴 -s ( 1s
/su 𝑛))
→ ((𝐴
·s 𝐵)
+s ((𝐴
-s 𝑡)
·s (𝑢
-s 𝐵))) =
((𝐴 ·s
𝐵) +s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝑢
-s 𝐵)))) |
130 | 129 | eqeq2d 2739 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = (𝐴 -s ( 1s
/su 𝑛))
→ (𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵))) ↔ 𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝑢
-s 𝐵))))) |
131 | 130 | rexbidv 3175 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (𝐴 -s ( 1s
/su 𝑛))
→ (∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵))) ↔ ∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝑢
-s 𝐵))))) |
132 | 30, 131 | ceqsexv 3523 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑡(𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)))) ↔ ∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝑢
-s 𝐵)))) |
133 | | r19.41v 3185 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑚 ∈
ℕs (𝑢 =
(𝐵 +s (
1s /su 𝑚)) ∧ 𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝑢
-s 𝐵)))) ↔
(∃𝑚 ∈
ℕs 𝑢 =
(𝐵 +s (
1s /su 𝑚)) ∧ 𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝑢
-s 𝐵))))) |
134 | 133 | exbii 1843 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑢∃𝑚 ∈ ℕs (𝑢 = (𝐵 +s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝑢
-s 𝐵)))) ↔
∃𝑢(∃𝑚 ∈ ℕs
𝑢 = (𝐵 +s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝑢
-s 𝐵))))) |
135 | | rexcom4 3282 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑚 ∈
ℕs ∃𝑢(𝑢 = (𝐵 +s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝑢
-s 𝐵)))) ↔
∃𝑢∃𝑚 ∈ ℕs
(𝑢 = (𝐵 +s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝑢
-s 𝐵))))) |
136 | 96 | rexab 3689 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝑢
-s 𝐵))) ↔
∃𝑢(∃𝑚 ∈ ℕs
𝑢 = (𝐵 +s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝑢
-s 𝐵))))) |
137 | 134, 135,
136 | 3bitr4ri 304 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝑢
-s 𝐵))) ↔
∃𝑚 ∈
ℕs ∃𝑢(𝑢 = (𝐵 +s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝑢
-s 𝐵))))) |
138 | 132, 137 | bitri 275 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑡(𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)))) ↔ ∃𝑚 ∈ ℕs ∃𝑢(𝑢 = (𝐵 +s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝑢
-s 𝐵))))) |
139 | 101 | oveq2d 7436 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 = (𝐵 +s ( 1s
/su 𝑚))
→ ((𝐴 -s
(𝐴 -s (
1s /su 𝑛))) ·s (𝑢 -s 𝐵)) = ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s ((𝐵
+s ( 1s /su 𝑚)) -s 𝐵))) |
140 | 139 | oveq2d 7436 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = (𝐵 +s ( 1s
/su 𝑚))
→ ((𝐴
·s 𝐵)
+s ((𝐴
-s (𝐴
-s ( 1s /su 𝑛))) ·s (𝑢 -s 𝐵))) = ((𝐴 ·s 𝐵) +s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s ((𝐵
+s ( 1s /su 𝑚)) -s 𝐵)))) |
141 | 140 | eqeq2d 2739 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = (𝐵 +s ( 1s
/su 𝑚))
→ (𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝑢
-s 𝐵))) ↔
𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s ((𝐵
+s ( 1s /su 𝑚)) -s 𝐵))))) |
142 | 100, 141 | ceqsexv 3523 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑢(𝑢 = (𝐵 +s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝑢
-s 𝐵)))) ↔
𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s ((𝐵
+s ( 1s /su 𝑚)) -s 𝐵)))) |
143 | 59, 109 | oveq12d 7438 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) ∧ 𝑚 ∈ ℕs)
→ ((𝐴 -s
(𝐴 -s (
1s /su 𝑛))) ·s ((𝐵 +s ( 1s
/su 𝑚))
-s 𝐵)) = ((
1s /su 𝑛) ·s ( 1s
/su 𝑚))) |
144 | 143 | oveq2d 7436 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) ∧ 𝑚 ∈ ℕs)
→ ((𝐴
·s 𝐵)
+s ((𝐴
-s (𝐴
-s ( 1s /su 𝑛))) ·s ((𝐵 +s ( 1s
/su 𝑚))
-s 𝐵))) =
((𝐴 ·s
𝐵) +s ((
1s /su 𝑛) ·s ( 1s
/su 𝑚)))) |
145 | 144 | eqeq2d 2739 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) ∧ 𝑚 ∈ ℕs)
→ (𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s ((𝐵
+s ( 1s /su 𝑚)) -s 𝐵))) ↔ 𝑧 = ((𝐴 ·s 𝐵) +s (( 1s
/su 𝑛)
·s ( 1s /su 𝑚))))) |
146 | 142, 145 | bitrid 283 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) ∧ 𝑚 ∈ ℕs)
→ (∃𝑢(𝑢 = (𝐵 +s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝑢
-s 𝐵)))) ↔
𝑧 = ((𝐴 ·s 𝐵) +s (( 1s
/su 𝑛)
·s ( 1s /su 𝑚))))) |
147 | 146 | rexbidva 3173 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) →
(∃𝑚 ∈
ℕs ∃𝑢(𝑢 = (𝐵 +s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s (𝐴 -s ( 1s
/su 𝑛)))
·s (𝑢
-s 𝐵)))) ↔
∃𝑚 ∈
ℕs 𝑧 =
((𝐴 ·s
𝐵) +s ((
1s /su 𝑛) ·s ( 1s
/su 𝑚))))) |
148 | 138, 147 | bitrid 283 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) →
(∃𝑡(𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)))) ↔ ∃𝑚 ∈ ℕs 𝑧 = ((𝐴 ·s 𝐵) +s (( 1s
/su 𝑛)
·s ( 1s /su 𝑚))))) |
149 | 148 | rexbidva 3173 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑛 ∈ ℕs ∃𝑡(𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)))) ↔ ∃𝑛 ∈ ℕs ∃𝑚 ∈ ℕs
𝑧 = ((𝐴 ·s 𝐵) +s (( 1s
/su 𝑛)
·s ( 1s /su 𝑚))))) |
150 | | remulscllem1 28241 |
. . . . . . . . . . . . 13
⊢
(∃𝑛 ∈
ℕs ∃𝑚 ∈ ℕs 𝑧 = ((𝐴 ·s 𝐵) +s (( 1s
/su 𝑛)
·s ( 1s /su 𝑚))) ↔ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 ·s 𝐵) +s ( 1s
/su 𝑝))) |
151 | 149, 150 | bitrdi 287 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑛 ∈ ℕs ∃𝑡(𝑡 = (𝐴 -s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)))) ↔ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 ·s 𝐵) +s ( 1s
/su 𝑝)))) |
152 | 127, 151 | bitrid 283 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵))) ↔ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 ·s 𝐵) +s ( 1s
/su 𝑝)))) |
153 | 152 | abbidv 2797 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → {𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)))} = {𝑧 ∣ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 ·s 𝐵) +s ( 1s
/su 𝑝))}) |
154 | | r19.41v 3185 |
. . . . . . . . . . . . . 14
⊢
(∃𝑛 ∈
ℕs (𝑡 =
(𝐴 +s (
1s /su 𝑛)) ∧ ∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝑡 -s 𝐴) ·s (𝐵 -s 𝑢)))) ↔ (∃𝑛 ∈ ℕs 𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝑡 -s 𝐴) ·s (𝐵 -s 𝑢))))) |
155 | 154 | exbii 1843 |
. . . . . . . . . . . . 13
⊢
(∃𝑡∃𝑛 ∈ ℕs (𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝑡 -s 𝐴) ·s (𝐵 -s 𝑢)))) ↔ ∃𝑡(∃𝑛 ∈ ℕs 𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝑡 -s 𝐴) ·s (𝐵 -s 𝑢))))) |
156 | | rexcom4 3282 |
. . . . . . . . . . . . 13
⊢
(∃𝑛 ∈
ℕs ∃𝑡(𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝑡 -s 𝐴) ·s (𝐵 -s 𝑢)))) ↔ ∃𝑡∃𝑛 ∈ ℕs (𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝑡 -s 𝐴) ·s (𝐵 -s 𝑢))))) |
157 | 82 | rexab 3689 |
. . . . . . . . . . . . 13
⊢
(∃𝑡 ∈
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝑡 -s 𝐴) ·s (𝐵 -s 𝑢))) ↔ ∃𝑡(∃𝑛 ∈ ℕs 𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝑡 -s 𝐴) ·s (𝐵 -s 𝑢))))) |
158 | 155, 156,
157 | 3bitr4ri 304 |
. . . . . . . . . . . 12
⊢
(∃𝑡 ∈
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝑡 -s 𝐴) ·s (𝐵 -s 𝑢))) ↔ ∃𝑛 ∈ ℕs ∃𝑡(𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝑡 -s 𝐴) ·s (𝐵 -s 𝑢))))) |
159 | 86 | oveq1d 7435 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = (𝐴 +s ( 1s
/su 𝑛))
→ ((𝑡 -s
𝐴) ·s
(𝐵 -s 𝑢)) = (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝐵
-s 𝑢))) |
160 | 159 | oveq2d 7436 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = (𝐴 +s ( 1s
/su 𝑛))
→ ((𝐴
·s 𝐵)
+s ((𝑡
-s 𝐴)
·s (𝐵
-s 𝑢))) =
((𝐴 ·s
𝐵) +s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝐵
-s 𝑢)))) |
161 | 160 | eqeq2d 2739 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = (𝐴 +s ( 1s
/su 𝑛))
→ (𝑧 = ((𝐴 ·s 𝐵) +s ((𝑡 -s 𝐴) ·s (𝐵 -s 𝑢))) ↔ 𝑧 = ((𝐴 ·s 𝐵) +s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝐵
-s 𝑢))))) |
162 | 161 | rexbidv 3175 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (𝐴 +s ( 1s
/su 𝑛))
→ (∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝑡 -s 𝐴) ·s (𝐵 -s 𝑢))) ↔ ∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝐵
-s 𝑢))))) |
163 | 85, 162 | ceqsexv 3523 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑡(𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝑡 -s 𝐴) ·s (𝐵 -s 𝑢)))) ↔ ∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝐵
-s 𝑢)))) |
164 | | r19.41v 3185 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑚 ∈
ℕs (𝑢 =
(𝐵 -s (
1s /su 𝑚)) ∧ 𝑧 = ((𝐴 ·s 𝐵) +s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝐵
-s 𝑢)))) ↔
(∃𝑚 ∈
ℕs 𝑢 =
(𝐵 -s (
1s /su 𝑚)) ∧ 𝑧 = ((𝐴 ·s 𝐵) +s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝐵
-s 𝑢))))) |
165 | 164 | exbii 1843 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑢∃𝑚 ∈ ℕs (𝑢 = (𝐵 -s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) +s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝐵
-s 𝑢)))) ↔
∃𝑢(∃𝑚 ∈ ℕs
𝑢 = (𝐵 -s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) +s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝐵
-s 𝑢))))) |
166 | | rexcom4 3282 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑚 ∈
ℕs ∃𝑢(𝑢 = (𝐵 -s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) +s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝐵
-s 𝑢)))) ↔
∃𝑢∃𝑚 ∈ ℕs
(𝑢 = (𝐵 -s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) +s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝐵
-s 𝑢))))) |
167 | 41 | rexab 3689 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝐵
-s 𝑢))) ↔
∃𝑢(∃𝑚 ∈ ℕs
𝑢 = (𝐵 -s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) +s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝐵
-s 𝑢))))) |
168 | 165, 166,
167 | 3bitr4ri 304 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝐵
-s 𝑢))) ↔
∃𝑚 ∈
ℕs ∃𝑢(𝑢 = (𝐵 -s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) +s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝐵
-s 𝑢))))) |
169 | 163, 168 | bitri 275 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑡(𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝑡 -s 𝐴) ·s (𝐵 -s 𝑢)))) ↔ ∃𝑚 ∈ ℕs ∃𝑢(𝑢 = (𝐵 -s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) +s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝐵
-s 𝑢))))) |
170 | 46 | oveq2d 7436 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 = (𝐵 -s ( 1s
/su 𝑚))
→ (((𝐴 +s (
1s /su 𝑛)) -s 𝐴) ·s (𝐵 -s 𝑢)) = (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝐵
-s (𝐵
-s ( 1s /su 𝑚))))) |
171 | 170 | oveq2d 7436 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = (𝐵 -s ( 1s
/su 𝑚))
→ ((𝐴
·s 𝐵)
+s (((𝐴
+s ( 1s /su 𝑛)) -s 𝐴) ·s (𝐵 -s 𝑢))) = ((𝐴 ·s 𝐵) +s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝐵
-s (𝐵
-s ( 1s /su 𝑚)))))) |
172 | 171 | eqeq2d 2739 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = (𝐵 -s ( 1s
/su 𝑚))
→ (𝑧 = ((𝐴 ·s 𝐵) +s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝐵
-s 𝑢))) ↔
𝑧 = ((𝐴 ·s 𝐵) +s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝐵
-s (𝐵
-s ( 1s /su 𝑚))))))) |
173 | 45, 172 | ceqsexv 3523 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑢(𝑢 = (𝐵 -s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) +s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝐵
-s 𝑢)))) ↔
𝑧 = ((𝐴 ·s 𝐵) +s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝐵
-s (𝐵
-s ( 1s /su 𝑚)))))) |
174 | 107, 66 | oveq12d 7438 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) ∧ 𝑚 ∈ ℕs)
→ (((𝐴 +s (
1s /su 𝑛)) -s 𝐴) ·s (𝐵 -s (𝐵 -s ( 1s
/su 𝑚)))) =
(( 1s /su 𝑛) ·s ( 1s
/su 𝑚))) |
175 | 174 | oveq2d 7436 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) ∧ 𝑚 ∈ ℕs)
→ ((𝐴
·s 𝐵)
+s (((𝐴
+s ( 1s /su 𝑛)) -s 𝐴) ·s (𝐵 -s (𝐵 -s ( 1s
/su 𝑚))))) =
((𝐴 ·s
𝐵) +s ((
1s /su 𝑛) ·s ( 1s
/su 𝑚)))) |
176 | 175 | eqeq2d 2739 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) ∧ 𝑚 ∈ ℕs)
→ (𝑧 = ((𝐴 ·s 𝐵) +s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝐵
-s (𝐵
-s ( 1s /su 𝑚))))) ↔ 𝑧 = ((𝐴 ·s 𝐵) +s (( 1s
/su 𝑛)
·s ( 1s /su 𝑚))))) |
177 | 173, 176 | bitrid 283 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) ∧ 𝑚 ∈ ℕs)
→ (∃𝑢(𝑢 = (𝐵 -s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) +s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝐵
-s 𝑢)))) ↔
𝑧 = ((𝐴 ·s 𝐵) +s (( 1s
/su 𝑛)
·s ( 1s /su 𝑚))))) |
178 | 177 | rexbidva 3173 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) →
(∃𝑚 ∈
ℕs ∃𝑢(𝑢 = (𝐵 -s ( 1s
/su 𝑚))
∧ 𝑧 = ((𝐴 ·s 𝐵) +s (((𝐴 +s ( 1s
/su 𝑛))
-s 𝐴)
·s (𝐵
-s 𝑢)))) ↔
∃𝑚 ∈
ℕs 𝑧 =
((𝐴 ·s
𝐵) +s ((
1s /su 𝑛) ·s ( 1s
/su 𝑚))))) |
179 | 169, 178 | bitrid 283 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑛 ∈ ℕs) →
(∃𝑡(𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝑡 -s 𝐴) ·s (𝐵 -s 𝑢)))) ↔ ∃𝑚 ∈ ℕs 𝑧 = ((𝐴 ·s 𝐵) +s (( 1s
/su 𝑛)
·s ( 1s /su 𝑚))))) |
180 | 179 | rexbidva 3173 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑛 ∈ ℕs ∃𝑡(𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝑡 -s 𝐴) ·s (𝐵 -s 𝑢)))) ↔ ∃𝑛 ∈ ℕs ∃𝑚 ∈ ℕs
𝑧 = ((𝐴 ·s 𝐵) +s (( 1s
/su 𝑛)
·s ( 1s /su 𝑚))))) |
181 | 180, 150 | bitrdi 287 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑛 ∈ ℕs ∃𝑡(𝑡 = (𝐴 +s ( 1s
/su 𝑛))
∧ ∃𝑢 ∈
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝑡 -s 𝐴) ·s (𝐵 -s 𝑢)))) ↔ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 ·s 𝐵) +s ( 1s
/su 𝑝)))) |
182 | 158, 181 | bitrid 283 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝑡 -s 𝐴) ·s (𝐵 -s 𝑢))) ↔ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 ·s 𝐵) +s ( 1s
/su 𝑝)))) |
183 | 182 | abbidv 2797 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → {𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝑡 -s 𝐴) ·s (𝐵 -s 𝑢)))} = {𝑧 ∣ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 ·s 𝐵) +s ( 1s
/su 𝑝))}) |
184 | 153, 183 | uneq12d 4163 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ({𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)))} ∪ {𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝑡 -s 𝐴) ·s (𝐵 -s 𝑢)))}) = ({𝑧 ∣ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 ·s 𝐵) +s ( 1s
/su 𝑝))}
∪ {𝑧 ∣
∃𝑝 ∈
ℕs 𝑧 =
((𝐴 ·s
𝐵) +s (
1s /su 𝑝))})) |
185 | | unidm 4151 |
. . . . . . . . 9
⊢ ({𝑧 ∣ ∃𝑝 ∈ ℕs
𝑧 = ((𝐴 ·s 𝐵) +s ( 1s
/su 𝑝))}
∪ {𝑧 ∣
∃𝑝 ∈
ℕs 𝑧 =
((𝐴 ·s
𝐵) +s (
1s /su 𝑝))}) = {𝑧 ∣ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 ·s 𝐵) +s ( 1s
/su 𝑝))} |
186 | 184, 185 | eqtrdi 2784 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ({𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)))} ∪ {𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝑡 -s 𝐴) ·s (𝐵 -s 𝑢)))}) = {𝑧 ∣ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 ·s 𝐵) +s ( 1s
/su 𝑝))}) |
187 | 122, 186 | oveq12d 7438 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (({𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑡) ·s (𝐵 -s 𝑢)))} ∪ {𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝑡 -s 𝐴) ·s (𝑢 -s 𝐵)))}) |s ({𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)))} ∪ {𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝑡 -s 𝐴) ·s (𝐵 -s 𝑢)))})) = ({𝑧 ∣ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 ·s 𝐵) -s ( 1s
/su 𝑝))} |s
{𝑧 ∣ ∃𝑝 ∈ ℕs
𝑧 = ((𝐴 ·s 𝐵) +s ( 1s
/su 𝑝))})) |
188 | 187 | 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 ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝐴 -s 𝑡) ·s (𝐵 -s 𝑢)))} ∪ {𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) -s ((𝑡 -s 𝐴) ·s (𝑢 -s 𝐵)))}) |s ({𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 +s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝐴 -s 𝑡) ·s (𝑢 -s 𝐵)))} ∪ {𝑧 ∣ ∃𝑡 ∈ {𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 +s ( 1s
/su 𝑛))}∃𝑢 ∈ {𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))}𝑧 = ((𝐴 ·s 𝐵) +s ((𝑡 -s 𝐴) ·s (𝐵 -s 𝑢)))})) = ({𝑧 ∣ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 ·s 𝐵) -s ( 1s
/su 𝑝))} |s
{𝑧 ∣ ∃𝑝 ∈ ℕs
𝑧 = ((𝐴 ·s 𝐵) +s ( 1s
/su 𝑝))})) |
189 | 22, 188 | eqtrd 2768 |
. . . . 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 𝑝))})) |
190 | 14, 189 | 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 𝑝))})) |
191 | 2, 11, 190 | 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 𝑝))})))) |
192 | 191 | an4s 659 |
. 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 𝑝))})))) |
193 | | elreno 28236 |
. . 3
⊢ (𝐴 ∈ ℝs
↔ (𝐴 ∈ No ∧ (∃𝑛 ∈ ℕs (( -us
‘𝑛) <s 𝐴 ∧ 𝐴 <s 𝑛) ∧ 𝐴 = ({𝑥 ∣ ∃𝑛 ∈ ℕs 𝑥 = (𝐴 -s ( 1s
/su 𝑛))} |s
{𝑥 ∣ ∃𝑛 ∈ ℕs
𝑥 = (𝐴 +s ( 1s
/su 𝑛))})))) |
194 | | elreno 28236 |
. . 3
⊢ (𝐵 ∈ ℝs
↔ (𝐵 ∈ No ∧ (∃𝑚 ∈ ℕs (( -us
‘𝑚) <s 𝐵 ∧ 𝐵 <s 𝑚) ∧ 𝐵 = ({𝑦 ∣ ∃𝑚 ∈ ℕs 𝑦 = (𝐵 -s ( 1s
/su 𝑚))} |s
{𝑦 ∣ ∃𝑚 ∈ ℕs
𝑦 = (𝐵 +s ( 1s
/su 𝑚))})))) |
195 | 193, 194 | anbi12i 627 |
. 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 𝑚))}))))) |
196 | | elreno 28236 |
. 2
⊢ ((𝐴 ·s 𝐵) ∈ ℝs
↔ ((𝐴
·s 𝐵)
∈ No ∧ (∃𝑝 ∈ ℕs (( -us
‘𝑝) <s (𝐴 ·s 𝐵) ∧ (𝐴 ·s 𝐵) <s 𝑝) ∧ (𝐴 ·s 𝐵) = ({𝑧 ∣ ∃𝑝 ∈ ℕs 𝑧 = ((𝐴 ·s 𝐵) -s ( 1s
/su 𝑝))} |s
{𝑧 ∣ ∃𝑝 ∈ ℕs
𝑧 = ((𝐴 ·s 𝐵) +s ( 1s
/su 𝑝))})))) |
197 | 192, 195,
196 | 3imtr4i 292 |
1
⊢ ((𝐴 ∈ ℝs
∧ 𝐵 ∈
ℝs) → (𝐴 ·s 𝐵) ∈
ℝs) |