Theorem zltp1let 4597

Description: Integer ordering relation.

Assertion

Ref	Expression
zltp1let	|- ((A e. ZZ /\ B e. ZZ) -> (A < B <-> (A + 1) <_ B))

Proof of Theorem zltp1let

Step	Hyp	Ref	Expression
1		nn0ltp1let 4556	. . . . . 6 |- ((A e. NN0 /\ B e. NN0) -> (A < B <-> (A + 1) <_ B))
2	1	a1i 7	. . . . 5 |- ((A e. RR /\ B e. RR) -> ((A e. NN0 /\ B e. NN0) -> (A < B <-> (A + 1) <_ B)))
3		recnt 4097	. . . . . . . . . . 11 |- (A e. RR -> A e. CC)
4		0cn 4100	. . . . . . . . . . . . 13 |- 0 e. CC
5		negcon1t 4167	. . . . . . . . . . . . 13 |- ((A e. CC /\ 0 e. CC) -> (-uA = 0 <-> -u0 = A))
6	4, 5	mpan2 519	. . . . . . . . . . . 12 |- (A e. CC -> (-uA = 0 <-> -u0 = A))
7		neg0 4170	. . . . . . . . . . . . . 14 |- -u0 = 0
8	7	cleq1i 1108	. . . . . . . . . . . . 13 |- (-u0 = A <-> 0 = A)
9		cleqcom 1103	. . . . . . . . . . . . 13 |- (0 = A <-> A = 0)
10	8, 9	bitr 151	. . . . . . . . . . . 12 |- (-u0 = A <-> A = 0)
11	6, 10	syl6bb 414	. . . . . . . . . . 11 |- (A e. CC -> (-uA = 0 <-> A = 0))
12	3, 11	syl 12	. . . . . . . . . 10 |- (A e. RR -> (-uA = 0 <-> A = 0))
13	12	orbi2d 466	. . . . . . . . 9 |- (A e. RR -> ((-uA e. NN \/ -uA = 0) <-> (-uA e. NN \/ A = 0)))
14		elnn0 4536	. . . . . . . . 9 |- (-uA e. NN0 <-> (-uA e. NN \/ -uA = 0))
15	13, 14	syl5bb 410	. . . . . . . 8 |- (A e. RR -> (-uA e. NN0 <-> (-uA e. NN \/ A = 0)))
16		elnn0 4536	. . . . . . . . 9 |- (B e. NN0 <-> (B e. NN \/ B = 0))
17	16	a1i 7	. . . . . . . 8 |- (A e. RR -> (B e. NN0 <-> (B e. NN \/ B = 0)))
18	15, 17	anbi12d 476	. . . . . . 7 |- (A e. RR -> ((-uA e. NN0 /\ B e. NN0) <-> ((-uA e. NN \/ A = 0) /\ (B e. NN \/ B = 0))))
19	18	adantr 306	. . . . . 6 |- ((A e. RR /\ B e. RR) -> ((-uA e. NN0 /\ B e. NN0) <-> ((-uA e. NN \/ A = 0) /\ (B e. NN \/ B = 0))))
20		lt0neg1t 4370	. . . . . . . . . . . . . . . 16 |- (A e. RR -> (A < 0 <-> 0 < -uA))
21		nngt0t 4441	. . . . . . . . . . . . . . . 16 |- (-uA e. NN -> 0 < -uA)
22	20, 21	syl5bir 184	. . . . . . . . . . . . . . 15 |- (A e. RR -> (-uA e. NN -> A < 0))
23	22	imp 277	. . . . . . . . . . . . . 14 |- ((A e. RR /\ -uA e. NN) -> A < 0)
24		nngt0t 4441	. . . . . . . . . . . . . 14 |- (B e. NN -> 0 < B)
25	23, 24	anim12i 268	. . . . . . . . . . . . 13 |- (((A e. RR /\ -uA e. NN) /\ B e. NN) -> (A < 0 /\ 0 < B))
26		ax0re 4063	. . . . . . . . . . . . . . . 16 |- 0 e. RR
27		axlttrn 4084	. . . . . . . . . . . . . . . 16 |- ((A e. RR /\ 0 e. RR /\ B e. RR) -> ((A < 0 /\ 0 < B) -> A < B))
28	26, 27	mp3an2 640	. . . . . . . . . . . . . . 15 |- ((A e. RR /\ B e. RR) -> ((A < 0 /\ 0 < B) -> A < B))
29		nnret 4427	. . . . . . . . . . . . . . 15 |- (B e. NN -> B e. RR)
30	28, 29	sylan2 346	. . . . . . . . . . . . . 14 |- ((A e. RR /\ B e. NN) -> ((A < 0 /\ 0 < B) -> A < B))
31	30	adantlr 310	. . . . . . . . . . . . 13 |- (((A e. RR /\ -uA e. NN) /\ B e. NN) -> ((A < 0 /\ 0 < B) -> A < B))
32	25, 31	mpd 46	. . . . . . . . . . . 12 |- (((A e. RR /\ -uA e. NN) /\ B e. NN) -> A < B)
33	21	adantl 305	. . . . . . . . . . . . . . . . . 18 |- ((A e. RR /\ -uA e. NN) -> 0 < -uA)
34	20	adantr 306	. . . . . . . . . . . . . . . . . 18 |- ((A e. RR /\ -uA e. NN) -> (A < 0 <-> 0 < -uA))
35	33, 34	mpbird 171	. . . . . . . . . . . . . . . . 17 |- ((A e. RR /\ -uA e. NN) -> A < 0)
36		ltlet 4286	. . . . . . . . . . . . . . . . . . 19 |- ((A e. RR /\ 0 e. RR) -> (A < 0 -> A <_ 0))
37	26, 36	mpan2 519	. . . . . . . . . . . . . . . . . 18 |- (A e. RR -> (A < 0 -> A <_ 0))
38	37	adantr 306	. . . . . . . . . . . . . . . . 17 |- ((A e. RR /\ -uA e. NN) -> (A < 0 -> A <_ 0))
39	35, 38	mpd 46	. . . . . . . . . . . . . . . 16 |- ((A e. RR /\ -uA e. NN) -> A <_ 0)
40		ax1re 4064	. . . . . . . . . . . . . . . . . 18 |- 1 e. RR
41		leadd1t 4350	. . . . . . . . . . . . . . . . . . 19 |- ((A e. RR /\ 0 e. RR /\ 1 e. RR) -> (A <_ 0 <-> (A + 1) <_ (0 + 1)))
42	26, 41	mp3an2 640	. . . . . . . . . . . . . . . . . 18 |- ((A e. RR /\ 1 e. RR) -> (A <_ 0 <-> (A + 1) <_ (0 + 1)))
43	40, 42	mpan2 519	. . . . . . . . . . . . . . . . 17 |- (A e. RR -> (A <_ 0 <-> (A + 1) <_ (0 + 1)))
44	43	adantr 306	. . . . . . . . . . . . . . . 16 |- ((A e. RR /\ -uA e. NN) -> (A <_ 0 <-> (A + 1) <_ (0 + 1)))
45	39, 44	mpbid 170	. . . . . . . . . . . . . . 15 |- ((A e. RR /\ -uA e. NN) -> (A + 1) <_ (0 + 1))
46		1cn 4101	. . . . . . . . . . . . . . . 16 |- 1 e. CC
47	46	addid2 4113	. . . . . . . . . . . . . . 15 |- (0 + 1) = 1
48	45, 47	syl6breq 2093	. . . . . . . . . . . . . 14 |- ((A e. RR /\ -uA e. NN) -> (A + 1) <_ 1)
49		nnge1t 4439	. . . . . . . . . . . . . 14 |- (B e. NN -> 1 <_ B)
50	48, 49	anim12i 268	. . . . . . . . . . . . 13 |- (((A e. RR /\ -uA e. NN) /\ B e. NN) -> ((A + 1) <_ 1 /\ 1 <_ B))
51		letrt 4291	. . . . . . . . . . . . . . . 16 |- (((A + 1) e. RR /\ 1 e. RR /\ B e. RR) -> (((A + 1) <_ 1 /\ 1 <_ B) -> (A + 1) <_ B))
52	40, 51	mp3an2 640	. . . . . . . . . . . . . . 15 |- (((A + 1) e. RR /\ B e. RR) -> (((A + 1) <_ 1 /\ 1 <_ B) -> (A + 1) <_ B))
53		axaddrcl 4067	. . . . . . . . . . . . . . . 16 |- ((A e. RR /\ 1 e. RR) -> (A + 1) e. RR)
54	40, 53	mpan2 519	. . . . . . . . . . . . . . 15 |- (A e. RR -> (A + 1) e. RR)
55	52, 54, 29	syl2an 349	. . . . . . . . . . . . . 14 |- ((A e. RR /\ B e. NN) -> (((A + 1) <_ 1 /\ 1 <_ B) -> (A + 1) <_ B))
56	55	adantlr 310	. . . . . . . . . . . . 13 |- (((A e. RR /\ -uA e. NN) /\ B e. NN) -> (((A + 1) <_ 1 /\ 1 <_ B) -> (A + 1) <_ B))
57	50, 56	mpd 46	. . . . . . . . . . . 12 |- (((A e. RR /\ -uA e. NN) /\ B e. NN) -> (A + 1) <_ B)
58	32, 57	jca 236	. . . . . . . . . . 11 |- (((A e. RR /\ -uA e. NN) /\ B e. NN) -> (A < B /\ (A + 1) <_ B))
59	58	exp31 293	. . . . . . . . . 10 |- (A e. RR -> (-uA e. NN -> (B e. NN -> (A < B /\ (A + 1) <_ B))))
60	59	imp3a 279	. . . . . . . . 9 |- (A e. RR -> ((-uA e. NN /\ B e. NN) -> (A < B /\ (A + 1) <_ B)))
61		pm5.1 501	. . . . . . . . 9 |- ((A < B /\ (A + 1) <_ B) -> (A < B <-> (A + 1) <_ B))
62	60, 61	syl6 23	. . . . . . . 8 |- (A e. RR -> ((-uA e. NN /\ B e. NN) -> (A < B <-> (A + 1) <_ B)))
63	62	adantr 306	. . . . . . 7 |- ((A e. RR /\ B e. RR) -> ((-uA e. NN /\ B e. NN) -> (A < B <-> (A + 1) <_ B)))
64		breq1 2065	. . . . . . . . . . 11 |- (A = 0 -> (A < B <-> 0 < B))
65		opreq1 3006	. . . . . . . . . . . . 13 |- (A = 0 -> (A + 1) = (0 + 1))
66	65, 47	syl6eq 1140	. . . . . . . . . . . 12 |- (A = 0 -> (A + 1) = 1)
67	66	breq1d 2071	. . . . . . . . . . 11 |- (A = 0 -> ((A + 1) <_ B <-> 1 <_ B))
68	64, 67	bibi12d 477	. . . . . . . . . 10 |- (A = 0 -> ((A < B <-> (A + 1) <_ B) <-> (0 < B <-> 1 <_ B)))
69		pm5.1 501	. . . . . . . . . . 11 |- ((0 < B /\ 1 <_ B) -> (0 < B <-> 1 <_ B))
70	69, 24, 49	sylanc 361	. . . . . . . . . 10 |- (B e. NN -> (0 < B <-> 1 <_ B))
71	68, 70	syl5bir 184	. . . . . . . . 9 |- (A = 0 -> (B e. NN -> (A < B <-> (A + 1) <_ B)))
72	71	imp 277	. . . . . . . 8 |- ((A = 0 /\ B e. NN) -> (A < B <-> (A + 1) <_ B))
73	72	a1i 7	. . . . . . 7 |- ((A e. RR /\ B e. RR) -> ((A = 0 /\ B e. NN) -> (A < B <-> (A + 1) <_ B)))
74		breq2 2066	. . . . . . . . . . . . 13 |- (B = 0 -> (A < B <-> A < 0))
75		breq2 2066	. . . . . . . . . . . . 13 |- (B = 0 -> ((A + 1) <_ B <-> (A + 1) <_ 0))
76	74, 75	bibi12d 477	. . . . . . . . . . . 12 |- (B = 0 -> ((A < B <-> (A + 1) <_ B) <-> (A < 0 <-> (A + 1) <_ 0)))
77		nnnn0t 4541	. . . . . . . . . . . . . . 15 |- (-uA e. NN -> -uA e. NN0)
78		0nn0 4546	. . . . . . . . . . . . . . . 16 |- 0 e. NN0
79		nn0ltlem1 4558	. . . . . . . . . . . . . . . 16 |- ((0 e. NN0 /\ -uA e. NN0) -> (0 < -uA <-> 0 <_ (-uA - 1)))
80	78, 79	mpan 518	. . . . . . . . . . . . . . 15 |- (-uA e. NN0 -> (0 < -uA <-> 0 <_ (-uA - 1)))
81	77, 80	syl 12	. . . . . . . . . . . . . 14 |- (-uA e. NN -> (0 < -uA <-> 0 <_ (-uA - 1)))
82	81	adantl 305	. . . . . . . . . . . . 13 |- ((A e. RR /\ -uA e. NN) -> (0 < -uA <-> 0 <_ (-uA - 1)))
83		le0neg1t 4372	. . . . . . . . . . . . . . . 16 |- ((A + 1) e. RR -> ((A + 1) <_ 0 <-> 0 <_ -u(A + 1)))
84	54, 83	syl 12	. . . . . . . . . . . . . . 15 |- (A e. RR -> ((A + 1) <_ 0 <-> 0 <_ -u(A + 1)))
85		negdit 4200	. . . . . . . . . . . . . . . . . . 19 |- ((A e. CC /\ 1 e. CC) -> -u(A