Proof of Theorem archiabllem2a
| Step | Hyp | Ref
| Expression |
| 1 | | simpllr 776 |
. . . 4
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ (𝑏 + 𝑏) ≤ 𝑋) → 𝑏 ∈ 𝐵) |
| 2 | | simplrl 777 |
. . . 4
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ (𝑏 + 𝑏) ≤ 𝑋) → 0 < 𝑏) |
| 3 | | simpr 484 |
. . . 4
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ (𝑏 + 𝑏) ≤ 𝑋) → (𝑏 + 𝑏) ≤ 𝑋) |
| 4 | | breq2 5147 |
. . . . . 6
⊢ (𝑐 = 𝑏 → ( 0 < 𝑐 ↔ 0 < 𝑏)) |
| 5 | | id 22 |
. . . . . . . 8
⊢ (𝑐 = 𝑏 → 𝑐 = 𝑏) |
| 6 | 5, 5 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑐 = 𝑏 → (𝑐 + 𝑐) = (𝑏 + 𝑏)) |
| 7 | 6 | breq1d 5153 |
. . . . . 6
⊢ (𝑐 = 𝑏 → ((𝑐 + 𝑐) ≤ 𝑋 ↔ (𝑏 + 𝑏) ≤ 𝑋)) |
| 8 | 4, 7 | anbi12d 632 |
. . . . 5
⊢ (𝑐 = 𝑏 → (( 0 < 𝑐 ∧ (𝑐 + 𝑐) ≤ 𝑋) ↔ ( 0 < 𝑏 ∧ (𝑏 + 𝑏) ≤ 𝑋))) |
| 9 | 8 | rspcev 3622 |
. . . 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 33080 |
. . . . . 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 2737 |
. . . . . 6
⊢
(-g‘𝑊) = (-g‘𝑊) |
| 20 | 18, 19 | grpsubcl 19038 |
. . . . 5
⊢ ((𝑊 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑋(-g‘𝑊)𝑏) ∈ 𝐵) |
| 21 | 14, 16, 17, 20 | syl3anc 1373 |
. . . 4
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → (𝑋(-g‘𝑊)𝑏) ∈ 𝐵) |
| 22 | | archiabllem.0 |
. . . . . . 7
⊢ 0 =
(0g‘𝑊) |
| 23 | 18, 22, 19 | grpsubid 19042 |
. . . . . 6
⊢ ((𝑊 ∈ Grp ∧ 𝑏 ∈ 𝐵) → (𝑏(-g‘𝑊)𝑏) = 0 ) |
| 24 | 14, 17, 23 | syl2anc 584 |
. . . . 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 33098 |
. . . . . 6
⊢ ((𝑊 ∈ oGrp ∧ (𝑏 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑏 < 𝑋) → (𝑏(-g‘𝑊)𝑏) < (𝑋(-g‘𝑊)𝑏)) |
| 29 | 25, 17, 16, 17, 26, 28 | syl131anc 1385 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → (𝑏(-g‘𝑊)𝑏) < (𝑋(-g‘𝑊)𝑏)) |
| 30 | 24, 29 | eqbrtrrd 5167 |
. . . 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 18959 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Grp ∧ 𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑏 + 𝑏) ∈ 𝐵) |
| 35 | 14, 17, 17, 34 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → (𝑏 + 𝑏) ∈ 𝐵) |
| 36 | | simpr 484 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → 𝑋 < (𝑏 + 𝑏)) |
| 37 | 18, 27, 19 | ogrpsublt 33098 |
. . . . . . . . 9
⊢ ((𝑊 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ (𝑏 + 𝑏) ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑋 < (𝑏 + 𝑏)) → (𝑋(-g‘𝑊)𝑏) < ((𝑏 + 𝑏)(-g‘𝑊)𝑏)) |
| 38 | 25, 16, 35, 17, 36, 37 | syl131anc 1385 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → (𝑋(-g‘𝑊)𝑏) < ((𝑏 + 𝑏)(-g‘𝑊)𝑏)) |
| 39 | 18, 31, 19 | grpaddsubass 19048 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Grp ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑏 + 𝑏)(-g‘𝑊)𝑏) = (𝑏 + (𝑏(-g‘𝑊)𝑏))) |
| 40 | 14, 17, 17, 17, 39 | syl13anc 1374 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → ((𝑏 + 𝑏)(-g‘𝑊)𝑏) = (𝑏 + (𝑏(-g‘𝑊)𝑏))) |
| 41 | 24 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → (𝑏 + (𝑏(-g‘𝑊)𝑏)) = (𝑏 + 0 )) |
| 42 | 18, 31, 22 | grprid 18986 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Grp ∧ 𝑏 ∈ 𝐵) → (𝑏 + 0 ) = 𝑏) |
| 43 | 14, 17, 42 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → (𝑏 + 0 ) = 𝑏) |
| 44 | 40, 41, 43 | 3eqtrd 2781 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → ((𝑏 + 𝑏)(-g‘𝑊)𝑏) = 𝑏) |
| 45 | 38, 44 | breqtrd 5169 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → (𝑋(-g‘𝑊)𝑏) < 𝑏) |
| 46 | 18, 27, 31, 14, 33, 21, 17, 21, 45 | ogrpaddltrd 33096 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → ((𝑋(-g‘𝑊)𝑏) + (𝑋(-g‘𝑊)𝑏)) < ((𝑋(-g‘𝑊)𝑏) + 𝑏)) |
| 47 | 18, 31, 19 | grpnpcan 19050 |
. . . . . . 7
⊢ ((𝑊 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → ((𝑋(-g‘𝑊)𝑏) + 𝑏) = 𝑋) |
| 48 | 14, 16, 17, 47 | syl3anc 1373 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → ((𝑋(-g‘𝑊)𝑏) + 𝑏) = 𝑋) |
| 49 | 46, 48 | breqtrd 5169 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → ((𝑋(-g‘𝑊)𝑏) + (𝑋(-g‘𝑊)𝑏)) < 𝑋) |
| 50 | | ovexd 7466 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) ∧ 𝑋 < (𝑏 + 𝑏)) → ((𝑋(-g‘𝑊)𝑏) + (𝑋(-g‘𝑊)𝑏)) ∈ V) |
| 51 | | archiabllem.e |
. . . . . . 7
⊢ ≤ =
(le‘𝑊) |
| 52 | 51, 27 | pltle 18378 |
. . . . . 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 5147 |
. . . . . 6
⊢ (𝑐 = (𝑋(-g‘𝑊)𝑏) → ( 0 < 𝑐 ↔ 0 < (𝑋(-g‘𝑊)𝑏))) |
| 56 | | id 22 |
. . . . . . . 8
⊢ (𝑐 = (𝑋(-g‘𝑊)𝑏) → 𝑐 = (𝑋(-g‘𝑊)𝑏)) |
| 57 | 56, 56 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑐 = (𝑋(-g‘𝑊)𝑏) → (𝑐 + 𝑐) = ((𝑋(-g‘𝑊)𝑏) + (𝑋(-g‘𝑊)𝑏))) |
| 58 | 57 | breq1d 5153 |
. . . . . 6
⊢ (𝑐 = (𝑋(-g‘𝑊)𝑏) → ((𝑐 + 𝑐) ≤ 𝑋 ↔ ((𝑋(-g‘𝑊)𝑏) + (𝑋(-g‘𝑊)𝑏)) ≤ 𝑋)) |
| 59 | 55, 58 | anbi12d 632 |
. . . . 5
⊢ (𝑐 = (𝑋(-g‘𝑊)𝑏) → (( 0 < 𝑐 ∧ (𝑐 + 𝑐) ≤ 𝑋) ↔ ( 0 < (𝑋(-g‘𝑊)𝑏) ∧ ((𝑋(-g‘𝑊)𝑏) + (𝑋(-g‘𝑊)𝑏)) ≤ 𝑋))) |
| 60 | 59 | rspcev 3622 |
. . . 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 33079 |
. . . . . 6
⊢ (𝑊 ∈ oGrp ↔ (𝑊 ∈ Grp ∧ 𝑊 ∈ oMnd)) |
| 64 | 63 | simprbi 496 |
. . . . 5
⊢ (𝑊 ∈ oGrp → 𝑊 ∈ oMnd) |
| 65 | | omndtos 33082 |
. . . . 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 32959 |
. . . 4
⊢ ((𝑊 ∈ Toset ∧ (𝑏 + 𝑏) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ((𝑏 + 𝑏) ≤ 𝑋 ∨ 𝑋 < (𝑏 + 𝑏))) |
| 72 | 66, 69, 70, 71 | syl3anc 1373 |
. . 3
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) → ((𝑏 + 𝑏) ≤ 𝑋 ∨ 𝑋 < (𝑏 + 𝑏))) |
| 73 | 10, 61, 72 | mpjaodan 961 |
. 2
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) → ∃𝑐 ∈ 𝐵 ( 0 < 𝑐 ∧ (𝑐 + 𝑐) ≤ 𝑋)) |
| 74 | | archiabllem2.3 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 0 < 𝑎) → ∃𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎)) |
| 75 | 74 | 3expia 1122 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ( 0 < 𝑎 → ∃𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎))) |
| 76 | 75 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑎 ∈ 𝐵 ( 0 < 𝑎 → ∃𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎))) |
| 77 | | archiabllem2a.5 |
. . 3
⊢ (𝜑 → 0 < 𝑋) |
| 78 | | breq2 5147 |
. . . . 5
⊢ (𝑎 = 𝑋 → ( 0 < 𝑎 ↔ 0 < 𝑋)) |
| 79 | | breq2 5147 |
. . . . . . 7
⊢ (𝑎 = 𝑋 → (𝑏 < 𝑎 ↔ 𝑏 < 𝑋)) |
| 80 | 79 | anbi2d 630 |
. . . . . 6
⊢ (𝑎 = 𝑋 → (( 0 < 𝑏 ∧ 𝑏 < 𝑎) ↔ ( 0 < 𝑏 ∧ 𝑏 < 𝑋))) |
| 81 | 80 | rexbidv 3179 |
. . . . 5
⊢ (𝑎 = 𝑋 → (∃𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎) ↔ ∃𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑋))) |
| 82 | 78, 81 | imbi12d 344 |
. . . 4
⊢ (𝑎 = 𝑋 → (( 0 < 𝑎 → ∃𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎)) ↔ ( 0 < 𝑋 → ∃𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑋)))) |
| 83 | 82 | rspcv 3618 |
. . 3
⊢ (𝑋 ∈ 𝐵 → (∀𝑎 ∈ 𝐵 ( 0 < 𝑎 → ∃𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎)) → ( 0 < 𝑋 → ∃𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑋)))) |
| 84 | 15, 76, 77, 83 | syl3c 66 |
. 2
⊢ (𝜑 → ∃𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑋)) |
| 85 | 73, 84 | r19.29a 3162 |
1
⊢ (𝜑 → ∃𝑐 ∈ 𝐵 ( 0 < 𝑐 ∧ (𝑐 + 𝑐) ≤ 𝑋)) |