MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  remulscl Structured version   Visualization version   GIF version

Theorem remulscl 28229
Description: The surreal reals are closed under multiplication. Part of theorem 13(ii) of [Conway] p. 24. (Contributed by Scott Fenton, 16-Apr-2025.)
Assertion
Ref Expression
remulscl ((๐ด โˆˆ โ„s โˆง ๐ต โˆˆ โ„s) โ†’ (๐ด ยทs ๐ต) โˆˆ โ„s)

Proof of Theorem remulscl
Dummy variables ๐‘ฅ ๐‘ฆ ๐‘ง ๐‘› ๐‘š ๐‘ ๐‘ก ๐‘ข are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mulscl 28033 . . . . 5 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ (๐ด ยทs ๐ต) โˆˆ No )
21adantr 480 . . . 4 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ((โˆƒ๐‘› โˆˆ โ„•s (( -us โ€˜๐‘›) <s ๐ด โˆง ๐ด <s ๐‘›) โˆง ๐ด = ({๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))} |s {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))})) โˆง (โˆƒ๐‘š โˆˆ โ„•s (( -us โ€˜๐‘š) <s ๐ต โˆง ๐ต <s ๐‘š) โˆง ๐ต = ({๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))} |s {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))})))) โ†’ (๐ด ยทs ๐ต) โˆˆ No )
3 remulscllem2 28228 . . . . . . 7 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ((๐‘› โˆˆ โ„•s โˆง ๐‘š โˆˆ โ„•s) โˆง ((( -us โ€˜๐‘›) <s ๐ด โˆง ๐ด <s ๐‘›) โˆง (( -us โ€˜๐‘š) <s ๐ต โˆง ๐ต <s ๐‘š)))) โ†’ โˆƒ๐‘ โˆˆ โ„•s (( -us โ€˜๐‘) <s (๐ด ยทs ๐ต) โˆง (๐ด ยทs ๐ต) <s ๐‘))
43expr 456 . . . . . 6 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง (๐‘› โˆˆ โ„•s โˆง ๐‘š โˆˆ โ„•s)) โ†’ (((( -us โ€˜๐‘›) <s ๐ด โˆง ๐ด <s ๐‘›) โˆง (( -us โ€˜๐‘š) <s ๐ต โˆง ๐ต <s ๐‘š)) โ†’ โˆƒ๐‘ โˆˆ โ„•s (( -us โ€˜๐‘) <s (๐ด ยทs ๐ต) โˆง (๐ด ยทs ๐ต) <s ๐‘)))
54rexlimdvva 3208 . . . . 5 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ (โˆƒ๐‘› โˆˆ โ„•s โˆƒ๐‘š โˆˆ โ„•s ((( -us โ€˜๐‘›) <s ๐ด โˆง ๐ด <s ๐‘›) โˆง (( -us โ€˜๐‘š) <s ๐ต โˆง ๐ต <s ๐‘š)) โ†’ โˆƒ๐‘ โˆˆ โ„•s (( -us โ€˜๐‘) <s (๐ด ยทs ๐ต) โˆง (๐ด ยทs ๐ต) <s ๐‘)))
6 simpl 482 . . . . . . 7 ((โˆƒ๐‘› โˆˆ โ„•s (( -us โ€˜๐‘›) <s ๐ด โˆง ๐ด <s ๐‘›) โˆง ๐ด = ({๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))} |s {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))})) โ†’ โˆƒ๐‘› โˆˆ โ„•s (( -us โ€˜๐‘›) <s ๐ด โˆง ๐ด <s ๐‘›))
7 simpl 482 . . . . . . 7 ((โˆƒ๐‘š โˆˆ โ„•s (( -us โ€˜๐‘š) <s ๐ต โˆง ๐ต <s ๐‘š) โˆง ๐ต = ({๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))} |s {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))})) โ†’ โˆƒ๐‘š โˆˆ โ„•s (( -us โ€˜๐‘š) <s ๐ต โˆง ๐ต <s ๐‘š))
86, 7anim12i 612 . . . . . 6 (((โˆƒ๐‘› โˆˆ โ„•s (( -us โ€˜๐‘›) <s ๐ด โˆง ๐ด <s ๐‘›) โˆง ๐ด = ({๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))} |s {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))})) โˆง (โˆƒ๐‘š โˆˆ โ„•s (( -us โ€˜๐‘š) <s ๐ต โˆง ๐ต <s ๐‘š) โˆง ๐ต = ({๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))} |s {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}))) โ†’ (โˆƒ๐‘› โˆˆ โ„•s (( -us โ€˜๐‘›) <s ๐ด โˆง ๐ด <s ๐‘›) โˆง โˆƒ๐‘š โˆˆ โ„•s (( -us โ€˜๐‘š) <s ๐ต โˆง ๐ต <s ๐‘š)))
9 reeanv 3223 . . . . . 6 (โˆƒ๐‘› โˆˆ โ„•s โˆƒ๐‘š โˆˆ โ„•s ((( -us โ€˜๐‘›) <s ๐ด โˆง ๐ด <s ๐‘›) โˆง (( -us โ€˜๐‘š) <s ๐ต โˆง ๐ต <s ๐‘š)) โ†” (โˆƒ๐‘› โˆˆ โ„•s (( -us โ€˜๐‘›) <s ๐ด โˆง ๐ด <s ๐‘›) โˆง โˆƒ๐‘š โˆˆ โ„•s (( -us โ€˜๐‘š) <s ๐ต โˆง ๐ต <s ๐‘š)))
108, 9sylibr 233 . . . . 5 (((โˆƒ๐‘› โˆˆ โ„•s (( -us โ€˜๐‘›) <s ๐ด โˆง ๐ด <s ๐‘›) โˆง ๐ด = ({๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))} |s {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))})) โˆง (โˆƒ๐‘š โˆˆ โ„•s (( -us โ€˜๐‘š) <s ๐ต โˆง ๐ต <s ๐‘š) โˆง ๐ต = ({๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))} |s {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}))) โ†’ โˆƒ๐‘› โˆˆ โ„•s โˆƒ๐‘š โˆˆ โ„•s ((( -us โ€˜๐‘›) <s ๐ด โˆง ๐ด <s ๐‘›) โˆง (( -us โ€˜๐‘š) <s ๐ต โˆง ๐ต <s ๐‘š)))
115, 10impel 505 . . . 4 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ((โˆƒ๐‘› โˆˆ โ„•s (( -us โ€˜๐‘›) <s ๐ด โˆง ๐ด <s ๐‘›) โˆง ๐ด = ({๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))} |s {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))})) โˆง (โˆƒ๐‘š โˆˆ โ„•s (( -us โ€˜๐‘š) <s ๐ต โˆง ๐ต <s ๐‘š) โˆง ๐ต = ({๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))} |s {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))})))) โ†’ โˆƒ๐‘ โˆˆ โ„•s (( -us โ€˜๐‘) <s (๐ด ยทs ๐ต) โˆง (๐ด ยทs ๐ต) <s ๐‘))
12 simpr 484 . . . . . 6 ((โˆƒ๐‘› โˆˆ โ„•s (( -us โ€˜๐‘›) <s ๐ด โˆง ๐ด <s ๐‘›) โˆง ๐ด = ({๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))} |s {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))})) โ†’ ๐ด = ({๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))} |s {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}))
13 simpr 484 . . . . . 6 ((โˆƒ๐‘š โˆˆ โ„•s (( -us โ€˜๐‘š) <s ๐ต โˆง ๐ต <s ๐‘š) โˆง ๐ต = ({๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))} |s {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))})) โ†’ ๐ต = ({๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))} |s {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}))
1412, 13anim12i 612 . . . . 5 (((โˆƒ๐‘› โˆˆ โ„•s (( -us โ€˜๐‘›) <s ๐ด โˆง ๐ด <s ๐‘›) โˆง ๐ด = ({๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))} |s {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))})) โˆง (โˆƒ๐‘š โˆˆ โ„•s (( -us โ€˜๐‘š) <s ๐ต โˆง ๐ต <s ๐‘š) โˆง ๐ต = ({๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))} |s {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}))) โ†’ (๐ด = ({๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))} |s {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}) โˆง ๐ต = ({๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))} |s {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))})))
15 recut 28223 . . . . . . . . 9 (๐ด โˆˆ No โ†’ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))} <<s {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))})
1615adantr 480 . . . . . . . 8 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))} <<s {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))})
1716adantr 480 . . . . . . 7 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง (๐ด = ({๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))} |s {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}) โˆง ๐ต = ({๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))} |s {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}))) โ†’ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))} <<s {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))})
18 recut 28223 . . . . . . . 8 (๐ต โˆˆ No โ†’ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))} <<s {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))})
1918ad2antlr 726 . . . . . . 7 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง (๐ด = ({๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))} |s {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}) โˆง ๐ต = ({๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))} |s {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}))) โ†’ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))} <<s {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))})
20 simprl 770 . . . . . . 7 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง (๐ด = ({๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))} |s {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}) โˆง ๐ต = ({๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))} |s {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}))) โ†’ ๐ด = ({๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))} |s {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}))
21 simprr 772 . . . . . . 7 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง (๐ด = ({๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))} |s {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}) โˆง ๐ต = ({๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))} |s {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}))) โ†’ ๐ต = ({๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))} |s {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}))
2217, 19, 20, 21mulsunif2 28069 . . . . . 6 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง (๐ด = ({๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))} |s {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}) โˆง ๐ต = ({๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))} |s {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}))) โ†’ (๐ด ยทs ๐ต) = (({๐‘ง โˆฃ โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐‘ก) ยทs (๐ต -s ๐‘ข)))} โˆช {๐‘ง โˆฃ โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐‘ก -s ๐ด) ยทs (๐‘ข -s ๐ต)))}) |s ({๐‘ง โˆฃ โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐‘ก) ยทs (๐‘ข -s ๐ต)))} โˆช {๐‘ง โˆฃ โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐‘ก -s ๐ด) ยทs (๐ต -s ๐‘ข)))})))
23 r19.41v 3185 . . . . . . . . . . . . . 14 (โˆƒ๐‘› โˆˆ โ„•s (๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐‘ก) ยทs (๐ต -s ๐‘ข)))) โ†” (โˆƒ๐‘› โˆˆ โ„•s ๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐‘ก) ยทs (๐ต -s ๐‘ข)))))
2423exbii 1843 . . . . . . . . . . . . 13 (โˆƒ๐‘กโˆƒ๐‘› โˆˆ โ„•s (๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐‘ก) ยทs (๐ต -s ๐‘ข)))) โ†” โˆƒ๐‘ก(โˆƒ๐‘› โˆˆ โ„•s ๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐‘ก) ยทs (๐ต -s ๐‘ข)))))
25 rexcom4 3282 . . . . . . . . . . . . 13 (โˆƒ๐‘› โˆˆ โ„•s โˆƒ๐‘ก(๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐‘ก) ยทs (๐ต -s ๐‘ข)))) โ†” โˆƒ๐‘กโˆƒ๐‘› โˆˆ โ„•s (๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐‘ก) ยทs (๐ต -s ๐‘ข)))))
26 eqeq1 2732 . . . . . . . . . . . . . . 15 (๐‘ฅ = ๐‘ก โ†’ (๐‘ฅ = (๐ด -s ( 1s /su ๐‘›)) โ†” ๐‘ก = (๐ด -s ( 1s /su ๐‘›))))
2726rexbidv 3175 . . . . . . . . . . . . . 14 (๐‘ฅ = ๐‘ก โ†’ (โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›)) โ†” โˆƒ๐‘› โˆˆ โ„•s ๐‘ก = (๐ด -s ( 1s /su ๐‘›))))
2827rexab 3689 . . . . . . . . . . . . 13 (โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐‘ก) ยทs (๐ต -s ๐‘ข))) โ†” โˆƒ๐‘ก(โˆƒ๐‘› โˆˆ โ„•s ๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐‘ก) ยทs (๐ต -s ๐‘ข)))))
2924, 25, 283bitr4ri 304 . . . . . . . . . . . 12 (โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐‘ก) ยทs (๐ต -s ๐‘ข))) โ†” โˆƒ๐‘› โˆˆ โ„•s โˆƒ๐‘ก(๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐‘ก) ยทs (๐ต -s ๐‘ข)))))
30 ovex 7453 . . . . . . . . . . . . . . . . 17 (๐ด -s ( 1s /su ๐‘›)) โˆˆ V
31 oveq2 7428 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โ†’ (๐ด -s ๐‘ก) = (๐ด -s (๐ด -s ( 1s /su ๐‘›))))
3231oveq1d 7435 . . . . . . . . . . . . . . . . . . . 20 (๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โ†’ ((๐ด -s ๐‘ก) ยทs (๐ต -s ๐‘ข)) = ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s ๐‘ข)))
3332oveq2d 7436 . . . . . . . . . . . . . . . . . . 19 (๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โ†’ ((๐ด ยทs ๐ต) -s ((๐ด -s ๐‘ก) ยทs (๐ต -s ๐‘ข))) = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s ๐‘ข))))
3433eqeq2d 2739 . . . . . . . . . . . . . . . . . 18 (๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โ†’ (๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐‘ก) ยทs (๐ต -s ๐‘ข))) โ†” ๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s ๐‘ข)))))
3534rexbidv 3175 . . . . . . . . . . . . . . . . 17 (๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โ†’ (โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐‘ก) ยทs (๐ต -s ๐‘ข))) โ†” โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s ๐‘ข)))))
3630, 35ceqsexv 3523 . . . . . . . . . . . . . . . 16 (โˆƒ๐‘ก(๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐‘ก) ยทs (๐ต -s ๐‘ข)))) โ†” โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s ๐‘ข))))
37 r19.41v 3185 . . . . . . . . . . . . . . . . . 18 (โˆƒ๐‘š โˆˆ โ„•s (๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s ๐‘ข)))) โ†” (โˆƒ๐‘š โˆˆ โ„•s ๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s ๐‘ข)))))
3837exbii 1843 . . . . . . . . . . . . . . . . 17 (โˆƒ๐‘ขโˆƒ๐‘š โˆˆ โ„•s (๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s ๐‘ข)))) โ†” โˆƒ๐‘ข(โˆƒ๐‘š โˆˆ โ„•s ๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s ๐‘ข)))))
39 rexcom4 3282 . . . . . . . . . . . . . . . . 17 (โˆƒ๐‘š โˆˆ โ„•s โˆƒ๐‘ข(๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s ๐‘ข)))) โ†” โˆƒ๐‘ขโˆƒ๐‘š โˆˆ โ„•s (๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s ๐‘ข)))))
40 eqeq1 2732 . . . . . . . . . . . . . . . . . . 19 (๐‘ฆ = ๐‘ข โ†’ (๐‘ฆ = (๐ต -s ( 1s /su ๐‘š)) โ†” ๐‘ข = (๐ต -s ( 1s /su ๐‘š))))
4140rexbidv 3175 . . . . . . . . . . . . . . . . . 18 (๐‘ฆ = ๐‘ข โ†’ (โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š)) โ†” โˆƒ๐‘š โˆˆ โ„•s ๐‘ข = (๐ต -s ( 1s /su ๐‘š))))
4241rexab 3689 . . . . . . . . . . . . . . . . 17 (โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s ๐‘ข))) โ†” โˆƒ๐‘ข(โˆƒ๐‘š โˆˆ โ„•s ๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s ๐‘ข)))))
4338, 39, 423bitr4ri 304 . . . . . . . . . . . . . . . 16 (โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s ๐‘ข))) โ†” โˆƒ๐‘š โˆˆ โ„•s โˆƒ๐‘ข(๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s ๐‘ข)))))
4436, 43bitri 275 . . . . . . . . . . . . . . 15 (โˆƒ๐‘ก(๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐‘ก) ยทs (๐ต -s ๐‘ข)))) โ†” โˆƒ๐‘š โˆˆ โ„•s โˆƒ๐‘ข(๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s ๐‘ข)))))
45 ovex 7453 . . . . . . . . . . . . . . . . . 18 (๐ต -s ( 1s /su ๐‘š)) โˆˆ V
46 oveq2 7428 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โ†’ (๐ต -s ๐‘ข) = (๐ต -s (๐ต -s ( 1s /su ๐‘š))))
4746oveq2d 7436 . . . . . . . . . . . . . . . . . . . 20 (๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โ†’ ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s ๐‘ข)) = ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s (๐ต -s ( 1s /su ๐‘š)))))
4847oveq2d 7436 . . . . . . . . . . . . . . . . . . 19 (๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โ†’ ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s ๐‘ข))) = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s (๐ต -s ( 1s /su ๐‘š))))))
4948eqeq2d 2739 . . . . . . . . . . . . . . . . . 18 (๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โ†’ (๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s ๐‘ข))) โ†” ๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s (๐ต -s ( 1s /su ๐‘š)))))))
5045, 49ceqsexv 3523 . . . . . . . . . . . . . . . . 17 (โˆƒ๐‘ข(๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s ๐‘ข)))) โ†” ๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s (๐ต -s ( 1s /su ๐‘š))))))
51 simplll 774 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ ๐ด โˆˆ No )
52 1sno 27759 . . . . . . . . . . . . . . . . . . . . . . 23 1s โˆˆ No
5352a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ 1s โˆˆ No )
54 nnsno 28195 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘› โˆˆ โ„•s โ†’ ๐‘› โˆˆ No )
5554ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ ๐‘› โˆˆ No )
56 nnne0s 28204 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘› โˆˆ โ„•s โ†’ ๐‘› โ‰  0s )
5756ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ ๐‘› โ‰  0s )
5853, 55, 57divscld 28121 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ ( 1s /su ๐‘›) โˆˆ No )
5951, 58nncansd 28002 . . . . . . . . . . . . . . . . . . . 20 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ (๐ด -s (๐ด -s ( 1s /su ๐‘›))) = ( 1s /su ๐‘›))
60 simpllr 775 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ ๐ต โˆˆ No )
61 nnsno 28195 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘š โˆˆ โ„•s โ†’ ๐‘š โˆˆ No )
6261adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ ๐‘š โˆˆ No )
63 nnne0s 28204 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘š โˆˆ โ„•s โ†’ ๐‘š โ‰  0s )
6463adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ ๐‘š โ‰  0s )
6553, 62, 64divscld 28121 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ ( 1s /su ๐‘š) โˆˆ No )
6660, 65nncansd 28002 . . . . . . . . . . . . . . . . . . . 20 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ (๐ต -s (๐ต -s ( 1s /su ๐‘š))) = ( 1s /su ๐‘š))
6759, 66oveq12d 7438 . . . . . . . . . . . . . . . . . . 19 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s (๐ต -s ( 1s /su ๐‘š)))) = (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š)))
6867oveq2d 7436 . . . . . . . . . . . . . . . . . 18 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s (๐ต -s ( 1s /su ๐‘š))))) = ((๐ด ยทs ๐ต) -s (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š))))
6968eqeq2d 2739 . . . . . . . . . . . . . . . . 17 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ (๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s (๐ต -s ( 1s /su ๐‘š))))) โ†” ๐‘ง = ((๐ด ยทs ๐ต) -s (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š)))))
7050, 69bitrid 283 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ (โˆƒ๐‘ข(๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s ๐‘ข)))) โ†” ๐‘ง = ((๐ด ยทs ๐ต) -s (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š)))))
7170rexbidva 3173 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โ†’ (โˆƒ๐‘š โˆˆ โ„•s โˆƒ๐‘ข(๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s ๐‘ข)))) โ†” โˆƒ๐‘š โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š)))))
7244, 71bitrid 283 . . . . . . . . . . . . . 14 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โ†’ (โˆƒ๐‘ก(๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐‘ก) ยทs (๐ต -s ๐‘ข)))) โ†” โˆƒ๐‘š โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š)))))
7372rexbidva 3173 . . . . . . . . . . . . 13 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ (โˆƒ๐‘› โˆˆ โ„•s โˆƒ๐‘ก(๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐‘ก) ยทs (๐ต -s ๐‘ข)))) โ†” โˆƒ๐‘› โˆˆ โ„•s โˆƒ๐‘š โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š)))))
74 remulscllem1 28227 . . . . . . . . . . . . 13 (โˆƒ๐‘› โˆˆ โ„•s โˆƒ๐‘š โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š))) โ†” โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s ( 1s /su ๐‘)))
7573, 74bitrdi 287 . . . . . . . . . . . 12 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ (โˆƒ๐‘› โˆˆ โ„•s โˆƒ๐‘ก(๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐‘ก) ยทs (๐ต -s ๐‘ข)))) โ†” โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s ( 1s /su ๐‘))))
7629, 75bitrid 283 . . . . . . . . . . 11 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ (โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐‘ก) ยทs (๐ต -s ๐‘ข))) โ†” โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s ( 1s /su ๐‘))))
7776abbidv 2797 . . . . . . . . . 10 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ {๐‘ง โˆฃ โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐‘ก) ยทs (๐ต -s ๐‘ข)))} = {๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s ( 1s /su ๐‘))})
78 r19.41v 3185 . . . . . . . . . . . . . 14 (โˆƒ๐‘› โˆˆ โ„•s (๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐‘ก -s ๐ด) ยทs (๐‘ข -s ๐ต)))) โ†” (โˆƒ๐‘› โˆˆ โ„•s ๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐‘ก -s ๐ด) ยทs (๐‘ข -s ๐ต)))))
7978exbii 1843 . . . . . . . . . . . . 13 (โˆƒ๐‘กโˆƒ๐‘› โˆˆ โ„•s (๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐‘ก -s ๐ด) ยทs (๐‘ข -s ๐ต)))) โ†” โˆƒ๐‘ก(โˆƒ๐‘› โˆˆ โ„•s ๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐‘ก -s ๐ด) ยทs (๐‘ข -s ๐ต)))))
80 rexcom4 3282 . . . . . . . . . . . . 13 (โˆƒ๐‘› โˆˆ โ„•s โˆƒ๐‘ก(๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐‘ก -s ๐ด) ยทs (๐‘ข -s ๐ต)))) โ†” โˆƒ๐‘กโˆƒ๐‘› โˆˆ โ„•s (๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐‘ก -s ๐ด) ยทs (๐‘ข -s ๐ต)))))
81 eqeq1 2732 . . . . . . . . . . . . . . 15 (๐‘ฅ = ๐‘ก โ†’ (๐‘ฅ = (๐ด +s ( 1s /su ๐‘›)) โ†” ๐‘ก = (๐ด +s ( 1s /su ๐‘›))))
8281rexbidv 3175 . . . . . . . . . . . . . 14 (๐‘ฅ = ๐‘ก โ†’ (โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›)) โ†” โˆƒ๐‘› โˆˆ โ„•s ๐‘ก = (๐ด +s ( 1s /su ๐‘›))))
8382rexab 3689 . . . . . . . . . . . . 13 (โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐‘ก -s ๐ด) ยทs (๐‘ข -s ๐ต))) โ†” โˆƒ๐‘ก(โˆƒ๐‘› โˆˆ โ„•s ๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐‘ก -s ๐ด) ยทs (๐‘ข -s ๐ต)))))
8479, 80, 833bitr4ri 304 . . . . . . . . . . . 12 (โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐‘ก -s ๐ด) ยทs (๐‘ข -s ๐ต))) โ†” โˆƒ๐‘› โˆˆ โ„•s โˆƒ๐‘ก(๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐‘ก -s ๐ด) ยทs (๐‘ข -s ๐ต)))))
85 ovex 7453 . . . . . . . . . . . . . . . . 17 (๐ด +s ( 1s /su ๐‘›)) โˆˆ V
86 oveq1 7427 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โ†’ (๐‘ก -s ๐ด) = ((๐ด +s ( 1s /su ๐‘›)) -s ๐ด))
8786oveq1d 7435 . . . . . . . . . . . . . . . . . . . 20 (๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โ†’ ((๐‘ก -s ๐ด) ยทs (๐‘ข -s ๐ต)) = (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐‘ข -s ๐ต)))
8887oveq2d 7436 . . . . . . . . . . . . . . . . . . 19 (๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โ†’ ((๐ด ยทs ๐ต) -s ((๐‘ก -s ๐ด) ยทs (๐‘ข -s ๐ต))) = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐‘ข -s ๐ต))))
8988eqeq2d 2739 . . . . . . . . . . . . . . . . . 18 (๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โ†’ (๐‘ง = ((๐ด ยทs ๐ต) -s ((๐‘ก -s ๐ด) ยทs (๐‘ข -s ๐ต))) โ†” ๐‘ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐‘ข -s ๐ต)))))
9089rexbidv 3175 . . . . . . . . . . . . . . . . 17 (๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โ†’ (โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐‘ก -s ๐ด) ยทs (๐‘ข -s ๐ต))) โ†” โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐‘ข -s ๐ต)))))
9185, 90ceqsexv 3523 . . . . . . . . . . . . . . . 16 (โˆƒ๐‘ก(๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐‘ก -s ๐ด) ยทs (๐‘ข -s ๐ต)))) โ†” โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐‘ข -s ๐ต))))
92 r19.41v 3185 . . . . . . . . . . . . . . . . . 18 (โˆƒ๐‘š โˆˆ โ„•s (๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐‘ข -s ๐ต)))) โ†” (โˆƒ๐‘š โˆˆ โ„•s ๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐‘ข -s ๐ต)))))
9392exbii 1843 . . . . . . . . . . . . . . . . 17 (โˆƒ๐‘ขโˆƒ๐‘š โˆˆ โ„•s (๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐‘ข -s ๐ต)))) โ†” โˆƒ๐‘ข(โˆƒ๐‘š โˆˆ โ„•s ๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐‘ข -s ๐ต)))))
94 rexcom4 3282 . . . . . . . . . . . . . . . . 17 (โˆƒ๐‘š โˆˆ โ„•s โˆƒ๐‘ข(๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐‘ข -s ๐ต)))) โ†” โˆƒ๐‘ขโˆƒ๐‘š โˆˆ โ„•s (๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐‘ข -s ๐ต)))))
95 eqeq1 2732 . . . . . . . . . . . . . . . . . . 19 (๐‘ฆ = ๐‘ข โ†’ (๐‘ฆ = (๐ต +s ( 1s /su ๐‘š)) โ†” ๐‘ข = (๐ต +s ( 1s /su ๐‘š))))
9695rexbidv 3175 . . . . . . . . . . . . . . . . . 18 (๐‘ฆ = ๐‘ข โ†’ (โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š)) โ†” โˆƒ๐‘š โˆˆ โ„•s ๐‘ข = (๐ต +s ( 1s /su ๐‘š))))
9796rexab 3689 . . . . . . . . . . . . . . . . 17 (โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐‘ข -s ๐ต))) โ†” โˆƒ๐‘ข(โˆƒ๐‘š โˆˆ โ„•s ๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐‘ข -s ๐ต)))))
9893, 94, 973bitr4ri 304 . . . . . . . . . . . . . . . 16 (โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐‘ข -s ๐ต))) โ†” โˆƒ๐‘š โˆˆ โ„•s โˆƒ๐‘ข(๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐‘ข -s ๐ต)))))
9991, 98bitri 275 . . . . . . . . . . . . . . 15 (โˆƒ๐‘ก(๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐‘ก -s ๐ด) ยทs (๐‘ข -s ๐ต)))) โ†” โˆƒ๐‘š โˆˆ โ„•s โˆƒ๐‘ข(๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐‘ข -s ๐ต)))))
100 ovex 7453 . . . . . . . . . . . . . . . . . 18 (๐ต +s ( 1s /su ๐‘š)) โˆˆ V
101 oveq1 7427 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โ†’ (๐‘ข -s ๐ต) = ((๐ต +s ( 1s /su ๐‘š)) -s ๐ต))
102101oveq2d 7436 . . . . . . . . . . . . . . . . . . . 20 (๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โ†’ (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐‘ข -s ๐ต)) = (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs ((๐ต +s ( 1s /su ๐‘š)) -s ๐ต)))
103102oveq2d 7436 . . . . . . . . . . . . . . . . . . 19 (๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โ†’ ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐‘ข -s ๐ต))) = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs ((๐ต +s ( 1s /su ๐‘š)) -s ๐ต))))
104103eqeq2d 2739 . . . . . . . . . . . . . . . . . 18 (๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โ†’ (๐‘ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐‘ข -s ๐ต))) โ†” ๐‘ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs ((๐ต +s ( 1s /su ๐‘š)) -s ๐ต)))))
105100, 104ceqsexv 3523 . . . . . . . . . . . . . . . . 17 (โˆƒ๐‘ข(๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐‘ข -s ๐ต)))) โ†” ๐‘ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs ((๐ต +s ( 1s /su ๐‘š)) -s ๐ต))))
106 pncan2s 27981 . . . . . . . . . . . . . . . . . . . . 21 ((๐ด โˆˆ No โˆง ( 1s /su ๐‘›) โˆˆ No ) โ†’ ((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) = ( 1s /su ๐‘›))
10751, 58, 106syl2anc 583 . . . . . . . . . . . . . . . . . . . 20 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ ((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) = ( 1s /su ๐‘›))
108 pncan2s 27981 . . . . . . . . . . . . . . . . . . . . 21 ((๐ต โˆˆ No โˆง ( 1s /su ๐‘š) โˆˆ No ) โ†’ ((๐ต +s ( 1s /su ๐‘š)) -s ๐ต) = ( 1s /su ๐‘š))
10960, 65, 108syl2anc 583 . . . . . . . . . . . . . . . . . . . 20 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ ((๐ต +s ( 1s /su ๐‘š)) -s ๐ต) = ( 1s /su ๐‘š))
110107, 109oveq12d 7438 . . . . . . . . . . . . . . . . . . 19 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs ((๐ต +s ( 1s /su ๐‘š)) -s ๐ต)) = (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š)))
111110oveq2d 7436 . . . . . . . . . . . . . . . . . 18 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs ((๐ต +s ( 1s /su ๐‘š)) -s ๐ต))) = ((๐ด ยทs ๐ต) -s (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š))))
112111eqeq2d 2739 . . . . . . . . . . . . . . . . 17 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ (๐‘ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs ((๐ต +s ( 1s /su ๐‘š)) -s ๐ต))) โ†” ๐‘ง = ((๐ด ยทs ๐ต) -s (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š)))))
113105, 112bitrid 283 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ (โˆƒ๐‘ข(๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐‘ข -s ๐ต)))) โ†” ๐‘ง = ((๐ด ยทs ๐ต) -s (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š)))))
114113rexbidva 3173 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โ†’ (โˆƒ๐‘š โˆˆ โ„•s โˆƒ๐‘ข(๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐‘ข -s ๐ต)))) โ†” โˆƒ๐‘š โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š)))))
11599, 114bitrid 283 . . . . . . . . . . . . . 14 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โ†’ (โˆƒ๐‘ก(๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐‘ก -s ๐ด) ยทs (๐‘ข -s ๐ต)))) โ†” โˆƒ๐‘š โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š)))))
116115rexbidva 3173 . . . . . . . . . . . . 13 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ (โˆƒ๐‘› โˆˆ โ„•s โˆƒ๐‘ก(๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐‘ก -s ๐ด) ยทs (๐‘ข -s ๐ต)))) โ†” โˆƒ๐‘› โˆˆ โ„•s โˆƒ๐‘š โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š)))))
117116, 74bitrdi 287 . . . . . . . . . . . 12 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ (โˆƒ๐‘› โˆˆ โ„•s โˆƒ๐‘ก(๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐‘ก -s ๐ด) ยทs (๐‘ข -s ๐ต)))) โ†” โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s ( 1s /su ๐‘))))
11884, 117bitrid 283 . . . . . . . . . . 11 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ (โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐‘ก -s ๐ด) ยทs (๐‘ข -s ๐ต))) โ†” โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s ( 1s /su ๐‘))))
119118abbidv 2797 . . . . . . . . . 10 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ {๐‘ง โˆฃ โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐‘ก -s ๐ด) ยทs (๐‘ข -s ๐ต)))} = {๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s ( 1s /su ๐‘))})
12077, 119uneq12d 4163 . . . . . . . . 9 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ ({๐‘ง โˆฃ โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐‘ก) ยทs (๐ต -s ๐‘ข)))} โˆช {๐‘ง โˆฃ โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐‘ก -s ๐ด) ยทs (๐‘ข -s ๐ต)))}) = ({๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s ( 1s /su ๐‘))} โˆช {๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s ( 1s /su ๐‘))}))
121 unidm 4151 . . . . . . . . 9 ({๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s ( 1s /su ๐‘))} โˆช {๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s ( 1s /su ๐‘))}) = {๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s ( 1s /su ๐‘))}
122120, 121eqtrdi 2784 . . . . . . . 8 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ ({๐‘ง โˆฃ โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐‘ก) ยทs (๐ต -s ๐‘ข)))} โˆช {๐‘ง โˆฃ โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐‘ก -s ๐ด) ยทs (๐‘ข -s ๐ต)))}) = {๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s ( 1s /su ๐‘))})
123 r19.41v 3185 . . . . . . . . . . . . . 14 (โˆƒ๐‘› โˆˆ โ„•s (๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐‘ก) ยทs (๐‘ข -s ๐ต)))) โ†” (โˆƒ๐‘› โˆˆ โ„•s ๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐‘ก) ยทs (๐‘ข -s ๐ต)))))
124123exbii 1843 . . . . . . . . . . . . 13 (โˆƒ๐‘กโˆƒ๐‘› โˆˆ โ„•s (๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐‘ก) ยทs (๐‘ข -s ๐ต)))) โ†” โˆƒ๐‘ก(โˆƒ๐‘› โˆˆ โ„•s ๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐‘ก) ยทs (๐‘ข -s ๐ต)))))
125 rexcom4 3282 . . . . . . . . . . . . 13 (โˆƒ๐‘› โˆˆ โ„•s โˆƒ๐‘ก(๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐‘ก) ยทs (๐‘ข -s ๐ต)))) โ†” โˆƒ๐‘กโˆƒ๐‘› โˆˆ โ„•s (๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐‘ก) ยทs (๐‘ข -s ๐ต)))))
12627rexab 3689 . . . . . . . . . . . . 13 (โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐‘ก) ยทs (๐‘ข -s ๐ต))) โ†” โˆƒ๐‘ก(โˆƒ๐‘› โˆˆ โ„•s ๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐‘ก) ยทs (๐‘ข -s ๐ต)))))
127124, 125, 1263bitr4ri 304 . . . . . . . . . . . 12 (โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐‘ก) ยทs (๐‘ข -s ๐ต))) โ†” โˆƒ๐‘› โˆˆ โ„•s โˆƒ๐‘ก(๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐‘ก) ยทs (๐‘ข -s ๐ต)))))
12831oveq1d 7435 . . . . . . . . . . . . . . . . . . . 20 (๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โ†’ ((๐ด -s ๐‘ก) ยทs (๐‘ข -s ๐ต)) = ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐‘ข -s ๐ต)))
129128oveq2d 7436 . . . . . . . . . . . . . . . . . . 19 (๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โ†’ ((๐ด ยทs ๐ต) +s ((๐ด -s ๐‘ก) ยทs (๐‘ข -s ๐ต))) = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐‘ข -s ๐ต))))
130129eqeq2d 2739 . . . . . . . . . . . . . . . . . 18 (๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โ†’ (๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐‘ก) ยทs (๐‘ข -s ๐ต))) โ†” ๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐‘ข -s ๐ต)))))
131130rexbidv 3175 . . . . . . . . . . . . . . . . 17 (๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โ†’ (โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐‘ก) ยทs (๐‘ข -s ๐ต))) โ†” โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐‘ข -s ๐ต)))))
13230, 131ceqsexv 3523 . . . . . . . . . . . . . . . 16 (โˆƒ๐‘ก(๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐‘ก) ยทs (๐‘ข -s ๐ต)))) โ†” โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐‘ข -s ๐ต))))
133 r19.41v 3185 . . . . . . . . . . . . . . . . . 18 (โˆƒ๐‘š โˆˆ โ„•s (๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐‘ข -s ๐ต)))) โ†” (โˆƒ๐‘š โˆˆ โ„•s ๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐‘ข -s ๐ต)))))
134133exbii 1843 . . . . . . . . . . . . . . . . 17 (โˆƒ๐‘ขโˆƒ๐‘š โˆˆ โ„•s (๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐‘ข -s ๐ต)))) โ†” โˆƒ๐‘ข(โˆƒ๐‘š โˆˆ โ„•s ๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐‘ข -s ๐ต)))))
135 rexcom4 3282 . . . . . . . . . . . . . . . . 17 (โˆƒ๐‘š โˆˆ โ„•s โˆƒ๐‘ข(๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐‘ข -s ๐ต)))) โ†” โˆƒ๐‘ขโˆƒ๐‘š โˆˆ โ„•s (๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐‘ข -s ๐ต)))))
13696rexab 3689 . . . . . . . . . . . . . . . . 17 (โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐‘ข -s ๐ต))) โ†” โˆƒ๐‘ข(โˆƒ๐‘š โˆˆ โ„•s ๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐‘ข -s ๐ต)))))
137134, 135, 1363bitr4ri 304 . . . . . . . . . . . . . . . 16 (โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐‘ข -s ๐ต))) โ†” โˆƒ๐‘š โˆˆ โ„•s โˆƒ๐‘ข(๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐‘ข -s ๐ต)))))
138132, 137bitri 275 . . . . . . . . . . . . . . 15 (โˆƒ๐‘ก(๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐‘ก) ยทs (๐‘ข -s ๐ต)))) โ†” โˆƒ๐‘š โˆˆ โ„•s โˆƒ๐‘ข(๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐‘ข -s ๐ต)))))
139101oveq2d 7436 . . . . . . . . . . . . . . . . . . . 20 (๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โ†’ ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐‘ข -s ๐ต)) = ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs ((๐ต +s ( 1s /su ๐‘š)) -s ๐ต)))
140139oveq2d 7436 . . . . . . . . . . . . . . . . . . 19 (๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โ†’ ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐‘ข -s ๐ต))) = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs ((๐ต +s ( 1s /su ๐‘š)) -s ๐ต))))
141140eqeq2d 2739 . . . . . . . . . . . . . . . . . 18 (๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โ†’ (๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐‘ข -s ๐ต))) โ†” ๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs ((๐ต +s ( 1s /su ๐‘š)) -s ๐ต)))))
142100, 141ceqsexv 3523 . . . . . . . . . . . . . . . . 17 (โˆƒ๐‘ข(๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐‘ข -s ๐ต)))) โ†” ๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs ((๐ต +s ( 1s /su ๐‘š)) -s ๐ต))))
14359, 109oveq12d 7438 . . . . . . . . . . . . . . . . . . 19 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs ((๐ต +s ( 1s /su ๐‘š)) -s ๐ต)) = (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š)))
144143oveq2d 7436 . . . . . . . . . . . . . . . . . 18 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs ((๐ต +s ( 1s /su ๐‘š)) -s ๐ต))) = ((๐ด ยทs ๐ต) +s (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š))))
145144eqeq2d 2739 . . . . . . . . . . . . . . . . 17 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ (๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs ((๐ต +s ( 1s /su ๐‘š)) -s ๐ต))) โ†” ๐‘ง = ((๐ด ยทs ๐ต) +s (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š)))))
146142, 145bitrid 283 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ (โˆƒ๐‘ข(๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐‘ข -s ๐ต)))) โ†” ๐‘ง = ((๐ด ยทs ๐ต) +s (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š)))))
147146rexbidva 3173 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โ†’ (โˆƒ๐‘š โˆˆ โ„•s โˆƒ๐‘ข(๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐‘ข -s ๐ต)))) โ†” โˆƒ๐‘š โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š)))))
148138, 147bitrid 283 . . . . . . . . . . . . . 14 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โ†’ (โˆƒ๐‘ก(๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐‘ก) ยทs (๐‘ข -s ๐ต)))) โ†” โˆƒ๐‘š โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š)))))
149148rexbidva 3173 . . . . . . . . . . . . 13 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ (โˆƒ๐‘› โˆˆ โ„•s โˆƒ๐‘ก(๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐‘ก) ยทs (๐‘ข -s ๐ต)))) โ†” โˆƒ๐‘› โˆˆ โ„•s โˆƒ๐‘š โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š)))))
150 remulscllem1 28227 . . . . . . . . . . . . 13 (โˆƒ๐‘› โˆˆ โ„•s โˆƒ๐‘š โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š))) โ†” โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s ( 1s /su ๐‘)))
151149, 150bitrdi 287 . . . . . . . . . . . 12 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ (โˆƒ๐‘› โˆˆ โ„•s โˆƒ๐‘ก(๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐‘ก) ยทs (๐‘ข -s ๐ต)))) โ†” โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s ( 1s /su ๐‘))))
152127, 151bitrid 283 . . . . . . . . . . 11 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ (โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐‘ก) ยทs (๐‘ข -s ๐ต))) โ†” โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s ( 1s /su ๐‘))))
153152abbidv 2797 . . . . . . . . . 10 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ {๐‘ง โˆฃ โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐‘ก) ยทs (๐‘ข -s ๐ต)))} = {๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s ( 1s /su ๐‘))})
154 r19.41v 3185 . . . . . . . . . . . . . 14 (โˆƒ๐‘› โˆˆ โ„•s (๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐‘ก -s ๐ด) ยทs (๐ต -s ๐‘ข)))) โ†” (โˆƒ๐‘› โˆˆ โ„•s ๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐‘ก -s ๐ด) ยทs (๐ต -s ๐‘ข)))))
155154exbii 1843 . . . . . . . . . . . . 13 (โˆƒ๐‘กโˆƒ๐‘› โˆˆ โ„•s (๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐‘ก -s ๐ด) ยทs (๐ต -s ๐‘ข)))) โ†” โˆƒ๐‘ก(โˆƒ๐‘› โˆˆ โ„•s ๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐‘ก -s ๐ด) ยทs (๐ต -s ๐‘ข)))))
156 rexcom4 3282 . . . . . . . . . . . . 13 (โˆƒ๐‘› โˆˆ โ„•s โˆƒ๐‘ก(๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐‘ก -s ๐ด) ยทs (๐ต -s ๐‘ข)))) โ†” โˆƒ๐‘กโˆƒ๐‘› โˆˆ โ„•s (๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐‘ก -s ๐ด) ยทs (๐ต -s ๐‘ข)))))
15782rexab 3689 . . . . . . . . . . . . 13 (โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐‘ก -s ๐ด) ยทs (๐ต -s ๐‘ข))) โ†” โˆƒ๐‘ก(โˆƒ๐‘› โˆˆ โ„•s ๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐‘ก -s ๐ด) ยทs (๐ต -s ๐‘ข)))))
158155, 156, 1573bitr4ri 304 . . . . . . . . . . . 12 (โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐‘ก -s ๐ด) ยทs (๐ต -s ๐‘ข))) โ†” โˆƒ๐‘› โˆˆ โ„•s โˆƒ๐‘ก(๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐‘ก -s ๐ด) ยทs (๐ต -s ๐‘ข)))))
15986oveq1d 7435 . . . . . . . . . . . . . . . . . . . 20 (๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โ†’ ((๐‘ก -s ๐ด) ยทs (๐ต -s ๐‘ข)) = (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s ๐‘ข)))
160159oveq2d 7436 . . . . . . . . . . . . . . . . . . 19 (๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โ†’ ((๐ด ยทs ๐ต) +s ((๐‘ก -s ๐ด) ยทs (๐ต -s ๐‘ข))) = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s ๐‘ข))))
161160eqeq2d 2739 . . . . . . . . . . . . . . . . . 18 (๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โ†’ (๐‘ง = ((๐ด ยทs ๐ต) +s ((๐‘ก -s ๐ด) ยทs (๐ต -s ๐‘ข))) โ†” ๐‘ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s ๐‘ข)))))
162161rexbidv 3175 . . . . . . . . . . . . . . . . 17 (๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โ†’ (โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐‘ก -s ๐ด) ยทs (๐ต -s ๐‘ข))) โ†” โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s ๐‘ข)))))
16385, 162ceqsexv 3523 . . . . . . . . . . . . . . . 16 (โˆƒ๐‘ก(๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐‘ก -s ๐ด) ยทs (๐ต -s ๐‘ข)))) โ†” โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s ๐‘ข))))
164 r19.41v 3185 . . . . . . . . . . . . . . . . . 18 (โˆƒ๐‘š โˆˆ โ„•s (๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s ๐‘ข)))) โ†” (โˆƒ๐‘š โˆˆ โ„•s ๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s ๐‘ข)))))
165164exbii 1843 . . . . . . . . . . . . . . . . 17 (โˆƒ๐‘ขโˆƒ๐‘š โˆˆ โ„•s (๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s ๐‘ข)))) โ†” โˆƒ๐‘ข(โˆƒ๐‘š โˆˆ โ„•s ๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s ๐‘ข)))))
166 rexcom4 3282 . . . . . . . . . . . . . . . . 17 (โˆƒ๐‘š โˆˆ โ„•s โˆƒ๐‘ข(๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s ๐‘ข)))) โ†” โˆƒ๐‘ขโˆƒ๐‘š โˆˆ โ„•s (๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s ๐‘ข)))))
16741rexab 3689 . . . . . . . . . . . . . . . . 17 (โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s ๐‘ข))) โ†” โˆƒ๐‘ข(โˆƒ๐‘š โˆˆ โ„•s ๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s ๐‘ข)))))
168165, 166, 1673bitr4ri 304 . . . . . . . . . . . . . . . 16 (โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s ๐‘ข))) โ†” โˆƒ๐‘š โˆˆ โ„•s โˆƒ๐‘ข(๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s ๐‘ข)))))
169163, 168bitri 275 . . . . . . . . . . . . . . 15 (โˆƒ๐‘ก(๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐‘ก -s ๐ด) ยทs (๐ต -s ๐‘ข)))) โ†” โˆƒ๐‘š โˆˆ โ„•s โˆƒ๐‘ข(๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s ๐‘ข)))))
17046oveq2d 7436 . . . . . . . . . . . . . . . . . . . 20 (๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โ†’ (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s ๐‘ข)) = (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s (๐ต -s ( 1s /su ๐‘š)))))
171170oveq2d 7436 . . . . . . . . . . . . . . . . . . 19 (๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โ†’ ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s ๐‘ข))) = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s (๐ต -s ( 1s /su ๐‘š))))))
172171eqeq2d 2739 . . . . . . . . . . . . . . . . . 18 (๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โ†’ (๐‘ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s ๐‘ข))) โ†” ๐‘ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s (๐ต -s ( 1s /su ๐‘š)))))))
17345, 172ceqsexv 3523 . . . . . . . . . . . . . . . . 17 (โˆƒ๐‘ข(๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s ๐‘ข)))) โ†” ๐‘ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s (๐ต -s ( 1s /su ๐‘š))))))
174107, 66oveq12d 7438 . . . . . . . . . . . . . . . . . . 19 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s (๐ต -s ( 1s /su ๐‘š)))) = (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š)))
175174oveq2d 7436 . . . . . . . . . . . . . . . . . 18 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s (๐ต -s ( 1s /su ๐‘š))))) = ((๐ด ยทs ๐ต) +s (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š))))
176175eqeq2d 2739 . . . . . . . . . . . . . . . . 17 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ (๐‘ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s (๐ต -s ( 1s /su ๐‘š))))) โ†” ๐‘ง = ((๐ด ยทs ๐ต) +s (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š)))))
177173, 176bitrid 283 . . . . . . . . . . . . . . . 16 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ (โˆƒ๐‘ข(๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s ๐‘ข)))) โ†” ๐‘ง = ((๐ด ยทs ๐ต) +s (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š)))))
178177rexbidva 3173 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โ†’ (โˆƒ๐‘š โˆˆ โ„•s โˆƒ๐‘ข(๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โˆง ๐‘ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s ๐‘ข)))) โ†” โˆƒ๐‘š โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š)))))
179169, 178bitrid 283 . . . . . . . . . . . . . 14 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โ†’ (โˆƒ๐‘ก(๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐‘ก -s ๐ด) ยทs (๐ต -s ๐‘ข)))) โ†” โˆƒ๐‘š โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š)))))
180179rexbidva 3173 . . . . . . . . . . . . 13 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ (โˆƒ๐‘› โˆˆ โ„•s โˆƒ๐‘ก(๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐‘ก -s ๐ด) ยทs (๐ต -s ๐‘ข)))) โ†” โˆƒ๐‘› โˆˆ โ„•s โˆƒ๐‘š โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š)))))
181180, 150bitrdi 287 . . . . . . . . . . . 12 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ (โˆƒ๐‘› โˆˆ โ„•s โˆƒ๐‘ก(๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โˆง โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐‘ก -s ๐ด) ยทs (๐ต -s ๐‘ข)))) โ†” โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s ( 1s /su ๐‘))))
182158, 181bitrid 283 . . . . . . . . . . 11 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ (โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐‘ก -s ๐ด) ยทs (๐ต -s ๐‘ข))) โ†” โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s ( 1s /su ๐‘))))
183182abbidv 2797 . . . . . . . . . 10 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ {๐‘ง โˆฃ โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐‘ก -s ๐ด) ยทs (๐ต -s ๐‘ข)))} = {๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s ( 1s /su ๐‘))})
184153, 183uneq12d 4163 . . . . . . . . 9 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ ({๐‘ง โˆฃ โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐‘ก) ยทs (๐‘ข -s ๐ต)))} โˆช {๐‘ง โˆฃ โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐‘ก -s ๐ด) ยทs (๐ต -s ๐‘ข)))}) = ({๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s ( 1s /su ๐‘))} โˆช {๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s ( 1s /su ๐‘))}))
185 unidm 4151 . . . . . . . . 9 ({๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s ( 1s /su ๐‘))} โˆช {๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s ( 1s /su ๐‘))}) = {๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s ( 1s /su ๐‘))}
186184, 185eqtrdi 2784 . . . . . . . 8 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ ({๐‘ง โˆฃ โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐‘ก) ยทs (๐‘ข -s ๐ต)))} โˆช {๐‘ง โˆฃ โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐‘ก -s ๐ด) ยทs (๐ต -s ๐‘ข)))}) = {๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s ( 1s /su ๐‘))})
187122, 186oveq12d 7438 . . . . . . 7 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ (({๐‘ง โˆฃ โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐‘ก) ยทs (๐ต -s ๐‘ข)))} โˆช {๐‘ง โˆฃ โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐‘ก -s ๐ด) ยทs (๐‘ข -s ๐ต)))}) |s ({๐‘ง โˆฃ โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐‘ก) ยทs (๐‘ข -s ๐ต)))} โˆช {๐‘ง โˆฃ โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐‘ก -s ๐ด) ยทs (๐ต -s ๐‘ข)))})) = ({๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s ( 1s /su ๐‘))} |s {๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s ( 1s /su ๐‘))}))
188187adantr 480 . . . . . 6 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง (๐ด = ({๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))} |s {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}) โˆง ๐ต = ({๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))} |s {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}))) โ†’ (({๐‘ง โˆฃ โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐‘ก) ยทs (๐ต -s ๐‘ข)))} โˆช {๐‘ง โˆฃ โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐‘ก -s ๐ด) ยทs (๐‘ข -s ๐ต)))}) |s ({๐‘ง โˆฃ โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐‘ก) ยทs (๐‘ข -s ๐ต)))} โˆช {๐‘ง โˆฃ โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐‘ก -s ๐ด) ยทs (๐ต -s ๐‘ข)))})) = ({๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s ( 1s /su ๐‘))} |s {๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s ( 1s /su ๐‘))}))
18922, 188eqtrd 2768 . . . . 5 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง (๐ด = ({๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))} |s {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}) โˆง ๐ต = ({๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))} |s {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}))) โ†’ (๐ด ยทs ๐ต) = ({๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s ( 1s /su ๐‘))} |s {๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s ( 1s /su ๐‘))}))
19014, 189sylan2 592 . . . 4 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ((โˆƒ๐‘› โˆˆ โ„•s (( -us โ€˜๐‘›) <s ๐ด โˆง ๐ด <s ๐‘›) โˆง ๐ด = ({๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))} |s {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))})) โˆง (โˆƒ๐‘š โˆˆ โ„•s (( -us โ€˜๐‘š) <s ๐ต โˆง ๐ต <s ๐‘š) โˆง ๐ต = ({๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))} |s {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))})))) โ†’ (๐ด ยทs ๐ต) = ({๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s ( 1s /su ๐‘))} |s {๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s ( 1s /su ๐‘))}))
1912, 11, 190jca32 515 . . 3 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ((โˆƒ๐‘› โˆˆ โ„•s (( -us โ€˜๐‘›) <s ๐ด โˆง ๐ด <s ๐‘›) โˆง ๐ด = ({๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))} |s {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))})) โˆง (โˆƒ๐‘š โˆˆ โ„•s (( -us โ€˜๐‘š) <s ๐ต โˆง ๐ต <s ๐‘š) โˆง ๐ต = ({๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))} |s {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))})))) โ†’ ((๐ด ยทs ๐ต) โˆˆ No โˆง (โˆƒ๐‘ โˆˆ โ„•s (( -us โ€˜๐‘) <s (๐ด ยทs ๐ต) โˆง (๐ด ยทs ๐ต) <s ๐‘) โˆง (๐ด ยทs ๐ต) = ({๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s ( 1s /su ๐‘))} |s {๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s ( 1s /su ๐‘))}))))
192191an4s 659 . 2 (((๐ด โˆˆ No โˆง (โˆƒ๐‘› โˆˆ โ„•s (( -us โ€˜๐‘›) <s ๐ด โˆง ๐ด <s ๐‘›) โˆง ๐ด = ({๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))} |s {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}))) โˆง (๐ต โˆˆ No โˆง (โˆƒ๐‘š โˆˆ โ„•s (( -us โ€˜๐‘š) <s ๐ต โˆง ๐ต <s ๐‘š) โˆง ๐ต = ({๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))} |s {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))})))) โ†’ ((๐ด ยทs ๐ต) โˆˆ No โˆง (โˆƒ๐‘ โˆˆ โ„•s (( -us โ€˜๐‘) <s (๐ด ยทs ๐ต) โˆง (๐ด ยทs ๐ต) <s ๐‘) โˆง (๐ด ยทs ๐ต) = ({๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s ( 1s /su ๐‘))} |s {๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s ( 1s /su ๐‘))}))))
193 elreno 28222 . . 3 (๐ด โˆˆ โ„s โ†” (๐ด โˆˆ No โˆง (โˆƒ๐‘› โˆˆ โ„•s (( -us โ€˜๐‘›) <s ๐ด โˆง ๐ด <s ๐‘›) โˆง ๐ด = ({๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))} |s {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}))))
194 elreno 28222 . . 3 (๐ต โˆˆ โ„s โ†” (๐ต โˆˆ No โˆง (โˆƒ๐‘š โˆˆ โ„•s (( -us โ€˜๐‘š) <s ๐ต โˆง ๐ต <s ๐‘š) โˆง ๐ต = ({๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))} |s {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}))))
195193, 194anbi12i 627 . 2 ((๐ด โˆˆ โ„s โˆง ๐ต โˆˆ โ„s) โ†” ((๐ด โˆˆ No โˆง (โˆƒ๐‘› โˆˆ โ„•s (( -us โ€˜๐‘›) <s ๐ด โˆง ๐ด <s ๐‘›) โˆง ๐ด = ({๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))} |s {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}))) โˆง (๐ต โˆˆ No โˆง (โˆƒ๐‘š โˆˆ โ„•s (( -us โ€˜๐‘š) <s ๐ต โˆง ๐ต <s ๐‘š) โˆง ๐ต = ({๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))} |s {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))})))))
196 elreno 28222 . 2 ((๐ด ยทs ๐ต) โˆˆ โ„s โ†” ((๐ด ยทs ๐ต) โˆˆ No โˆง (โˆƒ๐‘ โˆˆ โ„•s (( -us โ€˜๐‘) <s (๐ด ยทs ๐ต) โˆง (๐ด ยทs ๐ต) <s ๐‘) โˆง (๐ด ยทs ๐ต) = ({๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s ( 1s /su ๐‘))} |s {๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s ( 1s /su ๐‘))}))))
197192, 195, 1963imtr4i 292 1 ((๐ด โˆˆ โ„s โˆง ๐ต โˆˆ โ„s) โ†’ (๐ด ยทs ๐ต) โˆˆ โ„s)
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 395   = wceq 1534  โˆƒwex 1774   โˆˆ wcel 2099  {cab 2705   โ‰  wne 2937  โˆƒwrex 3067   โˆช cun 3945   class class class wbr 5148  โ€˜cfv 6548  (class class class)co 7420   No csur 27572   <s cslt 27573   <<s csslt 27712   |s cscut 27714   0s c0s 27754   1s c1s 27755   +s cadds 27875   -us cnegs 27931   -s csubs 27932   ยทs cmuls 28005   /su cdivs 28086  โ„•scnns 28185  โ„screno 28220
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740  ax-dc 10469
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3373  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-ot 4638  df-uni 4909  df-int 4950  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-se 5634  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6305  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-riota 7376  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7871  df-1st 7993  df-2nd 7994  df-frecs 8286  df-wrecs 8317  df-recs 8391  df-rdg 8430  df-1o 8486  df-2o 8487  df-oadd 8490  df-nadd 8686  df-no 27575  df-slt 27576  df-bday 27577  df-sle 27677  df-sslt 27713  df-scut 27715  df-0s 27756  df-1s 27757  df-made 27773  df-old 27774  df-left 27776  df-right 27777  df-norec 27854  df-norec2 27865  df-adds 27876  df-negs 27933  df-subs 27934  df-muls 28006  df-divs 28087  df-abss 28131  df-n0s 28186  df-nns 28187  df-reno 28221
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator