Proof of Theorem negsproplem7
Step | Hyp | Ref
| Expression |
1 | | bdayelon 27067 |
. . . 4
⊢ ( bday ‘𝐴) ∈ On |
2 | 1 | onordi 6425 |
. . 3
⊢ Ord
( bday ‘𝐴) |
3 | | bdayelon 27067 |
. . . 4
⊢ ( bday ‘𝐵) ∈ On |
4 | 3 | onordi 6425 |
. . 3
⊢ Ord
( bday ‘𝐵) |
5 | | ordtri3or 6347 |
. . 3
⊢ ((Ord
( bday ‘𝐴) ∧ Ord ( bday
‘𝐵)) →
(( bday ‘𝐴) ∈ ( bday
‘𝐵) ∨
( bday ‘𝐴) = ( bday
‘𝐵) ∨
( bday ‘𝐵) ∈ ( bday
‘𝐴))) |
6 | 2, 4, 5 | mp2an 690 |
. 2
⊢ (( bday ‘𝐴) ∈ ( bday
‘𝐵) ∨
( bday ‘𝐴) = ( bday
‘𝐵) ∨
( bday ‘𝐵) ∈ ( bday
‘𝐴)) |
7 | | negsproplem.1 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ No
∀𝑦 ∈ No ((( bday ‘𝑥) ∪ (
bday ‘𝑦))
∈ (( bday ‘𝐴) ∪ ( bday
‘𝐵)) → ((
-us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) |
8 | 7 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝐴)
∈ ( bday ‘𝐵)) → ∀𝑥 ∈ No
∀𝑦 ∈ No ((( bday ‘𝑥) ∪ (
bday ‘𝑦))
∈ (( bday ‘𝐴) ∪ ( bday
‘𝐵)) → ((
-us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) |
9 | | negsproplem4.1 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ No
) |
10 | 9 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝐴)
∈ ( bday ‘𝐵)) → 𝐴 ∈ No
) |
11 | | negsproplem4.2 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ No
) |
12 | 11 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝐴)
∈ ( bday ‘𝐵)) → 𝐵 ∈ No
) |
13 | | negsproplem4.3 |
. . . . . 6
⊢ (𝜑 → 𝐴 <s 𝐵) |
14 | 13 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝐴)
∈ ( bday ‘𝐵)) → 𝐴 <s 𝐵) |
15 | | simpr 485 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝐴)
∈ ( bday ‘𝐵)) → ( bday
‘𝐴) ∈
( bday ‘𝐵)) |
16 | 8, 10, 12, 14, 15 | negsproplem4 34317 |
. . . 4
⊢ ((𝜑 ∧ (
bday ‘𝐴)
∈ ( bday ‘𝐵)) → ( -us ‘𝐵) <s ( -us ‘𝐴)) |
17 | 16 | ex 413 |
. . 3
⊢ (𝜑 → ((
bday ‘𝐴)
∈ ( bday ‘𝐵) → ( -us ‘𝐵) <s ( -us ‘𝐴))) |
18 | 7 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝐴) =
( bday ‘𝐵)) → ∀𝑥 ∈ No
∀𝑦 ∈ No ((( bday ‘𝑥) ∪ (
bday ‘𝑦))
∈ (( bday ‘𝐴) ∪ ( bday
‘𝐵)) → ((
-us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) |
19 | 9 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝐴) =
( bday ‘𝐵)) → 𝐴 ∈ No
) |
20 | 11 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝐴) =
( bday ‘𝐵)) → 𝐵 ∈ No
) |
21 | 13 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝐴) =
( bday ‘𝐵)) → 𝐴 <s 𝐵) |
22 | | simpr 485 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝐴) =
( bday ‘𝐵)) → ( bday
‘𝐴) = ( bday ‘𝐵)) |
23 | 18, 19, 20, 21, 22 | negsproplem6 34319 |
. . . 4
⊢ ((𝜑 ∧ (
bday ‘𝐴) =
( bday ‘𝐵)) → ( -us ‘𝐵) <s ( -us ‘𝐴)) |
24 | 23 | ex 413 |
. . 3
⊢ (𝜑 → ((
bday ‘𝐴) =
( bday ‘𝐵) → ( -us ‘𝐵) <s ( -us ‘𝐴))) |
25 | 7 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝐵)
∈ ( bday ‘𝐴)) → ∀𝑥 ∈ No
∀𝑦 ∈ No ((( bday ‘𝑥) ∪ (
bday ‘𝑦))
∈ (( bday ‘𝐴) ∪ ( bday
‘𝐵)) → ((
-us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) |
26 | 9 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝐵)
∈ ( bday ‘𝐴)) → 𝐴 ∈ No
) |
27 | 11 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝐵)
∈ ( bday ‘𝐴)) → 𝐵 ∈ No
) |
28 | 13 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝐵)
∈ ( bday ‘𝐴)) → 𝐴 <s 𝐵) |
29 | | simpr 485 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝐵)
∈ ( bday ‘𝐴)) → ( bday
‘𝐵) ∈
( bday ‘𝐴)) |
30 | 25, 26, 27, 28, 29 | negsproplem5 34318 |
. . . 4
⊢ ((𝜑 ∧ (
bday ‘𝐵)
∈ ( bday ‘𝐴)) → ( -us ‘𝐵) <s ( -us ‘𝐴)) |
31 | 30 | ex 413 |
. . 3
⊢ (𝜑 → ((
bday ‘𝐵)
∈ ( bday ‘𝐴) → ( -us ‘𝐵) <s ( -us ‘𝐴))) |
32 | 17, 24, 31 | 3jaod 1428 |
. 2
⊢ (𝜑 → (((
bday ‘𝐴)
∈ ( bday ‘𝐵) ∨ ( bday
‘𝐴) = ( bday ‘𝐵) ∨ ( bday
‘𝐵) ∈
( bday ‘𝐴)) → ( -us ‘𝐵) <s ( -us ‘𝐴))) |
33 | 6, 32 | mpi 20 |
1
⊢ (𝜑 → ( -us ‘𝐵) <s ( -us ‘𝐴)) |