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

Theorem remulscl 28170
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 27974 . . . . 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 28169 . . . . . . 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 3203 . . . . 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 3218 . . . . . 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 28164 . . . . . . . . 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 28164 . . . . . . . 8 (๐ต โˆˆ No โ†’ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))} <<s {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))})
1918ad2antlr 724 . . . . . . 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 768 . . . . . . 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 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 ๐‘š))}))
2217, 19, 20, 21mulsunif2 28010 . . . . . 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 3180 . . . . . . . . . . . . . 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 1842 . . . . . . . . . . . . 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 3277 . . . . . . . . . . . . 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 2728 . . . . . . . . . . . . . . 15 (๐‘ฅ = ๐‘ก โ†’ (๐‘ฅ = (๐ด -s ( 1s /su ๐‘›)) โ†” ๐‘ก = (๐ด -s ( 1s /su ๐‘›))))
2726rexbidv 3170 . . . . . . . . . . . . . 14 (๐‘ฅ = ๐‘ก โ†’ (โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›)) โ†” โˆƒ๐‘› โˆˆ โ„•s ๐‘ก = (๐ด -s ( 1s /su ๐‘›))))
2827rexab 3683 . . . . . . . . . . . . 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 7435 . . . . . . . . . . . . . . . . 17 (๐ด -s ( 1s /su ๐‘›)) โˆˆ V
31 oveq2 7410 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โ†’ (๐ด -s ๐‘ก) = (๐ด -s (๐ด -s ( 1s /su ๐‘›))))
3231oveq1d 7417 . . . . . . . . . . . . . . . . . . . 20 (๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โ†’ ((๐ด -s ๐‘ก) ยทs (๐ต -s ๐‘ข)) = ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s ๐‘ข)))
3332oveq2d 7418 . . . . . . . . . . . . . . . . . . 19 (๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โ†’ ((๐ด ยทs ๐ต) -s ((๐ด -s ๐‘ก) ยทs (๐ต -s ๐‘ข))) = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s ๐‘ข))))
3433eqeq2d 2735 . . . . . . . . . . . . . . . . . 18 (๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โ†’ (๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐‘ก) ยทs (๐ต -s ๐‘ข))) โ†” ๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s ๐‘ข)))))
3534rexbidv 3170 . . . . . . . . . . . . . . . . 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 3518 . . . . . . . . . . . . . . . 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 3180 . . . . . . . . . . . . . . . . . 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 1842 . . . . . . . . . . . . . . . . 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 3277 . . . . . . . . . . . . . . . . 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 2728 . . . . . . . . . . . . . . . . . . 19 (๐‘ฆ = ๐‘ข โ†’ (๐‘ฆ = (๐ต -s ( 1s /su ๐‘š)) โ†” ๐‘ข = (๐ต -s ( 1s /su ๐‘š))))
4140rexbidv 3170 . . . . . . . . . . . . . . . . . 18 (๐‘ฆ = ๐‘ข โ†’ (โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š)) โ†” โˆƒ๐‘š โˆˆ โ„•s ๐‘ข = (๐ต -s ( 1s /su ๐‘š))))
4241rexab 3683 . . . . . . . . . . . . . . . . 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 7435 . . . . . . . . . . . . . . . . . 18 (๐ต -s ( 1s /su ๐‘š)) โˆˆ V
46 oveq2 7410 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โ†’ (๐ต -s ๐‘ข) = (๐ต -s (๐ต -s ( 1s /su ๐‘š))))
4746oveq2d 7418 . . . . . . . . . . . . . . . . . . . 20 (๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โ†’ ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s ๐‘ข)) = ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s (๐ต -s ( 1s /su ๐‘š)))))
4847oveq2d 7418 . . . . . . . . . . . . . . . . . . 19 (๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โ†’ ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s ๐‘ข))) = ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s (๐ต -s ( 1s /su ๐‘š))))))
4948eqeq2d 2735 . . . . . . . . . . . . . . . . . 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 3518 . . . . . . . . . . . . . . . . 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 772 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ ๐ด โˆˆ No )
52 1sno 27700 . . . . . . . . . . . . . . . . . . . . . . 23 1s โˆˆ No
5352a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ 1s โˆˆ No )
54 nnsno 28136 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘› โˆˆ โ„•s โ†’ ๐‘› โˆˆ No )
5554ad2antlr 724 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ ๐‘› โˆˆ No )
56 nnne0s 28145 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘› โˆˆ โ„•s โ†’ ๐‘› โ‰  0s )
5756ad2antlr 724 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ ๐‘› โ‰  0s )
5853, 55, 57divscld 28062 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ ( 1s /su ๐‘›) โˆˆ No )
5951, 58nncansd 27943 . . . . . . . . . . . . . . . . . . . 20 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ (๐ด -s (๐ด -s ( 1s /su ๐‘›))) = ( 1s /su ๐‘›))
60 simpllr 773 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ ๐ต โˆˆ No )
61 nnsno 28136 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘š โˆˆ โ„•s โ†’ ๐‘š โˆˆ No )
6261adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ ๐‘š โˆˆ No )
63 nnne0s 28145 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘š โˆˆ โ„•s โ†’ ๐‘š โ‰  0s )
6463adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ ๐‘š โ‰  0s )
6553, 62, 64divscld 28062 . . . . . . . . . . . . . . . . . . . . 21 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ ( 1s /su ๐‘š) โˆˆ No )
6660, 65nncansd 27943 . . . . . . . . . . . . . . . . . . . 20 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ (๐ต -s (๐ต -s ( 1s /su ๐‘š))) = ( 1s /su ๐‘š))
6759, 66oveq12d 7420 . . . . . . . . . . . . . . . . . . 19 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s (๐ต -s ( 1s /su ๐‘š)))) = (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š)))
6867oveq2d 7418 . . . . . . . . . . . . . . . . . 18 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ ((๐ด ยทs ๐ต) -s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐ต -s (๐ต -s ( 1s /su ๐‘š))))) = ((๐ด ยทs ๐ต) -s (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š))))
6968eqeq2d 2735 . . . . . . . . . . . . . . . . 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 3168 . . . . . . . . . . . . . . 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 3168 . . . . . . . . . . . . 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 28168 . . . . . . . . . . . . 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 2793 . . . . . . . . . 10 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ {๐‘ง โˆฃ โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐ด -s ๐‘ก) ยทs (๐ต -s ๐‘ข)))} = {๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s ( 1s /su ๐‘))})
78 r19.41v 3180 . . . . . . . . . . . . . 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 1842 . . . . . . . . . . . . 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 3277 . . . . . . . . . . . . 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 2728 . . . . . . . . . . . . . . 15 (๐‘ฅ = ๐‘ก โ†’ (๐‘ฅ = (๐ด +s ( 1s /su ๐‘›)) โ†” ๐‘ก = (๐ด +s ( 1s /su ๐‘›))))
8281rexbidv 3170 . . . . . . . . . . . . . 14 (๐‘ฅ = ๐‘ก โ†’ (โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›)) โ†” โˆƒ๐‘› โˆˆ โ„•s ๐‘ก = (๐ด +s ( 1s /su ๐‘›))))
8382rexab 3683 . . . . . . . . . . . . 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 7435 . . . . . . . . . . . . . . . . 17 (๐ด +s ( 1s /su ๐‘›)) โˆˆ V
86 oveq1 7409 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โ†’ (๐‘ก -s ๐ด) = ((๐ด +s ( 1s /su ๐‘›)) -s ๐ด))
8786oveq1d 7417 . . . . . . . . . . . . . . . . . . . 20 (๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โ†’ ((๐‘ก -s ๐ด) ยทs (๐‘ข -s ๐ต)) = (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐‘ข -s ๐ต)))
8887oveq2d 7418 . . . . . . . . . . . . . . . . . . 19 (๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โ†’ ((๐ด ยทs ๐ต) -s ((๐‘ก -s ๐ด) ยทs (๐‘ข -s ๐ต))) = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐‘ข -s ๐ต))))
8988eqeq2d 2735 . . . . . . . . . . . . . . . . . 18 (๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โ†’ (๐‘ง = ((๐ด ยทs ๐ต) -s ((๐‘ก -s ๐ด) ยทs (๐‘ข -s ๐ต))) โ†” ๐‘ง = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐‘ข -s ๐ต)))))
9089rexbidv 3170 . . . . . . . . . . . . . . . . 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 3518 . . . . . . . . . . . . . . . 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 3180 . . . . . . . . . . . . . . . . . 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 1842 . . . . . . . . . . . . . . . . 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 3277 . . . . . . . . . . . . . . . . 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 2728 . . . . . . . . . . . . . . . . . . 19 (๐‘ฆ = ๐‘ข โ†’ (๐‘ฆ = (๐ต +s ( 1s /su ๐‘š)) โ†” ๐‘ข = (๐ต +s ( 1s /su ๐‘š))))
9695rexbidv 3170 . . . . . . . . . . . . . . . . . 18 (๐‘ฆ = ๐‘ข โ†’ (โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š)) โ†” โˆƒ๐‘š โˆˆ โ„•s ๐‘ข = (๐ต +s ( 1s /su ๐‘š))))
9796rexab 3683 . . . . . . . . . . . . . . . . 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 7435 . . . . . . . . . . . . . . . . . 18 (๐ต +s ( 1s /su ๐‘š)) โˆˆ V
101 oveq1 7409 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โ†’ (๐‘ข -s ๐ต) = ((๐ต +s ( 1s /su ๐‘š)) -s ๐ต))
102101oveq2d 7418 . . . . . . . . . . . . . . . . . . . 20 (๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โ†’ (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐‘ข -s ๐ต)) = (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs ((๐ต +s ( 1s /su ๐‘š)) -s ๐ต)))
103102oveq2d 7418 . . . . . . . . . . . . . . . . . . 19 (๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โ†’ ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐‘ข -s ๐ต))) = ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs ((๐ต +s ( 1s /su ๐‘š)) -s ๐ต))))
104103eqeq2d 2735 . . . . . . . . . . . . . . . . . 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 3518 . . . . . . . . . . . . . . . . 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 27922 . . . . . . . . . . . . . . . . . . . . 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 27922 . . . . . . . . . . . . . . . . . . . . 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 7420 . . . . . . . . . . . . . . . . . . 19 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs ((๐ต +s ( 1s /su ๐‘š)) -s ๐ต)) = (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š)))
111110oveq2d 7418 . . . . . . . . . . . . . . . . . 18 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ ((๐ด ยทs ๐ต) -s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs ((๐ต +s ( 1s /su ๐‘š)) -s ๐ต))) = ((๐ด ยทs ๐ต) -s (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š))))
112111eqeq2d 2735 . . . . . . . . . . . . . . . . 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 3168 . . . . . . . . . . . . . . 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 3168 . . . . . . . . . . . . 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 2793 . . . . . . . . . 10 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ {๐‘ง โˆฃ โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) -s ((๐‘ก -s ๐ด) ยทs (๐‘ข -s ๐ต)))} = {๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s ( 1s /su ๐‘))})
12077, 119uneq12d 4157 . . . . . . . . 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 4145 . . . . . . . . 9 ({๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s ( 1s /su ๐‘))} โˆช {๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s ( 1s /su ๐‘))}) = {๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) -s ( 1s /su ๐‘))}
122120, 121eqtrdi 2780 . . . . . . . 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 3180 . . . . . . . . . . . . . 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 1842 . . . . . . . . . . . . 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 3277 . . . . . . . . . . . . 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 3683 . . . . . . . . . . . . 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 7417 . . . . . . . . . . . . . . . . . . . 20 (๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โ†’ ((๐ด -s ๐‘ก) ยทs (๐‘ข -s ๐ต)) = ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐‘ข -s ๐ต)))
129128oveq2d 7418 . . . . . . . . . . . . . . . . . . 19 (๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โ†’ ((๐ด ยทs ๐ต) +s ((๐ด -s ๐‘ก) ยทs (๐‘ข -s ๐ต))) = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐‘ข -s ๐ต))))
130129eqeq2d 2735 . . . . . . . . . . . . . . . . . 18 (๐‘ก = (๐ด -s ( 1s /su ๐‘›)) โ†’ (๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐‘ก) ยทs (๐‘ข -s ๐ต))) โ†” ๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐‘ข -s ๐ต)))))
131130rexbidv 3170 . . . . . . . . . . . . . . . . 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 3518 . . . . . . . . . . . . . . . 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 3180 . . . . . . . . . . . . . . . . . 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 1842 . . . . . . . . . . . . . . . . 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 3277 . . . . . . . . . . . . . . . . 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 3683 . . . . . . . . . . . . . . . . 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 7418 . . . . . . . . . . . . . . . . . . . 20 (๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โ†’ ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐‘ข -s ๐ต)) = ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs ((๐ต +s ( 1s /su ๐‘š)) -s ๐ต)))
140139oveq2d 7418 . . . . . . . . . . . . . . . . . . 19 (๐‘ข = (๐ต +s ( 1s /su ๐‘š)) โ†’ ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs (๐‘ข -s ๐ต))) = ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs ((๐ต +s ( 1s /su ๐‘š)) -s ๐ต))))
141140eqeq2d 2735 . . . . . . . . . . . . . . . . . 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 3518 . . . . . . . . . . . . . . . . 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 7420 . . . . . . . . . . . . . . . . . . 19 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs ((๐ต +s ( 1s /su ๐‘š)) -s ๐ต)) = (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š)))
144143oveq2d 7418 . . . . . . . . . . . . . . . . . 18 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ ((๐ด ยทs ๐ต) +s ((๐ด -s (๐ด -s ( 1s /su ๐‘›))) ยทs ((๐ต +s ( 1s /su ๐‘š)) -s ๐ต))) = ((๐ด ยทs ๐ต) +s (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š))))
145144eqeq2d 2735 . . . . . . . . . . . . . . . . 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 3168 . . . . . . . . . . . . . . 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 3168 . . . . . . . . . . . . 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 28168 . . . . . . . . . . . . 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 2793 . . . . . . . . . 10 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ {๐‘ง โˆฃ โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐ด -s ๐‘ก) ยทs (๐‘ข -s ๐ต)))} = {๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s ( 1s /su ๐‘))})
154 r19.41v 3180 . . . . . . . . . . . . . 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 1842 . . . . . . . . . . . . 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 3277 . . . . . . . . . . . . 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 3683 . . . . . . . . . . . . 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 7417 . . . . . . . . . . . . . . . . . . . 20 (๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โ†’ ((๐‘ก -s ๐ด) ยทs (๐ต -s ๐‘ข)) = (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s ๐‘ข)))
160159oveq2d 7418 . . . . . . . . . . . . . . . . . . 19 (๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โ†’ ((๐ด ยทs ๐ต) +s ((๐‘ก -s ๐ด) ยทs (๐ต -s ๐‘ข))) = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s ๐‘ข))))
161160eqeq2d 2735 . . . . . . . . . . . . . . . . . 18 (๐‘ก = (๐ด +s ( 1s /su ๐‘›)) โ†’ (๐‘ง = ((๐ด ยทs ๐ต) +s ((๐‘ก -s ๐ด) ยทs (๐ต -s ๐‘ข))) โ†” ๐‘ง = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s ๐‘ข)))))
162161rexbidv 3170 . . . . . . . . . . . . . . . . 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 3518 . . . . . . . . . . . . . . . 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 3180 . . . . . . . . . . . . . . . . . 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 1842 . . . . . . . . . . . . . . . . 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 3277 . . . . . . . . . . . . . . . . 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 3683 . . . . . . . . . . . . . . . . 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 7418 . . . . . . . . . . . . . . . . . . . 20 (๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โ†’ (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s ๐‘ข)) = (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s (๐ต -s ( 1s /su ๐‘š)))))
171170oveq2d 7418 . . . . . . . . . . . . . . . . . . 19 (๐‘ข = (๐ต -s ( 1s /su ๐‘š)) โ†’ ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s ๐‘ข))) = ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s (๐ต -s ( 1s /su ๐‘š))))))
172171eqeq2d 2735 . . . . . . . . . . . . . . . . . 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 3518 . . . . . . . . . . . . . . . . 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 7420 . . . . . . . . . . . . . . . . . . 19 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s (๐ต -s ( 1s /su ๐‘š)))) = (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š)))
175174oveq2d 7418 . . . . . . . . . . . . . . . . . 18 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐‘› โˆˆ โ„•s) โˆง ๐‘š โˆˆ โ„•s) โ†’ ((๐ด ยทs ๐ต) +s (((๐ด +s ( 1s /su ๐‘›)) -s ๐ด) ยทs (๐ต -s (๐ต -s ( 1s /su ๐‘š))))) = ((๐ด ยทs ๐ต) +s (( 1s /su ๐‘›) ยทs ( 1s /su ๐‘š))))
176175eqeq2d 2735 . . . . . . . . . . . . . . . . 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 3168 . . . . . . . . . . . . . . 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 3168 . . . . . . . . . . . . 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 2793 . . . . . . . . . 10 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ {๐‘ง โˆฃ โˆƒ๐‘ก โˆˆ {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}โˆƒ๐‘ข โˆˆ {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))}๐‘ง = ((๐ด ยทs ๐ต) +s ((๐‘ก -s ๐ด) ยทs (๐ต -s ๐‘ข)))} = {๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s ( 1s /su ๐‘))})
184153, 183uneq12d 4157 . . . . . . . . 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 4145 . . . . . . . . 9 ({๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s ( 1s /su ๐‘))} โˆช {๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s ( 1s /su ๐‘))}) = {๐‘ง โˆฃ โˆƒ๐‘ โˆˆ โ„•s ๐‘ง = ((๐ด ยทs ๐ต) +s ( 1s /su ๐‘))}
186184, 185eqtrdi 2780 . . . . . . . 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 7420 . . . . . . 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 2764 . . . . 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 657 . 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 28163 . . 3 (๐ด โˆˆ โ„s โ†” (๐ด โˆˆ No โˆง (โˆƒ๐‘› โˆˆ โ„•s (( -us โ€˜๐‘›) <s ๐ด โˆง ๐ด <s ๐‘›) โˆง ๐ด = ({๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด -s ( 1s /su ๐‘›))} |s {๐‘ฅ โˆฃ โˆƒ๐‘› โˆˆ โ„•s ๐‘ฅ = (๐ด +s ( 1s /su ๐‘›))}))))
194 elreno 28163 . . 3 (๐ต โˆˆ โ„s โ†” (๐ต โˆˆ No โˆง (โˆƒ๐‘š โˆˆ โ„•s (( -us โ€˜๐‘š) <s ๐ต โˆง ๐ต <s ๐‘š) โˆง ๐ต = ({๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต -s ( 1s /su ๐‘š))} |s {๐‘ฆ โˆฃ โˆƒ๐‘š โˆˆ โ„•s ๐‘ฆ = (๐ต +s ( 1s /su ๐‘š))}))))
195193, 194anbi12i 626 . 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 28163 . 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 1533  โˆƒwex 1773   โˆˆ wcel 2098  {cab 2701   โ‰  wne 2932  โˆƒwrex 3062   โˆช cun 3939   class class class wbr 5139  โ€˜cfv 6534  (class class class)co 7402   No csur 27513   <s cslt 27514   <<s csslt 27653   |s cscut 27655   0s c0s 27695   1s c1s 27696   +s cadds 27816   -us cnegs 27872   -s csubs 27873   ยทs cmuls 27946   /su cdivs 28027  โ„•scnns 28126  โ„screno 28161
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5276  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719  ax-dc 10438
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3960  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-tp 4626  df-op 4628  df-ot 4630  df-uni 4901  df-int 4942  df-iun 4990  df-br 5140  df-opab 5202  df-mpt 5223  df-tr 5257  df-id 5565  df-eprel 5571  df-po 5579  df-so 5580  df-fr 5622  df-se 5623  df-we 5624  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-pred 6291  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-riota 7358  df-ov 7405  df-oprab 7406  df-mpo 7407  df-om 7850  df-1st 7969  df-2nd 7970  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-2o 8463  df-oadd 8466  df-nadd 8662  df-no 27516  df-slt 27517  df-bday 27518  df-sle 27618  df-sslt 27654  df-scut 27656  df-0s 27697  df-1s 27698  df-made 27714  df-old 27715  df-left 27717  df-right 27718  df-norec 27795  df-norec2 27806  df-adds 27817  df-negs 27874  df-subs 27875  df-muls 27947  df-divs 28028  df-abss 28072  df-n0s 28127  df-nns 28128  df-reno 28162
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator