Metamath Proof Explorer

Theorem addclprlem1

Description: Lemma to prove downward closure in positive real addition. Part of proof of Proposition 9-3.5 of Gleason p. 123. (Contributed by NM, 13-Mar-1996) (New usage is discouraged.)

Ref Expression
Assertion addclprlem1 ( ( ( ๐ด โˆˆ P โˆง ๐‘” โˆˆ ๐ด ) โˆง ๐‘ฅ โˆˆ Q ) โ†’ ( ๐‘ฅ <Q ( ๐‘” +Q โ„Ž ) โ†’ ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ ๐‘” ) โˆˆ ๐ด ) )

Proof

Step Hyp Ref Expression
1 elprnq โŠข ( ( ๐ด โˆˆ P โˆง ๐‘” โˆˆ ๐ด ) โ†’ ๐‘” โˆˆ Q )
2 ltrnq โŠข ( ๐‘ฅ <Q ( ๐‘” +Q โ„Ž ) โ†” ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) <Q ( *Q โ€˜ ๐‘ฅ ) )
3 ltmnq โŠข ( ๐‘ฅ โˆˆ Q โ†’ ( ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) <Q ( *Q โ€˜ ๐‘ฅ ) โ†” ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) <Q ( ๐‘ฅ ยทQ ( *Q โ€˜ ๐‘ฅ ) ) ) )
4 ovex โŠข ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) โˆˆ V
5 ovex โŠข ( ๐‘ฅ ยทQ ( *Q โ€˜ ๐‘ฅ ) ) โˆˆ V
6 ltmnq โŠข ( ๐‘ค โˆˆ Q โ†’ ( ๐‘ฆ <Q ๐‘ง โ†” ( ๐‘ค ยทQ ๐‘ฆ ) <Q ( ๐‘ค ยทQ ๐‘ง ) ) )
7 vex โŠข ๐‘” โˆˆ V
8 mulcomnq โŠข ( ๐‘ฆ ยทQ ๐‘ง ) = ( ๐‘ง ยทQ ๐‘ฆ )
9 4 5 6 7 8 caovord2 โŠข ( ๐‘” โˆˆ Q โ†’ ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) <Q ( ๐‘ฅ ยทQ ( *Q โ€˜ ๐‘ฅ ) ) โ†” ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ ๐‘” ) <Q ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ๐‘ฅ ) ) ยทQ ๐‘” ) ) )
10 3 9 sylan9bbr โŠข ( ( ๐‘” โˆˆ Q โˆง ๐‘ฅ โˆˆ Q ) โ†’ ( ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) <Q ( *Q โ€˜ ๐‘ฅ ) โ†” ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ ๐‘” ) <Q ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ๐‘ฅ ) ) ยทQ ๐‘” ) ) )
11 2 10 bitrid โŠข ( ( ๐‘” โˆˆ Q โˆง ๐‘ฅ โˆˆ Q ) โ†’ ( ๐‘ฅ <Q ( ๐‘” +Q โ„Ž ) โ†” ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ ๐‘” ) <Q ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ๐‘ฅ ) ) ยทQ ๐‘” ) ) )
12 recidnq โŠข ( ๐‘ฅ โˆˆ Q โ†’ ( ๐‘ฅ ยทQ ( *Q โ€˜ ๐‘ฅ ) ) = 1Q )
13 12 oveq1d โŠข ( ๐‘ฅ โˆˆ Q โ†’ ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ๐‘ฅ ) ) ยทQ ๐‘” ) = ( 1Q ยทQ ๐‘” ) )
14 mulcomnq โŠข ( 1Q ยทQ ๐‘” ) = ( ๐‘” ยทQ 1Q )
15 mulidnq โŠข ( ๐‘” โˆˆ Q โ†’ ( ๐‘” ยทQ 1Q ) = ๐‘” )
16 14 15 eqtrid โŠข ( ๐‘” โˆˆ Q โ†’ ( 1Q ยทQ ๐‘” ) = ๐‘” )
17 13 16 sylan9eqr โŠข ( ( ๐‘” โˆˆ Q โˆง ๐‘ฅ โˆˆ Q ) โ†’ ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ๐‘ฅ ) ) ยทQ ๐‘” ) = ๐‘” )
18 17 breq2d โŠข ( ( ๐‘” โˆˆ Q โˆง ๐‘ฅ โˆˆ Q ) โ†’ ( ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ ๐‘” ) <Q ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ๐‘ฅ ) ) ยทQ ๐‘” ) โ†” ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ ๐‘” ) <Q ๐‘” ) )
19 11 18 bitrd โŠข ( ( ๐‘” โˆˆ Q โˆง ๐‘ฅ โˆˆ Q ) โ†’ ( ๐‘ฅ <Q ( ๐‘” +Q โ„Ž ) โ†” ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ ๐‘” ) <Q ๐‘” ) )
20 1 19 sylan โŠข ( ( ( ๐ด โˆˆ P โˆง ๐‘” โˆˆ ๐ด ) โˆง ๐‘ฅ โˆˆ Q ) โ†’ ( ๐‘ฅ <Q ( ๐‘” +Q โ„Ž ) โ†” ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ ๐‘” ) <Q ๐‘” ) )
21 prcdnq โŠข ( ( ๐ด โˆˆ P โˆง ๐‘” โˆˆ ๐ด ) โ†’ ( ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ ๐‘” ) <Q ๐‘” โ†’ ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ ๐‘” ) โˆˆ ๐ด ) )
22 21 adantr โŠข ( ( ( ๐ด โˆˆ P โˆง ๐‘” โˆˆ ๐ด ) โˆง ๐‘ฅ โˆˆ Q ) โ†’ ( ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ ๐‘” ) <Q ๐‘” โ†’ ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ ๐‘” ) โˆˆ ๐ด ) )
23 20 22 sylbid โŠข ( ( ( ๐ด โˆˆ P โˆง ๐‘” โˆˆ ๐ด ) โˆง ๐‘ฅ โˆˆ Q ) โ†’ ( ๐‘ฅ <Q ( ๐‘” +Q โ„Ž ) โ†’ ( ( ๐‘ฅ ยทQ ( *Q โ€˜ ( ๐‘” +Q โ„Ž ) ) ) ยทQ ๐‘” ) โˆˆ ๐ด ) )