| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | zre 12617 | . . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) | 
| 2 | 1 | leidd 11829 | . . . . . . . . 9
⊢ (𝑀 ∈ ℤ → 𝑀 ≤ 𝑀) | 
| 3 |  | uzind.5 | . . . . . . . . 9
⊢ (𝑀 ∈ ℤ → 𝜓) | 
| 4 | 2, 3 | jca 511 | . . . . . . . 8
⊢ (𝑀 ∈ ℤ → (𝑀 ≤ 𝑀 ∧ 𝜓)) | 
| 5 | 4 | ancli 548 | . . . . . . 7
⊢ (𝑀 ∈ ℤ → (𝑀 ∈ ℤ ∧ (𝑀 ≤ 𝑀 ∧ 𝜓))) | 
| 6 |  | breq2 5147 | . . . . . . . . 9
⊢ (𝑗 = 𝑀 → (𝑀 ≤ 𝑗 ↔ 𝑀 ≤ 𝑀)) | 
| 7 |  | uzind.1 | . . . . . . . . 9
⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓)) | 
| 8 | 6, 7 | anbi12d 632 | . . . . . . . 8
⊢ (𝑗 = 𝑀 → ((𝑀 ≤ 𝑗 ∧ 𝜑) ↔ (𝑀 ≤ 𝑀 ∧ 𝜓))) | 
| 9 | 8 | elrab 3692 | . . . . . . 7
⊢ (𝑀 ∈ {𝑗 ∈ ℤ ∣ (𝑀 ≤ 𝑗 ∧ 𝜑)} ↔ (𝑀 ∈ ℤ ∧ (𝑀 ≤ 𝑀 ∧ 𝜓))) | 
| 10 | 5, 9 | sylibr 234 | . . . . . 6
⊢ (𝑀 ∈ ℤ → 𝑀 ∈ {𝑗 ∈ ℤ ∣ (𝑀 ≤ 𝑗 ∧ 𝜑)}) | 
| 11 |  | peano2z 12658 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℤ → (𝑘 + 1) ∈
ℤ) | 
| 12 | 11 | a1i 11 | . . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → (𝑘 ∈ ℤ → (𝑘 + 1) ∈
ℤ)) | 
| 13 | 12 | adantrd 491 | . . . . . . . . 9
⊢ (𝑀 ∈ ℤ → ((𝑘 ∈ ℤ ∧ (𝑀 ≤ 𝑘 ∧ 𝜒)) → (𝑘 + 1) ∈ ℤ)) | 
| 14 |  | zre 12617 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℤ → 𝑘 ∈
ℝ) | 
| 15 |  | ltp1 12107 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℝ → 𝑘 < (𝑘 + 1)) | 
| 16 | 15 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ) → 𝑘 < (𝑘 + 1)) | 
| 17 |  | peano2re 11434 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈
ℝ) | 
| 18 | 17 | ancli 548 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℝ → (𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈
ℝ)) | 
| 19 |  | lelttr 11351 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ) →
((𝑀 ≤ 𝑘 ∧ 𝑘 < (𝑘 + 1)) → 𝑀 < (𝑘 + 1))) | 
| 20 | 19 | 3expb 1121 | . . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℝ ∧ (𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ)) →
((𝑀 ≤ 𝑘 ∧ 𝑘 < (𝑘 + 1)) → 𝑀 < (𝑘 + 1))) | 
| 21 | 18, 20 | sylan2 593 | . . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ) → ((𝑀 ≤ 𝑘 ∧ 𝑘 < (𝑘 + 1)) → 𝑀 < (𝑘 + 1))) | 
| 22 | 16, 21 | mpan2d 694 | . . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (𝑀 ≤ 𝑘 → 𝑀 < (𝑘 + 1))) | 
| 23 |  | ltle 11349 | . . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ) →
(𝑀 < (𝑘 + 1) → 𝑀 ≤ (𝑘 + 1))) | 
| 24 | 17, 23 | sylan2 593 | . . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (𝑀 < (𝑘 + 1) → 𝑀 ≤ (𝑘 + 1))) | 
| 25 | 22, 24 | syld 47 | . . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (𝑀 ≤ 𝑘 → 𝑀 ≤ (𝑘 + 1))) | 
| 26 | 1, 14, 25 | syl2an 596 | . . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑀 ≤ 𝑘 → 𝑀 ≤ (𝑘 + 1))) | 
| 27 | 26 | adantrd 491 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑀 ≤ 𝑘 ∧ 𝜒) → 𝑀 ≤ (𝑘 + 1))) | 
| 28 | 27 | expimpd 453 | . . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → ((𝑘 ∈ ℤ ∧ (𝑀 ≤ 𝑘 ∧ 𝜒)) → 𝑀 ≤ (𝑘 + 1))) | 
| 29 |  | uzind.6 | . . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘) → (𝜒 → 𝜃)) | 
| 30 | 29 | 3exp 1120 | . . . . . . . . . . 11
⊢ (𝑀 ∈ ℤ → (𝑘 ∈ ℤ → (𝑀 ≤ 𝑘 → (𝜒 → 𝜃)))) | 
| 31 | 30 | imp4d 424 | . . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → ((𝑘 ∈ ℤ ∧ (𝑀 ≤ 𝑘 ∧ 𝜒)) → 𝜃)) | 
| 32 | 28, 31 | jcad 512 | . . . . . . . . 9
⊢ (𝑀 ∈ ℤ → ((𝑘 ∈ ℤ ∧ (𝑀 ≤ 𝑘 ∧ 𝜒)) → (𝑀 ≤ (𝑘 + 1) ∧ 𝜃))) | 
| 33 | 13, 32 | jcad 512 | . . . . . . . 8
⊢ (𝑀 ∈ ℤ → ((𝑘 ∈ ℤ ∧ (𝑀 ≤ 𝑘 ∧ 𝜒)) → ((𝑘 + 1) ∈ ℤ ∧ (𝑀 ≤ (𝑘 + 1) ∧ 𝜃)))) | 
| 34 |  | breq2 5147 | . . . . . . . . . 10
⊢ (𝑗 = 𝑘 → (𝑀 ≤ 𝑗 ↔ 𝑀 ≤ 𝑘)) | 
| 35 |  | uzind.2 | . . . . . . . . . 10
⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒)) | 
| 36 | 34, 35 | anbi12d 632 | . . . . . . . . 9
⊢ (𝑗 = 𝑘 → ((𝑀 ≤ 𝑗 ∧ 𝜑) ↔ (𝑀 ≤ 𝑘 ∧ 𝜒))) | 
| 37 | 36 | elrab 3692 | . . . . . . . 8
⊢ (𝑘 ∈ {𝑗 ∈ ℤ ∣ (𝑀 ≤ 𝑗 ∧ 𝜑)} ↔ (𝑘 ∈ ℤ ∧ (𝑀 ≤ 𝑘 ∧ 𝜒))) | 
| 38 |  | breq2 5147 | . . . . . . . . . 10
⊢ (𝑗 = (𝑘 + 1) → (𝑀 ≤ 𝑗 ↔ 𝑀 ≤ (𝑘 + 1))) | 
| 39 |  | uzind.3 | . . . . . . . . . 10
⊢ (𝑗 = (𝑘 + 1) → (𝜑 ↔ 𝜃)) | 
| 40 | 38, 39 | anbi12d 632 | . . . . . . . . 9
⊢ (𝑗 = (𝑘 + 1) → ((𝑀 ≤ 𝑗 ∧ 𝜑) ↔ (𝑀 ≤ (𝑘 + 1) ∧ 𝜃))) | 
| 41 | 40 | elrab 3692 | . . . . . . . 8
⊢ ((𝑘 + 1) ∈ {𝑗 ∈ ℤ ∣ (𝑀 ≤ 𝑗 ∧ 𝜑)} ↔ ((𝑘 + 1) ∈ ℤ ∧ (𝑀 ≤ (𝑘 + 1) ∧ 𝜃))) | 
| 42 | 33, 37, 41 | 3imtr4g 296 | . . . . . . 7
⊢ (𝑀 ∈ ℤ → (𝑘 ∈ {𝑗 ∈ ℤ ∣ (𝑀 ≤ 𝑗 ∧ 𝜑)} → (𝑘 + 1) ∈ {𝑗 ∈ ℤ ∣ (𝑀 ≤ 𝑗 ∧ 𝜑)})) | 
| 43 | 42 | ralrimiv 3145 | . . . . . 6
⊢ (𝑀 ∈ ℤ →
∀𝑘 ∈ {𝑗 ∈ ℤ ∣ (𝑀 ≤ 𝑗 ∧ 𝜑)} (𝑘 + 1) ∈ {𝑗 ∈ ℤ ∣ (𝑀 ≤ 𝑗 ∧ 𝜑)}) | 
| 44 |  | peano5uzti 12708 | . . . . . 6
⊢ (𝑀 ∈ ℤ → ((𝑀 ∈ {𝑗 ∈ ℤ ∣ (𝑀 ≤ 𝑗 ∧ 𝜑)} ∧ ∀𝑘 ∈ {𝑗 ∈ ℤ ∣ (𝑀 ≤ 𝑗 ∧ 𝜑)} (𝑘 + 1) ∈ {𝑗 ∈ ℤ ∣ (𝑀 ≤ 𝑗 ∧ 𝜑)}) → {𝑤 ∈ ℤ ∣ 𝑀 ≤ 𝑤} ⊆ {𝑗 ∈ ℤ ∣ (𝑀 ≤ 𝑗 ∧ 𝜑)})) | 
| 45 | 10, 43, 44 | mp2and 699 | . . . . 5
⊢ (𝑀 ∈ ℤ → {𝑤 ∈ ℤ ∣ 𝑀 ≤ 𝑤} ⊆ {𝑗 ∈ ℤ ∣ (𝑀 ≤ 𝑗 ∧ 𝜑)}) | 
| 46 | 45 | sseld 3982 | . . . 4
⊢ (𝑀 ∈ ℤ → (𝑁 ∈ {𝑤 ∈ ℤ ∣ 𝑀 ≤ 𝑤} → 𝑁 ∈ {𝑗 ∈ ℤ ∣ (𝑀 ≤ 𝑗 ∧ 𝜑)})) | 
| 47 |  | breq2 5147 | . . . . 5
⊢ (𝑤 = 𝑁 → (𝑀 ≤ 𝑤 ↔ 𝑀 ≤ 𝑁)) | 
| 48 | 47 | elrab 3692 | . . . 4
⊢ (𝑁 ∈ {𝑤 ∈ ℤ ∣ 𝑀 ≤ 𝑤} ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) | 
| 49 |  | breq2 5147 | . . . . . 6
⊢ (𝑗 = 𝑁 → (𝑀 ≤ 𝑗 ↔ 𝑀 ≤ 𝑁)) | 
| 50 |  | uzind.4 | . . . . . 6
⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏)) | 
| 51 | 49, 50 | anbi12d 632 | . . . . 5
⊢ (𝑗 = 𝑁 → ((𝑀 ≤ 𝑗 ∧ 𝜑) ↔ (𝑀 ≤ 𝑁 ∧ 𝜏))) | 
| 52 | 51 | elrab 3692 | . . . 4
⊢ (𝑁 ∈ {𝑗 ∈ ℤ ∣ (𝑀 ≤ 𝑗 ∧ 𝜑)} ↔ (𝑁 ∈ ℤ ∧ (𝑀 ≤ 𝑁 ∧ 𝜏))) | 
| 53 | 46, 48, 52 | 3imtr3g 295 | . . 3
⊢ (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → (𝑁 ∈ ℤ ∧ (𝑀 ≤ 𝑁 ∧ 𝜏)))) | 
| 54 | 53 | 3impib 1117 | . 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → (𝑁 ∈ ℤ ∧ (𝑀 ≤ 𝑁 ∧ 𝜏))) | 
| 55 | 54 | simprrd 774 | 1
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝜏) |