Proof of Theorem mulsproplem7
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | rightssno 27921 | . . . 4
⊢ ( R
‘𝐵) ⊆  No | 
| 2 |  | mulsproplem7.4 | . . . 4
⊢ (𝜑 → 𝑆 ∈ ( R ‘𝐵)) | 
| 3 | 1, 2 | sselid 3980 | . . 3
⊢ (𝜑 → 𝑆 ∈  No
) | 
| 4 |  | mulsproplem7.6 | . . . 4
⊢ (𝜑 → 𝑈 ∈ ( R ‘𝐵)) | 
| 5 | 1, 4 | sselid 3980 | . . 3
⊢ (𝜑 → 𝑈 ∈  No
) | 
| 6 |  | sltlin 27795 | . . 3
⊢ ((𝑆 ∈ 
No  ∧ 𝑈 ∈
 No ) → (𝑆 <s 𝑈 ∨ 𝑆 = 𝑈 ∨ 𝑈 <s 𝑆)) | 
| 7 | 3, 5, 6 | syl2anc 584 | . 2
⊢ (𝜑 → (𝑆 <s 𝑈 ∨ 𝑆 = 𝑈 ∨ 𝑈 <s 𝑆)) | 
| 8 |  | mulsproplem.1 | . . . . . . . . 9
⊢ (𝜑 → ∀𝑎 ∈  No 
∀𝑏 ∈  No  ∀𝑐 ∈  No 
∀𝑑 ∈  No  ∀𝑒 ∈  No 
∀𝑓 ∈  No  (((( bday ‘𝑎) +no (
bday ‘𝑏))
∪ (((( bday ‘𝑐) +no ( bday
‘𝑒)) ∪
(( bday ‘𝑑) +no ( bday
‘𝑓))) ∪
((( bday ‘𝑐) +no ( bday
‘𝑓)) ∪
(( bday ‘𝑑) +no ( bday
‘𝑒))))) ∈
((( bday ‘𝐴) +no ( bday
‘𝐵)) ∪
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸))))) →
((𝑎 ·s
𝑏) ∈  No  ∧ ((𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓) → ((𝑐 ·s 𝑓) -s (𝑐 ·s 𝑒)) <s ((𝑑 ·s 𝑓) -s (𝑑 ·s 𝑒)))))) | 
| 9 |  | rightssold 27919 | . . . . . . . . . 10
⊢ ( R
‘𝐴) ⊆ ( O
‘( bday ‘𝐴)) | 
| 10 |  | mulsproplem7.3 | . . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ ( R ‘𝐴)) | 
| 11 | 9, 10 | sselid 3980 | . . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ ( O ‘(
bday ‘𝐴))) | 
| 12 |  | mulsproplem7.2 | . . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈  No
) | 
| 13 | 8, 11, 12 | mulsproplem2 28144 | . . . . . . . 8
⊢ (𝜑 → (𝑅 ·s 𝐵) ∈  No
) | 
| 14 |  | mulsproplem7.1 | . . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈  No
) | 
| 15 |  | rightssold 27919 | . . . . . . . . . 10
⊢ ( R
‘𝐵) ⊆ ( O
‘( bday ‘𝐵)) | 
| 16 | 15, 2 | sselid 3980 | . . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ ( O ‘(
bday ‘𝐵))) | 
| 17 | 8, 14, 16 | mulsproplem3 28145 | . . . . . . . 8
⊢ (𝜑 → (𝐴 ·s 𝑆) ∈  No
) | 
| 18 | 13, 17 | addscld 28014 | . . . . . . 7
⊢ (𝜑 → ((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) ∈  No
) | 
| 19 | 8, 11, 16 | mulsproplem4 28146 | . . . . . . 7
⊢ (𝜑 → (𝑅 ·s 𝑆) ∈  No
) | 
| 20 | 18, 19 | subscld 28094 | . . . . . 6
⊢ (𝜑 → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) ∈  No
) | 
| 21 | 20 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) ∈  No
) | 
| 22 |  | leftssold 27918 | . . . . . . . . . 10
⊢ ( L
‘𝐴) ⊆ ( O
‘( bday ‘𝐴)) | 
| 23 |  | mulsproplem7.5 | . . . . . . . . . 10
⊢ (𝜑 → 𝑇 ∈ ( L ‘𝐴)) | 
| 24 | 22, 23 | sselid 3980 | . . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ ( O ‘(
bday ‘𝐴))) | 
| 25 | 8, 24, 12 | mulsproplem2 28144 | . . . . . . . 8
⊢ (𝜑 → (𝑇 ·s 𝐵) ∈  No
) | 
| 26 | 25, 17 | addscld 28014 | . . . . . . 7
⊢ (𝜑 → ((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑆)) ∈  No
) | 
| 27 | 8, 24, 16 | mulsproplem4 28146 | . . . . . . 7
⊢ (𝜑 → (𝑇 ·s 𝑆) ∈  No
) | 
| 28 | 26, 27 | subscld 28094 | . . . . . 6
⊢ (𝜑 → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑇 ·s 𝑆)) ∈  No
) | 
| 29 | 28 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑇 ·s 𝑆)) ∈  No
) | 
| 30 | 15, 4 | sselid 3980 | . . . . . . . . 9
⊢ (𝜑 → 𝑈 ∈ ( O ‘(
bday ‘𝐵))) | 
| 31 | 8, 14, 30 | mulsproplem3 28145 | . . . . . . . 8
⊢ (𝜑 → (𝐴 ·s 𝑈) ∈  No
) | 
| 32 | 25, 31 | addscld 28014 | . . . . . . 7
⊢ (𝜑 → ((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) ∈  No
) | 
| 33 | 8, 24, 30 | mulsproplem4 28146 | . . . . . . 7
⊢ (𝜑 → (𝑇 ·s 𝑈) ∈  No
) | 
| 34 | 32, 33 | subscld 28094 | . . . . . 6
⊢ (𝜑 → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)) ∈  No
) | 
| 35 | 34 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)) ∈  No
) | 
| 36 |  | lltropt 27912 | . . . . . . . . . . 11
⊢ ( L
‘𝐴) <<s ( R
‘𝐴) | 
| 37 | 36 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → ( L ‘𝐴) <<s ( R ‘𝐴)) | 
| 38 | 37, 23, 10 | ssltsepcd 27840 | . . . . . . . . 9
⊢ (𝜑 → 𝑇 <s 𝑅) | 
| 39 |  | ssltright 27911 | . . . . . . . . . . 11
⊢ (𝐵 ∈ 
No  → {𝐵}
<<s ( R ‘𝐵)) | 
| 40 | 12, 39 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → {𝐵} <<s ( R ‘𝐵)) | 
| 41 |  | snidg 4659 | . . . . . . . . . . 11
⊢ (𝐵 ∈ 
No  → 𝐵 ∈
{𝐵}) | 
| 42 | 12, 41 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ {𝐵}) | 
| 43 | 40, 42, 2 | ssltsepcd 27840 | . . . . . . . . 9
⊢ (𝜑 → 𝐵 <s 𝑆) | 
| 44 |  | 0sno 27872 | . . . . . . . . . . . 12
⊢ 
0s ∈  No | 
| 45 | 44 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → 0s ∈  No ) | 
| 46 |  | leftssno 27920 | . . . . . . . . . . . 12
⊢ ( L
‘𝐴) ⊆  No | 
| 47 | 46, 23 | sselid 3980 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈  No
) | 
| 48 |  | rightssno 27921 | . . . . . . . . . . . 12
⊢ ( R
‘𝐴) ⊆  No | 
| 49 | 48, 10 | sselid 3980 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈  No
) | 
| 50 |  | bday0s 27874 | . . . . . . . . . . . . . . . 16
⊢ ( bday ‘ 0s ) = ∅ | 
| 51 | 50, 50 | oveq12i 7444 | . . . . . . . . . . . . . . 15
⊢ (( bday ‘ 0s ) +no ( bday ‘ 0s )) = (∅ +no
∅) | 
| 52 |  | 0elon 6437 | . . . . . . . . . . . . . . . 16
⊢ ∅
∈ On | 
| 53 |  | naddrid 8722 | . . . . . . . . . . . . . . . 16
⊢ (∅
∈ On → (∅ +no ∅) = ∅) | 
| 54 | 52, 53 | ax-mp 5 | . . . . . . . . . . . . . . 15
⊢ (∅
+no ∅) = ∅ | 
| 55 | 51, 54 | eqtri 2764 | . . . . . . . . . . . . . 14
⊢ (( bday ‘ 0s ) +no ( bday ‘ 0s )) =
∅ | 
| 56 | 55 | uneq1i 4163 | . . . . . . . . . . . . 13
⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵))))) =
(∅ ∪ (((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵))))) | 
| 57 |  | 0un 4395 | . . . . . . . . . . . . 13
⊢ (∅
∪ (((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵))))) =
(((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵)))) | 
| 58 | 56, 57 | eqtri 2764 | . . . . . . . . . . . 12
⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵))))) =
(((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵)))) | 
| 59 |  | oldbdayim 27928 | . . . . . . . . . . . . . . . . 17
⊢ (𝑇 ∈ ( O ‘( bday ‘𝐴)) → ( bday
‘𝑇) ∈
( bday ‘𝐴)) | 
| 60 | 24, 59 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (
bday ‘𝑇)
∈ ( bday ‘𝐴)) | 
| 61 |  | bdayelon 27822 | . . . . . . . . . . . . . . . . 17
⊢ ( bday ‘𝑇) ∈ On | 
| 62 |  | bdayelon 27822 | . . . . . . . . . . . . . . . . 17
⊢ ( bday ‘𝐴) ∈ On | 
| 63 |  | bdayelon 27822 | . . . . . . . . . . . . . . . . 17
⊢ ( bday ‘𝐵) ∈ On | 
| 64 |  | naddel1 8726 | . . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑇) ∈ On ∧ (
bday ‘𝐴)
∈ On ∧ ( bday ‘𝐵) ∈ On) → ((
bday ‘𝑇)
∈ ( bday ‘𝐴) ↔ (( bday
‘𝑇) +no ( bday ‘𝐵)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) | 
| 65 | 61, 62, 63, 64 | mp3an 1462 | . . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑇) ∈ ( bday
‘𝐴) ↔
(( bday ‘𝑇) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) | 
| 66 | 60, 65 | sylib 218 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((
bday ‘𝑇) +no
( bday ‘𝐵)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) | 
| 67 |  | oldbdayim 27928 | . . . . . . . . . . . . . . . . 17
⊢ (𝑅 ∈ ( O ‘( bday ‘𝐴)) → ( bday
‘𝑅) ∈
( bday ‘𝐴)) | 
| 68 | 11, 67 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (
bday ‘𝑅)
∈ ( bday ‘𝐴)) | 
| 69 |  | oldbdayim 27928 | . . . . . . . . . . . . . . . . 17
⊢ (𝑆 ∈ ( O ‘( bday ‘𝐵)) → ( bday
‘𝑆) ∈
( bday ‘𝐵)) | 
| 70 | 16, 69 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (
bday ‘𝑆)
∈ ( bday ‘𝐵)) | 
| 71 |  | naddel12 8739 | . . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝐴) ∈ On ∧ (
bday ‘𝐵)
∈ On) → ((( bday ‘𝑅) ∈ (
bday ‘𝐴) ∧
( bday ‘𝑆) ∈ ( bday
‘𝐵)) →
(( bday ‘𝑅) +no ( bday
‘𝑆)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) | 
| 72 | 62, 63, 71 | mp2an 692 | . . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑅) ∈ ( bday
‘𝐴) ∧
( bday ‘𝑆) ∈ ( bday
‘𝐵)) →
(( bday ‘𝑅) +no ( bday
‘𝑆)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) | 
| 73 | 68, 70, 72 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((
bday ‘𝑅) +no
( bday ‘𝑆)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) | 
| 74 | 66, 73 | jca 511 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((
bday ‘𝑇) +no
( bday ‘𝐵)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday
‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) | 
| 75 |  | naddel12 8739 | . . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝐴) ∈ On ∧ (
bday ‘𝐵)
∈ On) → ((( bday ‘𝑇) ∈ (
bday ‘𝐴) ∧
( bday ‘𝑆) ∈ ( bday
‘𝐵)) →
(( bday ‘𝑇) +no ( bday
‘𝑆)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) | 
| 76 | 62, 63, 75 | mp2an 692 | . . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑇) ∈ ( bday
‘𝐴) ∧
( bday ‘𝑆) ∈ ( bday
‘𝐵)) →
(( bday ‘𝑇) +no ( bday
‘𝑆)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) | 
| 77 | 60, 70, 76 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((
bday ‘𝑇) +no
( bday ‘𝑆)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) | 
| 78 |  | bdayelon 27822 | . . . . . . . . . . . . . . . . 17
⊢ ( bday ‘𝑅) ∈ On | 
| 79 |  | naddel1 8726 | . . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑅) ∈ On ∧ (
bday ‘𝐴)
∈ On ∧ ( bday ‘𝐵) ∈ On) → ((
bday ‘𝑅)
∈ ( bday ‘𝐴) ↔ (( bday
‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) | 
| 80 | 78, 62, 63, 79 | mp3an 1462 | . . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑅) ∈ ( bday
‘𝐴) ↔
(( bday ‘𝑅) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) | 
| 81 | 68, 80 | sylib 218 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((
bday ‘𝑅) +no
( bday ‘𝐵)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) | 
| 82 | 77, 81 | jca 511 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((
bday ‘𝑇) +no
( bday ‘𝑆)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday
‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) | 
| 83 |  | naddcl 8716 | . . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝑇) ∈ On ∧ (
bday ‘𝐵)
∈ On) → (( bday ‘𝑇) +no ( bday
‘𝐵)) ∈
On) | 
| 84 | 61, 63, 83 | mp2an 692 | . . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑇) +no ( bday
‘𝐵)) ∈
On | 
| 85 |  | bdayelon 27822 | . . . . . . . . . . . . . . . . . 18
⊢ ( bday ‘𝑆) ∈ On | 
| 86 |  | naddcl 8716 | . . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝑅) ∈ On ∧ (
bday ‘𝑆)
∈ On) → (( bday ‘𝑅) +no ( bday
‘𝑆)) ∈
On) | 
| 87 | 78, 85, 86 | mp2an 692 | . . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑅) +no ( bday
‘𝑆)) ∈
On | 
| 88 | 84, 87 | onun2i 6505 | . . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∈
On | 
| 89 |  | naddcl 8716 | . . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝑇) ∈ On ∧ (
bday ‘𝑆)
∈ On) → (( bday ‘𝑇) +no ( bday
‘𝑆)) ∈
On) | 
| 90 | 61, 85, 89 | mp2an 692 | . . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑇) +no ( bday
‘𝑆)) ∈
On | 
| 91 |  | naddcl 8716 | . . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝑅) ∈ On ∧ (
bday ‘𝐵)
∈ On) → (( bday ‘𝑅) +no ( bday
‘𝐵)) ∈
On) | 
| 92 | 78, 63, 91 | mp2an 692 | . . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑅) +no ( bday
‘𝐵)) ∈
On | 
| 93 | 90, 92 | onun2i 6505 | . . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵))) ∈
On | 
| 94 |  | naddcl 8716 | . . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝐴) ∈ On ∧ (
bday ‘𝐵)
∈ On) → (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) | 
| 95 | 62, 63, 94 | mp2an 692 | . . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On | 
| 96 |  | onunel 6488 | . . . . . . . . . . . . . . . 16
⊢
((((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∈
On ∧ ((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵))) ∈
On ∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → ((((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
(((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) | 
| 97 | 88, 93, 95, 96 | mp3an 1462 | . . . . . . . . . . . . . . 15
⊢
((((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
(((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) | 
| 98 |  | onunel 6488 | . . . . . . . . . . . . . . . . 17
⊢ (((( bday ‘𝑇) +no ( bday
‘𝐵)) ∈ On
∧ (( bday ‘𝑅) +no ( bday
‘𝑆)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → (((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑇) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑅) +no ( bday
‘𝑆)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) | 
| 99 | 84, 87, 95, 98 | mp3an 1462 | . . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑇) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑅) +no ( bday
‘𝑆)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) | 
| 100 |  | onunel 6488 | . . . . . . . . . . . . . . . . 17
⊢ (((( bday ‘𝑇) +no ( bday
‘𝑆)) ∈ On
∧ (( bday ‘𝑅) +no ( bday
‘𝐵)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → (((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑇) +no ( bday
‘𝑆)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑅) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) | 
| 101 | 90, 92, 95, 100 | mp3an 1462 | . . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑇) +no ( bday
‘𝑆)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑅) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) | 
| 102 | 99, 101 | anbi12i 628 | . . . . . . . . . . . . . . 15
⊢
((((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) ↔
(((( bday ‘𝑇) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑅) +no ( bday
‘𝑆)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) ∧
((( bday ‘𝑇) +no ( bday
‘𝑆)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑅) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) | 
| 103 | 97, 102 | bitri 275 | . . . . . . . . . . . . . 14
⊢
((((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
(((( bday ‘𝑇) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑅) +no ( bday
‘𝑆)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) ∧
((( bday ‘𝑇) +no ( bday
‘𝑆)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑅) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) | 
| 104 | 74, 82, 103 | sylanbrc 583 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((((
bday ‘𝑇) +no
( bday ‘𝐵)) ∪ (( bday
‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday
‘𝑇) +no ( bday ‘𝑆)) ∪ (( bday
‘𝑅) +no ( bday ‘𝐵)))) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) | 
| 105 |  | elun1 4181 | . . . . . . . . . . . . 13
⊢
((((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) →
(((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵)))) ∈
((( bday ‘𝐴) +no ( bday
‘𝐵)) ∪
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸)))))) | 
| 106 | 104, 105 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → ((((
bday ‘𝑇) +no
( bday ‘𝐵)) ∪ (( bday
‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday
‘𝑇) +no ( bday ‘𝑆)) ∪ (( bday
‘𝑅) +no ( bday ‘𝐵)))) ∈ ((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday
‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐸)))))) | 
| 107 | 58, 106 | eqeltrid 2844 | . . . . . . . . . . 11
⊢ (𝜑 → (((
bday ‘ 0s ) +no ( bday
‘ 0s )) ∪ (((( bday
‘𝑇) +no ( bday ‘𝐵)) ∪ (( bday
‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday
‘𝑇) +no ( bday ‘𝑆)) ∪ (( bday
‘𝑅) +no ( bday ‘𝐵))))) ∈ ((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday
‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐸)))))) | 
| 108 | 8, 45, 45, 47, 49, 12, 3, 107 | mulsproplem1 28143 | . . . . . . . . . 10
⊢ (𝜑 → (( 0s
·s 0s ) ∈  No 
∧ ((𝑇 <s 𝑅 ∧ 𝐵 <s 𝑆) → ((𝑇 ·s 𝑆) -s (𝑇 ·s 𝐵)) <s ((𝑅 ·s 𝑆) -s (𝑅 ·s 𝐵))))) | 
| 109 | 108 | simprd 495 | . . . . . . . . 9
⊢ (𝜑 → ((𝑇 <s 𝑅 ∧ 𝐵 <s 𝑆) → ((𝑇 ·s 𝑆) -s (𝑇 ·s 𝐵)) <s ((𝑅 ·s 𝑆) -s (𝑅 ·s 𝐵)))) | 
| 110 | 38, 43, 109 | mp2and 699 | . . . . . . . 8
⊢ (𝜑 → ((𝑇 ·s 𝑆) -s (𝑇 ·s 𝐵)) <s ((𝑅 ·s 𝑆) -s (𝑅 ·s 𝐵))) | 
| 111 | 27, 25, 19, 13 | sltsubsub2bd 28115 | . . . . . . . . 9
⊢ (𝜑 → (((𝑇 ·s 𝑆) -s (𝑇 ·s 𝐵)) <s ((𝑅 ·s 𝑆) -s (𝑅 ·s 𝐵)) ↔ ((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑆)) <s ((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑆)))) | 
| 112 | 13, 19 | subscld 28094 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑆)) ∈  No
) | 
| 113 | 25, 27 | subscld 28094 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑆)) ∈  No
) | 
| 114 | 112, 113,
17 | sltadd1d 28032 | . . . . . . . . 9
⊢ (𝜑 → (((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑆)) <s ((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑆)) ↔ (((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑆)) +s (𝐴 ·s 𝑆)) <s (((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑆)) +s (𝐴 ·s 𝑆)))) | 
| 115 | 111, 114 | bitrd 279 | . . . . . . . 8
⊢ (𝜑 → (((𝑇 ·s 𝑆) -s (𝑇 ·s 𝐵)) <s ((𝑅 ·s 𝑆) -s (𝑅 ·s 𝐵)) ↔ (((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑆)) +s (𝐴 ·s 𝑆)) <s (((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑆)) +s (𝐴 ·s 𝑆)))) | 
| 116 | 110, 115 | mpbid 232 | . . . . . . 7
⊢ (𝜑 → (((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑆)) +s (𝐴 ·s 𝑆)) <s (((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑆)) +s (𝐴 ·s 𝑆))) | 
| 117 | 13, 17, 19 | addsubsd 28113 | . . . . . . 7
⊢ (𝜑 → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) = (((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑆)) +s (𝐴 ·s 𝑆))) | 
| 118 | 25, 17, 27 | addsubsd 28113 | . . . . . . 7
⊢ (𝜑 → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑇 ·s 𝑆)) = (((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑆)) +s (𝐴 ·s 𝑆))) | 
| 119 | 116, 117,
118 | 3brtr4d 5174 | . . . . . 6
⊢ (𝜑 → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑇 ·s 𝑆))) | 
| 120 | 119 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑇 ·s 𝑆))) | 
| 121 |  | ssltleft 27910 | . . . . . . . . . . 11
⊢ (𝐴 ∈ 
No  → ( L ‘𝐴) <<s {𝐴}) | 
| 122 | 14, 121 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → ( L ‘𝐴) <<s {𝐴}) | 
| 123 |  | snidg 4659 | . . . . . . . . . . 11
⊢ (𝐴 ∈ 
No  → 𝐴 ∈
{𝐴}) | 
| 124 | 14, 123 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ {𝐴}) | 
| 125 | 122, 23, 124 | ssltsepcd 27840 | . . . . . . . . 9
⊢ (𝜑 → 𝑇 <s 𝐴) | 
| 126 | 55 | uneq1i 4163 | . . . . . . . . . . . . 13
⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑆))))) =
(∅ ∪ (((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑆))))) | 
| 127 |  | 0un 4395 | . . . . . . . . . . . . 13
⊢ (∅
∪ (((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑆))))) =
(((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑆)))) | 
| 128 | 126, 127 | eqtri 2764 | . . . . . . . . . . . 12
⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑆))))) =
(((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑆)))) | 
| 129 |  | oldbdayim 27928 | . . . . . . . . . . . . . . . . 17
⊢ (𝑈 ∈ ( O ‘( bday ‘𝐵)) → ( bday
‘𝑈) ∈
( bday ‘𝐵)) | 
| 130 | 30, 129 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (
bday ‘𝑈)
∈ ( bday ‘𝐵)) | 
| 131 |  | bdayelon 27822 | . . . . . . . . . . . . . . . . 17
⊢ ( bday ‘𝑈) ∈ On | 
| 132 |  | naddel2 8727 | . . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑈) ∈ On ∧ (
bday ‘𝐵)
∈ On ∧ ( bday ‘𝐴) ∈ On) → ((
bday ‘𝑈)
∈ ( bday ‘𝐵) ↔ (( bday
‘𝐴) +no ( bday ‘𝑈)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) | 
| 133 | 131, 63, 62, 132 | mp3an 1462 | . . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑈) ∈ ( bday
‘𝐵) ↔
(( bday ‘𝐴) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) | 
| 134 | 130, 133 | sylib 218 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((
bday ‘𝐴) +no
( bday ‘𝑈)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) | 
| 135 | 77, 134 | jca 511 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((
bday ‘𝑇) +no
( bday ‘𝑆)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday
‘𝐴) +no ( bday ‘𝑈)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) | 
| 136 |  | naddel12 8739 | . . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝐴) ∈ On ∧ (
bday ‘𝐵)
∈ On) → ((( bday ‘𝑇) ∈ (
bday ‘𝐴) ∧
( bday ‘𝑈) ∈ ( bday
‘𝐵)) →
(( bday ‘𝑇) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) | 
| 137 | 62, 63, 136 | mp2an 692 | . . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑇) ∈ ( bday
‘𝐴) ∧
( bday ‘𝑈) ∈ ( bday
‘𝐵)) →
(( bday ‘𝑇) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) | 
| 138 | 60, 130, 137 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((
bday ‘𝑇) +no
( bday ‘𝑈)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) | 
| 139 |  | naddel2 8727 | . . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑆) ∈ On ∧ (
bday ‘𝐵)
∈ On ∧ ( bday ‘𝐴) ∈ On) → ((
bday ‘𝑆)
∈ ( bday ‘𝐵) ↔ (( bday
‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) | 
| 140 | 85, 63, 62, 139 | mp3an 1462 | . . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑆) ∈ ( bday
‘𝐵) ↔
(( bday ‘𝐴) +no ( bday
‘𝑆)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) | 
| 141 | 70, 140 | sylib 218 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((
bday ‘𝐴) +no
( bday ‘𝑆)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) | 
| 142 | 138, 141 | jca 511 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((
bday ‘𝑇) +no
( bday ‘𝑈)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday
‘𝐴) +no ( bday ‘𝑆)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) | 
| 143 |  | naddcl 8716 | . . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝐴) ∈ On ∧ (
bday ‘𝑈)
∈ On) → (( bday ‘𝐴) +no ( bday
‘𝑈)) ∈
On) | 
| 144 | 62, 131, 143 | mp2an 692 | . . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝐴) +no ( bday
‘𝑈)) ∈
On | 
| 145 | 90, 144 | onun2i 6505 | . . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∈
On | 
| 146 |  | naddcl 8716 | . . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝑇) ∈ On ∧ (
bday ‘𝑈)
∈ On) → (( bday ‘𝑇) +no ( bday
‘𝑈)) ∈
On) | 
| 147 | 61, 131, 146 | mp2an 692 | . . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑇) +no ( bday
‘𝑈)) ∈
On | 
| 148 |  | naddcl 8716 | . . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝐴) ∈ On ∧ (
bday ‘𝑆)
∈ On) → (( bday ‘𝐴) +no ( bday
‘𝑆)) ∈
On) | 
| 149 | 62, 85, 148 | mp2an 692 | . . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝐴) +no ( bday
‘𝑆)) ∈
On | 
| 150 | 147, 149 | onun2i 6505 | . . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑆))) ∈
On | 
| 151 |  | onunel 6488 | . . . . . . . . . . . . . . . 16
⊢
((((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∈
On ∧ ((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑆))) ∈
On ∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → ((((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑆)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
(((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑆))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) | 
| 152 | 145, 150,
95, 151 | mp3an 1462 | . . . . . . . . . . . . . . 15
⊢
((((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑆)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
(((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑆))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) | 
| 153 |  | onunel 6488 | . . . . . . . . . . . . . . . . 17
⊢ (((( bday ‘𝑇) +no ( bday
‘𝑆)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝑈)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → (((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑇) +no ( bday
‘𝑆)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝐴) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) | 
| 154 | 90, 144, 95, 153 | mp3an 1462 | . . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑇) +no ( bday
‘𝑆)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝐴) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) | 
| 155 |  | onunel 6488 | . . . . . . . . . . . . . . . . 17
⊢ (((( bday ‘𝑇) +no ( bday
‘𝑈)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝑆)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → (((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑆))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝐴) +no ( bday
‘𝑆)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) | 
| 156 | 147, 149,
95, 155 | mp3an 1462 | . . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑆))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝐴) +no ( bday
‘𝑆)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) | 
| 157 | 154, 156 | anbi12i 628 | . . . . . . . . . . . . . . 15
⊢
((((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑆))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) ↔
(((( bday ‘𝑇) +no ( bday
‘𝑆)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝐴) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) ∧
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝐴) +no ( bday
‘𝑆)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) | 
| 158 | 152, 157 | bitri 275 | . . . . . . . . . . . . . 14
⊢
((((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑆)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
(((( bday ‘𝑇) +no ( bday
‘𝑆)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝐴) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) ∧
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝐴) +no ( bday
‘𝑆)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) | 
| 159 | 135, 142,
158 | sylanbrc 583 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((((
bday ‘𝑇) +no
( bday ‘𝑆)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑈))) ∪ ((( bday
‘𝑇) +no ( bday ‘𝑈)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑆)))) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) | 
| 160 |  | elun1 4181 | . . . . . . . . . . . . 13
⊢
((((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑆)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) →
(((( bday ‘𝑇) +no ( bday
‘𝑆)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝐴) +no ( bday
‘𝑆)))) ∈
((( bday ‘𝐴) +no ( bday
‘𝐵)) ∪
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸)))))) | 
| 161 | 159, 160 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → ((((
bday ‘𝑇) +no
( bday ‘𝑆)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑈))) ∪ ((( bday
‘𝑇) +no ( bday ‘𝑈)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑆)))) ∈ ((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday
‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐸)))))) | 
| 162 | 128, 161 | eqeltrid 2844 | . . . . . . . . . . 11
⊢ (𝜑 → (((
bday ‘ 0s ) +no ( bday
‘ 0s )) ∪ (((( bday
‘𝑇) +no ( bday ‘𝑆)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑈))) ∪ ((( bday
‘𝑇) +no ( bday ‘𝑈)) ∪ (( bday
‘𝐴) +no ( bday ‘𝑆))))) ∈ ((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday
‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐸)))))) | 
| 163 | 8, 45, 45, 47, 14, 3, 5, 162 | mulsproplem1 28143 | . . . . . . . . . 10
⊢ (𝜑 → (( 0s
·s 0s ) ∈  No 
∧ ((𝑇 <s 𝐴 ∧ 𝑆 <s 𝑈) → ((𝑇 ·s 𝑈) -s (𝑇 ·s 𝑆)) <s ((𝐴 ·s 𝑈) -s (𝐴 ·s 𝑆))))) | 
| 164 | 163 | simprd 495 | . . . . . . . . 9
⊢ (𝜑 → ((𝑇 <s 𝐴 ∧ 𝑆 <s 𝑈) → ((𝑇 ·s 𝑈) -s (𝑇 ·s 𝑆)) <s ((𝐴 ·s 𝑈) -s (𝐴 ·s 𝑆)))) | 
| 165 | 125, 164 | mpand 695 | . . . . . . . 8
⊢ (𝜑 → (𝑆 <s 𝑈 → ((𝑇 ·s 𝑈) -s (𝑇 ·s 𝑆)) <s ((𝐴 ·s 𝑈) -s (𝐴 ·s 𝑆)))) | 
| 166 | 165 | imp 406 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → ((𝑇 ·s 𝑈) -s (𝑇 ·s 𝑆)) <s ((𝐴 ·s 𝑈) -s (𝐴 ·s 𝑆))) | 
| 167 | 33, 31, 27, 17 | sltsubsub3bd 28116 | . . . . . . . . 9
⊢ (𝜑 → (((𝑇 ·s 𝑈) -s (𝑇 ·s 𝑆)) <s ((𝐴 ·s 𝑈) -s (𝐴 ·s 𝑆)) ↔ ((𝐴 ·s 𝑆) -s (𝑇 ·s 𝑆)) <s ((𝐴 ·s 𝑈) -s (𝑇 ·s 𝑈)))) | 
| 168 | 17, 27 | subscld 28094 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐴 ·s 𝑆) -s (𝑇 ·s 𝑆)) ∈  No
) | 
| 169 | 31, 33 | subscld 28094 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐴 ·s 𝑈) -s (𝑇 ·s 𝑈)) ∈  No
) | 
| 170 | 168, 169,
25 | sltadd2d 28031 | . . . . . . . . 9
⊢ (𝜑 → (((𝐴 ·s 𝑆) -s (𝑇 ·s 𝑆)) <s ((𝐴 ·s 𝑈) -s (𝑇 ·s 𝑈)) ↔ ((𝑇 ·s 𝐵) +s ((𝐴 ·s 𝑆) -s (𝑇 ·s 𝑆))) <s ((𝑇 ·s 𝐵) +s ((𝐴 ·s 𝑈) -s (𝑇 ·s 𝑈))))) | 
| 171 | 167, 170 | bitrd 279 | . . . . . . . 8
⊢ (𝜑 → (((𝑇 ·s 𝑈) -s (𝑇 ·s 𝑆)) <s ((𝐴 ·s 𝑈) -s (𝐴 ·s 𝑆)) ↔ ((𝑇 ·s 𝐵) +s ((𝐴 ·s 𝑆) -s (𝑇 ·s 𝑆))) <s ((𝑇 ·s 𝐵) +s ((𝐴 ·s 𝑈) -s (𝑇 ·s 𝑈))))) | 
| 172 | 171 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·s 𝑈) -s (𝑇 ·s 𝑆)) <s ((𝐴 ·s 𝑈) -s (𝐴 ·s 𝑆)) ↔ ((𝑇 ·s 𝐵) +s ((𝐴 ·s 𝑆) -s (𝑇 ·s 𝑆))) <s ((𝑇 ·s 𝐵) +s ((𝐴 ·s 𝑈) -s (𝑇 ·s 𝑈))))) | 
| 173 | 166, 172 | mpbid 232 | . . . . . 6
⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → ((𝑇 ·s 𝐵) +s ((𝐴 ·s 𝑆) -s (𝑇 ·s 𝑆))) <s ((𝑇 ·s 𝐵) +s ((𝐴 ·s 𝑈) -s (𝑇 ·s 𝑈)))) | 
| 174 | 25, 17, 27 | addsubsassd 28112 | . . . . . . 7
⊢ (𝜑 → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑇 ·s 𝑆)) = ((𝑇 ·s 𝐵) +s ((𝐴 ·s 𝑆) -s (𝑇 ·s 𝑆)))) | 
| 175 | 174 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑇 ·s 𝑆)) = ((𝑇 ·s 𝐵) +s ((𝐴 ·s 𝑆) -s (𝑇 ·s 𝑆)))) | 
| 176 | 25, 31, 33 | addsubsassd 28112 | . . . . . . 7
⊢ (𝜑 → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)) = ((𝑇 ·s 𝐵) +s ((𝐴 ·s 𝑈) -s (𝑇 ·s 𝑈)))) | 
| 177 | 176 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)) = ((𝑇 ·s 𝐵) +s ((𝐴 ·s 𝑈) -s (𝑇 ·s 𝑈)))) | 
| 178 | 173, 175,
177 | 3brtr4d 5174 | . . . . 5
⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑇 ·s 𝑆)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈))) | 
| 179 | 21, 29, 35, 120, 178 | slttrd 27805 | . . . 4
⊢ ((𝜑 ∧ 𝑆 <s 𝑈) → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈))) | 
| 180 | 179 | ex 412 | . . 3
⊢ (𝜑 → (𝑆 <s 𝑈 → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)))) | 
| 181 | 40, 42, 4 | ssltsepcd 27840 | . . . . . . 7
⊢ (𝜑 → 𝐵 <s 𝑈) | 
| 182 | 55 | uneq1i 4163 | . . . . . . . . . . 11
⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵))))) =
(∅ ∪ (((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵))))) | 
| 183 |  | 0un 4395 | . . . . . . . . . . 11
⊢ (∅
∪ (((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵))))) =
(((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵)))) | 
| 184 | 182, 183 | eqtri 2764 | . . . . . . . . . 10
⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵))))) =
(((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵)))) | 
| 185 |  | naddel12 8739 | . . . . . . . . . . . . . . 15
⊢ ((( bday ‘𝐴) ∈ On ∧ (
bday ‘𝐵)
∈ On) → ((( bday ‘𝑅) ∈ (
bday ‘𝐴) ∧
( bday ‘𝑈) ∈ ( bday
‘𝐵)) →
(( bday ‘𝑅) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) | 
| 186 | 62, 63, 185 | mp2an 692 | . . . . . . . . . . . . . 14
⊢ ((( bday ‘𝑅) ∈ ( bday
‘𝐴) ∧
( bday ‘𝑈) ∈ ( bday
‘𝐵)) →
(( bday ‘𝑅) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) | 
| 187 | 68, 130, 186 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((
bday ‘𝑅) +no
( bday ‘𝑈)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) | 
| 188 | 66, 187 | jca 511 | . . . . . . . . . . . 12
⊢ (𝜑 → (((
bday ‘𝑇) +no
( bday ‘𝐵)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday
‘𝑅) +no ( bday ‘𝑈)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) | 
| 189 | 138, 81 | jca 511 | . . . . . . . . . . . 12
⊢ (𝜑 → (((
bday ‘𝑇) +no
( bday ‘𝑈)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday
‘𝑅) +no ( bday ‘𝐵)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) | 
| 190 |  | naddcl 8716 | . . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑅) ∈ On ∧ (
bday ‘𝑈)
∈ On) → (( bday ‘𝑅) +no ( bday
‘𝑈)) ∈
On) | 
| 191 | 78, 131, 190 | mp2an 692 | . . . . . . . . . . . . . . 15
⊢ (( bday ‘𝑅) +no ( bday
‘𝑈)) ∈
On | 
| 192 | 84, 191 | onun2i 6505 | . . . . . . . . . . . . . 14
⊢ ((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈))) ∈
On | 
| 193 | 147, 92 | onun2i 6505 | . . . . . . . . . . . . . 14
⊢ ((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵))) ∈
On | 
| 194 |  | onunel 6488 | . . . . . . . . . . . . . 14
⊢
((((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈))) ∈
On ∧ ((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵))) ∈
On ∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → ((((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
(((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) | 
| 195 | 192, 193,
95, 194 | mp3an 1462 | . . . . . . . . . . . . 13
⊢
((((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
(((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) | 
| 196 |  | onunel 6488 | . . . . . . . . . . . . . . 15
⊢ (((( bday ‘𝑇) +no ( bday
‘𝐵)) ∈ On
∧ (( bday ‘𝑅) +no ( bday
‘𝑈)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → (((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑇) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑅) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) | 
| 197 | 84, 191, 95, 196 | mp3an 1462 | . . . . . . . . . . . . . 14
⊢ (((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑇) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑅) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) | 
| 198 |  | onunel 6488 | . . . . . . . . . . . . . . 15
⊢ (((( bday ‘𝑇) +no ( bday
‘𝑈)) ∈ On
∧ (( bday ‘𝑅) +no ( bday
‘𝐵)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → (((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑅) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) | 
| 199 | 147, 92, 95, 198 | mp3an 1462 | . . . . . . . . . . . . . 14
⊢ (((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑅) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) | 
| 200 | 197, 199 | anbi12i 628 | . . . . . . . . . . . . 13
⊢
((((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) ↔
(((( bday ‘𝑇) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑅) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) ∧
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑅) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) | 
| 201 | 195, 200 | bitri 275 | . . . . . . . . . . . 12
⊢
((((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
(((( bday ‘𝑇) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑅) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) ∧
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑅) +no ( bday
‘𝐵)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) | 
| 202 | 188, 189,
201 | sylanbrc 583 | . . . . . . . . . . 11
⊢ (𝜑 → ((((
bday ‘𝑇) +no
( bday ‘𝐵)) ∪ (( bday
‘𝑅) +no ( bday ‘𝑈))) ∪ ((( bday
‘𝑇) +no ( bday ‘𝑈)) ∪ (( bday
‘𝑅) +no ( bday ‘𝐵)))) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) | 
| 203 |  | elun1 4181 | . . . . . . . . . . 11
⊢
((((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) →
(((( bday ‘𝑇) +no ( bday
‘𝐵)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈))) ∪
((( bday ‘𝑇) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝐵)))) ∈
((( bday ‘𝐴) +no ( bday
‘𝐵)) ∪
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸)))))) | 
| 204 | 202, 203 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → ((((
bday ‘𝑇) +no
( bday ‘𝐵)) ∪ (( bday
‘𝑅) +no ( bday ‘𝑈))) ∪ ((( bday
‘𝑇) +no ( bday ‘𝑈)) ∪ (( bday
‘𝑅) +no ( bday ‘𝐵)))) ∈ ((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday
‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐸)))))) | 
| 205 | 184, 204 | eqeltrid 2844 | . . . . . . . . 9
⊢ (𝜑 → (((
bday ‘ 0s ) +no ( bday
‘ 0s )) ∪ (((( bday
‘𝑇) +no ( bday ‘𝐵)) ∪ (( bday
‘𝑅) +no ( bday ‘𝑈))) ∪ ((( bday
‘𝑇) +no ( bday ‘𝑈)) ∪ (( bday
‘𝑅) +no ( bday ‘𝐵))))) ∈ ((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday
‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐸)))))) | 
| 206 | 8, 45, 45, 47, 49, 12, 5, 205 | mulsproplem1 28143 | . . . . . . . 8
⊢ (𝜑 → (( 0s
·s 0s ) ∈  No 
∧ ((𝑇 <s 𝑅 ∧ 𝐵 <s 𝑈) → ((𝑇 ·s 𝑈) -s (𝑇 ·s 𝐵)) <s ((𝑅 ·s 𝑈) -s (𝑅 ·s 𝐵))))) | 
| 207 | 206 | simprd 495 | . . . . . . 7
⊢ (𝜑 → ((𝑇 <s 𝑅 ∧ 𝐵 <s 𝑈) → ((𝑇 ·s 𝑈) -s (𝑇 ·s 𝐵)) <s ((𝑅 ·s 𝑈) -s (𝑅 ·s 𝐵)))) | 
| 208 | 38, 181, 207 | mp2and 699 | . . . . . 6
⊢ (𝜑 → ((𝑇 ·s 𝑈) -s (𝑇 ·s 𝐵)) <s ((𝑅 ·s 𝑈) -s (𝑅 ·s 𝐵))) | 
| 209 | 8, 11, 30 | mulsproplem4 28146 | . . . . . . . 8
⊢ (𝜑 → (𝑅 ·s 𝑈) ∈  No
) | 
| 210 | 33, 25, 209, 13 | sltsubsub2bd 28115 | . . . . . . 7
⊢ (𝜑 → (((𝑇 ·s 𝑈) -s (𝑇 ·s 𝐵)) <s ((𝑅 ·s 𝑈) -s (𝑅 ·s 𝐵)) ↔ ((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑈)) <s ((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑈)))) | 
| 211 | 13, 209 | subscld 28094 | . . . . . . . 8
⊢ (𝜑 → ((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑈)) ∈  No
) | 
| 212 | 25, 33 | subscld 28094 | . . . . . . . 8
⊢ (𝜑 → ((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑈)) ∈  No
) | 
| 213 | 211, 212,
31 | sltadd1d 28032 | . . . . . . 7
⊢ (𝜑 → (((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑈)) <s ((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑈)) ↔ (((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑈)) +s (𝐴 ·s 𝑈)) <s (((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑈)) +s (𝐴 ·s 𝑈)))) | 
| 214 | 210, 213 | bitrd 279 | . . . . . 6
⊢ (𝜑 → (((𝑇 ·s 𝑈) -s (𝑇 ·s 𝐵)) <s ((𝑅 ·s 𝑈) -s (𝑅 ·s 𝐵)) ↔ (((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑈)) +s (𝐴 ·s 𝑈)) <s (((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑈)) +s (𝐴 ·s 𝑈)))) | 
| 215 | 208, 214 | mpbid 232 | . . . . 5
⊢ (𝜑 → (((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑈)) +s (𝐴 ·s 𝑈)) <s (((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑈)) +s (𝐴 ·s 𝑈))) | 
| 216 | 13, 31, 209 | addsubsd 28113 | . . . . 5
⊢ (𝜑 → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑅 ·s 𝑈)) = (((𝑅 ·s 𝐵) -s (𝑅 ·s 𝑈)) +s (𝐴 ·s 𝑈))) | 
| 217 | 25, 31, 33 | addsubsd 28113 | . . . . 5
⊢ (𝜑 → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)) = (((𝑇 ·s 𝐵) -s (𝑇 ·s 𝑈)) +s (𝐴 ·s 𝑈))) | 
| 218 | 215, 216,
217 | 3brtr4d 5174 | . . . 4
⊢ (𝜑 → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑅 ·s 𝑈)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈))) | 
| 219 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑆 = 𝑈 → (𝐴 ·s 𝑆) = (𝐴 ·s 𝑈)) | 
| 220 | 219 | oveq2d 7448 | . . . . . 6
⊢ (𝑆 = 𝑈 → ((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) = ((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑈))) | 
| 221 |  | oveq2 7440 | . . . . . 6
⊢ (𝑆 = 𝑈 → (𝑅 ·s 𝑆) = (𝑅 ·s 𝑈)) | 
| 222 | 220, 221 | oveq12d 7450 | . . . . 5
⊢ (𝑆 = 𝑈 → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) = (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑅 ·s 𝑈))) | 
| 223 | 222 | breq1d 5152 | . . . 4
⊢ (𝑆 = 𝑈 → ((((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)) ↔ (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑅 ·s 𝑈)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)))) | 
| 224 | 218, 223 | syl5ibrcom 247 | . . 3
⊢ (𝜑 → (𝑆 = 𝑈 → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)))) | 
| 225 | 20 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) ∈  No
) | 
| 226 | 13, 31 | addscld 28014 | . . . . . . 7
⊢ (𝜑 → ((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑈)) ∈  No
) | 
| 227 | 226, 209 | subscld 28094 | . . . . . 6
⊢ (𝜑 → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑅 ·s 𝑈)) ∈  No
) | 
| 228 | 227 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑅 ·s 𝑈)) ∈  No
) | 
| 229 | 34 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)) ∈  No
) | 
| 230 |  | ssltright 27911 | . . . . . . . . . . 11
⊢ (𝐴 ∈ 
No  → {𝐴}
<<s ( R ‘𝐴)) | 
| 231 | 14, 230 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → {𝐴} <<s ( R ‘𝐴)) | 
| 232 | 231, 124,
10 | ssltsepcd 27840 | . . . . . . . . 9
⊢ (𝜑 → 𝐴 <s 𝑅) | 
| 233 | 55 | uneq1i 4163 | . . . . . . . . . . . . 13
⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (((( bday ‘𝐴) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∪
((( bday ‘𝐴) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈))))) =
(∅ ∪ (((( bday ‘𝐴) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∪
((( bday ‘𝐴) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈))))) | 
| 234 |  | 0un 4395 | . . . . . . . . . . . . 13
⊢ (∅
∪ (((( bday ‘𝐴) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∪
((( bday ‘𝐴) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈))))) =
(((( bday ‘𝐴) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∪
((( bday ‘𝐴) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈)))) | 
| 235 | 233, 234 | eqtri 2764 | . . . . . . . . . . . 12
⊢ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (((( bday ‘𝐴) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∪
((( bday ‘𝐴) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈))))) =
(((( bday ‘𝐴) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∪
((( bday ‘𝐴) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈)))) | 
| 236 | 134, 73 | jca 511 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((
bday ‘𝐴) +no
( bday ‘𝑈)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday
‘𝑅) +no ( bday ‘𝑆)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) | 
| 237 | 141, 187 | jca 511 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((
bday ‘𝐴) +no
( bday ‘𝑆)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)) ∧ (( bday
‘𝑅) +no ( bday ‘𝑈)) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) | 
| 238 | 144, 87 | onun2i 6505 | . . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝐴) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∈
On | 
| 239 | 149, 191 | onun2i 6505 | . . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝐴) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈))) ∈
On | 
| 240 |  | onunel 6488 | . . . . . . . . . . . . . . . 16
⊢
((((( bday ‘𝐴) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∈
On ∧ ((( bday ‘𝐴) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈))) ∈
On ∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → ((((( bday ‘𝐴) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∪
((( bday ‘𝐴) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
(((( bday ‘𝐴) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
((( bday ‘𝐴) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) | 
| 241 | 238, 239,
95, 240 | mp3an 1462 | . . . . . . . . . . . . . . 15
⊢
((((( bday ‘𝐴) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∪
((( bday ‘𝐴) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
(((( bday ‘𝐴) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
((( bday ‘𝐴) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) | 
| 242 |  | onunel 6488 | . . . . . . . . . . . . . . . . 17
⊢ (((( bday ‘𝐴) +no ( bday
‘𝑈)) ∈ On
∧ (( bday ‘𝑅) +no ( bday
‘𝑆)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → (((( bday ‘𝐴) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝐴) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑅) +no ( bday
‘𝑆)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) | 
| 243 | 144, 87, 95, 242 | mp3an 1462 | . . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝐴) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝐴) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑅) +no ( bday
‘𝑆)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) | 
| 244 |  | onunel 6488 | . . . . . . . . . . . . . . . . 17
⊢ (((( bday ‘𝐴) +no ( bday
‘𝑆)) ∈ On
∧ (( bday ‘𝑅) +no ( bday
‘𝑈)) ∈ On
∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → (((( bday ‘𝐴) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝐴) +no ( bday
‘𝑆)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑅) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) | 
| 245 | 149, 191,
95, 244 | mp3an 1462 | . . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝐴) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
((( bday ‘𝐴) +no ( bday
‘𝑆)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑅) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)))) | 
| 246 | 243, 245 | anbi12i 628 | . . . . . . . . . . . . . . 15
⊢
((((( bday ‘𝐴) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
((( bday ‘𝐴) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) ↔
(((( bday ‘𝐴) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑅) +no ( bday
‘𝑆)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) ∧
((( bday ‘𝐴) +no ( bday
‘𝑆)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑅) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) | 
| 247 | 241, 246 | bitri 275 | . . . . . . . . . . . . . 14
⊢
((((( bday ‘𝐴) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∪
((( bday ‘𝐴) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
(((( bday ‘𝐴) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑅) +no ( bday
‘𝑆)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))) ∧
((( bday ‘𝐴) +no ( bday
‘𝑆)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) ∧
(( bday ‘𝑅) +no ( bday
‘𝑈)) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵))))) | 
| 248 | 236, 237,
247 | sylanbrc 583 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((((
bday ‘𝐴) +no
( bday ‘𝑈)) ∪ (( bday
‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday
‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday
‘𝑅) +no ( bday ‘𝑈)))) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵))) | 
| 249 |  | elun1 4181 | . . . . . . . . . . . . 13
⊢
((((( bday ‘𝐴) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∪
((( bday ‘𝐴) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈)))) ∈
(( bday ‘𝐴) +no ( bday
‘𝐵)) →
(((( bday ‘𝐴) +no ( bday
‘𝑈)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑆))) ∪
((( bday ‘𝐴) +no ( bday
‘𝑆)) ∪
(( bday ‘𝑅) +no ( bday
‘𝑈)))) ∈
((( bday ‘𝐴) +no ( bday
‘𝐵)) ∪
(((( bday ‘𝐶) +no ( bday
‘𝐸)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐹))) ∪
((( bday ‘𝐶) +no ( bday
‘𝐹)) ∪
(( bday ‘𝐷) +no ( bday
‘𝐸)))))) | 
| 250 | 248, 249 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → ((((
bday ‘𝐴) +no
( bday ‘𝑈)) ∪ (( bday
‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday
‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday
‘𝑅) +no ( bday ‘𝑈)))) ∈ ((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday
‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐸)))))) | 
| 251 | 235, 250 | eqeltrid 2844 | . . . . . . . . . . 11
⊢ (𝜑 → (((
bday ‘ 0s ) +no ( bday
‘ 0s )) ∪ (((( bday
‘𝐴) +no ( bday ‘𝑈)) ∪ (( bday
‘𝑅) +no ( bday ‘𝑆))) ∪ ((( bday
‘𝐴) +no ( bday ‘𝑆)) ∪ (( bday
‘𝑅) +no ( bday ‘𝑈))))) ∈ ((( bday
‘𝐴) +no ( bday ‘𝐵)) ∪ (((( bday
‘𝐶) +no ( bday ‘𝐸)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐹))) ∪ ((( bday
‘𝐶) +no ( bday ‘𝐹)) ∪ (( bday
‘𝐷) +no ( bday ‘𝐸)))))) | 
| 252 | 8, 45, 45, 14, 49, 5, 3, 251 | mulsproplem1 28143 | . . . . . . . . . 10
⊢ (𝜑 → (( 0s
·s 0s ) ∈  No 
∧ ((𝐴 <s 𝑅 ∧ 𝑈 <s 𝑆) → ((𝐴 ·s 𝑆) -s (𝐴 ·s 𝑈)) <s ((𝑅 ·s 𝑆) -s (𝑅 ·s 𝑈))))) | 
| 253 | 252 | simprd 495 | . . . . . . . . 9
⊢ (𝜑 → ((𝐴 <s 𝑅 ∧ 𝑈 <s 𝑆) → ((𝐴 ·s 𝑆) -s (𝐴 ·s 𝑈)) <s ((𝑅 ·s 𝑆) -s (𝑅 ·s 𝑈)))) | 
| 254 | 232, 253 | mpand 695 | . . . . . . . 8
⊢ (𝜑 → (𝑈 <s 𝑆 → ((𝐴 ·s 𝑆) -s (𝐴 ·s 𝑈)) <s ((𝑅 ·s 𝑆) -s (𝑅 ·s 𝑈)))) | 
| 255 | 254 | imp 406 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → ((𝐴 ·s 𝑆) -s (𝐴 ·s 𝑈)) <s ((𝑅 ·s 𝑆) -s (𝑅 ·s 𝑈))) | 
| 256 | 17, 19, 31, 209 | sltsubsubbd 28114 | . . . . . . . . 9
⊢ (𝜑 → (((𝐴 ·s 𝑆) -s (𝐴 ·s 𝑈)) <s ((𝑅 ·s 𝑆) -s (𝑅 ·s 𝑈)) ↔ ((𝐴 ·s 𝑆) -s (𝑅 ·s 𝑆)) <s ((𝐴 ·s 𝑈) -s (𝑅 ·s 𝑈)))) | 
| 257 | 17, 19 | subscld 28094 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐴 ·s 𝑆) -s (𝑅 ·s 𝑆)) ∈  No
) | 
| 258 | 31, 209 | subscld 28094 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐴 ·s 𝑈) -s (𝑅 ·s 𝑈)) ∈  No
) | 
| 259 | 257, 258,
13 | sltadd2d 28031 | . . . . . . . . 9
⊢ (𝜑 → (((𝐴 ·s 𝑆) -s (𝑅 ·s 𝑆)) <s ((𝐴 ·s 𝑈) -s (𝑅 ·s 𝑈)) ↔ ((𝑅 ·s 𝐵) +s ((𝐴 ·s 𝑆) -s (𝑅 ·s 𝑆))) <s ((𝑅 ·s 𝐵) +s ((𝐴 ·s 𝑈) -s (𝑅 ·s 𝑈))))) | 
| 260 | 256, 259 | bitrd 279 | . . . . . . . 8
⊢ (𝜑 → (((𝐴 ·s 𝑆) -s (𝐴 ·s 𝑈)) <s ((𝑅 ·s 𝑆) -s (𝑅 ·s 𝑈)) ↔ ((𝑅 ·s 𝐵) +s ((𝐴 ·s 𝑆) -s (𝑅 ·s 𝑆))) <s ((𝑅 ·s 𝐵) +s ((𝐴 ·s 𝑈) -s (𝑅 ·s 𝑈))))) | 
| 261 | 260 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝐴 ·s 𝑆) -s (𝐴 ·s 𝑈)) <s ((𝑅 ·s 𝑆) -s (𝑅 ·s 𝑈)) ↔ ((𝑅 ·s 𝐵) +s ((𝐴 ·s 𝑆) -s (𝑅 ·s 𝑆))) <s ((𝑅 ·s 𝐵) +s ((𝐴 ·s 𝑈) -s (𝑅 ·s 𝑈))))) | 
| 262 | 255, 261 | mpbid 232 | . . . . . 6
⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → ((𝑅 ·s 𝐵) +s ((𝐴 ·s 𝑆) -s (𝑅 ·s 𝑆))) <s ((𝑅 ·s 𝐵) +s ((𝐴 ·s 𝑈) -s (𝑅 ·s 𝑈)))) | 
| 263 | 13, 17, 19 | addsubsassd 28112 | . . . . . . 7
⊢ (𝜑 → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) = ((𝑅 ·s 𝐵) +s ((𝐴 ·s 𝑆) -s (𝑅 ·s 𝑆)))) | 
| 264 | 263 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) = ((𝑅 ·s 𝐵) +s ((𝐴 ·s 𝑆) -s (𝑅 ·s 𝑆)))) | 
| 265 | 13, 31, 209 | addsubsassd 28112 | . . . . . . 7
⊢ (𝜑 → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑅 ·s 𝑈)) = ((𝑅 ·s 𝐵) +s ((𝐴 ·s 𝑈) -s (𝑅 ·s 𝑈)))) | 
| 266 | 265 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑅 ·s 𝑈)) = ((𝑅 ·s 𝐵) +s ((𝐴 ·s 𝑈) -s (𝑅 ·s 𝑈)))) | 
| 267 | 262, 264,
266 | 3brtr4d 5174 | . . . . 5
⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) <s (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑅 ·s 𝑈))) | 
| 268 | 218 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑅 ·s 𝑈)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈))) | 
| 269 | 225, 228,
229, 267, 268 | slttrd 27805 | . . . 4
⊢ ((𝜑 ∧ 𝑈 <s 𝑆) → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈))) | 
| 270 | 269 | ex 412 | . . 3
⊢ (𝜑 → (𝑈 <s 𝑆 → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)))) | 
| 271 | 180, 224,
270 | 3jaod 1430 | . 2
⊢ (𝜑 → ((𝑆 <s 𝑈 ∨ 𝑆 = 𝑈 ∨ 𝑈 <s 𝑆) → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈)))) | 
| 272 | 7, 271 | mpd 15 | 1
⊢ (𝜑 → (((𝑅 ·s 𝐵) +s (𝐴 ·s 𝑆)) -s (𝑅 ·s 𝑆)) <s (((𝑇 ·s 𝐵) +s (𝐴 ·s 𝑈)) -s (𝑇 ·s 𝑈))) |