Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem zltp1let 6128

Description: Integer ordering relation.

Assertion

Ref	Expression
zltp1let

---

Proof of Theorem zltp1let

Step	Hyp	Ref	Expression
1		nn0ltp1let 6074	. . . . . 6
2	1	a1i 8	. . . . 5
3		recnt 5285	. . . . . . . . . . 11
4		0cn 5300	. . . . . . . . . . . . 13
5		negcon1t 5382	. . . . . . . . . . . . 13
6	4, 5	mpan2 694	. . . . . . . . . . . 12
7		neg0 5387	. . . . . . . . . . . . . 14
8	7	eqeq1i 1474	. . . . . . . . . . . . 13
9		eqcom 1469	. . . . . . . . . . . . 13
10	8, 9	bitr 173	. . . . . . . . . . . 12
11	6, 10	syl6bb 534	. . . . . . . . . . 11
12	3, 11	syl 10	. . . . . . . . . 10
13	12	orbi2d 612	. . . . . . . . 9
14		elnn0 6048	. . . . . . . . 9
15	13, 14	syl5bb 530	. . . . . . . 8
16		elnn0 6048	. . . . . . . . 9
17	16	a1i 8	. . . . . . . 8
18	15, 17	anbi12d 626	. . . . . . 7
19	18	adantr 389	. . . . . 6
20		lt0neg1t 5641	. . . . . . . . . . . . . . . 16
21		nngt0t 5894	. . . . . . . . . . . . . . . 16
22	20, 21	syl5bir 210	. . . . . . . . . . . . . . 15
23	22	imp 350	. . . . . . . . . . . . . 14
24		nngt0t 5894	. . . . . . . . . . . . . 14
25	23, 24	anim12i 333	. . . . . . . . . . . . 13
26		0re 5412	. . . . . . . . . . . . . . . 16
27		axlttrn 5476	. . . . . . . . . . . . . . . 16
28	26, 27	mp3an2 901	. . . . . . . . . . . . . . 15
29		nnret 5877	. . . . . . . . . . . . . . 15
30	28, 29	sylan2 451	. . . . . . . . . . . . . 14
31	30	adantlr 393	. . . . . . . . . . . . 13
32	25, 31	mpd 26	. . . . . . . . . . . 12
33		peano2re 5408	. . . . . . . . . . . . . 14
34	33	ad2antrr 404	. . . . . . . . . . . . 13
35		1re 5407	. . . . . . . . . . . . . 14
36	35	a1i 8	. . . . . . . . . . . . 13
37	29	adantl 388	. . . . . . . . . . . . 13
38		ltlet 5493	. . . . . . . . . . . . . . . . . . 19
39	26, 38	mpan2 694	. . . . . . . . . . . . . . . . . 18
40	39	adantr 389	. . . . . . . . . . . . . . . . 17
41	23, 40	mpd 26	. . . . . . . . . . . . . . . 16
42		leadd1t 5599	. . . . . . . . . . . . . . . . . 18
43	26, 35, 42	mp3an23 905	. . . . . . . . . . . . . . . . 17
44	43	adantr 389	. . . . . . . . . . . . . . . 16
45	41, 44	mpbid 195	. . . . . . . . . . . . . . 15
46		ax1cn 5241	. . . . . . . . . . . . . . . 16
47	46	addid2 5303	. . . . . . . . . . . . . . 15
48	45, 47	syl6breq 2644	. . . . . . . . . . . . . 14
49	48	adantr 389	. . . . . . . . . . . . 13
50		nnge1t 5891	. . . . . . . . . . . . . 14
51	50	adantl 388	. . . . . . . . . . . . 13
52	34, 36, 37, 49, 51	letrd 5499	. . . . . . . . . . . 12
53	32, 52	jca 288	. . . . . . . . . . 11
54	53	exp31 376	. . . . . . . . . 10
55	54	imp3a 361	. . . . . . . . 9
56		pm5.1 674	. . . . . . . . 9
57	55, 56	syl6 22	. . . . . . . 8
58	57	adantr 389	. . . . . . 7
59		breq1 2612	. . . . . . . . . . 11
60		opreq1 3953	. . . . . . . . . . . . 13
61	60, 47	syl6eq 1515	. . . . . . . . . . . 12
62	61	breq1d 2619	. . . . . . . . . . 11
63	59, 62	bibi12d 627	. . . . . . . . . 10
64		pm5.1 674	. . . . . . . . . . 11
65	64, 24, 50	sylanc 471	. . . . . . . . . 10
66	63, 65	syl5bir 210	. . . . . . . . 9
67	66	imp 350	. . . . . . . 8
68	67	a1i 8	. . . . . . 7
69		breq2 2613	. . . . . . . . . . . 12
70		breq2 2613	. . . . . . . . . . . 12
71	69, 70	bibi12d 627	. . . . . . . . . . 11
72		nnnn0t 6053	. . . . . . . . . . . . . 14
73		0nn0 6060	. . . . . . . . . . . . . . 15
74		nn0ltlem1t 6076	. . . . . . . . . . . . . . 15
75	73, 74	mpan 693	. . . . . . . . . . . . . 14
76	72, 75	syl 10	. . . . . . . . . . . . 13
77	76	adantl 388	. . . . . . . . . . . 12
78	20	adantr 389	. . . . . . . . . . . 12
79		le0neg1t 5643	. . . . . . . . . . . . . . 15
80	33, 79	syl 10	. . . . . . . . . . . . . 14
81		negdi2t 5428	. . . . . . . . . . . . . . . . 17
82	46, 81	mpan2 694	. . . . . . . . . . . . . . . 16
83	3, 82	syl 10	. . . . . . . . . . . . . . 15
84	83	breq2d 2620	. . . . . . . . . . . . . 14