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

Theorem prarloclemarch2 7420
Description: Like prarloclemarch 7419 but the integer must be at least two, and there is also ๐ต added to the right hand side. These details follow straightforwardly but are chosen to be helpful in the proof of prarloc 7504. (Contributed by Jim Kingdon, 25-Nov-2019.)
Assertion
Ref Expression
prarloclemarch2 ((๐ด โˆˆ Q โˆง ๐ต โˆˆ Q โˆง ๐ถ โˆˆ Q) โ†’ โˆƒ๐‘ฅ โˆˆ N (1o <N ๐‘ฅ โˆง ๐ด <Q (๐ต +Q ([โŸจ๐‘ฅ, 1oโŸฉ] ~Q ยทQ ๐ถ))))
Distinct variable groups:   ๐‘ฅ,๐ด   ๐‘ฅ,๐ต   ๐‘ฅ,๐ถ

Proof of Theorem prarloclemarch2
Dummy variable ๐‘ง is distinct from all other variables.
StepHypRef Expression
1 prarloclemarch 7419 . . 3 ((๐ด โˆˆ Q โˆง ๐ถ โˆˆ Q) โ†’ โˆƒ๐‘ง โˆˆ N ๐ด <Q ([โŸจ๐‘ง, 1oโŸฉ] ~Q ยทQ ๐ถ))
213adant2 1016 . 2 ((๐ด โˆˆ Q โˆง ๐ต โˆˆ Q โˆง ๐ถ โˆˆ Q) โ†’ โˆƒ๐‘ง โˆˆ N ๐ด <Q ([โŸจ๐‘ง, 1oโŸฉ] ~Q ยทQ ๐ถ))
3 pinn 7310 . . . . . . . 8 (๐‘ง โˆˆ N โ†’ ๐‘ง โˆˆ ฯ‰)
4 1pi 7316 . . . . . . . . . . . 12 1o โˆˆ N
54elexi 2751 . . . . . . . . . . 11 1o โˆˆ V
65sucid 4419 . . . . . . . . . 10 1o โˆˆ suc 1o
7 df-2o 6420 . . . . . . . . . 10 2o = suc 1o
86, 7eleqtrri 2253 . . . . . . . . 9 1o โˆˆ 2o
9 2onn 6524 . . . . . . . . . . 11 2o โˆˆ ฯ‰
10 nnaword2 6517 . . . . . . . . . . 11 ((2o โˆˆ ฯ‰ โˆง ๐‘ง โˆˆ ฯ‰) โ†’ 2o โІ (๐‘ง +o 2o))
119, 10mpan 424 . . . . . . . . . 10 (๐‘ง โˆˆ ฯ‰ โ†’ 2o โІ (๐‘ง +o 2o))
1211sseld 3156 . . . . . . . . 9 (๐‘ง โˆˆ ฯ‰ โ†’ (1o โˆˆ 2o โ†’ 1o โˆˆ (๐‘ง +o 2o)))
138, 12mpi 15 . . . . . . . 8 (๐‘ง โˆˆ ฯ‰ โ†’ 1o โˆˆ (๐‘ง +o 2o))
143, 13syl 14 . . . . . . 7 (๐‘ง โˆˆ N โ†’ 1o โˆˆ (๐‘ง +o 2o))
15 o1p1e2 6471 . . . . . . . . 9 (1o +o 1o) = 2o
16 addpiord 7317 . . . . . . . . . . 11 ((1o โˆˆ N โˆง 1o โˆˆ N) โ†’ (1o +N 1o) = (1o +o 1o))
174, 4, 16mp2an 426 . . . . . . . . . 10 (1o +N 1o) = (1o +o 1o)
18 addclpi 7328 . . . . . . . . . . 11 ((1o โˆˆ N โˆง 1o โˆˆ N) โ†’ (1o +N 1o) โˆˆ N)
194, 4, 18mp2an 426 . . . . . . . . . 10 (1o +N 1o) โˆˆ N
2017, 19eqeltrri 2251 . . . . . . . . 9 (1o +o 1o) โˆˆ N
2115, 20eqeltrri 2251 . . . . . . . 8 2o โˆˆ N
22 addpiord 7317 . . . . . . . 8 ((๐‘ง โˆˆ N โˆง 2o โˆˆ N) โ†’ (๐‘ง +N 2o) = (๐‘ง +o 2o))
2321, 22mpan2 425 . . . . . . 7 (๐‘ง โˆˆ N โ†’ (๐‘ง +N 2o) = (๐‘ง +o 2o))
2414, 23eleqtrrd 2257 . . . . . 6 (๐‘ง โˆˆ N โ†’ 1o โˆˆ (๐‘ง +N 2o))
25 addclpi 7328 . . . . . . . 8 ((๐‘ง โˆˆ N โˆง 2o โˆˆ N) โ†’ (๐‘ง +N 2o) โˆˆ N)
2621, 25mpan2 425 . . . . . . 7 (๐‘ง โˆˆ N โ†’ (๐‘ง +N 2o) โˆˆ N)
27 ltpiord 7320 . . . . . . . 8 ((1o โˆˆ N โˆง (๐‘ง +N 2o) โˆˆ N) โ†’ (1o <N (๐‘ง +N 2o) โ†” 1o โˆˆ (๐‘ง +N 2o)))
284, 27mpan 424 . . . . . . 7 ((๐‘ง +N 2o) โˆˆ N โ†’ (1o <N (๐‘ง +N 2o) โ†” 1o โˆˆ (๐‘ง +N 2o)))
2926, 28syl 14 . . . . . 6 (๐‘ง โˆˆ N โ†’ (1o <N (๐‘ง +N 2o) โ†” 1o โˆˆ (๐‘ง +N 2o)))
3024, 29mpbird 167 . . . . 5 (๐‘ง โˆˆ N โ†’ 1o <N (๐‘ง +N 2o))
3130adantl 277 . . . 4 (((๐ด โˆˆ Q โˆง ๐ต โˆˆ Q โˆง ๐ถ โˆˆ Q) โˆง ๐‘ง โˆˆ N) โ†’ 1o <N (๐‘ง +N 2o))
3231adantrr 479 . . 3 (((๐ด โˆˆ Q โˆง ๐ต โˆˆ Q โˆง ๐ถ โˆˆ Q) โˆง (๐‘ง โˆˆ N โˆง ๐ด <Q ([โŸจ๐‘ง, 1oโŸฉ] ~Q ยทQ ๐ถ))) โ†’ 1o <N (๐‘ง +N 2o))
33 nna0 6477 . . . . . . . . . . . . . . . . 17 (๐‘ง โˆˆ ฯ‰ โ†’ (๐‘ง +o โˆ…) = ๐‘ง)
34 0lt1o 6443 . . . . . . . . . . . . . . . . . . . 20 โˆ… โˆˆ 1o
35 1on 6426 . . . . . . . . . . . . . . . . . . . . . 22 1o โˆˆ On
3635onsuci 4517 . . . . . . . . . . . . . . . . . . . . 21 suc 1o โˆˆ On
37 ontr1 4391 . . . . . . . . . . . . . . . . . . . . 21 (suc 1o โˆˆ On โ†’ ((โˆ… โˆˆ 1o โˆง 1o โˆˆ suc 1o) โ†’ โˆ… โˆˆ suc 1o))
3836, 37ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((โˆ… โˆˆ 1o โˆง 1o โˆˆ suc 1o) โ†’ โˆ… โˆˆ suc 1o)
3934, 6, 38mp2an 426 . . . . . . . . . . . . . . . . . . 19 โˆ… โˆˆ suc 1o
4039, 7eleqtrri 2253 . . . . . . . . . . . . . . . . . 18 โˆ… โˆˆ 2o
41 nnaordi 6511 . . . . . . . . . . . . . . . . . . 19 ((2o โˆˆ ฯ‰ โˆง ๐‘ง โˆˆ ฯ‰) โ†’ (โˆ… โˆˆ 2o โ†’ (๐‘ง +o โˆ…) โˆˆ (๐‘ง +o 2o)))
429, 41mpan 424 . . . . . . . . . . . . . . . . . 18 (๐‘ง โˆˆ ฯ‰ โ†’ (โˆ… โˆˆ 2o โ†’ (๐‘ง +o โˆ…) โˆˆ (๐‘ง +o 2o)))
4340, 42mpi 15 . . . . . . . . . . . . . . . . 17 (๐‘ง โˆˆ ฯ‰ โ†’ (๐‘ง +o โˆ…) โˆˆ (๐‘ง +o 2o))
4433, 43eqeltrrd 2255 . . . . . . . . . . . . . . . 16 (๐‘ง โˆˆ ฯ‰ โ†’ ๐‘ง โˆˆ (๐‘ง +o 2o))
453, 44syl 14 . . . . . . . . . . . . . . 15 (๐‘ง โˆˆ N โ†’ ๐‘ง โˆˆ (๐‘ง +o 2o))
4645, 23eleqtrrd 2257 . . . . . . . . . . . . . 14 (๐‘ง โˆˆ N โ†’ ๐‘ง โˆˆ (๐‘ง +N 2o))
47 ltpiord 7320 . . . . . . . . . . . . . . 15 ((๐‘ง โˆˆ N โˆง (๐‘ง +N 2o) โˆˆ N) โ†’ (๐‘ง <N (๐‘ง +N 2o) โ†” ๐‘ง โˆˆ (๐‘ง +N 2o)))
4826, 47mpdan 421 . . . . . . . . . . . . . 14 (๐‘ง โˆˆ N โ†’ (๐‘ง <N (๐‘ง +N 2o) โ†” ๐‘ง โˆˆ (๐‘ง +N 2o)))
4946, 48mpbird 167 . . . . . . . . . . . . 13 (๐‘ง โˆˆ N โ†’ ๐‘ง <N (๐‘ง +N 2o))
50 mulidpi 7319 . . . . . . . . . . . . 13 (๐‘ง โˆˆ N โ†’ (๐‘ง ยทN 1o) = ๐‘ง)
51 mulcompig 7332 . . . . . . . . . . . . . . . 16 (((๐‘ง +N 2o) โˆˆ N โˆง 1o โˆˆ N) โ†’ ((๐‘ง +N 2o) ยทN 1o) = (1o ยทN (๐‘ง +N 2o)))
524, 51mpan2 425 . . . . . . . . . . . . . . 15 ((๐‘ง +N 2o) โˆˆ N โ†’ ((๐‘ง +N 2o) ยทN 1o) = (1o ยทN (๐‘ง +N 2o)))
5326, 52syl 14 . . . . . . . . . . . . . 14 (๐‘ง โˆˆ N โ†’ ((๐‘ง +N 2o) ยทN 1o) = (1o ยทN (๐‘ง +N 2o)))
54 mulidpi 7319 . . . . . . . . . . . . . . 15 ((๐‘ง +N 2o) โˆˆ N โ†’ ((๐‘ง +N 2o) ยทN 1o) = (๐‘ง +N 2o))
5526, 54syl 14 . . . . . . . . . . . . . 14 (๐‘ง โˆˆ N โ†’ ((๐‘ง +N 2o) ยทN 1o) = (๐‘ง +N 2o))
5653, 55eqtr3d 2212 . . . . . . . . . . . . 13 (๐‘ง โˆˆ N โ†’ (1o ยทN (๐‘ง +N 2o)) = (๐‘ง +N 2o))
5749, 50, 563brtr4d 4037 . . . . . . . . . . . 12 (๐‘ง โˆˆ N โ†’ (๐‘ง ยทN 1o) <N (1o ยทN (๐‘ง +N 2o)))
58 ordpipqqs 7375 . . . . . . . . . . . . . . 15 (((๐‘ง โˆˆ N โˆง 1o โˆˆ N) โˆง ((๐‘ง +N 2o) โˆˆ N โˆง 1o โˆˆ N)) โ†’ ([โŸจ๐‘ง, 1oโŸฉ] ~Q <Q [โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q โ†” (๐‘ง ยทN 1o) <N (1o ยทN (๐‘ง +N 2o))))
594, 58mpanl2 435 . . . . . . . . . . . . . 14 ((๐‘ง โˆˆ N โˆง ((๐‘ง +N 2o) โˆˆ N โˆง 1o โˆˆ N)) โ†’ ([โŸจ๐‘ง, 1oโŸฉ] ~Q <Q [โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q โ†” (๐‘ง ยทN 1o) <N (1o ยทN (๐‘ง +N 2o))))
604, 59mpanr2 438 . . . . . . . . . . . . 13 ((๐‘ง โˆˆ N โˆง (๐‘ง +N 2o) โˆˆ N) โ†’ ([โŸจ๐‘ง, 1oโŸฉ] ~Q <Q [โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q โ†” (๐‘ง ยทN 1o) <N (1o ยทN (๐‘ง +N 2o))))
6126, 60mpdan 421 . . . . . . . . . . . 12 (๐‘ง โˆˆ N โ†’ ([โŸจ๐‘ง, 1oโŸฉ] ~Q <Q [โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q โ†” (๐‘ง ยทN 1o) <N (1o ยทN (๐‘ง +N 2o))))
6257, 61mpbird 167 . . . . . . . . . . 11 (๐‘ง โˆˆ N โ†’ [โŸจ๐‘ง, 1oโŸฉ] ~Q <Q [โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q )
6362adantl 277 . . . . . . . . . 10 ((๐ถ โˆˆ Q โˆง ๐‘ง โˆˆ N) โ†’ [โŸจ๐‘ง, 1oโŸฉ] ~Q <Q [โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q )
64 opelxpi 4660 . . . . . . . . . . . . . . . 16 (((๐‘ง +N 2o) โˆˆ N โˆง 1o โˆˆ N) โ†’ โŸจ(๐‘ง +N 2o), 1oโŸฉ โˆˆ (N ร— N))
654, 64mpan2 425 . . . . . . . . . . . . . . 15 ((๐‘ง +N 2o) โˆˆ N โ†’ โŸจ(๐‘ง +N 2o), 1oโŸฉ โˆˆ (N ร— N))
66 enqex 7361 . . . . . . . . . . . . . . . 16 ~Q โˆˆ V
6766ecelqsi 6591 . . . . . . . . . . . . . . 15 (โŸจ(๐‘ง +N 2o), 1oโŸฉ โˆˆ (N ร— N) โ†’ [โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q โˆˆ ((N ร— N) / ~Q ))
6826, 65, 673syl 17 . . . . . . . . . . . . . 14 (๐‘ง โˆˆ N โ†’ [โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q โˆˆ ((N ร— N) / ~Q ))
69 df-nqqs 7349 . . . . . . . . . . . . . 14 Q = ((N ร— N) / ~Q )
7068, 69eleqtrrdi 2271 . . . . . . . . . . . . 13 (๐‘ง โˆˆ N โ†’ [โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q โˆˆ Q)
71 opelxpi 4660 . . . . . . . . . . . . . . . . 17 ((๐‘ง โˆˆ N โˆง 1o โˆˆ N) โ†’ โŸจ๐‘ง, 1oโŸฉ โˆˆ (N ร— N))
724, 71mpan2 425 . . . . . . . . . . . . . . . 16 (๐‘ง โˆˆ N โ†’ โŸจ๐‘ง, 1oโŸฉ โˆˆ (N ร— N))
7366ecelqsi 6591 . . . . . . . . . . . . . . . 16 (โŸจ๐‘ง, 1oโŸฉ โˆˆ (N ร— N) โ†’ [โŸจ๐‘ง, 1oโŸฉ] ~Q โˆˆ ((N ร— N) / ~Q ))
7472, 73syl 14 . . . . . . . . . . . . . . 15 (๐‘ง โˆˆ N โ†’ [โŸจ๐‘ง, 1oโŸฉ] ~Q โˆˆ ((N ร— N) / ~Q ))
7574, 69eleqtrrdi 2271 . . . . . . . . . . . . . 14 (๐‘ง โˆˆ N โ†’ [โŸจ๐‘ง, 1oโŸฉ] ~Q โˆˆ Q)
76 ltmnqg 7402 . . . . . . . . . . . . . 14 (([โŸจ๐‘ง, 1oโŸฉ] ~Q โˆˆ Q โˆง [โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q โˆˆ Q โˆง ๐ถ โˆˆ Q) โ†’ ([โŸจ๐‘ง, 1oโŸฉ] ~Q <Q [โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q โ†” (๐ถ ยทQ [โŸจ๐‘ง, 1oโŸฉ] ~Q ) <Q (๐ถ ยทQ [โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q )))
7775, 76syl3an1 1271 . . . . . . . . . . . . 13 ((๐‘ง โˆˆ N โˆง [โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q โˆˆ Q โˆง ๐ถ โˆˆ Q) โ†’ ([โŸจ๐‘ง, 1oโŸฉ] ~Q <Q [โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q โ†” (๐ถ ยทQ [โŸจ๐‘ง, 1oโŸฉ] ~Q ) <Q (๐ถ ยทQ [โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q )))
7870, 77syl3an2 1272 . . . . . . . . . . . 12 ((๐‘ง โˆˆ N โˆง ๐‘ง โˆˆ N โˆง ๐ถ โˆˆ Q) โ†’ ([โŸจ๐‘ง, 1oโŸฉ] ~Q <Q [โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q โ†” (๐ถ ยทQ [โŸจ๐‘ง, 1oโŸฉ] ~Q ) <Q (๐ถ ยทQ [โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q )))
79783anidm12 1295 . . . . . . . . . . 11 ((๐‘ง โˆˆ N โˆง ๐ถ โˆˆ Q) โ†’ ([โŸจ๐‘ง, 1oโŸฉ] ~Q <Q [โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q โ†” (๐ถ ยทQ [โŸจ๐‘ง, 1oโŸฉ] ~Q ) <Q (๐ถ ยทQ [โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q )))
8079ancoms 268 . . . . . . . . . 10 ((๐ถ โˆˆ Q โˆง ๐‘ง โˆˆ N) โ†’ ([โŸจ๐‘ง, 1oโŸฉ] ~Q <Q [โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q โ†” (๐ถ ยทQ [โŸจ๐‘ง, 1oโŸฉ] ~Q ) <Q (๐ถ ยทQ [โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q )))
8163, 80mpbid 147 . . . . . . . . 9 ((๐ถ โˆˆ Q โˆง ๐‘ง โˆˆ N) โ†’ (๐ถ ยทQ [โŸจ๐‘ง, 1oโŸฉ] ~Q ) <Q (๐ถ ยทQ [โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ))
82 mulcomnqg 7384 . . . . . . . . . 10 ((๐ถ โˆˆ Q โˆง [โŸจ๐‘ง, 1oโŸฉ] ~Q โˆˆ Q) โ†’ (๐ถ ยทQ [โŸจ๐‘ง, 1oโŸฉ] ~Q ) = ([โŸจ๐‘ง, 1oโŸฉ] ~Q ยทQ ๐ถ))
8375, 82sylan2 286 . . . . . . . . 9 ((๐ถ โˆˆ Q โˆง ๐‘ง โˆˆ N) โ†’ (๐ถ ยทQ [โŸจ๐‘ง, 1oโŸฉ] ~Q ) = ([โŸจ๐‘ง, 1oโŸฉ] ~Q ยทQ ๐ถ))
84 mulcomnqg 7384 . . . . . . . . . 10 ((๐ถ โˆˆ Q โˆง [โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q โˆˆ Q) โ†’ (๐ถ ยทQ [โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ) = ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ))
8570, 84sylan2 286 . . . . . . . . 9 ((๐ถ โˆˆ Q โˆง ๐‘ง โˆˆ N) โ†’ (๐ถ ยทQ [โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ) = ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ))
8681, 83, 853brtr3d 4036 . . . . . . . 8 ((๐ถ โˆˆ Q โˆง ๐‘ง โˆˆ N) โ†’ ([โŸจ๐‘ง, 1oโŸฉ] ~Q ยทQ ๐ถ) <Q ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ))
87863ad2antl3 1161 . . . . . . 7 (((๐ด โˆˆ Q โˆง ๐ต โˆˆ Q โˆง ๐ถ โˆˆ Q) โˆง ๐‘ง โˆˆ N) โ†’ ([โŸจ๐‘ง, 1oโŸฉ] ~Q ยทQ ๐ถ) <Q ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ))
8887adantrr 479 . . . . . 6 (((๐ด โˆˆ Q โˆง ๐ต โˆˆ Q โˆง ๐ถ โˆˆ Q) โˆง (๐‘ง โˆˆ N โˆง ๐ด <Q ([โŸจ๐‘ง, 1oโŸฉ] ~Q ยทQ ๐ถ))) โ†’ ([โŸจ๐‘ง, 1oโŸฉ] ~Q ยทQ ๐ถ) <Q ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ))
89 ltsonq 7399 . . . . . . . . . 10 <Q Or Q
90 ltrelnq 7366 . . . . . . . . . 10 <Q โІ (Q ร— Q)
9189, 90sotri 5026 . . . . . . . . 9 ((๐ด <Q ([โŸจ๐‘ง, 1oโŸฉ] ~Q ยทQ ๐ถ) โˆง ([โŸจ๐‘ง, 1oโŸฉ] ~Q ยทQ ๐ถ) <Q ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ)) โ†’ ๐ด <Q ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ))
9291ex 115 . . . . . . . 8 (๐ด <Q ([โŸจ๐‘ง, 1oโŸฉ] ~Q ยทQ ๐ถ) โ†’ (([โŸจ๐‘ง, 1oโŸฉ] ~Q ยทQ ๐ถ) <Q ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ) โ†’ ๐ด <Q ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ)))
9392adantl 277 . . . . . . 7 ((๐‘ง โˆˆ N โˆง ๐ด <Q ([โŸจ๐‘ง, 1oโŸฉ] ~Q ยทQ ๐ถ)) โ†’ (([โŸจ๐‘ง, 1oโŸฉ] ~Q ยทQ ๐ถ) <Q ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ) โ†’ ๐ด <Q ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ)))
9493adantl 277 . . . . . 6 (((๐ด โˆˆ Q โˆง ๐ต โˆˆ Q โˆง ๐ถ โˆˆ Q) โˆง (๐‘ง โˆˆ N โˆง ๐ด <Q ([โŸจ๐‘ง, 1oโŸฉ] ~Q ยทQ ๐ถ))) โ†’ (([โŸจ๐‘ง, 1oโŸฉ] ~Q ยทQ ๐ถ) <Q ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ) โ†’ ๐ด <Q ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ)))
9588, 94mpd 13 . . . . 5 (((๐ด โˆˆ Q โˆง ๐ต โˆˆ Q โˆง ๐ถ โˆˆ Q) โˆง (๐‘ง โˆˆ N โˆง ๐ด <Q ([โŸจ๐‘ง, 1oโŸฉ] ~Q ยทQ ๐ถ))) โ†’ ๐ด <Q ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ))
96 mulclnq 7377 . . . . . . . . . 10 (([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q โˆˆ Q โˆง ๐ถ โˆˆ Q) โ†’ ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ) โˆˆ Q)
9770, 96sylan 283 . . . . . . . . 9 ((๐‘ง โˆˆ N โˆง ๐ถ โˆˆ Q) โ†’ ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ) โˆˆ Q)
9897ancoms 268 . . . . . . . 8 ((๐ถ โˆˆ Q โˆง ๐‘ง โˆˆ N) โ†’ ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ) โˆˆ Q)
99983ad2antl3 1161 . . . . . . 7 (((๐ด โˆˆ Q โˆง ๐ต โˆˆ Q โˆง ๐ถ โˆˆ Q) โˆง ๐‘ง โˆˆ N) โ†’ ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ) โˆˆ Q)
100 simpl2 1001 . . . . . . 7 (((๐ด โˆˆ Q โˆง ๐ต โˆˆ Q โˆง ๐ถ โˆˆ Q) โˆง ๐‘ง โˆˆ N) โ†’ ๐ต โˆˆ Q)
101 ltaddnq 7408 . . . . . . 7 ((([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ) โˆˆ Q โˆง ๐ต โˆˆ Q) โ†’ ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ) <Q (([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ) +Q ๐ต))
10299, 100, 101syl2anc 411 . . . . . 6 (((๐ด โˆˆ Q โˆง ๐ต โˆˆ Q โˆง ๐ถ โˆˆ Q) โˆง ๐‘ง โˆˆ N) โ†’ ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ) <Q (([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ) +Q ๐ต))
103102adantrr 479 . . . . 5 (((๐ด โˆˆ Q โˆง ๐ต โˆˆ Q โˆง ๐ถ โˆˆ Q) โˆง (๐‘ง โˆˆ N โˆง ๐ด <Q ([โŸจ๐‘ง, 1oโŸฉ] ~Q ยทQ ๐ถ))) โ†’ ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ) <Q (([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ) +Q ๐ต))
10489, 90sotri 5026 . . . . 5 ((๐ด <Q ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ) โˆง ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ) <Q (([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ) +Q ๐ต)) โ†’ ๐ด <Q (([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ) +Q ๐ต))
10595, 103, 104syl2anc 411 . . . 4 (((๐ด โˆˆ Q โˆง ๐ต โˆˆ Q โˆง ๐ถ โˆˆ Q) โˆง (๐‘ง โˆˆ N โˆง ๐ด <Q ([โŸจ๐‘ง, 1oโŸฉ] ~Q ยทQ ๐ถ))) โ†’ ๐ด <Q (([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ) +Q ๐ต))
106 addcomnqg 7382 . . . . . . 7 ((([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ) โˆˆ Q โˆง ๐ต โˆˆ Q) โ†’ (([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ) +Q ๐ต) = (๐ต +Q ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ)))
10799, 100, 106syl2anc 411 . . . . . 6 (((๐ด โˆˆ Q โˆง ๐ต โˆˆ Q โˆง ๐ถ โˆˆ Q) โˆง ๐‘ง โˆˆ N) โ†’ (([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ) +Q ๐ต) = (๐ต +Q ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ)))
108107breq2d 4017 . . . . 5 (((๐ด โˆˆ Q โˆง ๐ต โˆˆ Q โˆง ๐ถ โˆˆ Q) โˆง ๐‘ง โˆˆ N) โ†’ (๐ด <Q (([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ) +Q ๐ต) โ†” ๐ด <Q (๐ต +Q ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ))))
109108adantrr 479 . . . 4 (((๐ด โˆˆ Q โˆง ๐ต โˆˆ Q โˆง ๐ถ โˆˆ Q) โˆง (๐‘ง โˆˆ N โˆง ๐ด <Q ([โŸจ๐‘ง, 1oโŸฉ] ~Q ยทQ ๐ถ))) โ†’ (๐ด <Q (([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ) +Q ๐ต) โ†” ๐ด <Q (๐ต +Q ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ))))
110105, 109mpbid 147 . . 3 (((๐ด โˆˆ Q โˆง ๐ต โˆˆ Q โˆง ๐ถ โˆˆ Q) โˆง (๐‘ง โˆˆ N โˆง ๐ด <Q ([โŸจ๐‘ง, 1oโŸฉ] ~Q ยทQ ๐ถ))) โ†’ ๐ด <Q (๐ต +Q ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ)))
111 simpr 110 . . . . 5 (((๐ด โˆˆ Q โˆง ๐ต โˆˆ Q โˆง ๐ถ โˆˆ Q) โˆง ๐‘ง โˆˆ N) โ†’ ๐‘ง โˆˆ N)
112 breq2 4009 . . . . . . . 8 (๐‘ฅ = (๐‘ง +N 2o) โ†’ (1o <N ๐‘ฅ โ†” 1o <N (๐‘ง +N 2o)))
113 opeq1 3780 . . . . . . . . . . . 12 (๐‘ฅ = (๐‘ง +N 2o) โ†’ โŸจ๐‘ฅ, 1oโŸฉ = โŸจ(๐‘ง +N 2o), 1oโŸฉ)
114113eceq1d 6573 . . . . . . . . . . 11 (๐‘ฅ = (๐‘ง +N 2o) โ†’ [โŸจ๐‘ฅ, 1oโŸฉ] ~Q = [โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q )
115114oveq1d 5892 . . . . . . . . . 10 (๐‘ฅ = (๐‘ง +N 2o) โ†’ ([โŸจ๐‘ฅ, 1oโŸฉ] ~Q ยทQ ๐ถ) = ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ))
116115oveq2d 5893 . . . . . . . . 9 (๐‘ฅ = (๐‘ง +N 2o) โ†’ (๐ต +Q ([โŸจ๐‘ฅ, 1oโŸฉ] ~Q ยทQ ๐ถ)) = (๐ต +Q ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ)))
117116breq2d 4017 . . . . . . . 8 (๐‘ฅ = (๐‘ง +N 2o) โ†’ (๐ด <Q (๐ต +Q ([โŸจ๐‘ฅ, 1oโŸฉ] ~Q ยทQ ๐ถ)) โ†” ๐ด <Q (๐ต +Q ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ))))
118112, 117anbi12d 473 . . . . . . 7 (๐‘ฅ = (๐‘ง +N 2o) โ†’ ((1o <N ๐‘ฅ โˆง ๐ด <Q (๐ต +Q ([โŸจ๐‘ฅ, 1oโŸฉ] ~Q ยทQ ๐ถ))) โ†” (1o <N (๐‘ง +N 2o) โˆง ๐ด <Q (๐ต +Q ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ)))))
119118rspcev 2843 . . . . . 6 (((๐‘ง +N 2o) โˆˆ N โˆง (1o <N (๐‘ง +N 2o) โˆง ๐ด <Q (๐ต +Q ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ)))) โ†’ โˆƒ๐‘ฅ โˆˆ N (1o <N ๐‘ฅ โˆง ๐ด <Q (๐ต +Q ([โŸจ๐‘ฅ, 1oโŸฉ] ~Q ยทQ ๐ถ))))
120119ex 115 . . . . 5 ((๐‘ง +N 2o) โˆˆ N โ†’ ((1o <N (๐‘ง +N 2o) โˆง ๐ด <Q (๐ต +Q ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ))) โ†’ โˆƒ๐‘ฅ โˆˆ N (1o <N ๐‘ฅ โˆง ๐ด <Q (๐ต +Q ([โŸจ๐‘ฅ, 1oโŸฉ] ~Q ยทQ ๐ถ)))))
121111, 26, 1203syl 17 . . . 4 (((๐ด โˆˆ Q โˆง ๐ต โˆˆ Q โˆง ๐ถ โˆˆ Q) โˆง ๐‘ง โˆˆ N) โ†’ ((1o <N (๐‘ง +N 2o) โˆง ๐ด <Q (๐ต +Q ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ))) โ†’ โˆƒ๐‘ฅ โˆˆ N (1o <N ๐‘ฅ โˆง ๐ด <Q (๐ต +Q ([โŸจ๐‘ฅ, 1oโŸฉ] ~Q ยทQ ๐ถ)))))
122121adantrr 479 . . 3 (((๐ด โˆˆ Q โˆง ๐ต โˆˆ Q โˆง ๐ถ โˆˆ Q) โˆง (๐‘ง โˆˆ N โˆง ๐ด <Q ([โŸจ๐‘ง, 1oโŸฉ] ~Q ยทQ ๐ถ))) โ†’ ((1o <N (๐‘ง +N 2o) โˆง ๐ด <Q (๐ต +Q ([โŸจ(๐‘ง +N 2o), 1oโŸฉ] ~Q ยทQ ๐ถ))) โ†’ โˆƒ๐‘ฅ โˆˆ N (1o <N ๐‘ฅ โˆง ๐ด <Q (๐ต +Q ([โŸจ๐‘ฅ, 1oโŸฉ] ~Q ยทQ ๐ถ)))))
12332, 110, 122mp2and 433 . 2 (((๐ด โˆˆ Q โˆง ๐ต โˆˆ Q โˆง ๐ถ โˆˆ Q) โˆง (๐‘ง โˆˆ N โˆง ๐ด <Q ([โŸจ๐‘ง, 1oโŸฉ] ~Q ยทQ ๐ถ))) โ†’ โˆƒ๐‘ฅ โˆˆ N (1o <N ๐‘ฅ โˆง ๐ด <Q (๐ต +Q ([โŸจ๐‘ฅ, 1oโŸฉ] ~Q ยทQ ๐ถ))))
1242, 123rexlimddv 2599 1 ((๐ด โˆˆ Q โˆง ๐ต โˆˆ Q โˆง ๐ถ โˆˆ Q) โ†’ โˆƒ๐‘ฅ โˆˆ N (1o <N ๐‘ฅ โˆง ๐ด <Q (๐ต +Q ([โŸจ๐‘ฅ, 1oโŸฉ] ~Q ยทQ ๐ถ))))
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   โ†” wb 105   โˆง w3a 978   = wceq 1353   โˆˆ wcel 2148  โˆƒwrex 2456   โІ wss 3131  โˆ…c0 3424  โŸจcop 3597   class class class wbr 4005  Oncon0 4365  suc csuc 4367  ฯ‰com 4591   ร— cxp 4626  (class class class)co 5877  1oc1o 6412  2oc2o 6413   +o coa 6416  [cec 6535   / cqs 6536  Ncnpi 7273   +N cpli 7274   ยทN cmi 7275   <N clti 7276   ~Q ceq 7280  Qcnq 7281   +Q cplq 7283   ยทQ cmq 7284   <Q cltq 7286
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
This theorem is referenced by:  prarloc  7504
  Copyright terms: Public domain W3C validator