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