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

Theorem prarloclemcalc 7514
Description: Some calculations for prarloc 7515. (Contributed by Jim Kingdon, 26-Oct-2019.)
Assertion
Ref Expression
prarloclemcalc (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ ๐ต <Q (๐ด +Q ๐‘ƒ))

Proof of Theorem prarloclemcalc
StepHypRef Expression
1 simprll 537 . . . . 5 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ ๐‘„ โˆˆ Q)
2 nqnq0a 7466 . . . . 5 ((๐‘„ โˆˆ Q โˆง ๐‘„ โˆˆ Q) โ†’ (๐‘„ +Q ๐‘„) = (๐‘„ +Q0 ๐‘„))
31, 1, 2syl2anc 411 . . . 4 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ (๐‘„ +Q ๐‘„) = (๐‘„ +Q0 ๐‘„))
43oveq2d 5904 . . 3 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ (๐ด +Q0 (๐‘„ +Q ๐‘„)) = (๐ด +Q0 (๐‘„ +Q0 ๐‘„)))
5 simpll 527 . . . . 5 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ ๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)))
6 simprrl 539 . . . . . 6 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ ๐‘‹ โˆˆ Q)
7 simprrr 540 . . . . . . . 8 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ ๐‘€ โˆˆ ฯ‰)
8 1pi 7327 . . . . . . . . . . 11 1o โˆˆ N
9 opelxpi 4670 . . . . . . . . . . 11 ((๐‘€ โˆˆ ฯ‰ โˆง 1o โˆˆ N) โ†’ โŸจ๐‘€, 1oโŸฉ โˆˆ (ฯ‰ ร— N))
108, 9mpan2 425 . . . . . . . . . 10 (๐‘€ โˆˆ ฯ‰ โ†’ โŸจ๐‘€, 1oโŸฉ โˆˆ (ฯ‰ ร— N))
11 enq0ex 7451 . . . . . . . . . . 11 ~Q0 โˆˆ V
1211ecelqsi 6602 . . . . . . . . . 10 (โŸจ๐‘€, 1oโŸฉ โˆˆ (ฯ‰ ร— N) โ†’ [โŸจ๐‘€, 1oโŸฉ] ~Q0 โˆˆ ((ฯ‰ ร— N) / ~Q0 ))
1310, 12syl 14 . . . . . . . . 9 (๐‘€ โˆˆ ฯ‰ โ†’ [โŸจ๐‘€, 1oโŸฉ] ~Q0 โˆˆ ((ฯ‰ ร— N) / ~Q0 ))
14 df-nq0 7437 . . . . . . . . 9 Q0 = ((ฯ‰ ร— N) / ~Q0 )
1513, 14eleqtrrdi 2281 . . . . . . . 8 (๐‘€ โˆˆ ฯ‰ โ†’ [โŸจ๐‘€, 1oโŸฉ] ~Q0 โˆˆ Q0)
167, 15syl 14 . . . . . . 7 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ [โŸจ๐‘€, 1oโŸฉ] ~Q0 โˆˆ Q0)
17 nqnq0 7453 . . . . . . . 8 Q โІ Q0
1817, 1sselid 3165 . . . . . . 7 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ ๐‘„ โˆˆ Q0)
19 mulclnq0 7464 . . . . . . 7 (([โŸจ๐‘€, 1oโŸฉ] ~Q0 โˆˆ Q0 โˆง ๐‘„ โˆˆ Q0) โ†’ ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„) โˆˆ Q0)
2016, 18, 19syl2anc 411 . . . . . 6 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„) โˆˆ Q0)
21 nqpnq0nq 7465 . . . . . 6 ((๐‘‹ โˆˆ Q โˆง ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„) โˆˆ Q0) โ†’ (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆˆ Q)
226, 20, 21syl2anc 411 . . . . 5 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆˆ Q)
235, 22eqeltrd 2264 . . . 4 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ ๐ด โˆˆ Q)
24 addclnq 7387 . . . . 5 ((๐‘„ โˆˆ Q โˆง ๐‘„ โˆˆ Q) โ†’ (๐‘„ +Q ๐‘„) โˆˆ Q)
251, 1, 24syl2anc 411 . . . 4 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ (๐‘„ +Q ๐‘„) โˆˆ Q)
26 nqnq0a 7466 . . . 4 ((๐ด โˆˆ Q โˆง (๐‘„ +Q ๐‘„) โˆˆ Q) โ†’ (๐ด +Q (๐‘„ +Q ๐‘„)) = (๐ด +Q0 (๐‘„ +Q ๐‘„)))
2723, 25, 26syl2anc 411 . . 3 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ (๐ด +Q (๐‘„ +Q ๐‘„)) = (๐ด +Q0 (๐‘„ +Q ๐‘„)))
28 simplr 528 . . . . . 6 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„)))
29 2onn 6535 . . . . . . . . . . . . . 14 2o โˆˆ ฯ‰
30 2on0 6440 . . . . . . . . . . . . . 14 2o โ‰  โˆ…
31 elni 7320 . . . . . . . . . . . . . 14 (2o โˆˆ N โ†” (2o โˆˆ ฯ‰ โˆง 2o โ‰  โˆ…))
3229, 30, 31mpbir2an 943 . . . . . . . . . . . . 13 2o โˆˆ N
33 nnppipi 7355 . . . . . . . . . . . . 13 ((๐‘€ โˆˆ ฯ‰ โˆง 2o โˆˆ N) โ†’ (๐‘€ +o 2o) โˆˆ N)
3432, 33mpan2 425 . . . . . . . . . . . 12 (๐‘€ โˆˆ ฯ‰ โ†’ (๐‘€ +o 2o) โˆˆ N)
35 opelxpi 4670 . . . . . . . . . . . 12 (((๐‘€ +o 2o) โˆˆ N โˆง 1o โˆˆ N) โ†’ โŸจ(๐‘€ +o 2o), 1oโŸฉ โˆˆ (N ร— N))
3634, 8, 35sylancl 413 . . . . . . . . . . 11 (๐‘€ โˆˆ ฯ‰ โ†’ โŸจ(๐‘€ +o 2o), 1oโŸฉ โˆˆ (N ร— N))
37 enqex 7372 . . . . . . . . . . . 12 ~Q โˆˆ V
3837ecelqsi 6602 . . . . . . . . . . 11 (โŸจ(๐‘€ +o 2o), 1oโŸฉ โˆˆ (N ร— N) โ†’ [โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q โˆˆ ((N ร— N) / ~Q ))
3936, 38syl 14 . . . . . . . . . 10 (๐‘€ โˆˆ ฯ‰ โ†’ [โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q โˆˆ ((N ร— N) / ~Q ))
40 df-nqqs 7360 . . . . . . . . . 10 Q = ((N ร— N) / ~Q )
4139, 40eleqtrrdi 2281 . . . . . . . . 9 (๐‘€ โˆˆ ฯ‰ โ†’ [โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q โˆˆ Q)
427, 41syl 14 . . . . . . . 8 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ [โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q โˆˆ Q)
43 mulclnq 7388 . . . . . . . 8 (([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q โˆˆ Q โˆง ๐‘„ โˆˆ Q) โ†’ ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„) โˆˆ Q)
4442, 1, 43syl2anc 411 . . . . . . 7 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„) โˆˆ Q)
45 nqnq0a 7466 . . . . . . 7 ((๐‘‹ โˆˆ Q โˆง ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„) โˆˆ Q) โ†’ (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„)) = (๐‘‹ +Q0 ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„)))
466, 44, 45syl2anc 411 . . . . . 6 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„)) = (๐‘‹ +Q0 ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„)))
47 nqnq0m 7467 . . . . . . . . 9 (([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q โˆˆ Q โˆง ๐‘„ โˆˆ Q) โ†’ ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„) = ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ0 ๐‘„))
4842, 1, 47syl2anc 411 . . . . . . . 8 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„) = ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ0 ๐‘„))
49 nqnq0pi 7450 . . . . . . . . . . 11 (((๐‘€ +o 2o) โˆˆ N โˆง 1o โˆˆ N) โ†’ [โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q0 = [โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q )
5034, 8, 49sylancl 413 . . . . . . . . . 10 (๐‘€ โˆˆ ฯ‰ โ†’ [โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q0 = [โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q )
517, 50syl 14 . . . . . . . . 9 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ [โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q0 = [โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q )
5251oveq1d 5903 . . . . . . . 8 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q0 ยทQ0 ๐‘„) = ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ0 ๐‘„))
5348, 52eqtr4d 2223 . . . . . . 7 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„) = ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q0 ยทQ0 ๐‘„))
5453oveq2d 5904 . . . . . 6 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ (๐‘‹ +Q0 ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„)) = (๐‘‹ +Q0 ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)))
5528, 46, 543eqtrd 2224 . . . . 5 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ ๐ต = (๐‘‹ +Q0 ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)))
56 nnanq0 7470 . . . . . . . . . 10 ((๐‘€ โˆˆ ฯ‰ โˆง 2o โˆˆ ฯ‰ โˆง 1o โˆˆ N) โ†’ [โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q0 = ([โŸจ๐‘€, 1oโŸฉ] ~Q0 +Q0 [โŸจ2o, 1oโŸฉ] ~Q0 ))
578, 56mp3an3 1336 . . . . . . . . 9 ((๐‘€ โˆˆ ฯ‰ โˆง 2o โˆˆ ฯ‰) โ†’ [โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q0 = ([โŸจ๐‘€, 1oโŸฉ] ~Q0 +Q0 [โŸจ2o, 1oโŸฉ] ~Q0 ))
587, 29, 57sylancl 413 . . . . . . . 8 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ [โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q0 = ([โŸจ๐‘€, 1oโŸฉ] ~Q0 +Q0 [โŸจ2o, 1oโŸฉ] ~Q0 ))
5958oveq1d 5903 . . . . . . 7 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q0 ยทQ0 ๐‘„) = (([โŸจ๐‘€, 1oโŸฉ] ~Q0 +Q0 [โŸจ2o, 1oโŸฉ] ~Q0 ) ยทQ0 ๐‘„))
60 opelxpi 4670 . . . . . . . . . . . 12 ((2o โˆˆ ฯ‰ โˆง 1o โˆˆ N) โ†’ โŸจ2o, 1oโŸฉ โˆˆ (ฯ‰ ร— N))
6129, 8, 60mp2an 426 . . . . . . . . . . 11 โŸจ2o, 1oโŸฉ โˆˆ (ฯ‰ ร— N)
6211ecelqsi 6602 . . . . . . . . . . 11 (โŸจ2o, 1oโŸฉ โˆˆ (ฯ‰ ร— N) โ†’ [โŸจ2o, 1oโŸฉ] ~Q0 โˆˆ ((ฯ‰ ร— N) / ~Q0 ))
6361, 62ax-mp 5 . . . . . . . . . 10 [โŸจ2o, 1oโŸฉ] ~Q0 โˆˆ ((ฯ‰ ร— N) / ~Q0 )
6463, 14eleqtrri 2263 . . . . . . . . 9 [โŸจ2o, 1oโŸฉ] ~Q0 โˆˆ Q0
65 distnq0r 7475 . . . . . . . . 9 ((๐‘„ โˆˆ Q0 โˆง [โŸจ๐‘€, 1oโŸฉ] ~Q0 โˆˆ Q0 โˆง [โŸจ2o, 1oโŸฉ] ~Q0 โˆˆ Q0) โ†’ (([โŸจ๐‘€, 1oโŸฉ] ~Q0 +Q0 [โŸจ2o, 1oโŸฉ] ~Q0 ) ยทQ0 ๐‘„) = (([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„) +Q0 ([โŸจ2o, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)))
6664, 65mp3an3 1336 . . . . . . . 8 ((๐‘„ โˆˆ Q0 โˆง [โŸจ๐‘€, 1oโŸฉ] ~Q0 โˆˆ Q0) โ†’ (([โŸจ๐‘€, 1oโŸฉ] ~Q0 +Q0 [โŸจ2o, 1oโŸฉ] ~Q0 ) ยทQ0 ๐‘„) = (([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„) +Q0 ([โŸจ2o, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)))
6718, 16, 66syl2anc 411 . . . . . . 7 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ (([โŸจ๐‘€, 1oโŸฉ] ~Q0 +Q0 [โŸจ2o, 1oโŸฉ] ~Q0 ) ยทQ0 ๐‘„) = (([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„) +Q0 ([โŸจ2o, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)))
6859, 67eqtrd 2220 . . . . . 6 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q0 ยทQ0 ๐‘„) = (([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„) +Q0 ([โŸจ2o, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)))
6968oveq2d 5904 . . . . 5 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ (๐‘‹ +Q0 ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) = (๐‘‹ +Q0 (([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„) +Q0 ([โŸจ2o, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„))))
70 nq02m 7477 . . . . . . . . 9 (๐‘„ โˆˆ Q0 โ†’ ([โŸจ2o, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„) = (๐‘„ +Q0 ๐‘„))
7170oveq2d 5904 . . . . . . . 8 (๐‘„ โˆˆ Q0 โ†’ (([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„) +Q0 ([โŸจ2o, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) = (([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„) +Q0 (๐‘„ +Q0 ๐‘„)))
7271oveq2d 5904 . . . . . . 7 (๐‘„ โˆˆ Q0 โ†’ (๐‘‹ +Q0 (([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„) +Q0 ([โŸจ2o, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„))) = (๐‘‹ +Q0 (([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„) +Q0 (๐‘„ +Q0 ๐‘„))))
7318, 72syl 14 . . . . . 6 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ (๐‘‹ +Q0 (([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„) +Q0 ([โŸจ2o, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„))) = (๐‘‹ +Q0 (([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„) +Q0 (๐‘„ +Q0 ๐‘„))))
7417, 6sselid 3165 . . . . . . 7 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ ๐‘‹ โˆˆ Q0)
75 addclnq0 7463 . . . . . . . 8 ((๐‘„ โˆˆ Q0 โˆง ๐‘„ โˆˆ Q0) โ†’ (๐‘„ +Q0 ๐‘„) โˆˆ Q0)
7618, 18, 75syl2anc 411 . . . . . . 7 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ (๐‘„ +Q0 ๐‘„) โˆˆ Q0)
77 addassnq0 7474 . . . . . . 7 ((๐‘‹ โˆˆ Q0 โˆง ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„) โˆˆ Q0 โˆง (๐‘„ +Q0 ๐‘„) โˆˆ Q0) โ†’ ((๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) +Q0 (๐‘„ +Q0 ๐‘„)) = (๐‘‹ +Q0 (([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„) +Q0 (๐‘„ +Q0 ๐‘„))))
7874, 20, 76, 77syl3anc 1248 . . . . . 6 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ ((๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) +Q0 (๐‘„ +Q0 ๐‘„)) = (๐‘‹ +Q0 (([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„) +Q0 (๐‘„ +Q0 ๐‘„))))
7973, 78eqtr4d 2223 . . . . 5 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ (๐‘‹ +Q0 (([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„) +Q0 ([โŸจ2o, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„))) = ((๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) +Q0 (๐‘„ +Q0 ๐‘„)))
8055, 69, 793eqtrd 2224 . . . 4 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ ๐ต = ((๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) +Q0 (๐‘„ +Q0 ๐‘„)))
81 oveq1 5895 . . . . . 6 (๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โ†’ (๐ด +Q0 (๐‘„ +Q0 ๐‘„)) = ((๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) +Q0 (๐‘„ +Q0 ๐‘„)))
8281eqeq2d 2199 . . . . 5 (๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โ†’ (๐ต = (๐ด +Q0 (๐‘„ +Q0 ๐‘„)) โ†” ๐ต = ((๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) +Q0 (๐‘„ +Q0 ๐‘„))))
835, 82syl 14 . . . 4 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ (๐ต = (๐ด +Q0 (๐‘„ +Q0 ๐‘„)) โ†” ๐ต = ((๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) +Q0 (๐‘„ +Q0 ๐‘„))))
8480, 83mpbird 167 . . 3 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ ๐ต = (๐ด +Q0 (๐‘„ +Q0 ๐‘„)))
854, 27, 843eqtr4rd 2231 . 2 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ ๐ต = (๐ด +Q (๐‘„ +Q ๐‘„)))
86 simprlr 538 . . 3 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ (๐‘„ +Q ๐‘„) <Q ๐‘ƒ)
87 ltrelnq 7377 . . . . . 6 <Q โІ (Q ร— Q)
8887brel 4690 . . . . 5 ((๐‘„ +Q ๐‘„) <Q ๐‘ƒ โ†’ ((๐‘„ +Q ๐‘„) โˆˆ Q โˆง ๐‘ƒ โˆˆ Q))
8986, 88syl 14 . . . 4 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ ((๐‘„ +Q ๐‘„) โˆˆ Q โˆง ๐‘ƒ โˆˆ Q))
90 ltanqg 7412 . . . . 5 (((๐‘„ +Q ๐‘„) โˆˆ Q โˆง ๐‘ƒ โˆˆ Q โˆง ๐ด โˆˆ Q) โ†’ ((๐‘„ +Q ๐‘„) <Q ๐‘ƒ โ†” (๐ด +Q (๐‘„ +Q ๐‘„)) <Q (๐ด +Q ๐‘ƒ)))
91903expa 1204 . . . 4 ((((๐‘„ +Q ๐‘„) โˆˆ Q โˆง ๐‘ƒ โˆˆ Q) โˆง ๐ด โˆˆ Q) โ†’ ((๐‘„ +Q ๐‘„) <Q ๐‘ƒ โ†” (๐ด +Q (๐‘„ +Q ๐‘„)) <Q (๐ด +Q ๐‘ƒ)))
9289, 23, 91syl2anc 411 . . 3 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ ((๐‘„ +Q ๐‘„) <Q ๐‘ƒ โ†” (๐ด +Q (๐‘„ +Q ๐‘„)) <Q (๐ด +Q ๐‘ƒ)))
9386, 92mpbid 147 . 2 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ (๐ด +Q (๐‘„ +Q ๐‘„)) <Q (๐ด +Q ๐‘ƒ))
9485, 93eqbrtrd 4037 1 (((๐ด = (๐‘‹ +Q0 ([โŸจ๐‘€, 1oโŸฉ] ~Q0 ยทQ0 ๐‘„)) โˆง ๐ต = (๐‘‹ +Q ([โŸจ(๐‘€ +o 2o), 1oโŸฉ] ~Q ยทQ ๐‘„))) โˆง ((๐‘„ โˆˆ Q โˆง (๐‘„ +Q ๐‘„) <Q ๐‘ƒ) โˆง (๐‘‹ โˆˆ Q โˆง ๐‘€ โˆˆ ฯ‰))) โ†’ ๐ต <Q (๐ด +Q ๐‘ƒ))
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   โ†” wb 105   = wceq 1363   โˆˆ wcel 2158   โ‰  wne 2357  โˆ…c0 3434  โŸจcop 3607   class class class wbr 4015  ฯ‰com 4601   ร— cxp 4636  (class class class)co 5888  1oc1o 6423  2oc2o 6424   +o coa 6427  [cec 6546   / cqs 6547  Ncnpi 7284   ~Q ceq 7291  Qcnq 7292   +Q cplq 7294   ยทQ cmq 7295   <Q cltq 7297   ~Q0 ceq0 7298  Q0cnq0 7299   +Q0 cplq0 7301   ยทQ0 cmq0 7302
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 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-coll 4130  ax-sep 4133  ax-nul 4141  ax-pow 4186  ax-pr 4221  ax-un 4445  ax-setind 4548  ax-iinf 4599
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 980  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-ral 2470  df-rex 2471  df-reu 2472  df-rab 2474  df-v 2751  df-sbc 2975  df-csb 3070  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-nul 3435  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-int 3857  df-iun 3900  df-br 4016  df-opab 4077  df-mpt 4078  df-tr 4114  df-eprel 4301  df-id 4305  df-iord 4378  df-on 4380  df-suc 4383  df-iom 4602  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-res 4650  df-ima 4651  df-iota 5190  df-fun 5230  df-fn 5231  df-f 5232  df-f1 5233  df-fo 5234  df-f1o 5235  df-fv 5236  df-ov 5891  df-oprab 5892  df-mpo 5893  df-1st 6154  df-2nd 6155  df-recs 6319  df-irdg 6384  df-1o 6430  df-2o 6431  df-oadd 6434  df-omul 6435  df-er 6548  df-ec 6550  df-qs 6554  df-ni 7316  df-pli 7317  df-mi 7318  df-lti 7319  df-plpq 7356  df-mpq 7357  df-enq 7359  df-nqqs 7360  df-plqqs 7361  df-mqqs 7362  df-ltnqqs 7365  df-enq0 7436  df-nq0 7437  df-plq0 7439  df-mq0 7440
This theorem is referenced by:  prarloc  7515
  Copyright terms: Public domain W3C validator