Proof of Theorem mulscan2d
Step | Hyp | Ref
| Expression |
1 | | mulscan2d.3 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ No
) |
2 | | 0sno 27256 |
. . . . 5
⊢
0s ∈ No |
3 | | sltneg 27448 |
. . . . 5
⊢ ((𝐶 ∈
No ∧ 0s ∈ No ) →
(𝐶 <s 0s
↔ ( -us ‘ 0s ) <s ( -us
‘𝐶))) |
4 | 1, 2, 3 | sylancl 586 |
. . . 4
⊢ (𝜑 → (𝐶 <s 0s ↔ ( -us
‘ 0s ) <s ( -us ‘𝐶))) |
5 | | negs0s 27430 |
. . . . 5
⊢ (
-us ‘ 0s ) = 0s |
6 | 5 | breq1i 5149 |
. . . 4
⊢ ((
-us ‘ 0s ) <s ( -us ‘𝐶) ↔ 0s <s (
-us ‘𝐶)) |
7 | 4, 6 | bitrdi 286 |
. . 3
⊢ (𝜑 → (𝐶 <s 0s ↔ 0s
<s ( -us ‘𝐶))) |
8 | | mulscan2d.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ No
) |
9 | 8, 1 | mulnegs2d 27545 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ·s ( -us
‘𝐶)) = (
-us ‘(𝐴
·s 𝐶))) |
10 | | mulscan2d.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ No
) |
11 | 10, 1 | mulnegs2d 27545 |
. . . . . . 7
⊢ (𝜑 → (𝐵 ·s ( -us
‘𝐶)) = (
-us ‘(𝐵
·s 𝐶))) |
12 | 9, 11 | eqeq12d 2748 |
. . . . . 6
⊢ (𝜑 → ((𝐴 ·s ( -us
‘𝐶)) = (𝐵 ·s (
-us ‘𝐶))
↔ ( -us ‘(𝐴 ·s 𝐶)) = ( -us ‘(𝐵 ·s 𝐶)))) |
13 | 8, 1 | mulscld 27520 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ·s 𝐶) ∈ No
) |
14 | 10, 1 | mulscld 27520 |
. . . . . . 7
⊢ (𝜑 → (𝐵 ·s 𝐶) ∈ No
) |
15 | | negs11 27452 |
. . . . . . 7
⊢ (((𝐴 ·s 𝐶) ∈
No ∧ (𝐵
·s 𝐶)
∈ No ) → (( -us
‘(𝐴
·s 𝐶)) =
( -us ‘(𝐵
·s 𝐶))
↔ (𝐴
·s 𝐶) =
(𝐵 ·s
𝐶))) |
16 | 13, 14, 15 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (( -us
‘(𝐴
·s 𝐶)) =
( -us ‘(𝐵
·s 𝐶))
↔ (𝐴
·s 𝐶) =
(𝐵 ·s
𝐶))) |
17 | 12, 16 | bitrd 278 |
. . . . 5
⊢ (𝜑 → ((𝐴 ·s ( -us
‘𝐶)) = (𝐵 ·s (
-us ‘𝐶))
↔ (𝐴
·s 𝐶) =
(𝐵 ·s
𝐶))) |
18 | 17 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 0s <s (
-us ‘𝐶))
→ ((𝐴
·s ( -us ‘𝐶)) = (𝐵 ·s ( -us
‘𝐶)) ↔ (𝐴 ·s 𝐶) = (𝐵 ·s 𝐶))) |
19 | 8 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 0s <s (
-us ‘𝐶))
→ 𝐴 ∈ No ) |
20 | 10 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 0s <s (
-us ‘𝐶))
→ 𝐵 ∈ No ) |
21 | 1 | negscld 27440 |
. . . . . 6
⊢ (𝜑 → ( -us
‘𝐶) ∈ No ) |
22 | 21 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 0s <s (
-us ‘𝐶))
→ ( -us ‘𝐶) ∈ No
) |
23 | | simpr 485 |
. . . . 5
⊢ ((𝜑 ∧ 0s <s (
-us ‘𝐶))
→ 0s <s ( -us ‘𝐶)) |
24 | 19, 20, 22, 23 | mulscan2dlem 27559 |
. . . 4
⊢ ((𝜑 ∧ 0s <s (
-us ‘𝐶))
→ ((𝐴
·s ( -us ‘𝐶)) = (𝐵 ·s ( -us
‘𝐶)) ↔ 𝐴 = 𝐵)) |
25 | 18, 24 | bitr3d 280 |
. . 3
⊢ ((𝜑 ∧ 0s <s (
-us ‘𝐶))
→ ((𝐴
·s 𝐶) =
(𝐵 ·s
𝐶) ↔ 𝐴 = 𝐵)) |
26 | 7, 25 | sylbida 592 |
. 2
⊢ ((𝜑 ∧ 𝐶 <s 0s ) → ((𝐴 ·s 𝐶) = (𝐵 ·s 𝐶) ↔ 𝐴 = 𝐵)) |
27 | 8 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 0s <s 𝐶) → 𝐴 ∈ No
) |
28 | 10 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 0s <s 𝐶) → 𝐵 ∈ No
) |
29 | 1 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 0s <s 𝐶) → 𝐶 ∈ No
) |
30 | | simpr 485 |
. . 3
⊢ ((𝜑 ∧ 0s <s 𝐶) → 0s <s
𝐶) |
31 | 27, 28, 29, 30 | mulscan2dlem 27559 |
. 2
⊢ ((𝜑 ∧ 0s <s 𝐶) → ((𝐴 ·s 𝐶) = (𝐵 ·s 𝐶) ↔ 𝐴 = 𝐵)) |
32 | | mulscan2d.4 |
. . 3
⊢ (𝜑 → 𝐶 ≠ 0s ) |
33 | | slttrine 27183 |
. . . 4
⊢ ((𝐶 ∈
No ∧ 0s ∈ No ) →
(𝐶 ≠ 0s
↔ (𝐶 <s
0s ∨ 0s <s 𝐶))) |
34 | 1, 2, 33 | sylancl 586 |
. . 3
⊢ (𝜑 → (𝐶 ≠ 0s ↔ (𝐶 <s 0s ∨
0s <s 𝐶))) |
35 | 32, 34 | mpbid 231 |
. 2
⊢ (𝜑 → (𝐶 <s 0s ∨ 0s
<s 𝐶)) |
36 | 26, 31, 35 | mpjaodan 957 |
1
⊢ (𝜑 → ((𝐴 ·s 𝐶) = (𝐵 ·s 𝐶) ↔ 𝐴 = 𝐵)) |