ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  caucvgsrlemoffcau GIF version

Theorem caucvgsrlemoffcau 7799
Description: Lemma for caucvgsr 7803. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.)
Hypotheses
Ref Expression
caucvgsr.f (๐œ‘ โ†’ ๐น:NโŸถR)
caucvgsr.cau (๐œ‘ โ†’ โˆ€๐‘› โˆˆ N โˆ€๐‘˜ โˆˆ N (๐‘› <N ๐‘˜ โ†’ ((๐นโ€˜๐‘›) <R ((๐นโ€˜๐‘˜) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) โˆง (๐นโ€˜๐‘˜) <R ((๐นโ€˜๐‘›) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ))))
caucvgsrlembnd.bnd (๐œ‘ โ†’ โˆ€๐‘š โˆˆ N ๐ด <R (๐นโ€˜๐‘š))
caucvgsrlembnd.offset ๐บ = (๐‘Ž โˆˆ N โ†ฆ (((๐นโ€˜๐‘Ž) +R 1R) +R (๐ด ยทR -1R)))
Assertion
Ref Expression
caucvgsrlemoffcau (๐œ‘ โ†’ โˆ€๐‘› โˆˆ N โˆ€๐‘˜ โˆˆ N (๐‘› <N ๐‘˜ โ†’ ((๐บโ€˜๐‘›) <R ((๐บโ€˜๐‘˜) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) โˆง (๐บโ€˜๐‘˜) <R ((๐บโ€˜๐‘›) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ))))
Distinct variable groups:   ๐ด,๐‘Ž   ๐ด,๐‘š   ๐น,๐‘Ž   ๐‘˜,๐‘Ž,๐‘›,๐œ‘   ๐‘›,๐‘™,๐‘ข
Allowed substitution hints:   ๐œ‘(๐‘ข,๐‘š,๐‘™)   ๐ด(๐‘ข,๐‘˜,๐‘›,๐‘™)   ๐น(๐‘ข,๐‘˜,๐‘š,๐‘›,๐‘™)   ๐บ(๐‘ข,๐‘˜,๐‘š,๐‘›,๐‘Ž,๐‘™)

Proof of Theorem caucvgsrlemoffcau
Dummy variables ๐‘“ ๐‘” โ„Ž are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 caucvgsr.cau . 2 (๐œ‘ โ†’ โˆ€๐‘› โˆˆ N โˆ€๐‘˜ โˆˆ N (๐‘› <N ๐‘˜ โ†’ ((๐นโ€˜๐‘›) <R ((๐นโ€˜๐‘˜) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) โˆง (๐นโ€˜๐‘˜) <R ((๐นโ€˜๐‘›) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ))))
2 caucvgsr.f . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐น:NโŸถR)
3 caucvgsrlembnd.bnd . . . . . . . . . . . 12 (๐œ‘ โ†’ โˆ€๐‘š โˆˆ N ๐ด <R (๐นโ€˜๐‘š))
4 caucvgsrlembnd.offset . . . . . . . . . . . 12 ๐บ = (๐‘Ž โˆˆ N โ†ฆ (((๐นโ€˜๐‘Ž) +R 1R) +R (๐ด ยทR -1R)))
52, 1, 3, 4caucvgsrlemoffval 7797 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ N) โ†’ ((๐บโ€˜๐‘›) +R ๐ด) = ((๐นโ€˜๐‘›) +R 1R))
65adantr 276 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ ((๐บโ€˜๐‘›) +R ๐ด) = ((๐นโ€˜๐‘›) +R 1R))
76eqcomd 2183 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ ((๐นโ€˜๐‘›) +R 1R) = ((๐บโ€˜๐‘›) +R ๐ด))
82ad2antrr 488 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ ๐น:NโŸถR)
9 simpr 110 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ ๐‘˜ โˆˆ N)
108, 9ffvelcdmd 5654 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ (๐นโ€˜๐‘˜) โˆˆ R)
11 simplr 528 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ ๐‘› โˆˆ N)
12 recnnpr 7549 . . . . . . . . . . . 12 (๐‘› โˆˆ N โ†’ โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ โˆˆ P)
13 prsrcl 7785 . . . . . . . . . . . 12 (โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ โˆˆ P โ†’ [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R โˆˆ R)
1411, 12, 133syl 17 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R โˆˆ R)
15 1sr 7752 . . . . . . . . . . . 12 1R โˆˆ R
1615a1i 9 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ 1R โˆˆ R)
17 addcomsrg 7756 . . . . . . . . . . . 12 ((๐‘“ โˆˆ R โˆง ๐‘” โˆˆ R) โ†’ (๐‘“ +R ๐‘”) = (๐‘” +R ๐‘“))
1817adantl 277 . . . . . . . . . . 11 ((((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โˆง (๐‘“ โˆˆ R โˆง ๐‘” โˆˆ R)) โ†’ (๐‘“ +R ๐‘”) = (๐‘” +R ๐‘“))
19 addasssrg 7757 . . . . . . . . . . . 12 ((๐‘“ โˆˆ R โˆง ๐‘” โˆˆ R โˆง โ„Ž โˆˆ R) โ†’ ((๐‘“ +R ๐‘”) +R โ„Ž) = (๐‘“ +R (๐‘” +R โ„Ž)))
2019adantl 277 . . . . . . . . . . 11 ((((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โˆง (๐‘“ โˆˆ R โˆง ๐‘” โˆˆ R โˆง โ„Ž โˆˆ R)) โ†’ ((๐‘“ +R ๐‘”) +R โ„Ž) = (๐‘“ +R (๐‘” +R โ„Ž)))
2110, 14, 16, 18, 20caov32d 6057 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ (((๐นโ€˜๐‘˜) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) +R 1R) = (((๐นโ€˜๐‘˜) +R 1R) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ))
222, 1, 3, 4caucvgsrlemoffval 7797 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘˜ โˆˆ N) โ†’ ((๐บโ€˜๐‘˜) +R ๐ด) = ((๐นโ€˜๐‘˜) +R 1R))
2322adantlr 477 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ ((๐บโ€˜๐‘˜) +R ๐ด) = ((๐นโ€˜๐‘˜) +R 1R))
2423oveq1d 5892 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ (((๐บโ€˜๐‘˜) +R ๐ด) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) = (((๐นโ€˜๐‘˜) +R 1R) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ))
252, 1, 3, 4caucvgsrlemofff 7798 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐บ:NโŸถR)
2625ad2antrr 488 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ ๐บ:NโŸถR)
2726, 9ffvelcdmd 5654 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ (๐บโ€˜๐‘˜) โˆˆ R)
283caucvgsrlemasr 7791 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐ด โˆˆ R)
2928ad2antrr 488 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ ๐ด โˆˆ R)
3027, 29, 14, 18, 20caov32d 6057 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ (((๐บโ€˜๐‘˜) +R ๐ด) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) = (((๐บโ€˜๐‘˜) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) +R ๐ด))
3121, 24, 303eqtr2d 2216 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ (((๐นโ€˜๐‘˜) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) +R 1R) = (((๐บโ€˜๐‘˜) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) +R ๐ด))
327, 31breq12d 4018 . . . . . . . 8 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ (((๐นโ€˜๐‘›) +R 1R) <R (((๐นโ€˜๐‘˜) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) +R 1R) โ†” ((๐บโ€˜๐‘›) +R ๐ด) <R (((๐บโ€˜๐‘˜) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) +R ๐ด)))
33 ltasrg 7771 . . . . . . . . . 10 ((๐‘“ โˆˆ R โˆง ๐‘” โˆˆ R โˆง โ„Ž โˆˆ R) โ†’ (๐‘“ <R ๐‘” โ†” (โ„Ž +R ๐‘“) <R (โ„Ž +R ๐‘”)))
3433adantl 277 . . . . . . . . 9 ((((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โˆง (๐‘“ โˆˆ R โˆง ๐‘” โˆˆ R โˆง โ„Ž โˆˆ R)) โ†’ (๐‘“ <R ๐‘” โ†” (โ„Ž +R ๐‘“) <R (โ„Ž +R ๐‘”)))
358, 11ffvelcdmd 5654 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ (๐นโ€˜๐‘›) โˆˆ R)
36 addclsr 7754 . . . . . . . . . 10 (((๐นโ€˜๐‘˜) โˆˆ R โˆง [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R โˆˆ R) โ†’ ((๐นโ€˜๐‘˜) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) โˆˆ R)
3710, 14, 36syl2anc 411 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ ((๐นโ€˜๐‘˜) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) โˆˆ R)
3834, 35, 37, 16, 18caovord2d 6046 . . . . . . . 8 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ ((๐นโ€˜๐‘›) <R ((๐นโ€˜๐‘˜) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) โ†” ((๐นโ€˜๐‘›) +R 1R) <R (((๐นโ€˜๐‘˜) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) +R 1R)))
3926, 11ffvelcdmd 5654 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ (๐บโ€˜๐‘›) โˆˆ R)
40 addclsr 7754 . . . . . . . . . 10 (((๐บโ€˜๐‘˜) โˆˆ R โˆง [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R โˆˆ R) โ†’ ((๐บโ€˜๐‘˜) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) โˆˆ R)
4127, 14, 40syl2anc 411 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ ((๐บโ€˜๐‘˜) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) โˆˆ R)
4234, 39, 41, 29, 18caovord2d 6046 . . . . . . . 8 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ ((๐บโ€˜๐‘›) <R ((๐บโ€˜๐‘˜) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) โ†” ((๐บโ€˜๐‘›) +R ๐ด) <R (((๐บโ€˜๐‘˜) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) +R ๐ด)))
4332, 38, 423bitr4d 220 . . . . . . 7 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ ((๐นโ€˜๐‘›) <R ((๐นโ€˜๐‘˜) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) โ†” (๐บโ€˜๐‘›) <R ((๐บโ€˜๐‘˜) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R )))
4423eqcomd 2183 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ ((๐นโ€˜๐‘˜) +R 1R) = ((๐บโ€˜๐‘˜) +R ๐ด))
4535, 14, 16, 18, 20caov32d 6057 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ (((๐นโ€˜๐‘›) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) +R 1R) = (((๐นโ€˜๐‘›) +R 1R) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ))
466oveq1d 5892 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ (((๐บโ€˜๐‘›) +R ๐ด) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) = (((๐นโ€˜๐‘›) +R 1R) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ))
4739, 29, 14, 18, 20caov32d 6057 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ (((๐บโ€˜๐‘›) +R ๐ด) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) = (((๐บโ€˜๐‘›) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) +R ๐ด))
4845, 46, 473eqtr2d 2216 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ (((๐นโ€˜๐‘›) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) +R 1R) = (((๐บโ€˜๐‘›) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) +R ๐ด))
4944, 48breq12d 4018 . . . . . . . 8 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ (((๐นโ€˜๐‘˜) +R 1R) <R (((๐นโ€˜๐‘›) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) +R 1R) โ†” ((๐บโ€˜๐‘˜) +R ๐ด) <R (((๐บโ€˜๐‘›) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) +R ๐ด)))
50 addclsr 7754 . . . . . . . . . 10 (((๐นโ€˜๐‘›) โˆˆ R โˆง [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R โˆˆ R) โ†’ ((๐นโ€˜๐‘›) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) โˆˆ R)
5135, 14, 50syl2anc 411 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ ((๐นโ€˜๐‘›) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) โˆˆ R)
5234, 10, 51, 16, 18caovord2d 6046 . . . . . . . 8 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ ((๐นโ€˜๐‘˜) <R ((๐นโ€˜๐‘›) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) โ†” ((๐นโ€˜๐‘˜) +R 1R) <R (((๐นโ€˜๐‘›) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) +R 1R)))
53 addclsr 7754 . . . . . . . . . 10 (((๐บโ€˜๐‘›) โˆˆ R โˆง [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R โˆˆ R) โ†’ ((๐บโ€˜๐‘›) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) โˆˆ R)
5439, 14, 53syl2anc 411 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ ((๐บโ€˜๐‘›) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) โˆˆ R)
5534, 27, 54, 29, 18caovord2d 6046 . . . . . . . 8 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ ((๐บโ€˜๐‘˜) <R ((๐บโ€˜๐‘›) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) โ†” ((๐บโ€˜๐‘˜) +R ๐ด) <R (((๐บโ€˜๐‘›) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) +R ๐ด)))
5649, 52, 553bitr4d 220 . . . . . . 7 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ ((๐นโ€˜๐‘˜) <R ((๐นโ€˜๐‘›) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) โ†” (๐บโ€˜๐‘˜) <R ((๐บโ€˜๐‘›) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R )))
5743, 56anbi12d 473 . . . . . 6 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ (((๐นโ€˜๐‘›) <R ((๐นโ€˜๐‘˜) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) โˆง (๐นโ€˜๐‘˜) <R ((๐นโ€˜๐‘›) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R )) โ†” ((๐บโ€˜๐‘›) <R ((๐บโ€˜๐‘˜) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) โˆง (๐บโ€˜๐‘˜) <R ((๐บโ€˜๐‘›) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ))))
5857biimpd 144 . . . . 5 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ (((๐นโ€˜๐‘›) <R ((๐นโ€˜๐‘˜) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) โˆง (๐นโ€˜๐‘˜) <R ((๐นโ€˜๐‘›) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R )) โ†’ ((๐บโ€˜๐‘›) <R ((๐บโ€˜๐‘˜) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) โˆง (๐บโ€˜๐‘˜) <R ((๐บโ€˜๐‘›) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ))))
5958imim2d 54 . . . 4 (((๐œ‘ โˆง ๐‘› โˆˆ N) โˆง ๐‘˜ โˆˆ N) โ†’ ((๐‘› <N ๐‘˜ โ†’ ((๐นโ€˜๐‘›) <R ((๐นโ€˜๐‘˜) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) โˆง (๐นโ€˜๐‘˜) <R ((๐นโ€˜๐‘›) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ))) โ†’ (๐‘› <N ๐‘˜ โ†’ ((๐บโ€˜๐‘›) <R ((๐บโ€˜๐‘˜) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) โˆง (๐บโ€˜๐‘˜) <R ((๐บโ€˜๐‘›) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R )))))
6059ralimdva 2544 . . 3 ((๐œ‘ โˆง ๐‘› โˆˆ N) โ†’ (โˆ€๐‘˜ โˆˆ N (๐‘› <N ๐‘˜ โ†’ ((๐นโ€˜๐‘›) <R ((๐นโ€˜๐‘˜) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) โˆง (๐นโ€˜๐‘˜) <R ((๐นโ€˜๐‘›) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ))) โ†’ โˆ€๐‘˜ โˆˆ N (๐‘› <N ๐‘˜ โ†’ ((๐บโ€˜๐‘›) <R ((๐บโ€˜๐‘˜) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) โˆง (๐บโ€˜๐‘˜) <R ((๐บโ€˜๐‘›) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R )))))
6160ralimdva 2544 . 2 (๐œ‘ โ†’ (โˆ€๐‘› โˆˆ N โˆ€๐‘˜ โˆˆ N (๐‘› <N ๐‘˜ โ†’ ((๐นโ€˜๐‘›) <R ((๐นโ€˜๐‘˜) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) โˆง (๐นโ€˜๐‘˜) <R ((๐นโ€˜๐‘›) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ))) โ†’ โˆ€๐‘› โˆˆ N โˆ€๐‘˜ โˆˆ N (๐‘› <N ๐‘˜ โ†’ ((๐บโ€˜๐‘›) <R ((๐บโ€˜๐‘˜) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) โˆง (๐บโ€˜๐‘˜) <R ((๐บโ€˜๐‘›) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R )))))
621, 61mpd 13 1 (๐œ‘ โ†’ โˆ€๐‘› โˆˆ N โˆ€๐‘˜ โˆˆ N (๐‘› <N ๐‘˜ โ†’ ((๐บโ€˜๐‘›) <R ((๐บโ€˜๐‘˜) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ) โˆง (๐บโ€˜๐‘˜) <R ((๐บโ€˜๐‘›) +R [โŸจ(โŸจ{๐‘™ โˆฃ ๐‘™ <Q (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q )}, {๐‘ข โˆฃ (*Qโ€˜[โŸจ๐‘›, 1oโŸฉ] ~Q ) <Q ๐‘ข}โŸฉ +P 1P), 1PโŸฉ] ~R ))))
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   โ†” wb 105   โˆง w3a 978   = wceq 1353   โˆˆ wcel 2148  {cab 2163  โˆ€wral 2455  โŸจcop 3597   class class class wbr 4005   โ†ฆ cmpt 4066  โŸถwf 5214  โ€˜cfv 5218  (class class class)co 5877  1oc1o 6412  [cec 6535  Ncnpi 7273   <N clti 7276   ~Q ceq 7280  *Qcrq 7285   <Q cltq 7286  Pcnp 7292  1Pc1p 7293   +P cpp 7294   ~R cer 7297  Rcnr 7298  1Rc1r 7300  -1Rcm1r 7301   +R cplr 7302   ยทR cmr 7303   <R cltr 7304
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4120  ax-sep 4123  ax-nul 4131  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-iinf 4589
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-tr 4104  df-eprel 4291  df-id 4295  df-po 4298  df-iso 4299  df-iord 4368  df-on 4370  df-suc 4373  df-iom 4592  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-ov 5880  df-oprab 5881  df-mpo 5882  df-1st 6143  df-2nd 6144  df-recs 6308  df-irdg 6373  df-1o 6419  df-2o 6420  df-oadd 6423  df-omul 6424  df-er 6537  df-ec 6539  df-qs 6543  df-ni 7305  df-pli 7306  df-mi 7307  df-lti 7308  df-plpq 7345  df-mpq 7346  df-enq 7348  df-nqqs 7349  df-plqqs 7350  df-mqqs 7351  df-1nqqs 7352  df-rq 7353  df-ltnqqs 7354  df-enq0 7425  df-nq0 7426  df-0nq0 7427  df-plq0 7428  df-mq0 7429  df-inp 7467  df-i1p 7468  df-iplp 7469  df-imp 7470  df-iltp 7471  df-enr 7727  df-nr 7728  df-plr 7729  df-mr 7730  df-ltr 7731  df-0r 7732  df-1r 7733  df-m1r 7734
This theorem is referenced by:  caucvgsrlemoffres  7801
  Copyright terms: Public domain W3C validator