Step | Hyp | Ref
| Expression |
1 | | mulscutlem.1 |
. 2
⊢ (𝜑 → 𝐴 ∈ No
) |
2 | | mulscutlem.2 |
. 2
⊢ (𝜑 → 𝐵 ∈ No
) |
3 | | mulsprop 27515 |
. . . . . . . . 9
⊢ (((𝑒 ∈
No ∧ 𝑓 ∈
No ) ∧ (𝑔 ∈ No
∧ ℎ ∈ No ) ∧ (𝑖 ∈ No
∧ 𝑗 ∈ No )) → ((𝑒 ·s 𝑓) ∈ No
∧ ((𝑔 <s ℎ ∧ 𝑖 <s 𝑗) → ((𝑔 ·s 𝑗) -s (𝑔 ·s 𝑖)) <s ((ℎ ·s 𝑗) -s (ℎ ·s 𝑖))))) |
4 | 3 | a1d 25 |
. . . . . . . 8
⊢ (((𝑒 ∈
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
‘ 0s ) +no ( bday ‘
0s )) ∪ (( bday ‘
0s ) +no ( bday ‘ 0s
))) ∪ ((( bday ‘ 0s ) +no
( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑒 ·s 𝑓) ∈
No ∧ ((𝑔 <s
ℎ ∧ 𝑖 <s 𝑗) → ((𝑔 ·s 𝑗) -s (𝑔 ·s 𝑖)) <s ((ℎ ·s 𝑗) -s (ℎ ·s 𝑖)))))) |
5 | 4 | 3expa 1118 |
. . . . . . 7
⊢ ((((𝑒 ∈
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
‘ 0s ) +no ( bday ‘
0s )) ∪ (( bday ‘
0s ) +no ( bday ‘ 0s
))) ∪ ((( bday ‘ 0s ) +no
( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑒 ·s 𝑓) ∈
No ∧ ((𝑔 <s
ℎ ∧ 𝑖 <s 𝑗) → ((𝑔 ·s 𝑗) -s (𝑔 ·s 𝑖)) <s ((ℎ ·s 𝑗) -s (ℎ ·s 𝑖)))))) |
6 | 5 | ralrimivva 3200 |
. . . . . 6
⊢ (((𝑒 ∈
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 ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑒 ·s 𝑓) ∈
No ∧ ((𝑔 <s
ℎ ∧ 𝑖 <s 𝑗) → ((𝑔 ·s 𝑗) -s (𝑔 ·s 𝑖)) <s ((ℎ ·s 𝑗) -s (ℎ ·s 𝑖)))))) |
7 | 6 | ralrimivva 3200 |
. . . . 5
⊢ ((𝑒 ∈
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 ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑒 ·s 𝑓) ∈
No ∧ ((𝑔 <s
ℎ ∧ 𝑖 <s 𝑗) → ((𝑔 ·s 𝑗) -s (𝑔 ·s 𝑖)) <s ((ℎ ·s 𝑗) -s (ℎ ·s 𝑖)))))) |
8 | 7 | rgen2 3197 |
. . . 4
⊢
∀𝑒 ∈
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 ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑒 ·s 𝑓) ∈
No ∧ ((𝑔 <s
ℎ ∧ 𝑖 <s 𝑗) → ((𝑔 ·s 𝑗) -s (𝑔 ·s 𝑖)) <s ((ℎ ·s 𝑗) -s (ℎ ·s 𝑖))))) |
9 | 8 | a1i 11 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ∀𝑒 ∈ 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 ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))) ∪ ((( bday ‘ 0s ) +no ( bday ‘ 0s )) ∪ (( bday ‘ 0s ) +no ( bday ‘ 0s ))))) → ((𝑒 ·s 𝑓) ∈
No ∧ ((𝑔 <s
ℎ ∧ 𝑖 <s 𝑗) → ((𝑔 ·s 𝑗) -s (𝑔 ·s 𝑖)) <s ((ℎ ·s 𝑗) -s (ℎ ·s 𝑖)))))) |
10 | | simpl 483 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → 𝐴 ∈ No
) |
11 | | simpr 485 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → 𝐵 ∈ No
) |
12 | 9, 10, 11 | mulsproplem10 27510 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ((𝐴 ·s 𝐵) ∈ No
∧ ({𝑎 ∣
∃𝑝 ∈ ( L
‘𝐴)∃𝑞 ∈ ( L ‘𝐵)𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ ( R ‘𝐴)∃𝑠 ∈ ( R ‘𝐵)𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) <<s {(𝐴 ·s 𝐵)} ∧ {(𝐴 ·s 𝐵)} <<s ({𝑐 ∣ ∃𝑡 ∈ ( L ‘𝐴)∃𝑢 ∈ ( R ‘𝐵)𝑐 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑑 ∣ ∃𝑣 ∈ ( R ‘𝐴)∃𝑤 ∈ ( L ‘𝐵)𝑑 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))}))) |
13 | 1, 2, 12 | syl2anc 584 |
1
⊢ (𝜑 → ((𝐴 ·s 𝐵) ∈ No
∧ ({𝑎 ∣
∃𝑝 ∈ ( L
‘𝐴)∃𝑞 ∈ ( L ‘𝐵)𝑎 = (((𝑝 ·s 𝐵) +s (𝐴 ·s 𝑞)) -s (𝑝 ·s 𝑞))} ∪ {𝑏 ∣ ∃𝑟 ∈ ( R ‘𝐴)∃𝑠 ∈ ( R ‘𝐵)𝑏 = (((𝑟 ·s 𝐵) +s (𝐴 ·s 𝑠)) -s (𝑟 ·s 𝑠))}) <<s {(𝐴 ·s 𝐵)} ∧ {(𝐴 ·s 𝐵)} <<s ({𝑐 ∣ ∃𝑡 ∈ ( L ‘𝐴)∃𝑢 ∈ ( R ‘𝐵)𝑐 = (((𝑡 ·s 𝐵) +s (𝐴 ·s 𝑢)) -s (𝑡 ·s 𝑢))} ∪ {𝑑 ∣ ∃𝑣 ∈ ( R ‘𝐴)∃𝑤 ∈ ( L ‘𝐵)𝑑 = (((𝑣 ·s 𝐵) +s (𝐴 ·s 𝑤)) -s (𝑣 ·s 𝑤))}))) |