Proof of Theorem xlt2addrd
Step | Hyp | Ref
| Expression |
1 | | xlt2addrd.1 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | 1 | rexrd 10782 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
3 | 2 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → 𝐴 ∈
ℝ*) |
4 | | 0xr 10779 |
. . . . 5
⊢ 0 ∈
ℝ* |
5 | 4 | a1i 11 |
. . . 4
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → 0 ∈
ℝ*) |
6 | | xaddid1 12730 |
. . . . . 6
⊢ (𝐴 ∈ ℝ*
→ (𝐴
+𝑒 0) = 𝐴) |
7 | 6 | eqcomd 2745 |
. . . . 5
⊢ (𝐴 ∈ ℝ*
→ 𝐴 = (𝐴 +𝑒
0)) |
8 | 3, 7 | syl 17 |
. . . 4
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → 𝐴 = (𝐴 +𝑒 0)) |
9 | 1 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → 𝐴 ∈ ℝ) |
10 | | ltpnf 12611 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → 𝐴 < +∞) |
11 | 9, 10 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → 𝐴 < +∞) |
12 | | simplr 769 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → 𝐵 = +∞) |
13 | 11, 12 | breqtrrd 5068 |
. . . 4
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → 𝐴 < 𝐵) |
14 | | 0ltpnf 12613 |
. . . . 5
⊢ 0 <
+∞ |
15 | | simpr 488 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → 𝐶 = +∞) |
16 | 14, 15 | breqtrrid 5078 |
. . . 4
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → 0 < 𝐶) |
17 | | oveq1 7190 |
. . . . . . 7
⊢ (𝑏 = 𝐴 → (𝑏 +𝑒 𝑐) = (𝐴 +𝑒 𝑐)) |
18 | 17 | eqeq2d 2750 |
. . . . . 6
⊢ (𝑏 = 𝐴 → (𝐴 = (𝑏 +𝑒 𝑐) ↔ 𝐴 = (𝐴 +𝑒 𝑐))) |
19 | | breq1 5043 |
. . . . . 6
⊢ (𝑏 = 𝐴 → (𝑏 < 𝐵 ↔ 𝐴 < 𝐵)) |
20 | 18, 19 | 3anbi12d 1438 |
. . . . 5
⊢ (𝑏 = 𝐴 → ((𝐴 = (𝑏 +𝑒 𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶) ↔ (𝐴 = (𝐴 +𝑒 𝑐) ∧ 𝐴 < 𝐵 ∧ 𝑐 < 𝐶))) |
21 | | oveq2 7191 |
. . . . . . 7
⊢ (𝑐 = 0 → (𝐴 +𝑒 𝑐) = (𝐴 +𝑒 0)) |
22 | 21 | eqeq2d 2750 |
. . . . . 6
⊢ (𝑐 = 0 → (𝐴 = (𝐴 +𝑒 𝑐) ↔ 𝐴 = (𝐴 +𝑒 0))) |
23 | | breq1 5043 |
. . . . . 6
⊢ (𝑐 = 0 → (𝑐 < 𝐶 ↔ 0 < 𝐶)) |
24 | 22, 23 | 3anbi13d 1439 |
. . . . 5
⊢ (𝑐 = 0 → ((𝐴 = (𝐴 +𝑒 𝑐) ∧ 𝐴 < 𝐵 ∧ 𝑐 < 𝐶) ↔ (𝐴 = (𝐴 +𝑒 0) ∧ 𝐴 < 𝐵 ∧ 0 < 𝐶))) |
25 | 20, 24 | rspc2ev 3541 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 0 ∈ ℝ* ∧ (𝐴 = (𝐴 +𝑒 0) ∧ 𝐴 < 𝐵 ∧ 0 < 𝐶)) → ∃𝑏 ∈ ℝ* ∃𝑐 ∈ ℝ*
(𝐴 = (𝑏 +𝑒 𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶)) |
26 | 3, 5, 8, 13, 16, 25 | syl113anc 1383 |
. . 3
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 = +∞) → ∃𝑏 ∈ ℝ*
∃𝑐 ∈
ℝ* (𝐴 =
(𝑏 +𝑒
𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶)) |
27 | 2 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → 𝐴 ∈
ℝ*) |
28 | | xlt2addrd.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈
ℝ*) |
29 | 28 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → 𝐶 ∈
ℝ*) |
30 | | 1xr 10791 |
. . . . . . . . 9
⊢ 1 ∈
ℝ* |
31 | 30 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → 1 ∈
ℝ*) |
32 | 31 | xnegcld 12789 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) →
-𝑒1 ∈ ℝ*) |
33 | 29, 32 | xaddcld 12790 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐶 +𝑒
-𝑒1) ∈ ℝ*) |
34 | 33 | xnegcld 12789 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) →
-𝑒(𝐶
+𝑒 -𝑒1) ∈
ℝ*) |
35 | 27, 34 | xaddcld 12790 |
. . . 4
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒
-𝑒(𝐶
+𝑒 -𝑒1)) ∈
ℝ*) |
36 | 1 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → 𝐴 ∈ ℝ) |
37 | 36 | renemnfd 10784 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → 𝐴 ≠ -∞) |
38 | | xrnepnf 12609 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈ ℝ*
∧ 𝐶 ≠ +∞)
↔ (𝐶 ∈ ℝ
∨ 𝐶 =
-∞)) |
39 | 38 | biimpi 219 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ ℝ*
∧ 𝐶 ≠ +∞)
→ (𝐶 ∈ ℝ
∨ 𝐶 =
-∞)) |
40 | 29, 39 | sylancom 591 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐶 ∈ ℝ ∨ 𝐶 = -∞)) |
41 | 40 | orcomd 870 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐶 = -∞ ∨ 𝐶 ∈ ℝ)) |
42 | | xlt2addrd.5 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 ≠ -∞) |
43 | 42 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → 𝐶 ≠ -∞) |
44 | 43 | neneqd 2940 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → ¬ 𝐶 = -∞) |
45 | | pm2.53 850 |
. . . . . . . . . . . 12
⊢ ((𝐶 = -∞ ∨ 𝐶 ∈ ℝ) → (¬
𝐶 = -∞ → 𝐶 ∈
ℝ)) |
46 | 41, 44, 45 | sylc 65 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → 𝐶 ∈ ℝ) |
47 | | 1re 10732 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
48 | | rexsub 12722 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ ℝ ∧ 1 ∈
ℝ) → (𝐶
+𝑒 -𝑒1) = (𝐶 − 1)) |
49 | 46, 47, 48 | sylancl 589 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐶 +𝑒
-𝑒1) = (𝐶 − 1)) |
50 | | resubcl 11041 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ ℝ ∧ 1 ∈
ℝ) → (𝐶 −
1) ∈ ℝ) |
51 | 46, 47, 50 | sylancl 589 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐶 − 1) ∈ ℝ) |
52 | 49, 51 | eqeltrd 2834 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐶 +𝑒
-𝑒1) ∈ ℝ) |
53 | | rexneg 12700 |
. . . . . . . . 9
⊢ ((𝐶 +𝑒
-𝑒1) ∈ ℝ → -𝑒(𝐶 +𝑒
-𝑒1) = -(𝐶 +𝑒
-𝑒1)) |
54 | 52, 53 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) →
-𝑒(𝐶
+𝑒 -𝑒1) = -(𝐶 +𝑒
-𝑒1)) |
55 | 52 | renegcld 11158 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → -(𝐶 +𝑒
-𝑒1) ∈ ℝ) |
56 | 54, 55 | eqeltrd 2834 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) →
-𝑒(𝐶
+𝑒 -𝑒1) ∈ ℝ) |
57 | 56 | renemnfd 10784 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) →
-𝑒(𝐶
+𝑒 -𝑒1) ≠ -∞) |
58 | 52 | renemnfd 10784 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐶 +𝑒
-𝑒1) ≠ -∞) |
59 | | xaddass 12738 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (-𝑒(𝐶 +𝑒
-𝑒1) ∈ ℝ* ∧
-𝑒(𝐶
+𝑒 -𝑒1) ≠ -∞) ∧ ((𝐶 +𝑒
-𝑒1) ∈ ℝ* ∧ (𝐶 +𝑒
-𝑒1) ≠ -∞)) → ((𝐴 +𝑒
-𝑒(𝐶
+𝑒 -𝑒1)) +𝑒 (𝐶 +𝑒
-𝑒1)) = (𝐴 +𝑒
(-𝑒(𝐶
+𝑒 -𝑒1) +𝑒 (𝐶 +𝑒
-𝑒1)))) |
60 | 27, 37, 34, 57, 33, 58, 59 | syl222anc 1387 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → ((𝐴 +𝑒
-𝑒(𝐶
+𝑒 -𝑒1)) +𝑒 (𝐶 +𝑒
-𝑒1)) = (𝐴 +𝑒
(-𝑒(𝐶
+𝑒 -𝑒1) +𝑒 (𝐶 +𝑒
-𝑒1)))) |
61 | | xaddcom 12729 |
. . . . . . . 8
⊢
((-𝑒(𝐶 +𝑒
-𝑒1) ∈ ℝ* ∧ (𝐶 +𝑒
-𝑒1) ∈ ℝ*) →
(-𝑒(𝐶
+𝑒 -𝑒1) +𝑒 (𝐶 +𝑒
-𝑒1)) = ((𝐶 +𝑒
-𝑒1) +𝑒 -𝑒(𝐶 +𝑒
-𝑒1))) |
62 | 34, 33, 61 | syl2anc 587 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) →
(-𝑒(𝐶
+𝑒 -𝑒1) +𝑒 (𝐶 +𝑒
-𝑒1)) = ((𝐶 +𝑒
-𝑒1) +𝑒 -𝑒(𝐶 +𝑒
-𝑒1))) |
63 | | xnegid 12727 |
. . . . . . . 8
⊢ ((𝐶 +𝑒
-𝑒1) ∈ ℝ* → ((𝐶 +𝑒
-𝑒1) +𝑒 -𝑒(𝐶 +𝑒
-𝑒1)) = 0) |
64 | 33, 63 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → ((𝐶 +𝑒
-𝑒1) +𝑒 -𝑒(𝐶 +𝑒
-𝑒1)) = 0) |
65 | 62, 64 | eqtrd 2774 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) →
(-𝑒(𝐶
+𝑒 -𝑒1) +𝑒 (𝐶 +𝑒
-𝑒1)) = 0) |
66 | 65 | oveq2d 7199 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒
(-𝑒(𝐶
+𝑒 -𝑒1) +𝑒 (𝐶 +𝑒
-𝑒1))) = (𝐴 +𝑒 0)) |
67 | 27, 6 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒 0) = 𝐴) |
68 | 60, 66, 67 | 3eqtrrd 2779 |
. . . 4
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → 𝐴 = ((𝐴 +𝑒
-𝑒(𝐶
+𝑒 -𝑒1)) +𝑒 (𝐶 +𝑒
-𝑒1))) |
69 | 36, 51 | resubcld 11159 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐴 − (𝐶 − 1)) ∈
ℝ) |
70 | | ltpnf 12611 |
. . . . . 6
⊢ ((𝐴 − (𝐶 − 1)) ∈ ℝ → (𝐴 − (𝐶 − 1)) < +∞) |
71 | 69, 70 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐴 − (𝐶 − 1)) < +∞) |
72 | | rexsub 12722 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ (𝐶 +𝑒
-𝑒1) ∈ ℝ) → (𝐴 +𝑒
-𝑒(𝐶
+𝑒 -𝑒1)) = (𝐴 − (𝐶 +𝑒
-𝑒1))) |
73 | 36, 52, 72 | syl2anc 587 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒
-𝑒(𝐶
+𝑒 -𝑒1)) = (𝐴 − (𝐶 +𝑒
-𝑒1))) |
74 | 49 | oveq2d 7199 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐴 − (𝐶 +𝑒
-𝑒1)) = (𝐴 − (𝐶 − 1))) |
75 | 73, 74 | eqtrd 2774 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒
-𝑒(𝐶
+𝑒 -𝑒1)) = (𝐴 − (𝐶 − 1))) |
76 | | simplr 769 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → 𝐵 = +∞) |
77 | 71, 75, 76 | 3brtr4d 5072 |
. . . 4
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐴 +𝑒
-𝑒(𝐶
+𝑒 -𝑒1)) < 𝐵) |
78 | 46 | ltm1d 11663 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐶 − 1) < 𝐶) |
79 | 49, 78 | eqbrtrd 5062 |
. . . 4
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → (𝐶 +𝑒
-𝑒1) < 𝐶) |
80 | | oveq1 7190 |
. . . . . . 7
⊢ (𝑏 = (𝐴 +𝑒
-𝑒(𝐶
+𝑒 -𝑒1)) → (𝑏 +𝑒 𝑐) = ((𝐴 +𝑒
-𝑒(𝐶
+𝑒 -𝑒1)) +𝑒 𝑐)) |
81 | 80 | eqeq2d 2750 |
. . . . . 6
⊢ (𝑏 = (𝐴 +𝑒
-𝑒(𝐶
+𝑒 -𝑒1)) → (𝐴 = (𝑏 +𝑒 𝑐) ↔ 𝐴 = ((𝐴 +𝑒
-𝑒(𝐶
+𝑒 -𝑒1)) +𝑒 𝑐))) |
82 | | breq1 5043 |
. . . . . 6
⊢ (𝑏 = (𝐴 +𝑒
-𝑒(𝐶
+𝑒 -𝑒1)) → (𝑏 < 𝐵 ↔ (𝐴 +𝑒
-𝑒(𝐶
+𝑒 -𝑒1)) < 𝐵)) |
83 | 81, 82 | 3anbi12d 1438 |
. . . . 5
⊢ (𝑏 = (𝐴 +𝑒
-𝑒(𝐶
+𝑒 -𝑒1)) → ((𝐴 = (𝑏 +𝑒 𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶) ↔ (𝐴 = ((𝐴 +𝑒
-𝑒(𝐶
+𝑒 -𝑒1)) +𝑒 𝑐) ∧ (𝐴 +𝑒
-𝑒(𝐶
+𝑒 -𝑒1)) < 𝐵 ∧ 𝑐 < 𝐶))) |
84 | | oveq2 7191 |
. . . . . . 7
⊢ (𝑐 = (𝐶 +𝑒
-𝑒1) → ((𝐴 +𝑒
-𝑒(𝐶
+𝑒 -𝑒1)) +𝑒 𝑐) = ((𝐴 +𝑒
-𝑒(𝐶
+𝑒 -𝑒1)) +𝑒 (𝐶 +𝑒
-𝑒1))) |
85 | 84 | eqeq2d 2750 |
. . . . . 6
⊢ (𝑐 = (𝐶 +𝑒
-𝑒1) → (𝐴 = ((𝐴 +𝑒
-𝑒(𝐶
+𝑒 -𝑒1)) +𝑒 𝑐) ↔ 𝐴 = ((𝐴 +𝑒
-𝑒(𝐶
+𝑒 -𝑒1)) +𝑒 (𝐶 +𝑒
-𝑒1)))) |
86 | | breq1 5043 |
. . . . . 6
⊢ (𝑐 = (𝐶 +𝑒
-𝑒1) → (𝑐 < 𝐶 ↔ (𝐶 +𝑒
-𝑒1) < 𝐶)) |
87 | 85, 86 | 3anbi13d 1439 |
. . . . 5
⊢ (𝑐 = (𝐶 +𝑒
-𝑒1) → ((𝐴 = ((𝐴 +𝑒
-𝑒(𝐶
+𝑒 -𝑒1)) +𝑒 𝑐) ∧ (𝐴 +𝑒
-𝑒(𝐶
+𝑒 -𝑒1)) < 𝐵 ∧ 𝑐 < 𝐶) ↔ (𝐴 = ((𝐴 +𝑒
-𝑒(𝐶
+𝑒 -𝑒1)) +𝑒 (𝐶 +𝑒
-𝑒1)) ∧ (𝐴 +𝑒
-𝑒(𝐶
+𝑒 -𝑒1)) < 𝐵 ∧ (𝐶 +𝑒
-𝑒1) < 𝐶))) |
88 | 83, 87 | rspc2ev 3541 |
. . . 4
⊢ (((𝐴 +𝑒
-𝑒(𝐶
+𝑒 -𝑒1)) ∈ ℝ* ∧
(𝐶 +𝑒
-𝑒1) ∈ ℝ* ∧ (𝐴 = ((𝐴 +𝑒
-𝑒(𝐶
+𝑒 -𝑒1)) +𝑒 (𝐶 +𝑒
-𝑒1)) ∧ (𝐴 +𝑒
-𝑒(𝐶
+𝑒 -𝑒1)) < 𝐵 ∧ (𝐶 +𝑒
-𝑒1) < 𝐶)) → ∃𝑏 ∈ ℝ* ∃𝑐 ∈ ℝ*
(𝐴 = (𝑏 +𝑒 𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶)) |
89 | 35, 33, 68, 77, 79, 88 | syl113anc 1383 |
. . 3
⊢ (((𝜑 ∧ 𝐵 = +∞) ∧ 𝐶 ≠ +∞) → ∃𝑏 ∈ ℝ*
∃𝑐 ∈
ℝ* (𝐴 =
(𝑏 +𝑒
𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶)) |
90 | 26, 89 | pm2.61dane 3022 |
. 2
⊢ ((𝜑 ∧ 𝐵 = +∞) → ∃𝑏 ∈ ℝ*
∃𝑐 ∈
ℝ* (𝐴 =
(𝑏 +𝑒
𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶)) |
91 | | xlt2addrd.2 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
92 | 91 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 𝐵 ∈
ℝ*) |
93 | 30 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 1 ∈
ℝ*) |
94 | 93 | xnegcld 12789 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → -𝑒1
∈ ℝ*) |
95 | 92, 94 | xaddcld 12790 |
. . . 4
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → (𝐵 +𝑒
-𝑒1) ∈ ℝ*) |
96 | 2 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 𝐴 ∈
ℝ*) |
97 | 95 | xnegcld 12789 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) →
-𝑒(𝐵
+𝑒 -𝑒1) ∈
ℝ*) |
98 | 96, 97 | xaddcld 12790 |
. . . 4
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒
-𝑒(𝐵
+𝑒 -𝑒1)) ∈
ℝ*) |
99 | | xaddcom 12729 |
. . . . . 6
⊢ (((𝐵 +𝑒
-𝑒1) ∈ ℝ* ∧ (𝐴 +𝑒
-𝑒(𝐵
+𝑒 -𝑒1)) ∈ ℝ*)
→ ((𝐵
+𝑒 -𝑒1) +𝑒 (𝐴 +𝑒
-𝑒(𝐵
+𝑒 -𝑒1))) = ((𝐴 +𝑒
-𝑒(𝐵
+𝑒 -𝑒1)) +𝑒 (𝐵 +𝑒
-𝑒1))) |
100 | 95, 98, 99 | syl2anc 587 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → ((𝐵 +𝑒
-𝑒1) +𝑒 (𝐴 +𝑒
-𝑒(𝐵
+𝑒 -𝑒1))) = ((𝐴 +𝑒
-𝑒(𝐵
+𝑒 -𝑒1)) +𝑒 (𝐵 +𝑒
-𝑒1))) |
101 | 1 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 𝐴 ∈ ℝ) |
102 | 101 | renemnfd 10784 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 𝐴 ≠ -∞) |
103 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 𝐵 ≠ +∞) |
104 | | xrnepnf 12609 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ +∞)
↔ (𝐵 ∈ ℝ
∨ 𝐵 =
-∞)) |
105 | 104 | biimpi 219 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℝ*
∧ 𝐵 ≠ +∞)
→ (𝐵 ∈ ℝ
∨ 𝐵 =
-∞)) |
106 | 92, 103, 105 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → (𝐵 ∈ ℝ ∨ 𝐵 = -∞)) |
107 | 106 | orcomd 870 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → (𝐵 = -∞ ∨ 𝐵 ∈ ℝ)) |
108 | | xlt2addrd.4 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ≠ -∞) |
109 | 108 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 𝐵 ≠ -∞) |
110 | 109 | neneqd 2940 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → ¬ 𝐵 = -∞) |
111 | | pm2.53 850 |
. . . . . . . . . . . 12
⊢ ((𝐵 = -∞ ∨ 𝐵 ∈ ℝ) → (¬
𝐵 = -∞ → 𝐵 ∈
ℝ)) |
112 | 107, 110,
111 | sylc 65 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 𝐵 ∈ ℝ) |
113 | | rexsub 12722 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ ∧ 1 ∈
ℝ) → (𝐵
+𝑒 -𝑒1) = (𝐵 − 1)) |
114 | 112, 47, 113 | sylancl 589 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → (𝐵 +𝑒
-𝑒1) = (𝐵 − 1)) |
115 | | resubcl 11041 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ ∧ 1 ∈
ℝ) → (𝐵 −
1) ∈ ℝ) |
116 | 112, 47, 115 | sylancl 589 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → (𝐵 − 1) ∈ ℝ) |
117 | 114, 116 | eqeltrd 2834 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → (𝐵 +𝑒
-𝑒1) ∈ ℝ) |
118 | | rexneg 12700 |
. . . . . . . . 9
⊢ ((𝐵 +𝑒
-𝑒1) ∈ ℝ → -𝑒(𝐵 +𝑒
-𝑒1) = -(𝐵 +𝑒
-𝑒1)) |
119 | 117, 118 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) →
-𝑒(𝐵
+𝑒 -𝑒1) = -(𝐵 +𝑒
-𝑒1)) |
120 | 117 | renegcld 11158 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → -(𝐵 +𝑒
-𝑒1) ∈ ℝ) |
121 | 119, 120 | eqeltrd 2834 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) →
-𝑒(𝐵
+𝑒 -𝑒1) ∈ ℝ) |
122 | 121 | renemnfd 10784 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) →
-𝑒(𝐵
+𝑒 -𝑒1) ≠ -∞) |
123 | 117 | renemnfd 10784 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → (𝐵 +𝑒
-𝑒1) ≠ -∞) |
124 | | xaddass 12738 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ -∞)
∧ (-𝑒(𝐵 +𝑒
-𝑒1) ∈ ℝ* ∧
-𝑒(𝐵
+𝑒 -𝑒1) ≠ -∞) ∧ ((𝐵 +𝑒
-𝑒1) ∈ ℝ* ∧ (𝐵 +𝑒
-𝑒1) ≠ -∞)) → ((𝐴 +𝑒
-𝑒(𝐵
+𝑒 -𝑒1)) +𝑒 (𝐵 +𝑒
-𝑒1)) = (𝐴 +𝑒
(-𝑒(𝐵
+𝑒 -𝑒1) +𝑒 (𝐵 +𝑒
-𝑒1)))) |
125 | 96, 102, 97, 122, 95, 123, 124 | syl222anc 1387 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → ((𝐴 +𝑒
-𝑒(𝐵
+𝑒 -𝑒1)) +𝑒 (𝐵 +𝑒
-𝑒1)) = (𝐴 +𝑒
(-𝑒(𝐵
+𝑒 -𝑒1) +𝑒 (𝐵 +𝑒
-𝑒1)))) |
126 | | xaddcom 12729 |
. . . . . . . . 9
⊢
((-𝑒(𝐵 +𝑒
-𝑒1) ∈ ℝ* ∧ (𝐵 +𝑒
-𝑒1) ∈ ℝ*) →
(-𝑒(𝐵
+𝑒 -𝑒1) +𝑒 (𝐵 +𝑒
-𝑒1)) = ((𝐵 +𝑒
-𝑒1) +𝑒 -𝑒(𝐵 +𝑒
-𝑒1))) |
127 | 97, 95, 126 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) →
(-𝑒(𝐵
+𝑒 -𝑒1) +𝑒 (𝐵 +𝑒
-𝑒1)) = ((𝐵 +𝑒
-𝑒1) +𝑒 -𝑒(𝐵 +𝑒
-𝑒1))) |
128 | | xnegid 12727 |
. . . . . . . . 9
⊢ ((𝐵 +𝑒
-𝑒1) ∈ ℝ* → ((𝐵 +𝑒
-𝑒1) +𝑒 -𝑒(𝐵 +𝑒
-𝑒1)) = 0) |
129 | 95, 128 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → ((𝐵 +𝑒
-𝑒1) +𝑒 -𝑒(𝐵 +𝑒
-𝑒1)) = 0) |
130 | 127, 129 | eqtrd 2774 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) →
(-𝑒(𝐵
+𝑒 -𝑒1) +𝑒 (𝐵 +𝑒
-𝑒1)) = 0) |
131 | 130 | oveq2d 7199 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒
(-𝑒(𝐵
+𝑒 -𝑒1) +𝑒 (𝐵 +𝑒
-𝑒1))) = (𝐴 +𝑒 0)) |
132 | 96, 6 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒 0) = 𝐴) |
133 | 131, 132 | eqtrd 2774 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒
(-𝑒(𝐵
+𝑒 -𝑒1) +𝑒 (𝐵 +𝑒
-𝑒1))) = 𝐴) |
134 | 100, 125,
133 | 3eqtrrd 2779 |
. . . 4
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 𝐴 = ((𝐵 +𝑒
-𝑒1) +𝑒 (𝐴 +𝑒
-𝑒(𝐵
+𝑒 -𝑒1)))) |
135 | 112 | ltm1d 11663 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → (𝐵 − 1) < 𝐵) |
136 | 114, 135 | eqbrtrd 5062 |
. . . 4
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → (𝐵 +𝑒
-𝑒1) < 𝐵) |
137 | 101, 116 | resubcld 11159 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → (𝐴 − (𝐵 − 1)) ∈
ℝ) |
138 | | ltpnf 12611 |
. . . . . 6
⊢ ((𝐴 − (𝐵 − 1)) ∈ ℝ → (𝐴 − (𝐵 − 1)) < +∞) |
139 | 137, 138 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → (𝐴 − (𝐵 − 1)) < +∞) |
140 | | rexsub 12722 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 +𝑒
-𝑒1) ∈ ℝ) → (𝐴 +𝑒
-𝑒(𝐵
+𝑒 -𝑒1)) = (𝐴 − (𝐵 +𝑒
-𝑒1))) |
141 | 101, 117,
140 | syl2anc 587 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒
-𝑒(𝐵
+𝑒 -𝑒1)) = (𝐴 − (𝐵 +𝑒
-𝑒1))) |
142 | 114 | oveq2d 7199 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → (𝐴 − (𝐵 +𝑒
-𝑒1)) = (𝐴 − (𝐵 − 1))) |
143 | 141, 142 | eqtrd 2774 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒
-𝑒(𝐵
+𝑒 -𝑒1)) = (𝐴 − (𝐵 − 1))) |
144 | | simpr 488 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → 𝐶 = +∞) |
145 | 139, 143,
144 | 3brtr4d 5072 |
. . . 4
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → (𝐴 +𝑒
-𝑒(𝐵
+𝑒 -𝑒1)) < 𝐶) |
146 | | oveq1 7190 |
. . . . . . 7
⊢ (𝑏 = (𝐵 +𝑒
-𝑒1) → (𝑏 +𝑒 𝑐) = ((𝐵 +𝑒
-𝑒1) +𝑒 𝑐)) |
147 | 146 | eqeq2d 2750 |
. . . . . 6
⊢ (𝑏 = (𝐵 +𝑒
-𝑒1) → (𝐴 = (𝑏 +𝑒 𝑐) ↔ 𝐴 = ((𝐵 +𝑒
-𝑒1) +𝑒 𝑐))) |
148 | | breq1 5043 |
. . . . . 6
⊢ (𝑏 = (𝐵 +𝑒
-𝑒1) → (𝑏 < 𝐵 ↔ (𝐵 +𝑒
-𝑒1) < 𝐵)) |
149 | 147, 148 | 3anbi12d 1438 |
. . . . 5
⊢ (𝑏 = (𝐵 +𝑒
-𝑒1) → ((𝐴 = (𝑏 +𝑒 𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶) ↔ (𝐴 = ((𝐵 +𝑒
-𝑒1) +𝑒 𝑐) ∧ (𝐵 +𝑒
-𝑒1) < 𝐵 ∧ 𝑐 < 𝐶))) |
150 | | oveq2 7191 |
. . . . . . 7
⊢ (𝑐 = (𝐴 +𝑒
-𝑒(𝐵
+𝑒 -𝑒1)) → ((𝐵 +𝑒
-𝑒1) +𝑒 𝑐) = ((𝐵 +𝑒
-𝑒1) +𝑒 (𝐴 +𝑒
-𝑒(𝐵
+𝑒 -𝑒1)))) |
151 | 150 | eqeq2d 2750 |
. . . . . 6
⊢ (𝑐 = (𝐴 +𝑒
-𝑒(𝐵
+𝑒 -𝑒1)) → (𝐴 = ((𝐵 +𝑒
-𝑒1) +𝑒 𝑐) ↔ 𝐴 = ((𝐵 +𝑒
-𝑒1) +𝑒 (𝐴 +𝑒
-𝑒(𝐵
+𝑒 -𝑒1))))) |
152 | | breq1 5043 |
. . . . . 6
⊢ (𝑐 = (𝐴 +𝑒
-𝑒(𝐵
+𝑒 -𝑒1)) → (𝑐 < 𝐶 ↔ (𝐴 +𝑒
-𝑒(𝐵
+𝑒 -𝑒1)) < 𝐶)) |
153 | 151, 152 | 3anbi13d 1439 |
. . . . 5
⊢ (𝑐 = (𝐴 +𝑒
-𝑒(𝐵
+𝑒 -𝑒1)) → ((𝐴 = ((𝐵 +𝑒
-𝑒1) +𝑒 𝑐) ∧ (𝐵 +𝑒
-𝑒1) < 𝐵 ∧ 𝑐 < 𝐶) ↔ (𝐴 = ((𝐵 +𝑒
-𝑒1) +𝑒 (𝐴 +𝑒
-𝑒(𝐵
+𝑒 -𝑒1))) ∧ (𝐵 +𝑒
-𝑒1) < 𝐵 ∧ (𝐴 +𝑒
-𝑒(𝐵
+𝑒 -𝑒1)) < 𝐶))) |
154 | 149, 153 | rspc2ev 3541 |
. . . 4
⊢ (((𝐵 +𝑒
-𝑒1) ∈ ℝ* ∧ (𝐴 +𝑒
-𝑒(𝐵
+𝑒 -𝑒1)) ∈ ℝ* ∧
(𝐴 = ((𝐵 +𝑒
-𝑒1) +𝑒 (𝐴 +𝑒
-𝑒(𝐵
+𝑒 -𝑒1))) ∧ (𝐵 +𝑒
-𝑒1) < 𝐵 ∧ (𝐴 +𝑒
-𝑒(𝐵
+𝑒 -𝑒1)) < 𝐶)) → ∃𝑏 ∈ ℝ* ∃𝑐 ∈ ℝ*
(𝐴 = (𝑏 +𝑒 𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶)) |
155 | 95, 98, 134, 136, 145, 154 | syl113anc 1383 |
. . 3
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 = +∞) → ∃𝑏 ∈ ℝ*
∃𝑐 ∈
ℝ* (𝐴 =
(𝑏 +𝑒
𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶)) |
156 | 1 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → 𝐴 ∈ ℝ) |
157 | 91 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → 𝐵 ∈
ℝ*) |
158 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → 𝐵 ≠ +∞) |
159 | 157, 158,
105 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → (𝐵 ∈ ℝ ∨ 𝐵 = -∞)) |
160 | 159 | orcomd 870 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → (𝐵 = -∞ ∨ 𝐵 ∈ ℝ)) |
161 | 108 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → 𝐵 ≠ -∞) |
162 | 161 | neneqd 2940 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → ¬ 𝐵 = -∞) |
163 | 160, 162,
111 | sylc 65 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → 𝐵 ∈ ℝ) |
164 | 28 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → 𝐶 ∈
ℝ*) |
165 | 164, 39 | sylancom 591 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → (𝐶 ∈ ℝ ∨ 𝐶 = -∞)) |
166 | 165 | orcomd 870 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → (𝐶 = -∞ ∨ 𝐶 ∈ ℝ)) |
167 | 42 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → 𝐶 ≠ -∞) |
168 | 167 | neneqd 2940 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → ¬ 𝐶 = -∞) |
169 | 166, 168,
45 | sylc 65 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → 𝐶 ∈ ℝ) |
170 | | xlt2addrd.6 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 < (𝐵 +𝑒 𝐶)) |
171 | 170 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → 𝐴 < (𝐵 +𝑒 𝐶)) |
172 | | rexadd 12721 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 +𝑒 𝐶) = (𝐵 + 𝐶)) |
173 | 163, 169,
172 | syl2anc 587 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → (𝐵 +𝑒 𝐶) = (𝐵 + 𝐶)) |
174 | 171, 173 | breqtrd 5066 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → 𝐴 < (𝐵 + 𝐶)) |
175 | 156, 163,
169, 174 | lt2addrd 30662 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ (𝐴 = (𝑏 + 𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶)) |
176 | | rexadd 12721 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑏 +𝑒 𝑐) = (𝑏 + 𝑐)) |
177 | 176 | eqeq2d 2750 |
. . . . . . 7
⊢ ((𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝐴 = (𝑏 +𝑒 𝑐) ↔ 𝐴 = (𝑏 + 𝑐))) |
178 | 177 | 3anbi1d 1441 |
. . . . . 6
⊢ ((𝑏 ∈ ℝ ∧ 𝑐 ∈ ℝ) → ((𝐴 = (𝑏 +𝑒 𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶) ↔ (𝐴 = (𝑏 + 𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶))) |
179 | 178 | 2rexbiia 3209 |
. . . . 5
⊢
(∃𝑏 ∈
ℝ ∃𝑐 ∈
ℝ (𝐴 = (𝑏 +𝑒 𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶) ↔ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ (𝐴 = (𝑏 + 𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶)) |
180 | 175, 179 | sylibr 237 |
. . . 4
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ (𝐴 = (𝑏 +𝑒 𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶)) |
181 | | ressxr 10776 |
. . . . . 6
⊢ ℝ
⊆ ℝ* |
182 | | ssrexv 3954 |
. . . . . 6
⊢ (ℝ
⊆ ℝ* → (∃𝑐 ∈ ℝ (𝐴 = (𝑏 +𝑒 𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶) → ∃𝑐 ∈ ℝ* (𝐴 = (𝑏 +𝑒 𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶))) |
183 | 181, 182 | ax-mp 5 |
. . . . 5
⊢
(∃𝑐 ∈
ℝ (𝐴 = (𝑏 +𝑒 𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶) → ∃𝑐 ∈ ℝ* (𝐴 = (𝑏 +𝑒 𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶)) |
184 | 183 | reximi 3158 |
. . . 4
⊢
(∃𝑏 ∈
ℝ ∃𝑐 ∈
ℝ (𝐴 = (𝑏 +𝑒 𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ* (𝐴 = (𝑏 +𝑒 𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶)) |
185 | | ssrexv 3954 |
. . . . 5
⊢ (ℝ
⊆ ℝ* → (∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ* (𝐴 = (𝑏 +𝑒 𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶) → ∃𝑏 ∈ ℝ* ∃𝑐 ∈ ℝ*
(𝐴 = (𝑏 +𝑒 𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶))) |
186 | 181, 185 | ax-mp 5 |
. . . 4
⊢
(∃𝑏 ∈
ℝ ∃𝑐 ∈
ℝ* (𝐴 =
(𝑏 +𝑒
𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶) → ∃𝑏 ∈ ℝ* ∃𝑐 ∈ ℝ*
(𝐴 = (𝑏 +𝑒 𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶)) |
187 | 180, 184,
186 | 3syl 18 |
. . 3
⊢ (((𝜑 ∧ 𝐵 ≠ +∞) ∧ 𝐶 ≠ +∞) → ∃𝑏 ∈ ℝ*
∃𝑐 ∈
ℝ* (𝐴 =
(𝑏 +𝑒
𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶)) |
188 | 155, 187 | pm2.61dane 3022 |
. 2
⊢ ((𝜑 ∧ 𝐵 ≠ +∞) → ∃𝑏 ∈ ℝ*
∃𝑐 ∈
ℝ* (𝐴 =
(𝑏 +𝑒
𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶)) |
189 | 90, 188 | pm2.61dane 3022 |
1
⊢ (𝜑 → ∃𝑏 ∈ ℝ* ∃𝑐 ∈ ℝ*
(𝐴 = (𝑏 +𝑒 𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶)) |