Step |
Hyp |
Ref |
Expression |
1 |
|
fzind.1 |
⊢ ( 𝑥 = 𝑀 → ( 𝜑 ↔ 𝜓 ) ) |
2 |
|
fzind.2 |
⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) ) |
3 |
|
fzind.3 |
⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑 ↔ 𝜃 ) ) |
4 |
|
fzind.4 |
⊢ ( 𝑥 = 𝐾 → ( 𝜑 ↔ 𝜏 ) ) |
5 |
|
fzind.5 |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → 𝜓 ) |
6 |
|
fzind.6 |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) → ( 𝜒 → 𝜃 ) ) |
7 |
|
breq1 |
⊢ ( 𝑥 = 𝑀 → ( 𝑥 ≤ 𝑁 ↔ 𝑀 ≤ 𝑁 ) ) |
8 |
7
|
anbi2d |
⊢ ( 𝑥 = 𝑀 → ( ( 𝑁 ∈ ℤ ∧ 𝑥 ≤ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) ) ) |
9 |
8 1
|
imbi12d |
⊢ ( 𝑥 = 𝑀 → ( ( ( 𝑁 ∈ ℤ ∧ 𝑥 ≤ 𝑁 ) → 𝜑 ) ↔ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → 𝜓 ) ) ) |
10 |
|
breq1 |
⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≤ 𝑁 ↔ 𝑦 ≤ 𝑁 ) ) |
11 |
10
|
anbi2d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝑁 ∈ ℤ ∧ 𝑥 ≤ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝑦 ≤ 𝑁 ) ) ) |
12 |
11 2
|
imbi12d |
⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑁 ∈ ℤ ∧ 𝑥 ≤ 𝑁 ) → 𝜑 ) ↔ ( ( 𝑁 ∈ ℤ ∧ 𝑦 ≤ 𝑁 ) → 𝜒 ) ) ) |
13 |
|
breq1 |
⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 ≤ 𝑁 ↔ ( 𝑦 + 1 ) ≤ 𝑁 ) ) |
14 |
13
|
anbi2d |
⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑁 ∈ ℤ ∧ 𝑥 ≤ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) ) ) |
15 |
14 3
|
imbi12d |
⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( 𝑁 ∈ ℤ ∧ 𝑥 ≤ 𝑁 ) → 𝜑 ) ↔ ( ( 𝑁 ∈ ℤ ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → 𝜃 ) ) ) |
16 |
|
breq1 |
⊢ ( 𝑥 = 𝐾 → ( 𝑥 ≤ 𝑁 ↔ 𝐾 ≤ 𝑁 ) ) |
17 |
16
|
anbi2d |
⊢ ( 𝑥 = 𝐾 → ( ( 𝑁 ∈ ℤ ∧ 𝑥 ≤ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁 ) ) ) |
18 |
17 4
|
imbi12d |
⊢ ( 𝑥 = 𝐾 → ( ( ( 𝑁 ∈ ℤ ∧ 𝑥 ≤ 𝑁 ) → 𝜑 ) ↔ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁 ) → 𝜏 ) ) ) |
19 |
5
|
3expib |
⊢ ( 𝑀 ∈ ℤ → ( ( 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → 𝜓 ) ) |
20 |
|
zre |
⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℝ ) |
21 |
|
zre |
⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ ) |
22 |
|
p1le |
⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → 𝑦 ≤ 𝑁 ) |
23 |
22
|
3expia |
⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑦 + 1 ) ≤ 𝑁 → 𝑦 ≤ 𝑁 ) ) |
24 |
20 21 23
|
syl2an |
⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑦 + 1 ) ≤ 𝑁 → 𝑦 ≤ 𝑁 ) ) |
25 |
24
|
imdistanda |
⊢ ( 𝑦 ∈ ℤ → ( ( 𝑁 ∈ ℤ ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → ( 𝑁 ∈ ℤ ∧ 𝑦 ≤ 𝑁 ) ) ) |
26 |
25
|
imim1d |
⊢ ( 𝑦 ∈ ℤ → ( ( ( 𝑁 ∈ ℤ ∧ 𝑦 ≤ 𝑁 ) → 𝜒 ) → ( ( 𝑁 ∈ ℤ ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → 𝜒 ) ) ) |
27 |
26
|
3ad2ant2 |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) → ( ( ( 𝑁 ∈ ℤ ∧ 𝑦 ≤ 𝑁 ) → 𝜒 ) → ( ( 𝑁 ∈ ℤ ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → 𝜒 ) ) ) |
28 |
|
zltp1le |
⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑦 < 𝑁 ↔ ( 𝑦 + 1 ) ≤ 𝑁 ) ) |
29 |
28
|
adantlr |
⊢ ( ( ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑦 < 𝑁 ↔ ( 𝑦 + 1 ) ≤ 𝑁 ) ) |
30 |
29
|
expcom |
⊢ ( 𝑁 ∈ ℤ → ( ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) → ( 𝑦 < 𝑁 ↔ ( 𝑦 + 1 ) ≤ 𝑁 ) ) ) |
31 |
30
|
pm5.32d |
⊢ ( 𝑁 ∈ ℤ → ( ( ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) ∧ 𝑦 < 𝑁 ) ↔ ( ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) ) ) |
32 |
31
|
adantl |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) ∧ 𝑦 < 𝑁 ) ↔ ( ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) ) ) |
33 |
6
|
expcom |
⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝜒 → 𝜃 ) ) ) |
34 |
33
|
3expa |
⊢ ( ( ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) ∧ 𝑦 < 𝑁 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝜒 → 𝜃 ) ) ) |
35 |
34
|
com12 |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) ∧ 𝑦 < 𝑁 ) → ( 𝜒 → 𝜃 ) ) ) |
36 |
32 35
|
sylbird |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → ( 𝜒 → 𝜃 ) ) ) |
37 |
36
|
ex |
⊢ ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ℤ → ( ( ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → ( 𝜒 → 𝜃 ) ) ) ) |
38 |
37
|
com23 |
⊢ ( 𝑀 ∈ ℤ → ( ( ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → ( 𝑁 ∈ ℤ → ( 𝜒 → 𝜃 ) ) ) ) |
39 |
38
|
expd |
⊢ ( 𝑀 ∈ ℤ → ( ( 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) → ( ( 𝑦 + 1 ) ≤ 𝑁 → ( 𝑁 ∈ ℤ → ( 𝜒 → 𝜃 ) ) ) ) ) |
40 |
39
|
3impib |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) → ( ( 𝑦 + 1 ) ≤ 𝑁 → ( 𝑁 ∈ ℤ → ( 𝜒 → 𝜃 ) ) ) ) |
41 |
40
|
impcomd |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) → ( ( 𝑁 ∈ ℤ ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → ( 𝜒 → 𝜃 ) ) ) |
42 |
41
|
a2d |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) → ( ( ( 𝑁 ∈ ℤ ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → 𝜒 ) → ( ( 𝑁 ∈ ℤ ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → 𝜃 ) ) ) |
43 |
27 42
|
syld |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ) → ( ( ( 𝑁 ∈ ℤ ∧ 𝑦 ≤ 𝑁 ) → 𝜒 ) → ( ( 𝑁 ∈ ℤ ∧ ( 𝑦 + 1 ) ≤ 𝑁 ) → 𝜃 ) ) ) |
44 |
9 12 15 18 19 43
|
uzind |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ) → ( ( 𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁 ) → 𝜏 ) ) |
45 |
44
|
expcomd |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ) → ( 𝐾 ≤ 𝑁 → ( 𝑁 ∈ ℤ → 𝜏 ) ) ) |
46 |
45
|
3expb |
⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ) ) → ( 𝐾 ≤ 𝑁 → ( 𝑁 ∈ ℤ → 𝜏 ) ) ) |
47 |
46
|
expcom |
⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ) → ( 𝑀 ∈ ℤ → ( 𝐾 ≤ 𝑁 → ( 𝑁 ∈ ℤ → 𝜏 ) ) ) ) |
48 |
47
|
com23 |
⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ) → ( 𝐾 ≤ 𝑁 → ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ℤ → 𝜏 ) ) ) ) |
49 |
48
|
3impia |
⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) → ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ℤ → 𝜏 ) ) ) |
50 |
49
|
impd |
⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝜏 ) ) |
51 |
50
|
impcom |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) → 𝜏 ) |