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

Theorem archnqq 7416
Description: For any fraction, there is an integer that is greater than it. This is also known as the "archimedean property". (Contributed by Jim Kingdon, 1-Dec-2019.)
Assertion
Ref Expression
archnqq (๐ด โˆˆ Q โ†’ โˆƒ๐‘ฅ โˆˆ N ๐ด <Q [โŸจ๐‘ฅ, 1oโŸฉ] ~Q )
Distinct variable group:   ๐‘ฅ,๐ด

Proof of Theorem archnqq
Dummy variables ๐‘ค ๐‘ง are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nqpi 7377 . 2 (๐ด โˆˆ Q โ†’ โˆƒ๐‘งโˆƒ๐‘ค((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง ๐ด = [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q ))
2 1pi 7314 . . . . . . 7 1o โˆˆ N
3 addclpi 7326 . . . . . . 7 ((๐‘ง โˆˆ N โˆง 1o โˆˆ N) โ†’ (๐‘ง +N 1o) โˆˆ N)
42, 3mpan2 425 . . . . . 6 (๐‘ง โˆˆ N โ†’ (๐‘ง +N 1o) โˆˆ N)
54adantr 276 . . . . 5 ((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ (๐‘ง +N 1o) โˆˆ N)
65adantr 276 . . . 4 (((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง ๐ด = [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q ) โ†’ (๐‘ง +N 1o) โˆˆ N)
7 pinn 7308 . . . . . . . . . . . . . 14 (๐‘ง โˆˆ N โ†’ ๐‘ง โˆˆ ฯ‰)
8 1onn 6521 . . . . . . . . . . . . . 14 1o โˆˆ ฯ‰
9 nnacl 6481 . . . . . . . . . . . . . 14 ((๐‘ง โˆˆ ฯ‰ โˆง 1o โˆˆ ฯ‰) โ†’ (๐‘ง +o 1o) โˆˆ ฯ‰)
107, 8, 9sylancl 413 . . . . . . . . . . . . 13 (๐‘ง โˆˆ N โ†’ (๐‘ง +o 1o) โˆˆ ฯ‰)
1110adantr 276 . . . . . . . . . . . 12 ((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ (๐‘ง +o 1o) โˆˆ ฯ‰)
12 nnm1 6526 . . . . . . . . . . . 12 ((๐‘ง +o 1o) โˆˆ ฯ‰ โ†’ ((๐‘ง +o 1o) ยทo 1o) = (๐‘ง +o 1o))
1311, 12syl 14 . . . . . . . . . . 11 ((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ ((๐‘ง +o 1o) ยทo 1o) = (๐‘ง +o 1o))
14 elni2 7313 . . . . . . . . . . . . . 14 (๐‘ค โˆˆ N โ†” (๐‘ค โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐‘ค))
15 nnord 4612 . . . . . . . . . . . . . . 15 (๐‘ค โˆˆ ฯ‰ โ†’ Ord ๐‘ค)
16 ordgt0ge1 6436 . . . . . . . . . . . . . . . 16 (Ord ๐‘ค โ†’ (โˆ… โˆˆ ๐‘ค โ†” 1o โŠ† ๐‘ค))
1716biimpa 296 . . . . . . . . . . . . . . 15 ((Ord ๐‘ค โˆง โˆ… โˆˆ ๐‘ค) โ†’ 1o โŠ† ๐‘ค)
1815, 17sylan 283 . . . . . . . . . . . . . 14 ((๐‘ค โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐‘ค) โ†’ 1o โŠ† ๐‘ค)
1914, 18sylbi 121 . . . . . . . . . . . . 13 (๐‘ค โˆˆ N โ†’ 1o โŠ† ๐‘ค)
2019adantl 277 . . . . . . . . . . . 12 ((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ 1o โŠ† ๐‘ค)
21 pinn 7308 . . . . . . . . . . . . . 14 (๐‘ค โˆˆ N โ†’ ๐‘ค โˆˆ ฯ‰)
2221adantl 277 . . . . . . . . . . . . 13 ((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ ๐‘ค โˆˆ ฯ‰)
23 nnaword1 6514 . . . . . . . . . . . . . . . 16 ((๐‘ง โˆˆ ฯ‰ โˆง 1o โˆˆ ฯ‰) โ†’ ๐‘ง โŠ† (๐‘ง +o 1o))
247, 8, 23sylancl 413 . . . . . . . . . . . . . . 15 (๐‘ง โˆˆ N โ†’ ๐‘ง โŠ† (๐‘ง +o 1o))
25 elni2 7313 . . . . . . . . . . . . . . . 16 (๐‘ง โˆˆ N โ†” (๐‘ง โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐‘ง))
2625simprbi 275 . . . . . . . . . . . . . . 15 (๐‘ง โˆˆ N โ†’ โˆ… โˆˆ ๐‘ง)
2724, 26sseldd 3157 . . . . . . . . . . . . . 14 (๐‘ง โˆˆ N โ†’ โˆ… โˆˆ (๐‘ง +o 1o))
2827adantr 276 . . . . . . . . . . . . 13 ((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ โˆ… โˆˆ (๐‘ง +o 1o))
29 nnmword 6519 . . . . . . . . . . . . . 14 (((1o โˆˆ ฯ‰ โˆง ๐‘ค โˆˆ ฯ‰ โˆง (๐‘ง +o 1o) โˆˆ ฯ‰) โˆง โˆ… โˆˆ (๐‘ง +o 1o)) โ†’ (1o โŠ† ๐‘ค โ†” ((๐‘ง +o 1o) ยทo 1o) โŠ† ((๐‘ง +o 1o) ยทo ๐‘ค)))
308, 29mp3anl1 1331 . . . . . . . . . . . . 13 (((๐‘ค โˆˆ ฯ‰ โˆง (๐‘ง +o 1o) โˆˆ ฯ‰) โˆง โˆ… โˆˆ (๐‘ง +o 1o)) โ†’ (1o โŠ† ๐‘ค โ†” ((๐‘ง +o 1o) ยทo 1o) โŠ† ((๐‘ง +o 1o) ยทo ๐‘ค)))
3122, 11, 28, 30syl21anc 1237 . . . . . . . . . . . 12 ((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ (1o โŠ† ๐‘ค โ†” ((๐‘ง +o 1o) ยทo 1o) โŠ† ((๐‘ง +o 1o) ยทo ๐‘ค)))
3220, 31mpbid 147 . . . . . . . . . . 11 ((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ ((๐‘ง +o 1o) ยทo 1o) โŠ† ((๐‘ง +o 1o) ยทo ๐‘ค))
3313, 32eqsstrrd 3193 . . . . . . . . . 10 ((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ (๐‘ง +o 1o) โŠ† ((๐‘ง +o 1o) ยทo ๐‘ค))
34 nna0 6475 . . . . . . . . . . . . 13 (๐‘ง โˆˆ ฯ‰ โ†’ (๐‘ง +o โˆ…) = ๐‘ง)
35 0lt1o 6441 . . . . . . . . . . . . . 14 โˆ… โˆˆ 1o
36 nnaordi 6509 . . . . . . . . . . . . . . 15 ((1o โˆˆ ฯ‰ โˆง ๐‘ง โˆˆ ฯ‰) โ†’ (โˆ… โˆˆ 1o โ†’ (๐‘ง +o โˆ…) โˆˆ (๐‘ง +o 1o)))
378, 36mpan 424 . . . . . . . . . . . . . 14 (๐‘ง โˆˆ ฯ‰ โ†’ (โˆ… โˆˆ 1o โ†’ (๐‘ง +o โˆ…) โˆˆ (๐‘ง +o 1o)))
3835, 37mpi 15 . . . . . . . . . . . . 13 (๐‘ง โˆˆ ฯ‰ โ†’ (๐‘ง +o โˆ…) โˆˆ (๐‘ง +o 1o))
3934, 38eqeltrrd 2255 . . . . . . . . . . . 12 (๐‘ง โˆˆ ฯ‰ โ†’ ๐‘ง โˆˆ (๐‘ง +o 1o))
407, 39syl 14 . . . . . . . . . . 11 (๐‘ง โˆˆ N โ†’ ๐‘ง โˆˆ (๐‘ง +o 1o))
4140adantr 276 . . . . . . . . . 10 ((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ ๐‘ง โˆˆ (๐‘ง +o 1o))
4233, 41sseldd 3157 . . . . . . . . 9 ((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ ๐‘ง โˆˆ ((๐‘ง +o 1o) ยทo ๐‘ค))
43 mulclpi 7327 . . . . . . . . . . . 12 (((๐‘ง +N 1o) โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ ((๐‘ง +N 1o) ยทN ๐‘ค) โˆˆ N)
444, 43sylan 283 . . . . . . . . . . 11 ((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ ((๐‘ง +N 1o) ยทN ๐‘ค) โˆˆ N)
45 ltpiord 7318 . . . . . . . . . . 11 ((๐‘ง โˆˆ N โˆง ((๐‘ง +N 1o) ยทN ๐‘ค) โˆˆ N) โ†’ (๐‘ง <N ((๐‘ง +N 1o) ยทN ๐‘ค) โ†” ๐‘ง โˆˆ ((๐‘ง +N 1o) ยทN ๐‘ค)))
4644, 45syldan 282 . . . . . . . . . 10 ((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ (๐‘ง <N ((๐‘ง +N 1o) ยทN ๐‘ค) โ†” ๐‘ง โˆˆ ((๐‘ง +N 1o) ยทN ๐‘ค)))
47 mulpiord 7316 . . . . . . . . . . . . 13 (((๐‘ง +N 1o) โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ ((๐‘ง +N 1o) ยทN ๐‘ค) = ((๐‘ง +N 1o) ยทo ๐‘ค))
484, 47sylan 283 . . . . . . . . . . . 12 ((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ ((๐‘ง +N 1o) ยทN ๐‘ค) = ((๐‘ง +N 1o) ยทo ๐‘ค))
49 addpiord 7315 . . . . . . . . . . . . . . 15 ((๐‘ง โˆˆ N โˆง 1o โˆˆ N) โ†’ (๐‘ง +N 1o) = (๐‘ง +o 1o))
502, 49mpan2 425 . . . . . . . . . . . . . 14 (๐‘ง โˆˆ N โ†’ (๐‘ง +N 1o) = (๐‘ง +o 1o))
5150adantr 276 . . . . . . . . . . . . 13 ((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ (๐‘ง +N 1o) = (๐‘ง +o 1o))
5251oveq1d 5890 . . . . . . . . . . . 12 ((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ ((๐‘ง +N 1o) ยทo ๐‘ค) = ((๐‘ง +o 1o) ยทo ๐‘ค))
5348, 52eqtrd 2210 . . . . . . . . . . 11 ((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ ((๐‘ง +N 1o) ยทN ๐‘ค) = ((๐‘ง +o 1o) ยทo ๐‘ค))
5453eleq2d 2247 . . . . . . . . . 10 ((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ (๐‘ง โˆˆ ((๐‘ง +N 1o) ยทN ๐‘ค) โ†” ๐‘ง โˆˆ ((๐‘ง +o 1o) ยทo ๐‘ค)))
5546, 54bitrd 188 . . . . . . . . 9 ((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ (๐‘ง <N ((๐‘ง +N 1o) ยทN ๐‘ค) โ†” ๐‘ง โˆˆ ((๐‘ง +o 1o) ยทo ๐‘ค)))
5642, 55mpbird 167 . . . . . . . 8 ((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ ๐‘ง <N ((๐‘ง +N 1o) ยทN ๐‘ค))
57 mulcompig 7330 . . . . . . . . . 10 (((๐‘ง +N 1o) โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ ((๐‘ง +N 1o) ยทN ๐‘ค) = (๐‘ค ยทN (๐‘ง +N 1o)))
584, 57sylan 283 . . . . . . . . 9 ((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ ((๐‘ง +N 1o) ยทN ๐‘ค) = (๐‘ค ยทN (๐‘ง +N 1o)))
5958breq2d 4016 . . . . . . . 8 ((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ (๐‘ง <N ((๐‘ง +N 1o) ยทN ๐‘ค) โ†” ๐‘ง <N (๐‘ค ยทN (๐‘ง +N 1o))))
6056, 59mpbid 147 . . . . . . 7 ((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ ๐‘ง <N (๐‘ค ยทN (๐‘ง +N 1o)))
615, 2jctir 313 . . . . . . . . 9 ((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ ((๐‘ง +N 1o) โˆˆ N โˆง 1o โˆˆ N))
62 ordpipqqs 7373 . . . . . . . . 9 (((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง ((๐‘ง +N 1o) โˆˆ N โˆง 1o โˆˆ N)) โ†’ ([โŸจ๐‘ง, ๐‘คโŸฉ] ~Q <Q [โŸจ(๐‘ง +N 1o), 1oโŸฉ] ~Q โ†” (๐‘ง ยทN 1o) <N (๐‘ค ยทN (๐‘ง +N 1o))))
6361, 62mpdan 421 . . . . . . . 8 ((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ ([โŸจ๐‘ง, ๐‘คโŸฉ] ~Q <Q [โŸจ(๐‘ง +N 1o), 1oโŸฉ] ~Q โ†” (๐‘ง ยทN 1o) <N (๐‘ค ยทN (๐‘ง +N 1o))))
64 mulidpi 7317 . . . . . . . . . 10 (๐‘ง โˆˆ N โ†’ (๐‘ง ยทN 1o) = ๐‘ง)
6564adantr 276 . . . . . . . . 9 ((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ (๐‘ง ยทN 1o) = ๐‘ง)
6665breq1d 4014 . . . . . . . 8 ((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ ((๐‘ง ยทN 1o) <N (๐‘ค ยทN (๐‘ง +N 1o)) โ†” ๐‘ง <N (๐‘ค ยทN (๐‘ง +N 1o))))
6763, 66bitrd 188 . . . . . . 7 ((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ ([โŸจ๐‘ง, ๐‘คโŸฉ] ~Q <Q [โŸจ(๐‘ง +N 1o), 1oโŸฉ] ~Q โ†” ๐‘ง <N (๐‘ค ยทN (๐‘ง +N 1o))))
6860, 67mpbird 167 . . . . . 6 ((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โ†’ [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q <Q [โŸจ(๐‘ง +N 1o), 1oโŸฉ] ~Q )
6968adantr 276 . . . . 5 (((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง ๐ด = [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q ) โ†’ [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q <Q [โŸจ(๐‘ง +N 1o), 1oโŸฉ] ~Q )
70 breq1 4007 . . . . . 6 (๐ด = [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q โ†’ (๐ด <Q [โŸจ(๐‘ง +N 1o), 1oโŸฉ] ~Q โ†” [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q <Q [โŸจ(๐‘ง +N 1o), 1oโŸฉ] ~Q ))
7170adantl 277 . . . . 5 (((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง ๐ด = [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q ) โ†’ (๐ด <Q [โŸจ(๐‘ง +N 1o), 1oโŸฉ] ~Q โ†” [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q <Q [โŸจ(๐‘ง +N 1o), 1oโŸฉ] ~Q ))
7269, 71mpbird 167 . . . 4 (((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง ๐ด = [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q ) โ†’ ๐ด <Q [โŸจ(๐‘ง +N 1o), 1oโŸฉ] ~Q )
73 opeq1 3779 . . . . . . 7 (๐‘ฅ = (๐‘ง +N 1o) โ†’ โŸจ๐‘ฅ, 1oโŸฉ = โŸจ(๐‘ง +N 1o), 1oโŸฉ)
7473eceq1d 6571 . . . . . 6 (๐‘ฅ = (๐‘ง +N 1o) โ†’ [โŸจ๐‘ฅ, 1oโŸฉ] ~Q = [โŸจ(๐‘ง +N 1o), 1oโŸฉ] ~Q )
7574breq2d 4016 . . . . 5 (๐‘ฅ = (๐‘ง +N 1o) โ†’ (๐ด <Q [โŸจ๐‘ฅ, 1oโŸฉ] ~Q โ†” ๐ด <Q [โŸจ(๐‘ง +N 1o), 1oโŸฉ] ~Q ))
7675rspcev 2842 . . . 4 (((๐‘ง +N 1o) โˆˆ N โˆง ๐ด <Q [โŸจ(๐‘ง +N 1o), 1oโŸฉ] ~Q ) โ†’ โˆƒ๐‘ฅ โˆˆ N ๐ด <Q [โŸจ๐‘ฅ, 1oโŸฉ] ~Q )
776, 72, 76syl2anc 411 . . 3 (((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง ๐ด = [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q ) โ†’ โˆƒ๐‘ฅ โˆˆ N ๐ด <Q [โŸจ๐‘ฅ, 1oโŸฉ] ~Q )
7877exlimivv 1896 . 2 (โˆƒ๐‘งโˆƒ๐‘ค((๐‘ง โˆˆ N โˆง ๐‘ค โˆˆ N) โˆง ๐ด = [โŸจ๐‘ง, ๐‘คโŸฉ] ~Q ) โ†’ โˆƒ๐‘ฅ โˆˆ N ๐ด <Q [โŸจ๐‘ฅ, 1oโŸฉ] ~Q )
791, 78syl 14 1 (๐ด โˆˆ Q โ†’ โˆƒ๐‘ฅ โˆˆ N ๐ด <Q [โŸจ๐‘ฅ, 1oโŸฉ] ~Q )
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   โ†” wb 105   = wceq 1353  โˆƒwex 1492   โˆˆ wcel 2148  โˆƒwrex 2456   โŠ† wss 3130  โˆ…c0 3423  โŸจcop 3596   class class class wbr 4004  Ord word 4363  ฯ‰com 4590  (class class class)co 5875  1oc1o 6410   +o coa 6414   ยทo comu 6415  [cec 6533  Ncnpi 7271   +N cpli 7272   ยทN cmi 7273   <N clti 7274   ~Q ceq 7278  Qcnq 7279   <Q cltq 7284
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 4119  ax-sep 4122  ax-nul 4130  ax-pow 4175  ax-pr 4210  ax-un 4434  ax-setind 4537  ax-iinf 4588
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 2740  df-sbc 2964  df-csb 3059  df-dif 3132  df-un 3134  df-in 3136  df-ss 3143  df-nul 3424  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-int 3846  df-iun 3889  df-br 4005  df-opab 4066  df-mpt 4067  df-tr 4103  df-eprel 4290  df-id 4294  df-iord 4367  df-on 4369  df-suc 4372  df-iom 4591  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-rn 4638  df-res 4639  df-ima 4640  df-iota 5179  df-fun 5219  df-fn 5220  df-f 5221  df-f1 5222  df-fo 5223  df-f1o 5224  df-fv 5225  df-ov 5878  df-oprab 5879  df-mpo 5880  df-1st 6141  df-2nd 6142  df-recs 6306  df-irdg 6371  df-1o 6417  df-oadd 6421  df-omul 6422  df-er 6535  df-ec 6537  df-qs 6541  df-ni 7303  df-pli 7304  df-mi 7305  df-lti 7306  df-enq 7346  df-nqqs 7347  df-ltnqqs 7352
This theorem is referenced by:  prarloclemarch  7417  nqprm  7541  archpr  7642  archrecnq  7662
  Copyright terms: Public domain W3C validator