Proof of Theorem smfmullem4
Step | Hyp | Ref
| Expression |
1 | | smfmullem4.x |
. . . . 5
⊢
Ⅎ𝑥𝜑 |
2 | | smfmullem4.r |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ ℝ) |
3 | 2 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 · 𝐷) < 𝑅) → 𝑅 ∈ ℝ) |
4 | | smfmullem4.k |
. . . . . . . . 9
⊢ 𝐾 = {𝑞 ∈ (ℚ ↑𝑚
(0...3)) ∣ ∀𝑢
∈ ((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅} |
5 | | inss1 3795 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∩ 𝐶) ⊆ 𝐴 |
6 | 5 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ∩ 𝐶) ⊆ 𝐴) |
7 | 6 | sselda 3568 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) → 𝑥 ∈ 𝐴) |
8 | | smfmullem4.b |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
9 | 7, 8 | syldan 486 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) → 𝐵 ∈ ℝ) |
10 | 9 | 3adant3 1074 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 · 𝐷) < 𝑅) → 𝐵 ∈ ℝ) |
11 | | elinel2 3762 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) → 𝑥 ∈ 𝐶) |
12 | 11 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) → 𝑥 ∈ 𝐶) |
13 | | smfmullem4.d |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐷 ∈ ℝ) |
14 | 12, 13 | syldan 486 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) → 𝐷 ∈ ℝ) |
15 | 14 | 3adant3 1074 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 · 𝐷) < 𝑅) → 𝐷 ∈ ℝ) |
16 | | simp3 1056 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 · 𝐷) < 𝑅) → (𝐵 · 𝐷) < 𝑅) |
17 | | eqid 2610 |
. . . . . . . . 9
⊢ ((𝑅 − (𝐵 · 𝐷)) / (1 + ((abs‘𝐵) + (abs‘𝐷)))) = ((𝑅 − (𝐵 · 𝐷)) / (1 + ((abs‘𝐵) + (abs‘𝐷)))) |
18 | | eqid 2610 |
. . . . . . . . 9
⊢ if(1 ≤
((𝑅 − (𝐵 · 𝐷)) / (1 + ((abs‘𝐵) + (abs‘𝐷)))), 1, ((𝑅 − (𝐵 · 𝐷)) / (1 + ((abs‘𝐵) + (abs‘𝐷))))) = if(1 ≤ ((𝑅 − (𝐵 · 𝐷)) / (1 + ((abs‘𝐵) + (abs‘𝐷)))), 1, ((𝑅 − (𝐵 · 𝐷)) / (1 + ((abs‘𝐵) + (abs‘𝐷))))) |
19 | 3, 4, 10, 15, 16, 17, 18 | smfmullem3 39678 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 · 𝐷) < 𝑅) → ∃𝑞 ∈ 𝐾 (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))) |
20 | | rabid 3095 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))} ↔ (𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3))))) |
21 | 20 | bicomi 213 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))) ↔ 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))}) |
22 | 21 | biimpi 205 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))) → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))}) |
23 | 22 | adantll 746 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) ∧ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))) → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))}) |
24 | 23 | adantlr 747 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) ∧ 𝑞 ∈ 𝐾) ∧ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))) → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))}) |
25 | | smfmullem4.e |
. . . . . . . . . . . . . . . . 17
⊢ 𝐸 = (𝑞 ∈ 𝐾 ↦ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))}) |
26 | 25 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐸 = (𝑞 ∈ 𝐾 ↦ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))})) |
27 | | inrab 3858 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑥 ∈ (𝐴 ∩ 𝐶) ∣ 𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1))} ∩ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3))}) = {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))} |
28 | | smfmullem4.s |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑆 ∈ SAlg) |
29 | | smfmullem4.a |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
30 | 29, 6 | ssexd 4733 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐴 ∩ 𝐶) ∈ V) |
31 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑆 ↾t (𝐴 ∩ 𝐶)) = (𝑆 ↾t (𝐴 ∩ 𝐶)) |
32 | 28, 30, 31 | subsalsal 39253 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑆 ↾t (𝐴 ∩ 𝐶)) ∈ SAlg) |
33 | 32 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝑆 ↾t (𝐴 ∩ 𝐶)) ∈ SAlg) |
34 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑥 𝑞 ∈ 𝐾 |
35 | 1, 34 | nfan 1816 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥(𝜑 ∧ 𝑞 ∈ 𝐾) |
36 | 28 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → 𝑆 ∈ SAlg) |
37 | 30 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝐴 ∩ 𝐶) ∈ V) |
38 | 9 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐾) ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) → 𝐵 ∈ ℝ) |
39 | | smfmullem4.m |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆)) |
40 | 28, 39, 6 | sssmfmpt 39637 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∩ 𝐶) ↦ 𝐵) ∈ (SMblFn‘𝑆)) |
41 | 40 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝑥 ∈ (𝐴 ∩ 𝐶) ↦ 𝐵) ∈ (SMblFn‘𝑆)) |
42 | | ssrab2 3650 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ {𝑞 ∈ (ℚ
↑𝑚 (0...3)) ∣ ∀𝑢 ∈ ((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅} ⊆ (ℚ
↑𝑚 (0...3)) |
43 | 4, 42 | eqsstri 3598 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝐾 ⊆ (ℚ
↑𝑚 (0...3)) |
44 | | reex 9906 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ℝ
∈ V |
45 | | qssre 11674 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ℚ
⊆ ℝ |
46 | | mapss 7786 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((ℝ
∈ V ∧ ℚ ⊆ ℝ) → (ℚ
↑𝑚 (0...3)) ⊆ (ℝ ↑𝑚
(0...3))) |
47 | 44, 45, 46 | mp2an 704 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (ℚ
↑𝑚 (0...3)) ⊆ (ℝ ↑𝑚
(0...3)) |
48 | 43, 47 | sstri 3577 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝐾 ⊆ (ℝ
↑𝑚 (0...3)) |
49 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑞 ∈ 𝐾 → 𝑞 ∈ 𝐾) |
50 | 48, 49 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑞 ∈ 𝐾 → 𝑞 ∈ (ℝ ↑𝑚
(0...3))) |
51 | 44 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑞 ∈ 𝐾 → ℝ ∈ V) |
52 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (0...3)
∈ V |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑞 ∈ 𝐾 → (0...3) ∈ V) |
54 | 51, 53 | elmapd 7758 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑞 ∈ 𝐾 → (𝑞 ∈ (ℝ ↑𝑚
(0...3)) ↔ 𝑞:(0...3)⟶ℝ)) |
55 | 50, 54 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑞 ∈ 𝐾 → 𝑞:(0...3)⟶ℝ) |
56 | | 0z 11265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 0 ∈
ℤ |
57 | | 3z 11287 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 3 ∈
ℤ |
58 | | 0re 9919 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 0 ∈
ℝ |
59 | | 3re 10971 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 3 ∈
ℝ |
60 | | 3pos 10991 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 0 <
3 |
61 | 58, 59, 60 | ltleii 10039 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 0 ≤
3 |
62 | 56, 57, 61 | 3pm3.2i 1232 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (0 ∈
ℤ ∧ 3 ∈ ℤ ∧ 0 ≤ 3) |
63 | | eluz2 11569 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (3 ∈
(ℤ≥‘0) ↔ (0 ∈ ℤ ∧ 3 ∈
ℤ ∧ 0 ≤ 3)) |
64 | 62, 63 | mpbir 220 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 3 ∈
(ℤ≥‘0) |
65 | | eluzfz1 12219 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (3 ∈
(ℤ≥‘0) → 0 ∈ (0...3)) |
66 | 64, 65 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ∈
(0...3) |
67 | 66 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑞 ∈ 𝐾 → 0 ∈ (0...3)) |
68 | 55, 67 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑞 ∈ 𝐾 → (𝑞‘0) ∈ ℝ) |
69 | 68 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝑞‘0) ∈ ℝ) |
70 | 69 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝑞‘0) ∈
ℝ*) |
71 | | 0le1 10430 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 0 ≤
1 |
72 | | 1re 9918 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 1 ∈
ℝ |
73 | | 1lt3 11073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 1 <
3 |
74 | 72, 59, 73 | ltleii 10039 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 1 ≤
3 |
75 | 71, 74 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (0 ≤ 1
∧ 1 ≤ 3) |
76 | | 1z 11284 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 1 ∈
ℤ |
77 | | elfz 12203 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((1
∈ ℤ ∧ 0 ∈ ℤ ∧ 3 ∈ ℤ) → (1 ∈
(0...3) ↔ (0 ≤ 1 ∧ 1 ≤ 3))) |
78 | 76, 56, 57, 77 | mp3an 1416 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (1 ∈
(0...3) ↔ (0 ≤ 1 ∧ 1 ≤ 3)) |
79 | 75, 78 | mpbir 220 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 ∈
(0...3) |
80 | 79 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑞 ∈ 𝐾 → 1 ∈ (0...3)) |
81 | 55, 80 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑞 ∈ 𝐾 → (𝑞‘1) ∈ ℝ) |
82 | 81 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝑞‘1) ∈ ℝ) |
83 | 82 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝑞‘1) ∈
ℝ*) |
84 | 35, 36, 37, 38, 41, 70, 83 | smfpimioompt 39671 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ 𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1))} ∈ (𝑆 ↾t (𝐴 ∩ 𝐶))) |
85 | 14 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐾) ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) → 𝐷 ∈ ℝ) |
86 | | smfmullem4.n |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ 𝐷) ∈ (SMblFn‘𝑆)) |
87 | 1, 12 | ssdf 38273 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐴 ∩ 𝐶) ⊆ 𝐶) |
88 | 28, 86, 87 | sssmfmpt 39637 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∩ 𝐶) ↦ 𝐷) ∈ (SMblFn‘𝑆)) |
89 | 88 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝑥 ∈ (𝐴 ∩ 𝐶) ↦ 𝐷) ∈ (SMblFn‘𝑆)) |
90 | | 0le2 10988 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 0 ≤
2 |
91 | | 2re 10967 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 2 ∈
ℝ |
92 | | 2lt3 11072 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 2 <
3 |
93 | 91, 59, 92 | ltleii 10039 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 2 ≤
3 |
94 | 90, 93 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (0 ≤ 2
∧ 2 ≤ 3) |
95 | | 2z 11286 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 2 ∈
ℤ |
96 | | elfz 12203 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((2
∈ ℤ ∧ 0 ∈ ℤ ∧ 3 ∈ ℤ) → (2 ∈
(0...3) ↔ (0 ≤ 2 ∧ 2 ≤ 3))) |
97 | 95, 56, 57, 96 | mp3an 1416 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (2 ∈
(0...3) ↔ (0 ≤ 2 ∧ 2 ≤ 3)) |
98 | 94, 97 | mpbir 220 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 2 ∈
(0...3) |
99 | 98 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑞 ∈ 𝐾 → 2 ∈ (0...3)) |
100 | 55, 99 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑞 ∈ 𝐾 → (𝑞‘2) ∈ ℝ) |
101 | 100 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝑞‘2) ∈ ℝ) |
102 | 101 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝑞‘2) ∈
ℝ*) |
103 | | eluzfz2 12220 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (3 ∈
(ℤ≥‘0) → 3 ∈ (0...3)) |
104 | 64, 103 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 3 ∈
(0...3) |
105 | 104 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑞 ∈ 𝐾 → 3 ∈ (0...3)) |
106 | 55, 105 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑞 ∈ 𝐾 → (𝑞‘3) ∈ ℝ) |
107 | 106 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝑞‘3) ∈ ℝ) |
108 | 107 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝑞‘3) ∈
ℝ*) |
109 | 35, 36, 37, 85, 89, 102, 108 | smfpimioompt 39671 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3))} ∈ (𝑆 ↾t (𝐴 ∩ 𝐶))) |
110 | 33, 84, 109 | salincld 39246 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → ({𝑥 ∈ (𝐴 ∩ 𝐶) ∣ 𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1))} ∩ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3))}) ∈ (𝑆 ↾t (𝐴 ∩ 𝐶))) |
111 | 27, 110 | syl5eqelr 2693 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))} ∈ (𝑆 ↾t (𝐴 ∩ 𝐶))) |
112 | 111 | elexd 3187 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))} ∈ V) |
113 | 26, 112 | fvmpt2d 6202 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝐸‘𝑞) = {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))}) |
114 | 113 | eqcomd 2616 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))} = (𝐸‘𝑞)) |
115 | 114 | adantlr 747 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) ∧ 𝑞 ∈ 𝐾) → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))} = (𝐸‘𝑞)) |
116 | 115 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) ∧ 𝑞 ∈ 𝐾) ∧ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))) → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))} = (𝐸‘𝑞)) |
117 | 24, 116 | eleqtrd 2690 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) ∧ 𝑞 ∈ 𝐾) ∧ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))) → 𝑥 ∈ (𝐸‘𝑞)) |
118 | 117 | ex 449 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) ∧ 𝑞 ∈ 𝐾) → ((𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3))) → 𝑥 ∈ (𝐸‘𝑞))) |
119 | 118 | 3adantl3 1212 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 · 𝐷) < 𝑅) ∧ 𝑞 ∈ 𝐾) → ((𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3))) → 𝑥 ∈ (𝐸‘𝑞))) |
120 | 119 | reximdva 3000 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 · 𝐷) < 𝑅) → (∃𝑞 ∈ 𝐾 (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3))) → ∃𝑞 ∈ 𝐾 𝑥 ∈ (𝐸‘𝑞))) |
121 | 19, 120 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 · 𝐷) < 𝑅) → ∃𝑞 ∈ 𝐾 𝑥 ∈ (𝐸‘𝑞)) |
122 | | eliun 4460 |
. . . . . . 7
⊢ (𝑥 ∈ ∪ 𝑞 ∈ 𝐾 (𝐸‘𝑞) ↔ ∃𝑞 ∈ 𝐾 𝑥 ∈ (𝐸‘𝑞)) |
123 | 121, 122 | sylibr 223 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶) ∧ (𝐵 · 𝐷) < 𝑅) → 𝑥 ∈ ∪
𝑞 ∈ 𝐾 (𝐸‘𝑞)) |
124 | 123 | 3exp 1256 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∩ 𝐶) → ((𝐵 · 𝐷) < 𝑅 → 𝑥 ∈ ∪
𝑞 ∈ 𝐾 (𝐸‘𝑞)))) |
125 | 1, 124 | ralrimi 2940 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ (𝐴 ∩ 𝐶)((𝐵 · 𝐷) < 𝑅 → 𝑥 ∈ ∪
𝑞 ∈ 𝐾 (𝐸‘𝑞))) |
126 | 34 | nfci 2741 |
. . . . . 6
⊢
Ⅎ𝑥𝐾 |
127 | | nfrab1 3099 |
. . . . . . . . 9
⊢
Ⅎ𝑥{𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))} |
128 | 126, 127 | nfmpt 4674 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑞 ∈ 𝐾 ↦ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))}) |
129 | 25, 128 | nfcxfr 2749 |
. . . . . . 7
⊢
Ⅎ𝑥𝐸 |
130 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑥𝑞 |
131 | 129, 130 | nffv 6110 |
. . . . . 6
⊢
Ⅎ𝑥(𝐸‘𝑞) |
132 | 126, 131 | nfiun 4484 |
. . . . 5
⊢
Ⅎ𝑥∪ 𝑞 ∈ 𝐾 (𝐸‘𝑞) |
133 | 132 | rabssf 38334 |
. . . 4
⊢ ({𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 · 𝐷) < 𝑅} ⊆ ∪ 𝑞 ∈ 𝐾 (𝐸‘𝑞) ↔ ∀𝑥 ∈ (𝐴 ∩ 𝐶)((𝐵 · 𝐷) < 𝑅 → 𝑥 ∈ ∪
𝑞 ∈ 𝐾 (𝐸‘𝑞))) |
134 | 125, 133 | sylibr 223 |
. . 3
⊢ (𝜑 → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 · 𝐷) < 𝑅} ⊆ ∪ 𝑞 ∈ 𝐾 (𝐸‘𝑞)) |
135 | | ssrab2 3650 |
. . . . . . 7
⊢ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))} ⊆ (𝐴 ∩ 𝐶) |
136 | 113, 135 | syl6eqss 3618 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝐸‘𝑞) ⊆ (𝐴 ∩ 𝐶)) |
137 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐾) ∧ 𝑥 ∈ (𝐸‘𝑞)) → 𝑥 ∈ (𝐸‘𝑞)) |
138 | 113 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐾) ∧ 𝑥 ∈ (𝐸‘𝑞)) → (𝐸‘𝑞) = {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))}) |
139 | 137, 138 | eleqtrd 2690 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐾) ∧ 𝑥 ∈ (𝐸‘𝑞)) → 𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))}) |
140 | | rabidim2 38313 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))} → (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))) |
141 | 139, 140 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐾) ∧ 𝑥 ∈ (𝐸‘𝑞)) → (𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)))) |
142 | 141 | simprd 478 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐾) ∧ 𝑥 ∈ (𝐸‘𝑞)) → 𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3))) |
143 | 141 | simpld 474 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐾) ∧ 𝑥 ∈ (𝐸‘𝑞)) → 𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1))) |
144 | 49, 4 | syl6eleq 2698 |
. . . . . . . . . . . 12
⊢ (𝑞 ∈ 𝐾 → 𝑞 ∈ {𝑞 ∈ (ℚ ↑𝑚
(0...3)) ∣ ∀𝑢
∈ ((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅}) |
145 | | rabidim2 38313 |
. . . . . . . . . . . 12
⊢ (𝑞 ∈ {𝑞 ∈ (ℚ ↑𝑚
(0...3)) ∣ ∀𝑢
∈ ((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅} → ∀𝑢 ∈ ((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅) |
146 | 144, 145 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑞 ∈ 𝐾 → ∀𝑢 ∈ ((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅) |
147 | 146 | ad2antlr 759 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐾) ∧ 𝑥 ∈ (𝐸‘𝑞)) → ∀𝑢 ∈ ((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅) |
148 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝐵 → (𝑢 · 𝑣) = (𝐵 · 𝑣)) |
149 | 148 | breq1d 4593 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝐵 → ((𝑢 · 𝑣) < 𝑅 ↔ (𝐵 · 𝑣) < 𝑅)) |
150 | 149 | ralbidv 2969 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝐵 → (∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅 ↔ ∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝐵 · 𝑣) < 𝑅)) |
151 | 150 | rspcva 3280 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ ∀𝑢 ∈ ((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝑅) → ∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝐵 · 𝑣) < 𝑅) |
152 | 143, 147,
151 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐾) ∧ 𝑥 ∈ (𝐸‘𝑞)) → ∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝐵 · 𝑣) < 𝑅) |
153 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝐷 → (𝐵 · 𝑣) = (𝐵 · 𝐷)) |
154 | 153 | breq1d 4593 |
. . . . . . . . . 10
⊢ (𝑣 = 𝐷 → ((𝐵 · 𝑣) < 𝑅 ↔ (𝐵 · 𝐷) < 𝑅)) |
155 | 154 | rspcva 3280 |
. . . . . . . . 9
⊢ ((𝐷 ∈ ((𝑞‘2)(,)(𝑞‘3)) ∧ ∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝐵 · 𝑣) < 𝑅) → (𝐵 · 𝐷) < 𝑅) |
156 | 142, 152,
155 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐾) ∧ 𝑥 ∈ (𝐸‘𝑞)) → (𝐵 · 𝐷) < 𝑅) |
157 | 156 | ex 449 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝑥 ∈ (𝐸‘𝑞) → (𝐵 · 𝐷) < 𝑅)) |
158 | 35, 157 | ralrimi 2940 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → ∀𝑥 ∈ (𝐸‘𝑞)(𝐵 · 𝐷) < 𝑅) |
159 | 136, 158 | jca 553 |
. . . . 5
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → ((𝐸‘𝑞) ⊆ (𝐴 ∩ 𝐶) ∧ ∀𝑥 ∈ (𝐸‘𝑞)(𝐵 · 𝐷) < 𝑅)) |
160 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑥(𝐴 ∩ 𝐶) |
161 | 131, 160 | ssrabf 38329 |
. . . . 5
⊢ ((𝐸‘𝑞) ⊆ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 · 𝐷) < 𝑅} ↔ ((𝐸‘𝑞) ⊆ (𝐴 ∩ 𝐶) ∧ ∀𝑥 ∈ (𝐸‘𝑞)(𝐵 · 𝐷) < 𝑅)) |
162 | 159, 161 | sylibr 223 |
. . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝐸‘𝑞) ⊆ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 · 𝐷) < 𝑅}) |
163 | 162 | iunssd 38299 |
. . 3
⊢ (𝜑 → ∪ 𝑞 ∈ 𝐾 (𝐸‘𝑞) ⊆ {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 · 𝐷) < 𝑅}) |
164 | 134, 163 | eqssd 3585 |
. 2
⊢ (𝜑 → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 · 𝐷) < 𝑅} = ∪
𝑞 ∈ 𝐾 (𝐸‘𝑞)) |
165 | | ovex 6577 |
. . . . . . 7
⊢ (ℚ
↑𝑚 (0...3)) ∈ V |
166 | | ssdomg 7887 |
. . . . . . 7
⊢ ((ℚ
↑𝑚 (0...3)) ∈ V → (𝐾 ⊆ (ℚ ↑𝑚
(0...3)) → 𝐾 ≼
(ℚ ↑𝑚 (0...3)))) |
167 | 165, 166 | ax-mp 5 |
. . . . . 6
⊢ (𝐾 ⊆ (ℚ
↑𝑚 (0...3)) → 𝐾 ≼ (ℚ ↑𝑚
(0...3))) |
168 | 43, 167 | ax-mp 5 |
. . . . 5
⊢ 𝐾 ≼ (ℚ
↑𝑚 (0...3)) |
169 | | qct 38519 |
. . . . . . . 8
⊢ ℚ
≼ ω |
170 | 169 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ ℚ ≼ ω) |
171 | | fzfid 12634 |
. . . . . . 7
⊢ (⊤
→ (0...3) ∈ Fin) |
172 | 170, 171 | mpct 38388 |
. . . . . 6
⊢ (⊤
→ (ℚ ↑𝑚 (0...3)) ≼
ω) |
173 | 172 | trud 1484 |
. . . . 5
⊢ (ℚ
↑𝑚 (0...3)) ≼ ω |
174 | | domtr 7895 |
. . . . 5
⊢ ((𝐾 ≼ (ℚ
↑𝑚 (0...3)) ∧ (ℚ ↑𝑚
(0...3)) ≼ ω) → 𝐾 ≼ ω) |
175 | 168, 173,
174 | mp2an 704 |
. . . 4
⊢ 𝐾 ≼
ω |
176 | 175 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐾 ≼ ω) |
177 | 111, 25 | fmptd 6292 |
. . . 4
⊢ (𝜑 → 𝐸:𝐾⟶(𝑆 ↾t (𝐴 ∩ 𝐶))) |
178 | 177 | ffvelrnda 6267 |
. . 3
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾) → (𝐸‘𝑞) ∈ (𝑆 ↾t (𝐴 ∩ 𝐶))) |
179 | 32, 176, 178 | saliuncl 39218 |
. 2
⊢ (𝜑 → ∪ 𝑞 ∈ 𝐾 (𝐸‘𝑞) ∈ (𝑆 ↾t (𝐴 ∩ 𝐶))) |
180 | 164, 179 | eqeltrd 2688 |
1
⊢ (𝜑 → {𝑥 ∈ (𝐴 ∩ 𝐶) ∣ (𝐵 · 𝐷) < 𝑅} ∈ (𝑆 ↾t (𝐴 ∩ 𝐶))) |