Step |
Hyp |
Ref |
Expression |
1 |
|
uzind2.1 |
⊢ ( 𝑗 = ( 𝑀 + 1 ) → ( 𝜑 ↔ 𝜓 ) ) |
2 |
|
uzind2.2 |
⊢ ( 𝑗 = 𝑘 → ( 𝜑 ↔ 𝜒 ) ) |
3 |
|
uzind2.3 |
⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝜑 ↔ 𝜃 ) ) |
4 |
|
uzind2.4 |
⊢ ( 𝑗 = 𝑁 → ( 𝜑 ↔ 𝜏 ) ) |
5 |
|
uzind2.5 |
⊢ ( 𝑀 ∈ ℤ → 𝜓 ) |
6 |
|
uzind2.6 |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀 < 𝑘 ) → ( 𝜒 → 𝜃 ) ) |
7 |
|
zltp1le |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 < 𝑁 ↔ ( 𝑀 + 1 ) ≤ 𝑁 ) ) |
8 |
|
peano2z |
⊢ ( 𝑀 ∈ ℤ → ( 𝑀 + 1 ) ∈ ℤ ) |
9 |
1
|
imbi2d |
⊢ ( 𝑗 = ( 𝑀 + 1 ) → ( ( 𝑀 ∈ ℤ → 𝜑 ) ↔ ( 𝑀 ∈ ℤ → 𝜓 ) ) ) |
10 |
2
|
imbi2d |
⊢ ( 𝑗 = 𝑘 → ( ( 𝑀 ∈ ℤ → 𝜑 ) ↔ ( 𝑀 ∈ ℤ → 𝜒 ) ) ) |
11 |
3
|
imbi2d |
⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝑀 ∈ ℤ → 𝜑 ) ↔ ( 𝑀 ∈ ℤ → 𝜃 ) ) ) |
12 |
4
|
imbi2d |
⊢ ( 𝑗 = 𝑁 → ( ( 𝑀 ∈ ℤ → 𝜑 ) ↔ ( 𝑀 ∈ ℤ → 𝜏 ) ) ) |
13 |
5
|
a1i |
⊢ ( ( 𝑀 + 1 ) ∈ ℤ → ( 𝑀 ∈ ℤ → 𝜓 ) ) |
14 |
|
zltp1le |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑀 < 𝑘 ↔ ( 𝑀 + 1 ) ≤ 𝑘 ) ) |
15 |
6
|
3expia |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑀 < 𝑘 → ( 𝜒 → 𝜃 ) ) ) |
16 |
14 15
|
sylbird |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑀 + 1 ) ≤ 𝑘 → ( 𝜒 → 𝜃 ) ) ) |
17 |
16
|
ex |
⊢ ( 𝑀 ∈ ℤ → ( 𝑘 ∈ ℤ → ( ( 𝑀 + 1 ) ≤ 𝑘 → ( 𝜒 → 𝜃 ) ) ) ) |
18 |
17
|
com3l |
⊢ ( 𝑘 ∈ ℤ → ( ( 𝑀 + 1 ) ≤ 𝑘 → ( 𝑀 ∈ ℤ → ( 𝜒 → 𝜃 ) ) ) ) |
19 |
18
|
imp |
⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑘 ) → ( 𝑀 ∈ ℤ → ( 𝜒 → 𝜃 ) ) ) |
20 |
19
|
3adant1 |
⊢ ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑘 ) → ( 𝑀 ∈ ℤ → ( 𝜒 → 𝜃 ) ) ) |
21 |
20
|
a2d |
⊢ ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑘 ) → ( ( 𝑀 ∈ ℤ → 𝜒 ) → ( 𝑀 ∈ ℤ → 𝜃 ) ) ) |
22 |
9 10 11 12 13 21
|
uzind |
⊢ ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) → ( 𝑀 ∈ ℤ → 𝜏 ) ) |
23 |
22
|
3exp |
⊢ ( ( 𝑀 + 1 ) ∈ ℤ → ( 𝑁 ∈ ℤ → ( ( 𝑀 + 1 ) ≤ 𝑁 → ( 𝑀 ∈ ℤ → 𝜏 ) ) ) ) |
24 |
8 23
|
syl |
⊢ ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ℤ → ( ( 𝑀 + 1 ) ≤ 𝑁 → ( 𝑀 ∈ ℤ → 𝜏 ) ) ) ) |
25 |
24
|
com34 |
⊢ ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ℤ → ( 𝑀 ∈ ℤ → ( ( 𝑀 + 1 ) ≤ 𝑁 → 𝜏 ) ) ) ) |
26 |
25
|
pm2.43a |
⊢ ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ℤ → ( ( 𝑀 + 1 ) ≤ 𝑁 → 𝜏 ) ) ) |
27 |
26
|
imp |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 + 1 ) ≤ 𝑁 → 𝜏 ) ) |
28 |
7 27
|
sylbid |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 < 𝑁 → 𝜏 ) ) |
29 |
28
|
3impia |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) → 𝜏 ) |