| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | id 22 | . . . . . 6
⊢ (𝑀 ∈ ℤs
→ 𝑀 ∈
ℤs) | 
| 2 |  | zno 28368 | . . . . . . . . 9
⊢ (𝑀 ∈ ℤs
→ 𝑀 ∈  No ) | 
| 3 |  | slerflex 27808 | . . . . . . . . 9
⊢ (𝑀 ∈ 
No  → 𝑀 ≤s
𝑀) | 
| 4 | 2, 3 | syl 17 | . . . . . . . 8
⊢ (𝑀 ∈ ℤs
→ 𝑀 ≤s 𝑀) | 
| 5 |  | uzsind.5 | . . . . . . . 8
⊢ (𝑀 ∈ ℤs
→ 𝜓) | 
| 6 | 1, 4, 5 | jca32 515 | . . . . . . 7
⊢ (𝑀 ∈ ℤs
→ (𝑀 ∈
ℤs ∧ (𝑀 ≤s 𝑀 ∧ 𝜓))) | 
| 7 |  | breq2 5147 | . . . . . . . . 9
⊢ (𝑗 = 𝑀 → (𝑀 ≤s 𝑗 ↔ 𝑀 ≤s 𝑀)) | 
| 8 |  | uzsind.1 | . . . . . . . . 9
⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓)) | 
| 9 | 7, 8 | anbi12d 632 | . . . . . . . 8
⊢ (𝑗 = 𝑀 → ((𝑀 ≤s 𝑗 ∧ 𝜑) ↔ (𝑀 ≤s 𝑀 ∧ 𝜓))) | 
| 10 | 9 | elrab 3692 | . . . . . . 7
⊢ (𝑀 ∈ {𝑗 ∈ ℤs ∣ (𝑀 ≤s 𝑗 ∧ 𝜑)} ↔ (𝑀 ∈ ℤs ∧ (𝑀 ≤s 𝑀 ∧ 𝜓))) | 
| 11 | 6, 10 | sylibr 234 | . . . . . 6
⊢ (𝑀 ∈ ℤs
→ 𝑀 ∈ {𝑗 ∈ ℤs
∣ (𝑀 ≤s 𝑗 ∧ 𝜑)}) | 
| 12 |  | simpl 482 | . . . . . . . 8
⊢ ((𝑀 ∈ ℤs
∧ (𝑘 ∈
ℤs ∧ (𝑀 ≤s 𝑘 ∧ 𝜒))) → 𝑀 ∈
ℤs) | 
| 13 |  | simprl 771 | . . . . . . . 8
⊢ ((𝑀 ∈ ℤs
∧ (𝑘 ∈
ℤs ∧ (𝑀 ≤s 𝑘 ∧ 𝜒))) → 𝑘 ∈ ℤs) | 
| 14 |  | simprrl 781 | . . . . . . . 8
⊢ ((𝑀 ∈ ℤs
∧ (𝑘 ∈
ℤs ∧ (𝑀 ≤s 𝑘 ∧ 𝜒))) → 𝑀 ≤s 𝑘) | 
| 15 |  | simprrr 782 | . . . . . . . 8
⊢ ((𝑀 ∈ ℤs
∧ (𝑘 ∈
ℤs ∧ (𝑀 ≤s 𝑘 ∧ 𝜒))) → 𝜒) | 
| 16 |  | id 22 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ℤs
→ 𝑘 ∈
ℤs) | 
| 17 |  | 1zs 28377 | . . . . . . . . . . . . 13
⊢ 
1s ∈ ℤs | 
| 18 | 17 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ℤs
→ 1s ∈ ℤs) | 
| 19 | 16, 18 | zaddscld 28381 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℤs
→ (𝑘 +s
1s ) ∈ ℤs) | 
| 20 | 19 | 3ad2ant2 1135 | . . . . . . . . . 10
⊢ ((𝑀 ∈ ℤs
∧ 𝑘 ∈
ℤs ∧ 𝑀
≤s 𝑘) → (𝑘 +s 1s )
∈ ℤs) | 
| 21 | 20 | adantr 480 | . . . . . . . . 9
⊢ (((𝑀 ∈ ℤs
∧ 𝑘 ∈
ℤs ∧ 𝑀
≤s 𝑘) ∧ 𝜒) → (𝑘 +s 1s ) ∈
ℤs) | 
| 22 | 2 | 3ad2ant1 1134 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤs
∧ 𝑘 ∈
ℤs ∧ 𝑀
≤s 𝑘) → 𝑀 ∈ 
No ) | 
| 23 | 19 | znod 28369 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ℤs
→ (𝑘 +s
1s ) ∈  No ) | 
| 24 | 23 | 3ad2ant2 1135 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤs
∧ 𝑘 ∈
ℤs ∧ 𝑀
≤s 𝑘) → (𝑘 +s 1s )
∈  No ) | 
| 25 |  | zno 28368 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℤs
→ 𝑘 ∈  No ) | 
| 26 | 25 | 3ad2ant2 1135 | . . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤs
∧ 𝑘 ∈
ℤs ∧ 𝑀
≤s 𝑘) → 𝑘 ∈ 
No ) | 
| 27 |  | simp3 1139 | . . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤs
∧ 𝑘 ∈
ℤs ∧ 𝑀
≤s 𝑘) → 𝑀 ≤s 𝑘) | 
| 28 | 25 | sltp1d 28048 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℤs
→ 𝑘 <s (𝑘 +s 1s
)) | 
| 29 | 28 | 3ad2ant2 1135 | . . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤs
∧ 𝑘 ∈
ℤs ∧ 𝑀
≤s 𝑘) → 𝑘 <s (𝑘 +s 1s
)) | 
| 30 | 22, 26, 24, 27, 29 | slelttrd 27806 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤs
∧ 𝑘 ∈
ℤs ∧ 𝑀
≤s 𝑘) → 𝑀 <s (𝑘 +s 1s
)) | 
| 31 | 22, 24, 30 | sltled 27814 | . . . . . . . . . 10
⊢ ((𝑀 ∈ ℤs
∧ 𝑘 ∈
ℤs ∧ 𝑀
≤s 𝑘) → 𝑀 ≤s (𝑘 +s 1s
)) | 
| 32 | 31 | adantr 480 | . . . . . . . . 9
⊢ (((𝑀 ∈ ℤs
∧ 𝑘 ∈
ℤs ∧ 𝑀
≤s 𝑘) ∧ 𝜒) → 𝑀 ≤s (𝑘 +s 1s
)) | 
| 33 |  | uzsind.6 | . . . . . . . . . 10
⊢ ((𝑀 ∈ ℤs
∧ 𝑘 ∈
ℤs ∧ 𝑀
≤s 𝑘) → (𝜒 → 𝜃)) | 
| 34 | 33 | imp 406 | . . . . . . . . 9
⊢ (((𝑀 ∈ ℤs
∧ 𝑘 ∈
ℤs ∧ 𝑀
≤s 𝑘) ∧ 𝜒) → 𝜃) | 
| 35 | 21, 32, 34 | jca32 515 | . . . . . . . 8
⊢ (((𝑀 ∈ ℤs
∧ 𝑘 ∈
ℤs ∧ 𝑀
≤s 𝑘) ∧ 𝜒) → ((𝑘 +s 1s ) ∈
ℤs ∧ (𝑀 ≤s (𝑘 +s 1s ) ∧ 𝜃))) | 
| 36 | 12, 13, 14, 15, 35 | syl31anc 1375 | . . . . . . 7
⊢ ((𝑀 ∈ ℤs
∧ (𝑘 ∈
ℤs ∧ (𝑀 ≤s 𝑘 ∧ 𝜒))) → ((𝑘 +s 1s ) ∈
ℤs ∧ (𝑀 ≤s (𝑘 +s 1s ) ∧ 𝜃))) | 
| 37 |  | breq2 5147 | . . . . . . . . . 10
⊢ (𝑗 = 𝑘 → (𝑀 ≤s 𝑗 ↔ 𝑀 ≤s 𝑘)) | 
| 38 |  | uzsind.2 | . . . . . . . . . 10
⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒)) | 
| 39 | 37, 38 | anbi12d 632 | . . . . . . . . 9
⊢ (𝑗 = 𝑘 → ((𝑀 ≤s 𝑗 ∧ 𝜑) ↔ (𝑀 ≤s 𝑘 ∧ 𝜒))) | 
| 40 | 39 | elrab 3692 | . . . . . . . 8
⊢ (𝑘 ∈ {𝑗 ∈ ℤs ∣ (𝑀 ≤s 𝑗 ∧ 𝜑)} ↔ (𝑘 ∈ ℤs ∧ (𝑀 ≤s 𝑘 ∧ 𝜒))) | 
| 41 | 40 | anbi2i 623 | . . . . . . 7
⊢ ((𝑀 ∈ ℤs
∧ 𝑘 ∈ {𝑗 ∈ ℤs
∣ (𝑀 ≤s 𝑗 ∧ 𝜑)}) ↔ (𝑀 ∈ ℤs ∧ (𝑘 ∈ ℤs
∧ (𝑀 ≤s 𝑘 ∧ 𝜒)))) | 
| 42 |  | breq2 5147 | . . . . . . . . 9
⊢ (𝑗 = (𝑘 +s 1s ) → (𝑀 ≤s 𝑗 ↔ 𝑀 ≤s (𝑘 +s 1s
))) | 
| 43 |  | uzsind.3 | . . . . . . . . 9
⊢ (𝑗 = (𝑘 +s 1s ) → (𝜑 ↔ 𝜃)) | 
| 44 | 42, 43 | anbi12d 632 | . . . . . . . 8
⊢ (𝑗 = (𝑘 +s 1s ) → ((𝑀 ≤s 𝑗 ∧ 𝜑) ↔ (𝑀 ≤s (𝑘 +s 1s ) ∧ 𝜃))) | 
| 45 | 44 | elrab 3692 | . . . . . . 7
⊢ ((𝑘 +s 1s )
∈ {𝑗 ∈
ℤs ∣ (𝑀 ≤s 𝑗 ∧ 𝜑)} ↔ ((𝑘 +s 1s ) ∈
ℤs ∧ (𝑀 ≤s (𝑘 +s 1s ) ∧ 𝜃))) | 
| 46 | 36, 41, 45 | 3imtr4i 292 | . . . . . 6
⊢ ((𝑀 ∈ ℤs
∧ 𝑘 ∈ {𝑗 ∈ ℤs
∣ (𝑀 ≤s 𝑗 ∧ 𝜑)}) → (𝑘 +s 1s ) ∈ {𝑗 ∈ ℤs
∣ (𝑀 ≤s 𝑗 ∧ 𝜑)}) | 
| 47 | 1, 11, 46 | peano5uzs 28390 | . . . . 5
⊢ (𝑀 ∈ ℤs
→ {𝑤 ∈
ℤs ∣ 𝑀 ≤s 𝑤} ⊆ {𝑗 ∈ ℤs ∣ (𝑀 ≤s 𝑗 ∧ 𝜑)}) | 
| 48 | 47 | sseld 3982 | . . . 4
⊢ (𝑀 ∈ ℤs
→ (𝑁 ∈ {𝑤 ∈ ℤs
∣ 𝑀 ≤s 𝑤} → 𝑁 ∈ {𝑗 ∈ ℤs ∣ (𝑀 ≤s 𝑗 ∧ 𝜑)})) | 
| 49 |  | breq2 5147 | . . . . 5
⊢ (𝑤 = 𝑁 → (𝑀 ≤s 𝑤 ↔ 𝑀 ≤s 𝑁)) | 
| 50 | 49 | elrab 3692 | . . . 4
⊢ (𝑁 ∈ {𝑤 ∈ ℤs ∣ 𝑀 ≤s 𝑤} ↔ (𝑁 ∈ ℤs ∧ 𝑀 ≤s 𝑁)) | 
| 51 |  | breq2 5147 | . . . . . 6
⊢ (𝑗 = 𝑁 → (𝑀 ≤s 𝑗 ↔ 𝑀 ≤s 𝑁)) | 
| 52 |  | uzsind.4 | . . . . . 6
⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏)) | 
| 53 | 51, 52 | anbi12d 632 | . . . . 5
⊢ (𝑗 = 𝑁 → ((𝑀 ≤s 𝑗 ∧ 𝜑) ↔ (𝑀 ≤s 𝑁 ∧ 𝜏))) | 
| 54 | 53 | elrab 3692 | . . . 4
⊢ (𝑁 ∈ {𝑗 ∈ ℤs ∣ (𝑀 ≤s 𝑗 ∧ 𝜑)} ↔ (𝑁 ∈ ℤs ∧ (𝑀 ≤s 𝑁 ∧ 𝜏))) | 
| 55 | 48, 50, 54 | 3imtr3g 295 | . . 3
⊢ (𝑀 ∈ ℤs
→ ((𝑁 ∈
ℤs ∧ 𝑀
≤s 𝑁) → (𝑁 ∈ ℤs
∧ (𝑀 ≤s 𝑁 ∧ 𝜏)))) | 
| 56 | 55 | 3impib 1117 | . 2
⊢ ((𝑀 ∈ ℤs
∧ 𝑁 ∈
ℤs ∧ 𝑀
≤s 𝑁) → (𝑁 ∈ ℤs
∧ (𝑀 ≤s 𝑁 ∧ 𝜏))) | 
| 57 | 56 | simprrd 774 | 1
⊢ ((𝑀 ∈ ℤs
∧ 𝑁 ∈
ℤs ∧ 𝑀
≤s 𝑁) → 𝜏) |