| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mulscutlem.1 | . 2
⊢ (𝜑 → 𝐴 ∈  No
) | 
| 2 |  | mulscutlem.2 | . 2
⊢ (𝜑 → 𝐵 ∈  No
) | 
| 3 |  | mulsprop 28157 | . . . . . . . . 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 3201 | . . . . . 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 3201 | . . . . 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 3198 | . . . 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 482 | . . 3
⊢ ((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No ) → 𝐴 ∈  No
) | 
| 11 |  | simpr 484 | . . 3
⊢ ((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No ) → 𝐵 ∈  No
) | 
| 12 | 9, 10, 11 | mulsproplem10 28152 | . 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 𝑤))}))) |