![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > uzind4s2 | GIF version |
Description: Induction on the upper set of integers that starts at an integer 𝑀, using explicit substitution. The hypotheses are the basis and the induction step. Use this instead of uzind4s 8987 when 𝑗 and 𝑘 must be distinct in [(𝑘 + 1) / 𝑗]𝜑. (Contributed by NM, 16-Nov-2005.) |
Ref | Expression |
---|---|
uzind4s2.1 | ⊢ (𝑀 ∈ ℤ → [𝑀 / 𝑗]𝜑) |
uzind4s2.2 | ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → ([𝑘 / 𝑗]𝜑 → [(𝑘 + 1) / 𝑗]𝜑)) |
Ref | Expression |
---|---|
uzind4s2 | ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → [𝑁 / 𝑗]𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfsbcq 2830 | . 2 ⊢ (𝑚 = 𝑀 → ([𝑚 / 𝑗]𝜑 ↔ [𝑀 / 𝑗]𝜑)) | |
2 | dfsbcq 2830 | . 2 ⊢ (𝑚 = 𝑛 → ([𝑚 / 𝑗]𝜑 ↔ [𝑛 / 𝑗]𝜑)) | |
3 | dfsbcq 2830 | . 2 ⊢ (𝑚 = (𝑛 + 1) → ([𝑚 / 𝑗]𝜑 ↔ [(𝑛 + 1) / 𝑗]𝜑)) | |
4 | dfsbcq 2830 | . 2 ⊢ (𝑚 = 𝑁 → ([𝑚 / 𝑗]𝜑 ↔ [𝑁 / 𝑗]𝜑)) | |
5 | uzind4s2.1 | . 2 ⊢ (𝑀 ∈ ℤ → [𝑀 / 𝑗]𝜑) | |
6 | dfsbcq 2830 | . . . 4 ⊢ (𝑘 = 𝑛 → ([𝑘 / 𝑗]𝜑 ↔ [𝑛 / 𝑗]𝜑)) | |
7 | oveq1 5601 | . . . . 5 ⊢ (𝑘 = 𝑛 → (𝑘 + 1) = (𝑛 + 1)) | |
8 | 7 | sbceq1d 2833 | . . . 4 ⊢ (𝑘 = 𝑛 → ([(𝑘 + 1) / 𝑗]𝜑 ↔ [(𝑛 + 1) / 𝑗]𝜑)) |
9 | 6, 8 | imbi12d 232 | . . 3 ⊢ (𝑘 = 𝑛 → (([𝑘 / 𝑗]𝜑 → [(𝑘 + 1) / 𝑗]𝜑) ↔ ([𝑛 / 𝑗]𝜑 → [(𝑛 + 1) / 𝑗]𝜑))) |
10 | uzind4s2.2 | . . 3 ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → ([𝑘 / 𝑗]𝜑 → [(𝑘 + 1) / 𝑗]𝜑)) | |
11 | 9, 10 | vtoclga 2677 | . 2 ⊢ (𝑛 ∈ (ℤ≥‘𝑀) → ([𝑛 / 𝑗]𝜑 → [(𝑛 + 1) / 𝑗]𝜑)) |
12 | 1, 2, 3, 4, 5, 11 | uzind4 8985 | 1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → [𝑁 / 𝑗]𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1436 [wsbc 2828 ‘cfv 4972 (class class class)co 5594 1c1 7272 + caddc 7274 ℤcz 8660 ℤ≥cuz 8928 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1379 ax-7 1380 ax-gen 1381 ax-ie1 1425 ax-ie2 1426 ax-8 1438 ax-10 1439 ax-11 1440 ax-i12 1441 ax-bndl 1442 ax-4 1443 ax-13 1447 ax-14 1448 ax-17 1462 ax-i9 1466 ax-ial 1470 ax-i5r 1471 ax-ext 2067 ax-sep 3925 ax-pow 3977 ax-pr 4003 ax-un 4227 ax-setind 4319 ax-cnex 7357 ax-resscn 7358 ax-1cn 7359 ax-1re 7360 ax-icn 7361 ax-addcl 7362 ax-addrcl 7363 ax-mulcl 7364 ax-addcom 7366 ax-addass 7368 ax-distr 7370 ax-i2m1 7371 ax-0lt1 7372 ax-0id 7374 ax-rnegex 7375 ax-cnre 7377 ax-pre-ltirr 7378 ax-pre-ltwlin 7379 ax-pre-lttrn 7380 ax-pre-ltadd 7382 |
This theorem depends on definitions: df-bi 115 df-3or 923 df-3an 924 df-tru 1290 df-fal 1293 df-nf 1393 df-sb 1690 df-eu 1948 df-mo 1949 df-clab 2072 df-cleq 2078 df-clel 2081 df-nfc 2214 df-ne 2252 df-nel 2347 df-ral 2360 df-rex 2361 df-reu 2362 df-rab 2364 df-v 2616 df-sbc 2829 df-dif 2988 df-un 2990 df-in 2992 df-ss 2999 df-pw 3411 df-sn 3431 df-pr 3432 df-op 3434 df-uni 3631 df-int 3666 df-br 3815 df-opab 3869 df-mpt 3870 df-id 4087 df-xp 4410 df-rel 4411 df-cnv 4412 df-co 4413 df-dm 4414 df-rn 4415 df-res 4416 df-ima 4417 df-iota 4937 df-fun 4974 df-fn 4975 df-f 4976 df-fv 4980 df-riota 5550 df-ov 5597 df-oprab 5598 df-mpt2 5599 df-pnf 7445 df-mnf 7446 df-xr 7447 df-ltxr 7448 df-le 7449 df-sub 7576 df-neg 7577 df-inn 8335 df-n0 8584 df-z 8661 df-uz 8929 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |