Proof of Theorem rexanuz2nf
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 0nn0 12541 | . . . . . . . 8
⊢ 0 ∈
ℕ0 | 
| 2 |  | nn0ge0 12551 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ 0 ≤ 𝑘) | 
| 3 | 2 | rgen 3063 | . . . . . . . 8
⊢
∀𝑘 ∈
ℕ0 0 ≤ 𝑘 | 
| 4 |  | fveq2 6906 | . . . . . . . . . . . 12
⊢ (𝑗 = 0 →
(ℤ≥‘𝑗) =
(ℤ≥‘0)) | 
| 5 |  | nn0uz 12920 | . . . . . . . . . . . 12
⊢
ℕ0 = (ℤ≥‘0) | 
| 6 | 4, 5 | eqtr4di 2795 | . . . . . . . . . . 11
⊢ (𝑗 = 0 →
(ℤ≥‘𝑗) = ℕ0) | 
| 7 | 6 | raleqdv 3326 | . . . . . . . . . 10
⊢ (𝑗 = 0 → (∀𝑘 ∈
(ℤ≥‘𝑗)(𝑗 = 0 ∧ 𝑗 ≤ 𝑘) ↔ ∀𝑘 ∈ ℕ0 (𝑗 = 0 ∧ 𝑗 ≤ 𝑘))) | 
| 8 | 2 | ad2antlr 727 | . . . . . . . . . . . 12
⊢ (((𝑗 = 0 ∧ 𝑘 ∈ ℕ0) ∧ (𝑗 = 0 ∧ 𝑗 ≤ 𝑘)) → 0 ≤ 𝑘) | 
| 9 |  | simpll 767 | . . . . . . . . . . . . 13
⊢ (((𝑗 = 0 ∧ 𝑘 ∈ ℕ0) ∧ 0 ≤
𝑘) → 𝑗 = 0) | 
| 10 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ (((𝑗 = 0 ∧ 𝑘 ∈ ℕ0) ∧ 0 ≤
𝑘) → 0 ≤ 𝑘) | 
| 11 | 9, 10 | eqbrtrd 5165 | . . . . . . . . . . . . 13
⊢ (((𝑗 = 0 ∧ 𝑘 ∈ ℕ0) ∧ 0 ≤
𝑘) → 𝑗 ≤ 𝑘) | 
| 12 | 9, 11 | jca 511 | . . . . . . . . . . . 12
⊢ (((𝑗 = 0 ∧ 𝑘 ∈ ℕ0) ∧ 0 ≤
𝑘) → (𝑗 = 0 ∧ 𝑗 ≤ 𝑘)) | 
| 13 | 8, 12 | impbida 801 | . . . . . . . . . . 11
⊢ ((𝑗 = 0 ∧ 𝑘 ∈ ℕ0) → ((𝑗 = 0 ∧ 𝑗 ≤ 𝑘) ↔ 0 ≤ 𝑘)) | 
| 14 | 13 | ralbidva 3176 | . . . . . . . . . 10
⊢ (𝑗 = 0 → (∀𝑘 ∈ ℕ0
(𝑗 = 0 ∧ 𝑗 ≤ 𝑘) ↔ ∀𝑘 ∈ ℕ0 0 ≤ 𝑘)) | 
| 15 | 7, 14 | bitrd 279 | . . . . . . . . 9
⊢ (𝑗 = 0 → (∀𝑘 ∈
(ℤ≥‘𝑗)(𝑗 = 0 ∧ 𝑗 ≤ 𝑘) ↔ ∀𝑘 ∈ ℕ0 0 ≤ 𝑘)) | 
| 16 | 15 | rspcev 3622 | . . . . . . . 8
⊢ ((0
∈ ℕ0 ∧ ∀𝑘 ∈ ℕ0 0 ≤ 𝑘) → ∃𝑗 ∈ ℕ0
∀𝑘 ∈
(ℤ≥‘𝑗)(𝑗 = 0 ∧ 𝑗 ≤ 𝑘)) | 
| 17 | 1, 3, 16 | mp2an 692 | . . . . . . 7
⊢
∃𝑗 ∈
ℕ0 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑗 = 0 ∧ 𝑗 ≤ 𝑘) | 
| 18 |  | rexanuz2nf.1 | . . . . . . . . 9
⊢ 𝑍 =
ℕ0 | 
| 19 |  | nfcv 2905 | . . . . . . . . 9
⊢
Ⅎ𝑗ℕ0 | 
| 20 | 18, 19 | nfcxfr 2903 | . . . . . . . 8
⊢
Ⅎ𝑗𝑍 | 
| 21 | 20, 19, 18 | rexeqif 45171 | . . . . . . 7
⊢
(∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)(𝑗 = 0 ∧ 𝑗 ≤ 𝑘) ↔ ∃𝑗 ∈ ℕ0 ∀𝑘 ∈
(ℤ≥‘𝑗)(𝑗 = 0 ∧ 𝑗 ≤ 𝑘)) | 
| 22 | 17, 21 | mpbir 231 | . . . . . 6
⊢
∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)(𝑗 = 0 ∧ 𝑗 ≤ 𝑘) | 
| 23 |  | rexanuz2nf.2 | . . . . . . . 8
⊢ (𝜑 ↔ (𝑗 = 0 ∧ 𝑗 ≤ 𝑘)) | 
| 24 | 23 | ralbii 3093 | . . . . . . 7
⊢
(∀𝑘 ∈
(ℤ≥‘𝑗)𝜑 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑗 = 0 ∧ 𝑗 ≤ 𝑘)) | 
| 25 | 24 | rexbii 3094 | . . . . . 6
⊢
(∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)𝜑 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑗 = 0 ∧ 𝑗 ≤ 𝑘)) | 
| 26 | 22, 25 | mpbir 231 | . . . . 5
⊢
∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)𝜑 | 
| 27 |  | 1nn0 12542 | . . . . . . . 8
⊢ 1 ∈
ℕ0 | 
| 28 |  | nngt0 12297 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ → 0 <
𝑘) | 
| 29 | 28 | rgen 3063 | . . . . . . . 8
⊢
∀𝑘 ∈
ℕ 0 < 𝑘 | 
| 30 |  | fveq2 6906 | . . . . . . . . . . 11
⊢ (𝑗 = 1 →
(ℤ≥‘𝑗) =
(ℤ≥‘1)) | 
| 31 |  | nnuz 12921 | . . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) | 
| 32 | 30, 31 | eqtr4di 2795 | . . . . . . . . . 10
⊢ (𝑗 = 1 →
(ℤ≥‘𝑗) = ℕ) | 
| 33 | 32 | raleqdv 3326 | . . . . . . . . 9
⊢ (𝑗 = 1 → (∀𝑘 ∈
(ℤ≥‘𝑗)0 < 𝑘 ↔ ∀𝑘 ∈ ℕ 0 < 𝑘)) | 
| 34 | 33 | rspcev 3622 | . . . . . . . 8
⊢ ((1
∈ ℕ0 ∧ ∀𝑘 ∈ ℕ 0 < 𝑘) → ∃𝑗 ∈ ℕ0 ∀𝑘 ∈
(ℤ≥‘𝑗)0 < 𝑘) | 
| 35 | 27, 29, 34 | mp2an 692 | . . . . . . 7
⊢
∃𝑗 ∈
ℕ0 ∀𝑘 ∈ (ℤ≥‘𝑗)0 < 𝑘 | 
| 36 | 20, 19, 18 | rexeqif 45171 | . . . . . . 7
⊢
(∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)0 < 𝑘 ↔ ∃𝑗 ∈ ℕ0 ∀𝑘 ∈
(ℤ≥‘𝑗)0 < 𝑘) | 
| 37 | 35, 36 | mpbir 231 | . . . . . 6
⊢
∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)0 < 𝑘 | 
| 38 |  | rexanuz2nf.3 | . . . . . . . 8
⊢ (𝜓 ↔ 0 < 𝑘) | 
| 39 | 38 | ralbii 3093 | . . . . . . 7
⊢
(∀𝑘 ∈
(ℤ≥‘𝑗)𝜓 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)0 < 𝑘) | 
| 40 | 39 | rexbii 3094 | . . . . . 6
⊢
(∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)𝜓 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)0 < 𝑘) | 
| 41 | 37, 40 | mpbir 231 | . . . . 5
⊢
∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)𝜓 | 
| 42 | 26, 41 | pm3.2i 470 | . . . 4
⊢
(∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)𝜑 ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓) | 
| 43 |  | nfv 1914 | . . . . . . . . 9
⊢
Ⅎ𝑘 ¬
((𝑗 = 0 ∧ 𝑗 ≤ 𝑗) ∧ 0 < 𝑗) | 
| 44 |  | nfcv 2905 | . . . . . . . . 9
⊢
Ⅎ𝑘𝑗 | 
| 45 |  | nfcv 2905 | . . . . . . . . 9
⊢
Ⅎ𝑘(ℤ≥‘𝑗) | 
| 46 | 5 | uzid3 45446 | . . . . . . . . . 10
⊢ (𝑗 ∈ ℕ0
→ 𝑗 ∈
(ℤ≥‘𝑗)) | 
| 47 | 46 | adantr 480 | . . . . . . . . 9
⊢ ((𝑗 ∈ ℕ0
∧ 𝑗 = 0) → 𝑗 ∈
(ℤ≥‘𝑗)) | 
| 48 |  | 0re 11263 | . . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ | 
| 49 | 48 | ltnri 11370 | . . . . . . . . . . . . 13
⊢  ¬ 0
< 0 | 
| 50 | 49 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝑗 = 0 → ¬ 0 <
0) | 
| 51 |  | eqcom 2744 | . . . . . . . . . . . . 13
⊢ (𝑗 = 0 ↔ 0 = 𝑗) | 
| 52 | 51 | biimpi 216 | . . . . . . . . . . . 12
⊢ (𝑗 = 0 → 0 = 𝑗) | 
| 53 | 50, 52 | brneqtrd 45081 | . . . . . . . . . . 11
⊢ (𝑗 = 0 → ¬ 0 < 𝑗) | 
| 54 | 53 | intnand 488 | . . . . . . . . . 10
⊢ (𝑗 = 0 → ¬ ((𝑗 = 0 ∧ 𝑗 ≤ 𝑗) ∧ 0 < 𝑗)) | 
| 55 | 54 | adantl 481 | . . . . . . . . 9
⊢ ((𝑗 ∈ ℕ0
∧ 𝑗 = 0) → ¬
((𝑗 = 0 ∧ 𝑗 ≤ 𝑗) ∧ 0 < 𝑗)) | 
| 56 |  | breq2 5147 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝑗 → (𝑗 ≤ 𝑘 ↔ 𝑗 ≤ 𝑗)) | 
| 57 | 56 | anbi2d 630 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝑗 → ((𝑗 = 0 ∧ 𝑗 ≤ 𝑘) ↔ (𝑗 = 0 ∧ 𝑗 ≤ 𝑗))) | 
| 58 | 23, 57 | bitrid 283 | . . . . . . . . . . 11
⊢ (𝑘 = 𝑗 → (𝜑 ↔ (𝑗 = 0 ∧ 𝑗 ≤ 𝑗))) | 
| 59 |  | breq2 5147 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝑗 → (0 < 𝑘 ↔ 0 < 𝑗)) | 
| 60 | 38, 59 | bitrid 283 | . . . . . . . . . . 11
⊢ (𝑘 = 𝑗 → (𝜓 ↔ 0 < 𝑗)) | 
| 61 | 58, 60 | anbi12d 632 | . . . . . . . . . 10
⊢ (𝑘 = 𝑗 → ((𝜑 ∧ 𝜓) ↔ ((𝑗 = 0 ∧ 𝑗 ≤ 𝑗) ∧ 0 < 𝑗))) | 
| 62 | 61 | notbid 318 | . . . . . . . . 9
⊢ (𝑘 = 𝑗 → (¬ (𝜑 ∧ 𝜓) ↔ ¬ ((𝑗 = 0 ∧ 𝑗 ≤ 𝑗) ∧ 0 < 𝑗))) | 
| 63 | 43, 44, 45, 47, 55, 62 | rspced 45172 | . . . . . . . 8
⊢ ((𝑗 ∈ ℕ0
∧ 𝑗 = 0) →
∃𝑘 ∈
(ℤ≥‘𝑗) ¬ (𝜑 ∧ 𝜓)) | 
| 64 | 46 | adantr 480 | . . . . . . . . 9
⊢ ((𝑗 ∈ ℕ0
∧ ¬ 𝑗 = 0) →
𝑗 ∈
(ℤ≥‘𝑗)) | 
| 65 |  | id 22 | . . . . . . . . . . . 12
⊢ (¬
𝑗 = 0 → ¬ 𝑗 = 0) | 
| 66 | 65 | intnanrd 489 | . . . . . . . . . . 11
⊢ (¬
𝑗 = 0 → ¬ (𝑗 = 0 ∧ 𝑗 ≤ 𝑗)) | 
| 67 | 66 | intnanrd 489 | . . . . . . . . . 10
⊢ (¬
𝑗 = 0 → ¬ ((𝑗 = 0 ∧ 𝑗 ≤ 𝑗) ∧ 0 < 𝑗)) | 
| 68 | 67 | adantl 481 | . . . . . . . . 9
⊢ ((𝑗 ∈ ℕ0
∧ ¬ 𝑗 = 0) →
¬ ((𝑗 = 0 ∧ 𝑗 ≤ 𝑗) ∧ 0 < 𝑗)) | 
| 69 | 43, 44, 45, 64, 68, 62 | rspced 45172 | . . . . . . . 8
⊢ ((𝑗 ∈ ℕ0
∧ ¬ 𝑗 = 0) →
∃𝑘 ∈
(ℤ≥‘𝑗) ¬ (𝜑 ∧ 𝜓)) | 
| 70 | 63, 69 | pm2.61dan 813 | . . . . . . 7
⊢ (𝑗 ∈ ℕ0
→ ∃𝑘 ∈
(ℤ≥‘𝑗) ¬ (𝜑 ∧ 𝜓)) | 
| 71 |  | rexnal 3100 | . . . . . . 7
⊢
(∃𝑘 ∈
(ℤ≥‘𝑗) ¬ (𝜑 ∧ 𝜓) ↔ ¬ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜑 ∧ 𝜓)) | 
| 72 | 70, 71 | sylib 218 | . . . . . 6
⊢ (𝑗 ∈ ℕ0
→ ¬ ∀𝑘
∈ (ℤ≥‘𝑗)(𝜑 ∧ 𝜓)) | 
| 73 | 72 | nrex 3074 | . . . . 5
⊢  ¬
∃𝑗 ∈
ℕ0 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜑 ∧ 𝜓) | 
| 74 | 20, 19, 18 | rexeqif 45171 | . . . . 5
⊢
(∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)(𝜑 ∧ 𝜓) ↔ ∃𝑗 ∈ ℕ0 ∀𝑘 ∈
(ℤ≥‘𝑗)(𝜑 ∧ 𝜓)) | 
| 75 | 73, 74 | mtbir 323 | . . . 4
⊢  ¬
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜑 ∧ 𝜓) | 
| 76 | 42, 75 | pm3.2i 470 | . . 3
⊢
((∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)𝜑 ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓) ∧ ¬ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜑 ∧ 𝜓)) | 
| 77 |  | annim 403 | . . 3
⊢
(((∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)𝜑 ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓) ∧ ¬ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜑 ∧ 𝜓)) ↔ ¬ ((∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜑 ∧ 𝜓))) | 
| 78 | 76, 77 | mpbi 230 | . 2
⊢  ¬
((∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜑 ∧ 𝜓)) | 
| 79 | 78 | nimnbi2 45169 | 1
⊢  ¬
(∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜑 ∧ 𝜓) ↔ (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓)) |