Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem zltp1let 4597

Description: Integer ordering relation.

**Assertion**
Ref	Expression
zltp1let	⊢ ((A ∈ ℤ ∧ B ∈ ℤ) → (A < B ↔ (A + 1) ≤ B))

**Proof of Theorem zltp1let**
Step	Hyp	Ref	Expression
1		nn0ltp1let 4556	. . . . . 6 ⊢ ((A ∈ ℕ₀ ∧ B ∈ ℕ₀) → (A < B ↔ (A + 1) ≤ B))
2	1	a1i 7	. . . . 5 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((A ∈ ℕ₀ ∧ B ∈ ℕ₀) → (A < B ↔ (A + 1) ≤ B)))
3		recnt 4097	. . . . . . . . . . 11 ⊢ (A ∈ ℝ → A ∈ ℂ)
4		0cn 4100	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℂ
5		negcon1t 4167	. . . . . . . . . . . . 13 ⊢ ((A ∈ ℂ ∧ 0 ∈ ℂ) → (-A = 0 ↔ -0 = A))
6	4, 5	mpan2 519	. . . . . . . . . . . 12 ⊢ (A ∈ ℂ → (-A = 0 ↔ -0 = A))
7		neg0 4170	. . . . . . . . . . . . . 14 ⊢ -0 = 0
8	7	cleq1i 1108	. . . . . . . . . . . . 13 ⊢ (-0 = A ↔ 0 = A)
9		cleqcom 1103	. . . . . . . . . . . . 13 ⊢ (0 = A ↔ A = 0)
10	8, 9	bitr 151	. . . . . . . . . . . 12 ⊢ (-0 = A ↔ A = 0)
11	6, 10	syl6bb 414	. . . . . . . . . . 11 ⊢ (A ∈ ℂ → (-A = 0 ↔ A = 0))
12	3, 11	syl 12	. . . . . . . . . 10 ⊢ (A ∈ ℝ → (-A = 0 ↔ A = 0))
13	12	orbi2d 466	. . . . . . . . 9 ⊢ (A ∈ ℝ → ((-A ∈ ℕ ∨ -A = 0) ↔ (-A ∈ ℕ ∨ A = 0)))
14		elnn0 4536	. . . . . . . . 9 ⊢ (-A ∈ ℕ₀ ↔ (-A ∈ ℕ ∨ -A = 0))
15	13, 14	syl5bb 410	. . . . . . . 8 ⊢ (A ∈ ℝ → (-A ∈ ℕ₀ ↔ (-A ∈ ℕ ∨ A = 0)))
16		elnn0 4536	. . . . . . . . 9 ⊢ (B ∈ ℕ₀ ↔ (B ∈ ℕ ∨ B = 0))
17	16	a1i 7	. . . . . . . 8 ⊢ (A ∈ ℝ → (B ∈ ℕ₀ ↔ (B ∈ ℕ ∨ B = 0)))
18	15, 17	anbi12d 476	. . . . . . 7 ⊢ (A ∈ ℝ → ((-A ∈ ℕ₀ ∧ B ∈ ℕ₀) ↔ ((-A ∈ ℕ ∨ A = 0) ∧ (B ∈ ℕ ∨ B = 0))))
19	18	adantr 306	. . . . . 6 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((-A ∈ ℕ₀ ∧ B ∈ ℕ₀) ↔ ((-A ∈ ℕ ∨ A = 0) ∧ (B ∈ ℕ ∨ B = 0))))
20		lt0neg1t 4370	. . . . . . . . . . . . . . . 16 ⊢ (A ∈ ℝ → (A < 0 ↔ 0 < -A))
21		nngt0t 4441	. . . . . . . . . . . . . . . 16 ⊢ (-A ∈ ℕ → 0 < -A)
22	20, 21	syl5bir 184	. . . . . . . . . . . . . . 15 ⊢ (A ∈ ℝ → (-A ∈ ℕ → A < 0))
23	22	imp 277	. . . . . . . . . . . . . 14 ⊢ ((A ∈ ℝ ∧ -A ∈ ℕ) → A < 0)
24		nngt0t 4441	. . . . . . . . . . . . . 14 ⊢ (B ∈ ℕ → 0 < B)
25	23, 24	anim12i 268	. . . . . . . . . . . . 13 ⊢ (((A ∈ ℝ ∧ -A ∈ ℕ) ∧ B ∈ ℕ) → (A < 0 ∧ 0 < B))
26		ax0re 4063	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ
27		axlttrn 4084	. . . . . . . . . . . . . . . 16 ⊢ ((A ∈ ℝ ∧ 0 ∈ ℝ ∧ B ∈ ℝ) → ((A < 0 ∧ 0 < B) → A < B))
28	26, 27	mp3an2 640	. . . . . . . . . . . . . . 15 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((A < 0 ∧ 0 < B) → A < B))
29		nnret 4427	. . . . . . . . . . . . . . 15 ⊢ (B ∈ ℕ → B ∈ ℝ)
30	28, 29	sylan2 346	. . . . . . . . . . . . . 14 ⊢ ((A ∈ ℝ ∧ B ∈ ℕ) → ((A < 0 ∧ 0 < B) → A < B))
31	30	adantlr 310	. . . . . . . . . . . . 13 ⊢ (((A ∈ ℝ ∧ -A ∈ ℕ) ∧ B ∈ ℕ) → ((A < 0 ∧ 0 < B) → A < B))
32	25, 31	mpd 46	. . . . . . . . . . . 12 ⊢ (((A ∈ ℝ ∧ -A ∈ ℕ) ∧ B ∈ ℕ) → A < B)
33	21	adantl 305	. . . . . . . . . . . . . . . . . 18 ⊢ ((A ∈ ℝ ∧ -A ∈ ℕ) → 0 < -A)
34	20	adantr 306	. . . . . . . . . . . . . . . . . 18 ⊢ ((A ∈ ℝ ∧ -A ∈ ℕ) → (A < 0 ↔ 0 < -A))
35	33, 34	mpbird 171	. . . . . . . . . . . . . . . . 17 ⊢ ((A ∈ ℝ ∧ -A ∈ ℕ) → A < 0)
36		ltlet 4286	. . . . . . . . . . . . . . . . . . 19 ⊢ ((A ∈ ℝ ∧ 0 ∈ ℝ) → (A < 0 → A ≤ 0))
37	26, 36	mpan2 519	. . . . . . . . . . . . . . . . . 18 ⊢ (A ∈ ℝ → (A < 0 → A ≤ 0))
38	37	adantr 306	. . . . . . . . . . . . . . . . 17 ⊢ ((A ∈ ℝ ∧ -A ∈ ℕ) → (A < 0 → A ≤ 0))
39	35, 38	mpd 46	. . . . . . . . . . . . . . . 16 ⊢ ((A ∈ ℝ ∧ -A ∈ ℕ) → A ≤ 0)
40		ax1re 4064	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℝ
41		leadd1t 4350	. . . . . . . . . . . . . . . . . . 19 ⊢ ((A ∈ ℝ ∧ 0 ∈ ℝ ∧ 1 ∈ ℝ) → (A ≤ 0 ↔ (A + 1) ≤ (0 + 1)))
42	26, 41	mp3an2 640	. . . . . . . . . . . . . . . . . 18 ⊢ ((A ∈ ℝ ∧ 1 ∈ ℝ) → (A ≤ 0 ↔ (A + 1) ≤ (0 + 1)))
43	40, 42	mpan2 519	. . . . . . . . . . . . . . . . 17 ⊢ (A ∈ ℝ → (A ≤ 0 ↔ (A + 1) ≤ (0 + 1)))
44	43	adantr 306	. . . . . . . . . . . . . . . 16 ⊢ ((A ∈ ℝ ∧ -A ∈ ℕ) → (A ≤ 0 ↔ (A + 1) ≤ (0 + 1)))
45	39, 44	mpbid 170	. . . . . . . . . . . . . . 15 ⊢ ((A ∈ ℝ ∧ -A ∈ ℕ) → (A + 1) ≤ (0 + 1))
46		1cn 4101	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℂ
47	46	addid2 4113	. . . . . . . . . . . . . . 15 ⊢ (0 + 1) = 1
48	45, 47	syl6breq 2093	. . . . . . . . . . . . . 14 ⊢ ((A ∈ ℝ ∧ -A ∈ ℕ) → (A + 1) ≤ 1)
49		nnge1t 4439	. . . . . . . . . . . . . 14 ⊢ (B ∈ ℕ → 1 ≤ B)
50	48, 49	anim12i 268	. . . . . . . . . . . . 13 ⊢ (((A ∈ ℝ ∧ -A ∈ ℕ) ∧ B ∈ ℕ) → ((A + 1) ≤ 1 ∧ 1 ≤ B))
51		letrt 4291	. . . . . . . . . . . . . . . 16 ⊢ (((A + 1) ∈ ℝ ∧ 1 ∈ ℝ ∧ B ∈ ℝ) → (((A + 1) ≤ 1 ∧ 1 ≤ B) → (A + 1) ≤ B))
52	40, 51	mp3an2 640	. . . . . . . . . . . . . . 15 ⊢ (((A + 1) ∈ ℝ ∧ B ∈ ℝ) → (((A + 1) ≤ 1 ∧ 1 ≤ B) → (A + 1) ≤ B))
53		axaddrcl 4067	. . . . . . . . . . . . . . . 16 ⊢ ((A ∈ ℝ ∧ 1 ∈ ℝ) → (A + 1) ∈ ℝ)
54	40, 53	mpan2 519	. . . . . . . . . . . . . . 15 ⊢ (A ∈ ℝ → (A + 1) ∈ ℝ)
55	52, 54, 29	syl2an 349	. . . . . . . . . . . . . 14 ⊢ ((A ∈ ℝ ∧ B ∈ ℕ) → (((A + 1) ≤ 1 ∧ 1 ≤ B) → (A + 1) ≤ B))
56	55	adantlr 310	. . . . . . . . . . . . 13 ⊢ (((A ∈ ℝ ∧ -A ∈ ℕ) ∧ B ∈ ℕ) → (((A + 1) ≤ 1 ∧ 1 ≤ B) → (A + 1) ≤ B))
57	50, 56	mpd 46	. . . . . . . . . . . 12 ⊢ (((A ∈ ℝ ∧ -A ∈ ℕ) ∧ B ∈ ℕ) → (A + 1) ≤ B)
58	32, 57	jca 236	. . . . . . . . . . 11 ⊢ (((A ∈ ℝ ∧ -A ∈ ℕ) ∧ B ∈ ℕ) → (A < B ∧ (A + 1) ≤ B))
59	58	exp31 293	. . . . . . . . . 10 ⊢ (A ∈ ℝ → (-A ∈ ℕ → (B ∈ ℕ → (A < B ∧ (A + 1) ≤ B))))
60	59	imp3a 279	. . . . . . . . 9 ⊢ (A ∈ ℝ → ((-A ∈ ℕ ∧ B ∈ ℕ) → (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 ∈ ℝ → ((-A ∈ ℕ ∧ B ∈ ℕ) → (A < B ↔ (A + 1) ≤ B)))
63	62	adantr 306	. . . . . . 7 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((-A ∈ ℕ ∧ B ∈ ℕ) → (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 ∈ ℕ → (0 < B ↔ 1 ≤ B))
71	68, 70	syl5bir 184	. . . . . . . . 9 ⊢ (A = 0 → (B ∈ ℕ → (A < B ↔ (A + 1) ≤ B)))
72	71	imp 277	. . . . . . . 8 ⊢ ((A = 0 ∧ B ∈ ℕ) → (A < B ↔ (A + 1) ≤ B))
73	72	a1i 7	. . . . . . 7 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((A = 0 ∧ B ∈ ℕ) → (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 ⊢ (-A ∈ ℕ → -A ∈ ℕ₀)
78		0nn0 4546	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℕ₀
79		nn0ltlem1 4558	. . . . . . . . . . . . . . . 16 ⊢ ((0 ∈ ℕ₀ ∧ -A ∈ ℕ₀) → (0 < -A ↔ 0 ≤ (-A − 1)))
80	78, 79	mpan 518	. . . . . . . . . . . . . . 15 ⊢ (-A ∈ ℕ₀ → (0 < -A ↔ 0 ≤ (-A − 1)))
81	77, 80	syl 12	. . . . . . . . . . . . . 14 ⊢ (-A ∈ ℕ → (0 < -A ↔ 0 ≤ (-A − 1)))
82	81	adantl 305	. . . . . . . . . . . . 13 ⊢ ((A ∈ ℝ ∧ -A ∈ ℕ) → (0 < -A ↔ 0 ≤ (-A − 1)))
83		le0neg1t 4372	. . . . . . . . . . . . . . . 16 ⊢ ((A + 1) ∈ ℝ → ((A + 1) ≤ 0 ↔ 0 ≤ -(A + 1)))
84	54, 83	syl 12	. . . . . . . . . . . . . . 15 ⊢ (A ∈ ℝ → ((A + 1) ≤ 0 ↔ 0 ≤ -(A + 1)))
85		negdit 4200	. . . . . . . . . . . . . . . . . . 19 ⊢ ((A ∈ ℂ ∧ 1 ∈ ℂ) → -(A + 1) = (-A + -1))
86		subnegt 4149	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((-A ∈ ℂ ∧ 1 ∈ ℂ) → (-A − 1) = (-A + -1))
87		negclt 4141	. . . . . . . . . . . . . . . . . . . 20 ⊢ (A ∈ ℂ → -A ∈ ℂ)
88	86, 87	sylan 343	. . . . . . . . . . . . . . . . . . 19 ⊢ ((A ∈ ℂ ∧ 1 ∈ ℂ) → (-A − 1) = (-A + -1))
89	85, 88	eqtr4d 1131	. . . . . . . . . . . . . . . . . 18 ⊢ ((A ∈ ℂ ∧ 1 ∈ ℂ) → -(A + 1) = (-A − 1))
90	46, 89	mpan2 519	. . . . . . . . . . . . . . . . 17 ⊢ (A ∈ ℂ → -(A + 1) = (-A − 1))
91	3, 90	syl 12	. . . . . . . . . . . . . . . 16 ⊢ (A ∈ ℝ → -(A + 1) = (-A − 1))
92	91	breq2d 2072	. . . . . . . . . . . . . . 15 ⊢ (A ∈ ℝ → (0 ≤ -(A + 1) ↔ 0 ≤ (-A − 1)))
93	84, 92	bitrd 406	. . . . . . . . . . . . . 14 ⊢ (A ∈ ℝ → ((A + 1) ≤ 0 ↔ 0 ≤ (-A − 1)))
94	93	adantr 306	. . . . . . . . . . . . 13 ⊢ ((A ∈ ℝ ∧ -A ∈ ℕ) → ((A + 1) ≤ 0 ↔ 0 ≤ (-A − 1)))
95	82, 34, 94	3bitr4d 424	. . . . . . . . . . . 12 ⊢ ((A ∈ ℝ ∧ -A ∈ ℕ) → (A < 0 ↔ (A + 1) ≤ 0))
96	76, 95	syl5bir 184	. . . . . . . . . . 11 ⊢ (B = 0 → ((A ∈ ℝ ∧ -A ∈ ℕ) → (A < B ↔ (A + 1) ≤ B)))
97	96	com12 13	. . . . . . . . . 10 ⊢ ((A ∈ ℝ ∧ -A ∈ ℕ) → (B = 0 → (A < B ↔ (A + 1) ≤ B)))
98	97	exp 291	. . . . . . . . 9 ⊢ (A ∈ ℝ → (-A ∈ ℕ → (B = 0 → (A < B ↔ (A + 1) ≤ B))))
99	98	imp3a 279	. . . . . . . 8 ⊢ (A ∈ ℝ → ((-A ∈ ℕ ∧ B = 0) → (A < B ↔ (A + 1) ≤ B)))
100	99	adantr 306	. . . . . . 7 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((-A ∈ ℕ ∧ B = 0) → (A < B ↔ (A + 1) ≤ B)))
101	26	ltnr 4338	. . . . . . . . . 10 ⊢ ¬ 0 < 0
102		lt01 4377	. . . . . . . . . . 11 ⊢ 0 < 1
103	40, 26	lelt 4301	. . . . . . . . . . . 12 ⊢ (1 ≤ 0 ↔ ¬ 0 < 1)
104	103	bicon2i 194	. . . . . . . . . . 11 ⊢ (0 < 1 ↔ ¬ 1 ≤ 0)
105	102, 104	mpbi 164	. . . . . . . . . 10 ⊢ ¬ 1 ≤ 0
106		pm5.21 502	. . . . . . . . . 10 ⊢ ((¬ 0 < 0 ∧ ¬ 1 ≤ 0) → (0 < 0 ↔ 1 ≤ 0))
107	101, 105, 106	mp2an 520	. . . . . . . . 9 ⊢ (0 < 0 ↔ 1 ≤ 0)
108		breq2 2066	. . . . . . . . . . 11 ⊢ (B = 0 → (0 < B ↔ 0 < 0))
109		breq2 2066	. . . . . . . . . . 11 ⊢ (B = 0 → (1 ≤ B ↔ 1 ≤ 0))
110	108, 109	bibi12d 477	. . . . . . . . . 10 ⊢ (B = 0 → ((0 < B ↔ 1 ≤ B) ↔ (0 < 0 ↔ 1 ≤ 0)))
111	68, 110	sylan9bb 418	. . . . . . . . 9 ⊢ ((A = 0 ∧ B = 0) → ((A < B ↔ (A + 1) ≤ B) ↔ (0 < 0 ↔ 1 ≤ 0)))
112	107, 111	mpbiri 169	. . . . . . . 8 ⊢ ((A = 0 ∧ B = 0) → (A < B ↔ (A + 1) ≤ B))
113	112	a1i 7	. . . . . . 7 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((A = 0 ∧ B = 0) → (A < B ↔ (A + 1) ≤ B)))
114	63, 73, 100, 113	ccased 563	. . . . . 6 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (((-A ∈ ℕ ∨ A = 0) ∧ (B ∈ ℕ ∨ B = 0)) → (A < B ↔ (A + 1) ≤ B)))
115	19, 114	sylbid 178	. . . . 5 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((-A ∈ ℕ₀ ∧ B ∈ ℕ₀) → (A < B ↔ (A + 1) ≤ B)))
116		nn0ge0t 4550	. . . . . . . . . . . . . 14 ⊢ (-B ∈ ℕ₀ → 0 ≤ -B)
117	116	adantl 305	. . . . . . . . . . . . 13 ⊢ ((B ∈ ℝ ∧ -B ∈ ℕ₀) → 0 ≤ -B)
118		le0neg1t 4372	. . . . . . . . . . . . . 14 ⊢ (B ∈ ℝ → (B ≤ 0 ↔ 0 ≤ -B))
119	118	adantr 306	. . . . . . . . . . . . 13 ⊢ ((B ∈ ℝ ∧ -B ∈ ℕ₀) → (B ≤ 0 ↔ 0 ≤ -B))
120	117, 119	mpbird 171	. . . . . . . . . . . 12 ⊢ ((B ∈ ℝ ∧ -B ∈ ℕ₀) → B ≤ 0)
121	120	adantrl 311	. . . . . . . . . . 11 ⊢ ((B ∈ ℝ ∧ (A ∈ ℕ₀ ∧ -B ∈ ℕ₀)) → B ≤ 0)
122	121	adantll 309	. . . . . . . . . 10 ⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ (A ∈ ℕ₀ ∧ -B ∈ ℕ₀)) → B ≤ 0)
123		nn0ge0t 4550	. . . . . . . . . . 11 ⊢ (A ∈ ℕ₀ → 0 ≤ A)
124	123	ad2antrl 322	. . . . . . . . . 10 ⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ (A ∈ ℕ₀ ∧ -B ∈ ℕ₀)) → 0 ≤ A)
125		letrt 4291	. . . . . . . . . . . . 13 ⊢ ((B ∈ ℝ ∧ 0 ∈ ℝ ∧ A ∈ ℝ) → ((B ≤ 0 ∧ 0 ≤ A) → B ≤ A))
126	26, 125	mp3an2 640	. . . . . . . . . . . 12 ⊢ ((B ∈ ℝ ∧ A ∈ ℝ) → ((B ≤ 0 ∧ 0 ≤ A) → B ≤ A))
127	126	ancoms 334	. . . . . . . . . . 11 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((B ≤ 0 ∧ 0 ≤ A) → B ≤ A))
128	127	adantr 306	. . . . . . . . . 10 ⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ (A ∈ ℕ₀ ∧ -B ∈ ℕ₀)) → ((B ≤ 0 ∧ 0 ≤ A) → B ≤ A))
129	122, 124, 128	mp2and 526	. . . . . . . . 9 ⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ (A ∈ ℕ₀ ∧ -B ∈ ℕ₀)) → B ≤ A)
130		leltt 4278	. . . . . . . . . . 11 ⊢ ((B ∈ ℝ ∧ A ∈ ℝ) → (B ≤ A ↔ ¬ A < B))
131	130	ancoms 334	. . . . . . . . . 10 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (B ≤ A ↔ ¬ A < B))
132	131	adantr 306	. . . . . . . . 9 ⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ (A ∈ ℕ₀ ∧ -B ∈ ℕ₀)) → (B ≤ A ↔ ¬ A < B))
133	129, 132	mpbid 170	. . . . . . . 8 ⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ (A ∈ ℕ₀ ∧ -B ∈ ℕ₀)) → ¬ A < B)
134		ltplus1t 4383	. . . . . . . . . . 11 ⊢ (A ∈ ℝ → A < (A + 1))
135	134	ad2antll 320	. . . . . . . . . 10 ⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ (A ∈ ℕ₀ ∧ -B ∈ ℕ₀)) → A < (A + 1))
136		lelttrt 4289	. . . . . . . . . . . . . 14 ⊢ ((B ∈ ℝ ∧ A ∈ ℝ ∧ (A + 1) ∈ ℝ) → ((B ≤ A ∧ A < (A + 1)) → B < (A + 1)))
137	136	3expb 613	. . . . . . . . . . . . 13 ⊢ ((B ∈ ℝ ∧ (A ∈ ℝ ∧ (A + 1) ∈ ℝ)) → ((B ≤ A ∧ A < (A + 1)) → B < (A + 1)))
138	54	ancli 244	. . . . . . . . . . . . 13 ⊢ (A ∈ ℝ → (A ∈ ℝ ∧ (A + 1) ∈ ℝ))
139	137, 138	sylan2 346	. . . . . . . . . . . 12 ⊢ ((B ∈ ℝ ∧ A ∈ ℝ) → ((B ≤ A ∧ A < (A + 1)) → B < (A + 1)))
140	139	ancoms 334	. . . . . . . . . . 11 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((B ≤ A ∧ A < (A + 1)) → B < (A + 1)))
141	140	adantr 306	. . . . . . . . . 10 ⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ (A ∈ ℕ₀ ∧ -B ∈ ℕ₀)) → ((B ≤ A ∧ A < (A + 1)) → B < (A + 1)))
142	129, 135, 141	mp2and 526	. . . . . . . . 9 ⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ (A ∈ ℕ₀ ∧ -B ∈ ℕ₀)) → B < (A + 1))
143		leltt 4278	. . . . . . . . . . . 12 ⊢ (((A + 1) ∈ ℝ ∧ B ∈ ℝ) → ((A + 1) ≤ B ↔ ¬ B < (A + 1)))
144	143, 54	sylan 343	. . . . . . . . . . 11 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((A + 1) ≤ B ↔ ¬ B < (A + 1)))
145	144	bicon2d 404	. . . . . . . . . 10 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (B < (A + 1) ↔ ¬ (A + 1) ≤ B))
146	145	adantr 306	. . . . . . . . 9 ⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ (A ∈ ℕ₀ ∧ -B ∈ ℕ₀)) → (B < (A + 1) ↔ ¬ (A + 1) ≤ B))
147	142, 146	mpbid 170	. . . . . . . 8 ⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ (A ∈ ℕ₀ ∧ -B ∈ ℕ₀)) → ¬ (A + 1) ≤ B)
148	133, 147	jca 236	. . . . . . 7 ⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ (A ∈ ℕ₀ ∧ -B ∈ ℕ₀)) → (¬ A < B ∧ ¬ (A + 1) ≤ B))
149	148	exp 291	. . . . . 6 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((A ∈ ℕ₀ ∧ -B ∈ ℕ₀) → (¬ A < B ∧ ¬ (A + 1) ≤ B)))
150		pm5.21 502	. . . . . 6 ⊢ ((¬ A < B ∧ ¬ (A + 1) ≤ B) → (A < B ↔ (A + 1) ≤ B))
151	149, 150	syl6 23	. . . . 5 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((A ∈ ℕ₀ ∧ -B ∈ ℕ₀) → (A < B ↔ (A + 1) ≤ B)))
152		nn0ltlem1 4558	. . . . . . . . 9 ⊢ ((-B ∈ ℕ₀ ∧ -A ∈ ℕ₀) → (-B < -A ↔ -B ≤ (-A − 1)))
153	152	ancoms 334	. . . . . . . 8 ⊢ ((-A ∈ ℕ₀ ∧ -B ∈ ℕ₀) → (-B < -A ↔ -B ≤ (-A − 1)))
154	153	adantl 305	. . . . . . 7 ⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ (-A ∈ ℕ₀ ∧ -B ∈ ℕ₀)) → (-B < -A ↔ -B ≤ (-A − 1)))
155		ltnegt 4366	. . . . . . . 8 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A < B ↔ -B < -A))
156	155	adantr 306	. . . . . . 7 ⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ (-A ∈ ℕ₀ ∧ -B ∈ ℕ₀)) → (A < B ↔ -B < -A))
157		lenegt 4368	. . . . . . . . . 10 ⊢ (((A + 1) ∈ ℝ ∧ B ∈ ℝ) → ((A + 1) ≤ B ↔ -B ≤ -(A + 1)))
158	157, 54	sylan 343	. . . . . . . . 9 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((A + 1) ≤ B ↔ -B ≤ -(A + 1)))
159	46, 85	mpan2 519	. . . . . . . . . . . . 13 ⊢ (A ∈ ℂ → -(A + 1) = (-A + -1))
160	46, 86	mpan2 519	. . . . . . . . . . . . . 14 ⊢ (-A ∈ ℂ → (-A − 1) = (-A + -1))
161	87, 160	syl 12	. . . . . . . . . . . . 13 ⊢ (A ∈ ℂ → (-A − 1) = (-A + -1))
162	159, 161	eqtr4d 1131	. . . . . . . . . . . 12 ⊢ (A ∈ ℂ → -(A + 1) = (-A − 1))
163	3, 162	syl 12	. . . . . . . . . . 11 ⊢ (A ∈ ℝ → -(A + 1) = (-A − 1))
164	163	breq2d 2072	. . . . . . . . . 10 ⊢ (A ∈ ℝ → (-B ≤ -(A + 1) ↔ -B ≤ (-A − 1)))
165	164	adantr 306	. . . . . . . . 9 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (-B ≤ -(A + 1) ↔ -B ≤ (-A − 1)))
166	158, 165	bitrd 406	. . . . . . . 8 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((A + 1) ≤ B ↔ -B ≤ (-A − 1)))
167	166	adantr 306	. . . . . . 7 ⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ (-A ∈ ℕ₀ ∧ -B ∈ ℕ₀)) → ((A + 1) ≤ B ↔ -B ≤ (-A − 1)))
168	154, 156, 167	3bitr4d 424	. . . . . 6 ⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ (-A ∈ ℕ₀ ∧ -B ∈ ℕ₀)) → (A < B ↔ (A + 1) ≤ B))
169	168	exp 291	. . . . 5 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((-A ∈ ℕ₀ ∧ -B ∈ ℕ₀) → (A < B ↔ (A + 1) ≤ B)))
170	2, 115, 151, 169	ccased 563	. . . 4 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (((A ∈ ℕ₀ ∨ -A ∈ ℕ₀) ∧ (B ∈ ℕ₀ ∨ -B ∈ ℕ₀)) → (A < B ↔ (A + 1) ≤ B)))
171	170	imp 277	. . 3 ⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ ((A ∈ ℕ₀ ∨ -A ∈ ℕ₀) ∧ (B ∈ ℕ₀ ∨ -B ∈ ℕ₀))) → (A < B ↔ (A + 1) ≤ B))
172	171	an4s 390	. 2 ⊢ (((A ∈ ℝ ∧ (A ∈ ℕ₀ ∨ -A ∈ ℕ₀)) ∧ (B ∈ ℝ ∧ (B ∈ ℕ₀ ∨ -B ∈ ℕ₀))) → (A < B ↔ (A + 1) ≤ B))
173		elznn0 4576	. 2 ⊢ (A ∈ ℤ ↔ (A ∈ ℝ ∧ (A ∈ ℕ₀ ∨ -A ∈ ℕ₀)))
174		elznn0 4576	. 2 ⊢ (B ∈ ℤ ↔ (B ∈ ℝ ∧ (B ∈ ℕ₀ ∨ -B ∈ ℕ₀)))
175	172, 173, 174	syl2anb 350	1 ⊢ ((A ∈ ℤ ∧ B ∈ ℤ) → (A < B ↔ (A + 1) ≤ B))

Colors of variables: wff set class

Syntax hints: ¬ wn 1 → wi 2 ↔ wb 127 ∨ wo 195 ∧ wa 196 = wceq 1091 ∈ wcel 1092 class class class wbr 2054 (class class class)co 3001 ℂcc 4026 ℝcr 4027 0cc0 4028 1c1 4029 + caddc 4031 < clt 4033 − cmin 4089 -cneg 4090 ≤ cle 4092 ℕcn 4093 ℕ₀cn0 4094 ℤcz 4095

This theorem is referenced by: zleltp1t 4598 zlem1ltt 4599

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077 ax-reg 1078 ax-inf 1079

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ne 1192 df-ral 1205 df-rex 1206 df-reu 1207 df-rab 1208 df-v 1349 df-sbc 1441 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-pss 1494 df-nul 1708 df-if 1777 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-int 1966 df-iun 1996 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-lim 2204 df-suc 2205 df-om 2373 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-f 2434 df-f1 2435 df-fv 2438 df-rdg 2970 df-opr 3003 df-oprab 3004 df-1o 3104 df-oadd 3106 df-omul 3107 df-er 3200 df-ec 3202 df-qs 3205 df-ni 3794 df-pli 3795 df-mi 3796 df-lti 3797 df-plpq 3829 df-mpq 3830 df-enq 3831 df-nq 3832 df-plq 3833 df-mq 3834 df-rq 3835 df-ltq 3836 df-1q 3837 df-np 3880 df-1p 3881 df-plp 3882 df-mp 3883 df-ltp 3884 df-plpr 3958 df-mpr 3959 df-enr 3960 df-nr 3961 df-plr 3962 df-mr 3963 df-ltr 3964 df-0r 3965 df-1r 3966 df-m1r 3967 df-c 4034 df-0 4035 df-1 4036 df-r 4038 df-plus 4039 df-mul 4040 df-lt 4041 df-sub 4133 df-neg 4135 df-le 4277 df-n 4423 df-n0 4535 df-z 4564

metamath.org