Proof of Theorem fzind
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | breq1 5146 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑀 → (𝑥 ≤ 𝑁 ↔ 𝑀 ≤ 𝑁)) | 
| 2 | 1 | anbi2d 630 | . . . . . . . . . 10
⊢ (𝑥 = 𝑀 → ((𝑁 ∈ ℤ ∧ 𝑥 ≤ 𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))) | 
| 3 |  | fzind.1 | . . . . . . . . . 10
⊢ (𝑥 = 𝑀 → (𝜑 ↔ 𝜓)) | 
| 4 | 2, 3 | imbi12d 344 | . . . . . . . . 9
⊢ (𝑥 = 𝑀 → (((𝑁 ∈ ℤ ∧ 𝑥 ≤ 𝑁) → 𝜑) ↔ ((𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝜓))) | 
| 5 |  | breq1 5146 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑥 ≤ 𝑁 ↔ 𝑦 ≤ 𝑁)) | 
| 6 | 5 | anbi2d 630 | . . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝑁 ∈ ℤ ∧ 𝑥 ≤ 𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝑦 ≤ 𝑁))) | 
| 7 |  | fzind.2 | . . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) | 
| 8 | 6, 7 | imbi12d 344 | . . . . . . . . 9
⊢ (𝑥 = 𝑦 → (((𝑁 ∈ ℤ ∧ 𝑥 ≤ 𝑁) → 𝜑) ↔ ((𝑁 ∈ ℤ ∧ 𝑦 ≤ 𝑁) → 𝜒))) | 
| 9 |  | breq1 5146 | . . . . . . . . . . 11
⊢ (𝑥 = (𝑦 + 1) → (𝑥 ≤ 𝑁 ↔ (𝑦 + 1) ≤ 𝑁)) | 
| 10 | 9 | anbi2d 630 | . . . . . . . . . 10
⊢ (𝑥 = (𝑦 + 1) → ((𝑁 ∈ ℤ ∧ 𝑥 ≤ 𝑁) ↔ (𝑁 ∈ ℤ ∧ (𝑦 + 1) ≤ 𝑁))) | 
| 11 |  | fzind.3 | . . . . . . . . . 10
⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃)) | 
| 12 | 10, 11 | imbi12d 344 | . . . . . . . . 9
⊢ (𝑥 = (𝑦 + 1) → (((𝑁 ∈ ℤ ∧ 𝑥 ≤ 𝑁) → 𝜑) ↔ ((𝑁 ∈ ℤ ∧ (𝑦 + 1) ≤ 𝑁) → 𝜃))) | 
| 13 |  | breq1 5146 | . . . . . . . . . . 11
⊢ (𝑥 = 𝐾 → (𝑥 ≤ 𝑁 ↔ 𝐾 ≤ 𝑁)) | 
| 14 | 13 | anbi2d 630 | . . . . . . . . . 10
⊢ (𝑥 = 𝐾 → ((𝑁 ∈ ℤ ∧ 𝑥 ≤ 𝑁) ↔ (𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁))) | 
| 15 |  | fzind.4 | . . . . . . . . . 10
⊢ (𝑥 = 𝐾 → (𝜑 ↔ 𝜏)) | 
| 16 | 14, 15 | imbi12d 344 | . . . . . . . . 9
⊢ (𝑥 = 𝐾 → (((𝑁 ∈ ℤ ∧ 𝑥 ≤ 𝑁) → 𝜑) ↔ ((𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁) → 𝜏))) | 
| 17 |  | fzind.5 | . . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝜓) | 
| 18 | 17 | 3expib 1123 | . . . . . . . . 9
⊢ (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝜓)) | 
| 19 |  | zre 12617 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℝ) | 
| 20 |  | zre 12617 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) | 
| 21 |  | p1le 12112 | . . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑦 + 1) ≤ 𝑁) → 𝑦 ≤ 𝑁) | 
| 22 | 21 | 3expia 1122 | . . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑦 + 1) ≤ 𝑁 → 𝑦 ≤ 𝑁)) | 
| 23 | 19, 20, 22 | syl2an 596 | . . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑦 + 1) ≤ 𝑁 → 𝑦 ≤ 𝑁)) | 
| 24 | 23 | imdistanda 571 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ ℤ → ((𝑁 ∈ ℤ ∧ (𝑦 + 1) ≤ 𝑁) → (𝑁 ∈ ℤ ∧ 𝑦 ≤ 𝑁))) | 
| 25 | 24 | imim1d 82 | . . . . . . . . . . 11
⊢ (𝑦 ∈ ℤ → (((𝑁 ∈ ℤ ∧ 𝑦 ≤ 𝑁) → 𝜒) → ((𝑁 ∈ ℤ ∧ (𝑦 + 1) ≤ 𝑁) → 𝜒))) | 
| 26 | 25 | 3ad2ant2 1135 | . . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦) → (((𝑁 ∈ ℤ ∧ 𝑦 ≤ 𝑁) → 𝜒) → ((𝑁 ∈ ℤ ∧ (𝑦 + 1) ≤ 𝑁) → 𝜒))) | 
| 27 |  | zltp1le 12667 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑦 < 𝑁 ↔ (𝑦 + 1) ≤ 𝑁)) | 
| 28 | 27 | adantlr 715 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦) ∧ 𝑁 ∈ ℤ) → (𝑦 < 𝑁 ↔ (𝑦 + 1) ≤ 𝑁)) | 
| 29 | 28 | expcom 413 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℤ → ((𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦) → (𝑦 < 𝑁 ↔ (𝑦 + 1) ≤ 𝑁))) | 
| 30 | 29 | pm5.32d 577 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℤ → (((𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦) ∧ 𝑦 < 𝑁) ↔ ((𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦) ∧ (𝑦 + 1) ≤ 𝑁))) | 
| 31 | 30 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦) ∧ 𝑦 < 𝑁) ↔ ((𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦) ∧ (𝑦 + 1) ≤ 𝑁))) | 
| 32 |  | fzind.6 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁)) → (𝜒 → 𝜃)) | 
| 33 | 32 | expcom 413 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝜒 → 𝜃))) | 
| 34 | 33 | 3expa 1119 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦) ∧ 𝑦 < 𝑁) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝜒 → 𝜃))) | 
| 35 | 34 | com12 32 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦) ∧ 𝑦 < 𝑁) → (𝜒 → 𝜃))) | 
| 36 | 31, 35 | sylbird 260 | . . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦) ∧ (𝑦 + 1) ≤ 𝑁) → (𝜒 → 𝜃))) | 
| 37 | 36 | ex 412 | . . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℤ → (𝑁 ∈ ℤ → (((𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦) ∧ (𝑦 + 1) ≤ 𝑁) → (𝜒 → 𝜃)))) | 
| 38 | 37 | com23 86 | . . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℤ → (((𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦) ∧ (𝑦 + 1) ≤ 𝑁) → (𝑁 ∈ ℤ → (𝜒 → 𝜃)))) | 
| 39 | 38 | expd 415 | . . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℤ → ((𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦) → ((𝑦 + 1) ≤ 𝑁 → (𝑁 ∈ ℤ → (𝜒 → 𝜃))))) | 
| 40 | 39 | 3impib 1117 | . . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦) → ((𝑦 + 1) ≤ 𝑁 → (𝑁 ∈ ℤ → (𝜒 → 𝜃)))) | 
| 41 | 40 | impcomd 411 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦) → ((𝑁 ∈ ℤ ∧ (𝑦 + 1) ≤ 𝑁) → (𝜒 → 𝜃))) | 
| 42 | 41 | a2d 29 | . . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦) → (((𝑁 ∈ ℤ ∧ (𝑦 + 1) ≤ 𝑁) → 𝜒) → ((𝑁 ∈ ℤ ∧ (𝑦 + 1) ≤ 𝑁) → 𝜃))) | 
| 43 | 26, 42 | syld 47 | . . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦) → (((𝑁 ∈ ℤ ∧ 𝑦 ≤ 𝑁) → 𝜒) → ((𝑁 ∈ ℤ ∧ (𝑦 + 1) ≤ 𝑁) → 𝜃))) | 
| 44 | 4, 8, 12, 16, 18, 43 | uzind 12710 | . . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾) → ((𝑁 ∈ ℤ ∧ 𝐾 ≤ 𝑁) → 𝜏)) | 
| 45 | 44 | expcomd 416 | . . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾) → (𝐾 ≤ 𝑁 → (𝑁 ∈ ℤ → 𝜏))) | 
| 46 | 45 | 3expb 1121 | . . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ (𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾)) → (𝐾 ≤ 𝑁 → (𝑁 ∈ ℤ → 𝜏))) | 
| 47 | 46 | expcom 413 | . . . . 5
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾) → (𝑀 ∈ ℤ → (𝐾 ≤ 𝑁 → (𝑁 ∈ ℤ → 𝜏)))) | 
| 48 | 47 | com23 86 | . . . 4
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾) → (𝐾 ≤ 𝑁 → (𝑀 ∈ ℤ → (𝑁 ∈ ℤ → 𝜏)))) | 
| 49 | 48 | 3impia 1118 | . . 3
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁) → (𝑀 ∈ ℤ → (𝑁 ∈ ℤ → 𝜏))) | 
| 50 | 49 | impd 410 | . 2
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝜏)) | 
| 51 | 50 | impcom 407 | 1
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) → 𝜏) |