Step |
Hyp |
Ref |
Expression |
1 |
|
uzind.1 |
⊢ ( 𝑗 = 𝑀 → ( 𝜑 ↔ 𝜓 ) ) |
2 |
|
uzind.2 |
⊢ ( 𝑗 = 𝑘 → ( 𝜑 ↔ 𝜒 ) ) |
3 |
|
uzind.3 |
⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝜑 ↔ 𝜃 ) ) |
4 |
|
uzind.4 |
⊢ ( 𝑗 = 𝑁 → ( 𝜑 ↔ 𝜏 ) ) |
5 |
|
uzind.5 |
⊢ ( 𝑀 ∈ ℤ → 𝜓 ) |
6 |
|
uzind.6 |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) → ( 𝜒 → 𝜃 ) ) |
7 |
|
zre |
⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ ) |
8 |
7
|
leidd |
⊢ ( 𝑀 ∈ ℤ → 𝑀 ≤ 𝑀 ) |
9 |
8 5
|
jca |
⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ≤ 𝑀 ∧ 𝜓 ) ) |
10 |
9
|
ancli |
⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ∈ ℤ ∧ ( 𝑀 ≤ 𝑀 ∧ 𝜓 ) ) ) |
11 |
|
breq2 |
⊢ ( 𝑗 = 𝑀 → ( 𝑀 ≤ 𝑗 ↔ 𝑀 ≤ 𝑀 ) ) |
12 |
11 1
|
anbi12d |
⊢ ( 𝑗 = 𝑀 → ( ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) ↔ ( 𝑀 ≤ 𝑀 ∧ 𝜓 ) ) ) |
13 |
12
|
elrab |
⊢ ( 𝑀 ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) } ↔ ( 𝑀 ∈ ℤ ∧ ( 𝑀 ≤ 𝑀 ∧ 𝜓 ) ) ) |
14 |
10 13
|
sylibr |
⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) } ) |
15 |
|
peano2z |
⊢ ( 𝑘 ∈ ℤ → ( 𝑘 + 1 ) ∈ ℤ ) |
16 |
15
|
a1i |
⊢ ( 𝑀 ∈ ℤ → ( 𝑘 ∈ ℤ → ( 𝑘 + 1 ) ∈ ℤ ) ) |
17 |
16
|
adantrd |
⊢ ( 𝑀 ∈ ℤ → ( ( 𝑘 ∈ ℤ ∧ ( 𝑀 ≤ 𝑘 ∧ 𝜒 ) ) → ( 𝑘 + 1 ) ∈ ℤ ) ) |
18 |
|
zre |
⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℝ ) |
19 |
|
ltp1 |
⊢ ( 𝑘 ∈ ℝ → 𝑘 < ( 𝑘 + 1 ) ) |
20 |
19
|
adantl |
⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → 𝑘 < ( 𝑘 + 1 ) ) |
21 |
|
peano2re |
⊢ ( 𝑘 ∈ ℝ → ( 𝑘 + 1 ) ∈ ℝ ) |
22 |
21
|
ancli |
⊢ ( 𝑘 ∈ ℝ → ( 𝑘 ∈ ℝ ∧ ( 𝑘 + 1 ) ∈ ℝ ) ) |
23 |
|
lelttr |
⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ ( 𝑘 + 1 ) ∈ ℝ ) → ( ( 𝑀 ≤ 𝑘 ∧ 𝑘 < ( 𝑘 + 1 ) ) → 𝑀 < ( 𝑘 + 1 ) ) ) |
24 |
23
|
3expb |
⊢ ( ( 𝑀 ∈ ℝ ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 + 1 ) ∈ ℝ ) ) → ( ( 𝑀 ≤ 𝑘 ∧ 𝑘 < ( 𝑘 + 1 ) ) → 𝑀 < ( 𝑘 + 1 ) ) ) |
25 |
22 24
|
sylan2 |
⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( ( 𝑀 ≤ 𝑘 ∧ 𝑘 < ( 𝑘 + 1 ) ) → 𝑀 < ( 𝑘 + 1 ) ) ) |
26 |
20 25
|
mpan2d |
⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝑀 ≤ 𝑘 → 𝑀 < ( 𝑘 + 1 ) ) ) |
27 |
|
ltle |
⊢ ( ( 𝑀 ∈ ℝ ∧ ( 𝑘 + 1 ) ∈ ℝ ) → ( 𝑀 < ( 𝑘 + 1 ) → 𝑀 ≤ ( 𝑘 + 1 ) ) ) |
28 |
21 27
|
sylan2 |
⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝑀 < ( 𝑘 + 1 ) → 𝑀 ≤ ( 𝑘 + 1 ) ) ) |
29 |
26 28
|
syld |
⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝑀 ≤ 𝑘 → 𝑀 ≤ ( 𝑘 + 1 ) ) ) |
30 |
7 18 29
|
syl2an |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑀 ≤ 𝑘 → 𝑀 ≤ ( 𝑘 + 1 ) ) ) |
31 |
30
|
adantrd |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑀 ≤ 𝑘 ∧ 𝜒 ) → 𝑀 ≤ ( 𝑘 + 1 ) ) ) |
32 |
31
|
expimpd |
⊢ ( 𝑀 ∈ ℤ → ( ( 𝑘 ∈ ℤ ∧ ( 𝑀 ≤ 𝑘 ∧ 𝜒 ) ) → 𝑀 ≤ ( 𝑘 + 1 ) ) ) |
33 |
6
|
3exp |
⊢ ( 𝑀 ∈ ℤ → ( 𝑘 ∈ ℤ → ( 𝑀 ≤ 𝑘 → ( 𝜒 → 𝜃 ) ) ) ) |
34 |
33
|
imp4d |
⊢ ( 𝑀 ∈ ℤ → ( ( 𝑘 ∈ ℤ ∧ ( 𝑀 ≤ 𝑘 ∧ 𝜒 ) ) → 𝜃 ) ) |
35 |
32 34
|
jcad |
⊢ ( 𝑀 ∈ ℤ → ( ( 𝑘 ∈ ℤ ∧ ( 𝑀 ≤ 𝑘 ∧ 𝜒 ) ) → ( 𝑀 ≤ ( 𝑘 + 1 ) ∧ 𝜃 ) ) ) |
36 |
17 35
|
jcad |
⊢ ( 𝑀 ∈ ℤ → ( ( 𝑘 ∈ ℤ ∧ ( 𝑀 ≤ 𝑘 ∧ 𝜒 ) ) → ( ( 𝑘 + 1 ) ∈ ℤ ∧ ( 𝑀 ≤ ( 𝑘 + 1 ) ∧ 𝜃 ) ) ) ) |
37 |
|
breq2 |
⊢ ( 𝑗 = 𝑘 → ( 𝑀 ≤ 𝑗 ↔ 𝑀 ≤ 𝑘 ) ) |
38 |
37 2
|
anbi12d |
⊢ ( 𝑗 = 𝑘 → ( ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) ↔ ( 𝑀 ≤ 𝑘 ∧ 𝜒 ) ) ) |
39 |
38
|
elrab |
⊢ ( 𝑘 ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) } ↔ ( 𝑘 ∈ ℤ ∧ ( 𝑀 ≤ 𝑘 ∧ 𝜒 ) ) ) |
40 |
|
breq2 |
⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝑀 ≤ 𝑗 ↔ 𝑀 ≤ ( 𝑘 + 1 ) ) ) |
41 |
40 3
|
anbi12d |
⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) ↔ ( 𝑀 ≤ ( 𝑘 + 1 ) ∧ 𝜃 ) ) ) |
42 |
41
|
elrab |
⊢ ( ( 𝑘 + 1 ) ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) } ↔ ( ( 𝑘 + 1 ) ∈ ℤ ∧ ( 𝑀 ≤ ( 𝑘 + 1 ) ∧ 𝜃 ) ) ) |
43 |
36 39 42
|
3imtr4g |
⊢ ( 𝑀 ∈ ℤ → ( 𝑘 ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) } → ( 𝑘 + 1 ) ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) } ) ) |
44 |
43
|
ralrimiv |
⊢ ( 𝑀 ∈ ℤ → ∀ 𝑘 ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) } ( 𝑘 + 1 ) ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) } ) |
45 |
|
peano5uzti |
⊢ ( 𝑀 ∈ ℤ → ( ( 𝑀 ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) } ∧ ∀ 𝑘 ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) } ( 𝑘 + 1 ) ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) } ) → { 𝑤 ∈ ℤ ∣ 𝑀 ≤ 𝑤 } ⊆ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) } ) ) |
46 |
14 44 45
|
mp2and |
⊢ ( 𝑀 ∈ ℤ → { 𝑤 ∈ ℤ ∣ 𝑀 ≤ 𝑤 } ⊆ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) } ) |
47 |
46
|
sseld |
⊢ ( 𝑀 ∈ ℤ → ( 𝑁 ∈ { 𝑤 ∈ ℤ ∣ 𝑀 ≤ 𝑤 } → 𝑁 ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) } ) ) |
48 |
|
breq2 |
⊢ ( 𝑤 = 𝑁 → ( 𝑀 ≤ 𝑤 ↔ 𝑀 ≤ 𝑁 ) ) |
49 |
48
|
elrab |
⊢ ( 𝑁 ∈ { 𝑤 ∈ ℤ ∣ 𝑀 ≤ 𝑤 } ↔ ( 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) ) |
50 |
|
breq2 |
⊢ ( 𝑗 = 𝑁 → ( 𝑀 ≤ 𝑗 ↔ 𝑀 ≤ 𝑁 ) ) |
51 |
50 4
|
anbi12d |
⊢ ( 𝑗 = 𝑁 → ( ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) ↔ ( 𝑀 ≤ 𝑁 ∧ 𝜏 ) ) ) |
52 |
51
|
elrab |
⊢ ( 𝑁 ∈ { 𝑗 ∈ ℤ ∣ ( 𝑀 ≤ 𝑗 ∧ 𝜑 ) } ↔ ( 𝑁 ∈ ℤ ∧ ( 𝑀 ≤ 𝑁 ∧ 𝜏 ) ) ) |
53 |
47 49 52
|
3imtr3g |
⊢ ( 𝑀 ∈ ℤ → ( ( 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → ( 𝑁 ∈ ℤ ∧ ( 𝑀 ≤ 𝑁 ∧ 𝜏 ) ) ) ) |
54 |
53
|
3impib |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → ( 𝑁 ∈ ℤ ∧ ( 𝑀 ≤ 𝑁 ∧ 𝜏 ) ) ) |
55 |
54
|
simprrd |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → 𝜏 ) |