Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 1lt2nq | Structured version Visualization version GIF version |
Description: One is less than two (one plus one). (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.) |
Ref | Expression |
---|---|
1lt2nq | ⊢ 1Q <Q (1Q +Q 1Q) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1lt2pi 10484 | . . . . . 6 ⊢ 1o <N (1o +N 1o) | |
2 | 1pi 10462 | . . . . . . 7 ⊢ 1o ∈ N | |
3 | mulidpi 10465 | . . . . . . 7 ⊢ (1o ∈ N → (1o ·N 1o) = 1o) | |
4 | 2, 3 | ax-mp 5 | . . . . . 6 ⊢ (1o ·N 1o) = 1o |
5 | addclpi 10471 | . . . . . . . 8 ⊢ ((1o ∈ N ∧ 1o ∈ N) → (1o +N 1o) ∈ N) | |
6 | 2, 2, 5 | mp2an 692 | . . . . . . 7 ⊢ (1o +N 1o) ∈ N |
7 | mulidpi 10465 | . . . . . . 7 ⊢ ((1o +N 1o) ∈ N → ((1o +N 1o) ·N 1o) = (1o +N 1o)) | |
8 | 6, 7 | ax-mp 5 | . . . . . 6 ⊢ ((1o +N 1o) ·N 1o) = (1o +N 1o) |
9 | 1, 4, 8 | 3brtr4i 5069 | . . . . 5 ⊢ (1o ·N 1o) <N ((1o +N 1o) ·N 1o) |
10 | ordpipq 10521 | . . . . 5 ⊢ (〈1o, 1o〉 <pQ 〈(1o +N 1o), 1o〉 ↔ (1o ·N 1o) <N ((1o +N 1o) ·N 1o)) | |
11 | 9, 10 | mpbir 234 | . . . 4 ⊢ 〈1o, 1o〉 <pQ 〈(1o +N 1o), 1o〉 |
12 | df-1nq 10495 | . . . 4 ⊢ 1Q = 〈1o, 1o〉 | |
13 | 12, 12 | oveq12i 7203 | . . . . 5 ⊢ (1Q +pQ 1Q) = (〈1o, 1o〉 +pQ 〈1o, 1o〉) |
14 | addpipq 10516 | . . . . . 6 ⊢ (((1o ∈ N ∧ 1o ∈ N) ∧ (1o ∈ N ∧ 1o ∈ N)) → (〈1o, 1o〉 +pQ 〈1o, 1o〉) = 〈((1o ·N 1o) +N (1o ·N 1o)), (1o ·N 1o)〉) | |
15 | 2, 2, 2, 2, 14 | mp4an 693 | . . . . 5 ⊢ (〈1o, 1o〉 +pQ 〈1o, 1o〉) = 〈((1o ·N 1o) +N (1o ·N 1o)), (1o ·N 1o)〉 |
16 | 4, 4 | oveq12i 7203 | . . . . . 6 ⊢ ((1o ·N 1o) +N (1o ·N 1o)) = (1o +N 1o) |
17 | 16, 4 | opeq12i 4775 | . . . . 5 ⊢ 〈((1o ·N 1o) +N (1o ·N 1o)), (1o ·N 1o)〉 = 〈(1o +N 1o), 1o〉 |
18 | 13, 15, 17 | 3eqtri 2763 | . . . 4 ⊢ (1Q +pQ 1Q) = 〈(1o +N 1o), 1o〉 |
19 | 11, 12, 18 | 3brtr4i 5069 | . . 3 ⊢ 1Q <pQ (1Q +pQ 1Q) |
20 | lterpq 10549 | . . 3 ⊢ (1Q <pQ (1Q +pQ 1Q) ↔ ([Q]‘1Q) <Q ([Q]‘(1Q +pQ 1Q))) | |
21 | 19, 20 | mpbi 233 | . 2 ⊢ ([Q]‘1Q) <Q ([Q]‘(1Q +pQ 1Q)) |
22 | 1nq 10507 | . . . 4 ⊢ 1Q ∈ Q | |
23 | nqerid 10512 | . . . 4 ⊢ (1Q ∈ Q → ([Q]‘1Q) = 1Q) | |
24 | 22, 23 | ax-mp 5 | . . 3 ⊢ ([Q]‘1Q) = 1Q |
25 | 24 | eqcomi 2745 | . 2 ⊢ 1Q = ([Q]‘1Q) |
26 | addpqnq 10517 | . . 3 ⊢ ((1Q ∈ Q ∧ 1Q ∈ Q) → (1Q +Q 1Q) = ([Q]‘(1Q +pQ 1Q))) | |
27 | 22, 22, 26 | mp2an 692 | . 2 ⊢ (1Q +Q 1Q) = ([Q]‘(1Q +pQ 1Q)) |
28 | 21, 25, 27 | 3brtr4i 5069 | 1 ⊢ 1Q <Q (1Q +Q 1Q) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1543 ∈ wcel 2112 〈cop 4533 class class class wbr 5039 ‘cfv 6358 (class class class)co 7191 1oc1o 8173 Ncnpi 10423 +N cpli 10424 ·N cmi 10425 <N clti 10426 +pQ cplpq 10427 <pQ cltpq 10429 Qcnq 10431 1Qc1q 10432 [Q]cerq 10433 +Q cplq 10434 <Q cltq 10437 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2708 ax-sep 5177 ax-nul 5184 ax-pr 5307 ax-un 7501 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2728 df-clel 2809 df-nfc 2879 df-ne 2933 df-ral 3056 df-rex 3057 df-reu 3058 df-rmo 3059 df-rab 3060 df-v 3400 df-sbc 3684 df-csb 3799 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-pss 3872 df-nul 4224 df-if 4426 df-pw 4501 df-sn 4528 df-pr 4530 df-tp 4532 df-op 4534 df-uni 4806 df-iun 4892 df-br 5040 df-opab 5102 df-mpt 5121 df-tr 5147 df-id 5440 df-eprel 5445 df-po 5453 df-so 5454 df-fr 5494 df-we 5496 df-xp 5542 df-rel 5543 df-cnv 5544 df-co 5545 df-dm 5546 df-rn 5547 df-res 5548 df-ima 5549 df-pred 6140 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6316 df-fun 6360 df-fn 6361 df-f 6362 df-f1 6363 df-fo 6364 df-f1o 6365 df-fv 6366 df-ov 7194 df-oprab 7195 df-mpo 7196 df-om 7623 df-1st 7739 df-2nd 7740 df-wrecs 8025 df-recs 8086 df-rdg 8124 df-1o 8180 df-oadd 8184 df-omul 8185 df-er 8369 df-ni 10451 df-pli 10452 df-mi 10453 df-lti 10454 df-plpq 10487 df-ltpq 10489 df-enq 10490 df-nq 10491 df-erq 10492 df-plq 10493 df-1nq 10495 df-ltnq 10497 |
This theorem is referenced by: ltaddnq 10553 |
Copyright terms: Public domain | W3C validator |