Proof of Theorem smfmullem2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | smfmullem2.p | . . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ ℚ) | 
| 2 |  | smfmullem2.r | . . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ ℚ) | 
| 3 |  | smfmullem2.s | . . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ ℚ) | 
| 4 |  | smfmullem2.z | . . . . . . . 8
⊢ (𝜑 → 𝑍 ∈ ℚ) | 
| 5 | 1, 2, 3, 4 | s4cld 14913 | . . . . . . 7
⊢ (𝜑 → 〈“𝑃𝑅𝑆𝑍”〉 ∈ Word
ℚ) | 
| 6 |  | s4len 14939 | . . . . . . . 8
⊢
(♯‘〈“𝑃𝑅𝑆𝑍”〉) = 4 | 
| 7 | 6 | a1i 11 | . . . . . . 7
⊢ (𝜑 →
(♯‘〈“𝑃𝑅𝑆𝑍”〉) = 4) | 
| 8 | 5, 7 | jca 511 | . . . . . 6
⊢ (𝜑 → (〈“𝑃𝑅𝑆𝑍”〉 ∈ Word ℚ ∧
(♯‘〈“𝑃𝑅𝑆𝑍”〉) = 4)) | 
| 9 |  | qex 13004 | . . . . . . . 8
⊢ ℚ
∈ V | 
| 10 | 9 | a1i 11 | . . . . . . 7
⊢ (𝜑 → ℚ ∈
V) | 
| 11 |  | 4nn0 12547 | . . . . . . . 8
⊢ 4 ∈
ℕ0 | 
| 12 | 11 | a1i 11 | . . . . . . 7
⊢ (𝜑 → 4 ∈
ℕ0) | 
| 13 |  | wrdmap 14585 | . . . . . . 7
⊢ ((ℚ
∈ V ∧ 4 ∈ ℕ0) → ((〈“𝑃𝑅𝑆𝑍”〉 ∈ Word ℚ ∧
(♯‘〈“𝑃𝑅𝑆𝑍”〉) = 4) ↔
〈“𝑃𝑅𝑆𝑍”〉 ∈ (ℚ
↑m (0..^4)))) | 
| 14 | 10, 12, 13 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → ((〈“𝑃𝑅𝑆𝑍”〉 ∈ Word ℚ ∧
(♯‘〈“𝑃𝑅𝑆𝑍”〉) = 4) ↔
〈“𝑃𝑅𝑆𝑍”〉 ∈ (ℚ
↑m (0..^4)))) | 
| 15 | 8, 14 | mpbid 232 | . . . . 5
⊢ (𝜑 → 〈“𝑃𝑅𝑆𝑍”〉 ∈ (ℚ
↑m (0..^4))) | 
| 16 |  | 3z 12652 | . . . . . . . . . 10
⊢ 3 ∈
ℤ | 
| 17 |  | fzval3 13774 | . . . . . . . . . 10
⊢ (3 ∈
ℤ → (0...3) = (0..^(3 + 1))) | 
| 18 | 16, 17 | ax-mp 5 | . . . . . . . . 9
⊢ (0...3) =
(0..^(3 + 1)) | 
| 19 |  | 3p1e4 12412 | . . . . . . . . . 10
⊢ (3 + 1) =
4 | 
| 20 | 19 | oveq2i 7443 | . . . . . . . . 9
⊢ (0..^(3 +
1)) = (0..^4) | 
| 21 | 18, 20 | eqtri 2764 | . . . . . . . 8
⊢ (0...3) =
(0..^4) | 
| 22 | 21 | eqcomi 2745 | . . . . . . 7
⊢ (0..^4) =
(0...3) | 
| 23 | 22 | a1i 11 | . . . . . 6
⊢ (𝜑 → (0..^4) =
(0...3)) | 
| 24 | 23 | oveq2d 7448 | . . . . 5
⊢ (𝜑 → (ℚ
↑m (0..^4)) = (ℚ ↑m
(0...3))) | 
| 25 | 15, 24 | eleqtrd 2842 | . . . 4
⊢ (𝜑 → 〈“𝑃𝑅𝑆𝑍”〉 ∈ (ℚ
↑m (0...3))) | 
| 26 |  | simpr 484 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘0)(,)(〈“𝑃𝑅𝑆𝑍”〉‘1))) → 𝑢 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘0)(,)(〈“𝑃𝑅𝑆𝑍”〉‘1))) | 
| 27 |  | s4fv0 14935 | . . . . . . . . . 10
⊢ (𝑃 ∈ ℚ →
(〈“𝑃𝑅𝑆𝑍”〉‘0) = 𝑃) | 
| 28 | 1, 27 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (〈“𝑃𝑅𝑆𝑍”〉‘0) = 𝑃) | 
| 29 |  | s4fv1 14936 | . . . . . . . . . 10
⊢ (𝑅 ∈ ℚ →
(〈“𝑃𝑅𝑆𝑍”〉‘1) = 𝑅) | 
| 30 | 2, 29 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (〈“𝑃𝑅𝑆𝑍”〉‘1) = 𝑅) | 
| 31 | 28, 30 | oveq12d 7450 | . . . . . . . 8
⊢ (𝜑 → ((〈“𝑃𝑅𝑆𝑍”〉‘0)(,)(〈“𝑃𝑅𝑆𝑍”〉‘1)) = (𝑃(,)𝑅)) | 
| 32 | 31 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘0)(,)(〈“𝑃𝑅𝑆𝑍”〉‘1))) →
((〈“𝑃𝑅𝑆𝑍”〉‘0)(,)(〈“𝑃𝑅𝑆𝑍”〉‘1)) = (𝑃(,)𝑅)) | 
| 33 | 26, 32 | eleqtrd 2842 | . . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘0)(,)(〈“𝑃𝑅𝑆𝑍”〉‘1))) → 𝑢 ∈ (𝑃(,)𝑅)) | 
| 34 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘2)(,)(〈“𝑃𝑅𝑆𝑍”〉‘3))) → 𝑣 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘2)(,)(〈“𝑃𝑅𝑆𝑍”〉‘3))) | 
| 35 |  | s4fv2 14937 | . . . . . . . . . . . . . 14
⊢ (𝑆 ∈ ℚ →
(〈“𝑃𝑅𝑆𝑍”〉‘2) = 𝑆) | 
| 36 | 3, 35 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (〈“𝑃𝑅𝑆𝑍”〉‘2) = 𝑆) | 
| 37 |  | s4fv3 14938 | . . . . . . . . . . . . . 14
⊢ (𝑍 ∈ ℚ →
(〈“𝑃𝑅𝑆𝑍”〉‘3) = 𝑍) | 
| 38 | 4, 37 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (〈“𝑃𝑅𝑆𝑍”〉‘3) = 𝑍) | 
| 39 | 36, 38 | oveq12d 7450 | . . . . . . . . . . . 12
⊢ (𝜑 → ((〈“𝑃𝑅𝑆𝑍”〉‘2)(,)(〈“𝑃𝑅𝑆𝑍”〉‘3)) = (𝑆(,)𝑍)) | 
| 40 | 39 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘2)(,)(〈“𝑃𝑅𝑆𝑍”〉‘3))) →
((〈“𝑃𝑅𝑆𝑍”〉‘2)(,)(〈“𝑃𝑅𝑆𝑍”〉‘3)) = (𝑆(,)𝑍)) | 
| 41 | 34, 40 | eleqtrd 2842 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘2)(,)(〈“𝑃𝑅𝑆𝑍”〉‘3))) → 𝑣 ∈ (𝑆(,)𝑍)) | 
| 42 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ (𝑆(,)𝑍)) → 𝑣 ∈ (𝑆(,)𝑍)) | 
| 43 | 41, 42 | syldan 591 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘2)(,)(〈“𝑃𝑅𝑆𝑍”〉‘3))) → 𝑣 ∈ (𝑆(,)𝑍)) | 
| 44 | 43 | adantlr 715 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ (𝑃(,)𝑅)) ∧ 𝑣 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘2)(,)(〈“𝑃𝑅𝑆𝑍”〉‘3))) → 𝑣 ∈ (𝑆(,)𝑍)) | 
| 45 |  | smfmullem2.a | . . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 46 | 45 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ (𝑃(,)𝑅)) ∧ 𝑣 ∈ (𝑆(,)𝑍)) → 𝐴 ∈ ℝ) | 
| 47 |  | smfmullem2.u | . . . . . . . . . 10
⊢ (𝜑 → 𝑈 ∈ ℝ) | 
| 48 | 47 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ (𝑃(,)𝑅)) ∧ 𝑣 ∈ (𝑆(,)𝑍)) → 𝑈 ∈ ℝ) | 
| 49 |  | smfmullem2.v | . . . . . . . . . 10
⊢ (𝜑 → 𝑉 ∈ ℝ) | 
| 50 | 49 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ (𝑃(,)𝑅)) ∧ 𝑣 ∈ (𝑆(,)𝑍)) → 𝑉 ∈ ℝ) | 
| 51 |  | smfmullem2.l | . . . . . . . . . 10
⊢ (𝜑 → (𝑈 · 𝑉) < 𝐴) | 
| 52 | 51 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ (𝑃(,)𝑅)) ∧ 𝑣 ∈ (𝑆(,)𝑍)) → (𝑈 · 𝑉) < 𝐴) | 
| 53 |  | smfmullem2.x | . . . . . . . . 9
⊢ 𝑋 = ((𝐴 − (𝑈 · 𝑉)) / (1 + ((abs‘𝑈) + (abs‘𝑉)))) | 
| 54 |  | smfmullem2.y | . . . . . . . . 9
⊢ 𝑌 = if(1 ≤ 𝑋, 1, 𝑋) | 
| 55 |  | smfmullem2.p2 | . . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ((𝑈 − 𝑌)(,)𝑈)) | 
| 56 | 55 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ (𝑃(,)𝑅)) ∧ 𝑣 ∈ (𝑆(,)𝑍)) → 𝑃 ∈ ((𝑈 − 𝑌)(,)𝑈)) | 
| 57 |  | smfmullem2.42 | . . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ (𝑈(,)(𝑈 + 𝑌))) | 
| 58 | 57 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ (𝑃(,)𝑅)) ∧ 𝑣 ∈ (𝑆(,)𝑍)) → 𝑅 ∈ (𝑈(,)(𝑈 + 𝑌))) | 
| 59 |  | smfmullem2.w2 | . . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ ((𝑉 − 𝑌)(,)𝑉)) | 
| 60 | 59 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ (𝑃(,)𝑅)) ∧ 𝑣 ∈ (𝑆(,)𝑍)) → 𝑆 ∈ ((𝑉 − 𝑌)(,)𝑉)) | 
| 61 |  | smfmullem2.z2 | . . . . . . . . . 10
⊢ (𝜑 → 𝑍 ∈ (𝑉(,)(𝑉 + 𝑌))) | 
| 62 | 61 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ (𝑃(,)𝑅)) ∧ 𝑣 ∈ (𝑆(,)𝑍)) → 𝑍 ∈ (𝑉(,)(𝑉 + 𝑌))) | 
| 63 |  | simplr 768 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ (𝑃(,)𝑅)) ∧ 𝑣 ∈ (𝑆(,)𝑍)) → 𝑢 ∈ (𝑃(,)𝑅)) | 
| 64 |  | simpr 484 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ (𝑃(,)𝑅)) ∧ 𝑣 ∈ (𝑆(,)𝑍)) → 𝑣 ∈ (𝑆(,)𝑍)) | 
| 65 | 46, 48, 50, 52, 53, 54, 56, 58, 60, 62, 63, 64 | smfmullem1 46811 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ (𝑃(,)𝑅)) ∧ 𝑣 ∈ (𝑆(,)𝑍)) → (𝑢 · 𝑣) < 𝐴) | 
| 66 | 44, 65 | syldan 591 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ (𝑃(,)𝑅)) ∧ 𝑣 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘2)(,)(〈“𝑃𝑅𝑆𝑍”〉‘3))) → (𝑢 · 𝑣) < 𝐴) | 
| 67 | 66 | ralrimiva 3145 | . . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ (𝑃(,)𝑅)) → ∀𝑣 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘2)(,)(〈“𝑃𝑅𝑆𝑍”〉‘3))(𝑢 · 𝑣) < 𝐴) | 
| 68 | 33, 67 | syldan 591 | . . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘0)(,)(〈“𝑃𝑅𝑆𝑍”〉‘1))) →
∀𝑣 ∈
((〈“𝑃𝑅𝑆𝑍”〉‘2)(,)(〈“𝑃𝑅𝑆𝑍”〉‘3))(𝑢 · 𝑣) < 𝐴) | 
| 69 | 68 | ralrimiva 3145 | . . . 4
⊢ (𝜑 → ∀𝑢 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘0)(,)(〈“𝑃𝑅𝑆𝑍”〉‘1))∀𝑣 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘2)(,)(〈“𝑃𝑅𝑆𝑍”〉‘3))(𝑢 · 𝑣) < 𝐴) | 
| 70 | 25, 69 | jca 511 | . . 3
⊢ (𝜑 → (〈“𝑃𝑅𝑆𝑍”〉 ∈ (ℚ
↑m (0...3)) ∧ ∀𝑢 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘0)(,)(〈“𝑃𝑅𝑆𝑍”〉‘1))∀𝑣 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘2)(,)(〈“𝑃𝑅𝑆𝑍”〉‘3))(𝑢 · 𝑣) < 𝐴)) | 
| 71 |  | fveq1 6904 | . . . . . . 7
⊢ (𝑞 = 〈“𝑃𝑅𝑆𝑍”〉 → (𝑞‘0) = (〈“𝑃𝑅𝑆𝑍”〉‘0)) | 
| 72 |  | fveq1 6904 | . . . . . . 7
⊢ (𝑞 = 〈“𝑃𝑅𝑆𝑍”〉 → (𝑞‘1) = (〈“𝑃𝑅𝑆𝑍”〉‘1)) | 
| 73 | 71, 72 | oveq12d 7450 | . . . . . 6
⊢ (𝑞 = 〈“𝑃𝑅𝑆𝑍”〉 → ((𝑞‘0)(,)(𝑞‘1)) = ((〈“𝑃𝑅𝑆𝑍”〉‘0)(,)(〈“𝑃𝑅𝑆𝑍”〉‘1))) | 
| 74 | 73 | raleqdv 3325 | . . . . 5
⊢ (𝑞 = 〈“𝑃𝑅𝑆𝑍”〉 → (∀𝑢 ∈ ((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝐴 ↔ ∀𝑢 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘0)(,)(〈“𝑃𝑅𝑆𝑍”〉‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝐴)) | 
| 75 |  | fveq1 6904 | . . . . . . . 8
⊢ (𝑞 = 〈“𝑃𝑅𝑆𝑍”〉 → (𝑞‘2) = (〈“𝑃𝑅𝑆𝑍”〉‘2)) | 
| 76 |  | fveq1 6904 | . . . . . . . 8
⊢ (𝑞 = 〈“𝑃𝑅𝑆𝑍”〉 → (𝑞‘3) = (〈“𝑃𝑅𝑆𝑍”〉‘3)) | 
| 77 | 75, 76 | oveq12d 7450 | . . . . . . 7
⊢ (𝑞 = 〈“𝑃𝑅𝑆𝑍”〉 → ((𝑞‘2)(,)(𝑞‘3)) = ((〈“𝑃𝑅𝑆𝑍”〉‘2)(,)(〈“𝑃𝑅𝑆𝑍”〉‘3))) | 
| 78 | 77 | raleqdv 3325 | . . . . . 6
⊢ (𝑞 = 〈“𝑃𝑅𝑆𝑍”〉 → (∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝐴 ↔ ∀𝑣 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘2)(,)(〈“𝑃𝑅𝑆𝑍”〉‘3))(𝑢 · 𝑣) < 𝐴)) | 
| 79 | 78 | ralbidv 3177 | . . . . 5
⊢ (𝑞 = 〈“𝑃𝑅𝑆𝑍”〉 → (∀𝑢 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘0)(,)(〈“𝑃𝑅𝑆𝑍”〉‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝐴 ↔ ∀𝑢 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘0)(,)(〈“𝑃𝑅𝑆𝑍”〉‘1))∀𝑣 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘2)(,)(〈“𝑃𝑅𝑆𝑍”〉‘3))(𝑢 · 𝑣) < 𝐴)) | 
| 80 | 74, 79 | bitrd 279 | . . . 4
⊢ (𝑞 = 〈“𝑃𝑅𝑆𝑍”〉 → (∀𝑢 ∈ ((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝐴 ↔ ∀𝑢 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘0)(,)(〈“𝑃𝑅𝑆𝑍”〉‘1))∀𝑣 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘2)(,)(〈“𝑃𝑅𝑆𝑍”〉‘3))(𝑢 · 𝑣) < 𝐴)) | 
| 81 |  | smfmullem2.k | . . . 4
⊢ 𝐾 = {𝑞 ∈ (ℚ ↑m (0...3))
∣ ∀𝑢 ∈
((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝐴} | 
| 82 | 80, 81 | elrab2 3694 | . . 3
⊢
(〈“𝑃𝑅𝑆𝑍”〉 ∈ 𝐾 ↔ (〈“𝑃𝑅𝑆𝑍”〉 ∈ (ℚ
↑m (0...3)) ∧ ∀𝑢 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘0)(,)(〈“𝑃𝑅𝑆𝑍”〉‘1))∀𝑣 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘2)(,)(〈“𝑃𝑅𝑆𝑍”〉‘3))(𝑢 · 𝑣) < 𝐴)) | 
| 83 | 70, 82 | sylibr 234 | . 2
⊢ (𝜑 → 〈“𝑃𝑅𝑆𝑍”〉 ∈ 𝐾) | 
| 84 |  | qssre 13002 | . . . . . . 7
⊢ ℚ
⊆ ℝ | 
| 85 | 84, 1 | sselid 3980 | . . . . . 6
⊢ (𝜑 → 𝑃 ∈ ℝ) | 
| 86 | 85 | rexrd 11312 | . . . . 5
⊢ (𝜑 → 𝑃 ∈
ℝ*) | 
| 87 | 84, 2 | sselid 3980 | . . . . . 6
⊢ (𝜑 → 𝑅 ∈ ℝ) | 
| 88 | 87 | rexrd 11312 | . . . . 5
⊢ (𝜑 → 𝑅 ∈
ℝ*) | 
| 89 | 54 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → 𝑌 = if(1 ≤ 𝑋, 1, 𝑋)) | 
| 90 |  | 1rp 13039 | . . . . . . . . . . . 12
⊢ 1 ∈
ℝ+ | 
| 91 | 90 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℝ+) | 
| 92 | 53 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 = ((𝐴 − (𝑈 · 𝑉)) / (1 + ((abs‘𝑈) + (abs‘𝑉))))) | 
| 93 | 47, 49 | remulcld 11292 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑈 · 𝑉) ∈ ℝ) | 
| 94 |  | difrp 13074 | . . . . . . . . . . . . . . 15
⊢ (((𝑈 · 𝑉) ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((𝑈 · 𝑉) < 𝐴 ↔ (𝐴 − (𝑈 · 𝑉)) ∈
ℝ+)) | 
| 95 | 93, 45, 94 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑈 · 𝑉) < 𝐴 ↔ (𝐴 − (𝑈 · 𝑉)) ∈
ℝ+)) | 
| 96 | 51, 95 | mpbid 232 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 − (𝑈 · 𝑉)) ∈
ℝ+) | 
| 97 |  | 1red 11263 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈
ℝ) | 
| 98 | 47 | recnd 11290 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑈 ∈ ℂ) | 
| 99 | 98 | abscld 15476 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (abs‘𝑈) ∈
ℝ) | 
| 100 | 49 | recnd 11290 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑉 ∈ ℂ) | 
| 101 | 100 | abscld 15476 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (abs‘𝑉) ∈
ℝ) | 
| 102 | 99, 101 | readdcld 11291 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((abs‘𝑈) + (abs‘𝑉)) ∈ ℝ) | 
| 103 | 97, 102 | readdcld 11291 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (1 + ((abs‘𝑈) + (abs‘𝑉))) ∈ ℝ) | 
| 104 |  | 0re 11264 | . . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ | 
| 105 | 104 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ∈
ℝ) | 
| 106 | 91 | rpgt0d 13081 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 < 1) | 
| 107 | 98 | absge0d 15484 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 0 ≤ (abs‘𝑈)) | 
| 108 | 100 | absge0d 15484 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 0 ≤ (abs‘𝑉)) | 
| 109 | 99, 101 | addge01d 11852 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (0 ≤ (abs‘𝑉) ↔ (abs‘𝑈) ≤ ((abs‘𝑈) + (abs‘𝑉)))) | 
| 110 | 108, 109 | mpbid 232 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (abs‘𝑈) ≤ ((abs‘𝑈) + (abs‘𝑉))) | 
| 111 | 105, 99, 102, 107, 110 | letrd 11419 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 ≤ ((abs‘𝑈) + (abs‘𝑉))) | 
| 112 | 97, 102 | addge01d 11852 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (0 ≤ ((abs‘𝑈) + (abs‘𝑉)) ↔ 1 ≤ (1 + ((abs‘𝑈) + (abs‘𝑉))))) | 
| 113 | 111, 112 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ≤ (1 +
((abs‘𝑈) +
(abs‘𝑉)))) | 
| 114 | 105, 97, 103, 106, 113 | ltletrd 11422 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < (1 +
((abs‘𝑈) +
(abs‘𝑉)))) | 
| 115 | 103, 114 | elrpd 13075 | . . . . . . . . . . . . 13
⊢ (𝜑 → (1 + ((abs‘𝑈) + (abs‘𝑉))) ∈
ℝ+) | 
| 116 | 96, 115 | rpdivcld 13095 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴 − (𝑈 · 𝑉)) / (1 + ((abs‘𝑈) + (abs‘𝑉)))) ∈
ℝ+) | 
| 117 | 92, 116 | eqeltrd 2840 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈
ℝ+) | 
| 118 | 91, 117 | ifcld 4571 | . . . . . . . . . 10
⊢ (𝜑 → if(1 ≤ 𝑋, 1, 𝑋) ∈
ℝ+) | 
| 119 | 89, 118 | eqeltrd 2840 | . . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈
ℝ+) | 
| 120 | 119 | rpred 13078 | . . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ ℝ) | 
| 121 | 47, 120 | resubcld 11692 | . . . . . . 7
⊢ (𝜑 → (𝑈 − 𝑌) ∈ ℝ) | 
| 122 | 121 | rexrd 11312 | . . . . . 6
⊢ (𝜑 → (𝑈 − 𝑌) ∈
ℝ*) | 
| 123 | 47 | rexrd 11312 | . . . . . 6
⊢ (𝜑 → 𝑈 ∈
ℝ*) | 
| 124 |  | iooltub 45528 | . . . . . 6
⊢ (((𝑈 − 𝑌) ∈ ℝ* ∧ 𝑈 ∈ ℝ*
∧ 𝑃 ∈ ((𝑈 − 𝑌)(,)𝑈)) → 𝑃 < 𝑈) | 
| 125 | 122, 123,
55, 124 | syl3anc 1372 | . . . . 5
⊢ (𝜑 → 𝑃 < 𝑈) | 
| 126 | 47, 120 | readdcld 11291 | . . . . . . 7
⊢ (𝜑 → (𝑈 + 𝑌) ∈ ℝ) | 
| 127 | 126 | rexrd 11312 | . . . . . 6
⊢ (𝜑 → (𝑈 + 𝑌) ∈
ℝ*) | 
| 128 |  | ioogtlb 45513 | . . . . . 6
⊢ ((𝑈 ∈ ℝ*
∧ (𝑈 + 𝑌) ∈ ℝ*
∧ 𝑅 ∈ (𝑈(,)(𝑈 + 𝑌))) → 𝑈 < 𝑅) | 
| 129 | 123, 127,
57, 128 | syl3anc 1372 | . . . . 5
⊢ (𝜑 → 𝑈 < 𝑅) | 
| 130 | 86, 88, 47, 125, 129 | eliood 45516 | . . . 4
⊢ (𝜑 → 𝑈 ∈ (𝑃(,)𝑅)) | 
| 131 | 31 | eqcomd 2742 | . . . 4
⊢ (𝜑 → (𝑃(,)𝑅) = ((〈“𝑃𝑅𝑆𝑍”〉‘0)(,)(〈“𝑃𝑅𝑆𝑍”〉‘1))) | 
| 132 | 130, 131 | eleqtrd 2842 | . . 3
⊢ (𝜑 → 𝑈 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘0)(,)(〈“𝑃𝑅𝑆𝑍”〉‘1))) | 
| 133 | 84, 3 | sselid 3980 | . . . . . 6
⊢ (𝜑 → 𝑆 ∈ ℝ) | 
| 134 | 133 | rexrd 11312 | . . . . 5
⊢ (𝜑 → 𝑆 ∈
ℝ*) | 
| 135 | 84, 4 | sselid 3980 | . . . . . 6
⊢ (𝜑 → 𝑍 ∈ ℝ) | 
| 136 | 135 | rexrd 11312 | . . . . 5
⊢ (𝜑 → 𝑍 ∈
ℝ*) | 
| 137 | 49, 120 | resubcld 11692 | . . . . . . 7
⊢ (𝜑 → (𝑉 − 𝑌) ∈ ℝ) | 
| 138 | 137 | rexrd 11312 | . . . . . 6
⊢ (𝜑 → (𝑉 − 𝑌) ∈
ℝ*) | 
| 139 | 49 | rexrd 11312 | . . . . . 6
⊢ (𝜑 → 𝑉 ∈
ℝ*) | 
| 140 |  | iooltub 45528 | . . . . . 6
⊢ (((𝑉 − 𝑌) ∈ ℝ* ∧ 𝑉 ∈ ℝ*
∧ 𝑆 ∈ ((𝑉 − 𝑌)(,)𝑉)) → 𝑆 < 𝑉) | 
| 141 | 138, 139,
59, 140 | syl3anc 1372 | . . . . 5
⊢ (𝜑 → 𝑆 < 𝑉) | 
| 142 | 49, 120 | readdcld 11291 | . . . . . . 7
⊢ (𝜑 → (𝑉 + 𝑌) ∈ ℝ) | 
| 143 | 142 | rexrd 11312 | . . . . . 6
⊢ (𝜑 → (𝑉 + 𝑌) ∈
ℝ*) | 
| 144 |  | ioogtlb 45513 | . . . . . 6
⊢ ((𝑉 ∈ ℝ*
∧ (𝑉 + 𝑌) ∈ ℝ*
∧ 𝑍 ∈ (𝑉(,)(𝑉 + 𝑌))) → 𝑉 < 𝑍) | 
| 145 | 139, 143,
61, 144 | syl3anc 1372 | . . . . 5
⊢ (𝜑 → 𝑉 < 𝑍) | 
| 146 | 134, 136,
49, 141, 145 | eliood 45516 | . . . 4
⊢ (𝜑 → 𝑉 ∈ (𝑆(,)𝑍)) | 
| 147 | 39 | eqcomd 2742 | . . . 4
⊢ (𝜑 → (𝑆(,)𝑍) = ((〈“𝑃𝑅𝑆𝑍”〉‘2)(,)(〈“𝑃𝑅𝑆𝑍”〉‘3))) | 
| 148 | 146, 147 | eleqtrd 2842 | . . 3
⊢ (𝜑 → 𝑉 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘2)(,)(〈“𝑃𝑅𝑆𝑍”〉‘3))) | 
| 149 | 132, 148 | jca 511 | . 2
⊢ (𝜑 → (𝑈 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘0)(,)(〈“𝑃𝑅𝑆𝑍”〉‘1)) ∧ 𝑉 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘2)(,)(〈“𝑃𝑅𝑆𝑍”〉‘3)))) | 
| 150 |  | nfv 1913 | . . 3
⊢
Ⅎ𝑞(𝑈 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘0)(,)(〈“𝑃𝑅𝑆𝑍”〉‘1)) ∧ 𝑉 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘2)(,)(〈“𝑃𝑅𝑆𝑍”〉‘3))) | 
| 151 |  | nfcv 2904 | . . 3
⊢
Ⅎ𝑞〈“𝑃𝑅𝑆𝑍”〉 | 
| 152 |  | nfrab1 3456 | . . . 4
⊢
Ⅎ𝑞{𝑞 ∈ (ℚ ↑m (0...3))
∣ ∀𝑢 ∈
((𝑞‘0)(,)(𝑞‘1))∀𝑣 ∈ ((𝑞‘2)(,)(𝑞‘3))(𝑢 · 𝑣) < 𝐴} | 
| 153 | 81, 152 | nfcxfr 2902 | . . 3
⊢
Ⅎ𝑞𝐾 | 
| 154 | 73 | eleq2d 2826 | . . . 4
⊢ (𝑞 = 〈“𝑃𝑅𝑆𝑍”〉 → (𝑈 ∈ ((𝑞‘0)(,)(𝑞‘1)) ↔ 𝑈 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘0)(,)(〈“𝑃𝑅𝑆𝑍”〉‘1)))) | 
| 155 | 77 | eleq2d 2826 | . . . 4
⊢ (𝑞 = 〈“𝑃𝑅𝑆𝑍”〉 → (𝑉 ∈ ((𝑞‘2)(,)(𝑞‘3)) ↔ 𝑉 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘2)(,)(〈“𝑃𝑅𝑆𝑍”〉‘3)))) | 
| 156 | 154, 155 | anbi12d 632 | . . 3
⊢ (𝑞 = 〈“𝑃𝑅𝑆𝑍”〉 → ((𝑈 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝑉 ∈ ((𝑞‘2)(,)(𝑞‘3))) ↔ (𝑈 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘0)(,)(〈“𝑃𝑅𝑆𝑍”〉‘1)) ∧ 𝑉 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘2)(,)(〈“𝑃𝑅𝑆𝑍”〉‘3))))) | 
| 157 | 150, 151,
153, 156 | rspcef 45082 | . 2
⊢
((〈“𝑃𝑅𝑆𝑍”〉 ∈ 𝐾 ∧ (𝑈 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘0)(,)(〈“𝑃𝑅𝑆𝑍”〉‘1)) ∧ 𝑉 ∈ ((〈“𝑃𝑅𝑆𝑍”〉‘2)(,)(〈“𝑃𝑅𝑆𝑍”〉‘3)))) →
∃𝑞 ∈ 𝐾 (𝑈 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝑉 ∈ ((𝑞‘2)(,)(𝑞‘3)))) | 
| 158 | 83, 149, 157 | syl2anc 584 | 1
⊢ (𝜑 → ∃𝑞 ∈ 𝐾 (𝑈 ∈ ((𝑞‘0)(,)(𝑞‘1)) ∧ 𝑉 ∈ ((𝑞‘2)(,)(𝑞‘3)))) |