![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ltaddnq | GIF version |
Description: The sum of two fractions is greater than one of them. (Contributed by NM, 14-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) |
Ref | Expression |
---|---|
ltaddnq | ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → 𝐴 <Q (𝐴 +Q 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1lt2nq 6658 | . . . . . . 7 ⊢ 1Q <Q (1Q +Q 1Q) | |
2 | 1nq 6618 | . . . . . . . 8 ⊢ 1Q ∈ Q | |
3 | addclnq 6627 | . . . . . . . . 9 ⊢ ((1Q ∈ Q ∧ 1Q ∈ Q) → (1Q +Q 1Q) ∈ Q) | |
4 | 2, 2, 3 | mp2an 417 | . . . . . . . 8 ⊢ (1Q +Q 1Q) ∈ Q |
5 | ltmnqg 6653 | . . . . . . . 8 ⊢ ((1Q ∈ Q ∧ (1Q +Q 1Q) ∈ Q ∧ 𝐵 ∈ Q) → (1Q <Q (1Q +Q 1Q) ↔ (𝐵 ·Q 1Q) <Q (𝐵 ·Q (1Q +Q 1Q)))) | |
6 | 2, 4, 5 | mp3an12 1259 | . . . . . . 7 ⊢ (𝐵 ∈ Q → (1Q <Q (1Q +Q 1Q) ↔ (𝐵 ·Q 1Q) <Q (𝐵 ·Q (1Q +Q 1Q)))) |
7 | 1, 6 | mpbii 146 | . . . . . 6 ⊢ (𝐵 ∈ Q → (𝐵 ·Q 1Q) <Q (𝐵 ·Q (1Q +Q 1Q))) |
8 | mulidnq 6641 | . . . . . 6 ⊢ (𝐵 ∈ Q → (𝐵 ·Q 1Q) = 𝐵) | |
9 | distrnqg 6639 | . . . . . . . 8 ⊢ ((𝐵 ∈ Q ∧ 1Q ∈ Q ∧ 1Q ∈ Q) → (𝐵 ·Q (1Q +Q 1Q)) = ((𝐵 ·Q 1Q) +Q (𝐵 ·Q 1Q))) | |
10 | 2, 2, 9 | mp3an23 1261 | . . . . . . 7 ⊢ (𝐵 ∈ Q → (𝐵 ·Q (1Q +Q 1Q)) = ((𝐵 ·Q 1Q) +Q (𝐵 ·Q 1Q))) |
11 | 8, 8 | oveq12d 5561 | . . . . . . 7 ⊢ (𝐵 ∈ Q → ((𝐵 ·Q 1Q) +Q (𝐵 ·Q 1Q)) = (𝐵 +Q 𝐵)) |
12 | 10, 11 | eqtrd 2114 | . . . . . 6 ⊢ (𝐵 ∈ Q → (𝐵 ·Q (1Q +Q 1Q)) = (𝐵 +Q 𝐵)) |
13 | 7, 8, 12 | 3brtr3d 3822 | . . . . 5 ⊢ (𝐵 ∈ Q → 𝐵 <Q (𝐵 +Q 𝐵)) |
14 | 13 | adantl 271 | . . . 4 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → 𝐵 <Q (𝐵 +Q 𝐵)) |
15 | simpr 108 | . . . . 5 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → 𝐵 ∈ Q) | |
16 | addclnq 6627 | . . . . . . 7 ⊢ ((𝐵 ∈ Q ∧ 𝐵 ∈ Q) → (𝐵 +Q 𝐵) ∈ Q) | |
17 | 16 | anidms 389 | . . . . . 6 ⊢ (𝐵 ∈ Q → (𝐵 +Q 𝐵) ∈ Q) |
18 | 17 | adantl 271 | . . . . 5 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐵 +Q 𝐵) ∈ Q) |
19 | simpl 107 | . . . . 5 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → 𝐴 ∈ Q) | |
20 | ltanqg 6652 | . . . . 5 ⊢ ((𝐵 ∈ Q ∧ (𝐵 +Q 𝐵) ∈ Q ∧ 𝐴 ∈ Q) → (𝐵 <Q (𝐵 +Q 𝐵) ↔ (𝐴 +Q 𝐵) <Q (𝐴 +Q (𝐵 +Q 𝐵)))) | |
21 | 15, 18, 19, 20 | syl3anc 1170 | . . . 4 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐵 <Q (𝐵 +Q 𝐵) ↔ (𝐴 +Q 𝐵) <Q (𝐴 +Q (𝐵 +Q 𝐵)))) |
22 | 14, 21 | mpbid 145 | . . 3 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 +Q 𝐵) <Q (𝐴 +Q (𝐵 +Q 𝐵))) |
23 | addcomnqg 6633 | . . 3 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 +Q 𝐵) = (𝐵 +Q 𝐴)) | |
24 | addcomnqg 6633 | . . . . 5 ⊢ ((𝑟 ∈ Q ∧ 𝑠 ∈ Q) → (𝑟 +Q 𝑠) = (𝑠 +Q 𝑟)) | |
25 | 24 | adantl 271 | . . . 4 ⊢ (((𝐴 ∈ Q ∧ 𝐵 ∈ Q) ∧ (𝑟 ∈ Q ∧ 𝑠 ∈ Q)) → (𝑟 +Q 𝑠) = (𝑠 +Q 𝑟)) |
26 | addassnqg 6634 | . . . . 5 ⊢ ((𝑟 ∈ Q ∧ 𝑠 ∈ Q ∧ 𝑡 ∈ Q) → ((𝑟 +Q 𝑠) +Q 𝑡) = (𝑟 +Q (𝑠 +Q 𝑡))) | |
27 | 26 | adantl 271 | . . . 4 ⊢ (((𝐴 ∈ Q ∧ 𝐵 ∈ Q) ∧ (𝑟 ∈ Q ∧ 𝑠 ∈ Q ∧ 𝑡 ∈ Q)) → ((𝑟 +Q 𝑠) +Q 𝑡) = (𝑟 +Q (𝑠 +Q 𝑡))) |
28 | 19, 15, 15, 25, 27 | caov12d 5713 | . . 3 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 +Q (𝐵 +Q 𝐵)) = (𝐵 +Q (𝐴 +Q 𝐵))) |
29 | 22, 23, 28 | 3brtr3d 3822 | . 2 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐵 +Q 𝐴) <Q (𝐵 +Q (𝐴 +Q 𝐵))) |
30 | addclnq 6627 | . . 3 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 +Q 𝐵) ∈ Q) | |
31 | ltanqg 6652 | . . 3 ⊢ ((𝐴 ∈ Q ∧ (𝐴 +Q 𝐵) ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 <Q (𝐴 +Q 𝐵) ↔ (𝐵 +Q 𝐴) <Q (𝐵 +Q (𝐴 +Q 𝐵)))) | |
32 | 19, 30, 15, 31 | syl3anc 1170 | . 2 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 <Q (𝐴 +Q 𝐵) ↔ (𝐵 +Q 𝐴) <Q (𝐵 +Q (𝐴 +Q 𝐵)))) |
33 | 29, 32 | mpbird 165 | 1 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → 𝐴 <Q (𝐴 +Q 𝐵)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ↔ wb 103 ∧ w3a 920 = wceq 1285 ∈ wcel 1434 class class class wbr 3793 (class class class)co 5543 Qcnq 6532 1Qc1q 6533 +Q cplq 6534 ·Q cmq 6535 <Q cltq 6537 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-13 1445 ax-14 1446 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2064 ax-coll 3901 ax-sep 3904 ax-nul 3912 ax-pow 3956 ax-pr 3972 ax-un 4196 ax-setind 4288 ax-iinf 4337 |
This theorem depends on definitions: df-bi 115 df-dc 777 df-3or 921 df-3an 922 df-tru 1288 df-fal 1291 df-nf 1391 df-sb 1687 df-eu 1945 df-mo 1946 df-clab 2069 df-cleq 2075 df-clel 2078 df-nfc 2209 df-ne 2247 df-ral 2354 df-rex 2355 df-reu 2356 df-rab 2358 df-v 2604 df-sbc 2817 df-csb 2910 df-dif 2976 df-un 2978 df-in 2980 df-ss 2987 df-nul 3259 df-pw 3392 df-sn 3412 df-pr 3413 df-op 3415 df-uni 3610 df-int 3645 df-iun 3688 df-br 3794 df-opab 3848 df-mpt 3849 df-tr 3884 df-eprel 4052 df-id 4056 df-iord 4129 df-on 4131 df-suc 4134 df-iom 4340 df-xp 4377 df-rel 4378 df-cnv 4379 df-co 4380 df-dm 4381 df-rn 4382 df-res 4383 df-ima 4384 df-iota 4897 df-fun 4934 df-fn 4935 df-f 4936 df-f1 4937 df-fo 4938 df-f1o 4939 df-fv 4940 df-ov 5546 df-oprab 5547 df-mpt2 5548 df-1st 5798 df-2nd 5799 df-recs 5954 df-irdg 6019 df-1o 6065 df-oadd 6069 df-omul 6070 df-er 6172 df-ec 6174 df-qs 6178 df-ni 6556 df-pli 6557 df-mi 6558 df-lti 6559 df-plpq 6596 df-mpq 6597 df-enq 6599 df-nqqs 6600 df-plqqs 6601 df-mqqs 6602 df-1nqqs 6603 df-ltnqqs 6605 |
This theorem is referenced by: ltexnqq 6660 nsmallnqq 6664 subhalfnqq 6666 ltbtwnnqq 6667 prarloclemarch2 6671 ltexprlemm 6852 ltexprlemopl 6853 addcanprleml 6866 addcanprlemu 6867 recexprlemm 6876 cauappcvgprlemm 6897 cauappcvgprlemopl 6898 cauappcvgprlem2 6912 caucvgprlemnkj 6918 caucvgprlemnbj 6919 caucvgprlemm 6920 caucvgprlemopl 6921 caucvgprprlemnjltk 6943 caucvgprprlemopl 6949 |
Copyright terms: Public domain | W3C validator |