Step | Hyp | Ref
| Expression |
1 | | sbequ 1761 |
. . . . . . 7
⊢ (𝑤 = 𝑧 → ([𝑤 / 𝑟]𝜑 ↔ [𝑧 / 𝑟]𝜑)) |
2 | 1 | anbi2d 451 |
. . . . . 6
⊢ (𝑤 = 𝑧 → ((𝜃 ∧ [𝑤 / 𝑟]𝜑) ↔ (𝜃 ∧ [𝑧 / 𝑟]𝜑))) |
3 | | sbequ 1761 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑧 → ([𝑤 / 𝑥]𝜓 ↔ [𝑧 / 𝑥]𝜓)) |
4 | 3 | anbi1d 452 |
. . . . . . . . 9
⊢ (𝑤 = 𝑧 → (([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ ([𝑧 / 𝑥]𝜓 ∧ 𝜑))) |
5 | 4 | rexbidv 2369 |
. . . . . . . 8
⊢ (𝑤 = 𝑧 → (∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))) |
6 | 5 | imbi2d 228 |
. . . . . . 7
⊢ (𝑤 = 𝑧 → (([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) ↔ ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) |
7 | 6 | ralbidv 2368 |
. . . . . 6
⊢ (𝑤 = 𝑧 → (∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) ↔ ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) |
8 | 2, 7 | imbi12d 232 |
. . . . 5
⊢ (𝑤 = 𝑧 → (((𝜃 ∧ [𝑤 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))) ↔ ((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))))) |
9 | | sbequ 1761 |
. . . . . . 7
⊢ (𝑤 = 𝑥 → ([𝑤 / 𝑟]𝜑 ↔ [𝑥 / 𝑟]𝜑)) |
10 | 9 | anbi2d 451 |
. . . . . 6
⊢ (𝑤 = 𝑥 → ((𝜃 ∧ [𝑤 / 𝑟]𝜑) ↔ (𝜃 ∧ [𝑥 / 𝑟]𝜑))) |
11 | | sbequ12r 1695 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑥 → ([𝑤 / 𝑥]𝜓 ↔ 𝜓)) |
12 | 11 | anbi1d 452 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → (([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ (𝜓 ∧ 𝜑))) |
13 | 12 | rexbidv 2369 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → (∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑))) |
14 | 13 | imbi2d 228 |
. . . . . . 7
⊢ (𝑤 = 𝑥 → (([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) ↔ ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑)))) |
15 | 14 | ralbidv 2368 |
. . . . . 6
⊢ (𝑤 = 𝑥 → (∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) ↔ ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑)))) |
16 | 10, 15 | imbi12d 232 |
. . . . 5
⊢ (𝑤 = 𝑥 → (((𝜃 ∧ [𝑤 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))) ↔ ((𝜃 ∧ [𝑥 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑))))) |
17 | | nfv 1461 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦 𝑤 ∈
ℕ0 |
18 | | nfcv 2219 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦(0...(𝑤 − 1)) |
19 | | nfv 1461 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦(𝜃 ∧ [𝑧 / 𝑟]𝜑) |
20 | | nfra1 2397 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)) |
21 | 19, 20 | nfim 1504 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))) |
22 | 18, 21 | nfralxy 2402 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))) |
23 | 17, 22 | nfan 1497 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(𝑤 ∈ ℕ0
∧ ∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) |
24 | | nfv 1461 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(𝜃 ∧ [𝑤 / 𝑟]𝜑) |
25 | 23, 24 | nfan 1497 |
. . . . . . . . 9
⊢
Ⅎ𝑦((𝑤 ∈ ℕ0
∧ ∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) |
26 | | nfv 1461 |
. . . . . . . . 9
⊢
Ⅎ𝑦 𝑤 = 0 |
27 | 25, 26 | nfan 1497 |
. . . . . . . 8
⊢
Ⅎ𝑦(((𝑤 ∈ ℕ0
∧ ∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0) |
28 | | simplr 496 |
. . . . . . . . . 10
⊢
((((((𝑤 ∈
ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → 𝑦 ∈ ℕ0) |
29 | | nfv 1461 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑟∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑦 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)) |
30 | | breq2 3789 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = 𝑦 → (𝑧 ∥ 𝑟 ↔ 𝑧 ∥ 𝑦)) |
31 | 30 | imbi1d 229 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 = 𝑦 → ((𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)) ↔ (𝑧 ∥ 𝑦 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)))) |
32 | 31 | ralbidv 2368 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = 𝑦 → (∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)) ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑦 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)))) |
33 | 29, 32 | sbie 1714 |
. . . . . . . . . . . . 13
⊢ ([𝑦 / 𝑟]∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)) ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑦 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))) |
34 | | nn0z 8371 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ ℕ0
→ 𝑧 ∈
ℤ) |
35 | | dvds0 10210 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ ℤ → 𝑧 ∥ 0) |
36 | 34, 35 | syl 14 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ℕ0
→ 𝑧 ∥
0) |
37 | 36 | biantrurd 299 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ℕ0
→ (𝑧 ∥ 𝑦 ↔ (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))) |
38 | 37 | biimpd 142 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ℕ0
→ (𝑧 ∥ 𝑦 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))) |
39 | 33, 38 | mprgbir 2421 |
. . . . . . . . . . . 12
⊢ [𝑦 / 𝑟]∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)) |
40 | | nfv 1461 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑟 𝑤 = 0 |
41 | | dfsbcq2 2818 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 0 → ([𝑤 / 𝑥]𝜓 ↔ [0 / 𝑥]𝜓)) |
42 | | bezout.sub-gcd |
. . . . . . . . . . . . . . . 16
⊢ (𝜓 ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦))) |
43 | 42 | sbcbii 2873 |
. . . . . . . . . . . . . . 15
⊢
([0 / 𝑥]𝜓 ↔ [0 / 𝑥]∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦))) |
44 | | c0ex 7113 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
V |
45 | | breq2 3789 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 0 → (𝑧 ∥ 𝑥 ↔ 𝑧 ∥ 0)) |
46 | 45 | anbi1d 452 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 0 → ((𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦) ↔ (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))) |
47 | 46 | imbi2d 228 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 0 → ((𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)) ↔ (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)))) |
48 | 47 | ralbidv 2368 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 0 → (∀𝑧 ∈ ℕ0
(𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)) ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)))) |
49 | 44, 48 | sbcie 2848 |
. . . . . . . . . . . . . . 15
⊢
([0 / 𝑥]∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)) ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))) |
50 | 43, 49 | bitri 182 |
. . . . . . . . . . . . . 14
⊢
([0 / 𝑥]𝜓 ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦))) |
51 | 41, 50 | syl6bb 194 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 0 → ([𝑤 / 𝑥]𝜓 ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)))) |
52 | 40, 51 | sbbid 1767 |
. . . . . . . . . . . 12
⊢ (𝑤 = 0 → ([𝑦 / 𝑟][𝑤 / 𝑥]𝜓 ↔ [𝑦 / 𝑟]∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 0 ∧ 𝑧 ∥ 𝑦)))) |
53 | 39, 52 | mpbiri 166 |
. . . . . . . . . . 11
⊢ (𝑤 = 0 → [𝑦 / 𝑟][𝑤 / 𝑥]𝜓) |
54 | 53 | ad3antlr 476 |
. . . . . . . . . 10
⊢
((((((𝑤 ∈
ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → [𝑦 / 𝑟][𝑤 / 𝑥]𝜓) |
55 | | simpr 108 |
. . . . . . . . . 10
⊢
((((((𝑤 ∈
ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → [𝑦 / 𝑟]𝜑) |
56 | | nfs1v 1856 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑟[𝑦 / 𝑟][𝑤 / 𝑥]𝜓 |
57 | | nfs1v 1856 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑟[𝑦 / 𝑟]𝜑 |
58 | 56, 57 | nfan 1497 |
. . . . . . . . . . 11
⊢
Ⅎ𝑟([𝑦 / 𝑟][𝑤 / 𝑥]𝜓 ∧ [𝑦 / 𝑟]𝜑) |
59 | | sbequ12 1694 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑦 → ([𝑤 / 𝑥]𝜓 ↔ [𝑦 / 𝑟][𝑤 / 𝑥]𝜓)) |
60 | | sbequ12 1694 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑟]𝜑)) |
61 | 59, 60 | anbi12d 456 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑦 → (([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ ([𝑦 / 𝑟][𝑤 / 𝑥]𝜓 ∧ [𝑦 / 𝑟]𝜑))) |
62 | 58, 61 | rspce 2696 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0
∧ ([𝑦 / 𝑟][𝑤 / 𝑥]𝜓 ∧ [𝑦 / 𝑟]𝜑)) → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) |
63 | 28, 54, 55, 62 | syl12anc 1167 |
. . . . . . . . 9
⊢
((((((𝑤 ∈
ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) |
64 | 63 | exp31 356 |
. . . . . . . 8
⊢ ((((𝑤 ∈ ℕ0
∧ ∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0) → (𝑦 ∈ ℕ0 → ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)))) |
65 | 27, 64 | ralrimi 2432 |
. . . . . . 7
⊢ ((((𝑤 ∈ ℕ0
∧ ∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 𝑤 = 0) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))) |
66 | | nfv 1461 |
. . . . . . . . . 10
⊢
Ⅎ𝑦0 < 𝑤 |
67 | 25, 66 | nfan 1497 |
. . . . . . . . 9
⊢
Ⅎ𝑦(((𝑤 ∈ ℕ0
∧ ∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) |
68 | | bezout.is-bezout |
. . . . . . . . . . 11
⊢ (𝜑 ↔ ∃𝑠 ∈ ℤ ∃𝑡 ∈ ℤ 𝑟 = ((𝐴 · 𝑠) + (𝐵 · 𝑡))) |
69 | | simplrl 501 |
. . . . . . . . . . . . 13
⊢ ((((𝑤 ∈ ℕ0
∧ ∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → 𝜃) |
70 | | bezout.a |
. . . . . . . . . . . . 13
⊢ (𝜃 → 𝐴 ∈
ℕ0) |
71 | 69, 70 | syl 14 |
. . . . . . . . . . . 12
⊢ ((((𝑤 ∈ ℕ0
∧ ∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → 𝐴 ∈
ℕ0) |
72 | 71 | ad2antrr 471 |
. . . . . . . . . . 11
⊢
((((((𝑤 ∈
ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → 𝐴 ∈
ℕ0) |
73 | | bezout.b |
. . . . . . . . . . . . 13
⊢ (𝜃 → 𝐵 ∈
ℕ0) |
74 | 69, 73 | syl 14 |
. . . . . . . . . . . 12
⊢ ((((𝑤 ∈ ℕ0
∧ ∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → 𝐵 ∈
ℕ0) |
75 | 74 | ad2antrr 471 |
. . . . . . . . . . 11
⊢
((((((𝑤 ∈
ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → 𝐵 ∈
ℕ0) |
76 | | simplll 499 |
. . . . . . . . . . . . 13
⊢ ((((𝑤 ∈ ℕ0
∧ ∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → 𝑤 ∈ ℕ0) |
77 | | simpr 108 |
. . . . . . . . . . . . 13
⊢ ((((𝑤 ∈ ℕ0
∧ ∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → 0 < 𝑤) |
78 | | elnnnn0b 8332 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ ℕ ↔ (𝑤 ∈ ℕ0
∧ 0 < 𝑤)) |
79 | 76, 77, 78 | sylanbrc 408 |
. . . . . . . . . . . 12
⊢ ((((𝑤 ∈ ℕ0
∧ ∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → 𝑤 ∈ ℕ) |
80 | 79 | ad2antrr 471 |
. . . . . . . . . . 11
⊢
((((((𝑤 ∈
ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → 𝑤 ∈ ℕ) |
81 | | simpr 108 |
. . . . . . . . . . 11
⊢
((((((𝑤 ∈
ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → [𝑦 / 𝑟]𝜑) |
82 | | simplr 496 |
. . . . . . . . . . 11
⊢
((((((𝑤 ∈
ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → 𝑦 ∈ ℕ0) |
83 | | simplrr 502 |
. . . . . . . . . . . . 13
⊢ ((((𝑤 ∈ ℕ0
∧ ∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → [𝑤 / 𝑟]𝜑) |
84 | | sbsbc 2819 |
. . . . . . . . . . . . 13
⊢ ([𝑤 / 𝑟]𝜑 ↔ [𝑤 / 𝑟]𝜑) |
85 | 83, 84 | sylib 120 |
. . . . . . . . . . . 12
⊢ ((((𝑤 ∈ ℕ0
∧ ∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → [𝑤 / 𝑟]𝜑) |
86 | 85 | ad2antrr 471 |
. . . . . . . . . . 11
⊢
((((((𝑤 ∈
ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → [𝑤 / 𝑟]𝜑) |
87 | | breq1 3788 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑎 → (𝑧 ∥ 𝑟 ↔ 𝑎 ∥ 𝑟)) |
88 | | breq1 3788 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑎 → (𝑧 ∥ 𝑥 ↔ 𝑎 ∥ 𝑥)) |
89 | | breq1 3788 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑎 → (𝑧 ∥ 𝑦 ↔ 𝑎 ∥ 𝑦)) |
90 | 88, 89 | anbi12d 456 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑎 → ((𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦) ↔ (𝑎 ∥ 𝑥 ∧ 𝑎 ∥ 𝑦))) |
91 | 87, 90 | imbi12d 232 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑎 → ((𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)) ↔ (𝑎 ∥ 𝑟 → (𝑎 ∥ 𝑥 ∧ 𝑎 ∥ 𝑦)))) |
92 | 91 | cbvralv 2577 |
. . . . . . . . . . . 12
⊢
(∀𝑧 ∈
ℕ0 (𝑧
∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)) ↔ ∀𝑎 ∈ ℕ0 (𝑎 ∥ 𝑟 → (𝑎 ∥ 𝑥 ∧ 𝑎 ∥ 𝑦))) |
93 | 42, 92 | bitri 182 |
. . . . . . . . . . 11
⊢ (𝜓 ↔ ∀𝑎 ∈ ℕ0 (𝑎 ∥ 𝑟 → (𝑎 ∥ 𝑥 ∧ 𝑎 ∥ 𝑦))) |
94 | 69 | ad3antrrr 475 |
. . . . . . . . . . . . 13
⊢
(((((((𝑤 ∈
ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → 𝜃) |
95 | | simpr 108 |
. . . . . . . . . . . . 13
⊢
(((((((𝑤 ∈
ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → [(𝑦 mod 𝑤) / 𝑟]𝜑) |
96 | 94, 95 | jca 300 |
. . . . . . . . . . . 12
⊢
(((((((𝑤 ∈
ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → (𝜃 ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑)) |
97 | 83 | ad3antrrr 475 |
. . . . . . . . . . . 12
⊢
(((((((𝑤 ∈
ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → [𝑤 / 𝑟]𝜑) |
98 | | simpllr 500 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝑤 ∈
ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → 𝑦 ∈ ℕ0) |
99 | 98 | nn0zd 8467 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑤 ∈
ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → 𝑦 ∈ ℤ) |
100 | 79 | ad3antrrr 475 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑤 ∈
ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → 𝑤 ∈ ℕ) |
101 | | zmodfz 9348 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℤ ∧ 𝑤 ∈ ℕ) → (𝑦 mod 𝑤) ∈ (0...(𝑤 − 1))) |
102 | 99, 100, 101 | syl2anc 403 |
. . . . . . . . . . . . 13
⊢
(((((((𝑤 ∈
ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → (𝑦 mod 𝑤) ∈ (0...(𝑤 − 1))) |
103 | | simpll 495 |
. . . . . . . . . . . . . 14
⊢
((((((𝑤 ∈
ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → (((𝑤 ∈ ℕ0 ∧
∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤)) |
104 | | simpr 108 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ ℕ0
∧ ∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) → ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) |
105 | 104 | ad3antrrr 475 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑤 ∈
ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) |
106 | | nfv 1461 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑦[𝑤 / 𝑟]𝜑 |
107 | | nfcv 2219 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑦ℕ0 |
108 | | nfs1v 1856 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑦[𝑤 / 𝑦]𝜓 |
109 | 108 | nfsbxy 1859 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑦[𝑧 / 𝑥][𝑤 / 𝑦]𝜓 |
110 | | nfv 1461 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑦𝜑 |
111 | 109, 110 | nfan 1497 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑦([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑) |
112 | 107, 111 | nfrexxy 2403 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑦∃𝑟 ∈ ℕ0
([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑) |
113 | 106, 112 | nfim 1504 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑦([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)) |
114 | | sbequ 1761 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑤 → ([𝑦 / 𝑟]𝜑 ↔ [𝑤 / 𝑟]𝜑)) |
115 | | nfv 1461 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑥 𝑦 = 𝑤 |
116 | | sbequ12 1694 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = 𝑤 → (𝜓 ↔ [𝑤 / 𝑦]𝜓)) |
117 | 115, 116 | sbbid 1767 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 𝑤 → ([𝑧 / 𝑥]𝜓 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓)) |
118 | 117 | anbi1d 452 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑤 → (([𝑧 / 𝑥]𝜓 ∧ 𝜑) ↔ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))) |
119 | 118 | rexbidv 2369 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑤 → (∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑) ↔ ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))) |
120 | 114, 119 | imbi12d 232 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑤 → (([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)) ↔ ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))) |
121 | 113, 120 | rspc 2695 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ ℕ0
→ (∀𝑦 ∈
ℕ0 ([𝑦 /
𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))) |
122 | 121 | imim2d 53 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ ℕ0
→ (((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))) → ((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))))) |
123 | 122 | ralimdv 2430 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ ℕ0
→ (∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))) → ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))))) |
124 | 123 | ad4antr 477 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑤 ∈
ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → (∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))) → ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))))) |
125 | 105, 124 | mpd 13 |
. . . . . . . . . . . . . 14
⊢
(((((𝑤 ∈
ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))) |
126 | 103, 125 | sylan 277 |
. . . . . . . . . . . . 13
⊢
(((((((𝑤 ∈
ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))) |
127 | | dfsbcq2 2818 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑦 mod 𝑤) → ([𝑧 / 𝑟]𝜑 ↔ [(𝑦 mod 𝑤) / 𝑟]𝜑)) |
128 | 127 | anbi2d 451 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑦 mod 𝑤) → ((𝜃 ∧ [𝑧 / 𝑟]𝜑) ↔ (𝜃 ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑))) |
129 | | sbsbc 2819 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓) |
130 | | sbsbc 2819 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ([𝑤 / 𝑦]𝜓 ↔ [𝑤 / 𝑦]𝜓) |
131 | 130 | sbcbii 2873 |
. . . . . . . . . . . . . . . . . . . 20
⊢
([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓) |
132 | 129, 131 | bitri 182 |
. . . . . . . . . . . . . . . . . . 19
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓) |
133 | 132 | anbi1i 445 |
. . . . . . . . . . . . . . . . . 18
⊢ (([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑) ↔ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)) |
134 | | dfsbcq 2817 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = (𝑦 mod 𝑤) → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ [(𝑦 mod 𝑤) / 𝑥][𝑤 / 𝑦]𝜓)) |
135 | 134 | anbi1d 452 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = (𝑦 mod 𝑤) → (([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑) ↔ ([(𝑦 mod 𝑤) / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))) |
136 | 133, 135 | syl5bb 190 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝑦 mod 𝑤) → (([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑) ↔ ([(𝑦 mod 𝑤) / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))) |
137 | 136 | rexbidv 2369 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑦 mod 𝑤) → (∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑) ↔ ∃𝑟 ∈ ℕ0 ([(𝑦 mod 𝑤) / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))) |
138 | 137 | imbi2d 228 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑦 mod 𝑤) → (([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)) ↔ ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([(𝑦 mod 𝑤) / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))) |
139 | 128, 138 | imbi12d 232 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑦 mod 𝑤) → (((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))) ↔ ((𝜃 ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([(𝑦 mod 𝑤) / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))))) |
140 | 139 | rspcv 2697 |
. . . . . . . . . . . . 13
⊢ ((𝑦 mod 𝑤) ∈ (0...(𝑤 − 1)) → (∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))) → ((𝜃 ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([(𝑦 mod 𝑤) / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑))))) |
141 | 102, 126,
140 | sylc 61 |
. . . . . . . . . . . 12
⊢
(((((((𝑤 ∈
ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → ((𝜃 ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → ([𝑤 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([(𝑦 mod 𝑤) / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)))) |
142 | 96, 97, 141 | mp2d 46 |
. . . . . . . . . . 11
⊢
(((((((𝑤 ∈
ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) ∧ [(𝑦 mod 𝑤) / 𝑟]𝜑) → ∃𝑟 ∈ ℕ0 ([(𝑦 mod 𝑤) / 𝑥][𝑤 / 𝑦]𝜓 ∧ 𝜑)) |
143 | | nfv 1461 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥 𝑤 ∈
ℕ0 |
144 | | nfcv 2219 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥(0...(𝑤 − 1)) |
145 | | nfv 1461 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥(𝜃 ∧ [𝑧 / 𝑟]𝜑) |
146 | | nfcv 2219 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥ℕ0 |
147 | | nfv 1461 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥𝜑 |
148 | 147 | nfsbxy 1859 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥[𝑦 / 𝑟]𝜑 |
149 | | nfs1v 1856 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑥[𝑧 / 𝑥]𝜓 |
150 | 149, 147 | nfan 1497 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥([𝑧 / 𝑥]𝜓 ∧ 𝜑) |
151 | 146, 150 | nfrexxy 2403 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥∃𝑟 ∈ ℕ0
([𝑧 / 𝑥]𝜓 ∧ 𝜑) |
152 | 148, 151 | nfim 1504 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)) |
153 | 146, 152 | nfralxy 2402 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)) |
154 | 145, 153 | nfim 1504 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))) |
155 | 144, 154 | nfralxy 2402 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))) |
156 | 143, 155 | nfan 1497 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(𝑤 ∈ ℕ0
∧ ∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) |
157 | | nfv 1461 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(𝜃 ∧ [𝑤 / 𝑟]𝜑) |
158 | 156, 157 | nfan 1497 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥((𝑤 ∈ ℕ0
∧ ∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) |
159 | | nfv 1461 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥0 < 𝑤 |
160 | 158, 159 | nfan 1497 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(((𝑤 ∈ ℕ0
∧ ∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) |
161 | | nfv 1461 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥 𝑦 ∈
ℕ0 |
162 | 160, 161 | nfan 1497 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥((((𝑤 ∈ ℕ0
∧ ∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) |
163 | 162, 148 | nfan 1497 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(((((𝑤 ∈ ℕ0
∧ ∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) |
164 | | nfv 1461 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑟 𝑤 ∈
ℕ0 |
165 | | nfcv 2219 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑟(0...(𝑤 − 1)) |
166 | | nfv 1461 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑟𝜃 |
167 | | nfs1v 1856 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑟[𝑧 / 𝑟]𝜑 |
168 | 166, 167 | nfan 1497 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑟(𝜃 ∧ [𝑧 / 𝑟]𝜑) |
169 | | nfcv 2219 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑟ℕ0 |
170 | | nfre1 2407 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑟∃𝑟 ∈ ℕ0
([𝑧 / 𝑥]𝜓 ∧ 𝜑) |
171 | 57, 170 | nfim 1504 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑟([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)) |
172 | 169, 171 | nfralxy 2402 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑟∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)) |
173 | 168, 172 | nfim 1504 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑟((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))) |
174 | 165, 173 | nfralxy 2402 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑟∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))) |
175 | 164, 174 | nfan 1497 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑟(𝑤 ∈ ℕ0
∧ ∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) |
176 | | nfs1v 1856 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑟[𝑤 / 𝑟]𝜑 |
177 | 166, 176 | nfan 1497 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑟(𝜃 ∧ [𝑤 / 𝑟]𝜑) |
178 | 175, 177 | nfan 1497 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑟((𝑤 ∈ ℕ0
∧ ∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) |
179 | | nfv 1461 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑟0 < 𝑤 |
180 | 178, 179 | nfan 1497 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑟(((𝑤 ∈ ℕ0
∧ ∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) |
181 | | nfv 1461 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑟 𝑦 ∈
ℕ0 |
182 | 180, 181 | nfan 1497 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑟((((𝑤 ∈ ℕ0
∧ ∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) |
183 | 182, 57 | nfan 1497 |
. . . . . . . . . . 11
⊢
Ⅎ𝑟(((((𝑤 ∈ ℕ0
∧ ∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) |
184 | 68, 72, 75, 80, 81, 82, 86, 93, 142, 163, 183 | bezoutlemstep 10386 |
. . . . . . . . . 10
⊢
((((((𝑤 ∈
ℕ0 ∧ ∀𝑧 ∈ (0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) ∧ 𝑦 ∈ ℕ0) ∧ [𝑦 / 𝑟]𝜑) → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) |
185 | 184 | exp31 356 |
. . . . . . . . 9
⊢ ((((𝑤 ∈ ℕ0
∧ ∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → (𝑦 ∈ ℕ0 → ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)))) |
186 | 67, 185 | ralrimi 2432 |
. . . . . . . 8
⊢ ((((𝑤 ∈ ℕ0
∧ ∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))) |
187 | | sbsbc 2819 |
. . . . . . . . . . . 12
⊢ ([𝑤 / 𝑥]𝜓 ↔ [𝑤 / 𝑥]𝜓) |
188 | 187 | anbi1i 445 |
. . . . . . . . . . 11
⊢ (([𝑤 / 𝑥]𝜓 ∧ 𝜑) ↔ ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) |
189 | 188 | rexbii 2373 |
. . . . . . . . . 10
⊢
(∃𝑟 ∈
ℕ0 ([𝑤 /
𝑥]𝜓 ∧ 𝜑) ↔ ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) |
190 | 189 | imbi2i 224 |
. . . . . . . . 9
⊢ (([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) ↔ ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))) |
191 | 190 | ralbii 2372 |
. . . . . . . 8
⊢
(∀𝑦 ∈
ℕ0 ([𝑦 /
𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑)) ↔ ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))) |
192 | 186, 191 | sylibr 132 |
. . . . . . 7
⊢ ((((𝑤 ∈ ℕ0
∧ ∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) ∧ 0 < 𝑤) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))) |
193 | | nn0nlt0 8314 |
. . . . . . . . 9
⊢ (𝑤 ∈ ℕ0
→ ¬ 𝑤 <
0) |
194 | | nn0z 8371 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ ℕ0
→ 𝑤 ∈
ℤ) |
195 | | ztri3or0 8393 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ ℤ → (𝑤 < 0 ∨ 𝑤 = 0 ∨ 0 < 𝑤)) |
196 | 194, 195 | syl 14 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ℕ0
→ (𝑤 < 0 ∨ 𝑤 = 0 ∨ 0 < 𝑤)) |
197 | | 3orass 922 |
. . . . . . . . . . 11
⊢ ((𝑤 < 0 ∨ 𝑤 = 0 ∨ 0 < 𝑤) ↔ (𝑤 < 0 ∨ (𝑤 = 0 ∨ 0 < 𝑤))) |
198 | 196, 197 | sylib 120 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ℕ0
→ (𝑤 < 0 ∨
(𝑤 = 0 ∨ 0 < 𝑤))) |
199 | 198 | orcomd 680 |
. . . . . . . . 9
⊢ (𝑤 ∈ ℕ0
→ ((𝑤 = 0 ∨ 0 <
𝑤) ∨ 𝑤 < 0)) |
200 | 193, 199 | ecased 1280 |
. . . . . . . 8
⊢ (𝑤 ∈ ℕ0
→ (𝑤 = 0 ∨ 0 <
𝑤)) |
201 | 200 | ad2antrr 471 |
. . . . . . 7
⊢ (((𝑤 ∈ ℕ0
∧ ∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) → (𝑤 = 0 ∨ 0 < 𝑤)) |
202 | 65, 192, 201 | mpjaodan 744 |
. . . . . 6
⊢ (((𝑤 ∈ ℕ0
∧ ∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑)))) ∧ (𝜃 ∧ [𝑤 / 𝑟]𝜑)) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))) |
203 | 202 | exp31 356 |
. . . . 5
⊢ (𝑤 ∈ ℕ0
→ (∀𝑧 ∈
(0...(𝑤 − 1))((𝜃 ∧ [𝑧 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑧 / 𝑥]𝜓 ∧ 𝜑))) → ((𝜃 ∧ [𝑤 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 ([𝑤 / 𝑥]𝜓 ∧ 𝜑))))) |
204 | 8, 16, 203 | nn0sinds 9430 |
. . . 4
⊢ (𝑥 ∈ ℕ0
→ ((𝜃 ∧ [𝑥 / 𝑟]𝜑) → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑)))) |
205 | 204 | expd 254 |
. . 3
⊢ (𝑥 ∈ ℕ0
→ (𝜃 → ([𝑥 / 𝑟]𝜑 → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑))))) |
206 | 205 | impcom 123 |
. 2
⊢ ((𝜃 ∧ 𝑥 ∈ ℕ0) → ([𝑥 / 𝑟]𝜑 → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑)))) |
207 | 206 | ralrimiva 2434 |
1
⊢ (𝜃 → ∀𝑥 ∈ ℕ0 ([𝑥 / 𝑟]𝜑 → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑)))) |