addltmul - Intuitionistic Logic Explorer

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

Theorem addltmul 9287

Description: Sum is less than product for numbers greater than 2. (Contributed by Stefan Allan, 24-Sep-2010.)

**Assertion**
Ref	Expression
addltmul	$/\$ $/\$ $/\$

**Proof of Theorem addltmul**
Step	Hyp	Ref	Expression
1		2re 9119	. . . . . . 7
2		1re 8084	. . . . . . 7
3		ltsub1 8544	. . . . . . 7 $/\$ $/\$
4	1, 2, 3	mp3an13 1341	. . . . . 6
5		2m1e1 9167	. . . . . . 7
6	5	breq1i 4055	. . . . . 6
7	4, 6	bitrdi 196	. . . . 5
8		ltsub1 8544	. . . . . . 7 $/\$ $/\$
9	1, 2, 8	mp3an13 1341	. . . . . 6
10	5	breq1i 4055	. . . . . 6
11	9, 10	bitrdi 196	. . . . 5
12	7, 11	bi2anan9 606	. . . 4 $/\$ $/\$ $/\$
13		peano2rem 8352	. . . . 5
14		peano2rem 8352	. . . . 5
15		mulgt1 8949	. . . . . 6 $/\$ $/\$ $/\$
16	15	ex 115	. . . . 5 $/\$ $/\$
17	13, 14, 16	syl2an 289	. . . 4 $/\$ $/\$
18	12, 17	sylbid 150	. . 3 $/\$ $/\$
19		recn 8071	. . . . . 6
20		recn 8071	. . . . . 6
21		ax-1cn 8031	. . . . . . 7
22		mulsub 8486	. . . . . . . 8 $/\$ $/\$ $/\$
23	21, 22	mpanl2 435	. . . . . . 7 $/\$ $/\$
24	21, 23	mpanr2 438	. . . . . 6 $/\$
25	19, 20, 24	syl2an 289	. . . . 5 $/\$
26	25	breq2d 4060	. . . 4 $/\$
27		remulcl 8066	. . . . . . . 8 $/\$
28	2, 27	mpan2 425	. . . . . . 7
29		remulcl 8066	. . . . . . . 8 $/\$
30	2, 29	mpan2 425	. . . . . . 7
31		readdcl 8064	. . . . . . 7 $/\$
32	28, 30, 31	syl2an 289	. . . . . 6 $/\$
33		remulcl 8066	. . . . . . 7 $/\$
34	2, 2	remulcli 8099	. . . . . . 7
35		readdcl 8064	. . . . . . 7 $/\$
36	33, 34, 35	sylancl 413	. . . . . 6 $/\$
37		ltaddsub2 8523	. . . . . . 7 $/\$ $/\$
38	2, 37	mp3an2 1338	. . . . . 6 $/\$
39	32, 36, 38	syl2anc 411	. . . . 5 $/\$
40		1t1e1 9202	. . . . . . 7
41	40	oveq2i 5965	. . . . . 6
42	41	breq2i 4056	. . . . 5
43	39, 42	bitr3di 195	. . . 4 $/\$
44		ltadd1 8515	. . . . . . 7 $/\$ $/\$
45	2, 44	mp3an3 1339	. . . . . 6 $/\$
46	32, 33, 45	syl2anc 411	. . . . 5 $/\$
47		ax-1rid 8045	. . . . . . 7
48		ax-1rid 8045	. . . . . . 7
49	47, 48	oveqan12d 5973	. . . . . 6 $/\$
50	49	breq1d 4058	. . . . 5 $/\$
51	46, 50	bitr3d 190	. . . 4 $/\$
52	26, 43, 51	3bitrd 214	. . 3 $/\$
53	18, 52	sylibd 149	. 2 $/\$ $/\$
54	53	imp 124	1 $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105

wceq 1373

wcel 2177 class class class wbr 4048 (class class class)co 5954

cc 7936

cr 7937

c1 7939

caddc 7941

cmul 7943

clt 8120

cmin 8256

c2 9100

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 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-sep 4167 ax-pow 4223 ax-pr 4258 ax-un 4485 ax-setind 4590 ax-cnex 8029 ax-resscn 8030 ax-1cn 8031 ax-1re 8032 ax-icn 8033 ax-addcl 8034 ax-addrcl 8035 ax-mulcl 8036 ax-mulrcl 8037 ax-addcom 8038 ax-mulcom 8039 ax-addass 8040 ax-mulass 8041 ax-distr 8042 ax-i2m1 8043 ax-0lt1 8044 ax-1rid 8045 ax-0id 8046 ax-rnegex 8047 ax-precex 8048 ax-cnre 8049 ax-pre-lttrn 8052 ax-pre-ltadd 8054 ax-pre-mulgt0 8055

This theorem depends on definitions: df-bi 117 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ne 2378 df-nel 2473 df-ral 2490 df-rex 2491 df-reu 2492 df-rab 2494 df-v 2775 df-sbc 3001 df-dif 3170 df-un 3172 df-in 3174 df-ss 3181 df-pw 3620 df-sn 3641 df-pr 3642 df-op 3644 df-uni 3854 df-br 4049 df-opab 4111 df-id 4345 df-xp 4686 df-rel 4687 df-cnv 4688 df-co 4689 df-dm 4690 df-iota 5238 df-fun 5279 df-fv 5285 df-riota 5909 df-ov 5957 df-oprab 5958 df-mpo 5959 df-pnf 8122 df-mnf 8123 df-ltxr 8125 df-sub 8258 df-neg 8259 df-2 9108

This theorem is referenced by: (None)

W3C validator