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

Theorem prarloclemlt 7510
Description: Two possible ways of contracting an interval which straddles a Dedekind cut. Lemma for prarloc 7520. (Contributed by Jim Kingdon, 10-Nov-2019.)
Assertion
Ref Expression
prarloclemlt (((๐‘‹ โˆˆ ฯ‰ โˆง (โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐ด โˆˆ ๐ฟ โˆง ๐‘ƒ โˆˆ Q)) โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (๐ด +Q ([โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q ยทQ ๐‘ƒ)) <Q (๐ด +Q ([โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ)))

Proof of Theorem prarloclemlt
StepHypRef Expression
1 2onn 6540 . . . . . . . . . . . 12 2o โˆˆ ฯ‰
2 nnacl 6499 . . . . . . . . . . . 12 ((๐‘ฆ โˆˆ ฯ‰ โˆง 2o โˆˆ ฯ‰) โ†’ (๐‘ฆ +o 2o) โˆˆ ฯ‰)
31, 2mpan2 425 . . . . . . . . . . 11 (๐‘ฆ โˆˆ ฯ‰ โ†’ (๐‘ฆ +o 2o) โˆˆ ฯ‰)
4 nnaword1 6532 . . . . . . . . . . 11 (((๐‘ฆ +o 2o) โˆˆ ฯ‰ โˆง ๐‘‹ โˆˆ ฯ‰) โ†’ (๐‘ฆ +o 2o) โІ ((๐‘ฆ +o 2o) +o ๐‘‹))
53, 4sylan 283 . . . . . . . . . 10 ((๐‘ฆ โˆˆ ฯ‰ โˆง ๐‘‹ โˆˆ ฯ‰) โ†’ (๐‘ฆ +o 2o) โІ ((๐‘ฆ +o 2o) +o ๐‘‹))
6 1oex 6443 . . . . . . . . . . . . . 14 1o โˆˆ V
76sucid 4432 . . . . . . . . . . . . 13 1o โˆˆ suc 1o
8 df-2o 6436 . . . . . . . . . . . . 13 2o = suc 1o
97, 8eleqtrri 2265 . . . . . . . . . . . 12 1o โˆˆ 2o
10 nnaordi 6527 . . . . . . . . . . . . 13 ((2o โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (1o โˆˆ 2o โ†’ (๐‘ฆ +o 1o) โˆˆ (๐‘ฆ +o 2o)))
111, 10mpan 424 . . . . . . . . . . . 12 (๐‘ฆ โˆˆ ฯ‰ โ†’ (1o โˆˆ 2o โ†’ (๐‘ฆ +o 1o) โˆˆ (๐‘ฆ +o 2o)))
129, 11mpi 15 . . . . . . . . . . 11 (๐‘ฆ โˆˆ ฯ‰ โ†’ (๐‘ฆ +o 1o) โˆˆ (๐‘ฆ +o 2o))
1312adantr 276 . . . . . . . . . 10 ((๐‘ฆ โˆˆ ฯ‰ โˆง ๐‘‹ โˆˆ ฯ‰) โ†’ (๐‘ฆ +o 1o) โˆˆ (๐‘ฆ +o 2o))
145, 13sseldd 3171 . . . . . . . . 9 ((๐‘ฆ โˆˆ ฯ‰ โˆง ๐‘‹ โˆˆ ฯ‰) โ†’ (๐‘ฆ +o 1o) โˆˆ ((๐‘ฆ +o 2o) +o ๐‘‹))
1514ancoms 268 . . . . . . . 8 ((๐‘‹ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (๐‘ฆ +o 1o) โˆˆ ((๐‘ฆ +o 2o) +o ๐‘‹))
16 1pi 7332 . . . . . . . . . . 11 1o โˆˆ N
17 nnppipi 7360 . . . . . . . . . . 11 ((๐‘ฆ โˆˆ ฯ‰ โˆง 1o โˆˆ N) โ†’ (๐‘ฆ +o 1o) โˆˆ N)
1816, 17mpan2 425 . . . . . . . . . 10 (๐‘ฆ โˆˆ ฯ‰ โ†’ (๐‘ฆ +o 1o) โˆˆ N)
1918adantl 277 . . . . . . . . 9 ((๐‘‹ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (๐‘ฆ +o 1o) โˆˆ N)
20 o1p1e2 6487 . . . . . . . . . . . . . 14 (1o +o 1o) = 2o
21 1onn 6539 . . . . . . . . . . . . . . 15 1o โˆˆ ฯ‰
22 nnppipi 7360 . . . . . . . . . . . . . . 15 ((1o โˆˆ ฯ‰ โˆง 1o โˆˆ N) โ†’ (1o +o 1o) โˆˆ N)
2321, 16, 22mp2an 426 . . . . . . . . . . . . . 14 (1o +o 1o) โˆˆ N
2420, 23eqeltrri 2263 . . . . . . . . . . . . 13 2o โˆˆ N
25 nnppipi 7360 . . . . . . . . . . . . 13 ((๐‘ฆ โˆˆ ฯ‰ โˆง 2o โˆˆ N) โ†’ (๐‘ฆ +o 2o) โˆˆ N)
2624, 25mpan2 425 . . . . . . . . . . . 12 (๐‘ฆ โˆˆ ฯ‰ โ†’ (๐‘ฆ +o 2o) โˆˆ N)
27 pinn 7326 . . . . . . . . . . . 12 ((๐‘ฆ +o 2o) โˆˆ N โ†’ (๐‘ฆ +o 2o) โˆˆ ฯ‰)
2826, 27syl 14 . . . . . . . . . . 11 (๐‘ฆ โˆˆ ฯ‰ โ†’ (๐‘ฆ +o 2o) โˆˆ ฯ‰)
29 nnacom 6503 . . . . . . . . . . 11 ((๐‘‹ โˆˆ ฯ‰ โˆง (๐‘ฆ +o 2o) โˆˆ ฯ‰) โ†’ (๐‘‹ +o (๐‘ฆ +o 2o)) = ((๐‘ฆ +o 2o) +o ๐‘‹))
3028, 29sylan2 286 . . . . . . . . . 10 ((๐‘‹ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (๐‘‹ +o (๐‘ฆ +o 2o)) = ((๐‘ฆ +o 2o) +o ๐‘‹))
31 nnppipi 7360 . . . . . . . . . . 11 ((๐‘‹ โˆˆ ฯ‰ โˆง (๐‘ฆ +o 2o) โˆˆ N) โ†’ (๐‘‹ +o (๐‘ฆ +o 2o)) โˆˆ N)
3226, 31sylan2 286 . . . . . . . . . 10 ((๐‘‹ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (๐‘‹ +o (๐‘ฆ +o 2o)) โˆˆ N)
3330, 32eqeltrrd 2267 . . . . . . . . 9 ((๐‘‹ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ((๐‘ฆ +o 2o) +o ๐‘‹) โˆˆ N)
34 ltpiord 7336 . . . . . . . . 9 (((๐‘ฆ +o 1o) โˆˆ N โˆง ((๐‘ฆ +o 2o) +o ๐‘‹) โˆˆ N) โ†’ ((๐‘ฆ +o 1o) <N ((๐‘ฆ +o 2o) +o ๐‘‹) โ†” (๐‘ฆ +o 1o) โˆˆ ((๐‘ฆ +o 2o) +o ๐‘‹)))
3519, 33, 34syl2anc 411 . . . . . . . 8 ((๐‘‹ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ((๐‘ฆ +o 1o) <N ((๐‘ฆ +o 2o) +o ๐‘‹) โ†” (๐‘ฆ +o 1o) โˆˆ ((๐‘ฆ +o 2o) +o ๐‘‹)))
3615, 35mpbird 167 . . . . . . 7 ((๐‘‹ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (๐‘ฆ +o 1o) <N ((๐‘ฆ +o 2o) +o ๐‘‹))
37 mulidpi 7335 . . . . . . . . 9 ((๐‘ฆ +o 1o) โˆˆ N โ†’ ((๐‘ฆ +o 1o) ยทN 1o) = (๐‘ฆ +o 1o))
3819, 37syl 14 . . . . . . . 8 ((๐‘‹ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ((๐‘ฆ +o 1o) ยทN 1o) = (๐‘ฆ +o 1o))
39 mulcompig 7348 . . . . . . . . . 10 ((((๐‘ฆ +o 2o) +o ๐‘‹) โˆˆ N โˆง 1o โˆˆ N) โ†’ (((๐‘ฆ +o 2o) +o ๐‘‹) ยทN 1o) = (1o ยทN ((๐‘ฆ +o 2o) +o ๐‘‹)))
4033, 16, 39sylancl 413 . . . . . . . . 9 ((๐‘‹ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (((๐‘ฆ +o 2o) +o ๐‘‹) ยทN 1o) = (1o ยทN ((๐‘ฆ +o 2o) +o ๐‘‹)))
41 mulidpi 7335 . . . . . . . . . 10 (((๐‘ฆ +o 2o) +o ๐‘‹) โˆˆ N โ†’ (((๐‘ฆ +o 2o) +o ๐‘‹) ยทN 1o) = ((๐‘ฆ +o 2o) +o ๐‘‹))
4233, 41syl 14 . . . . . . . . 9 ((๐‘‹ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (((๐‘ฆ +o 2o) +o ๐‘‹) ยทN 1o) = ((๐‘ฆ +o 2o) +o ๐‘‹))
4340, 42eqtr3d 2224 . . . . . . . 8 ((๐‘‹ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (1o ยทN ((๐‘ฆ +o 2o) +o ๐‘‹)) = ((๐‘ฆ +o 2o) +o ๐‘‹))
4438, 43breq12d 4031 . . . . . . 7 ((๐‘‹ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (((๐‘ฆ +o 1o) ยทN 1o) <N (1o ยทN ((๐‘ฆ +o 2o) +o ๐‘‹)) โ†” (๐‘ฆ +o 1o) <N ((๐‘ฆ +o 2o) +o ๐‘‹)))
4536, 44mpbird 167 . . . . . 6 ((๐‘‹ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ((๐‘ฆ +o 1o) ยทN 1o) <N (1o ยทN ((๐‘ฆ +o 2o) +o ๐‘‹)))
46 simpr 110 . . . . . . 7 ((๐‘‹ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ๐‘ฆ โˆˆ ฯ‰)
47 ordpipqqs 7391 . . . . . . . . . 10 ((((๐‘ฆ +o 1o) โˆˆ N โˆง 1o โˆˆ N) โˆง (((๐‘ฆ +o 2o) +o ๐‘‹) โˆˆ N โˆง 1o โˆˆ N)) โ†’ ([โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q <Q [โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q โ†” ((๐‘ฆ +o 1o) ยทN 1o) <N (1o ยทN ((๐‘ฆ +o 2o) +o ๐‘‹))))
4816, 47mpanl2 435 . . . . . . . . 9 (((๐‘ฆ +o 1o) โˆˆ N โˆง (((๐‘ฆ +o 2o) +o ๐‘‹) โˆˆ N โˆง 1o โˆˆ N)) โ†’ ([โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q <Q [โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q โ†” ((๐‘ฆ +o 1o) ยทN 1o) <N (1o ยทN ((๐‘ฆ +o 2o) +o ๐‘‹))))
4916, 48mpanr2 438 . . . . . . . 8 (((๐‘ฆ +o 1o) โˆˆ N โˆง ((๐‘ฆ +o 2o) +o ๐‘‹) โˆˆ N) โ†’ ([โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q <Q [โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q โ†” ((๐‘ฆ +o 1o) ยทN 1o) <N (1o ยทN ((๐‘ฆ +o 2o) +o ๐‘‹))))
5018, 49sylan 283 . . . . . . 7 ((๐‘ฆ โˆˆ ฯ‰ โˆง ((๐‘ฆ +o 2o) +o ๐‘‹) โˆˆ N) โ†’ ([โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q <Q [โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q โ†” ((๐‘ฆ +o 1o) ยทN 1o) <N (1o ยทN ((๐‘ฆ +o 2o) +o ๐‘‹))))
5146, 33, 50syl2anc 411 . . . . . 6 ((๐‘‹ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ([โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q <Q [โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q โ†” ((๐‘ฆ +o 1o) ยทN 1o) <N (1o ยทN ((๐‘ฆ +o 2o) +o ๐‘‹))))
5245, 51mpbird 167 . . . . 5 ((๐‘‹ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ [โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q <Q [โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q )
5352adantlr 477 . . . 4 (((๐‘‹ โˆˆ ฯ‰ โˆง (โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐ด โˆˆ ๐ฟ โˆง ๐‘ƒ โˆˆ Q)) โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ [โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q <Q [โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q )
54 opelxpi 4673 . . . . . . . . 9 (((๐‘ฆ +o 1o) โˆˆ N โˆง 1o โˆˆ N) โ†’ โŸจ(๐‘ฆ +o 1o), 1oโŸฉ โˆˆ (N ร— N))
5519, 16, 54sylancl 413 . . . . . . . 8 ((๐‘‹ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ โŸจ(๐‘ฆ +o 1o), 1oโŸฉ โˆˆ (N ร— N))
56 enqex 7377 . . . . . . . . 9 ~Q โˆˆ V
5756ecelqsi 6607 . . . . . . . 8 (โŸจ(๐‘ฆ +o 1o), 1oโŸฉ โˆˆ (N ร— N) โ†’ [โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q โˆˆ ((N ร— N) / ~Q ))
5855, 57syl 14 . . . . . . 7 ((๐‘‹ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ [โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q โˆˆ ((N ร— N) / ~Q ))
59 df-nqqs 7365 . . . . . . 7 Q = ((N ร— N) / ~Q )
6058, 59eleqtrrdi 2283 . . . . . 6 ((๐‘‹ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ [โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q โˆˆ Q)
6160adantlr 477 . . . . 5 (((๐‘‹ โˆˆ ฯ‰ โˆง (โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐ด โˆˆ ๐ฟ โˆง ๐‘ƒ โˆˆ Q)) โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ [โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q โˆˆ Q)
62 opelxpi 4673 . . . . . . . . 9 ((((๐‘ฆ +o 2o) +o ๐‘‹) โˆˆ N โˆง 1o โˆˆ N) โ†’ โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ โˆˆ (N ร— N))
6333, 16, 62sylancl 413 . . . . . . . 8 ((๐‘‹ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ โˆˆ (N ร— N))
6456ecelqsi 6607 . . . . . . . 8 (โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ โˆˆ (N ร— N) โ†’ [โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q โˆˆ ((N ร— N) / ~Q ))
6563, 64syl 14 . . . . . . 7 ((๐‘‹ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ [โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q โˆˆ ((N ร— N) / ~Q ))
6665, 59eleqtrrdi 2283 . . . . . 6 ((๐‘‹ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ [โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q โˆˆ Q)
6766adantlr 477 . . . . 5 (((๐‘‹ โˆˆ ฯ‰ โˆง (โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐ด โˆˆ ๐ฟ โˆง ๐‘ƒ โˆˆ Q)) โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ [โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q โˆˆ Q)
68 simplr3 1043 . . . . 5 (((๐‘‹ โˆˆ ฯ‰ โˆง (โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐ด โˆˆ ๐ฟ โˆง ๐‘ƒ โˆˆ Q)) โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ๐‘ƒ โˆˆ Q)
69 ltmnqg 7418 . . . . 5 (([โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q โˆˆ Q โˆง [โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q โˆˆ Q โˆง ๐‘ƒ โˆˆ Q) โ†’ ([โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q <Q [โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q โ†” (๐‘ƒ ยทQ [โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q ) <Q (๐‘ƒ ยทQ [โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q )))
7061, 67, 68, 69syl3anc 1249 . . . 4 (((๐‘‹ โˆˆ ฯ‰ โˆง (โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐ด โˆˆ ๐ฟ โˆง ๐‘ƒ โˆˆ Q)) โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ([โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q <Q [โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q โ†” (๐‘ƒ ยทQ [โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q ) <Q (๐‘ƒ ยทQ [โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q )))
7153, 70mpbid 147 . . 3 (((๐‘‹ โˆˆ ฯ‰ โˆง (โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐ด โˆˆ ๐ฟ โˆง ๐‘ƒ โˆˆ Q)) โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (๐‘ƒ ยทQ [โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q ) <Q (๐‘ƒ ยทQ [โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q ))
72 mulcomnqg 7400 . . . . 5 ((๐‘ƒ โˆˆ Q โˆง [โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q โˆˆ Q) โ†’ (๐‘ƒ ยทQ [โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q ) = ([โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q ยทQ ๐‘ƒ))
7368, 61, 72syl2anc 411 . . . 4 (((๐‘‹ โˆˆ ฯ‰ โˆง (โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐ด โˆˆ ๐ฟ โˆง ๐‘ƒ โˆˆ Q)) โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (๐‘ƒ ยทQ [โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q ) = ([โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q ยทQ ๐‘ƒ))
74 mulcomnqg 7400 . . . . 5 ((๐‘ƒ โˆˆ Q โˆง [โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q โˆˆ Q) โ†’ (๐‘ƒ ยทQ [โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q ) = ([โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ))
7568, 67, 74syl2anc 411 . . . 4 (((๐‘‹ โˆˆ ฯ‰ โˆง (โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐ด โˆˆ ๐ฟ โˆง ๐‘ƒ โˆˆ Q)) โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (๐‘ƒ ยทQ [โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q ) = ([โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ))
7673, 75breq12d 4031 . . 3 (((๐‘‹ โˆˆ ฯ‰ โˆง (โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐ด โˆˆ ๐ฟ โˆง ๐‘ƒ โˆˆ Q)) โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ((๐‘ƒ ยทQ [โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q ) <Q (๐‘ƒ ยทQ [โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q ) โ†” ([โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q ยทQ ๐‘ƒ) <Q ([โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ)))
7771, 76mpbid 147 . 2 (((๐‘‹ โˆˆ ฯ‰ โˆง (โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐ด โˆˆ ๐ฟ โˆง ๐‘ƒ โˆˆ Q)) โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ([โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q ยทQ ๐‘ƒ) <Q ([โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ))
78 mulclnq 7393 . . . 4 (([โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q โˆˆ Q โˆง ๐‘ƒ โˆˆ Q) โ†’ ([โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q ยทQ ๐‘ƒ) โˆˆ Q)
7961, 68, 78syl2anc 411 . . 3 (((๐‘‹ โˆˆ ฯ‰ โˆง (โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐ด โˆˆ ๐ฟ โˆง ๐‘ƒ โˆˆ Q)) โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ([โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q ยทQ ๐‘ƒ) โˆˆ Q)
80 mulclnq 7393 . . . 4 (([โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q โˆˆ Q โˆง ๐‘ƒ โˆˆ Q) โ†’ ([โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ) โˆˆ Q)
8167, 68, 80syl2anc 411 . . 3 (((๐‘‹ โˆˆ ฯ‰ โˆง (โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐ด โˆˆ ๐ฟ โˆง ๐‘ƒ โˆˆ Q)) โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ([โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ) โˆˆ Q)
82 simplr1 1041 . . . 4 (((๐‘‹ โˆˆ ฯ‰ โˆง (โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐ด โˆˆ ๐ฟ โˆง ๐‘ƒ โˆˆ Q)) โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P)
83 simplr2 1042 . . . 4 (((๐‘‹ โˆˆ ฯ‰ โˆง (โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐ด โˆˆ ๐ฟ โˆง ๐‘ƒ โˆˆ Q)) โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ๐ด โˆˆ ๐ฟ)
84 elprnql 7498 . . . 4 ((โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐ด โˆˆ ๐ฟ) โ†’ ๐ด โˆˆ Q)
8582, 83, 84syl2anc 411 . . 3 (((๐‘‹ โˆˆ ฯ‰ โˆง (โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐ด โˆˆ ๐ฟ โˆง ๐‘ƒ โˆˆ Q)) โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ๐ด โˆˆ Q)
86 ltanqg 7417 . . 3 ((([โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q ยทQ ๐‘ƒ) โˆˆ Q โˆง ([โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ) โˆˆ Q โˆง ๐ด โˆˆ Q) โ†’ (([โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q ยทQ ๐‘ƒ) <Q ([โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ) โ†” (๐ด +Q ([โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q ยทQ ๐‘ƒ)) <Q (๐ด +Q ([โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ))))
8779, 81, 85, 86syl3anc 1249 . 2 (((๐‘‹ โˆˆ ฯ‰ โˆง (โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐ด โˆˆ ๐ฟ โˆง ๐‘ƒ โˆˆ Q)) โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (([โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q ยทQ ๐‘ƒ) <Q ([โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ) โ†” (๐ด +Q ([โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q ยทQ ๐‘ƒ)) <Q (๐ด +Q ([โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ))))
8877, 87mpbid 147 1 (((๐‘‹ โˆˆ ฯ‰ โˆง (โŸจ๐ฟ, ๐‘ˆโŸฉ โˆˆ P โˆง ๐ด โˆˆ ๐ฟ โˆง ๐‘ƒ โˆˆ Q)) โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (๐ด +Q ([โŸจ(๐‘ฆ +o 1o), 1oโŸฉ] ~Q ยทQ ๐‘ƒ)) <Q (๐ด +Q ([โŸจ((๐‘ฆ +o 2o) +o ๐‘‹), 1oโŸฉ] ~Q ยทQ ๐‘ƒ)))
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   โ†” wb 105   โˆง w3a 980   = wceq 1364   โˆˆ wcel 2160   โІ wss 3144  โŸจcop 3610   class class class wbr 4018  suc csuc 4380  ฯ‰com 4604   ร— cxp 4639  (class class class)co 5891  1oc1o 6428  2oc2o 6429   +o coa 6432  [cec 6551   / cqs 6552  Ncnpi 7289   ยทN cmi 7291   <N clti 7292   ~Q ceq 7296  Qcnq 7297   +Q cplq 7299   ยทQ cmq 7300   <Q cltq 7302  Pcnp 7308
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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4133  ax-sep 4136  ax-nul 4144  ax-pow 4189  ax-pr 4224  ax-un 4448  ax-setind 4551  ax-iinf 4602
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-ral 2473  df-rex 2474  df-reu 2475  df-rab 2477  df-v 2754  df-sbc 2978  df-csb 3073  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-nul 3438  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-iun 3903  df-br 4019  df-opab 4080  df-mpt 4081  df-tr 4117  df-eprel 4304  df-id 4308  df-iord 4381  df-on 4383  df-suc 4386  df-iom 4605  df-xp 4647  df-rel 4648  df-cnv 4649  df-co 4650  df-dm 4651  df-rn 4652  df-res 4653  df-ima 4654  df-iota 5193  df-fun 5233  df-fn 5234  df-f 5235  df-f1 5236  df-fo 5237  df-f1o 5238  df-fv 5239  df-ov 5894  df-oprab 5895  df-mpo 5896  df-1st 6159  df-2nd 6160  df-recs 6324  df-irdg 6389  df-1o 6435  df-2o 6436  df-oadd 6439  df-omul 6440  df-er 6553  df-ec 6555  df-qs 6559  df-ni 7321  df-pli 7322  df-mi 7323  df-lti 7324  df-plpq 7361  df-mpq 7362  df-enq 7364  df-nqqs 7365  df-plqqs 7366  df-mqqs 7367  df-ltnqqs 7370  df-inp 7483
This theorem is referenced by:  prarloclem3step  7513
  Copyright terms: Public domain W3C validator