Metamath Proof Explorer

Theorem prub

Description: A positive fraction not in a positive real is an upper bound. Remark (1) of Gleason p. 122. (Contributed by NM, 25-Feb-1996) (New usage is discouraged.)

Ref Expression
Assertion prub ⊢A∈𝑷∧B∈A∧C∈𝑸→¬C∈A→B<𝑸C

Proof

Step Hyp Ref Expression
1 eleq1 ⊢B=C→B∈A↔C∈A
2 1 biimpcd ⊢B∈A→B=C→C∈A
3 2 adantl ⊢A∈𝑷∧B∈A→B=C→C∈A
4 prcdnq ⊢A∈𝑷∧B∈A→C<𝑸B→C∈A
5 3 4 jaod ⊢A∈𝑷∧B∈A→B=C∨C<𝑸B→C∈A
6 5 con3d ⊢A∈𝑷∧B∈A→¬C∈A→¬B=C∨C<𝑸B
7 6 adantr ⊢A∈𝑷∧B∈A∧C∈𝑸→¬C∈A→¬B=C∨C<𝑸B
8 elprnq ⊢A∈𝑷∧B∈A→B∈𝑸
9 ltsonq ⊢<𝑸Or𝑸
10 sotric ⊢<𝑸Or𝑸∧B∈𝑸∧C∈𝑸→B<𝑸C↔¬B=C∨C<𝑸B
11 9 10 mpan ⊢B∈𝑸∧C∈𝑸→B<𝑸C↔¬B=C∨C<𝑸B
12 8 11 sylan ⊢A∈𝑷∧B∈A∧C∈𝑸→B<𝑸C↔¬B=C∨C<𝑸B
13 7 12 sylibrd ⊢A∈𝑷∧B∈A∧C∈𝑸→¬C∈A→B<𝑸C