Proof of Theorem archiabllem2a
Step | Hyp | Ref
| Expression |
1 | | simpllr 776 |
. . . 4
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ (𝑏 + 𝑏) ≤ 𝑋) → 𝑏 ∈ 𝐵) |
2 | | simplrl 777 |
. . . 4
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ (𝑏 + 𝑏) ≤ 𝑋) → 0 < 𝑏) |
3 | | simpr 488 |
. . . 4
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ (𝑏 + 𝑏) ≤ 𝑋) → (𝑏 + 𝑏) ≤ 𝑋) |
4 | | breq2 5074 |
. . . . . 6
⊢ (𝑐 = 𝑏 → ( 0 < 𝑐 ↔ 0 < 𝑏)) |
5 | | id 22 |
. . . . . . . 8
⊢ (𝑐 = 𝑏 → 𝑐 = 𝑏) |
6 | 5, 5 | oveq12d 7253 |
. . . . . . 7
⊢ (𝑐 = 𝑏 → (𝑐 + 𝑐) = (𝑏 + 𝑏)) |
7 | 6 | breq1d 5080 |
. . . . . 6
⊢ (𝑐 = 𝑏 → ((𝑐 + 𝑐) ≤ 𝑋 ↔ (𝑏 + 𝑏) ≤ 𝑋)) |
8 | 4, 7 | anbi12d 634 |
. . . . 5
⊢ (𝑐 = 𝑏 → (( 0 < 𝑐 ∧ (𝑐 + 𝑐) ≤ 𝑋) ↔ ( 0 < 𝑏 ∧ (𝑏 + 𝑏) ≤ 𝑋))) |
9 | 8 | rspcev 3552 |
. . . 4
⊢ ((𝑏 ∈ 𝐵 ∧ ( 0 < 𝑏 ∧ (𝑏 + 𝑏) ≤ 𝑋)) → ∃𝑐 ∈ 𝐵 ( 0 < 𝑐 ∧ (𝑐 + 𝑐) ≤ 𝑋)) |
10 | 1, 2, 3, 9 | syl12anc 837 |
. . 3
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ (𝑏 + 𝑏) ≤ 𝑋) → ∃𝑐 ∈ 𝐵 ( 0 < 𝑐 ∧ (𝑐 + 𝑐) ≤ 𝑋)) |
11 | | simplll 775 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → 𝜑) |
12 | | archiabllem.g |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ oGrp) |
13 | | ogrpgrp 31080 |
. . . . . 6
⊢ (𝑊 ∈ oGrp → 𝑊 ∈ Grp) |
14 | 11, 12, 13 | 3syl 18 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → 𝑊 ∈ Grp) |
15 | | archiabllem2a.4 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
16 | 11, 15 | syl 17 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → 𝑋 ∈ 𝐵) |
17 | | simpllr 776 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → 𝑏 ∈ 𝐵) |
18 | | archiabllem.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑊) |
19 | | eqid 2739 |
. . . . . 6
⊢
(-g‘𝑊) = (-g‘𝑊) |
20 | 18, 19 | grpsubcl 18476 |
. . . . 5
⊢ ((𝑊 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑋(-g‘𝑊)𝑏) ∈ 𝐵) |
21 | 14, 16, 17, 20 | syl3anc 1373 |
. . . 4
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → (𝑋(-g‘𝑊)𝑏) ∈ 𝐵) |
22 | | archiabllem.0 |
. . . . . . 7
⊢ 0 =
(0g‘𝑊) |
23 | 18, 22, 19 | grpsubid 18480 |
. . . . . 6
⊢ ((𝑊 ∈ Grp ∧ 𝑏 ∈ 𝐵) → (𝑏(-g‘𝑊)𝑏) = 0 ) |
24 | 14, 17, 23 | syl2anc 587 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → (𝑏(-g‘𝑊)𝑏) = 0 ) |
25 | 11, 12 | syl 17 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → 𝑊 ∈ oGrp) |
26 | | simplrr 778 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → 𝑏 < 𝑋) |
27 | | archiabllem.t |
. . . . . . 7
⊢ < =
(lt‘𝑊) |
28 | 18, 27, 19 | ogrpsublt 31098 |
. . . . . 6
⊢ ((𝑊 ∈ oGrp ∧ (𝑏 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 < 𝑋) → (𝑏(-g‘𝑊)𝑏) < (𝑋(-g‘𝑊)𝑏)) |
29 | 25, 17, 16, 17, 26, 28 | syl131anc 1385 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → (𝑏(-g‘𝑊)𝑏) < (𝑋(-g‘𝑊)𝑏)) |
30 | 24, 29 | eqbrtrrd 5094 |
. . . 4
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → 0 < (𝑋(-g‘𝑊)𝑏)) |
31 | | archiabllem2.1 |
. . . . . . 7
⊢ + =
(+g‘𝑊) |
32 | | archiabllem2.2 |
. . . . . . . 8
⊢ (𝜑 →
(oppg‘𝑊) ∈ oGrp) |
33 | 11, 32 | syl 17 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → (oppg‘𝑊) ∈ oGrp) |
34 | 18, 31 | grpcl 18406 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Grp ∧ 𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑏 + 𝑏) ∈ 𝐵) |
35 | 14, 17, 17, 34 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → (𝑏 + 𝑏) ∈ 𝐵) |
36 | | simpr 488 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → 𝑋 < (𝑏 + 𝑏)) |
37 | 18, 27, 19 | ogrpsublt 31098 |
. . . . . . . . 9
⊢ ((𝑊 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ (𝑏 + 𝑏) ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑋 < (𝑏 + 𝑏)) → (𝑋(-g‘𝑊)𝑏) < ((𝑏 + 𝑏)(-g‘𝑊)𝑏)) |
38 | 25, 16, 35, 17, 36, 37 | syl131anc 1385 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → (𝑋(-g‘𝑊)𝑏) < ((𝑏 + 𝑏)(-g‘𝑊)𝑏)) |
39 | 18, 31, 19 | grpaddsubass 18486 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Grp ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑏 + 𝑏)(-g‘𝑊)𝑏) = (𝑏 + (𝑏(-g‘𝑊)𝑏))) |
40 | 14, 17, 17, 17, 39 | syl13anc 1374 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → ((𝑏 + 𝑏)(-g‘𝑊)𝑏) = (𝑏 + (𝑏(-g‘𝑊)𝑏))) |
41 | 24 | oveq2d 7251 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → (𝑏 + (𝑏(-g‘𝑊)𝑏)) = (𝑏 + 0 )) |
42 | 18, 31, 22 | grprid 18431 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Grp ∧ 𝑏 ∈ 𝐵) → (𝑏 + 0 ) = 𝑏) |
43 | 14, 17, 42 | syl2anc 587 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → (𝑏 + 0 ) = 𝑏) |
44 | 40, 41, 43 | 3eqtrd 2783 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → ((𝑏 + 𝑏)(-g‘𝑊)𝑏) = 𝑏) |
45 | 38, 44 | breqtrd 5096 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → (𝑋(-g‘𝑊)𝑏) < 𝑏) |
46 | 18, 27, 31, 14, 33, 21, 17, 21, 45 | ogrpaddltrd 31096 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → ((𝑋(-g‘𝑊)𝑏) + (𝑋(-g‘𝑊)𝑏)) < ((𝑋(-g‘𝑊)𝑏) + 𝑏)) |
47 | 18, 31, 19 | grpnpcan 18488 |
. . . . . . 7
⊢ ((𝑊 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → ((𝑋(-g‘𝑊)𝑏) + 𝑏) = 𝑋) |
48 | 14, 16, 17, 47 | syl3anc 1373 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → ((𝑋(-g‘𝑊)𝑏) + 𝑏) = 𝑋) |
49 | 46, 48 | breqtrd 5096 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → ((𝑋(-g‘𝑊)𝑏) + (𝑋(-g‘𝑊)𝑏)) < 𝑋) |
50 | | ovexd 7270 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → ((𝑋(-g‘𝑊)𝑏) + (𝑋(-g‘𝑊)𝑏)) ∈ V) |
51 | | archiabllem.e |
. . . . . . 7
⊢ ≤ =
(le‘𝑊) |
52 | 51, 27 | pltle 17872 |
. . . . . 6
⊢ ((𝑊 ∈ Grp ∧ ((𝑋(-g‘𝑊)𝑏) + (𝑋(-g‘𝑊)𝑏)) ∈ V ∧ 𝑋 ∈ 𝐵) → (((𝑋(-g‘𝑊)𝑏) + (𝑋(-g‘𝑊)𝑏)) < 𝑋 → ((𝑋(-g‘𝑊)𝑏) + (𝑋(-g‘𝑊)𝑏)) ≤ 𝑋)) |
53 | 14, 50, 16, 52 | syl3anc 1373 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → (((𝑋(-g‘𝑊)𝑏) + (𝑋(-g‘𝑊)𝑏)) < 𝑋 → ((𝑋(-g‘𝑊)𝑏) + (𝑋(-g‘𝑊)𝑏)) ≤ 𝑋)) |
54 | 49, 53 | mpd 15 |
. . . 4
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → ((𝑋(-g‘𝑊)𝑏) + (𝑋(-g‘𝑊)𝑏)) ≤ 𝑋) |
55 | | breq2 5074 |
. . . . . 6
⊢ (𝑐 = (𝑋(-g‘𝑊)𝑏) → ( 0 < 𝑐 ↔ 0 < (𝑋(-g‘𝑊)𝑏))) |
56 | | id 22 |
. . . . . . . 8
⊢ (𝑐 = (𝑋(-g‘𝑊)𝑏) → 𝑐 = (𝑋(-g‘𝑊)𝑏)) |
57 | 56, 56 | oveq12d 7253 |
. . . . . . 7
⊢ (𝑐 = (𝑋(-g‘𝑊)𝑏) → (𝑐 + 𝑐) = ((𝑋(-g‘𝑊)𝑏) + (𝑋(-g‘𝑊)𝑏))) |
58 | 57 | breq1d 5080 |
. . . . . 6
⊢ (𝑐 = (𝑋(-g‘𝑊)𝑏) → ((𝑐 + 𝑐) ≤ 𝑋 ↔ ((𝑋(-g‘𝑊)𝑏) + (𝑋(-g‘𝑊)𝑏)) ≤ 𝑋)) |
59 | 55, 58 | anbi12d 634 |
. . . . 5
⊢ (𝑐 = (𝑋(-g‘𝑊)𝑏) → (( 0 < 𝑐 ∧ (𝑐 + 𝑐) ≤ 𝑋) ↔ ( 0 < (𝑋(-g‘𝑊)𝑏) ∧ ((𝑋(-g‘𝑊)𝑏) + (𝑋(-g‘𝑊)𝑏)) ≤ 𝑋))) |
60 | 59 | rspcev 3552 |
. . . 4
⊢ (((𝑋(-g‘𝑊)𝑏) ∈ 𝐵 ∧ ( 0 < (𝑋(-g‘𝑊)𝑏) ∧ ((𝑋(-g‘𝑊)𝑏) + (𝑋(-g‘𝑊)𝑏)) ≤ 𝑋)) → ∃𝑐 ∈ 𝐵 ( 0 < 𝑐 ∧ (𝑐 + 𝑐) ≤ 𝑋)) |
61 | 21, 30, 54, 60 | syl12anc 837 |
. . 3
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → ∃𝑐 ∈ 𝐵 ( 0 < 𝑐 ∧ (𝑐 + 𝑐) ≤ 𝑋)) |
62 | 12 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) → 𝑊 ∈ oGrp) |
63 | | isogrp 31079 |
. . . . . 6
⊢ (𝑊 ∈ oGrp ↔ (𝑊 ∈ Grp ∧ 𝑊 ∈ oMnd)) |
64 | 63 | simprbi 500 |
. . . . 5
⊢ (𝑊 ∈ oGrp → 𝑊 ∈ oMnd) |
65 | | omndtos 31082 |
. . . . 5
⊢ (𝑊 ∈ oMnd → 𝑊 ∈ Toset) |
66 | 62, 64, 65 | 3syl 18 |
. . . 4
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) → 𝑊 ∈ Toset) |
67 | 62, 13 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) → 𝑊 ∈ Grp) |
68 | | simplr 769 |
. . . . 5
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) → 𝑏 ∈ 𝐵) |
69 | 67, 68, 68, 34 | syl3anc 1373 |
. . . 4
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) → (𝑏 + 𝑏) ∈ 𝐵) |
70 | 15 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) → 𝑋 ∈ 𝐵) |
71 | 18, 51, 27 | tlt2 30998 |
. . . 4
⊢ ((𝑊 ∈ Toset ∧ (𝑏 + 𝑏) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ((𝑏 + 𝑏) ≤ 𝑋 ∨ 𝑋 < (𝑏 + 𝑏))) |
72 | 66, 69, 70, 71 | syl3anc 1373 |
. . 3
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) → ((𝑏 + 𝑏) ≤ 𝑋 ∨ 𝑋 < (𝑏 + 𝑏))) |
73 | 10, 61, 72 | mpjaodan 959 |
. 2
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) → ∃𝑐 ∈ 𝐵 ( 0 < 𝑐 ∧ (𝑐 + 𝑐) ≤ 𝑋)) |
74 | | archiabllem2.3 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 0 < 𝑎) → ∃𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎)) |
75 | 74 | 3expia 1123 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ( 0 < 𝑎 → ∃𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎))) |
76 | 75 | ralrimiva 3108 |
. . 3
⊢ (𝜑 → ∀𝑎 ∈ 𝐵 ( 0 < 𝑎 → ∃𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎))) |
77 | | archiabllem2a.5 |
. . 3
⊢ (𝜑 → 0 < 𝑋) |
78 | | breq2 5074 |
. . . . 5
⊢ (𝑎 = 𝑋 → ( 0 < 𝑎 ↔ 0 < 𝑋)) |
79 | | breq2 5074 |
. . . . . . 7
⊢ (𝑎 = 𝑋 → (𝑏 < 𝑎 ↔ 𝑏 < 𝑋)) |
80 | 79 | anbi2d 632 |
. . . . . 6
⊢ (𝑎 = 𝑋 → (( 0 < 𝑏 ∧ 𝑏 < 𝑎) ↔ ( 0 < 𝑏 ∧ 𝑏 < 𝑋))) |
81 | 80 | rexbidv 3226 |
. . . . 5
⊢ (𝑎 = 𝑋 → (∃𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎) ↔ ∃𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑋))) |
82 | 78, 81 | imbi12d 348 |
. . . 4
⊢ (𝑎 = 𝑋 → (( 0 < 𝑎 → ∃𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎)) ↔ ( 0 < 𝑋 → ∃𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑋)))) |
83 | 82 | rspcv 3547 |
. . 3
⊢ (𝑋 ∈ 𝐵 → (∀𝑎 ∈ 𝐵 ( 0 < 𝑎 → ∃𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎)) → ( 0 < 𝑋 → ∃𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑋)))) |
84 | 15, 76, 77, 83 | syl3c 66 |
. 2
⊢ (𝜑 → ∃𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) |
85 | 73, 84 | r19.29a 3218 |
1
⊢ (𝜑 → ∃𝑐 ∈ 𝐵 ( 0 < 𝑐 ∧ (𝑐 + 𝑐) ≤ 𝑋)) |