Proof of Theorem negsproplem7
| Step | Hyp | Ref
| Expression |
| 1 | | bdayelon 27821 |
. . . 4
⊢ ( bday ‘𝐴) ∈ On |
| 2 | 1 | onordi 6495 |
. . 3
⊢ Ord
( bday ‘𝐴) |
| 3 | | bdayelon 27821 |
. . . 4
⊢ ( bday ‘𝐵) ∈ On |
| 4 | 3 | onordi 6495 |
. . 3
⊢ Ord
( bday ‘𝐵) |
| 5 | | ordtri3or 6416 |
. . 3
⊢ ((Ord
( bday ‘𝐴) ∧ Ord ( bday
‘𝐵)) →
(( bday ‘𝐴) ∈ ( bday
‘𝐵) ∨
( bday ‘𝐴) = ( bday
‘𝐵) ∨
( bday ‘𝐵) ∈ ( bday
‘𝐴))) |
| 6 | 2, 4, 5 | mp2an 692 |
. 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 480 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝐴)
∈ ( bday ‘𝐵)) → ∀𝑥 ∈ No
∀𝑦 ∈ No ((( bday ‘𝑥) ∪ (
bday ‘𝑦))
∈ (( bday ‘𝐴) ∪ ( bday
‘𝐵)) → ((
-us ‘𝑥)
∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us
‘𝑥))))) |
| 9 | | negsproplem4.1 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ No
) |
| 10 | 9 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝐴)
∈ ( bday ‘𝐵)) → 𝐴 ∈ No
) |
| 11 | | negsproplem4.2 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ No
) |
| 12 | 11 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝐴)
∈ ( bday ‘𝐵)) → 𝐵 ∈ No
) |
| 13 | | negsproplem4.3 |
. . . . . 6
⊢ (𝜑 → 𝐴 <s 𝐵) |
| 14 | 13 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝐴)
∈ ( bday ‘𝐵)) → 𝐴 <s 𝐵) |
| 15 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝐴)
∈ ( bday ‘𝐵)) → ( bday
‘𝐴) ∈
( bday ‘𝐵)) |
| 16 | 8, 10, 12, 14, 15 | negsproplem4 28063 |
. . . 4
⊢ ((𝜑 ∧ (
bday ‘𝐴)
∈ ( bday ‘𝐵)) → ( -us ‘𝐵) <s ( -us
‘𝐴)) |
| 17 | 16 | ex 412 |
. . 3
⊢ (𝜑 → ((
bday ‘𝐴)
∈ ( bday ‘𝐵) → ( -us ‘𝐵) <s ( -us
‘𝐴))) |
| 18 | 7 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝐴) =
( bday ‘𝐵)) → ∀𝑥 ∈ No
∀𝑦 ∈ No ((( bday ‘𝑥) ∪ (
bday ‘𝑦))
∈ (( bday ‘𝐴) ∪ ( bday
‘𝐵)) → ((
-us ‘𝑥)
∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us
‘𝑥))))) |
| 19 | 9 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝐴) =
( bday ‘𝐵)) → 𝐴 ∈ No
) |
| 20 | 11 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝐴) =
( bday ‘𝐵)) → 𝐵 ∈ No
) |
| 21 | 13 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝐴) =
( bday ‘𝐵)) → 𝐴 <s 𝐵) |
| 22 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝐴) =
( bday ‘𝐵)) → ( bday
‘𝐴) = ( bday ‘𝐵)) |
| 23 | 18, 19, 20, 21, 22 | negsproplem6 28065 |
. . . 4
⊢ ((𝜑 ∧ (
bday ‘𝐴) =
( bday ‘𝐵)) → ( -us ‘𝐵) <s ( -us
‘𝐴)) |
| 24 | 23 | ex 412 |
. . 3
⊢ (𝜑 → ((
bday ‘𝐴) =
( bday ‘𝐵) → ( -us ‘𝐵) <s ( -us
‘𝐴))) |
| 25 | 7 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝐵)
∈ ( bday ‘𝐴)) → ∀𝑥 ∈ No
∀𝑦 ∈ No ((( bday ‘𝑥) ∪ (
bday ‘𝑦))
∈ (( bday ‘𝐴) ∪ ( bday
‘𝐵)) → ((
-us ‘𝑥)
∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us
‘𝑥))))) |
| 26 | 9 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝐵)
∈ ( bday ‘𝐴)) → 𝐴 ∈ No
) |
| 27 | 11 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝐵)
∈ ( bday ‘𝐴)) → 𝐵 ∈ No
) |
| 28 | 13 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝐵)
∈ ( bday ‘𝐴)) → 𝐴 <s 𝐵) |
| 29 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝐵)
∈ ( bday ‘𝐴)) → ( bday
‘𝐵) ∈
( bday ‘𝐴)) |
| 30 | 25, 26, 27, 28, 29 | negsproplem5 28064 |
. . . 4
⊢ ((𝜑 ∧ (
bday ‘𝐵)
∈ ( bday ‘𝐴)) → ( -us ‘𝐵) <s ( -us
‘𝐴)) |
| 31 | 30 | ex 412 |
. . 3
⊢ (𝜑 → ((
bday ‘𝐵)
∈ ( bday ‘𝐴) → ( -us ‘𝐵) <s ( -us
‘𝐴))) |
| 32 | 17, 24, 31 | 3jaod 1431 |
. 2
⊢ (𝜑 → (((
bday ‘𝐴)
∈ ( bday ‘𝐵) ∨ ( bday
‘𝐴) = ( bday ‘𝐵) ∨ ( bday
‘𝐵) ∈
( bday ‘𝐴)) → ( -us ‘𝐵) <s ( -us
‘𝐴))) |
| 33 | 6, 32 | mpi 20 |
1
⊢ (𝜑 → ( -us
‘𝐵) <s (
-us ‘𝐴)) |