MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elfznelfzo Structured version   Visualization version   GIF version

Theorem elfznelfzo 12390
Description: A value in a finite set of sequential integers is a border value if it is not contained in the half-open integer range contained in the finite set of sequential integers. (Contributed by Alexander van der Vekens, 31-Oct-2017.)
Assertion
Ref Expression
elfznelfzo ((𝑦 ∈ (0...𝐾) ∧ ¬ 𝑦 ∈ (1..^𝐾)) → (𝑦 = 0 ∨ 𝑦 = 𝐾))

Proof of Theorem elfznelfzo
StepHypRef Expression
1 elfz2nn0 12251 . . 3 (𝑦 ∈ (0...𝐾) ↔ (𝑦 ∈ ℕ0𝐾 ∈ ℕ0𝑦𝐾))
2 nn0z 11229 . . . . . . . 8 (𝑦 ∈ ℕ0𝑦 ∈ ℤ)
3 nn0z 11229 . . . . . . . 8 (𝐾 ∈ ℕ0𝐾 ∈ ℤ)
42, 3anim12i 587 . . . . . . 7 ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0) → (𝑦 ∈ ℤ ∧ 𝐾 ∈ ℤ))
543adant3 1073 . . . . . 6 ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0𝑦𝐾) → (𝑦 ∈ ℤ ∧ 𝐾 ∈ ℤ))
6 elfzom1b 12384 . . . . . 6 ((𝑦 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑦 ∈ (1..^𝐾) ↔ (𝑦 − 1) ∈ (0..^(𝐾 − 1))))
75, 6syl 17 . . . . 5 ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0𝑦𝐾) → (𝑦 ∈ (1..^𝐾) ↔ (𝑦 − 1) ∈ (0..^(𝐾 − 1))))
87notbid 306 . . . 4 ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0𝑦𝐾) → (¬ 𝑦 ∈ (1..^𝐾) ↔ ¬ (𝑦 − 1) ∈ (0..^(𝐾 − 1))))
9 elfzo0 12327 . . . . . . 7 ((𝑦 − 1) ∈ (0..^(𝐾 − 1)) ↔ ((𝑦 − 1) ∈ ℕ0 ∧ (𝐾 − 1) ∈ ℕ ∧ (𝑦 − 1) < (𝐾 − 1)))
109a1i 11 . . . . . 6 ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0𝑦𝐾) → ((𝑦 − 1) ∈ (0..^(𝐾 − 1)) ↔ ((𝑦 − 1) ∈ ℕ0 ∧ (𝐾 − 1) ∈ ℕ ∧ (𝑦 − 1) < (𝐾 − 1))))
1110notbid 306 . . . . 5 ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0𝑦𝐾) → (¬ (𝑦 − 1) ∈ (0..^(𝐾 − 1)) ↔ ¬ ((𝑦 − 1) ∈ ℕ0 ∧ (𝐾 − 1) ∈ ℕ ∧ (𝑦 − 1) < (𝐾 − 1))))
12 3ianor 1047 . . . . . . 7 (¬ ((𝑦 − 1) ∈ ℕ0 ∧ (𝐾 − 1) ∈ ℕ ∧ (𝑦 − 1) < (𝐾 − 1)) ↔ (¬ (𝑦 − 1) ∈ ℕ0 ∨ ¬ (𝐾 − 1) ∈ ℕ ∨ ¬ (𝑦 − 1) < (𝐾 − 1)))
13 elnnne0 11149 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ ↔ (𝑦 ∈ ℕ0𝑦 ≠ 0))
14 df-ne 2777 . . . . . . . . . . . . . . . . . 18 (𝑦 ≠ 0 ↔ ¬ 𝑦 = 0)
1514anbi2i 725 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℕ0𝑦 ≠ 0) ↔ (𝑦 ∈ ℕ0 ∧ ¬ 𝑦 = 0))
1613, 15bitr2i 263 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℕ0 ∧ ¬ 𝑦 = 0) ↔ 𝑦 ∈ ℕ)
17 nnm1nn0 11177 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (𝑦 − 1) ∈ ℕ0)
1816, 17sylbi 205 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ0 ∧ ¬ 𝑦 = 0) → (𝑦 − 1) ∈ ℕ0)
1918ex 448 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ0 → (¬ 𝑦 = 0 → (𝑦 − 1) ∈ ℕ0))
2019con1d 137 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ0 → (¬ (𝑦 − 1) ∈ ℕ0𝑦 = 0))
2120imp 443 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ0 ∧ ¬ (𝑦 − 1) ∈ ℕ0) → 𝑦 = 0)
2221orcd 405 . . . . . . . . . . 11 ((𝑦 ∈ ℕ0 ∧ ¬ (𝑦 − 1) ∈ ℕ0) → (𝑦 = 0 ∨ 𝑦 = 𝐾))
2322ex 448 . . . . . . . . . 10 (𝑦 ∈ ℕ0 → (¬ (𝑦 − 1) ∈ ℕ0 → (𝑦 = 0 ∨ 𝑦 = 𝐾)))
24233ad2ant1 1074 . . . . . . . . 9 ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0𝑦𝐾) → (¬ (𝑦 − 1) ∈ ℕ0 → (𝑦 = 0 ∨ 𝑦 = 𝐾)))
2524com12 32 . . . . . . . 8 (¬ (𝑦 − 1) ∈ ℕ0 → ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0𝑦𝐾) → (𝑦 = 0 ∨ 𝑦 = 𝐾)))
26 ioran 509 . . . . . . . . . . . 12 (¬ (𝑦 = 0 ∨ 𝑦 = 𝐾) ↔ (¬ 𝑦 = 0 ∧ ¬ 𝑦 = 𝐾))
27 nn1m1nn 10883 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ℕ → (𝑦 = 1 ∨ (𝑦 − 1) ∈ ℕ))
28 df-ne 2777 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦𝐾 ↔ ¬ 𝑦 = 𝐾)
29 nn0re 11144 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 ∈ ℕ0𝑦 ∈ ℝ)
3029ad2antlr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝐾 ∈ ℕ0𝑦 ∈ ℕ0) ∧ 𝑦𝐾) → 𝑦 ∈ ℝ)
31 nn0re 11144 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝐾 ∈ ℕ0𝐾 ∈ ℝ)
3231adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐾 ∈ ℕ0𝑦 ∈ ℕ0) → 𝐾 ∈ ℝ)
3332adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝐾 ∈ ℕ0𝑦 ∈ ℕ0) ∧ 𝑦𝐾) → 𝐾 ∈ ℝ)
34 simpr 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝐾 ∈ ℕ0𝑦 ∈ ℕ0) ∧ 𝑦𝐾) → 𝑦𝐾)
3530, 33, 34leltned 10037 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝐾 ∈ ℕ0𝑦 ∈ ℕ0) ∧ 𝑦𝐾) → (𝑦 < 𝐾𝐾𝑦))
36 necom 2830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑦𝐾𝐾𝑦)
3735, 36syl6rbbr 277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐾 ∈ ℕ0𝑦 ∈ ℕ0) ∧ 𝑦𝐾) → (𝑦𝐾𝑦 < 𝐾))
3837adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝐾 ∈ ℕ0𝑦 ∈ ℕ0) ∧ 𝑦𝐾) ∧ 𝑦 = 1) → (𝑦𝐾𝑦 < 𝐾))
39 breq1 4576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 = 1 → (𝑦 < 𝐾 ↔ 1 < 𝐾))
4039biimpa 499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑦 = 1 ∧ 𝑦 < 𝐾) → 1 < 𝐾)
41 1red 9907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐾 ∈ ℕ0𝑦 ∈ ℕ0) → 1 ∈ ℝ)
4241, 32, 41ltsub1d 10481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐾 ∈ ℕ0𝑦 ∈ ℕ0) → (1 < 𝐾 ↔ (1 − 1) < (𝐾 − 1)))
43 1m1e0 10932 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (1 − 1) = 0
4443breq1i 4580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((1 − 1) < (𝐾 − 1) ↔ 0 < (𝐾 − 1))
45 1zzd 11237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝐾 ∈ ℕ0 → 1 ∈ ℤ)
463, 45zsubcld 11315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝐾 ∈ ℕ0 → (𝐾 − 1) ∈ ℤ)
4746adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝐾 ∈ ℕ0𝑦 ∈ ℕ0) → (𝐾 − 1) ∈ ℤ)
4847adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝐾 ∈ ℕ0𝑦 ∈ ℕ0) ∧ 0 < (𝐾 − 1)) → (𝐾 − 1) ∈ ℤ)
49 simpr 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝐾 ∈ ℕ0𝑦 ∈ ℕ0) ∧ 0 < (𝐾 − 1)) → 0 < (𝐾 − 1))
50 elnnz 11216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝐾 − 1) ∈ ℕ ↔ ((𝐾 − 1) ∈ ℤ ∧ 0 < (𝐾 − 1)))
5148, 49, 50sylanbrc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝐾 ∈ ℕ0𝑦 ∈ ℕ0) ∧ 0 < (𝐾 − 1)) → (𝐾 − 1) ∈ ℕ)
5251ex 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐾 ∈ ℕ0𝑦 ∈ ℕ0) → (0 < (𝐾 − 1) → (𝐾 − 1) ∈ ℕ))
5344, 52syl5bi 230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐾 ∈ ℕ0𝑦 ∈ ℕ0) → ((1 − 1) < (𝐾 − 1) → (𝐾 − 1) ∈ ℕ))
5442, 53sylbid 228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐾 ∈ ℕ0𝑦 ∈ ℕ0) → (1 < 𝐾 → (𝐾 − 1) ∈ ℕ))
5540, 54syl5 33 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐾 ∈ ℕ0𝑦 ∈ ℕ0) → ((𝑦 = 1 ∧ 𝑦 < 𝐾) → (𝐾 − 1) ∈ ℕ))
5655expd 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐾 ∈ ℕ0𝑦 ∈ ℕ0) → (𝑦 = 1 → (𝑦 < 𝐾 → (𝐾 − 1) ∈ ℕ)))
5756adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐾 ∈ ℕ0𝑦 ∈ ℕ0) ∧ 𝑦𝐾) → (𝑦 = 1 → (𝑦 < 𝐾 → (𝐾 − 1) ∈ ℕ)))
5857imp 443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝐾 ∈ ℕ0𝑦 ∈ ℕ0) ∧ 𝑦𝐾) ∧ 𝑦 = 1) → (𝑦 < 𝐾 → (𝐾 − 1) ∈ ℕ))
5938, 58sylbid 228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝐾 ∈ ℕ0𝑦 ∈ ℕ0) ∧ 𝑦𝐾) ∧ 𝑦 = 1) → (𝑦𝐾 → (𝐾 − 1) ∈ ℕ))
6059exp31 627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐾 ∈ ℕ0𝑦 ∈ ℕ0) → (𝑦𝐾 → (𝑦 = 1 → (𝑦𝐾 → (𝐾 − 1) ∈ ℕ))))
6160com14 93 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦𝐾 → (𝑦𝐾 → (𝑦 = 1 → ((𝐾 ∈ ℕ0𝑦 ∈ ℕ0) → (𝐾 − 1) ∈ ℕ))))
6228, 61sylbir 223 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑦 = 𝐾 → (𝑦𝐾 → (𝑦 = 1 → ((𝐾 ∈ ℕ0𝑦 ∈ ℕ0) → (𝐾 − 1) ∈ ℕ))))
6362com23 83 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑦 = 𝐾 → (𝑦 = 1 → (𝑦𝐾 → ((𝐾 ∈ ℕ0𝑦 ∈ ℕ0) → (𝐾 − 1) ∈ ℕ))))
6463com14 93 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐾 ∈ ℕ0𝑦 ∈ ℕ0) → (𝑦 = 1 → (𝑦𝐾 → (¬ 𝑦 = 𝐾 → (𝐾 − 1) ∈ ℕ))))
6564ex 448 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐾 ∈ ℕ0 → (𝑦 ∈ ℕ0 → (𝑦 = 1 → (𝑦𝐾 → (¬ 𝑦 = 𝐾 → (𝐾 − 1) ∈ ℕ)))))
6665com14 93 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦𝐾 → (𝑦 ∈ ℕ0 → (𝑦 = 1 → (𝐾 ∈ ℕ0 → (¬ 𝑦 = 𝐾 → (𝐾 − 1) ∈ ℕ)))))
6766com13 85 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 1 → (𝑦 ∈ ℕ0 → (𝑦𝐾 → (𝐾 ∈ ℕ0 → (¬ 𝑦 = 𝐾 → (𝐾 − 1) ∈ ℕ)))))
6829ad2antlr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑦 − 1) ∈ ℕ ∧ 𝑦 ∈ ℕ0) ∧ 𝐾 ∈ ℕ0) → 𝑦 ∈ ℝ)
6931adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑦 − 1) ∈ ℕ ∧ 𝑦 ∈ ℕ0) ∧ 𝐾 ∈ ℕ0) → 𝐾 ∈ ℝ)
70 1red 9907 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑦 − 1) ∈ ℕ ∧ 𝑦 ∈ ℕ0) ∧ 𝐾 ∈ ℕ0) → 1 ∈ ℝ)
7168, 69, 70lesub1d 10479 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑦 − 1) ∈ ℕ ∧ 𝑦 ∈ ℕ0) ∧ 𝐾 ∈ ℕ0) → (𝑦𝐾 ↔ (𝑦 − 1) ≤ (𝐾 − 1)))
723ad2antlr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝑦 − 1) ∈ ℕ ∧ 𝑦 ∈ ℕ0) ∧ 𝐾 ∈ ℕ0) ∧ (𝑦 − 1) ≤ (𝐾 − 1)) → 𝐾 ∈ ℤ)
73 1zzd 11237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝑦 − 1) ∈ ℕ ∧ 𝑦 ∈ ℕ0) ∧ 𝐾 ∈ ℕ0) ∧ (𝑦 − 1) ≤ (𝐾 − 1)) → 1 ∈ ℤ)
7472, 73zsubcld 11315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝑦 − 1) ∈ ℕ ∧ 𝑦 ∈ ℕ0) ∧ 𝐾 ∈ ℕ0) ∧ (𝑦 − 1) ≤ (𝐾 − 1)) → (𝐾 − 1) ∈ ℤ)
75 nngt0 10892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑦 − 1) ∈ ℕ → 0 < (𝑦 − 1))
76 0red 9893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0) → 0 ∈ ℝ)
77 peano2rem 10195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑦 ∈ ℝ → (𝑦 − 1) ∈ ℝ)
7829, 77syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 ∈ ℕ0 → (𝑦 − 1) ∈ ℝ)
7978adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0) → (𝑦 − 1) ∈ ℝ)
80 peano2rem 10195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝐾 ∈ ℝ → (𝐾 − 1) ∈ ℝ)
8131, 80syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝐾 ∈ ℕ0 → (𝐾 − 1) ∈ ℝ)
8281adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0) → (𝐾 − 1) ∈ ℝ)
83 ltletr 9976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((0 ∈ ℝ ∧ (𝑦 − 1) ∈ ℝ ∧ (𝐾 − 1) ∈ ℝ) → ((0 < (𝑦 − 1) ∧ (𝑦 − 1) ≤ (𝐾 − 1)) → 0 < (𝐾 − 1)))
8476, 79, 82, 83syl3anc 1317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0) → ((0 < (𝑦 − 1) ∧ (𝑦 − 1) ≤ (𝐾 − 1)) → 0 < (𝐾 − 1)))
8584ex 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑦 ∈ ℕ0 → (𝐾 ∈ ℕ0 → ((0 < (𝑦 − 1) ∧ (𝑦 − 1) ≤ (𝐾 − 1)) → 0 < (𝐾 − 1))))
8685com13 85 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((0 < (𝑦 − 1) ∧ (𝑦 − 1) ≤ (𝐾 − 1)) → (𝐾 ∈ ℕ0 → (𝑦 ∈ ℕ0 → 0 < (𝐾 − 1))))
8786ex 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (0 < (𝑦 − 1) → ((𝑦 − 1) ≤ (𝐾 − 1) → (𝐾 ∈ ℕ0 → (𝑦 ∈ ℕ0 → 0 < (𝐾 − 1)))))
8887com24 92 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (0 < (𝑦 − 1) → (𝑦 ∈ ℕ0 → (𝐾 ∈ ℕ0 → ((𝑦 − 1) ≤ (𝐾 − 1) → 0 < (𝐾 − 1)))))
8975, 88syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑦 − 1) ∈ ℕ → (𝑦 ∈ ℕ0 → (𝐾 ∈ ℕ0 → ((𝑦 − 1) ≤ (𝐾 − 1) → 0 < (𝐾 − 1)))))
9089imp41 616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝑦 − 1) ∈ ℕ ∧ 𝑦 ∈ ℕ0) ∧ 𝐾 ∈ ℕ0) ∧ (𝑦 − 1) ≤ (𝐾 − 1)) → 0 < (𝐾 − 1))
9174, 90, 50sylanbrc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝑦 − 1) ∈ ℕ ∧ 𝑦 ∈ ℕ0) ∧ 𝐾 ∈ ℕ0) ∧ (𝑦 − 1) ≤ (𝐾 − 1)) → (𝐾 − 1) ∈ ℕ)
9291a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝑦 − 1) ∈ ℕ ∧ 𝑦 ∈ ℕ0) ∧ 𝐾 ∈ ℕ0) ∧ (𝑦 − 1) ≤ (𝐾 − 1)) → (¬ 𝑦 = 𝐾 → (𝐾 − 1) ∈ ℕ))
9392ex 448 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑦 − 1) ∈ ℕ ∧ 𝑦 ∈ ℕ0) ∧ 𝐾 ∈ ℕ0) → ((𝑦 − 1) ≤ (𝐾 − 1) → (¬ 𝑦 = 𝐾 → (𝐾 − 1) ∈ ℕ)))
9471, 93sylbid 228 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑦 − 1) ∈ ℕ ∧ 𝑦 ∈ ℕ0) ∧ 𝐾 ∈ ℕ0) → (𝑦𝐾 → (¬ 𝑦 = 𝐾 → (𝐾 − 1) ∈ ℕ)))
9594ex 448 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑦 − 1) ∈ ℕ ∧ 𝑦 ∈ ℕ0) → (𝐾 ∈ ℕ0 → (𝑦𝐾 → (¬ 𝑦 = 𝐾 → (𝐾 − 1) ∈ ℕ))))
9695com23 83 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑦 − 1) ∈ ℕ ∧ 𝑦 ∈ ℕ0) → (𝑦𝐾 → (𝐾 ∈ ℕ0 → (¬ 𝑦 = 𝐾 → (𝐾 − 1) ∈ ℕ))))
9796ex 448 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 − 1) ∈ ℕ → (𝑦 ∈ ℕ0 → (𝑦𝐾 → (𝐾 ∈ ℕ0 → (¬ 𝑦 = 𝐾 → (𝐾 − 1) ∈ ℕ)))))
9867, 97jaoi 392 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 = 1 ∨ (𝑦 − 1) ∈ ℕ) → (𝑦 ∈ ℕ0 → (𝑦𝐾 → (𝐾 ∈ ℕ0 → (¬ 𝑦 = 𝐾 → (𝐾 − 1) ∈ ℕ)))))
9927, 98syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ℕ → (𝑦 ∈ ℕ0 → (𝑦𝐾 → (𝐾 ∈ ℕ0 → (¬ 𝑦 = 𝐾 → (𝐾 − 1) ∈ ℕ)))))
10013, 99sylbir 223 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ℕ0𝑦 ≠ 0) → (𝑦 ∈ ℕ0 → (𝑦𝐾 → (𝐾 ∈ ℕ0 → (¬ 𝑦 = 𝐾 → (𝐾 − 1) ∈ ℕ)))))
101100ex 448 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ0 → (𝑦 ≠ 0 → (𝑦 ∈ ℕ0 → (𝑦𝐾 → (𝐾 ∈ ℕ0 → (¬ 𝑦 = 𝐾 → (𝐾 − 1) ∈ ℕ))))))
102101pm2.43a 51 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ0 → (𝑦 ≠ 0 → (𝑦𝐾 → (𝐾 ∈ ℕ0 → (¬ 𝑦 = 𝐾 → (𝐾 − 1) ∈ ℕ)))))
103102com24 92 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ0 → (𝐾 ∈ ℕ0 → (𝑦𝐾 → (𝑦 ≠ 0 → (¬ 𝑦 = 𝐾 → (𝐾 − 1) ∈ ℕ)))))
1041033imp 1248 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0𝑦𝐾) → (𝑦 ≠ 0 → (¬ 𝑦 = 𝐾 → (𝐾 − 1) ∈ ℕ)))
105104com3l 86 . . . . . . . . . . . . . 14 (𝑦 ≠ 0 → (¬ 𝑦 = 𝐾 → ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0𝑦𝐾) → (𝐾 − 1) ∈ ℕ)))
10614, 105sylbir 223 . . . . . . . . . . . . 13 𝑦 = 0 → (¬ 𝑦 = 𝐾 → ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0𝑦𝐾) → (𝐾 − 1) ∈ ℕ)))
107106imp 443 . . . . . . . . . . . 12 ((¬ 𝑦 = 0 ∧ ¬ 𝑦 = 𝐾) → ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0𝑦𝐾) → (𝐾 − 1) ∈ ℕ))
10826, 107sylbi 205 . . . . . . . . . . 11 (¬ (𝑦 = 0 ∨ 𝑦 = 𝐾) → ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0𝑦𝐾) → (𝐾 − 1) ∈ ℕ))
109108com12 32 . . . . . . . . . 10 ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0𝑦𝐾) → (¬ (𝑦 = 0 ∨ 𝑦 = 𝐾) → (𝐾 − 1) ∈ ℕ))
110109con1d 137 . . . . . . . . 9 ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0𝑦𝐾) → (¬ (𝐾 − 1) ∈ ℕ → (𝑦 = 0 ∨ 𝑦 = 𝐾)))
111110com12 32 . . . . . . . 8 (¬ (𝐾 − 1) ∈ ℕ → ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0𝑦𝐾) → (𝑦 = 0 ∨ 𝑦 = 𝐾)))
11229adantr 479 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0) → 𝑦 ∈ ℝ)
11331adantl 480 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0) → 𝐾 ∈ ℝ)
114 1red 9907 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0) → 1 ∈ ℝ)
115112, 113, 1143jca 1234 . . . . . . . . . . . . . 14 ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0) → (𝑦 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 1 ∈ ℝ))
1161153adant3 1073 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0𝑦𝐾) → (𝑦 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 1 ∈ ℝ))
117 ltsub1 10369 . . . . . . . . . . . . 13 ((𝑦 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 1 ∈ ℝ) → (𝑦 < 𝐾 ↔ (𝑦 − 1) < (𝐾 − 1)))
118116, 117syl 17 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0𝑦𝐾) → (𝑦 < 𝐾 ↔ (𝑦 − 1) < (𝐾 − 1)))
119118bicomd 211 . . . . . . . . . . 11 ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0𝑦𝐾) → ((𝑦 − 1) < (𝐾 − 1) ↔ 𝑦 < 𝐾))
120119notbid 306 . . . . . . . . . 10 ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0𝑦𝐾) → (¬ (𝑦 − 1) < (𝐾 − 1) ↔ ¬ 𝑦 < 𝐾))
121 eqlelt 9972 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℝ ∧ 𝐾 ∈ ℝ) → (𝑦 = 𝐾 ↔ (𝑦𝐾 ∧ ¬ 𝑦 < 𝐾)))
12229, 31, 121syl2an 492 . . . . . . . . . . . . . 14 ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0) → (𝑦 = 𝐾 ↔ (𝑦𝐾 ∧ ¬ 𝑦 < 𝐾)))
123122biimpar 500 . . . . . . . . . . . . 13 (((𝑦 ∈ ℕ0𝐾 ∈ ℕ0) ∧ (𝑦𝐾 ∧ ¬ 𝑦 < 𝐾)) → 𝑦 = 𝐾)
124123olcd 406 . . . . . . . . . . . 12 (((𝑦 ∈ ℕ0𝐾 ∈ ℕ0) ∧ (𝑦𝐾 ∧ ¬ 𝑦 < 𝐾)) → (𝑦 = 0 ∨ 𝑦 = 𝐾))
125124exp43 637 . . . . . . . . . . 11 (𝑦 ∈ ℕ0 → (𝐾 ∈ ℕ0 → (𝑦𝐾 → (¬ 𝑦 < 𝐾 → (𝑦 = 0 ∨ 𝑦 = 𝐾)))))
1261253imp 1248 . . . . . . . . . 10 ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0𝑦𝐾) → (¬ 𝑦 < 𝐾 → (𝑦 = 0 ∨ 𝑦 = 𝐾)))
127120, 126sylbid 228 . . . . . . . . 9 ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0𝑦𝐾) → (¬ (𝑦 − 1) < (𝐾 − 1) → (𝑦 = 0 ∨ 𝑦 = 𝐾)))
128127com12 32 . . . . . . . 8 (¬ (𝑦 − 1) < (𝐾 − 1) → ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0𝑦𝐾) → (𝑦 = 0 ∨ 𝑦 = 𝐾)))
12925, 111, 1283jaoi 1382 . . . . . . 7 ((¬ (𝑦 − 1) ∈ ℕ0 ∨ ¬ (𝐾 − 1) ∈ ℕ ∨ ¬ (𝑦 − 1) < (𝐾 − 1)) → ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0𝑦𝐾) → (𝑦 = 0 ∨ 𝑦 = 𝐾)))
13012, 129sylbi 205 . . . . . 6 (¬ ((𝑦 − 1) ∈ ℕ0 ∧ (𝐾 − 1) ∈ ℕ ∧ (𝑦 − 1) < (𝐾 − 1)) → ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0𝑦𝐾) → (𝑦 = 0 ∨ 𝑦 = 𝐾)))
131130com12 32 . . . . 5 ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0𝑦𝐾) → (¬ ((𝑦 − 1) ∈ ℕ0 ∧ (𝐾 − 1) ∈ ℕ ∧ (𝑦 − 1) < (𝐾 − 1)) → (𝑦 = 0 ∨ 𝑦 = 𝐾)))
13211, 131sylbid 228 . . . 4 ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0𝑦𝐾) → (¬ (𝑦 − 1) ∈ (0..^(𝐾 − 1)) → (𝑦 = 0 ∨ 𝑦 = 𝐾)))
1338, 132sylbid 228 . . 3 ((𝑦 ∈ ℕ0𝐾 ∈ ℕ0𝑦𝐾) → (¬ 𝑦 ∈ (1..^𝐾) → (𝑦 = 0 ∨ 𝑦 = 𝐾)))
1341, 133sylbi 205 . 2 (𝑦 ∈ (0...𝐾) → (¬ 𝑦 ∈ (1..^𝐾) → (𝑦 = 0 ∨ 𝑦 = 𝐾)))
135134imp 443 1 ((𝑦 ∈ (0...𝐾) ∧ ¬ 𝑦 ∈ (1..^𝐾)) → (𝑦 = 0 ∨ 𝑦 = 𝐾))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382  w3o 1029  w3a 1030   = wceq 1474  wcel 1975  wne 2775   class class class wbr 4573  (class class class)co 6523  cr 9787  0cc0 9788  1c1 9789   < clt 9926  cle 9927  cmin 10113  cn 10863  0cn0 11135  cz 11206  ...cfz 12148  ..^cfzo 12285
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-nul 4708  ax-pow 4760  ax-pr 4824  ax-un 6820  ax-cnex 9844  ax-resscn 9845  ax-1cn 9846  ax-icn 9847  ax-addcl 9848  ax-addrcl 9849  ax-mulcl 9850  ax-mulrcl 9851  ax-mulcom 9852  ax-addass 9853  ax-mulass 9854  ax-distr 9855  ax-i2m1 9856  ax-1ne0 9857  ax-1rid 9858  ax-rnegex 9859  ax-rrecex 9860  ax-cnre 9861  ax-pre-lttri 9862  ax-pre-lttrn 9863  ax-pre-ltadd 9864  ax-pre-mulgt0 9865
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-nel 2778  df-ral 2896  df-rex 2897  df-reu 2898  df-rab 2900  df-v 3170  df-sbc 3398  df-csb 3495  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-pss 3551  df-nul 3870  df-if 4032  df-pw 4105  df-sn 4121  df-pr 4123  df-tp 4125  df-op 4127  df-uni 4363  df-iun 4447  df-br 4574  df-opab 4634  df-mpt 4635  df-tr 4671  df-eprel 4935  df-id 4939  df-po 4945  df-so 4946  df-fr 4983  df-we 4985  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037  df-pred 5579  df-ord 5625  df-on 5626  df-lim 5627  df-suc 5628  df-iota 5750  df-fun 5788  df-fn 5789  df-f 5790  df-f1 5791  df-fo 5792  df-f1o 5793  df-fv 5794  df-riota 6485  df-ov 6526  df-oprab 6527  df-mpt2 6528  df-om 6931  df-1st 7032  df-2nd 7033  df-wrecs 7267  df-recs 7328  df-rdg 7366  df-er 7602  df-en 7815  df-dom 7816  df-sdom 7817  df-pnf 9928  df-mnf 9929  df-xr 9930  df-ltxr 9931  df-le 9932  df-sub 10115  df-neg 10116  df-nn 10864  df-n0 11136  df-z 11207  df-uz 11516  df-fz 12149  df-fzo 12286
This theorem is referenced by:  elfznelfzob  12391  injresinjlem  12401
  Copyright terms: Public domain W3C validator